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

Goal state before:
pp: u b c : ℕ → ℝ
n₀ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n₀ ≤ n
⊢ u n ≤ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * rexp (∑ i ∈ Ico n₀ n, c i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.DiscreteGronwall

Goal state before:
pp: u b c : ℕ → ℝ
n₀ n₁ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n ∈ Ico n₀ n₁
⊢ ∀ i ∈ Ico n₀ n₁, 0 ≤ b i

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace 𝕜 V
inst✝⁷ : CompleteSpace V
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : InnerProductSpace 𝕜 W
inst✝⁴ : CompleteSpace W
F : Type u_4
inst✝³ : EquivLike F (V →L[𝕜] V) (W →L[𝕜] W)
inst✝² : NonUnitalAlgEquivClass F 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
inst✝¹ : StarHomClass F (V →L[𝕜] V) (W →L[𝕜] W)
inst✝ : ContinuousMapClass F (V →L[𝕜] V) (W →L[𝕜] W)
f : F
x y : V →L[𝕜] V
⊢ f x ≤ f y ↔ x ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
α : ℝ → E
t₀ : ℝ
x₀ : E
⊢ picard f t₀ x₀ α t₀ = x₀

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : dist (f a) (g a) ≤ δ
⊢ ∀ t ∈ Icc a b, dist (f t) (g t) ≤ gronwallBound δ (↑K) (εf + εg) (t - a)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
α : ℝ → E
s : Set ℝ
u : Set E
n : WithTop ℕ∞
hf : ContDiffOn ℝ n (uncurry f) (s ×ˢ u)
hα : ContDiffOn ℝ n α s
hmem : ∀ t ∈ s, α t ∈ u
⊢ ContDiffOn ℝ n (fun t ↦ (t, α t)) s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
α : ℝ → E
s : Set ℝ
u : Set E
n : WithTop ℕ∞
hf : ContDiffOn ℝ n (uncurry f) (s ×ˢ u)
hα : ContDiffOn ℝ n α s
hmem : ∀ t ∈ s, α t ∈ u
⊢ MapsTo (fun t ↦ (t, α t)) s (s ×ˢ u)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
α : ℝ → E
s : Set ℝ
u : Set E
n : WithTop ℕ∞
hf : ContDiffOn ℝ n (uncurry f) (s ×ˢ u)
hα : ContDiffOn ℝ n α s
hmem : ∀ t ∈ s, α t ∈ u
⊢ ContDiffOn ℝ n (fun t ↦ f t (α t)) s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Gronwall

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 ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : dist (f a) (g a) ≤ δ
⊢ ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
r L : ℝ≥0
α β : FunSpace t₀ x₀ r L
h : ∀ (t : ↑(Icc tmin tmax)), α.toFun t = β.toFun t
⊢ α = β

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.DiscreteGronwall

Goal state before:
pp: u b c : ℕ → ℝ
n₀ n₁ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n ∈ Ico n₀ n₁
this : 0 ≤ ∑ k ∈ Ico n₀ n₁, b k
⊢ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * rexp (∑ i ∈ Ico n₀ n, c i) ≤
    (u n₀ + ∑ k ∈ Ico n₀ n₁, b k) * rexp (∑ i ∈ Ico n₀ n₁, c i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.DiscreteGronwall

Goal state before:
pp: u b c : ℕ → ℝ
n₀ n₁ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n ∈ Ico n₀ n₁
⊢ u n ≤ (u n₀ + ∑ k ∈ Ico n₀ n₁, b k) * rexp (∑ i ∈ Ico n₀ n₁, c i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Gronwall

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 ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : dist (f a) (g a) ≤ δ
f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0
⊢ ∀ t ∈ Ico a b, dist (v t (g t)) (v t (g t)) ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
α β : FunSpace t₀ x₀ r L
h : (fun α ↦ { toFun := α.toFun, continuous_toFun := ⋯ }) α = (fun α ↦ { toFun := α.toFun, continuous_toFun := ⋯ }) β
⊢ α = β

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
L : ℝ≥0
α : FunSpace t₀ x₀ 0 L
⊢ α.toFun t₀ = x₀

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
dt : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun x ↦ x + dt) (v ∘ fun x ↦ x + dt) (-dt +ᵥ s)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
dt : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun x ↦ x + dt) (v ∘ fun x ↦ x + dt) (-dt +ᵥ s) ↔ IsIntegralCurveOn γ v s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
dt : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun x ↦ x - dt) (v ∘ fun x ↦ x - dt) (dt +ᵥ s) ↔ IsIntegralCurveOn γ v s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ dt : ℝ
⊢ IsIntegralCurveAt (γ ∘ fun x ↦ x + dt) (v ∘ fun x ↦ x + dt) (t₀ - dt) ↔ IsIntegralCurveAt γ v t₀

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
r L : ℝ≥0
⊢ (range fun α ↦ toContinuousMap α) = {α | LipschitzWith L ⇑α ∧ α t₀ ∈ closedBall x₀ ↑r}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ dt : ℝ
⊢ IsIntegralCurveAt (γ ∘ fun x ↦ x - dt) (v ∘ fun x ↦ x - dt) (t₀ + dt) ↔ IsIntegralCurveAt γ v t₀

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
hγ : IsIntegralCurve γ v
dt : ℝ
⊢ IsIntegralCurve (γ ∘ fun x ↦ x + dt) (v ∘ fun x ↦ x + dt)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace 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
hα : IsFixedPt (FunSpace.next hf hx) α
⊢ α.compProj ↑t₀ = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
dt : ℝ
⊢ IsIntegralCurve (γ ∘ fun x ↦ x + dt) (v ∘ fun x ↦ x + dt) ↔ IsIntegralCurve γ v

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
dt : ℝ
⊢ IsIntegralCurve (γ ∘ fun x ↦ x - dt) (v ∘ fun x ↦ x - dt) ↔ IsIntegralCurve γ v

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
a t : ℝ
ht : t ∈ {t | t * a ∈ s}
⊢ HasDerivWithinAt (γ ∘ fun x ↦ x * a) ((a • v ∘ fun x ↦ x * a) t ((γ ∘ fun x ↦ x * a) t)) {t | t * a ∈ s} t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
inst✝ : CompleteSpace E
⊢ Continuous fun a ↦ ‖a t₀ - x₀‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
⊢ a⁻¹ • s = {t | t * a ∈ s}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Gronwall

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 ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : dist (f a) (g a) ≤ δ
⊢ ∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * rexp (↑K * (t - a))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
inst✝ : CompleteSpace E
⊢ Continuous fun a ↦ ↑r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
inst✝ : CompleteSpace E
⊢ CompleteSpace (FunSpace t₀ x₀ r L)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
r L : ℝ≥0
α : FunSpace t₀ x₀ r L
t : ↑(Icc tmin tmax)
⊢ α.compProj ↑t = α.toFun t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
r L : ℝ≥0
α : FunSpace t₀ x₀ r L
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ α.compProj t = α.toFun ⟨t, ht⟩

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace 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
⊢ ∃ α, α ↑t₀ = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeriesComplex

Goal state before:
pp: p : ℂ
⊢ (Summable fun n ↦ 1 / ↑n ^ p) ↔ 1 < p.re

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r
t : ↑(Icc tmin tmax)
⊢ ‖α.toFun t - α.toFun t₀‖ + ‖α.toFun t₀ - x₀‖ ≤ ↑L * |↑t - ↑t₀| + ↑r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r
t : ↑(Icc tmin tmax)
⊢ ↑L * |↑t - ↑t₀| + ↑r ≤ ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) + ↑r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r
t : ↑(Icc tmin tmax)
⊢ ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) + ↑r ≤ ↑a - ↑r + ↑r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r
t : ↑(Icc tmin tmax)
⊢ α.toFun t ∈ closedBall x₀ ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
⊢ IsIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (a⁻¹ • s) ↔ IsIntegralCurveOn γ v s

Tactic:
by

Goal state after:
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₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : FunSpace t₀ x₀ r L
t : ↑(Icc tmin tmax)
⊢ IntervalIntegrable (fun t' ↦ f t' (α.compProj t')) volume ↑t₀ ↑t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
ε : ℝ
hε : ε > 0
h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ ε / |a| > 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
hγ : IsIntegralCurveAt γ v t₀
a : ℝ
ha : a ≠ 0
⊢ IsIntegralCurveAt (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (t₀ / a)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
⊢ IsIntegralCurveAt (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (t₀ / a) ↔ IsIntegralCurveAt γ v t₀

Tactic:
by

Goal state after:
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 y : 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
t₁ t₂ : ↑(Icc tmin tmax)
⊢ dist (picard f (↑t₀) x α.compProj ↑t₁) (picard f (↑t₀) x α.compProj ↑t₂) ≤ ↑L * dist t₁ t₂

Tactic:
by

Goal state after:
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 y : 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
⊢ picard f (↑t₀) x α.compProj ↑t₀ ∈ closedBall x₀ ↑r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
hγ : IsIntegralCurve γ v
a : ℝ
⊢ IsIntegralCurve (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a)

Tactic:
by

Goal state after:
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
⊢ (next hf hx α).toFun t₀ = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
⊢ IsIntegralCurve (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) ↔ IsIntegralCurve γ v

Tactic:
by

Goal state after:
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
⊢ IsFixedPt (next hf hx) α ↔ ∀ (t : ↑(Icc tmin tmax)), α.toFun t = picard f (↑t₀) x α.compProj ↑t

Tactic:
by

Goal state after:
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
n : ℕ
t : ↑(Icc tmin tmax)
α β : FunSpace t₀ x₀ r L
h : dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
⊢ ↑K * dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
    ↑K ^ (n + 1) * |↑t - ↑t₀| ^ n / ↑n ! * dist α β

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
⊢ ∃ α,
    (∀ x ∈ closedBall x₀ ↑r,
        α x ↑t₀ = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Icc tmin tmax) t) ∧
      ∃ L', ∀ t ∈ Icc tmin tmax, LipschitzOnWith L' (fun x ↦ α x t) (closedBall x₀ ↑r)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
⊢ ∃ α,
    (∀ x ∈ closedBall x₀ ↑r,
        α (x, ↑t₀) = x ∧
          ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (fun x_1 ↦ α (x, x_1)) (f t (α (x, t))) (Icc tmin tmax) t) ∧
      ContinuousOn α (closedBall x₀ ↑r ×ˢ Icc tmin tmax)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: 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 > 0, ∃ ε > 0, ∀ x ∈ closedBall x₀ r, ∃ α, α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t

Tactic:
by

Goal state after:
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 : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ Continuous fun x ↦ ↑K ^ (n + 1) * |x - ↑t₀| ^ n / ↑n ! * dist α β

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: 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
⊢ t₀ - ε < t₀

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: 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
⊢ t₀ < t₀ + ε

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ : ℝ
⊢ ∃ α, ∀ᶠ (xt : E × ℝ) in 𝓝 x₀ ×ˢ 𝓝 t₀, α xt.1 t₀ = xt.1 ∧ HasDerivAt (α xt.1) (f (α xt.1 xt.2)) xt.2

Tactic:
by

Goal state after:
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 ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : f a = g a
t : ℝ
ht : t ∈ Icc a b
⊢ f t = g t

Tactic:
by

Goal state after:
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
t : ℝ
ht : t ∈ Ico (-b) (-a)
⊢ -t ∈ Ioc a b

Tactic:
by

Goal state after:
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
⊢ ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))

Tactic:
by

Goal state after:
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))
this : EqOn (f ∘ Neg.neg) (g ∘ Neg.neg) (Icc (-b) (-a))
⊢ EqOn f g (Icc a b)

Tactic:
by

Goal state after:
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))
⊢ (f ∘ Neg.neg) (-b) = (g ∘ Neg.neg) (-b)

Tactic:
by

Goal state after: