awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_mod_cast rw_mod_cast₁ rw_mod_cast₂ rw_mod_cast₃ rw_mod_cast₄ 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)))
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)))
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‖ 2 / HPow.hPow (β := ℕ) ‖x‖ 2)))
rw_mod_cast₈ :
  ∀ (h : ⟪x, y⟫ = 0),
    Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) =
      Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ * (1 + HPow.hPow (β := ℕ) ‖y‖ 2 / (‖x‖ * ‖x‖))))
rw_mod_cast₉ :
  ∀ (h : ⟪x, y⟫ = 0),
    Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ * (1 + ‖y‖ * ‖y‖ / (‖x‖ * ‖x‖))))
rw_mod_cast₁₀ :
  ∀ (h : ⟪x, y⟫ = 0),
    Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) =
      Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ * 1 + ‖x‖ * ‖x‖ * (‖y‖ * ‖y‖ / (‖x‖ * ‖x‖))))
rw_mod_cast₁₁ :
  ∀ (h : ⟪x, y⟫ = 0),
    Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) =
      Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖x‖ * ‖x‖ * (‖y‖ * ‖y‖ / (‖x‖ * ‖x‖))))
rw_mod_cast₁₂ :
  ∀ (h : ⟪x, y⟫ = 0),
    Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) =
      Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) / (‖x‖ * ‖x‖)))
rw_mod_cast₁₃ :
  ∀ (h : ⟪x, y⟫ = 0),
    Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) =
      Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ * (‖x‖ * ‖x‖) / (‖x‖ * ‖x‖)))
rw_mod_cast₁₄ :
  ∀ (h : ⟪x, y⟫ = 0),
    Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) =
      Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ * (‖x‖ * ‖x‖ / (‖x‖ * ‖x‖))))
rw_mod_cast₁₅ :
  ∀ (h : ⟪x, y⟫ = 0), Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ * 1))
⊢ 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]

Premises used: mul_div, Iff.mpr, Norm.norm, HMul.hMul, pow_two, Real.sqrt_mul, mul_self_pos, LT.lt.ne', norm_ne_zero_iff, div_pow, sq_nonneg, mul_comm, mul_add, mul_one, 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 : ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
⊢ 0 < angle x (x + y)

Tactic:
rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_pos,
    norm_add_eq_sqrt_iff_real_inner_eq_zero.2 h]

Premises used: Iff.mpr, Real.arccos_pos, norm_add_eq_sqrt_iff_real_inner_eq_zero, InnerProductGeometry.angle_add_eq_arccos_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 ∨ y ≠ 0
pos : ∀ (hx : x = 0), ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
neg : ∀ (hx : ¬x = 0), ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
⊢ ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1

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
h0 : x = 0 ∨ y ≠ 0
hx : x = 0
⊢ ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1

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
h0 : x = 0 ∨ y ≠ 0
hx : ¬x = 0
neg : ‖x‖ * ‖x‖ < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
⊢ ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1

Tactic:
rw [div_lt_one (Real.sqrt_pos.2 (Left.add_pos_of_pos_of_nonneg (mul_self_pos.2
    (norm_ne_zero_iff.2 hx)) (mul_self_nonneg _))), Real.lt_sqrt (norm_nonneg _), pow_two]

Premises used: mul_self_nonneg, Iff.mpr, pow_two, Left.add_pos_of_pos_of_nonneg, mul_self_pos, Real.sqrt_pos, norm_ne_zero_iff, div_lt_one, Real.lt_sqrt, 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
hx : ¬x = 0
⊢ ‖x‖ * ‖x‖ < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
simpa [hx] using 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
rw : 0 ≤ ‖x‖ / ‖x + y‖
⊢ angle x (x + y) ≤ π / 2

Tactic:
rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_le_pi_div_two]

Premises used: Real.arccos_le_pi_div_two, InnerProductGeometry.angle_add_eq_arccos_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
⊢ 0 ≤ ‖x‖ / ‖x + y‖

Tactic:
div_nonneg (norm_nonneg _) (norm_nonneg _)

Premises used: div_nonneg, 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
⊢ 0 ≤ ‖x‖ / ‖x + y‖

Tactic:
exact div_nonneg (norm_nonneg _) (norm_nonneg _)

Premises used: div_nonneg, 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
rw : 0 < ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)
⊢ angle x (x + y) < π / 2

Tactic:
rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_lt_pi_div_two,
    norm_add_eq_sqrt_iff_real_inner_eq_zero.2 h]

Premises used: Iff.mpr, norm_add_eq_sqrt_iff_real_inner_eq_zero, InnerProductGeometry.angle_add_eq_arccos_of_inner_eq_zero, Real.arccos_lt_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
h0 : x ≠ 0
⊢ 0 < ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)

Tactic:
div_pos (norm_pos_iff.2 h0) (Real.sqrt_pos.2 (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, norm_pos_iff, Left.add_pos_of_pos_of_nonneg, mul_self_pos, Real.sqrt_pos, norm_ne_zero_iff, div_pos
-- 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‖ * ‖x‖ + ‖y‖ * ‖y‖)

Tactic:
exact div_pos (norm_pos_iff.2 h0) (Real.sqrt_pos.2 (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, norm_pos_iff, Left.add_pos_of_pos_of_nonneg, mul_self_pos, Real.sqrt_pos, norm_ne_zero_iff, div_pos
-- 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
⊢ LE.le (α := ℝ) (-1) 0

Tactic:
simp
-- 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 : ‖x‖ ≤ ‖x + y‖
⊢ Real.cos (angle x (x + y)) = ‖x‖ / ‖x + y‖

Tactic:
rw [angle_add_eq_arccos_of_inner_eq_zero h,
    Real.cos_arccos (le_trans (by simp) (div_nonneg (norm_nonneg _) (norm_nonneg _)))
      (div_le_one_of_le₀ _ (norm_nonneg _))]

Premises used: div_le_one_of_le₀, Real.cos_arccos, InnerProductGeometry.angle_add_eq_arccos_of_inner_eq_zero, div_nonneg, norm_nonneg, le_trans
-- 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 : ‖x‖ * ‖x‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
⊢ ‖x‖ ≤ ‖x + y‖

Tactic:
rw [mul_self_le_mul_self_iff (norm_nonneg _) (norm_nonneg _),
    norm_add_sq_eq_norm_sq_add_norm_sq_real h]

Premises used: mul_self_le_mul_self_iff, 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
⊢ ‖x‖ * ‖x‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
le_add_of_nonneg_right (mul_self_nonneg _)

Premises used: mul_self_nonneg, le_add_of_nonneg_right
-- 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
⊢ ‖x‖ * ‖x‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
exact le_add_of_nonneg_right (mul_self_nonneg _)

Premises used: le_add_of_nonneg_right
-- 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
⊢ LE.le (α := ℝ) (-1) 0

Tactic:
simp
-- 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 : ‖y‖ ≤ ‖x + y‖
⊢ Real.sin (angle x (x + y)) = ‖y‖ / ‖x + y‖

Tactic:
rw [angle_add_eq_arcsin_of_inner_eq_zero h h0,
    Real.sin_arcsin (le_trans (by simp) (div_nonneg (norm_nonneg _) (norm_nonneg _)))
      (div_le_one_of_le₀ _ (norm_nonneg _))]

Premises used: div_le_one_of_le₀, Real.sin_arcsin, div_nonneg, InnerProductGeometry.angle_add_eq_arcsin_of_inner_eq_zero, norm_nonneg, le_trans
-- 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 : ‖y‖ * ‖y‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
⊢ ‖y‖ ≤ ‖x + y‖

Tactic:
rw [mul_self_le_mul_self_iff (norm_nonneg _) (norm_nonneg _),
    norm_add_sq_eq_norm_sq_add_norm_sq_real h]

Premises used: mul_self_le_mul_self_iff, 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 ∨ y ≠ 0
⊢ ‖y‖ * ‖y‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
le_add_of_nonneg_left (mul_self_nonneg _)

Premises used: mul_self_nonneg, le_add_of_nonneg_left
-- 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
⊢ ‖y‖ * ‖y‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
exact le_add_of_nonneg_left (mul_self_nonneg _)

Premises used: le_add_of_nonneg_left
-- 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 : ∀ (h0 : x = 0), Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖
neg : ∀ (h0 : ¬x = 0), Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖
⊢ Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖

Tactic:
by_cases h0 : 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
h0 : x = 0
⊢ Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖

Tactic:
simp [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
neg : Real.tan (Real.arctan (‖y‖ / ‖x‖)) = ‖y‖ / ‖x‖
neg₁ neg₂ : ‖y‖ / ‖x‖ = ‖y‖ / ‖x‖
⊢ Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖

Tactic:
rw [angle_add_eq_arctan_of_inner_eq_zero h h0, Real.tan_arctan]

Premises used: InnerProductGeometry.angle_add_eq_arctan_of_inner_eq_zero, Real.tan_arctan
-- 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 : ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
⊢ Real.cos (angle x (x + y)) * ‖x + y‖ = ‖x‖

Tactic:
rw [cos_angle_add_of_inner_eq_zero h]

Premises used: InnerProductGeometry.cos_angle_add_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
pos : ∀ (hxy : ‖x + y‖ = 0), ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
neg : ∀ (hxy : ¬‖x + y‖ = 0), ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

Tactic:
by_cases hxy : ‖x + y‖ = 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
hxy : ‖x + y‖ = 0
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
have h' := norm_add_sq_eq_norm_sq_add_norm_sq_real h
-- 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
hxy : ‖x + y‖ = 0
h' : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
⊢ ‖x‖ = 0 ∧ ‖y‖ * ‖y‖ = 0

Tactic:
rw [hxy, zero_mul, eq_comm,
      add_eq_zero_iff_of_nonneg (mul_self_nonneg ‖x‖) (mul_self_nonneg ‖y‖), mul_self_eq_zero] at h'

Premises used: mul_self_nonneg, Norm.norm, mul_self_eq_zero, add_eq_zero_iff_of_nonneg, MulZeroClass.zero_mul, eq_comm
-- 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
hxy : ‖x + y‖ = 0
h' : ‖x‖ = 0 ∧ ‖y‖ * ‖y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

Tactic:
simp [h'.1]

Premises used: And.left
-- 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
hxy : ¬‖x + y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

Tactic:
div_mul_cancel₀ _ hxy

Premises used: div_mul_cancel₀
-- 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
hxy : ¬‖x + y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

Tactic:
exact div_mul_cancel₀ _ hxy

Premises used: div_mul_cancel₀
-- 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 : ∀ (h0 : x = 0 ∧ y = 0), Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
neg : ∀ (h0 : ¬(x = 0 ∧ y = 0)), Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖

Tactic:
by_cases h0 : x = 0 ∧ y = 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
h0 : x = 0 ∧ y = 0
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖

Tactic:
simp [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)
⊢ ¬x = 0 ∨ ¬y = 0

Tactic:
rw [not_and_or] at h0

Premises used: not_and_or
-- 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
neg : ‖x + y‖ ≠ 0
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖

Tactic:
rw [sin_angle_add_of_inner_eq_zero h h0, div_mul_cancel₀]

Premises used: div_mul_cancel₀, InnerProductGeometry.sin_angle_add_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 ∨ ¬y = 0
neg : ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ≠ 0
⊢ ‖x + y‖ ≠ 0

Tactic:
rw [← mul_self_ne_zero, norm_add_sq_eq_norm_sq_add_norm_sq_real h]

Premises used: mul_self_ne_zero, 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
⊢ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ≠ 0

Tactic:
(ne_of_lt ?_).symm

Premises used: Ne.symm, 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
neg : 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
⊢ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ≠ 0

Tactic:
refine (ne_of_lt ?_).symm

Premises used: Ne.symm, 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
neg : ∀ (h0 : ¬x = 0), 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
neg₁ : ∀ (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
rw : ‖y‖ / ‖x‖ * ‖x‖ = ‖y‖
⊢ Real.tan (angle x (x + y)) * ‖x‖ = ‖y‖

Tactic:
rw [tan_angle_add_of_inner_eq_zero h]

Premises used: InnerProductGeometry.tan_angle_add_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 ∨ y = 0
inl : ∀ (h0 : x ≠ 0), ‖y‖ / ‖x‖ * ‖x‖ = ‖y‖
inr : ∀ (h0 : y = 0), ‖y‖ / ‖x‖ * ‖x‖ = ‖y‖
⊢ ‖y‖ / ‖x‖ * ‖x‖ = ‖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
⊢ ‖y‖ / ‖x‖ * ‖x‖ = ‖y‖

Tactic:
simp [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 : y = 0
⊢ ‖y‖ / ‖x‖ * ‖x‖ = ‖y‖

Tactic:
simp [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
rw : ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
⊢ ‖x‖ / Real.cos (angle x (x + y)) = ‖x + y‖

Tactic:
rw [cos_angle_add_of_inner_eq_zero h]

Premises used: InnerProductGeometry.cos_angle_add_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 ∨ y = 0
inl : ∀ (h0 : x ≠ 0), ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
inr : ∀ (h0 : y = 0), ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + 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
inl : ‖x‖ * ‖x + y‖ / ‖x‖ = ‖x + y‖
inl₁ : ‖x + y‖ * ‖x‖ / ‖x‖ = ‖x + y‖
inl₂ : ‖x + y‖ * ‖x‖ * ‖x‖⁻¹ = ‖x + y‖
inl₃ inl₄ : ‖x + y‖ = ‖x + y‖
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖

Tactic:
rw [div_div_eq_mul_div, mul_comm, div_eq_mul_inv, mul_inv_cancel_right₀ (norm_ne_zero_iff.2 h0)]

Premises used: Iff.mpr, div_div_eq_mul_div, div_eq_mul_inv, mul_inv_cancel_right₀, norm_ne_zero_iff, mul_comm
-- 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
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖

Tactic:
simp [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
inl : ∀ (h0 : x = 0), ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖
inr : ∀ (h0 : y ≠ 0), ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + 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
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖

Tactic:
simp [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 : y ≠ 0
inr : ‖y‖ / (‖y‖ / ‖x + y‖) = ‖x + y‖
inr₁ : ‖y‖ * ‖x + y‖ / ‖y‖ = ‖x + y‖
inr₂ : ‖x + y‖ * ‖y‖ / ‖y‖ = ‖x + y‖
inr₃ : ‖x + y‖ * ‖y‖ * ‖y‖⁻¹ = ‖x + y‖
inr₄ inr₅ : ‖x + y‖ = ‖x + y‖
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖

Tactic:
rw [sin_angle_add_of_inner_eq_zero h (Or.inr h0), div_div_eq_mul_div, mul_comm, div_eq_mul_inv,
    mul_inv_cancel_right₀ (norm_ne_zero_iff.2 h0)]

Premises used: Iff.mpr, div_div_eq_mul_div, div_eq_mul_inv, mul_inv_cancel_right₀, norm_ne_zero_iff, mul_comm, InnerProductGeometry.sin_angle_add_of_inner_eq_zero, Or.inr
-- 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 : ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
⊢ ‖y‖ / Real.tan (angle x (x + y)) = ‖x‖

Tactic:
rw [tan_angle_add_of_inner_eq_zero h]

Premises used: InnerProductGeometry.tan_angle_add_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 ∨ y ≠ 0
inl : ∀ (h0 : x = 0), ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
inr : ∀ (h0 : y ≠ 0), ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖

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
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖

Tactic:
simp [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 : y ≠ 0
inr : ‖y‖ * ‖x‖ / ‖y‖ = ‖x‖
inr₁ : ‖x‖ * ‖y‖ / ‖y‖ = ‖x‖
inr₂ : ‖x‖ * ‖y‖ * ‖y‖⁻¹ = ‖x‖
inr₃ inr₄ : ‖x‖ = ‖x‖
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖

Tactic:
rw [div_div_eq_mul_div, mul_comm, div_eq_mul_inv, mul_inv_cancel_right₀ (norm_ne_zero_iff.2 h0)]

Premises used: Iff.mpr, div_div_eq_mul_div, div_eq_mul_inv, mul_inv_cancel_right₀, norm_ne_zero_iff, mul_comm
-- 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
⊢ ⟪x, -y⟫ = 0

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Premises used: inner_neg_right, neg_eq_zero