awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
⊢ Continuous[inst_1, inst_1] fun (a : V) ↦ -a
have conv : Continuous[inst_1, inst_1] fun (v : V) ↦ p -ᵥ (v +ᵥ p)
Tactic: conv =>
      enter [1, v]
      equals p -ᵥ (v +ᵥ p) => rw [vsub_vadd_eq_vsub_sub, vsub_self, zero_sub]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalAddGroup G
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (x : G × G) ↦ x.1 -ᵥ x.2
have simp : Continuous[instTopologicalSpaceProd, inst_1] fun (x : G × G) ↦ x.1 - x.2
Tactic: simp only [vsub_eq_sub]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
ι : Type u_1
V : ι → Type u_2
P : ι → Type u_3
inst : (i : ι) → AddCommGroup (V i)
inst_1 : (i : ι) → TopologicalSpace (V i)
inst_2 : (i : ι) → AddTorsor.{u_2, u_3} (V i) (P i)
inst_3 : (i : ι) → TopologicalSpace (P i)
inst_4 : ∀ (i : ι), IsTopologicalAddTorsor.{u_2, u_3} (P i)
⊢ ∀ (i : ι), Continuous[instTopologicalSpaceProd, inst_3 i] fun (a : ((i : ι) → V i) × ((i : ι) → P i)) ↦ (a.1 +ᵥ a.2) i
have simp : ∀ (i : ι), Continuous[instTopologicalSpaceProd, inst_3 i] fun (a : ((i : ι) → V i) × ((i : ι) → P i)) ↦ a.1 i +ᵥ a.2 i
Tactic: simp only [Pi.vadd_apply']
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
ι : Type u_1
V : ι → Type u_2
P : ι → Type u_3
inst : (i : ι) → AddCommGroup (V i)
inst_1 : (i : ι) → TopologicalSpace (V i)
inst_2 : (i : ι) → AddTorsor.{u_2, u_3} (V i) (P i)
inst_3 : (i : ι) → TopologicalSpace (P i)
inst_4 : ∀ (i : ι), IsTopologicalAddTorsor.{u_2, u_3} (P i)
⊢ ∀ (i : ι), Continuous[instTopologicalSpaceProd, inst_1 i] fun (a : ((i : ι) → P i) × ((i : ι) → P i)) ↦ (a.1 -ᵥ a.2) i
have simp : ∀ (i : ι), Continuous[instTopologicalSpaceProd, inst_1 i] fun (a : ((i : ι) → P i) × ((i : ι) → P i)) ↦ a.1 i -ᵥ a.2 i
Tactic: simp only [Pi.vsub_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
M : Type u_1
s : Set M
inst : Mul M
inst_1 : TopologicalSpace M
inst_2 : SeparatelyContinuousMul M
inst_3 : T2Space M
⊢ IsClosed[inst_1] s.centralizer
have rw : IsClosed[inst_1] (⋂ (i : M), {x : M | i ∈ s → i * x = x * i})
Tactic: rw [centralizer, setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
M : Type u_1
s : Set M
inst : Mul M
inst_1 : TopologicalSpace M
inst_2 : SeparatelyContinuousMul M
inst_3 : T2Space M
⊢ IsClosed[inst_1] (⋂ (i : M), {x : M | i ∈ s → i * x = x * i})
have refine : ∀ (t : Set M),
  Membership.mem (γ := Set (Set M)) (range fun (i : M) ↦ {x : M | i ∈ s → i * x = x * i}) t → IsClosed[inst_1] t
Tactic: refine isClosed_sInter ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
M : Type u_1
s : Set M
inst : Mul M
inst_1 : TopologicalSpace M
inst_2 : SeparatelyContinuousMul M
inst_3 : T2Space M
m : M
⊢ IsClosed[inst_1] ((fun (i : M) ↦ ({x : M | i ∈ s → i * x = x * i} : Set M)) m)
have refine_1 : Continuous[inst_1, inst_1] (HMul.hMul m)
Tactic: refine isClosed_imp (by simp) <| isClosed_eq ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
M : Type u_1
s : Set M
inst : Mul M
inst_1 : TopologicalSpace M
inst_2 : SeparatelyContinuousMul M
inst_3 : T2Space M
m : M
refine_1 : Continuous[inst_1, inst_1] (HMul.hMul m)
⊢ IsClosed[inst_1] ((fun (i : M) ↦ ({x : M | i ∈ s → i * x = x * i} : Set M)) m)
have refine_2 : Continuous[inst_1, inst_1] fun (x : M) ↦ x * m
Tactic: refine isClosed_imp (by simp) <| isClosed_eq ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
a : G
⊢ Eq (α := G ≃ₜ G) (Homeomorph.symm (Homeomorph.mulLeft a)) (Homeomorph.mulLeft a⁻¹)
have H : ∀ (x : G),
  Eq (α := G) ((Homeomorph.symm (Homeomorph.mulLeft a) : (a : G) → G) x : G)
    ((Homeomorph.mulLeft a⁻¹ : (a : G) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
c a : G
⊢ map (fun (x : G) ↦ c * x) (𝓝[≠] a) = 𝓝[≠] (c * a)
have h : Eq (α := Set G) {c * a}ᶜ (image (α := G) (⇑(Homeomorph.mulLeft c) : (a : G) → G) {a}ᶜ)
Tactic: convert! (Homeomorph.mulLeft c).isEmbedding.map_nhdsWithin_eq .. using 2
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
a : G
⊢ Eq (α := G ≃ₜ G) (Homeomorph.symm (Homeomorph.mulRight a)) (Homeomorph.mulRight a⁻¹)
have H : ∀ (x : G),
  Eq (α := G) ((Homeomorph.symm (Homeomorph.mulRight a) : (a : G) → G) x : G)
    ((Homeomorph.mulRight a⁻¹ : (a : G) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
c a : G
⊢ map (fun (x : G) ↦ x * c) (𝓝[≠] a) = 𝓝[≠] (a * c)
have h : Eq (α := Set G) {a * c}ᶜ (image (α := G) (⇑(Homeomorph.mulRight c) : (a : G) → G) {a}ᶜ)
Tactic: convert! (Homeomorph.mulRight c).isEmbedding.map_nhdsWithin_eq .. using 2
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
h : Eq (α := Set G) (connectedComponent 1) {1}
g : G
⊢ connectedComponent g = {g}
have rw : connectedComponent (g * 1) = {g * 1}
Tactic: rw [← mul_one g, ← smul_connectedComponent, h, Set.smul_set_singleton, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
h : Eq (α := Set G) (connectedComponent 1) {1}
g : G
rw : connectedComponent (g * 1) = {g * 1}
⊢ connectedComponent g = {g}
have rw₁ : HSMul.hSMul (β := Set G) g (connectedComponent 1) = {g * 1}
Tactic: rw [← mul_one g, ← smul_connectedComponent, h, Set.smul_set_singleton, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
h : Eq (α := Set G) (connectedComponent 1) {1}
g : G
rw : connectedComponent (g * 1) = {g * 1}
rw₁ : HSMul.hSMul (β := Set G) g (connectedComponent 1) = {g * 1}
⊢ connectedComponent g = {g}
have rw₂ : HSMul.hSMul (β := Set G) g {1} = {g * 1}
Tactic: rw [← mul_one g, ← smul_connectedComponent, h, Set.smul_set_singleton, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
h : Eq (α := Set G) (connectedComponent 1) {1}
g : G
rw : connectedComponent (g * 1) = {g * 1}
rw₁ : HSMul.hSMul (β := Set G) g (connectedComponent 1) = {g * 1}
rw₂ : HSMul.hSMul (β := Set G) g {1} = {g * 1}
⊢ connectedComponent g = {g}
have rw₃ : Eq (α := Set G) {HSMul.hSMul (β := G) g 1} {g * 1}
Tactic: rw [← mul_one g, ← smul_connectedComponent, h, Set.smul_set_singleton, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
h : Eq (α := Set G) (connectedComponent 1) {1}
g : G
rw : connectedComponent (g * 1) = {g * 1}
rw₁ : HSMul.hSMul (β := Set G) g (connectedComponent 1) = {g * 1}
rw₂ : HSMul.hSMul (β := Set G) g {1} = {g * 1}
rw₃ : Eq (α := Set G) {HSMul.hSMul (β := G) g 1} {g * 1}
⊢ connectedComponent g = {g}
have rw₄ : Eq (α := Set G) {g * 1} {g * 1}
Tactic: rw [← mul_one g, ← smul_connectedComponent, h, Set.smul_set_singleton, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b)) ↔ Tendsto f l (𝓝 c)
have refine : Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b)) → Tendsto f l (𝓝 c)
Tactic: refine ⟨?_, Tendsto.mul_const b⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b)) → Tendsto f l (𝓝 c)
have h : Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b)) → ∀ (x : α), f x = f x * b * b⁻¹
Tactic: convert! Tendsto.mul_const b⁻¹ using 3
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b)) → ∀ (x : α), f x = f x * b * b⁻¹
⊢ Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b)) → Tendsto f l (𝓝 c)
have h₁ : Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b)) → c = c * b * b⁻¹
Tactic: convert! Tendsto.mul_const b⁻¹ using 3
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b))
x : α
⊢ f x = f x * b * b⁻¹
have h : f x = f x
Tactic: rw [mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x * b) l (𝓝 (c * b))
⊢ c = c * b * b⁻¹
have h : c = c
Tactic: rw [mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c)) ↔ Tendsto f l (𝓝 c)
have refine : Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c)) → Tendsto f l (𝓝 c)
Tactic: refine ⟨?_, Tendsto.const_mul b⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c)) → Tendsto f l (𝓝 c)
have h : Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c)) → ∀ (x : α), f x = b⁻¹ * (b * f x)
Tactic: convert! Tendsto.const_mul b⁻¹ using 3
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c)) → ∀ (x : α), f x = b⁻¹ * (b * f x)
⊢ Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c)) → Tendsto f l (𝓝 c)
have h₁ : Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c)) → c = b⁻¹ * (b * c)
Tactic: convert! Tendsto.const_mul b⁻¹ using 3
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c))
x : α
⊢ f x = b⁻¹ * (b * f x)
have h : f x = f x
Tactic: rw [inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ b * f x) l (𝓝 (b * c))
⊢ c = b⁻¹ * (b * c)
have h : c = c
Tactic: rw [inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : FunLike F α β
inst_1 : Group α
inst_2 : DivisionMonoid β
inst_3 : MonoidHomClass F α β
tβ : TopologicalSpace β
inst_4 : ContinuousInv β
f : F
_tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
⊢ ContinuousInv α
have refine : Continuous[TopologicalSpace.induced (⇑f : (a : α) → β) tβ, tβ] (comp (β := α) (⇑f : (a : α) → β) fun (a : α) ↦ a⁻¹)
Tactic: refine ⟨continuous_induced_rng.2 ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : FunLike F α β
inst_1 : Group α
inst_2 : DivisionMonoid β
inst_3 : MonoidHomClass F α β
tβ : TopologicalSpace β
inst_4 : ContinuousInv β
f : F
_tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
⊢ Continuous[TopologicalSpace.induced (⇑f : (a : α) → β) tβ, tβ] (comp (β := α) (⇑f : (a : α) → β) fun (a : α) ↦ a⁻¹)
have simp : Continuous[TopologicalSpace.induced (⇑f : (a : α) → β) tβ, tβ] fun (x : α) ↦ ((f : (a : α) → β) x)⁻¹
Tactic: simp only [Function.comp_def, map_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : TopologicalSpace G₂
inst_1 : T2Space G₂
inst_2 : Inv G₁
inst_3 : Inv G₂
inst_4 : ContinuousInv G₂
⊢ IsClosed[Pi.topologicalSpace] {f : G₁ → G₂ | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}
have simp : IsClosed[Pi.topologicalSpace] (⋂ (i : G₁), {x : G₁ → G₂ | x i⁻¹ = (x i)⁻¹})
Tactic: simp only [setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
s : Set G
hs : IsCompact s
⊢ IsCompact s⁻¹
have rw : IsCompact (X := G) ((fun (x : G) ↦ x⁻¹) '' s)
Tactic: rw [← image_inv_eq_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : InvolutiveInv G
inst_2 : ContinuousInv G
a : G
⊢ (𝓝[≠] a)⁻¹ = 𝓝[≠] a⁻¹
have h : Eq (α := Set G) {a⁻¹}ᶜ (image (α := G) (⇑(Homeomorph.inv G) : (a : G) → G) {a}ᶜ)
Tactic: convert! (Homeomorph.inv G).isEmbedding.map_nhdsWithin_eq .. using 2
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G
have rw : ContinuousInv G
Tactic: rw [inf_eq_iInf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G
have refine : ∀ (b : Bool), ContinuousInv G
Tactic: refine continuousInv_iInf fun b => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
b : Bool
⊢ ContinuousInv G
have false : ContinuousInv G
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
b : Bool
false : ContinuousInv G
⊢ ContinuousInv G
have true : ContinuousInv G
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousMul H
c a : H
⊢ map (fun (x : H) ↦ c * x) (𝓝[>] a) = 𝓝[>] (c * a)
have h : Ioi (c * a) = (⇑(Homeomorph.mulLeft c) : (a : H) → H) '' Ioi a
Tactic: convert! (Homeomorph.mulLeft c).isEmbedding.map_nhdsWithin_eq .. using 2
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousMul H
c a : H
⊢ map (fun (x : H) ↦ c * x) (𝓝[<] a) = 𝓝[<] (c * a)
have h : Iio (c * a) = (⇑(Homeomorph.mulLeft c) : (a : H) → H) '' Iio a
Tactic: convert! (Homeomorph.mulLeft c).isEmbedding.map_nhdsWithin_eq .. using 2
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousMul H
c a : H
⊢ map (fun (x : H) ↦ x * c) (𝓝[>] a) = 𝓝[>] (a * c)
have h : Ioi (a * c) = (⇑(Homeomorph.mulRight c) : (a : H) → H) '' Ioi a
Tactic: convert! (Homeomorph.mulRight c).isEmbedding.map_nhdsWithin_eq .. using 2
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousMul H
c a : H
⊢ map (fun (x : H) ↦ x * c) (𝓝[<] a) = 𝓝[<] (a * c)
have h : Iio (a * c) = (⇑(Homeomorph.mulRight c) : (a : H) → H) '' Iio a
Tactic: convert! (Homeomorph.mulRight c).isEmbedding.map_nhdsWithin_eq .. using 2
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousInv H
a : H
⊢ (𝓝[>] a)⁻¹ = 𝓝[<] a⁻¹
have h : Iio a⁻¹ = (⇑(Homeomorph.inv H) : (a : H) → H) '' Ioi a
Tactic: convert! (Homeomorph.inv H).isEmbedding.map_nhdsWithin_eq .. using 2
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
H : Type x
inst : TopologicalSpace H
inst_1 : CommGroup H
inst_2 : PartialOrder H
inst_3 : IsOrderedMonoid H
inst_4 : ContinuousInv H
a : H
⊢ (𝓝[<] a)⁻¹ = 𝓝[>] a⁻¹
have h : Ioi a⁻¹ = (⇑(Homeomorph.inv H) : (a : H) → H) '' Iio a
Tactic: convert! (Homeomorph.inv H).isEmbedding.map_nhdsWithin_eq .. using 2
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Set G
hS : Membership.mem (γ := Filter G) (𝓝 1) S
⊢ Membership.mem (γ := Filter G) (𝓝 1) S⁻¹
have rwa : ∀ (hS : Membership.mem (γ := Filter G) (map Inv.inv (𝓝 1)) S), Membership.mem (γ := Filter G) (𝓝 1) S⁻¹
Tactic: rwa [← nhds_one_symm'] at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
H : Type x
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst, inst_4] (⇑f : (a : G) → H)
hf' : DenseRange.{x, w} (X := H) (α := G) (⇑f : (a : G) → H)
s : Subgroup G
hs : s.topologicalClosure = ⊤
⊢ (Subgroup.map f s).topologicalClosure = ⊤
have rw : ∀ (hs : (↑s.topologicalClosure : Set G) = (↑⊤ : Set G)), (↑(Subgroup.map f s).topologicalClosure : Set H) = (↑⊤ : Set H)
Tactic: rw [SetLike.ext'_iff] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
H : Type x
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst, inst_4] (⇑f : (a : G) → H)
hf' : DenseRange.{x, w} (X := H) (α := G) (⇑f : (a : G) → H)
s : Subgroup G
hs : (↑s.topologicalClosure : Set G) = (↑⊤ : Set G)
⊢ (↑(Subgroup.map f s).topologicalClosure : Set H) = (↑⊤ : Set H)
have simp : ∀ (hs : Dense (↑s : Set G)), Dense (↑(Subgroup.map f s) : Set H)
Tactic: simp only [Subgroup.topologicalClosure_coe, Subgroup.coe_top, ← dense_iff_closure_eq] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
N : Subgroup G
inst_3 : N.Normal
n : G
hn : n ∈ N.topologicalClosure
g : G
⊢ g * n * g⁻¹ ∈ N.topologicalClosure
have apply : MapsTo (fun (h : G) ↦ g * h * g⁻¹) (↑N : Set G) (↑N : Set G)
Tactic: apply map_mem_closure (IsTopologicalGroup.continuous_conj g) hn
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : MulOneClass G
inst_2 : ContinuousMul G
g h : G
hg : Membership.mem (γ := Set G) (connectedComponent 1) g
hh : Membership.mem (γ := Set G) (connectedComponent 1) h
⊢ Membership.mem (γ := Set G) (connectedComponent 1) (g * h)
have rw : g * h ∈ connectedComponent g
Tactic: rw [connectedComponent_eq hg]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : MulOneClass G
inst_2 : ContinuousMul G
g h : G
hg : Membership.mem (γ := Set G) (connectedComponent 1) g
hh : Membership.mem (γ := Set G) (connectedComponent 1) h
⊢ g ∈ connectedComponent (g * h)
have a : Membership.mem (γ := Set G) ((fun (x : G) ↦ g * x) '' connectedComponent h) g
Tactic: apply Continuous.image_connectedComponent_subset (continuous_const_mul g)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : MulOneClass G
inst_2 : ContinuousMul G
g h : G
hg : Membership.mem (γ := Set G) (connectedComponent 1) g
hh : Membership.mem (γ := Set G) (connectedComponent 1) h
⊢ Membership.mem (γ := Set G) ((fun (x : G) ↦ g * x) '' connectedComponent h) g
have a : Membership.mem (γ := Set G) ((fun (x : G) ↦ g * x) '' connectedComponent 1) g
Tactic: rw [← connectedComponent_eq hh]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : MulOneClass G
inst_2 : ContinuousMul G
g h : G
hg : Membership.mem (γ := Set G) (connectedComponent 1) g
hh : Membership.mem (γ := Set G) (connectedComponent 1) h
⊢ g * h ∈ connectedComponent g
have hmul : g ∈ connectedComponent (g * h)
Tactic: have hmul : g ∈ connectedComponent (g * h) := by
    apply Continuous.image_connectedComponent_subset (continuous_const_mul g)
    rw [← connectedComponent_eq hh]
    exact ⟨(1 : G), mem_connectedComponent, by simp only [mul_one]⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : DivisionMonoid G
inst_2 : ContinuousInv G
g : G
hg : Membership.mem (γ := Set G) (connectedComponent 1) g
⊢ Membership.mem (γ := Set G) (connectedComponent 1) g⁻¹
have rw : Membership.mem (γ := Set G) (connectedComponent 1⁻¹) g⁻¹
Tactic: rw [← inv_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s
have this : Membership.mem (γ := Filter (G × G)) (𝓝 (1, 1)) ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ⁻¹' s)
Tactic: have : (fun p : G × G => p.1 * p.2⁻¹) ⁻¹' s ∈ 𝓝 ((1, 1) : G × G) :=
    continuousAt_fst.mul continuousAt_snd.inv (by simpa)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : HasBasis (𝓝 1) p s
x : G
⊢ (𝓝 x).HasBasis p fun (i : ι) ↦ {y : G | y / x ∈ s i}
have rw : HasBasis.{w, u_1} (α := G) (Filter.comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1)) p fun (i : ι) ↦
  {y : G | y / x ∈ s i}
Tactic: rw [← nhds_translation_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : HasBasis (𝓝 1) p s
x : G
⊢ HasBasis.{w, u_1} (α := G) (Filter.comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1)) p fun (i : ι) ↦
    {y : G | y / x ∈ s i}
have simp_rw : HasBasis.{w, u_1} (α := G) (Filter.comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1)) p fun (i : ι) ↦
  {y : G | y * x⁻¹ ∈ s i}
Tactic: simp_rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x : G
s : Set G
⊢ x ∈ closure[inst] s ↔ ∀ (U : Set G), Membership.mem (γ := Filter G) (𝓝 1) U → ∃ y ∈ s, y / x ∈ U
have rw : (∀ (i : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) i → ∃ y ∈ s, Membership.mem (γ := Set G) {y : G | y / x ∈ id i} y) ↔
  ∀ (U : Set G), Membership.mem (γ := Filter G) (𝓝 1) U → ∃ y ∈ s, y / x ∈ U
Tactic: rw [mem_closure_iff_nhds_basis ((𝓝 1 : Filter G).basis_sets.nhds_of_one x)]