awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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)
⊢ (∀ (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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ IsOpen[inst] (s ∩ f ⁻¹' t)
have mp : ∀ (u : Set α) (u_open : IsOpen[inst] u) (hu : f ⁻¹' t ∩ s = u ∩ s), IsOpen[inst] (s ∩ f ⁻¹' t)
Tactic: rcases h t ht with ⟨u, u_open, hu⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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] (s ∩ f ⁻¹' t)
have mp : IsOpen[inst] (u ∩ s)
Tactic: rw [inter_comm, hu]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
have mpr : f ⁻¹' t ∩ s = s ∩ f ⁻¹' t ∩ s
Tactic: refine ⟨s ∩ f ⁻¹' t, h t ht, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ f ⁻¹' t ∩ s = s ∩ f ⁻¹' t ∩ s
have mpr : f ⁻¹' t ∩ s = f ⁻¹' t ∩ s ∩ s
Tactic: rw [@inter_comm _ s (f ⁻¹' t), inter_assoc, inter_self]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ f ⁻¹' t ∩ s = s ∩ f ⁻¹' t ∩ s
have mpr₁ : f ⁻¹' t ∩ s = f ⁻¹' t ∩ (s ∩ s)
Tactic: rw [@inter_comm _ s (f ⁻¹' t), inter_assoc, inter_self]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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)
⊢ f ⁻¹' t ∩ s = s ∩ f ⁻¹' t ∩ s
have mpr₂ : f ⁻¹' t ∩ s = f ⁻¹' t ∩ s
Tactic: rw [@inter_comm _ s (f ⁻¹' t), inter_assoc, inter_self]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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] (f ⁻¹' t)
have h₁ : f ⁻¹' t = s ∩ f ⁻¹' t
Tactic: convert! (continuousOn_open_iff hs).mp h t ht
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ f ⁻¹' t = s ∩ f ⁻¹' t
have h₁ : f ⁻¹' t = f ⁻¹' t ∩ s
Tactic: rw [inter_comm, inter_eq_self_of_subset_left hp]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ f ⁻¹' t = s ∩ f ⁻¹' t
have h₂ : f ⁻¹' t = f ⁻¹' t
Tactic: rw [inter_comm, inter_eq_self_of_subset_left hp]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ IsClosed[inst] (s ∩ f ⁻¹' t)
have rcases : ∀ (u : Set α) (hu : IsClosed[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s), IsClosed[inst] (s ∩ f ⁻¹' t)
Tactic: rcases continuousOn_iff_isClosed.1 hf t ht with ⟨u, hu⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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] (s ∩ f ⁻¹' t)
have rw : IsClosed[inst] (u ∩ s)
Tactic: rw [inter_comm, hu.2]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ interior (s ∩ f ⁻¹' t) = s ∩ interior (f ⁻¹' t)
have rw : interior s ∩ interior (f ⁻¹' t) = s ∩ interior (f ⁻¹' t)
Tactic: rw [interior_inter, hs.interior_eq]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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)
⊢ interior (s ∩ f ⁻¹' t) = s ∩ interior (f ⁻¹' t)
have rw₁ : s ∩ interior (f ⁻¹' t) = s ∩ interior (f ⁻¹' t)
Tactic: rw [interior_inter, hs.interior_eq]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ ContinuousWithinAt f s x
have rcases : ∀ (t : Set α) (open_t : IsOpen[inst] t) (xt : x ∈ t) (ct : ContinuousOn f (s ∩ t)), ContinuousWithinAt f s x
Tactic: rcases h x xs with ⟨t, open_t, xt, ct⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (hypothesis)
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 x
have this : ContinuousWithinAt f (s ∩ t) x
Tactic: have := ct x ⟨xs, xt⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ ContinuousWithinAt f s x
have rwa : ∀ (this : Tendsto f (𝓝[s ∩ t] x) (𝓝 (f x))), ContinuousWithinAt f s x
Tactic: rwa [ContinuousWithinAt, ← nhdsWithin_restrict _ xt open_t] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ ContinuousWithinAt f s x
have rwa₁ : ∀ (this : Tendsto f (𝓝[s] x) (𝓝 (f x))), ContinuousWithinAt f s x
Tactic: rwa [ContinuousWithinAt, ← nhdsWithin_restrict _ xt open_t] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
β : Type u_5
T : Set (Set β)
f : α → β
x : α
h : x ∈ s
⊢ Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x
have simp : (∀ (i : Set β), f x ∈ i → i ∈ T → ∀ᶠ (a : α) in 𝓝[s] x, f a ∈ i) ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x
Tactic: simp only [TopologicalSpace.nhds_generateFrom, tendsto_iInf, tendsto_principal, mem_setOf_eq,
      and_imp]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ¬AccPt x (𝓟 s)
⊢ ContinuousWithinAt f s x
have rw : ContinuousWithinAt f (s \ {x}) x
Tactic: rw [← continuousWithinAt_diff_self]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
⊢ ContinuousWithinAt f {x}ᶜ x ↔ ContinuousAt f x
have rw : ContinuousWithinAt f (univ \ {x}) x ↔ ContinuousAt f x
Tactic: rw [compl_eq_univ_diff, continuousWithinAt_diff_self, continuousWithinAt_univ]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
rw : ContinuousWithinAt f (univ \ {x}) x ↔ ContinuousAt f x
⊢ ContinuousWithinAt f {x}ᶜ x ↔ ContinuousAt f x
have rw₁ : ContinuousWithinAt f univ x ↔ ContinuousAt f x
Tactic: rw [compl_eq_univ_diff, continuousWithinAt_diff_self, continuousWithinAt_univ]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
rw : ContinuousWithinAt f (univ \ {x}) x ↔ ContinuousAt f x
rw₁ : ContinuousWithinAt f univ x ↔ ContinuousAt f x
⊢ ContinuousWithinAt f {x}ᶜ x ↔ ContinuousAt f x
have rw₂ : ContinuousAt f x ↔ ContinuousAt f x
Tactic: rw [compl_eq_univ_diff, continuousWithinAt_diff_self, continuousWithinAt_univ]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
h : ¬AccPt x (𝓟 {x}ᶜ)
⊢ ContinuousAt f x
have rw : ContinuousWithinAt f {x}ᶜ x
Tactic: rw [← continuousWithinAt_compl_self]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
h : s ∈ 𝓝 x
⊢ ContinuousWithinAt f s x ↔ ContinuousAt f x
have rw : ContinuousWithinAt f (univ ∩ s) x ↔ ContinuousAt f x
Tactic: rw [← univ_inter s, continuousWithinAt_inter h, continuousWithinAt_univ]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
h : s ∈ 𝓝 x
rw : ContinuousWithinAt f (univ ∩ s) x ↔ ContinuousAt f x
⊢ ContinuousWithinAt f s x ↔ ContinuousAt f x
have rw₁ : ContinuousWithinAt f univ x ↔ ContinuousAt f x
Tactic: rw [← univ_inter s, continuousWithinAt_inter h, continuousWithinAt_univ]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
h : s ∈ 𝓝 x
rw : ContinuousWithinAt f (univ ∩ s) x ↔ ContinuousAt f x
rw₁ : ContinuousWithinAt f univ x ↔ ContinuousAt f x
⊢ ContinuousWithinAt f s x ↔ ContinuousAt f x
have rw₂ : ContinuousAt f x ↔ ContinuousAt f x
Tactic: rw [← univ_inter s, continuousWithinAt_inter h, continuousWithinAt_univ]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
h : Continuous[inst, inst_1] f
⊢ ContinuousOn f s
have h₁ : ContinuousOn f univ
Tactic: rw [← continuousOn_univ] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))
have A : ContinuousWithinAt f s₁ x
Tactic: have A := (h x (h₁ hx)).mono h₁
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
A : Tendsto f (𝓝[s₁] x) (𝓝 (f x))
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))
have A₁ : Tendsto f (𝓝[s₁] x) (𝓝 (g x))
Tactic: rw [← h' hx] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
x : α
h : f =ᶠ[𝓝[s] x] g
hx : f x = g x
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x
have rw : Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ ContinuousWithinAt g s x
Tactic: rw [ContinuousWithinAt, hx, tendsto_congr' h, ContinuousWithinAt]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
x : α
h : f =ᶠ[𝓝[s] x] g
hx : f x = g x
rw : Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ ContinuousWithinAt g s x
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x
have rw₁ : Tendsto f (𝓝[s] x) (𝓝 (g x)) ↔ ContinuousWithinAt g s x
Tactic: rw [ContinuousWithinAt, hx, tendsto_congr' h, ContinuousWithinAt]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
x : α
h : f =ᶠ[𝓝[s] x] g
hx : f x = g x
rw : Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ ContinuousWithinAt g s x
rw₁ : Tendsto f (𝓝[s] x) (𝓝 (g x)) ↔ ContinuousWithinAt g s x
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x
have rw₂ : Tendsto g (𝓝[s] x) (𝓝 (g x)) ↔ ContinuousWithinAt g s x
Tactic: rw [ContinuousWithinAt, hx, tendsto_congr' h, ContinuousWithinAt]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
x : α
h : f =ᶠ[𝓝[s] x] g
hx : f x = g x
rw : Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ ContinuousWithinAt g s x
rw₁ : Tendsto f (𝓝[s] x) (𝓝 (g x)) ↔ ContinuousWithinAt g s x
rw₂ : Tendsto g (𝓝[s] x) (𝓝 (g x)) ↔ ContinuousWithinAt g s x
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x
have rw₃ : Tendsto g (𝓝[s] x) (𝓝 (g x)) ↔ Tendsto g (𝓝[s] x) (𝓝 (g x))
Tactic: rw [ContinuousWithinAt, hx, tendsto_congr' h, ContinuousWithinAt]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
h : MapsTo f s t
hy : f x = y
⊢ ContinuousWithinAt (g ∘ f) s x
have hg₁ : ContinuousWithinAt g t (f x)
Tactic: subst hy
Cleared hypotheses: y, hg, hy
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
hy : f x = y
⊢ ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x
have hg₁ : ContinuousWithinAt g t (f x)
Tactic: subst hy
Cleared hypotheses: y, hg, hy
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
h : f ⁻¹' t ∈ 𝓝[s] x
hy : f x = y
⊢ ContinuousWithinAt (g ∘ f) s x
have hg₁ : ContinuousWithinAt g t (f x)
Tactic: subst hy
Cleared hypotheses: y, hg, hy
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
hs : t ∈ 𝓝[f '' s] y
hy : f x = y
⊢ ContinuousWithinAt (g ∘ f) s x
have hg₁ : ContinuousWithinAt g t (f x)
Tactic: subst hy
Cleared hypotheses: y, hg, hs, hy
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
hs : t ∈ 𝓝[f '' s] y
hy : f x = y
hg₁ : ContinuousWithinAt g t (f x)
⊢ ContinuousWithinAt (g ∘ f) s x
have hs₁ : t ∈ 𝓝[f '' s] f x
Tactic: subst hy
Cleared hypotheses: y, hg, hs, hy
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
y : β
hg : ContinuousAt g y
hf : ContinuousWithinAt f s x
hy : f x = y
⊢ ContinuousWithinAt (g ∘ f) s x
have hg₁ : ContinuousAt g (f x)
Tactic: subst hy
Cleared hypotheses: y, hg, hy
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : β → γ
f : α → β
s : Set β
hg : ContinuousOn g s
hf : Continuous[inst, inst_1] f
hs : ∀ (x : α), f x ∈ s
⊢ Continuous[inst, inst_2] (g ∘ f)
have rw : ∀ (hf : ContinuousOn f univ) (hs : ∀ (x : α), f x ∈ s), ContinuousOn (g ∘ f) univ
Tactic: rw [← continuousOn_univ] at *
Cleared hypotheses: hf, hs
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f : β × γ → δ
g : α → β
h : α → γ
x : α
s : Set α
y : β × γ
hf : ContinuousAt f y
hg : ContinuousWithinAt g s x
hh : ContinuousWithinAt h s x
e : (g x, h x) = y
⊢ ContinuousWithinAt.{u_1, u_4} (Y := δ) (fun (x : α) ↦ f (g x, h x)) s x
have hf₁ : ContinuousAt f (g x, h x)
Tactic: rw [← e] at hf
Cleared hypotheses: hf, hg, hh, e
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s (x.1, x.2) ↔
    ContinuousWithinAt.{u_2, u_3} (Y := γ) (fun (x_1 : β) ↦ f ((x.1, x.2).1, x_1)) {b : β | ((x.1, x.2).1, b) ∈ s}
      (x.1, x.2).2
have simp_rw : Tendsto f (map (Prod.mk x.1) (𝓝 x.2 ⊓ 𝓟 (Prod.mk x.1 ⁻¹' s))) (𝓝 (f (x.1, x.2))) ↔
  Tendsto (fun (x_1 : β) ↦ f (x.1, x_1)) (𝓝 x.2 ⊓ 𝓟 {b : β | (x.1, b) ∈ s}) (𝓝 (f (x.1, x.2)))
Tactic: simp_rw [ContinuousWithinAt, nhdsWithin, nhds_prod_eq, nhds_discrete, pure_prod,
    ← map_inf_principal_preimage]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s (x.1, x.2) ↔
    ContinuousWithinAt.{u_1, u_3} (Y := γ) (fun (x_1 : α) ↦ f (x_1, (x.1, x.2).2)) {a : α | (a, (x.1, x.2).2) ∈ s}
      (x.1, x.2).1
have simp_rw : Tendsto f (map (fun (a : α) ↦ (a, x.2)) (𝓝 x.1 ⊓ 𝓟 ((fun (a : α) ↦ (a, x.2)) ⁻¹' s))) (𝓝 (f (x.1, x.2))) ↔
  Tendsto (fun (x_1 : α) ↦ f (x_1, x.2)) (𝓝 x.1 ⊓ 𝓟 {a : α | (a, x.2) ∈ s}) (𝓝 (f (x.1, x.2)))
Tactic: simp_rw [ContinuousWithinAt, nhdsWithin, nhds_prod_eq, nhds_discrete, prod_pure,
    ← map_inf_principal_preimage]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology α
f : α × β → γ
x : α × β
⊢ ContinuousAt f x ↔ ContinuousAt.{u_2, u_3} (Y := γ) (fun (x_1 : β) ↦ f (x.1, x_1)) x.2
have simp_rw : ContinuousWithinAt f univ x ↔ ContinuousWithinAt.{u_2, u_3} (Y := γ) (fun (x_1 : β) ↦ f (x.1, x_1)) univ x.2
Tactic: simp_rw [← continuousWithinAt_univ]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology β
f : α × β → γ
x : α × β
⊢ ContinuousAt f x ↔ ContinuousAt.{u_1, u_3} (Y := γ) (fun (x_1 : α) ↦ f (x_1, x.2)) x.1
have simp_rw : ContinuousWithinAt f univ x ↔ ContinuousWithinAt.{u_1, u_3} (Y := γ) (fun (x_1 : α) ↦ f (x_1, x.2)) univ x.1
Tactic: simp_rw [← continuousWithinAt_univ]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
⊢ ContinuousOn f s ↔ ∀ (a : α), ContinuousOn.{u_2, u_3} (Y := γ) (fun (x : β) ↦ f (a, x)) {b : β | (a, b) ∈ s}
have simp_rw : (∀ (a : α) (b : β),
    (a, b) ∈ s → ContinuousWithinAt.{u_2, u_3} (Y := γ) (fun (x : β) ↦ f (a, x)) {b : β | (a, b) ∈ s} b) ↔
  ∀ (a : α) (x : β),
    Membership.mem (γ := Set β) {b : β | (a, b) ∈ s} x →
      ContinuousWithinAt.{u_2, u_3} (Y := γ) (fun (x : β) ↦ f (a, x)) {b : β | (a, b) ∈ s} x
Tactic: simp_rw [ContinuousOn, Prod.forall, continuousWithinAt_prod_of_discrete_left]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
⊢ ContinuousOn f s ↔ ∀ (b : β), ContinuousOn.{u_1, u_3} (Y := γ) (fun (x : α) ↦ f (x, b)) {a : α | (a, b) ∈ s}
have simp_rw : (∀ (a : α) (b : β),
    (a, b) ∈ s → ContinuousWithinAt.{u_1, u_3} (Y := γ) (fun (x : α) ↦ f (x, b)) {a : α | (a, b) ∈ s} a) ↔
  ∀ (b : β) (x : α),
    Membership.mem (γ := Set α) {a : α | (a, b) ∈ s} x →
      ContinuousWithinAt.{u_1, u_3} (Y := γ) (fun (x : α) ↦ f (x, b)) {a : α | (a, b) ∈ s} x
Tactic: simp_rw [ContinuousOn, Prod.forall, continuousWithinAt_prod_of_discrete_right]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology α
f : α × β → γ
⊢ Continuous[instTopologicalSpaceProd, inst_2] f ↔ ∀ (a : α), Continuous[inst_1, inst_2] fun (x : β) ↦ f (a, x)
have simp_rw : ContinuousOn f univ ↔ ∀ (a : α), ContinuousOn.{u_2, u_3} (Y := γ) (fun (x : β) ↦ f (a, x)) univ
Tactic: simp_rw [← continuousOn_univ]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology β
f : α × β → γ
⊢ Continuous[instTopologicalSpaceProd, inst_2] f ↔ ∀ (b : β), Continuous[inst, inst_2] fun (x : α) ↦ f (x, b)
have simp_rw : ContinuousOn f univ ↔ ∀ (b : β), ContinuousOn.{u_1, u_3} (Y := γ) (fun (x : α) ↦ f (x, b)) univ
Tactic: simp_rw [← continuousOn_univ]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology α
f : α × β → γ
⊢ IsOpenMap f ↔ ∀ (a : α), IsOpenMap.{u_2, u_3} (Y := γ) fun (x : β) ↦ f (a, x)
have simp_rw : (∀ (a : α) (b : β), 𝓝 (f (a, b)) ≤ map (f ∘ Prod.mk a) (𝓝 b)) ↔
  ∀ (a : α) (x : β), 𝓝 (f (a, x)) ≤ map (fun (x : β) ↦ f (a, x)) (𝓝 x)
Tactic: simp_rw [isOpenMap_iff_nhds_le, Prod.forall, nhds_prod_eq, nhds_discrete, pure_prod, map_map]