awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Quotient (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
N : Subgroup G
inst_3 : N.Normal
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace N] fun (p : (G ⧸ N) × G ⧸ N) ↦ p.1 * p.2
have rw : Continuous[instTopologicalSpaceProd, instTopologicalSpace N] ((fun (p : (G ⧸ N) × G ⧸ N) ↦ p.1 * p.2) ∘ Prod.map mk mk)
Tactic: rw [← (isOpenQuotientMap_mk.prodMap isOpenQuotientMap_mk).continuous_comp_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Quotient (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Subgroup G
hH : IsCompact (↑H : Set G)
t : Set G
ht : IsClosed[inst] t
⊢ IsClosed[instTopologicalSpace H] (mk '' t)
have rw : IsClosed[inst] (t * (↑H : Set G))
Tactic: rw [← (isQuotientMap_mk H).isClosed_preimage, preimage_image_mk_eq_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : DivInvMonoid G
inst_1 : TopologicalSpace G
x y : G
⊢ (MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x) ↔ MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x
have simp_rw : ClusterPt x (map (fun (x : ℤ) ↦ y ^ x) atTop) ↔ ClusterPt x (map (fun (x : ℕ) ↦ y ^ x) atTop)
Tactic: simp_rw [MapClusterPt, ← Nat.map_cast_int_atTop, map_map, comp_def, zpow_natCast]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : DivInvMonoid G
inst_1 : TopologicalSpace G
x y : G
simp_rw : ClusterPt x (map (fun (x : ℤ) ↦ y ^ x) atTop) ↔ ClusterPt x (map (fun (x : ℕ) ↦ y ^ x) atTop)
⊢ (MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x) ↔ MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x
have simp_rw₁ : ClusterPt x (map (fun (x : ℤ) ↦ y ^ x) (map Nat.cast atTop)) ↔ ClusterPt x (map (fun (x : ℕ) ↦ y ^ x) atTop)
Tactic: simp_rw [MapClusterPt, ← Nat.map_cast_int_atTop, map_map, comp_def, zpow_natCast]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : DivInvMonoid G
inst_1 : TopologicalSpace G
x y : G
simp_rw : ClusterPt x (map (fun (x : ℤ) ↦ y ^ x) atTop) ↔ ClusterPt x (map (fun (x : ℕ) ↦ y ^ x) atTop)
simp_rw₁ : ClusterPt x (map (fun (x : ℤ) ↦ y ^ x) (map Nat.cast atTop)) ↔ ClusterPt x (map (fun (x : ℕ) ↦ y ^ x) atTop)
⊢ (MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x) ↔ MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x
have simp_rw₂ : ClusterPt x (map ((fun (x : ℤ) ↦ y ^ x) ∘ Nat.cast) atTop) ↔ ClusterPt x (map (fun (x : ℕ) ↦ y ^ x) atTop)
Tactic: simp_rw [MapClusterPt, ← Nat.map_cast_int_atTop, map_map, comp_def, zpow_natCast]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : DivInvMonoid G
inst_1 : TopologicalSpace G
x y : G
simp_rw : ClusterPt x (map (fun (x : ℤ) ↦ y ^ x) atTop) ↔ ClusterPt x (map (fun (x : ℕ) ↦ y ^ x) atTop)
simp_rw₁ : ClusterPt x (map (fun (x : ℤ) ↦ y ^ x) (map Nat.cast atTop)) ↔ ClusterPt x (map (fun (x : ℕ) ↦ y ^ x) atTop)
simp_rw₂ : ClusterPt x (map ((fun (x : ℤ) ↦ y ^ x) ∘ Nat.cast) atTop) ↔ ClusterPt x (map (fun (x : ℕ) ↦ y ^ x) atTop)
⊢ (MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x) ↔ MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x
have simp_rw₃ : ClusterPt x (map (fun (x : ℕ) ↦ HPow.hPow (β := ℤ) y (↑x : ℤ)) atTop) ↔ ClusterPt x (map (fun (x : ℕ) ↦ y ^ x) atTop)
Tactic: simp_rw [MapClusterPt, ← Nat.map_cast_int_atTop, map_map, comp_def, zpow_natCast]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
⊢ MapClusterPt (x ^ m) atTop fun (x_1 : ℕ) ↦ x ^ x_1
have obtain : ∀ (y : G) (hy : MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1), MapClusterPt (x ^ m) atTop fun (x_1 : ℕ) ↦ x ^ x_1
Tactic: obtain ⟨y, hy⟩ : ∃ y, MapClusterPt y atTop (x ^ · : ℤ → G) :=
    exists_clusterPt_of_compactSpace _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1
⊢ MapClusterPt (x ^ m) atTop fun (x_1 : ℕ) ↦ x ^ x_1
have rw : MapClusterPt (x ^ m) atTop fun (x_1 : ℤ) ↦ x ^ x_1
Tactic: rw [← mapClusterPt_atTop_zpow_iff_pow]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1
⊢ MapClusterPt (x ^ m) (Filter.curry atTop atTop)
    (HasUncurry.uncurry (α := (a b : ℤ) → G) fun (a b : ℤ) ↦ x ^ (m + b - a))
have this : ContinuousAt (Y := G) (fun (yz : G × G) ↦ x ^ m * yz.2 / yz.1) (y, y)
Tactic: have : ContinuousAt (fun yz ↦ x ^ m * yz.2 / yz.1) (y, y) := by fun_prop
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1
⊢ MapClusterPt (x ^ m) atTop fun (x_1 : ℤ) ↦ x ^ x_1
have H : MapClusterPt (x ^ m) (Filter.curry atTop atTop)
  (HasUncurry.uncurry (α := (a b : ℤ) → G) fun (a b : ℤ) ↦ x ^ (m + b - a))
Tactic: have H : MapClusterPt (x ^ m) (atTop.curry atTop) ↿(fun a b ↦ x ^ (m + b - a)) := by
    have : ContinuousAt (fun yz ↦ x ^ m * yz.2 / yz.1) (y, y) := by fun_prop
    simpa only [comp_def, ← zpow_sub, ← zpow_add, div_eq_mul_inv, Prod.map, mul_inv_cancel_right]
      using (hy.curry_prodMap hy).continuousAt_comp this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1
H :
  MapClusterPt (x ^ m) (Filter.curry atTop atTop)
    (HasUncurry.uncurry (α := (a b : ℤ) → G) fun (a b : ℤ) ↦ x ^ (m + b - a))
⊢ MapClusterPt (x ^ m) atTop fun (x_1 : ℤ) ↦ x ^ x_1
have suffices : Tendsto (HasUncurry.uncurry (α := (a b : ℤ) → ℤ) fun (a b : ℤ) ↦ m + b - a) (Filter.curry atTop atTop) atTop
Tactic: suffices Tendsto ↿(fun a b ↦ m + b - a) (atTop.curry atTop) atTop from H.of_comp this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1
H :
  MapClusterPt (x ^ m) (Filter.curry atTop atTop)
    (HasUncurry.uncurry (α := (a b : ℤ) → G) fun (a b : ℤ) ↦ x ^ (m + b - a))
⊢ Tendsto (HasUncurry.uncurry (α := (a b : ℤ) → ℤ) fun (a b : ℤ) ↦ m + b - a) (Filter.curry atTop atTop) atTop
have refine : ∀ (a : ℤ), Tendsto (β := ℤ) (fun (b : ℤ) ↦ m + b - a) atTop atTop
Tactic: refine Tendsto.curry <| .of_forall fun a ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x y : G
⊢ [MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x, MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x,
      Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℕ) ↦ y ^ x)) x,
      Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℤ) ↦ y ^ x)) x].TFAE
have tfae_2_iff_1 : (MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x) ↔ MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x
Tactic: tfae_have 2 ↔ 1 := mapClusterPt_atTop_zpow_iff_pow
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x) ↔ MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x
⊢ ∀ (a : Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℕ) ↦ y ^ x)) x),
    Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℤ) ↦ y ^ x)) x
have refine : ∀ (h : Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℕ) ↦ y ^ x)) x) (n : ℕ),
  Membership.mem (γ := Set G) (range fun (x : ℤ) ↦ y ^ x) (y ^ n)
Tactic: refine fun h ↦ closure_mono (range_subset_iff.2 fun n ↦ ?_) h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x) ↔ MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x
⊢ [MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x, MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x,
      Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℕ) ↦ y ^ x)) x,
      Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℤ) ↦ y ^ x)) x].TFAE
have tfae_3_to_4 : ∀ (a : Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℕ) ↦ y ^ x)) x),
  Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℤ) ↦ y ^ x)) x
Tactic: tfae_have 3 → 4 := by
    refine fun h ↦ closure_mono (range_subset_iff.2 fun n ↦ ?_) h
    exact ⟨n, zpow_natCast _ _⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x) ↔ MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x
tfae_3_to_4 :
  ∀ (a : Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℕ) ↦ y ^ x)) x),
    Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℤ) ↦ y ^ x)) x
⊢ ∀ (a : Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℤ) ↦ y ^ x)) x),
    MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x
have refine : ∀ (h : Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℤ) ↦ y ^ x)) x),
  Subset.{u_1} (α := Set G) (range fun (x : ℤ) ↦ y ^ x) {x : G | ClusterPt x (map (fun (x : ℕ) ↦ y ^ x) atTop)}
Tactic: refine fun h ↦ closure_minimal ?_ isClosed_setOf_clusterPt h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x) ↔ MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x
tfae_3_to_4 :
  ∀ (a : Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℕ) ↦ y ^ x)) x),
    Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℤ) ↦ y ^ x)) x
⊢ [MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x, MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x,
      Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℕ) ↦ y ^ x)) x,
      Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℤ) ↦ y ^ x)) x].TFAE
have tfae_4_to_1 : ∀ (a : Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℤ) ↦ y ^ x)) x),
  MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x
Tactic: tfae_have 4 → 1 := by
    refine fun h ↦ closure_minimal ?_ isClosed_setOf_clusterPt h
    exact range_subset_iff.2 (mapClusterPt_self_zpow_atTop_pow _)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x) ↔ MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x
tfae_3_to_4 :
  ∀ (a : Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℕ) ↦ y ^ x)) x),
    Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℤ) ↦ y ^ x)) x
tfae_4_to_1 :
  ∀ (a : Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℤ) ↦ y ^ x)) x),
    MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x
⊢ ∀ (a : MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x),
    Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℕ) ↦ y ^ x)) x
have rw : ∀ (a : MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x), ClusterPt x (𝓟 (range fun (x : ℕ) ↦ y ^ x))
Tactic: rw [mem_closure_iff_clusterPt]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x) ↔ MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x
tfae_3_to_4 :
  ∀ (a : Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℕ) ↦ y ^ x)) x),
    Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℤ) ↦ y ^ x)) x
tfae_4_to_1 :
  ∀ (a : Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℤ) ↦ y ^ x)) x),
    MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x
⊢ [MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x, MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x,
      Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℕ) ↦ y ^ x)) x,
      Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℤ) ↦ y ^ x)) x].TFAE
have tfae_1_to_3 : ∀ (a : MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x),
  Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℕ) ↦ y ^ x)) x
Tactic: tfae_have 1 → 3 := by
    rw [mem_closure_iff_clusterPt]
    exact (ClusterPt.mono · (le_principal_iff.2 range_mem_map))
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
⊢ Eq.{u_1 + 1} (α := Set G) (closure[inst_1] (range fun (x_1 : ℤ) ↦ x ^ x_1))
    (closure[inst_1] (range fun (x_1 : ℕ) ↦ x ^ x_1))
have h : ∀ (y : G),
  Membership.mem (γ := Set G) (closure[inst_1] (range fun (x_1 : ℤ) ↦ x ^ x_1)) y ↔
    Membership.mem (γ := Set G) (closure[inst_1] (range fun (x_1 : ℕ) ↦ x ^ x_1)) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
s : Set G
⊢ Eq (α := Submonoid G) (Submonoid.topologicalClosure (Subgroup.toSubmonoid (Subgroup.closure s)))
    (Submonoid.topologicalClosure (Submonoid.closure s))
have refine : LE.le (α := Submonoid G) (Submonoid.topologicalClosure (Subgroup.toSubmonoid (Subgroup.closure s)))
  (Submonoid.topologicalClosure (Submonoid.closure s))
Tactic: refine le_antisymm ?_ (closure_mono <| Subgroup.le_closure_toSubmonoid _)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
s : Set G
⊢ LE.le (α := Submonoid G) (Submonoid.topologicalClosure (Subgroup.toSubmonoid (Subgroup.closure s)))
    (Submonoid.topologicalClosure (Submonoid.closure s))
have refine : LE.le (α := Submonoid G) (Subgroup.toSubmonoid (Subgroup.closure s))
  (Submonoid.topologicalClosure (Submonoid.closure s))
Tactic: refine Submonoid.topologicalClosure_minimal _ ?_ isClosed_closure
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
s : Set G
⊢ LE.le (α := Submonoid G) (Subgroup.toSubmonoid (Subgroup.closure s))
    (Submonoid.topologicalClosure (Submonoid.closure s))
have rw : s ∪ s⁻¹ ⊆ (↑(Submonoid.topologicalClosure (Submonoid.closure s)) : Set G)
Tactic: rw [Subgroup.closure_toSubmonoid, Submonoid.closure_le]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
s : Set G
⊢ s ∪ s⁻¹ ⊆ (↑(Submonoid.topologicalClosure (Submonoid.closure s)) : Set G)
have refine : ∀ (x : G) (hx : x ∈ s⁻¹), x ∈ (↑(Submonoid.topologicalClosure (Submonoid.closure s)) : Set G)
Tactic: refine union_subset (Submonoid.subset_closure.trans subset_closure) fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
s : Set G
x : G
hx : x ∈ s⁻¹
⊢ x ∈ (↑(Submonoid.topologicalClosure (Submonoid.closure s)) : Set G)
have refine : x ∈ closure[inst_1] (↑(Submonoid.powers x⁻¹) : Set G)
Tactic: refine closure_mono (Submonoid.powers_le.2 (Submonoid.subset_closure <| Set.mem_inv.1 hx)) ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.SubmonoidClosure (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
s : Set G
x : G
hx : x ∈ s⁻¹
⊢ x ∈ closure[inst_1] (↑(Submonoid.powers x⁻¹) : Set G)
have rw : Membership.mem (γ := Subgroup G) (Subgroup.topologicalClosure (Subgroup.zpowers x⁻¹)) x⁻¹
Tactic: rw [Submonoid.coe_powers, ← closure_range_zpow_eq_pow, ← Subgroup.coe_zpowers,
    ← Subgroup.topologicalClosure_coe, SetLike.mem_coe, ← inv_mem_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.TopologicalAbelianization (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
x y : G_ab G
a b : G
⊢ Membership.mem (γ := Subgroup G) (Subgroup.topologicalClosure (commutator G))
    (HMul.hMul (α := G) ((fun (x1 x2 : G) ↦ x1 * x2) a b)⁻¹ ((fun (x1 x2 : G) ↦ x1 * x2) b a))
have h : (a * b)⁻¹ * (b * a) = ⁅b⁻¹, a⁻¹⁆
Tactic: have h : (a * b)⁻¹ * (b * a) = ⁅b⁻¹, a⁻¹⁆ := by group
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.TopologicalAbelianization (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
x y : G_ab G
a b : G
h : (a * b)⁻¹ * (b * a) = ⁅b⁻¹, a⁻¹⁆
⊢ Membership.mem (γ := Subgroup G) (Subgroup.topologicalClosure (commutator G))
    (HMul.hMul (α := G) ((fun (x1 x2 : G) ↦ x1 * x2) a b)⁻¹ ((fun (x1 x2 : G) ↦ x1 * x2) b a))
have rw : Membership.mem (γ := Subgroup G) (Subgroup.topologicalClosure (commutator G)) ⁅b⁻¹, a⁻¹⁆
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : MonoidWithZero M
inst_2 : Zero α
inst_3 : MulActionWithZero M α
inst_4 : UniformContinuousConstSMul M α
r : M
⊢ HSMul.hSMul (β := Completion α) r 0 = 0
have rw : HSMul.hSMul (β := Completion α) r (↑0 : Completion α) = (↑0 : Completion α)
Tactic: rw [← coe_zero, ← coe_smul, MulActionWithZero.smul_zero r]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : MonoidWithZero M
inst_2 : Zero α
inst_3 : MulActionWithZero M α
inst_4 : UniformContinuousConstSMul M α
r : M
rw : HSMul.hSMul (β := Completion α) r (↑0 : Completion α) = (↑0 : Completion α)
⊢ HSMul.hSMul (β := Completion α) r 0 = 0
have rw₁ : Eq (α := Completion α) (↑(HSMul.hSMul (β := α) r 0) : Completion α) (↑0 : Completion α)
Tactic: rw [← coe_zero, ← coe_smul, MulActionWithZero.smul_zero r]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : MonoidWithZero M
inst_2 : Zero α
inst_3 : MulActionWithZero M α
inst_4 : UniformContinuousConstSMul M α
r : M
rw : HSMul.hSMul (β := Completion α) r (↑0 : Completion α) = (↑0 : Completion α)
rw₁ : Eq (α := Completion α) (↑(HSMul.hSMul (β := α) r 0) : Completion α) (↑0 : Completion α)
⊢ HSMul.hSMul (β := Completion α) r 0 = 0
have rw₂ : Eq.{u_3 + 1} (α := Completion α) (↑0 : Completion α) (↑0 : Completion α)
Tactic: rw [← coe_zero, ← coe_smul, MulActionWithZero.smul_zero r]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : MonoidWithZero M
inst_2 : Zero α
inst_3 : MulActionWithZero M α
inst_4 : UniformContinuousConstSMul M α
a : α
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := M) (β := Completion α) 0 (↑a : Completion α) = 0
have rw : Eq (α := Completion α) (↑(HSMul.hSMul.{u_1, u_3, u_3} (α := M) 0 a) : Completion α) 0
Tactic: rw [← coe_smul, zero_smul, coe_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : MonoidWithZero M
inst_2 : Zero α
inst_3 : MulActionWithZero M α
inst_4 : UniformContinuousConstSMul M α
a : α
rw : Eq (α := Completion α) (↑(HSMul.hSMul.{u_1, u_3, u_3} (α := M) 0 a) : Completion α) 0
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := M) (β := Completion α) 0 (↑a : Completion α) = 0
have rw₁ : Eq.{u_3 + 1} (α := Completion α) (↑0 : Completion α) 0
Tactic: rw [← coe_smul, zero_smul, coe_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : MonoidWithZero M
inst_2 : Zero α
inst_3 : MulActionWithZero M α
inst_4 : UniformContinuousConstSMul M α
a : α
rw : Eq (α := Completion α) (↑(HSMul.hSMul.{u_1, u_3, u_3} (α := M) 0 a) : Completion α) 0
rw₁ : Eq.{u_3 + 1} (α := Completion α) (↑0 : Completion α) 0
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := M) (β := Completion α) 0 (↑a : Completion α) = 0
have rw₂ : Eq.{u_3 + 1} (α := Completion α) 0 0
Tactic: rw [← coe_smul, zero_smul, coe_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a_1 b_1 c_1 : Completion α
a b c : α
⊢ HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α) + (↑c : Completion α) =
    (↑a : Completion α) + HAdd.hAdd (α := Completion α) (↑b : Completion α) (↑c : Completion α)
have rw_mod_cast : Eq (α := Completion α) (↑(a + b + c) : Completion α) (↑(a + (b + c)) : Completion α)
Tactic: rw_mod_cast [add_assoc]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a_1 b_1 c_1 : Completion α
a b c : α
⊢ HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α) + (↑c : Completion α) =
    (↑a : Completion α) + HAdd.hAdd (α := Completion α) (↑b : Completion α) (↑c : Completion α)
have repeat' : Eq (α := Completion α) (↑(a + b + c) : Completion α) (↑(a + (b + c)) : Completion α)
Tactic: repeat' rw_mod_cast [add_assoc]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a_1 : Completion α
a : α
⊢ HAdd.hAdd (α := Completion α) 0 (↑a : Completion α) = (↑a : Completion α)
have rw : HAdd.hAdd (α := Completion α) (↑0 : Completion α) (↑a : Completion α) = (↑a : Completion α)
Tactic: rw [← coe_zero, ← coe_add, zero_add]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a_1 : Completion α
a : α
rw : HAdd.hAdd (α := Completion α) (↑0 : Completion α) (↑a : Completion α) = (↑a : Completion α)
⊢ HAdd.hAdd (α := Completion α) 0 (↑a : Completion α) = (↑a : Completion α)
have rw₁ : Eq (α := Completion α) (↑(0 + a) : Completion α) (↑a : Completion α)
Tactic: rw [← coe_zero, ← coe_add, zero_add]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a_1 : Completion α
a : α
rw : HAdd.hAdd (α := Completion α) (↑0 : Completion α) (↑a : Completion α) = (↑a : Completion α)
rw₁ : Eq (α := Completion α) (↑(0 + a) : Completion α) (↑a : Completion α)
⊢ HAdd.hAdd (α := Completion α) 0 (↑a : Completion α) = (↑a : Completion α)
have rw₂ : Eq (α := Completion α) (↑a : Completion α) (↑a : Completion α)
Tactic: rw [← coe_zero, ← coe_add, zero_add]