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
⊢ 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
have mp : 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: constructor
-- 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
mp :
  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
⊢ 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
have mpr : ⟪x, y⟫ = 0 →
  HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: constructor
-- 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 :
  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
have linarith : ⟪x, y⟫ < 0 →
  -(HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 -
          (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2)) +
      4 * (⟪x, y⟫ - 0) =
    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
h :
  HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2
linarith :
  ⟪x, y⟫ < 0 →
    -(HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 -
            (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2)) +
        4 * (⟪x, y⟫ - 0) =
      0
⊢ ⟪x, y⟫ = 0
have linarith₁ : ⟪x, y⟫ < 0 → GT.gt (α := ℝ) 4 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
h :
  HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2
linarith :
  ⟪x, y⟫ < 0 →
    -(HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 -
            (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2)) +
        4 * (⟪x, y⟫ - 0) =
      0
linarith₁ : ⟪x, y⟫ < 0 → GT.gt (α := ℝ) 4 0
⊢ ⟪x, y⟫ = 0
have linarith₂ : 0 < ⟪x, y⟫ →
  HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 -
        (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2) +
      4 * (0 - ⟪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
h :
  HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2
linarith :
  ⟪x, y⟫ < 0 →
    -(HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 -
            (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2)) +
        4 * (⟪x, y⟫ - 0) =
      0
linarith₁ : ⟪x, y⟫ < 0 → GT.gt (α := ℝ) 4 0
linarith₂ :
  0 < ⟪x, y⟫ →
    HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 -
          (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2) +
        4 * (0 - ⟪x, y⟫) =
      0
⊢ ⟪x, y⟫ = 0
have linarith₃ : 0 < ⟪x, y⟫ → GT.gt (α := ℝ) 4 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
h : ⟪x, y⟫ = 0
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2
have linarith : HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 <
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 →
  4 * -(⟪x, y⟫ - 0) +
      (HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 -
        (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖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
h : ⟪x, y⟫ = 0
linarith :
  HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 <
      HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 →
    4 * -(⟪x, y⟫ - 0) +
        (HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 -
          (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2)) =
      0
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2
have linarith₁ : HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 <
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 →
  GT.gt (α := ℝ) 4 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
h : ⟪x, y⟫ = 0
linarith :
  HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 <
      HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 →
    4 * -(⟪x, y⟫ - 0) +
        (HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 -
          (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2)) =
      0
linarith₁ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 <
      HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 →
    GT.gt (α := ℝ) 4 0
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2
have linarith₂ : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 <
    HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 →
  4 * (⟪x, y⟫ - 0) +
      (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 -
        (HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖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
h : ⟪x, y⟫ = 0
linarith :
  HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 <
      HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 →
    4 * -(⟪x, y⟫ - 0) +
        (HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 -
          (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2)) =
      0
linarith₁ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 <
      HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 →
    GT.gt (α := ℝ) 4 0
linarith₂ :
  HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 <
      HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 →
    4 * (⟪x, y⟫ - 0) +
        (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 -
          (HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2)) =
      0
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2
have linarith₃ : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 <
    HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 →
  GT.gt (α := ℝ) 4 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
⊢ cos (angle x y) = 1 ↔ angle x y = 0
have rw : cos (angle x y) = cos 0 ↔ angle x y = 0
Tactic: rw [← cos_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
⊢ cos (angle x y) = 0 ↔ angle x y = π / 2
have rw : cos (angle x y) = cos (π / 2) ↔ angle x y = π / 2
Tactic: rw [← cos_pi_div_two]
-- 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
⊢ cos (angle x y) = cos (π / 2) ↔ angle x y = π / 2
have apply : π / 2 ∈ Icc 0 π
Tactic: apply injOn_cos.eq_iff ⟨angle_nonneg x y, angle_le_pi 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
⊢ π / 2 ∈ Icc 0 π
have left : 0 ≤ π / 2
Tactic: constructor
-- 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
left : 0 ≤ π / 2
⊢ π / 2 ∈ Icc 0 π
have right : π / 2 ≤ π
Tactic: constructor
-- 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
⊢ 0 ≤ π / 2
have linarith : π / 2 < 0 → 2 / 2 = 1
Tactic: linarith [pi_pos]
-- 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
linarith : π / 2 < 0 → 2 / 2 = 1
⊢ 0 ≤ π / 2
have linarith₁ : π / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [pi_pos]
-- 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
linarith : π / 2 < 0 → 2 / 2 = 1
linarith₁ : π / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ π / 2
have linarith₂ : π / 2 < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [pi_pos]
-- 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
linarith : π / 2 < 0 → 2 / 2 = 1
linarith₁ : π / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ π / 2
have linarith₃ : π / 2 < 0 → 1 * π - HMul.hMul (α := ℝ) 2 0 + (0 - π) = 0
Tactic: linarith [pi_pos]
-- 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
⊢ π / 2 ≤ π
have linarith : π < π / 2 → 2 / 2 = 1
Tactic: linarith [pi_pos]
-- 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
linarith : π < π / 2 → 2 / 2 = 1
⊢ π / 2 ≤ π
have linarith₁ : π < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [pi_pos]
-- 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
linarith : π < π / 2 → 2 / 2 = 1
linarith₁ : π < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ π / 2 ≤ π
have linarith₂ : π < π / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith [pi_pos]
-- 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
linarith : π < π / 2 → 2 / 2 = 1
linarith₁ : π < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < π / 2 → GT.gt (α := ℝ) 2 0
⊢ π / 2 ≤ π
have linarith₃ : π < π / 2 → 2 * π - 1 * π + (0 - π) = 0
Tactic: linarith [pi_pos]
-- 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
⊢ cos (angle x y) = -1 ↔ angle x y = π
have rw : cos (angle x y) = cos π ↔ angle x y = π
Tactic: rw [← cos_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
⊢ sin (angle x y) = 0 ↔ angle x y = 0 ∨ angle x y = π
have rw : cos (angle x y) = 1 ∨ cos (angle x y) = -1 ↔ angle x y = 0 ∨ angle x y = π
Tactic: rw [sin_eq_zero_iff_cos_eq, cos_eq_one_iff_angle_eq_zero, cos_eq_neg_one_iff_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
rw : cos (angle x y) = 1 ∨ cos (angle x y) = -1 ↔ angle x y = 0 ∨ angle x y = π
⊢ sin (angle x y) = 0 ↔ angle x y = 0 ∨ angle x y = π
have rw₁ : angle x y = 0 ∨ cos (angle x y) = -1 ↔ angle x y = 0 ∨ angle x y = π
Tactic: rw [sin_eq_zero_iff_cos_eq, cos_eq_one_iff_angle_eq_zero, cos_eq_neg_one_iff_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
rw : cos (angle x y) = 1 ∨ cos (angle x y) = -1 ↔ angle x y = 0 ∨ angle x y = π
rw₁ : angle x y = 0 ∨ cos (angle x y) = -1 ↔ angle x y = 0 ∨ angle x y = π
⊢ sin (angle x y) = 0 ↔ angle x y = 0 ∨ angle x y = π
have rw₂ : angle x y = 0 ∨ angle x y = π ↔ angle x y = 0 ∨ angle x y = π
Tactic: rw [sin_eq_zero_iff_cos_eq, cos_eq_one_iff_angle_eq_zero, cos_eq_neg_one_iff_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
h : angle x y = π / 2
⊢ sin (angle x y) = 1
have rw : sin (π / 2) = 1
Tactic: rw [h, sin_pi_div_two]
-- 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 = π / 2
rw : sin (π / 2) = 1
⊢ sin (angle x y) = 1
have rw₁ : Eq (α := ℝ) 1 1
Tactic: rw [h, sin_pi_div_two]
-- 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
⊢ sin (angle x y) = 1 ↔ angle x y = π / 2
have refine : ∀ (h : sin (angle x y) = 1), angle x y = π / 2
Tactic: refine ⟨fun h => ?_, fun h => by rw [h, sin_pi_div_two]⟩
-- 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 : sin (angle x y) = 1
⊢ angle x y = π / 2
have rw : √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2) = 0
Tactic: rw [← cos_eq_zero_iff_angle_eq_pi_div_two, ← abs_eq_zero, abs_cos_eq_sqrt_one_sub_sin_sq, 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
⊢ angle (NormedSpace.normalize x) y = angle x y
have pos : ∀ (hx : x = 0), angle (NormedSpace.normalize x) y = angle x y
Tactic: by_cases hx : x = 0
-- 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
pos : ∀ (hx : x = 0), angle (NormedSpace.normalize x) y = angle x y
⊢ angle (NormedSpace.normalize x) y = angle x y
have neg : ∀ (hx : ¬x = 0), angle (NormedSpace.normalize x) y = angle x y
Tactic: by_cases hx : x = 0
-- 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
⊢ angle (NormedSpace.normalize x) y = angle x y
have neg : angle (‖x‖⁻¹ • x) y = angle x y
Tactic: rw [NormedSpace.normalize, angle_smul_left_of_pos _ _ (by positivity)]
-- 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
neg : angle (‖x‖⁻¹ • x) y = angle x y
⊢ angle (NormedSpace.normalize x) y = angle x y
have neg₁ : angle x y = angle x y
Tactic: rw [NormedSpace.normalize, angle_smul_left_of_pos _ _ (by positivity)]
-- 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 (NormedSpace.normalize y) = angle x y
have rw : angle (NormedSpace.normalize y) x = angle x y
Tactic: rw [angle_comm, angle_normalize_left, angle_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
rw : angle (NormedSpace.normalize y) x = angle x y
⊢ angle x (NormedSpace.normalize y) = angle x y
have rw₁ : angle y x = angle x y
Tactic: rw [angle_comm, angle_normalize_left, angle_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
rw : angle (NormedSpace.normalize y) x = angle x y
rw₁ : angle y x = angle x y
⊢ angle x (NormedSpace.normalize y) = angle x y
have rw₂ : angle x y = angle x y
Tactic: rw [angle_comm, angle_normalize_left, angle_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f' : E →L[ℝ] F
h : IsConformalMap f'
u v : E
⊢ angle.{u_2} (V := F) ((f' : (a : E) → F) u : F) ((f' : (a : E) → F) v : F) = angle u v
have obtain : ∀ (c : ℝ) (hc : c ≠ 0) (li : E →ₗᵢ[ℝ] F),
  angle.{u_2} (V := F) ((c • li.toContinuousLinearMap : (a : E) → F) u : F)
      ((c • li.toContinuousLinearMap : (a : E) → F) v : F) =
    angle u v
Tactic: obtain ⟨c, hc, li, rfl⟩ := h
Cleared hypotheses: f', h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct (hypothesis)
Goal:
a b : EuclideanSpace ℝ (Fin 3)
⊢ Norm.norm (E := WithLp 2 (Fin 3 → ℝ))
      (toLp 2
          ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
              (a : Fin 3 → ℝ) → Fin 3 → ℝ)
            b.ofLp) :
        WithLp 2 (Fin 3 → ℝ)) =
    ‖a‖ * ‖b‖ * sin (angle a b)
have this : 0 ≤ sin (angle a b)
Tactic: have := sin_angle_nonneg a b
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct (goal)
Goal:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
⊢ Norm.norm (E := WithLp 2 (Fin 3 → ℝ))
      (toLp 2
          ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
              (a : Fin 3 → ℝ) → Fin 3 → ℝ)
            b.ofLp) :
        WithLp 2 (Fin 3 → ℝ)) =
    ‖a‖ * ‖b‖ * sin (angle a b)
have refine : HPow.hPow (β := ℕ)
    (Norm.norm (E := WithLp 2 (Fin 3 → ℝ))
      (toLp 2
          ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
              (a : Fin 3 → ℝ) → Fin 3 → ℝ)
            b.ofLp) :
        WithLp 2 (Fin 3 → ℝ)))
    2 =
  HPow.hPow (β := ℕ) (‖a‖ * ‖b‖ * sin (angle a b)) 2
Tactic: refine sq_eq_sq₀ (by positivity) (by positivity) |>.mp ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct (goal)
Goal:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
⊢ HPow.hPow (β := ℕ)
      (Norm.norm (E := WithLp 2 (Fin 3 → ℝ))
        (toLp 2
            ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
                (a : Fin 3 → ℝ) → Fin 3 → ℝ)
              b.ofLp) :
          WithLp 2 (Fin 3 → ℝ)))
      2 =
    HPow.hPow (β := ℕ) (‖a‖ * ‖b‖ * sin (angle a b)) 2
have trans : HPow.hPow (β := ℕ)
    (Norm.norm (E := WithLp 2 (Fin 3 → ℝ))
      (toLp 2
          ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
              (a : Fin 3 → ℝ) → Fin 3 → ℝ)
            b.ofLp) :
        WithLp 2 (Fin 3 → ℝ)))
    2 =
  HPow.hPow (β := ℕ) ‖a‖ 2 * HPow.hPow (β := ℕ) ‖b‖ 2 - HPow.hPow (β := ℕ) ⟪a, b⟫ 2
Tactic: trans ‖a‖ ^ 2 * ‖b‖ ^ 2 - ⟪a, b⟫ ^ 2
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct (goal)
Goal:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
trans :
  HPow.hPow (β := ℕ)
      (Norm.norm (E := WithLp 2 (Fin 3 → ℝ))
        (toLp 2
            ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
                (a : Fin 3 → ℝ) → Fin 3 → ℝ)
              b.ofLp) :
          WithLp 2 (Fin 3 → ℝ)))
      2 =
    HPow.hPow (β := ℕ) ‖a‖ 2 * HPow.hPow (β := ℕ) ‖b‖ 2 - HPow.hPow (β := ℕ) ⟪a, b⟫ 2
⊢ HPow.hPow (β := ℕ)
      (Norm.norm (E := WithLp 2 (Fin 3 → ℝ))
        (toLp 2
            ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
                (a : Fin 3 → ℝ) → Fin 3 → ℝ)
              b.ofLp) :
          WithLp 2 (Fin 3 → ℝ)))
      2 =
    HPow.hPow (β := ℕ) (‖a‖ * ‖b‖ * sin (angle a b)) 2
have trans₁ : HPow.hPow (β := ℕ) ‖a‖ 2 * HPow.hPow (β := ℕ) ‖b‖ 2 - HPow.hPow (β := ℕ) ⟪a, b⟫ 2 =
  HPow.hPow (β := ℕ) (‖a‖ * ‖b‖ * sin (angle a b)) 2
Tactic: trans ‖a‖ ^ 2 * ‖b‖ ^ 2 - ⟪a, b⟫ ^ 2
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct (goal)
Goal:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
⊢ HPow.hPow (β := ℕ)
      (Norm.norm (E := WithLp 2 (Fin 3 → ℝ))
        (toLp 2
            ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
                (a : Fin 3 → ℝ) → Fin 3 → ℝ)
              b.ofLp) :
          WithLp 2 (Fin 3 → ℝ)))
      2 =
    HPow.hPow (β := ℕ) ‖a‖ 2 * HPow.hPow (β := ℕ) ‖b‖ 2 - HPow.hPow (β := ℕ) ⟪a, b⟫ 2
have simp_rw : (RCLike.re : (a : ℝ) → ℝ)
    (inner ℝ (E := WithLp 2 (Fin 3 → ℝ))
      (toLp 2
          ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
              (a : Fin 3 → ℝ) → Fin 3 → ℝ)
            b.ofLp) :
        WithLp 2 (Fin 3 → ℝ))
      (toLp 2
          ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
              (a : Fin 3 → ℝ) → Fin 3 → ℝ)
            b.ofLp) :
        WithLp 2 (Fin 3 → ℝ))) =
  HMul.hMul (α := ℝ) (β := ℝ) ((RCLike.re : (a : ℝ) → ℝ) ⟪a, a⟫ : ℝ) ((RCLike.re : (a : ℝ) → ℝ) ⟪b, b⟫ : ℝ) -
    HPow.hPow (β := ℕ) ⟪a, b⟫ 2
Tactic: simp_rw [norm_sq_eq_re_inner (𝕜 := ℝ), EuclideanSpace.inner_eq_star_dotProduct, star_trivial,
      RCLike.re_to_real, cross_dot_cross, dotProduct_comm (ofLp b) (ofLp a), sq]