awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct (goal)
Goal:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
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
⊢ 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 : ℝ) → ℝ)
    (dotProduct (m := Fin 3)
      ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
          (a : Fin 3 → ℝ) → Fin 3 → ℝ)
        b.ofLp)
      (star
        ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
            (a : Fin 3 → ℝ) → Fin 3 → ℝ)
          b.ofLp))) =
  HMul.hMul (α := ℝ) (β := ℝ) ((RCLike.re : (a : ℝ) → ℝ) (a.ofLp ⬝ᵥ star a.ofLp) : ℝ)
      ((RCLike.re : (a : ℝ) → ℝ) (b.ofLp ⬝ᵥ star b.ofLp) : ℝ) -
    HPow.hPow (β := ℕ) (b.ofLp ⬝ᵥ star a.ofLp) 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct (goal)
Goal:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
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
simp_rw₁ :
  (RCLike.re : (a : ℝ) → ℝ)
      (dotProduct (m := Fin 3)
        ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
            (a : Fin 3 → ℝ) → Fin 3 → ℝ)
          b.ofLp)
        (star
          ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
              (a : Fin 3 → ℝ) → Fin 3 → ℝ)
            b.ofLp))) =
    HMul.hMul (α := ℝ) (β := ℝ) ((RCLike.re : (a : ℝ) → ℝ) (a.ofLp ⬝ᵥ star a.ofLp) : ℝ)
        ((RCLike.re : (a : ℝ) → ℝ) (b.ofLp ⬝ᵥ star b.ofLp) : ℝ) -
      HPow.hPow (β := ℕ) (b.ofLp ⬝ᵥ star a.ofLp) 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‖ 2 * HPow.hPow (β := ℕ) ‖b‖ 2 - HPow.hPow (β := ℕ) ⟪a, b⟫ 2
have simp_rw₂ : (RCLike.re : (a : ℝ) → ℝ)
    (dotProduct (m := Fin 3)
      ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
          (a : Fin 3 → ℝ) → Fin 3 → ℝ)
        b.ofLp)
      ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
          (a : Fin 3 → ℝ) → Fin 3 → ℝ)
        b.ofLp)) =
  HMul.hMul (α := ℝ) (β := ℝ) ((RCLike.re : (a : ℝ) → ℝ) (a.ofLp ⬝ᵥ a.ofLp) : ℝ)
      ((RCLike.re : (a : ℝ) → ℝ) (b.ofLp ⬝ᵥ b.ofLp) : ℝ) -
    HPow.hPow (β := ℕ) (b.ofLp ⬝ᵥ a.ofLp) 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct (goal)
Goal:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
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
simp_rw₁ :
  (RCLike.re : (a : ℝ) → ℝ)
      (dotProduct (m := Fin 3)
        ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
            (a : Fin 3 → ℝ) → Fin 3 → ℝ)
          b.ofLp)
        (star
          ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
              (a : Fin 3 → ℝ) → Fin 3 → ℝ)
            b.ofLp))) =
    HMul.hMul (α := ℝ) (β := ℝ) ((RCLike.re : (a : ℝ) → ℝ) (a.ofLp ⬝ᵥ star a.ofLp) : ℝ)
        ((RCLike.re : (a : ℝ) → ℝ) (b.ofLp ⬝ᵥ star b.ofLp) : ℝ) -
      HPow.hPow (β := ℕ) (b.ofLp ⬝ᵥ star a.ofLp) 2
simp_rw₂ :
  (RCLike.re : (a : ℝ) → ℝ)
      (dotProduct (m := Fin 3)
        ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
            (a : Fin 3 → ℝ) → Fin 3 → ℝ)
          b.ofLp)
        ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
            (a : Fin 3 → ℝ) → Fin 3 → ℝ)
          b.ofLp)) =
    HMul.hMul (α := ℝ) (β := ℝ) ((RCLike.re : (a : ℝ) → ℝ) (a.ofLp ⬝ᵥ a.ofLp) : ℝ)
        ((RCLike.re : (a : ℝ) → ℝ) (b.ofLp ⬝ᵥ b.ofLp) : ℝ) -
      HPow.hPow (β := ℕ) (b.ofLp ⬝ᵥ a.ofLp) 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‖ 2 * HPow.hPow (β := ℕ) ‖b‖ 2 - HPow.hPow (β := ℕ) ⟪a, b⟫ 2
have simp_rw₃ : dotProduct (m := Fin 3)
    ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
        (a : Fin 3 → ℝ) → Fin 3 → ℝ)
      b.ofLp)
    ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
        (a : Fin 3 → ℝ) → Fin 3 → ℝ)
      b.ofLp) =
  a.ofLp ⬝ᵥ a.ofLp * b.ofLp ⬝ᵥ b.ofLp - HPow.hPow (β := ℕ) (b.ofLp ⬝ᵥ a.ofLp) 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s : AffineSubspace ℝ P
inst_4 : s.direction.HasOrthogonalProjection
h : p' ∈ s
⊢ ∠ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = π / 2
have this : Nonempty.{u_2 + 1} ↥s
Tactic: haveI : Nonempty s := ⟨p', h⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s : AffineSubspace ℝ P
inst_4 : s.direction.HasOrthogonalProjection
h : p' ∈ s
this : Nonempty.{u_2 + 1} ↥s
⊢ ∠ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = π / 2
have rw : inner ℝ (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P))
    (p' -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) =
  0
Tactic: rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s : AffineSubspace ℝ P
inst_4 : s.direction.HasOrthogonalProjection
h : p' ∈ s
⊢ ∠ p' (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p = π / 2
have rw : ∠ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = π / 2
Tactic: rw [angle_comm, angle_self_orthogonalProjection p h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p p' : P
s : AffineSubspace ℝ P
inst_4 : s.direction.HasOrthogonalProjection
h : p' ∈ s
rw : ∠ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = π / 2
⊢ ∠ p' (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p = π / 2
have rw₁ : π / 2 = π / 2
Tactic: rw [angle_comm, angle_self_orthogonalProjection p h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ angle x y = π / 2
have rw : ⟪x, y⟫ = 0 ↔ angle x y = π / 2
Tactic: rw [norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ angle x y = π / 2
have rw : ⟪x, y⟫ = 0 ↔ angle x y = π / 2
Tactic: rw [norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ angle x (x + y) = Real.arccos (‖x‖ / ‖x + y‖)
have rw : Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)
Tactic: rw [angle, inner_add_right, h, add_zero, real_inner_self_eq_norm_mul_norm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)
have pos : ∀ (hx : ‖x‖ = 0), Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)
Tactic: by_cases hx : ‖x‖ = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
pos : ∀ (hx : ‖x‖ = 0), Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)
have neg : ∀ (hx : ¬‖x‖ = 0), Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)
Tactic: by_cases hx : ‖x‖ = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
hx : ¬‖x‖ = 0
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)
have neg : Real.arccos (‖x‖ * ‖x‖ / ‖x‖ / ‖x + y‖) = Real.arccos (‖x‖ / ‖x + y‖)
Tactic: rw [div_mul_eq_div_div, mul_self_div_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
hx : ¬‖x‖ = 0
neg : Real.arccos (‖x‖ * ‖x‖ / ‖x‖ / ‖x + y‖) = Real.arccos (‖x‖ / ‖x + y‖)
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)
have neg₁ : Real.arccos (‖x‖ / ‖x + y‖) = Real.arccos (‖x‖ / ‖x + y‖)
Tactic: rw [div_mul_eq_div_div, mul_self_div_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 ≠ 0
have rw : 0 ≠ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
Tactic: rw [pow_two, norm_add_sq_eq_norm_sq_add_norm_sq_real h, ne_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ 0 ≠ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
have refine : 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
Tactic: refine ne_of_lt ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
have inl : ∀ (h0 : x ≠ 0), 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
Tactic: rcases h0 with (h0 | h0)
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
inl : ∀ (h0 : x ≠ 0), 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
have inr : ∀ (h0 : y ≠ 0), 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
Tactic: rcases h0 with (h0 | h0)
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ angle x (x + y) = Real.arcsin (‖y‖ / ‖x + y‖)
have hxy : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≠ 0
Tactic: have hxy : ‖x + y‖ ^ 2 ≠ 0 := by
    rw [pow_two, norm_add_sq_eq_norm_sq_add_norm_sq_real h, ne_comm]
    refine ne_of_lt ?_
    rcases h0 with (h0 | h0)
    · exact
        Left.add_pos_of_pos_of_nonneg (mul_self_pos.2 (norm_ne_zero_iff.2 h0)) (mul_self_nonneg _)
    · exact
        Left.add_pos_of_nonneg_of_pos (mul_self_nonneg _) (mul_self_pos.2 (norm_ne_zero_iff.2 h0))
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
hxy : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≠ 0
⊢ angle x (x + y) = Real.arcsin (‖y‖ / ‖x + y‖)
have rw : Real.arcsin √((HPow.hPow (β := ℕ) ‖x + y‖ 2 - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
  Real.arcsin (‖y‖ / ‖x + y‖)
Tactic: rw [angle_add_eq_arccos_of_inner_eq_zero h,
    Real.arccos_eq_arcsin (div_nonneg (norm_nonneg _) (norm_nonneg _)), div_pow, one_sub_div hxy]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
hxy : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≠ 0
⊢ Real.arcsin √((HPow.hPow (β := ℕ) ‖x + y‖ 2 - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
    Real.arcsin (‖y‖ / ‖x + y‖)
have nth_rw : Real.arcsin √((‖x + y‖ * ‖x + y‖ - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
  Real.arcsin (‖y‖ / ‖x + y‖)
Tactic: nth_rw 1 [pow_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
hxy : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≠ 0
⊢ Real.arcsin √((‖x + y‖ * ‖x + y‖ - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
    Real.arcsin (‖y‖ / ‖x + y‖)
have rw : Real.arcsin √((‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
  Real.arcsin (‖y‖ / ‖x + y‖)
Tactic: rw [norm_add_sq_eq_norm_sq_add_norm_sq_real h, pow_two, add_sub_cancel_left, ← pow_two, ← div_pow,
    Real.sqrt_sq (div_nonneg (norm_nonneg _) (norm_nonneg _))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
hxy : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≠ 0
rw :
  Real.arcsin √((‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
    Real.arcsin (‖y‖ / ‖x + y‖)
⊢ Real.arcsin √((‖x + y‖ * ‖x + y‖ - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
    Real.arcsin (‖y‖ / ‖x + y‖)
have rw₁ : Real.arcsin √((‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x‖ * ‖x‖) / HPow.hPow (β := ℕ) ‖x + y‖ 2) = Real.arcsin (‖y‖ / ‖x + y‖)
Tactic: rw [norm_add_sq_eq_norm_sq_add_norm_sq_real h, pow_two, add_sub_cancel_left, ← pow_two, ← div_pow,
    Real.sqrt_sq (div_nonneg (norm_nonneg _) (norm_nonneg _))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
hxy : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≠ 0
rw :
  Real.arcsin √((‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
    Real.arcsin (‖y‖ / ‖x + y‖)
rw₁ : Real.arcsin √((‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x‖ * ‖x‖) / HPow.hPow (β := ℕ) ‖x + y‖ 2) = Real.arcsin (‖y‖ / ‖x + y‖)
⊢ Real.arcsin √((‖x + y‖ * ‖x + y‖ - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
    Real.arcsin (‖y‖ / ‖x + y‖)
have rw₂ : Real.arcsin √(‖y‖ * ‖y‖ / HPow.hPow (β := ℕ) ‖x + y‖ 2) = Real.arcsin (‖y‖ / ‖x + y‖)
Tactic: rw [norm_add_sq_eq_norm_sq_add_norm_sq_real h, pow_two, add_sub_cancel_left, ← pow_two, ← div_pow,
    Real.sqrt_sq (div_nonneg (norm_nonneg _) (norm_nonneg _))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
hxy : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≠ 0
rw :
  Real.arcsin √((‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
    Real.arcsin (‖y‖ / ‖x + y‖)
rw₁ : Real.arcsin √((‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x‖ * ‖x‖) / HPow.hPow (β := ℕ) ‖x + y‖ 2) = Real.arcsin (‖y‖ / ‖x + y‖)
rw₂ : Real.arcsin √(‖y‖ * ‖y‖ / HPow.hPow (β := ℕ) ‖x + y‖ 2) = Real.arcsin (‖y‖ / ‖x + y‖)
⊢ Real.arcsin √((‖x + y‖ * ‖x + y‖ - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
    Real.arcsin (‖y‖ / ‖x + y‖)
have rw₃ : Real.arcsin √(HPow.hPow (β := ℕ) ‖y‖ 2 / HPow.hPow (β := ℕ) ‖x + y‖ 2) = Real.arcsin (‖y‖ / ‖x + y‖)
Tactic: rw [norm_add_sq_eq_norm_sq_add_norm_sq_real h, pow_two, add_sub_cancel_left, ← pow_two, ← div_pow,
    Real.sqrt_sq (div_nonneg (norm_nonneg _) (norm_nonneg _))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
hxy : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≠ 0
rw :
  Real.arcsin √((‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
    Real.arcsin (‖y‖ / ‖x + y‖)
rw₁ : Real.arcsin √((‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x‖ * ‖x‖) / HPow.hPow (β := ℕ) ‖x + y‖ 2) = Real.arcsin (‖y‖ / ‖x + y‖)
rw₂ : Real.arcsin √(‖y‖ * ‖y‖ / HPow.hPow (β := ℕ) ‖x + y‖ 2) = Real.arcsin (‖y‖ / ‖x + y‖)
rw₃ : Real.arcsin √(HPow.hPow (β := ℕ) ‖y‖ 2 / HPow.hPow (β := ℕ) ‖x + y‖ 2) = Real.arcsin (‖y‖ / ‖x + y‖)
⊢ Real.arcsin √((‖x + y‖ * ‖x + y‖ - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
    Real.arcsin (‖y‖ / ‖x + y‖)
have rw₄ : Real.arcsin √(HPow.hPow (β := ℕ) (‖y‖ / ‖x + y‖) 2) = Real.arcsin (‖y‖ / ‖x + y‖)
Tactic: rw [norm_add_sq_eq_norm_sq_add_norm_sq_real h, pow_two, add_sub_cancel_left, ← pow_two, ← div_pow,
    Real.sqrt_sq (div_nonneg (norm_nonneg _) (norm_nonneg _))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
hxy : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≠ 0
rw :
  Real.arcsin √((‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
    Real.arcsin (‖y‖ / ‖x + y‖)
rw₁ : Real.arcsin √((‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x‖ * ‖x‖) / HPow.hPow (β := ℕ) ‖x + y‖ 2) = Real.arcsin (‖y‖ / ‖x + y‖)
rw₂ : Real.arcsin √(‖y‖ * ‖y‖ / HPow.hPow (β := ℕ) ‖x + y‖ 2) = Real.arcsin (‖y‖ / ‖x + y‖)
rw₃ : Real.arcsin √(HPow.hPow (β := ℕ) ‖y‖ 2 / HPow.hPow (β := ℕ) ‖x + y‖ 2) = Real.arcsin (‖y‖ / ‖x + y‖)
rw₄ : Real.arcsin √(HPow.hPow (β := ℕ) (‖y‖ / ‖x + y‖) 2) = Real.arcsin (‖y‖ / ‖x + y‖)
⊢ Real.arcsin √((‖x + y‖ * ‖x + y‖ - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
    Real.arcsin (‖y‖ / ‖x + y‖)
have rw₅ : Real.arcsin (‖y‖ / ‖x + y‖) = Real.arcsin (‖y‖ / ‖x + y‖)
Tactic: rw [norm_add_sq_eq_norm_sq_add_norm_sq_real h, pow_two, add_sub_cancel_left, ← pow_two, ← div_pow,
    Real.sqrt_sq (div_nonneg (norm_nonneg _) (norm_nonneg _))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0
⊢ angle x (x + y) = Real.arctan (‖y‖ / ‖x‖)
have rw : Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / (‖x‖ * √(1 + HPow.hPow (β := ℕ) (‖y‖ / ‖x‖) 2)))
Tactic: rw [angle_add_eq_arcsin_of_inner_eq_zero h (Or.inl h0), Real.arctan_eq_arcsin, ←
    div_mul_eq_div_div, norm_add_eq_sqrt_iff_real_inner_eq_zero.2 h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0
⊢ Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / (‖x‖ * √(1 + HPow.hPow (β := ℕ) (‖y‖ / ‖x‖) 2)))
have nth_rw : Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) =
  Real.arcsin (‖y‖ / (√(HPow.hPow (β := ℕ) ‖x‖ 2) * √(1 + HPow.hPow (β := ℕ) (‖y‖ / ‖x‖) 2)))
Tactic: nth_rw 3 [← Real.sqrt_sq (norm_nonneg x)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0
⊢ Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) =
    Real.arcsin (‖y‖ / (√(HPow.hPow (β := ℕ) ‖x‖ 2) * √(1 + HPow.hPow (β := ℕ) (‖y‖ / ‖x‖) 2)))
have rw_mod_cast : ∀ (h : ⟪x, y⟫ = 0),
  Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) =
    Real.arcsin (‖y‖ / (√(HPow.hPow (β := ℕ) ‖x‖ 2) * √(1 + HPow.hPow (β := ℕ) (‖y‖ / ‖x‖) 2)))
Tactic: rw_mod_cast [← Real.sqrt_mul (sq_nonneg _), div_pow, pow_two, pow_two, mul_add, mul_one, mul_div,
    mul_comm (‖x‖ * ‖x‖), ← mul_div, div_self (mul_self_pos.2 (norm_ne_zero_iff.2 h0)).ne', mul_one]
Cleared hypotheses: h