-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
lemma derivWithin_mul_const_field (u : 𝕜') :
    derivWithin (fun y => v y * u) s x = derivWithin v s x * u

Proof state:
case h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
x✝ : 𝕜
⊢ v x✝ = v x✝ * u * u⁻¹

Tactic:
simp [hu]

Result:
no goals

Proof state:
case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
this : v = fun x => v x * u * u⁻¹
⊢ ¬DifferentiableWithinAt 𝕜 (fun y => v y * u) s x

Tactic:
exact fun h_diff ↦ hv <| this ▸ h_diff.mul_const _

Result:
no goals

Proof state:
case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
⊢ derivWithin (fun y => v y * u) s x = derivWithin v s x * u

Tactic:
by_cases hu : u = 0

Result:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : u = 0
⊢ derivWithin (fun y => v y * u) s x = derivWithin v s x * u

case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
⊢ derivWithin (fun y => v y * u) s x = derivWithin v s x * u

Proof state:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : u = 0
⊢ derivWithin (fun y => v y * u) s x = derivWithin v s x * u

Tactic:
simp [hu]

Result:
no goals

Proof state:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : DifferentiableWithinAt 𝕜 v s x
⊢ derivWithin (fun y => v y * u) s x = derivWithin v s x * u

Tactic:
rw [derivWithin_mul_const hv u]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
⊢ v = fun x => v x * u * u⁻¹

Tactic:
ext

Result:
case h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
x✝ : 𝕜
⊢ v x✝ = v x✝ * u * u⁻¹

Proof state:
case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
⊢ derivWithin (fun y => v y * u) s x = derivWithin v s x * u

Tactic:
rw [derivWithin_zero_of_not_differentiableWithinAt hv, zero_mul,
    derivWithin_zero_of_not_differentiableWithinAt]

Result:
case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
⊢ ¬DifferentiableWithinAt 𝕜 (fun y => v y * u) s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
⊢ derivWithin (fun y => v y * u) s x = derivWithin v s x * u

Tactic:
by_cases hv : DifferentiableWithinAt 𝕜 v s x

Result:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : DifferentiableWithinAt 𝕜 v s x
⊢ derivWithin (fun y => v y * u) s x = derivWithin v s x * u

case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
⊢ derivWithin (fun y => v y * u) s x = derivWithin v s x * u

Proof state:
case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
⊢ ¬DifferentiableWithinAt 𝕜 (fun y => v y * u) s x

Tactic:
have : v = fun x ↦ (v x * u) * u⁻¹ := by ext; simp [hu]

Result:
case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
this : v = fun x => v x * u * u⁻¹
⊢ ¬DifferentiableWithinAt 𝕜 (fun y => v y * u) s x