awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
h : n ≤ -1
⊢ π + -(2 * π) < HAdd.hAdd (α := ℝ) 0 0

Tactic:
linear_combination Real.pi_pos

Premises used: Real.pi_pos
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
h : angle x y + n • (2 * π) = angle x (x + y) + angle y (x + y)
⊢ -1 < n

Tactic:
have : -1 < n := by
    replace h := h.ge
    contrapose! h
    grw [h, neg_smul, one_smul, angle_le_pi, ← angle_nonneg, ← angle_nonneg]
    linear_combination Real.pi_pos
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
h : angle x y + n • (2 * π) = angle x (x + y) + angle y (x + y)
this : -1 < n
⊢ angle x y + n • (2 * π) ≤ angle x (x + y) + angle y (x + y)

Tactic:
replace h := h.le
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : angle x y + n • (2 * π) ≤ angle x (x + y) + angle y (x + y)
by_contra! : ∀ (hn : 1 ≤ n), False
⊢ n < 1

Tactic:
by_contra! hn
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : angle x y + n • (2 * π) ≤ angle x (x + y) + angle y (x + y)
hn : 1 ≤ n
⊢ π + π ≤ angle x (x + y) + angle y (x + y)

Tactic:
grw [← hn, one_smul, ← angle_nonneg x y, zero_add, two_mul] at h

Premises used: two_mul, zero_add, one_smul, InnerProductGeometry.angle_nonneg
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : angle x y + n • (2 * π) ≤ angle x (x + y) + angle y (x + y)
hn : 1 ≤ n
h₁ : π + π ≤ angle x (x + y) + angle y (x + y)
⊢ 1 ≤ n

Tactic:
grw [← hn, one_smul, ← angle_nonneg x y, zero_add, two_mul] at h

Premises used: two_mul, zero_add, one_smul, InnerProductGeometry.angle_nonneg
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : π + π ≤ angle x (x + y) + angle y (x + y)
hn : 1 ≤ n
⊢ π + π ≤ angle y (x + y) + angle x (x + y)

Tactic:
have h' := h.trans_eq (add_comm _ _)
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : π + π ≤ angle x (x + y) + angle y (x + y)
hn : 1 ≤ n
h' : π + π ≤ angle y (x + y) + angle x (x + y)
⊢ π + π ≤ π + angle y (x + y)

Tactic:
grw [angle_le_pi] at h' h

Premises used: InnerProductGeometry.angle_le_pi
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : π + π ≤ angle x (x + y) + angle y (x + y)
hn : 1 ≤ n
h' : π + π ≤ angle y (x + y) + angle x (x + y)
h₁ : π + π ≤ π + angle y (x + y)
⊢ 1 ≤ n

Tactic:
grw [angle_le_pi] at h' h

Premises used: InnerProductGeometry.angle_le_pi
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : π + π ≤ angle x (x + y) + angle y (x + y)
hn : 1 ≤ n
h' : π + π ≤ angle y (x + y) + angle x (x + y)
h₁ : π + π ≤ π + angle y (x + y)
hn₁ : 1 ≤ n
⊢ π + π ≤ π + angle x (x + y)

Tactic:
grw [angle_le_pi] at h' h

Premises used: InnerProductGeometry.angle_le_pi
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : π + π ≤ π + angle y (x + y)
hn : 1 ≤ n
h' : π + π ≤ π + angle x (x + y)
⊢ x + y ≠ 0 ∧ ∃ r < 0, y = r • (x + y)

Tactic:
rw [add_le_add_iff_left, (angle_le_pi _ _).ge_iff_eq, angle_comm, angle_eq_pi_iff] at h' h

Premises used: InnerProductGeometry.angle_le_pi, add_le_add_iff_left, InnerProductGeometry.angle_comm, LE.le.ge_iff_eq, InnerProductGeometry.angle_eq_pi_iff
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : π + π ≤ π + angle y (x + y)
hn : 1 ≤ n
h' : π + π ≤ π + angle x (x + y)
h₁ : x + y ≠ 0 ∧ ∃ r < 0, y = r • (x + y)
⊢ 1 ≤ n

Tactic:
rw [add_le_add_iff_left, (angle_le_pi _ _).ge_iff_eq, angle_comm, angle_eq_pi_iff] at h' h

Premises used: InnerProductGeometry.angle_le_pi, add_le_add_iff_left, InnerProductGeometry.angle_comm, LE.le.ge_iff_eq, InnerProductGeometry.angle_eq_pi_iff
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : π + π ≤ π + angle y (x + y)
hn : 1 ≤ n
h' : π + π ≤ π + angle x (x + y)
h₁ : x + y ≠ 0 ∧ ∃ r < 0, y = r • (x + y)
hn₁ : 1 ≤ n
⊢ x + y ≠ 0 ∧ ∃ r < 0, x = r • (x + y)

Tactic:
rw [add_le_add_iff_left, (angle_le_pi _ _).ge_iff_eq, angle_comm, angle_eq_pi_iff] at h' h

Premises used: InnerProductGeometry.angle_le_pi, add_le_add_iff_left, InnerProductGeometry.angle_comm, LE.le.ge_iff_eq, InnerProductGeometry.angle_eq_pi_iff
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : x + y ≠ 0 ∧ ∃ r < 0, y = r • (x + y)
hn : 1 ≤ n
h' : x + y ≠ 0 ∧ ∃ r < 0, x = r • (x + y)
obtain : ∀ (hxy : x + y ≠ 0) (r₁ : ℝ) (r₁_pos : r₁ < 0) (hr₁ : x = r₁ • (x + y)), False
⊢ False

Tactic:
obtain ⟨hxy, r₁, r₁_pos, hr₁⟩ := h'
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : x + y ≠ 0 ∧ ∃ r < 0, y = r • (x + y)
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
obtain : ∀ (r₂ : ℝ) (r₂_pos : r₂ < 0) (hr₂ : y = r₂ • (x + y)), False
⊢ False

Tactic:
obtain ⟨-, r₂, r₂_pos, hr₂⟩ := h
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
rw : (r₁ + r₂) • (x + y) - HSMul.hSMul (α := ℝ) 1 (x + y) = 0
rw₁ : r₁ • (x + y) + r₂ • (x + y) - HSMul.hSMul (α := ℝ) 1 (x + y) = 0
rw₂ : r₁ • (x + y) + r₂ • (x + y) - (x + y) = 0
rw₃ : x + r₂ • (x + y) - (x + y) = 0
rw₄ : x + y - (x + y) = 0
rw₅ rw₆ : x + y = x + y
⊢ (r₁ + r₂ - 1) • (x + y) = 0

Tactic:
rw [sub_smul, add_smul, one_smul, ← hr₁, ← hr₂, sub_eq_zero]

Premises used: sub_eq_zero, sub_smul, one_smul, add_smul
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
⊢ (r₁ + r₂ - 1) • (x + y) = 0

Tactic:
have : (r₁ + r₂ - 1) • (x + y) = 0 := by
      rw [sub_smul, add_smul, one_smul, ← hr₁, ← hr₂, sub_eq_zero]
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this_1 : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
this : (r₁ + r₂ - 1) • (x + y) = 0
inl : r₁ + r₂ - 1 = 0 → False
inr : x + y = 0 → False
⊢ False

Tactic:
cases smul_eq_zero.1 this

Premises used: Iff.mp, smul_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this_1 : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
this : (r₁ + r₂ - 1) • (x + y) = 0
h_1 : r₁ + r₂ - 1 = 0
linarith : -1 + (r₁ - 0) + (r₂ - 0) + -(r₁ + r₂ - 1 - 0) = 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this_1 : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
this : (r₁ + r₂ - 1) • (x + y) = 0
h_1 : x + y = 0
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
h : angle x y + n • (2 * π) = angle x (x + y) + angle y (x + y)
this : -1 < n
⊢ n < 1

Tactic:
have : n < 1 := by
    replace h := h.le
    by_contra! hn
    grw [← hn, one_smul, ← angle_nonneg x y, zero_add, two_mul] at h
    have h' := h.trans_eq (add_comm _ _)
    grw [angle_le_pi] at h' h
    rw [add_le_add_iff_left, (angle_le_pi _ _).ge_iff_eq, angle_comm, angle_eq_pi_iff] at h' h
    obtain ⟨hxy, r₁, r₁_pos, hr₁⟩ := h'
    obtain ⟨-, r₂, r₂_pos, hr₂⟩ := h
    have : (r₁ + r₂ - 1) • (x + y) = 0 := by
      rw [sub_smul, add_smul, one_smul, ← hr₁, ← hr₂, sub_eq_zero]
    cases smul_eq_zero.1 this
    · linarith
    · contradiction
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
h : angle x y + n • (2 * π) = angle x (x + y) + angle y (x + y)
this_1 : -1 < n
this : n < 1
⊢ n = 0

Tactic:
lia
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
h : angle x y + n • (2 * π) = angle x (x + y) + angle y (x + y)
this_1 : -1 < n
this : n < 1
⊢ angle x y + HSMul.hSMul (α := ℤ) 0 (2 * π) = angle x (x + y) + angle y (x + y)

Tactic:
obtain rfl : n = 0 := by lia

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
h : angle x y + n • (2 * π) = angle x (x + y) + angle y (x + y)
this_1 : -1 < n
this : n < 1
h₁ : angle x y + HSMul.hSMul (α := ℤ) 0 (2 * π) = angle x (x + y) + angle y (x + y)
⊢ LT.lt (α := ℤ) (-1) 0

Tactic:
obtain rfl : n = 0 := by lia

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
h : angle x y + n • (2 * π) = angle x (x + y) + angle y (x + y)
this_1 : -1 < n
this : n < 1
h₁ : angle x y + HSMul.hSMul (α := ℤ) 0 (2 * π) = angle x (x + y) + angle y (x + y)
this₁ : LT.lt (α := ℤ) (-1) 0
⊢ LT.lt (α := ℤ) 0 1

Tactic:
obtain rfl : n = 0 := by lia

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
h : angle x y + HSMul.hSMul (α := ℤ) 0 (2 * π) = angle x (x + y) + angle y (x + y)
this_1 : LT.lt (α := ℤ) (-1) 0
this : LT.lt (α := ℤ) 0 1
⊢ angle x y = angle x (x + y) + angle y (x + y)

Tactic:
simpa using h
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
⊢ angle (x - y) y = angle (x - y) (x - y + y) + angle y (x - y + y)

Tactic:
have h := angle_eq_angle_add_add_angle_add (x - y) hy
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
h : angle (x - y) y = angle (x - y) (x - y + y) + angle y (x - y + y)
⊢ angle (x - y) y = angle (x - y) x + angle y x

Tactic:
rw [sub_add_cancel] at h

Premises used: sub_add_cancel
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
h : angle (x - y) y = angle (x - y) x + angle y x
rw : angle x y + angle x (x - y) + (π - angle y (x - y)) = π
⊢ angle x y + angle x (x - y) + angle y (y - x) = π

Tactic:
rw [← neg_sub x y, angle_neg_right]

Premises used: neg_sub, InnerProductGeometry.angle_neg_right
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
h : angle (x - y) y = angle (x - y) x + angle y x
⊢ angle y (x - y) = angle x (x - y) + angle x y

Tactic:
simp only [angle_comm] at h ⊢

Premises used: InnerProductGeometry.angle_comm
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
h : angle y (x - y) = angle x (x - y) + angle x y
⊢ angle x y + angle x (x - y) + (π - angle y (x - y)) = π

Tactic:
linear_combination -h
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : HSMul.hSMul (α := ℤ) 2 (o.oangle x (x - y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
⊢ (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : HSMul.hSMul (α := ℤ) 2 (o.oangle x (x - y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
⊢ (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign

Tactic:
have hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign := by simp
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : HSMul.hSMul (α := ℤ) 2 (o.oangle x (x - y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
⊢ o.oangle x (x - y) = o.oangle (y - x) y ∨ o.oangle x (x - y) = o.oangle (y - x) y + (↑π : Real.Angle)

Tactic:
rw [Real.Angle.two_zsmul_eq_iff] at h

Premises used: Real.Angle.two_zsmul_eq_iff
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : HSMul.hSMul (α := ℤ) 2 (o.oangle x (x - y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h₁ : o.oangle x (x - y) = o.oangle (y - x) y ∨ o.oangle x (x - y) = o.oangle (y - x) y + (↑π : Real.Angle)
⊢ o.oangle x y ≠ 0

Tactic:
rw [Real.Angle.two_zsmul_eq_iff] at h

Premises used: Real.Angle.two_zsmul_eq_iff
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : HSMul.hSMul (α := ℤ) 2 (o.oangle x (x - y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h₁ : o.oangle x (x - y) = o.oangle (y - x) y ∨ o.oangle x (x - y) = o.oangle (y - x) y + (↑π : Real.Angle)
h0₁ : o.oangle x y ≠ 0
⊢ o.oangle x y ≠ (↑π : Real.Angle)

Tactic:
rw [Real.Angle.two_zsmul_eq_iff] at h

Premises used: Real.Angle.two_zsmul_eq_iff
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : HSMul.hSMul (α := ℤ) 2 (o.oangle x (x - y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h₁ : o.oangle x (x - y) = o.oangle (y - x) y ∨ o.oangle x (x - y) = o.oangle (y - x) y + (↑π : Real.Angle)
h0₁ : o.oangle x y ≠ 0
hpi₁ : o.oangle x y ≠ (↑π : Real.Angle)
⊢ (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign

Tactic:
rw [Real.Angle.two_zsmul_eq_iff] at h

Premises used: Real.Angle.two_zsmul_eq_iff
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x (x - y) = o.oangle (y - x) y ∨ o.oangle x (x - y) = o.oangle (y - x) y + (↑π : Real.Angle)
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
inl : ∀ (h : o.oangle x (x - y) = o.oangle (y - x) y), ‖x‖ = ‖y‖
inr : ∀ (h : o.oangle x (x - y) = o.oangle (y - x) y + (↑π : Real.Angle)), ‖x‖ = ‖y‖
⊢ ‖x‖ = ‖y‖

Tactic:
rcases h with h | h
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : o.oangle x (x - y) = o.oangle (y - x) y
⊢ angle x (x - y) = angle y (y - x)

Tactic:
rw [← o.angle_eq_iff_oangle_eq_of_sign_eq (o.left_ne_zero_of_oangle_ne_zero h0)
      (sub_ne_zero_of_ne (o.ne_of_oangle_ne_zero h0))
      (sub_ne_zero_of_ne (o.ne_of_oangle_ne_zero h0).symm)
      (o.right_ne_zero_of_oangle_ne_zero h0) hs, angle_comm (y - x)] at h

Premises used: Orientation.left_ne_zero_of_oangle_ne_zero, HSub.hSub, Orientation.ne_of_oangle_ne_zero, Ne.symm, Orientation.right_ne_zero_of_oangle_ne_zero, Orientation.angle_eq_iff_oangle_eq_of_sign_eq, InnerProductGeometry.angle_comm, sub_ne_zero_of_ne
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : angle x (x - y) = angle y (y - x)
⊢ ‖x‖ = ‖y‖

Tactic:
norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi h ?_

Premises used: InnerProductGeometry.norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : angle x (x - y) = angle y (y - x)
inl : angle x y ≠ π
⊢ ‖x‖ = ‖y‖

Tactic:
refine norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi h ?_

Premises used: InnerProductGeometry.norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : angle x (x - y) = angle y (y - x)
inl : ¬o.oangle x y = (↑π : Real.Angle)
⊢ angle x y ≠ π

Tactic:
rw [ne_eq, ← o.oangle_eq_pi_iff_angle_eq_pi]

Premises used: Orientation.oangle_eq_pi_iff_angle_eq_pi, ne_eq
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : angle x (x - y) = angle y (y - x)
⊢ ¬o.oangle x y = (↑π : Real.Angle)

Tactic:
hpi
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : angle x (x - y) = angle y (y - x)
⊢ ¬o.oangle x y = (↑π : Real.Angle)

Tactic:
exact hpi
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : o.oangle x (x - y) = o.oangle (y - x) y + (↑π : Real.Angle)
⊢ o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle)

Tactic:
rw [h, Real.Angle.sign_add_pi, SignType.neg_eq_self_iff, oangle_sign_sub_left_swap,
      o.oangle_rev, Real.Angle.sign_neg, SignType.neg_eq_zero_iff,
      Real.Angle.sign_eq_zero_iff] at hs

Premises used: Orientation.oangle_sign_sub_left_swap, Real.Angle.sign_neg, SignType.neg_eq_zero_iff, SignType.neg_eq_self_iff, Real.Angle.sign_eq_zero_iff, Real.Angle.sign_add_pi, Orientation.oangle_rev