awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Projection (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p' : P
s : AffineSubspace ℝ P
inst_5 : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
⊢ ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(π / 2) : Real.Angle) ∨
    ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(-π / 2) : Real.Angle)
have this : Nonempty.{u_2 + 1} ↥s
Tactic: haveI : Nonempty s := ⟨p', h⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Projection (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p' : P
s : AffineSubspace ℝ P
inst_5 : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
this : Nonempty.{u_2 + 1} ↥s
⊢ ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(π / 2) : Real.Angle) ∨
    ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(-π / 2) : Real.Angle)
have hpne : p ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
Tactic: have hpne : p ≠ orthogonalProjection s p := Ne.symm (orthogonalProjection_eq_self_iff.not.2 hp)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Projection (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p' : P
s : AffineSubspace ℝ P
inst_5 : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
this : Nonempty.{u_2 + 1} ↥s
hpne : p ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
⊢ ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(π / 2) : Real.Angle) ∨
    ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(-π / 2) : Real.Angle)
have ha : ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' =
    (↑(∠ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p') : Real.Angle) ∨
  ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' =
    -(↑(∠ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p') : Real.Angle)
Tactic: have ha := oangle_eq_angle_or_eq_neg_angle hpne hp'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Projection (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p' : P
s : AffineSubspace ℝ P
inst_5 : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
this : Nonempty.{u_2 + 1} ↥s
hpne : p ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
ha :
  ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' =
      (↑(∠ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p') : Real.Angle) ∨
    ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' =
      -(↑(∠ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p') : Real.Angle)
⊢ ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(π / 2) : Real.Angle) ∨
    ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(-π / 2) : Real.Angle)
have ha₁ : ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(π / 2) : Real.Angle) ∨
  ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = -(↑(π / 2) : Real.Angle)
Tactic: rw [angle_self_orthogonalProjection p h] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Projection (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p' : P
s : AffineSubspace ℝ P
inst_5 : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
this : Nonempty.{u_2 + 1} ↥s
hpne : p ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
ha :
  ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(π / 2) : Real.Angle) ∨
    ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = -(↑(π / 2) : Real.Angle)
⊢ ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(π / 2) : Real.Angle) ∨
    ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(-π / 2) : Real.Angle)
have rwa : ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(π / 2) : Real.Angle) ∨
  ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(-(π / 2)) : Real.Angle)
Tactic: rwa [neg_div]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Projection (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p' : P
s : AffineSubspace ℝ P
inst_5 : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
⊢ ∡ p' (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p = (↑(π / 2) : Real.Angle) ∨
    ∡ p' (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p = (↑(-π / 2) : Real.Angle)
have rw : ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(π / 2) : Real.Angle) ∨
  ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(-π / 2) : Real.Angle)
Tactic: rw [oangle_rev, neg_eq_iff_eq_neg, neg_eq_iff_eq_neg, or_comm, ← Real.Angle.coe_neg, neg_div,
    neg_neg, ← Real.Angle.coe_neg, ← neg_div]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Projection (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p' : P
s : AffineSubspace ℝ P
inst_5 : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p') = (↑π : Real.Angle)
have rw : ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(π / 2) : Real.Angle) ∨
  ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(-π / 2) : Real.Angle)
Tactic: rw [Real.Angle.two_zsmul_eq_pi_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Projection (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p p' : P
s : AffineSubspace ℝ P
inst_5 : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p' (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p) = (↑π : Real.Angle)
have rw : ∡ p' (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p = (↑(π / 2) : Real.Angle) ∨
  ∡ p' (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p = (↑(-π / 2) : Real.Angle)
Tactic: rw [Real.Angle.two_zsmul_eq_pi_iff]
-- 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 (x + y)).sign = 1
have rw : (o.oangle x y).sign = 1
Tactic: 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)
rw : (o.oangle x y).sign = 1
⊢ (o.oangle x (x + y)).sign = 1
have rw₁ : (↑(π / 2) : Real.Angle).sign = 1
Tactic: 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)
rw : (o.oangle x y).sign = 1
rw₁ : (↑(π / 2) : Real.Angle).sign = 1
⊢ (o.oangle x (x + y)).sign = 1
have rw₂ : Eq (α := SignType) 1 1
Tactic: rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
-- 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) = (↑(Real.arccos (‖x‖ / ‖x + y‖)) : Real.Angle)
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) = (↑(Real.arccos (‖x‖ / ‖x + y‖)) : Real.Angle)
have rw : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle) = (↑(Real.arccos (‖x‖ / ‖x + y‖)) : Real.Angle)
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs,
    InnerProductGeometry.angle_add_eq_arccos_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) = (↑(Real.arccos (‖x‖ / ‖x + y‖)) : Real.Angle)
⊢ o.oangle x (x + y) = (↑(Real.arccos (‖x‖ / ‖x + y‖)) : Real.Angle)
have rw₁ : (↑(Real.arccos (‖x‖ / ‖x + y‖)) : Real.Angle) = (↑(Real.arccos (‖x‖ / ‖x + y‖)) : Real.Angle)
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs,
    InnerProductGeometry.angle_add_eq_arccos_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 = (↑(Real.arccos (‖y‖ / ‖x + y‖)) : Real.Angle)
have rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), (-o).oangle y (x + y) = (↑(Real.arccos (‖y‖ / ‖x + y‖)) : Real.Angle)
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) = (↑(Real.arccos (‖y‖ / ‖x + y‖)) : Real.Angle)
have rw : (-o).oangle y (y + x) = (↑(Real.arccos (‖y‖ / ‖y + x‖)) : Real.Angle)
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) = (↑(Real.arcsin (‖y‖ / ‖x + y‖)) : Real.Angle)
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) = (↑(Real.arcsin (‖y‖ / ‖x + y‖)) : Real.Angle)
have rw : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle) = (↑(Real.arcsin (‖y‖ / ‖x + y‖)) : Real.Angle)
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs,
    InnerProductGeometry.angle_add_eq_arcsin_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) = (↑(Real.arcsin (‖y‖ / ‖x + y‖)) : Real.Angle)
⊢ o.oangle x (x + y) = (↑(Real.arcsin (‖y‖ / ‖x + y‖)) : Real.Angle)
have rw₁ : (↑(Real.arcsin (‖y‖ / ‖x + y‖)) : Real.Angle) = (↑(Real.arcsin (‖y‖ / ‖x + y‖)) : Real.Angle)
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs,
    InnerProductGeometry.angle_add_eq_arcsin_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 = (↑(Real.arcsin (‖x‖ / ‖x + y‖)) : Real.Angle)
have rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), (-o).oangle y (x + y) = (↑(Real.arcsin (‖x‖ / ‖x + y‖)) : Real.Angle)
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) = (↑(Real.arcsin (‖x‖ / ‖x + y‖)) : Real.Angle)
have rw : (-o).oangle y (y + x) = (↑(Real.arcsin (‖x‖ / ‖y + x‖)) : Real.Angle)
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) = (↑(Real.arctan (‖y‖ / ‖x‖)) : Real.Angle)
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) = (↑(Real.arctan (‖y‖ / ‖x‖)) : Real.Angle)
have rw : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle) = (↑(Real.arctan (‖y‖ / ‖x‖)) : Real.Angle)
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs,
    InnerProductGeometry.angle_add_eq_arctan_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h) (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) = (↑(Real.arctan (‖y‖ / ‖x‖)) : Real.Angle)
⊢ o.oangle x (x + y) = (↑(Real.arctan (‖y‖ / ‖x‖)) : Real.Angle)
have rw₁ : (↑(Real.arctan (‖y‖ / ‖x‖)) : Real.Angle) = (↑(Real.arctan (‖y‖ / ‖x‖)) : Real.Angle)
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs,
    InnerProductGeometry.angle_add_eq_arctan_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h) (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 = (↑(Real.arctan (‖x‖ / ‖y‖)) : Real.Angle)
have rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), (-o).oangle y (x + y) = (↑(Real.arctan (‖x‖ / ‖y‖)) : Real.Angle)
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) = (↑(Real.arctan (‖x‖ / ‖y‖)) : Real.Angle)
have rw : (-o).oangle y (y + x) = (↑(Real.arctan (‖x‖ / ‖y‖)) : Real.Angle)
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‖ / ‖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)).cos = ‖x‖ / ‖x + y‖
have rw : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).cos = ‖x‖ / ‖x + y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    InnerProductGeometry.cos_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).cos = ‖x‖ / ‖x + y‖
⊢ (o.oangle x (x + y)).cos = ‖x‖ / ‖x + y‖
have rw₁ : Real.cos (InnerProductGeometry.angle x (x + y)) = ‖x‖ / ‖x + y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    InnerProductGeometry.cos_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).cos = ‖x‖ / ‖x + y‖
rw₁ : Real.cos (InnerProductGeometry.angle x (x + y)) = ‖x‖ / ‖x + y‖
⊢ (o.oangle x (x + y)).cos = ‖x‖ / ‖x + y‖
have rw₂ : ‖x‖ / ‖x + y‖ = ‖x‖ / ‖x + y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    InnerProductGeometry.cos_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).cos = ‖y‖ / ‖x + y‖
have rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ((-o).oangle y (x + y)).cos = ‖y‖ / ‖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)).cos = ‖y‖ / ‖x + y‖
have rw : ((-o).oangle y (y + x)).cos = ‖y‖ / ‖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)).sin = ‖y‖ / ‖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)).sin = ‖y‖ / ‖x + y‖
have rw : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).sin = ‖y‖ / ‖x + y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    InnerProductGeometry.sin_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 : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).sin = ‖y‖ / ‖x + y‖
⊢ (o.oangle x (x + y)).sin = ‖y‖ / ‖x + y‖
have rw₁ : Real.sin (InnerProductGeometry.angle x (x + y)) = ‖y‖ / ‖x + y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    InnerProductGeometry.sin_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 : (↑(InnerProductGeometry.angle x (x + y)) : Real.Angle).sin = ‖y‖ / ‖x + y‖
rw₁ : Real.sin (InnerProductGeometry.angle x (x + y)) = ‖y‖ / ‖x + y‖
⊢ (o.oangle x (x + y)).sin = ‖y‖ / ‖x + y‖
have rw₂ : ‖y‖ / ‖x + y‖ = ‖y‖ / ‖x + y‖
Tactic: rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    InnerProductGeometry.sin_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)
⊢ (o.oangle (x + y) y).sin = ‖x‖ / ‖x + y‖
have rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ((-o).oangle y (x + y)).sin = ‖x‖ / ‖x + y‖
Tactic: rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
Cleared hypotheses: h