awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_2
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : SMulCommClass R β β
r : R
f g : α →C₀ β
x_1 : α
⊢ Eq.{v + 1} (α := β) ((r • f • g : (a : α) → β) x_1 : β) ((f • r • g : (a : α) → β) x_1 : β)
have h : r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
  HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
Tactic: simp only [smul_eq_mul, coe_smul, coe_mul, Pi.smul_apply, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_2
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : SMulCommClass R β β
r : R
f g : α →C₀ β
x_1 : α
⊢ r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
have h : r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
  HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
Tactic: rw [← smul_eq_mul, ← smul_eq_mul, smul_comm]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_2
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : SMulCommClass R β β
r : R
f g : α →C₀ β
x_1 : α
h :
  r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
⊢ r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
have h₁ : r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
  HSMul.hSMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
Tactic: rw [← smul_eq_mul, ← smul_eq_mul, smul_comm]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_2
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : SMulCommClass R β β
r : R
f g : α →C₀ β
x_1 : α
h :
  r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
h₁ :
  r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HSMul.hSMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
⊢ r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
have h₂ : HSMul.hSMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β)) =
  HSMul.hSMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
Tactic: rw [← smul_eq_mul, ← smul_eq_mul, smul_comm]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : F
⊢ ∃ (C : ℝ), ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C
have obtain : ∀ (K : Set α) (hK₁ : IsCompact K) (hK₂ : Kᶜ ⊆ preimage.{u, v} (β := β) (⇑f : (a : α) → β) (closedBall 0 1)),
  ∃ (C : ℝ), ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C
Tactic: obtain ⟨K : Set α, hK₁, hK₂⟩ := mem_cocompact.mp
    (tendsto_def.mp (zero_at_infty (f : F)) _ (closedBall_mem_nhds (0 : β) zero_lt_one))
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ preimage.{u, v} (β := β) (⇑f : (a : α) → β) (closedBall 0 1)
⊢ ∃ (C : ℝ), ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C
have obtain : ∀ (C : ℝ) (hC : Subset.{v} (α := Set β) ((⇑f : (a : α) → β) '' K) (closedBall 0 C)),
  ∃ (C : ℝ), ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C
Tactic: obtain ⟨C, hC⟩ := (hK₁.image (map_continuous f)).isBounded.subset_closedBall (0 : β)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ preimage.{u, v} (β := β) (⇑f : (a : α) → β) (closedBall 0 1)
C : ℝ
hC : Subset.{v} (α := Set β) ((⇑f : (a : α) → β) '' K) (closedBall 0 C)
⊢ ∃ (C : ℝ), ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C
have refine : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ max C 1 + max C 1
Tactic: refine ⟨max C 1 + max C 1, fun x y => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ preimage.{u, v} (β := β) (⇑f : (a : α) → β) (closedBall 0 1)
C : ℝ
hC : Subset.{v} (α := Set β) ((⇑f : (a : α) → β) '' K) (closedBall 0 C)
x_1 y x : α
⊢ Membership.mem.{v, v} (α := β) (γ := Set β) (closedBall 0 (max C 1)) ((f : (a : α) → β) x : β)
have pos : ∀ (hx : x ∈ K), Membership.mem.{v, v} (α := β) (γ := Set β) (closedBall 0 (max C 1)) ((f : (a : α) → β) x : β)
Tactic: by_cases hx : x ∈ K
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ preimage.{u, v} (β := β) (⇑f : (a : α) → β) (closedBall 0 1)
C : ℝ
hC : Subset.{v} (α := Set β) ((⇑f : (a : α) → β) '' K) (closedBall 0 C)
x_1 y x : α
pos : ∀ (hx : x ∈ K), Membership.mem.{v, v} (α := β) (γ := Set β) (closedBall 0 (max C 1)) ((f : (a : α) → β) x : β)
⊢ Membership.mem.{v, v} (α := β) (γ := Set β) (closedBall 0 (max C 1)) ((f : (a : α) → β) x : β)
have neg : ∀ (hx : x ∉ K), Membership.mem.{v, v} (α := β) (γ := Set β) (closedBall 0 (max C 1)) ((f : (a : α) → β) x : β)
Tactic: by_cases hx : x ∈ K
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (hypothesis)
Goal:
F : Type u_1
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ preimage.{u, v} (β := β) (⇑f : (a : α) → β) (closedBall 0 1)
C : ℝ
hC : Subset.{v} (α := Set β) ((⇑f : (a : α) → β) '' K) (closedBall 0 C)
x y : α
⊢ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ max C 1 + max C 1
have this : ∀ (x : α), Membership.mem.{v, v} (α := β) (γ := Set β) (closedBall 0 (max C 1)) ((f : (a : α) → β) x : β)
Tactic: have : ∀ x, f x ∈ closedBall (0 : β) (max C 1) := by
    intro x
    by_cases hx : x ∈ K
    · exact (mem_closedBall.mp <| hC ⟨x, hx, rfl⟩).trans (le_max_left _ _)
    · exact (mem_closedBall.mp <| mem_preimage.mp (hK₂ hx)).trans (le_max_right _ _)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f g : α →C₀ β
h : f.toBCF = g.toBCF
⊢ f = g
have h₁ : ∀ (x : α), Eq.{v + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
⊢ Isometry (α := α →C₀ β) toBCF
have tauto : ∀ (x1 x2 : α →C₀ β), edist x1.toBCF x2.toBCF = edist x1 x2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
⊢ IsClosed (X := α →ᵇ β) (range (ι := α →C₀ β) toBCF)
have refine : ∀ (f : α →ᵇ β) (hf : ClusterPt f (𝓟 (range (ι := α →C₀ β) toBCF))),
  Membership.mem (γ := Set (α →ᵇ β)) (range (ι := α →C₀ β) toBCF) f
Tactic: refine isClosed_iff_clusterPt.mpr fun f hf => ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (hypothesis)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ClusterPt f (𝓟 (range (ι := α →C₀ β) toBCF))
⊢ Membership.mem (γ := Set (α →ᵇ β)) (range (ι := α →C₀ β) toBCF) f
have hf₁ : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
Tactic: rw [clusterPt_principal_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
⊢ Tendsto.{u, v} (β := β) (⇑f : (a : α) → β) (cocompact α) (𝓝 0)
have refine : ∀ (ε : ℝ) (hε : ε > 0), ∀ᶠ (x : α) in cocompact α, dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < ε
Tactic: refine Metric.tendsto_nhds.mpr fun ε hε => ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : α) in cocompact α, dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < ε
have obtain : ∀ (g : α →C₀ β) (hg : g.toBCF ∈ ball f (ε / 2)),
  ∀ᶠ (x : α) in cocompact α, dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < ε
Tactic: obtain ⟨_, hg, g, rfl⟩ := hf (ball f (ε / 2)) (ball_mem_nhds f <| half_pos hε)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : g.toBCF ∈ ball f (ε / 2)
⊢ ∀ᶠ (x : α) in cocompact α, dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < ε
have refine : ∀ (x : α) (hx : dist.{v} (α := β) ((g : (a : α) → β) x : β) (0 : β) < ε / 2),
  dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < ε
Tactic: refine (Metric.tendsto_nhds.mp (zero_at_infty g) (ε / 2) (half_pos hε)).mp
      (Eventually.of_forall fun x hx => ?_)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : g.toBCF ∈ ball f (ε / 2)
x : α
hx : dist.{v} (α := β) ((g : (a : α) → β) x : β) (0 : β) < ε / 2
⊢ dist g.toBCF f + ε / 2 ≤ ε
have grw : ε / 2 + ε / 2 ≤ ε
Tactic: grw [mem_ball.1 hg, add_halves ε]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : g.toBCF ∈ ball f (ε / 2)
x : α
hx : dist.{v} (α := β) ((g : (a : α) → β) x : β) (0 : β) < ε / 2
grw : ε / 2 + ε / 2 ≤ ε
⊢ dist g.toBCF f + ε / 2 ≤ ε
have grw₁ : ε ≤ ε
Tactic: grw [mem_ball.1 hg, add_halves ε]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : g.toBCF ∈ ball f (ε / 2)
x : α
hx : dist.{v} (α := β) ((g : (a : α) → β) x : β) (0 : β) < ε / 2
⊢ dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < ε
have dist : dist g.toBCF f + ε / 2 ≤ ε
Tactic: calc
      dist (f x) 0 ≤ dist (g.toBCF x) (f x) + dist (g x) 0 := dist_triangle_left _ _ _
      _ < dist g.toBCF f + ε / 2 := add_lt_add_of_le_of_lt (dist_coe_le_dist x) hx
      _ ≤ ε := by grw [mem_ball.1 hg, add_halves ε]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ZeroAtInfty (hypothesis)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
⊢ Membership.mem (γ := Set (α →ᵇ β)) (range (ι := α →C₀ β) toBCF) f
have this : Tendsto.{u, v} (β := β) (⇑f : (a : α) → β) (cocompact α) (𝓝 0)
Tactic: have : Tendsto f (cocompact α) (𝓝 0) := by
    refine Metric.tendsto_nhds.mpr fun ε hε => ?_
    obtain ⟨_, hg, g, rfl⟩ := hf (ball f (ε / 2)) (ball_mem_nhds f <| half_pos hε)
    refine (Metric.tendsto_nhds.mp (zero_at_infty g) (ε / 2) (half_pos hε)).mp
      (Eventually.of_forall fun x hx => ?_)
    calc
      dist (f x) 0 ≤ dist (g.toBCF x) (f x) + dist (g x) 0 := dist_triangle_left _ _ _
      _ < dist g.toBCF f + ε / 2 := add_lt_add_of_le_of_lt (dist_coe_le_dist x) hx
      _ ≤ ε := by grw [mem_ball.1 hg, add_halves ε]
-- 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 univ x ↔ ContinuousAt f x
have rw : ContinuousWithinAt f univ x ↔ Tendsto f (𝓝 x) (𝓝 (f x))
Tactic: rw [ContinuousAt, ContinuousWithinAt, nhdsWithin_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 ↔ Tendsto f (𝓝 x) (𝓝 (f x))
⊢ ContinuousWithinAt f univ x ↔ ContinuousAt f x
have rw₁ : Tendsto f (𝓝[univ] x) (𝓝 (f x)) ↔ Tendsto f (𝓝 x) (𝓝 (f x))
Tactic: rw [ContinuousAt, ContinuousWithinAt, nhdsWithin_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 ↔ Tendsto f (𝓝 x) (𝓝 (f x))
rw₁ : Tendsto f (𝓝[univ] x) (𝓝 (f x)) ↔ Tendsto f (𝓝 x) (𝓝 (f x))
⊢ ContinuousWithinAt f univ x ↔ ContinuousAt f x
have rw₂ : Tendsto f (𝓝 x) (𝓝 (f x)) ↔ Tendsto f (𝓝 x) (𝓝 (f x))
Tactic: rw [ContinuousAt, ContinuousWithinAt, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
y : β
s t : Set β
h : ContinuousWithinAt f (f ⁻¹' s) x
ht : t ∈ 𝓝[s] y
hxy : y = f x
⊢ f ⁻¹' t ∈ 𝓝[f ⁻¹' s] x
have ht₁ : t ∈ 𝓝[s] f x
Tactic: rw [hxy] at ht
Cleared hypotheses: ht, hxy
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : x ∉ closure[inst] s
⊢ ContinuousWithinAt f s x
have hx₁ : 𝓝[s] x = ⊥
Tactic: rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx
Cleared hypotheses: hx
-- 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 : α
hx : 𝓝[s] x = ⊥
⊢ ContinuousWithinAt f s x
have rw : Tendsto f ⊥ (𝓝 (f x))
Tactic: rw [ContinuousWithinAt, hx]
-- 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 β
⊢ IsOpen[instTopologicalSpaceSubtype] (s.restrict (π := fun (a : α) ↦ β) f ⁻¹' t) ↔
    ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
have 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
Tactic: rw [isOpen_induced_iff, Set.restrict_eq, Set.preimage_comp]
-- 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 β
⊢ (∃ (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
have simp : (∃ (t_1 : Set α), IsOpen[inst] t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t) ↔ ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
Tactic: simp only [Subtype.preimage_coe_eq_preimage_coe_iff]
-- 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 β
⊢ (∃ (t_1 : Set α), IsOpen[inst] t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t) ↔ ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
have mp : (∃ (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
-- 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 β
mp : (∃ (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 ∧ s ∩ t_1 = s ∩ f ⁻¹' t) ↔ ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
have mpr : (∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s) → ∃ (t_1 : Set α), IsOpen[inst] t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsOpen[inst_1] t → ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
have this : ∀ (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⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsOpen[inst_1] t → ∃ (u : Set α), IsOpen[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
have 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
Tactic: rw [continuousOn_iff_continuous_restrict, continuous_def]
-- 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 β
⊢ IsClosed[instTopologicalSpaceSubtype] (s.restrict (π := fun (a : α) ↦ β) f ⁻¹' t) ↔
    ∃ (u : Set α), IsClosed[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
have 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
Tactic: rw [isClosed_induced_iff, Set.restrict_eq, Set.preimage_comp]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsClosed[inst_1] t → ∃ (u : Set α), IsClosed[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
have this : ∀ (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]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsClosed[inst_1] t → ∃ (u : Set α), IsClosed[inst] u ∧ f ⁻¹' t ∩ s = u ∩ s
have 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
Tactic: rw [continuousOn_iff_continuous_restrict, continuous_iff_isClosed]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ ContinuousAt f x
have rw : Tendsto f (𝓝[s i] x) (𝓝 (f x))
Tactic: rw [ContinuousAt, ← nhdsWithin_eq_nhds.2 hi]
-- 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
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsOpen[inst_1] t → IsOpen[inst] (s ∩ f ⁻¹' t)
have 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)
Tactic: rw [continuousOn_iff']
-- 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
⊢ (∀ (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 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)
Tactic: constructor