awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
linarith linarith₁ linarith₂ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₃ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 → 2 / 2 = 1
linarith₄ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 →
    GT.gt (α := ℝ) 2 0
linarith₆ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 →
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 +
        (2 * ⟪x, y⟫ -
          (1 * HPow.hPow (β := ℕ) (1 * ‖x‖) 2 + 1 * HPow.hPow (β := ℕ) (1 * ‖y‖) 2 -
            1 * HPow.hPow (β := ℕ) (1 * ‖x‖ + 1 * ‖y‖) 2)) =
      0
linarith₇ linarith₈ linarith₉ :
  (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 < ⟪x, y⟫ →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₁₀ :
  (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 < ⟪x, y⟫ → 2 / 2 = 1
linarith₁₁ :
  (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 < ⟪x, y⟫ →
    HMul.hMul (α := ℝ) 1 2 = 2
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2
have linarith₁₂ : (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 < ⟪x, y⟫ →
  GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
linarith linarith₁ linarith₂ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₃ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 → 2 / 2 = 1
linarith₄ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 →
    GT.gt (α := ℝ) 2 0
linarith₆ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 →
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 +
        (2 * ⟪x, y⟫ -
          (1 * HPow.hPow (β := ℕ) (1 * ‖x‖) 2 + 1 * HPow.hPow (β := ℕ) (1 * ‖y‖) 2 -
            1 * HPow.hPow (β := ℕ) (1 * ‖x‖ + 1 * ‖y‖) 2)) =
      0
linarith₇ linarith₈ linarith₉ :
  (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 < ⟪x, y⟫ →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₁₀ :
  (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 < ⟪x, y⟫ → 2 / 2 = 1
linarith₁₁ :
  (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 < ⟪x, y⟫ →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₂ :
  (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 < ⟪x, y⟫ →
    GT.gt (α := ℝ) 2 0
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2
have linarith₁₃ : (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 < ⟪x, y⟫ →
  -(HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) +
      (1 * HPow.hPow (β := ℕ) (1 * ‖x‖) 2 + 1 * HPow.hPow (β := ℕ) (1 * ‖y‖) 2 -
          1 * HPow.hPow (β := ℕ) (1 * ‖x‖ + 1 * ‖y‖) 2 -
        2 * ⟪x, y⟫) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ ⟪x, y⟫ = -(‖x‖ * ‖y‖)
have by : ⟪x, y⟫ = (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2
Tactic: calc
    ⟪x, y⟫ = (‖x‖ ^ 2 + ‖y‖ ^ 2 - (‖x‖ + ‖y‖) ^ 2) / 2 := by linarith
    _ = -(‖x‖ * ‖y‖) := by ring
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
by : ⟪x, y⟫ = (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2
⊢ ⟪x, y⟫ = -(‖x‖ * ‖y‖)
have by₁ : (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 = -(‖x‖ * ‖y‖)
Tactic: calc
    ⟪x, y⟫ = (‖x‖ ^ 2 + ‖y‖ ^ 2 - (‖x‖ + ‖y‖) ^ 2) / 2 := by linarith
    _ = -(‖x‖ * ‖y‖) := by ring
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ ↔ angle x y = 0
have refine : ‖x + y‖ = ‖x‖ + ‖y‖ → angle x y = 0
Tactic: refine ⟨?_, norm_add_eq_add_norm_of_angle_eq_zero⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x - y‖ = |‖x‖ - ‖y‖| ↔ angle x y = 0
have refine : ∀ (h : ‖x - y‖ = |‖x‖ - ‖y‖|), angle x y = 0
Tactic: refine ⟨fun h => ?_, norm_sub_eq_abs_sub_norm_of_angle_eq_zero⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
⊢ angle x y = 0
have rw : ⟪x, y⟫ = ‖x‖ * ‖y‖
Tactic: rw [← inner_eq_mul_norm_iff_angle_eq_zero hx hy]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
⊢ HPow.hPow (β := ℕ) ‖x - y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
have rw : HPow.hPow (β := ℕ) |‖x‖ - ‖y‖| 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖
have h1 : HPow.hPow (β := ℕ) ‖x - y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
Tactic: have h1 : ‖x - y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2 := by
    rw [h]
    exact sq_abs (‖x‖ - ‖y‖)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : HPow.hPow (β := ℕ) ‖x - y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖
have h1₁ : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
Tactic: rw [norm_sub_pow_two_real] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2
have linarith : ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
  1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
linarith linarith₁ linarith₂ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2
have linarith₃ : ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
linarith linarith₁ linarith₂ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₃ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 → 2 / 2 = 1
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2
have linarith₄ : ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
  HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
linarith linarith₁ linarith₂ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₃ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 → 2 / 2 = 1
linarith₄ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2
have linarith₅ : ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
  GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
linarith linarith₁ linarith₂ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₃ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 → 2 / 2 = 1
linarith₄ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    GT.gt (α := ℝ) 2 0
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2
have linarith₆ : ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
  HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2 +
      (2 * ⟪x, y⟫ -
        (1 * HPow.hPow (β := ℕ) (1 * ‖x‖ + 1 * ‖y‖) 2 - 1 * HPow.hPow (β := ℕ) (1 * ‖x‖) 2 -
          1 * HPow.hPow (β := ℕ) (1 * ‖y‖) 2)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
linarith linarith₁ linarith₂ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₃ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 → 2 / 2 = 1
linarith₄ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    GT.gt (α := ℝ) 2 0
linarith₆ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2 +
        (2 * ⟪x, y⟫ -
          (1 * HPow.hPow (β := ℕ) (1 * ‖x‖ + 1 * ‖y‖) 2 - 1 * HPow.hPow (β := ℕ) (1 * ‖x‖) 2 -
            1 * HPow.hPow (β := ℕ) (1 * ‖y‖) 2)) =
      0
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2
have linarith₇ : (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ →
  1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
linarith linarith₁ linarith₂ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₃ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 → 2 / 2 = 1
linarith₄ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    GT.gt (α := ℝ) 2 0
linarith₆ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2 +
        (2 * ⟪x, y⟫ -
          (1 * HPow.hPow (β := ℕ) (1 * ‖x‖ + 1 * ‖y‖) 2 - 1 * HPow.hPow (β := ℕ) (1 * ‖x‖) 2 -
            1 * HPow.hPow (β := ℕ) (1 * ‖y‖) 2)) =
      0
linarith₇ linarith₈ linarith₉ :
  (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2
have linarith₁₀ : (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
linarith linarith₁ linarith₂ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₃ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 → 2 / 2 = 1
linarith₄ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    GT.gt (α := ℝ) 2 0
linarith₆ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2 +
        (2 * ⟪x, y⟫ -
          (1 * HPow.hPow (β := ℕ) (1 * ‖x‖ + 1 * ‖y‖) 2 - 1 * HPow.hPow (β := ℕ) (1 * ‖x‖) 2 -
            1 * HPow.hPow (β := ℕ) (1 * ‖y‖) 2)) =
      0
linarith₇ linarith₈ linarith₉ :
  (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₁₀ :
  (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ → 2 / 2 = 1
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2
have linarith₁₁ : (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ →
  HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
linarith linarith₁ linarith₂ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₃ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 → 2 / 2 = 1
linarith₄ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    GT.gt (α := ℝ) 2 0
linarith₆ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2 +
        (2 * ⟪x, y⟫ -
          (1 * HPow.hPow (β := ℕ) (1 * ‖x‖ + 1 * ‖y‖) 2 - 1 * HPow.hPow (β := ℕ) (1 * ‖x‖) 2 -
            1 * HPow.hPow (β := ℕ) (1 * ‖y‖) 2)) =
      0
linarith₇ linarith₈ linarith₉ :
  (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₁₀ :
  (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ → 2 / 2 = 1
linarith₁₁ :
  (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ →
    HMul.hMul (α := ℝ) 1 2 = 2
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2
have linarith₁₂ : (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ →
  GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
linarith linarith₁ linarith₂ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₃ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 → 2 / 2 = 1
linarith₄ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    GT.gt (α := ℝ) 2 0
linarith₆ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2 +
        (2 * ⟪x, y⟫ -
          (1 * HPow.hPow (β := ℕ) (1 * ‖x‖ + 1 * ‖y‖) 2 - 1 * HPow.hPow (β := ℕ) (1 * ‖x‖) 2 -
            1 * HPow.hPow (β := ℕ) (1 * ‖y‖) 2)) =
      0
linarith₇ linarith₈ linarith₉ :
  (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₁₀ :
  (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ → 2 / 2 = 1
linarith₁₁ :
  (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₂ :
  (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ →
    GT.gt (α := ℝ) 2 0
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2
have linarith₁₃ : (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ →
  -(HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2) +
      (1 * HPow.hPow (β := ℕ) (1 * ‖x‖ + 1 * ‖y‖) 2 - 1 * HPow.hPow (β := ℕ) (1 * ‖x‖) 2 -
          1 * HPow.hPow (β := ℕ) (1 * ‖y‖) 2 -
        2 * ⟪x, y⟫) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖
have by : ⟪x, y⟫ = (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2
Tactic: calc
    ⟪x, y⟫ = ((‖x‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖y‖ ^ 2) / 2 := by linarith
    _ = ‖x‖ * ‖y‖ := by ring
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
by : ⟪x, y⟫ = (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖
have by₁ : (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 = ‖x‖ * ‖y‖
Tactic: calc
    ⟪x, y⟫ = ((‖x‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖y‖ ^ 2) / 2 := by linarith
    _ = ‖x‖ * ‖y‖ := by ring
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ ‖x + y‖ = ‖x - y‖ ↔ angle x y = π / 2
have rw : HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 ↔
  ⟪x, y⟫ = 0
Tactic: rw [← sq_eq_sq₀ (norm_nonneg (x + y)) (norm_nonneg (x - y)),
    ← inner_eq_zero_iff_angle_eq_pi_div_two x y, norm_add_pow_two_real, norm_sub_pow_two_real]