awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
h :
  (∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
    ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)
h₂ : ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
x_1 : Sigma σ
i : ι
x : σ i
⊢ range (Sigma.mk (β := σ) i) ∈ comap f (𝓝 (f (Sigma.mk (β := σ) i x)))
have refine_2 : ∀ (U : Set X) (hUo : IsOpen[inst_1] U) (hU : ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i),
  range (Sigma.mk (β := σ) i) ∈ comap f (𝓝 (f (Sigma.mk (β := σ) i x)))
Tactic: rcases h₂ i with ⟨U, hUo, hU⟩
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
h :
  (∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
    ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)
h₂ : ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
x_1 : Sigma σ
i : ι
x : σ i
U : Set X
hUo : IsOpen[inst_1] U
hU : ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
⊢ range (Sigma.mk (β := σ) i) ∈ comap f (𝓝 (f (Sigma.mk (β := σ) i x)))
have h : ∀ (y : Sigma σ) (hy : y ∈ f ⁻¹' U), Membership.mem (γ := Set (Sigma σ)) (range (Sigma.mk (β := σ) i)) y
Tactic: filter_upwards [preimage_mem_comap <| hUo.mem_nhds <| (hU _).2 rfl] with y hy
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (ULift.{v, u} X)
rw : IsOpen[induced down inst] s ↔ IsOpen[inst] (up ⁻¹' s)
rw₁ : IsOpen[induced (⇑Equiv.ulift : (a : ULift.{v, u} X) → X) inst] s ↔ IsOpen[inst] (up ⁻¹' s)
⊢ IsOpen[topologicalSpace] s ↔ IsOpen[inst] (up ⁻¹' s)
have rw₂ : IsOpen[coinduced (⇑Equiv.ulift.symm : (a : X) → ULift.{v, u} X) inst] s ↔ IsOpen[inst] (up ⁻¹' s)
Tactic: rw [ULift.topologicalSpace, ← Equiv.ulift_apply, ← Equiv.ulift.coinduced_symm, ← isOpen_coinduced]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (ULift.{v, u} X)
rw : IsOpen[induced down inst] s ↔ IsOpen[inst] (up ⁻¹' s)
rw₁ : IsOpen[induced (⇑Equiv.ulift : (a : ULift.{v, u} X) → X) inst] s ↔ IsOpen[inst] (up ⁻¹' s)
rw₂ : IsOpen[coinduced (⇑Equiv.ulift.symm : (a : X) → ULift.{v, u} X) inst] s ↔ IsOpen[inst] (up ⁻¹' s)
⊢ IsOpen[topologicalSpace] s ↔ IsOpen[inst] (up ⁻¹' s)
have rw₃ : IsOpen[coinduced (⇑Equiv.ulift.symm : (a : X) → ULift.{v, u} X) inst] s ↔ IsOpen[coinduced up inst] s
Tactic: rw [ULift.topologicalSpace, ← Equiv.ulift_apply, ← Equiv.ulift.coinduced_symm, ← isOpen_coinduced]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (ULift.{v, u} X)
⊢ IsClosed[topologicalSpace] s ↔ IsClosed[inst] (up ⁻¹' s)
have rw : IsOpen[topologicalSpace] sᶜ ↔ IsClosed[inst] (up ⁻¹' s)
Tactic: rw [← isOpen_compl_iff, ← isOpen_compl_iff, isOpen_iff, preimage_compl]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (ULift.{v, u} X)
rw : IsOpen[topologicalSpace] sᶜ ↔ IsClosed[inst] (up ⁻¹' s)
⊢ IsClosed[topologicalSpace] s ↔ IsClosed[inst] (up ⁻¹' s)
have rw₁ : IsOpen[topologicalSpace] sᶜ ↔ IsOpen[inst] (up ⁻¹' s)ᶜ
Tactic: rw [← isOpen_compl_iff, ← isOpen_compl_iff, isOpen_iff, preimage_compl]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (ULift.{v, u} X)
rw : IsOpen[topologicalSpace] sᶜ ↔ IsClosed[inst] (up ⁻¹' s)
rw₁ : IsOpen[topologicalSpace] sᶜ ↔ IsOpen[inst] (up ⁻¹' s)ᶜ
⊢ IsClosed[topologicalSpace] s ↔ IsClosed[inst] (up ⁻¹' s)
have rw₂ : IsOpen[inst] (up ⁻¹' sᶜ) ↔ IsOpen[inst] (up ⁻¹' s)ᶜ
Tactic: rw [← isOpen_compl_iff, ← isOpen_compl_iff, isOpen_iff, preimage_compl]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (ULift.{v, u} X)
rw : IsOpen[topologicalSpace] sᶜ ↔ IsClosed[inst] (up ⁻¹' s)
rw₁ : IsOpen[topologicalSpace] sᶜ ↔ IsOpen[inst] (up ⁻¹' s)ᶜ
rw₂ : IsOpen[inst] (up ⁻¹' sᶜ) ↔ IsOpen[inst] (up ⁻¹' s)ᶜ
⊢ IsClosed[topologicalSpace] s ↔ IsClosed[inst] (up ⁻¹' s)
have rw₃ : IsOpen[inst] (up ⁻¹' s)ᶜ ↔ IsOpen[inst] (up ⁻¹' s)ᶜ
Tactic: rw [← isOpen_compl_iff, ← isOpen_compl_iff, isOpen_iff, preimage_compl]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ Continuous[ULift.topologicalSpace, ULift.topologicalSpace] (ULift.map f)
have change : Continuous[ULift.topologicalSpace, ULift.topologicalSpace] (ULift.up ∘ f ∘ ULift.down)
Tactic: change Continuous (ULift.up ∘ f ∘ ULift.down)
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
t : Set (↑s : Type u)
ht : IsOpen[instTopologicalSpaceSubtype] t
hs : IsOpen[inst] s
⊢ IsOpen[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t)
have rcases : ∀ (s' : Set X) (hs' : IsOpen[inst] s') (ht : IsOpen[instTopologicalSpaceSubtype] (s ↓∩ s')),
  IsOpen[inst] (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (s ↓∩ s'))
Tactic: rcases isOpen_induced_iff.mp ht with ⟨s', hs', rfl⟩
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
s' : Set X
hs' : IsOpen[inst] s'
ht : IsOpen[instTopologicalSpaceSubtype] (s ↓∩ s')
⊢ IsOpen[inst] (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (s ↓∩ s'))
have rw : IsOpen[inst] (s ∩ s')
Tactic: rw [Subtype.image_preimage_coe]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
t : Set (↑s : Type u)
ht : IsClosed[instTopologicalSpaceSubtype] t
hs : IsClosed[inst] s
⊢ IsClosed[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t)
have rcases : ∀ (s' : Set X) (hs' : IsClosed[inst] s') (ht : IsClosed[instTopologicalSpaceSubtype] (s ↓∩ s')),
  IsClosed[inst] (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (s ↓∩ s'))
Tactic: rcases isClosed_induced_iff.mp ht with ⟨s', hs', rfl⟩
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsClosed[inst] s
s' : Set X
hs' : IsClosed[inst] s'
ht : IsClosed[instTopologicalSpaceSubtype] (s ↓∩ s')
⊢ IsClosed[inst] (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (s ↓∩ s'))
have rw : IsClosed[inst] (s ∩ s')
Tactic: rw [Subtype.image_preimage_coe]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
p : X × Y → Prop
⊢ (∀ᶠ (q : X × Y) in 𝓝ˢ (s ×ˢ t), p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ (px : X → Prop),
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧
            ∃ (py : Y → Prop), (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
have simp_rw : (∀ x ∈ s ×ˢ t, ∀ᶠ (q : X × Y) in 𝓝 x, p q) ↔
  ∀ x ∈ s,
    ∀ y ∈ t,
      ∃ (px : X → Prop),
        (∀ᶠ (x' : X) in 𝓝 x, px x') ∧
          ∃ (py : Y → Prop), (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
Tactic: simp_rw [eventually_nhdsSet_iff_forall, forall_prod_set, nhds_prod_eq, eventually_prod_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
p : X × Y → Prop
simp_rw :
  (∀ x ∈ s ×ˢ t, ∀ᶠ (q : X × Y) in 𝓝 x, p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ (px : X → Prop),
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧
            ∃ (py : Y → Prop), (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
⊢ (∀ᶠ (q : X × Y) in 𝓝ˢ (s ×ˢ t), p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ (px : X → Prop),
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧
            ∃ (py : Y → Prop), (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
have simp_rw₁ : (∀ x ∈ s, ∀ y ∈ t, ∀ᶠ (q : X × Y) in 𝓝 (x, y), p q) ↔
  ∀ x ∈ s,
    ∀ y ∈ t,
      ∃ (px : X → Prop),
        (∀ᶠ (x' : X) in 𝓝 x, px x') ∧
          ∃ (py : Y → Prop), (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
Tactic: simp_rw [eventually_nhdsSet_iff_forall, forall_prod_set, nhds_prod_eq, eventually_prod_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
p : X × Y → Prop
simp_rw :
  (∀ x ∈ s ×ˢ t, ∀ᶠ (q : X × Y) in 𝓝 x, p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ (px : X → Prop),
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧
            ∃ (py : Y → Prop), (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
simp_rw₁ :
  (∀ x ∈ s, ∀ y ∈ t, ∀ᶠ (q : X × Y) in 𝓝 (x, y), p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ (px : X → Prop),
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧
            ∃ (py : Y → Prop), (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
⊢ (∀ᶠ (q : X × Y) in 𝓝ˢ (s ×ˢ t), p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ (px : X → Prop),
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧
            ∃ (py : Y → Prop), (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
have simp_rw₂ : (∀ x ∈ s, ∀ y ∈ t, ∀ᶠ (q : X × Y) in 𝓝 x ×ˢ 𝓝 y, p q) ↔
  ∀ x ∈ s,
    ∀ y ∈ t,
      ∃ (px : X → Prop),
        (∀ᶠ (x' : X) in 𝓝 x, px x') ∧
          ∃ (py : Y → Prop), (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
Tactic: simp_rw [eventually_nhdsSet_iff_forall, forall_prod_set, nhds_prod_eq, eventually_prod_iff]
-- Lean 4 proof step from Mathlib.Topology.Continuous (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ Y
⊢ Continuous[inst_1, inst] (⇑e.symm : (a : Y) → X) ↔ IsOpenMap.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
have simp_rw : (∀ (s : Set X), IsOpen[inst] s → IsOpen[inst_1] ((⇑e.symm : (a : Y) → X) ⁻¹' s)) ↔
  IsOpenMap.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
Tactic: simp_rw [continuous_def, ← Equiv.image_eq_preimage_symm, IsOpenMap]
-- Lean 4 proof step from Mathlib.Topology.Continuous (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ Y
simp_rw :
  (∀ (s : Set X), IsOpen[inst] s → IsOpen[inst_1] ((⇑e.symm : (a : Y) → X) ⁻¹' s)) ↔
    IsOpenMap.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
⊢ Continuous[inst_1, inst] (⇑e.symm : (a : Y) → X) ↔ IsOpenMap.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
have simp_rw₁ : (∀ (s : Set X), IsOpen[inst] s → IsOpen[inst_1] ((⇑e : (a : X) → Y) '' s)) ↔
  IsOpenMap.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
Tactic: simp_rw [continuous_def, ← Equiv.image_eq_preimage_symm, IsOpenMap]
-- Lean 4 proof step from Mathlib.Topology.Continuous (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ Y
⊢ IsOpenMap.{u_2, u_1} (X := Y) (Y := X) (⇑e.symm : (a : Y) → X) ↔ Continuous[inst, inst_1] (⇑e : (a : X) → Y)
have simp_rw : Continuous[inst, inst_1] (⇑e.symm.symm : (a : X) → Y) ↔ Continuous[inst, inst_1] (⇑e : (a : X) → Y)
Tactic: simp_rw [← Equiv.continuous_symm_iff, Equiv.symm_symm]
-- Lean 4 proof step from Mathlib.Topology.Continuous (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : ∀ (s : Set Y), f ⁻¹' interior s ⊆ interior (f ⁻¹' s)
s : Set Y
hs : IsOpen[inst_1] s
⊢ f ⁻¹' s ⊆ interior (f ⁻¹' s)
have grw : f ⁻¹' s ⊆ f ⁻¹' interior s
Tactic: grw [← h, hs.interior_eq]
-- Lean 4 proof step from Mathlib.Topology.Continuous (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : ∀ (s : Set Y), f ⁻¹' interior s ⊆ interior (f ⁻¹' s)
s : Set Y
hs : IsOpen[inst_1] s
grw : f ⁻¹' s ⊆ f ⁻¹' interior s
⊢ f ⁻¹' s ⊆ interior (f ⁻¹' s)
have grw₁ : f ⁻¹' s ⊆ f ⁻¹' s
Tactic: grw [← h, hs.interior_eq]
-- Lean 4 proof step from Mathlib.Topology.Continuous (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
x : X
y : Y
g : Y → Z
hg : ContinuousAt g y
hf : ContinuousAt f x
hy : f x = y
⊢ ContinuousAt (g ∘ f) x
have hg₁ : ContinuousAt g (f x)
Tactic: subst hy
Cleared hypotheses: y, hg, hy
-- Lean 4 proof step from Mathlib.Topology.Continuous (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
t : Set Y
⊢ closure[inst] (f ⁻¹' t) ⊆ f ⁻¹' closure[inst_1] t
have rw : closure[inst] (f ⁻¹' t) ⊆ closure[inst] (f ⁻¹' closure[inst_1] t)
Tactic: rw [← (isClosed_closure.preimage hf).closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Continuous (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
t : Set Y
h : MapsTo f s t
hc : Continuous[inst, inst_1] f
⊢ MapsTo f (closure[inst] s) (closure[inst_1] t)
have simp : ∀ ⦃x : X⦄, ClusterPt x (𝓟 s) → ClusterPt (f x) (𝓟 t)
Tactic: simp only [MapsTo, mem_closure_iff_clusterPt]
-- Lean 4 proof step from Mathlib.Topology.Continuous (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : ∀ (s : Set X), f '' closure[inst] s ⊆ closure[inst_1] (f '' s)
s : Set Y
hs : IsClosed[inst_1] s
⊢ closure[inst] (f ⁻¹' s) ⊆ f ⁻¹' s
have grw : f ⁻¹' closure[inst_1] (f '' f ⁻¹' s) ⊆ f ⁻¹' s
Tactic: grw [image_subset_iff.mp <| h <| f ⁻¹' s, image_preimage_subset, hs.closure_subset]
-- Lean 4 proof step from Mathlib.Topology.Continuous (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : ∀ (s : Set X), f '' closure[inst] s ⊆ closure[inst_1] (f '' s)
s : Set Y
hs : IsClosed[inst_1] s
grw : f ⁻¹' closure[inst_1] (f '' f ⁻¹' s) ⊆ f ⁻¹' s
⊢ closure[inst] (f ⁻¹' s) ⊆ f ⁻¹' s
have grw₁ : f ⁻¹' closure[inst_1] s ⊆ f ⁻¹' s
Tactic: grw [image_subset_iff.mp <| h <| f ⁻¹' s, image_preimage_subset, hs.closure_subset]
-- Lean 4 proof step from Mathlib.Topology.Continuous (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : ∀ (s : Set X), f '' closure[inst] s ⊆ closure[inst_1] (f '' s)
s : Set Y
hs : IsClosed[inst_1] s
grw : f ⁻¹' closure[inst_1] (f '' f ⁻¹' s) ⊆ f ⁻¹' s
grw₁ : f ⁻¹' closure[inst_1] s ⊆ f ⁻¹' s
⊢ closure[inst] (f ⁻¹' s) ⊆ f ⁻¹' s
have grw₂ : f ⁻¹' s ⊆ f ⁻¹' s
Tactic: grw [image_subset_iff.mp <| h <| f ⁻¹' s, image_preimage_subset, hs.closure_subset]
-- Lean 4 proof step from Mathlib.Topology.Continuous (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
l : Filter X
l' : Filter Y
h : Tendsto f l l'
s : Set Y
hs : s ∈ l'
⊢ ∀ᶠ (a : X) in l.lift' closure[inst], f a ∈ closure[inst_1] s
have h₁ : ∀ (a : X),
  Membership.mem (γ := Set X)
    {x : X |
      x ∈ closure[inst] (f ⁻¹' s) → Membership.mem (γ := Set X) {x : X | (fun (a : X) ↦ f a ∈ closure[inst_1] s) x} x}
    a
Tactic: filter_upwards [mem_lift' (h hs)] using (mapsTo_preimage _ _).closure hf
-- Lean 4 proof step from Mathlib.Topology.Continuous (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
l : Filter X
l' : Filter Y
h : Tendsto f l l'
s : Set Y
hs : s ∈ l'
h₁ :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        x ∈ closure[inst] (f ⁻¹' s) → Membership.mem (γ := Set X) {x : X | (fun (a : X) ↦ f a ∈ closure[inst_1] s) x} x}
      a
⊢ ∀ᶠ (a : X) in l.lift' closure[inst], f a ∈ closure[inst_1] s
have h₂ : ∀ a ∈ closure[inst] (f ⁻¹' s), f a ∈ closure[inst_1] s
Tactic: filter_upwards [mem_lift' (h hs)] using (mapsTo_preimage _ _).closure hf
-- Lean 4 proof step from Mathlib.Topology.Continuous (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hf : Continuous[inst, inst_1] f
hs : Dense s
⊢ range f ⊆ closure[inst_1] (f '' s)
have rw : f '' closure[inst] s ⊆ closure[inst_1] (f '' s)
Tactic: rw [← image_univ, ← hs.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Continuous (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_4
f : α → X
s : Set X
hf : DenseRange f
hs : IsOpen[inst] s
⊢ s ⊆ closure[inst] (f '' f ⁻¹' s)
have rw : s ⊆ closure[inst] (s ∩ range f)
Tactic: rw [image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.Topology.Continuous (goal)
Goal:
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
α : Type u_4
g : Y → Z
f : α → Y
hg : DenseRange g
hf : DenseRange f
cg : Continuous[inst, inst_1] g
⊢ DenseRange (g ∘ f)
have rw : Dense (g '' range f)
Tactic: rw [DenseRange, range_comp]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : LocallyCompactSpace α
inst_3 : Mul β
inst_4 : ContinuousMul β
⊢ Continuous (Y := C(α, β)) fun (p : C(α, β) × C(α, β)) ↦ p.1 * p.2
have refine : Continuous (X := (C(α, β) × C(α, β)) × α) (Y := β)
  (Function.uncurry fun (x : C(α, β) × C(α, β)) (y : α) ↦ (x.1 * x.2 : (a : α) → β) y)
Tactic: refine continuous_of_continuous_uncurry _ ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : LocallyCompactSpace α
inst_3 : Mul β
inst_4 : ContinuousMul β
⊢ Continuous (X := (C(α, β) × C(α, β)) × α) (Y := β)
    (Function.uncurry fun (x : C(α, β) × C(α, β)) (y : α) ↦ (x.1 * x.2 : (a : α) → β) y)
have h1 : Continuous (Y := β) fun (x : (C(α, β) × C(α, β)) × α) ↦ (x.1.1 : (a : α) → β) x.2
Tactic: have h1 : Continuous fun x : (C(α, β) × C(α, β)) × α => x.fst.fst x.snd :=
      continuous_eval.comp (continuous_fst.prodMap continuous_id)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : LocallyCompactSpace α
inst_3 : Mul β
inst_4 : ContinuousMul β
h1 : Continuous (Y := β) fun (x : (C(α, β) × C(α, β)) × α) ↦ (x.1.1 : (a : α) → β) x.2
⊢ Continuous (X := (C(α, β) × C(α, β)) × α) (Y := β)
    (Function.uncurry fun (x : C(α, β) × C(α, β)) (y : α) ↦ (x.1 * x.2 : (a : α) → β) y)
have h2 : Continuous (Y := β) fun (x : (C(α, β) × C(α, β)) × α) ↦ (x.1.2 : (a : α) → β) x.2
Tactic: have h2 : Continuous fun x : (C(α, β) × C(α, β)) × α => x.fst.snd x.snd :=
      continuous_eval.comp (continuous_snd.prodMap continuous_id)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommGroup β
inst_3 : IsTopologicalGroup β
this : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
⊢ Continuous (Y := C(α, β)) fun (p : C(α, β) × C(α, β)) ↦ p.1 * p.2
have this₁ : IsUniformGroup β
Tactic: have : IsUniformGroup β := isUniformGroup_of_commGroup
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommGroup β
inst_3 : IsTopologicalGroup β
this_1 : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
⊢ Continuous (Y := C(α, β)) fun (p : C(α, β) × C(α, β)) ↦ p.1 * p.2
have rw : ∀ (x : C(α, β) × C(α, β)), ContinuousAt (Y := C(α, β)) (fun (p : C(α, β) × C(α, β)) ↦ p.1 * p.2) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommGroup β
inst_3 : IsTopologicalGroup β
this_1 : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
f g : C(α, β)
⊢ ContinuousAt (Y := C(α, β)) (fun (p : C(α, β) × C(α, β)) ↦ p.1 * p.2) (f, g)
have rw : ∀ (K : Set α),
  IsCompact K →
    TendstoUniformlyOn (β := β) (fun (i : C(α, β) × C(α, β)) (a : α) ↦ (i.1 * i.2 : (a : α) → β) a)
      (⇑((f, g).1 * (f, g).2) : (a : α) → β) (nhds f ×ˢ nhds g) K
Tactic: rw [ContinuousAt, tendsto_iff_forall_isCompact_tendstoUniformlyOn, nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommGroup β
inst_3 : IsTopologicalGroup β
this : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
⊢ Continuous (Y := C(α, β)) fun (a : C(α, β)) ↦ a⁻¹
have this₁ : IsUniformGroup β
Tactic: have : IsUniformGroup β := isUniformGroup_of_commGroup
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommGroup β
inst_3 : IsTopologicalGroup β
this_1 : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
⊢ Continuous (Y := C(α, β)) fun (a : C(α, β)) ↦ a⁻¹
have rw : ∀ (x : C(α, β)), ContinuousAt (Y := C(α, β)) (fun (a : C(α, β)) ↦ a⁻¹) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommGroup β
inst_3 : IsTopologicalGroup β
this_1 : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
f : C(α, β)
⊢ ContinuousAt (Y := C(α, β)) (fun (a : C(α, β)) ↦ a⁻¹) f
have rw : ∀ (K : Set α),
  IsCompact K →
    TendstoUniformlyOn (β := β) (fun (i : C(α, β)) (a : α) ↦ (i⁻¹ : (a : α) → β) a) (⇑f⁻¹ : (a : α) → β) (nhds f) K
Tactic: rw [ContinuousAt, tendsto_iff_forall_isCompact_tendstoUniformlyOn]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : IsTopologicalSemiring A
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
⊢ Eq (α := C(α, A)) { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) 1, continuous_toFun := ⋯ } 1
have h : ∀ (a : α),
  Eq.{u_3 + 1} (α := A)
    (({ toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) 1, continuous_toFun := sorry } : (a : α) → A) a : A)
    ((1 : (a : α) → A) a : A)
Tactic: ext _
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Algebra (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : IsTopologicalSemiring A
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
c₁ c₂ : R
⊢ { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) (c₁ * c₂), continuous_toFun := ⋯ } =
    HMul.hMul (α := C(α, A))
      { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₁, continuous_toFun := ⋯ : C(α, A) }
      { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₂, continuous_toFun := ⋯ : C(α, A) }
have h : ∀ (a : α),
  Eq.{u_3 + 1} (α := A)
    (({ toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) (c₁ * c₂), continuous_toFun := sorry } : (a : α) → A) a : A)
    ((HMul.hMul (α := C(α, A))
            { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₁, continuous_toFun := sorry : C(α, A) }
            { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₂, continuous_toFun := sorry : C(α, A) } :
          (a : α) → A)
        a :
      A)
Tactic: ext _