mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ r : ℝ
hr : r > 0
ε : ℝ
hε : ε > 0
α : (x : E) → x ∈ closedBall x₀ r → ℝ → E
hα : ∀ (x : E) (a : x ∈ closedBall x₀ r), α x a t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt (α x a) (f (α x a t)) t
⊢ closedBall x₀ r ×ˢ Ioo (t₀ - ε) (t₀ + ε) ∈ 𝓝 x₀ ×ˢ 𝓝 t₀

pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ r : ℝ
hr : r > 0
ε : ℝ
hε : ε > 0
α : (x : E) → x ∈ closedBall x₀ r → ℝ → E
hα : ∀ (x : E) (a : x ∈ closedBall x₀ r), α x a t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt (α x a) (f (α x a t)) t
⊢ ∀ y ∈ closedBall x₀ r ×ˢ Ioo (t₀ - ε) (t₀ + ε),
    (fun x ↦ if hx : x ∈ closedBall x₀ r then α x hx else 0) y.1 t₀ = y.1 ∧
      HasDerivAt ((fun x ↦ if hx : x ∈ closedBall x₀ r then α x hx else 0) y.1)
        (f ((fun x ↦ if hx : x ∈ closedBall x₀ r then α x hx else 0) y.1 y.2)) y.2

Tactic:
·

Goal state after:
case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ r : ℝ
hr : r > 0
ε : ℝ
hε : ε > 0
α : (x : E) → x ∈ closedBall x₀ r → ℝ → E
hα : ∀ (x : E) (a : x ∈ closedBall x₀ r), α x a t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt (α x a) (f (α x a t)) t
⊢ closedBall x₀ r ×ˢ Ioo (t₀ - ε) (t₀ + ε) ∈ 𝓝 x₀ ×ˢ 𝓝 t₀
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ r : ℝ
hr : r > 0
ε : ℝ
hε : ε > 0
α : (x : E) → x ∈ closedBall x₀ r → ℝ → E
hα : ∀ (x : E) (a : x ∈ closedBall x₀ r), α x a t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt (α x a) (f (α x a t)) t
⊢ ∀ y ∈ closedBall x₀ r ×ˢ Ioo (t₀ - ε) (t₀ + ε),
    (fun x ↦ if hx : x ∈ closedBall x₀ r then α x hx else 0) y.1 t₀ = y.1 ∧
      HasDerivAt ((fun x ↦ if hx : x ∈ closedBall x₀ r then α x hx else 0) y.1)
        (f ((fun x ↦ if hx : x ∈ closedBall x₀ r then α x hx else 0) y.1 y.2)) y.2

Tactic:
·

Goal state after:
case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ r : ℝ
hr : r > 0
ε : ℝ
hε : ε > 0
α : (x : E) → x ∈ closedBall x₀ r → ℝ → E
hα : ∀ (x : E) (a : x ∈ closedBall x₀ r), α x a t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt (α x a) (f (α x a t)) t
⊢ ∀ y ∈ closedBall x₀ r ×ˢ Ioo (t₀ - ε) (t₀ + ε),
    (fun x ↦ if hx : x ∈ closedBall x₀ r then α x hx else 0) y.1 t₀ = y.1 ∧
      HasDerivAt ((fun x ↦ if hx : x ∈ closedBall x₀ r then α x hx else 0) y.1)
        (f ((fun x ↦ if hx : x ∈ closedBall x₀ r then α x hx else 0) y.1 y.2)) y.2
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
⊢ ∀ t ∈ Ico (-b) (-a), HasDerivWithinAt (f ∘ Neg.neg) ((Neg.neg ∘ v (-t)) ((f ∘ Neg.neg) t)) (Ici t) t

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
⊢ ∀ t ∈ Ico (-b) (-a), HasDerivWithinAt (g ∘ Neg.neg) ((Neg.neg ∘ v (-t)) ((g ∘ Neg.neg) t)) (Ici t) t

Tactic:
·

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
⊢ ∀ t ∈ Ico (-b) (-a), HasDerivWithinAt (f ∘ Neg.neg) ((Neg.neg ∘ v (-t)) ((f ∘ Neg.neg) t)) (Ici t) t
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
⊢ ∀ t ∈ Ico (-b) (-a), HasDerivWithinAt (g ∘ Neg.neg) ((Neg.neg ∘ v (-t)) ((g ∘ Neg.neg) t)) (Ici t) t

Tactic:
·

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
⊢ ∀ t ∈ Ico (-b) (-a), HasDerivWithinAt (g ∘ Neg.neg) ((Neg.neg ∘ v (-t)) ((g ∘ Neg.neg) t)) (Ici t) t
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t
hfs : ∀ t ∈ Ioo a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t
hgs : ∀ t ∈ Ioo a b, g t ∈ s t
heq : f t₀ = g t₀
⊢ EqOn f g (Icc a t₀)

pp: case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t
hfs : ∀ t ∈ Ioo a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t
hgs : ∀ t ∈ Ioo a b, g t ∈ s t
heq : f t₀ = g t₀
⊢ EqOn f g (Icc t₀ b)

Tactic:
·

Goal state after:
case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t
hfs : ∀ t ∈ Ioo a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t
hgs : ∀ t ∈ Ioo a b, g t ∈ s t
heq : f t₀ = g t₀
⊢ EqOn f g (Icc a t₀)
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t
hfs : ∀ t ∈ Ioo a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t
hgs : ∀ t ∈ Ioo a b, g t ∈ s t
heq : f t₀ = g t₀
⊢ EqOn f g (Icc t₀ b)

Tactic:
·

Goal state after:
case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t
hfs : ∀ t ∈ Ioo a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t
hgs : ∀ t ∈ Ioo a b, g t ∈ s t
heq : f t₀ = g t₀
⊢ EqOn f g (Icc t₀ b)
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t' : ℝ
ht' : t' ∈ Ioo a b
h : t' < t₀
⊢ f t' = g t'

pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t' : ℝ
ht' : t' ∈ Ioo a b
h : t₀ ≤ t'
⊢ f t' = g t'

Tactic:
·

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t' : ℝ
ht' : t' ∈ Ioo a b
h : t' < t₀
⊢ f t' = g t'
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t' : ℝ
ht' : t' ∈ Ioo a b
h : t₀ ≤ t'
⊢ f t' = g t'

Tactic:
·

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t' : ℝ
ht' : t' ∈ Ioo a b
h : t₀ ≤ t'
⊢ f t' = g t'
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
⊢ ∀ (x_1 : ↑(Icc tmin tmax)),
    dist ((toContinuousMap ((next hf hx)^[n] α)) x_1) ((toContinuousMap ((next hf hx)^[n] β)) x_1) ≤
      (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n ! * dist α β

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
⊢ 0 ≤ (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n ! * dist α β

Tactic:
·

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
⊢ ∀ (x_1 : ↑(Icc tmin tmax)),
    dist ((toContinuousMap ((next hf hx)^[n] α)) x_1) ((toContinuousMap ((next hf hx)^[n] β)) x_1) ≤
      (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n ! * dist α β
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P = 0
⊢ (fun x ↦ eval x P) ~[atTop] fun x ↦ P.leadingCoeff * x ^ P.natDegree

pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x ↦ eval x P) ~[atTop] fun x ↦ P.leadingCoeff * x ^ P.natDegree

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P = 0
⊢ (fun x ↦ eval x P) ~[atTop] fun x ↦ P.leadingCoeff * x ^ P.natDegree
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x ↦ eval x P) ~[atTop] fun x ↦ P.leadingCoeff * x ^ P.natDegree

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x ↦ eval x P) ~[atTop] fun x ↦ P.leadingCoeff * x ^ P.natDegree
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
⊢ 0 ≤ (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n ! * dist α β

Tactic:
·

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
⊢ 0 ≤ (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n ! * dist α β
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < P.degree
hP : 0 ≤ P.leadingCoeff
⊢ Tendsto (fun x ↦ |eval x P|) atTop atTop

pp: case inr
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < P.degree
hP : P.leadingCoeff ≤ 0
⊢ Tendsto (fun x ↦ |eval x P|) atTop atTop

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < P.degree
hP : 0 ≤ P.leadingCoeff
⊢ Tendsto (fun x ↦ |eval x P|) atTop atTop
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < P.degree
hP : P.leadingCoeff ≤ 0
⊢ Tendsto (fun x ↦ |eval x P|) atTop atTop

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < P.degree
hP : P.leadingCoeff ≤ 0
⊢ Tendsto (fun x ↦ |eval x P|) atTop atTop
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: case inl
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
ha : ‖a‖₊ = 1
⊢ ‖a‖₊ < p.cauchyBound

pp: case inr
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
ha : ‖a‖₊ ≠ 1
⊢ ‖a‖₊ < p.cauchyBound

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
ha : ‖a‖₊ = 1
⊢ ‖a‖₊ < p.cauchyBound
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x ↦ eval x P) atTop (𝓝 c)
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

pp: case refine_2
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
⊢ Tendsto (fun x ↦ eval x P) atTop (𝓝 c)

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x ↦ eval x P) atTop (𝓝 c)
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x ↦ eval x P) atTop (𝓝 c)
this : Tendsto (fun x ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x ↦ eval x P) atTop (𝓝 c)
this : Tendsto (fun x ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : ¬P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x ↦ eval x P) atTop (𝓝 c)
this : Tendsto (fun x ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x ↦ eval x P) atTop (𝓝 c)
hP : P.leadingCoeff = 0
this : 0 = c
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
exact ⟨_root_.trans hP this, by simp [leadingCoeff_eq_zero.1 hP]⟩

Goal state after:
Module: Mathlib.Analysis.Polynomial.Fourier

Goal state before:
pp: p : ℂ[X]
n : ℤ
⊢ fourierCoeff (⇑(toAddCircle p)) n = if 0 ≤ n then p.coeff n.natAbs else 0

Tactic:
by
  have : n < 0 ∨ ∃ k : ℕ, n = k := lt_or_ge n 0 |>.imp_right Int.eq_ofNat_of_zero_le
  induction p using Polynomial.induction_on' with obtain (hn | ⟨k, rfl⟩) := this
  | add p q hp hq =>
    simp_all [not_le_of_gt, fourierCoeff.add (toAddCircle.integrable p) (toAddCircle.integrable q)]
  | monomial m a =>
    simp_all [not_le_of_gt, coeff_monomial, toAddCircle_monomial_eq_smul_fourier,
      fourierCoeff.const_smul, fourierCoeff_fourier, Pi.single_apply]
    grind

Goal state after:
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x ↦ eval x P) atTop (𝓝 c)
this : Tendsto (fun x ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : ¬P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x ↦ eval x P) atTop (𝓝 c)
this : Tendsto (fun x ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : ¬P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
⊢ Tendsto (fun x ↦ eval x P) atTop (𝓝 c)

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
⊢ Tendsto (fun x ↦ eval x P) atTop (𝓝 c)
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case e'_5
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
x✝ : 𝕜
⊢ eval x✝ P = ((fun x ↦ eval x (P.comp (-X))) ∘ Neg.neg) x✝

pp: case e'_6
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
x✝ : 𝕜
⊢ P.leadingCoeff * x✝ ^ P.natDegree = ((fun x ↦ (P.comp (-X)).leadingCoeff * x ^ (P.comp (-X)).natDegree) ∘ Neg.neg) x✝

Tactic:
·

Goal state after:
case e'_5
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
x✝ : 𝕜
⊢ eval x✝ P = ((fun x ↦ eval x (P.comp (-X))) ∘ Neg.neg) x✝
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case e'_6
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
x✝ : 𝕜
⊢ P.leadingCoeff * x✝ ^ P.natDegree = ((fun x ↦ (P.comp (-X)).leadingCoeff * x ^ (P.comp (-X)).natDegree) ∘ Neg.neg) x✝

Tactic:
·

Goal state after:
case e'_6
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
x✝ : 𝕜
⊢ P.leadingCoeff * x✝ ^ P.natDegree = ((fun x ↦ (P.comp (-X)).leadingCoeff * x ^ (P.comp (-X)).natDegree) ∘ Neg.neg) x✝
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
ha✝ : ‖a‖₊ ≠ 1
ha : ‖a‖₊ < 1
⊢ ‖a‖₊ < p.cauchyBound

pp: case inr.inr
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
ha✝ : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
⊢ ‖a‖₊ < p.cauchyBound

Tactic:
·

Goal state after:
case inr.inl
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
ha✝ : ‖a‖₊ ≠ 1
ha : ‖a‖₊ < 1
⊢ ‖a‖₊ < p.cauchyBound
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : P = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atTop] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atTop] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : P = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atTop] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)