[GOAL]
k : Type u_1
inst✝⁹ : Ring k
V : Type u_2
P : Type u_3
V₁ : Type u_4
P₁ : Type u_5
V₂ : Type u_6
P₂ : Type u_7
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
v : V
⊢ v +ᵥ ⊥ = ⊥
[PROOFSTEP]
ext
[GOAL]
case h
k : Type u_1
inst✝⁹ : Ring k
V : Type u_2
P : Type u_3
V₁ : Type u_4
P₁ : Type u_5
V₂ : Type u_6
P₂ : Type u_7
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
v : V
x✝ : P
⊢ x✝ ∈ v +ᵥ ⊥ ↔ x✝ ∈ ⊥
[PROOFSTEP]
simp [pointwise_vadd_eq_map, map_bot]
[GOAL]
k : Type u_1
inst✝⁹ : Ring k
V : Type u_2
P : Type u_3
V₁ : Type u_4
P₁ : Type u_5
V₂ : Type u_6
P₂ : Type u_7
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
v : V
s : AffineSubspace k P
⊢ direction (v +ᵥ s) = direction s
[PROOFSTEP]
rw [pointwise_vadd_eq_map, map_direction]
[GOAL]
k : Type u_1
inst✝⁹ : Ring k
V : Type u_2
P : Type u_3
V₁ : Type u_4
P₁ : Type u_5
V₂ : Type u_6
P₂ : Type u_7
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
v : V
s : AffineSubspace k P
⊢ Submodule.map (↑(AffineEquiv.constVAdd k P v)).linear (direction s) = direction s
[PROOFSTEP]
exact Submodule.map_id _
[GOAL]
k : Type u_1
inst✝⁹ : Ring k
V : Type u_2
P : Type u_3
V₁ : Type u_4
P₁ : Type u_5
V₂ : Type u_6
P₂ : Type u_7
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
⊢ map f (v +ᵥ s) = ↑f.linear v +ᵥ map f s
[PROOFSTEP]
erw [pointwise_vadd_eq_map, pointwise_vadd_eq_map, map_map, map_map]
[GOAL]
k : Type u_1
inst✝⁹ : Ring k
V : Type u_2
P : Type u_3
V₁ : Type u_4
P₁ : Type u_5
V₂ : Type u_6
P₂ : Type u_7
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
⊢ map (AffineMap.comp f ↑(AffineEquiv.constVAdd k P₁ v)) s =
    map (AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ (↑f.linear v))) f) s
[PROOFSTEP]
congr 1
[GOAL]
case e_f
k : Type u_1
inst✝⁹ : Ring k
V : Type u_2
P : Type u_3
V₁ : Type u_4
P₁ : Type u_5
V₂ : Type u_6
P₂ : Type u_7
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
⊢ AffineMap.comp f ↑(AffineEquiv.constVAdd k P₁ v) = AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ (↑f.linear v))) f
[PROOFSTEP]
ext
[GOAL]
case e_f.h
k : Type u_1
inst✝⁹ : Ring k
V : Type u_2
P : Type u_3
V₁ : Type u_4
P₁ : Type u_5
V₂ : Type u_6
P₂ : Type u_7
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
p✝ : P₁
⊢ ↑(AffineMap.comp f ↑(AffineEquiv.constVAdd k P₁ v)) p✝ =
    ↑(AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ (↑f.linear v))) f) p✝
[PROOFSTEP]
exact f.map_vadd _ _


[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a : k
⊢ slope f a a = 0
[PROOFSTEP]
rw [slope, sub_self, inv_zero, zero_smul]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
⊢ (b - a) • slope f a b = f b -ᵥ f a
[PROOFSTEP]
rcases eq_or_ne a b with (rfl | hne)
[GOAL]
case inl
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a : k
⊢ (a - a) • slope f a a = f a -ᵥ f a
[PROOFSTEP]
rw [sub_self, zero_smul, vsub_self]
[GOAL]
case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
hne : a ≠ b
⊢ (b - a) • slope f a b = f b -ᵥ f a
[PROOFSTEP]
rw [slope, smul_inv_smul₀ (sub_ne_zero.2 hne.symm)]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
⊢ (b - a) • slope f a b +ᵥ f a = f b
[PROOFSTEP]
rw [sub_smul_slope, vsub_vadd]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → E
c : PE
⊢ (slope fun x => f x +ᵥ c) = slope f
[PROOFSTEP]
ext a b
[GOAL]
case h.h
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → E
c : PE
a b : k
⊢ slope (fun x => f x +ᵥ c) a b = slope f a b
[PROOFSTEP]
simp only [slope, vadd_vsub_vadd_cancel_right, vsub_eq_sub]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → E
a b : k
h : a ≠ b
⊢ slope (fun x => (x - a) • f x) a b = f b
[PROOFSTEP]
simp [slope, inv_smul_smul₀ (sub_ne_zero.2 h.symm)]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
h : slope f a b = 0
⊢ f a = f b
[PROOFSTEP]
rw [← sub_smul_slope_vadd f a b, h, smul_zero, zero_vadd]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝⁶ : Field k
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module k E
inst✝³ : AddTorsor E PE
F : Type u_4
PF : Type u_5
inst✝² : AddCommGroup F
inst✝¹ : Module k F
inst✝ : AddTorsor F PF
f : PE →ᵃ[k] PF
g : k → PE
a b : k
⊢ slope (↑f ∘ g) a b = ↑f.linear (slope g a b)
[PROOFSTEP]
simp only [slope, (· ∘ ·), f.linear.map_smul, f.linearMap_vsub]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
⊢ slope f a b = slope f b a
[PROOFSTEP]
rw [slope, slope, ← neg_vsub_eq_vsub_rev, smul_neg, ← neg_smul, neg_inv, neg_sub]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
[PROOFSTEP]
by_cases hab : a = b
[GOAL]
case pos
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
hab : a = b
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
[PROOFSTEP]
subst hab
[GOAL]
case pos
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a c : k
⊢ ((a - a) / (c - a)) • slope f a a + ((c - a) / (c - a)) • slope f a c = slope f a c
[PROOFSTEP]
rw [sub_self, zero_div, zero_smul, zero_add]
[GOAL]
case pos
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a c : k
⊢ ((c - a) / (c - a)) • slope f a c = slope f a c
[PROOFSTEP]
by_cases hac : a = c
[GOAL]
case pos
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a c : k
hac : a = c
⊢ ((c - a) / (c - a)) • slope f a c = slope f a c
[PROOFSTEP]
simp [hac]
[GOAL]
case neg
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a c : k
hac : ¬a = c
⊢ ((c - a) / (c - a)) • slope f a c = slope f a c
[PROOFSTEP]
rw [div_self (sub_ne_zero.2 <| Ne.symm hac), one_smul]
[GOAL]
case neg
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
[PROOFSTEP]
by_cases hbc : b = c
[GOAL]
case pos
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : b = c
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
[PROOFSTEP]
subst hbc
[GOAL]
case pos
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
hab : ¬a = b
⊢ ((b - a) / (b - a)) • slope f a b + ((b - b) / (b - a)) • slope f b b = slope f a b
[PROOFSTEP]
simp [sub_ne_zero.2 (Ne.symm hab)]
[GOAL]
case neg
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : ¬b = c
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
[PROOFSTEP]
rw [add_comm]
[GOAL]
case neg
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : ¬b = c
⊢ ((c - b) / (c - a)) • slope f b c + ((b - a) / (c - a)) • slope f a b = slope f a c
[PROOFSTEP]
simp_rw [slope, div_eq_inv_mul, mul_smul, ← smul_add, smul_inv_smul₀ (sub_ne_zero.2 <| Ne.symm hab),
  smul_inv_smul₀ (sub_ne_zero.2 <| Ne.symm hbc), vsub_add_vsub_cancel]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
h : a ≠ c
⊢ ↑(lineMap (slope f a b) (slope f b c)) ((c - b) / (c - a)) = slope f a c
[PROOFSTEP]
field_simp [sub_ne_zero.2 h.symm, ← sub_div_sub_smul_slope_add_sub_div_sub_smul_slope f a b c, lineMap_apply_module]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
⊢ ↑(lineMap (slope f (↑(lineMap a b) r) b) (slope f a (↑(lineMap a b) r))) r = slope f a b
[PROOFSTEP]
obtain rfl | hab : a = b ∨ a ≠ b := Classical.em _
[GOAL]
case inl
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a r : k
⊢ ↑(lineMap (slope f (↑(lineMap a a) r) a) (slope f a (↑(lineMap a a) r))) r = slope f a a
[PROOFSTEP]
simp
[GOAL]
case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ ↑(lineMap (slope f (↑(lineMap a b) r) b) (slope f a (↑(lineMap a b) r))) r = slope f a b
[PROOFSTEP]
rw [slope_comm _ a, slope_comm _ a, slope_comm _ _ b]
[GOAL]
case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ ↑(lineMap (slope f b (↑(lineMap a b) r)) (slope f (↑(lineMap a b) r) a)) r = slope f b a
[PROOFSTEP]
convert lineMap_slope_slope_sub_div_sub f b (lineMap a b r) a hab.symm using 2
[GOAL]
case h.e'_2.h.e'_6
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ r = (a - ↑(lineMap a b) r) / (a - b)
[PROOFSTEP]
rw [lineMap_apply_ring, eq_div_iff (sub_ne_zero.2 hab), sub_mul, one_mul, mul_sub, ← sub_sub, sub_sub_cancel]