[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
x : P × P × P
hx12 : x.fst ≠ x.snd.fst
hx32 : x.snd.snd ≠ x.snd.fst
⊢ ContinuousAt (fun y => ∡ y.fst y.snd.fst y.snd.snd) x
[PROOFSTEP]
let f : P × P × P → V × V := fun y => (y.1 -ᵥ y.2.1, y.2.2 -ᵥ y.2.1)
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
x : P × P × P
hx12 : x.fst ≠ x.snd.fst
hx32 : x.snd.snd ≠ x.snd.fst
f : P × P × P → V × V := fun y => (y.fst -ᵥ y.snd.fst, y.snd.snd -ᵥ y.snd.fst)
⊢ ContinuousAt (fun y => ∡ y.fst y.snd.fst y.snd.snd) x
[PROOFSTEP]
have hf1 : (f x).1 ≠ 0 := by simp [hx12]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
x : P × P × P
hx12 : x.fst ≠ x.snd.fst
hx32 : x.snd.snd ≠ x.snd.fst
f : P × P × P → V × V := fun y => (y.fst -ᵥ y.snd.fst, y.snd.snd -ᵥ y.snd.fst)
⊢ (f x).fst ≠ 0
[PROOFSTEP]
simp [hx12]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
x : P × P × P
hx12 : x.fst ≠ x.snd.fst
hx32 : x.snd.snd ≠ x.snd.fst
f : P × P × P → V × V := fun y => (y.fst -ᵥ y.snd.fst, y.snd.snd -ᵥ y.snd.fst)
hf1 : (f x).fst ≠ 0
⊢ ContinuousAt (fun y => ∡ y.fst y.snd.fst y.snd.snd) x
[PROOFSTEP]
have hf2 : (f x).2 ≠ 0 := by simp [hx32]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
x : P × P × P
hx12 : x.fst ≠ x.snd.fst
hx32 : x.snd.snd ≠ x.snd.fst
f : P × P × P → V × V := fun y => (y.fst -ᵥ y.snd.fst, y.snd.snd -ᵥ y.snd.fst)
hf1 : (f x).fst ≠ 0
⊢ (f x).snd ≠ 0
[PROOFSTEP]
simp [hx32]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
x : P × P × P
hx12 : x.fst ≠ x.snd.fst
hx32 : x.snd.snd ≠ x.snd.fst
f : P × P × P → V × V := fun y => (y.fst -ᵥ y.snd.fst, y.snd.snd -ᵥ y.snd.fst)
hf1 : (f x).fst ≠ 0
hf2 : (f x).snd ≠ 0
⊢ ContinuousAt (fun y => ∡ y.fst y.snd.fst y.snd.snd) x
[PROOFSTEP]
exact
  (o.continuousAt_oangle hf1 hf2).comp
    ((continuous_fst.vsub continuous_snd.fst).prod_mk (continuous_snd.snd.vsub continuous_snd.fst)).continuousAt
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ : P
⊢ ∡ p₁ p₁ p₂ = 0
[PROOFSTEP]
simp [oangle]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ : P
⊢ ∡ p₁ p₂ p₂ = 0
[PROOFSTEP]
simp [oangle]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₁ ≠ p₂
[PROOFSTEP]
rw [← @vsub_ne_zero V]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₁ -ᵥ p₂ ≠ 0
[PROOFSTEP]
exact o.left_ne_zero_of_oangle_ne_zero h
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₃ ≠ p₂
[PROOFSTEP]
rw [← @vsub_ne_zero V]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₃ -ᵥ p₂ ≠ 0
[PROOFSTEP]
exact o.right_ne_zero_of_oangle_ne_zero h
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₁ ≠ p₃
[PROOFSTEP]
rw [← (vsub_left_injective p₂).ne_iff]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₁ -ᵥ p₂ ≠ p₃ -ᵥ p₂
[PROOFSTEP]
exact o.ne_of_oangle_ne_zero h
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : Real.Angle.sign (∡ p₁ p₂ p₃) = 1
⊢ 1 ≠ 0
[PROOFSTEP]
decide
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : Real.Angle.sign (∡ p₁ p₂ p₃) = 1
⊢ 1 ≠ 0
[PROOFSTEP]
decide
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : Real.Angle.sign (∡ p₁ p₂ p₃) = 1
⊢ 1 ≠ 0
[PROOFSTEP]
decide
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : Real.Angle.sign (∡ p₁ p₂ p₃) = -1
⊢ -1 ≠ 0
[PROOFSTEP]
decide
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : Real.Angle.sign (∡ p₁ p₂ p₃) = -1
⊢ -1 ≠ 0
[PROOFSTEP]
decide
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : Real.Angle.sign (∡ p₁ p₂ p₃) = -1
⊢ -1 ≠ 0
[PROOFSTEP]
decide
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ p₁ p₂ p₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ ↑π ↔ AffineIndependent ℝ ![p₁, p₂, p₃]
[PROOFSTEP]
rw [oangle, o.oangle_ne_zero_and_ne_pi_iff_linearIndependent,
  affineIndependent_iff_linearIndependent_vsub ℝ _ (1 : Fin 3), ←
  linearIndependent_equiv (finSuccAboveEquiv (1 : Fin 3)).toEquiv]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ LinearIndependent ℝ ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] ↔
    LinearIndependent ℝ
      ((fun i => Matrix.vecCons p₁ ![p₂, p₃] ↑i -ᵥ Matrix.vecCons p₁ ![p₂, p₃] 1) ∘ ↑(finSuccAboveEquiv 1).toEquiv)
[PROOFSTEP]
convert Iff.rfl
[GOAL]
case h.e'_2.h.e'_4
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ (fun i => Matrix.vecCons p₁ ![p₂, p₃] ↑i -ᵥ Matrix.vecCons p₁ ![p₂, p₃] 1) ∘ ↑(finSuccAboveEquiv 1).toEquiv =
    ![p₁ -ᵥ p₂, p₃ -ᵥ p₂]
[PROOFSTEP]
ext i
[GOAL]
case h.e'_2.h.e'_4.h
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
i : Fin 2
⊢ ((fun i => Matrix.vecCons p₁ ![p₂, p₃] ↑i -ᵥ Matrix.vecCons p₁ ![p₂, p₃] 1) ∘ ↑(finSuccAboveEquiv 1).toEquiv) i =
    Matrix.vecCons (p₁ -ᵥ p₂) ![p₃ -ᵥ p₂] i
[PROOFSTEP]
fin_cases i
[GOAL]
case h.e'_2.h.e'_4.h.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ((fun i => Matrix.vecCons p₁ ![p₂, p₃] ↑i -ᵥ Matrix.vecCons p₁ ![p₂, p₃] 1) ∘ ↑(finSuccAboveEquiv 1).toEquiv)
      { val := 0, isLt := (_ : 0 < 2) } =
    Matrix.vecCons (p₁ -ᵥ p₂) ![p₃ -ᵥ p₂] { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2.h.e'_4.h.tail.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ((fun i => Matrix.vecCons p₁ ![p₂, p₃] ↑i -ᵥ Matrix.vecCons p₁ ![p₂, p₃] 1) ∘ ↑(finSuccAboveEquiv 1).toEquiv)
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    Matrix.vecCons (p₁ -ᵥ p₂) ![p₃ -ᵥ p₂] { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
rfl
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ p₁ p₂ p₃ = 0 ∨ ∡ p₁ p₂ p₃ = ↑π ↔ Collinear ℝ {p₁, p₂, p₃}
[PROOFSTEP]
rw [← not_iff_not, not_or, oangle_ne_zero_and_ne_pi_iff_affineIndependent, affineIndependent_iff_not_collinear_set]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆
⊢ AffineIndependent ℝ ![p₁, p₂, p₃] ↔ AffineIndependent ℝ ![p₄, p₅, p₆]
[PROOFSTEP]
simp_rw [← oangle_ne_zero_and_ne_pi_iff_affineIndependent, ← Real.Angle.two_zsmul_ne_zero_iff, h]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆
⊢ Collinear ℝ {p₁, p₂, p₃} ↔ Collinear ℝ {p₄, p₅, p₆}
[PROOFSTEP]
simp_rw [← oangle_eq_zero_or_eq_pi_iff_collinear, ← Real.Angle.two_zsmul_eq_zero_iff, h]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : vectorSpan ℝ {p₁, p₂} = vectorSpan ℝ {p₄, p₅}
h₃₂₆₅ : vectorSpan ℝ {p₃, p₂} = vectorSpan ℝ {p₆, p₅}
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆
[PROOFSTEP]
simp_rw [vectorSpan_pair] at h₁₂₄₅ h₃₂₆₅ 
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : Submodule.span ℝ {p₁ -ᵥ p₂} = Submodule.span ℝ {p₄ -ᵥ p₅}
h₃₂₆₅ : Submodule.span ℝ {p₃ -ᵥ p₂} = Submodule.span ℝ {p₆ -ᵥ p₅}
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆
[PROOFSTEP]
exact o.two_zsmul_oangle_of_span_eq_of_span_eq h₁₂₄₅ h₃₂₆₅
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : affineSpan ℝ {p₁, p₂} ∥ affineSpan ℝ {p₄, p₅}
h₃₂₆₅ : affineSpan ℝ {p₃, p₂} ∥ affineSpan ℝ {p₆, p₅}
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆
[PROOFSTEP]
rw [AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq] at h₁₂₄₅ h₃₂₆₅ 
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : vectorSpan ℝ {p₁, p₂} = vectorSpan ℝ {p₄, p₅}
h₃₂₆₅ : vectorSpan ℝ {p₃, p₂} = vectorSpan ℝ {p₆, p₅}
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆
[PROOFSTEP]
exact two_zsmul_oangle_of_vectorSpan_eq h₁₂₄₅ h₃₂₆₅
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : dist p₁ p₂ = dist p₁ p₃
⊢ ∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁
[PROOFSTEP]
simp_rw [dist_eq_norm_vsub V] at h 
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁
[PROOFSTEP]
rw [oangle, oangle, ← vsub_sub_vsub_cancel_left p₃ p₂ p₁, ← vsub_sub_vsub_cancel_left p₂ p₃ p₁,
  o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : dist p₁ p₂ = dist p₁ p₃
⊢ ∡ p₃ p₁ p₂ = ↑π - 2 • ∡ p₁ p₂ p₃
[PROOFSTEP]
simp_rw [dist_eq_norm_vsub V] at h 
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ∡ p₃ p₁ p₂ = ↑π - 2 • ∡ p₁ p₂ p₃
[PROOFSTEP]
rw [oangle, oangle]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ Orientation.oangle o (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) = ↑π - 2 • Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
[PROOFSTEP]
convert o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq _ h using 1
[GOAL]
case h.e'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ Orientation.oangle o (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) = Orientation.oangle o (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
[PROOFSTEP]
rw [← neg_vsub_eq_vsub_rev p₁ p₃, ← neg_vsub_eq_vsub_rev p₁ p₂, o.oangle_neg_neg]
[GOAL]
case h.e'_3
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ↑π - 2 • Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ↑π - 2 • Orientation.oangle o (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃)
[PROOFSTEP]
rw [← o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]
[GOAL]
case h.e'_3
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ↑π - 2 • Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ↑π - 2 • Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃))
[PROOFSTEP]
simp
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₁ -ᵥ p₂ ≠ p₁ -ᵥ p₃
[PROOFSTEP]
simpa using hn
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : dist p₁ p₂ = dist p₁ p₃
⊢ |Real.Angle.toReal (∡ p₁ p₂ p₃)| < π / 2
[PROOFSTEP]
simp_rw [dist_eq_norm_vsub V] at h 
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ |Real.Angle.toReal (∡ p₁ p₂ p₃)| < π / 2
[PROOFSTEP]
rw [oangle, ← vsub_sub_vsub_cancel_left p₃ p₂ p₁]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ |Real.Angle.toReal (Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)))| < π / 2
[PROOFSTEP]
exact o.abs_oangle_sub_right_toReal_lt_pi_div_two h
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p p₁ p₂ : P
h : Real.Angle.sign (∡ p₁ p p₂) = 0
⊢ p₁ = p ∨ p₂ = p ∨ ∠ p₁ p p₂ = 0 ∨ ∠ p₁ p p₂ = π
[PROOFSTEP]
convert o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero h
[GOAL]
case h.e'_1.a
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p p₁ p₂ : P
h : Real.Angle.sign (∡ p₁ p p₂) = 0
⊢ p₁ = p ↔ p₁ -ᵥ p = 0
[PROOFSTEP]
simp
[GOAL]
case h.e'_2.h.e'_1.a
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p p₁ p₂ : P
h : Real.Angle.sign (∡ p₁ p p₂) = 0
⊢ p₂ = p ↔ p₂ -ᵥ p = 0
[PROOFSTEP]
simp
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∠ p₁ p₂ p₃ = π / 2
[PROOFSTEP]
rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ inner (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = 0
[PROOFSTEP]
exact o.inner_eq_zero_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∠ p₃ p₂ p₁ = π / 2
[PROOFSTEP]
rw [angle_comm]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∠ p₁ p₂ p₃ = π / 2
[PROOFSTEP]
exact angle_eq_pi_div_two_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(-π / 2)
⊢ ∠ p₁ p₂ p₃ = π / 2
[PROOFSTEP]
rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(-π / 2)
⊢ inner (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = 0
[PROOFSTEP]
exact o.inner_eq_zero_of_oangle_eq_neg_pi_div_two h
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(-π / 2)
⊢ ∠ p₃ p₂ p₁ = π / 2
[PROOFSTEP]
rw [angle_comm]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(-π / 2)
⊢ ∠ p₁ p₂ p₃ = π / 2
[PROOFSTEP]
exact angle_eq_pi_div_two_of_oangle_eq_neg_pi_div_two h
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ -Real.Angle.sign (∡ p₁ p₂ p₃) = Real.Angle.sign (∡ p₂ p₁ p₃)
[PROOFSTEP]
rw [eq_comm, oangle, oangle, ← o.oangle_neg_neg, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev, ←
  vsub_sub_vsub_cancel_left p₁ p₃ p₂, ← neg_vsub_eq_vsub_rev p₃ p₂, sub_eq_add_neg, neg_vsub_eq_vsub_rev p₂ p₁,
  add_comm, ← @neg_one_smul ℝ]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ Real.Angle.sign (Orientation.oangle o (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ + -1 • (p₃ -ᵥ p₂))) =
    -Real.Angle.sign (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂))
[PROOFSTEP]
nth_rw 2 [← one_smul ℝ (p₁ -ᵥ p₂)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ Real.Angle.sign (Orientation.oangle o (p₁ -ᵥ p₂) (1 • (p₁ -ᵥ p₂) + -1 • (p₃ -ᵥ p₂))) =
    -Real.Angle.sign (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂))
[PROOFSTEP]
rw [o.oangle_sign_smul_add_smul_right]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ↑SignType.sign (-1) * Real.Angle.sign (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    -Real.Angle.sign (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂))
[PROOFSTEP]
simp
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ -Real.Angle.sign (∡ p₁ p₂ p₃) = Real.Angle.sign (∡ p₃ p₂ p₁)
[PROOFSTEP]
rw [oangle_rev, Real.Angle.sign_neg, neg_neg]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ -Real.Angle.sign (∡ p₁ p₂ p₃) = Real.Angle.sign (∡ p₁ p₃ p₂)
[PROOFSTEP]
rw [oangle_swap₁₃_sign, ← oangle_swap₁₂_sign, oangle_swap₁₃_sign]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ Real.Angle.sign (∡ p₂ p₃ p₁) = Real.Angle.sign (∡ p₁ p₂ p₃)
[PROOFSTEP]
rw [← oangle_swap₁₂_sign, oangle_swap₁₃_sign]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ p₁ p₂ p₃ = ↑π ↔ Sbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
rw [oangle_eq_pi_iff_angle_eq_pi, angle_eq_pi_iff_sbtw]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ ∡ p₃ p₂ p₁ = ↑π
[PROOFSTEP]
rw [oangle_eq_pi_iff_oangle_rev_eq_pi, ← h.oangle₁₂₃_eq_pi]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
⊢ ∡ p₂ p₁ p₃ = 0
[PROOFSTEP]
by_cases hp₂p₁ : p₂ = p₁
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : p₂ = p₁
⊢ ∡ p₂ p₁ p₃ = 0
[PROOFSTEP]
simp [hp₂p₁]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : ¬p₂ = p₁
⊢ ∡ p₂ p₁ p₃ = 0
[PROOFSTEP]
by_cases hp₃p₁ : p₃ = p₁
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : ¬p₂ = p₁
hp₃p₁ : p₃ = p₁
⊢ ∡ p₂ p₁ p₃ = 0
[PROOFSTEP]
simp [hp₃p₁]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : ¬p₂ = p₁
hp₃p₁ : ¬p₃ = p₁
⊢ ∡ p₂ p₁ p₃ = 0
[PROOFSTEP]
rw [oangle_eq_zero_iff_angle_eq_zero hp₂p₁ hp₃p₁]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : ¬p₂ = p₁
hp₃p₁ : ¬p₃ = p₁
⊢ ∠ p₂ p₁ p₃ = 0
[PROOFSTEP]
exact h.angle₂₁₃_eq_zero_of_ne hp₂p₁
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
⊢ ∡ p₃ p₁ p₂ = 0
[PROOFSTEP]
rw [oangle_eq_zero_iff_oangle_rev_eq_zero, h.oangle₂₁₃_eq_zero]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
[PROOFSTEP]
by_cases hp₁p₂ : p₁ = p₂
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hp₁p₂ : p₁ = p₂
⊢ ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
[PROOFSTEP]
simp [hp₁p₂]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hp₁p₂ : ¬p₁ = p₂
⊢ ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
[PROOFSTEP]
by_cases hp₃p₂ : p₃ = p₂
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hp₁p₂ : ¬p₁ = p₂
hp₃p₂ : p₃ = p₂
⊢ ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
[PROOFSTEP]
simp [hp₃p₂]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hp₁p₂ : ¬p₁ = p₂
hp₃p₂ : ¬p₃ = p₂
⊢ ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
[PROOFSTEP]
rw [oangle_eq_zero_iff_angle_eq_zero hp₁p₂ hp₃p₂, angle_eq_zero_iff_ne_and_wbtw]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hp₁p₂ : ¬p₁ = p₂
hp₃p₂ : ¬p₃ = p₂
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
[PROOFSTEP]
simp [hp₁p₂, hp₃p₂]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Wbtw ℝ p₂ p₁ p₁'
hp₁p₂ : p₁ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃
[PROOFSTEP]
by_cases hp₃p₂ : p₃ = p₂
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Wbtw ℝ p₂ p₁ p₁'
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ = p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃
[PROOFSTEP]
simp [hp₃p₂]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Wbtw ℝ p₂ p₁ p₁'
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : ¬p₃ = p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃
[PROOFSTEP]
by_cases hp₁'p₂ : p₁' = p₂
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Wbtw ℝ p₂ p₁ p₁'
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hp₁'p₂ : p₁' = p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃
[PROOFSTEP]
rw [hp₁'p₂, wbtw_self_iff] at h 
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : p₁ = p₂
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hp₁'p₂ : p₁' = p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃
[PROOFSTEP]
exact False.elim (hp₁p₂ h)
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Wbtw ℝ p₂ p₁ p₁'
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hp₁'p₂ : ¬p₁' = p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃
[PROOFSTEP]
rw [← oangle_add hp₁'p₂ hp₁p₂ hp₃p₂, h.oangle₃₁₂_eq_zero, zero_add]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₃' : P
h : Wbtw ℝ p₂ p₃ p₃'
hp₃p₂ : p₃ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃'
[PROOFSTEP]
rw [oangle_rev, h.oangle_eq_left hp₃p₂, ← oangle_rev]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃
[PROOFSTEP]
by_cases h : p₁ = p₂
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : p₁ = p₂
⊢ ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃
[PROOFSTEP]
simp [h]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ¬p₁ = p₂
⊢ ∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃
[PROOFSTEP]
exact (sbtw_midpoint_of_ne ℝ h).symm.oangle_eq_left
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ (midpoint ℝ p₂ p₁) p₂ p₃ = ∡ p₁ p₂ p₃
[PROOFSTEP]
rw [midpoint_comm, oangle_midpoint_left]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃
[PROOFSTEP]
by_cases h : p₃ = p₂
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : p₃ = p₂
⊢ ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃
[PROOFSTEP]
simp [h]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ¬p₃ = p₂
⊢ ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃
[PROOFSTEP]
exact (sbtw_midpoint_of_ne ℝ h).symm.oangle_eq_right
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ p₁ p₂ (midpoint ℝ p₂ p₃) = ∡ p₁ p₂ p₃
[PROOFSTEP]
rw [midpoint_comm, oangle_midpoint_right]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₁'
hp₃p₂ : p₃ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃ + ↑π
[PROOFSTEP]
rw [← h.oangle₁₂₃_eq_pi, oangle_add_swap h.left_ne h.right_ne hp₃p₂]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₃' : P
h : Sbtw ℝ p₃ p₂ p₃'
hp₁p₂ : p₁ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃' + ↑π
[PROOFSTEP]
rw [← h.oangle₃₂₁_eq_pi, oangle_add hp₁p₂ h.right_ne h.left_ne]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ p₃' : P
h₁ : Sbtw ℝ p₁ p₂ p₁'
h₃ : Sbtw ℝ p₃ p₂ p₃'
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃'
[PROOFSTEP]
rw [h₁.oangle_eq_add_pi_left h₃.left_ne, h₃.oangle_eq_add_pi_right h₁.right_ne, add_assoc, Real.Angle.coe_pi_add_coe_pi,
  add_zero]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃
[PROOFSTEP]
by_cases hp₃p₂ : p₃ = p₂
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : p₃ = p₂
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃
[PROOFSTEP]
simp [hp₃p₂]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃
[PROOFSTEP]
rcases h.wbtw_or_wbtw_or_wbtw with (hw | hw | hw)
[GOAL]
case neg.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁ p₂ p₁'
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃
[PROOFSTEP]
have hw' : Sbtw ℝ p₁ p₂ p₁' := ⟨hw, hp₁p₂.symm, hp₁'p₂.symm⟩
[GOAL]
case neg.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁ p₂ p₁'
hw' : Sbtw ℝ p₁ p₂ p₁'
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃
[PROOFSTEP]
rw [hw'.oangle_eq_add_pi_left hp₃p₂, smul_add, Real.Angle.two_zsmul_coe_pi, add_zero]
[GOAL]
case neg.inr.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₂ p₁' p₁
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃
[PROOFSTEP]
rw [hw.oangle_eq_left hp₁'p₂]
[GOAL]
case neg.inr.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁' p₁ p₂
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃
[PROOFSTEP]
rw [hw.symm.oangle_eq_left hp₁p₂]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₃' : P
h : Collinear ℝ {p₃, p₂, p₃'}
hp₃p₂ : p₃ ≠ p₂
hp₃'p₂ : p₃' ≠ p₂
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁ p₂ p₃'
[PROOFSTEP]
rw [oangle_rev, smul_neg, h.two_zsmul_oangle_eq_left hp₃p₂ hp₃'p₂, ← smul_neg, ← oangle_rev]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
⊢ dist p₁ p = dist p₂ p ↔ ∃ r, r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p
[PROOFSTEP]
refine' ⟨fun hd => _, fun hr => _⟩
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd : dist p₁ p = dist p₂ p
⊢ ∃ r, r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p
[PROOFSTEP]
have hi : ⟪p₂ -ᵥ p₁, p -ᵥ midpoint ℝ p₁ p₂⟫ = 0 :=
  by
  rw [@dist_eq_norm_vsub' V, @dist_eq_norm_vsub' V, ← mul_self_inj (norm_nonneg _) (norm_nonneg _), ←
    real_inner_self_eq_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm] at hd 
  simp_rw [vsub_midpoint, ← vsub_sub_vsub_cancel_left p₂ p₁ p, inner_sub_left, inner_add_right, inner_smul_right, hd,
    real_inner_comm (p -ᵥ p₁)]
  abel
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd : dist p₁ p = dist p₂ p
⊢ inner (p₂ -ᵥ p₁) (p -ᵥ midpoint ℝ p₁ p₂) = 0
[PROOFSTEP]
rw [@dist_eq_norm_vsub' V, @dist_eq_norm_vsub' V, ← mul_self_inj (norm_nonneg _) (norm_nonneg _), ←
  real_inner_self_eq_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm] at hd 
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd✝¹ : ‖p -ᵥ p₁‖ * ‖p -ᵥ p₁‖ = ‖p -ᵥ p₂‖ * ‖p -ᵥ p₂‖
hd✝ : inner (p -ᵥ p₁) (p -ᵥ p₁) = ‖p -ᵥ p₂‖ * ‖p -ᵥ p₂‖
hd : inner (p -ᵥ p₁) (p -ᵥ p₁) = inner (p -ᵥ p₂) (p -ᵥ p₂)
⊢ inner (p₂ -ᵥ p₁) (p -ᵥ midpoint ℝ p₁ p₂) = 0
[PROOFSTEP]
simp_rw [vsub_midpoint, ← vsub_sub_vsub_cancel_left p₂ p₁ p, inner_sub_left, inner_add_right, inner_smul_right, hd,
  real_inner_comm (p -ᵥ p₁)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd✝¹ : ‖p -ᵥ p₁‖ * ‖p -ᵥ p₁‖ = ‖p -ᵥ p₂‖ * ‖p -ᵥ p₂‖
hd✝ : inner (p -ᵥ p₁) (p -ᵥ p₁) = ‖p -ᵥ p₂‖ * ‖p -ᵥ p₂‖
hd : inner (p -ᵥ p₁) (p -ᵥ p₁) = inner (p -ᵥ p₂) (p -ᵥ p₂)
⊢ ⅟2 * inner (p -ᵥ p₂) (p -ᵥ p₂) + ⅟2 * inner (p -ᵥ p₁) (p -ᵥ p₂) -
      (⅟2 * inner (p -ᵥ p₁) (p -ᵥ p₂) + ⅟2 * inner (p -ᵥ p₂) (p -ᵥ p₂)) =
    0
[PROOFSTEP]
abel
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd✝¹ : ‖p -ᵥ p₁‖ * ‖p -ᵥ p₁‖ = ‖p -ᵥ p₂‖ * ‖p -ᵥ p₂‖
hd✝ : inner (p -ᵥ p₁) (p -ᵥ p₁) = ‖p -ᵥ p₂‖ * ‖p -ᵥ p₂‖
hd : inner (p -ᵥ p₁) (p -ᵥ p₁) = inner (p -ᵥ p₂) (p -ᵥ p₂)
⊢ ⅟2 * inner (p -ᵥ p₂) (p -ᵥ p₂) + ⅟2 * inner (p -ᵥ p₁) (p -ᵥ p₂) -
      (⅟2 * inner (p -ᵥ p₁) (p -ᵥ p₂) + ⅟2 * inner (p -ᵥ p₂) (p -ᵥ p₂)) =
    0
[PROOFSTEP]
abel
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd : dist p₁ p = dist p₂ p
hi : inner (p₂ -ᵥ p₁) (p -ᵥ midpoint ℝ p₁ p₂) = 0
⊢ ∃ r, r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p
[PROOFSTEP]
rw [@Orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two V _ _ _ o,
  or_iff_right (vsub_ne_zero.2 h.symm)] at hi 
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd : dist p₁ p = dist p₂ p
hi : ∃ r, r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) = p -ᵥ midpoint ℝ p₁ p₂
⊢ ∃ r, r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p
[PROOFSTEP]
rcases hi with ⟨r, hr⟩
[GOAL]
case refine'_1.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd : dist p₁ p = dist p₂ p
r : ℝ
hr : r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) = p -ᵥ midpoint ℝ p₁ p₂
⊢ ∃ r, r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p
[PROOFSTEP]
rw [eq_comm, ← eq_vadd_iff_vsub_eq] at hr 
[GOAL]
case refine'_1.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd : dist p₁ p = dist p₂ p
r : ℝ
hr : p = r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂
⊢ ∃ r, r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p
[PROOFSTEP]
exact ⟨r, hr.symm⟩
[GOAL]
case refine'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hr : ∃ r, r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p
⊢ dist p₁ p = dist p₂ p
[PROOFSTEP]
rcases hr with ⟨r, rfl⟩
[GOAL]
case refine'_2.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ : P
h : p₁ ≠ p₂
r : ℝ
⊢ dist p₁ (r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂) =
    dist p₂ (r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂)
[PROOFSTEP]
simp_rw [@dist_eq_norm_vsub V, vsub_vadd_eq_vsub_sub, left_vsub_midpoint, right_vsub_midpoint, invOf_eq_inv, ←
  neg_vsub_eq_vsub_rev p₂ p₁, ← mul_self_inj (norm_nonneg _) (norm_nonneg _), ← real_inner_self_eq_norm_mul_norm,
  inner_sub_sub_self]
[GOAL]
case refine'_2.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ : P
h : p₁ ≠ p₂
r : ℝ
⊢ inner (2⁻¹ • -(p₂ -ᵥ p₁)) (2⁻¹ • -(p₂ -ᵥ p₁)) -
          inner (2⁻¹ • -(p₂ -ᵥ p₁)) (r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁)) -
        inner (r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁)) (2⁻¹ • -(p₂ -ᵥ p₁)) +
      inner (r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁)) (r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁)) =
    inner (2⁻¹ • (p₂ -ᵥ p₁)) (2⁻¹ • (p₂ -ᵥ p₁)) -
          inner (2⁻¹ • (p₂ -ᵥ p₁)) (r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁)) -
        inner (r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁)) (2⁻¹ • (p₂ -ᵥ p₁)) +
      inner (r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁)) (r • ↑(Orientation.rotation o ↑(π / 2)) (p₂ -ᵥ p₁))
[PROOFSTEP]
simp [-neg_vsub_eq_vsub_rev]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
⊢ Real.Angle.sign (∡ p₁ p₅ p₂) = Real.Angle.sign (∡ p₃ p₅ p₄)
[PROOFSTEP]
by_cases hc₅₁₂ : Collinear ℝ ({ p₅, p₁, p₂ } : Set P)
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ {p₅, p₁, p₂}
⊢ Real.Angle.sign (∡ p₁ p₅ p₂) = Real.Angle.sign (∡ p₃ p₅ p₄)
[PROOFSTEP]
have hc₅₁₂₃₄ : Collinear ℝ ({ p₅, p₁, p₂, p₃, p₄ } : Set P) :=
  (hc.collinear_insert_iff_of_ne (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_insert _ _)) hp₁p₂).2 hc₅₁₂
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ {p₅, p₁, p₂}
hc₅₁₂₃₄ : Collinear ℝ {p₅, p₁, p₂, p₃, p₄}
⊢ Real.Angle.sign (∡ p₁ p₅ p₂) = Real.Angle.sign (∡ p₃ p₅ p₄)
[PROOFSTEP]
have hc₅₃₄ : Collinear ℝ ({ p₅, p₃, p₄ } : Set P) :=
  (hc.collinear_insert_iff_of_ne (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_insert _ _)))
        (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _)))) hp₃p₄).1
    hc₅₁₂₃₄
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ {p₅, p₁, p₂}
hc₅₁₂₃₄ : Collinear ℝ {p₅, p₁, p₂, p₃, p₄}
hc₅₃₄ : Collinear ℝ {p₅, p₃, p₄}
⊢ Real.Angle.sign (∡ p₁ p₅ p₂) = Real.Angle.sign (∡ p₃ p₅ p₄)
[PROOFSTEP]
rw [Set.insert_comm] at hc₅₁₂ hc₅₃₄ 
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ {p₁, p₅, p₂}
hc₅₁₂₃₄ : Collinear ℝ {p₅, p₁, p₂, p₃, p₄}
hc₅₃₄ : Collinear ℝ {p₃, p₅, p₄}
⊢ Real.Angle.sign (∡ p₁ p₅ p₂) = Real.Angle.sign (∡ p₃ p₅ p₄)
[PROOFSTEP]
have hs₁₅₂ := oangle_eq_zero_or_eq_pi_iff_collinear.2 hc₅₁₂
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ {p₁, p₅, p₂}
hc₅₁₂₃₄ : Collinear ℝ {p₅, p₁, p₂, p₃, p₄}
hc₅₃₄ : Collinear ℝ {p₃, p₅, p₄}
hs₁₅₂ : ∡ p₁ p₅ p₂ = 0 ∨ ∡ p₁ p₅ p₂ = ↑π
⊢ Real.Angle.sign (∡ p₁ p₅ p₂) = Real.Angle.sign (∡ p₃ p₅ p₄)
[PROOFSTEP]
have hs₃₅₄ := oangle_eq_zero_or_eq_pi_iff_collinear.2 hc₅₃₄
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ {p₁, p₅, p₂}
hc₅₁₂₃₄ : Collinear ℝ {p₅, p₁, p₂, p₃, p₄}
hc₅₃₄ : Collinear ℝ {p₃, p₅, p₄}
hs₁₅₂ : ∡ p₁ p₅ p₂ = 0 ∨ ∡ p₁ p₅ p₂ = ↑π
hs₃₅₄ : ∡ p₃ p₅ p₄ = 0 ∨ ∡ p₃ p₅ p₄ = ↑π
⊢ Real.Angle.sign (∡ p₁ p₅ p₂) = Real.Angle.sign (∡ p₃ p₅ p₄)
[PROOFSTEP]
rw [← Real.Angle.sign_eq_zero_iff] at hs₁₅₂ hs₃₅₄ 
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ {p₁, p₅, p₂}
hc₅₁₂₃₄ : Collinear ℝ {p₅, p₁, p₂, p₃, p₄}
hc₅₃₄ : Collinear ℝ {p₃, p₅, p₄}
hs₁₅₂ : Real.Angle.sign (∡ p₁ p₅ p₂) = 0
hs₃₅₄ : Real.Angle.sign (∡ p₃ p₅ p₄) = 0
⊢ Real.Angle.sign (∡ p₁ p₅ p₂) = Real.Angle.sign (∡ p₃ p₅ p₄)
[PROOFSTEP]
rw [hs₁₅₂, hs₃₅₄]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
⊢ Real.Angle.sign (∡ p₁ p₅ p₂) = Real.Angle.sign (∡ p₃ p₅ p₄)
[PROOFSTEP]
let s : Set (P × P × P) :=
  (fun x : line[ℝ, p₁, p₂] × V => (x.1, p₅, x.2 +ᵥ (x.1 : P))) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
⊢ Real.Angle.sign (∡ p₁ p₅ p₂) = Real.Angle.sign (∡ p₃ p₅ p₄)
[PROOFSTEP]
have hco : IsConnected s :=
  haveI : ConnectedSpace line[ℝ, p₁, p₂] := AddTorsor.connectedSpace _ _
  (isConnected_univ.prod (isConnected_setOf_sameRay_and_ne_zero (vsub_ne_zero.2 hp₁p₂.symm))).image _
    (continuous_fst.subtype_val.prod_mk
        (continuous_const.prod_mk (continuous_snd.vadd continuous_fst.subtype_val))).continuousOn
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
⊢ Real.Angle.sign (∡ p₁ p₅ p₂) = Real.Angle.sign (∡ p₃ p₅ p₄)
[PROOFSTEP]
have hf : ContinuousOn (fun p : P × P × P => ∡ p.1 p.2.1 p.2.2) s :=
  by
  refine' ContinuousAt.continuousOn fun p hp => continuousAt_oangle _ _
  all_goals
    simp_rw [Set.mem_image, Set.mem_prod, Set.mem_univ, true_and_iff, Prod.ext_iff] at hp 
    obtain ⟨q₁, q₅, q₂⟩ := p
    dsimp only at hp ⊢
    obtain ⟨⟨⟨q, hq⟩, v⟩, hv, rfl, rfl, rfl⟩ := hp
    dsimp only [Subtype.coe_mk, Set.mem_setOf] at hv ⊢
    obtain ⟨hvr, -⟩ := hv
    rintro rfl
    refine' hc₅₁₂ ((collinear_insert_iff_of_mem_affineSpan _).2 (collinear_pair _ _ _))
  · exact hq
  · refine' vadd_mem_of_mem_direction _ hq
    rw [← exists_nonneg_left_iff_sameRay (vsub_ne_zero.2 hp₁p₂.symm)] at hvr 
    obtain ⟨r, -, rfl⟩ := hvr
    rw [direction_affineSpan]
    exact smul_vsub_rev_mem_vectorSpan_pair _ _ _
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
⊢ ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
[PROOFSTEP]
refine' ContinuousAt.continuousOn fun p hp => continuousAt_oangle _ _
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
p : P × P × P
hp : p ∈ s
⊢ p.fst ≠ p.snd.fst
case refine'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
p : P × P × P
hp : p ∈ s
⊢ p.snd.snd ≠ p.snd.fst
[PROOFSTEP]
all_goals
  simp_rw [Set.mem_image, Set.mem_prod, Set.mem_univ, true_and_iff, Prod.ext_iff] at hp 
  obtain ⟨q₁, q₅, q₂⟩ := p
  dsimp only at hp ⊢
  obtain ⟨⟨⟨q, hq⟩, v⟩, hv, rfl, rfl, rfl⟩ := hp
  dsimp only [Subtype.coe_mk, Set.mem_setOf] at hv ⊢
  obtain ⟨hvr, -⟩ := hv
  rintro rfl
  refine' hc₅₁₂ ((collinear_insert_iff_of_mem_affineSpan _).2 (collinear_pair _ _ _))
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
p : P × P × P
hp : p ∈ s
⊢ p.fst ≠ p.snd.fst
[PROOFSTEP]
simp_rw [Set.mem_image, Set.mem_prod, Set.mem_univ, true_and_iff, Prod.ext_iff] at hp 
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
p : P × P × P
hp : ∃ x, x.snd ∈ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0} ∧ ↑x.fst = p.fst ∧ p₅ = p.snd.fst ∧ x.snd +ᵥ ↑x.fst = p.snd.snd
⊢ p.fst ≠ p.snd.fst
[PROOFSTEP]
obtain ⟨q₁, q₅, q₂⟩ := p
[GOAL]
case refine'_1.mk.mk
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
q₁ q₅ q₂ : P
hp :
  ∃ x,
    x.snd ∈ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0} ∧
      ↑x.fst = (q₁, q₅, q₂).fst ∧ p₅ = (q₁, q₅, q₂).snd.fst ∧ x.snd +ᵥ ↑x.fst = (q₁, q₅, q₂).snd.snd
⊢ (q₁, q₅, q₂).fst ≠ (q₁, q₅, q₂).snd.fst
[PROOFSTEP]
dsimp only at hp ⊢
[GOAL]
case refine'_1.mk.mk
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
q₁ q₅ q₂ : P
hp : ∃ x, x.snd ∈ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0} ∧ ↑x.fst = q₁ ∧ p₅ = q₅ ∧ x.snd +ᵥ ↑x.fst = q₂
⊢ q₁ ≠ q₅
[PROOFSTEP]
obtain ⟨⟨⟨q, hq⟩, v⟩, hv, rfl, rfl, rfl⟩ := hp
[GOAL]
case refine'_1.mk.mk.intro.mk.mk.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
v : V
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
hv : ({ val := q, property := hq }, v).snd ∈ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
⊢ ↑({ val := q, property := hq }, v).fst ≠ p₅
[PROOFSTEP]
dsimp only [Subtype.coe_mk, Set.mem_setOf] at hv ⊢
[GOAL]
case refine'_1.mk.mk.intro.mk.mk.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
v : V
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
hv : v ∈ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
⊢ q ≠ p₅
[PROOFSTEP]
obtain ⟨hvr, -⟩ := hv
[GOAL]
case refine'_1.mk.mk.intro.mk.mk.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
v : V
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
hvr : SameRay ℝ (p₂ -ᵥ p₁) v
⊢ q ≠ p₅
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1.mk.mk.intro.mk.mk.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
v : V
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
hvr : SameRay ℝ (p₂ -ᵥ p₁) v
hc₅₁₂ : ¬Collinear ℝ {q, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, q, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
⊢ False
[PROOFSTEP]
refine' hc₅₁₂ ((collinear_insert_iff_of_mem_affineSpan _).2 (collinear_pair _ _ _))
[GOAL]
case refine'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
p : P × P × P
hp : p ∈ s
⊢ p.snd.snd ≠ p.snd.fst
[PROOFSTEP]
simp_rw [Set.mem_image, Set.mem_prod, Set.mem_univ, true_and_iff, Prod.ext_iff] at hp 
[GOAL]
case refine'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
p : P × P × P
hp : ∃ x, x.snd ∈ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0} ∧ ↑x.fst = p.fst ∧ p₅ = p.snd.fst ∧ x.snd +ᵥ ↑x.fst = p.snd.snd
⊢ p.snd.snd ≠ p.snd.fst
[PROOFSTEP]
obtain ⟨q₁, q₅, q₂⟩ := p
[GOAL]
case refine'_2.mk.mk
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
q₁ q₅ q₂ : P
hp :
  ∃ x,
    x.snd ∈ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0} ∧
      ↑x.fst = (q₁, q₅, q₂).fst ∧ p₅ = (q₁, q₅, q₂).snd.fst ∧ x.snd +ᵥ ↑x.fst = (q₁, q₅, q₂).snd.snd
⊢ (q₁, q₅, q₂).snd.snd ≠ (q₁, q₅, q₂).snd.fst
[PROOFSTEP]
dsimp only at hp ⊢
[GOAL]
case refine'_2.mk.mk
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
q₁ q₅ q₂ : P
hp : ∃ x, x.snd ∈ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0} ∧ ↑x.fst = q₁ ∧ p₅ = q₅ ∧ x.snd +ᵥ ↑x.fst = q₂
⊢ q₂ ≠ q₅
[PROOFSTEP]
obtain ⟨⟨⟨q, hq⟩, v⟩, hv, rfl, rfl, rfl⟩ := hp
[GOAL]
case refine'_2.mk.mk.intro.mk.mk.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
v : V
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
hv : ({ val := q, property := hq }, v).snd ∈ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
⊢ ({ val := q, property := hq }, v).snd +ᵥ ↑({ val := q, property := hq }, v).fst ≠ p₅
[PROOFSTEP]
dsimp only [Subtype.coe_mk, Set.mem_setOf] at hv ⊢
[GOAL]
case refine'_2.mk.mk.intro.mk.mk.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
v : V
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
hv : v ∈ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
⊢ v +ᵥ q ≠ p₅
[PROOFSTEP]
obtain ⟨hvr, -⟩ := hv
[GOAL]
case refine'_2.mk.mk.intro.mk.mk.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
v : V
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
hvr : SameRay ℝ (p₂ -ᵥ p₁) v
⊢ v +ᵥ q ≠ p₅
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_2.mk.mk.intro.mk.mk.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
v : V
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
hvr : SameRay ℝ (p₂ -ᵥ p₁) v
hc₅₁₂ : ¬Collinear ℝ {v +ᵥ q, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, v +ᵥ q, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
⊢ False
[PROOFSTEP]
refine' hc₅₁₂ ((collinear_insert_iff_of_mem_affineSpan _).2 (collinear_pair _ _ _))
[GOAL]
case refine'_1.mk.mk.intro.mk.mk.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
v : V
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
hvr : SameRay ℝ (p₂ -ᵥ p₁) v
hc₅₁₂ : ¬Collinear ℝ {q, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, q, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
⊢ q ∈ affineSpan ℝ {p₁, p₂}
[PROOFSTEP]
exact hq
[GOAL]
case refine'_2.mk.mk.intro.mk.mk.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
v : V
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
hvr : SameRay ℝ (p₂ -ᵥ p₁) v
hc₅₁₂ : ¬Collinear ℝ {v +ᵥ q, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, v +ᵥ q, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
⊢ v +ᵥ q ∈ affineSpan ℝ {p₁, p₂}
[PROOFSTEP]
refine' vadd_mem_of_mem_direction _ hq
[GOAL]
case refine'_2.mk.mk.intro.mk.mk.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
v : V
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
hvr : SameRay ℝ (p₂ -ᵥ p₁) v
hc₅₁₂ : ¬Collinear ℝ {v +ᵥ q, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, v +ᵥ q, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
⊢ v ∈ direction (affineSpan ℝ {p₁, p₂})
[PROOFSTEP]
rw [← exists_nonneg_left_iff_sameRay (vsub_ne_zero.2 hp₁p₂.symm)] at hvr 
[GOAL]
case refine'_2.mk.mk.intro.mk.mk.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
v : V
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
hvr : ∃ r, 0 ≤ r ∧ r • (p₂ -ᵥ p₁) = v
hc₅₁₂ : ¬Collinear ℝ {v +ᵥ q, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, v +ᵥ q, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
⊢ v ∈ direction (affineSpan ℝ {p₁, p₂})
[PROOFSTEP]
obtain ⟨r, -, rfl⟩ := hvr
[GOAL]
case refine'_2.mk.mk.intro.mk.mk.intro.intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
r : ℝ
hc₅₁₂ : ¬Collinear ℝ {r • (p₂ -ᵥ p₁) +ᵥ q, p₁, p₂}
s : Set (P × P × P) :=
  (fun x => (↑x.fst, r • (p₂ -ᵥ p₁) +ᵥ q, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
⊢ r • (p₂ -ᵥ p₁) ∈ direction (affineSpan ℝ {p₁, p₂})
[PROOFSTEP]
rw [direction_affineSpan]
[GOAL]
case refine'_2.mk.mk.intro.mk.mk.intro.intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
r : ℝ
hc₅₁₂ : ¬Collinear ℝ {r • (p₂ -ᵥ p₁) +ᵥ q, p₁, p₂}
s : Set (P × P × P) :=
  (fun x => (↑x.fst, r • (p₂ -ᵥ p₁) +ᵥ q, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
⊢ r • (p₂ -ᵥ p₁) ∈ vectorSpan ℝ {p₁, p₂}
[PROOFSTEP]
exact smul_vsub_rev_mem_vectorSpan_pair _ _ _
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
⊢ Real.Angle.sign (∡ p₁ p₅ p₂) = Real.Angle.sign (∡ p₃ p₅ p₄)
[PROOFSTEP]
have hsp : ∀ p : P × P × P, p ∈ s → ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ π :=
  by
  intro p hp
  simp_rw [Set.mem_image, Set.mem_prod, Set.mem_setOf, Set.mem_univ, true_and_iff, Prod.ext_iff] at hp 
  obtain ⟨q₁, q₅, q₂⟩ := p
  dsimp only at hp ⊢
  obtain ⟨⟨⟨q, hq⟩, v⟩, hv, rfl, rfl, rfl⟩ := hp
  dsimp only [Subtype.coe_mk, Set.mem_setOf] at hv ⊢
  obtain ⟨hvr, hv0⟩ := hv
  rw [← exists_nonneg_left_iff_sameRay (vsub_ne_zero.2 hp₁p₂.symm)] at hvr 
  obtain ⟨r, -, rfl⟩ := hvr
  change q ∈ line[ℝ, p₁, p₂] at hq 
  rw [oangle_ne_zero_and_ne_pi_iff_affineIndependent]
  refine'
    affineIndependent_of_ne_of_mem_of_not_mem_of_mem _ hq
      (fun h => hc₅₁₂ ((collinear_insert_iff_of_mem_affineSpan h).2 (collinear_pair _ _ _))) _
  · rwa [← @vsub_ne_zero V, vsub_vadd_eq_vsub_sub, vsub_self, zero_sub, neg_ne_zero]
  · refine' vadd_mem_of_mem_direction _ hq
    rw [direction_affineSpan]
    exact smul_vsub_rev_mem_vectorSpan_pair _ _ _
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
⊢ ∀ (p : P × P × P), p ∈ s → ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
[PROOFSTEP]
intro p hp
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
p : P × P × P
hp : p ∈ s
⊢ ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
[PROOFSTEP]
simp_rw [Set.mem_image, Set.mem_prod, Set.mem_setOf, Set.mem_univ, true_and_iff, Prod.ext_iff] at hp 
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
p : P × P × P
hp : ∃ x, (SameRay ℝ (p₂ -ᵥ p₁) x.snd ∧ x.snd ≠ 0) ∧ ↑x.fst = p.fst ∧ p₅ = p.snd.fst ∧ x.snd +ᵥ ↑x.fst = p.snd.snd
⊢ ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
[PROOFSTEP]
obtain ⟨q₁, q₅, q₂⟩ := p
[GOAL]
case mk.mk
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
q₁ q₅ q₂ : P
hp :
  ∃ x,
    (SameRay ℝ (p₂ -ᵥ p₁) x.snd ∧ x.snd ≠ 0) ∧
      ↑x.fst = (q₁, q₅, q₂).fst ∧ p₅ = (q₁, q₅, q₂).snd.fst ∧ x.snd +ᵥ ↑x.fst = (q₁, q₅, q₂).snd.snd
⊢ ∡ (q₁, q₅, q₂).fst (q₁, q₅, q₂).snd.fst (q₁, q₅, q₂).snd.snd ≠ 0 ∧
    ∡ (q₁, q₅, q₂).fst (q₁, q₅, q₂).snd.fst (q₁, q₅, q₂).snd.snd ≠ ↑π
[PROOFSTEP]
dsimp only at hp ⊢
[GOAL]
case mk.mk
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
q₁ q₅ q₂ : P
hp : ∃ x, (SameRay ℝ (p₂ -ᵥ p₁) x.snd ∧ x.snd ≠ 0) ∧ ↑x.fst = q₁ ∧ p₅ = q₅ ∧ x.snd +ᵥ ↑x.fst = q₂
⊢ ∡ q₁ q₅ q₂ ≠ 0 ∧ ∡ q₁ q₅ q₂ ≠ ↑π
[PROOFSTEP]
obtain ⟨⟨⟨q, hq⟩, v⟩, hv, rfl, rfl, rfl⟩ := hp
[GOAL]
case mk.mk.intro.mk.mk.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
v : V
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
hv : SameRay ℝ (p₂ -ᵥ p₁) ({ val := q, property := hq }, v).snd ∧ ({ val := q, property := hq }, v).snd ≠ 0
⊢ ∡ (↑({ val := q, property := hq }, v).fst) p₅
        (({ val := q, property := hq }, v).snd +ᵥ ↑({ val := q, property := hq }, v).fst) ≠
      0 ∧
    ∡ (↑({ val := q, property := hq }, v).fst) p₅
        (({ val := q, property := hq }, v).snd +ᵥ ↑({ val := q, property := hq }, v).fst) ≠
      ↑π
[PROOFSTEP]
dsimp only [Subtype.coe_mk, Set.mem_setOf] at hv ⊢
[GOAL]
case mk.mk.intro.mk.mk.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
v : V
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
hv : SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0
⊢ ∡ q p₅ (v +ᵥ q) ≠ 0 ∧ ∡ q p₅ (v +ᵥ q) ≠ ↑π
[PROOFSTEP]
obtain ⟨hvr, hv0⟩ := hv
[GOAL]
case mk.mk.intro.mk.mk.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
v : V
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
hvr : SameRay ℝ (p₂ -ᵥ p₁) v
hv0 : v ≠ 0
⊢ ∡ q p₅ (v +ᵥ q) ≠ 0 ∧ ∡ q p₅ (v +ᵥ q) ≠ ↑π
[PROOFSTEP]
rw [← exists_nonneg_left_iff_sameRay (vsub_ne_zero.2 hp₁p₂.symm)] at hvr 
[GOAL]
case mk.mk.intro.mk.mk.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
v : V
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
hvr : ∃ r, 0 ≤ r ∧ r • (p₂ -ᵥ p₁) = v
hv0 : v ≠ 0
⊢ ∡ q p₅ (v +ᵥ q) ≠ 0 ∧ ∡ q p₅ (v +ᵥ q) ≠ ↑π
[PROOFSTEP]
obtain ⟨r, -, rfl⟩ := hvr
[GOAL]
case mk.mk.intro.mk.mk.intro.intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
q : P
hq : q ∈ affineSpan ℝ {p₁, p₂}
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
⊢ ∡ q p₅ (r • (p₂ -ᵥ p₁) +ᵥ q) ≠ 0 ∧ ∡ q p₅ (r • (p₂ -ᵥ p₁) +ᵥ q) ≠ ↑π
[PROOFSTEP]
change q ∈ line[ℝ, p₁, p₂] at hq 
[GOAL]
case mk.mk.intro.mk.mk.intro.intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
q : P
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
hq : q ∈ affineSpan ℝ {p₁, p₂}
⊢ ∡ q p₅ (r • (p₂ -ᵥ p₁) +ᵥ q) ≠ 0 ∧ ∡ q p₅ (r • (p₂ -ᵥ p₁) +ᵥ q) ≠ ↑π
[PROOFSTEP]
rw [oangle_ne_zero_and_ne_pi_iff_affineIndependent]
[GOAL]
case mk.mk.intro.mk.mk.intro.intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
q : P
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
hq : q ∈ affineSpan ℝ {p₁, p₂}
⊢ AffineIndependent ℝ ![q, p₅, r • (p₂ -ᵥ p₁) +ᵥ q]
[PROOFSTEP]
refine'
  affineIndependent_of_ne_of_mem_of_not_mem_of_mem _ hq
    (fun h => hc₅₁₂ ((collinear_insert_iff_of_mem_affineSpan h).2 (collinear_pair _ _ _))) _
[GOAL]
case mk.mk.intro.mk.mk.intro.intro.intro.intro.intro.intro.refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
q : P
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
hq : q ∈ affineSpan ℝ {p₁, p₂}
⊢ q ≠ r • (p₂ -ᵥ p₁) +ᵥ q
[PROOFSTEP]
rwa [← @vsub_ne_zero V, vsub_vadd_eq_vsub_sub, vsub_self, zero_sub, neg_ne_zero]
[GOAL]
case mk.mk.intro.mk.mk.intro.intro.intro.intro.intro.intro.refine'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
q : P
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
hq : q ∈ affineSpan ℝ {p₁, p₂}
⊢ r • (p₂ -ᵥ p₁) +ᵥ q ∈ affineSpan ℝ {p₁, p₂}
[PROOFSTEP]
refine' vadd_mem_of_mem_direction _ hq
[GOAL]
case mk.mk.intro.mk.mk.intro.intro.intro.intro.intro.intro.refine'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
q : P
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
hq : q ∈ affineSpan ℝ {p₁, p₂}
⊢ r • (p₂ -ᵥ p₁) ∈ direction (affineSpan ℝ {p₁, p₂})
[PROOFSTEP]
rw [direction_affineSpan]
[GOAL]
case mk.mk.intro.mk.mk.intro.intro.intro.intro.intro.intro.refine'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
q : P
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
hq : q ∈ affineSpan ℝ {p₁, p₂}
⊢ r • (p₂ -ᵥ p₁) ∈ vectorSpan ℝ {p₁, p₂}
[PROOFSTEP]
exact smul_vsub_rev_mem_vectorSpan_pair _ _ _
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
hsp : ∀ (p : P × P × P), p ∈ s → ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
⊢ Real.Angle.sign (∡ p₁ p₅ p₂) = Real.Angle.sign (∡ p₃ p₅ p₄)
[PROOFSTEP]
have hp₁p₂s : (p₁, p₅, p₂) ∈ s :=
  by
  simp_rw [Set.mem_image, Set.mem_prod, Set.mem_setOf, Set.mem_univ, true_and_iff, Prod.ext_iff]
  refine' ⟨⟨⟨p₁, left_mem_affineSpan_pair _ _ _⟩, p₂ -ᵥ p₁⟩, ⟨SameRay.rfl, vsub_ne_zero.2 hp₁p₂.symm⟩, _⟩
  simp
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
hsp : ∀ (p : P × P × P), p ∈ s → ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
⊢ (p₁, p₅, p₂) ∈ s
[PROOFSTEP]
simp_rw [Set.mem_image, Set.mem_prod, Set.mem_setOf, Set.mem_univ, true_and_iff, Prod.ext_iff]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
hsp : ∀ (p : P × P × P), p ∈ s → ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
⊢ ∃ x, (SameRay ℝ (p₂ -ᵥ p₁) x.snd ∧ x.snd ≠ 0) ∧ ↑x.fst = p₁ ∧ True ∧ x.snd +ᵥ ↑x.fst = p₂
[PROOFSTEP]
refine' ⟨⟨⟨p₁, left_mem_affineSpan_pair _ _ _⟩, p₂ -ᵥ p₁⟩, ⟨SameRay.rfl, vsub_ne_zero.2 hp₁p₂.symm⟩, _⟩
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
hsp : ∀ (p : P × P × P), p ∈ s → ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
⊢ ↑({ val := p₁, property := (_ : p₁ ∈ affineSpan ℝ {p₁, p₂}) }, p₂ -ᵥ p₁).fst = p₁ ∧
    True ∧
      ({ val := p₁, property := (_ : p₁ ∈ affineSpan ℝ {p₁, p₂}) }, p₂ -ᵥ p₁).snd +ᵥ
          ↑({ val := p₁, property := (_ : p₁ ∈ affineSpan ℝ {p₁, p₂}) }, p₂ -ᵥ p₁).fst =
        p₂
[PROOFSTEP]
simp
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
hsp : ∀ (p : P × P × P), p ∈ s → ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
hp₁p₂s : (p₁, p₅, p₂) ∈ s
⊢ Real.Angle.sign (∡ p₁ p₅ p₂) = Real.Angle.sign (∡ p₃ p₅ p₄)
[PROOFSTEP]
have hp₃p₄s : (p₃, p₅, p₄) ∈ s :=
  by
  simp_rw [Set.mem_image, Set.mem_prod, Set.mem_setOf, Set.mem_univ, true_and_iff, Prod.ext_iff]
  refine'
    ⟨⟨⟨p₃,
          hc.mem_affineSpan_of_mem_of_ne (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_insert _ _))
            (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_insert _ _))) hp₁p₂⟩,
        p₄ -ᵥ p₃⟩,
      ⟨hr, vsub_ne_zero.2 hp₃p₄.symm⟩, _⟩
  simp
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
hsp : ∀ (p : P × P × P), p ∈ s → ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
hp₁p₂s : (p₁, p₅, p₂) ∈ s
⊢ (p₃, p₅, p₄) ∈ s
[PROOFSTEP]
simp_rw [Set.mem_image, Set.mem_prod, Set.mem_setOf, Set.mem_univ, true_and_iff, Prod.ext_iff]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
hsp : ∀ (p : P × P × P), p ∈ s → ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
hp₁p₂s : (p₁, p₅, p₂) ∈ s
⊢ ∃ x, (SameRay ℝ (p₂ -ᵥ p₁) x.snd ∧ x.snd ≠ 0) ∧ ↑x.fst = p₃ ∧ True ∧ x.snd +ᵥ ↑x.fst = p₄
[PROOFSTEP]
refine'
  ⟨⟨⟨p₃,
        hc.mem_affineSpan_of_mem_of_ne (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_insert _ _))
          (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_insert _ _))) hp₁p₂⟩,
      p₄ -ᵥ p₃⟩,
    ⟨hr, vsub_ne_zero.2 hp₃p₄.symm⟩, _⟩
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
hsp : ∀ (p : P × P × P), p ∈ s → ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
hp₁p₂s : (p₁, p₅, p₂) ∈ s
⊢ ↑({ val := p₃, property := (_ : p₃ ∈ affineSpan ℝ {p₁, p₂}) }, p₄ -ᵥ p₃).fst = p₃ ∧
    True ∧
      ({ val := p₃, property := (_ : p₃ ∈ affineSpan ℝ {p₁, p₂}) }, p₄ -ᵥ p₃).snd +ᵥ
          ↑({ val := p₃, property := (_ : p₃ ∈ affineSpan ℝ {p₁, p₂}) }, p₄ -ᵥ p₃).fst =
        p₄
[PROOFSTEP]
simp
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x => (↑x.fst, p₅, x.snd +ᵥ ↑x.fst)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) s
hsp : ∀ (p : P × P × P), p ∈ s → ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
hp₁p₂s : (p₁, p₅, p₂) ∈ s
hp₃p₄s : (p₃, p₅, p₄) ∈ s
⊢ Real.Angle.sign (∡ p₁ p₅ p₂) = Real.Angle.sign (∡ p₃ p₅ p₄)
[PROOFSTEP]
convert Real.Angle.sign_eq_of_continuousOn hco hf hsp hp₃p₄s hp₁p₂s
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ Collinear ℝ {p₁, p₂, p₂, p₃}
[PROOFSTEP]
simpa using h.wbtw.collinear
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Wbtw ℝ p₁ p₂ p₃
hne : p₁ ≠ p₂
⊢ Collinear ℝ {p₁, p₂, p₁, p₃}
[PROOFSTEP]
simpa [Set.insert_comm p₂] using h.collinear
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Wbtw ℝ p₁ p₂ p₃
hne : p₂ ≠ p₃
⊢ Real.Angle.sign (∡ p₂ p₄ p₃) = Real.Angle.sign (∡ p₁ p₄ p₃)
[PROOFSTEP]
simp_rw [oangle_rev p₃, Real.Angle.sign_neg, h.symm.oangle_sign_eq_of_ne_left _ hne.symm]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
⊢ Real.Angle.sign (∡ p₁ p₄ p₂) = Real.Angle.sign (∡ p₁ p₃ p₂)
[PROOFSTEP]
by_cases h : p₁ = p₂
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : p₁ = p₂
⊢ Real.Angle.sign (∡ p₁ p₄ p₂) = Real.Angle.sign (∡ p₁ p₃ p₂)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
⊢ Real.Angle.sign (∡ p₁ p₄ p₂) = Real.Angle.sign (∡ p₁ p₃ p₂)
[PROOFSTEP]
let sp : Set (P × P × P) := (fun p : P => (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
⊢ Real.Angle.sign (∡ p₁ p₄ p₂) = Real.Angle.sign (∡ p₁ p₃ p₂)
[PROOFSTEP]
have hc : IsConnected sp :=
  (isConnected_setOf_sSameSide hp₃p₄.2.1 hp₃p₄.nonempty).image _
    (continuous_const.prod_mk (Continuous.Prod.mk_left _)).continuousOn
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
⊢ Real.Angle.sign (∡ p₁ p₄ p₂) = Real.Angle.sign (∡ p₁ p₃ p₂)
[PROOFSTEP]
have hf : ContinuousOn (fun p : P × P × P => ∡ p.1 p.2.1 p.2.2) sp :=
  by
  refine' ContinuousAt.continuousOn fun p hp => continuousAt_oangle _ _
  all_goals
    simp_rw [Set.mem_image, Set.mem_setOf] at hp 
    obtain ⟨p', hp', rfl⟩ := hp
    dsimp only
    rintro rfl
  · exact hp'.2.2 hp₁
  · exact hp'.2.2 hp₂
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
⊢ ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) sp
[PROOFSTEP]
refine' ContinuousAt.continuousOn fun p hp => continuousAt_oangle _ _
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
p : P × P × P
hp : p ∈ sp
⊢ p.fst ≠ p.snd.fst
case refine'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
p : P × P × P
hp : p ∈ sp
⊢ p.snd.snd ≠ p.snd.fst
[PROOFSTEP]
all_goals
  simp_rw [Set.mem_image, Set.mem_setOf] at hp 
  obtain ⟨p', hp', rfl⟩ := hp
  dsimp only
  rintro rfl
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
p : P × P × P
hp : p ∈ sp
⊢ p.fst ≠ p.snd.fst
[PROOFSTEP]
simp_rw [Set.mem_image, Set.mem_setOf] at hp 
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
p : P × P × P
hp : ∃ x, SSameSide s p₃ x ∧ (p₁, x, p₂) = p
⊢ p.fst ≠ p.snd.fst
[PROOFSTEP]
obtain ⟨p', hp', rfl⟩ := hp
[GOAL]
case refine'_1.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
p' : P
hp' : SSameSide s p₃ p'
⊢ (p₁, p', p₂).fst ≠ (p₁, p', p₂).snd.fst
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_1.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
p' : P
hp' : SSameSide s p₃ p'
⊢ p₁ ≠ p'
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
p : P × P × P
hp : p ∈ sp
⊢ p.snd.snd ≠ p.snd.fst
[PROOFSTEP]
simp_rw [Set.mem_image, Set.mem_setOf] at hp 
[GOAL]
case refine'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
p : P × P × P
hp : ∃ x, SSameSide s p₃ x ∧ (p₁, x, p₂) = p
⊢ p.snd.snd ≠ p.snd.fst
[PROOFSTEP]
obtain ⟨p', hp', rfl⟩ := hp
[GOAL]
case refine'_2.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
p' : P
hp' : SSameSide s p₃ p'
⊢ (p₁, p', p₂).snd.snd ≠ (p₁, p', p₂).snd.fst
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_2.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
p' : P
hp' : SSameSide s p₃ p'
⊢ p₂ ≠ p'
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
hp' : SSameSide s p₃ p₁
⊢ False
[PROOFSTEP]
exact hp'.2.2 hp₁
[GOAL]
case refine'_2.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
hp' : SSameSide s p₃ p₂
⊢ False
[PROOFSTEP]
exact hp'.2.2 hp₂
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) sp
⊢ Real.Angle.sign (∡ p₁ p₄ p₂) = Real.Angle.sign (∡ p₁ p₃ p₂)
[PROOFSTEP]
have hsp : ∀ p : P × P × P, p ∈ sp → ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ π :=
  by
  intro p hp
  simp_rw [Set.mem_image, Set.mem_setOf] at hp 
  obtain ⟨p', hp', rfl⟩ := hp
  dsimp only
  rw [oangle_ne_zero_and_ne_pi_iff_affineIndependent]
  exact affineIndependent_of_ne_of_mem_of_not_mem_of_mem h hp₁ hp'.2.2 hp₂
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) sp
⊢ ∀ (p : P × P × P), p ∈ sp → ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
[PROOFSTEP]
intro p hp
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) sp
p : P × P × P
hp : p ∈ sp
⊢ ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
[PROOFSTEP]
simp_rw [Set.mem_image, Set.mem_setOf] at hp 
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) sp
p : P × P × P
hp : ∃ x, SSameSide s p₃ x ∧ (p₁, x, p₂) = p
⊢ ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
[PROOFSTEP]
obtain ⟨p', hp', rfl⟩ := hp
[GOAL]
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) sp
p' : P
hp' : SSameSide s p₃ p'
⊢ ∡ (p₁, p', p₂).fst (p₁, p', p₂).snd.fst (p₁, p', p₂).snd.snd ≠ 0 ∧
    ∡ (p₁, p', p₂).fst (p₁, p', p₂).snd.fst (p₁, p', p₂).snd.snd ≠ ↑π
[PROOFSTEP]
dsimp only
[GOAL]
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) sp
p' : P
hp' : SSameSide s p₃ p'
⊢ ∡ p₁ p' p₂ ≠ 0 ∧ ∡ p₁ p' p₂ ≠ ↑π
[PROOFSTEP]
rw [oangle_ne_zero_and_ne_pi_iff_affineIndependent]
[GOAL]
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) sp
p' : P
hp' : SSameSide s p₃ p'
⊢ AffineIndependent ℝ ![p₁, p', p₂]
[PROOFSTEP]
exact affineIndependent_of_ne_of_mem_of_not_mem_of_mem h hp₁ hp'.2.2 hp₂
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) sp
hsp : ∀ (p : P × P × P), p ∈ sp → ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
⊢ Real.Angle.sign (∡ p₁ p₄ p₂) = Real.Angle.sign (∡ p₁ p₃ p₂)
[PROOFSTEP]
have hp₃ : (p₁, p₃, p₂) ∈ sp := Set.mem_image_of_mem _ (sSameSide_self_iff.2 ⟨hp₃p₄.nonempty, hp₃p₄.2.1⟩)
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) sp
hsp : ∀ (p : P × P × P), p ∈ sp → ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
hp₃ : (p₁, p₃, p₂) ∈ sp
⊢ Real.Angle.sign (∡ p₁ p₄ p₂) = Real.Angle.sign (∡ p₁ p₃ p₂)
[PROOFSTEP]
have hp₄ : (p₁, p₄, p₂) ∈ sp := Set.mem_image_of_mem _ hp₃p₄
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SSameSide s p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | SSameSide s p₃ p}
hc : IsConnected sp
hf : ContinuousOn (fun p => ∡ p.fst p.snd.fst p.snd.snd) sp
hsp : ∀ (p : P × P × P), p ∈ sp → ∡ p.fst p.snd.fst p.snd.snd ≠ 0 ∧ ∡ p.fst p.snd.fst p.snd.snd ≠ ↑π
hp₃ : (p₁, p₃, p₂) ∈ sp
hp₄ : (p₁, p₄, p₂) ∈ sp
⊢ Real.Angle.sign (∡ p₁ p₄ p₂) = Real.Angle.sign (∡ p₁ p₃ p₂)
[PROOFSTEP]
convert Real.Angle.sign_eq_of_continuousOn hc hf hsp hp₃ hp₄
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SOppSide s p₃ p₄
⊢ Real.Angle.sign (∡ p₁ p₄ p₂) = -Real.Angle.sign (∡ p₁ p₃ p₂)
[PROOFSTEP]
have hp₁p₃ : p₁ ≠ p₃ := by rintro rfl; exact hp₃p₄.left_not_mem hp₁
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SOppSide s p₃ p₄
⊢ p₁ ≠ p₃
[PROOFSTEP]
rintro rfl
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SOppSide s p₁ p₄
⊢ False
[PROOFSTEP]
exact hp₃p₄.left_not_mem hp₁
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : SOppSide s p₃ p₄
hp₁p₃ : p₁ ≠ p₃
⊢ Real.Angle.sign (∡ p₁ p₄ p₂) = -Real.Angle.sign (∡ p₁ p₃ p₂)
[PROOFSTEP]
rw [← (hp₃p₄.symm.trans (sOppSide_pointReflection hp₁ hp₃p₄.left_not_mem)).oangle_sign_eq hp₁ hp₂, ←
  oangle_rotate_sign p₁, ← oangle_rotate_sign p₁, oangle_swap₁₃_sign,
  (sbtw_pointReflection_of_ne ℝ hp₁p₃).symm.oangle_sign_eq _]
