awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)))
⊢ 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
-- 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
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)))
⊢ 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‖ 2 / HPow.hPow (β := ℕ) ‖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
-- 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
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)))
⊢ 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‖ / √(‖x‖ * ‖x‖ * (1 + HPow.hPow (β := ℕ) ‖y‖ 2 / (‖x‖ * ‖x‖))))
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
-- 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
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‖))))
⊢ 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‖ / √(‖x‖ * ‖x‖ * (1 + ‖y‖ * ‖y‖ / (‖x‖ * ‖x‖))))
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
-- 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
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‖))))
⊢ 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‖ / √(‖x‖ * ‖x‖ * 1 + ‖x‖ * ‖x‖ * (‖y‖ * ‖y‖ / (‖x‖ * ‖x‖))))
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
-- 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
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‖))))
⊢ 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‖ / √(‖x‖ * ‖x‖ + ‖x‖ * ‖x‖ * (‖y‖ * ‖y‖ / (‖x‖ * ‖x‖))))
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
-- 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
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‖))))
⊢ 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‖ / √(‖x‖ * ‖x‖ + ‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) / (‖x‖ * ‖x‖)))
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
-- 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
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‖)))
⊢ 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‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ * (‖x‖ * ‖x‖) / (‖x‖ * ‖x‖)))
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
-- 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
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‖)))
⊢ 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‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ * (‖x‖ * ‖x‖ / (‖x‖ * ‖x‖))))
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
-- 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
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‖))))
⊢ 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‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ * 1))
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
-- 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 < angle x (x + y)
have rw : ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
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]
-- 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
⊢ ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
have pos : ∀ (hx : x = 0), ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
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
h0 : x = 0 ∨ y ≠ 0
pos : ∀ (hx : x = 0), ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
⊢ ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
have neg : ∀ (hx : ¬x = 0), ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
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
h0 : x = 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
have neg : ‖x‖ * ‖x‖ < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
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]
-- 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) ≤ π / 2
have rw : 0 ≤ ‖x‖ / ‖x + y‖
Tactic: rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_le_pi_div_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
⊢ angle x (x + y) < π / 2
have rw : 0 < ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)
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]
-- 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.cos (angle x (x + y)) = ‖x‖ / ‖x + y‖
have rw : ‖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 _))]
-- 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
⊢ ‖x‖ ≤ ‖x + y‖
have rw : ‖x‖ * ‖x‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
Tactic: rw [mul_self_le_mul_self_iff (norm_nonneg _) (norm_nonneg _),
    norm_add_sq_eq_norm_sq_add_norm_sq_real 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 ∨ y ≠ 0
⊢ Real.sin (angle x (x + y)) = ‖y‖ / ‖x + y‖
have rw : ‖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 _))]
-- 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
⊢ ‖y‖ ≤ ‖x + y‖
have rw : ‖y‖ * ‖y‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
Tactic: rw [mul_self_le_mul_self_iff (norm_nonneg _) (norm_nonneg _),
    norm_add_sq_eq_norm_sq_add_norm_sq_real 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
⊢ Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖
have pos : ∀ (h0 : x = 0), Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖
Tactic: by_cases h0 : 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 : ∀ (h0 : x = 0), Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖
⊢ Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖
have neg : ∀ (h0 : ¬x = 0), Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖
Tactic: by_cases h0 : 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
h0 : ¬x = 0
⊢ Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖
have neg : Real.tan (Real.arctan (‖y‖ / ‖x‖)) = ‖y‖ / ‖x‖
Tactic: rw [angle_add_eq_arctan_of_inner_eq_zero h h0, Real.tan_arctan]
-- 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
neg : Real.tan (Real.arctan (‖y‖ / ‖x‖)) = ‖y‖ / ‖x‖
⊢ Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖
have neg₁ : ‖y‖ / ‖x‖ = ‖y‖ / ‖x‖
Tactic: rw [angle_add_eq_arctan_of_inner_eq_zero h h0, Real.tan_arctan]
-- 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.cos (angle x (x + y)) * ‖x + y‖ = ‖x‖
have rw : ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
Tactic: rw [cos_angle_add_of_inner_eq_zero 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
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
have pos : ∀ (hxy : ‖x + y‖ = 0), ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
Tactic: by_cases hxy : ‖x + y‖ = 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 : ∀ (hxy : ‖x + y‖ = 0), ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
have neg : ∀ (hxy : ¬‖x + y‖ = 0), ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
Tactic: by_cases hxy : ‖x + y‖ = 0