awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace γ
inst_2 : Preorder β
f g : α → β
x : α
s t : Set α
y z : β
simp_rw :
  (∀ (x : α), SemicontinuousAt (fun (x1 : α) (x2 : β) ↦ ¬f x1 ≤ x2) x) ↔
    ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y
simp_rw₁ :
  (∀ (x : α) (y : β), ¬f x ≤ y → ∀ᶠ (x' : α) in 𝓝 x, ¬f x' ≤ y) ↔
    ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y
⊢ (Semicontinuous fun (x1 : α) (x2 : β) ↦ ¬f x1 ≤ x2) ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y
have simp_rw₂ : (∀ (x : α) (y : β), ¬f x ≤ y → ¬∃ᶠ (x : α) in 𝓝 x, f x ≤ y) ↔
  ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y
Tactic: simp_rw [Semicontinuous, SemicontinuousAt, ← not_frequently, not_imp_not]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder β
f g : α → β
s : Set α
a : α
h : LowerSemicontinuousWithinAt f s a
has : a ∈ s
hfg : f =ᶠ[𝓝[s] a] g
⊢ ∀ᶠ (x : α) in 𝓝[s] a, ∀ (y : β), f x > y ↔ g x > y
have h₁ : ∀ (x : α) (hx : f x = g x) (y : β), f x > y ↔ g x > y
Tactic: filter_upwards [hfg] with x hx
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
s : Set α
a : α
h : LowerHemicontinuousWithinAt f s a
has : a ∈ s
hfg : f =ᶠ[𝓝[s] a] g
⊢ ∀ᶠ (x : α) in 𝓝[s] a, ∀ (y : Set β), IsOpen[inst_1] y ∧ (f x ∩ y).Nonempty ↔ IsOpen[inst_1] y ∧ (g x ∩ y).Nonempty
have h₁ : ∀ (x : α) (hx : f x = g x) (y : Set β), IsOpen[inst_1] y ∧ (f x ∩ y).Nonempty ↔ IsOpen[inst_1] y ∧ (g x ∩ y).Nonempty
Tactic: filter_upwards [hfg] with x hx
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ LowerHemicontinuousWithinAt f s x ↔ ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t
have rw : (∀ (x_1 : Set β), IsOpen[inst_1] x_1ᶜ → (f x ∩ x_1ᶜ).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ x_1ᶜ).Nonempty) ↔
  ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t
Tactic: rw [lowerHemicontinuousWithinAt_iff, compl_surjective.forall]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ (∀ (x_1 : Set β), IsOpen[inst_1] x_1ᶜ → (f x ∩ x_1ᶜ).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ x_1ᶜ).Nonempty) ↔
    ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t
have simp : (∀ (x_1 : Set β), IsClosed[inst_1] x_1 → (f x ∩ x_1ᶜ).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ x_1ᶜ).Nonempty) ↔
  ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t
Tactic: simp only [isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ (∀ (x_1 : Set β), IsClosed[inst_1] x_1 → (f x ∩ x_1ᶜ).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ x_1ᶜ).Nonempty) ↔
    ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t
have refine : ∀ (t : Set β) (ht : IsClosed[inst_1] t),
  ((f x ∩ tᶜ).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ tᶜ).Nonempty) ↔ (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t
Tactic: refine forall₂_congr fun t ht ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
s : Set α
t : Set β
ht : IsClosed[inst_1] t
⊢ ((f x ∩ tᶜ).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ tᶜ).Nonempty) ↔ (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t
have rw : (¬∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ tᶜ).Nonempty) → ¬(f x ∩ tᶜ).Nonempty ↔ (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t
Tactic: rw [← not_imp_not]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
⊢ LowerHemicontinuousAt f x ↔ ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t
have rw : (∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[univ] x, f x' ⊆ t) → f x ⊆ t) ↔
  ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t
Tactic: rw [← lowerHemicontinuousWithinAt_univ_iff, lowerHemicontinuousWithinAt_iff_frequently]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
s : Set α
a : α
h : UpperHemicontinuousWithinAt f s a
has : a ∈ s
hfg : ∀ᶠ (x : α) in 𝓝[s] a, f x = g x
⊢ ∀ᶠ (x : α) in 𝓝[s] a, ∀ (y : Set β), y ∈ 𝓝ˢ (f x) ↔ y ∈ 𝓝ˢ (g x)
have h₁ : ∀ (x : α) (hx : f x = g x) (y : Set β), y ∈ 𝓝ˢ (f x) ↔ y ∈ 𝓝ˢ (g x)
Tactic: filter_upwards [hfg] with x hx
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ UpperHemicontinuousWithinAt f s x ↔
    ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
have rw : (∀ (x_1 : Set β), (∃ᶠ (x' : α) in 𝓝[s] x, x_1ᶜ ∉ 𝓝ˢ (f x')) → x_1ᶜ ∉ 𝓝ˢ (f x)) ↔
  ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
Tactic: rw [UpperHemicontinuousWithinAt, semicontinuousWithinAt_iff_frequently, compl_surjective.forall]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
⊢ UpperHemicontinuousAt f x ↔
    ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝 x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
have rw : (∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝[univ] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty) ↔
  ∀ (t : Set β), IsClosed[inst_1] t → (∃ᶠ (x' : α) in 𝓝 x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
Tactic: rw [← upperHemicontinuousWithinAt_univ_iff, upperHemicontinuousWithinAt_iff_frequently]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
⊢ UpperHemicontinuousWithinAt f s x ↔ ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
have rw : (∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
  ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
Tactic: rw [upperHemicontinuousWithinAt_iff, hasBasis_nhdsSet _ |>.forall_iff ?mono]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
rw :
  (∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
⊢ UpperHemicontinuousWithinAt f s x ↔ ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
have rw₁ : ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → (∀ᶠ (x' : α) in 𝓝[s] x, s_1 ∈ 𝓝ˢ (f x')) → ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')
Tactic: rw [upperHemicontinuousWithinAt_iff, hasBasis_nhdsSet _ |>.forall_iff ?mono]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
⊢ (∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
have simp : (∀ (i : Set β), IsOpen[inst_1] i → f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
  ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
Tactic: simp only [and_imp]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
⊢ (∀ (i : Set β), IsOpen[inst_1] i → f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
have h : ∀ (a : Set β) (b : IsOpen[inst_1] a),
  (f x ⊆ a → ∀ᶠ (x' : α) in 𝓝[s] x, a ∈ 𝓝ˢ (f x')) ↔ f x ⊆ a → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ a
Tactic: apply forall₂_congr
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
⊢ (∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')) ↔ ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝[s] x
have rw : (∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
  ∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝[s] x
Tactic: rw [hasBasis_nhdsSet (f x) |>.forall_iff ?h₁, hasBasis_nhdsSet (f x) |>.forall_iff ?h₂]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
rw :
  (∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝[s] x
⊢ (∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')) ↔ ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝[s] x
have rw₁ : ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → f ⁻¹' Iic s_1 ∈ 𝓝[s] x → f ⁻¹' Iic t ∈ 𝓝[s] x
Tactic: rw [hasBasis_nhdsSet (f x) |>.forall_iff ?h₁, hasBasis_nhdsSet (f x) |>.forall_iff ?h₂]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
rw :
  (∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝[s] x
rw₁ : ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → f ⁻¹' Iic s_1 ∈ 𝓝[s] x → f ⁻¹' Iic t ∈ 𝓝[s] x
⊢ (∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')) ↔ ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝[s] x
have rw₂ : ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → (∀ᶠ (x' : α) in 𝓝[s] x, s_1 ∈ 𝓝ˢ (f x')) → ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')
Tactic: rw [hasBasis_nhdsSet (f x) |>.forall_iff ?h₁, hasBasis_nhdsSet (f x) |>.forall_iff ?h₂]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s_1 : Set α
x : α
s t : Set β
hst : s ⊆ t
⊢ f ⁻¹' Iic s ∈ 𝓝[s_1] x → f ⁻¹' Iic t ∈ 𝓝[s_1] x
have hxy : s ≤ t
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
⊢ (∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → ∀ᶠ (x' : α) in 𝓝[s] x, i ∈ 𝓝ˢ (f x')) ↔
    ∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝[s] x
have refine : ∀ (u : Set β),
  IsOpen[inst_1] u ∧ f x ⊆ u →
    ∀ (hu : IsOpen[inst_1] u) (hfu : f x ⊆ u), (∀ᶠ (x' : α) in 𝓝[s] x, u ∈ 𝓝ˢ (f x')) ↔ f ⁻¹' Iic u ∈ 𝓝[s] x
Tactic: refine forall₂_congr fun u ⟨hu, hfu⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ UpperHemicontinuous f ↔ ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic u)
have simp_rw : (∀ (x : α), ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 x) ↔ ∀ (u : Set β), IsOpen[inst_1] u → ∀ x ∈ f ⁻¹' Iic u, f ⁻¹' Iic u ∈ 𝓝 x
Tactic: simp_rw [upperHemicontinuous_iff_preimage_Iic, isOpen_iff_mem_nhds (s := f ⁻¹' (Iic _))]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
| (∀ (x : α), ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 x) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → ∀ x ∈ f ⁻¹' Iic u, f ⁻¹' Iic u ∈ 𝓝 x
have enter : ∀ (x : α), ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 x
Tactic: enter [1, x]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
s t : Set β
hst : s ⊆ t
⊢ f ⁻¹' Iic s ∈ 𝓝 x → f ⁻¹' Iic t ∈ 𝓝 x
have hxy : s ≤ t
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
| ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 x
have rw : ∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝 x
Tactic: rw [hasBasis_nhdsSet (f x) |>.forall_iff <|
      fun s t hst ↦ by gcongr; exact hst]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
| (∀ (x : α), ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 x) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → ∀ x ∈ f ⁻¹' Iic u, f ⁻¹' Iic u ∈ 𝓝 x
have enter : ∀ (x : α) (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝 x
Tactic: enter [1, x]
    rw [hasBasis_nhdsSet (f x) |>.forall_iff <|
      fun s t hst ↦ by gcongr; exact hst]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ (∀ (x : α), ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 x) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → ∀ x ∈ f ⁻¹' Iic u, f ⁻¹' Iic u ∈ 𝓝 x
have conv : (∀ (x : α) (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝 x) ↔
  ∀ (u : Set β), IsOpen[inst_1] u → ∀ x ∈ f ⁻¹' Iic u, f ⁻¹' Iic u ∈ 𝓝 x
Tactic: conv =>
    enter [1, x]
    rw [hasBasis_nhdsSet (f x) |>.forall_iff <|
      fun s t hst ↦ by gcongr; exact hst]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
| ∀ (u : Set β), IsClosed[inst_1] u → IsClosed[inst] (f ⁻¹' Iic uᶜ)ᶜ
have rw : ∀ (x : Set β), IsClosed[inst_1] xᶜ → IsClosed[inst] (f ⁻¹' Iic xᶜᶜ)ᶜ
Tactic: rw [compl_surjective.forall]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
| ∀ (x : Set β), IsClosed[inst_1] xᶜ → IsClosed[inst] (f ⁻¹' Iic xᶜᶜ)ᶜ
have simp : ∀ (x : Set β), IsOpen[inst_1] x → IsOpen[inst] (f ⁻¹' Iic x)
Tactic: simp [← isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
| ∀ (u : Set β), IsClosed[inst_1] u → IsClosed[inst] (f ⁻¹' Iic uᶜ)ᶜ
have rw : ∀ (x : Set β), IsOpen[inst_1] x → IsOpen[inst] (f ⁻¹' Iic x)
Tactic: rw [compl_surjective.forall]
    simp [← isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ UpperHemicontinuous f ↔ ∀ (u : Set β), IsClosed[inst_1] u → IsClosed[inst] (f ⁻¹' Iic uᶜ)ᶜ
have conv_rhs : UpperHemicontinuous f ↔ ∀ (x : Set β), IsOpen[inst_1] x → IsOpen[inst] (f ⁻¹' Iic x)
Tactic: conv_rhs =>
    rw [compl_surjective.forall]
    simp [← isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
⊢ IsClosedMap f ↔ UpperHemicontinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f ⁻¹' {x}
have rw : (∀ {u : Set α}, IsOpen[inst] u → IsOpen[inst_1] (kernImage f u)) ↔
  ∀ (u : Set α), IsOpen[inst] u → IsOpen[inst_1] ((fun (x : β) ↦ f ⁻¹' {x}) ⁻¹' Iic u)
Tactic: rw [isClosedMap_iff_kernImage, upperHemicontinuous_iff_isOpen_preimage_Iic]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ LowerHemicontinuous f ↔ ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
have this : ∀ (u : Set β), (f ⁻¹' Iic uᶜ)ᶜ = {x : α | (f x ∩ u).Nonempty}
Tactic: have (u : Set β) : (f ⁻¹' (Iic uᶜ))ᶜ = {x | (f x ∩ u).Nonempty} := by
    simp [Set.ext_iff, Iic, Set.mem_compl_iff, Set.not_subset, Set.Nonempty]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
this : ∀ (u : Set β), (f ⁻¹' Iic uᶜ)ᶜ = {x : α | (f x ∩ u).Nonempty}
⊢ LowerHemicontinuous f ↔ ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
have simp_rw : (∀ (x : α), LowerHemicontinuousAt f x) ↔ ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
Tactic: simp_rw [lowerHemicontinuous_iff, lowerHemicontinuousAt_iff, this, isOpen_iff_mem_nhds,
    forall_comm (α := α), mem_setOf, Filter.Eventually]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
this : ∀ (u : Set β), (f ⁻¹' Iic uᶜ)ᶜ = {x : α | (f x ∩ u).Nonempty}
simp_rw : (∀ (x : α), LowerHemicontinuousAt f x) ↔ ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
⊢ LowerHemicontinuous f ↔ ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
have simp_rw₁ : (∀ (x : α) (u : Set β), IsOpen[inst_1] u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x, (f x' ∩ u).Nonempty) ↔
  ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
Tactic: simp_rw [lowerHemicontinuous_iff, lowerHemicontinuousAt_iff, this, isOpen_iff_mem_nhds,
    forall_comm (α := α), mem_setOf, Filter.Eventually]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
this : ∀ (u : Set β), (f ⁻¹' Iic uᶜ)ᶜ = {x : α | (f x ∩ u).Nonempty}
simp_rw : (∀ (x : α), LowerHemicontinuousAt f x) ↔ ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
simp_rw₁ :
  (∀ (x : α) (u : Set β), IsOpen[inst_1] u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x, (f x' ∩ u).Nonempty) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
⊢ LowerHemicontinuous f ↔ ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
have simp_rw₂ : (∀ (x : α) (u : Set β), IsOpen[inst_1] u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x, (f x' ∩ u).Nonempty) ↔
  ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] {x : α | (f x ∩ u).Nonempty}
Tactic: simp_rw [lowerHemicontinuous_iff, lowerHemicontinuousAt_iff, this, isOpen_iff_mem_nhds,
    forall_comm (α := α), mem_setOf, Filter.Eventually]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
this : ∀ (u : Set β), (f ⁻¹' Iic uᶜ)ᶜ = {x : α | (f x ∩ u).Nonempty}
simp_rw : (∀ (x : α), LowerHemicontinuousAt f x) ↔ ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
simp_rw₁ :
  (∀ (x : α) (u : Set β), IsOpen[inst_1] u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x, (f x' ∩ u).Nonempty) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
simp_rw₂ :
  (∀ (x : α) (u : Set β), IsOpen[inst_1] u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x, (f x' ∩ u).Nonempty) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] {x : α | (f x ∩ u).Nonempty}
⊢ LowerHemicontinuous f ↔ ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
have simp_rw₃ : (∀ (x : α) (u : Set β), (∀ x ∈ u, u ∈ 𝓝 x) → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x, (f x' ∩ u).Nonempty) ↔
  ∀ (u : Set β),
    (∀ x ∈ u, u ∈ 𝓝 x) →
      ∀ (x : α), Membership.mem (γ := Set α) {x : α | (f x ∩ u).Nonempty} x → {x : α | (f x ∩ u).Nonempty} ∈ 𝓝 x
Tactic: simp_rw [lowerHemicontinuous_iff, lowerHemicontinuousAt_iff, this, isOpen_iff_mem_nhds,
    forall_comm (α := α), mem_setOf, Filter.Eventually]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
this : ∀ (u : Set β), (f ⁻¹' Iic uᶜ)ᶜ = {x : α | (f x ∩ u).Nonempty}
simp_rw : (∀ (x : α), LowerHemicontinuousAt f x) ↔ ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
simp_rw₁ :
  (∀ (x : α) (u : Set β), IsOpen[inst_1] u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x, (f x' ∩ u).Nonempty) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
simp_rw₂ :
  (∀ (x : α) (u : Set β), IsOpen[inst_1] u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x, (f x' ∩ u).Nonempty) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] {x : α | (f x ∩ u).Nonempty}
simp_rw₃ :
  (∀ (x : α) (u : Set β), (∀ x ∈ u, u ∈ 𝓝 x) → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x, (f x' ∩ u).Nonempty) ↔
    ∀ (u : Set β),
      (∀ x ∈ u, u ∈ 𝓝 x) →
        ∀ (x : α), Membership.mem (γ := Set α) {x : α | (f x ∩ u).Nonempty} x → {x : α | (f x ∩ u).Nonempty} ∈ 𝓝 x
⊢ LowerHemicontinuous f ↔ ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
have simp_rw₄ : (∀ (b : Set β) (b_1 : ∀ x ∈ b, b ∈ 𝓝 x) (a : α), (f a ∩ b).Nonempty → ∀ᶠ (x' : α) in 𝓝 a, (f x' ∩ b).Nonempty) ↔
  ∀ (u : Set β),
    (∀ x ∈ u, u ∈ 𝓝 x) →
      ∀ (x : α), Membership.mem (γ := Set α) {x : α | (f x ∩ u).Nonempty} x → {x : α | (f x ∩ u).Nonempty} ∈ 𝓝 x
Tactic: simp_rw [lowerHemicontinuous_iff, lowerHemicontinuousAt_iff, this, isOpen_iff_mem_nhds,
    forall_comm (α := α), mem_setOf, Filter.Eventually]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
this : ∀ (u : Set β), (f ⁻¹' Iic uᶜ)ᶜ = {x : α | (f x ∩ u).Nonempty}
simp_rw : (∀ (x : α), LowerHemicontinuousAt f x) ↔ ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
simp_rw₁ :
  (∀ (x : α) (u : Set β), IsOpen[inst_1] u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x, (f x' ∩ u).Nonempty) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
simp_rw₂ :
  (∀ (x : α) (u : Set β), IsOpen[inst_1] u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x, (f x' ∩ u).Nonempty) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] {x : α | (f x ∩ u).Nonempty}
simp_rw₃ :
  (∀ (x : α) (u : Set β), (∀ x ∈ u, u ∈ 𝓝 x) → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x, (f x' ∩ u).Nonempty) ↔
    ∀ (u : Set β),
      (∀ x ∈ u, u ∈ 𝓝 x) →
        ∀ (x : α), Membership.mem (γ := Set α) {x : α | (f x ∩ u).Nonempty} x → {x : α | (f x ∩ u).Nonempty} ∈ 𝓝 x
simp_rw₄ :
  (∀ (b : Set β) (b_1 : ∀ x ∈ b, b ∈ 𝓝 x) (a : α), (f a ∩ b).Nonempty → ∀ᶠ (x' : α) in 𝓝 a, (f x' ∩ b).Nonempty) ↔
    ∀ (u : Set β),
      (∀ x ∈ u, u ∈ 𝓝 x) →
        ∀ (x : α), Membership.mem (γ := Set α) {x : α | (f x ∩ u).Nonempty} x → {x : α | (f x ∩ u).Nonempty} ∈ 𝓝 x
⊢ LowerHemicontinuous f ↔ ∀ (u : Set β), IsOpen[inst_1] u → IsOpen[inst] (f ⁻¹' Iic uᶜ)ᶜ
have simp_rw₅ : (∀ (b : Set β) (b_1 : ∀ x ∈ b, b ∈ 𝓝 x) (a : α), (f a ∩ b).Nonempty → ∀ᶠ (x' : α) in 𝓝 a, (f x' ∩ b).Nonempty) ↔
  ∀ (u : Set β), (∀ x ∈ u, u ∈ 𝓝 x) → ∀ (x : α), (f x ∩ u).Nonempty → {x : α | (f x ∩ u).Nonempty} ∈ 𝓝 x
Tactic: simp_rw [lowerHemicontinuous_iff, lowerHemicontinuousAt_iff, this, isOpen_iff_mem_nhds,
    forall_comm (α := α), mem_setOf, Filter.Eventually]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Hemicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
| ∀ (u : Set β), IsClosed[inst_1] u → IsClosed[inst] (f ⁻¹' Iic u)
have rw : ∀ (x : Set β), IsClosed[inst_1] xᶜ → IsClosed[inst] (f ⁻¹' Iic xᶜ)
Tactic: rw [compl_surjective.forall]