mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case zero_eq
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
⊢ ∀ x ∈ s, ((q (f x)).taylorComp (p x) 0).curry0 = (g ∘ f) x

pp: case fderivWithin
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
⊢ ∀ (m : ℕ),
    ↑m < n →
      ∀ x ∈ s,
        HasFDerivWithinAt (fun x ↦ (q (f x)).taylorComp (p x) m) ((q (f x)).taylorComp (p x) m.succ).curryLeft s x

pp: case cont
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ (q (f x)).taylorComp (p x) m) s

Tactic:
·

Goal state after:
case zero_eq
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
⊢ ∀ x ∈ s, ((q (f x)).taylorComp (p x) 0).curry0 = (g ∘ f) x
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: case hc₀
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : (𝓝[>] 0 ⊓ 𝓟 {x_1 | x + ↑x_1 • y ∈ s}).NeBot
⊢ Tendsto ?m.98 (𝓝[>] 0 ⊓ 𝓟 {t | x + ↑t • y ∈ s}) (𝓝[≠] 0)

pp: case hmem
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : (𝓝[>] 0 ⊓ 𝓟 {x_1 | x + ↑x_1 • y ∈ s}).NeBot
⊢ ∀ᶠ (n : ℝ≥0) in 𝓝[>] 0 ⊓ 𝓟 {t | x + ↑t • y ∈ s}, x + ?m.98 n • y ∈ s

pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : (𝓝[>] 0 ⊓ 𝓟 {x_1 | x + ↑x_1 • y ∈ s}).NeBot
⊢ ℝ≥0 → ℝ≥0

Tactic:
·

Goal state after:
case hc₀
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : (𝓝[>] 0 ⊓ 𝓟 {x_1 | x + ↑x_1 • y ∈ s}).NeBot
⊢ Tendsto ?m.98 (𝓝[>] 0 ⊓ 𝓟 {t | x + ↑t • y ∈ s}) (𝓝[≠] 0)
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: case hmem
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : (𝓝[>] 0 ⊓ 𝓟 {x_1 | x + ↑x_1 • y ∈ s}).NeBot
⊢ ∀ᶠ (n : ℝ≥0) in 𝓝[>] 0 ⊓ 𝓟 {t | x + ↑t • y ∈ s}, x + id n • y ∈ s

Tactic:
·

Goal state after:
case hmem
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : (𝓝[>] 0 ⊓ 𝓟 {x_1 | x + ↑x_1 • y ∈ s}).NeBot
⊢ ∀ᶠ (n : ℝ≥0) in 𝓝[>] 0 ⊓ 𝓟 {t | x + ↑t • y ∈ s}, x + id n • y ∈ s
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case fderivWithin
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
⊢ ∀ (m : ℕ),
    ↑m < n →
      ∀ x ∈ s,
        HasFDerivWithinAt (fun x ↦ (q (f x)).taylorComp (p x) m) ((q (f x)).taylorComp (p x) m.succ).curryLeft s x

pp: case cont
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ (q (f x)).taylorComp (p x) m) s

Tactic:
·

Goal state after:
case fderivWithin
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
⊢ ∀ (m : ℕ),
    ↑m < n →
      ∀ x ∈ s,
        HasFDerivWithinAt (fun x ↦ (q (f x)).taylorComp (p x) m) ((q (f x)).taylorComp (p x) m.succ).curryLeft s x
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: case mp
s : Set ℝ
a : ℝ
⊢ 1 ∈ posTangentConeAt s a → a ∈ closure (Ioi a ∩ s)

pp: case mpr
s : Set ℝ
a : ℝ
⊢ a ∈ closure (Ioi a ∩ s) → 1 ∈ posTangentConeAt s a

Tactic:
·

Goal state after:
case mp
s : Set ℝ
a : ℝ
⊢ 1 ∈ posTangentConeAt s a → a ∈ closure (Ioi a ∩ s)
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case succ.zero
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
⊢ iteratedDerivWithin 0 (fun x ↦ x ^ (i + 1)) s x = ↑((i + 1).descFactorial 0) * x ^ (i + 1 - 0)

pp: case succ.succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
⊢ iteratedDerivWithin (k + 1) (fun x ↦ x ^ (i + 1)) s x = ↑((i + 1).descFactorial (k + 1)) * x ^ (i + 1 - (k + 1))

Tactic:
·

Goal state after:
case succ.zero
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
⊢ iteratedDerivWithin 0 (fun x ↦ x ^ (i + 1)) s x = ↑((i + 1).descFactorial 0) * x ^ (i + 1 - 0)
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:

Tactic:
iteratedFDerivWithin 𝕜 (i + 1) (-f) s x h =
          fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x (h 0) (Fin.tail h) :=
        iteratedFDerivWithin_succ_apply_left _
      _ = fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x (h 0) (Fin.tail h) := by
        rw [fderivWithin_congr' (@hi) hx, Pi.neg_def]
      _ = -(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s) x (h 0) (Fin.tail h) := by
        rw [fderivWithin_neg (hu x hx), neg_apply, neg_apply]
      _ = -(iteratedFDerivWithin 𝕜 (i + 1) f s) x h := by
        rw [iteratedFDerivWithin_succ_apply_left]

Goal state after:
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: case mpr
s : Set ℝ
a : ℝ
⊢ a ∈ closure (Ioi a ∩ s) → 1 ∈ posTangentConeAt s a

Tactic:
·

Goal state after:
case mpr
s : Set ℝ
a : ℝ
⊢ a ∈ closure (Ioi a ∩ s) → 1 ∈ posTangentConeAt s a
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)

Tactic:
by_cases! hab : a = b

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a = b
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)

case neg
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a = b
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)

pp: case neg
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a = b
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case neg.hB
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
⊢ Icc a b ⊆ closure[inst✝⁵] (Ioo a b)

pp: case neg.hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
⊢ ∀ x ∈ Icc a b, ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
·

Goal state after:
case neg.hB
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
⊢ Icc a b ⊆ closure[inst✝⁵] (Ioo a b)
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case neg.hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
⊢ ∀ x ∈ Icc a b, ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
·

Goal state after:
case neg.hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
⊢ ∀ x ∈ Icc a b, ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case neg.hf.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
b : α
la lb : β
inst✝ : RegularSpace β
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
x : α
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[>] x) (𝓝 la)
hab : x ≠ b
x_in : x ∈ Icc x b
⊢ ∃ y, Tendsto f (𝓝[Ioo x b] x) (𝓝 y)

pp: case neg.hf.inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a : α
la lb : β
inst✝ : RegularSpace β
ha : Tendsto f (𝓝[>] a) (𝓝 la)
x : α
hf : ContinuousOn f (Ioo a x)
hb : Tendsto f (𝓝[<] x) (𝓝 lb)
hab : a ≠ x
x_in : x ∈ Icc a x
⊢ ∃ y, Tendsto f (𝓝[Ioo a x] x) (𝓝 y)

pp: case neg.hf.inr.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
x : α
x_in : x ∈ Icc a b
h : x ∈ Ioo a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
·

Goal state after:
case neg.hf.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
b : α
la lb : β
inst✝ : RegularSpace β
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
x : α
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[>] x) (𝓝 la)
hab : x ≠ b
x_in : x ∈ Icc x b
⊢ ∃ y, Tendsto f (𝓝[Ioo x b] x) (𝓝 y)
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case neg.hf.inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a : α
la lb : β
inst✝ : RegularSpace β
ha : Tendsto f (𝓝[>] a) (𝓝 la)
x : α
hf : ContinuousOn f (Ioo a x)
hb : Tendsto f (𝓝[<] x) (𝓝 lb)
hab : a ≠ x
x_in : x ∈ Icc a x
⊢ ∃ y, Tendsto f (𝓝[Ioo a x] x) (𝓝 y)

pp: case neg.hf.inr.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
x : α
x_in : x ∈ Icc a b
h : x ∈ Ioo a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
·

Goal state after:
case neg.hf.inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a : α
la lb : β
inst✝ : RegularSpace β
ha : Tendsto f (𝓝[>] a) (𝓝 la)
x : α
hf : ContinuousOn f (Ioo a x)
hb : Tendsto f (𝓝[<] x) (𝓝 lb)
hab : a ≠ x
x_in : x ∈ Icc a x
⊢ ∃ y, Tendsto f (𝓝[Ioo a x] x) (𝓝 y)
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case neg.hf.inr.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
x : α
x_in : x ∈ Icc a b
h : x ∈ Ioo a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
·

Goal state after:
case neg.hf.inr.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
x : α
x_in : x ∈ Icc a b
h : x ∈ Ioo a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)

Tactic:
by_cases! hab : a = b

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a = b
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)

case neg
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a = b
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)

pp: case neg
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a = b
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case neg.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
hab' : a < b
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)

pp: case neg.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
hba' : b < a
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)

Tactic:
·

Goal state after:
case neg.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
hab' : a < b
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case neg.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
hba' : b < a
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)

Tactic:
·

Goal state after:
case neg.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
hba' : b < a
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a ≥ b
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)

pp: case neg
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a ≥ b
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case neg.hB
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
⊢ Ico a b ⊆ closure[inst✝⁵] (Ioo a b)

pp: case neg.hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
⊢ ∀ x ∈ Ico a b, ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
·

Goal state after:
case neg.hB
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
⊢ Ico a b ⊆ closure[inst✝⁵] (Ioo a b)
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case neg.hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
⊢ ∀ x ∈ Ico a b, ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
·

Goal state after:
case neg.hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
⊢ ∀ x ∈ Ico a b, ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)