-- 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
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 * π < π + π + π
hn0 : 0 ≤ n
⊢ π + π + π = 3 * π

Tactic:
ring

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 ≤ ↑n
h3lt : angle x y + angle x (x - y) + angle y (y - x) < π + π + π
⊢ 0 ≤ n

Tactic:
norm_cast at h0

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) < π + π + π
hxy : ¬angle x y = π
⊢ False

Tactic:
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:
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)
h3lt : ↑n * π < 3 * π
hn0 : 0 ≤ n
⊢ n < 3

Tactic:
replace h3lt := lt_of_mul_lt_mul_right h3lt (le_of_lt Real.pi_pos)

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)
hn0 : 0 ≤ n
h3lt : ↑n < 3
⊢ n < 3

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)
hnlt : ¬π + angle x (x - y) + angle y (y - x) < π + π + π
hx : x ≠ 0
r : ℝ
hr : r < 0
hxr : y = r • x
⊢ False

Tactic:
rw [hxr, ← one_smul ℝ x, ← mul_smul, mul_one, ← sub_smul, one_smul, sub_eq_add_neg,
  angle_smul_right_of_pos _ _ (add_pos zero_lt_one (neg_pos_of_neg hr)), angle_self hx,
  add_zero] at 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
⊢ False

Proof state:
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) = π

Tactic:
simp [hn] at hcos

Result:
no goals

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 * π
⊢ angle x y + angle x (x - y) + angle y (y - x) = π

Tactic:
have h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x) :=
  add_nonneg (add_nonneg (angle_nonneg _ _) (angle_nonneg _ _)) (angle_nonneg _ _)

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 * π
h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)
⊢ 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
⊢ π + angle (r • x) (r • x - x) < π + π + π

Tactic:
rw [add_assoc]

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) < π + (π + π)

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 (x - y) + angle y (y - x) < π + π + π
hxy : angle x y = π
⊢ False

Tactic:
rw [angle_eq_pi_iff] at hxy

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 (x - y) + angle y (y - x) < π + π + π
hxy : x ≠ 0 ∧ ∃ r < 0, y = r • x
⊢ 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
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) = π

Tactic:
obtain ⟨n, hn⟩ := hsin

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 : ↑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:
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) = π

Tactic:
norm_num [hn]

Result:
no goals