awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : Group β
inst_5 : IsUniformGroup β
inst_6 : FunLike hom α β
inst_7 : MonoidHomClass hom α β
f : hom
h : Tendsto.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) (𝓝 1) (𝓝 1)
⊢ UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)
have this : Eq (α := α × α → β) ((fun (x : β × β) ↦ x.2 / x.1) ∘ fun (x : α × α) ↦ ((f : (a : α) → β) x.1, (f : (a : α) → β) x.2))
  fun (x : α × α) ↦ (f : (a : α) → β) (x.2 / x.1)
Tactic: have :
    ((fun x : β × β => x.2 / x.1) ∘ fun x : α × α => (f x.1, f x.2)) = fun x : α × α =>
      f (x.2 / x.1) := by ext; simp only [Function.comp_apply, map_div]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : Group β
inst_5 : IsUniformGroup β
inst_6 : FunLike hom α β
inst_7 : MonoidHomClass hom α β
f : hom
h : Tendsto.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) (𝓝 1) (𝓝 1)
this :
  Eq (α := α × α → β) ((fun (x : β × β) ↦ x.2 / x.1) ∘ fun (x : α × α) ↦ ((f : (a : α) → β) x.1, (f : (a : α) → β) x.2))
    fun (x : α × α) ↦ (f : (a : α) → β) (x.2 / x.1)
⊢ UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)
have rw : Tendsto.{u_1, u_2} (β := β) (fun (x : α × α) ↦ (f : (a : α) → β) (x.2 / x.1))
  (comap (β := α) (fun (x : α × α) ↦ x.2 / x.1) (𝓝 1)) (𝓝 1)
Tactic: rw [UniformContinuous, uniformity_eq_comap_nhds_one α, uniformity_eq_comap_nhds_one β,
    tendsto_comap_iff, this]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : DiscreteTopology β
inst_5 : Group β
inst_6 : IsUniformGroup β
inst_7 : FunLike hom α β
inst_8 : MonoidHomClass hom α β
f : hom
⊢ UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) ↔
    IsOpen[inst.toTopologicalSpace] (↑(MonoidHom.ker (↑f : α →* β)) : Set α)
have refine_1 : ∀ (hf : UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)),
  IsOpen[inst.toTopologicalSpace] (↑(MonoidHom.ker (↑f : α →* β)) : Set α)
Tactic: refine ⟨fun hf => ?_, fun hf => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : DiscreteTopology β
inst_5 : Group β
inst_6 : IsUniformGroup β
inst_7 : FunLike hom α β
inst_8 : MonoidHomClass hom α β
f : hom
refine_1 :
  ∀ (hf : UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)),
    IsOpen[inst.toTopologicalSpace] (↑(MonoidHom.ker (↑f : α →* β)) : Set α)
⊢ UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) ↔
    IsOpen[inst.toTopologicalSpace] (↑(MonoidHom.ker (↑f : α →* β)) : Set α)
have refine_2 : ∀ (hf : IsOpen[inst.toTopologicalSpace] (↑(MonoidHom.ker (↑f : α →* β)) : Set α)),
  UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)
Tactic: refine ⟨fun hf => ?_, fun hf => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : DiscreteTopology β
inst_5 : Group β
inst_6 : IsUniformGroup β
inst_7 : FunLike hom α β
inst_8 : MonoidHomClass hom α β
f : hom
hf : IsOpen[inst.toTopologicalSpace] (↑(MonoidHom.ker (↑f : α →* β)) : Set α)
⊢ UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)
have refine_2 : ContinuousAt.{u_1, u_2} (X := α) (Y := β) (⇑f : (a : α) → β) 1
Tactic: apply uniformContinuous_of_continuousAt_one
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : DiscreteTopology β
inst_5 : Group β
inst_6 : IsUniformGroup β
inst_7 : FunLike hom α β
inst_8 : MonoidHomClass hom α β
f : hom
hf : IsOpen[inst.toTopologicalSpace] (↑(MonoidHom.ker (↑f : α →* β)) : Set α)
⊢ ContinuousAt.{u_1, u_2} (X := α) (Y := β) (⇑f : (a : α) → β) 1
have refine_2 : ∀ᶠ (x : α) in 𝓝 1, Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) (1 : β)
Tactic: rw [ContinuousAt, nhds_discrete β, map_one, tendsto_pure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : Group β
inst_5 : IsUniformGroup β
inst_6 : FunLike hom α β
inst_7 : MonoidHomClass hom α β
f : hom
h : Continuous[inst.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑f : (a : α) → β)
this :
  Tendsto.{u_1, u_2} (α := α) (β := β) ((⇑f : (a : α) → β) : (a : α) → β) (𝓝 1) (𝓝 ((f : (a : α) → β) 1) : Filter β)
⊢ Tendsto.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) (𝓝 1) (𝓝 1)
have rwa : ∀ (this : Tendsto.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) (𝓝 1) (𝓝 1)),
  Tendsto.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) (𝓝 1) (𝓝 1)
Tactic: rwa [map_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
U : Set G
H : Membership.mem (γ := Filter G) (𝓝 1) U
⊢ Membership.mem (γ := Filter G)
    (map (fun (p : G × G) ↦ p.2 * p.1⁻¹)
      (Filter.lift' (α := G × G) (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1)) fun (s : Set (G × G)) ↦
        SetRel.comp s s))
    U
have rcases : ∀ (V : Set G) (V_nhds : Membership.mem (γ := Filter G) (𝓝 1) V) (V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U),
  Membership.mem (γ := Filter G)
    (map (fun (p : G × G) ↦ p.2 * p.1⁻¹)
      (Filter.lift' (α := G × G) (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1)) fun (s : Set (G × G)) ↦
        SetRel.comp s s))
    U
Tactic: rcases exists_nhds_one_split H with ⟨V, V_nhds, V_mul⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
U : Set G
H : Membership.mem (γ := Filter G) (𝓝 1) U
V : Set G
V_nhds : Membership.mem (γ := Filter G) (𝓝 1) V
V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U
⊢ Membership.mem (γ := Filter G)
    (map (fun (p : G × G) ↦ p.2 * p.1⁻¹)
      (Filter.lift' (α := G × G) (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1)) fun (s : Set (G × G)) ↦
        SetRel.comp s s))
    U
have refine : Subset (α := Set (G × G))
  (SetRel.comp (β := G) ((fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V) ((fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V))
  ((fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' U)
Tactic: refine mem_map.2 (mem_of_superset (mem_lift' <| preimage_mem_comap V_nhds) ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
U : Set G
H : Membership.mem (γ := Filter G) (𝓝 1) U
⊢ Membership.mem (γ := Filter G)
    (map (fun (p : G × G) ↦ p.1⁻¹ * p.2)
      (Filter.lift' (α := G × G) (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1)) fun (s : Set (G × G)) ↦
        SetRel.comp s s))
    U
have rcases : ∀ (V : Set G) (V_nhds : Membership.mem (γ := Filter G) (𝓝 1) V) (V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U),
  Membership.mem (γ := Filter G)
    (map (fun (p : G × G) ↦ p.1⁻¹ * p.2)
      (Filter.lift' (α := G × G) (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1)) fun (s : Set (G × G)) ↦
        SetRel.comp s s))
    U
Tactic: rcases exists_nhds_one_split H with ⟨V, V_nhds, V_mul⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
U : Set G
H : Membership.mem (γ := Filter G) (𝓝 1) U
V : Set G
V_nhds : Membership.mem (γ := Filter G) (𝓝 1) V
V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U
⊢ Membership.mem (γ := Filter G)
    (map (fun (p : G × G) ↦ p.1⁻¹ * p.2)
      (Filter.lift' (α := G × G) (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1)) fun (s : Set (G × G)) ↦
        SetRel.comp s s))
    U
have refine : Subset (α := Set (G × G))
  (SetRel.comp (β := G) ((fun (p : G × G) ↦ p.1⁻¹ * p.2) ⁻¹' V) ((fun (p : G × G) ↦ p.1⁻¹ * p.2) ⁻¹' V))
  ((fun (p : G × G) ↦ p.1⁻¹ * p.2) ⁻¹' U)
Tactic: refine mem_map.2 (mem_of_superset (mem_lift' <| preimage_mem_comap V_nhds) ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ IsUniformGroup G
have uniformContinuous_div : UniformContinuous (β := G) fun (p : G × G) ↦ p.1 / p.2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ Eq.{u_1 + 1} (α := (x : (G × G) × G × G) → G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
have h : ∀ (x : (G × G) × G × G),
  x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹) =
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
x : (G × G) × G × G
⊢ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹) =
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) x
have h : x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹) = x.1.2 * x.1.1⁻¹ * (x.2.1 * x.2.2⁻¹)
Tactic: simp only [Function.comp_apply, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
x : (G × G) × G × G
⊢ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹) = x.1.2 * x.1.1⁻¹ * (x.2.1 * x.2.2⁻¹)
have h : x.1.2 * (x.1.1⁻¹ * x.2.1 * x.2.2⁻¹) = x.1.2 * x.1.1⁻¹ * (x.2.1 * x.2.2⁻¹)
Tactic: rw [mul_assoc, mul_comm x.2.2⁻¹, mul_comm x.2.1]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ UniformContinuous (β := G) fun (p : G × G) ↦ p.1 / p.2
have this : Eq.{u_1 + 1} (α := (x : (G × G) × G × G) → G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
  ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
Tactic: have : (fun (x : (G × G) × (G × G)) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹)) =
    (fun (p : G × G) ↦ p.1 * p.2⁻¹)
      ∘ (fun (p : (G × G) × (G × G)) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) := by
    ext x
    simp only [Function.comp_apply, mul_inv_rev, inv_inv]
    rw [mul_assoc, mul_comm x.2.2⁻¹, mul_comm x.2.1]
    simp [mul_assoc]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
this :
  Eq.{u_1 + 1} (α := (x : (G × G) × G × G) → G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
⊢ UniformContinuous (β := G) fun (p : G × G) ↦ p.1 / p.2
have uniformContinuous_div : Tendsto (β := G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
  (comap (β := G × G) (fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) (𝓝 (1, 1))) (𝓝 1)
Tactic: simp only [UniformContinuous, div_eq_mul_inv, uniformity_prod_eq_prod,
    uniformity_eq_comap_nhds_one', prod_comap_comap_eq, ← nhds_prod_eq, tendsto_comap_iff,
    Function.comp_def, mul_inv_rev, inv_inv, tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
this :
  Eq.{u_1 + 1} (α := (x : (G × G) × G × G) → G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
⊢ Tendsto (β := G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
    (comap (β := G × G) (fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) (𝓝 (1, 1))) (𝓝 1)
have uniformContinuous_div : Tendsto.{u_1, u_1} (α := (G × G) × G × G) (β := G)
  ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
  (comap (β := G × G) (fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) (𝓝 (1, 1))) (𝓝 1)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
this :
  Eq.{u_1 + 1} (α := (x : (G × G) × G × G) → G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
⊢ Tendsto.{u_1, u_1} (α := (G × G) × G × G) (β := G)
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
    (comap (β := G × G) (fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) (𝓝 (1, 1))) (𝓝 1)
have apply : Tendsto (β := G) (fun (p : G × G) ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 1)
Tactic: apply Tendsto.comp ?_ tendsto_comap
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
this :
  Eq.{u_1 + 1} (α := (x : (G × G) × G × G) → G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
⊢ Tendsto (β := G) (fun (p : G × G) ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 1)
have nth_rewrite : Tendsto (fun (p : G × G) ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 (HMul.hMul (α := G) 1 1⁻¹))
Tactic: nth_rewrite 3 [show (1 : G) = 1 * 1⁻¹ by simp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
G : Type u_2
u : UniformSpace G
inst : Group G
inst_1 : IsUniformGroup G
⊢ IsTopologicalGroup.rightUniformSpace G = u
have h : 𝓤 G = 𝓤 G
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
G : Type u_2
u : UniformSpace G
inst : Group G
inst_1 : IsUniformGroup G
⊢ 𝓤 G = 𝓤 G
have h : comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1) = 𝓤 G
Tactic: rw [uniformity_eq_comap_nhds_one' G, uniformity_eq_comap_mul_inv_nhds_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
G : Type u_2
u : UniformSpace G
inst : Group G
inst_1 : IsUniformGroup G
h : comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1) = 𝓤 G
⊢ 𝓤 G = 𝓤 G
have h₁ : Eq.{u_2 + 1} (α := Filter (G × G)) (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1))
  (comap (β := G) (fun (x : G × G) ↦ x.2 * x.1⁻¹) (𝓝 1))
Tactic: rw [uniformity_eq_comap_nhds_one' G, uniformity_eq_comap_mul_inv_nhds_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
H K : Subgroup G
hHK : H ≤ K
⊢ ∀ (s : Set ↥H),
    IsOpen[instTopologicalSpaceSubtype] ((⇑(subgroupOfEquivOfLe hHK) : (a : ↥(H.subgroupOf K)) → ↥H) ⁻¹' s) ↔
      IsOpen[instTopologicalSpaceSubtype] s
have simp : ∀ (s : Set ↥H),
  (∃ (a : Set G),
      IsOpen[inst_1] a ∧
        Eq (α := Set { x : ↥K // x ∈ (↑(H.subgroupOf K) : Set ↥K) })
          (Subtype.val (p := fun (x : ↥K) ↦ x ∈ (↑(H.subgroupOf K) : Set ↥K)) ⁻¹'
            Subtype.val (p := fun (x : G) ↦ x ∈ (↑K : Set G)) ⁻¹' a)
          ((⇑{ toFun := fun (g : ↥(H.subgroupOf K)) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ H) (↑(↑g : ↥K) : G) sorry,
                  invFun := fun (g : ↥H) ↦
                    Subtype.mk (p := fun (x : ↥K) ↦ x ∈ H.subgroupOf K)
                      (Subtype.mk (p := fun (x : G) ↦ x ∈ K) (↑g : G) sorry) sorry,
                  left_inv := sorry, right_inv := sorry, map_mul' := sorry : ↥(H.subgroupOf K) ≃* ↥H } :
              (a : ↥(H.subgroupOf K)) → ↥H) ⁻¹'
            s)) ↔
    ∃ (t : Set G), IsOpen[inst_1] t ∧ Subtype.val (p := fun (x : G) ↦ x ∈ (↑H : Set G)) ⁻¹' t = s
Tactic: simp only [subgroupOfEquivOfLe, Topology.IsInducing.subtypeVal.isOpen_iff,
      exists_exists_and_eq_and]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
inst_4 : H.FiniteIndex
⊢ DiscreteTopology.{u_1} ↥H ↔ DiscreteTopology G
have refine : ∀ (hH : DiscreteTopology.{u_1} ↥H), DiscreteTopology G
Tactic: refine ⟨fun hH ↦ ?_, fun hG ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
inst_4 : H.FiniteIndex
hH : DiscreteTopology.{u_1} ↥H
this : IsOpen[inst_1] (↑H : Set G)
⊢ DiscreteTopology G
have rw : IsOpen[inst_1] {1}
Tactic: rw [discreteTopology_iff_isOpen_singleton_one, isOpen_singleton_iff_nhds_eq_pure,
        ← H.coe_one, ← this.isOpenEmbedding_subtypeVal.map_nhds_eq, nhds_discrete, map_pure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
inst_4 : H.FiniteIndex
hH : DiscreteTopology.{u_1} ↥H
this : IsOpen[inst_1] (↑H : Set G)
rw : IsOpen[inst_1] {1}
⊢ DiscreteTopology G
have rw₁ : Eq.{u_1 + 1} (α := Filter G) (𝓝 1) (pure 1)
Tactic: rw [discreteTopology_iff_isOpen_singleton_one, isOpen_singleton_iff_nhds_eq_pure,
        ← H.coe_one, ← this.isOpenEmbedding_subtypeVal.map_nhds_eq, nhds_discrete, map_pure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
inst_4 : H.FiniteIndex
hH : DiscreteTopology.{u_1} ↥H
this : IsOpen[inst_1] (↑H : Set G)
rw : IsOpen[inst_1] {1}
rw₁ : Eq.{u_1 + 1} (α := Filter G) (𝓝 1) (pure 1)
⊢ DiscreteTopology G
have rw₂ : Eq.{u_1 + 1} (α := Filter G) (𝓝 (↑1 : G)) (pure (↑1 : G))
Tactic: rw [discreteTopology_iff_isOpen_singleton_one, isOpen_singleton_iff_nhds_eq_pure,
        ← H.coe_one, ← this.isOpenEmbedding_subtypeVal.map_nhds_eq, nhds_discrete, map_pure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
inst_4 : H.FiniteIndex
hH : DiscreteTopology.{u_1} ↥H
this : IsOpen[inst_1] (↑H : Set G)
rw : IsOpen[inst_1] {1}
rw₁ : Eq.{u_1 + 1} (α := Filter G) (𝓝 1) (pure 1)
rw₂ : Eq.{u_1 + 1} (α := Filter G) (𝓝 (↑1 : G)) (pure (↑1 : G))
⊢ DiscreteTopology G
have rw₃ : Eq.{u_1 + 1} (α := Filter G)
  (Filter.map (α := { x : G // x ∈ (↑H : Set G) }) (Subtype.val (p := fun (x : G) ↦ x ∈ (↑H : Set G))) (𝓝 1))
  (pure (↑1 : G))
Tactic: rw [discreteTopology_iff_isOpen_singleton_one, isOpen_singleton_iff_nhds_eq_pure,
        ← H.coe_one, ← this.isOpenEmbedding_subtypeVal.map_nhds_eq, nhds_discrete, map_pure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
inst_4 : H.FiniteIndex
hH : DiscreteTopology.{u_1} ↥H
this : IsOpen[inst_1] (↑H : Set G)
rw : IsOpen[inst_1] {1}
rw₁ : Eq.{u_1 + 1} (α := Filter G) (𝓝 1) (pure 1)
rw₂ : Eq.{u_1 + 1} (α := Filter G) (𝓝 (↑1 : G)) (pure (↑1 : G))
rw₃ :
  Eq.{u_1 + 1} (α := Filter G)
    (Filter.map (α := { x : G // x ∈ (↑H : Set G) }) (Subtype.val (p := fun (x : G) ↦ x ∈ (↑H : Set G))) (𝓝 1))
    (pure (↑1 : G))
⊢ DiscreteTopology G
have rw₄ : Eq.{u_1 + 1} (α := Filter G)
  (Filter.map (α := { x : G // x ∈ (↑H : Set G) }) (Subtype.val (p := fun (x : G) ↦ x ∈ (↑H : Set G))) (pure 1))
  (pure (↑1 : G))
Tactic: rw [discreteTopology_iff_isOpen_singleton_one, isOpen_singleton_iff_nhds_eq_pure,
        ← H.coe_one, ← this.isOpenEmbedding_subtypeVal.map_nhds_eq, nhds_discrete, map_pure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
inst_4 : H.FiniteIndex
hH : DiscreteTopology.{u_1} ↥H
this : IsOpen[inst_1] (↑H : Set G)
rw : IsOpen[inst_1] {1}
rw₁ : Eq.{u_1 + 1} (α := Filter G) (𝓝 1) (pure 1)
rw₂ : Eq.{u_1 + 1} (α := Filter G) (𝓝 (↑1 : G)) (pure (↑1 : G))
rw₃ :
  Eq.{u_1 + 1} (α := Filter G)
    (Filter.map (α := { x : G // x ∈ (↑H : Set G) }) (Subtype.val (p := fun (x : G) ↦ x ∈ (↑H : Set G))) (𝓝 1))
    (pure (↑1 : G))
rw₄ :
  Eq.{u_1 + 1} (α := Filter G)
    (Filter.map (α := { x : G // x ∈ (↑H : Set G) }) (Subtype.val (p := fun (x : G) ↦ x ∈ (↑H : Set G))) (pure 1))
    (pure (↑1 : G))
⊢ DiscreteTopology G
have rw₅ : Eq.{u_1 + 1} (α := Filter G) (pure (↑1 : G)) (pure (↑1 : G))
Tactic: rw [discreteTopology_iff_isOpen_singleton_one, isOpen_singleton_iff_nhds_eq_pure,
        ← H.coe_one, ← this.isOpenEmbedding_subtypeVal.map_nhds_eq, nhds_discrete, map_pure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
inst_4 : H.FiniteIndex
hH : DiscreteTopology.{u_1} ↥H
⊢ DiscreteTopology G
have suffices : IsOpen[inst_1] (↑H : Set G)
Tactic: suffices IsOpen (H : Set G) by
    rw [discreteTopology_iff_isOpen_singleton_one, isOpen_singleton_iff_nhds_eq_pure,
        ← H.coe_one, ← this.isOpenEmbedding_subtypeVal.map_nhds_eq, nhds_discrete, map_pure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H K : Subgroup G
hHK : H ≤ K
inst_4 : H.IsFiniteRelIndex K
⊢ DiscreteTopology.{u_1} ↥H ↔ DiscreteTopology.{u_1} ↥K
have this : (H.subgroupOf K).FiniteIndex
Tactic: haveI : (H.subgroupOf K).FiniteIndex := IsFiniteRelIndex.to_finiteIndex_subgroupOf
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H K : Subgroup G
hHK : H ≤ K
inst_4 : H.IsFiniteRelIndex K
this : (H.subgroupOf K).FiniteIndex
⊢ DiscreteTopology.{u_1} ↥H ↔ DiscreteTopology.{u_1} ↥K
have rw : DiscreteTopology.{u_1} ↥(H.subgroupOf K) ↔ DiscreteTopology.{u_1} ↥K
Tactic: rw [← (subgroupOfContinuousMulEquivOfLe hHK).discreteTopology_iff,
    discreteTopology_iff_of_finiteIndex]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H K : Subgroup G
hHK : H ≤ K
inst_4 : H.IsFiniteRelIndex K
this : (H.subgroupOf K).FiniteIndex
rw : DiscreteTopology.{u_1} ↥(H.subgroupOf K) ↔ DiscreteTopology.{u_1} ↥K
⊢ DiscreteTopology.{u_1} ↥H ↔ DiscreteTopology.{u_1} ↥K
have rw₁ : DiscreteTopology.{u_1} ↥K ↔ DiscreteTopology.{u_1} ↥K
Tactic: rw [← (subgroupOfContinuousMulEquivOfLe hHK).discreteTopology_iff,
    discreteTopology_iff_of_finiteIndex]