awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact HasDerivWithinAt.derivWithin (this t ht) <| (uniqueDiffOn_Icc hlt).uniqueDiffWithinAt ht

Premises used: uniqueDiffOn_Icc, UniqueDiffOn.uniqueDiffWithinAt, HasDerivWithinAt.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
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)
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)
⊢ ContDiffOn ℝ (↑n : 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

Premises used: uniqueDiffOn_Icc, contDiffOn_zero, Nat.cast_add, contDiffOn_succ_iff_derivWithin, Nat.cast_zero, HasDerivWithinAt.continuousOn, 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
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
neg : ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) {t₀}
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)

Tactic:
rw [(subsingleton_Icc_of_ge (not_lt.mp hlt)).eq_singleton_of_mem ht₀]

Premises used: Set.Subsingleton.eq_singleton_of_mem, not_lt, Iff.mp, Set.subsingleton_Icc_of_ge
-- 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 : Membership.mem (γ := Set ℝ) {t₀} t
neg : ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) {t₀} t₀
⊢ ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) {t₀} t

Tactic:
rw [eq_of_mem_singleton ht]

Premises used: Set.eq_of_mem_singleton
-- 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 : Membership.mem (γ := Set ℝ) {t₀} t
⊢ ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) {t₀} t₀

Tactic:
contDiffWithinAt_singleton

Premises used: contDiffWithinAt_singleton
-- 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 : Membership.mem (γ := Set ℝ) {t₀} t
⊢ ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) {t₀} t₀

Tactic:
exact contDiffWithinAt_singleton

Premises used: contDiffWithinAt_singleton
-- 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
hf : ContDiffOn ℝ (↑⊤ : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
top :
  ∀ (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)) (n : ℕ),
    ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
⊢ ContDiffOn ℝ (↑⊤ : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)

Tactic:
rw [contDiffOn_infty] at *

Premises used: contDiffOn_infty
-- 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
hf : ∀ (n : ℕ), ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
⊢ ∀ (n : ℕ), ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)

Tactic:
fun k ↦ contDiffOn_nat_picard_Icc ht₀ (hf k) hα hmem x₀ heqon

Premises used: ODE.contDiffOn_nat_picard_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
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 : ∀ (n : ℕ), ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
⊢ ∀ (n : ℕ), ContDiffOn ℝ (↑n : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)

Tactic:
exact fun k ↦ contDiffOn_nat_picard_Icc ht₀ (hf k) hα hmem x₀ heqon

Premises used: ODE.contDiffOn_nat_picard_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
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
n : ℕ
hf : ContDiffOn ℝ (↑(↑n : ℕ∞) : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
⊢ ContDiffOn ℝ (↑(↑n : ℕ∞) : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)

Tactic:
contDiffOn_nat_picard_Icc ht₀ hf hα hmem x₀ heqon

Premises used: ODE.contDiffOn_nat_picard_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
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
n : ℕ
hf : ContDiffOn ℝ (↑(↑n : ℕ∞) : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
⊢ ContDiffOn ℝ (↑(↑n : ℕ∞) : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)

Tactic:
exact contDiffOn_nat_picard_Icc ht₀ hf hα hmem x₀ heqon

Premises used: ODE.contDiffOn_nat_picard_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
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)
coe :
  ∀ (n : ℕ) (hf : ContDiffOn ℝ (↑(↑n : ℕ∞) : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)),
    ContDiffOn ℝ (↑(↑n : ℕ∞) : WithTop ℕ∞) (picard f t₀ x₀ α) (Icc tmin tmax)
⊢ 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

Premises used: contDiffOn_infty, ODE.contDiffOn_nat_picard_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
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)
neg : ∀ (hlt : ¬tmin < tmax), ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) α (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
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
⊢ let t₀ := (tmin + tmax) / 2;
  t₀ = (tmin + tmax) / 2

Tactic:
set t₀ := (tmin + tmax) / 2 with h

Premises used: HAdd.hAdd
-- 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
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
linarith₃ : t₀ < tmin → tmin - tmax + -(2 * t₀ - (1 * tmin + 1 * tmax)) + 2 * (t₀ - tmin) = 0
linarith₄ : t₀ < tmin → GT.gt (α := ℝ) 2 0
⊢ tmin ≤ t₀

Tactic:
linarith
-- 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
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 : tmax < t₀ → 2 / 2 = 1
linarith₁ : tmax < t₀ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : tmax < t₀ → GT.gt (α := ℝ) 2 0
linarith₃ : tmax < t₀ → tmin - tmax + (2 * t₀ - (1 * tmin + 1 * tmax)) + 2 * (tmax - t₀) = 0
linarith₄ : tmax < t₀ → GT.gt (α := ℝ) 2 0
⊢ t₀ ≤ tmax

Tactic:
linarith
-- 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
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
⊢ t₀ ∈ Icc tmin tmax

Tactic:
have ht₀ : t₀ ∈ Icc tmin tmax := ⟨by linarith, by linarith⟩
-- 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
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
ht₀ : t₀ ∈ Icc tmin tmax
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ uIcc t₀ t ⊆ Icc tmin tmax

Tactic:
have : uIcc t₀ t ⊆ Icc tmin tmax := uIcc_subset_Icc ht₀ 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
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
ht₀ : t₀ ∈ Icc tmin tmax
t : ℝ
ht : t ∈ Icc tmin tmax
this : uIcc t₀ t ⊆ Icc tmin tmax
rw rw₁ : α t = α t
⊢ α t = picard f t₀ (α t₀) α t

Tactic:
rw [picard_eq_of_hasDerivAt (hf.continuousOn.mono (prod_subset_prod_left this))
        (fun t' ht' ↦ hα t' (this ht') |>.mono this) (hmem.mono_left this)]

Premises used: Set.MapsTo.mono_left, Set.prod_subset_prod_left, HasDerivWithinAt.mono, ContDiffOn.continuousOn, ContinuousOn.mono, ODE.picard_eq_of_hasDerivAt
-- 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
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
ht₀ : t₀ ∈ Icc tmin tmax
⊢ ∀ t ∈ Icc tmin tmax, α t = picard f t₀ (α t₀) α t

Tactic:
have : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ (α t₀) α t := by
      intro t ht
      have : uIcc t₀ t ⊆ Icc tmin tmax := uIcc_subset_Icc ht₀ ht
      rw [picard_eq_of_hasDerivAt (hf.continuousOn.mono (prod_subset_prod_left this))
        (fun t' ht' ↦ hα t' (this ht') |>.mono this) (hmem.mono_left this)]
-- 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
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
ht₀ : t₀ ∈ Icc tmin tmax
this : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ (α t₀) α t
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)

Tactic:
contDiffOn_enat_picard_Icc ht₀ hf (HasDerivWithinAt.continuousOn hα) hmem (α t₀) this
      |>.congr this

Premises used: ContDiffOn.congr, ODE.contDiffOn_enat_picard_Icc, 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
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
ht₀ : t₀ ∈ Icc tmin tmax
this : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ (α t₀) α t
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)

Tactic:
exact contDiffOn_enat_picard_Icc ht₀ hf (HasDerivWithinAt.continuousOn hα) hmem (α t₀) this
      |>.congr this

Premises used: ContDiffOn.congr, ODE.contDiffOn_enat_picard_Icc, 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
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
⊢ tmax < tmin ∨ tmax = tmin

Tactic:
rw [not_lt, le_iff_lt_or_eq] at hlt

Premises used: le_iff_lt_or_eq, not_lt
-- 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
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
h : tmax < tmin
x : ℝ
ht : x ∈ Icc tmin tmax
⊢ Membership.mem (γ := Set ℝ) ∅ x

Tactic:
rw [Icc_eq_empty (not_le.mpr h)] at ht

Premises used: not_le, Iff.mpr, Set.Icc_eq_empty
-- 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
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
h : tmax < tmin
x : ℝ
ht : Membership.mem (γ := Set ℝ) ∅ x
neg : False
⊢ ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax) x

Tactic:
exfalso
-- 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
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
h : tmax < tmin
x : ℝ
ht : Membership.mem (γ := Set ℝ) ∅ x
⊢ False

Tactic:
notMem_empty _ ht

Premises used: Set.notMem_empty
-- 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
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
h : tmax < tmin
x : ℝ
ht : Membership.mem (γ := Set ℝ) ∅ x
⊢ False

Tactic:
exact notMem_empty _ ht

Premises used: Set.notMem_empty
-- 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
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
h : tmax = tmin
neg : ContDiffOn ℝ (↑n : WithTop ℕ∞) α {tmin}
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)

Tactic:
rw [h, Icc_self]

Premises used: Set.Icc_self
-- 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
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
h : tmax = tmin
x : ℝ
ht : Membership.mem (γ := Set ℝ) {tmin} x
neg : ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) α {tmin} tmin
⊢ ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) α {tmin} x

Tactic:
rw [eq_of_mem_singleton ht]

Premises used: Set.eq_of_mem_singleton
-- 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
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
h : tmax = tmin
x : ℝ
ht : Membership.mem (γ := Set ℝ) {tmin} x
⊢ ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) α {tmin} tmin

Tactic:
contDiffWithinAt_singleton

Premises used: contDiffWithinAt_singleton
-- 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
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
h : tmax = tmin
x : ℝ
ht : Membership.mem (γ := Set ℝ) {tmin} x
⊢ ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) α {tmin} tmin

Tactic:
exact contDiffWithinAt_singleton

Premises used: contDiffWithinAt_singleton
-- 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
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 : tmax < tmin ∨ tmax = tmin
neg : ∀ (h : tmax < tmin), ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
neg₁ : ∀ (h : tmax = tmin), ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)

Tactic:
cases hlt with
    | inl h =>
      intro _ ht
      rw [Icc_eq_empty (not_le.mpr h)] at ht
      exfalso
      exact notMem_empty _ ht
    | inr h =>
      rw [h, Icc_self]
      intro _ ht
      rw [eq_of_mem_singleton ht]
      exact contDiffWithinAt_singleton

Premises used: Set.Icc_self, contDiffWithinAt_singleton
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
⊢ ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ closedBall x₀ (↑a : ℝ))

Tactic:
continuousOn_prod_of_continuousOn_lipschitzOnWith' _ K hf.lipschitzOnWith hf.continuousOn

Premises used: IsPicardLindelof.continuousOn, IsPicardLindelof.lipschitzOnWith, continuousOn_prod_of_continuousOn_lipschitzOnWith'
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
tmin tmax tmin' tmax' : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
t₀' : (↑(Icc tmin' tmax') : Type)
ht₀ : (↑t₀ : ℝ) = (↑t₀' : ℝ)
htmin : tmin ≤ tmin'
htmax : tmax' ≤ tmax
apply : (↑L : ℝ) * max (tmax' - (↑t₀' : ℝ)) ((↑t₀' : ℝ) - tmin') ≤ (↑a : ℝ) - (↑r : ℝ)
⊢ IsPicardLindelof f t₀' x₀ a r L K

Tactic:
apply hf.shrink t₀' htmin htmax le_rfl

Premises used: le_rfl, IsPicardLindelof.shrink