awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hxy : ‖x + y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
have h' : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
Tactic: have h' := norm_add_sq_eq_norm_sq_add_norm_sq_real h
-- 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
hxy : ‖x + y‖ = 0
h' : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
have h'₁ : ‖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'
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
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
have pos : ∀ (h0 : x = 0 ∧ y = 0), Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
Tactic: by_cases h0 : x = 0 ∧ 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 : ∀ (h0 : x = 0 ∧ y = 0), Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
have neg : ∀ (h0 : ¬(x = 0 ∧ y = 0)), Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
Tactic: by_cases h0 : x = 0 ∧ y = 0
-- 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)
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
have h0₁ : ¬x = 0 ∨ ¬y = 0
Tactic: rw [not_and_or] at 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
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
have neg : ‖x + y‖ ≠ 0
Tactic: rw [sin_angle_add_of_inner_eq_zero h h0, div_mul_cancel₀]
-- 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 + y‖ ≠ 0
have neg : ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ≠ 0
Tactic: rw [← mul_self_ne_zero, 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
⊢ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ≠ 0
have neg : 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
Tactic: refine (ne_of_lt ?_).symm
-- 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 neg : ∀ (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
neg : ∀ (h0 : ¬x = 0), 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
have neg₁ : ∀ (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 (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.tan (angle x (x + y)) * ‖x‖ = ‖y‖
have rw : ‖y‖ / ‖x‖ * ‖x‖ = ‖y‖
Tactic: rw [tan_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
h0 : x ≠ 0 ∨ y = 0
⊢ ‖y‖ / ‖x‖ * ‖x‖ = ‖y‖
have inl : ∀ (h0 : x ≠ 0), ‖y‖ / ‖x‖ * ‖x‖ = ‖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), ‖y‖ / ‖x‖ * ‖x‖ = ‖y‖
⊢ ‖y‖ / ‖x‖ * ‖x‖ = ‖y‖
have inr : ∀ (h0 : y = 0), ‖y‖ / ‖x‖ * ‖x‖ = ‖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
⊢ ‖x‖ / Real.cos (angle x (x + y)) = ‖x + y‖
have rw : ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
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
h0 : x ≠ 0 ∨ y = 0
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
have inl : ∀ (h0 : x ≠ 0), ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + 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), ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
have inr : ∀ (h0 : y = 0), ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + 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
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
have inl : ‖x‖ * ‖x + y‖ / ‖x‖ = ‖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)]
-- 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
inl : ‖x‖ * ‖x + y‖ / ‖x‖ = ‖x + y‖
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
have inl₁ : ‖x + y‖ * ‖x‖ / ‖x‖ = ‖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)]
-- 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
inl : ‖x‖ * ‖x + y‖ / ‖x‖ = ‖x + y‖
inl₁ : ‖x + y‖ * ‖x‖ / ‖x‖ = ‖x + y‖
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
have inl₂ : ‖x + y‖ * ‖x‖ * ‖x‖⁻¹ = ‖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)]
-- 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
inl : ‖x‖ * ‖x + y‖ / ‖x‖ = ‖x + y‖
inl₁ : ‖x + y‖ * ‖x‖ / ‖x‖ = ‖x + y‖
inl₂ : ‖x + y‖ * ‖x‖ * ‖x‖⁻¹ = ‖x + y‖
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
have inl₃ : ‖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)]
-- 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‖ / Real.sin (angle x (x + y)) = ‖x + y‖
have inl : ∀ (h0 : x = 0), ‖y‖ / Real.sin (angle x (x + y)) = ‖x + 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), ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖
have inr : ∀ (h0 : y ≠ 0), ‖y‖ / Real.sin (angle x (x + y)) = ‖x + 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 : y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖
have inr : ‖y‖ / (‖y‖ / ‖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)]
-- 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 : y ≠ 0
inr : ‖y‖ / (‖y‖ / ‖x + y‖) = ‖x + y‖
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖
have inr₁ : ‖y‖ * ‖x + y‖ / ‖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)]
-- 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 : y ≠ 0
inr : ‖y‖ / (‖y‖ / ‖x + y‖) = ‖x + y‖
inr₁ : ‖y‖ * ‖x + y‖ / ‖y‖ = ‖x + y‖
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖
have inr₂ : ‖x + y‖ * ‖y‖ / ‖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)]
-- 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 : y ≠ 0
inr : ‖y‖ / (‖y‖ / ‖x + y‖) = ‖x + y‖
inr₁ : ‖y‖ * ‖x + y‖ / ‖y‖ = ‖x + y‖
inr₂ : ‖x + y‖ * ‖y‖ / ‖y‖ = ‖x + y‖
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖
have inr₃ : ‖x + y‖ * ‖y‖ * ‖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)]
-- 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 : 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‖
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖
have inr₄ : ‖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)]
-- 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‖ / Real.tan (angle x (x + y)) = ‖x‖
have rw : ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
Tactic: rw [tan_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
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
have inl : ∀ (h0 : x = 0), ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
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), ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
have inr : ∀ (h0 : y ≠ 0), ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
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 : y ≠ 0
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
have inr : ‖y‖ * ‖x‖ / ‖y‖ = ‖x‖
Tactic: rw [div_div_eq_mul_div, mul_comm, div_eq_mul_inv, mul_inv_cancel_right₀ (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 : y ≠ 0
inr : ‖y‖ * ‖x‖ / ‖y‖ = ‖x‖
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
have inr₁ : ‖x‖ * ‖y‖ / ‖y‖ = ‖x‖
Tactic: rw [div_div_eq_mul_div, mul_comm, div_eq_mul_inv, mul_inv_cancel_right₀ (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 : y ≠ 0
inr : ‖y‖ * ‖x‖ / ‖y‖ = ‖x‖
inr₁ : ‖x‖ * ‖y‖ / ‖y‖ = ‖x‖
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
have inr₂ : ‖x‖ * ‖y‖ * ‖y‖⁻¹ = ‖x‖
Tactic: rw [div_div_eq_mul_div, mul_comm, div_eq_mul_inv, mul_inv_cancel_right₀ (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 : y ≠ 0
inr : ‖y‖ * ‖x‖ / ‖y‖ = ‖x‖
inr₁ : ‖x‖ * ‖y‖ / ‖y‖ = ‖x‖
inr₂ : ‖x‖ * ‖y‖ * ‖y‖⁻¹ = ‖x‖
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
have inr₃ : ‖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)]
-- 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
⊢ angle x (x - y) = Real.arccos (‖x‖ / ‖x - y‖)
have h₁ : ⟪x, -y⟫ = 0
Tactic: rw [← neg_eq_zero, ← inner_neg_right] at h
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
⊢ angle x (x - y) = Real.arccos (‖x‖ / ‖x - y‖)
have rw : angle x (x + -y) = Real.arccos (‖x‖ / ‖x + -y‖)
Tactic: rw [sub_eq_add_neg, angle_add_eq_arccos_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
rw : angle x (x + -y) = Real.arccos (‖x‖ / ‖x + -y‖)
⊢ angle x (x - y) = Real.arccos (‖x‖ / ‖x - y‖)
have rw₁ : Real.arccos (‖x‖ / ‖x + -y‖) = Real.arccos (‖x‖ / ‖x + -y‖)
Tactic: rw [sub_eq_add_neg, angle_add_eq_arccos_of_inner_eq_zero h]
-- 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 h₁ : ⟪x, -y⟫ = 0
Tactic: rw [← neg_eq_zero, ← inner_neg_right] at h
Cleared hypotheses: h, 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 h0₁ : x ≠ 0 ∨ -y ≠ 0
Tactic: rw [or_comm, ← neg_ne_zero, or_comm] at 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
⊢ angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)
have rw : angle x (x + -y) = Real.arcsin (‖y‖ / ‖x + -y‖)
Tactic: rw [sub_eq_add_neg, angle_add_eq_arcsin_of_inner_eq_zero h h0, norm_neg]
-- 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
rw : angle x (x + -y) = Real.arcsin (‖y‖ / ‖x + -y‖)
⊢ angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)
have rw₁ : Real.arcsin (‖-y‖ / ‖x + -y‖) = Real.arcsin (‖y‖ / ‖x + -y‖)
Tactic: rw [sub_eq_add_neg, angle_add_eq_arcsin_of_inner_eq_zero h h0, norm_neg]
-- 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
rw : angle x (x + -y) = Real.arcsin (‖y‖ / ‖x + -y‖)
rw₁ : Real.arcsin (‖-y‖ / ‖x + -y‖) = Real.arcsin (‖y‖ / ‖x + -y‖)
⊢ angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)
have rw₂ : Real.arcsin (‖y‖ / ‖x + -y‖) = Real.arcsin (‖y‖ / ‖x + -y‖)
Tactic: rw [sub_eq_add_neg, angle_add_eq_arcsin_of_inner_eq_zero h h0, norm_neg]
-- 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
⊢ angle x (x - y) = Real.arctan (‖y‖ / ‖x‖)
have h₁ : ⟪x, -y⟫ = 0
Tactic: rw [← neg_eq_zero, ← inner_neg_right] at h
Cleared hypotheses: h, 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
⊢ angle x (x - y) = Real.arctan (‖y‖ / ‖x‖)
have rw : angle x (x + -y) = Real.arctan (‖y‖ / ‖x‖)
Tactic: rw [sub_eq_add_neg, angle_add_eq_arctan_of_inner_eq_zero h h0, norm_neg]
-- 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 : angle x (x + -y) = Real.arctan (‖y‖ / ‖x‖)
⊢ angle x (x - y) = Real.arctan (‖y‖ / ‖x‖)
have rw₁ : Real.arctan (‖-y‖ / ‖x‖) = Real.arctan (‖y‖ / ‖x‖)
Tactic: rw [sub_eq_add_neg, angle_add_eq_arctan_of_inner_eq_zero h h0, norm_neg]
-- 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 : angle x (x + -y) = Real.arctan (‖y‖ / ‖x‖)
rw₁ : Real.arctan (‖-y‖ / ‖x‖) = Real.arctan (‖y‖ / ‖x‖)
⊢ angle x (x - y) = Real.arctan (‖y‖ / ‖x‖)
have rw₂ : Real.arctan (‖y‖ / ‖x‖) = Real.arctan (‖y‖ / ‖x‖)
Tactic: rw [sub_eq_add_neg, angle_add_eq_arctan_of_inner_eq_zero h h0, norm_neg]
-- 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
⊢ 0 < angle x (x - y)
have h₁ : ⟪x, -y⟫ = 0
Tactic: rw [← neg_eq_zero, ← inner_neg_right] at h
Cleared hypotheses: h, 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
⊢ 0 < angle x (x - y)
have h0₁ : x = 0 ∨ -y ≠ 0
Tactic: rw [← neg_ne_zero] at 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
⊢ 0 < angle x (x - y)
have rw : 0 < angle x (x + -y)
Tactic: rw [sub_eq_add_neg]
-- 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
⊢ angle x (x - y) ≤ π / 2
have h₁ : ⟪x, -y⟫ = 0
Tactic: rw [← neg_eq_zero, ← inner_neg_right] at h
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
⊢ angle x (x - y) ≤ π / 2
have rw : angle x (x + -y) ≤ π / 2
Tactic: rw [sub_eq_add_neg]
-- 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
⊢ angle x (x - y) < π / 2
have h₁ : ⟪x, -y⟫ = 0
Tactic: rw [← neg_eq_zero, ← inner_neg_right] at h
Cleared hypotheses: h, 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
⊢ angle x (x - y) < π / 2
have rw : angle x (x + -y) < π / 2
Tactic: rw [sub_eq_add_neg]
-- 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
⊢ Real.cos (angle x (x - y)) = ‖x‖ / ‖x - y‖
have h₁ : ⟪x, -y⟫ = 0
Tactic: rw [← neg_eq_zero, ← inner_neg_right] at h
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
⊢ Real.cos (angle x (x - y)) = ‖x‖ / ‖x - y‖
have rw : Real.cos (angle x (x + -y)) = ‖x‖ / ‖x + -y‖
Tactic: rw [sub_eq_add_neg, 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
rw : Real.cos (angle x (x + -y)) = ‖x‖ / ‖x + -y‖
⊢ Real.cos (angle x (x - y)) = ‖x‖ / ‖x - y‖
have rw₁ : ‖x‖ / ‖x + -y‖ = ‖x‖ / ‖x + -y‖
Tactic: rw [sub_eq_add_neg, cos_angle_add_of_inner_eq_zero h]
-- 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
⊢ Real.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖
have h₁ : ⟪x, -y⟫ = 0
Tactic: rw [← neg_eq_zero, ← inner_neg_right] at h
Cleared hypotheses: h, 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
⊢ Real.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖
have h0₁ : x ≠ 0 ∨ -y ≠ 0
Tactic: rw [or_comm, ← neg_ne_zero, or_comm] at 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
⊢ Real.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖
have rw : Real.sin (angle x (x + -y)) = ‖y‖ / ‖x + -y‖
Tactic: rw [sub_eq_add_neg, sin_angle_add_of_inner_eq_zero h h0, norm_neg]
-- 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
rw : Real.sin (angle x (x + -y)) = ‖y‖ / ‖x + -y‖
⊢ Real.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖
have rw₁ : ‖-y‖ / ‖x + -y‖ = ‖y‖ / ‖x + -y‖
Tactic: rw [sub_eq_add_neg, sin_angle_add_of_inner_eq_zero h h0, norm_neg]
-- 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
rw : Real.sin (angle x (x + -y)) = ‖y‖ / ‖x + -y‖
rw₁ : ‖-y‖ / ‖x + -y‖ = ‖y‖ / ‖x + -y‖
⊢ Real.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖
have rw₂ : ‖y‖ / ‖x + -y‖ = ‖y‖ / ‖x + -y‖
Tactic: rw [sub_eq_add_neg, sin_angle_add_of_inner_eq_zero h h0, norm_neg]
-- 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
⊢ Real.tan (angle x (x - y)) = ‖y‖ / ‖x‖
have h₁ : ⟪x, -y⟫ = 0
Tactic: rw [← neg_eq_zero, ← inner_neg_right] at h
Cleared hypotheses: h