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
α : ℝ → E
s : Set ℝ
u : Set E
n : WithTop ℕ∞
hf : ContDiffOn ℝ n (uncurry f) (s ×ˢ u)
hα : ContDiffOn ℝ n α s
hmem : ∀ t ∈ s, α t ∈ u
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : ∀ ⦃x : ℝ⦄, x ∈ s → (fun (t : ℝ) ↦ (t, α t)) x ∈ s ×ˢ u
⊢ MapsTo (fun (t : ℝ) ↦ (t, α t)) s (s ×ˢ u)

Tactic:
tauto
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
α : ℝ → E
s : Set ℝ
u : Set E
n : WithTop ℕ∞
hf : ContDiffOn ℝ n (uncurry f) (s ×ˢ u)
hα : ContDiffOn ℝ n α s
hmem : ∀ t ∈ s, α t ∈ u
⊢ ContDiffOn.{0, 0, u_1} ℝ (F := E) n (fun (t : ℝ) ↦ f t (α t)) s

Tactic:
simpa only [← uncurry_apply_pair f] using hf.comp (by fun_prop) (by tauto)

Premises used: ContDiffOn.comp, Function.uncurry_apply_pair
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
α : ℝ → E
s : Set ℝ
u : Set E
hf : ContinuousOn (uncurry f) (s ×ˢ u)
hα : ContinuousOn α s
hmem : MapsTo α s u
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (t : ℝ) ↦ f t (α t)) s

Tactic:
contDiffOn_zero.mp <| (contDiffOn_comp (contDiffOn_zero.mpr hf) (contDiffOn_zero.mpr hα) hmem)

Premises used: Iff.mpr, contDiffOn_zero, ODE.contDiffOn_comp, Iff.mp
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
h : ∀ (t : (↑(Icc tmin tmax) : Type)), α.toFun t = β.toFun t
mk :
  ∀ (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 } = β
⊢ α = β

Tactic:
cases α
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
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 }
⊢ { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ : FunSpace t₀ x₀ r L } = β

Tactic:
cases β
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
mk : toFun = toFun_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:
simp only [mk.injEq]

Premises used: ODE.FunSpace.mk.injEq
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
mk : ∀ (t : (↑(Icc tmin tmax) : Type)), toFun t = toFun_1 t
⊢ toFun = toFun_1

Tactic:
ext t
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
t : (↑(Icc tmin tmax) : Type)
⊢ toFun t = toFun_1 t

Tactic:
h t
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
t : (↑(Icc tmin tmax) : Type)
⊢ toFun t = toFun_1 t

Tactic:
exact h t
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
r L : ℝ≥0
α : FunSpace t₀ x₀ L r
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] α.toFun

Tactic:
α.lipschitzWith.continuous

Premises used: LipschitzWith.continuous, ODE.FunSpace.lipschitzWith
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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) }) β)
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 := ⋯ : 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 } = β
⊢ α = β

Tactic:
cases α
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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) }) β)
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 := ⋯ : 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_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 }
⊢ { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ : FunSpace t₀ x₀ r L } = β

Tactic:
cases β
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a 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 :
  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_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:
simpa using h
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : (↑(Icc tmin tmax) : Type)
⊢ (((toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) α :
          C((↑(Icc tmin tmax) : Type), E)) :
        (a : (↑(Icc tmin tmax) : Type)) → E)
      t =
    α.toFun t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
L : ℝ≥0
α : FunSpace t₀ x₀ 0 L
⊢ α.toFun t₀ = x₀

Tactic:
simpa using α.mem_closedBall₀

Premises used: ODE.FunSpace.mem_closedBall₀
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
r L : ℝ≥0
⊢ IsUniformInducing (β := C((↑(Icc tmin tmax) : Type), E)) fun (α : FunSpace t₀ x₀ r L) ↦
    (toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) α

Tactic:
⟨rfl⟩

Premises used: IsUniformInducing.mk, rfl
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
r L : ℝ≥0
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)}
        α
⊢ 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)}

Tactic:
ext α
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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)}
      α
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)) α)
      α
⊢ 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
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
r L : ℝ≥0
α : (↑(Icc tmin tmax) : Type) → E
hα1 : LipschitzWith L α
hα2 : α t₀ ∈ closedBall x₀ (↑r : ℝ)
⊢ 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)}
    ((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)))
      { toFun := α, lipschitzWith := hα1, mem_closedBall₀ := hα2 })

Tactic:
⟨hα1, hα2⟩

Premises used: Set.Mem, setOf, And.intro
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
r L : ℝ≥0
α : (↑(Icc tmin tmax) : Type) → E
hα1 : LipschitzWith L α
hα2 : α t₀ ∈ closedBall x₀ (↑r : ℝ)
⊢ 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)}
    ((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)))
      { toFun := α, lipschitzWith := hα1, mem_closedBall₀ := hα2 })

Tactic:
exact ⟨hα1, hα2⟩
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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α1 : LipschitzWith (α := (↑(Icc tmin tmax) : Type)) (β := E) L (⇑α : (a : (↑(Icc tmin tmax) : Type)) → E)
hα2 : 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:
⟨⟨α, hα1, hα2⟩, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, DFunLike.coe, rfl, ODE.FunSpace.mk
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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α1 : LipschitzWith (α := (↑(Icc tmin tmax) : Type)) (β := E) L (⇑α : (a : (↑(Icc tmin tmax) : Type)) → E)
hα2 : 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:
exact ⟨⟨α, hα1, hα2⟩, rfl⟩
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
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)) α)
⊢ CompleteSpace.{u_1} (FunSpace t₀ x₀ r L)

Tactic:
rw [completeSpace_iff_isComplete_range isUniformInducing_toContinuousMap]

Premises used: ODE.FunSpace.isUniformInducing_toContinuousMap, completeSpace_iff_isComplete_range
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
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)) α)
⊢ 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:
apply IsClosed.isComplete

Premises used: IsClosed.isComplete
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
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)})
⊢ 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:
rw [range_toContinuousMap, setOf_and]

Premises used: Set.setOf_and, ODE.FunSpace.range_toContinuousMap
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
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)}
⊢ 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:
apply isClosed_setOf_lipschitzWith L |>.preimage continuous_coeFun |>.inter

Premises used: IsClosed.preimage, IsClosed.inter, continuous_coeFun, isClosed_setOf_lipschitzWith
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
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 : ℝ)}
⊢ 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:
simp_rw [mem_closedBall_iff_norm]

Premises used: mem_closedBall_iff_norm
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
⊢ Continuous (Y := ℝ) fun (a : C((↑(Icc tmin tmax) : Type), E)) ↦
    ‖HSub.hSub (α := E) ((a : (a : (↑(Icc tmin tmax) : Type)) → E) t₀ : E) x₀‖

Tactic:
fun_prop
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
⊢ Continuous (Y := ℝ) fun (a : C((↑(Icc tmin tmax) : Type), E)) ↦ (↑r : ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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) |
      ‖HSub.hSub (α := E) ((a : (a : (↑(Icc tmin tmax) : Type)) → E) t₀ : E) x₀‖ ≤ (↑r : ℝ)}

Tactic:
exact isClosed_le (by fun_prop) (by fun_prop)

Premises used: isClosed_le
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ℝ
⊢ α.compProj t = α.toFun (projIcc tmin tmax ⋯ t)

Tactic:
rfl

Premises used: ODE.FunSpace.compProj, rfl
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : (↑(Icc tmin tmax) : Type)
⊢ α.compProj (↑t : ℝ) = α.toFun t

Tactic:
simp only [compProj_apply, projIcc_val]

Premises used: Set.projIcc_val, ODE.FunSpace.compProj_apply