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
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
r L : ℝ≥0
β : FunSpace t₀ x₀ r L
toFun : (↑(Icc tmin tmax) : Type) → E
lipschitzWith : LipschitzWith L toFun
mem_closedBall₀ : toFun t₀ ∈ closedBall x₀ (↑r : ℝ)
h :
  ∀ (t : (↑(Icc tmin tmax) : Type)),
    { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ : FunSpace t₀ x₀ r L }.toFun
        t =
      β.toFun t
⊢ { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ : FunSpace t₀ x₀ r L } = β
have mk : ∀ (toFun_1 : (↑(Icc tmin tmax) : Type) → E) (lipschitzWith_1 : LipschitzWith L toFun_1)
  (mem_closedBall₀_1 : toFun_1 t₀ ∈ closedBall x₀ (↑r : ℝ))
  (h :
    ∀ (t : (↑(Icc tmin tmax) : Type)),
      { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ : FunSpace t₀ x₀ r L }.toFun
          t =
        { toFun := toFun_1, lipschitzWith := lipschitzWith_1, mem_closedBall₀ := mem_closedBall₀_1 :
              FunSpace t₀ x₀ r L }.toFun
          t),
  { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ : FunSpace t₀ x₀ r L } =
    { toFun := toFun_1, lipschitzWith := lipschitzWith_1, mem_closedBall₀ := mem_closedBall₀_1 }
Tactic: cases β
Cleared hypotheses: β, h
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
r L : ℝ≥0
toFun : (↑(Icc tmin tmax) : Type) → E
lipschitzWith : LipschitzWith L toFun
mem_closedBall₀ : toFun t₀ ∈ closedBall x₀ (↑r : ℝ)
toFun_1 : (↑(Icc tmin tmax) : Type) → E
lipschitzWith_1 : LipschitzWith L toFun_1
mem_closedBall₀_1 : toFun_1 t₀ ∈ closedBall x₀ (↑r : ℝ)
h :
  ∀ (t : (↑(Icc tmin tmax) : Type)),
    { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ : FunSpace t₀ x₀ r L }.toFun
        t =
      { toFun := toFun_1, lipschitzWith := lipschitzWith_1, mem_closedBall₀ := mem_closedBall₀_1 :
            FunSpace t₀ x₀ r L }.toFun
        t
⊢ { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ : FunSpace t₀ x₀ r L } =
    { toFun := toFun_1, lipschitzWith := lipschitzWith_1, mem_closedBall₀ := mem_closedBall₀_1 }
have mk : toFun = toFun_1
Tactic: simp only [mk.injEq]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
r L : ℝ≥0
toFun : (↑(Icc tmin tmax) : Type) → E
lipschitzWith : LipschitzWith L toFun
mem_closedBall₀ : toFun t₀ ∈ closedBall x₀ (↑r : ℝ)
toFun_1 : (↑(Icc tmin tmax) : Type) → E
lipschitzWith_1 : LipschitzWith L toFun_1
mem_closedBall₀_1 : toFun_1 t₀ ∈ closedBall x₀ (↑r : ℝ)
h :
  ∀ (t : (↑(Icc tmin tmax) : Type)),
    { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ : FunSpace t₀ x₀ r L }.toFun
        t =
      { toFun := toFun_1, lipschitzWith := lipschitzWith_1, mem_closedBall₀ := mem_closedBall₀_1 :
            FunSpace t₀ x₀ r L }.toFun
        t
⊢ toFun = toFun_1
have mk : ∀ (t : (↑(Icc tmin tmax) : Type)), toFun t = toFun_1 t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α β : FunSpace t₀ x₀ r L
h :
  Eq.{u_1 + 1} (α := C((↑(Icc tmin tmax) : Type), E))
    ((fun (α : FunSpace t₀ x₀ r L) ↦ { toFun := α.toFun, continuous_toFun := ⋯ : C((↑(Icc tmin tmax) : Type), E) }) α)
    ((fun (α : FunSpace t₀ x₀ r L) ↦ { toFun := α.toFun, continuous_toFun := ⋯ : C((↑(Icc tmin tmax) : Type), E) }) β)
⊢ α = β
have mk : ∀ (toFun : (↑(Icc tmin tmax) : Type) → E) (lipschitzWith : LipschitzWith L toFun)
  (mem_closedBall₀ : toFun t₀ ∈ closedBall x₀ (↑r : ℝ))
  (h :
    Eq.{u_1 + 1} (α := C((↑(Icc tmin tmax) : Type), E))
      ((fun (α : FunSpace t₀ x₀ r L) ↦ { toFun := α.toFun, continuous_toFun := sorry : C((↑(Icc tmin tmax) : Type), E) })
        { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ })
      ((fun (α : FunSpace t₀ x₀ r L) ↦ { toFun := α.toFun, continuous_toFun := sorry : C((↑(Icc tmin tmax) : Type), E) })
        β)),
  { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ : FunSpace t₀ x₀ r L } = β
Tactic: cases α
Cleared hypotheses: α, h
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
β : FunSpace t₀ x₀ r L
toFun : (↑(Icc tmin tmax) : Type) → E
lipschitzWith : LipschitzWith L toFun
mem_closedBall₀ : toFun t₀ ∈ closedBall x₀ (↑r : ℝ)
h :
  Eq.{u_1 + 1} (α := C((↑(Icc tmin tmax) : Type), E))
    ((fun (α : FunSpace t₀ x₀ r L) ↦ { toFun := α.toFun, continuous_toFun := ⋯ : C((↑(Icc tmin tmax) : Type), E) })
      { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ })
    ((fun (α : FunSpace t₀ x₀ r L) ↦ { toFun := α.toFun, continuous_toFun := ⋯ : C((↑(Icc tmin tmax) : Type), E) }) β)
⊢ { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ : FunSpace t₀ x₀ r L } = β
have mk : ∀ (toFun_1 : (↑(Icc tmin tmax) : Type) → E) (lipschitzWith_1 : LipschitzWith L toFun_1)
  (mem_closedBall₀_1 : toFun_1 t₀ ∈ closedBall x₀ (↑r : ℝ))
  (h :
    Eq.{u_1 + 1} (α := C((↑(Icc tmin tmax) : Type), E))
      ((fun (α : FunSpace t₀ x₀ r L) ↦ { toFun := α.toFun, continuous_toFun := sorry : C((↑(Icc tmin tmax) : Type), E) })
        { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ })
      ((fun (α : FunSpace t₀ x₀ r L) ↦ { toFun := α.toFun, continuous_toFun := sorry : C((↑(Icc tmin tmax) : Type), E) })
        { toFun := toFun_1, lipschitzWith := lipschitzWith_1, mem_closedBall₀ := mem_closedBall₀_1 })),
  { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ : FunSpace t₀ x₀ r L } =
    { toFun := toFun_1, lipschitzWith := lipschitzWith_1, mem_closedBall₀ := mem_closedBall₀_1 }
Tactic: cases β
Cleared hypotheses: β, h
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
r L : ℝ≥0
⊢ Eq.{u_1 + 1} (α := Set C((↑(Icc tmin tmax) : Type), E))
    (range fun (α : FunSpace t₀ x₀ r L) ↦
      (toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) α)
    {α : C((↑(Icc tmin tmax) : Type), E) |
      LipschitzWith (α := (↑(Icc tmin tmax) : Type)) (β := E) L (⇑α : (a : (↑(Icc tmin tmax) : Type)) → E) ∧
        Membership.mem (α := E) (closedBall x₀ (↑r : ℝ)) ((α : (a : (↑(Icc tmin tmax) : Type)) → E) t₀ : E)}
have h : ∀ (α : C((↑(Icc tmin tmax) : Type), E)),
  Membership.mem (γ := Set C((↑(Icc tmin tmax) : Type), E))
      (range fun (α : FunSpace t₀ x₀ r L) ↦
        (toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) α)
      α ↔
    Membership.mem (γ := Set C((↑(Icc tmin tmax) : Type), E))
      {α : C((↑(Icc tmin tmax) : Type), E) |
        LipschitzWith (α := (↑(Icc tmin tmax) : Type)) (β := E) L (⇑α : (a : (↑(Icc tmin tmax) : Type)) → E) ∧
          Membership.mem (α := E) (closedBall x₀ (↑r : ℝ)) ((α : (a : (↑(Icc tmin tmax) : Type)) → E) t₀ : E)}
      α
Tactic: ext α
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
r L : ℝ≥0
α : C((↑(Icc tmin tmax) : Type), E)
⊢ Membership.mem (γ := Set C((↑(Icc tmin tmax) : Type), E))
      (range fun (α : FunSpace t₀ x₀ r L) ↦
        (toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) α)
      α ↔
    Membership.mem (γ := Set C((↑(Icc tmin tmax) : Type), E))
      {α : C((↑(Icc tmin tmax) : Type), E) |
        LipschitzWith (α := (↑(Icc tmin tmax) : Type)) (β := E) L (⇑α : (a : (↑(Icc tmin tmax) : Type)) → E) ∧
          Membership.mem (α := E) (closedBall x₀ (↑r : ℝ)) ((α : (a : (↑(Icc tmin tmax) : Type)) → E) t₀ : E)}
      α
have h : Membership.mem (γ := Set C((↑(Icc tmin tmax) : Type), E))
    (range fun (α : FunSpace t₀ x₀ r L) ↦
      (toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) α)
    α →
  Membership.mem (γ := Set C((↑(Icc tmin tmax) : Type), E))
    {α : C((↑(Icc tmin tmax) : Type), E) |
      LipschitzWith (α := (↑(Icc tmin tmax) : Type)) (β := E) L (⇑α : (a : (↑(Icc tmin tmax) : Type)) → E) ∧
        Membership.mem (α := E) (closedBall x₀ (↑r : ℝ)) ((α : (a : (↑(Icc tmin tmax) : Type)) → E) t₀ : E)}
    α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
r L : ℝ≥0
α : C((↑(Icc tmin tmax) : Type), E)
h :
  Membership.mem (γ := Set C((↑(Icc tmin tmax) : Type), E))
      (range fun (α : FunSpace t₀ x₀ r L) ↦
        (toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) α)
      α →
    Membership.mem (γ := Set C((↑(Icc tmin tmax) : Type), E))
      {α : C((↑(Icc tmin tmax) : Type), E) |
        LipschitzWith (α := (↑(Icc tmin tmax) : Type)) (β := E) L (⇑α : (a : (↑(Icc tmin tmax) : Type)) → E) ∧
          Membership.mem (α := E) (closedBall x₀ (↑r : ℝ)) ((α : (a : (↑(Icc tmin tmax) : Type)) → E) t₀ : E)}
      α
⊢ Membership.mem (γ := Set C((↑(Icc tmin tmax) : Type), E))
      (range fun (α : FunSpace t₀ x₀ r L) ↦
        (toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) α)
      α ↔
    Membership.mem (γ := Set C((↑(Icc tmin tmax) : Type), E))
      {α : C((↑(Icc tmin tmax) : Type), E) |
        LipschitzWith (α := (↑(Icc tmin tmax) : Type)) (β := E) L (⇑α : (a : (↑(Icc tmin tmax) : Type)) → E) ∧
          Membership.mem (α := E) (closedBall x₀ (↑r : ℝ)) ((α : (a : (↑(Icc tmin tmax) : Type)) → E) t₀ : E)}
      α
have h₁ : Membership.mem (γ := Set C((↑(Icc tmin tmax) : Type), E))
    {α : C((↑(Icc tmin tmax) : Type), E) |
      LipschitzWith (α := (↑(Icc tmin tmax) : Type)) (β := E) L (⇑α : (a : (↑(Icc tmin tmax) : Type)) → E) ∧
        Membership.mem (α := E) (closedBall x₀ (↑r : ℝ)) ((α : (a : (↑(Icc tmin tmax) : Type)) → E) t₀ : E)}
    α →
  Membership.mem (γ := Set C((↑(Icc tmin tmax) : Type), E))
    (range fun (α : FunSpace t₀ x₀ r L) ↦
      (toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) α)
    α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
inst_1 : CompleteSpace E
⊢ CompleteSpace.{u_1} (FunSpace t₀ x₀ r L)
have rw : IsComplete.{u_1} (α := C((↑(Icc tmin tmax) : Type), E))
  (range fun (α : FunSpace t₀ x₀ r L) ↦
    (toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) α)
Tactic: rw [completeSpace_iff_isComplete_range isUniformInducing_toContinuousMap]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
inst_1 : CompleteSpace E
⊢ IsComplete.{u_1} (α := C((↑(Icc tmin tmax) : Type), E))
    (range fun (α : FunSpace t₀ x₀ r L) ↦
      (toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) α)
have h : IsClosed.{u_1} (X := C((↑(Icc tmin tmax) : Type), E))
  (range fun (α : FunSpace t₀ x₀ r L) ↦
    (toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) α)
Tactic: apply IsClosed.isComplete
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
inst_1 : CompleteSpace E
⊢ IsClosed.{u_1} (X := C((↑(Icc tmin tmax) : Type), E))
    (range fun (α : FunSpace t₀ x₀ r L) ↦
      (toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) α)
have h : IsClosed.{u_1} (X := C((↑(Icc tmin tmax) : Type), E))
  ({a : C((↑(Icc tmin tmax) : Type), E) |
      LipschitzWith (α := (↑(Icc tmin tmax) : Type)) (β := E) L (⇑a : (a : (↑(Icc tmin tmax) : Type)) → E)} ∩
    {a : C((↑(Icc tmin tmax) : Type), E) |
      Membership.mem (α := E) (closedBall x₀ (↑r : ℝ)) ((a : (a : (↑(Icc tmin tmax) : Type)) → E) t₀ : E)})
Tactic: rw [range_toContinuousMap, setOf_and]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
inst_1 : CompleteSpace E
⊢ IsClosed.{u_1} (X := C((↑(Icc tmin tmax) : Type), E))
    ({a : C((↑(Icc tmin tmax) : Type), E) |
        LipschitzWith (α := (↑(Icc tmin tmax) : Type)) (β := E) L (⇑a : (a : (↑(Icc tmin tmax) : Type)) → E)} ∩
      {a : C((↑(Icc tmin tmax) : Type), E) |
        Membership.mem (α := E) (closedBall x₀ (↑r : ℝ)) ((a : (a : (↑(Icc tmin tmax) : Type)) → E) t₀ : E)})
have h : IsClosed.{u_1} (X := C((↑(Icc tmin tmax) : Type), E))
  {a : C((↑(Icc tmin tmax) : Type), E) |
    Membership.mem (α := E) (closedBall x₀ (↑r : ℝ)) ((a : (a : (↑(Icc tmin tmax) : Type)) → E) t₀ : E)}
Tactic: apply isClosed_setOf_lipschitzWith L |>.preimage continuous_coeFun |>.inter
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
inst_1 : CompleteSpace E
⊢ IsClosed.{u_1} (X := C((↑(Icc tmin tmax) : Type), E))
    {a : C((↑(Icc tmin tmax) : Type), E) |
      Membership.mem (α := E) (closedBall x₀ (↑r : ℝ)) ((a : (a : (↑(Icc tmin tmax) : Type)) → E) t₀ : E)}
have h : IsClosed.{u_1} (X := C((↑(Icc tmin tmax) : Type), E))
  {a : C((↑(Icc tmin tmax) : Type), E) |
    ‖HSub.hSub (α := E) ((a : (a : (↑(Icc tmin tmax) : Type)) → E) t₀ : E) x₀‖ ≤ (↑r : ℝ)}
Tactic: simp_rw [mem_closedBall_iff_norm]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
r L : ℝ≥0
α : FunSpace t₀ x₀ r L
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ α.compProj t = α.toFun (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t ht)
have rw : α.toFun (projIcc tmin tmax sorry t) = α.toFun (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t ht)
Tactic: rw [compProj_apply, projIcc_of_mem]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
r L : ℝ≥0
α : FunSpace t₀ x₀ r L
t : ℝ
ht : t ∈ Icc tmin tmax
rw : α.toFun (projIcc tmin tmax ⋯ t) = α.toFun (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t ht)
⊢ α.compProj t = α.toFun (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t ht)
have rw₁ : α.toFun (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t ht) =
  α.toFun (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t ht)
Tactic: rw [compProj_apply, projIcc_of_mem]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : (↑(Icc tmin tmax) : Type)
⊢ α.toFun t ∈ closedBall x₀ (↑a : ℝ)
have rw : ‖α.toFun t - x₀‖ ≤ (↑a : ℝ)
Tactic: rw [mem_closedBall, dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : (↑(Icc tmin tmax) : Type)
⊢ ‖α.toFun t - α.toFun t₀‖ + ‖α.toFun t₀ - x₀‖ ≤ (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)| + (↑r : ℝ)
have apply : ‖α.toFun t - α.toFun t₀‖ ≤ (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|
Tactic: apply add_le_add _ <| mem_closedBall_iff_norm.mp α.mem_closedBall₀
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : (↑(Icc tmin tmax) : Type)
⊢ ‖α.toFun t - α.toFun t₀‖ ≤ (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|
have rw : dist (α.toFun t) (α.toFun t₀) ≤ (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|
Tactic: rw [← dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : (↑(Icc tmin tmax) : Type)
⊢ (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)| + (↑r : ℝ) ≤ (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) + (↑r : ℝ)
have bc : |(↑t : ℝ) - (↑t₀ : ℝ)| ≤ max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : (↑(Icc tmin tmax) : Type)
⊢ ‖α.toFun t - x₀‖ ≤ (↑a : ℝ)
have t₁ : ‖α.toFun t - α.toFun t₀‖ + ‖α.toFun t₀ - x₀‖ ≤ (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)| + (↑r : ℝ)
Tactic: calc
    ‖α t - x₀‖ ≤ ‖α t - α t₀‖ + ‖α t₀ - x₀‖ := norm_sub_le_norm_sub_add_norm_sub ..
    _ ≤ L * |t.1 - t₀.1| + r := by
      apply add_le_add _ <| mem_closedBall_iff_norm.mp α.mem_closedBall₀
      rw [← dist_eq_norm]
      exact α.lipschitzWith.dist_le_mul t t₀
    _ ≤ L * max (tmax - t₀) (t₀ - tmin) + r := by
      gcongr
      exact abs_sub_le_max_sub t.2.1 t.2.2 _
    _ ≤ a - r + r := by gcongr
    _ = a := sub_add_cancel _ _
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : (↑(Icc tmin tmax) : Type)
t₁ : ‖α.toFun t - α.toFun t₀‖ + ‖α.toFun t₀ - x₀‖ ≤ (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)| + (↑r : ℝ)
⊢ ‖α.toFun t - x₀‖ ≤ (↑a : ℝ)
have t₂ : (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)| + (↑r : ℝ) ≤ (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) + (↑r : ℝ)
Tactic: calc
    ‖α t - x₀‖ ≤ ‖α t - α t₀‖ + ‖α t₀ - x₀‖ := norm_sub_le_norm_sub_add_norm_sub ..
    _ ≤ L * |t.1 - t₀.1| + r := by
      apply add_le_add _ <| mem_closedBall_iff_norm.mp α.mem_closedBall₀
      rw [← dist_eq_norm]
      exact α.lipschitzWith.dist_le_mul t t₀
    _ ≤ L * max (tmax - t₀) (t₀ - tmin) + r := by
      gcongr
      exact abs_sub_le_max_sub t.2.1 t.2.2 _
    _ ≤ a - r + r := by gcongr
    _ = a := sub_add_cancel _ _
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : (↑(Icc tmin tmax) : Type)
t₁ : ‖α.toFun t - α.toFun t₀‖ + ‖α.toFun t₀ - x₀‖ ≤ (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)| + (↑r : ℝ)
t₂ : (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)| + (↑r : ℝ) ≤ (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) + (↑r : ℝ)
⊢ ‖α.toFun t - x₀‖ ≤ (↑a : ℝ)
have t₃ : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) + (↑r : ℝ) ≤ (↑a : ℝ) - (↑r : ℝ) + (↑r : ℝ)
Tactic: calc
    ‖α t - x₀‖ ≤ ‖α t - α t₀‖ + ‖α t₀ - x₀‖ := norm_sub_le_norm_sub_add_norm_sub ..
    _ ≤ L * |t.1 - t₀.1| + r := by
      apply add_le_add _ <| mem_closedBall_iff_norm.mp α.mem_closedBall₀
      rw [← dist_eq_norm]
      exact α.lipschitzWith.dist_le_mul t t₀
    _ ≤ L * max (tmax - t₀) (t₀ - tmin) + r := by
      gcongr
      exact abs_sub_le_max_sub t.2.1 t.2.2 _
    _ ≤ a - r + r := by gcongr
    _ = a := sub_add_cancel _ _
-- 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
hf : IsPicardLindelof f t₀ x₀ a r L K
α : FunSpace t₀ x₀ r L
t : (↑(Icc tmin tmax) : Type)
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (t' : ℝ) ↦ f t' (α.compProj t')) volume (↑t₀ : ℝ) (↑t : ℝ)
have hu : ContinuousOn.{0, u_1} (Y := E) (fun (t' : ℝ) ↦ f t' (α.compProj 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
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
α : FunSpace t₀ x₀ r L
t : (↑(Icc tmin tmax) : Type)
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (t' : ℝ) ↦ f t' (α.compProj t')) (uIcc (↑t₀ : ℝ) (↑t : ℝ))
have hu : uIcc (↑t₀ : ℝ) (↑t : ℝ) ⊆ Icc tmin tmax
Tactic: apply α.continuousOn_comp_compProj hf |>.mono
-- 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₀ 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) : Type)
⊢ dist (picard f (↑t₀ : ℝ) x α.compProj (↑t₁ : ℝ)) (picard f (↑t₀ : ℝ) x α.compProj (↑t₂ : ℝ)) ≤ (↑L : ℝ) * dist t₁ t₂
have rw : norm.{u_1} (E := E) (∫ (x : ℝ) in (↑t₂ : ℝ)..(↑t₁ : ℝ), f x (α.compProj x)) ≤ (↑L : ℝ) * |(↑t₁ : ℝ) - (↑t₂ : ℝ)|
Tactic: rw [dist_eq_norm, picard_apply, picard_apply, add_sub_add_left_eq_sub,
      integral_interval_sub_left (intervalIntegrable_comp_compProj hf _ t₁)
        (intervalIntegrable_comp_compProj hf _ t₂), Subtype.dist_eq, Real.dist_eq]
-- 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₀ 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) : Type)
⊢ norm.{u_1} (E := E) (∫ (x : ℝ) in (↑t₂ : ℝ)..(↑t₁ : ℝ), f x (α.compProj x)) ≤ (↑L : ℝ) * |(↑t₁ : ℝ) - (↑t₂ : ℝ)|
have h : ∀ x ∈ uIoc (↑t₂ : ℝ) (↑t₁ : ℝ), ‖f x (α.compProj x)‖ ≤ (↑L : ℝ)
Tactic: apply intervalIntegral.norm_integral_le_of_norm_le_const
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
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) : Type)
t : ℝ
ht : t ∈ uIoc (↑t₂ : ℝ) (↑t₁ : ℝ)
⊢ ‖f t (α.compProj t)‖ ≤ (↑L : ℝ)
have ht₁ : t ∈ Icc tmin tmax
Tactic: have ht : t ∈ Icc tmin tmax := subset_trans uIoc_subset_uIcc (uIcc_subset_Icc t₂.2 t₁.2) ht
-- 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₀ 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) : Type)), α.toFun t = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)
have mp : IsFixedPt (next hf hx) α → ∀ (t : (↑(Icc tmin tmax) : Type)), α.toFun t = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)
Tactic: constructor