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
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
have inr : √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
  √(‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - ⟪x, y⟫ * ⟪x, y⟫)
Tactic: simp only [real_inner_self_eq_norm_mul_norm]
-- 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
⊢ sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)
have rw : sin (angle x y) = sin (angle x y) * (‖x‖ * ‖y‖) / (‖x‖ * ‖y‖)
Tactic: rw [← sin_angle_mul_norm_mul_norm]
-- 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 : x + y ≠ 0
⊢ sin (angle x (x + y)) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖)
have rw : √(⟪x, x⟫ * ⟪x + y, x + y⟫ - ⟪x, x + y⟫ * ⟪x, x + y⟫) / (‖x‖ * ‖x + y‖) =
  √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖)
Tactic: rw [sin_angle 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 : x + y ≠ 0
⊢ √(⟪x, x⟫ * ⟪x + y, x + y⟫ - ⟪x, x + y⟫ * ⟪x, x + y⟫) / (‖x‖ * ‖x + y‖) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖)
have field_simp : √(⟪x, x⟫ * ⟪x + y, x + y⟫ - HPow.hPow (β := ℕ) ⟪x, x + y⟫ 2) = √(⟪x, x⟫ * ⟪y, y⟫ - HPow.hPow (β := ℕ) ⟪x, y⟫ 2)
Tactic: field_simp
-- 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 : x + y ≠ 0
⊢ √(⟪x, x⟫ * ⟪x + y, x + y⟫ - HPow.hPow (β := ℕ) ⟪x, x + y⟫ 2) = √(⟪x, x⟫ * ⟪y, y⟫ - HPow.hPow (β := ℕ) ⟪x, y⟫ 2)
have simp : √(⟪x, x⟫ * (⟪x, x⟫ + ⟪x, y⟫ + (⟪x, y⟫ + ⟪y, y⟫)) - HPow.hPow (β := ℕ) (⟪x, x⟫ + ⟪x, y⟫) 2) =
  √(⟪x, x⟫ * ⟪y, y⟫ - HPow.hPow (β := ℕ) ⟪x, y⟫ 2)
Tactic: simp only [inner_add_left, inner_add_right, real_inner_comm]
-- 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
⊢ angle x y = 0 ↔ x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x
have rw : ⟪x, y⟫ / (‖x‖ * ‖y‖) ≤ 1
Tactic: rw [angle, ← real_inner_div_norm_mul_norm_eq_one_iff, Real.arccos_eq_zero, LE.le.ge_iff_eq',
    eq_comm]
-- 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
⊢ angle x y = π ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x
have rw : -1 ≤ ⟪x, y⟫ / (‖x‖ * ‖y‖)
Tactic: rw [angle, ← real_inner_div_norm_mul_norm_eq_neg_one_iff, Real.arccos_eq_pi, LE.le.ge_iff_eq']
-- 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 z : V
h : angle x y = π
⊢ angle x z + angle y z = π
have rcases : x ≠ 0 → ∀ (r : ℝ) (hr : r < 0) (h : angle x (r • x) = π), angle x z + angle (r • x) z = π
Tactic: rcases angle_eq_pi_iff.1 h with ⟨_, ⟨r, ⟨hr, rfl⟩⟩⟩
Cleared hypotheses: y, h
-- 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 z : V
left : x ≠ 0
r : ℝ
hr : r < 0
h : angle x (r • x) = π
⊢ angle x z + angle (r • x) z = π
have rw : angle x z + angle (-x) z = π
Tactic: rw [angle_smul_left_of_neg x z hr, angle_neg_left, add_sub_cancel]
-- 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 z : V
left : x ≠ 0
r : ℝ
hr : r < 0
h : angle x (r • x) = π
rw : angle x z + angle (-x) z = π
⊢ angle x z + angle (r • x) z = π
have rw₁ : angle x z + (π - angle x z) = π
Tactic: rw [angle_smul_left_of_neg x z hr, angle_neg_left, add_sub_cancel]
-- 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 z : V
left : x ≠ 0
r : ℝ
hr : r < 0
h : angle x (r • x) = π
rw : angle x z + angle (-x) z = π
rw₁ : angle x z + (π - angle x z) = π
⊢ angle x z + angle (r • x) z = π
have rw₂ : π = π
Tactic: rw [angle_smul_left_of_neg x z hr, angle_neg_left, add_sub_cancel]
-- 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 = π
have refine : ∀ (h : ⟪x, y⟫ = -(‖x‖ * ‖y‖)), angle x y = π
Tactic: refine ⟨fun h => ?_, inner_eq_neg_mul_norm_of_angle_eq_pi⟩
-- 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‖)
⊢ angle x y = π
have h₁ : ‖x‖ * ‖y‖ ≠ 0
Tactic: have h₁ : ‖x‖ * ‖y‖ ≠ 0 := (mul_pos (norm_pos_iff.mpr hx) (norm_pos_iff.mpr hy)).ne'
-- 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‖)
h₁ : ‖x‖ * ‖y‖ ≠ 0
⊢ angle x y = π
have rw : arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = π
Tactic: rw [angle, h, neg_div, div_self h₁, Real.arccos_neg_one]
-- 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‖)
h₁ : ‖x‖ * ‖y‖ ≠ 0
rw : arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = π
⊢ angle x y = π
have rw₁ : arccos (-(‖x‖ * ‖y‖) / (‖x‖ * ‖y‖)) = π
Tactic: rw [angle, h, neg_div, div_self h₁, Real.arccos_neg_one]
-- 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‖)
h₁ : ‖x‖ * ‖y‖ ≠ 0
rw : arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = π
rw₁ : arccos (-(‖x‖ * ‖y‖) / (‖x‖ * ‖y‖)) = π
⊢ angle x y = π
have rw₂ : arccos (-(‖x‖ * ‖y‖ / (‖x‖ * ‖y‖))) = π
Tactic: rw [angle, h, neg_div, div_self h₁, Real.arccos_neg_one]
-- 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‖)
h₁ : ‖x‖ * ‖y‖ ≠ 0
rw : arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = π
rw₁ : arccos (-(‖x‖ * ‖y‖) / (‖x‖ * ‖y‖)) = π
rw₂ : arccos (-(‖x‖ * ‖y‖ / (‖x‖ * ‖y‖))) = π
⊢ angle x y = π
have rw₃ : arccos (-1) = π
Tactic: rw [angle, h, neg_div, div_self h₁, Real.arccos_neg_one]
-- 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‖)
h₁ : ‖x‖ * ‖y‖ ≠ 0
rw : arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = π
rw₁ : arccos (-(‖x‖ * ‖y‖) / (‖x‖ * ‖y‖)) = π
rw₂ : arccos (-(‖x‖ * ‖y‖ / (‖x‖ * ‖y‖))) = π
rw₃ : arccos (-1) = π
⊢ angle x y = π
have rw₄ : π = π
Tactic: rw [angle, h, neg_div, div_self h₁, Real.arccos_neg_one]
-- 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 => ?_, inner_eq_mul_norm_of_angle_eq_zero⟩
-- 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‖
⊢ angle x y = 0
have h₁ : ‖x‖ * ‖y‖ ≠ 0
Tactic: have h₁ : ‖x‖ * ‖y‖ ≠ 0 := (mul_pos (norm_pos_iff.mpr hx) (norm_pos_iff.mpr hy)).ne'
-- 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‖
h₁ : ‖x‖ * ‖y‖ ≠ 0
⊢ angle x y = 0
have rw : arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = 0
Tactic: rw [angle, h, div_self h₁, Real.arccos_one]
-- 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‖
h₁ : ‖x‖ * ‖y‖ ≠ 0
rw : arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = 0
⊢ angle x y = 0
have rw₁ : arccos (‖x‖ * ‖y‖ / (‖x‖ * ‖y‖)) = 0
Tactic: rw [angle, h, div_self h₁, Real.arccos_one]
-- 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‖
h₁ : ‖x‖ * ‖y‖ ≠ 0
rw : arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = 0
rw₁ : arccos (‖x‖ * ‖y‖ / (‖x‖ * ‖y‖)) = 0
⊢ angle x y = 0
have rw₂ : arccos 1 = 0
Tactic: rw [angle, h, div_self h₁, Real.arccos_one]
-- 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‖
h₁ : ‖x‖ * ‖y‖ ≠ 0
rw : arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = 0
rw₁ : arccos (‖x‖ * ‖y‖ / (‖x‖ * ‖y‖)) = 0
rw₂ : arccos 1 = 0
⊢ angle x y = 0
have rw₃ : Eq (α := ℝ) 0 0
Tactic: rw [angle, h, div_self h₁, Real.arccos_one]
-- 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
h : angle x y = π
⊢ ‖x - y‖ = ‖x‖ + ‖y‖
have rw : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * -(‖x‖ * ‖y‖) + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
Tactic: rw [← sq_eq_sq₀ (norm_nonneg (x - y)) (add_nonneg (norm_nonneg x) (norm_nonneg y)),
    norm_sub_pow_two_real, inner_eq_neg_mul_norm_of_angle_eq_pi h]
-- 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
h : angle x y = 0
⊢ ‖x + y‖ = ‖x‖ + ‖y‖
have rw : HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * (‖x‖ * ‖y‖) + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
Tactic: rw [← sq_eq_sq₀ (norm_nonneg (x + y)) (add_nonneg (norm_nonneg x) (norm_nonneg y)),
    norm_add_pow_two_real, inner_eq_mul_norm_of_angle_eq_zero h]
-- 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
h : angle x y = 0
⊢ ‖x - y‖ = |‖x‖ - ‖y‖|
have rw : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * (‖x‖ * ‖y‖) + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
Tactic: rw [← sq_eq_sq₀ (norm_nonneg (x - y)) (abs_nonneg (‖x‖ - ‖y‖)), norm_sub_pow_two_real,
    inner_eq_mul_norm_of_angle_eq_zero h, sq_abs (‖x‖ - ‖y‖)]
-- 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 = π
have refine : ∀ (h : ‖x - y‖ = ‖x‖ + ‖y‖), angle x y = π
Tactic: refine ⟨fun h => ?_, norm_sub_eq_add_norm_of_angle_eq_pi⟩
-- 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 = π
have rw : ⟪x, y⟫ = -(‖x‖ * ‖y‖)
Tactic: rw [← inner_eq_neg_mul_norm_iff_angle_eq_pi hx hy]
-- 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 hxy₁ : 0 ≤ ‖x - y‖
Tactic: obtain ⟨hxy₁, hxy₂⟩ := norm_nonneg (x - y), add_nonneg (norm_nonneg x) (norm_nonneg 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‖
hxy₁ : 0 ≤ ‖x - y‖
⊢ ⟪x, y⟫ = -(‖x‖ * ‖y‖)
have hxy₂ : 0 ≤ ‖x‖ + ‖y‖
Tactic: obtain ⟨hxy₁, hxy₂⟩ := norm_nonneg (x - y), add_nonneg (norm_nonneg x) (norm_nonneg 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‖
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ ⟪x, y⟫ = -(‖x‖ * ‖y‖)
have h₁ : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
Tactic: rw [← sq_eq_sq₀ hxy₁ hxy₂, norm_sub_pow_two_real] at h
Cleared hypotheses: h, hxy₁, hxy₂
-- 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⟫ = (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2
have linarith : ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖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 : 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
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2
have linarith₃ : ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖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 : 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
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2
have linarith₄ : ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖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 : 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
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2
have linarith₅ : ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖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 : 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
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2
have 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
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
⊢ ⟪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⟫ →
  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 : 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
⊢ ⟪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⟫ → 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 : 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
⊢ ⟪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⟫ →
  HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith