-- Mathlib/Analysis/Normed/Affine/ContinuousAffineMap.lean
theorem contLinear_eq_zero_iff_exists_const (f : P →ᴬ[R] Q) :
    f.contLinear = 0 ↔ ∃ q, f = const R P q

Proof state:
case refine_1.h
R : Type u_2
V : Type u_3
W : Type u_4
P : Type u_6
Q : Type u_7
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : MetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
inst✝² : NormedField R
inst✝¹ : NormedSpace R V
inst✝ : NormedSpace R W
f : P →ᴬ[R] Q
h : f.contLinear = 0
x✝ : V
⊢ (↑f).linear x✝ = 0 x✝

Tactic:
rw [← coe_contLinear_eq_linear, h]

Result:
case refine_1.h
R : Type u_2
V : Type u_3
W : Type u_4
P : Type u_6
Q : Type u_7
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : MetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
inst✝² : NormedField R
inst✝¹ : NormedSpace R V
inst✝ : NormedSpace R W
f : P →ᴬ[R] Q
h : f.contLinear = 0
x✝ : V
⊢ ↑0 x✝ = 0 x✝

Proof state:
case refine_1.h
R : Type u_2
V : Type u_3
W : Type u_4
P : Type u_6
Q : Type u_7
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : MetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
inst✝² : NormedField R
inst✝¹ : NormedSpace R V
inst✝ : NormedSpace R W
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : f = const R P q
p✝ : P
⊢ ↑(const R P q) p✝ = (AffineMap.const R P q) p✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_2
V : Type u_3
W : Type u_4
P : Type u_6
Q : Type u_7
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : MetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
inst✝² : NormedField R
inst✝¹ : NormedSpace R V
inst✝ : NormedSpace R W
f : P →ᴬ[R] Q
⊢ f.contLinear = 0 ↔ (↑f).linear = 0

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩ <;> ext

Result:
case refine_1.h
R : Type u_2
V : Type u_3
W : Type u_4
P : Type u_6
Q : Type u_7
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : MetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
inst✝² : NormedField R
inst✝¹ : NormedSpace R V
inst✝ : NormedSpace R W
f : P →ᴬ[R] Q
h : f.contLinear = 0
x✝ : V
⊢ (↑f).linear x✝ = 0 x✝

case refine_2.h
R : Type u_2
V : Type u_3
W : Type u_4
P : Type u_6
Q : Type u_7
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : MetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
inst✝² : NormedField R
inst✝¹ : NormedSpace R V
inst✝ : NormedSpace R W
f : P →ᴬ[R] Q
h : (↑f).linear = 0
x✝ : V
⊢ f.contLinear x✝ = 0 x✝

Proof state:
R : Type u_2
V : Type u_3
W : Type u_4
P : Type u_6
Q : Type u_7
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : MetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
inst✝² : NormedField R
inst✝¹ : NormedSpace R V
inst✝ : NormedSpace R W
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
h₂ : ∀ (q : Q), f = const R P q ↔ ↑f = AffineMap.const R P q
⊢ (↑f).linear = 0 ↔ ∃ q, ↑f = AffineMap.const R P q

Tactic:
exact (f : P →ᵃ[R] Q).linear_eq_zero_iff_exists_const

Result:
no goals