awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle) = (↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle) = (↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
rw₂ : (↑(Real.arcsin (dist p₃ p₂ / dist p₃ p₁)) : Real.Angle) = (↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
⊢ ∡ p₃ p₁ p₂ = (↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
have rw₃ : (↑(Real.arcsin (dist p₃ p₂ / dist p₃ p₁)) : Real.Angle) = (↑(Real.arcsin (dist p₃ p₂ / dist p₃ p₁)) : Real.Angle)
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm,
    angle_eq_arcsin_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (left_ne_of_oangle_eq_pi_div_two h)),
    dist_comm p₁ p₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ ∡ p₂ p₃ p₁ = (↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂)) : Real.Angle)
have hs : (∡ p₂ p₃ p₁).sign = 1
Tactic: have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, 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
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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ ∡ p₂ p₃ p₁ = (↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂)) : Real.Angle)
have rw : (↑(∠ p₂ p₃ p₁) : Real.Angle) = (↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂)) : Real.Angle)
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs,
    angle_eq_arctan_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (right_ne_of_oangle_eq_pi_div_two h)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
rw : (↑(∠ p₂ p₃ p₁) : Real.Angle) = (↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂)) : Real.Angle)
⊢ ∡ p₂ p₃ p₁ = (↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂)) : Real.Angle)
have rw₁ : (↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂)) : Real.Angle) = (↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂)) : Real.Angle)
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs,
    angle_eq_arctan_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (right_ne_of_oangle_eq_pi_div_two h)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ ∡ p₃ p₁ p₂ = (↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂)) : Real.Angle)
have hs : (∡ p₃ p₁ p₂).sign = 1
Tactic: have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, 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
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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ ∡ p₃ p₁ p₂ = (↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂)) : Real.Angle)
have rw : (↑(∠ p₃ p₁ p₂) : Real.Angle) = (↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂)) : Real.Angle)
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm,
    angle_eq_arctan_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (left_ne_of_oangle_eq_pi_div_two h)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle) = (↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂)) : Real.Angle)
⊢ ∡ p₃ p₁ p₂ = (↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂)) : Real.Angle)
have rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle) = (↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂)) : Real.Angle)
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm,
    angle_eq_arctan_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (left_ne_of_oangle_eq_pi_div_two h)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle) = (↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂)) : Real.Angle)
rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle) = (↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂)) : Real.Angle)
⊢ ∡ p₃ p₁ p₂ = (↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂)) : Real.Angle)
have rw₂ : (↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂)) : Real.Angle) = (↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂)) : Real.Angle)
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm,
    angle_eq_arctan_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (left_ne_of_oangle_eq_pi_div_two h)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2
have pos : ∀ (hp₂ : p₂ = p₃), |(∡ p₂ p₃ p₁).toReal| < π / 2
Tactic: by_cases hp₂ : p₂ = p₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
pos : ∀ (hp₂ : p₂ = p₃), |(∡ p₂ p₃ p₁).toReal| < π / 2
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2
have neg : ∀ (hp₂ : ¬p₂ = p₃), |(∡ p₂ p₃ p₁).toReal| < π / 2
Tactic: by_cases hp₂ : p₂ = p₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
hp₂ : ¬p₂ = p₃
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2
have pos : ∀ (hp₁ : p₁ = p₃), |(∡ p₂ p₃ p₁).toReal| < π / 2
Tactic: by_cases hp₁ : p₁ = p₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
hp₂ : ¬p₂ = p₃
pos : ∀ (hp₁ : p₁ = p₃), |(∡ p₂ p₃ p₁).toReal| < π / 2
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2
have neg : ∀ (hp₁ : ¬p₁ = p₃), |(∡ p₂ p₃ p₁).toReal| < π / 2
Tactic: by_cases hp₁ : p₁ = p₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
hp₂ : ¬p₂ = p₃
hp₁ : ¬p₁ = p₃
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2
have neg : ∠ p₂ p₃ p₁ < π / 2
Tactic: rw [← angle_eq_abs_oangle_toReal hp₂ hp₁]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ p₄ p₅ p₆ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁) = HSMul.hSMul (α := ℤ) 2 (∡ p₅ p₆ p₄)
h₁₂₃ : ∠ p₁ p₂ p₃ = π / 2
h₄₅₆ : ∠ p₄ p₅ p₆ = π / 2
⊢ ∡ p₂ p₃ p₁ = ∡ p₅ p₆ p₄
have rwa : ∀ (h : ∡ p₂ p₃ p₁ = ∡ p₅ p₆ p₄) (h₁₂₃ : ∠ p₁ p₂ p₃ = π / 2) (h₄₅₆ : ∠ p₄ p₅ p₆ = π / 2), ∡ p₂ p₃ p₁ = ∡ p₅ p₆ p₄
Tactic: rwa [Real.Angle.two_zsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two
    (abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two h₁₂₃)
    (abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two h₄₅₆)] at h
Cleared hypotheses: h, h₁₂₃, h₄₅₆
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ p₄ p₅ p₆ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁) = HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₆ p₅)
h₁₂₃ : ∠ p₁ p₂ p₃ = π / 2
h₄₅₆ : ∠ p₄ p₅ p₆ = π / 2
⊢ ∡ p₂ p₃ p₁ = ∡ p₄ p₆ p₅
have refine : |(∡ p₄ p₆ p₅).toReal| < π / 2
Tactic: refine (Real.Angle.two_zsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two
    (abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two h₁₂₃) ?_).1 h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ p₄ p₅ p₆ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁) = HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₆ p₅)
h₁₂₃ : ∠ p₁ p₂ p₃ = π / 2
h₄₅₆ : ∠ p₄ p₅ p₆ = π / 2
⊢ |(∡ p₄ p₆ p₅).toReal| < π / 2
have rw : |(∡ p₅ p₆ p₄).toReal| < π / 2
Tactic: rw [oangle_rev, Real.Angle.abs_toReal_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ (∡ p₂ p₃ p₁).cos = dist p₃ p₂ / dist p₁ p₃
have hs : (∡ p₂ p₃ p₁).sign = 1
Tactic: have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, 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
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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ (∡ p₂ p₃ p₁).cos = dist p₃ p₂ / dist p₁ p₃
have rw : (↑(∠ p₂ p₃ p₁) : Real.Angle).cos = dist p₃ p₂ / dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    cos_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
rw : (↑(∠ p₂ p₃ p₁) : Real.Angle).cos = dist p₃ p₂ / dist p₁ p₃
⊢ (∡ p₂ p₃ p₁).cos = dist p₃ p₂ / dist p₁ p₃
have rw₁ : Real.cos (∠ p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    cos_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
rw : (↑(∠ p₂ p₃ p₁) : Real.Angle).cos = dist p₃ p₂ / dist p₁ p₃
rw₁ : Real.cos (∠ p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃
⊢ (∡ p₂ p₃ p₁).cos = dist p₃ p₂ / dist p₁ p₃
have rw₂ : dist p₃ p₂ / dist p₁ p₃ = dist p₃ p₂ / dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    cos_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ (∡ p₃ p₁ p₂).cos = dist p₁ p₂ / dist p₁ p₃
have hs : (∡ p₃ p₁ p₂).sign = 1
Tactic: have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, 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
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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ (∡ p₃ p₁ p₂).cos = dist p₁ p₂ / dist p₁ p₃
have rw : (↑(∠ p₃ p₁ p₂) : Real.Angle).cos = dist p₁ p₂ / dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe,
    cos_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h),
    dist_comm p₁ p₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle).cos = dist p₁ p₂ / dist p₁ p₃
⊢ (∡ p₃ p₁ p₂).cos = dist p₁ p₂ / dist p₁ p₃
have rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle).cos = dist p₁ p₂ / dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe,
    cos_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h),
    dist_comm p₁ p₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle).cos = dist p₁ p₂ / dist p₁ p₃
rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle).cos = dist p₁ p₂ / dist p₁ p₃
⊢ (∡ p₃ p₁ p₂).cos = dist p₁ p₂ / dist p₁ p₃
have rw₂ : Real.cos (∠ p₂ p₁ p₃) = dist p₁ p₂ / dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe,
    cos_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h),
    dist_comm p₁ p₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle).cos = dist p₁ p₂ / dist p₁ p₃
rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle).cos = dist p₁ p₂ / dist p₁ p₃
rw₂ : Real.cos (∠ p₂ p₁ p₃) = dist p₁ p₂ / dist p₁ p₃
⊢ (∡ p₃ p₁ p₂).cos = dist p₁ p₂ / dist p₁ p₃
have rw₃ : dist p₁ p₂ / dist p₃ p₁ = dist p₁ p₂ / dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe,
    cos_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h),
    dist_comm p₁ p₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle).cos = dist p₁ p₂ / dist p₁ p₃
rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle).cos = dist p₁ p₂ / dist p₁ p₃
rw₂ : Real.cos (∠ p₂ p₁ p₃) = dist p₁ p₂ / dist p₁ p₃
rw₃ : dist p₁ p₂ / dist p₃ p₁ = dist p₁ p₂ / dist p₁ p₃
⊢ (∡ p₃ p₁ p₂).cos = dist p₁ p₂ / dist p₁ p₃
have rw₄ : dist p₁ p₂ / dist p₃ p₁ = dist p₁ p₂ / dist p₃ p₁
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe,
    cos_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h),
    dist_comm p₁ p₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ (∡ p₂ p₃ p₁).sin = dist p₁ p₂ / dist p₁ p₃
have hs : (∡ p₂ p₃ p₁).sign = 1
Tactic: have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, 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
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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ (∡ p₂ p₃ p₁).sin = dist p₁ p₂ / dist p₁ p₃
have rw : (↑(∠ p₂ p₃ p₁) : Real.Angle).sin = dist p₁ p₂ / dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    sin_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
rw : (↑(∠ p₂ p₃ p₁) : Real.Angle).sin = dist p₁ p₂ / dist p₁ p₃
⊢ (∡ p₂ p₃ p₁).sin = dist p₁ p₂ / dist p₁ p₃
have rw₁ : Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    sin_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
rw : (↑(∠ p₂ p₃ p₁) : Real.Angle).sin = dist p₁ p₂ / dist p₁ p₃
rw₁ : Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
⊢ (∡ p₂ p₃ p₁).sin = dist p₁ p₂ / dist p₁ p₃
have rw₂ : dist p₁ p₂ / dist p₁ p₃ = dist p₁ p₂ / dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    sin_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ (∡ p₃ p₁ p₂).sin = dist p₃ p₂ / dist p₁ p₃
have hs : (∡ p₃ p₁ p₂).sign = 1
Tactic: have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, 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
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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ (∡ p₃ p₁ p₂).sin = dist p₃ p₂ / dist p₁ p₃
have rw : (↑(∠ p₃ p₁ p₂) : Real.Angle).sin = dist p₃ p₂ / dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe,
    sin_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (left_ne_of_oangle_eq_pi_div_two h)),
    dist_comm p₁ p₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle).sin = dist p₃ p₂ / dist p₁ p₃
⊢ (∡ p₃ p₁ p₂).sin = dist p₃ p₂ / dist p₁ p₃
have rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle).sin = dist p₃ p₂ / dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe,
    sin_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (left_ne_of_oangle_eq_pi_div_two h)),
    dist_comm p₁ p₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle).sin = dist p₃ p₂ / dist p₁ p₃
rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle).sin = dist p₃ p₂ / dist p₁ p₃
⊢ (∡ p₃ p₁ p₂).sin = dist p₃ p₂ / dist p₁ p₃
have rw₂ : Real.sin (∠ p₂ p₁ p₃) = dist p₃ p₂ / dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe,
    sin_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (left_ne_of_oangle_eq_pi_div_two h)),
    dist_comm p₁ p₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (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₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle).sin = dist p₃ p₂ / dist p₁ p₃
rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle).sin = dist p₃ p₂ / dist p₁ p₃
rw₂ : Real.sin (∠ p₂ p₁ p₃) = dist p₃ p₂ / dist p₁ p₃
⊢ (∡ p₃ p₁ p₂).sin = dist p₃ p₂ / dist p₁ p₃
have rw₃ : dist p₃ p₂ / dist p₃ p₁ = dist p₃ p₂ / dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe,
    sin_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (left_ne_of_oangle_eq_pi_div_two h)),
    dist_comm p₁ p₃]