awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : sin (angle x y) = 1
rw : √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2) = 0
⊢ angle x y = π / 2

Tactic:
rw [← cos_eq_zero_iff_angle_eq_pi_div_two, ← abs_eq_zero, abs_cos_eq_sqrt_one_sub_sin_sq, h]

Premises used: InnerProductGeometry.cos_eq_zero_iff_angle_eq_pi_div_two, abs_eq_zero, Real.abs_cos_eq_sqrt_one_sub_sin_sq
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : sin (angle x y) = 1
⊢ √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2) = 0

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hxy : angle x y = 0
h : ‖x‖ = ‖y‖
⊢ x = y

Tactic:
grind [angle_eq_zero_iff, norm_smul, Real.norm_eq_abs, norm_ne_zero_iff, abs, one_smul]

Premises used: norm_smul, abs, InnerProductGeometry.angle_eq_zero_iff, one_smul, norm_ne_zero_iff, Real.norm_eq_abs
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
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
neg : ∀ (hx : ¬x = 0), angle (NormedSpace.normalize x) y = angle x y
⊢ angle (NormedSpace.normalize x) y = angle x y

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
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

Tactic:
simp [hx]
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ¬x = 0
⊢ 0 < ‖x‖⁻¹

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
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
neg₁ neg₂ : angle x y = angle x y
⊢ angle (NormedSpace.normalize x) y = angle x y

Tactic:
rw [NormedSpace.normalize, angle_smul_left_of_pos _ _ (by positivity)]

Premises used: NormedSpace.normalize, InnerProductGeometry.angle_smul_left_of_pos
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
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
rw₂ rw₃ : angle x y = angle x y
⊢ angle x (NormedSpace.normalize y) = angle x y

Tactic:
rw [angle_comm, angle_normalize_left, angle_comm]

Premises used: InnerProductGeometry.angle_normalize_left, InnerProductGeometry.angle_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ⟪x, y⟫ = cos (angle x y)

Tactic:
simp [cos_angle, hx, hy]

Premises used: InnerProductGeometry.cos_angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal
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
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
⊢ angle.{u_2} (V := F) ((f' : (a : E) → F) u : F) ((f' : (a : E) → F) v : F) = angle u v

Tactic:
obtain ⟨c, hc, li, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
u v : E
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:
(angle_smul_smul hc _ _).trans (li.angle_map _ _)

Premises used: InnerProductGeometry.angle_smul_smul, Eq.trans, LinearIsometry.angle_map
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
u v : E
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:
exact (angle_smul_smul hc _ _).trans (li.angle_map _ _)

Premises used: InnerProductGeometry.angle_smul_smul, Eq.trans, LinearIsometry.angle_map
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal
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 → F
x : E
f' : E →L[ℝ] F
h : HasFDerivAt f f' x
H : ConformalAt f x
u v : E
⊢ angle.{u_2} (V := F) ((f' : (a : E) → F) u : F) ((f' : (a : E) → F) v : F) = angle u v

Tactic:
let ⟨_, h₁, c⟩ := H
  h₁.unique h ▸ IsConformalMap.preserves_angle c u v

Premises used: InnerProductGeometry.angle, _private.0.InnerProductGeometry.ConformalAt.preserves_angle.match_1, Eq.rec, HasFDerivAt.unique, Eq, DFunLike.coe, InnerProductGeometry.IsConformalMap.preserves_angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct
Goal:
a b : EuclideanSpace ℝ (Fin 3)
⊢ 0 ≤ sin (angle a b)

Tactic:
have := sin_angle_nonneg a b
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct
Goal:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
⊢ 0 ≤
    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 → ℝ))

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct
Goal:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
⊢ 0 ≤ ‖a‖ * ‖b‖ * sin (angle a b)

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct
Goal:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
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
⊢ 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)

Tactic:
refine sq_eq_sq₀ (by positivity) (by positivity) |>.mp ?_

Premises used: Iff.mp, sq_eq_sq₀
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct
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
trans₁ :
  HPow.hPow (β := ℕ) ‖a‖ 2 * HPow.hPow (β := ℕ) ‖b‖ 2 - HPow.hPow (β := ℕ) ⟪a, b⟫ 2 =
    HPow.hPow (β := ℕ) (‖a‖ * ‖b‖ * sin (angle 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

Tactic:
trans ‖a‖ ^ 2 * ‖b‖ ^ 2 - ⟪a, b⟫ ^ 2
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct
Goal:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
⊢ HPow.hPow (β := ℕ) ‖a‖ 2 * HPow.hPow (β := ℕ) ‖b‖ 2 - HPow.hPow (β := ℕ) ⟪a, b⟫ 2 =
    HPow.hPow (β := ℕ) (‖a‖ * ‖b‖ * sin (angle a b)) 2

Tactic:
linear_combination (‖a‖ * ‖b‖) ^ 2 * (sin_sq_add_cos_sq (angle a b)).symm +
      congrArg (· ^ 2) (cos_angle_mul_norm_mul_norm a b)

Premises used: Norm.norm, HMul.hMul, congrArg, InnerProductGeometry.angle, InnerProductGeometry.cos_angle_mul_norm_mul_norm, HPow.hPow, Real.sin_sq_add_cos_sq, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct
Goal:
a b : Fin 3 → ℝ
⊢ Norm.norm (E := WithLp 2 (Fin 3 → ℝ))
      (toLp 2
          ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
              (a : Fin 3 → ℝ) → Fin 3 → ℝ)
            b) :
        WithLp 2 (Fin 3 → ℝ)) =
    Norm.norm (E := WithLp 2 (Fin 3 → ℝ)) (toLp 2 a) * Norm.norm (E := WithLp 2 (Fin 3 → ℝ)) (toLp 2 b) *
      sin (angle (V := WithLp 2 (Fin 3 → ℝ)) (toLp 2 a) (toLp 2 b))

Tactic:
simp [← norm_ofLp_crossProduct (toLp 2 a) (toLp 2 b)]

Premises used: WithLp.toLp, InnerProductGeometry.norm_ofLp_crossProduct, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection
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
⊢ Nonempty.{u_2 + 1} ↥s

Tactic:
haveI : Nonempty s := ⟨p', h⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection
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
rw :
  inner ℝ (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P))
      (p' -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) =
    0
⊢ ∠ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = π / 2

Tactic:
rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]

Premises used: InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection
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
⊢ inner ℝ (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P))
      (p' -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) =
    0

Tactic:
Submodule.inner_left_of_mem_orthogonal (K := s.direction)
    (AffineSubspace.vsub_mem_direction h (orthogonalProjection_mem _))
    (vsub_orthogonalProjection_mem_direction_orthogonal _ _)

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, AffineSubspace.vsub_mem_direction, Submodule.inner_left_of_mem_orthogonal, EuclideanGeometry.orthogonalProjection_mem
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection
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
⊢ inner ℝ (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P))
      (p' -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) =
    0

Tactic:
exact Submodule.inner_left_of_mem_orthogonal (K := s.direction)
    (AffineSubspace.vsub_mem_direction h (orthogonalProjection_mem _))
    (vsub_orthogonalProjection_mem_direction_orthogonal _ _)

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, AffineSubspace.vsub_mem_direction, Submodule.inner_left_of_mem_orthogonal, EuclideanGeometry.orthogonalProjection_mem
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection
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
rw₁ rw₂ : π / 2 = π / 2
⊢ ∠ p' (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p = π / 2

Tactic:
rw [angle_comm, angle_self_orthogonalProjection p h]

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_self_orthogonalProjection
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw : ⟪x, y⟫ = 0 ↔ angle x y = π / 2
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ angle x y = π / 2

Tactic:
rw [norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero]

Premises used: norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ ⟪x, y⟫ = 0 ↔ angle x y = π / 2

Tactic:
inner_eq_zero_iff_angle_eq_pi_div_two x y

Premises used: InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ ⟪x, y⟫ = 0 ↔ angle x y = π / 2

Tactic:
exact inner_eq_zero_iff_angle_eq_pi_div_two x y

Premises used: InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : angle x y = π / 2
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
(norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two x y).2 h

Premises used: Iff.mpr, InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw : ⟪x, y⟫ = 0 ↔ angle x y = π / 2
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ angle x y = π / 2

Tactic:
rw [norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero]

Premises used: norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : angle x y = π / 2
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
(norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two x y).2 h

Premises used: Iff.mpr, InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
rw : Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)
⊢ angle x (x + y) = Real.arccos (‖x‖ / ‖x + y‖)

Tactic:
rw [angle, inner_add_right, h, add_zero, real_inner_self_eq_norm_mul_norm]

Premises used: InnerProductGeometry.angle, inner_add_right, real_inner_self_eq_norm_mul_norm, add_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
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‖)
neg : ∀ (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‖)

Tactic:
by_cases hx : ‖x‖ = 0
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
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‖)

Tactic:
simp [hx]
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
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‖)
neg₁ neg₂ : Real.arccos (‖x‖ / ‖x + y‖) = Real.arccos (‖x‖ / ‖x + y‖)
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)

Tactic:
rw [div_mul_eq_div_div, mul_self_div_self]

Premises used: div_mul_eq_div_div, mul_self_div_self
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
rw : 0 ≠ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 ≠ 0

Tactic:
rw [pow_two, norm_add_sq_eq_norm_sq_add_norm_sq_real h, ne_comm]

Premises used: pow_two, ne_comm, norm_add_sq_eq_norm_sq_add_norm_sq_real
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
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‖

Tactic:
ne_of_lt ?_

Premises used: ne_of_lt
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
refine : 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
⊢ 0 ≠ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
refine ne_of_lt ?_

Premises used: ne_of_lt
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
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‖
inr : ∀ (h0 : y ≠ 0), 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
rcases h0 with (h0 | h0)
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
Left.add_pos_of_pos_of_nonneg (mul_self_pos.2 (norm_ne_zero_iff.2 h0)) (mul_self_nonneg _)

Premises used: mul_self_nonneg, Iff.mpr, Left.add_pos_of_pos_of_nonneg, mul_self_pos, norm_ne_zero_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
exact
        Left.add_pos_of_pos_of_nonneg (mul_self_pos.2 (norm_ne_zero_iff.2 h0)) (mul_self_nonneg _)

Premises used: mul_self_nonneg, Iff.mpr, Left.add_pos_of_pos_of_nonneg, mul_self_pos, norm_ne_zero_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : y ≠ 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
Left.add_pos_of_nonneg_of_pos (mul_self_nonneg _) (mul_self_pos.2 (norm_ne_zero_iff.2 h0))

Premises used: mul_self_nonneg, Iff.mpr, Left.add_pos_of_nonneg_of_pos, mul_self_pos, norm_ne_zero_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : y ≠ 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
exact
        Left.add_pos_of_nonneg_of_pos (mul_self_nonneg _) (mul_self_pos.2 (norm_ne_zero_iff.2 h0))

Premises used: Iff.mpr, Left.add_pos_of_nonneg_of_pos, mul_self_pos, norm_ne_zero_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
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

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))
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
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 √((HPow.hPow (β := ℕ) ‖x + y‖ 2 - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
    Real.arcsin (‖y‖ / ‖x + y‖)
⊢ angle x (x + y) = 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]

Premises used: Real.arccos_eq_arcsin, InnerProductGeometry.angle_add_eq_arccos_of_inner_eq_zero, div_pow, div_nonneg, one_sub_div, norm_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
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
nth_rw :
  Real.arcsin √((‖x + y‖ * ‖x + y‖ - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
    Real.arcsin (‖y‖ / ‖x + y‖)
⊢ Real.arcsin √((HPow.hPow (β := ℕ) ‖x + y‖ 2 - HPow.hPow (β := ℕ) ‖x‖ 2) / HPow.hPow (β := ℕ) ‖x + y‖ 2) =
    Real.arcsin (‖y‖ / ‖x + y‖)

Tactic:
nth_rw 1 [pow_two]

Premises used: pow_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
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‖)
rw₅ rw₆ : Real.arcsin (‖y‖ / ‖x + y‖) = 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‖)

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 _))]

Premises used: pow_two, add_sub_cancel_left, div_pow, Real.sqrt_sq, div_nonneg, norm_nonneg, norm_add_sq_eq_norm_sq_add_norm_sq_real
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0
rw : Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / (‖x‖ * √(1 + HPow.hPow (β := ℕ) (‖y‖ / ‖x‖) 2)))
⊢ angle x (x + y) = Real.arctan (‖y‖ / ‖x‖)

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]

Premises used: Iff.mpr, Real.arctan_eq_arcsin, norm_add_eq_sqrt_iff_real_inner_eq_zero, Or.inl, div_mul_eq_div_div, InnerProductGeometry.angle_add_eq_arcsin_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0
nth_rw :
  Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) =
    Real.arcsin (‖y‖ / (√(HPow.hPow (β := ℕ) ‖x‖ 2) * √(1 + HPow.hPow (β := ℕ) (‖y‖ / ‖x‖) 2)))
⊢ Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / (‖x‖ * √(1 + HPow.hPow (β := ℕ) (‖y‖ / ‖x‖) 2)))

Tactic:
nth_rw 3 [← Real.sqrt_sq (norm_nonneg x)]

Premises used: Real.sqrt_sq, norm_nonneg