-- Mathlib/Analysis/ODE/PicardLindelof.lean
theorem range_toContinuousMap :
    range toContinuousMap =
      {f : C(Icc v.tMin v.tMax, E) | f v.t₀ = v.x₀ ∧ LipschitzWith v.C f}

Proof state:
case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ {f | f v.t₀ = v.x₀ ∧ LipschitzWith v.C ⇑f} → f ∈ range ⇑toContinuousMap

Tactic:
rcases f with ⟨f, hf⟩

Result:
case h.mpr.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : ↑(Icc v.tMin v.tMax) → E
hf : Continuous f
⊢ { toFun := f, continuous_toFun := hf } ∈ {f | f v.t₀ = v.x₀ ∧ LipschitzWith v.C ⇑f} →
    { toFun := f, continuous_toFun := hf } ∈ range ⇑toContinuousMap

Proof state:
case h.mpr.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : ↑(Icc v.tMin v.tMax) → E
hf : Continuous f
⊢ { toFun := f, continuous_toFun := hf } ∈ {f | f v.t₀ = v.x₀ ∧ LipschitzWith v.C ⇑f} →
    { toFun := f, continuous_toFun := hf } ∈ range ⇑toContinuousMap

Tactic:
rintro ⟨hf₀, hf_lip⟩

Result:
case h.mpr.mk.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : ↑(Icc v.tMin v.tMax) → E
hf : Continuous f
hf₀ : { toFun := f, continuous_toFun := hf } v.t₀ = v.x₀
hf_lip : LipschitzWith v.C ⇑{ toFun := f, continuous_toFun := hf }
⊢ { toFun := f, continuous_toFun := hf } ∈ range ⇑toContinuousMap

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
⊢ range ⇑toContinuousMap = {f | f v.t₀ = v.x₀ ∧ LipschitzWith v.C ⇑f}

Tactic:
ext f

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ range ⇑toContinuousMap ↔ f ∈ {f | f v.t₀ = v.x₀ ∧ LipschitzWith v.C ⇑f}

Proof state:
case h.mp
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ range ⇑toContinuousMap → f ∈ {f | f v.t₀ = v.x₀ ∧ LipschitzWith v.C ⇑f}

Tactic:
rintro ⟨⟨f, hf₀, hf_lip⟩, rfl⟩

Result:
case h.mp.intro.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : ↑(Icc v.tMin v.tMax) → E
hf₀ : f v.t₀ = v.x₀
hf_lip : LipschitzWith v.C f
⊢ toContinuousMap { toFun := f, map_t₀' := hf₀, lipschitz' := hf_lip } ∈ {f | f v.t₀ = v.x₀ ∧ LipschitzWith v.C ⇑f}

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ range ⇑toContinuousMap ↔ f ∈ {f | f v.t₀ = v.x₀ ∧ LipschitzWith v.C ⇑f}

Tactic:
constructor

Result:
case h.mp
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ range ⇑toContinuousMap → f ∈ {f | f v.t₀ = v.x₀ ∧ LipschitzWith v.C ⇑f}

case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ {f | f v.t₀ = v.x₀ ∧ LipschitzWith v.C ⇑f} → f ∈ range ⇑toContinuousMap

Proof state:
case h.mp.intro.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : ↑(Icc v.tMin v.tMax) → E
hf₀ : f v.t₀ = v.x₀
hf_lip : LipschitzWith v.C f
⊢ toContinuousMap { toFun := f, map_t₀' := hf₀, lipschitz' := hf_lip } ∈ {f | f v.t₀ = v.x₀ ∧ LipschitzWith v.C ⇑f}

Tactic:
exact ⟨hf₀, hf_lip⟩

Result:
no goals

Proof state:
case h.mpr.mk.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : ↑(Icc v.tMin v.tMax) → E
hf : Continuous f
hf₀ : { toFun := f, continuous_toFun := hf } v.t₀ = v.x₀
hf_lip : LipschitzWith v.C ⇑{ toFun := f, continuous_toFun := hf }
⊢ { toFun := f, continuous_toFun := hf } ∈ range ⇑toContinuousMap

Tactic:
exact ⟨⟨f, hf₀, hf_lip⟩, rfl⟩

Result:
no goals