awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ((-o).oangle y (x + y)).sin = ‖x‖ / ‖x + y‖
have rw : ((-o).oangle y (y + x)).sin = ‖x‖ / ‖y + x‖
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ (o.oangle x (x + y)).tan = ‖y‖ / ‖x‖
have hs : (o.oangle x (x + y)).sign = 1
Tactic: have hs : (o.oangle x (x + y)).sign = 1 := by
    rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
⊢ (o.oangle x (x + y)).tan = ‖y‖ / ‖x‖
have rw : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).tan = ‖y‖ / ‖x‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    InnerProductGeometry.tan_angle_add_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
rw : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).tan = ‖y‖ / ‖x‖
⊢ (o.oangle x (x + y)).tan = ‖y‖ / ‖x‖
have rw₁ : Real.tan (InnerProductGeometry.angle x (x + y)) = ‖y‖ / ‖x‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    InnerProductGeometry.tan_angle_add_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
rw : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).tan = ‖y‖ / ‖x‖
rw₁ : Real.tan (InnerProductGeometry.angle x (x + y)) = ‖y‖ / ‖x‖
⊢ (o.oangle x (x + y)).tan = ‖y‖ / ‖x‖
have rw₂ : ‖y‖ / ‖x‖ = ‖y‖ / ‖x‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    InnerProductGeometry.tan_angle_add_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ (o.oangle (x + y) y).tan = ‖x‖ / ‖y‖
have rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ((-o).oangle y (x + y)).tan = ‖x‖ / ‖y‖
Tactic: rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ((-o).oangle y (x + y)).tan = ‖x‖ / ‖y‖
have rw : ((-o).oangle y (y + x)).tan = ‖x‖ / ‖y‖
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ (o.oangle x (x + y)).cos * ‖x + y‖ = ‖x‖
have hs : (o.oangle x (x + y)).sign = 1
Tactic: have hs : (o.oangle x (x + y)).sign = 1 := by
    rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
⊢ (o.oangle x (x + y)).cos * ‖x + y‖ = ‖x‖
have rw : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).cos * ‖x + y‖ = ‖x‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    InnerProductGeometry.cos_angle_add_mul_norm_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
rw : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).cos * ‖x + y‖ = ‖x‖
⊢ (o.oangle x (x + y)).cos * ‖x + y‖ = ‖x‖
have rw₁ : Real.cos (InnerProductGeometry.angle x (x + y)) * ‖x + y‖ = ‖x‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    InnerProductGeometry.cos_angle_add_mul_norm_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
rw : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).cos * ‖x + y‖ = ‖x‖
rw₁ : Real.cos (InnerProductGeometry.angle x (x + y)) * ‖x + y‖ = ‖x‖
⊢ (o.oangle x (x + y)).cos * ‖x + y‖ = ‖x‖
have rw₂ : ‖x‖ = ‖x‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    InnerProductGeometry.cos_angle_add_mul_norm_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ (o.oangle (x + y) y).cos * ‖x + y‖ = ‖y‖
have rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ((-o).oangle y (x + y)).cos * ‖x + y‖ = ‖y‖
Tactic: rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ((-o).oangle y (x + y)).cos * ‖x + y‖ = ‖y‖
have rw : ((-o).oangle y (y + x)).cos * ‖y + x‖ = ‖y‖
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ (o.oangle x (x + y)).sin * ‖x + y‖ = ‖y‖
have hs : (o.oangle x (x + y)).sign = 1
Tactic: have hs : (o.oangle x (x + y)).sign = 1 := by
    rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
⊢ (o.oangle x (x + y)).sin * ‖x + y‖ = ‖y‖
have rw : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).sin * ‖x + y‖ = ‖y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    InnerProductGeometry.sin_angle_add_mul_norm_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
rw : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).sin * ‖x + y‖ = ‖y‖
⊢ (o.oangle x (x + y)).sin * ‖x + y‖ = ‖y‖
have rw₁ : Real.sin (InnerProductGeometry.angle x (x + y)) * ‖x + y‖ = ‖y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    InnerProductGeometry.sin_angle_add_mul_norm_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
rw : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).sin * ‖x + y‖ = ‖y‖
rw₁ : Real.sin (InnerProductGeometry.angle x (x + y)) * ‖x + y‖ = ‖y‖
⊢ (o.oangle x (x + y)).sin * ‖x + y‖ = ‖y‖
have rw₂ : ‖y‖ = ‖y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    InnerProductGeometry.sin_angle_add_mul_norm_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ (o.oangle (x + y) y).sin * ‖x + y‖ = ‖x‖
have rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ((-o).oangle y (x + y)).sin * ‖x + y‖ = ‖x‖
Tactic: rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ((-o).oangle y (x + y)).sin * ‖x + y‖ = ‖x‖
have rw : ((-o).oangle y (y + x)).sin * ‖y + x‖ = ‖x‖
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ (o.oangle x (x + y)).tan * ‖x‖ = ‖y‖
have hs : (o.oangle x (x + y)).sign = 1
Tactic: have hs : (o.oangle x (x + y)).sign = 1 := by
    rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
⊢ (o.oangle x (x + y)).tan * ‖x‖ = ‖y‖
have rw : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).tan * ‖x‖ = ‖y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    InnerProductGeometry.tan_angle_add_mul_norm_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inl (o.left_ne_zero_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
rw : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).tan * ‖x‖ = ‖y‖
⊢ (o.oangle x (x + y)).tan * ‖x‖ = ‖y‖
have rw₁ : Real.tan (InnerProductGeometry.angle x (x + y)) * ‖x‖ = ‖y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    InnerProductGeometry.tan_angle_add_mul_norm_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inl (o.left_ne_zero_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
rw : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).tan * ‖x‖ = ‖y‖
rw₁ : Real.tan (InnerProductGeometry.angle x (x + y)) * ‖x‖ = ‖y‖
⊢ (o.oangle x (x + y)).tan * ‖x‖ = ‖y‖
have rw₂ : ‖y‖ = ‖y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    InnerProductGeometry.tan_angle_add_mul_norm_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inl (o.left_ne_zero_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ (o.oangle (x + y) y).tan * ‖y‖ = ‖x‖
have rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ((-o).oangle y (x + y)).tan * ‖y‖ = ‖x‖
Tactic: rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ((-o).oangle y (x + y)).tan * ‖y‖ = ‖x‖
have rw : ((-o).oangle y (y + x)).tan * ‖y‖ = ‖x‖
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ ‖x‖ / (o.oangle x (x + y)).cos = ‖x + y‖
have hs : (o.oangle x (x + y)).sign = 1
Tactic: have hs : (o.oangle x (x + y)).sign = 1 := by
    rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
⊢ ‖x‖ / (o.oangle x (x + y)).cos = ‖x + y‖
have rw : ‖x‖ / (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).cos = ‖x + y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    InnerProductGeometry.norm_div_cos_angle_add_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inl (o.left_ne_zero_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
rw : ‖x‖ / (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).cos = ‖x + y‖
⊢ ‖x‖ / (o.oangle x (x + y)).cos = ‖x + y‖
have rw₁ : ‖x‖ / Real.cos (InnerProductGeometry.angle x (x + y)) = ‖x + y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    InnerProductGeometry.norm_div_cos_angle_add_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inl (o.left_ne_zero_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
rw : ‖x‖ / (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).cos = ‖x + y‖
rw₁ : ‖x‖ / Real.cos (InnerProductGeometry.angle x (x + y)) = ‖x + y‖
⊢ ‖x‖ / (o.oangle x (x + y)).cos = ‖x + y‖
have rw₂ : ‖x + y‖ = ‖x + y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    InnerProductGeometry.norm_div_cos_angle_add_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inl (o.left_ne_zero_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ ‖y‖ / (o.oangle (x + y) y).cos = ‖x + y‖
have rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ‖y‖ / ((-o).oangle y (x + y)).cos = ‖x + y‖
Tactic: rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ‖y‖ / ((-o).oangle y (x + y)).cos = ‖x + y‖
have rw : ‖y‖ / ((-o).oangle y (y + x)).cos = ‖y + x‖
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ ‖y‖ / (o.oangle x (x + y)).sin = ‖x + y‖
have hs : (o.oangle x (x + y)).sign = 1
Tactic: have hs : (o.oangle x (x + y)).sign = 1 := by
    rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
⊢ ‖y‖ / (o.oangle x (x + y)).sin = ‖x + y‖
have rw : ‖y‖ / (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).sin = ‖x + y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    InnerProductGeometry.norm_div_sin_angle_add_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inr (o.right_ne_zero_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
rw : ‖y‖ / (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).sin = ‖x + y‖
⊢ ‖y‖ / (o.oangle x (x + y)).sin = ‖x + y‖
have rw₁ : ‖y‖ / Real.sin (InnerProductGeometry.angle x (x + y)) = ‖x + y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    InnerProductGeometry.norm_div_sin_angle_add_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inr (o.right_ne_zero_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
rw : ‖y‖ / (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).sin = ‖x + y‖
rw₁ : ‖y‖ / Real.sin (InnerProductGeometry.angle x (x + y)) = ‖x + y‖
⊢ ‖y‖ / (o.oangle x (x + y)).sin = ‖x + y‖
have rw₂ : ‖x + y‖ = ‖x + y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    InnerProductGeometry.norm_div_sin_angle_add_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inr (o.right_ne_zero_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ ‖x‖ / (o.oangle (x + y) y).sin = ‖x + y‖
have rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ‖x‖ / ((-o).oangle y (x + y)).sin = ‖x + y‖
Tactic: rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ‖x‖ / ((-o).oangle y (x + y)).sin = ‖x + y‖
have rw : ‖x‖ / ((-o).oangle y (y + x)).sin = ‖y + x‖
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ ‖y‖ / (o.oangle x (x + y)).tan = ‖x‖
have hs : (o.oangle x (x + y)).sign = 1
Tactic: have hs : (o.oangle x (x + y)).sign = 1 := by
    rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
⊢ ‖y‖ / (o.oangle x (x + y)).tan = ‖x‖
have rw : ‖y‖ / (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).tan = ‖x‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    InnerProductGeometry.norm_div_tan_angle_add_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inr (o.right_ne_zero_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
rw : ‖y‖ / (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).tan = ‖x‖
⊢ ‖y‖ / (o.oangle x (x + y)).tan = ‖x‖
have rw₁ : ‖y‖ / Real.tan (InnerProductGeometry.angle x (x + y)) = ‖x‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    InnerProductGeometry.norm_div_tan_angle_add_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inr (o.right_ne_zero_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle x (x + y)).sign = 1
rw : ‖y‖ / (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).tan = ‖x‖
rw₁ : ‖y‖ / Real.tan (InnerProductGeometry.angle x (x + y)) = ‖x‖
⊢ ‖y‖ / (o.oangle x (x + y)).tan = ‖x‖
have rw₂ : ‖x‖ = ‖x‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    InnerProductGeometry.norm_div_tan_angle_add_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inr (o.right_ne_zero_of_oangle_eq_pi_div_two h))]