awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
x : α
rw : ∀ (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝 x
| ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 x

Tactic:
rw [hasBasis_nhdsSet (f x) |>.forall_iff <|
      fun s t hst ↦ by gcongr; exact hst]

Premises used: hasBasis_nhdsSet, Filter.HasBasis.forall_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
enter : ∀ (x : α) (i : Set β), IsOpen[inst_1] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝 x
| (∀ (x : α), ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 x) ↔
    ∀ (u : Set β), IsOpen[inst_1] u → ∀ x ∈ f ⁻¹' Iic u, f ⁻¹' Iic u ∈ 𝓝 x

Tactic:
enter [1, x]
    rw [hasBasis_nhdsSet (f x) |>.forall_iff <|
      fun s t hst ↦ by gcongr; exact hst]
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
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
⊢ (∀ (x : α), ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 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]
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ (∀ (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:
simp [forall_comm (α := α)]

Premises used: forall_comm
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
rw : ∀ (x : Set β), IsClosed[inst_1] xᶜ → IsClosed[inst] (f ⁻¹' Iic xᶜᶜ)ᶜ
| ∀ (u : Set β), IsClosed[inst_1] u → IsClosed[inst] (f ⁻¹' Iic uᶜ)ᶜ

Tactic:
rw [compl_surjective.forall]

Premises used: Function.Surjective.forall, compl_surjective
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
simp : ∀ (x : Set β), IsOpen[inst_1] x → IsOpen[inst] (f ⁻¹' Iic x)
| ∀ (x : Set β), IsClosed[inst_1] xᶜ → IsClosed[inst] (f ⁻¹' Iic xᶜᶜ)ᶜ

Tactic:
simp [← isOpen_compl_iff]

Premises used: isOpen_compl_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
rw : ∀ (x : Set β), IsOpen[inst_1] x → IsOpen[inst] (f ⁻¹' Iic x)
| ∀ (u : Set β), IsClosed[inst_1] u → IsClosed[inst] (f ⁻¹' Iic uᶜ)ᶜ

Tactic:
rw [compl_surjective.forall]
    simp [← isOpen_compl_iff]

Premises used: Function.Surjective.forall, compl_surjective, isOpen_compl_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
conv_rhs : UpperHemicontinuous f ↔ ∀ (x : Set β), IsOpen[inst_1] x → IsOpen[inst] (f ⁻¹' Iic x)
⊢ UpperHemicontinuous f ↔ ∀ (u : Set β), IsClosed[inst_1] u → IsClosed[inst] (f ⁻¹' Iic uᶜ)ᶜ

Tactic:
conv_rhs =>
    rw [compl_surjective.forall]
    simp [← isOpen_compl_iff]

Premises used: Function.Surjective.forall, compl_surjective, isOpen_compl_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ UpperHemicontinuous f ↔ ∀ (x : Set β), IsOpen[inst_1] x → IsOpen[inst] (f ⁻¹' Iic x)

Tactic:
upperHemicontinuous_iff_isOpen_preimage_Iic

Premises used: upperHemicontinuous_iff_isOpen_preimage_Iic
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ UpperHemicontinuous f ↔ ∀ (x : Set β), IsOpen[inst_1] x → IsOpen[inst] (f ⁻¹' Iic x)

Tactic:
exact upperHemicontinuous_iff_isOpen_preimage_Iic

Premises used: upperHemicontinuous_iff_isOpen_preimage_Iic
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
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)
⊢ IsClosedMap f ↔ UpperHemicontinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f ⁻¹' {x}

Tactic:
rw [isClosedMap_iff_kernImage, upperHemicontinuous_iff_isOpen_preimage_Iic]

Premises used: isClosedMap_iff_kernImage, upperHemicontinuous_iff_isOpen_preimage_Iic
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
⊢ (∀ {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:
aesop
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
u : Set β
⊢ (f ⁻¹' Iic uᶜ)ᶜ = {x : α | (f x ∩ u).Nonempty}

Tactic:
simp [Set.ext_iff, Iic, Set.mem_compl_iff, Set.not_subset, Set.Nonempty]

Premises used: Set.Nonempty, Set.not_subset, Set.Iic, Set.ext_iff, Set.mem_compl_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ ∀ (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]
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
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
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
⊢ LowerHemicontinuous f ↔ ∀ (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]

Premises used: lowerHemicontinuous_iff, Filter.Eventually, forall_comm, Set.mem_setOf, lowerHemicontinuousAt_iff, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
rw : ∀ (x : Set β), IsClosed[inst_1] xᶜ → IsClosed[inst] (f ⁻¹' Iic xᶜ)
| ∀ (u : Set β), IsClosed[inst_1] u → IsClosed[inst] (f ⁻¹' Iic u)

Tactic:
rw [compl_surjective.forall]

Premises used: Function.Surjective.forall, compl_surjective
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
simp : ∀ (x : Set β), IsOpen[inst_1] x → IsOpen[inst] (f ⁻¹' Iic xᶜ)ᶜ
| ∀ (x : Set β), IsClosed[inst_1] xᶜ → IsClosed[inst] (f ⁻¹' Iic xᶜ)

Tactic:
simp [← isOpen_compl_iff]

Premises used: isOpen_compl_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
rw : ∀ (x : Set β), IsOpen[inst_1] x → IsOpen[inst] (f ⁻¹' Iic xᶜ)ᶜ
| ∀ (u : Set β), IsClosed[inst_1] u → IsClosed[inst] (f ⁻¹' Iic u)

Tactic:
rw [compl_surjective.forall]
    simp [← isOpen_compl_iff]

Premises used: Function.Surjective.forall, compl_surjective, isOpen_compl_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
conv_rhs : LowerHemicontinuous f ↔ ∀ (x : Set β), IsOpen[inst_1] x → IsOpen[inst] (f ⁻¹' Iic xᶜ)ᶜ
⊢ LowerHemicontinuous f ↔ ∀ (u : Set β), IsClosed[inst_1] u → IsClosed[inst] (f ⁻¹' Iic u)

Tactic:
conv_rhs =>
    rw [compl_surjective.forall]
    simp [← isOpen_compl_iff]

Premises used: Function.Surjective.forall, compl_surjective, isOpen_compl_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ LowerHemicontinuous f ↔ ∀ (x : Set β), IsOpen[inst_1] x → IsOpen[inst] (f ⁻¹' Iic xᶜ)ᶜ

Tactic:
lowerHemicontinuous_iff_isOpen_compl_preimage_Iic_compl

Premises used: Set.Mem, setOf, lowerHemicontinuous_iff_isOpen_compl_preimage_Iic_compl
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ LowerHemicontinuous f ↔ ∀ (x : Set β), IsOpen[inst_1] x → IsOpen[inst] (f ⁻¹' Iic xᶜ)ᶜ

Tactic:
exact lowerHemicontinuous_iff_isOpen_compl_preimage_Iic_compl

Premises used: lowerHemicontinuous_iff_isOpen_compl_preimage_Iic_compl
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
rw :
  (∀ {u : Set α}, IsClosed[inst] u → IsClosed[inst_1] (kernImage f u)) ↔
    ∀ (u : Set α), IsClosed[inst] u → IsClosed[inst_1] ((fun (x : β) ↦ f ⁻¹' {x}) ⁻¹' Iic u)
⊢ IsOpenMap f ↔ LowerHemicontinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f ⁻¹' {x}

Tactic:
rw [isOpenMap_iff_kernImage, lowerHemicontinuous_iff_isClosed_preimage_Iic]

Premises used: lowerHemicontinuous_iff_isClosed_preimage_Iic, isOpenMap_iff_kernImage
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
⊢ (∀ {u : Set α}, IsClosed[inst] u → IsClosed[inst_1] (kernImage f u)) ↔
    ∀ (u : Set α), IsClosed[inst] u → IsClosed[inst_1] ((fun (x : β) ↦ f ⁻¹' {x}) ⁻¹' Iic u)

Tactic:
aesop
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ UpperHemicontinuous (β := α) fun (x : α) ↦ {x}

Tactic:
simp [upperHemicontinuous_iff, upperHemicontinuousAt_iff]

Premises used: upperHemicontinuousAt_iff, upperHemicontinuous_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
⊢ UpperHemicontinuousWithinAt.{u_1, u_2} (β := β) (fun (x : α) ↦ {f x}) s x ↔ ContinuousWithinAt f s x

Tactic:
⟨?_, fun hf ↦ upperHemicontinuous_singleton_id.upperHemicontinuousWithinAt _ _ |>.comp hf
    (mapsTo_image _ _)⟩

Premises used: upperHemicontinuous_singleton_id, UpperHemicontinuous.upperHemicontinuousWithinAt, Set.mapsTo_image, UpperHemicontinuousWithinAt.comp, Iff.intro, Set.image
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
refine : UpperHemicontinuousWithinAt.{u_1, u_2} (β := β) (fun (x : α) ↦ {f x}) s x → ContinuousWithinAt f s x
⊢ UpperHemicontinuousWithinAt.{u_1, u_2} (β := β) (fun (x : α) ↦ {f x}) s x ↔ ContinuousWithinAt f s x

Tactic:
refine ⟨?_, fun hf ↦ upperHemicontinuous_singleton_id.upperHemicontinuousWithinAt _ _ |>.comp hf
    (mapsTo_image _ _)⟩
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
simp : (∀ t ∈ 𝓝 (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝 (f x')) → ∀ s_1 ∈ 𝓝 (f x), ∀ᶠ (x : α) in 𝓝[s] x, f x ∈ s_1
⊢ UpperHemicontinuousWithinAt.{u_1, u_2} (β := β) (fun (x : α) ↦ {f x}) s x → ContinuousWithinAt f s x

Tactic:
simp only [upperHemicontinuousWithinAt_iff, nhdsSet_singleton, ContinuousWithinAt,
    tendsto_iff_forall_eventually_mem]

Premises used: ContinuousWithinAt, upperHemicontinuousWithinAt_iff, Filter.tendsto_iff_forall_eventually_mem, nhdsSet_singleton
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ∀ t ∈ 𝓝 (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝 (f x')
t : Set β
ht : t ∈ 𝓝 (f x)
h₁ : ∀ (x : α), t ∈ 𝓝 (f x) → f x ∈ t
⊢ ∀ᶠ (x : α) in 𝓝[s] x, f x ∈ t

Tactic:
filter_upwards [h t ht] with x
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x_1 : α
h : ∀ t ∈ 𝓝 (f x_1), ∀ᶠ (x' : α) in 𝓝[s] x_1, t ∈ 𝓝 (f x')
t : Set β
ht : t ∈ 𝓝 (f x_1)
x : α
⊢ t ∈ 𝓝 (f x) → f x ∈ t

Tactic:
mem_of_mem_nhds

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x_1 : α
h : ∀ t ∈ 𝓝 (f x_1), ∀ᶠ (x' : α) in 𝓝[s] x_1, t ∈ 𝓝 (f x')
t : Set β
ht : t ∈ 𝓝 (f x_1)
x : α
⊢ t ∈ 𝓝 (f x) → f x ∈ t

Tactic:
exact mem_of_mem_nhds

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
⊢ UpperHemicontinuousAt.{u_1, u_2} (β := β) (fun (x : α) ↦ {f x}) x ↔ ContinuousAt f x

Tactic:
simp [← upperHemicontinuousWithinAt_univ_iff, continuousWithinAt_univ]

Premises used: continuousWithinAt_univ, upperHemicontinuousWithinAt_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
⊢ UpperHemicontinuousOn.{u_1, u_2} (β := β) (fun (x : α) ↦ {f x}) s ↔ ContinuousOn f s

Tactic:
forall₂_congr <| fun _ _ ↦ upperHemicontinuousWithinAt_singleton_iff

Premises used: forall₂_congr, ContinuousOn, upperHemicontinuousWithinAt_singleton_iff, SemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
⊢ (UpperHemicontinuous.{u_1, u_2} (β := β) fun (x : α) ↦ {f x}) ↔ Continuous[inst, inst_1] f

Tactic:
simp [← upperHemicontinuousOn_univ_iff]

Premises used: upperHemicontinuousOn_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
s : Set α
x : α
hf : UpperHemicontinuousWithinAt f s x
hg : UpperHemicontinuousWithinAt g s x
⊢ ∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')

Tactic:
rw [upperHemicontinuousWithinAt_iff] at hf hg ⊢

Premises used: upperHemicontinuousWithinAt_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
s : Set α
x : α
hf : UpperHemicontinuousWithinAt f s x
hg : UpperHemicontinuousWithinAt g s x
hf₁ : ∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')
⊢ ∀ t ∈ 𝓝ˢ (g x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (g x')

Tactic:
rw [upperHemicontinuousWithinAt_iff] at hf hg ⊢

Premises used: upperHemicontinuousWithinAt_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
s : Set α
x : α
hf : ∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')
hg : ∀ t ∈ 𝓝ˢ (g x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (g x')
⊢ ∀ t ∈ 𝓝ˢ (f x ∪ g x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x' ∪ g x')

Tactic:
aesop
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
s : Set α
hf : UpperHemicontinuousOn f s
hg : UpperHemicontinuousOn g s
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt f s x

Tactic:
rw [upperHemicontinuousOn_iff] at hf hg ⊢

Premises used: upperHemicontinuousOn_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
s : Set α
hf : UpperHemicontinuousOn f s
hg : UpperHemicontinuousOn g s
hf₁ : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt g s x

Tactic:
rw [upperHemicontinuousOn_iff] at hf hg ⊢

Premises used: upperHemicontinuousOn_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
s : Set α
hf : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
hg : ∀ x ∈ s, UpperHemicontinuousWithinAt g s x
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∪ g x) s x

Tactic:
fun x hx ↦ (hf x hx).union (hg x hx)

Premises used: UpperHemicontinuousWithinAt.union
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
s : Set α
hf : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
hg : ∀ x ∈ s, UpperHemicontinuousWithinAt g s x
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∪ g x) s x

Tactic:
exact fun x hx ↦ (hf x hx).union (hg x hx)

Premises used: UpperHemicontinuousWithinAt.union
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
x : α
hf : UpperHemicontinuousAt f x
hg : UpperHemicontinuousAt g x
rw :
  ∀ (hf : UpperHemicontinuousWithinAt f univ x) (hg : UpperHemicontinuousWithinAt g univ x),
    UpperHemicontinuousWithinAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∪ g x) univ x
⊢ UpperHemicontinuousAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∪ g x) x

Tactic:
rw [← upperHemicontinuousWithinAt_univ_iff] at hf hg ⊢

Premises used: upperHemicontinuousWithinAt_univ_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
x : α
hf : UpperHemicontinuousWithinAt f univ x
hg : UpperHemicontinuousWithinAt g univ x
⊢ UpperHemicontinuousWithinAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∪ g x) univ x

Tactic:
hf.union hg

Premises used: UpperHemicontinuousWithinAt.union
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
x : α
hf : UpperHemicontinuousWithinAt f univ x
hg : UpperHemicontinuousWithinAt g univ x
⊢ UpperHemicontinuousWithinAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∪ g x) univ x

Tactic:
exact hf.union hg

Premises used: UpperHemicontinuousWithinAt.union
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
hf : UpperHemicontinuous f
hg : UpperHemicontinuous g
⊢ ∀ (x : α), UpperHemicontinuousAt f x

Tactic:
rw [upperHemicontinuous_iff] at hf hg ⊢

Premises used: upperHemicontinuous_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
hf : UpperHemicontinuous f
hg : UpperHemicontinuous g
hf₁ : ∀ (x : α), UpperHemicontinuousAt f x
⊢ ∀ (x : α), UpperHemicontinuousAt g x

Tactic:
rw [upperHemicontinuous_iff] at hf hg ⊢

Premises used: upperHemicontinuous_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
hf : ∀ (x : α), UpperHemicontinuousAt f x
hg : ∀ (x : α), UpperHemicontinuousAt g x
⊢ ∀ (x : α), UpperHemicontinuousAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∪ g x) x

Tactic:
fun x ↦ (hf x).union (hg x)

Premises used: UpperHemicontinuousAt.union
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → Set β
hf : ∀ (x : α), UpperHemicontinuousAt f x
hg : ∀ (x : α), UpperHemicontinuousAt g x
⊢ ∀ (x : α), UpperHemicontinuousAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∪ g x) x

Tactic:
exact fun x ↦ (hf x).union (hg x)

Premises used: UpperHemicontinuousAt.union
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
hf : UpperHemicontinuousWithinAt f s x
u : Set β
hu : IsClosed[inst_1] u
rw :
  ∀ (hf : ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u) {u : Set β}
    (hu : IsClosed[inst_1] u) (u_1 : Set β), IsOpen[inst_1] u_1 → f x ∩ u ⊆ u_1 → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∩ u ⊆ u_1
⊢ UpperHemicontinuousWithinAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∩ u) s x

Tactic:
rw [upperHemicontinuousWithinAt_iff_forall_isOpen] at hf ⊢

Premises used: upperHemicontinuousWithinAt_iff_forall_isOpen
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
hf : ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
u : Set β
hu : IsClosed[inst_1] u
t : Set β
ht_open : IsOpen[inst_1] t
ht : f x ∩ u ⊆ t
⊢ f x ⊆ t ∪ uᶜ

Tactic:
grind
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
hf : ∀ (u : Set β), IsOpen[inst_1] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u
u : Set β
hu : IsClosed[inst_1] u
t : Set β
ht_open : IsOpen[inst_1] t
ht : f x ∩ u ⊆ t
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t ∪ uᶜ

Tactic:
specialize hf (t ∪ uᶜ) (ht_open.union hu.isOpen_compl) (by grind)

Premises used: IsClosed.isOpen_compl, Compl.compl, IsOpen.union, Union.union
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
x : α
u : Set β
hu : IsClosed[inst_1] u
t : Set β
ht_open : IsOpen[inst_1] t
ht : f x ∩ u ⊆ t
hf : ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t ∪ uᶜ
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∩ u ⊆ t

Tactic:
grind
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
hf : UpperHemicontinuousOn f s
u : Set β
hu : IsClosed[inst_1] u
rw :
  ∀ (hf : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x) {u : Set β} (hu : IsClosed[inst_1] u),
    ∀ x ∈ s, UpperHemicontinuousWithinAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∩ u) s x
⊢ UpperHemicontinuousOn.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∩ u) s

Tactic:
rw [upperHemicontinuousOn_iff] at hf ⊢

Premises used: upperHemicontinuousOn_iff
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
s : Set α
hf : ∀ x ∈ s, UpperHemicontinuousWithinAt f s x
u : Set β
hu : IsClosed[inst_1] u
⊢ ∀ x ∈ s, UpperHemicontinuousWithinAt.{u_3, u_4} (β := β) (fun (x : α) ↦ f x ∩ u) s x

Tactic:
(hf · · |>.inter hu)

Premises used: UpperHemicontinuousWithinAt.inter