Theory Topological_Group

✐‹creator "Niklas Krofta"›
section ‹General theory of Topological Groups›
theory Topological_Group
  imports 
    "HOL-Algebra.Group" 
    "HOL-Algebra.Coset"
    "HOL-Analysis.Abstract_Topology" 
    "HOL-Analysis.Product_Topology" 
    "HOL-Analysis.T1_Spaces"
    "HOL-Analysis.Abstract_Metric_Spaces"
     Uniform_Structure 
begin

paragraph ‹Summary›
text ‹
  In this section we define topological groups and prove basic results about them.
  We also introduce the left and right uniform structures of topological groups and
  prove the Birkhoff-Kakutani theorem.
›

subsection ‹Auxiliary definitions and results›
subsubsection ‹Miscellaneous›

lemma connected_components_homeo:
  assumes homeo: "homeomorphic_map T1 T2 φ" and in_space: "x ∈ topspace T1"
  shows "φ`(connected_component_of_set T1 x) = connected_component_of_set T2 (φ x)"
proof
  let ?Z = connected_component_of_set
  show "φ`(?Z T1 x) ⊆ ?Z T2 (φ x)"
    by (metis connected_component_of_eq connected_component_of_maximal connectedin_connected_component_of homeo homeomorphic_map_connectedness_eq imageI in_space mem_Collect_eq)
next
  let ?Z = connected_component_of_set
  from homeo obtain ψ where ψ_homeo: "homeomorphic_map T2 T1 ψ"
    and ψ_inv: "(∀y ∈ topspace T1. ψ (φ y) = y) ∧ (∀y ∈ topspace T2. φ (ψ y) = y)"
    by (smt (verit) homeomorphic_map_maps homeomorphic_maps_map)
  from homeo in_space have "φ x ∈ topspace T2"
    using homeomorphic_imp_surjective_map by blast
  then have "ψ`(?Z T2 (φ x)) ⊆ ?Z T1 (ψ (φ x))"
    by (metis connected_component_of_eq connected_component_of_maximal connectedin_connected_component_of ψ_homeo homeomorphic_map_connectedness_eq imageI mem_Collect_eq)
  then show "?Z T2 (φ x) ⊆ φ`(?Z T1 x)"
    by (smt (verit, del_insts) ψ_inv connected_component_of_subset_topspace image_subset_iff in_space subsetD subsetI)
qed

lemma open_map_prod_top:
  assumes "open_map T1 T3 f" and "open_map T2 T4 g"
  shows "open_map (prod_topology T1 T2) (prod_topology T3 T4) (λ(x, y). (f x, g y))"
proof (unfold open_map_def, standard, standard)
  let ?p = "λ(x, y). (f x, g y)"
  fix U assume "openin (prod_topology T1 T2) U"
  then obtain 𝒰 where h𝒰: "𝒰 ⊆ {V × W | V W. openin T1 V ∧ openin T2 W} ∧ ⋃ 𝒰 = U"
    unfolding openin_prod_topology union_of_def using arbitrary_def by auto
  then have "?p`U = ⋃ {?p`VW | VW. VW ∈ 𝒰}" by blast
  then have "?p`U = ⋃ {?p`(V × W) | V W. V × W ∈ 𝒰 ∧ openin T1 V ∧ openin T2 W}" 
    using h𝒰 by blast
  moreover have "?p`(V × W) = (f`V) × (g`W)" for V W by fast
  ultimately have "?p`U = ⋃ {(f`V) × (g`W) | V W. V × W ∈ 𝒰 ∧ openin T1 V ∧ openin T2 W}" by presburger
  moreover have "openin (prod_topology T3 T4) ((f`V) × (g`W))" if "openin T1 V ∧ openin T2 W" for V W
    using openin_prod_Times_iff assms that open_map_def by metis
  ultimately show "openin (prod_topology T3 T4) (?p`U)" by fastforce
qed

lemma injective_quotient_map_homeo:
  assumes "quotient_map T1 T2 q" and inj: "inj_on q (topspace T1)"
  shows "homeomorphic_map T1 T2 q" using assms
    unfolding homeomorphic_eq_everything_map injective_quotient_map[OF inj] by fast

lemma (in group) subgroupI_alt:
  assumes subset: "H ⊆ carrier G" and nonempty: "H ≠ {}" and 
    closed: "⋀σ τ. σ ∈ H ∧ τ ∈ H ⟹ σ ⊗ inv τ ∈ H"
  shows "subgroup H G"
proof -
  from nonempty obtain η where "η ∈ H" by blast
  then have "𝟭 ∈ H" using closed[of η η] subset r_inv by fastforce
  then have closed_inv: "inv σ ∈ H" if "σ ∈ H" for σ
    using closed[of 𝟭 σ] r_inv r_one subset that by force
  then have "σ ⊗ τ ∈ H" if "σ ∈ H ∧ τ ∈ H" for σ τ
    using closed[of σ "inv τ"] inv_inv subset subset_iff that by auto
  then show ?thesis using assms closed_inv by (auto intro: subgroupI)
qed

lemma subgroup_intersection: 
  assumes "subgroup H G" and "subgroup H' G"
  shows "subgroup (H ∩ H') G"
  using assms unfolding subgroup_def by force

subsubsection ‹Quotient topology›

definition quot_topology :: "'a topology ⇒ ('a ⇒ 'b) ⇒ 'b topology" where
"quot_topology T q = topology (λU. U ⊆ q`(topspace T) ∧ openin T {x ∈ topspace T. q x ∈ U})"

lemma quot_topology_open:
  fixes T :: "'a topology" and q :: "'a ⇒ 'b"
  defines "openin_quot U ≡ U ⊆ q`(topspace T) ∧ openin T {x ∈ topspace T. q x ∈ U}"
  shows "openin (quot_topology T q) = openin_quot"
proof -
  have "istopology openin_quot"
  proof -
    have "openin_quot (U1 ∩ U2)" if "openin_quot U1 ∧ openin_quot U2" for U1 U2
    proof -
      have "{x ∈ topspace T. q x ∈ U1 ∩ U2} = {x ∈ topspace T. q x ∈ U1} ∩ {x ∈ topspace T. q x ∈ U2}" by blast
      then show ?thesis using that unfolding openin_quot_def by auto
    qed
    moreover have "openin_quot (⋃ 𝒰)" if "∀U∈𝒰. openin_quot U" for 𝒰
    proof -
      have "{x ∈ topspace T. q x ∈ ⋃ 𝒰} = ⋃ {{x ∈ topspace T. q x ∈ U} | U. U ∈ 𝒰}" by blast
      then show ?thesis using that unfolding openin_quot_def by auto
    qed
    ultimately show ?thesis using istopology_def
      by (smt (verit) Collect_cong Sup_set_def UnionI Union_iff image_eqI mem_Collect_eq mem_Collect_eq openin_topspace subsetI subset_antisym topspace_def)
  qed
  from topology_inverse'[OF this] show ?thesis using quot_topology_def unfolding openin_quot_def by metis
qed

lemma projection_quotient_map: "quotient_map T (quot_topology T q) q" 
proof (unfold quotient_map_def, intro conjI)
  have "openin (quot_topology T q) (q ` topspace T)" using quot_topology_open
    by (smt (verit) image_subset_iff mem_Collect_eq openin_subtopology_refl subsetI subtopology_superset)
  then show "q ` topspace T = topspace (quot_topology T q)" using quot_topology_open
    by (metis (no_types, opaque_lifting) openin_subset openin_topspace subset_antisym)
next
  show "∀U ⊆ topspace (quot_topology T q).
       openin T {x ∈ topspace T. q x ∈ U} = openin (quot_topology T q) U"
    using quot_topology_open by (metis (mono_tags, lifting) openin_topspace order_trans)
qed

corollary topspace_quot_topology [simp]: "topspace (quot_topology T q) = q`(topspace T)"
  using projection_quotient_map quotient_imp_surjective_map by metis

corollary projection_continuous: "continuous_map T (quot_topology T q) q"
  using projection_quotient_map quotient_imp_continuous_map by fast

subsection ‹Definition and basic results›

locale topological_group = group +
  fixes T :: "'g topology"
  assumes group_is_space [simp]: "topspace T = carrier G"
  assumes inv_continuous: "continuous_map T T (λσ. inv σ)"
  assumes mul_continuous: "continuous_map (prod_topology T T) T (λ(σ,τ). σ⊗τ)"
begin

lemma in_space_iff_in_group [iff]: "σ ∈ topspace T ⟷ σ ∈ carrier G" 
  by auto

lemma translations_continuous [intro]:
  assumes in_group: "σ ∈ carrier G"
  shows "continuous_map T T (λτ. σ⊗τ)" and "continuous_map T T (λτ. τ⊗σ)"
proof -
  have "continuous_map T (prod_topology T T) (λτ. (σ,τ))"
    by (auto intro: continuous_map_pairedI simp: in_group)
  moreover have "(λτ. σ⊗τ) = (λ(σ,τ). σ⊗τ) ∘ (λτ. (σ,τ))" by auto
  ultimately show "continuous_map T T (λτ. σ⊗τ)"
    using mul_continuous continuous_map_compose by metis
next
  have "continuous_map T (prod_topology T T) (λτ. (τ,σ))"
    by (auto intro: continuous_map_pairedI simp: in_group)
  moreover have "(λτ. τ⊗σ) = (λ(σ,τ). σ⊗τ) ∘ (λτ. (τ,σ))" by auto
  ultimately show "continuous_map T T (λτ. τ⊗σ)"
    using mul_continuous continuous_map_compose by metis
qed

lemma translations_homeos:
  assumes in_group: "σ ∈ carrier G"
  shows "homeomorphic_map T T (λτ. σ⊗τ)" and "homeomorphic_map T T (λτ. τ⊗σ)"
proof -
  have "∀τ∈topspace T. inv σ ⊗ (σ ⊗ τ) = τ" by (simp add: group.inv_solve_left' in_group)
  moreover have "∀τ∈topspace T. σ ⊗ (inv σ ⊗ τ) = τ"
    by (metis group_is_space in_group inv_closed l_one m_assoc r_inv)
  ultimately have "homeomorphic_maps T T (λτ. σ⊗τ) (λτ. (inv σ)⊗τ)"
    using homeomorphic_maps_def in_group by blast
  then show "homeomorphic_map T T (λτ. σ⊗τ)" using homeomorphic_maps_map by blast
next
  have "∀τ∈topspace T. τ ⊗ σ ⊗ inv σ = τ"
    by (simp add: group.inv_solve_right' in_group)
  moreover have "∀τ∈topspace T. τ ⊗ inv σ ⊗ σ = τ" by (simp add: in_group m_assoc)
  ultimately have "homeomorphic_maps T T (λτ. τ⊗σ) (λτ. τ⊗(inv σ))"
    using homeomorphic_maps_def in_group by blast
  then show "homeomorphic_map T T (λτ. τ⊗σ)" using homeomorphic_maps_map by blast
qed

abbreviation conjugation :: "'g ⇒ 'g ⇒ 'g" where
"conjugation σ τ ≡ σ ⊗ τ ⊗ inv σ"

corollary conjugation_homeo:
  assumes in_group: "σ ∈ carrier G"
  shows "homeomorphic_map T T (conjugation σ)"
proof -
  have "conjugation σ = (λτ. τ ⊗ inv σ) ∘ (λτ. σ ⊗ τ)" by auto
  then show ?thesis using translations_homeos homeomorphic_map_compose
    by (metis in_group inv_closed)
qed

corollary open_set_translations:
  assumes open_set: "openin T U" and in_group: "σ ∈ carrier G"
  shows "openin T (σ <# U)" and "openin T (U #> σ)"
proof -
  let ?φ = "λτ. σ ⊗ τ"
  have "σ <# U = ?φ`U" unfolding l_coset_def by blast
  then show "openin T (σ <# U)" using translations_homeos[OF in_group]
    by (metis homeomorphic_map_openness_eq open_set)
next
  let ?ψ = "λτ. τ ⊗ σ"
  have "U #> σ = ?ψ`U" unfolding r_coset_def by fast
  then show "openin T (U #> σ)" using translations_homeos[OF in_group]
    by (metis homeomorphic_map_openness_eq open_set)
qed

corollary closed_set_translations:
  assumes closed_set: "closedin T U" and in_group: "σ ∈ carrier G"
  shows "closedin T (σ <# U)" and "closedin T (U #> σ)"
proof -
  let ?φ = "λτ. σ⊗τ"
  have "σ <# U = ?φ`U" unfolding l_coset_def by fast
  then show "closedin T (σ <# U)" using translations_homeos[OF in_group]
    by (metis homeomorphic_map_closedness_eq closed_set)
next
  let ?ψ = "λτ. τ⊗σ"
  have "U #> σ = ?ψ`U" unfolding r_coset_def by fast
  then show "closedin T (U #> σ)" using translations_homeos[OF in_group]
    by (metis homeomorphic_map_closedness_eq closed_set)
qed

lemma inverse_homeo: "homeomorphic_map T T (λσ. inv σ)"
  using homeomorphic_map_involution[OF inv_continuous] by auto

subsection ‹Subspaces and quotient spaces›

abbreviation connected_component_1 :: "'g set" where
"connected_component_1 ≡ connected_component_of_set T 𝟭"

lemma connected_component_1_props: 
  shows "connected_component_1 ⊲ G" and "closedin T connected_component_1"
proof -
  let ?Z = "connected_component_of_set T"
  have in_space: "(?Z 𝟭) ⊆ topspace T"
    using connected_component_of_subset_topspace by fastforce
  have "subgroup (?Z 𝟭) G"
  proof (rule subgroupI)
    show "(?Z 𝟭) ⊆ carrier G" using in_space by auto
  next
    show "(?Z 𝟭) ≠ {}"
      by (metis connected_component_of_eq_empty group_is_space one_closed)
  next
    fix σ assume hσ: "σ ∈ (?Z 𝟭)"
    let ?φ = "λη. inv η"
    have "?φ`(?Z 𝟭) = ?Z 𝟭" using connected_components_homeo
      by (metis group_is_space inv_one inverse_homeo one_closed)
    then show "inv σ ∈ (?Z 𝟭)" using hσ by blast
  next
    fix σ τ assume hσ: "σ ∈ (?Z 𝟭)" and hτ: "τ ∈ (?Z 𝟭)"
    let ?φ = "λη. σ ⊗ η"
    have "?φ`(?Z 𝟭) = ?Z σ" using connected_components_homeo
      by (metis group_is_space hσ in_space one_closed r_one subset_eq translations_homeos(1))
    moreover have "?Z σ = ?Z 𝟭" using hσ by (simp add: connected_component_of_equiv)
    ultimately show "σ ⊗ τ ∈ ?Z 𝟭" using hτ by blast
  qed
  moreover have "conjugation σ τ ∈ ?Z 𝟭" if hστ: "σ ∈ carrier G ∧ τ ∈ ?Z 𝟭" for σ τ
  proof -
    let ?φ = "conjugation σ"
    have "?φ`(?Z 𝟭) = ?Z (?φ 𝟭)" using connected_components_homeo
      by (metis conjugation_homeo group_is_space one_closed hστ)
    then show ?thesis using r_inv r_one hστ by auto
  qed
  ultimately show "connected_component_1 ⊲ G" using normal_inv_iff by blast
next
  show "closedin T connected_component_1" by (simp add: closedin_connected_component_of)
qed

lemma group_prod_space [simp]: "topspace (prod_topology T T) = (carrier G) × (carrier G)"
  by auto

no_notation eq_closure_of (‹closure'_ofı›)

lemma subgroup_closure:
  assumes H_subgroup: "subgroup H G"
  shows "subgroup (T closure_of H) G"
proof -
  have subset: "T closure_of H ⊆ carrier G"
    by (metis closedin_closure_of closedin_subset group_is_space)
  have nonempty: "T closure_of H ≠ {}"
    by (simp add: assms closure_of_eq_empty group.subgroupE(1) subgroupE(2))
  
  let ?φ = "λ(σ,τ). σ ⊗ inv τ"
  have φ_continuous: "continuous_map (prod_topology T T) T ?φ"
  proof -
    have "continuous_map (prod_topology T T) (prod_topology T T) (λ(σ, τ). (σ, inv τ))"
      using continuous_map_prod_top inv_continuous by fastforce
    moreover have "?φ = (λ(σ, τ). σ ⊗ τ) ∘ (λ(σ, τ). (σ, inv τ))" by fastforce
    ultimately show ?thesis using mul_continuous continuous_map_compose by force
  qed

  have "σ ⊗ inv τ ∈ T closure_of H" 
    if hστ: "σ ∈ T closure_of H ∧ τ ∈ T closure_of H" for σ τ
  proof -
    have in_space: "σ ⊗ inv τ ∈ topspace T" using subset hστ by fast
    have "∃η ∈ H. η ∈ U" if hU: "openin T U ∧ σ ⊗ inv τ ∈ U" for U
    proof -
      let ?V = "{x ∈ topspace (prod_topology T T). ?φ x ∈ U}"
      have "openin (prod_topology T T) ?V" 
        using φ_continuous hU openin_continuous_map_preimage by blast
      moreover have "(σ,τ) ∈ ?V"
        using hU group_prod_space hστ subset by force
      ultimately obtain V1 V2 where 
        hV1V2: "openin T V1 ∧ openin T V2 ∧ σ ∈ V1 ∧ τ ∈ V2 ∧ V1 × V2 ⊆ ?V"
        by (smt (verit) openin_prod_topology_alt) 
      then obtain σ' τ' where hσ'τ': "σ' ∈ V1 ∩ H ∧ τ' ∈ V2 ∩ H" using hστ
        by (meson all_not_in_conv disjoint_iff openin_Int_closure_of_eq_empty)
      then have "?φ (σ',τ') ∈ U" using hV1V2 by blast
      moreover have "?φ (σ',τ') ∈ H" using hσ'τ' H_subgroup subgroupE(3,4) by simp
      ultimately show ?thesis by blast
    qed
    then show ?thesis using closure_of_def in_space by force
  qed
  then show ?thesis using subgroupI_alt subset nonempty by blast
qed

lemma normal_subgroup_closure:
  assumes normal_subgroup: "N ⊲ G"
  shows "(T closure_of N) ⊲ G"
proof -
  have "(conjugation σ)`(T closure_of N) ⊆ T closure_of N" if hσ: "σ ∈ carrier G" for σ 
  proof -
    have "(conjugation σ)`N ⊆ N" using normal_subgroup normal_invE(2) hσ by auto
    then have "T closure_of (conjugation σ)`N ⊆ T closure_of N" 
      using closure_of_mono by meson
    moreover have "(conjugation σ)`(T closure_of N) ⊆ T closure_of (conjugation σ)`N"
      using hσ conjugation_homeo
      by (meson continuous_map_eq_image_closure_subset homeomorphic_imp_continuous_map)
    ultimately show ?thesis by blast
  qed
  moreover have "subgroup (T closure_of N) G" using subgroup_closure
    by (simp add: normal_invE(1) normal_subgroup)
  ultimately show ?thesis using normal_inv_iff by auto
qed

lemma topological_subgroup:
  assumes "subgroup H G"
  shows "topological_group (G ⦇carrier := H⦈) (subtopology T H)"
proof -
  interpret subgroup H G by fact
  let ?ℋ = "(G ⦇carrier := H⦈)" and ?T' = "subtopology T H"
  have H_subspace: "topspace ?T' = H" using topspace_subtopology_subset by force
  have "continuous_map ?T' T (λσ. inv σ)" using continuous_map_from_subtopology inv_continuous by blast
  moreover have "(λσ. inv σ) ∈ topspace ?T' → H" unfolding Pi_def H_subspace by blast
  ultimately have "continuous_map ?T' ?T' (λσ. inv σ)" using continuous_map_into_subtopology by blast
  then have sub_inv_continuous: "continuous_map ?T' ?T' (λσ. inv⇘?ℋ⇙ σ)"
    using continuous_map_eq H_subspace m_inv_consistent assms by fastforce
  have "continuous_map (prod_topology ?T' ?T') T (λ(σ,τ). σ ⊗ τ)" 
    unfolding subtopology_Times[symmetric] using continuous_map_from_subtopology[OF mul_continuous] by fast
  moreover have "(λ(σ,τ). σ ⊗ τ) ∈ topspace (prod_topology ?T' ?T') → H" 
    unfolding Pi_def topspace_prod_topology H_subspace by fast
  ultimately have "continuous_map (prod_topology ?T' ?T') ?T' (λ(σ,τ). σ ⊗ τ)"
    using continuous_map_into_subtopology by blast
  then have "continuous_map (prod_topology ?T' ?T') ?T' (λ(σ,τ). σ ⊗⇘?ℋ⇙ τ)" by fastforce
  then show ?thesis unfolding topological_group_def topological_group_axioms_def using H_subspace sub_inv_continuous by auto
qed

text ‹Topology on the set of cosets of some subgroup›

abbreviation coset_topology :: "'g set ⇒ 'g set topology" where
"coset_topology H ≡ quot_topology T (r_coset G H)"

lemma coset_topology_topspace[simp]:
  shows "topspace (coset_topology H) = (r_coset G H)`(carrier G)"
  using projection_quotient_map quotient_imp_surjective_map group_is_space by metis

lemma projection_open_map:
  assumes subgroup: "subgroup H G"
  shows "open_map T (coset_topology H) (r_coset G H)"
proof (unfold open_map_def, standard, standard)
  fix U assume hU: "openin T U"
  let ?π = "r_coset G H"
  let ?V = "{σ ∈ topspace T. ?π σ ∈ ?π`U}"
  have subsets: "H ⊆ carrier G ∧ U ⊆ carrier G"
    using subgroup hU  openin_subset by (force elim!: subgroupE)
  have "?V = {σ ∈ carrier G. ∃τ ∈ U. H #> σ = H #> τ}" using image_def by blast 
  then have "?V = {σ ∈ carrier G. ∃τ ∈ U. σ ∈ H #> τ}" using subsets 
    by (smt (verit) Collect_cong rcos_self repr_independence subgroup subset_eq)
  also have "... = (⋃η ∈ H. η <# U)" unfolding r_coset_def l_coset_def using subsets by auto
  moreover have "openin T (η <# U)" if "η ∈ H" for η
    using open_set_translations(1)[OF hU] subsets that by blast
  ultimately have "openin T ?V" by fastforce
  then show "openin (coset_topology H) (?π`U)" using quot_topology_open hU
    by (metis (mono_tags, lifting) Collect_cong image_mono openin_subset)
qed

lemma topological_quotient_group:
  assumes normal_subgroup: "N ⊲ G"
  shows "topological_group (G Mod N) (coset_topology N)"
proof -
  interpret normal N G by fact
  let ?π = "r_coset G N"
  let ?T' = "coset_topology N"
  have quot_space: "topspace ?T' = ?π`(carrier G)" using coset_topology_topspace by presburger
  then have quot_group_quot_space: "topspace ?T' = carrier (G Mod N)" using carrier_FactGroup by metis

  let ?quot_mul = "λ(Nσ, Nτ). Nσ ⊗⇘G Mod N⇙ Nτ"
  have π_prod_space: "topspace (prod_topology ?T' ?T') = ?π`(carrier G) × ?π`(carrier G)"
    using quot_space topspace_prod_topology by simp
  have quot_mul_continuous: "continuous_map (prod_topology ?T' ?T') ?T' ?quot_mul"
  proof (unfold continuous_map_def, intro conjI ballI allI impI)
    show "?quot_mul ∈ topspace (prod_topology ?T' ?T') → topspace ?T'" 
      using rcos_sum unfolding quot_space π_prod_space by auto
  next
    fix U assume hU: "openin ?T' U"
    let ?V = "{p ∈ topspace (prod_topology ?T' ?T'). ?quot_mul p ∈ U}"
    let ?W = "{(σ,τ) ∈ topspace (prod_topology T T). N #> (σ ⊗ τ) ∈ U}"
    let ?π2 = "λ(σ, τ). (N #> σ, N #> τ)"
    have "(λ(σ,τ). N #> (σ ⊗ τ)) = ?π ∘ (λ(σ,τ). σ ⊗ τ)" by fastforce
    then have "continuous_map (prod_topology T T) ?T' (λ(σ,τ). N #> (σ ⊗ τ))"
      using continuous_map_compose mul_continuous projection_continuous by fastforce
    then have "openin (prod_topology T T) ?W"
      using hU openin_continuous_map_preimage
      by (smt (verit) Collect_cong case_prodE case_prodI2 case_prod_conv)
    moreover have "open_map (prod_topology T T) (prod_topology ?T' ?T') ?π2"
      using projection_open_map open_map_prod_top by (metis subgroup_axioms)
    ultimately have "openin (prod_topology ?T' ?T') (?π2`?W)" using open_map_def by blast
    moreover have "?V = ?π2`?W"
      using rcos_sum unfolding π_prod_space group_prod_space by auto
    ultimately show "openin (prod_topology ?T' ?T') ?V" by presburger
  qed

  let ?quot_inv = "λNσ. inv⇘G Mod N⇙ Nσ"
  have π_inv: "?quot_inv (N #> σ) = ?π (inv σ)" if "σ ∈ carrier G" for σ 
    using inv_FactGroup rcos_inv carrier_FactGroup that by blast 
  have "continuous_map ?T' ?T' ?quot_inv"
  proof (unfold continuous_map_def, intro conjI ballI allI impI)
    show "?quot_inv ∈ topspace ?T' → topspace ?T'" using π_inv quot_space by auto
  next
    fix U assume hU: "openin ?T' U"
    let ?V = "{Nσ ∈ topspace ?T'. ?quot_inv Nσ ∈ U}"
    let ?W = "{σ ∈ topspace T. N #> (inv σ) ∈ U}"
    have "(λσ. N #> (inv σ)) = ?π ∘ (λσ. inv σ)" by fastforce
    then have "continuous_map T ?T' (λσ. N #> (inv σ))"
      using continuous_map_compose projection_continuous inv_continuous 
      by (metis (no_types, lifting)) 
    then have "openin T ?W" using hU openin_continuous_map_preimage by blast
    then have "openin ?T' (?π`?W)" 
      using projection_open_map by (simp add: open_map_def subgroup_axioms)
    moreover have "?V = ?π`?W" using π_inv quot_space by force
    ultimately show "openin ?T' ?V" by presburger
  qed

  then show ?thesis unfolding topological_group_def topological_group_axioms_def
    using quot_group_quot_space quot_mul_continuous factorgroup_is_group by blast
qed

text ‹
  See cite‹"stackexchange_quot_groups"› for our approach to proving that quotient groups
  of topological groups are topological.
›

abbreviation neighborhood :: "'g ⇒ 'g set ⇒ bool" where
"neighborhood σ U ≡ openin T U ∧ σ ∈ U"

abbreviation symmetric :: "'g set ⇒ bool" where
"symmetric S ≡ {inv σ | σ. σ ∈ S} ⊆ S"

text 
  ‹Note that this implies the other inclusion, so symmetric subsets are equal to their 
  image under inversion.
›

lemma neighborhoods_of_1:
  assumes "neighborhood 𝟭 U"
  shows "∃V. neighborhood 𝟭 V ∧ symmetric V ∧ V <#> V ⊆ U"
proof -
  have a: "∃V⊆U'. neighborhood 𝟭 V ∧ symmetric V" if hU': "neighborhood 𝟭 U'" for U'
  proof -
    let ?W = "{σ ∈ carrier G. inv σ ∈ U'}"
    let ?V = "?W ∩ ((λσ. inv σ)`?W)"
    have "neighborhood 𝟭 ?W" using openin_continuous_map_preimage[OF inv_continuous]
        hU' inv_one by fastforce
    moreover from this have "neighborhood 𝟭 ((λσ. inv σ)`?W)" using inverse_homeo 
        homeomorphic_imp_open_map inv_one image_eqI open_map_def by (metis (mono_tags, lifting))
    ultimately have neighborhood: "neighborhood 𝟭 ?V" by blast
    have "inv σ ∈ ?V" if "σ ∈ ?V" for σ using that by auto
    then have "symmetric ?V" by fast
    moreover have "σ ∈ U'" if "σ ∈ ?V" for σ using that by blast
    ultimately show ?thesis using neighborhood by blast
  qed
  have b: "∃V. neighborhood 𝟭 V ∧ V <#> V ⊆ U'" if hU': "neighborhood 𝟭 U'" for U' 
  proof -
    let ?W = "{(σ,τ) ∈ carrier G × carrier G. σ⊗τ ∈ U'}"
    have preimage_mul: "?W = {x ∈ topspace (prod_topology T T). (λ(σ,τ). σ⊗τ) x ∈ U'}"
      using topspace_prod_topology by fastforce
    then have "openin (prod_topology T T) ?W ∧ (𝟭,𝟭) ∈ ?W" 
      using openin_continuous_map_preimage[OF mul_continuous] hU' r_one by fastforce
    then obtain W1 W2 where hW1W2: "neighborhood 𝟭 W1 ∧ neighborhood 𝟭 W2 ∧ W1×W2⊆?W"
      using openin_prod_topology_alt[where S="?W"] by meson
    let ?V = "W1 ∩ W2"
    from hW1W2 have "neighborhood 𝟭 ?V" by fast
    moreover have "σ⊗τ ∈ U'" if "σ∈?V ∧ τ∈?V" for σ τ using preimage_mul hW1W2 that by blast
    ultimately show ?thesis unfolding set_mult_def by blast
  qed
  from b[OF assms] obtain W where hW: "neighborhood 𝟭 W ∧ W <#> W ⊆ U" by presburger
  from this a obtain V where "V⊆W ∧ neighborhood 𝟭 V ∧ symmetric V" by presburger
  moreover from this have "V <#> V ⊆ U" using hW mono_set_mult by blast
  ultimately show ?thesis unfolding set_mult_def by blast
qed

lemma Hausdorff_coset_space:
  assumes subgroup: "subgroup H G" and H_closed: "closedin T H"
  shows "Hausdorff_space (coset_topology H)"
proof (unfold Hausdorff_space_def, intro allI impI)
  interpret subgroup H G by fact
  let ?π = "r_coset G H"
  let ?T' = "coset_topology H"
  fix Hσ Hτ assume cosets: "Hσ ∈ topspace ?T' ∧ Hτ ∈ topspace ?T' ∧ Hσ ≠ Hτ"
  then obtain σ τ where hστ: "σ ∈ carrier G ∧ τ ∈ carrier G ∧ Hσ = H #> σ ∧ Hτ = H #> τ" by auto
  then have "σ ∉ H #> τ" using cosets subgroup repr_independence by blast
  have "𝟭 ∉ (inv σ) <# (H #> τ)" 
  proof
    assume "𝟭 ∈ inv σ <# (H #> τ)"
    then obtain η where hη: "η ∈ H ∧ 𝟭 = (inv σ) ⊗ (η ⊗ τ)" unfolding r_coset_def l_coset_def by auto
    then have "σ = η ⊗ τ"
      by (metis (no_types, lifting) Units_eq Units_m_closed group.inv_comm group_l_invI hστ inv_closed inv_inv inv_unique' l_inv_ex mem_carrier)
    then show "False" using ‹σ ∉ H #> τ› hη r_coset_def by fast
  qed
  let ?U = "topspace T - ((inv σ) <# (H #> τ))"
  have "closedin T ((inv σ) <# (H #> τ))" 
      using closed_set_translations closed_set_translations[OF H_closed] hστ by simp
  then have "neighborhood 𝟭 ?U" using ‹𝟭 ∉ (inv σ) <# (H #> τ)› by blast
  then obtain V where hV: "neighborhood 𝟭 V ∧ symmetric V ∧ V <#> V ⊆ ?U"
    using neighborhoods_of_1 by presburger
  let ?V1 = "σ <# V" and ?V2 = "τ <# V"
  have disjoint: "?π`?V1 ∩ ?π`?V2 = {}"
  proof (rule ccontr)
    assume "?π`?V1 ∩ ?π`?V2 ≠ {}"
    then obtain υ1 υ2 where hυ1υ2: "υ1 ∈ V ∧ υ2 ∈ V ∧ ?π (σ⊗υ1) = ?π (τ⊗υ2)" 
      unfolding l_coset_def by auto
    moreover then have υ1υ2_in_group: "υ1 ∈ carrier G ∧ υ2 ∈ carrier G" 
      using hV openin_subset by force
    ultimately have in_H: "(σ⊗υ1) ⊗ inv (τ⊗υ2) ∈ H" 
      using subgroup repr_independenceD rcos_module_imp hστ m_closed 
      by (metis group.rcos_self is_group subgroup.m_closed subgroup_self)
    let ?η = "(σ⊗υ1) ⊗ inv (τ⊗υ2)"
    have "?η = σ ⊗ (υ1 ⊗ inv υ2) ⊗ inv τ" using hστ υ1υ2_in_group m_assoc
      by (simp add: inv_mult_group subgroupE(4) subgroup_self)
    then have "inv σ ⊗ (?η ⊗ τ) = υ1 ⊗ inv υ2" 
      using hστ υ1υ2_in_group m_assoc inv_solve_left' by auto
    then have "υ1 ⊗ inv υ2 ∈ (inv σ) <# (H #> τ)" 
      unfolding l_coset_def r_coset_def using hστ inv_closed in_H by force
    moreover have "υ1 ⊗ inv υ2 ∈ ?U" using hυ1υ2 hV unfolding set_mult_def by blast
    ultimately show "False" by force 
  qed
  have "neighborhood σ ?V1 ∧ neighborhood τ ?V2"
    using open_set_translations[of V] l_coset_def hV hστ r_one by force
  then have "openin ?T' (?π`?V1) ∧ openin ?T' (?π`?V2) ∧ Hσ ∈ ?π`?V1 ∧ Hτ ∈ ?π`?V2"
    using projection_open_map open_map_def subgroup hστ by fast
  then show "∃W1 W2. openin ?T' W1 ∧ openin ?T' W2 ∧ Hσ ∈ W1 ∧ Hτ ∈ W2 ∧ disjnt W1 W2"
    using disjoint disjnt_def by meson
qed

lemma Hausdorff_coset_space_converse:
  assumes subgroup: "subgroup H G"
  assumes Hausdorff: "Hausdorff_space (coset_topology H)"
  shows "closedin T H"
proof -
  interpret subgroup H G by fact
  let ?T' = "coset_topology H"
  have "H ∈ topspace ?T'" using coset_topology_topspace coset_join2[of 𝟭 H] subgroup by auto
  then have "closedin ?T' {H}" 
    using t1_space_closedin_singleton Hausdorff_imp_t1_space[OF Hausdorff] by fast
  then have preimage_closed: "closedin T {σ ∈ carrier G. H #> σ = H}" 
    using projection_continuous closedin_continuous_map_preimage by fastforce
  have "σ ∈ H ⟷ H #> σ = H" if "σ ∈ carrier G" for σ
    using coset_join1 coset_join2 subgroup that by metis
  then have "H = {σ ∈ carrier G. H #> σ = H}" using subset by auto
  then show ?thesis using preimage_closed by presburger
qed

corollary Hausdorff_coset_space_iff:
  assumes subgroup: "subgroup H G"
  shows "Hausdorff_space (coset_topology H) ⟷ closedin T H"
  using Hausdorff_coset_space Hausdorff_coset_space_converse subgroup by blast

corollary topological_group_hausdorff_iff_one_closed:
  shows "Hausdorff_space T ⟷ closedin T {𝟭}"
proof -
  let ?π = "r_coset G {𝟭}"
  have "inj_on ?π (carrier G)" unfolding inj_on_def r_coset_def by simp
  then have "homeomorphic_map T (coset_topology {𝟭}) ?π"
    using projection_quotient_map injective_quotient_map_homeo group_is_space by metis
  then have "Hausdorff_space T ⟷ Hausdorff_space (coset_topology {𝟭})" 
    using homeomorphic_Hausdorff_space homeomorphic_map_imp_homeomorphic_space by blast
  then show ?thesis using Hausdorff_coset_space_iff triv_subgroup by blast
qed

lemma set_mult_one_subset:
  assumes "A ⊆ carrier G ∧ B ⊆ carrier G" and "𝟭 ∈ B"
  shows "A ⊆ A <#> B" 
  unfolding set_mult_def using assms r_one by force

lemma open_set_mult_open:
  assumes "openin T U ∧ S ⊆ carrier G"
  shows "openin T (S <#> U)"
proof -
  have "S <#> U = (⋃σ∈S. σ <# U)" unfolding set_mult_def l_coset_def by blast
  moreover have "openin T (σ <# U)" if "σ ∈ S" for σ using open_set_translations(1) assms that by auto
  ultimately show ?thesis by auto
qed

lemma open_set_inv_open:
  assumes "openin T U"
  shows "openin T (set_inv U)"
proof -
  have "set_inv U = (λσ. inv σ)`U" unfolding image_def SET_INV_def by blast
  then show ?thesis using inverse_homeo homeomorphic_imp_open_map open_map_def assms by metis
qed

lemma open_set_in_carrier[elim]:
  assumes "openin T U"
  shows "U ⊆ carrier G"
  using openin_subset assms by force

subsection ‹Uniform structures›

abbreviation left_entourage :: "'g set ⇒ ('g × 'g) set" where
"left_entourage U ≡ {(σ,τ) ∈ carrier G × carrier G. inv σ ⊗ τ ∈ U}"

abbreviation right_entourage :: "'g set ⇒ ('g × 'g) set" where
"right_entourage U ≡ {(σ,τ) ∈ carrier G × carrier G. σ ⊗ inv τ ∈ U}"

definition left_uniformity :: "'g uniformity" where "left_uniformity =
  uniformity (carrier G, λE. E ⊆ carrier G × carrier G ∧ (∃U. neighborhood 𝟭 U ∧ left_entourage U ⊆ E))"

definition right_uniformity :: "'g uniformity" where "right_uniformity =
  uniformity (carrier G, λE. E ⊆ carrier G × carrier G ∧ (∃U. neighborhood 𝟭 U ∧ right_entourage U ⊆ E))"

lemma
  uspace_left_uniformity[simp]: "uspace left_uniformity = carrier G" (is ?space_def) and
  entourage_left_uniformity: "entourage_in left_uniformity = 
    (λE. E ⊆ carrier G × carrier G ∧ (∃U. neighborhood 𝟭 U ∧ left_entourage U ⊆ E))" (is ?entourage_def)
proof -
  let ?Φ = "λE. E ⊆ carrier G × carrier G ∧ (∃U. neighborhood 𝟭 U ∧ left_entourage U ⊆ E)"
  have "?Φ (carrier G × carrier G)" 
    using exI[where x="carrier G"] openin_topspace by force
  moreover have "Id_on (carrier G) ⊆ E ∧ ?Φ (E¯) ∧ (∃F. ?Φ F ∧ F O F ⊆ E) ∧ 
    (∀F. E ⊆ F ∧ F ⊆ carrier G × carrier G ⟶ ?Φ F)" if hE: "?Φ E" for E
  proof -
    from hE obtain U where hU: "neighborhood 𝟭 U ∧ left_entourage U ⊆ E" by presburger
    then have U_subset: "U ⊆ carrier G" using openin_subset by force
    from hU have "Id_on (carrier G) ⊆ E" by fastforce
    moreover have "?Φ (E¯)"
    proof -
      have "(τ,σ) ∈ E" if "σ ∈ carrier G ∧ τ ∈ carrier G ∧ inv σ ⊗ τ ∈ set_inv U" for σ τ
      proof -
        have "inv τ ⊗ σ = inv (inv σ ⊗ τ)" using that inv_mult_group by auto
        from this have "inv τ ⊗ σ ∈ U" using that inv_inv U_subset unfolding SET_INV_def by auto
        then show ?thesis using that hU by fast
      qed
      then have "left_entourage (set_inv U) ⊆ E¯" by blast 
      moreover have "neighborhood 𝟭 (set_inv U)" using inv_one hU open_set_inv_open SET_INV_def by fastforce
      ultimately show ?thesis using hE by auto
    qed
    moreover have "∃F. ?Φ F ∧ F O F ⊆ E"
    proof -
      obtain V where hV: "neighborhood 𝟭 V ∧ V <#> V ⊆ U"
        using neighborhoods_of_1 hU by meson
      let ?F = "left_entourage V"
      have "(σ,ρ) ∈ E" if "(σ,τ) ∈ ?F ∧ (τ,ρ) ∈ ?F" for σ τ ρ
      proof -
        have "σ ∈ carrier G ∧ τ ∈ carrier G ∧ ρ ∈ carrier G" using that by force
        then have "inv σ ⊗ ρ = (inv σ ⊗ τ) ⊗ (inv τ ⊗ ρ)"
          using m_assoc inv_closed m_closed r_inv r_one by metis  
        moreover have "(inv σ ⊗ τ) ⊗ (inv τ ⊗ ρ) ∈ U" using that hV unfolding set_mult_def by fast
        ultimately show ?thesis using hU that by force
      qed
      moreover have "?Φ ?F" using hV by blast
      ultimately show ?thesis using hV by auto
    qed
    moreover have "∀F. E ⊆ F ∧ F ⊆ carrier G × carrier G ⟶ ?Φ F" using hE by auto
    ultimately show ?thesis by blast
  qed
  moreover have "?Φ (E ∩ F)" if hEF: "?Φ E ∧ ?Φ F" for E F
  proof -
    from hEF obtain U V where
      hU: "neighborhood 𝟭 U ∧ left_entourage U ⊆ E" and
      hV: "neighborhood 𝟭 V ∧ left_entourage V ⊆ F" by presburger
    then have "neighborhood 𝟭 (U ∩ V) ∧ left_entourage (U ∩ V) ⊆ E ∩ F" by fast
    then show ?thesis using that by auto
  qed
  ultimately have "uniformity_on (carrier G) ?Φ"
    unfolding uniformity_on_def by auto
  from uniformity_inverse'[OF this] show ?space_def and ?entourage_def unfolding left_uniformity_def by auto
qed

lemma
  uspace_right_uniformity[simp]: "uspace right_uniformity = carrier G" (is ?space_def) and
  entourage_right_uniformity: "entourage_in right_uniformity =  
    (λE. E ⊆ carrier G × carrier G ∧ (∃U. neighborhood 𝟭 U ∧ right_entourage U ⊆ E))" (is ?entourage_def)
proof -
  let ?Φ = "λE. E ⊆ carrier G × carrier G ∧ (∃U. neighborhood 𝟭 U ∧ right_entourage U ⊆ E)"
  have "?Φ (carrier G × carrier G)" 
    using exI[where x="carrier G"] openin_topspace by force
  moreover have "Id_on (carrier G) ⊆ E ∧ ?Φ (E¯) ∧ (∃F. ?Φ F ∧ F O F ⊆ E) ∧ 
    (∀F. E ⊆ F ∧ F ⊆ carrier G × carrier G ⟶ ?Φ F)" if hE: "?Φ E" for E
  proof -
    from hE obtain U where 
      hU: "neighborhood 𝟭 U ∧ right_entourage U ⊆ E"
      by presburger
    then have U_subset: "U ⊆ carrier G" using openin_subset by force
    from hU have "Id_on (carrier G) ⊆ E" by fastforce
    moreover have "?Φ (E¯)"
    proof -
      have "(τ,σ) ∈ E" if "σ ∈ carrier G ∧ τ ∈ carrier G ∧ σ ⊗ inv τ ∈ set_inv U" for σ τ
      proof -
        have "τ ⊗ inv σ = inv (σ ⊗ inv τ)" using that inv_mult_group by auto
        from this have "τ ⊗ inv σ ∈ U" using that inv_inv U_subset unfolding SET_INV_def by auto
        then show ?thesis using that hU by fast
      qed
      then have "right_entourage (set_inv U) ⊆ E¯" by blast 
      moreover have "neighborhood 𝟭 (set_inv U)" using inv_one hU open_set_inv_open SET_INV_def by fastforce
      ultimately show ?thesis using hE by auto
    qed
    moreover have "∃F. ?Φ F ∧ F O F ⊆ E"
    proof -
      obtain V where hV: "neighborhood 𝟭 V ∧ V <#> V ⊆ U"
        using neighborhoods_of_1 hU by meson
      let ?F = "right_entourage V"
      have "(σ,ρ) ∈ E" if "(σ,τ) ∈ ?F ∧ (τ,ρ) ∈ ?F" for σ τ ρ
      proof -
        have "σ ∈ carrier G ∧ τ ∈ carrier G ∧ ρ ∈ carrier G" using that by force
        then have "σ ⊗ inv ρ = (σ ⊗ inv τ) ⊗ (τ ⊗ inv ρ)"
          using m_assoc inv_closed m_closed l_inv r_one by metis  
        moreover have "(σ ⊗ inv τ) ⊗ (τ ⊗ inv ρ) ∈ U" using that hV unfolding set_mult_def by fast
        ultimately show ?thesis using hU that by force
      qed
      moreover have "?Φ ?F" using hV by blast
      ultimately show ?thesis using hV by auto
    qed
    moreover have "∀F. E ⊆ F ∧ F ⊆ carrier G × carrier G ⟶ ?Φ F" using hE by auto
    ultimately show ?thesis by blast
  qed
  moreover have "?Φ (E ∩ F)" if hEF: "?Φ E ∧ ?Φ F" for E F
  proof -
    from hEF obtain U V where
      hU: "neighborhood 𝟭 U ∧ right_entourage U ⊆ E" and
      hV: "neighborhood 𝟭 V ∧ right_entourage V ⊆ F"
      by presburger
    then have "neighborhood 𝟭 (U ∩ V) ∧ right_entourage (U ∩ V) ⊆ E ∩ F" by fast
    then show ?thesis using that by auto
  qed
  ultimately have "uniformity_on (carrier G) ?Φ"
    unfolding uniformity_on_def by auto
  from uniformity_inverse'[OF this] show ?space_def and ?entourage_def unfolding right_uniformity_def by auto
qed

lemma left_uniformity_induces_group_topology [simp]:
  shows "utopology left_uniformity = T"
proof -
  let ?Φ = left_uniformity
  let ?T' = "utopology ?Φ"
  have "openin T U ⟷ openin ?T' U" for U
  proof
    assume U_open: "openin T U"
    have "∃E. entourage_in ?Φ E ∧ E``{σ} ⊆ U" if hσ: "σ ∈ U" for σ
    proof -
      let ?E = "left_entourage (inv σ <# U)"
      have in_group: "σ ∈ carrier G" using hσ U_open open_set_in_carrier by blast
      then have "openin T (inv σ <# U)"
        using inv_closed open_set_translations(1) U_open by presburger
      then have "neighborhood 𝟭 (inv σ <# U)"
        using hσ in_group r_inv unfolding l_coset_def SET_INV_def by force
      then have "entourage_in ?Φ ?E" unfolding entourage_left_uniformity by blast
      moreover have "τ ∈ U" if "τ ∈ ?E``{σ}" for τ
      proof -
        from that have "inv σ ⊗ τ ∈ inv σ <# U" by force
        then obtain ρ where hρ: "ρ ∈ U ∧ inv σ ⊗ τ = inv σ ⊗ ρ" unfolding l_coset_def by fast
        then have "ρ ∈ carrier G ∧ τ ∈ carrier G" using that open_set_in_carrier U_open by fast
        then have "τ = ρ" using in_group hρ inv_closed by (metis Units_eq Units_l_cancel)
        then show ?thesis using hρ by simp
      qed
      ultimately show ?thesis by blast
    qed
    moreover have "U ⊆ uspace ?Φ" using openin_subset U_open by force
    ultimately show "openin ?T' U" unfolding openin_utopology by force
  next
    assume U_open: "openin ?T' U"
    have "∃W. neighborhood σ W ∧ W ⊆ U" if hσ: "σ ∈ U" for σ
    proof -
      have in_group: "σ ∈ carrier G" using hσ U_open openin_subset topspace_utopology by force
      from U_open hσ obtain E where hE: "entourage_in ?Φ E ∧ E``{σ} ⊆ U"
        unfolding openin_utopology by blast
      then obtain V where hV: "neighborhood 𝟭 V ∧ left_entourage V ⊆ E"
        unfolding entourage_left_uniformity by fastforce
      let ?W = "{τ ∈ carrier G. inv σ ⊗ τ ∈ V}"
      from hV have W_subset: "?W ⊆ E``{σ}" using in_group by fast
      have "continuous_map T T (λτ. inv σ ⊗ τ)" using translations_continuous in_group inv_closed by blast
      then have "openin T ?W" using openin_continuous_map_preimage hV by fastforce
      then have "neighborhood σ ?W" using in_group r_inv hV by simp
      then show ?thesis using W_subset hE by fast
    qed
    then show "openin T U" using openin_subopen by force
  qed
  then show ?thesis using topology_eq by blast
qed

lemma right_uniformity_induces_group_topology [simp]:
  shows "utopology right_uniformity = T"
proof -
  let ?Φ = right_uniformity
  let ?T' = "utopology ?Φ"
  have "openin T U ⟷ openin ?T' U" for U
  proof
    assume U_open: "openin T U"
    have "∃E. entourage_in ?Φ E ∧ E``{σ} ⊆ U" if hσ: "σ ∈ U" for σ
    proof -
      let ?E = "right_entourage (σ <# set_inv U)"
      have in_group: "σ ∈ carrier G" using hσ U_open open_set_in_carrier by blast
      then have "openin T (σ <# set_inv U)"
        using open_set_inv_open open_set_translations(1) U_open by presburger
      then have "neighborhood 𝟭 (σ <# set_inv U)"
        using hσ in_group r_inv unfolding l_coset_def SET_INV_def by force
      then have "entourage_in ?Φ ?E" unfolding entourage_right_uniformity by blast
      moreover have "τ ∈ U" if "τ ∈ ?E``{σ}" for τ
      proof -
        from that have "σ ⊗ inv τ ∈ σ <# set_inv U" by force
        then obtain ρ where hρ: "ρ ∈ U ∧ σ ⊗ inv τ = σ ⊗ inv ρ"
          unfolding l_coset_def SET_INV_def by fast
        then have "ρ ∈ carrier G ∧ τ ∈ carrier G" using that open_set_in_carrier U_open by fast
        then have "τ = ρ" using in_group hρ inv_closed by (metis Units_eq Units_l_cancel inv_inv)
        then show ?thesis using hρ by simp
      qed
      ultimately show ?thesis by blast
    qed
    moreover have "U ⊆ uspace ?Φ" using openin_subset U_open by force
    ultimately show "openin ?T' U" unfolding openin_utopology by force
  next
    assume U_open: "openin ?T' U"
    have "∃W. neighborhood σ W ∧ W ⊆ U" if hσ: "σ ∈ U" for σ
    proof -
      have in_group: "σ ∈ carrier G" using hσ U_open openin_subset topspace_utopology by force
      from U_open hσ obtain E where hE: "entourage_in ?Φ E ∧ E``{σ} ⊆ U"
        unfolding openin_utopology by blast
      then obtain V where hV: "neighborhood 𝟭 V ∧ right_entourage V ⊆ E"
        unfolding entourage_right_uniformity by fastforce
      let ?W = "{τ ∈ carrier G. σ ⊗ inv τ ∈ V}"
      from hV have W_subset: "?W ⊆ E``{σ}" using in_group by fast
      have "(λτ. σ ⊗ inv τ) = (λτ. σ ⊗ τ) ∘ (λτ. inv τ)" by fastforce
      then have "continuous_map T T (λτ. σ ⊗ inv τ)" using continuous_map_compose inv_continuous
          translations_continuous[OF in_group] by metis
      then have "openin T ?W" using openin_continuous_map_preimage hV by fastforce
      then have "neighborhood σ ?W" using in_group r_inv hV by simp
      then show ?thesis using W_subset hE by fast
    qed
    then show "openin T U" using openin_subopen by force
  qed
  then show ?thesis using topology_eq by blast
qed

lemma translations_ucontinuous:
  assumes in_group: "σ ∈ carrier G"
  shows "ucontinuous left_uniformity left_uniformity (λτ. σ ⊗ τ)" and
    "ucontinuous right_uniformity right_uniformity (λτ. τ ⊗ σ)"
proof -
  let ?Φ = left_uniformity
  have "entourage_in ?Φ {(τ1, τ2) ∈ uspace ?Φ × uspace ?Φ. (σ ⊗ τ1, σ ⊗ τ2) ∈ E}"
    if hE: "entourage_in ?Φ E" for E
  proof -
    let ?F = "{(τ1, τ2) ∈ uspace ?Φ × uspace ?Φ. (σ ⊗ τ1, σ ⊗ τ2) ∈ E}"
    from hE obtain U where hU: "neighborhood 𝟭 U ∧ left_entourage U ⊆ E"
      unfolding entourage_left_uniformity by auto
    have "(τ1, τ2) ∈ ?F" if "τ1 ∈ carrier G ∧ τ2 ∈ carrier G ∧ inv τ1 ⊗ τ2 ∈ U" for τ1 τ2
    proof -
      have "inv (σ ⊗ τ1) ⊗ (σ ⊗ τ2) = inv τ1 ⊗ τ2"
        using that in_group m_closed inv_closed inv_mult_group m_assoc r_inv r_one
        by (smt (verit, ccfv_threshold))
      then have "(σ ⊗ τ1, σ ⊗ τ2) ∈ E" using that hU in_group m_closed by fastforce
      then show ?thesis using that by auto
    qed
    then have "left_entourage U ⊆ ?F" by force
    then show ?thesis unfolding entourage_left_uniformity using hU by auto
  qed
  moreover have "(λτ. σ ⊗ τ) ∈ uspace ?Φ → uspace ?Φ"
    unfolding Pi_def using uspace_left_uniformity in_group m_closed by force
  ultimately show "ucontinuous ?Φ ?Φ (λτ. σ ⊗ τ)"
    unfolding ucontinuous_def by fast
next
  let ?Φ = right_uniformity
  have "entourage_in ?Φ {(τ1, τ2) ∈ uspace ?Φ × uspace ?Φ. (τ1 ⊗ σ, τ2 ⊗ σ) ∈ E}"
    if hE: "entourage_in ?Φ E" for E
  proof -
    let ?F = "{(τ1, τ2) ∈ uspace ?Φ × uspace ?Φ. (τ1 ⊗ σ, τ2 ⊗ σ) ∈ E}"
    from hE obtain U where hU: "neighborhood 𝟭 U ∧ right_entourage U ⊆ E"
      unfolding entourage_right_uniformity by auto
    have "(τ1, τ2) ∈ ?F" if "τ1 ∈ carrier G ∧ τ2 ∈ carrier G ∧ τ1 ⊗ inv τ2 ∈ U" for τ1 τ2
    proof -
      have "(τ1 ⊗ σ) ⊗ inv (τ2 ⊗ σ) = τ1 ⊗ inv τ2"
        using that in_group m_closed inv_closed inv_mult_group m_assoc r_inv r_one
        by (smt (verit, ccfv_threshold))
      then have "(τ1 ⊗ σ, τ2 ⊗ σ) ∈ E" using that hU in_group m_closed by fastforce
      then show ?thesis using that by simp
    qed
    then have "right_entourage U ⊆ ?F" by force
    then show ?thesis unfolding entourage_right_uniformity using hU by auto
  qed
  moreover have "(λτ. τ ⊗ σ) ∈ uspace ?Φ → uspace ?Φ"
    unfolding Pi_def using entourage_right_uniformity in_group m_closed by force
  ultimately show "ucontinuous ?Φ ?Φ (λτ. τ ⊗ σ)" 
    unfolding ucontinuous_def by fast
qed

subsection ‹The Birkhoff-Kakutani theorem›
subsubsection ‹Prenorms on groups›

definition group_prenorm :: "('g ⇒ real) ⇒ bool" where
"group_prenorm N ⟷
  N 𝟭 = 0 ∧
  (∀σ τ. σ ∈ carrier G ∧ τ ∈ carrier G ⟶ N (σ ⊗ τ) ≤ N σ + N τ) ∧
  (∀σ ∈ carrier G. N (inv σ) = N σ)"

lemma group_prenorm_clauses[elim]:
  assumes "group_prenorm N"
  obtains 
    "N 𝟭 = 0" and 
    "⋀σ τ. σ ∈ carrier G ⟹ τ ∈ carrier G ⟹ N (σ ⊗ τ) ≤ N σ + N τ" and 
    "⋀σ. σ ∈ carrier G ⟹ N (inv σ) = N σ"
  using assms unfolding group_prenorm_def by auto

proposition group_prenorm_nonnegative:
  assumes prenorm: "group_prenorm N"
  shows "∀σ ∈ carrier G. N σ ≥ 0"
proof
  fix σ assume "σ ∈ carrier G"
  from r_inv this have "0 ≤ N σ + N σ" using assms inv_closed group_prenorm_clauses by metis
  then show "N σ ≥ 0" by fastforce
qed

proposition group_prenorm_reverse_triangle_ineq:
  assumes prenorm: "group_prenorm N" and in_group: "σ ∈ carrier G ∧ τ ∈ carrier G"
  shows "¦N σ - N τ¦ ≤ N (σ ⊗ inv τ)"
proof -
  have "σ = σ ⊗ inv τ ⊗ τ" using in_group inv_closed r_one l_inv m_assoc by metis
  then have a: "N σ ≤ N (σ ⊗ inv τ) + N τ" using in_group inv_closed m_closed prenorm group_prenorm_clauses by metis
  have "inv τ = inv σ ⊗ (σ ⊗ inv τ)" using in_group inv_closed l_one l_inv m_assoc by metis 
  then have b: "N τ ≤ N σ + N (σ ⊗ inv τ)" using in_group inv_closed m_closed prenorm group_prenorm_clauses by metis
  from a b show ?thesis by linarith
qed

definition induced_group_prenorm :: "('g ⇒ real) ⇒ 'g ⇒ real" where
"induced_group_prenorm f σ = (SUP τ ∈ carrier G. ¦f (τ ⊗ σ) - f τ¦)"
  
lemma induced_group_prenorm_welldefined:
  fixes f :: "'g ⇒ real"
  assumes f_bounded: "∃c.∀τ ∈ carrier G. ¦f τ¦ ≤ c" and in_group: "σ ∈ carrier G"
  shows "bdd_above ((λτ. ¦f (τ ⊗ σ) - f τ¦)`(carrier G))"
proof -
  from f_bounded obtain c where hc: "∀τ ∈ carrier G. ¦f τ¦ ≤ c" by blast
  have "¦f (τ ⊗ σ) - f τ¦ ≤ 2*c" if "τ ∈ carrier G" for τ
  proof -
    have "¦f (τ ⊗ σ) - f τ¦ ≤ ¦f (τ ⊗ σ)¦ + ¦f τ¦" using abs_triangle_ineq by simp
    then show ?thesis using in_group that m_closed f_bounded hc by (smt (verit, best))
  qed
  then show ?thesis unfolding bdd_above_def image_def by blast
qed

lemma bounded_function_induces_group_prenorm:
  fixes f :: "'g ⇒ real"
  assumes f_bounded: "∃c.∀σ ∈ carrier G. ¦f σ¦ ≤ c"
  shows "group_prenorm (induced_group_prenorm f)"
proof -
  let ?N = "λσ. SUP τ ∈ carrier G. ¦f (τ ⊗ σ) - f τ¦"
  have "?N 𝟭 = (SUP τ ∈ carrier G. 0)" using r_one by simp 
  then have "?N 𝟭 = 0" using carrier_not_empty by simp
  moreover have "?N (σ ⊗ τ) ≤ ?N σ + ?N τ" if hστ: "σ ∈ carrier G ∧ τ ∈ carrier G" for σ τ
  proof -
    have "¦f (ρ ⊗ (σ ⊗ τ)) - f ρ¦ ≤ ?N σ + ?N τ" if "ρ ∈ carrier G" for ρ
    proof -
      have a: "¦f (ρ ⊗ (σ ⊗ τ)) - f ρ¦ ≤ ¦f (ρ ⊗ (σ ⊗ τ)) - f (ρ ⊗ σ)¦ + ¦f (ρ ⊗ σ) - f ρ¦" 
        using abs_triangle_ineq by linarith
      have "¦f (ρ ⊗ σ ⊗ τ) - f (ρ ⊗ σ)¦ ≤ ?N τ" 
        using induced_group_prenorm_welldefined[OF f_bounded] that hστ m_closed cSUP_upper by meson
      then have b: "¦f (ρ ⊗ (σ ⊗ τ)) - f (ρ ⊗ σ)¦ ≤ ?N τ" using m_assoc that hστ by simp
      have c: "¦f (ρ ⊗ σ) - f ρ¦ ≤ ?N σ" using induced_group_prenorm_welldefined[OF f_bounded] hστ that cSUP_upper by meson
      from a b c show ?thesis by argo
    qed                              
    then show ?thesis using cSUP_least carrier_not_empty by meson
  qed
  moreover have "?N (inv σ) = ?N σ" if hσ: "σ ∈ carrier G" for σ
  proof -
    have "¦f (τ ⊗ inv σ) - f τ¦ ∈ {¦f (ρ ⊗ σ) - f ρ¦ | ρ. ρ ∈ carrier G }" if "τ ∈ carrier G" for τ
    proof -
      have "¦f (τ ⊗ inv σ) - f τ¦ = ¦f (τ ⊗ inv σ) - f (τ ⊗ inv σ ⊗ σ)¦" 
        using hσ that m_assoc r_one l_inv by simp
      then have "¦f (τ ⊗ inv σ) - f τ¦ = ¦f (τ ⊗ inv σ ⊗ σ) - f (τ ⊗ inv σ)¦" by argo
      then show ?thesis using hσ that m_closed by blast
    qed
    moreover 
    have "¦f (ρ ⊗ σ) - f ρ¦ ∈ {¦f (τ ⊗ inv σ) - f τ¦ | τ. τ ∈ carrier G }" if "ρ ∈ carrier G" for ρ
    proof -
      have "¦f (ρ ⊗ σ) - f ρ¦ = ¦f (ρ ⊗ σ) - f (ρ ⊗ σ ⊗ inv σ)¦" 
        using hσ that m_assoc r_one r_inv by simp
      then have "¦f (ρ ⊗ σ) - f ρ¦ = ¦f (ρ ⊗ σ ⊗ inv σ) - f (ρ ⊗ σ)¦" by argo
      then show ?thesis using hσ that by blast
    qed
    ultimately have "{¦f (τ ⊗ inv σ) - f τ¦ | τ. τ ∈ carrier G} = {¦f (ρ ⊗ σ) - f ρ¦ | ρ. ρ ∈ carrier G}" by blast
    then show ?thesis by (simp add: setcompr_eq_image)
  qed
  ultimately show ?thesis unfolding induced_group_prenorm_def group_prenorm_def by fast
qed

lemma neighborhood_1_translation:
  assumes "neighborhood 𝟭 U" and "σ ∈ carrier G ∨ σ ∈ topspace T"
  shows "neighborhood σ (σ <# U)"
proof -
  have "openin T (σ <# U)" using assms open_set_translations(1) by simp
  then show ?thesis unfolding l_coset_def using assms r_one by force
qed
           
proposition group_prenorm_continuous_if_continuous_at_1:
  assumes prenorm: "group_prenorm N" and 
    continuous_at_1: "∀ε>0.∃U. neighborhood 𝟭 U ∧ (∀σ∈U. N σ < ε)"
  shows "continuous_map T euclideanreal N"
proof -
  have "∃V. neighborhood σ V ∧ (∀τ∈V. N τ ∈ Met_TC.mball (N σ) ε)" 
    if hσ: "σ ∈ topspace T" and hε: "ε > 0" for σ ε
  proof -
    from continuous_at_1 obtain U where hU: "neighborhood 𝟭 U ∧ (∀τ∈U. N τ < ε)" using hε by presburger
    then have "neighborhood σ (σ <# U)" using hσ neighborhood_1_translation by blast
    moreover have "N (σ ⊗ τ) ∈ Met_TC.mball (N σ) ε" if "τ ∈ U" for τ
    proof -
      have in_group: "σ ∈ carrier G ∧ τ ∈ carrier G" using hσ that openin_subset hU by blast
      then have "(inv σ) ⊗ (σ ⊗ τ) = τ" using l_inv l_one m_assoc inv_closed by metis
      then have "¦N (inv σ) - N (inv (σ ⊗ τ))¦ ≤ N τ" using group_prenorm_reverse_triangle_ineq 
          in_group inv_closed m_closed by (metis inv_inv prenorm)
      then have "¦N σ - N (σ ⊗ τ)¦ < ε" 
        using prenorm in_group m_closed inv_closed hU that by fastforce
      then show ?thesis unfolding Met_TC.mball_def dist_real_def by fast
    qed
    ultimately show ?thesis unfolding l_coset_def by blast
  qed
  then show ?thesis using Metric_space.continuous_map_to_metric
    by (metis Met_TC.Metric_space_axioms mtopology_is_euclidean)
qed

subsubsection ‹A prenorm respecting the group topology›

context
  fixes U :: "nat ⇒ 'g set"
  assumes U_neighborhood: "∀n. neighborhood 𝟭 (U n)"
  assumes U_props: "∀n. symmetric (U n) ∧ (U (n + 1)) <#> (U (n + 1)) ⊆ (U n)"
begin

private fun V :: "nat ⇒ nat ⇒ 'g set" where
"V m n = (
  if m = 0 then {} else
  if m = 1 then U n else
  if m > 2^n then carrier G else
  if even m then V (m div 2) (n - 1) else
  V ((m - 1) div 2) (n - 1) <#> U n
)"

private lemma U_in_group: "U k ⊆ carrier G" using U_neighborhood open_set_in_carrier by fast

private lemma V_in_group:
  shows "V m n ⊆ carrier G"
proof (induction n arbitrary: m)
  case (Suc n)
  then have "V ((m - 1) div 2) n <#> U (Suc n) ⊆ carrier G"
    unfolding set_mult_def using U_in_group by fast
  then show ?case using U_in_group Suc by simp
qed (auto simp: U_in_group)

private lemma V_mult:
  shows "m ≥ 1 ⟹ V m n <#> U n ⊆ V (m + 1) n"
proof (induction n arbitrary: m)
  case 0
  then have "V (m + 1) 0 = carrier G" by simp
  then show ?case unfolding set_mult_def using V_in_group U_in_group by fast
next
  case (Suc n)
  then show ?case
  proof (cases "m + 1 > 2^(Suc n)")
    case True
    then have "V (m + 1) (Suc n) = carrier G" by force
    then show ?thesis unfolding set_mult_def using V_in_group U_in_group by blast
  next
    case m_in_bounds: False
    then show ?thesis
    proof (cases "m = 1")
      case True
      then show ?thesis using U_in_group U_props by force
    next
      case m_not_1: False
      then show ?thesis
      proof (cases "even m")
        case True
        then have "V m (Suc n) <#> U (Suc n) = V (m + 1) (Suc n)" using m_in_bounds m_not_1 Suc(2) by auto
        then show ?thesis by blast
      next
        case m_odd: False
        have U_mult: "U (Suc n) <#> U (Suc n) ⊆ U n" using U_props by simp 
        have not_zero: "(m - 1) div 2 ≥ 1" using Suc(2) m_not_1 m_odd by presburger
        have arith: "(m - 1) div 2 + 1 = (m + 1) div 2" using Suc(2) by simp
        have "V m (Suc n) <#> U (Suc n) = V ((m - 1) div 2) n <#> U (Suc n) <#> U (Suc n)" using m_odd m_in_bounds m_not_1 Suc(2) by simp
        also have "... = V ((m - 1) div 2) n <#> (U (Suc n) <#> U (Suc n))" using set_mult_assoc V_in_group U_in_group by simp
        also have "... ⊆ V ((m - 1) div 2) n <#> U n" using mono_set_mult U_mult by blast
        also have "... ⊆ V ((m - 1) div 2 + 1) n" using Suc(1) not_zero by blast
        also have "...  = V ((m + 1) div 2) n" using arith by presburger
        also have "... =  V (m + 1) (Suc n)" using m_odd m_not_1 m_in_bounds Suc(2) by simp
        finally show ?thesis by blast
      qed
    qed
  qed
qed

private lemma V_mono:
  assumes smaller: "(real m1)/2^n1 ≤ (real m2)/2^n2" and not_zero: "m1 ≥ 1 ∧ m2 ≥ 1"
  shows "V m1 n1 ⊆ V m2 n2"
proof -
  have "V m n ⊆ V (m + 1) n" if "m ≥ 1" for m n
  proof -
    have "V m n <#> U n ⊆ V (m + 1) n" using V_mult U_props that by presburger
    moreover have "V m n ⊆ carrier G ∧ U n ⊆ carrier G" using U_in_group V_in_group by auto
    ultimately show ?thesis using set_mult_one_subset U_neighborhood by blast
  qed
  then have subset_suc: "V m n ⊆ V (m + 1) n" for m n by simp
  have "V m n ⊆ V (m + k) n" for m n k
  proof (induction k)
    case (Suc k)
    then show ?case unfolding Suc_eq_plus1 using subset_suc Suc
      by (metis (no_types, opaque_lifting) add.assoc dual_order.trans)
  qed (simp)
  then have a: "V m n ⊆ V m' n" if "m' ≥ m" for m m' n using that le_Suc_ex by blast
  have b: "V m n = V (m * 2^k) (n+k)" if "m ≥ 1" for m n k
  proof (induction k)
    case (Suc k)
    have "V (m * 2^k * 2) (n + k + 1) = V (m * 2^k) (n + k)" using that by simp
    then show ?case unfolding Suc_eq_plus1 using Suc by simp
  qed (auto)
  show ?thesis
  proof (cases "n1 ≤ n2")
    case True
    have "(real m1)/2^n1 = (real (m1 * 2^(n2 - n1)))/(2^n1 * 2^(n2 - n1))" by fastforce
    also have "... = (real (m1 * 2^(n2 - n1)))/2^n2" using True by (metis le_add_diff_inverse power_add)
    finally have "(real (m1 * 2^(n2 - n1)))/2^n2 ≤ (real m2)/2^n2" using smaller by fastforce
    then have ineq: "m1 * 2^(n2 - n1) ≤ m2"
      by (smt (verit) divide_cancel_right divide_right_mono linorder_le_cases of_nat_eq_iff of_nat_mono order_antisym_conv power_not_zero zero_le_power)
    from b have "V m1 n1 = V (m1 * 2^(n2 - n1)) (n1 + (n2 - n1))" using not_zero by blast
    also have "... = V (m1 * 2^(n2 - n1)) n2" using True by force
    finally show ?thesis using a[OF ineq] by blast
  next
    case False
    then have n2_leq_n1: "n2 ≤ n1" by simp
    have "(real m2)/2^n2 = (real (m2 * 2^(n1 - n2)))/(2^n2 * 2^(n1 - n2))" by fastforce
    also have "... = (real (m2 * 2^(n1 - n2)))/2^n1" using n2_leq_n1 by (metis le_add_diff_inverse power_add)
    finally have "(real (m2 * 2^(n1 - n2)))/2^n1 ≥ (real m1)/2^n1" using smaller by fastforce
    then have ineq: "m2 * 2^(n1 - n2) ≥ m1"
      by (smt (verit) divide_cancel_right divide_right_mono linorder_le_cases of_nat_eq_iff of_nat_mono order_antisym_conv power_not_zero zero_le_power)
    from b have "V m2 n2 = V (m2 * 2^(n1 - n2)) (n2 + (n1 - n2))" using not_zero by blast
    also have "... = V (m2 * 2^(n1 - n2)) n1" using n2_leq_n1 by force
    finally show ?thesis using a[OF ineq] by blast
  qed
qed

private lemma approx_number_by_multiples:
  assumes hx: "x ≥ 0" and hc: "c > 0"
  shows "∃k :: nat ≥ 1. (real (k-1))/c ≤ x ∧ x < (real k)/c"
proof -
  let ?k = "⌊x * c⌋ + 1"
  have "?k ≥ 1" using assms by simp
  moreover from this have "real (nat ?k) = ?k" by auto
  moreover have "(?k-1)/c ≤ x ∧ x < ?k/c" 
    using assms by (simp add: mult_imp_div_pos_le pos_less_divide_eq)
  ultimately show ?thesis
    by (smt (verit) nat_diff_distrib nat_le_eq_zle nat_one_as_int of_nat_nat)
qed

lemma construction_of_prenorm_respecting_topology:
  shows "∃N. group_prenorm N ∧ 
    (∀n. {σ ∈ carrier G. N σ < 1/2^n} ⊆ U n) ∧ 
    (∀n. U n ⊆ {σ ∈ carrier G. N σ ≤ 2/2^n})"
proof -
  define f :: "'g ⇒ real" where "f σ = Inf {(real m)/2^n | m n. σ ∈ V m n}" for σ
  define N :: "'g ⇒ real" where "N = induced_group_prenorm f"

  have "σ ∈ V 2 0" if "σ ∈ carrier G" for σ using that by auto
  then have contains_2: "(real 2)/2^0 ∈ {(real m)/2^n | m n. σ ∈ V m n}" if "σ ∈ carrier G" for σ using that by blast
  then have nonempty: "{(real m)/2^n | m n. σ ∈ V m n} ≠ {}" if "σ ∈ carrier G" for σ using that by fast
  have positive: "(real m)/2^n ≥ 0" for m n by simp
  then have bdd_below: "bdd_below {(real m)/2^n | m n. σ ∈ V m n}" for σ by fast
  have f_bounds: "0 ≤ f σ ∧ f σ ≤ 2" if hσ: "σ ∈ carrier G" for σ
  proof -
    from bdd_below have "f σ ≤ (real 2)/2^0" unfolding f_def using cInf_lower contains_2[OF hσ] by meson
    moreover have "0 ≤ f σ" using cInf_greatest contains_2[OF hσ] unfolding f_def using positive
      by (smt (verit, del_insts) Collect_mem_eq empty_Collect_eq mem_Collect_eq)
    ultimately show ?thesis by fastforce
  qed
  then have N_welldefined: "bdd_above ((λτ. ¦f (τ ⊗ σ) - f τ¦) ` carrier G)" if "σ ∈ carrier G" for σ
    using induced_group_prenorm_welldefined that by (metis (full_types) abs_of_nonneg)

  have in_V_if_f_smaller: "σ ∈ V m n" if hσ: "σ ∈ carrier G" and smaller: "f σ < (real m)/2^n" for σ m n
  proof -
    from cInf_lessD obtain q where hq: "q ∈ {(real m)/2^n | m n. σ ∈ V m n} ∧ q < (real m)/2^n"
      using smaller nonempty[OF hσ] unfolding f_def by (metis (mono_tags, lifting))
    then obtain m' n' where hm'n': "σ ∈ V m' n' ∧ q = (real m')/2^n'" by fast
    moreover have "m' ≥ 1"
    proof (rule ccontr)
      assume "¬ m' ≥ 1"
      then have "V m' n' = {}" by force
      then show "False" using hm'n' by blast
    qed
    moreover have "m ≥ 1" using f_bounds smaller hσ
      by (metis divide_eq_0_iff less_numeral_extra(3) less_one linorder_le_less_linear nle_le of_nat_0 order_less_imp_le)
    ultimately have "V m' n' ⊆ V m n" using V_mono hq U_props open_set_in_carrier by simp
    then show ?thesis using hm'n' by fast
  qed
  have f_1_vanishes: "f 𝟭 = 0"
  proof (rule ccontr)
    assume "f 𝟭 ≠ 0"
    then have "f 𝟭 > 0" using f_bounds by fastforce
    then obtain n where hn: "f 𝟭 > (real 1)/2^n"
      by (metis divide_less_eq_1 of_nat_1 one_less_numeral_iff power_one_over real_arch_pow_inv semiring_norm(76) zero_less_numeral)
    have "𝟭 ∈ V 1 n" using U_neighborhood by simp
    then have "(real 1)/2^n ∈ {(real m)/2^n |m n. 𝟭 ∈ V m n}" by fast
    then show "False" using hn cInf_lower bdd_below[of 𝟭] unfolding f_def by (smt (verit, ccfv_threshold))
  qed
  have in_U_if_N_small: "σ ∈ U n" if in_group: "σ ∈ carrier G" and N_small: "N σ < 1/2^n" for σ n
  proof -
    have "f σ = ¦f (𝟭 ⊗ σ) - f 𝟭¦" using in_group l_one f_1_vanishes f_bounds by force
    moreover have "... ≤ N σ" unfolding N_def induced_group_prenorm_def
      using cSUP_upper N_welldefined[OF in_group] by (metis (mono_tags, lifting) one_closed)
    ultimately have "σ ∈ V 1 n" using in_V_if_f_smaller[OF in_group] N_small by (smt (verit) of_nat_1) 
    then show ?thesis by fastforce
  qed
  have N_bounds: "N σ ≤ 2/2^n" if hσ: "σ ∈ U n" for σ n
  proof -
    have diff_bounded: "f (τ ⊗ σ) - f τ ≤ 2/2^n ∧ f (τ ⊗ inv σ) - f τ ≤ 2/2^n" if hτ: "τ ∈ carrier G" for τ
    proof -
      obtain k where hk: "k ≥ 1 ∧ (real (k-1))/2^n ≤ f τ ∧ f τ < (real k)/2^n"
        using approx_number_by_multiples[of "f τ" "2^n"] f_bounds[OF hτ] by auto
      then have "τ ∈ V k n" using in_V_if_f_smaller[OF hτ] by blast
      moreover have "σ ∈ V 1 n ∧ inv σ ∈ V 1 n" using hσ U_props by auto
      moreover have "V k n <#> V 1 n ⊆ V (k + 1) n"
        using V_mult U_props open_set_in_carrier hk by auto
      ultimately have "τ ⊗ σ ∈ V (k + 1) n ∧ τ ⊗ inv σ ∈ V (k + 1) n" 
        unfolding set_mult_def by fast
      then have a: "(real (k + 1))/2^n ∈ {(real m)/2^n | m n. τ ⊗ σ ∈ V m n}
        ∧ (real (k + 1))/2^n ∈ {(real m)/2^n | m n. τ ⊗ inv σ ∈ V m n}" by fast
      then have "f (τ ⊗ σ) ≤ (real (k + 1))/2^n" 
        unfolding f_def using cInf_lower[of "(real (k + 1))/2^n"] bdd_below by presburger
      moreover from a have "f (τ ⊗ inv σ) ≤ (real (k + 1))/2^n" 
        unfolding f_def using cInf_lower[of "(real (k + 1))/2^n"] bdd_below by presburger
      ultimately show ?thesis using hk
        by (smt (verit, ccfv_SIG) diff_divide_distrib of_nat_1 of_nat_add of_nat_diff)
    qed
    have "¦f (ρ ⊗ σ) - f ρ¦ ≤ 2/2^n" if hρ: "ρ ∈ carrier G" for ρ
    proof -
      have in_group: "σ ∈ carrier G" using hσ U_in_group by fast
      then have "f (ρ ⊗ σ ⊗ inv σ) - f (ρ ⊗ σ) ≤ 2/2^n" using diff_bounded[of "ρ ⊗ σ"] hρ m_closed by fast
      moreover have "ρ ⊗ σ ⊗ inv σ = ρ" using m_assoc r_inv r_one in_group inv_closed hρ by presburger
      ultimately have "f ρ - f (ρ ⊗ σ) ≤ 2/2^n" by force
      moreover have "f (ρ ⊗ σ) - f ρ ≤ 2/2^n" using diff_bounded[OF hρ] by fast
      ultimately show ?thesis by force
    qed
    then show ?thesis unfolding N_def induced_group_prenorm_def using cSUP_least carrier_not_empty by meson
  qed
  then have "U n ⊆ {σ ∈ carrier G. N σ ≤ 2/2^n}" for n using U_in_group by blast
  moreover have "group_prenorm N" unfolding N_def 
    using bounded_function_induces_group_prenorm f_bounds by (metis abs_of_nonneg)
  ultimately show ?thesis using in_U_if_N_small by blast
qed
end

subsubsection ‹Proof of Birkhoff-Kakutani›

lemma first_countable_neighborhoods_of_1_sequence:
  assumes "first_countable T"
  shows "∃U :: nat ⇒ 'g set. 
    (∀n. neighborhood 𝟭 (U n) ∧ symmetric (U n) ∧ U (n + 1) <#> U (n + 1) ⊆ U n) ∧ 
    (∀W. neighborhood 𝟭 W ⟶ (∃n. U n ⊆ W))"
proof -
  from assms obtain ℬ where hℬ: 
    "countable ℬ ∧ (∀W∈ℬ. openin T W) ∧ (∀U. neighborhood 𝟭 U ⟶ (∃W∈ℬ. 𝟭 ∈ W ∧ W ⊆ U))"
    unfolding first_countable_def by fastforce
  define 𝔅 :: "'g set set" where "𝔅 = insert (carrier G) {W ∈ ℬ. 𝟭 ∈ W}"
  define B :: "nat ⇒ 'g set" where "B = from_nat_into 𝔅"
  have "𝔅 ≠ {} ∧ (∀W∈𝔅. neighborhood 𝟭 W)" unfolding 𝔅_def using hℬ
    by (metis group_is_space insert_iff insert_not_empty mem_Collect_eq one_closed openin_topspace)
  then have B_neighborhood: "∀n. neighborhood 𝟭 (B n)" unfolding B_def by (simp add: from_nat_into)
  define P where "P n V ⟷ V ⊆ B n ∧ neighborhood 𝟭 V ∧ symmetric V" for n V
  define Q where "Q (n :: nat) V W ⟷ W <#> W ⊆ V" for n V W
  have "∃V. P 0 V"
  proof -
    obtain W where "neighborhood 𝟭 W ∧ symmetric W ∧ W <#> W ⊆ B 0" 
      using neighborhoods_of_1 B_neighborhood by fastforce
    moreover from this have "W ⊆ B 0" using set_mult_one_subset open_set_in_carrier by blast
    ultimately show ?thesis unfolding P_def by auto
  qed
  moreover have "∃W. P (Suc n) W ∧ Q n V W" if "P n V" for n V
  proof -
    have "neighborhood 𝟭 (V ∩ B (Suc n))" using B_neighborhood that unfolding P_def by auto
    then obtain W where "neighborhood 𝟭 W ∧ symmetric W ∧ W <#> W ⊆ V ∩ B (Suc n)" 
      using neighborhoods_of_1 by fastforce
    moreover from this have "W ⊆ B (Suc n)" 
      using set_mult_one_subset[of W W] open_set_in_carrier[of W] by fast
    ultimately show ?thesis unfolding P_def Q_def by auto
  qed
  ultimately obtain U where hU: "∀n. P n (U n) ∧ Q n (U n) (U (Suc n))"
    using dependent_nat_choice by metis
  moreover have "∃n. U n ⊆ W" if "neighborhood 𝟭 W" for W
  proof -
    from that obtain W' where hW': "W' ∈ ℬ ∧ 𝟭 ∈ W' ∧ W' ⊆ W" using hℬ by blast
    then have "W' ∈ 𝔅 ∧ countable 𝔅" unfolding 𝔅_def using hℬ by simp
    then obtain n where "B n = W'" unfolding B_def using from_nat_into_to_nat_on by fast
    then show ?thesis using hW' hU unfolding P_def by blast
  qed
  ultimately show ?thesis unfolding P_def Q_def by auto
qed

definition "left_invariant_metric Δ ⟷ Metric_space (carrier G) Δ ∧
  (∀σ τ ρ. σ ∈ carrier G ∧ τ ∈ carrier G ∧ ρ ∈ carrier G ⟶ Δ (ρ ⊗ σ) (ρ ⊗ τ) = Δ σ τ)"

definition "right_invariant_metric Δ ⟷ Metric_space (carrier G) Δ ∧
  (∀σ τ ρ. σ ∈ carrier G ∧ τ ∈ carrier G ∧ ρ ∈ carrier G ⟶ Δ (σ ⊗ ρ) (τ ⊗ ρ) = Δ σ τ)"

lemma left_invariant_metricE:
  assumes "left_invariant_metric Δ" "σ ∈ carrier G" "τ ∈ carrier G" "ρ ∈ carrier G"
  shows "Δ (ρ ⊗ σ) (ρ ⊗ τ) = Δ σ τ"
  using assms unfolding left_invariant_metric_def by blast

lemma right_invariant_metricE:
  assumes "right_invariant_metric Δ" "σ ∈ carrier G" "τ ∈ carrier G" "ρ ∈ carrier G"
  shows "Δ (σ ⊗ ρ) (τ ⊗ ρ) = Δ σ τ"
  using assms unfolding right_invariant_metric_def by blast

theorem Birkhoff_Kakutani_left:
  assumes Hausdorff: "Hausdorff_space T" and first_countable: "first_countable T"
  shows "∃Δ. left_invariant_metric Δ ∧ Metric_space.mtopology (carrier G) Δ = T"
proof -
  from first_countable obtain U :: "nat ⇒ 'g set" where 
    U_props: "∀n. neighborhood 𝟭 (U n) ∧ symmetric (U n) ∧ U (n + 1) <#> U (n + 1) ⊆ U n" and
    neighborhood_base: "∀W. neighborhood 𝟭 W ⟶ (∃n. U n ⊆ W)"
    using first_countable_neighborhoods_of_1_sequence by auto
  from U_props obtain N where
    prenorm: "group_prenorm N" and
    norm_ball_in_U: "∀n. {σ ∈ carrier G. N σ < 1/2^n} ⊆ U n" and
    U_in_norm_ball: "∀n. U n ⊆ {σ ∈ carrier G. N σ ≤ 2/2^n}"
    using construction_of_prenorm_respecting_topology by meson
  have continuous: "continuous_map T euclideanreal N" using prenorm
  proof (rule group_prenorm_continuous_if_continuous_at_1, intro allI impI)
    fix ε :: real assume "ε > 0"
    then obtain n where hn: "1/2^n < ε" 
      by (metis divide_less_eq_1_pos one_less_numeral_iff power_one_over real_arch_pow_inv semiring_norm(76) zero_less_numeral)
    then have "N σ < ε" if "σ ∈ U (n + 1)" for σ using that U_in_norm_ball by fastforce
    then show "∃U. neighborhood 𝟭 U ∧ (∀σ∈U. N σ < ε)" using U_props by meson
  qed
  let ?B = "λε. {σ ∈ carrier G. N σ < ε}"
  let ?Δ = "λσ τ. N (inv σ ⊗ τ)"
  let ?δ = "λσ τ. if σ ∈ carrier G ∧ τ ∈ carrier G then ?Δ σ τ else 42"
  have "?Δ σ τ ≥ 0" if "σ ∈ carrier G ∧ τ ∈ carrier G" for σ τ
    using group_prenorm_nonnegative prenorm that by blast
  moreover have "?Δ σ τ = ?Δ τ σ" if "σ ∈ carrier G ∧ τ ∈ carrier G" for σ τ
  proof -
    have "inv τ ⊗ σ = inv (inv σ ⊗ τ)" using inv_mult_group inv_inv that by auto
    then show ?thesis using prenorm that by fastforce
  qed
  moreover have "?Δ σ τ = 0 ⟷ σ = τ" if "σ ∈ carrier G ∧ τ ∈ carrier G" for σ τ
  proof
    assume "?Δ σ τ = 0"
    then have "inv σ ⊗ τ ∈ U n" for n using norm_ball_in_U that by fastforce
    then have "inv σ ⊗ τ ∈ W" if "neighborhood 𝟭 W" for W using neighborhood_base that by auto
    then have "inv σ ⊗ τ = 𝟭" using Hausdorff_space_sing_Inter_opens[of T 𝟭] Hausdorff by blast
    then show "σ = τ" using inv_comm inv_equality that by fastforce
  next
    assume "σ = τ"
    then show "?Δ σ τ = 0" using that prenorm by force
  qed
  moreover have "?Δ σ ρ ≤ ?Δ σ τ + ?Δ τ ρ" if "σ ∈ carrier G ∧ τ ∈ carrier G ∧ ρ ∈ carrier G" for σ τ ρ
  proof -
    have "inv σ ⊗ ρ = (inv σ ⊗ τ) ⊗ (inv τ ⊗ ρ)" using m_assoc[symmetric] that by (simp add: inv_solve_right)
    then show ?thesis using prenorm that by auto
  qed                        
  ultimately have metric: "Metric_space (carrier G) ?δ" unfolding Metric_space_def by auto
  then interpret Metric_space "carrier G" ?δ by blast
  have "?Δ (ρ ⊗ σ) (ρ ⊗ τ) = ?Δ σ τ" if "σ ∈ carrier G ∧ τ ∈ carrier G ∧ ρ ∈ carrier G" for σ τ ρ
  proof -
    have "inv σ ⊗ τ = inv (ρ ⊗ σ) ⊗ (ρ ⊗ τ)" using that m_assoc[symmetric] by (simp add: inv_solve_left inv_solve_right)
    then show ?thesis by simp
  qed
  then have left_invariant: "left_invariant_metric ?δ" 
    unfolding left_invariant_metric_def using metric by auto
  have mball_coset_of_norm_ball: "mball σ ε = σ <# ?B ε" if hσ: "σ ∈ carrier G" for σ ε
  proof -
    have "mball σ ε = {τ ∈ carrier G. N (inv σ ⊗ τ) < ε}" unfolding mball_def using hσ by auto
    also have "... = σ <# (?B ε)"
    proof -
      have "τ ∈ σ <# (?B ε)" if "τ ∈ carrier G ∧ N (inv σ ⊗ τ) < ε" for τ
      proof -
        have "σ ⊗ (inv σ ⊗ τ) = τ" using hσ that by (metis inv_closed inv_solve_left m_closed)
        moreover have "inv σ ⊗ τ ∈ ?B ε" using hσ that by fastforce
        ultimately show ?thesis unfolding l_coset_def by force
      qed
      moreover have "τ ∈ carrier G ∧ N (inv σ ⊗ τ) < ε" if "τ ∈ σ <# (?B ε)" for τ
      proof -
        from that obtain ρ where "ρ ∈ ?B ε ∧ τ = σ ⊗ ρ" unfolding l_coset_def by blast
        moreover from this have "inv σ ⊗ τ = ρ" using hσ by (simp add: inv_solve_left')
        ultimately show ?thesis using hσ by simp
      qed
      ultimately show ?thesis by blast
    qed
    finally show ?thesis by presburger
  qed
  define ball where "ball S ⟷ (∃σ ε. σ ∈ carrier G ∧ S = mball σ ε)" for S
  have "openin mtopology V" if "ball V" for V using that unfolding ball_def by fast
  moreover have "∃W. ball W ∧ σ ∈ W ∧ W ⊆ V" if "openin mtopology V ∧ σ ∈ V" for σ V
    unfolding ball_def using openin_mtopology that by (smt (verit, best) centre_in_mball_iff subset_iff)
  ultimately have openin_metric: "openin mtopology = arbitrary union_of ball" 
    by (simp add: openin_topology_base_unique)
  have "openin T V" if "ball V" for V
  proof -
    from that obtain σ ε where "σ ∈ carrier G ∧ V = σ <# ?B ε" 
      unfolding ball_def using mball_coset_of_norm_ball by blast
    moreover have "openin T (?B ε)" using continuous
      by (simp add: continuous_map_upper_lower_semicontinuous_lt)
    ultimately show ?thesis using open_set_translations(1) by presburger
  qed
  moreover have "∃W. ball W ∧ σ ∈ W ∧ W ⊆ V" if "neighborhood σ V" for σ V
  proof -
    from that have in_group: "σ ∈ carrier G" using open_set_in_carrier by fast
    then have "neighborhood 𝟭 (inv σ <# V)" 
      using l_coset_def open_set_translations(1) that l_inv by fastforce
    then obtain n where "U n ⊆ inv σ <# V" using neighborhood_base by presburger
    then have "?B (1/2^n) ⊆ inv σ <# V" using norm_ball_in_U by blast
    then have "σ <# ?B (1/2^n) ⊆ σ <# (inv σ <# V)" unfolding l_coset_def by fast
    also have "... = V" using in_group that open_set_in_carrier by (simp add: lcos_m_assoc lcos_mult_one)
    finally have "mball σ (1/2^n) ⊆ V" using mball_coset_of_norm_ball in_group by blast
    then show ?thesis unfolding ball_def
      by (smt (verit) centre_in_mball_iff divide_pos_pos in_group one_add_one zero_less_power zero_less_two)
  qed
  ultimately have "openin T = arbitrary union_of ball" by (simp add: openin_topology_base_unique)
  then show ?thesis using left_invariant openin_metric topology_eq by fastforce
qed

theorem Birkhoff_Kakutani_right:
  assumes Hausdorff: "Hausdorff_space T" and first_countable: "first_countable T"
  shows "∃Δ. right_invariant_metric Δ ∧ Metric_space.mtopology (carrier G) Δ = T"
proof -
  from first_countable obtain U :: "nat ⇒ 'g set" where 
    U_props: "∀n. neighborhood 𝟭 (U n) ∧ symmetric (U n) ∧ U (n + 1) <#> U (n + 1) ⊆ U n" and
    neighborhood_base: "∀W. neighborhood 𝟭 W ⟶ (∃n. U n ⊆ W)"
    using first_countable_neighborhoods_of_1_sequence by auto
  from U_props obtain N where
    prenorm: "group_prenorm N" and
    norm_ball_in_U: "∀n. {σ ∈ carrier G. N σ < 1/2^n} ⊆ U n" and
    U_in_norm_ball: "∀n. U n ⊆ {σ ∈ carrier G. N σ ≤ 2/2^n}"
    using construction_of_prenorm_respecting_topology by meson
  have continuous: "continuous_map T euclideanreal N" using prenorm
  proof (rule group_prenorm_continuous_if_continuous_at_1, intro allI impI)
    fix ε :: real assume "ε > 0"
    then obtain n where hn: "1/2^n < ε" 
      by (metis divide_less_eq_1_pos one_less_numeral_iff power_one_over real_arch_pow_inv semiring_norm(76) zero_less_numeral)
    then have "N σ < ε" if "σ ∈ U (n + 1)" for σ using that U_in_norm_ball by fastforce
    then show "∃U. neighborhood 𝟭 U ∧ (∀σ∈U. N σ < ε)" using U_props by meson
  qed
  let ?B = "λε. {σ ∈ carrier G. N σ < ε}"
  let ?Δ = "λσ τ. N (σ ⊗ inv τ)"
  let ?δ = "λσ τ. if σ ∈ carrier G ∧ τ ∈ carrier G then ?Δ σ τ else 42"
  have "?Δ σ τ ≥ 0" if "σ ∈ carrier G ∧ τ ∈ carrier G" for σ τ
    using group_prenorm_nonnegative prenorm that by blast
  moreover have "?Δ σ τ = ?Δ τ σ" if "σ ∈ carrier G ∧ τ ∈ carrier G" for σ τ
  proof -
    have "τ ⊗ inv σ = inv (σ ⊗ inv τ)" using inv_mult_group inv_inv that by auto
    then show ?thesis using prenorm that by auto 
  qed
  moreover have "?Δ σ τ = 0 ⟷ σ = τ" if "σ ∈ carrier G ∧ τ ∈ carrier G" for σ τ
  proof
    assume "?Δ σ τ = 0"
    then have "σ ⊗ inv τ ∈ U n" for n using norm_ball_in_U that by fastforce
    then have "σ ⊗ inv τ ∈ W" if "neighborhood 𝟭 W" for W using neighborhood_base that by auto
    then have "σ ⊗ inv τ = 𝟭" using Hausdorff_space_sing_Inter_opens[of T 𝟭] Hausdorff by blast
    then show "σ = τ" using inv_equality that by fastforce
  next
    assume "σ = τ"
    then show "?Δ σ τ = 0" using that prenorm by force
  qed
  moreover have "?Δ σ ρ ≤ ?Δ σ τ + ?Δ τ ρ" if "σ ∈ carrier G ∧ τ ∈ carrier G ∧ ρ ∈ carrier G" for σ τ ρ
  proof -
    have "σ ⊗ inv ρ = (σ ⊗ inv τ) ⊗ (τ ⊗ inv ρ)" using m_assoc that by (simp add: inv_solve_left)
    then show ?thesis using prenorm that by auto
  qed                        
  ultimately have metric: "Metric_space (carrier G) ?δ" unfolding Metric_space_def by auto
  then interpret Metric_space "carrier G" ?δ by blast
  have "?Δ (σ ⊗ ρ) (τ ⊗ ρ) = ?Δ σ τ" if "σ ∈ carrier G ∧ τ ∈ carrier G ∧ ρ ∈ carrier G" for σ τ ρ
  proof -
    have "σ ⊗ inv τ = (σ ⊗ ρ) ⊗ inv (τ ⊗ ρ)" using that m_assoc by (simp add: inv_solve_left inv_solve_right)
    then show ?thesis by simp
  qed
  then have right_invariant: "right_invariant_metric ?δ" 
    unfolding right_invariant_metric_def using metric by auto
  have mball_coset_of_norm_ball: "mball σ ε = ?B ε #> σ" if hσ: "σ ∈ carrier G" for σ ε
  proof -
    have "mball σ ε = {τ ∈ carrier G. N (σ ⊗ inv τ) < ε}" unfolding mball_def using hσ by auto
    also have "... = (?B ε) #> σ"
    proof -
      have "τ ∈ (?B ε) #> σ" if "τ ∈ carrier G ∧ N (σ ⊗ inv τ) < ε" for τ
      proof -
        have "inv (σ ⊗ inv τ) ⊗ σ = τ" using hσ that by (simp add: inv_mult_group m_assoc)
        moreover have "inv (σ ⊗ inv τ) ∈ ?B ε" using hσ that prenorm by fastforce
        ultimately show ?thesis unfolding r_coset_def by force
      qed
      moreover have "τ ∈ carrier G ∧ N (σ ⊗ inv τ) < ε" if "τ ∈ (?B ε) #> σ" for τ
      proof -
        from that obtain ρ where "ρ ∈ ?B ε ∧ τ = ρ ⊗ σ" unfolding r_coset_def by blast
        moreover from this have "σ ⊗ inv τ = inv ρ" using hσ
          by (metis (no_types, lifting) inv_closed inv_mult_group inv_solve_left m_closed mem_Collect_eq)
        ultimately show ?thesis using hσ prenorm by fastforce
      qed
      ultimately show ?thesis by blast
    qed
    finally show ?thesis by presburger
  qed
  define ball where "ball S ⟷ (∃σ ε. σ ∈ carrier G ∧ S = mball σ ε)" for S
  have "openin mtopology V" if "ball V" for V using that unfolding ball_def by fast
  moreover have "∃W. ball W ∧ σ ∈ W ∧ W ⊆ V" if "openin mtopology V ∧ σ ∈ V" for σ V
    unfolding ball_def using openin_mtopology that by (smt (verit, best) centre_in_mball_iff subset_iff)
  ultimately have openin_metric: "openin mtopology = arbitrary union_of ball" 
    by (simp add: openin_topology_base_unique)
  have "openin T V" if "ball V" for V
  proof -
    from that obtain σ ε where "σ ∈ carrier G ∧ V = ?B ε #> σ" 
      unfolding ball_def using mball_coset_of_norm_ball by blast
    moreover have "openin T (?B ε)" using continuous
      by (simp add: continuous_map_upper_lower_semicontinuous_lt)
    ultimately show ?thesis using open_set_translations(2) by presburger
  qed
  moreover have "∃W. ball W ∧ σ ∈ W ∧ W ⊆ V" if "neighborhood σ V" for σ V
  proof -
    from that have in_group: "σ ∈ carrier G" using open_set_in_carrier by fast
    then have "neighborhood 𝟭 (V #> inv σ)" 
      using r_coset_def open_set_translations(2) that r_inv by fastforce
    then obtain n where "U n ⊆ V #> inv σ" using neighborhood_base by presburger
    then have "?B (1/2^n) ⊆ V #> inv σ" using norm_ball_in_U by blast
    then have "?B (1/2^n) #> σ ⊆ (V #> inv σ) #> σ" unfolding r_coset_def by fast
    also have "...  = V" using in_group that open_set_in_carrier by (simp add: coset_mult_assoc)
    finally have "mball σ (1/2^n) ⊆ V" using mball_coset_of_norm_ball in_group by blast
    then show ?thesis unfolding ball_def
      by (smt (verit) centre_in_mball_iff divide_pos_pos in_group one_add_one zero_less_power zero_less_two)
  qed
  ultimately have "openin T = arbitrary union_of ball" by (simp add: openin_topology_base_unique)
  then show ?thesis using right_invariant openin_metric topology_eq by fastforce
qed                                     

corollary Birkhoff_Kakutani_iff:
  shows "metrizable_space T ⟷ Hausdorff_space T ∧ first_countable T"
  using Birkhoff_Kakutani_left Metric_space.metrizable_space_mtopology metrizable_imp_Hausdorff_space 
    metrizable_imp_first_countable unfolding left_invariant_metric_def by metis

end

end