-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi {x y : V}
    (h : angle x (x - y) = angle y (y - x)) (hpi : angle x y ≠ π) : ‖x‖ = ‖y‖

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
hx0 : ¬x = 0
hy0 : ¬y = 0
hyx : ¬‖y‖ = ‖x‖
h : angle x y = π
⊢ False

Tactic:
exact hpi h

Result:
no goals

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = inner x y * (‖x‖⁻¹ - ‖y‖⁻¹)
hx0 : ¬x = 0
⊢ ‖x‖ = ‖y‖

Tactic:
by_cases hy0 : y = 0

Result:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = inner x y * (‖x‖⁻¹ - ‖y‖⁻¹)
hx0 : ¬x = 0
hy0 : y = 0
⊢ ‖x‖ = ‖y‖

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = inner x y * (‖x‖⁻¹ - ‖y‖⁻¹)
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ‖x‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : inner x (x - y) / (‖x‖ * ‖x - y‖) = inner y (y - x) / (‖y‖ * ‖y - x‖)
⊢ ‖x‖ = ‖y‖

Tactic:
by_cases hxy : x = y

Result:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : inner x (x - y) / (‖x‖ * ‖x - y‖) = inner y (y - x) / (‖y‖ * ‖y - x‖)
hxy : x = y
⊢ ‖x‖ = ‖y‖

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : inner x (x - y) / (‖x‖ * ‖x - y‖) = inner y (y - x) / (‖y‖ * ‖y - x‖)
hxy : ¬x = y
⊢ ‖x‖ = ‖y‖

Proof state:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : inner x (x - y) / (‖x‖ * ‖x - y‖) = inner y (y - x) / (‖y‖ * ‖y - x‖)
hxy : x = y
⊢ ‖x‖ = ‖y‖

Tactic:
rw [hxy]

Result:
no goals

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = inner x y * (‖x‖⁻¹ - ‖y‖⁻¹)
⊢ ‖x‖ = ‖y‖

Tactic:
by_cases hx0 : x = 0

Result:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = inner x y * (‖x‖⁻¹ - ‖y‖⁻¹)
hx0 : x = 0
⊢ ‖x‖ = ‖y‖

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = inner x y * (‖x‖⁻¹ - ‖y‖⁻¹)
hx0 : ¬x = 0
⊢ ‖x‖ = ‖y‖

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : inner x (x - y) * ‖x‖⁻¹ * ‖x - y‖⁻¹ = inner y (y - x) * ‖y‖⁻¹ * ‖x - y‖⁻¹
hxy : ¬x = y
⊢ ‖x‖ = ‖y‖

Tactic:
replace h :=
  mul_right_cancel₀ (inv_ne_zero fun hz => hxy (eq_of_sub_eq_zero (norm_eq_zero.1 hz))) h

Result:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : inner x (x - y) * ‖x‖⁻¹ = inner y (y - x) * ‖y‖⁻¹
⊢ ‖x‖ = ‖y‖

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : (‖y‖ - ‖x‖) * -1 = (‖y‖ - ‖x‖) * (inner x y / (‖x‖ * ‖y‖))
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ‖y‖ = ‖x‖

Tactic:
by_contra hyx

Result:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : (‖y‖ - ‖x‖) * -1 = (‖y‖ - ‖x‖) * (inner x y / (‖x‖ * ‖y‖))
hx0 : ¬x = 0
hy0 : ¬y = 0
hyx : ¬‖y‖ = ‖x‖
⊢ False

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : (‖y‖ - ‖x‖) * -1 = (‖y‖ - ‖x‖) * (inner x y / (‖x‖ * ‖y‖))
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ‖x‖ = ‖y‖

Tactic:
symm

Result:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : (‖y‖ - ‖x‖) * -1 = (‖y‖ - ‖x‖) * (inner x y / (‖x‖ * ‖y‖))
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ‖y‖ = ‖x‖

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : inner x (x - y) / (‖x‖ * ‖x - y‖) = inner y (y - x) / (‖y‖ * ‖y - x‖)
hxy : ¬x = y
⊢ ‖x‖ = ‖y‖

Tactic:
rw [← norm_neg (y - x), neg_sub, mul_comm, mul_comm ‖y‖, div_eq_mul_inv, div_eq_mul_inv,
  mul_inv_rev, mul_inv_rev, ← mul_assoc, ← mul_assoc] at h

Result:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : inner x (x - y) * ‖x‖⁻¹ * ‖x - y‖⁻¹ = inner y (y - x) * ‖y‖⁻¹ * ‖x - y‖⁻¹
hxy : ¬x = y
⊢ ‖x‖ = ‖y‖

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : (‖y‖ - ‖x‖) * -1 = (‖y‖ - ‖x‖) * (inner x y / (‖x‖ * ‖y‖))
hx0 : ¬x = 0
hy0 : ¬y = 0
hyx : ¬‖y‖ = ‖x‖
⊢ False

Tactic:
replace h := (mul_left_cancel₀ (sub_ne_zero_of_ne hyx) h).symm

Result:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
hx0 : ¬x = 0
hy0 : ¬y = 0
hyx : ¬‖y‖ = ‖x‖
h : inner x y / (‖x‖ * ‖y‖) = -1
⊢ False

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : inner x (x - y) * ‖x‖⁻¹ = inner y (y - x) * ‖y‖⁻¹
⊢ ‖x‖ = ‖y‖

Tactic:
rw [inner_sub_right, inner_sub_right, real_inner_comm x y, real_inner_self_eq_norm_mul_norm,
  real_inner_self_eq_norm_mul_norm, mul_sub_right_distrib, mul_sub_right_distrib,
  mul_self_mul_inv, mul_self_mul_inv, sub_eq_sub_iff_sub_eq_sub, ← mul_sub_left_distrib] at h

Result:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = inner x y * (‖x‖⁻¹ - ‖y‖⁻¹)
⊢ ‖x‖ = ‖y‖

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = inner x y * (‖x‖⁻¹ - ‖y‖⁻¹)
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ‖x‖ = ‖y‖

Tactic:
rw [inv_sub_inv (fun hz => hx0 (norm_eq_zero.1 hz)) fun hz => hy0 (norm_eq_zero.1 hz), ←
  neg_sub, ← mul_div_assoc, mul_comm, mul_div_assoc, ← mul_neg_one] at h

Result:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : (‖y‖ - ‖x‖) * -1 = (‖y‖ - ‖x‖) * (inner x y / (‖x‖ * ‖y‖))
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ‖x‖ = ‖y‖

Proof state:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = inner x y * (‖x‖⁻¹ - ‖y‖⁻¹)
hx0 : x = 0
⊢ ‖x‖ = ‖y‖

Tactic:
rw [hx0, norm_zero, inner_zero_left, zero_mul, zero_sub, neg_eq_zero] at h

Result:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖y‖ = 0
hx0 : x = 0
⊢ ‖x‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x (x - y) = angle y (y - x)
hpi : angle x y ≠ π
⊢ ‖x‖ = ‖y‖

Tactic:
replace h := Real.arccos_injOn (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x (x - y)))
  (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one y (y - x))) h

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : inner x (x - y) / (‖x‖ * ‖x - y‖) = inner y (y - x) / (‖y‖ * ‖y - x‖)
⊢ ‖x‖ = ‖y‖