awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ :
  ∡ (t.points i₂) (t.points i₁) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₁' : excenter t signs = excenter t {i₂}
h₂' : excenter t signs = excenter t {i₁}
h₁'₁ : excenter t {i₁} = excenter t {i₂}
⊢ excenter t signs = excenter t {i₁}

Tactic:
rw [h₂'] at h₁'
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ :
  ∡ (t.points i₂) (t.points i₁) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₁' : excenter t {i₁} = excenter t {i₂}
h₂' : excenter t signs = excenter t {i₁}
inl : False
⊢ excenter t signs = excenter t {i₃}

Tactic:
exfalso
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ :
  ∡ (t.points i₂) (t.points i₁) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₁' : excenter t {i₁} = excenter t {i₂}
h₂' : excenter t signs = excenter t {i₁}
⊢ False

Tactic:
t.excenter_singleton_injective.ne h₁₂ h₁'

Premises used: Affine.Simplex.excenter_singleton_injective, Function.Injective.ne
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ :
  ∡ (t.points i₂) (t.points i₁) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₁' : excenter t {i₁} = excenter t {i₂}
h₂' : excenter t signs = excenter t {i₁}
⊢ False

Tactic:
exact t.excenter_singleton_injective.ne h₁₂ h₁'

Premises used: Affine.Simplex.excenter_singleton_injective, Function.Injective.ne
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ :
  ∡ (t.points i₂) (t.points i₁) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₂' : excenter t signs = excenter t {i₃} ∨ excenter t signs = excenter t {i₁}
h₁' : excenter t signs = excenter t {i₃}
⊢ excenter t signs = excenter t {i₃}

Tactic:
h₁'
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ :
  ∡ (t.points i₂) (t.points i₁) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₂' : excenter t signs = excenter t {i₃} ∨ excenter t signs = excenter t {i₁}
h₁' : excenter t signs = excenter t {i₃}
⊢ excenter t signs = excenter t {i₃}

Tactic:
exact 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)
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
⊢ (x.1 -ᵥ x.2.1, x.2.2 -ᵥ x.2.1).1 ≠ 0

Tactic:
simp [*]
-- 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)
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
⊢ (x.1 -ᵥ x.2.1, x.2.2 -ᵥ x.2.1).2 ≠ 0

Tactic:
simp [*]
-- 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)
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
funProp : (x.1 -ᵥ x.2.1, x.2.2 -ᵥ x.2.1).1 ≠ 0
funProp₁ : (x.1 -ᵥ x.2.1, x.2.2 -ᵥ x.2.1).2 ≠ 0
⊢ ContinuousAt (Y := Real.Angle) (fun (y : P × P × P) ↦ Orientation.oangle o (y.1 -ᵥ y.2.1) (y.2.2 -ᵥ y.2.1)) x

Tactic:
fun_prop (disch := simp [*])
-- 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₂ = 0

Tactic:
simp [oangle]

Premises used: EuclideanGeometry.oangle
-- 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₂ = 0

Tactic:
simp [oangle]

Premises used: EuclideanGeometry.oangle
-- 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₁ = 0

Tactic:
o.oangle_self _

Premises used: EuclideanGeometry.oangle, Orientation.oangle_self, 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
h : ∡ p₁ p₂ p₃ ≠ 0
rw : p₁ -ᵥ p₂ ≠ 0
⊢ p₁ ≠ p₂

Tactic:
rw [← @vsub_ne_zero V]

Premises used: vsub_ne_zero
-- 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 : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₁ -ᵥ p₂ ≠ 0

Tactic:
o.left_ne_zero_of_oangle_ne_zero h

Premises used: Orientation.left_ne_zero_of_oangle_ne_zero, 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
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₁ -ᵥ p₂ ≠ 0

Tactic:
exact o.left_ne_zero_of_oangle_ne_zero h

Premises used: Orientation.left_ne_zero_of_oangle_ne_zero, 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
h : ∡ p₁ p₂ p₃ ≠ 0
rw : p₃ -ᵥ p₂ ≠ 0
⊢ p₃ ≠ p₂

Tactic:
rw [← @vsub_ne_zero V]

Premises used: vsub_ne_zero
-- 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 : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₃ -ᵥ p₂ ≠ 0

Tactic:
o.right_ne_zero_of_oangle_ne_zero h

Premises used: Orientation.right_ne_zero_of_oangle_ne_zero, 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
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₃ -ᵥ p₂ ≠ 0

Tactic:
exact o.right_ne_zero_of_oangle_ne_zero h

Premises used: Orientation.right_ne_zero_of_oangle_ne_zero, 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
h : ∡ p₁ p₂ p₃ ≠ 0
rw : p₁ -ᵥ p₂ ≠ p₃ -ᵥ p₂
⊢ p₁ ≠ p₃

Tactic:
rw [← (vsub_left_injective p₂).ne_iff]

Premises used: Function.Injective.ne_iff, vsub_left_injective
-- 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 : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₁ -ᵥ p₂ ≠ p₃ -ᵥ p₂

Tactic:
o.ne_of_oangle_ne_zero h

Premises used: Orientation.ne_of_oangle_ne_zero, 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
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₁ -ᵥ p₂ ≠ p₃ -ᵥ p₂

Tactic:
exact o.ne_of_oangle_ne_zero h

Premises used: Orientation.ne_of_oangle_ne_zero, 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
h : ∡ p₁ p₂ p₃ = (↑π : Real.Angle)
⊢ p₁ ≠ p₂

Tactic:
left_ne_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_ne_zero : ∡ p₁ p₂ p₃ ≠ 0)

Premises used: EuclideanGeometry.left_ne_of_oangle_ne_zero, Eq.rec, Real.Angle.pi_ne_zero, Eq.symm
-- 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 : ∡ p₁ p₂ p₃ = (↑π : Real.Angle)
⊢ p₃ ≠ p₂

Tactic:
right_ne_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_ne_zero : ∡ p₁ p₂ p₃ ≠ 0)

Premises used: Eq.rec, Real.Angle.pi_ne_zero, Eq.symm, EuclideanGeometry.right_ne_of_oangle_ne_zero
-- 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 : ∡ p₁ p₂ p₃ = (↑π : Real.Angle)
⊢ p₁ ≠ p₃

Tactic:
left_ne_right_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_ne_zero : ∡ p₁ p₂ p₃ ≠ 0)

Premises used: Eq.rec, EuclideanGeometry.left_ne_right_of_oangle_ne_zero, Real.Angle.pi_ne_zero, Eq.symm
-- 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 : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ p₁ ≠ p₂

Tactic:
left_ne_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_div_two_ne_zero : ∡ p₁ p₂ p₃ ≠ 0)

Premises used: EuclideanGeometry.left_ne_of_oangle_ne_zero, Real.Angle.pi_div_two_ne_zero, Eq.rec, Eq.symm
-- 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 : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ p₃ ≠ p₂

Tactic:
right_ne_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_div_two_ne_zero : ∡ p₁ p₂ p₃ ≠ 0)

Premises used: Real.Angle.pi_div_two_ne_zero, Eq.rec, Eq.symm, EuclideanGeometry.right_ne_of_oangle_ne_zero
-- 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 : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ p₁ ≠ p₃

Tactic:
left_ne_right_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_div_two_ne_zero : ∡ p₁ p₂ p₃ ≠ 0)

Premises used: Real.Angle.pi_div_two_ne_zero, Eq.rec, EuclideanGeometry.left_ne_right_of_oangle_ne_zero, Eq.symm
-- 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 : ∡ p₁ p₂ p₃ = (↑(-π / 2) : Real.Angle)
⊢ p₁ ≠ p₂

Tactic:
left_ne_of_oangle_ne_zero (h.symm ▸ Real.Angle.neg_pi_div_two_ne_zero : ∡ p₁ p₂ p₃ ≠ 0)

Premises used: EuclideanGeometry.left_ne_of_oangle_ne_zero, Real.Angle.neg_pi_div_two_ne_zero, Eq.rec, Eq.symm
-- 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 : ∡ p₁ p₂ p₃ = (↑(-π / 2) : Real.Angle)
⊢ p₃ ≠ p₂

Tactic:
right_ne_of_oangle_ne_zero (h.symm ▸ Real.Angle.neg_pi_div_two_ne_zero : ∡ p₁ p₂ p₃ ≠ 0)

Premises used: Real.Angle.neg_pi_div_two_ne_zero, Eq.rec, Eq.symm, EuclideanGeometry.right_ne_of_oangle_ne_zero
-- 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 : ∡ p₁ p₂ p₃ = (↑(-π / 2) : Real.Angle)
⊢ p₁ ≠ p₃

Tactic:
left_ne_right_of_oangle_ne_zero (h.symm ▸ Real.Angle.neg_pi_div_two_ne_zero : ∡ p₁ p₂ p₃ ≠ 0)

Premises used: Real.Angle.neg_pi_div_two_ne_zero, Eq.rec, EuclideanGeometry.left_ne_right_of_oangle_ne_zero, Eq.symm
-- 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 : (∡ p₁ p₂ p₃).sign ≠ 0
⊢ p₁ ≠ p₂

Tactic:
left_ne_of_oangle_ne_zero (Real.Angle.sign_ne_zero_iff.1 h).1

Premises used: EuclideanGeometry.left_ne_of_oangle_ne_zero, And.left, Real.Angle.sign_ne_zero_iff, Iff.mp
-- 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 : (∡ p₁ p₂ p₃).sign ≠ 0
⊢ p₃ ≠ p₂

Tactic:
right_ne_of_oangle_ne_zero (Real.Angle.sign_ne_zero_iff.1 h).1

Premises used: And.left, Real.Angle.sign_ne_zero_iff, Iff.mp, EuclideanGeometry.right_ne_of_oangle_ne_zero
-- 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 : (∡ p₁ p₂ p₃).sign ≠ 0
⊢ p₁ ≠ p₃

Tactic:
left_ne_right_of_oangle_ne_zero (Real.Angle.sign_ne_zero_iff.1 h).1

Premises used: EuclideanGeometry.left_ne_right_of_oangle_ne_zero, And.left, Real.Angle.sign_ne_zero_iff, Iff.mp
-- 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 : (∡ p₁ p₂ p₃).sign = 1
⊢ Ne (α := SignType) 1 0

Tactic:
decide
-- 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 : (∡ p₁ p₂ p₃).sign = -1
⊢ Ne (α := SignType) (-1) 0

Tactic:
decide
-- 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₁ = -∡ p₁ p₂ p₃

Tactic:
o.oangle_rev _ _

Premises used: EuclideanGeometry.oangle, Orientation.oangle_rev, 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₃ + ∡ p₃ p₂ p₁ = 0

Tactic:
o.oangle_add_oangle_rev _ _

Premises used: EuclideanGeometry.oangle, Orientation.oangle_add_oangle_rev, 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₃ = 0 ↔ ∡ p₃ p₂ p₁ = 0

Tactic:
o.oangle_eq_zero_iff_oangle_rev_eq_zero

Premises used: EuclideanGeometry.oangle, Orientation.oangle_eq_zero_iff_oangle_rev_eq_zero, 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₃ = (↑π : Real.Angle) ↔ ∡ p₃ p₂ p₁ = (↑π : Real.Angle)

Tactic:
o.oangle_eq_pi_iff_oangle_rev_eq_pi

Premises used: EuclideanGeometry.oangle, Orientation.oangle_eq_pi_iff_oangle_rev_eq_pi, 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
r : ℝ
h : r ≠ 0
simp_rw : Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
⊢ ∡ (P := P) ((AffineMap.homothety p r : (a : P) → P) p₁ : P) ((AffineMap.homothety p r : (a : P) → P) p₂ : P)
      ((AffineMap.homothety p r : (a : P) → P) p₃ : P) =
    ∡ p₁ p₂ p₃

Tactic:
simp_rw [oangle, ← AffineMap.linearMap_vsub, AffineMap.homothety_linear, LinearMap.smul_apply,
    LinearMap.id_coe, id_eq]

Premises used: EuclideanGeometry.oangle, LinearMap.smul_apply, LinearMap.id_coe, AffineMap.linearMap_vsub, AffineMap.homothety_linear, id_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
r : ℝ
h : r ≠ 0
inl :
  ∀ (hlt : r < 0), Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
inr :
  ∀ (hlt : 0 < r), 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₂)

Tactic:
rcases h.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
r : ℝ
h : r ≠ 0
hlt : r < 0
⊢ Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)

Tactic:
simp [hlt, -neg_vsub_eq_vsub_rev]

Premises used: 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
r : ℝ
h : r ≠ 0
hlt : 0 < r
⊢ Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)

Tactic:
simp [hlt, -neg_vsub_eq_vsub_rev]

Premises used: 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
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 }))
⊢ ∡ p₁ p₂ p₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ (↑π : Real.Angle) ↔ AffineIndependent ℝ ![p₁, p₂, p₃]

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))]

Premises used: EuclideanGeometry.oangle, Orientation.oangle_ne_zero_and_ne_pi_iff_linearIndependent, Real, linearIndependent_equiv, finSuccAboveEquiv, affineIndependent_iff_linearIndependent_vsub, OfNat.ofNat, 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
⊢ LinearIndependent ℝ ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] ↔ LinearIndependent ℝ ![p₁ -ᵥ p₂, p₃ -ᵥ p₂]

Tactic:
Iff.rfl

Premises used: Iff.rfl