-- 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
⊢ ↑0 x✝ = 0 x✝

Tactic:
rfl

Result:
no goals

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
⊢ ↑f p✝ = (AffineMap.const R P q) p✝

Tactic:
rw [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 ↔ (↑f).linear = 0
q : Q
h : f = const R P q
p✝ : P
⊢ ↑(const R P q) p✝ = (AffineMap.const R P q) p✝

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
⊢ ∀ (q : Q), f = const R P q ↔ ↑f = AffineMap.const R P q

Tactic:
intro q

Result:
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
⊢ f = const R P q ↔ ↑f = AffineMap.const R P q

Proof state:
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.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : ↑f = AffineMap.const R P q
x✝ : P
⊢ f x✝ = (const R P q) x✝

Tactic:
rw [← coe_toAffineMap, h]

Result:
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.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : ↑f = AffineMap.const R P q
x✝ : P
⊢ (AffineMap.const R P q) x✝ = (const R P q) x✝

Proof state:
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✝

Tactic:
rw [← coe_linear_eq_coe_contLinear, h]

Result:
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
⊢ 0 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.contLinear = 0 ↔ ∃ q, f = const R P q

Tactic:
simp_rw [h₁, h₂]

Result:
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

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
q : Q
⊢ f = const R P q ↔ ↑f = AffineMap.const R P q

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 ↔ (↑f).linear = 0
q : Q
h : f = const R P q
p✝ : P
⊢ ↑f p✝ = (AffineMap.const R P q) p✝

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.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : ↑f = AffineMap.const R P q
x✝ : P
⊢ f x✝ = (const R P q) x✝

Proof state:
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.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : ↑f = AffineMap.const R P q
x✝ : P
⊢ (AffineMap.const R P q) x✝ = (const R P q) x✝

Tactic:
rfl

Result:
no goals

Proof state:
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
⊢ 0 x✝ = 0 x✝

Tactic:
rfl

Result:
no goals