-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem angle_add_angle_sub_add_angle_sub_eq_pi {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    angle x y + angle x (x - y) + angle y (y - x) = π

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
hsin : Real.sin (angle x y + angle x (x - y) + angle y (y - x)) = 0
⊢ angle x y + angle x (x - y) + angle y (y - x) = π

Tactic:
rw [Real.sin_eq_zero_iff] at hsin

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
hsin : ∃ n, ↑n * π = angle x y + angle x (x - y) + angle y (y - x)
⊢ angle x y + angle x (x - y) + angle y (y - x) = π

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
n : ℤ
hn : angle x y + angle x (x - y) + angle y (y - x) = ↑n * π
h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)
⊢ angle x y + angle x (x - y) + angle y (y - x) < π + π + π

Tactic:
by_contra hnlt

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
n : ℤ
hn : angle x y + angle x (x - y) + angle y (y - x) = ↑n * π
h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)
hnlt : ¬angle x y + angle x (x - y) + angle y (y - x) < π + π + π
⊢ False

Proof state:
case intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
n : ℤ
hn : ↑n * π = angle x y + angle x (x - y) + angle y (y - x)
⊢ angle x y + angle x (x - y) + angle y (y - x) = π

Tactic:
symm at hn

Result:
case intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
n : ℤ
hn : angle x y + angle x (x - y) + angle y (y - x) = ↑n * π
⊢ angle x y + angle x (x - y) + angle y (y - x) = π

Proof state:
case intro.«0»
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
n : ℤ
h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)
h3lt : angle x y + angle x (x - y) + angle y (y - x) < π + π + π
hn : angle x y + angle x (x - y) + angle y (y - x) = ↑0 * π
hn0 : 0 ≤ 0
hn3 : 0 < 3
⊢ angle x y + angle x (x - y) + angle y (y - x) = π

Tactic:
simp [hn] at hcos

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
n : ℤ
hn : angle x y + angle x (x - y) + angle y (y - x) = ↑n * π
h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)
hnlt : ¬angle x y + angle x (x - y) + angle y (y - x) < π + π + π
⊢ False

Tactic:
have hxy : angle x y = π := by
  by_contra hxy
  exact hnlt (add_lt_add_of_lt_of_le (add_lt_add_of_lt_of_le (lt_of_le_of_ne
    (angle_le_pi _ _) hxy) (angle_le_pi _ _)) (angle_le_pi _ _))

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
n : ℤ
hn : angle x y + angle x (x - y) + angle y (y - x) = ↑n * π
h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)
hnlt : ¬angle x y + angle x (x - y) + angle y (y - x) < π + π + π
hxy : angle x y = π
⊢ False

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
n : ℤ
hn : angle x y + angle x (x - y) + angle y (y - x) = ↑n * π
h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)
h3lt : angle x y + angle x (x - y) + angle y (y - x) < π + π + π
hn0 : 0 ≤ n
⊢ n < 3

Tactic:
rw [hn, show π + π + π = 3 * π by ring] at h3lt

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
n : ℤ
hn : angle x y + angle x (x - y) + angle y (y - x) = ↑n * π
h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)
h3lt : ↑n * π < 3 * π
hn0 : 0 ≤ n
⊢ n < 3

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
⊢ angle x y + angle x (x - y) + angle y (y - x) = π

Tactic:
have hsin := sin_angle_add_angle_sub_add_angle_sub_eq_zero hx hy

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
hsin : Real.sin (angle x y + angle x (x - y) + angle y (y - x)) = 0
⊢ angle x y + angle x (x - y) + angle y (y - x) = π

Proof state:
case intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
n : ℤ
hn : angle x y + angle x (x - y) + angle y (y - x) = ↑n * π
h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)
h3lt : angle x y + angle x (x - y) + angle y (y - x) < π + π + π
hn0 : 0 ≤ n
hn3 : n < 3
⊢ angle x y + angle x (x - y) + angle y (y - x) = π

Tactic:
interval_cases n

Result:
case intro.«0»
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
n : ℤ
h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)
h3lt : angle x y + angle x (x - y) + angle y (y - x) < π + π + π
hn : angle x y + angle x (x - y) + angle y (y - x) = ↑0 * π
hn0 : 0 ≤ 0
hn3 : 0 < 3
⊢ angle x y + angle x (x - y) + angle y (y - x) = π

case intro.«1»
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
n : ℤ
h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)
h3lt : angle x y + angle x (x - y) + angle y (y - x) < π + π + π
hn : angle x y + angle x (x - y) + angle y (y - x) = ↑1 * π
hn0 : 0 ≤ 1
hn3 : 1 < 3
⊢ angle x y + angle x (x - y) + angle y (y - x) = π

case intro.«2»
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
n : ℤ
h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)
h3lt : angle x y + angle x (x - y) + angle y (y - x) < π + π + π
hn : angle x y + angle x (x - y) + angle y (y - x) = ↑2 * π
hn0 : 0 ≤ 2
hn3 : 2 < 3
⊢ angle x y + angle x (x - y) + angle y (y - x) = π

Proof state:
case intro.intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx✝ : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
n : ℤ
hn : angle x y + angle x (x - y) + angle y (y - x) = ↑n * π
h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)
hx : x ≠ 0
r : ℝ
hnlt : ¬π + angle (r • x) (r • x - x) < π + π + π
hr : r < 0
hxr : y = r • x
⊢ False

Tactic:
apply hnlt

Result:
case intro.intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx✝ : x ≠ 0
hy : y ≠ 0
hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
n : ℤ
hn : angle x y + angle x (x - y) + angle y (y - x) = ↑n * π
h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)
hx : x ≠ 0
r : ℝ
hnlt : ¬π + angle (r • x) (r • x - x) < π + π + π
hr : r < 0
hxr : y = r • x
⊢ π + angle (r • x) (r • x - x) < π + π + π