awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
inst : Group G
inst_1 : Monoid H
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace H
inst_4 : ContinuousInv G
f : MonoidHom.{w, x} G Hˣ
hf : Continuous[inst_2, inst_3] (⇑(MonoidHom.comp (Units.coeHom H) f) : (a : G) → H)
simp_rw : Continuous[inst_2, instTopologicalSpaceMulOpposite] fun (x : G) ↦ op (↑((f : (a : G) → Hˣ) x⁻¹) : H)
⊢ Continuous[inst_2, instTopologicalSpaceMulOpposite] fun (x : G) ↦ op (↑((f : (a : G) → Hˣ) x)⁻¹ : H)

Tactic:
simp_rw [← map_inv]

Premises used: map_inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
inst : Group G
inst_1 : Monoid H
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace H
inst_4 : ContinuousInv G
f : MonoidHom.{w, x} G Hˣ
hf : Continuous[inst_2, inst_3] (⇑(MonoidHom.comp (Units.coeHom H) f) : (a : G) → H)
⊢ Continuous[inst_2, instTopologicalSpaceMulOpposite] fun (x : G) ↦ op (↑((f : (a : G) → Hˣ) x⁻¹) : H)

Tactic:
MulOpposite.continuous_op.comp (hf.comp continuous_inv)

Premises used: Continuous.comp, ContinuousInv.continuous_inv, MulOpposite.continuous_op
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
inst : Group G
inst_1 : Monoid H
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace H
inst_4 : ContinuousInv G
f : MonoidHom.{w, x} G Hˣ
hf : Continuous[inst_2, inst_3] (⇑(MonoidHom.comp (Units.coeHom H) f) : (a : G) → H)
⊢ Continuous[inst_2, instTopologicalSpaceMulOpposite] fun (x : G) ↦ op (↑((f : (a : G) → Hˣ) x⁻¹) : H)

Tactic:
exact MulOpposite.continuous_op.comp (hf.comp continuous_inv)

Premises used: Continuous.comp, ContinuousInv.continuous_inv, MulOpposite.continuous_op
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
α : Type u
inst : Monoid α
⊢ Eq (α := Set (α × αᵐᵒᵖ)) (range (ι := αˣ) (⇑(embedProduct α) : (a : αˣ) → α × αᵐᵒᵖ))
    {p : α × αᵐᵒᵖ | p.1 * unop p.2 = 1 ∧ unop p.2 * p.1 = 1}

Tactic:
Set.range_eq_iff _ _ |>.mpr
    ⟨fun a ↦ ⟨a.mul_inv, a.inv_mul⟩, fun p hp ↦ ⟨⟨p.1, unop p.2, hp.1, hp.2⟩, rfl⟩⟩

Premises used: Iff.mpr, Units.inv_mul, Units.mul_inv, Prod.fst, And.right, And.left, And.intro, Units.mk, Exists.intro, MulOpposite.unop, Prod.snd, rfl, Set.range_eq_iff
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
α : Type u
inst : Monoid α
inst_1 : TopologicalSpace α
inst_2 : T1Space α
inst_3 : ContinuousMul α
rw : IsClosed[instTopologicalSpaceProd] {p : α × αᵐᵒᵖ | p.1 * unop p.2 = 1 ∧ unop p.2 * p.1 = 1}
⊢ IsClosed[instTopologicalSpaceProd] (range (ι := αˣ) (⇑(embedProduct α) : (a : αˣ) → α × αᵐᵒᵖ))

Tactic:
rw [range_embedProduct]

Premises used: Units.range_embedProduct
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
α : Type u
inst : Monoid α
inst_1 : TopologicalSpace α
inst_2 : T1Space α
inst_3 : ContinuousMul α
⊢ IsClosed[instTopologicalSpaceProd] {p : α × αᵐᵒᵖ | p.1 * unop p.2 = 1 ∧ unop p.2 * p.1 = 1}

Tactic:
.inter (isClosed_singleton.preimage ?_) (isClosed_singleton.preimage ?_)

Premises used: Set.Mem, setOf, Set.inter, IsClosed.preimage, IsClosed.inter, isClosed_singleton
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
α : Type u
inst : Monoid α
inst_1 : TopologicalSpace α
inst_2 : T1Space α
inst_3 : ContinuousMul α
refine_1 : Continuous[instTopologicalSpaceProd, inst_1] fun (p : α × αᵐᵒᵖ) ↦ p.1 * unop p.2
refine_2 : Continuous[instTopologicalSpaceProd, inst_1] fun (p : α × αᵐᵒᵖ) ↦ unop p.2 * p.1
⊢ IsClosed[instTopologicalSpaceProd] {p : α × αᵐᵒᵖ | p.1 * unop p.2 = 1 ∧ unop p.2 * p.1 = 1}

Tactic:
refine .inter (isClosed_singleton.preimage ?_) (isClosed_singleton.preimage ?_)
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
α : Type u
inst : Monoid α
inst_1 : TopologicalSpace α
inst_2 : T1Space α
inst_3 : ContinuousMul α
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : α × αᵐᵒᵖ) ↦ p.1 * unop p.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
α : Type u
inst : Monoid α
inst_1 : TopologicalSpace α
inst_2 : T1Space α
inst_3 : ContinuousMul α
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : α × αᵐᵒᵖ) ↦ unop p.2 * p.1

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
α : Type u
β : Type v
inst : Monoid α
inst_1 : TopologicalSpace α
inst_2 : Monoid β
inst_3 : TopologicalSpace β
inst_4 : ContinuousMul α
inst_5 : T1Space α
f : α →* β
hf : IsClosedEmbedding.{u, v} (X := α) (Y := β) (⇑f : (a : α) → β)
⊢ IsClosedEmbedding.{u, v} (X := αˣ) (Y := βˣ) (⇑(map f) : (a : αˣ) → βˣ)

Tactic:
.of_comp isEmbedding_embedProduct ?_

Premises used: Units.isEmbedding_embedProduct, Topology.IsClosedEmbedding.of_comp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
α : Type u
β : Type v
inst : Monoid α
inst_1 : TopologicalSpace α
inst_2 : Monoid β
inst_3 : TopologicalSpace β
inst_4 : ContinuousMul α
inst_5 : T1Space α
f : α →* β
hf : IsClosedEmbedding.{u, v} (X := α) (Y := β) (⇑f : (a : α) → β)
refine :
  IsClosedEmbedding.{u, v} (X := αˣ) (Y := β × βᵐᵒᵖ)
    (comp (β := βˣ) (⇑(embedProduct β) : (a : βˣ) → β × βᵐᵒᵖ) (⇑(map f) : (a : αˣ) → βˣ))
⊢ IsClosedEmbedding.{u, v} (X := αˣ) (Y := βˣ) (⇑(map f) : (a : αˣ) → βˣ)

Tactic:
refine .of_comp isEmbedding_embedProduct ?_
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
α : Type u
β : Type v
inst : Monoid α
inst_1 : TopologicalSpace α
inst_2 : Monoid β
inst_3 : TopologicalSpace β
inst_4 : ContinuousMul α
inst_5 : T1Space α
f : α →* β
hf : IsClosedEmbedding.{u, v} (X := α) (Y := β) (⇑f : (a : α) → β)
⊢ IsClosedEmbedding.{u, v} (X := αˣ) (Y := β × βᵐᵒᵖ)
    (comp (β := βˣ) (⇑(embedProduct β) : (a : βˣ) → β × βᵐᵒᵖ) (⇑(map f) : (a : αˣ) → βˣ))

Tactic:
(hf.prodMap (opHomeomorph.isClosedEmbedding.comp
    <| hf.comp opHomeomorph.symm.isClosedEmbedding)).comp isClosedEmbedding_embedProduct

Premises used: MulOpposite.opHomeomorph, Topology.IsClosedEmbedding.comp, Prod.map, Topology.IsClosedEmbedding.prodMap, Homeomorph.symm, Units.isClosedEmbedding_embedProduct, MulOpposite.unop, Homeomorph.isClosedEmbedding, MulOpposite.op
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
α : Type u
β : Type v
inst : Monoid α
inst_1 : TopologicalSpace α
inst_2 : Monoid β
inst_3 : TopologicalSpace β
inst_4 : ContinuousMul α
inst_5 : T1Space α
f : α →* β
hf : IsClosedEmbedding.{u, v} (X := α) (Y := β) (⇑f : (a : α) → β)
⊢ IsClosedEmbedding.{u, v} (X := αˣ) (Y := β × βᵐᵒᵖ)
    (comp (β := βˣ) (⇑(embedProduct β) : (a : βˣ) → β × βᵐᵒᵖ) (⇑(map f) : (a : αˣ) → βˣ))

Tactic:
exact (hf.prodMap (opHomeomorph.isClosedEmbedding.comp
    <| hf.comp opHomeomorph.symm.isClosedEmbedding)).comp isClosedEmbedding_embedProduct

Premises used: MulOpposite.opHomeomorph, Topology.IsClosedEmbedding.comp, Topology.IsClosedEmbedding.prodMap, Homeomorph.symm, Units.isClosedEmbedding_embedProduct, Homeomorph.isClosedEmbedding
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : Monoid α
inst_1 : TopologicalSpace α
inst_2 : Monoid β
inst_3 : TopologicalSpace β
inst_4 : T1Space α
inst_5 : ContinuousMul α
inst_6 : CompactSpace α
⊢ CompactSpace.{u} αˣ

Tactic:
isClosedEmbedding_embedProduct.compactSpace

Premises used: Topology.IsClosedEmbedding.compactSpace, Units.isClosedEmbedding_embedProduct
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : Monoid α
inst_1 : TopologicalSpace α
inst_2 : Monoid β
inst_3 : TopologicalSpace β
inst_4 : T1Space α
inst_5 : ContinuousMul α
inst_6 : WeaklyLocallyCompactSpace α
⊢ WeaklyLocallyCompactSpace.{u} αˣ

Tactic:
isClosedEmbedding_embedProduct.weaklyLocallyCompactSpace

Premises used: Topology.IsClosedEmbedding.weaklyLocallyCompactSpace, Units.isClosedEmbedding_embedProduct
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : Monoid α
inst_1 : TopologicalSpace α
inst_2 : Monoid β
inst_3 : TopologicalSpace β
inst_4 : T1Space α
inst_5 : ContinuousMul α
inst_6 : LocallyCompactSpace α
⊢ LocallyCompactSpace.{u} αˣ

Tactic:
isClosedEmbedding_embedProduct.locallyCompactSpace

Premises used: Units.isClosedEmbedding_embedProduct, Topology.IsClosedEmbedding.locallyCompactSpace
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
α : Type u
inst : Monoid α
inst_1 : TopologicalSpace α
inst_2 : T1Space α
inst_3 : ContinuousMul α
S : Submonoid α
hS : IsCompact (↑S : Set α)
⊢ IsCompact ((↑S : Set α) ×ˢ (↑S.op : Set αᵐᵒᵖ))

Tactic:
have : IsCompact (S ×ˢ S.op) := hS.prod (opHomeomorph.isCompact_preimage.mp hS)
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
α : Type u
inst : Monoid α
inst_1 : TopologicalSpace α
inst_2 : T1Space α
inst_3 : ContinuousMul α
S : Submonoid α
hS : IsCompact (↑S : Set α)
this : IsCompact ((↑S : Set α) ×ˢ (↑S.op : Set αᵐᵒᵖ))
⊢ IsCompact (↑S.units : Set αˣ)

Tactic:
isClosedEmbedding_embedProduct.isCompact_preimage this

Premises used: Set.Mem, setOf, Set.prod, Set.preimage, Topology.IsClosedEmbedding.isCompact_preimage, Units.isClosedEmbedding_embedProduct, MulOpposite.unop
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
α : Type u
inst : Monoid α
inst_1 : TopologicalSpace α
inst_2 : T1Space α
inst_3 : ContinuousMul α
S : Submonoid α
hS : IsCompact (↑S : Set α)
this : IsCompact ((↑S : Set α) ×ˢ (↑S.op : Set αᵐᵒᵖ))
⊢ IsCompact (↑S.units : Set αˣ)

Tactic:
exact isClosedEmbedding_embedProduct.isCompact_preimage this

Premises used: Topology.IsClosedEmbedding.isCompact_preimage, Units.isClosedEmbedding_embedProduct
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Group G
ts : Set (TopologicalSpace G)
h : ∀ t ∈ ts, IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
letI := sInf ts
  { toContinuousInv :=
      @continuousInv_sInf _ _ _ fun t ht => @IsTopologicalGroup.toContinuousInv G t _ <| h t ht
    toContinuousMul :=
      @continuousMul_sInf _ _ _ fun t ht =>
        @IsTopologicalGroup.toContinuousMul G t _ <| h t ht }

Premises used: continuousMul_sInf, IsTopologicalGroup.mk, continuousInv_sInf, IsTopologicalGroup.toContinuousMul, IsTopologicalGroup.toContinuousInv
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
ι : Sort u_1
inst : Group G
ts' : ι → TopologicalSpace G
h' : ∀ (i : ι), IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
topologicalGroup_sInf (Set.forall_mem_range.mpr h')

Premises used: Iff.mpr, Set.forall_mem_range, topologicalGroup_sInf
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
ι : Sort u_1
inst : Group G
ts' : ι → TopologicalSpace G
h' : ∀ (i : ι), IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
exact topologicalGroup_sInf (Set.forall_mem_range.mpr h')

Premises used: Iff.mpr, Set.forall_mem_range, topologicalGroup_sInf
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
rw : IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
rw [inf_eq_iInf]

Premises used: inf_eq_iInf
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
topologicalGroup_iInf fun b => ?_

Premises used: topologicalGroup_iInf
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
refine : ∀ (b : Bool), IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
refine topologicalGroup_iInf fun b => ?_

Premises used: topologicalGroup_iInf
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
b : Bool
false : IsTopologicalGroup G
true : IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
cases b
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
assumption
-- Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
A B : ClosedSubgroup G
h : (↑A : Subgroup G) = (↑B : Subgroup G)
carrier : ∀ (x : G), x ∈ (↑A : Subgroup G).carrier ↔ x ∈ (↑B : Subgroup G).carrier
⊢ A = B

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
A B : ClosedSubgroup G
h : (↑A : Subgroup G) = (↑B : Subgroup G)
x : G
carrier carrier₁ : x ∈ (↑B : Subgroup G).carrier ↔ x ∈ (↑B : Subgroup G).carrier
⊢ x ∈ (↑A : Subgroup G).carrier ↔ x ∈ (↑B : Subgroup G).carrier

Tactic:
rw [h]
-- Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
H : ClosedSubgroup G
⊢ CompactSpace.{u} ↥H

Tactic:
isCompact_iff_compactSpace.mp (IsClosed.isCompact H.isClosed')

Premises used: isCompact_iff_compactSpace, ClosedSubgroup.isClosed', IsClosed.isCompact, Iff.mp
-- Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
h : IsClosed (↑H : Set G)
rw : IsClosed (↑(⨅ (g : ConjAct G), g • H) : Set G)
⊢ IsClosed (↑H.normalCore : Set G)

Tactic:
rw [normalCore_eq_iInf_conjAct]

Premises used: Subgroup.normalCore_eq_iInf_conjAct
-- Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
h : IsClosed (↑H : Set G)
push_cast : IsClosed.{u} (X := G) (⋂ (i : ConjAct G), i • (↑H : Set G))
⊢ IsClosed (↑(⨅ (g : ConjAct G), g • H) : Set G)

Tactic:
push_cast
-- Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
h : IsClosed (↑H : Set G)
h₁ : ∀ (i : ConjAct G), IsClosed (i • (↑H : Set G))
⊢ IsClosed.{u} (X := G) (⋂ (i : ConjAct G), i • (↑H : Set G))

Tactic:
apply isClosed_iInter

Premises used: isClosed_iInter
-- Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
h : IsClosed (↑H : Set G)
g : ConjAct G
⊢ IsClosed (X := G)
    ((fun (h : G) ↦
        HMul.hMul (β := G) (HMul.hMul (α := G) ((ConjAct.ofConjAct : (a : ConjAct G) → G) g⁻¹ : G) h)
          (((ConjAct.ofConjAct : (a : ConjAct G) → G) g⁻¹)⁻¹ : G)) ⁻¹'
      (↑H : Set G))

Tactic:
IsClosed.preimage (IsTopologicalGroup.continuous_conj (ConjAct.ofConjAct g⁻¹)) h

Premises used: Inv.inv, ConjAct.ofConjAct, IsClosed.preimage, DFunLike.coe, IsTopologicalGroup.continuous_conj
-- Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
h : IsClosed (↑H : Set G)
g : ConjAct G
h₁ :
  g • (↑H : Set G) =
    (fun (h : G) ↦
        HMul.hMul (β := G) (HMul.hMul (α := G) ((ConjAct.ofConjAct : (a : ConjAct G) → G) g⁻¹ : G) h)
          (((ConjAct.ofConjAct : (a : ConjAct G) → G) g⁻¹)⁻¹ : G)) ⁻¹'
      (↑H : Set G)
⊢ IsClosed (g • (↑H : Set G))

Tactic:
convert! IsClosed.preimage (IsTopologicalGroup.continuous_conj (ConjAct.ofConjAct g⁻¹)) h using 1

Premises used: Inv.inv, ConjAct.ofConjAct, IsClosed.preimage, DFunLike.coe, IsTopologicalGroup.continuous_conj
-- Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
h : IsClosed (↑H : Set G)
g : ConjAct G
⊢ g • (↑H : Set G) =
    (fun (h : G) ↦
        HMul.hMul (β := G) (HMul.hMul (α := G) ((ConjAct.ofConjAct : (a : ConjAct G) → G) g⁻¹ : G) h)
          (((ConjAct.ofConjAct : (a : ConjAct G) → G) g⁻¹)⁻¹ : G)) ⁻¹'
      (↑H : Set G)

Tactic:
Set.ext (fun t ↦ Set.mem_smul_set_iff_inv_smul_mem)

Premises used: Set.ext, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
h : IsClosed (↑H : Set G)
g : ConjAct G
⊢ g • (↑H : Set G) =
    (fun (h : G) ↦
        HMul.hMul (β := G) (HMul.hMul (α := G) ((ConjAct.ofConjAct : (a : ConjAct G) → G) g⁻¹ : G) h)
          (((ConjAct.ofConjAct : (a : ConjAct G) → G) g⁻¹)⁻¹ : G)) ⁻¹'
      (↑H : Set G)

Tactic:
exact Set.ext (fun t ↦ Set.mem_smul_set_iff_inv_smul_mem)

Premises used: Set.ext, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
inst_3 : H.FiniteIndex
h : IsClosed (↑H : Set G)
⊢ T1Space.{u} (G ⧸ H)

Tactic:
rw [← QuotientGroup.t1Space_iff] at h

Premises used: QuotientGroup.t1Space_iff
-- Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
inst_3 : H.FiniteIndex
h : T1Space.{u} (G ⧸ H)
rw : DiscreteTopology.{u} (G ⧸ H)
⊢ IsOpen (↑H : Set G)

Tactic:
rw [← QuotientGroup.discreteTopology_iff]

Premises used: QuotientGroup.discreteTopology_iff
-- Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
inst_3 : H.FiniteIndex
h : T1Space.{u} (G ⧸ H)
⊢ DiscreteTopology.{u} (G ⧸ H)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.Group.Compact
Goal:
G : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : PositiveCompacts G
⊢ LocallyCompactSpace G

Tactic:
let ⟨_x, hx⟩ := K.interior_nonempty
  K.isCompact.locallyCompactSpace_of_mem_nhds_of_group (mem_interior_iff_mem_nhds.1 hx)

Premises used: mem_interior_iff_mem_nhds, TopologicalSpace.PositiveCompacts.interior_nonempty, IsCompact.locallyCompactSpace_of_mem_nhds_of_group, _private.0.TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group.match_1, Iff.mp, TopologicalSpace.PositiveCompacts.isCompact, LocallyCompactSpace
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
⊢ IsInducing (X := A →ₜ* B) toContinuousMap

Tactic:
⟨rfl⟩

Premises used: Topology.IsInducing.mk, rfl
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
⊢ IsEmbedding (X := A →ₜ* B) toContinuousMap

Tactic:
⟨isInducing_toContinuousMap A B, toContinuousMap_injective⟩

Premises used: ContinuousMonoidHom.isInducing_toContinuousMap, ContinuousMonoidHom.toContinuousMap_injective, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : Monoid D
inst_4 : CommGroup E
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace D
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalGroup E
⊢ ContinuousEvalConst (A →ₜ* B) A B

Tactic:
.of_continuous_forget (isInducing_toContinuousMap A B).continuous

Premises used: ContinuousMonoidHom.isInducing_toContinuousMap, ContinuousEvalConst.of_continuous_forget, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : Monoid D
inst_4 : CommGroup E
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace D
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalGroup E
inst_11 : LocallyCompactPair A B
⊢ ContinuousEval (A →ₜ* B) A B

Tactic:
.of_continuous_forget (isInducing_toContinuousMap A B).continuous

Premises used: ContinuousMonoidHom.isInducing_toContinuousMap, Topology.IsInducing.continuous, ContinuousEval.of_continuous_forget
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
⊢ Eq (α := Set C(A, B)) (Set.range (ι := A →ₜ* B) toContinuousMap)
    {f : C(A, B) |
      Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B) ∧
        ∀ (x y : A),
          (f : (a : A) → B) (x * y) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)}

Tactic:
Set.Subset.antisymm (Set.range_subset_iff.2 fun f ↦ ⟨map_one f, map_mul f⟩) ?_

Premises used: Set.Subset.antisymm, Iff.mpr, map_mul, map_one, And.intro, Set.range_subset_iff
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
refine :
  Subset (α := Set C(A, B))
    {f : C(A, B) |
      Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B) ∧
        ∀ (x y : A),
          (f : (a : A) → B) (x * y) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)}
    (Set.range (ι := A →ₜ* B) toContinuousMap)
⊢ Eq (α := Set C(A, B)) (Set.range (ι := A →ₜ* B) toContinuousMap)
    {f : C(A, B) |
      Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B) ∧
        ∀ (x y : A),
          (f : (a : A) → B) (x * y) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)}

Tactic:
refine Set.Subset.antisymm (Set.range_subset_iff.2 fun f ↦ ⟨map_one f, map_mul f⟩) ?_
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
f : C(A, B)
h1 : Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
hmul :
  ∀ (x y : A),
    (f : (a : A) → B) (x * y) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
⊢ Membership.mem (γ := Set C(A, B)) (Set.range (ι := A →ₜ* B) toContinuousMap) f

Tactic:
⟨{ f with map_one' := h1, map_mul' := hmul }, rfl⟩

Premises used: ContinuousMonoidHom.mk, Set.Mem, OneHom.mk, setOf, MonoidHom.mk, ContinuousMap.continuous_toFun, Exists.intro, ContinuousMap.toFun, Set.range, rfl
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
f : C(A, B)
h1 : Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
hmul :
  ∀ (x y : A),
    (f : (a : A) → B) (x * y) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
⊢ Membership.mem (γ := Set C(A, B)) (Set.range (ι := A →ₜ* B) toContinuousMap) f

Tactic:
exact ⟨{ f with map_one' := h1, map_mul' := hmul }, rfl⟩
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
inst_4 : ContinuousMul B
inst_5 : T2Space B
simp :
  IsClosed (X := C(A, B))
    ({a : C(A, B) | Eq.{u_3 + 1} (α := B) ((a : (a : A) → B) 1 : B) (1 : B)} ∩
      ⋂ (i : A),
        ⋂ (i_1 : A),
          {x : C(A, B) |
            (x : (a : A) → B) (i * i_1) =
              HMul.hMul (α := B) (β := B) ((x : (a : A) → B) i : B) ((x : (a : A) → B) i_1 : B)})
⊢ IsClosed (X := C(A, B)) (Set.range (ι := A →ₜ* B) toContinuousMap)

Tactic:
simp only [range_toContinuousMap, Set.setOf_and, Set.setOf_forall]

Premises used: Set.setOf_and, ContinuousMonoidHom.range_toContinuousMap, Set.setOf_forall
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
inst_4 : ContinuousMul B
inst_5 : T2Space B
⊢ IsClosed (X := C(A, B))
    ({a : C(A, B) | Eq.{u_3 + 1} (α := B) ((a : (a : A) → B) 1 : B) (1 : B)} ∩
      ⋂ (i : A),
        ⋂ (i_1 : A),
          {x : C(A, B) |
            (x : (a : A) → B) (i * i_1) =
              HMul.hMul (α := B) (β := B) ((x : (a : A) → B) i : B) ((x : (a : A) → B) i_1 : B)})

Tactic:
.inter (isClosed_singleton.preimage (continuous_eval_const 1)) <|
      isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ ?_

Premises used: ContinuousEvalConst.continuous_eval_const, IsClosed.preimage, IsClosed.inter, OfNat.ofNat, isClosed_singleton, isClosed_iInter