-- Mathlib/Analysis/Calculus/FDeriv/Norm.lean
theorem ContDiffAt.contDiffAt_norm_of_smul (h : ContDiffAt ℝ n (‖·‖) (t • x)) :
    ContDiffAt ℝ n (‖·‖) x

Proof state:
case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : 1 ≤ n
h : ContDiffAt ℝ n (fun x => ‖x‖) (0 • x)
⊢ ContDiffAt ℝ n (fun x => ‖x‖) x

Tactic:
by_cases hE : Nontrivial E

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : 1 ≤ n
h : ContDiffAt ℝ n (fun x => ‖x‖) (0 • x)
hE : Nontrivial E
⊢ ContDiffAt ℝ n (fun x => ‖x‖) x

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : 1 ≤ n
h : ContDiffAt ℝ n (fun x => ‖x‖) (0 • x)
hE : ¬Nontrivial E
⊢ ContDiffAt ℝ n (fun x => ‖x‖) x

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
h : ContDiffAt ℝ n (fun x => ‖x‖) (t • x)
hn : 1 ≤ n
⊢ ContDiffAt ℝ n (fun x => ‖x‖) x

Tactic:
obtain rfl | ht := eq_or_ne t 0

Result:
case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : 1 ≤ n
h : ContDiffAt ℝ n (fun x => ‖x‖) (0 • x)
⊢ ContDiffAt ℝ n (fun x => ‖x‖) x

case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
h : ContDiffAt ℝ n (fun x => ‖x‖) (t • x)
hn : 1 ≤ n
ht : t ≠ 0
⊢ ContDiffAt ℝ n (fun x => ‖x‖) x

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h : ContDiffAt ℝ ⊥ (fun x => ‖x‖) (t • x)
⊢ ContDiffAt ℝ ⊥ (fun x => ‖x‖) x

Tactic:
apply contDiffAt_zero.2

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h : ContDiffAt ℝ ⊥ (fun x => ‖x‖) (t • x)
⊢ ∃ u ∈ nhds x, ContinuousOn (fun x => ‖x‖) u

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
h : ContDiffAt ℝ n (fun x => ‖x‖) (t • x)
hn : ⊥ < n
⊢ ContDiffAt ℝ n (fun x => ‖x‖) x

Tactic:
replace hn : 1 ≤ n := ENat.add_one_natCast_le_withTop_of_lt hn

Result:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
h : ContDiffAt ℝ n (fun x => ‖x‖) (t • x)
hn : 1 ≤ n
⊢ ContDiffAt ℝ n (fun x => ‖x‖) x

Proof state:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : 1 ≤ n
h : ContDiffAt ℝ n (fun x => ‖x‖) (0 • x)
hE : Subsingleton E
⊢ ContDiffAt ℝ n (Function.const E ‖0‖) x

Tactic:
exact contDiffAt_const

Result:
no goals

Proof state:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : 1 ≤ n
h : ContDiffAt ℝ n (fun x => ‖x‖) (0 • x)
hE : ¬Nontrivial E
⊢ ContDiffAt ℝ n (fun x => ‖x‖) x

Tactic:
rw [not_nontrivial_iff_subsingleton] at hE

Result:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : 1 ≤ n
h : ContDiffAt ℝ n (fun x => ‖x‖) (0 • x)
hE : Subsingleton E
⊢ ContDiffAt ℝ n (fun x => ‖x‖) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
h : ContDiffAt ℝ n (fun x => ‖x‖) (t • x)
⊢ ContDiffAt ℝ n (fun x => ‖x‖) x

Tactic:
rcases eq_bot_or_bot_lt n with rfl | hn

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h : ContDiffAt ℝ ⊥ (fun x => ‖x‖) (t • x)
⊢ ContDiffAt ℝ ⊥ (fun x => ‖x‖) x

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
h : ContDiffAt ℝ n (fun x => ‖x‖) (t • x)
hn : ⊥ < n
⊢ ContDiffAt ℝ n (fun x => ‖x‖) x

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : 1 ≤ n
h : ContDiffAt ℝ n (fun x => ‖x‖) (0 • x)
hE : Nontrivial E
⊢ ContDiffAt ℝ n (fun x => ‖x‖) x

Tactic:
rw [zero_smul] at h

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : 1 ≤ n
h : ContDiffAt ℝ n (fun x => ‖x‖) 0
hE : Nontrivial E
⊢ ContDiffAt ℝ n (fun x => ‖x‖) x

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h : ContDiffAt ℝ ⊥ (fun x => ‖x‖) (t • x)
⊢ ∃ u ∈ nhds x, ContinuousOn (fun x => ‖x‖) u

Tactic:
exact ⟨univ, univ_mem, continuous_norm.continuousOn⟩

Result:
no goals

Proof state:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
h : ContDiffAt ℝ n (fun x => ‖x‖) (t • x)
hn : 1 ≤ n
ht : t ≠ 0
⊢ ContDiffAt ℝ n (fun x => ‖x‖) x

Tactic:
exact contDiffAt_norm_smul_iff ht |>.2 h

Result:
no goals