-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
/-- A variant of `deriv_const_smul` without differentiability assumption when the scalar
multiplication is by field elements. -/
lemma deriv_const_smul' {f : 𝕜 → F} {x : 𝕜} {R : Type*} [Field R] [Module R F] [SMulCommClass 𝕜 R F]
    [ContinuousConstSMul R F] (c : R) :
    deriv (fun y ↦ c • f y) x = c • deriv f x

Proof state:
case neg.inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
R : Type u_3
inst✝³ : Field R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : ¬DifferentiableAt 𝕜 f x
hc : c ≠ 0
⊢ deriv (fun y => c • f y) x = c • deriv f x

Tactic:
have H : ¬DifferentiableAt 𝕜 (fun y ↦ c • f y) x := by
  contrapose! hf
  conv => enter [2, y]; rw [← inv_smul_smul₀ hc (f y)]
  exact DifferentiableAt.const_smul hf c⁻¹

Result:
case neg.inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
R : Type u_3
inst✝³ : Field R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : ¬DifferentiableAt 𝕜 f x
hc : c ≠ 0
H : ¬DifferentiableAt 𝕜 (fun y => c • f y) x
⊢ deriv (fun y => c • f y) x = c • deriv f x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
R : Type u_3
inst✝³ : Field R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hc : c ≠ 0
hf : DifferentiableAt 𝕜 (fun y => c • f y) x
⊢ DifferentiableAt 𝕜 f x

Tactic:
conv => enter [2, y]; rw [← inv_smul_smul₀ hc (f y)]

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
R : Type u_3
inst✝³ : Field R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hc : c ≠ 0
hf : DifferentiableAt 𝕜 (fun y => c • f y) x
⊢ DifferentiableAt 𝕜 (fun y => c⁻¹ • c • f y) x

Proof state:
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
R : Type u_3
inst✝³ : Field R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : DifferentiableAt 𝕜 f x
⊢ deriv (fun y => c • f y) x = c • deriv f x

Tactic:
exact deriv_const_smul c hf

Result:
no goals

Proof state:
case neg.inl
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
R : Type u_3
inst✝³ : Field R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
hf : ¬DifferentiableAt 𝕜 f x
⊢ deriv (fun y => 0 • f y) x = 0 • deriv f x

Tactic:
simp only [zero_smul, deriv_const']

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
R : Type u_3
inst✝³ : Field R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : ¬DifferentiableAt 𝕜 f x
hc : c ≠ 0
⊢ ¬DifferentiableAt 𝕜 (fun y => c • f y) x

Tactic:
contrapose! hf

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
R : Type u_3
inst✝³ : Field R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hc : c ≠ 0
hf : DifferentiableAt 𝕜 (fun y => c • f y) x
⊢ DifferentiableAt 𝕜 f x

Proof state:
case neg.inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
R : Type u_3
inst✝³ : Field R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : ¬DifferentiableAt 𝕜 f x
hc : c ≠ 0
H : ¬DifferentiableAt 𝕜 (fun y => c • f y) x
⊢ deriv (fun y => c • f y) x = c • deriv f x

Tactic:
rw [deriv_zero_of_not_differentiableAt hf, deriv_zero_of_not_differentiableAt H, smul_zero]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
R : Type u_3
inst✝³ : Field R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
⊢ deriv (fun y => c • f y) x = c • deriv f x

Tactic:
by_cases hf : DifferentiableAt 𝕜 f x

Result:
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
R : Type u_3
inst✝³ : Field R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : DifferentiableAt 𝕜 f x
⊢ deriv (fun y => c • f y) x = c • deriv f x

case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
R : Type u_3
inst✝³ : Field R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : ¬DifferentiableAt 𝕜 f x
⊢ deriv (fun y => c • f y) x = c • deriv f x

Proof state:
case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
R : Type u_3
inst✝³ : Field R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : ¬DifferentiableAt 𝕜 f x
⊢ deriv (fun y => c • f y) x = c • deriv f x

Tactic:
rcases eq_or_ne c 0 with rfl | hc

Result:
case neg.inl
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
R : Type u_3
inst✝³ : Field R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
hf : ¬DifferentiableAt 𝕜 f x
⊢ deriv (fun y => 0 • f y) x = 0 • deriv f x

case neg.inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
R : Type u_3
inst✝³ : Field R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : ¬DifferentiableAt 𝕜 f x
hc : c ≠ 0
⊢ deriv (fun y => c • f y) x = c • deriv f x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
R : Type u_3
inst✝³ : Field R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hc : c ≠ 0
hf : DifferentiableAt 𝕜 (fun y => c • f y) x
⊢ DifferentiableAt 𝕜 (fun y => c⁻¹ • c • f y) x

Tactic:
exact DifferentiableAt.const_smul hf c⁻¹

Result:
no goals