awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
simp_rw :
  inst =
    induced (Y := Set α) (fun (x : α) ↦ {x})
      (generateFrom
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₁ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₂ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x}) (powerset '' {U : Set α | IsOpen[inst] U}) ∪
        image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
          ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₃ :
  inst =
    generateFrom
      ((fun (x : Set α) ↦ (fun (x : α) ↦ {x}) ⁻¹' 𝒫 x) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (x : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {s : Set α | (s ∩ x).Nonempty}) ''
          {U : Set α | IsOpen[inst] U})
simp_rw₄ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {t : Set α | t ⊆ a}) ''
          {U : Set α | IsOpen[inst] U} ∪
        (fun (x : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {s : Set α | (s ∩ x).Nonempty}) ''
          {U : Set α | IsOpen[inst] U})
simp_rw₅ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ {a_1 : α | {a_1} ⊆ a}) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (a : Set α) ↦ {a_1 : α | ({a_1} ∩ a).Nonempty}) '' {U : Set α | IsOpen[inst] U})
simp_rw₆ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (a : Set α) ↦ {a_1 : α | ({a_1} ∩ a).Nonempty}) '' {U : Set α | IsOpen[inst] U})
simp_rw₇ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U})
⊢ inst = induced (fun (x : α) ↦ {x}) (TopologicalSpace.vietoris α)
have simp_rw₈ : inst = generateFrom ((fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U})
Tactic: simp_rw [TopologicalSpace.vietoris, induced_generateFrom_eq, image_union, image_image,
      powerset, preimage_setOf_eq, singleton_subset_iff, singleton_inter_nonempty, union_self,
      setOf_mem_eq, image_id', generateFrom_setOf_isOpen]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
simp_rw :
  inst =
    induced (Y := Set α) (fun (x : α) ↦ {x})
      (generateFrom
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₁ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₂ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x}) (powerset '' {U : Set α | IsOpen[inst] U}) ∪
        image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
          ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₃ :
  inst =
    generateFrom
      ((fun (x : Set α) ↦ (fun (x : α) ↦ {x}) ⁻¹' 𝒫 x) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (x : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {s : Set α | (s ∩ x).Nonempty}) ''
          {U : Set α | IsOpen[inst] U})
simp_rw₄ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {t : Set α | t ⊆ a}) ''
          {U : Set α | IsOpen[inst] U} ∪
        (fun (x : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {s : Set α | (s ∩ x).Nonempty}) ''
          {U : Set α | IsOpen[inst] U})
simp_rw₅ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ {a_1 : α | {a_1} ⊆ a}) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (a : Set α) ↦ {a_1 : α | ({a_1} ∩ a).Nonempty}) '' {U : Set α | IsOpen[inst] U})
simp_rw₆ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (a : Set α) ↦ {a_1 : α | ({a_1} ∩ a).Nonempty}) '' {U : Set α | IsOpen[inst] U})
simp_rw₇ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U})
simp_rw₈ : inst = generateFrom ((fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U})
⊢ inst = induced (fun (x : α) ↦ {x}) (TopologicalSpace.vietoris α)
have simp_rw₉ : inst = generateFrom ((fun (a : Set α) ↦ a) '' {U : Set α | IsOpen[inst] U})
Tactic: simp_rw [TopologicalSpace.vietoris, induced_generateFrom_eq, image_union, image_image,
      powerset, preimage_setOf_eq, singleton_subset_iff, singleton_inter_nonempty, union_self,
      setOf_mem_eq, image_id', generateFrom_setOf_isOpen]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
simp_rw :
  inst =
    induced (Y := Set α) (fun (x : α) ↦ {x})
      (generateFrom
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₁ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₂ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x}) (powerset '' {U : Set α | IsOpen[inst] U}) ∪
        image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
          ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₃ :
  inst =
    generateFrom
      ((fun (x : Set α) ↦ (fun (x : α) ↦ {x}) ⁻¹' 𝒫 x) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (x : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {s : Set α | (s ∩ x).Nonempty}) ''
          {U : Set α | IsOpen[inst] U})
simp_rw₄ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {t : Set α | t ⊆ a}) ''
          {U : Set α | IsOpen[inst] U} ∪
        (fun (x : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {s : Set α | (s ∩ x).Nonempty}) ''
          {U : Set α | IsOpen[inst] U})
simp_rw₅ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ {a_1 : α | {a_1} ⊆ a}) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (a : Set α) ↦ {a_1 : α | ({a_1} ∩ a).Nonempty}) '' {U : Set α | IsOpen[inst] U})
simp_rw₆ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (a : Set α) ↦ {a_1 : α | ({a_1} ∩ a).Nonempty}) '' {U : Set α | IsOpen[inst] U})
simp_rw₇ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U})
simp_rw₈ : inst = generateFrom ((fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U})
simp_rw₉ : inst = generateFrom ((fun (a : Set α) ↦ a) '' {U : Set α | IsOpen[inst] U})
⊢ inst = induced (fun (x : α) ↦ {x}) (TopologicalSpace.vietoris α)
have simp_rw₁₀ : inst = generateFrom {U : Set α | IsOpen[inst] U}
Tactic: simp_rw [TopologicalSpace.vietoris, induced_generateFrom_eq, image_union, image_image,
      powerset, preimage_setOf_eq, singleton_subset_iff, singleton_inter_nonempty, union_self,
      setOf_mem_eq, image_id', generateFrom_setOf_isOpen]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
⊢ IsClosed[t] (range fun (x : α) ↦ {x})
have rw : ∀ (x : Set α), Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ x → (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 x
Tactic: rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
s : Set α
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ s
⊢ (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 s
have inl : ∀ (hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ ∅),
  Membership.mem (γ := Filter (Set α)) (𝓝 ∅) (range fun (x : α) ↦ {x})ᶜ
Tactic: rcases Set.eq_empty_or_nonempty s with rfl | h
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
s : Set α
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ s
inl :
  ∀ (hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ ∅),
    Membership.mem (γ := Filter (Set α)) (𝓝 ∅) (range fun (x : α) ↦ {x})ᶜ
⊢ (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 s
have inr : ∀ (h : s.Nonempty), (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 s
Tactic: rcases Set.eq_empty_or_nonempty s with rfl | h
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ ∅
⊢ Membership.mem (γ := Filter (Set α)) (𝓝 ∅) (range fun (x : α) ↦ {x})ᶜ
have inl : Membership.mem (γ := Filter (Set α)) (pure ∅) (range fun (x : α) ↦ {x})ᶜ
Tactic: rwa [(isOpen_singleton_iff_nhds_eq_pure _).mp h₁, Filter.mem_pure]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
s : Set α
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ s
h : s.Nonempty
⊢ (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 s
have inr : ∀ (x : α) (hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ {x}) (h : Set.Nonempty (α := α) {x}),
  Membership.mem (γ := Filter (Set α)) (𝓝 {x}) (range fun (x : α) ↦ {x})ᶜ
Tactic: rcases h.exists_eq_singleton_or_nontrivial with ⟨x, rfl⟩ | ⟨x, hx, y, hy, hxy⟩
Cleared hypotheses: s, hs, h
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
s : Set α
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ s
h : s.Nonempty
inr :
  ∀ (x : α) (hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ {x}) (h : Set.Nonempty (α := α) {x}),
    Membership.mem (γ := Filter (Set α)) (𝓝 {x}) (range fun (x : α) ↦ {x})ᶜ
⊢ (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 s
have inr₁ : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s) (hxy : x ≠ y), (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 s
Tactic: rcases h.exists_eq_singleton_or_nontrivial with ⟨x, rfl⟩ | ⟨x, hx, y, hy, hxy⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
s : Set α
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ s
h : s.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 s
have inr : ∀ (U V : Set α) (hU : IsOpen[inst] U) (hV : IsOpen[inst] V) (hxU : x ∈ U) (hyV : y ∈ V) (hUV : Disjoint U V),
  (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 s
Tactic: obtain ⟨U, V, hU, hV, hxU, hyV, hUV⟩ := t2_separation hxy
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
s : Set α
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ s
h : s.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
U V : Set α
hU : IsOpen[inst] U
hV : IsOpen[inst] V
hxU : x ∈ U
hyV : y ∈ V
hUV : Disjoint U V
⊢ (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 s
have h₃ : ∀ (a : Set α),
  Membership.mem (γ := Set (Set α)) ({s : Set α | (s ∩ U).Nonempty} ∩ {s : Set α | (s ∩ V).Nonempty}) a →
    Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ a
Tactic: filter_upwards [(h₂ hU).inter (h₂ hV) |>.mem_nhds ⟨⟨x, hx, hxU⟩, ⟨y, hy, hyV⟩⟩]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
s : Set α
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ s
h : s.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
U V : Set α
hU : IsOpen[inst] U
hV : IsOpen[inst] V
hxU : x ∈ U
hyV : y ∈ V
hUV : Disjoint U V
z : α
hzU : Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ U).Nonempty} ((fun (x : α) ↦ ({x} : Set α)) z)
hzV : Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ V).Nonempty} ((fun (x : α) ↦ ({x} : Set α)) z)
⊢ False
have hzU₁ : z ∈ U
Tactic: rw [Set.mem_setOf, Set.singleton_inter_nonempty] at hzU hzV
Cleared hypotheses: hzU, hzV
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
s : Set α
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ s
h : s.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
U V : Set α
hU : IsOpen[inst] U
hV : IsOpen[inst] V
hxU : x ∈ U
hyV : y ∈ V
hUV : Disjoint U V
z : α
hzU : Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ U).Nonempty} ((fun (x : α) ↦ ({x} : Set α)) z)
hzV : Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ V).Nonempty} ((fun (x : α) ↦ ({x} : Set α)) z)
hzU₁ : z ∈ U
⊢ False
have hzV₁ : z ∈ V
Tactic: rw [Set.mem_setOf, Set.singleton_inter_nonempty] at hzU hzV
Cleared hypotheses: hzU, hzV
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.vietoris α] fun (x : Set α × Set α) ↦ x.1 ∪ x.2
have simp_rw : (∀ (U : Set α),
    IsOpen[inst] U → IsOpen[instTopologicalSpaceProd] ({a : Set α × Set α | a.1 ⊆ U} ∩ {a : Set α × Set α | a.2 ⊆ U})) ∧
  ∀ (F : Set α),
    IsClosed[inst] F →
      IsClosed[instTopologicalSpaceProd] ({a : Set α × Set α | a.1 ⊆ F} ∩ {a : Set α × Set α | a.2 ⊆ F})
Tactic: simp_rw [continuous_iff, powerset, preimage_setOf_eq, union_subset_iff, setOf_and]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
inst_1 : Finite ι
⊢ Continuous[Pi.topologicalSpace, TopologicalSpace.vietoris α] range
have simp_rw : (∀ (U : Set α), IsOpen[inst] U → IsOpen[Pi.topologicalSpace] (⋂ (i : ι), {x : ι → α | x i ∈ U})) ∧
  ∀ (F : Set α), IsClosed[inst] F → IsClosed[Pi.topologicalSpace] (⋂ (i : ι), {x : ι → α | x i ∈ F})
Tactic: simp_rw [continuous_iff, powerset, preimage_setOf_eq, range_subset_iff, setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous[inst, inst_1] f
⊢ Continuous[TopologicalSpace.vietoris α, TopologicalSpace.vietoris β] fun (x : Set α) ↦ f '' x
have simp_rw : (∀ (U : Set β), IsOpen[inst_1] U → IsOpen[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' U}) ∧
  ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' F}
Tactic: simp_rw [continuous_iff, powerset, preimage_setOf_eq, image_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous[inst, inst_1] f
⊢ (∀ (U : Set β), IsOpen[inst_1] U → IsOpen[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' U}) ∧
    ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' F}
have left : ∀ (U : Set β), IsOpen[inst_1] U → IsOpen[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' U}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous[inst, inst_1] f
left : ∀ (U : Set β), IsOpen[inst_1] U → IsOpen[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' U}
⊢ (∀ (U : Set β), IsOpen[inst_1] U → IsOpen[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' U}) ∧
    ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' F}
have right : ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' F}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsInducing f
⊢ IsInducing.{u_1, u_2} (Y := Set β) fun (x : Set α) ↦ f '' x
have eq_induced : TopologicalSpace.vietoris α = induced (fun (x : Set α) ↦ f '' x) (TopologicalSpace.vietoris β)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsInducing f
⊢ TopologicalSpace.vietoris α = induced (fun (x : Set α) ↦ f '' x) (TopologicalSpace.vietoris β)
have this : Eq.{u_1 + 1} (α := Set (Set α)) {U : Set α | IsOpen[inst] U}
  ((fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V})
Tactic: have : {U : Set α | IsOpen U} = (f ⁻¹' ·) '' {V : Set β | IsOpen V} :=
    Set.ext fun _ => hf.isOpen_iff
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsInducing f
this :
  Eq.{u_1 + 1} (α := Set (Set α)) {U : Set α | IsOpen[inst] U}
    ((fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V})
⊢ TopologicalSpace.vietoris α = induced (fun (x : Set α) ↦ f '' x) (TopologicalSpace.vietoris β)
have eq_induced : Eq.{u_1 + 1} (α := TopologicalSpace (Set α))
  (generateFrom
    (powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
  (induced.{u_1, u_2} (Y := Set β) (fun (x : Set α) ↦ f '' x)
    (generateFrom
      (powerset '' {U : Set β | IsOpen[inst_1] U} ∪
        (fun (V : Set β) ↦ {s : Set β | (s ∩ V).Nonempty}) '' {U : Set β | IsOpen[inst_1] U})))
Tactic: simp_rw [TopologicalSpace.vietoris, this, induced_generateFrom_eq, image_union, image_image,
    powerset, preimage_setOf_eq, image_subset_iff, image_inter_nonempty_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsInducing f
this :
  Eq.{u_1 + 1} (α := Set (Set α)) {U : Set α | IsOpen[inst] U}
    ((fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V})
eq_induced :
  Eq.{u_1 + 1} (α := TopologicalSpace (Set α))
    (generateFrom
      (powerset '' {U : Set α | IsOpen[inst] U} ∪
        (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
    (induced.{u_1, u_2} (Y := Set β) (fun (x : Set α) ↦ f '' x)
      (generateFrom
        (powerset '' {U : Set β | IsOpen[inst_1] U} ∪
          (fun (V : Set β) ↦ {s : Set β | (s ∩ V).Nonempty}) '' {U : Set β | IsOpen[inst_1] U})))
⊢ TopologicalSpace.vietoris α = induced (fun (x : Set α) ↦ f '' x) (TopologicalSpace.vietoris β)
have eq_induced₁ : Eq.{u_1 + 1} (α := TopologicalSpace (Set α))
  (generateFrom
    (powerset '' (fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) ''
        (fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V}))
  (induced.{u_1, u_2} (Y := Set β) (fun (x : Set α) ↦ f '' x)
    (generateFrom
      (powerset '' {V : Set β | IsOpen[inst_1] V} ∪
        (fun (V : Set β) ↦ {s : Set β | (s ∩ V).Nonempty}) '' {V : Set β | IsOpen[inst_1] V})))
Tactic: simp_rw [TopologicalSpace.vietoris, this, induced_generateFrom_eq, image_union, image_image,
    powerset, preimage_setOf_eq, image_subset_iff, image_inter_nonempty_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsInducing f
this :
  Eq.{u_1 + 1} (α := Set (Set α)) {U : Set α | IsOpen[inst] U}
    ((fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V})
eq_induced :
  Eq.{u_1 + 1} (α := TopologicalSpace (Set α))
    (generateFrom
      (powerset '' {U : Set α | IsOpen[inst] U} ∪
        (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
    (induced.{u_1, u_2} (Y := Set β) (fun (x : Set α) ↦ f '' x)
      (generateFrom
        (powerset '' {U : Set β | IsOpen[inst_1] U} ∪
          (fun (V : Set β) ↦ {s : Set β | (s ∩ V).Nonempty}) '' {U : Set β | IsOpen[inst_1] U})))
eq_induced₁ :
  Eq.{u_1 + 1} (α := TopologicalSpace (Set α))
    (generateFrom
      (powerset '' (fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V} ∪
        (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) ''
          (fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V}))
    (induced.{u_1, u_2} (Y := Set β) (fun (x : Set α) ↦ f '' x)
      (generateFrom
        (powerset '' {V : Set β | IsOpen[inst_1] V} ∪
          (fun (V : Set β) ↦ {s : Set β | (s ∩ V).Nonempty}) '' {V : Set β | IsOpen[inst_1] V})))
⊢ TopologicalSpace.vietoris α = induced (fun (x : Set α) ↦ f '' x) (TopologicalSpace.vietoris β)
have eq_induced₂ : Eq.{u_1 + 1} (α := TopologicalSpace (Set α))
  (generateFrom
    (powerset '' (fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) ''
        (fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V}))
  (generateFrom
    (image.{u_2, u_1} (α := Set (Set β)) (preimage fun (x : Set α) ↦ f '' x)
      (powerset '' {V : Set β | IsOpen[inst_1] V} ∪
        (fun (V : Set β) ↦ {s : Set β | (s ∩ V).Nonempty}) '' {V : Set β | IsOpen[inst_1] V})))
Tactic: simp_rw [TopologicalSpace.vietoris, this, induced_generateFrom_eq, image_union, image_image,
    powerset, preimage_setOf_eq, image_subset_iff, image_inter_nonempty_iff]