awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
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₃
rw₂ rw₃ : dist p₁ p₂ / dist p₁ p₃ = dist p₁ p₂ / dist p₁ p₃
⊢ (∡ p₂ p₃ p₁).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))]

Premises used: EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.sin_angle_of_angle_eq_pi_div_two, Real.Angle.sin_coe, EuclideanGeometry.left_ne_of_oangle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one, Or.inl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
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₃
rw₃ : dist p₃ p₂ / dist p₃ p₁ = dist p₃ p₂ / dist p₁ p₃
rw₄ rw₅ : dist p₃ p₂ / dist p₃ p₁ = dist p₃ p₂ / dist p₃ p₁
⊢ (∡ p₃ p₁ p₂).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₃]

Premises used: EuclideanGeometry.angle_comm, dist_comm, EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.sin_angle_of_angle_eq_pi_div_two, Real.Angle.sin_coe, EuclideanGeometry.left_ne_of_oangle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one, Or.inr
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
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).tan = dist p₁ p₂ / dist p₃ p₂
rw₁ : Real.tan (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂
rw₂ rw₃ : dist p₁ p₂ / dist p₃ p₂ = dist p₁ p₂ / dist p₃ p₂
⊢ (∡ p₂ p₃ p₁).tan = dist p₁ p₂ / dist p₃ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    tan_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

Premises used: EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.tan_angle_of_angle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one, Real.Angle.tan_coe
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
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).tan = dist p₃ p₂ / dist p₁ p₂
rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle).tan = dist p₃ p₂ / dist p₁ p₂
rw₂ : Real.tan (∠ p₂ p₁ p₃) = dist p₃ p₂ / dist p₁ p₂
rw₃ rw₄ : dist p₃ p₂ / dist p₁ p₂ = dist p₃ p₂ / dist p₁ p₂
⊢ (∡ p₃ p₁ p₂).tan = dist p₃ p₂ / dist p₁ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.tan_coe,
    tan_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.tan_angle_of_angle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one, Real.Angle.tan_coe
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
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₂
rw₂ rw₃ : dist p₃ p₂ = dist p₃ p₂
⊢ (∡ p₂ p₃ p₁).cos * dist p₁ p₃ = dist p₃ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    cos_angle_mul_dist_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

Premises used: EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.cos_angle_mul_dist_of_angle_eq_pi_div_two, Real.Angle.cos_coe, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
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₃ : Real.cos (∠ p₂ p₁ p₃) * dist p₃ p₁ = dist p₁ p₂
rw₄ rw₅ : dist p₁ p₂ = dist p₁ p₂
⊢ (∡ p₃ p₁ p₂).cos * dist p₁ p₃ = dist p₁ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe, dist_comm p₁ p₃,
    cos_angle_mul_dist_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

Premises used: EuclideanGeometry.angle_comm, dist_comm, EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.cos_angle_mul_dist_of_angle_eq_pi_div_two, Real.Angle.cos_coe, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
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₂
rw₂ rw₃ : dist p₁ p₂ = dist p₁ p₂
⊢ (∡ p₂ p₃ p₁).sin * dist p₁ p₃ = dist p₁ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    sin_angle_mul_dist_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

Premises used: EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two, Real.Angle.sin_coe, EuclideanGeometry.sin_angle_mul_dist_of_angle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
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₂
rw₃ : Real.sin (∠ p₂ p₁ p₃) * dist p₃ p₁ = dist p₃ p₂
rw₄ rw₅ : dist p₃ p₂ = dist p₃ p₂
⊢ (∡ p₃ p₁ p₂).sin * dist p₁ p₃ = dist p₃ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe, dist_comm p₁ p₃,
    sin_angle_mul_dist_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

Premises used: EuclideanGeometry.angle_comm, dist_comm, EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two, Real.Angle.sin_coe, EuclideanGeometry.sin_angle_mul_dist_of_angle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
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).tan * dist p₃ p₂ = dist p₁ p₂
rw₁ : Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂
rw₂ rw₃ : dist p₁ p₂ = dist p₁ p₂
⊢ (∡ p₂ p₃ p₁).tan * dist p₃ p₂ = dist p₁ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    tan_angle_mul_dist_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (right_ne_of_oangle_eq_pi_div_two h))]

Premises used: EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.tan_angle_mul_dist_of_angle_eq_pi_div_two, EuclideanGeometry.right_ne_of_oangle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one, Or.inr, Real.Angle.tan_coe
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
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).tan * dist p₁ p₂ = dist p₃ p₂
rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle).tan * dist p₁ p₂ = dist p₃ p₂
rw₂ : Real.tan (∠ p₂ p₁ p₃) * dist p₁ p₂ = dist p₃ p₂
rw₃ rw₄ : dist p₃ p₂ = dist p₃ p₂
⊢ (∡ p₃ p₁ p₂).tan * dist p₁ p₂ = dist p₃ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.tan_coe,
    tan_angle_mul_dist_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))]

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.tan_angle_mul_dist_of_angle_eq_pi_div_two, EuclideanGeometry.left_ne_of_oangle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one, Or.inr, Real.Angle.tan_coe
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
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 : dist p₃ p₂ / (↑(∠ p₂ p₃ p₁) : Real.Angle).cos = dist p₁ p₃
rw₁ : dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃
rw₂ rw₃ : dist p₁ p₃ = dist p₁ p₃
⊢ dist p₃ p₂ / (∡ p₂ p₃ p₁).cos = dist p₁ p₃

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    dist_div_cos_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (right_ne_of_oangle_eq_pi_div_two h))]

Premises used: EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two, Real.Angle.cos_coe, EuclideanGeometry.dist_div_cos_angle_of_angle_eq_pi_div_two, EuclideanGeometry.right_ne_of_oangle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one, Or.inr
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
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 : dist p₁ p₂ / (↑(∠ p₃ p₁ p₂) : Real.Angle).cos = dist p₁ p₃
rw₁ : dist p₁ p₂ / (↑(∠ p₂ p₁ p₃) : Real.Angle).cos = dist p₁ p₃
rw₂ : dist p₁ p₂ / Real.cos (∠ p₂ p₁ p₃) = dist p₁ p₃
rw₃ : dist p₁ p₂ / Real.cos (∠ p₂ p₁ p₃) = dist p₃ p₁
rw₄ rw₅ : dist p₃ p₁ = dist p₃ p₁
⊢ dist p₁ p₂ / (∡ p₃ p₁ p₂).cos = dist p₁ p₃

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe, dist_comm p₁ p₃,
    dist_div_cos_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))]

Premises used: EuclideanGeometry.angle_comm, dist_comm, EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two, Real.Angle.cos_coe, EuclideanGeometry.left_ne_of_oangle_eq_pi_div_two, EuclideanGeometry.dist_div_cos_angle_of_angle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one, Or.inr
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
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 : dist p₁ p₂ / (↑(∠ p₂ p₃ p₁) : Real.Angle).sin = dist p₁ p₃
rw₁ : dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃
rw₂ rw₃ : dist p₁ p₃ = dist p₁ p₃
⊢ dist p₁ p₂ / (∡ p₂ p₃ p₁).sin = dist p₁ p₃

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    dist_div_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))]

Premises used: EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.dist_div_sin_angle_of_angle_eq_pi_div_two, Real.Angle.sin_coe, EuclideanGeometry.left_ne_of_oangle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one, Or.inl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
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 : dist p₃ p₂ / (↑(∠ p₃ p₁ p₂) : Real.Angle).sin = dist p₁ p₃
rw₁ : dist p₃ p₂ / (↑(∠ p₂ p₁ p₃) : Real.Angle).sin = dist p₁ p₃
rw₂ : dist p₃ p₂ / Real.sin (∠ p₂ p₁ p₃) = dist p₁ p₃
rw₃ : dist p₃ p₂ / Real.sin (∠ p₂ p₁ p₃) = dist p₃ p₁
rw₄ rw₅ : dist p₃ p₁ = dist p₃ p₁
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).sin = dist p₁ p₃

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe, dist_comm p₁ p₃,
    dist_div_sin_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (right_ne_of_oangle_eq_pi_div_two h))]

Premises used: EuclideanGeometry.angle_comm, dist_comm, EuclideanGeometry.dist_div_sin_angle_of_angle_eq_pi_div_two, EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two, Real.Angle.sin_coe, EuclideanGeometry.right_ne_of_oangle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one, Or.inl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
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 : dist p₁ p₂ / (↑(∠ p₂ p₃ p₁) : Real.Angle).tan = dist p₃ p₂
rw₁ : dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
rw₂ rw₃ : dist p₃ p₂ = dist p₃ p₂
⊢ dist p₁ p₂ / (∡ p₂ p₃ p₁).tan = dist p₃ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    dist_div_tan_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))]

Premises used: EuclideanGeometry.dist_div_tan_angle_of_angle_eq_pi_div_two, EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.left_ne_of_oangle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one, Or.inl, Real.Angle.tan_coe
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
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 : dist p₃ p₂ / (↑(∠ p₃ p₁ p₂) : Real.Angle).tan = dist p₁ p₂
rw₁ : dist p₃ p₂ / (↑(∠ p₂ p₁ p₃) : Real.Angle).tan = dist p₁ p₂
rw₂ : dist p₃ p₂ / Real.tan (∠ p₂ p₁ p₃) = dist p₁ p₂
rw₃ rw₄ : dist p₁ p₂ = dist p₁ p₂
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).tan = dist p₁ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.tan_coe,
    dist_div_tan_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (right_ne_of_oangle_eq_pi_div_two h))]

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.dist_div_tan_angle_of_angle_eq_pi_div_two, EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.right_ne_of_oangle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one, Or.inl, Real.Angle.tan_coe
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Goal:
V : Type u_1
V' : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedAddCommGroup V'
inst_2 : InnerProductSpace ℝ V
inst_3 : InnerProductSpace ℝ V'
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x y : V
simp :
  θ.cos *
        (θ.cos * ⟪x, y⟫ +
          HMul.hMul (β := ℝ) θ.sin ((((o.areaForm : (a : V) → V →ₗ[ℝ] ℝ) x : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) y : ℝ)) +
      θ.sin *
        (HMul.hMul (β := ℝ) θ.cos (-(((o.areaForm : (a : V) → V →ₗ[ℝ] ℝ) x : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) y : ℝ) +
          θ.sin * - -⟪x, y⟫) =
    ⟪x, y⟫
⊢ inner ℝ (E := V)
      ((HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id + θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V) :
            (a : V) → V)
          x :
        V)
      ((HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id + θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V) :
            (a : V) → V)
          y :
        V) =
    ⟪x, y⟫

Tactic:
simp only [RCLike.conj_to_real, id, LinearMap.smul_apply, LinearMap.add_apply,
        LinearMap.id_coe, LinearEquiv.coe_coe, LinearIsometryEquiv.coe_toLinearEquiv,
        Orientation.areaForm_rightAngleRotation_left, Orientation.inner_rightAngleRotation_left,
        Orientation.inner_rightAngleRotation_right, inner_add_left, inner_smul_left,
        inner_add_right, inner_smul_right]

Premises used: LinearMap.smul_apply, LinearMap.id_coe, LinearMap.add_apply, LinearIsometryEquiv.coe_toLinearEquiv, id, inner_add_left, inner_add_right, Orientation.inner_rightAngleRotation_left, inner_smul_right, RCLike.conj_to_real, Orientation.inner_rightAngleRotation_right, Orientation.areaForm_rightAngleRotation_left, LinearEquiv.coe_coe, inner_smul_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Goal:
V : Type u_1
V' : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedAddCommGroup V'
inst_2 : InnerProductSpace ℝ V
inst_3 : InnerProductSpace ℝ V'
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x y : V
⊢ θ.cos *
        (θ.cos * ⟪x, y⟫ +
          HMul.hMul (β := ℝ) θ.sin ((((o.areaForm : (a : V) → V →ₗ[ℝ] ℝ) x : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) y : ℝ)) +
      θ.sin *
        (HMul.hMul (β := ℝ) θ.cos (-(((o.areaForm : (a : V) → V →ₗ[ℝ] ℝ) x : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) y : ℝ) +
          θ.sin * - -⟪x, y⟫) =
    ⟪x, y⟫

Tactic:
linear_combination ⟪x, y⟫ * θ.cos_sq_add_sin_sq

Premises used: Real.Angle.cos_sq_add_sin_sq
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ (o.rotationAux θ : (a : V) → V) x =
    θ.cos • x + HSMul.hSMul (β := V) θ.sin ((o.rightAngleRotation : (a : V) → V) x : V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Goal:
V : Type u_1
V' : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedAddCommGroup V'
inst_2 : InnerProductSpace ℝ V
inst_3 : InnerProductSpace ℝ V'
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
h :
  ∀ (x : V),
    Eq (α := V)
      (((o.rotationAux θ).toLinearMap ∘ₗ
              (HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id -
                θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) :
            (a : V) → V)
          x :
        V)
      ((LinearMap.id : (a : V) → V) x : V)
⊢ (o.rotationAux θ).toLinearMap ∘ₗ
      (HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id - θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) =
    LinearMap.id

Tactic:
ext x
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Goal:
V : Type u_1
V' : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedAddCommGroup V'
inst_2 : InnerProductSpace ℝ V
inst_3 : InnerProductSpace ℝ V'
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ Eq.{u_1 + 1} (α := V) ((fun (t : ℝ) ↦ t • x) (HPow.hPow (β := ℕ) θ.cos 2 + HPow.hPow (β := ℕ) θ.sin 2))
    ((fun (t : ℝ) ↦ t • x) 1)

Tactic:
congr_arg (fun t : ℝ => t • x) θ.cos_sq_add_sin_sq

Premises used: Real.Angle.cos_sq_add_sin_sq, congr_arg, HSMul.hSMul
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Goal:
V : Type u_1
V' : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedAddCommGroup V'
inst_2 : InnerProductSpace ℝ V
inst_3 : InnerProductSpace ℝ V'
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
h :
  ((o.rotationAux θ).toLinearMap ∘ₗ
          (HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id -
            θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) :
        (a : V) → V)
      x =
    (HPow.hPow (β := ℕ) θ.cos 2 + HPow.hPow (β := ℕ) θ.sin 2) • x
h₁ : (LinearMap.id : (a : V) → V) x = HSMul.hSMul (α := ℝ) 1 x
⊢ Eq (α := V)
    (((o.rotationAux θ).toLinearMap ∘ₗ
            (HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id -
              θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) :
          (a : V) → V)
        x :
      V)
    ((LinearMap.id : (a : V) → V) x : V)

Tactic:
convert! congr_arg (fun t : ℝ => t • x) θ.cos_sq_add_sin_sq using 1

Premises used: Real.Angle.cos_sq_add_sin_sq, congr_arg, HSMul.hSMul
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Goal:
V : Type u_1
V' : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedAddCommGroup V'
inst_2 : InnerProductSpace ℝ V
inst_3 : InnerProductSpace ℝ V'
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
h :
  θ.cos • (θ.cos • x - HSMul.hSMul (β := V) θ.sin ((o.rightAngleRotation : (a : V) → V) x : V)) +
      θ.sin • (HSMul.hSMul (β := V) θ.cos ((o.rightAngleRotation : (a : V) → V) x : V) - θ.sin • -x) =
    (HPow.hPow (β := ℕ) θ.cos 2 + HPow.hPow (β := ℕ) θ.sin 2) • x
⊢ ((o.rotationAux θ).toLinearMap ∘ₗ
          (HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id -
            θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) :
        (a : V) → V)
      x =
    (HPow.hPow (β := ℕ) θ.cos 2 + HPow.hPow (β := ℕ) θ.sin 2) • x

Tactic:
simp only [o.rightAngleRotation_rightAngleRotation, o.rotationAux_apply,
          Function.comp_apply, id, LinearEquiv.coe_coe, LinearIsometry.coe_toLinearMap,
          LinearIsometryEquiv.coe_toLinearEquiv, map_smul, map_sub, LinearMap.coe_comp,
          LinearMap.id_coe, LinearMap.smul_apply, LinearMap.sub_apply]

Premises used: LinearIsometry.coe_toLinearMap, map_sub, LinearMap.smul_apply, LinearMap.id_coe, LinearIsometryEquiv.coe_toLinearEquiv, id, Orientation.rightAngleRotation_rightAngleRotation, LinearMap.coe_comp, LinearMap.sub_apply, Function.comp_apply, Orientation.rotationAux_apply, LinearEquiv.coe_coe, map_smul