awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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 : ℕ) ↦ ∑ i ∈ Finset.range x, (↑C : ℝ) ^ i) Filter.atTop (𝓝 (↑(1 - C)⁻¹ : ℝ))
have h₁ : (↑(1 - C)⁻¹ : ℝ) = (1 - (↑C : ℝ))⁻¹
Tactic: convert! hasSum_geometric_of_lt_one C.2 (h y hy).1 |>.tendsto_sum_nat
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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
⊢ HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
have a : HasDerivWithinAt (fun (x : ℝ) ↦ ∫ (τ : ℝ) in t₀..x, f τ (α τ)) (f t (α t)) (Icc tmin tmax) t
Tactic: apply HasDerivWithinAt.const_add
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
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
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ ∫ (τ : ℝ) in t₀..x, f τ (α τ)) (f t (α t)) (Icc tmin tmax) t
have this : Fact (t ∈ Icc tmin tmax)
Tactic: have : Fact (t ∈ Icc tmin tmax) := ⟨ht⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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)
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ ∫ (τ : ℝ) in t₀..x, f τ (α τ)) (f t (α t)) (Icc tmin tmax) t
have apply : IntervalIntegrable.{u_1} (ε := E) (fun (t : ℝ) ↦ f t (α t)) volume t₀ 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)
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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)
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (t : ℝ) ↦ f t (α t)) volume t₀ t
have hu : ContinuousOn.{0, u_1} (Y := E) (fun (t : ℝ) ↦ f t (α t)) (uIcc t₀ t)
Tactic: apply ContinuousOn.intervalIntegrable
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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)
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (t : ℝ) ↦ f t (α t)) (uIcc t₀ t)
have hu : uIcc t₀ t ⊆ Icc tmin tmax
Tactic: apply continuousOn_comp hf hα hmem |>.mono
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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
⊢ picard f t₀ (α t₀) α t = α t
have rw : ∀ x ∈ Ioo (min t₀ t) (max t₀ t), HasDerivWithinAt α (f x (α x)) (Ioi x) x
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)]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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)
⊢ HasDerivWithinAt α (f t' (α t')) (Ioi t') t'
have h : HasDerivAt α (f t' (α t')) t'
Tactic: apply HasDerivAt.hasDerivWithinAt
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
have pos : ∀ (hlt : tmin < tmax), ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
Tactic: by_cases hlt : tmin < tmax
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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)
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
have neg : ∀ (hlt : ¬tmin < tmax), ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
Tactic: by_cases hlt : tmin < tmax
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
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
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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)
⊢ ContDiffOn ℝ (↑0 : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
have pos : ∀ (hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)), ContinuousOn (picard f t₀ x₀ α) (Icc tmin tmax)
Tactic: simp only [Nat.cast_zero, contDiffOn_zero] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
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 ℝ (↑(n + 1) : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
have hf₁ : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) (uncurry f) (Icc tmin tmax ×ˢ u)
Tactic: simp only [Nat.cast_add, Nat.cast_one] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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)
⊢ ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) (picard f t₀ x₀ α) (Icc tmin tmax)
have 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)
Tactic: rw [contDiffOn_succ_iff_derivWithin <| uniqueDiffOn_Icc hlt]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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)
⊢ 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)
have pos : 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, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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)
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) (derivWithin (picard f t₀ x₀ α) (Icc tmin tmax)) (Icc tmin tmax)
have pos : ∀ x ∈ Icc tmin tmax, derivWithin (picard f t₀ x₀ α) (Icc tmin tmax) x = f x (α x)
Tactic: apply contDiffOn_comp hf.of_succ (ContDiffOn.congr (hn hf.of_succ) heqon) hmem |>.congr
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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
this : ∀ (t : ℝ) (ht : t ∈ Icc tmin tmax), HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
have pos : ∀ (hf : ContDiffOn ℝ (↑0 : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)),
  ContDiffOn ℝ (↑0 : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
Tactic: induction n with
    | zero =>
      simp only [Nat.cast_zero, contDiffOn_zero] at *
      exact HasDerivWithinAt.continuousOn this
    | succ n hn =>
      simp only [Nat.cast_add, Nat.cast_one] at *
      rw [contDiffOn_succ_iff_derivWithin <| uniqueDiffOn_Icc hlt]
      refine ⟨fun t ht ↦ HasDerivWithinAt.differentiableWithinAt (this t ht), by simp, ?_⟩
      apply contDiffOn_comp hf.of_succ (ContDiffOn.congr (hn hf.of_succ) heqon) hmem |>.congr
      intro t ht
      exact HasDerivWithinAt.derivWithin (this t ht) <| (uniqueDiffOn_Icc hlt).uniqueDiffWithinAt ht
Cleared hypotheses: n, hf
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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
this : ∀ (t : ℝ) (ht : t ∈ Icc tmin tmax), HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
pos :
  ∀ (hf : ContDiffOn ℝ (↑0 : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)),
    ContDiffOn ℝ (↑0 : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
have pos₁ : ∀ (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 ℝ (↑(n + 1) : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
Tactic: induction n with
    | zero =>
      simp only [Nat.cast_zero, contDiffOn_zero] at *
      exact HasDerivWithinAt.continuousOn this
    | succ n hn =>
      simp only [Nat.cast_add, Nat.cast_one] at *
      rw [contDiffOn_succ_iff_derivWithin <| uniqueDiffOn_Icc hlt]
      refine ⟨fun t ht ↦ HasDerivWithinAt.differentiableWithinAt (this t ht), by simp, ?_⟩
      apply contDiffOn_comp hf.of_succ (ContDiffOn.congr (hn hf.of_succ) heqon) hmem |>.congr
      intro t ht
      exact HasDerivWithinAt.derivWithin (this t ht) <| (uniqueDiffOn_Icc hlt).uniqueDiffWithinAt ht
Cleared hypotheses: n, hf
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
have neg : ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) {t₀}
Tactic: rw [(subsingleton_Icc_of_ge (not_lt.mp hlt)).eq_singleton_of_mem ht₀]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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 : Membership.mem (γ := Set ℝ) {t₀} t
⊢ ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) {t₀} t
have neg : ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) {t₀} t₀
Tactic: rw [eq_of_mem_singleton ht]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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
hf : ContDiffOn ℝ (↑⊤ : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
⊢ ContDiffOn ℝ (↑⊤ : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
have top : ∀ (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)) (n : ℕ),
  ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
Tactic: rw [contDiffOn_infty] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
have top : ∀ (hf : ContDiffOn ℝ (↑⊤ : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)),
  ContDiffOn ℝ (↑⊤ : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
Tactic: induction n with
  | top =>
    rw [contDiffOn_infty] at *
    exact fun k ↦ contDiffOn_nat_picard_Icc ht₀ (hf k) hα hmem x₀ heqon
  | coe n => exact contDiffOn_nat_picard_Icc ht₀ hf hα hmem x₀ heqon
Cleared hypotheses: n, hf
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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
top :
  ∀ (hf : ContDiffOn ℝ (↑⊤ : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)),
    ContDiffOn ℝ (↑⊤ : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
have coe : ∀ (n : ℕ) (hf : ContDiffOn ℝ (↑(↑n : ℕ∞) : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)),
  ContDiffOn ℝ (↑(↑n : ℕ∞) : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
Tactic: induction n with
  | top =>
    rw [contDiffOn_infty] at *
    exact fun k ↦ contDiffOn_nat_picard_Icc ht₀ (hf k) hα hmem x₀ heqon
  | coe n => exact contDiffOn_nat_picard_Icc ht₀ hf hα hmem x₀ heqon
Cleared hypotheses: n, hf
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
have pos : ∀ (hlt : tmin < tmax), ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
Tactic: by_cases hlt : tmin < tmax
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
pos : ∀ (hlt : tmin < tmax), ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
have neg : ∀ (hlt : ¬tmin < tmax), ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
Tactic: by_cases hlt : tmin < tmax
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
hlt : tmin < tmax
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
have h : let t₀ := (tmin + tmax) / 2;
t₀ = (tmin + tmax) / 2
Tactic: set t₀ := (tmin + tmax) / 2 with h
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
hlt : tmin < tmax
t₀ : ℝ := (tmin + tmax) / 2
h : t₀ = (tmin + tmax) / 2
⊢ tmin ≤ t₀
have linarith : t₀ < tmin → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
hlt : tmin < tmax
t₀ : ℝ := (tmin + tmax) / 2
h : t₀ = (tmin + tmax) / 2
linarith : t₀ < tmin → 2 / 2 = 1
⊢ tmin ≤ t₀
have linarith₁ : t₀ < tmin → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
hlt : tmin < tmax
t₀ : ℝ := (tmin + tmax) / 2
h : t₀ = (tmin + tmax) / 2
linarith : t₀ < tmin → 2 / 2 = 1
linarith₁ : t₀ < tmin → HMul.hMul (α := ℝ) 1 2 = 2
⊢ tmin ≤ t₀
have linarith₂ : t₀ < tmin → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
hlt : tmin < tmax
t₀ : ℝ := (tmin + tmax) / 2
h : t₀ = (tmin + tmax) / 2
linarith : t₀ < tmin → 2 / 2 = 1
linarith₁ : t₀ < tmin → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : t₀ < tmin → GT.gt (α := ℝ) 2 0
⊢ tmin ≤ t₀
have linarith₃ : t₀ < tmin → tmin - tmax + -(2 * t₀ - (1 * tmin + 1 * tmax)) + 2 * (t₀ - tmin) = 0
Tactic: linarith