awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
hS4 : S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1
⊢ Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
have rw : ∀
  (h :
    Equicontinuous (ι :=
      { x : X → Y // Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x })
      (Subtype.val (p := fun (x : X → Y) ↦
        Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x)))
  (hS4 : S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1),
  Equicontinuous (ι := { x : X → Y // Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S3) x })
    (Subtype.val (p := fun (x : X → Y) ↦
      Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S3) x))
Tactic: rw [equicontinuous_iff_range, ← Set.image_eq_range] at h ⊢
Cleared hypotheses: h, hS4
-- 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 // Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x })
    (Subtype.val (p := fun (x : X → Y) ↦
      Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x))
hS4 : S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1
⊢ Equicontinuous (ι := { x : X → Y // Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S3) x })
    (Subtype.val (p := fun (x : X → Y) ↦
      Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S3) x))
have rwa : ∀ (h : Equicontinuous (ι := { x : X → Y // x ∈ S4 }) (Subtype.val (p := fun (x : X → Y) ↦ x ∈ S4)))
  (hS4 : S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1),
  Equicontinuous (ι := { x : X → Y // Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S3) x })
    (Subtype.val (p := fun (x : X → Y) ↦
      Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S3) x))
Tactic: rwa [← hS4] at h
Cleared hypotheses: h, hS4
-- 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)
hS4 : S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1
⊢ LocallyCompactSpace (X →ₜ* Y)
have h₁ : Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
Tactic: replace h : Equicontinuous ((↑) : S3 → X → Y) := by
    rw [equicontinuous_iff_range, ← Set.image_eq_range] at h ⊢
    rwa [← hS4] at 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
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
hS4 : S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
⊢ S4 = (U.pi (α := fun (x : X) ↦ Y) fun (x : X) ↦ W) ∩ Set.range (ι := X →* Y) (DFunLike.coe (β := fun (x : X) ↦ Y))
have simp_rw : ∀ (x : X → Y),
  (∃ (x_1 : X →* Y), Set.MapsTo (⇑x_1 : (a : X) → Y) U W ∧ (⇑x_1 : (a : X) → Y) = x) ↔
    Membership.mem (γ := Set (X → Y))
      ((U.pi (α := fun (x : X) ↦ Y) fun (x : X) ↦ W) ∩ Set.range (ι := X →* Y) (DFunLike.coe (β := fun (x : X) ↦ Y))) x
Tactic: simp_rw [hS4, Set.ext_iff, Set.mem_image, S1, Set.mem_setOf_eq]
-- 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
hS4 : S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
⊢ LocallyCompactSpace (X →ₜ* Y)
have hS4₁ : S4 = (U.pi (α := fun (x : X) ↦ Y) fun (x : X) ↦ W) ∩ Set.range (ι := X →* Y) (DFunLike.coe (β := fun (x : X) ↦ Y))
Tactic: replace hS4 : S4 = Set.pi U (fun _ ↦ W) ∩ Set.range ((↑) : (X →* Y) → (X → Y)) := by
    simp_rw [hS4, Set.ext_iff, Set.mem_image, S1, Set.mem_setOf_eq]
    exact fun f ↦ ⟨fun ⟨g, hg, hf⟩ ↦ hf ▸ ⟨hg, g, rfl⟩, fun ⟨hg, g, hf⟩ ↦ ⟨g, hf ▸ hg, hf⟩⟩
Cleared hypotheses: hS4
-- 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 : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
hS4 : S4 = (U.pi (α := fun (x : X) ↦ Y) fun (x : X) ↦ W) ∩ Set.range (ι := X →* Y) (DFunLike.coe (β := fun (x : X) ↦ Y))
⊢ LocallyCompactSpace (X →ₜ* Y)
have hS4₁ : IsClosed[Pi.topologicalSpace] S4
Tactic: replace hS4 : IsClosed S4 :=
    hS4.symm ▸ (isClosed_set_pi (fun _ _ ↦ hWc.isClosed)).inter (MonoidHom.isClosed_range_coe X Y)
Cleared hypotheses: hS4
-- 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 : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
hS4 : IsClosed[Pi.topologicalSpace] S4
T : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U (interior W)}
⊢ (interior S2).Nonempty
have h1 : T.Nonempty
Tactic: have h1 : T.Nonempty := ⟨1, fun _ _ ↦ mem_interior_iff_mem_nhds.mpr hWo⟩
-- 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 : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
hS4 : IsClosed[Pi.topologicalSpace] S4
T : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U (interior W)}
h1 : T.Nonempty
⊢ (interior S2).Nonempty
have h2 : T ⊆ S2
Tactic: have h2 : T ⊆ S2 := fun f hf ↦ hf.mono_right interior_subset
-- 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 : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
hS4 : IsClosed[Pi.topologicalSpace] S4
T : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U (interior W)}
h1 : T.Nonempty
h2 : T ⊆ S2
⊢ (interior S2).Nonempty
have h3 : IsOpen T
Tactic: have h3 : IsOpen T := isOpen_induced (ContinuousMap.isOpen_setOf_mapsTo hU isOpen_interior)
-- 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 : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
hS4 : IsClosed[Pi.topologicalSpace] S4
⊢ LocallyCompactSpace (X →ₜ* Y)
have hS2 : (interior S2).Nonempty
Tactic: have hS2 : (interior S2).Nonempty := by
    let T : Set (ContinuousMonoidHom X Y) := {f | Set.MapsTo f U (interior W)}
    have h1 : T.Nonempty := ⟨1, fun _ _ ↦ mem_interior_iff_mem_nhds.mpr hWo⟩
    have h2 : T ⊆ S2 := fun f hf ↦ hf.mono_right interior_subset
    have h3 : IsOpen T := isOpen_induced (ContinuousMap.isOpen_setOf_mapsTo hU isOpen_interior)
    exact h1.mono (interior_maximal h2 h3)
-- 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
inst_8 : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : Filter.HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) V
⊢ LocallyCompactSpace (X →ₜ* Y)
have obtain : ∀ (U0 : Set X) (hU0c : IsCompact U0) (hU0o : Membership.mem (γ := Filter X) (𝓝 1) U0), LocallyCompactSpace (X →ₜ* Y)
Tactic: obtain ⟨U0, hU0c, hU0o⟩ := exists_compact_mem_nhds (1 : X)
-- 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
inst_8 : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : Filter.HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : Membership.mem (γ := Filter X) (𝓝 1) U0
U_aux : ℕ → (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7) :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7))
      (Subtype.mk (p := fun (x : Set X) ↦
        Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x) U0 hU0o)
      (fun (x : ℕ) (S : (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7)) ↦
        let h := ⋯;
        Subtype.mk (p := fun (x : Set X) ↦
          Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x)
          (Classical.choose (p := fun (x : Set X) ↦
            Membership.mem (γ := Filter X) (𝓝 1) x ∧ IsClosed[inst] x ∧ x⁻¹ = x ∧ x * x ⊆ (↑S : Set X)) h)
          ⋯)
      t
U : ℕ → Set X := fun (n : ℕ) ↦ (↑(U_aux n) : Set X)
⊢ LocallyCompactSpace (X →ₜ* Y)
have hU1 : ∀ (n : ℕ), Membership.mem (γ := Filter X) (𝓝 1) (U n)
Tactic: have hU1 : ∀ n, U n ∈ nhds 1 := fun n ↦ (U_aux n).2
-- 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
inst_8 : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : Filter.HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : Membership.mem (γ := Filter X) (𝓝 1) U0
U_aux : ℕ → (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7) :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7))
      (Subtype.mk (p := fun (x : Set X) ↦
        Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x) U0 hU0o)
      (fun (x : ℕ) (S : (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7)) ↦
        let h := ⋯;
        Subtype.mk (p := fun (x : Set X) ↦
          Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x)
          (Classical.choose (p := fun (x : Set X) ↦
            Membership.mem (γ := Filter X) (𝓝 1) x ∧ IsClosed[inst] x ∧ x⁻¹ = x ∧ x * x ⊆ (↑S : Set X)) h)
          ⋯)
      t
U : ℕ → Set X := fun (n : ℕ) ↦ (↑(U_aux n) : Set X)
hU1 : ∀ (n : ℕ), Membership.mem (γ := Filter X) (𝓝 1) (U n)
⊢ LocallyCompactSpace (X →ₜ* Y)
have hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
Tactic: have hU2 : ∀ n, U (n + 1) * U (n + 1) ⊆ U n :=
    fun n ↦ (Classical.choose_spec (exists_closed_nhds_one_inv_eq_mul_subset (U_aux n).2)).2.2.2
-- 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
inst_8 : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : Filter.HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : Membership.mem (γ := Filter X) (𝓝 1) U0
U_aux : ℕ → (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7) :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7))
      (Subtype.mk (p := fun (x : Set X) ↦
        Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x) U0 hU0o)
      (fun (x : ℕ) (S : (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7)) ↦
        let h := ⋯;
        Subtype.mk (p := fun (x : Set X) ↦
          Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x)
          (Classical.choose (p := fun (x : Set X) ↦
            Membership.mem (γ := Filter X) (𝓝 1) x ∧ IsClosed[inst] x ∧ x⁻¹ = x ∧ x * x ⊆ (↑S : Set X)) h)
          ⋯)
      t
U : ℕ → Set X := fun (n : ℕ) ↦ (↑(U_aux n) : Set X)
hU1 : ∀ (n : ℕ), Membership.mem (γ := Filter X) (𝓝 1) (U n)
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
⊢ LocallyCompactSpace (X →ₜ* Y)
have hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
Tactic: have hU3 : ∀ n, U (n + 1) ⊆ U n :=
    fun n x hx ↦ hU2 n (mul_one x ▸ Set.mul_mem_mul hx (mem_of_mem_nhds (hU1 (n + 1))))
-- 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
inst_8 : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : Filter.HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : Membership.mem (γ := Filter X) (𝓝 1) U0
U_aux : ℕ → (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7) :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7))
      (Subtype.mk (p := fun (x : Set X) ↦
        Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x) U0 hU0o)
      (fun (x : ℕ) (S : (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7)) ↦
        let h := ⋯;
        Subtype.mk (p := fun (x : Set X) ↦
          Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x)
          (Classical.choose (p := fun (x : Set X) ↦
            Membership.mem (γ := Filter X) (𝓝 1) x ∧ IsClosed[inst] x ∧ x⁻¹ = x ∧ x * x ⊆ (↑S : Set X)) h)
          ⋯)
      t
U : ℕ → Set X := fun (n : ℕ) ↦ (↑(U_aux n) : Set X)
hU1 : ∀ (n : ℕ), Membership.mem (γ := Filter X) (𝓝 1) (U n)
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
f : X →* Y
hf : Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)
n : ℕ
zero : Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)
⊢ Set.MapsTo (⇑f : (a : X) → Y) (U n) (V n)
have succ : ∀ (n : ℕ) (ih : Set.MapsTo (⇑f : (a : X) → Y) (U n) (V n)), Set.MapsTo (⇑f : (a : X) → Y) (U (n + 1)) (V (n + 1))
Tactic: induction n with
    | zero => exact hf
    | succ n ih =>
      exact fun x hx ↦ hV (ih (hU3 n hx)) (map_mul f x x ▸ ih (hU2 n (Set.mul_mem_mul hx hx)))
Cleared hypotheses: n
-- 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
inst_8 : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : Filter.HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : Membership.mem (γ := Filter X) (𝓝 1) U0
U_aux : ℕ → (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7) :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7))
      (Subtype.mk (p := fun (x : Set X) ↦
        Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x) U0 hU0o)
      (fun (x : ℕ) (S : (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7)) ↦
        let h := ⋯;
        Subtype.mk (p := fun (x : Set X) ↦
          Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x)
          (Classical.choose (p := fun (x : Set X) ↦
            Membership.mem (γ := Filter X) (𝓝 1) x ∧ IsClosed[inst] x ∧ x⁻¹ = x ∧ x * x ⊆ (↑S : Set X)) h)
          ⋯)
      t
U : ℕ → Set X := fun (n : ℕ) ↦ (↑(U_aux n) : Set X)
hU1 : ∀ (n : ℕ), Membership.mem (γ := Filter X) (𝓝 1) (U n)
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
⊢ LocallyCompactSpace (X →ₜ* Y)
have hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f : (a : X) → Y) (U n) (V n)
Tactic: have hU4 : ∀ f : X →* Y, Set.MapsTo f (U 0) (V 0) → ∀ n, Set.MapsTo f (U n) (V n) := by
    intro f hf n
    induction n with
    | zero => exact hf
    | succ n ih =>
      exact fun x hx ↦ hV (ih (hU3 n hx)) (map_mul f x x ▸ ih (hU2 n (Set.mul_mem_mul hx hx)))