-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
/-- If `minSmoothness 𝕜 m ≤ n` for some (finite) integer `m`, then one can
find `n' ∈ [minSmoothness 𝕜 m, n]` which is not `∞`: over `ℝ` or `ℂ`, just take `m`, and otherwise
just take `ω`. The interest of this technical lemma is that, if a function is `C^{n'}` at a point
for `n' ≠ ∞`, then it is `C^{n'}` on a neighborhood of the point (this property fails only
in `C^∞` smoothness, see `ContDiffWithinAt.contDiffOn`). -/
lemma exist_minSmoothness_le_ne_infty {n : WithTop ℕ∞} {m : ℕ} (hm : minSmoothness 𝕜 m ≤ n) :
    ∃ n', minSmoothness 𝕜 m ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
m : ℕ
hm : minSmoothness 𝕜 ↑m ≤ n
⊢ ∃ n', minSmoothness 𝕜 ↑m ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Tactic:
simp only [minSmoothness] at hm ⊢

Result:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n
⊢ ∃ n', (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Proof state:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n
h : IsRCLikeNormedField 𝕜
⊢ ∃ n', ↑m ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Tactic:
simp only [h, ↓reduceIte] at hm

Result:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
m : ℕ
h : IsRCLikeNormedField 𝕜
hm : ↑m ≤ n
⊢ ∃ n', ↑m ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
m : ℕ
h : IsRCLikeNormedField 𝕜
hm : ↑m ≤ n
⊢ ↑m ≠ ∞

Tactic:
simp

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n
h : ¬IsRCLikeNormedField 𝕜
⊢ ∃ n', ω ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Tactic:
simp only [h, ↓reduceIte, top_le_iff] at hm

Result:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
m : ℕ
h : ¬IsRCLikeNormedField 𝕜
hm : n = ω
⊢ ∃ n', ω ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Proof state:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
m : ℕ
h : IsRCLikeNormedField 𝕜
hm : ↑m ≤ n
⊢ ∃ n', ↑m ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Tactic:
exact ⟨m, le_rfl, hm, by simp⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
m : ℕ
h : ¬IsRCLikeNormedField 𝕜
hm : n = ω
⊢ ω ≠ ∞

Tactic:
simp

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
m : ℕ
h : ¬IsRCLikeNormedField 𝕜
hm : n = ω
⊢ ∃ n', ω ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Tactic:
refine ⟨ω, le_rfl, by simp [hm], by simp⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n
⊢ ∃ n', (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Tactic:
split_ifs with h

Result:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n
h : IsRCLikeNormedField 𝕜
⊢ ∃ n', ↑m ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n
h : ¬IsRCLikeNormedField 𝕜
⊢ ∃ n', ω ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
m : ℕ
h : ¬IsRCLikeNormedField 𝕜
hm : n = ω
⊢ ω ≤ n

Tactic:
simp [hm]

Result:
no goals