mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hn : x ≠ y
h : ‖x‖ = ‖y‖
⊢ o.oangle y x = ↑π - (o.oangle (y - x) y + o.oangle (y - x) y)

Tactic:
← o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hn : x ≠ y
h : ‖x‖ = ‖y‖
⊢ o.oangle y x = ↑π - (o.oangle x (x - y) + o.oangle (y - x) y)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x = 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1

Tactic:
div_lt_one (Real.sqrt_pos.2 (Left.add_pos_of_pos_of_nonneg (mul_self_pos.2
    (norm_ne_zero_iff.2 hx)) (mul_self_nonneg _))),

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x = 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ ‖x‖ < √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₃ : P
r : ℝ
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃) r ≠ p₁
hr0' : r ≠ 0
hr0 : 0 < r
⊢ p₃ -ᵥ p₁ = r⁻¹ • ((AffineMap.lineMap p₁ p₃) r -ᵥ p₁)

Tactic:
rw [AffineMap.lineMap_apply, vadd_vsub_assoc, vsub_self, add_zero, smul_smul,
    inv_mul_cancel₀ hr0', one_smul]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : vectorSpan ℝ {p₁, p₂} = vectorSpan ℝ {p₄, p₅}
h₃₂₆₅ : vectorSpan ℝ {p₃, p₂} = vectorSpan ℝ {p₆, p₅}
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆

Tactic:
vectorSpan_pair

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : ℝ ∙ (p₁ -ᵥ p₂) = ℝ ∙ (p₄ -ᵥ p₅)
h₃₂₆₅ : ℝ ∙ (p₃ -ᵥ p₂) = ℝ ∙ (p₆ -ᵥ p₅)
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case e'_3
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ↑π - 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ↑π - 2 • o.oangle (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃)

Tactic:
← o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h

Goal state after:
case e'_3
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ↑π - 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ↑π - 2 • o.oangle (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃))
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arccos (dist p₃ p₂ / dist p₁ p₃)

Tactic:
dist_eq_norm_vsub' V p₃ p₂,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arccos (‖p₂ -ᵥ p₃‖ / dist p₁ p₃)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : dist p₁ p₂ = dist p₁ p₃
⊢ |(∡ p₁ p₂ p₃).toReal| < π / 2

Tactic:
by
  simp_rw [dist_eq_norm_vsub V] at h
  rw [oangle, ← vsub_sub_vsub_cancel_left p₃ p₂ p₁]
  exact o.abs_oangle_sub_right_toReal_lt_pi_div_two h

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arctan (‖p₁ -ᵥ p₂‖ / dist p₃ p₂)

Tactic:
dist_eq_norm_vsub' V p₃ p₂,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arctan (‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃‖)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
⊢ Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = dist p₃ p₂ / dist p₁ p₃

Tactic:
dist_eq_norm_vsub' V p₃ p₂,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
⊢ Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = ‖p₂ -ᵥ p₃‖ / dist p₁ p₃
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x + y) y).tan * ‖y‖ = ‖x‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
  rw [add_comm]
  exact (-o).tan_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two h

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
⊢ Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = ‖p₁ -ᵥ p₂‖ / dist p₃ p₂

Tactic:
dist_eq_norm_vsub' V p₃ p₂,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
⊢ Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = ‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃‖
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x - y) x).cos = ‖x‖ / ‖x - y‖

Tactic:
by
  rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
  exact (-o).cos_oangle_sub_right_of_oangle_eq_pi_div_two h

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ (o.oangle y (y - x)).sin = ‖x‖ / ‖y - x‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    InnerProductGeometry.sin_angle_sub_of_inner_eq_zero
      (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inl (o.right_ne_zero_of_oangle_eq_pi_div_two h))]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
⊢ Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * dist p₁ p₃ = dist p₃ p₂

Tactic:
dist_eq_norm_vsub' V p₃ p₂,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
⊢ Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * dist p₁ p₃ = ‖p₂ -ᵥ p₃‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0
⊢ Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * dist p₃ p₂ = ‖p₁ -ᵥ p₂‖

Tactic:
dist_eq_norm_vsub' V p₃ p₂,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0
⊢ Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * ‖p₂ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0
⊢ dist p₃ p₂ / Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = dist p₁ p₃

Tactic:
dist_eq_norm_vsub' V p₃ p₂,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0
⊢ ‖p₂ -ᵥ p₃‖ / Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = dist p₁ p₃
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case neg.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁ p₂ p₁'
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃

pp: case neg.inr.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₂ p₁' p₁
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃

pp: case neg.inr.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁' p₁ p₂
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃

Tactic:
· have hw' : Sbtw ℝ p₁ p₂ p₁' := ⟨hw, hp₁p₂.symm, hp₁'p₂.symm⟩
    rw [hw'.oangle_eq_add_pi_left hp₃p₂, smul_add, Real.Angle.two_zsmul_coe_pi, add_zero]

Goal state after:
case neg.inr.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₂ p₁' p₁
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃

case neg.inr.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁' p₁ p₂
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ ‖p₁ -ᵥ p₂‖ / Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = dist p₃ p₂

Tactic:
dist_eq_norm_vsub' V p₃ p₂,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ ‖p₁ -ᵥ p₂‖ / Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = ‖p₂ -ᵥ p₃‖
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ 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))]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : ∑ i ∈ s, w₁ i = 1
h₂ : ∑ i ∈ s, w₂ i = 1
⊢ dist ((Finset.affineCombination ℝ s p) w₁) ((Finset.affineCombination ℝ s p) w₂) *
      dist ((Finset.affineCombination ℝ s p) w₁) ((Finset.affineCombination ℝ s p) w₂) =
    (-∑ i₁ ∈ s, ∑ i₂ ∈ s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2

Tactic:
dist_eq_norm_vsub V (s.affineCombination ℝ p w₁) (s.affineCombination ℝ p w₂),

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : ∑ i ∈ s, w₁ i = 1
h₂ : ∑ i ∈ s, w₂ i = 1
⊢ ‖(Finset.affineCombination ℝ s p) w₁ -ᵥ (Finset.affineCombination ℝ s p) w₂‖ *
      ‖(Finset.affineCombination ℝ s p) w₁ -ᵥ (Finset.affineCombination ℝ s p) w₂‖ =
    (-∑ i₁ ∈ s, ∑ i₂ ∈ s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: P : Type u_2
inst✝ : MetricSpace P
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ dist s.center p₁ = dist s.center p₂

Tactic:
rw [mem_sphere'.1 hp₁, mem_sphere'.1 hp₂]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h : dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
ho : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
⊢ p = p₁

Tactic:
have hs := orthogonalProjection_sup_of_orthogonalProjection_eq ho

Goal state after:
case pos
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h : dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
ho : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
hs : ↑((orthogonalProjection (line[ℝ, p₁, p₂] ⊔ line[ℝ, p₁, p₃])) p) = ↑((orthogonalProjection line[ℝ, p₁, p₂]) p)
⊢ p = p₁
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: case refine_1.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p q : P
h : s.orthRadius p ≤ s.orthRadius q
h' : (ℝ ∙ (p -ᵥ s.center))ᗮ ≤ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • 0 = q -ᵥ s.center
hp : p = s.center
⊢ p = q ∨ q = s.center

Tactic:
smul_zero,

Goal state after:
case refine_1.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p q : P
h : s.orthRadius p ≤ s.orthRadius q
h' : (ℝ ∙ (p -ᵥ s.center))ᗮ ≤ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : 0 = q -ᵥ s.center
hp : p = s.center
⊢ p = q ∨ q = s.center
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p q : P
⊢ (∃ z, z • (p -ᵥ s.center) = q -ᵥ s.center) ∧
      (¬(↑(mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ)).Nonempty ↔ ¬(↑(mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ)).Nonempty) ↔
    ∃ r, r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)

Tactic:
mk'_nonempty,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p q : P
⊢ (∃ z, z • (p -ᵥ s.center) = q -ᵥ s.center) ∧ True ↔ ∃ r, r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
⊢ s₁.radius = 0 ∧ s₁.center ∈ s₂ → s₁.IsExtTangentAt s₂ s₁.center

Tactic:
rintro ⟨hr, hc⟩
    refine ⟨?_, hc, ?_⟩
    · rw [center_mem_iff, hr]
    · simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
⊢ s₁.radius = 0 ∧ s₁.center ∈ s₂ → s₁.IsIntTangentAt s₂ s₁.center

Tactic:
rintro ⟨hr, hc⟩
    refine ⟨?_, hc, ?_⟩
    · rw [center_mem_iff, hr]
    · simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∡ (t.points i₂) (t.points i₁) (incenter t) = ∡ (incenter t) (t.points i₁) (t.points i₃)

Tactic:
rw [← (t.sbtw_touchpoint_empty h₁₃ h₁₂ h₂₃.symm).oangle_eq_left,
    ← (t.sbtw_touchpoint_empty h₁₂ h₁₃ h₂₃).oangle_eq_right]

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∡ (touchpoint t ∅ i₃) (t.points i₁) (incenter t) = ∡ (incenter t) (t.points i₁) (touchpoint t ∅ i₂)
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
h : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
⊢ s₁.IsExtTangent s₂

Tactic:
refine ⟨AffineMap.lineMap s₁.center s₂.center (s₁.radius / (s₁.radius + s₂.radius)), ?_⟩

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
h : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
⊢ s₁.IsExtTangentAt s₂ ((AffineMap.lineMap s₁.center s₂.center) (s₁.radius / (s₁.radius + s₂.radius)))
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∡ (t.points i₂) (t.points i₁) (excenter t {i₁}) = ∡ (excenter t {i₁}) (t.points i₁) (t.points i₃)

Tactic:
(t.touchpoint_singleton_sbtw h₁₃ h₁₂ h₂₃.symm).symm.oangle_eq_left,

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∡ (touchpoint t {i₁} i₃) (t.points i₁) (excenter t {i₁}) = ∡ (excenter t {i₁}) (t.points i₁) (t.points i₃)
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
h₁ : dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₂).orthogonalProjectionSpan p)
h₂ : dist p ↑((faceOpposite t i₁).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p)
hp : p ∈ affineSpan ℝ (Set.range t.points)
i : Fin (2 + 1)
h : i = i₁ ∨ i = i₂ ∨ i = i₃
⊢ dist p ↑((faceOpposite t i).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p)

Tactic:
rcases h with rfl | rfl | rfl <;> grind

Goal state after:
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
⊢ (s.reindex e).excenterWeightsUnnorm signs = s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) ∘ ⇑e.symm

Tactic:
ext i
  simp [excenterWeightsUnnorm]

Goal state after: