awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
rw :
  (∃ (t_1 : Set α),
      IsOpen[inst] t_1 ∧
        Eq (α := Set (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1)
          (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' f ⁻¹' t)) ↔
    ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ IsOpen[instTopologicalSpaceSubtype] (s.restrict (π := fun (a : α) ↦ β) f ⁻¹' t) ↔
    ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
rw [isOpen_induced_iff, Set.restrict_eq, Set.preimage_comp]

Premises used: Set.preimage_comp, Set.restrict_eq, isOpen_induced_iff
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
simp : (∃ (t_1 : Set α), IsOpen[inst] t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t) ↔ ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ (∃ (t_1 : Set α),
      IsOpen[inst] t_1 ∧
        Eq (α := Set (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1)
          (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' f ⁻¹' t)) ↔
    ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
simp only [Subtype.preimage_coe_eq_preimage_coe_iff]

Premises used: Subtype.preimage_coe_eq_preimage_coe_iff
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
mp : (∃ (t_1 : Set α), IsOpen[inst] t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t) → ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
mpr : (∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s) → ∃ (t_1 : Set α), IsOpen[inst] t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t
⊢ (∃ (t_1 : Set α), IsOpen[inst] t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t) ↔ ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
constructor
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
u : Set α
ou : IsOpen[inst] u
useq : s ∩ u = s ∩ f ⁻¹' t
⊢ f ⁻¹' t ∩ s = u ∩ s

Tactic:
simpa only [Set.inter_comm, eq_comm] using useq

Premises used: eq_comm, Set.inter_comm
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
u : Set α
ou : IsOpen[inst] u
useq : s ∩ u = s ∩ f ⁻¹' t
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
exact ⟨u, ou, by simpa only [Set.inter_comm, eq_comm] using useq⟩
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
u : Set α
ou : IsOpen[inst] u
useq : f ⁻¹' t ∩ s = u ∩ s
⊢ s ∩ u = s ∩ f ⁻¹' t

Tactic:
simpa only [Set.inter_comm, eq_comm] using useq

Premises used: eq_comm, Set.inter_comm
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
u : Set α
ou : IsOpen[inst] u
useq : f ⁻¹' t ∩ s = u ∩ s
⊢ ∃ (t_1 : Set α), IsOpen[inst] t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t

Tactic:
exact ⟨u, ou, by simpa only [Set.inter_comm, eq_comm] using useq⟩
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
⊢ ∀ (t : Set β),
    IsOpen[instTopologicalSpaceSubtype] (s.restrict (π := fun (a : α) ↦ β) f ⁻¹' t) ↔
      ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
have : ∀ t, IsOpen (s.restrict f ⁻¹' t) ↔ ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s := by
    intro t
    rw [isOpen_induced_iff, Set.restrict_eq, Set.preimage_comp]
    simp only [Subtype.preimage_coe_eq_preimage_coe_iff]
    constructor <;>
      · rintro ⟨u, ou, useq⟩
        exact ⟨u, ou, by simpa only [Set.inter_comm, eq_comm] using useq⟩
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
this :
  ∀ (t : Set β),
    IsOpen[instTopologicalSpaceSubtype] (s.restrict (π := fun (a : α) ↦ β) f ⁻¹' t) ↔
      ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
rw :
  (∀ (s_1 : Set β),
      IsOpen[inst_1] s_1 → IsOpen[instTopologicalSpaceSubtype] (s.restrict (π := fun (a : α) ↦ β) f ⁻¹' s_1)) ↔
    ∀ (t : Set β), IsOpen[inst_1] t → ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsOpen[inst_1] t → ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
rw [continuousOn_iff_continuous_restrict, continuous_def]

Premises used: continuousOn_iff_continuous_restrict, continuous_def
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
this :
  ∀ (t : Set β),
    IsOpen[instTopologicalSpaceSubtype] (s.restrict (π := fun (a : α) ↦ β) f ⁻¹' t) ↔
      ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ (∀ (s_1 : Set β),
      IsOpen[inst_1] s_1 → IsOpen[instTopologicalSpaceSubtype] (s.restrict (π := fun (a : α) ↦ β) f ⁻¹' s_1)) ↔
    ∀ (t : Set β), IsOpen[inst_1] t → ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
simp only [this]
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_5
β : Type u_6
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
s : Set α
f : α → β
h₂ : ContinuousOn f s
⊢ ContinuousOn f s

Tactic:
fun x hx _u hu =>
  map_mono (inf_le_inf_right _ <| nhds_mono h₁) (h₂ x hx hu)

Premises used: Filter.map_mono, ContinuousWithinAt, Set.Mem, inf_le_inf_right, Filter.Tendsto, nhds_mono, Filter.principal, ContinuousOn
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_5
β : Type u_6
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₃
s : Set α
f : α → β
h₂ : ContinuousOn f s
⊢ ContinuousOn f s

Tactic:
fun x hx _u hu =>
  h₂ x hx <| nhds_mono h₁ hu

Premises used: ContinuousWithinAt, Filter.Tendsto, nhds_mono, ContinuousOn
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
rw :
  (∃ (t_1 : Set α),
      IsClosed[inst] t_1 ∧
        Eq (α := Set (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1)
          (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' f ⁻¹' t)) ↔
    ∃ (u : Set α), IsClosed[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ IsClosed[instTopologicalSpaceSubtype] (s.restrict (π := fun (a : α) ↦ β) f ⁻¹' t) ↔
    ∃ (u : Set α), IsClosed[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
rw [isClosed_induced_iff, Set.restrict_eq, Set.preimage_comp]

Premises used: Set.preimage_comp, isClosed_induced_iff, Set.restrict_eq
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
⊢ (∃ (t_1 : Set α),
      IsClosed[inst] t_1 ∧
        Eq (α := Set (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1)
          (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' f ⁻¹' t)) ↔
    ∃ (u : Set α), IsClosed[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
simp only [Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm, Set.inter_comm s]

Premises used: eq_comm, Set.inter_comm, Subtype.preimage_coe_eq_preimage_coe_iff
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
⊢ ∀ (t : Set β),
    IsClosed[instTopologicalSpaceSubtype] (s.restrict (π := fun (a : α) ↦ β) f ⁻¹' t) ↔
      ∃ (u : Set α), IsClosed[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
have : ∀ t, IsClosed (s.restrict f ⁻¹' t) ↔ ∃ u : Set α, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s := by
    intro t
    rw [isClosed_induced_iff, Set.restrict_eq, Set.preimage_comp]
    simp only [Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm, Set.inter_comm s]
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
this :
  ∀ (t : Set β),
    IsClosed[instTopologicalSpaceSubtype] (s.restrict (π := fun (a : α) ↦ β) f ⁻¹' t) ↔
      ∃ (u : Set α), IsClosed[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
rw :
  (∀ (s_1 : Set β),
      IsClosed[inst_1] s_1 → IsClosed[instTopologicalSpaceSubtype] (s.restrict (π := fun (a : α) ↦ β) f ⁻¹' s_1)) ↔
    ∀ (t : Set β), IsClosed[inst_1] t → ∃ (u : Set α), IsClosed[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsClosed[inst_1] t → ∃ (u : Set α), IsClosed[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
rw [continuousOn_iff_continuous_restrict, continuous_iff_isClosed]

Premises used: continuous_iff_isClosed, continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
this :
  ∀ (t : Set β),
    IsClosed[instTopologicalSpaceSubtype] (s.restrict (π := fun (a : α) ↦ β) f ⁻¹' t) ↔
      ∃ (u : Set α), IsClosed[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ (∀ (s_1 : Set β),
      IsClosed[inst_1] s_1 → IsClosed[instTopologicalSpaceSubtype] (s.restrict (π := fun (a : α) ↦ β) f ⁻¹' s_1)) ↔
    ∀ (t : Set β), IsClosed[inst_1] t → ∃ (u : Set α), IsClosed[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
simp only [this]
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Sort u_5
s : ι → Set α
hs : ∀ (x : α), ∃ (i : ι), s i ∈ 𝓝 x
hf : ∀ (i : ι), ContinuousOn f (s i)
x : α
i : ι
hi : s i ∈ 𝓝 x
rw : Tendsto f (𝓝[s i] x) (𝓝 (f x))
⊢ ContinuousAt f x

Tactic:
rw [ContinuousAt, ← nhdsWithin_eq_nhds.2 hi]

Premises used: Iff.mpr, ContinuousAt, nhdsWithin_eq_nhds
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Sort u_5
s : ι → Set α
hs : ∀ (x : α), ∃ (i : ι), s i ∈ 𝓝 x
hf : ∀ (i : ι), ContinuousOn f (s i)
x : α
i : ι
hi : s i ∈ 𝓝 x
⊢ Tendsto f (𝓝[s i] x) (𝓝 (f x))

Tactic:
hf _ _ (mem_of_mem_nhds hi)

Premises used: ContinuousWithinAt, mem_of_mem_nhds
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Sort u_5
s : ι → Set α
hs : ∀ (x : α), ∃ (i : ι), s i ∈ 𝓝 x
hf : ∀ (i : ι), ContinuousOn f (s i)
x : α
i : ι
hi : s i ∈ 𝓝 x
⊢ Tendsto f (𝓝[s i] x) (𝓝 (f x))

Tactic:
exact hf _ _ (mem_of_mem_nhds hi)

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
⊢ ContinuousOn f ∅

Tactic:
fun _ => False.elim

Premises used: Set.Mem, False.elim, ContinuousOn
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
a : α
⊢ ContinuousWithinAt f {a} a

Tactic:
simpa only [ContinuousWithinAt, nhdsWithin_singleton, tendsto_pure_left] using fun s =>
      mem_of_mem_nhds

Premises used: nhdsWithin_singleton, Filter.tendsto_pure_left, ContinuousWithinAt, mem_of_mem_nhds
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
hs : s.Subsingleton
f : α → β
⊢ ContinuousOn f s

Tactic:
hs.induction_on (continuousOn_empty f) (continuousOn_singleton f)

Premises used: continuousOn_singleton, Set.Subsingleton.induction_on, continuousOn_empty
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst] s
rw :
  (∀ (t : Set β), IsOpen[inst_1] t → ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s) ↔
    ∀ (t : Set β), IsOpen[inst_1] t → IsOpen[inst] (s ∩ f ⁻¹' t)
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsOpen[inst_1] t → IsOpen[inst] (s ∩ f ⁻¹' t)

Tactic:
rw [continuousOn_iff']

Premises used: continuousOn_iff'
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst] s
mp :
  (∀ (t : Set β), IsOpen[inst_1] t → ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s) →
    ∀ (t : Set β), IsOpen[inst_1] t → IsOpen[inst] (s ∩ f ⁻¹' t)
mpr :
  (∀ (t : Set β), IsOpen[inst_1] t → IsOpen[inst] (s ∩ f ⁻¹' t)) →
    ∀ (t : Set β), IsOpen[inst_1] t → ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ (∀ (t : Set β), IsOpen[inst_1] t → ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s) ↔
    ∀ (t : Set β), IsOpen[inst_1] t → IsOpen[inst] (s ∩ f ⁻¹' t)

Tactic:
constructor
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst] s
h : ∀ (t : Set β), IsOpen[inst_1] t → ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen[inst_1] t
mp : ∀ (u : Set α) (u_open : IsOpen[inst] u) (hu : f ⁻¹' t ∩ s = u ∩ s), IsOpen[inst] (s ∩ f ⁻¹' t)
⊢ IsOpen[inst] (s ∩ f ⁻¹' t)

Tactic:
rcases h t ht with ⟨u, u_open, hu⟩
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst] s
h : ∀ (t : Set β), IsOpen[inst_1] t → ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen[inst_1] t
u : Set α
u_open : IsOpen[inst] u
hu : f ⁻¹' t ∩ s = u ∩ s
mp : IsOpen[inst] (u ∩ s)
⊢ IsOpen[inst] (s ∩ f ⁻¹' t)

Tactic:
rw [inter_comm, hu]

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst] s
h : ∀ (t : Set β), IsOpen[inst_1] t → ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen[inst_1] t
u : Set α
u_open : IsOpen[inst] u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ IsOpen[inst] (u ∩ s)

Tactic:
apply IsOpen.inter u_open hs

Premises used: IsOpen.inter
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst] s
h : ∀ (t : Set β), IsOpen[inst_1] t → IsOpen[inst] (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen[inst_1] t
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
⟨s ∩ f ⁻¹' t, h t ht, ?_⟩

Premises used: Inter.inter, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst] s
h : ∀ (t : Set β), IsOpen[inst_1] t → IsOpen[inst] (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen[inst_1] t
mpr : f ⁻¹' t ∩ s = s ∩ f ⁻¹' t ∩ s
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
refine ⟨s ∩ f ⁻¹' t, h t ht, ?_⟩
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst] s
h : ∀ (t : Set β), IsOpen[inst_1] t → IsOpen[inst] (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen[inst_1] t
mpr : f ⁻¹' t ∩ s = f ⁻¹' t ∩ s ∩ s
mpr₁ : f ⁻¹' t ∩ s = f ⁻¹' t ∩ (s ∩ s)
mpr₂ mpr₃ : f ⁻¹' t ∩ s = f ⁻¹' t ∩ s
⊢ f ⁻¹' t ∩ s = s ∩ f ⁻¹' t ∩ s

Tactic:
rw [@inter_comm _ s (f ⁻¹' t), inter_assoc, inter_self]

Premises used: Set.inter_self, Set.inter_comm, Set.preimage, Set.inter_assoc
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsOpen[inst] s
ht : IsOpen[inst_1] t
⊢ IsOpen[inst] (s ∩ f ⁻¹' t)

Tactic:
(continuousOn_open_iff hs).1 hf t ht

Premises used: Iff.mp, continuousOn_open_iff
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
h : ContinuousOn f s
hs : IsOpen[inst] s
hp : f ⁻¹' t ⊆ s
ht : IsOpen[inst_1] t
⊢ IsOpen[inst] (s ∩ f ⁻¹' t)

Tactic:
(continuousOn_open_iff hs).mp h t ht

Premises used: Iff.mp, continuousOn_open_iff
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
h : ContinuousOn f s
hs : IsOpen[inst] s
hp : f ⁻¹' t ⊆ s
ht : IsOpen[inst_1] t
h₁ : f ⁻¹' t = s ∩ f ⁻¹' t
⊢ IsOpen[inst] (f ⁻¹' t)

Tactic:
convert! (continuousOn_open_iff hs).mp h t ht

Premises used: Iff.mp, continuousOn_open_iff
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
h : ContinuousOn f s
hs : IsOpen[inst] s
hp : f ⁻¹' t ⊆ s
ht : IsOpen[inst_1] t
h₁ : f ⁻¹' t = f ⁻¹' t ∩ s
h₂ h₃ : f ⁻¹' t = f ⁻¹' t
⊢ f ⁻¹' t = s ∩ f ⁻¹' t

Tactic:
rw [inter_comm, inter_eq_self_of_subset_left hp]

Premises used: Set.inter_comm, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsClosed[inst] s
ht : IsClosed[inst_1] t
rcases : ∀ (u : Set α) (hu : IsClosed[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s), IsClosed[inst] (s ∩ f ⁻¹' t)
⊢ IsClosed[inst] (s ∩ f ⁻¹' t)

Tactic:
rcases continuousOn_iff_isClosed.1 hf t ht with ⟨u, hu⟩

Premises used: Iff.mp, continuousOn_iff_isClosed
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsClosed[inst] s
ht : IsClosed[inst_1] t
u : Set α
hu : IsClosed[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
rw : IsClosed[inst] (u ∩ s)
⊢ IsClosed[inst] (s ∩ f ⁻¹' t)

Tactic:
rw [inter_comm, hu.2]

Premises used: Set.inter_comm, And.right
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsClosed[inst] s
ht : IsClosed[inst_1] t
u : Set α
hu : IsClosed[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ IsClosed[inst] (u ∩ s)

Tactic:
apply IsClosed.inter hu.1 hs

Premises used: And.left, IsClosed.inter
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsOpen[inst] s
rw : interior s ∩ interior (f ⁻¹' t) = s ∩ interior (f ⁻¹' t)
rw₁ rw₂ : s ∩ interior (f ⁻¹' t) = s ∩ interior (f ⁻¹' t)
⊢ interior (s ∩ f ⁻¹' t) = s ∩ interior (f ⁻¹' t)

Tactic:
rw [interior_inter, hs.interior_eq]

Premises used: interior_inter, IsOpen.interior_eq
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ (t : Set α), IsOpen[inst] t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
rcases : ∀ (t : Set α) (open_t : IsOpen[inst] t) (xt : x ∈ t) (ct : ContinuousOn f (s ∩ t)), ContinuousWithinAt f s x
⊢ ContinuousWithinAt f s x

Tactic:
rcases h x xs with ⟨t, open_t, xt, ct⟩
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ (t : Set α), IsOpen[inst] t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
t : Set α
open_t : IsOpen[inst] t
xt : x ∈ t
ct : ContinuousOn f (s ∩ t)
⊢ ContinuousWithinAt f (s ∩ t) x

Tactic:
have := ct x ⟨xs, xt⟩
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ (t : Set α), IsOpen[inst] t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
t : Set α
open_t : IsOpen[inst] t
xt : x ∈ t
ct : ContinuousOn f (s ∩ t)
this : ContinuousWithinAt f (s ∩ t) x
rwa : ∀ (this : Tendsto f (𝓝[s ∩ t] x) (𝓝 (f x))), ContinuousWithinAt f s x
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : Tendsto f (𝓝[s] x) (𝓝 (f x))), ContinuousWithinAt f s x
⊢ ContinuousWithinAt f s x

Tactic:
rwa [ContinuousWithinAt, ← nhdsWithin_restrict _ xt open_t] at this

Premises used: ContinuousWithinAt, nhdsWithin_restrict
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
β : Type u_5
T : Set (Set β)
f : α → β
x : α
h : x ∈ s
simp : (∀ (i : Set β), f x ∈ i → i ∈ T → ∀ᶠ (a : α) in 𝓝[s] x, f a ∈ i) ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x
⊢ Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x

Tactic:
simp only [TopologicalSpace.nhds_generateFrom, tendsto_iInf, tendsto_principal, mem_setOf_eq,
      and_imp]

Premises used: and_imp, TopologicalSpace.nhds_generateFrom, Filter.tendsto_principal, Set.mem_setOf_eq, Filter.tendsto_iInf
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
β : Type u_5
T : Set (Set β)
f : α → β
x : α
h : x ∈ s
⊢ (∀ (i : Set β), f x ∈ i → i ∈ T → ∀ᶠ (a : α) in 𝓝[s] x, f a ∈ i) ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x

Tactic:
forall_congr' fun t => forall_comm

Premises used: forall_comm, forall_congr'
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
β : Type u_5
T : Set (Set β)
f : α → β
x : α
h : x ∈ s
⊢ (∀ (i : Set β), f x ∈ i → i ∈ T → ∀ᶠ (a : α) in 𝓝[s] x, f a ∈ i) ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x

Tactic:
exact forall_congr' fun t => forall_comm

Premises used: forall_comm, forall_congr'
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_5
s : Set α
T : Set (Set β)
f : α → β
h : ∀ t ∈ T, IsOpen[inst] (s ∩ f ⁻¹' t)
⊢ ContinuousOn f s

Tactic:
continuousOn_to_generateFrom_iff.2 fun _x hx t ht hxt => mem_nhdsWithin.2
    ⟨_, h t ht, ⟨hx, hxt⟩, fun _y hy => hy.1.2⟩

Premises used: Iff.mpr, mem_nhdsWithin, Inter.inter, And.right, Set.preimage, And.left, And.intro, Exists.intro, continuousOn_to_generateFrom_iff
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s t : Set α
x : α
h : ContinuousWithinAt f t x
hs : s ⊆ t
⊢ ContinuousWithinAt f s x

Tactic:
h.mono_left (nhdsWithin_mono x hs)

Premises used: ContinuousWithinAt, Filter.Tendsto.mono_left, nhdsWithin_mono
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s t : Set α
x : α
h : ContinuousWithinAt f t x
hs : t ∈ 𝓝[s] x
⊢ ContinuousWithinAt f s x

Tactic:
h.mono_left (nhdsWithin_le_of_mem hs)

Premises used: ContinuousWithinAt, nhdsWithin_le_of_mem, Filter.Tendsto.mono_left
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s t : Set α
x : α
h : s =ᶠ[𝓝 x] t
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_eq_iff_eventuallyEq.mpr h]

Premises used: Iff.mpr, ContinuousWithinAt, nhdsWithin_eq_iff_eventuallyEq
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s t : Set α
x : α
hf : ContinuousWithinAt f s x
h : s =ᶠ[𝓝 x] t
⊢ ContinuousWithinAt f t x

Tactic:
(continuousWithinAt_congr_set h).1 hf

Premises used: continuousWithinAt_congr_set, Iff.mp
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s t : Set α
x : α
h : t ∈ 𝓝[s] x
⊢ ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x

Tactic:
simp [ContinuousWithinAt, nhdsWithin_restrict'' s h]

Premises used: ContinuousWithinAt, nhdsWithin_restrict''
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s t : Set α
x : α
h : t ∈ 𝓝 x
⊢ ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x

Tactic:
simp [ContinuousWithinAt, nhdsWithin_restrict' s h]

Premises used: ContinuousWithinAt, nhdsWithin_restrict'
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s t : Set α
x : α
⊢ ContinuousWithinAt f (s ∪ t) x ↔ ContinuousWithinAt f s x ∧ ContinuousWithinAt f t x

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_union, tendsto_sup]

Premises used: ContinuousWithinAt, Filter.tendsto_sup, nhdsWithin_union