awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
hy : y ∈ closedBall x₀ (↑r : ℝ)
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ Filter.Tendsto (fun (x : ℕ) ↦ (next hf hy)^[m]^[x] α) Filter.atTop (𝓝 (ContractingWith.fixedPoint (next hf hy)^[m] ⋯))

Tactic:
exact h y hy |>.tendsto_iterate_fixedPoint α

Premises used: ContractingWith.tendsto_iterate_fixedPoint
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
hy : y ∈ closedBall x₀ (↑r : ℝ)
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
nth_rw :
  Filter.Tendsto
    (fun (x_1 : ℕ) ↦
      HMul.hMul (α := ℝ) (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ))
          (∑ i ∈ Finset.range x_1, (↑C : ℝ) ^ i) *
        dist x y)
    Filter.atTop (𝓝 (L' * dist x y))
⊢ Filter.Tendsto
    (fun (x : ℕ) ↦
      HMul.hMul (α := ℝ) (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ))
          (∑ i ∈ Finset.range x, (↑C : ℝ) ^ i) *
        dist α (next hf hy α))
    Filter.atTop (𝓝 (L' * dist x y))

Tactic:
nth_rw 1 [← hα, dist_next_next]

Premises used: ODE.FunSpace.dist_next_next
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
hy : y ∈ closedBall x₀ (↑r : ℝ)
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
hf₁ :
  Filter.Tendsto
    (fun (x : ℕ) ↦
      HMul.hMul (α := ℝ) (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ))
        (∑ i ∈ Finset.range x, (↑C : ℝ) ^ i))
    Filter.atTop (𝓝 L')
⊢ Filter.Tendsto
    (fun (x_1 : ℕ) ↦
      HMul.hMul (α := ℝ) (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ))
          (∑ i ∈ Finset.range x_1, (↑C : ℝ) ^ i) *
        dist x y)
    Filter.atTop (𝓝 (L' * dist x y))

Tactic:
apply Filter.Tendsto.mul_const

Premises used: Filter.Tendsto.mul_const
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
hy : y ∈ closedBall x₀ (↑r : ℝ)
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
hf₁ : Filter.Tendsto (fun (x : ℕ) ↦ ∑ i ∈ Finset.range x, (↑C : ℝ) ^ i) Filter.atTop (𝓝 (↑(1 - C)⁻¹ : ℝ))
⊢ Filter.Tendsto
    (fun (x : ℕ) ↦
      HMul.hMul (α := ℝ) (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ))
        (∑ i ∈ Finset.range x, (↑C : ℝ) ^ i))
    Filter.atTop (𝓝 L')

Tactic:
apply Filter.Tendsto.const_mul

Premises used: Filter.Tendsto.const_mul
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
hy : y ∈ closedBall x₀ (↑r : ℝ)
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ Filter.Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (↑C : ℝ) ^ i) Filter.atTop (𝓝 (1 - (↑C : ℝ))⁻¹)

Tactic:
hasSum_geometric_of_lt_one C.2 (h y hy).1 |>.tendsto_sum_nat

Premises used: HasSum.tendsto_sum_nat, And.left, Subtype.property, hasSum_geometric_of_lt_one
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
hy : y ∈ closedBall x₀ (↑r : ℝ)
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
h₁ : (↑(1 - C)⁻¹ : ℝ) = (1 - (↑C : ℝ))⁻¹
⊢ Filter.Tendsto (fun (x : ℕ) ↦ ∑ i ∈ Finset.range x, (↑C : ℝ) ^ i) Filter.atTop (𝓝 (↑(1 - C)⁻¹ : ℝ))

Tactic:
convert! hasSum_geometric_of_lt_one C.2 (h y hy).1 |>.tendsto_sum_nat

Premises used: HasSum.tendsto_sum_nat, And.left, Subtype.property, hasSum_geometric_of_lt_one
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
hy : y ∈ closedBall x₀ (↑r : ℝ)
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ (↑(1 - C)⁻¹ : ℝ) = (1 - (↑C : ℝ))⁻¹

Tactic:
simp [NNReal.coe_sub <| le_of_lt (h y hy).1, NNReal.coe_one]

Premises used: le_of_lt, And.left, NNReal.coe_one, NNReal.coe_sub
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
t : ℝ
ht : t ∈ Icc tmin tmax
a : HasDerivWithinAt (fun (x : ℝ) ↦ ∫ (τ : ℝ) in t₀..x, f τ (α τ)) (f t (α t)) (Icc tmin tmax) t
⊢ HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t

Tactic:
apply HasDerivWithinAt.const_add

Premises used: HasDerivWithinAt.const_add
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ Fact (t ∈ Icc tmin tmax)

Tactic:
have : Fact (t ∈ Icc tmin tmax) := ⟨ht⟩
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
t : ℝ
ht : t ∈ Icc tmin tmax
this : Fact (t ∈ Icc tmin tmax)
apply : IntervalIntegrable.{u_1} (ε := E) (fun (t : ℝ) ↦ f t (α t)) volume t₀ t
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ ∫ (τ : ℝ) in t₀..x, f τ (α τ)) (f t (α t)) (Icc tmin tmax) t

Tactic:
apply intervalIntegral.integral_hasDerivWithinAt_right _ -- need `CompleteSpace E` and `Icc`
    (continuousOn_comp hf hα hmem |>.stronglyMeasurableAtFilter_nhdsWithin measurableSet_Icc t)
    (continuousOn_comp hf hα hmem _ ht)

Premises used: intervalIntegral.integral_hasDerivWithinAt_right, measurableSet_Icc, ContinuousOn.stronglyMeasurableAtFilter_nhdsWithin, ODE.continuousOn_comp
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
t : ℝ
ht : t ∈ Icc tmin tmax
this : Fact (t ∈ Icc tmin tmax)
hu : ContinuousOn.{0, u_1} (Y := E) (fun (t : ℝ) ↦ f t (α t)) (uIcc t₀ t)
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (t : ℝ) ↦ f t (α t)) volume t₀ t

Tactic:
apply ContinuousOn.intervalIntegrable

Premises used: ContinuousOn.intervalIntegrable
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
t : ℝ
ht : t ∈ Icc tmin tmax
this : Fact (t ∈ Icc tmin tmax)
hu : uIcc t₀ t ⊆ Icc tmin tmax
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (t : ℝ) ↦ f t (α t)) (uIcc t₀ t)

Tactic:
apply continuousOn_comp hf hα hmem |>.mono

Premises used: ContinuousOn.mono, ODE.continuousOn_comp
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
t : ℝ
ht : t ∈ Icc tmin tmax
this : Fact (t ∈ Icc tmin tmax)
⊢ uIcc t₀ t ⊆ Icc tmin tmax

Tactic:
uIcc_subset_Icc ht₀ ht

Premises used: Set.uIcc_subset_Icc
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
t : ℝ
ht : t ∈ Icc tmin tmax
this : Fact (t ∈ Icc tmin tmax)
⊢ uIcc t₀ t ⊆ Icc tmin tmax

Tactic:
exact uIcc_subset_Icc ht₀ ht

Premises used: Set.uIcc_subset_Icc
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ t : ℝ
hf : ContinuousOn (uncurry f) (uIcc t₀ t ×ˢ u)
hα : ∀ t' ∈ uIcc t₀ t, HasDerivWithinAt α (f t' (α t')) (uIcc t₀ t) t'
hmap : MapsTo α (uIcc t₀ t) u
rw : ∀ x ∈ Ioo (min t₀ t) (max t₀ t), HasDerivWithinAt α (f x (α x)) (Ioi x) x
⊢ picard f t₀ (α t₀) α t = α t

Tactic:
rw [← add_sub_cancel (α t₀) (α t), picard_apply,
    integral_eq_sub_of_hasDeriv_right (HasDerivWithinAt.continuousOn hα) _
      (continuousOn_comp hf (HasDerivWithinAt.continuousOn hα) hmap |>.intervalIntegrable)]

Premises used: intervalIntegral.integral_eq_sub_of_hasDeriv_right, add_sub_cancel, HasDerivWithinAt.continuousOn, ContinuousOn.intervalIntegrable, ODE.continuousOn_comp, ODE.picard_apply
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ t : ℝ
hf : ContinuousOn (uncurry f) (uIcc t₀ t ×ˢ u)
hα : ∀ t' ∈ uIcc t₀ t, HasDerivWithinAt α (f t' (α t')) (uIcc t₀ t) t'
hmap : MapsTo α (uIcc t₀ t) u
t' : ℝ
ht' : t' ∈ Ioo (min t₀ t) (max t₀ t)
h : HasDerivAt α (f t' (α t')) t'
⊢ HasDerivWithinAt α (f t' (α t')) (Ioi t') t'

Tactic:
apply HasDerivAt.hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ t : ℝ
hf : ContinuousOn (uncurry f) (uIcc t₀ t ×ˢ u)
hα : ∀ t' ∈ uIcc t₀ t, HasDerivWithinAt α (f t' (α t')) (uIcc t₀ t) t'
hmap : MapsTo α (uIcc t₀ t) u
t' : ℝ
ht' : t' ∈ Ioo (min t₀ t) (max t₀ t)
⊢ HasDerivAt α (f t' (α t')) t'

Tactic:
hα t' (Ioo_subset_Icc_self ht') |>.hasDerivAt <| Icc_mem_nhds ht'.1 ht'.2

Premises used: Set.Ioo_subset_Icc_self, And.right, And.left, HasDerivWithinAt.hasDerivAt, Icc_mem_nhds
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ t : ℝ
hf : ContinuousOn (uncurry f) (uIcc t₀ t ×ˢ u)
hα : ∀ t' ∈ uIcc t₀ t, HasDerivWithinAt α (f t' (α t')) (uIcc t₀ t) t'
hmap : MapsTo α (uIcc t₀ t) u
t' : ℝ
ht' : t' ∈ Ioo (min t₀ t) (max t₀ t)
⊢ HasDerivAt α (f t' (α t')) t'

Tactic:
exact hα t' (Ioo_subset_Icc_self ht') |>.hasDerivAt <| Icc_mem_nhds ht'.1 ht'.2

Premises used: Set.Ioo_subset_Icc_self, And.right, And.left, HasDerivWithinAt.hasDerivAt, Icc_mem_nhds
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
n : ℕ
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
pos : ∀ (hlt : tmin < tmax), ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
neg : ∀ (hlt : ¬tmin < tmax), ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)

Tactic:
by_cases hlt : tmin < tmax
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
n : ℕ
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : tmin < tmax
⊢ ∀ (t : ℝ) (ht : t ∈ Icc tmin tmax), HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t

Tactic:
have (t) (ht : t ∈ Icc tmin tmax) :=
      hasDerivWithinAt_picard_Icc ht₀ hf.continuousOn hα hmem x₀ ht
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : tmin < tmax
this : ∀ (t : ℝ) (ht : t ∈ Icc tmin tmax), HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
hf : ContDiffOn ℝ (↑0 : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
pos : ∀ (hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)), ContinuousOn (picard f t₀ x₀ α) (Icc tmin tmax)
⊢ ContDiffOn ℝ (↑0 : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)

Tactic:
simp only [Nat.cast_zero, contDiffOn_zero] at *

Premises used: contDiffOn_zero, Nat.cast_zero
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : tmin < tmax
this : ∀ (t : ℝ) (ht : t ∈ Icc tmin tmax), HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)
⊢ ContinuousOn (picard f t₀ x₀ α) (Icc tmin tmax)

Tactic:
HasDerivWithinAt.continuousOn this

Premises used: HasDerivWithinAt.continuousOn
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : tmin < tmax
this : ∀ (t : ℝ) (ht : t ∈ Icc tmin tmax), HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)
⊢ ContinuousOn (picard f t₀ x₀ α) (Icc tmin tmax)

Tactic:
exact HasDerivWithinAt.continuousOn this

Premises used: HasDerivWithinAt.continuousOn
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : tmin < tmax
this : ∀ (t : ℝ) (ht : t ∈ Icc tmin tmax), HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
n : ℕ
hn :
  ∀ (hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)),
    ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
⊢ ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) (uncurry f) (Icc tmin tmax ×ˢ u)

Tactic:
simp only [Nat.cast_add, Nat.cast_one] at *

Premises used: Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : tmin < tmax
this : ∀ (t : ℝ) (ht : t ∈ Icc tmin tmax), HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
n : ℕ
hn :
  ∀ (hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)),
    ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) (uncurry f) (Icc tmin tmax ×ˢ u)
pos :
  DifferentiableOn ℝ (picard f t₀ x₀ α) (Icc tmin tmax) ∧
    (Eq (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) ⊤ → AnalyticOn ℝ (picard f t₀ x₀ α) (Icc tmin tmax)) ∧
      ContDiffOn ℝ (↑n : WithTop ℕ∞) (derivWithin (picard f t₀ x₀ α) (Icc tmin tmax)) (Icc tmin tmax)
⊢ ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) (picard f t₀ x₀ α) (Icc tmin tmax)

Tactic:
rw [contDiffOn_succ_iff_derivWithin <| uniqueDiffOn_Icc hlt]

Premises used: uniqueDiffOn_Icc, contDiffOn_succ_iff_derivWithin
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : tmin < tmax
this : ∀ (t : ℝ) (ht : t ∈ Icc tmin tmax), HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
n : ℕ
hn :
  ∀ (hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)),
    ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) (uncurry f) (Icc tmin tmax ×ˢ u)
⊢ Eq (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) ⊤ → AnalyticOn ℝ (picard f t₀ x₀ α) (Icc tmin tmax)

Tactic:
simp
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : tmin < tmax
this : ∀ (t : ℝ) (ht : t ∈ Icc tmin tmax), HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
n : ℕ
hn :
  ∀ (hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)),
    ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) (uncurry f) (Icc tmin tmax ×ˢ u)
pos : ContDiffOn ℝ (↑n : WithTop ℕ∞) (derivWithin (picard f t₀ x₀ α) (Icc tmin tmax)) (Icc tmin tmax)
⊢ DifferentiableOn ℝ (picard f t₀ x₀ α) (Icc tmin tmax) ∧
    (Eq (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) ⊤ → AnalyticOn ℝ (picard f t₀ x₀ α) (Icc tmin tmax)) ∧
      ContDiffOn ℝ (↑n : WithTop ℕ∞) (derivWithin (picard f t₀ x₀ α) (Icc tmin tmax)) (Icc tmin tmax)

Tactic:
refine ⟨fun t ht ↦ HasDerivWithinAt.differentiableWithinAt (this t ht), by simp, ?_⟩
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : tmin < tmax
this : ∀ (t : ℝ) (ht : t ∈ Icc tmin tmax), HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
n : ℕ
hn :
  ∀ (hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)),
    ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) (uncurry f) (Icc tmin tmax ×ˢ u)
pos : ∀ x ∈ Icc tmin tmax, derivWithin (picard f t₀ x₀ α) (Icc tmin tmax) x = f x (α x)
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) (derivWithin (picard f t₀ x₀ α) (Icc tmin tmax)) (Icc tmin tmax)

Tactic:
apply contDiffOn_comp hf.of_succ (ContDiffOn.congr (hn hf.of_succ) heqon) hmem |>.congr

Premises used: ContDiffOn.congr, ODE.contDiffOn_comp, ContDiffOn.of_succ
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : tmin < tmax
this : ∀ (t : ℝ) (ht : t ∈ Icc tmin tmax), HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
n : ℕ
hn :
  ∀ (hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)),
    ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) (uncurry f) (Icc tmin tmax ×ˢ u)
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ derivWithin (picard f t₀ x₀ α) (Icc tmin tmax) t = f t (α t)

Tactic:
HasDerivWithinAt.derivWithin (this t ht) <| (uniqueDiffOn_Icc hlt).uniqueDiffWithinAt ht

Premises used: uniqueDiffOn_Icc, UniqueDiffOn.uniqueDiffWithinAt, HasDerivWithinAt.derivWithin