awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h :
  (fun (i : { x : Fin 3 // x ≠ 1 }) ↦ ![p₁, p₂, p₃] (↑i : Fin 3) -ᵥ ![p₁, p₂, p₃] 1) ∘
      (⇑(finSuccAboveEquiv 1) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 1 }) =
    ![p₁ -ᵥ p₂, p₃ -ᵥ p₂]
⊢ LinearIndependent ℝ ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] ↔
    LinearIndependent.{0, 0, u_1} (ι := Fin 2) ℝ (M := V)
      ((fun (i : { x : Fin 3 // x ≠ 1 }) ↦ ![p₁, p₂, p₃] (↑i : Fin 3) -ᵥ ![p₁, p₂, p₃] 1) ∘
        (⇑(finSuccAboveEquiv 1) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 1 }))

Tactic:
convert! Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h :
  ∀ (i : Fin 2),
    ((fun (i : { x : Fin 3 // x ≠ 1 }) ↦ ![p₁, p₂, p₃] (↑i : Fin 3) -ᵥ ![p₁, p₂, p₃] 1) ∘
          (⇑(finSuccAboveEquiv 1) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 1 }))
        i =
      ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] i
⊢ (fun (i : { x : Fin 3 // x ≠ 1 }) ↦ ![p₁, p₂, p₃] (↑i : Fin 3) -ᵥ ![p₁, p₂, p₃] 1) ∘
      (⇑(finSuccAboveEquiv 1) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 1 }) =
    ![p₁ -ᵥ p₂, p₃ -ᵥ p₂]

Tactic:
ext i
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
i : Fin 2
h :
  Function.comp (α := Fin 2) (fun (i : { x : Fin 3 // x ≠ 1 }) ↦ ![p₁, p₂, p₃] (↑i : Fin 3) -ᵥ ![p₁, p₂, p₃] 1)
      (⇑(finSuccAboveEquiv 1) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 1 }) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) =
    ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))
h₁ :
  Function.comp (α := Fin 2) (fun (i : { x : Fin 3 // x ≠ 1 }) ↦ ![p₁, p₂, p₃] (↑i : Fin 3) -ᵥ ![p₁, p₂, p₃] 1)
      (⇑(finSuccAboveEquiv 1) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 1 }) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) =
    ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))
⊢ ((fun (i : { x : Fin 3 // x ≠ 1 }) ↦ ![p₁, p₂, p₃] (↑i : Fin 3) -ᵥ ![p₁, p₂, p₃] 1) ∘
        (⇑(finSuccAboveEquiv 1) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 1 }))
      i =
    ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] i

Tactic:
fin_cases i
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ Function.comp (α := Fin 2) (fun (i : { x : Fin 3 // x ≠ 1 }) ↦ ![p₁, p₂, p₃] (↑i : Fin 3) -ᵥ ![p₁, p₂, p₃] 1)
      (⇑(finSuccAboveEquiv 1) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 1 }) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) =
    ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))

Tactic:
rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ Function.comp (α := Fin 2) (fun (i : { x : Fin 3 // x ≠ 1 }) ↦ ![p₁, p₂, p₃] (↑i : Fin 3) -ᵥ ![p₁, p₂, p₃] 1)
      (⇑(finSuccAboveEquiv 1) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 1 }) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) =
    ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))

Tactic:
rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
rw : ¬(∡ p₁ p₂ p₃ = 0 ∨ ∡ p₁ p₂ p₃ = (↑π : Real.Angle)) ↔ ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
rw₁ : ¬∡ p₁ p₂ p₃ = 0 ∧ ¬∡ p₁ p₂ p₃ = (↑π : Real.Angle) ↔ ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
rw₂ : AffineIndependent ℝ ![p₁, p₂, p₃] ↔ ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
rw₃ rw₄ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃} ↔ ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ ∡ p₁ p₂ p₃ = 0 ∨ ∡ p₁ p₂ p₃ = (↑π : Real.Angle) ↔ Collinear ℝ (P := P) {p₁, p₂, p₃}

Tactic:
rw [← not_iff_not, not_or, oangle_ne_zero_and_ne_pi_iff_affineIndependent,
    affineIndependent_iff_not_collinear_set]

Premises used: not_iff_not, affineIndependent_iff_not_collinear_set, EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent, not_or
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
rw : ∡ p₁ p₂ p₃ = 0 ∨ ∡ p₁ p₂ p₃ = (↑π : Real.Angle) ↔ Collinear ℝ (P := P) {p₁, p₂, p₃}
rw₁ rw₂ : Collinear ℝ (P := P) {p₁, p₂, p₃} ↔ Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ (∡ p₁ p₂ p₃).sign = 0 ↔ Collinear ℝ (P := P) {p₁, p₂, p₃}

Tactic:
rw [Real.Angle.sign_eq_zero_iff, oangle_eq_zero_or_eq_pi_iff_collinear]

Premises used: Real.Angle.sign_eq_zero_iff, EuclideanGeometry.oangle_eq_zero_or_eq_pi_iff_collinear
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
rw : AffineIndependent ℝ ![p₁, p₂, p₃] ↔ ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
rw₁ rw₂ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃} ↔ ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ ∡ p₁ p₂ p₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ (↑π : Real.Angle) ↔ ¬Collinear ℝ (P := P) {p₁, p₂, p₃}

Tactic:
rw [oangle_ne_zero_and_ne_pi_iff_affineIndependent, affineIndependent_iff_not_collinear_set]

Premises used: affineIndependent_iff_not_collinear_set, EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₅ p₆)
simp_rw : ∡ p₁ p₂ p₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ (↑π : Real.Angle) ↔ ∡ p₄ p₅ p₆ ≠ 0 ∧ ∡ p₄ p₅ p₆ ≠ (↑π : Real.Angle)
simp_rw₁ : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) ≠ 0 ↔ HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₅ p₆) ≠ 0
⊢ AffineIndependent ℝ ![p₁, p₂, p₃] ↔ AffineIndependent ℝ ![p₄, p₅, p₆]

Tactic:
simp_rw [← oangle_ne_zero_and_ne_pi_iff_affineIndependent, ← Real.Angle.two_zsmul_ne_zero_iff, h]

Premises used: Real.Angle.two_zsmul_ne_zero_iff, EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₅ p₆)
simp_rw : ∡ p₁ p₂ p₃ = 0 ∨ ∡ p₁ p₂ p₃ = (↑π : Real.Angle) ↔ ∡ p₄ p₅ p₆ = 0 ∨ ∡ p₄ p₅ p₆ = (↑π : Real.Angle)
simp_rw₁ : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = 0 ↔ HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₅ p₆) = 0
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃} ↔ Collinear ℝ (P := P) {p₄, p₅, p₆}

Tactic:
simp_rw [← oangle_eq_zero_or_eq_pi_iff_collinear, ← Real.Angle.two_zsmul_eq_zero_iff, h]

Premises used: EuclideanGeometry.oangle_eq_zero_or_eq_pi_iff_collinear, Real.Angle.two_zsmul_eq_zero_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : Eq (α := Submodule ℝ V) (vectorSpan ℝ (P := P) {p₁, p₂}) (vectorSpan ℝ (P := P) {p₄, p₅})
h₃₂₆₅ : Eq (α := Submodule ℝ V) (vectorSpan ℝ (P := P) {p₃, p₂}) (vectorSpan ℝ (P := P) {p₆, p₅})
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ (p₁ -ᵥ p₂)) (ℝ ∙ (p₄ -ᵥ p₅))

Tactic:
simp_rw [vectorSpan_pair] at h₁₂₄₅ h₃₂₆₅

Premises used: vectorSpan_pair
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : Eq (α := Submodule ℝ V) (vectorSpan ℝ (P := P) {p₁, p₂}) (vectorSpan ℝ (P := P) {p₄, p₅})
h₃₂₆₅ : Eq (α := Submodule ℝ V) (vectorSpan ℝ (P := P) {p₃, p₂}) (vectorSpan ℝ (P := P) {p₆, p₅})
h₁₂₄₆ : Eq (α := Submodule ℝ V) (ℝ ∙ (p₁ -ᵥ p₂)) (ℝ ∙ (p₄ -ᵥ p₅))
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ (p₃ -ᵥ p₂)) (ℝ ∙ (p₆ -ᵥ p₅))

Tactic:
simp_rw [vectorSpan_pair] at h₁₂₄₅ h₃₂₆₅

Premises used: vectorSpan_pair
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : Eq (α := Submodule ℝ V) (ℝ ∙ (p₁ -ᵥ p₂)) (ℝ ∙ (p₄ -ᵥ p₅))
h₃₂₆₅ : Eq (α := Submodule ℝ V) (ℝ ∙ (p₃ -ᵥ p₂)) (ℝ ∙ (p₆ -ᵥ p₅))
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₅ p₆)

Tactic:
exact o.two_zsmul_oangle_of_span_eq_of_span_eq h₁₂₄₅ h₃₂₆₅

Premises used: Orientation.two_zsmul_oangle_of_span_eq_of_span_eq, EuclideanGeometry.o
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₁, p₂}) (affineSpan ℝ {p₄, p₅})
h₃₂₆₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₃, p₂}) (affineSpan ℝ {p₆, p₅})
⊢ Eq (α := Submodule ℝ V) (vectorSpan ℝ (P := P) {p₁, p₂}) (vectorSpan ℝ (P := P) {p₄, p₅})

Tactic:
rw [AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq] at h₁₂₄₅ h₃₂₆₅

Premises used: AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₁, p₂}) (affineSpan ℝ {p₄, p₅})
h₃₂₆₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₃, p₂}) (affineSpan ℝ {p₆, p₅})
h₁₂₄₆ : Eq (α := Submodule ℝ V) (vectorSpan ℝ (P := P) {p₁, p₂}) (vectorSpan ℝ (P := P) {p₄, p₅})
⊢ Eq (α := Submodule ℝ V) (vectorSpan ℝ (P := P) {p₃, p₂}) (vectorSpan ℝ (P := P) {p₆, p₅})

Tactic:
rw [AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq] at h₁₂₄₅ h₃₂₆₅

Premises used: AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : Eq (α := Submodule ℝ V) (vectorSpan ℝ (P := P) {p₁, p₂}) (vectorSpan ℝ (P := P) {p₄, p₅})
h₃₂₆₅ : Eq (α := Submodule ℝ V) (vectorSpan ℝ (P := P) {p₃, p₂}) (vectorSpan ℝ (P := P) {p₆, p₅})
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₅ p₆)

Tactic:
two_zsmul_oangle_of_vectorSpan_eq h₁₂₄₅ h₃₂₆₅

Premises used: EuclideanGeometry.two_zsmul_oangle_of_vectorSpan_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : Eq (α := Submodule ℝ V) (vectorSpan ℝ (P := P) {p₁, p₂}) (vectorSpan ℝ (P := P) {p₄, p₅})
h₃₂₆₅ : Eq (α := Submodule ℝ V) (vectorSpan ℝ (P := P) {p₃, p₂}) (vectorSpan ℝ (P := P) {p₆, p₅})
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₅ p₆)

Tactic:
exact two_zsmul_oangle_of_vectorSpan_eq h₁₂₄₅ h₃₂₆₅

Premises used: EuclideanGeometry.two_zsmul_oangle_of_vectorSpan_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan ℝ {p₁, p₃}
h₄ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₄
h₆ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₆
h₁₂₄₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₁, p₂}) (affineSpan ℝ {p₄, p₅})
h₃₂₆₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₃, p₂}) (affineSpan ℝ {p₆, p₅})
rw :
  LE.le (α := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₆, p₄}))
    (AffineSubspace.direction (P := P) (affineSpan ℝ {p₁, p₃}))
⊢ LE.le (α := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₆, p₄}))
    (AffineSubspace.direction (P := P) (affineSpan ℝ {p₃, p₁}))

Tactic:
rw [Set.pair_comm p₃]

Premises used: Set.pair_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan ℝ {p₁, p₃}
h₄ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₄
h₆ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₆
h₁₂₄₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₁, p₂}) (affineSpan ℝ {p₄, p₅})
h₃₂₆₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₃, p₂}) (affineSpan ℝ {p₆, p₅})
⊢ LE.le (α := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₆, p₄}))
    (AffineSubspace.direction (P := P) (affineSpan ℝ {p₁, p₃}))

Tactic:
AffineSubspace.direction_le (affineSpan_pair_le_of_mem_of_mem h₆ h₄)

Premises used: AffineSubspace.direction_le, affineSpan_pair_le_of_mem_of_mem
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan ℝ {p₁, p₃}
h₄ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₄
h₆ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₆
h₁₂₄₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₁, p₂}) (affineSpan ℝ {p₄, p₅})
h₃₂₆₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₃, p₂}) (affineSpan ℝ {p₆, p₅})
⊢ LE.le (α := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₆, p₄}))
    (AffineSubspace.direction (P := P) (affineSpan ℝ {p₁, p₃}))

Tactic:
exact AffineSubspace.direction_le (affineSpan_pair_le_of_mem_of_mem h₆ h₄)

Premises used: AffineSubspace.direction_le, affineSpan_pair_le_of_mem_of_mem
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan ℝ {p₁, p₃}
h₄ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₄
h₆ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₆
h₁₂₄₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₁, p₂}) (affineSpan ℝ {p₄, p₅})
h₃₂₆₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₃, p₂}) (affineSpan ℝ {p₆, p₅})
⊢ LE.le (α := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₆, p₄}))
    (AffineSubspace.direction (P := P) (affineSpan ℝ {p₃, p₁}))

Tactic:
have hd : line[ℝ, p₆, p₄].direction ≤ line[ℝ, p₃, p₁].direction := by
    rw [Set.pair_comm p₃]
    exact AffineSubspace.direction_le (affineSpan_pair_le_of_mem_of_mem h₆ h₄)
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan ℝ {p₁, p₃}
h₄ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₄
h₆ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₆
h₁₂₄₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₁, p₂}) (affineSpan ℝ {p₄, p₅})
h₃₂₆₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₃, p₂}) (affineSpan ℝ {p₆, p₅})
hd :
  LE.le (α := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₆, p₄}))
    (AffineSubspace.direction (P := P) (affineSpan ℝ {p₃, p₁}))
obtain :
  ∀ (r : ℝ) (hr : r ≠ 0) (h₅₄ : p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁)) (h₆₅ : p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂)),
    Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₄ -ᵥ p₅) (p₆ -ᵥ p₅)
⊢ Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₄ -ᵥ p₅) (p₆ -ᵥ p₅)

Tactic:
obtain ⟨r, hr, h₅₄, h₆₅, -⟩ := exists_eq_smul_of_parallel h₂ h₁₂₄₅
    (Set.pair_comm p₃ p₂ ▸ Set.pair_comm p₆ p₅ ▸ h₃₂₆₅).direction_eq.symm.le hd

Premises used: exists_eq_smul_of_parallel
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan ℝ {p₁, p₃}
h₄ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₄
h₆ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₆
h₁₂₄₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₁, p₂}) (affineSpan ℝ {p₄, p₅})
h₃₂₆₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₃, p₂}) (affineSpan ℝ {p₆, p₅})
hd :
  LE.le (α := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₆, p₄}))
    (AffineSubspace.direction (P := P) (affineSpan ℝ {p₃, p₁}))
r : ℝ
hr : r ≠ 0
h₅₄ : p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁)
h₆₅ : p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂)
⊢ p₄ -ᵥ p₅ = r • (p₁ -ᵥ p₂)

Tactic:
rw [← neg_inj, neg_vsub_eq_vsub_rev, ← smul_neg, neg_vsub_eq_vsub_rev] at h₅₄

Premises used: smul_neg, neg_inj, neg_vsub_eq_vsub_rev
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan ℝ {p₁, p₃}
h₄ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₄
h₆ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₆
h₁₂₄₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₁, p₂}) (affineSpan ℝ {p₄, p₅})
h₃₂₆₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₃, p₂}) (affineSpan ℝ {p₆, p₅})
hd :
  LE.le (α := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₆, p₄}))
    (AffineSubspace.direction (P := P) (affineSpan ℝ {p₃, p₁}))
r : ℝ
hr : r ≠ 0
h₅₄ : p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁)
h₆₅ : p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂)
h₅₅ : p₄ -ᵥ p₅ = r • (p₁ -ᵥ p₂)
⊢ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂)

Tactic:
rw [← neg_inj, neg_vsub_eq_vsub_rev, ← smul_neg, neg_vsub_eq_vsub_rev] at h₅₄

Premises used: smul_neg, neg_inj, neg_vsub_eq_vsub_rev
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan ℝ {p₁, p₃}
h₄ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₄
h₆ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₆
h₁₂₄₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₁, p₂}) (affineSpan ℝ {p₄, p₅})
h₃₂₆₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₃, p₂}) (affineSpan ℝ {p₆, p₅})
hd :
  LE.le (α := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₆, p₄}))
    (AffineSubspace.direction (P := P) (affineSpan ℝ {p₃, p₁}))
r : ℝ
hr : r ≠ 0
h₅₄ : p₄ -ᵥ p₅ = r • (p₁ -ᵥ p₂)
h₆₅ : p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂)
rw : Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂))
⊢ Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₄ -ᵥ p₅) (p₆ -ᵥ p₅)

Tactic:
rw [h₅₄, h₆₅]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan ℝ {p₁, p₃}
h₄ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₄
h₆ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₆
h₁₂₄₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₁, p₂}) (affineSpan ℝ {p₄, p₅})
h₃₂₆₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₃, p₂}) (affineSpan ℝ {p₆, p₅})
hd :
  LE.le (α := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₆, p₄}))
    (AffineSubspace.direction (P := P) (affineSpan ℝ {p₃, p₁}))
r : ℝ
hr : r ≠ 0
h₅₄ : p₄ -ᵥ p₅ = r • (p₁ -ᵥ p₂)
h₆₅ : p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂)
inl :
  ∀ (hlt : r < 0), Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂))
inr :
  ∀ (hlt : 0 < r), Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂))
⊢ Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂))

Tactic:
rcases hr.lt_or_gt with hlt | hlt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan ℝ {p₁, p₃}
h₄ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₄
h₆ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₃}) p₆
h₁₂₄₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₁, p₂}) (affineSpan ℝ {p₄, p₅})
h₃₂₆₅ : AffineSubspace.Parallel (P := P) (affineSpan ℝ {p₃, p₂}) (affineSpan ℝ {p₆, p₅})
hd :
  LE.le (α := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₆, p₄}))
    (AffineSubspace.direction (P := P) (affineSpan ℝ {p₃, p₁}))
r : ℝ
hr : r ≠ 0
h₅₄ : p₄ -ᵥ p₅ = r • (p₁ -ᵥ p₂)
h₆₅ : p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂)
hlt : r < 0
⊢ Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂))

Tactic:
simp [-neg_vsub_eq_vsub_rev, hlt]

Premises used: neg_vsub_eq_vsub_rev