Theorem: toto' (extend.lean)

State before:
f : ℝ → ℝ
a b : ℝ
n : ℕ
h : ContDiffOn ℝ (↑n) f (uIcc a b)
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (uIcc a b)
Tactic:
cases eq_or_ne a b
State after:
case inl
f : ℝ → ℝ
a b : ℝ
n : ℕ
h : ContDiffOn ℝ (↑n) f (uIcc a b)
h✝ : a = b
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (uIcc a b)

case inr
f : ℝ → ℝ
a b : ℝ
n : ℕ
h : ContDiffOn ℝ (↑n) f (uIcc a b)
h✝ : a ≠ b
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (uIcc a b)

State before:
f : ℝ → ℝ
a b : ℝ
n : ℕ
h : ContDiffOn ℝ (↑n) f (uIcc a b)
hab : a = b
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (uIcc a b)
Tactic:
case inl hab => exact ⟨λ _ => f a, by simp [hab, contDiff_const]⟩
State after:
no goals

State before:
f : ℝ → ℝ
a b : ℝ
n : ℕ
h : ContDiffOn ℝ (↑n) f (uIcc a b)
hab : a = b
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (uIcc a b)
Tactic:
exact ⟨λ _ => f a, by simp [hab, contDiff_const]⟩
State after:
no goals

State before:
f : ℝ → ℝ
a b : ℝ
n : ℕ
h : ContDiffOn ℝ (↑n) f (uIcc a b)
hab : a = b
⊢ (ContDiff ℝ ↑n fun x => f a) ∧ EqOn (fun x => f a) f (uIcc a b)
Tactic:
simp [hab, contDiff_const]
State after:
no goals

State before:
f : ℝ → ℝ
a b : ℝ
n : ℕ
h : ContDiffOn ℝ (↑n) f (uIcc a b)
hab : a ≠ b
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (uIcc a b)
Tactic:
case inr hab => exact toto (min_lt_max.2 hab) h
State after:
no goals

State before:
f : ℝ → ℝ
a b : ℝ
n : ℕ
h : ContDiffOn ℝ (↑n) f (uIcc a b)
hab : a ≠ b
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (uIcc a b)
Tactic:
exact toto (min_lt_max.2 hab) h
State after:
no goals