Theorem: last (Sard/LocallyLipschitz.lean)

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
a : ℝ
K : ℝ≥0
c : ℝ≥0∞
⊢ ↑‖a‖.toNNReal * (↑K * c) = ↑(‖a‖.toNNReal * K) * c
Tactic:
have : c ≠ ∞ := by sorry
State after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
a : ℝ
K : ℝ≥0
c : ℝ≥0∞
this : c ≠ ⊤
⊢ ↑‖a‖.toNNReal * (↑K * c) = ↑(‖a‖.toNNReal * K) * c

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
a : ℝ
K : ℝ≥0
c : ℝ≥0∞
this : c ≠ ⊤
⊢ ↑‖a‖.toNNReal * (↑K * c) = ↑(‖a‖.toNNReal * K) * c
Tactic:
lift c to ℝ≥0 using this
State after:
case intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
a : ℝ
K c : ℝ≥0
⊢ ↑‖a‖.toNNReal * (↑K * ↑c) = ↑(‖a‖.toNNReal * K) * ↑c

State before:
case intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
a : ℝ
K c : ℝ≥0
⊢ ↑‖a‖.toNNReal * (↑K * ↑c) = ↑(‖a‖.toNNReal * K) * ↑c
Tactic:
sorry
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
a : ℝ
K : ℝ≥0
c : ℝ≥0∞
⊢ c ≠ ⊤
Tactic:
sorry
State after:
no goals