awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 y : G
rw :
  Eq.{w + 1} (α := Filter G)
    (map (fun (x_1 : G) ↦ x * x_1) (map (fun (x : G) ↦ x * y) (map₂ (fun (x1 x2 : G) ↦ x1 * x2) (𝓝 1) (𝓝 1))))
    (map₂ (fun (a b : G) ↦ x * (a * b * y)) (𝓝 1) (𝓝 1))
rw₁ :
  Eq.{w + 1} (α := Filter G) (map (fun (x_1 : G) ↦ x * x_1) (map₂ (fun (a b : G) ↦ a * b * y) (𝓝 1) (𝓝 1)))
    (map₂ (fun (a b : G) ↦ x * (a * b * y)) (𝓝 1) (𝓝 1))
⊢ Eq (α := Filter G) (map (fun (x_1 : G) ↦ x * x_1) (map (fun (x : G) ↦ x * y) (HMul.hMul (α := Filter G) (𝓝 1) (𝓝 1))))
    (map₂ (fun (a b : G) ↦ x * (a * b * y)) (𝓝 1) (𝓝 1))
have rw₂ : Eq.{w + 1} (α := Filter G) (map₂ (fun (a b : G) ↦ x * (a * b * y)) (𝓝 1) (𝓝 1))
  (map₂ (fun (a b : G) ↦ x * (a * b * y)) (𝓝 1) (𝓝 1))
Tactic: rw [← map₂_mul, map_map₂, map_map₂]
-- 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 y : G
⊢ map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) = 𝓝 x * 𝓝 y
have rw : map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) = map (fun (x_1 : G) ↦ x * x_1) (𝓝 1) * 𝓝 y
Tactic: rw [← map_mul_left_nhds_one x, ← map_mul_right_nhds_one y, ← map₂_mul, map₂_map_left,
        map₂_map_right]
-- 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 y : G
rw : map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) = map (fun (x_1 : G) ↦ x * x_1) (𝓝 1) * 𝓝 y
⊢ map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) = 𝓝 x * 𝓝 y
have rw₁ : map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) =
  HMul.hMul (α := Filter G) (map (fun (x_1 : G) ↦ x * x_1) (𝓝 1)) (map (fun (x : G) ↦ x * y) (𝓝 1))
Tactic: rw [← map_mul_left_nhds_one x, ← map_mul_right_nhds_one y, ← map₂_mul, map₂_map_left,
        map₂_map_right]
-- 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 y : G
rw : map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) = map (fun (x_1 : G) ↦ x * x_1) (𝓝 1) * 𝓝 y
rw₁ :
  map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) =
    HMul.hMul (α := Filter G) (map (fun (x_1 : G) ↦ x * x_1) (𝓝 1)) (map (fun (x : G) ↦ x * y) (𝓝 1))
⊢ map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) = 𝓝 x * 𝓝 y
have rw₂ : Eq.{w + 1} (α := Filter G) (map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1))
  (map₂ (fun (x1 x2 : G) ↦ x1 * x2) (map (fun (x_1 : G) ↦ x * x_1) (𝓝 1)) (map (fun (x : G) ↦ x * y) (𝓝 1)))
Tactic: rw [← map_mul_left_nhds_one x, ← map_mul_right_nhds_one y, ← map₂_mul, map₂_map_left,
        map₂_map_right]
-- 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 y : G
rw : map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) = map (fun (x_1 : G) ↦ x * x_1) (𝓝 1) * 𝓝 y
rw₁ :
  map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) =
    HMul.hMul (α := Filter G) (map (fun (x_1 : G) ↦ x * x_1) (𝓝 1)) (map (fun (x : G) ↦ x * y) (𝓝 1))
rw₂ :
  Eq.{w + 1} (α := Filter G) (map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1))
    (map₂ (fun (x1 x2 : G) ↦ x1 * x2) (map (fun (x_1 : G) ↦ x * x_1) (𝓝 1)) (map (fun (x : G) ↦ x * y) (𝓝 1)))
⊢ map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) = 𝓝 x * 𝓝 y
have rw₃ : Eq.{w + 1} (α := Filter G) (map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1))
  (map₂ (fun (a b : G) ↦ x * a * b) (𝓝 1) (map (fun (x : G) ↦ x * y) (𝓝 1)))
Tactic: rw [← map_mul_left_nhds_one x, ← map_mul_right_nhds_one y, ← map₂_mul, map₂_map_left,
        map₂_map_right]
-- 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 y : G
rw : map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) = map (fun (x_1 : G) ↦ x * x_1) (𝓝 1) * 𝓝 y
rw₁ :
  map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) =
    HMul.hMul (α := Filter G) (map (fun (x_1 : G) ↦ x * x_1) (𝓝 1)) (map (fun (x : G) ↦ x * y) (𝓝 1))
rw₂ :
  Eq.{w + 1} (α := Filter G) (map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1))
    (map₂ (fun (x1 x2 : G) ↦ x1 * x2) (map (fun (x_1 : G) ↦ x * x_1) (𝓝 1)) (map (fun (x : G) ↦ x * y) (𝓝 1)))
rw₃ :
  Eq.{w + 1} (α := Filter G) (map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1))
    (map₂ (fun (a b : G) ↦ x * a * b) (𝓝 1) (map (fun (x : G) ↦ x * y) (𝓝 1)))
⊢ map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) = 𝓝 x * 𝓝 y
have rw₄ : Eq.{w + 1} (α := Filter G) (map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1))
  (map₂ (fun (a b : G) ↦ x * a * (b * y)) (𝓝 1) (𝓝 1))
Tactic: rw [← map_mul_left_nhds_one x, ← map_mul_right_nhds_one y, ← map₂_mul, map₂_map_left,
        map₂_map_right]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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, Units.instTopologicalSpaceUnits] (⇑f : (a : G) → Hˣ)
have apply : Continuous[inst_2, inferInstance]
  (Function.comp (β := Hˣ) (⇑(Units.embedProduct H) : (a : Hˣ) → H × Hᵐᵒᵖ) (⇑f : (a : G) → Hˣ))
Tactic: apply continuous_induced_rng.mpr ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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, inferInstance]
    (Function.comp (β := Hˣ) (⇑(Units.embedProduct H) : (a : Hˣ) → H × Hᵐᵒᵖ) (⇑f : (a : G) → Hˣ))
have refine : Continuous[inst_2, instTopologicalSpaceMulOpposite] fun (x : G) ↦ op (↑((f : (a : G) → Hˣ) x)⁻¹ : H)
Tactic: refine continuous_prodMk.mpr ⟨hf, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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)
have simp_rw : Continuous[inst_2, instTopologicalSpaceMulOpposite] fun (x : G) ↦ op (↑((f : (a : G) → Hˣ) x⁻¹) : H)
Tactic: simp_rw [← map_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
inst : Monoid α
inst_1 : TopologicalSpace α
inst_2 : T1Space α
inst_3 : ContinuousMul α
⊢ IsClosed[instTopologicalSpaceProd] (range (ι := αˣ) (⇑(embedProduct α) : (a : αˣ) → α × αᵐᵒᵖ))
have rw : IsClosed[instTopologicalSpaceProd] {p : α × αᵐᵒᵖ | p.1 * unop p.2 = 1 ∧ unop p.2 * p.1 = 1}
Tactic: rw [range_embedProduct]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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}
have refine_1 : Continuous[instTopologicalSpaceProd, inst_1] fun (p : α × αᵐᵒᵖ) ↦ p.1 * unop p.2
Tactic: refine .inter (isClosed_singleton.preimage ?_) (isClosed_singleton.preimage ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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
⊢ IsClosed[instTopologicalSpaceProd] {p : α × αᵐᵒᵖ | p.1 * unop p.2 = 1 ∧ unop p.2 * p.1 = 1}
have refine_2 : Continuous[instTopologicalSpaceProd, inst_1] fun (p : α × αᵐᵒᵖ) ↦ unop p.2 * p.1
Tactic: refine .inter (isClosed_singleton.preimage ?_) (isClosed_singleton.preimage ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
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 : αˣ) → βˣ)
have refine : IsClosedEmbedding.{u, v} (X := αˣ) (Y := β × βᵐᵒᵖ)
  (comp (β := βˣ) (⇑(embedProduct β) : (a : βˣ) → β × βᵐᵒᵖ) (⇑(map f) : (a : αˣ) → βˣ))
Tactic: refine .of_comp isEmbedding_embedProduct ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
Goal:
α : Type u
inst : Monoid α
inst_1 : TopologicalSpace α
inst_2 : T1Space α
inst_3 : ContinuousMul α
S : Submonoid α
hS : IsCompact (↑S : Set α)
⊢ IsCompact (↑S.units : Set αˣ)
have this : IsCompact ((↑S : Set α) ×ˢ (↑S.op : Set αᵐᵒᵖ))
Tactic: have : IsCompact (S ×ˢ S.op) := hS.prod (opHomeomorph.isCompact_preimage.mp hS)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
⊢ IsTopologicalGroup G
have rw : IsTopologicalGroup G
Tactic: rw [inf_eq_iInf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
⊢ IsTopologicalGroup G
have refine : ∀ (b : Bool), IsTopologicalGroup G
Tactic: refine topologicalGroup_iInf fun b => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
b : Bool
⊢ IsTopologicalGroup G
have false : IsTopologicalGroup G
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
b : Bool
false : IsTopologicalGroup G
⊢ IsTopologicalGroup G
have true : IsTopologicalGroup G
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.ClosedSubgroup (goal)
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
A B : ClosedSubgroup G
h : (↑A : Subgroup G) = (↑B : Subgroup G)
⊢ A = B
have carrier : ∀ (x : G), x ∈ (↑A : Subgroup G).carrier ↔ x ∈ (↑B : Subgroup G).carrier
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.ClosedSubgroup (goal)
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
A B : ClosedSubgroup G
h : (↑A : Subgroup G) = (↑B : Subgroup G)
x : G
⊢ x ∈ (↑A : Subgroup G).carrier ↔ x ∈ (↑B : Subgroup G).carrier
have carrier : x ∈ (↑B : Subgroup G).carrier ↔ x ∈ (↑B : Subgroup G).carrier
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.ClosedSubgroup (goal)
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
h : IsClosed (↑H : Set G)
⊢ IsClosed (↑H.normalCore : Set G)
have rw : IsClosed (↑(⨅ (g : ConjAct G), g • H) : Set G)
Tactic: rw [normalCore_eq_iInf_conjAct]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.ClosedSubgroup (goal)
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
h : IsClosed (↑H : Set G)
⊢ IsClosed (↑(⨅ (g : ConjAct G), g • H) : Set G)
have push_cast : IsClosed.{u} (X := G) (⋂ (i : ConjAct G), i • (↑H : Set G))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.ClosedSubgroup (goal)
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
h : IsClosed (↑H : Set G)
⊢ IsClosed.{u} (X := G) (⋂ (i : ConjAct G), i • (↑H : Set G))
have h₁ : ∀ (i : ConjAct G), IsClosed (i • (↑H : Set G))
Tactic: apply isClosed_iInter
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.ClosedSubgroup (goal)
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 (g • (↑H : Set G))
have 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)
Tactic: convert! IsClosed.preimage (IsTopologicalGroup.continuous_conj (ConjAct.ofConjAct g⁻¹)) h using 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.ClosedSubgroup (hypothesis)
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)
⊢ IsOpen (↑H : Set G)
have h₁ : T1Space.{u} (G ⧸ H)
Tactic: rw [← QuotientGroup.t1Space_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.ClosedSubgroup (goal)
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)
⊢ IsOpen (↑H : Set G)
have rw : DiscreteTopology.{u} (G ⧸ H)
Tactic: rw [← QuotientGroup.discreteTopology_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.CompactOpen (goal)
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)}
have 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)
Tactic: refine Set.Subset.antisymm (Set.range_subset_iff.2 fun f ↦ ⟨map_one f, map_mul f⟩) ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.CompactOpen (goal)
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)) (Set.range (ι := A →ₜ* B) toContinuousMap)
have 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)})
Tactic: simp only [range_toContinuousMap, Set.setOf_and, Set.setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.CompactOpen (goal)
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)})
have refine : ∀ (x y : A),
  IsClosed (X := C(A, B))
    {x_1 : C(A, B) |
      (x_1 : (a : A) → B) (x * y) = HMul.hMul (α := B) (β := B) ((x_1 : (a : A) → B) x : B) ((x_1 : (a : A) → B) y : B)}
Tactic: refine .inter (isClosed_singleton.preimage (continuous_eval_const 1)) <|
      isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.CompactOpen (hypothesis)
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
h :
  EquicontinuousAt (X := X) (α := Y)
    (fun (f : (↑{f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U V} : Type (max u_7 u_8))) ↦
      (⇑(↑f : X →* Y) : (a : X) → Y))
    1
⊢ LocallyCompactSpace (X →ₜ* Y)
have h₁ : Equicontinuous (ι := (↑{f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U V} : Type (max u_7 u_8))) (X := X) (α := Y)
  (DFunLike.coe (β := fun (x : X) ↦ Y) ∘
    Subtype.val (p := fun (x : X →* Y) ↦
      Membership.mem (γ := Set (X →* Y)) {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U V} x))
Tactic: replace h := equicontinuous_of_equicontinuousAt_one _ h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.CompactOpen (goal)
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
h :
  Equicontinuous (ι := (↑{f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U V} : Type (max u_7 u_8))) (X := X) (α := Y)
    (DFunLike.coe (β := fun (x : X) ↦ Y) ∘
      Subtype.val (p := fun (x : X →* Y) ↦
        Membership.mem (γ := Set (X →* Y)) {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U V} x))
⊢ LocallyCompactSpace (X →ₜ* Y)
have obtain : ∀ (W : Set Y) (hWo : Membership.mem (γ := Filter Y) (𝓝 1) W) (hWV : W ⊆ V) (hWc : IsCompact W),
  LocallyCompactSpace (X →ₜ* Y)
Tactic: obtain ⟨W, hWo, hWV, hWc⟩ := local_compact_nhds hV
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.CompactOpen (hypothesis)
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
h :
  Equicontinuous (ι := (↑{f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U V} : Type (max u_7 u_8))) (X := X) (α := Y)
    (DFunLike.coe (β := fun (x : X) ↦ Y) ∘
      Subtype.val (p := fun (x : X →* Y) ↦
        Membership.mem (γ := Set (X →* Y)) {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U V} x))
W : Set Y
hWo : Membership.mem (γ := Filter Y) (𝓝 1) W
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S2 : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe (β := fun (x : X) ↦ Y) '' S3
⊢ LocallyCompactSpace (X →ₜ* Y)
have h₁ : Equicontinuous (X := X) (α := Y) fun (x : (↑S1 : Type (max u_7 u_8))) ↦ (⇑(↑x : X →* Y) : (a : X) → Y)
Tactic: replace h : Equicontinuous ((↑) : S1 → X → Y) :=
    h.comp (Subtype.map _root_.id fun f hf ↦ hf.mono_right hWV)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.CompactOpen (goal)
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
W : Set Y
hWo : Membership.mem (γ := Filter Y) (𝓝 1) W
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S2 : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe (β := fun (x : X) ↦ Y) '' S3
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S1 : Type (max u_7 u_8))) ↦ (⇑(↑x : X →* Y) : (a : X) → Y)
⊢ S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1
have h₁ : ∀ (x : X → Y), x ∈ S4 ↔ Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.CompactOpen (goal)
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
W : Set Y
hWo : Membership.mem (γ := Filter Y) (𝓝 1) W
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S2 : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe (β := fun (x : X) ↦ Y) '' S3
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S1 : Type (max u_7 u_8))) ↦ (⇑(↑x : X →* Y) : (a : X) → Y)
x : X → Y
⊢ x ∈ S4 ↔ Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x
have h₁ : x ∈ S4 → Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.CompactOpen (goal)
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
W : Set Y
hWo : Membership.mem (γ := Filter Y) (𝓝 1) W
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S2 : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe (β := fun (x : X) ↦ Y) '' S3
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S1 : Type (max u_7 u_8))) ↦ (⇑(↑x : X →* Y) : (a : X) → Y)
x : X → Y
h₁ : x ∈ S4 → Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x
⊢ x ∈ S4 ↔ Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x
have h₂ : Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x → x ∈ S4
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.CompactOpen (hypothesis)
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
W : Set Y
hWo : Membership.mem (γ := Filter Y) (𝓝 1) W
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S2 : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe (β := fun (x : X) ↦ Y) '' S3
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S1 : Type (max u_7 u_8))) ↦ (⇑(↑x : X →* Y) : (a : X) → Y)
⊢ LocallyCompactSpace (X →ₜ* Y)
have hS4 : S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1
Tactic: have hS4 : S4 = (↑) '' S1 := by
    ext
    constructor
    · rintro ⟨-, ⟨f, hf, rfl⟩, rfl⟩
      exact ⟨f, hf, rfl⟩
    · rintro ⟨f, hf, rfl⟩
      exact ⟨⟨f, h.continuous ⟨f, hf⟩⟩, ⟨⟨f, h.continuous ⟨f, hf⟩⟩, hf, rfl⟩, rfl⟩