awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits (goal)
Goal:
P : ProfiniteGrp.{u}
this :
  IsClosed (X :=
    (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u))
    (Set.range (ι :=
      (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      (⇑(Hom.hom P.toLimit) : (a : (↑P.toProfinite.toTop : Type u)) → (↑(limit P.diagram).toProfinite.toTop : Type u)))
rw :
  Eq (α :=
    Set
      (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u))
    (Set.range (ι :=
      (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      (⇑(Hom.hom P.toLimit) : (a : (↑P.toProfinite.toTop : Type u)) → (↑(limit P.diagram).toProfinite.toTop : Type u)))
    Set.univ
rw₁ :
  Eq (α :=
    Set
      (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u))
    (closure
      (Set.range (ι :=
        (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        (⇑(Hom.hom P.toLimit) :
          (a : (↑P.toProfinite.toTop : Type u)) → (↑(limit P.diagram).toProfinite.toTop : Type u))))
    Set.univ
⊢ Function.Surjective (α :=
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (β :=
    (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u))
    (⇑(Hom.hom P.toLimit) : (a : (↑P.toProfinite.toTop : Type u)) → (↑(limit P.diagram).toProfinite.toTop : Type u))
have rw₂ : Eq.{u + 1} (α :=
  Set
    (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u))
  Set.univ Set.univ
Tactic: rw [← Set.range_eq_univ, ← closure_eq_iff_isClosed.mpr this,
    Dense.closure_eq (denseRange_toLimit P)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits (goal)
Goal:
P : ProfiniteGrp.{u}
⊢ Function.Injective (α :=
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (β :=
    (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u))
    (⇑(Hom.hom P.toLimit).toMonoidHom :
      (a : (↑P.toProfinite.toTop : Type u)) → (↑(limit P.diagram).toProfinite.toTop : Type u))
have rw : ∀ x ∈ (Hom.hom P.toLimit).ker, x = 1
Tactic: rw [← MonoidHom.ker_eq_bot_iff, Subgroup.eq_bot_iff_forall]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits (goal)
Goal:
P : ProfiniteGrp.{u}
x : (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
h : x ∈ (Hom.hom P.toLimit).ker
⊢ x = 1
have by_contra : ∀ (xne1 : ¬x = 1), False
Tactic: by_contra xne1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits (goal)
Goal:
P : ProfiniteGrp.{u}
x : (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
h : x ∈ (Hom.hom P.toLimit).ker
xne1 : ¬x = 1
⊢ False
have rcases : ∀
  (H :
    OpenNormalSubgroup
      (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
  (hH : (↑H : Set (↑P.toProfinite.toTop : Type u)) ⊆ {x}ᶜ), False
Tactic: rcases exist_openNormalSubgroup_sub_open_nhds_of_one (isOpen_compl_singleton)
    (Set.mem_compl_singleton_iff.mpr fun a => xne1 a.symm) with ⟨H, hH⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits (goal)
Goal:
P : ProfiniteGrp.{u}
⊢ IsIso P.toLimit
have rw : Function.Bijective (α :=
  (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (β :=
  (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u))
  (⇑(ConcreteCategory.hom (FC := fun (X Y : ProfiniteGrp.{u}) ↦
        (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) →ₜ*
          (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        (CC := fun (X : ProfiniteGrp.{u}) ↦
        (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        P.toLimit) :
    (a : (↑P.toProfinite.toTop : Type u)) → (↑(limit P.diagram).toProfinite.toTop : Type u))
Tactic: rw [CategoryTheory.ConcreteCategory.isIso_iff_bijective]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ClopenNhdofOne (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
⊢ ∃ (H : OpenNormalSubgroup G), (↑H : Set G) ⊆ W
have rcases : ∀ (H : OpenSubgroup G) (hH : (↑H : Set G) ⊆ W), ∃ (H : OpenNormalSubgroup G), (↑H : Set G) ⊆ W
Tactic: rcases exist_openSubgroup_sub_clopen_nhds_of_one WClopen einW with ⟨H, hH⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ClopenNhdofOne (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
H : OpenSubgroup G
hH : (↑H : Set G) ⊆ W
⊢ ∃ (H : OpenNormalSubgroup G), (↑H : Set G) ⊆ W
have this : (↑H : Subgroup G).FiniteIndex
Tactic: have : Subgroup.FiniteIndex H.toSubgroup := H.finiteIndex_of_finite_quotient
-- Lean 4 proof step from Mathlib.Topology.Algebra.ClopenNhdofOne (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
H : OpenSubgroup G
hH : (↑H : Set G) ⊆ W
this : (↑H : Subgroup G).FiniteIndex
⊢ ∃ (H : OpenNormalSubgroup G), (↑H : Set G) ⊆ W
have h : (↑(let __Subgroup := (↑H : Subgroup G).normalCore;
      { toSubgroup := __Subgroup, isOpen' := sorry, isNormal' := sorry : OpenNormalSubgroup G }) :
    Set G) ⊆
  W
Tactic: use { toSubgroup := Subgroup.normalCore H
        isOpen' := Subgroup.isOpen_of_isClosed_of_finiteIndex _ (H.normalCore_isClosed H.isClosed) }
-- Lean 4 proof step from Mathlib.Topology.Algebra.ClopenNhdofOne (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
U : Set G
UOpen : IsOpen U
einU : 1 ∈ U
w : Set G
⊢ ∃ t ⊆ U, IsOpen t ∧ 1 ∈ t
have h : U ⊆ U ∧ IsOpen U ∧ 1 ∈ U
Tactic: use U
-- Lean 4 proof step from Mathlib.Topology.Algebra.ClopenNhdofOne (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
U : Set G
UOpen : IsOpen U
einU : 1 ∈ U
⊢ ∃ (H : OpenNormalSubgroup G), (↑H : Set G) ⊆ U
have rcases : ∀ (W : Set G) (hW : 1 ∈ W ∧ IsClopen W) (h : id W ⊆ U), ∃ (H : OpenNormalSubgroup G), (↑H : Set G) ⊆ U
Tactic: rcases ((Filter.HasBasis.mem_iff' ((nhds_basis_clopen (1 : G))) U).mp <|
    mem_nhds_iff.mpr (by use U)) with ⟨W, hW, h⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ClopenNhdofOne (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
U : Set G
UOpen : IsOpen U
einU : 1 ∈ U
W : Set G
hW : 1 ∈ W ∧ IsClopen W
h : id W ⊆ U
⊢ ∃ (H : OpenNormalSubgroup G), (↑H : Set G) ⊆ U
have rcases : ∀ (H : OpenNormalSubgroup G) (hH : (↑H : Set G) ⊆ W), ∃ (H : OpenNormalSubgroup G), (↑H : Set G) ⊆ U
Tactic: rcases IsTopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhds_of_one hW.2 hW.1 with ⟨H, hH⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ClopenNhdofOne (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
⊢ (↑H : Subgroup G) = sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}
have a : (↑H : Subgroup G) ≤ sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Algebra.ClopenNhdofOne (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
a : (↑H : Subgroup G) ≤ sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}
⊢ (↑H : Subgroup G) = sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}
have a₁ : sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N} ≤ (↑H : Subgroup G)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Algebra.ClopenNhdofOne (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
⊢ g ∈ (↑H : Subgroup G)
have a : ∀ (hg_not : g ∉ (↑H : Subgroup G)), False
Tactic: by_contra hg_not
-- Lean 4 proof step from Mathlib.Topology.Algebra.ClopenNhdofOne (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
⊢ False
have UOpen : IsOpen U
Tactic: have UOpen : IsOpen U :=
      ((Homeomorph.mulLeft g).isClosedMap _ H.isClosed').isOpen_compl
-- Lean 4 proof step from Mathlib.Topology.Algebra.ClopenNhdofOne (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
⊢ 1 ∈ U
have refine : 1 ∈ g • (↑H : Set G) → ∀ (l : G) (hl : l ∈ (↑H : Set G)) (hgl : g * l = 1), False
Tactic: refine Set.mem_compl (fun ⟨l, hl, (hgl : g * l = 1)⟩ ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.ClopenNhdofOne (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
h : 1 ∈ g • (↑H : Set G)
l : G
hl : l ∈ (↑H : Set G)
hgl : g * l = 1
⊢ False
have hgl₁ : g⁻¹ = l
Tactic: rw [← inv_eq_iff_mul_eq_one] at hgl
Cleared hypotheses: hgl
-- Lean 4 proof step from Mathlib.Topology.Algebra.ClopenNhdofOne (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
⊢ False
have einU : 1 ∈ U
Tactic: have einU : 1 ∈ U := by
      refine Set.mem_compl (fun ⟨l, hl, (hgl : g * l = 1)⟩ ↦ ?_)
      rw [← inv_eq_iff_mul_eq_one] at hgl
      exact hg_not <| inv_mem_iff.mp (hgl ▸ hl)
-- Lean 4 proof step from Mathlib.Topology.Algebra.ClopenNhdofOne (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
⊢ False
have a : ∀ (N : OpenNormalSubgroup G) (hN : (↑N : Set G) ⊆ U), False
Tactic: obtain ⟨N, hN⟩ := exist_openNormalSubgroup_sub_open_nhds_of_one UOpen einU
-- Lean 4 proof step from Mathlib.Topology.Algebra.ClopenNhdofOne (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : (↑N : Set G) ⊆ U
NH : Subgroup G := (↑N.toOpenSubgroup : Subgroup G) ⊔ (↑H : Subgroup G)
hg' : g ∈ NH
⊢ False
have rcases : ∀ (y : G) (hy : y ∈ (↑N.toOpenSubgroup : Subgroup G)) (z : G) (hz : z ∈ (↑H : Subgroup G)) (hyz : y * z = g), False
Tactic: rcases Subgroup.mem_sup_of_normal_left.mp hg' with ⟨y, hy, z, hz, hyz⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ClopenNhdofOne (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : (↑N : Set G) ⊆ U
NH : Subgroup G := (↑N.toOpenSubgroup : Subgroup G) ⊔ (↑H : Subgroup G)
hg' : g ∈ NH
y : G
hy : y ∈ (↑N.toOpenSubgroup : Subgroup G)
z : G
hz : z ∈ (↑H : Subgroup G)
hyz : y * z = g
⊢ False
have hyz₁ : y = g * z⁻¹
Tactic: rw [← eq_mul_inv_iff_mul_eq] at hyz
Cleared hypotheses: hyz
-- Lean 4 proof step from Mathlib.Topology.Algebra.ClopenNhdofOne (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : (↑N : Set G) ⊆ U
NH : Subgroup G := (↑N.toOpenSubgroup : Subgroup G) ⊔ (↑H : Subgroup G)
⊢ False
have hg_not' : g ∉ NH
Tactic: have hg_not' : g ∉ NH := by
      by_contra hg'
      rcases Subgroup.mem_sup_of_normal_left.mp hg' with ⟨y, hy, z, hz, hyz⟩
      rw [← eq_mul_inv_iff_mul_eq] at hyz
      exact hN (hyz ▸ hy) <| mem_leftCoset g (inv_mem_iff.mpr hz)
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
s : Set M
t : Set α
⊢ s • closure[inst] t ⊆ closure[inst] (s • t)
have simp : Subset.{u_2} (α := Set α) (⋃ a ∈ s, a • closure[inst] t) (closure[inst] (⋃ a ∈ s, a • t))
Tactic: simp only [← iUnion_smul_set]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
M : Type u_1
N : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul N β
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : ContinuousConstSMul N β
σ : M → N
⊢ IsClosed[Pi.topologicalSpace] {f : α → β | ∀ (c : M) (x : α), f (c • x) = σ c • f x}
have simp : IsClosed[Pi.topologicalSpace] (⋂ (i : M), ⋂ (i_1 : α), {x : α → β | x (i • i_1) = σ i • x i_1})
Tactic: simp only [Set.setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
c : G
s : Set α
hs : Dense s
⊢ Dense (c • s)
have rw : ∀ (hs : closure[inst] s = univ), closure[inst] (c • s) = univ
Tactic: rw [dense_iff_closure_eq] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
c : G
s : Set α
hs : closure[inst] s = univ
⊢ closure[inst] (c • s) = univ
have rw : c • closure[inst] s = univ
Tactic: rw [closure_smul, hs, smul_set_univ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
c : G
s : Set α
hs : closure[inst] s = univ
rw : c • closure[inst] s = univ
⊢ closure[inst] (c • s) = univ
have rw₁ : HSMul.hSMul (β := Set α) c univ = univ
Tactic: rw [closure_smul, hs, smul_set_univ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
c : G
s : Set α
hs : closure[inst] s = univ
rw : c • closure[inst] s = univ
rw₁ : HSMul.hSMul (β := Set α) c univ = univ
⊢ closure[inst] (c • s) = univ
have rw₂ : Eq.{u_2 + 1} (α := Set α) univ univ
Tactic: rw [closure_smul, hs, smul_set_univ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
s : Set G
t : Set α
ht : IsOpen[inst] t
⊢ IsOpen[inst] (s • t)
have rw : IsOpen[inst] (⋃ a ∈ s, a • t)
Tactic: rw [← iUnion_smul_set]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
G : Type u_4
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : ContinuousConstSMul G G
g : G
s : Set G
⊢ g • s ∈ 𝓝 g ↔ Membership.mem (γ := Filter G) (𝓝 1) s
have rw : g⁻¹ • g • s ∈ 𝓝 (g⁻¹ • g) ↔ Membership.mem (γ := Filter G) (𝓝 1) s
Tactic: rw [← smul_mem_nhds_smul_iff g⁻¹]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
⊢ T1Space α ↔ IsClosed[inst] {x}
have refine : ∀ (hx : IsClosed[inst] {x}) (y : α), IsClosed[inst] {y}
Tactic: refine ⟨fun H ↦ isClosed_singleton, fun hx ↦ ⟨fun y ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
hx : IsClosed[inst] {x}
y : α
⊢ IsClosed[inst] {y}
have rcases : ∀ (g : G), IsClosed[inst] {g • x}
Tactic: rcases MulAction.exists_smul_eq G x y with ⟨g, rfl⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
hx : IsClosed[inst] {x}
g : G
⊢ IsClosed[inst] {g • x}
have rw : IsClosed[inst] (HSMul.hSMul (β := Set α) g {x})
Tactic: rw [← image_singleton, image_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
⊢ DiscreteTopology α ↔ IsOpen[inst] {x}
have rw : (∀ (a : α), IsOpen[inst] {a}) ↔ IsOpen[inst] {x}
Tactic: rw [discreteTopology_iff_isOpen_singleton]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
⊢ (∀ (a : α), IsOpen[inst] {a}) ↔ IsOpen[inst] {x}
have refine : ∀ (hx : IsOpen[inst] {x}) (y : α), IsOpen[inst] {y}
Tactic: refine ⟨fun H ↦ H _, fun hx y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
hx : IsOpen[inst] {x}
y : α
⊢ IsOpen[inst] {y}
have rcases : ∀ (g : G), IsOpen[inst] {g • x}
Tactic: rcases MulAction.exists_smul_eq G x y with ⟨g, rfl⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
hx : IsOpen[inst] {x}
g : G
⊢ IsOpen[inst] {g • x}
have rw : IsOpen[inst] (HSMul.hSMul (β := Set α) g {x})
Tactic: rw [← image_singleton, image_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
c : G₀
s : Set E
⊢ closure[inst_3] (c • s) = c • closure[inst_3] s
have inl : closure[inst_3] (HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 s) =
  HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 (closure[inst_3] s)
Tactic: rcases eq_or_ne c 0 with (rfl | hc)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
c : G₀
s : Set E
inl :
  closure[inst_3] (HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 s) =
    HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 (closure[inst_3] s)
⊢ closure[inst_3] (c • s) = c • closure[inst_3] s
have inr : ∀ (hc : c ≠ 0), closure[inst_3] (c • s) = c • closure[inst_3] s
Tactic: rcases eq_or_ne c 0 with (rfl | hc)
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
s : Set E
⊢ closure[inst_3] (HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 s) =
    HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 (closure[inst_3] s)
have inl : closure[inst_3] (HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) (β := Set E) 0 ∅) =
  HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) (β := Set E) 0 (closure[inst_3] ∅)
Tactic: rcases eq_empty_or_nonempty s with (rfl | hs)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
s : Set E
inl :
  closure[inst_3] (HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) (β := Set E) 0 ∅) =
    HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) (β := Set E) 0 (closure[inst_3] ∅)
⊢ closure[inst_3] (HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 s) =
    HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 (closure[inst_3] s)
have inl₁ : ∀ (hs : s.Nonempty),
  closure[inst_3] (HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 s) =
    HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 (closure[inst_3] s)
Tactic: rcases eq_empty_or_nonempty s with (rfl | hs)
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
s : Set E
hs : s.Nonempty
⊢ closure[inst_3] (HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 s) =
    HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 (closure[inst_3] s)
have inl : Eq.{u_5 + 1} (α := Set E) (closure[inst_3] 0) 0
Tactic: rw [zero_smul_set hs, zero_smul_set hs.closure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
c : G₀
⊢ IsClosedMap (Y := E) fun (x : E) ↦ c • x
have inl : IsClosedMap (Y := E) fun (x : E) ↦ HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 x
Tactic: rcases eq_or_ne c 0 with (rfl | hne)
Cleared hypotheses: c