𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
h₂ : ∀ (q : Q), f = const R P q ↔ f.toAffineMap = AffineMap.const R P q
⊢ f.linear = 0 ↔ ∃ q, f.toAffineMap = AffineMap.const R P q
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
h₂ : ∀ (q : Q), f = const R P q ↔ f.toAffineMap = AffineMap.const R P q
⊢ contLinear f = 0 ↔ ∃ q, f = const R P q
simp_rw [h₁, h₂]
no goals
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
h₂ : ∀ (q : Q), f = const R P q ↔ f.toAffineMap = AffineMap.const R P q
⊢ f.linear = 0 ↔ ∃ q, f.toAffineMap = AffineMap.const R P q
exact (f : P →ᵃ[R] Q).linear_eq_zero_iff_exists_const
case refine'_1.h
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h : contLinear f = 0
x✝ : V
⊢ ↑f.linear x✝ = ↑0 x✝

case refine'_2.h
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h : f.linear = 0
x✝ : V
⊢ ↑(contLinear f) x✝ = ↑0 x✝
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
⊢ contLinear f = 0 ↔ f.linear = 0
refine' ⟨fun h => _, fun h => _⟩ <;> ext
case refine'_1.h
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h : contLinear f = 0
x✝ : V
⊢ ↑↑0 x✝ = ↑0 x✝
case refine'_1.h
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h : contLinear f = 0
x✝ : V
⊢ ↑f.linear x✝ = ↑0 x✝
rw [← coe_contLinear_eq_linear, h]
no goals
case refine'_1.h
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h : contLinear f = 0
x✝ : V
⊢ ↑↑0 x✝ = ↑0 x✝
rfl
case refine'_2.h
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h : f.linear = 0
x✝ : V
⊢ ↑0 x✝ = ↑0 x✝
case refine'_2.h
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h : f.linear = 0
x✝ : V
⊢ ↑(contLinear f) x✝ = ↑0 x✝
rw [← coe_linear_eq_coe_contLinear, h]
no goals
case refine'_2.h
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h : f.linear = 0
x✝ : V
⊢ ↑0 x✝ = ↑0 x✝
rfl
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
q : Q
⊢ f = const R P q ↔ f.toAffineMap = AffineMap.const R P q
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
⊢ ∀ (q : Q), f = const R P q ↔ f.toAffineMap = AffineMap.const R P q
intro q
case refine'_1.h
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
q : Q
h : f = const R P q
p✝ : P
⊢ ↑f.toAffineMap p✝ = ↑(AffineMap.const R P q) p✝

case refine'_2.h
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
q : Q
h : f.toAffineMap = AffineMap.const R P q
x✝ : P
⊢ ↑f x✝ = ↑(const R P q) x✝
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
q : Q
⊢ f = const R P q ↔ f.toAffineMap = AffineMap.const R P q
refine' ⟨fun h => _, fun h => _⟩ <;> ext
case refine'_1.h
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
q : Q
h : f = const R P q
p✝ : P
⊢ ↑(const R P q).toAffineMap p✝ = ↑(AffineMap.const R P q) p✝
case refine'_1.h
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
q : Q
h : f = const R P q
p✝ : P
⊢ ↑f.toAffineMap p✝ = ↑(AffineMap.const R P q) p✝
rw [h]
no goals
case refine'_1.h
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
q : Q
h : f = const R P q
p✝ : P
⊢ ↑(const R P q).toAffineMap p✝ = ↑(AffineMap.const R P q) p✝
rfl
case refine'_2.h
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
q : Q
h : f.toAffineMap = AffineMap.const R P q
x✝ : P
⊢ ↑(AffineMap.const R P q) x✝ = ↑(const R P q) x✝
case refine'_2.h
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
q : Q
h : f.toAffineMap = AffineMap.const R P q
x✝ : P
⊢ ↑f x✝ = ↑(const R P q) x✝
rw [← coe_to_affineMap, h]
no goals
case refine'_2.h
𝕜 : Type ?u.49821
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.49833
P : Type u_4
Q : Type u_5
Q₂ : Type ?u.49842
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
q : Q
h : f.toAffineMap = AffineMap.const R P q
x✝ : P
⊢ ↑(AffineMap.const R P q) x✝ = ↑(const R P q) x✝
rfl