awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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
r : ℝ
h : r ≠ 0
inl :
  ∀ (hlt : r < 0), 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₂)) = Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
have inr : ∀ (hlt : 0 < r), Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
Tactic: rcases h.lt_or_gt with hlt | hlt
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ (↑π : Real.Angle) ↔ AffineIndependent ℝ ![p₁, p₂, p₃]
have rw : 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: rw [oangle, o.oangle_ne_zero_and_ne_pi_iff_linearIndependent,
    affineIndependent_iff_linearIndependent_vsub ℝ _ (1 : Fin 3), ←
    linearIndependent_equiv (finSuccAboveEquiv (1 : Fin 3))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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
⊢ 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 }))
have 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₂]
Tactic: convert! Iff.rfl
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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
⊢ (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₂]
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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
⊢ ((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
have 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, sorry⟩) =
  ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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))
⊢ ((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
have 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, sorry⟩) =
  ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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₃ = 0 ∨ ∡ p₁ p₂ p₃ = (↑π : Real.Angle) ↔ Collinear ℝ (P := P) {p₁, p₂, p₃}
have rw : ¬(∡ 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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₃}
⊢ ∡ p₁ p₂ p₃ = 0 ∨ ∡ p₁ p₂ p₃ = (↑π : Real.Angle) ↔ Collinear ℝ (P := P) {p₁, p₂, p₃}
have rw₁ : ¬∡ 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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₃}
⊢ ∡ p₁ p₂ p₃ = 0 ∨ ∡ p₁ p₂ p₃ = (↑π : Real.Angle) ↔ Collinear ℝ (P := P) {p₁, p₂, p₃}
have rw₂ : AffineIndependent ℝ ![p₁, p₂, p₃] ↔ ¬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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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₃}
⊢ ∡ p₁ p₂ p₃ = 0 ∨ ∡ p₁ p₂ p₃ = (↑π : Real.Angle) ↔ Collinear ℝ (P := P) {p₁, p₂, p₃}
have rw₃ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃} ↔ ¬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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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₃).sign = 0 ↔ Collinear ℝ (P := P) {p₁, p₂, p₃}
have rw : ∡ p₁ p₂ p₃ = 0 ∨ ∡ p₁ p₂ p₃ = (↑π : Real.Angle) ↔ Collinear ℝ (P := P) {p₁, p₂, p₃}
Tactic: rw [Real.Angle.sign_eq_zero_iff, oangle_eq_zero_or_eq_pi_iff_collinear]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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₃}
⊢ (∡ p₁ p₂ p₃).sign = 0 ↔ Collinear ℝ (P := P) {p₁, p₂, p₃}
have rw₁ : Collinear ℝ (P := P) {p₁, p₂, p₃} ↔ Collinear ℝ (P := P) {p₁, p₂, p₃}
Tactic: rw [Real.Angle.sign_eq_zero_iff, oangle_eq_zero_or_eq_pi_iff_collinear]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ (↑π : Real.Angle) ↔ ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
have rw : AffineIndependent ℝ ![p₁, p₂, p₃] ↔ ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
Tactic: rw [oangle_ne_zero_and_ne_pi_iff_affineIndependent, affineIndependent_iff_not_collinear_set]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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₃}
⊢ ∡ p₁ p₂ p₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ (↑π : Real.Angle) ↔ ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
have rw₁ : ¬Collinear ℝ (P := P) {p₁, p₂, p₃} ↔ ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
Tactic: rw [oangle_ne_zero_and_ne_pi_iff_affineIndependent, affineIndependent_iff_not_collinear_set]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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₆)
⊢ AffineIndependent ℝ ![p₁, p₂, p₃] ↔ AffineIndependent ℝ ![p₄, p₅, p₆]
have simp_rw : ∡ p₁ p₂ p₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ (↑π : Real.Angle) ↔ ∡ p₄ p₅ p₆ ≠ 0 ∧ ∡ p₄ p₅ p₆ ≠ (↑π : Real.Angle)
Tactic: simp_rw [← oangle_ne_zero_and_ne_pi_iff_affineIndependent, ← Real.Angle.two_zsmul_ne_zero_iff, h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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)
⊢ AffineIndependent ℝ ![p₁, p₂, p₃] ↔ AffineIndependent ℝ ![p₄, p₅, p₆]
have simp_rw₁ : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) ≠ 0 ↔ HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₅ p₆) ≠ 0
Tactic: simp_rw [← oangle_ne_zero_and_ne_pi_iff_affineIndependent, ← Real.Angle.two_zsmul_ne_zero_iff, h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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₆)
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃} ↔ Collinear ℝ (P := P) {p₄, p₅, p₆}
have simp_rw : ∡ p₁ p₂ p₃ = 0 ∨ ∡ p₁ p₂ p₃ = (↑π : Real.Angle) ↔ ∡ p₄ p₅ p₆ = 0 ∨ ∡ p₄ p₅ p₆ = (↑π : Real.Angle)
Tactic: simp_rw [← oangle_eq_zero_or_eq_pi_iff_collinear, ← Real.Angle.two_zsmul_eq_zero_iff, h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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)
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃} ↔ Collinear ℝ (P := P) {p₄, p₅, p₆}
have simp_rw₁ : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = 0 ↔ HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₅ p₆) = 0
Tactic: simp_rw [← oangle_eq_zero_or_eq_pi_iff_collinear, ← Real.Angle.two_zsmul_eq_zero_iff, h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (hypothesis)
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₆)
have h₁₂₄₆ : Eq (α := Submodule ℝ V) (ℝ ∙ (p₁ -ᵥ p₂)) (ℝ ∙ (p₄ -ᵥ p₅))
Tactic: simp_rw [vectorSpan_pair] at h₁₂₄₅ h₃₂₆₅
Cleared hypotheses: h₁₂₄₅, h₃₂₆₅
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (hypothesis)
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₅))
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₅ p₆)
have h₃₂₆₆ : Eq (α := Submodule ℝ V) (ℝ ∙ (p₃ -ᵥ p₂)) (ℝ ∙ (p₆ -ᵥ p₅))
Tactic: simp_rw [vectorSpan_pair] at h₁₂₄₅ h₃₂₆₅
Cleared hypotheses: h₁₂₄₅, h₃₂₆₅
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (hypothesis)
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₅})
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₅ p₆)
have h₁₂₄₆ : 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₃₂₆₅
Cleared hypotheses: h₁₂₄₅, h₃₂₆₅
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (hypothesis)
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₅})
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₅ p₆)
have h₃₂₆₆ : 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₃₂₆₅
Cleared hypotheses: h₁₂₄₅, h₃₂₆₅
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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₁}))
have rw : LE.le (α := Submodule ℝ V) (AffineSubspace.direction (P := P) (affineSpan ℝ {p₆, p₄}))
  (AffineSubspace.direction (P := P) (affineSpan ℝ {p₁, p₃}))
Tactic: rw [Set.pair_comm p₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (hypothesis)
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₅})
⊢ Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₄ -ᵥ p₅) (p₆ -ᵥ p₅)
have hd : 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₄)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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₁}))
⊢ Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₄ -ᵥ p₅) (p₆ -ᵥ p₅)
have 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₅)
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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (hypothesis)
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₂)
⊢ Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₄ -ᵥ p₅) (p₆ -ᵥ p₅)
have h₅₅ : p₄ -ᵥ p₅ = r • (p₁ -ᵥ p₂)
Tactic: rw [← neg_inj, neg_vsub_eq_vsub_rev, ← smul_neg, neg_vsub_eq_vsub_rev] at h₅₄
Cleared hypotheses: h₅₄, h₆₅
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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₂)
⊢ Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₄ -ᵥ p₅) (p₆ -ᵥ p₅)
have rw : Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂))
Tactic: rw [h₅₄, h₆₅]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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₂)
⊢ Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂))
have inl : ∀ (hlt : r < 0), 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