[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
x✝¹ x✝ : P1 →ᵃ[k] P2
f : P1 → P2
f_linear : V1 →ₗ[k] V2
f_add : ∀ (p : P1) (v : V1), f (v +ᵥ p) = ↑f_linear v +ᵥ f p
g : P1 → P2
g_linear : V1 →ₗ[k] V2
g_add : ∀ (p : P1) (v : V1), g (v +ᵥ p) = ↑g_linear v +ᵥ g p
h : f = g
⊢ { toFun := f, linear := f_linear, map_vadd' := f_add } = { toFun := g, linear := g_linear, map_vadd' := g_add }
[PROOFSTEP]
cases' (AddTorsor.Nonempty : Nonempty P1) with p
[GOAL]
case intro
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
x✝¹ x✝ : P1 →ᵃ[k] P2
f : P1 → P2
f_linear : V1 →ₗ[k] V2
f_add : ∀ (p : P1) (v : V1), f (v +ᵥ p) = ↑f_linear v +ᵥ f p
g : P1 → P2
g_linear : V1 →ₗ[k] V2
g_add : ∀ (p : P1) (v : V1), g (v +ᵥ p) = ↑g_linear v +ᵥ g p
h : f = g
p : P1
⊢ { toFun := f, linear := f_linear, map_vadd' := f_add } = { toFun := g, linear := g_linear, map_vadd' := g_add }
[PROOFSTEP]
congr with v
[GOAL]
case intro.e_linear.h
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
x✝¹ x✝ : P1 →ᵃ[k] P2
f : P1 → P2
f_linear : V1 →ₗ[k] V2
f_add : ∀ (p : P1) (v : V1), f (v +ᵥ p) = ↑f_linear v +ᵥ f p
g : P1 → P2
g_linear : V1 →ₗ[k] V2
g_add : ∀ (p : P1) (v : V1), g (v +ᵥ p) = ↑g_linear v +ᵥ g p
h : f = g
p : P1
v : V1
⊢ ↑f_linear v = ↑g_linear v
[PROOFSTEP]
apply vadd_right_cancel (f p)
[GOAL]
case intro.e_linear.h
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
x✝¹ x✝ : P1 →ᵃ[k] P2
f : P1 → P2
f_linear : V1 →ₗ[k] V2
f_add : ∀ (p : P1) (v : V1), f (v +ᵥ p) = ↑f_linear v +ᵥ f p
g : P1 → P2
g_linear : V1 →ₗ[k] V2
g_add : ∀ (p : P1) (v : V1), g (v +ᵥ p) = ↑g_linear v +ᵥ g p
h : f = g
p : P1
v : V1
⊢ ↑f_linear v +ᵥ f p = ↑g_linear v +ᵥ f p
[PROOFSTEP]
erw [← f_add, h, ← g_add]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
p1 p2 : P1
⊢ ↑f.linear (p1 -ᵥ p2) = ↑f p1 -ᵥ ↑f p2
[PROOFSTEP]
conv_rhs => rw [← vsub_vadd p1 p2, map_vadd, vadd_vsub]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
p1 p2 : P1
| ↑f p1 -ᵥ ↑f p2
[PROOFSTEP]
rw [← vsub_vadd p1 p2, map_vadd, vadd_vsub]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
p1 p2 : P1
| ↑f p1 -ᵥ ↑f p2
[PROOFSTEP]
rw [← vsub_vadd p1 p2, map_vadd, vadd_vsub]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
p1 p2 : P1
| ↑f p1 -ᵥ ↑f p2
[PROOFSTEP]
rw [← vsub_vadd p1 p2, map_vadd, vadd_vsub]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p : P2
x✝¹ : P1
x✝ : V1
this : AddAction V2 P2 := inferInstance
⊢ Function.const P1 p (x✝ +ᵥ x✝¹) = ↑0 x✝ +ᵥ Function.const P1 p x✝¹
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
⊢ f.linear = 0 ↔ ∃ q, f = const k P1 q
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
h : f.linear = 0
⊢ ∃ q, f = const k P1 q
[PROOFSTEP]
use f (Classical.arbitrary P1)
[GOAL]
case h
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
h : f.linear = 0
⊢ f = const k P1 (↑f (Classical.arbitrary P1))
[PROOFSTEP]
ext
[GOAL]
case h.h
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
h : f.linear = 0
p✝ : P1
⊢ ↑f p✝ = ↑(const k P1 (↑f (Classical.arbitrary P1))) p✝
[PROOFSTEP]
rw [coe_const, Function.const_apply, ← @vsub_eq_zero_iff_eq V2, ← f.linearMap_vsub, h, LinearMap.zero_apply]
[GOAL]
case refine'_2
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
h : ∃ q, f = const k P1 q
⊢ f.linear = 0
[PROOFSTEP]
rcases h with ⟨q, rfl⟩
[GOAL]
case refine'_2.intro
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
q : P2
⊢ (const k P1 q).linear = 0
[PROOFSTEP]
exact const_linear k P1 q
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 → P2
f' : V1 →ₗ[k] V2
p : P1
h : ∀ (p' : P1), f p' = ↑f' (p' -ᵥ p) +ᵥ f p
p' : P1
v : V1
⊢ f (v +ᵥ p') = ↑f' v +ᵥ f p'
[PROOFSTEP]
rw [h, h p', vadd_vsub_assoc, f'.map_add, vadd_vadd]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹⁵ : Ring k
inst✝¹⁴ : AddCommGroup V1
inst✝¹³ : Module k V1
inst✝¹² : AffineSpace V1 P1
inst✝¹¹ : AddCommGroup V2
inst✝¹⁰ : Module k V2
inst✝⁹ : AffineSpace V2 P2
inst✝⁸ : AddCommGroup V3
inst✝⁷ : Module k V3
inst✝⁶ : AffineSpace V3 P3
inst✝⁵ : AddCommGroup V4
inst✝⁴ : Module k V4
inst✝³ : AffineSpace V4 P4
R : Type u_10
inst✝² : Monoid R
inst✝¹ : DistribMulAction R V2
inst✝ : SMulCommClass k R V2
c : R
f : P1 →ᵃ[k] V2
p : P1
v : V1
⊢ (c • ↑f) (v +ᵥ p) = ↑(c • f.linear) v +ᵥ (c • ↑f) p
[PROOFSTEP]
simp [smul_add, map_vadd f]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f g : P1 →ᵃ[k] V2
p : P1
v : V1
⊢ (↑f + ↑g) (v +ᵥ p) = ↑(f.linear + g.linear) v +ᵥ (↑f + ↑g) p
[PROOFSTEP]
simp [add_add_add_comm, (map_vadd)]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f g : P1 →ᵃ[k] V2
p : P1
v : V1
⊢ (↑f - ↑g) (v +ᵥ p) = ↑(f.linear - g.linear) v +ᵥ (↑f - ↑g) p
[PROOFSTEP]
simp [sub_add_sub_comm, (map_vadd)]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] V2
p : P1
v : V1
⊢ (-↑f) (v +ᵥ p) = ↑(-f.linear) v +ᵥ (-↑f) p
[PROOFSTEP]
simp [add_comm, map_vadd f]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] V2
g : P1 →ᵃ[k] P2
this : AddAction V2 P2 := inferInstance
p : P1
v : V1
⊢ (fun p => ↑f p +ᵥ ↑g p) (v +ᵥ p) = ↑(f.linear + g.linear) v +ᵥ (fun p => ↑f p +ᵥ ↑g p) p
[PROOFSTEP]
simp [vadd_vadd, add_right_comm, (map_vadd)]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f g : P1 →ᵃ[k] P2
p : P1
v : V1
⊢ (fun p => ↑f p -ᵥ ↑g p) (v +ᵥ p) = ↑(f.linear - g.linear) v +ᵥ (fun p => ↑f p -ᵥ ↑g p) p
[PROOFSTEP]
simp [(map_vadd), (vsub_vadd_eq_vsub_sub), (vadd_vsub_assoc), add_sub, sub_add_eq_add_sub]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P2 →ᵃ[k] P3
g : P1 →ᵃ[k] P2
⊢ ∀ (p : P1) (v : V1), (↑f ∘ ↑g) (v +ᵥ p) = ↑(LinearMap.comp f.linear g.linear) v +ᵥ (↑f ∘ ↑g) p
[PROOFSTEP]
intro p v
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P2 →ᵃ[k] P3
g : P1 →ᵃ[k] P2
p : P1
v : V1
⊢ (↑f ∘ ↑g) (v +ᵥ p) = ↑(LinearMap.comp f.linear g.linear) v +ᵥ (↑f ∘ ↑g) p
[PROOFSTEP]
rw [Function.comp_apply, g.map_vadd, f.map_vadd]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P2 →ᵃ[k] P3
g : P1 →ᵃ[k] P2
p : P1
v : V1
⊢ ↑f.linear (↑g.linear v) +ᵥ ↑f (↑g p) = ↑(LinearMap.comp f.linear g.linear) v +ᵥ (↑f ∘ ↑g) p
[PROOFSTEP]
rfl
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
⊢ Function.Injective ↑f.linear ↔ Function.Injective ↑f
[PROOFSTEP]
obtain ⟨p⟩ := (inferInstance : Nonempty P1)
[GOAL]
case intro
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
p : P1
⊢ Function.Injective ↑f.linear ↔ Function.Injective ↑f
[PROOFSTEP]
have h : ⇑f.linear = (Equiv.vaddConst (f p)).symm ∘ f ∘ Equiv.vaddConst p :=
  by
  ext v
  simp [f.map_vadd, vadd_vsub_assoc]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
p : P1
⊢ ↑f.linear = ↑(Equiv.vaddConst (↑f p)).symm ∘ ↑f ∘ ↑(Equiv.vaddConst p)
[PROOFSTEP]
ext v
[GOAL]
case h
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
p : P1
v : V1
⊢ ↑f.linear v = (↑(Equiv.vaddConst (↑f p)).symm ∘ ↑f ∘ ↑(Equiv.vaddConst p)) v
[PROOFSTEP]
simp [f.map_vadd, vadd_vsub_assoc]
[GOAL]
case intro
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
p : P1
h : ↑f.linear = ↑(Equiv.vaddConst (↑f p)).symm ∘ ↑f ∘ ↑(Equiv.vaddConst p)
⊢ Function.Injective ↑f.linear ↔ Function.Injective ↑f
[PROOFSTEP]
rw [h, Equiv.comp_injective, Equiv.injective_comp]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
⊢ Function.Surjective ↑f.linear ↔ Function.Surjective ↑f
[PROOFSTEP]
obtain ⟨p⟩ := (inferInstance : Nonempty P1)
[GOAL]
case intro
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
p : P1
⊢ Function.Surjective ↑f.linear ↔ Function.Surjective ↑f
[PROOFSTEP]
have h : ⇑f.linear = (Equiv.vaddConst (f p)).symm ∘ f ∘ Equiv.vaddConst p :=
  by
  ext v
  simp [f.map_vadd, vadd_vsub_assoc]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
p : P1
⊢ ↑f.linear = ↑(Equiv.vaddConst (↑f p)).symm ∘ ↑f ∘ ↑(Equiv.vaddConst p)
[PROOFSTEP]
ext v
[GOAL]
case h
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
p : P1
v : V1
⊢ ↑f.linear v = (↑(Equiv.vaddConst (↑f p)).symm ∘ ↑f ∘ ↑(Equiv.vaddConst p)) v
[PROOFSTEP]
simp [f.map_vadd, vadd_vsub_assoc]
[GOAL]
case intro
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
p : P1
h : ↑f.linear = ↑(Equiv.vaddConst (↑f p)).symm ∘ ↑f ∘ ↑(Equiv.vaddConst p)
⊢ Function.Surjective ↑f.linear ↔ Function.Surjective ↑f
[PROOFSTEP]
rw [h, Equiv.comp_surjective, Equiv.surjective_comp]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
⊢ ↑f '' s -ᵥ ↑f '' t = ↑f.linear '' (s -ᵥ t)
[PROOFSTEP]
ext v
[GOAL]
case h
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
v : V2
⊢ v ∈ ↑f '' s -ᵥ ↑f '' t ↔ v ∈ ↑f.linear '' (s -ᵥ t)
[PROOFSTEP]
simp only [(Set.mem_vsub), Set.mem_image, exists_exists_and_eq_and, exists_and_left, ← f.linearMap_vsub]
[GOAL]
case h
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
v : V2
⊢ (∃ a, a ∈ s ∧ ∃ a_1, a_1 ∈ t ∧ ↑f.linear (a -ᵥ a_1) = v) ↔
    ∃ x, (∃ x_1, x_1 ∈ s ∧ ∃ x_2, x_2 ∈ t ∧ x_1 -ᵥ x_2 = x) ∧ ↑f.linear x = v
[PROOFSTEP]
constructor
[GOAL]
case h.mp
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
v : V2
⊢ (∃ a, a ∈ s ∧ ∃ a_1, a_1 ∈ t ∧ ↑f.linear (a -ᵥ a_1) = v) →
    ∃ x, (∃ x_1, x_1 ∈ s ∧ ∃ x_2, x_2 ∈ t ∧ x_1 -ᵥ x_2 = x) ∧ ↑f.linear x = v
[PROOFSTEP]
rintro ⟨x, hx, y, hy, hv⟩
[GOAL]
case h.mp.intro.intro.intro.intro
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
v : V2
x : P1
hx : x ∈ s
y : P1
hy : y ∈ t
hv : ↑f.linear (x -ᵥ y) = v
⊢ ∃ x, (∃ x_1, x_1 ∈ s ∧ ∃ x_2, x_2 ∈ t ∧ x_1 -ᵥ x_2 = x) ∧ ↑f.linear x = v
[PROOFSTEP]
exact ⟨x -ᵥ y, ⟨x, hx, y, hy, rfl⟩, hv⟩
[GOAL]
case h.mpr
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
v : V2
⊢ (∃ x, (∃ x_1, x_1 ∈ s ∧ ∃ x_2, x_2 ∈ t ∧ x_1 -ᵥ x_2 = x) ∧ ↑f.linear x = v) →
    ∃ a, a ∈ s ∧ ∃ a_1, a_1 ∈ t ∧ ↑f.linear (a -ᵥ a_1) = v
[PROOFSTEP]
rintro ⟨-, ⟨x, hx, y, hy, rfl⟩, rfl⟩
[GOAL]
case h.mpr.intro.intro.intro.intro.intro.intro
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
x : P1
hx : x ∈ s
y : P1
hy : y ∈ t
⊢ ∃ a, a ∈ s ∧ ∃ a_1, a_1 ∈ t ∧ ↑f.linear (a -ᵥ a_1) = ↑f.linear (x -ᵥ y)
[PROOFSTEP]
exact ⟨x, hx, y, hy, rfl⟩
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p₀ p₁ : V1
c : k
⊢ ↑(lineMap p₀ p₁) c = (1 - c) • p₀ + c • p₁
[PROOFSTEP]
simp [lineMap_apply_module', smul_sub, sub_smul]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p₀ p₁ : V1
c : k
⊢ c • p₁ - c • p₀ + p₀ = p₀ - c • p₀ + c • p₁
[PROOFSTEP]
abel
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p₀ p₁ : V1
c : k
⊢ c • p₁ - c • p₀ + p₀ = p₀ - c • p₀ + c • p₁
[PROOFSTEP]
abel
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p : P1
v : V1
c : k
⊢ ↑(lineMap p (v +ᵥ p)) c = c • v +ᵥ p
[PROOFSTEP]
rw [lineMap_apply, vadd_vsub]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p : P1
c : k
⊢ ↑(lineMap p p) c = p
[PROOFSTEP]
letI : AddAction V1 P1 := inferInstance
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p : P1
c : k
this : AddAction V1 P1 := inferInstance
⊢ ↑(lineMap p p) c = p
[PROOFSTEP]
simp [(lineMap_apply), (vsub_self)]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p₀ p₁ : P1
⊢ ↑(lineMap p₀ p₁) 0 = p₀
[PROOFSTEP]
letI : AddAction V1 P1 := inferInstance
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p₀ p₁ : P1
this : AddAction V1 P1 := inferInstance
⊢ ↑(lineMap p₀ p₁) 0 = p₀
[PROOFSTEP]
simp [(lineMap_apply)]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p₀ p₁ : P1
⊢ ↑(lineMap p₀ p₁) 1 = p₁
[PROOFSTEP]
simp [(lineMap_apply), (vsub_vadd)]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹³ : Ring k
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k V4
inst✝¹ : AffineSpace V4 P4
inst✝ : NoZeroSMulDivisors k V1
p₀ p₁ : P1
c₁ c₂ : k
⊢ ↑(lineMap p₀ p₁) c₁ = ↑(lineMap p₀ p₁) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂
[PROOFSTEP]
rw [lineMap_apply, lineMap_apply, ← @vsub_eq_zero_iff_eq V1, vadd_vsub_vadd_cancel_right, ← sub_smul, smul_eq_zero,
  sub_eq_zero, vsub_eq_zero_iff_eq, or_comm, eq_comm]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹³ : Ring k
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k V4
inst✝¹ : AffineSpace V4 P4
inst✝ : NoZeroSMulDivisors k V1
p₀ p₁ : P1
c : k
⊢ ↑(lineMap p₀ p₁) c = p₀ ↔ p₀ = p₁ ∨ c = 0
[PROOFSTEP]
rw [← @lineMap_eq_lineMap_iff k V1, lineMap_apply_zero]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹³ : Ring k
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k V4
inst✝¹ : AffineSpace V4 P4
inst✝ : NoZeroSMulDivisors k V1
p₀ p₁ : P1
c : k
⊢ ↑(lineMap p₀ p₁) c = p₁ ↔ p₀ = p₁ ∨ c = 1
[PROOFSTEP]
rw [← @lineMap_eq_lineMap_iff k V1, lineMap_apply_one]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
p₀ p₁ : P1
c : k
⊢ ↑f (↑(lineMap p₀ p₁) c) = ↑(lineMap (↑f p₀) (↑f p₁)) c
[PROOFSTEP]
simp [(lineMap_apply), (map_vadd), (linearMap_vsub)]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p₀ p₁ : P1
⊢ lineMap p₀ p₁ = comp (lineMap p₁ p₀) (lineMap 1 0)
[PROOFSTEP]
rw [comp_lineMap]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p₀ p₁ : P1
⊢ lineMap p₀ p₁ = lineMap (↑(lineMap p₁ p₀) 1) (↑(lineMap p₁ p₀) 0)
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p₀ p₁ : P1
c : k
⊢ ↑(lineMap p₀ p₁) (1 - c) = ↑(lineMap p₁ p₀) c
[PROOFSTEP]
rw [lineMap_symm p₀, comp_apply]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p₀ p₁ : P1
c : k
⊢ ↑(lineMap p₁ p₀) (↑(lineMap 1 0) (1 - c)) = ↑(lineMap p₁ p₀) c
[PROOFSTEP]
congr
[GOAL]
case h.e_6.h
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p₀ p₁ : P1
c : k
⊢ ↑(lineMap 1 0) (1 - c) = c
[PROOFSTEP]
simp [lineMap_apply]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p₀ p₁ : P1
c : k
⊢ p₀ -ᵥ ↑(lineMap p₀ p₁) c = c • (p₀ -ᵥ p₁)
[PROOFSTEP]
rw [← neg_vsub_eq_vsub_rev, lineMap_vsub_left, ← smul_neg, neg_vsub_eq_vsub_rev]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p₀ p₁ : P1
c : k
⊢ ↑(lineMap p₀ p₁) c -ᵥ p₁ = (1 - c) • (p₀ -ᵥ p₁)
[PROOFSTEP]
rw [← lineMap_apply_one_sub, lineMap_vsub_left]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p₀ p₁ : P1
c : k
⊢ p₁ -ᵥ ↑(lineMap p₀ p₁) c = (1 - c) • (p₁ -ᵥ p₀)
[PROOFSTEP]
rw [← lineMap_apply_one_sub, left_vsub_lineMap]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : V1 →ᵃ[k] V2
⊢ ↑f = ↑f.linear + fun x => ↑f 0
[PROOFSTEP]
ext x
[GOAL]
case h
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : V1 →ᵃ[k] V2
x : V1
⊢ ↑f x = (↑f.linear + fun x => ↑f 0) x
[PROOFSTEP]
calc
  f x = f.linear x +ᵥ f 0 := by rw [← f.map_vadd, vadd_eq_add, add_zero]
  _ = (f.linear + fun _ : V1 => f 0) x := rfl
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : V1 →ᵃ[k] V2
x : V1
⊢ ↑f x = ↑f.linear x +ᵥ ↑f 0
[PROOFSTEP]
rw [← f.map_vadd, vadd_eq_add, add_zero]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : V1 →ᵃ[k] V2
⊢ ↑f.linear = ↑f - fun x => ↑f 0
[PROOFSTEP]
rw [decomp]
[GOAL]
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : V1 →ᵃ[k] V2
⊢ ↑f.linear = (↑f.linear + fun x => ↑f 0) - fun x => (↑f.linear + fun x => ↑f 0) 0
[PROOFSTEP]
simp only [LinearMap.map_zero, Pi.add_apply, add_sub_cancel, zero_add]
[GOAL]
k✝ : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b : k
⊢ ↑f '' Set.uIcc a b = Set.uIcc (↑f a) (↑f b)
[PROOFSTEP]
have : ⇑f = (fun x => x + f 0) ∘ fun x => x * (f 1 - f 0) :=
  by
  ext x
  change f x = x • (f 1 -ᵥ f 0) +ᵥ f 0
  rw [← f.linearMap_vsub, ← f.linear.map_smul, ← f.map_vadd]
  simp only [vsub_eq_sub, add_zero, mul_one, vadd_eq_add, sub_zero, smul_eq_mul]
[GOAL]
k✝ : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b : k
⊢ ↑f = (fun x => x + ↑f 0) ∘ fun x => x * (↑f 1 - ↑f 0)
[PROOFSTEP]
ext x
[GOAL]
case h
k✝ : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b x : k
⊢ ↑f x = ((fun x => x + ↑f 0) ∘ fun x => x * (↑f 1 - ↑f 0)) x
[PROOFSTEP]
change f x = x • (f 1 -ᵥ f 0) +ᵥ f 0
[GOAL]
case h
k✝ : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b x : k
⊢ ↑f x = x • (↑f 1 -ᵥ ↑f 0) +ᵥ ↑f 0
[PROOFSTEP]
rw [← f.linearMap_vsub, ← f.linear.map_smul, ← f.map_vadd]
[GOAL]
case h
k✝ : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b x : k
⊢ ↑f x = ↑f (x • (1 -ᵥ 0) +ᵥ 0)
[PROOFSTEP]
simp only [vsub_eq_sub, add_zero, mul_one, vadd_eq_add, sub_zero, smul_eq_mul]
[GOAL]
k✝ : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b : k
this : ↑f = (fun x => x + ↑f 0) ∘ fun x => x * (↑f 1 - ↑f 0)
⊢ ↑f '' Set.uIcc a b = Set.uIcc (↑f a) (↑f b)
[PROOFSTEP]
rw [this, Set.image_comp]
[GOAL]
k✝ : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹³ : Ring k✝
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k✝ V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k✝ V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k✝ V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k✝ V4
inst✝¹ : AffineSpace V4 P4
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b : k
this : ↑f = (fun x => x + ↑f 0) ∘ fun x => x * (↑f 1 - ↑f 0)
⊢ (fun x => x + ↑f 0) '' ((fun x => x * (↑f 1 - ↑f 0)) '' Set.uIcc a b) =
    Set.uIcc (((fun x => x + ↑f 0) ∘ fun x => x * (↑f 1 - ↑f 0)) a)
      (((fun x => x + ↑f 0) ∘ fun x => x * (↑f 1 - ↑f 0)) b)
[PROOFSTEP]
simp only [Set.image_add_const_uIcc, Set.image_mul_const_uIcc, Function.comp_apply]
[GOAL]
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V1
inst✝⁶ : AffineSpace V1 P1
inst✝⁵ : AddCommGroup V2
inst✝⁴ : Module k V1
inst✝³ : Module k V2
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
⊢ ∀ (x y : V1 →ᵃ[k] V2),
    (fun f => (↑f 0, f.linear)) (x + y) = (fun f => (↑f 0, f.linear)) x + (fun f => (↑f 0, f.linear)) y
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V1
inst✝⁶ : AffineSpace V1 P1
inst✝⁵ : AddCommGroup V2
inst✝⁴ : Module k V1
inst✝³ : Module k V2
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
⊢ ∀ (r : R) (x : V1 →ᵃ[k] V2),
    AddHom.toFun
        { toFun := fun f => (↑f 0, f.linear),
          map_add' :=
            (_ :
              ∀ (a a_1 : V1 →ᵃ[k] V2),
                (↑a 0 + ↑a_1 0, a.linear + a_1.linear) = (↑a 0 + ↑a_1 0, a.linear + a_1.linear)) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := fun f => (↑f 0, f.linear),
            map_add' :=
              (_ :
                ∀ (a a_1 : V1 →ᵃ[k] V2),
                  (↑a 0 + ↑a_1 0, a.linear + a_1.linear) = (↑a 0 + ↑a_1 0, a.linear + a_1.linear)) }
          x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V1
inst✝⁶ : AffineSpace V1 P1
inst✝⁵ : AddCommGroup V2
inst✝⁴ : Module k V1
inst✝³ : Module k V2
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
f : V1 →ᵃ[k] V2
⊢ (fun p => LinearMap.toAffineMap p.snd + const k V1 p.fst)
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun f => (↑f 0, f.linear),
                map_add' :=
                  (_ :
                    ∀ (a a_1 : V1 →ᵃ[k] V2),
                      (↑a 0 + ↑a_1 0, a.linear + a_1.linear) = (↑a 0 + ↑a_1 0, a.linear + a_1.linear)) },
            map_smul' :=
              (_ :
                ∀ (a : R) (a_1 : V1 →ᵃ[k] V2), (a • ↑a_1 0, a • a_1.linear) = (a • ↑a_1 0, a • a_1.linear)) }.toAddHom
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V1
inst✝⁶ : AffineSpace V1 P1
inst✝⁵ : AddCommGroup V2
inst✝⁴ : Module k V1
inst✝³ : Module k V2
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
f : V1 →ᵃ[k] V2
p✝ : V1
⊢ ↑((fun p => LinearMap.toAffineMap p.snd + const k V1 p.fst)
          (AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun f => (↑f 0, f.linear),
                    map_add' :=
                      (_ :
                        ∀ (a a_1 : V1 →ᵃ[k] V2),
                          (↑a 0 + ↑a_1 0, a.linear + a_1.linear) = (↑a 0 + ↑a_1 0, a.linear + a_1.linear)) },
                map_smul' :=
                  (_ :
                    ∀ (a : R) (a_1 : V1 →ᵃ[k] V2),
                      (a • ↑a_1 0, a • a_1.linear) = (a • ↑a_1 0, a • a_1.linear)) }.toAddHom
            f))
      p✝ =
    ↑f p✝
[PROOFSTEP]
rw [f.decomp]
[GOAL]
case h
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V1
inst✝⁶ : AffineSpace V1 P1
inst✝⁵ : AddCommGroup V2
inst✝⁴ : Module k V1
inst✝³ : Module k V2
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
f : V1 →ᵃ[k] V2
p✝ : V1
⊢ ↑((fun p => LinearMap.toAffineMap p.snd + const k V1 p.fst)
          (AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun f => (↑f 0, f.linear),
                    map_add' :=
                      (_ :
                        ∀ (a a_1 : V1 →ᵃ[k] V2),
                          (↑a 0 + ↑a_1 0, a.linear + a_1.linear) = (↑a 0 + ↑a_1 0, a.linear + a_1.linear)) },
                map_smul' :=
                  (_ :
                    ∀ (a : R) (a_1 : V1 →ᵃ[k] V2),
                      (a • ↑a_1 0, a • a_1.linear) = (a • ↑a_1 0, a • a_1.linear)) }.toAddHom
            f))
      p✝ =
    (↑f.linear + fun x => ↑f 0) p✝
[PROOFSTEP]
simp [const_apply _ _]
  -- porting note: `simp` needs `_`s to use this lemma
[GOAL]
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V1
inst✝⁶ : AffineSpace V1 P1
inst✝⁵ : AddCommGroup V2
inst✝⁴ : Module k V1
inst✝³ : Module k V2
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
⊢ Function.RightInverse (fun p => LinearMap.toAffineMap p.snd + const k V1 p.fst)
    {
          toAddHom :=
            { toFun := fun f => (↑f 0, f.linear),
              map_add' :=
                (_ :
                  ∀ (a a_1 : V1 →ᵃ[k] V2),
                    (↑a 0 + ↑a_1 0, a.linear + a_1.linear) = (↑a 0 + ↑a_1 0, a.linear + a_1.linear)) },
          map_smul' :=
            (_ :
              ∀ (a : R) (a_1 : V1 →ᵃ[k] V2),
                (a • ↑a_1 0, a • a_1.linear) = (a • ↑a_1 0, a • a_1.linear)) }.toAddHom.toFun
[PROOFSTEP]
rintro ⟨v, f⟩
[GOAL]
case mk
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V1
inst✝⁶ : AffineSpace V1 P1
inst✝⁵ : AddCommGroup V2
inst✝⁴ : Module k V1
inst✝³ : Module k V2
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
v : V2
f : V1 →ₗ[k] V2
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun f => (↑f 0, f.linear),
              map_add' :=
                (_ :
                  ∀ (a a_1 : V1 →ᵃ[k] V2),
                    (↑a 0 + ↑a_1 0, a.linear + a_1.linear) = (↑a 0 + ↑a_1 0, a.linear + a_1.linear)) },
          map_smul' :=
            (_ : ∀ (a : R) (a_1 : V1 →ᵃ[k] V2), (a • ↑a_1 0, a • a_1.linear) = (a • ↑a_1 0, a • a_1.linear)) }.toAddHom
      ((fun p => LinearMap.toAffineMap p.snd + const k V1 p.fst) (v, f)) =
    (v, f)
[PROOFSTEP]
ext
[GOAL]
case mk.h₁
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V1
inst✝⁶ : AffineSpace V1 P1
inst✝⁵ : AddCommGroup V2
inst✝⁴ : Module k V1
inst✝³ : Module k V2
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
v : V2
f : V1 →ₗ[k] V2
⊢ (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun f => (↑f 0, f.linear),
                map_add' :=
                  (_ :
                    ∀ (a a_1 : V1 →ᵃ[k] V2),
                      (↑a 0 + ↑a_1 0, a.linear + a_1.linear) = (↑a 0 + ↑a_1 0, a.linear + a_1.linear)) },
            map_smul' :=
              (_ :
                ∀ (a : R) (a_1 : V1 →ᵃ[k] V2), (a • ↑a_1 0, a • a_1.linear) = (a • ↑a_1 0, a • a_1.linear)) }.toAddHom
        ((fun p => LinearMap.toAffineMap p.snd + const k V1 p.fst) (v, f))).fst =
    (v, f).fst
[PROOFSTEP]
simp [const_apply _ _, const_linear _ _]
  -- porting note: `simp` needs `_`s
[GOAL]
case mk.h₂.h
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V1
inst✝⁶ : AffineSpace V1 P1
inst✝⁵ : AddCommGroup V2
inst✝⁴ : Module k V1
inst✝³ : Module k V2
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
v : V2
f : V1 →ₗ[k] V2
x✝ : V1
⊢ ↑(AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun f => (↑f 0, f.linear),
                    map_add' :=
                      (_ :
                        ∀ (a a_1 : V1 →ᵃ[k] V2),
                          (↑a 0 + ↑a_1 0, a.linear + a_1.linear) = (↑a 0 + ↑a_1 0, a.linear + a_1.linear)) },
                map_smul' :=
                  (_ :
                    ∀ (a : R) (a_1 : V1 →ᵃ[k] V2),
                      (a • ↑a_1 0, a • a_1.linear) = (a • ↑a_1 0, a • a_1.linear)) }.toAddHom
            ((fun p => LinearMap.toAffineMap p.snd + const k V1 p.fst) (v, f))).snd
      x✝ =
    ↑(v, f).snd x✝
[PROOFSTEP]
simp [const_apply _ _, const_linear _ _]
  -- porting note: `simp` needs `_`s
[GOAL]
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
inst✝⁵ : CommRing k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V1
inst✝ : Module k V2
c : P1
⊢ homothety c 1 = id k P1
[PROOFSTEP]
ext p
[GOAL]
case h
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
inst✝⁵ : CommRing k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V1
inst✝ : Module k V2
c p : P1
⊢ ↑(homothety c 1) p = ↑(id k P1) p
[PROOFSTEP]
simp [homothety_apply]
[GOAL]
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
inst✝⁵ : CommRing k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V1
inst✝ : Module k V2
c : P1
r₁ r₂ : k
p : P1
⊢ ↑(homothety c (r₁ * r₂)) p = ↑(homothety c r₁) (↑(homothety c r₂) p)
[PROOFSTEP]
simp only [homothety_apply, mul_smul, vadd_vsub]
[GOAL]
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
inst✝⁵ : CommRing k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V1
inst✝ : Module k V2
c : P1
⊢ homothety c 0 = const k P1 c
[PROOFSTEP]
ext p
[GOAL]
case h
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
inst✝⁵ : CommRing k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V1
inst✝ : Module k V2
c p : P1
⊢ ↑(homothety c 0) p = ↑(const k P1 c) p
[PROOFSTEP]
simp [homothety_apply]
[GOAL]
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
inst✝⁵ : CommRing k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V1
inst✝ : Module k V2
c : P1
r₁ r₂ : k
⊢ homothety c (r₁ + r₂) = r₁ • (id k P1 -ᵥ const k P1 c) +ᵥ homothety c r₂
[PROOFSTEP]
simp only [homothety_def, add_smul, vadd_vadd]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a b : 𝕜
f : E →ᵃ[𝕜] F
h : a + b = 1
⊢ ↑f (a • x + b • y) = a • ↑f x + b • ↑f y
[PROOFSTEP]
simp only [Convex.combo_eq_smul_sub_add h, ← vsub_eq_sub]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a b : 𝕜
f : E →ᵃ[𝕜] F
h : a + b = 1
⊢ ↑f (b • (y -ᵥ x) + x) = b • (↑f y -ᵥ ↑f x) + ↑f x
[PROOFSTEP]
exact f.apply_lineMap _ _ _
