mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case right
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
hp₁p₂ : p₂ -ᵥ p₁ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ p₃ -ᵥ p₁ = (-r + 1) • (p₂ -ᵥ p₁)

Tactic:
add_smul,

Goal state after:
case right
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
hp₁p₂ : p₂ -ᵥ p₁ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ p₃ -ᵥ p₁ = -r • (p₂ -ᵥ p₁) + 1 • (p₂ -ᵥ p₁)
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₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
left✝ : p₂ -ᵥ p₃ ≠ 0
r : ℝ
hr : r < 0
hpr : p₄ -ᵥ p₃ = r • (p₂ -ᵥ p₃)
⊢ (-r + 1) • (p₃ -ᵥ p₂) = p₄ -ᵥ p₂

Tactic:
add_smul,

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₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
left✝ : p₂ -ᵥ p₃ ≠ 0
r : ℝ
hr : r < 0
hpr : p₄ -ᵥ p₃ = r • (p₂ -ᵥ p₃)
⊢ -r • (p₃ -ᵥ p₂) + 1 • (p₃ -ᵥ p₂) = p₄ -ᵥ p₂
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case neg.inr.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hx : ¬x = 0
hr : 0 < r
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

Tactic:
exact Or.inl (SameRay.sameRay_pos_smul_right x hr)

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

Goal state before:
pp: case neg.mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
H : x ≠ 0 ∧ r • (o.rotation ↑(π / 2)) x ≠ 0
⊢ (∃ r_1, 0 < r_1 ∧ r • (o.rotation ↑(π / 2)) x = r_1 • (o.rotation ↑(π / 2)) x) ∨
    ∃ r_1, 0 < r_1 ∧ r • (o.rotation ↑(π / 2)) x = -r_1 • (o.rotation ↑(π / 2)) x

Tactic:
rcases lt_trichotomy 0 r with (hr0 | rfl | hr0)

Goal state after:
case neg.mpr.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
H : x ≠ 0 ∧ r • (o.rotation ↑(π / 2)) x ≠ 0
hr0 : 0 < r
⊢ (∃ r_1, 0 < r_1 ∧ r • (o.rotation ↑(π / 2)) x = r_1 • (o.rotation ↑(π / 2)) x) ∨
    ∃ r_1, 0 < r_1 ∧ r • (o.rotation ↑(π / 2)) x = -r_1 • (o.rotation ↑(π / 2)) x

case neg.mpr.inr.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
H : x ≠ 0 ∧ 0 • (o.rotation ↑(π / 2)) x ≠ 0
⊢ (∃ r, 0 < r ∧ 0 • (o.rotation ↑(π / 2)) x = r • (o.rotation ↑(π / 2)) x) ∨
    ∃ r, 0 < r ∧ 0 • (o.rotation ↑(π / 2)) x = -r • (o.rotation ↑(π / 2)) x

case neg.mpr.inr.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
H : x ≠ 0 ∧ r • (o.rotation ↑(π / 2)) x ≠ 0
hr0 : r < 0
⊢ (∃ r_1, 0 < r_1 ∧ r • (o.rotation ↑(π / 2)) x = r_1 • (o.rotation ↑(π / 2)) x) ∨
    ∃ r_1, 0 < r_1 ∧ r • (o.rotation ↑(π / 2)) x = -r_1 • (o.rotation ↑(π / 2)) x
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₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
⊢ p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ p₁ - r • (p₃ -ᵥ p₁))

Tactic:
vsub_self,

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
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
⊢ p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (0 - r • (p₃ -ᵥ p₁))
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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle x y + o.oangle y z = o.oangle x z

Tactic:
oangle

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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ ↑((o.kahler x) y).arg + ↑((o.kahler y) z).arg = ↑((o.kahler x) z).arg
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
exact
        Left.add_pos_of_pos_of_nonneg (mul_self_pos.2 (norm_ne_zero_iff.2 h0)) (mul_self_nonneg _)

Goal state after:
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⁻¹ • (r • (p₃ -ᵥ p₁) + (p₁ -ᵥ p₁))

Tactic:
vsub_self,

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
r : ℝ
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃) r ≠ p₁
hr0' : r ≠ 0
hr0 : 0 < r
⊢ p₃ -ᵥ p₁ = r⁻¹ • (r • (p₃ -ᵥ p₁) + 0)
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₂ : p₂ ∉ line[ℝ, p₁, p₃]
h₄ : p₄ ∈ line[ℝ, p₁, p₃]
h₆ : p₆ ∈ line[ℝ, p₁, p₃]
h₁₂₄₅ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₄, p₅]
h₃₂₆₅ : line[ℝ, p₃, p₂] ∥ line[ℝ, p₆, p₅]
⊢ o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ∡ p₄ p₅ p₆

Tactic:
oangle

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₂ ∉ line[ℝ, p₁, p₃]
h₄ : p₄ ∈ line[ℝ, p₁, p₃]
h₆ : p₆ ∈ line[ℝ, p₁, p₃]
h₁₂₄₅ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₄, p₅]
h₃₂₆₅ : line[ℝ, p₃, p₂] ∥ line[ℝ, p₆, p₅]
⊢ o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = o.oangle (p₄ -ᵥ p₅) (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
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ o.oangle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) = ↑π - 2 • ∡ p₁ p₂ p₃

Tactic:
oangle

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
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ o.oangle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) = ↑π - 2 • o.oangle (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 (x + y)).tan = ‖y‖ / ‖x‖

Tactic:
by
  have hs : (o.oangle x (x + y)).sign = 1 := by
    rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
  rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    InnerProductGeometry.tan_angle_add_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]

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)
⊢ (o.oangle (x - y) x).cos = ‖x‖ / ‖x - y‖

Tactic:
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)
⊢ ‖y‖ / (o.oangle y (y - x)).cos = ‖y - x‖

Tactic:
have hs : (o.oangle y (y - x)).sign = 1 := by
    rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
  rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    InnerProductGeometry.norm_div_cos_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.Oriented.Basic

Goal state before:
pp: case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ∃ g, g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
⊢ ∃ g, g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)

Tactic:
rcases h with ⟨m, h, hm⟩
    change m 0 • x + m 1 • y = 0 at h
    refine ⟨![m 0 - m 1 * r, m 1], ?_⟩
    change (m 0 - m 1 * r) • x + m 1 • (r • x + y) = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0)
    rw [sub_smul, smul_add, smul_smul, ← add_assoc, sub_add_cancel]
    refine ⟨h, not_and_or.1 fun h0 => ?_⟩
    obtain ⟨h0, h1⟩ := h0
    rw [h1] at h0 hm
    rw [zero_mul, sub_zero] at h0
    simp [h0] at hm

Goal state after:
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
⊢ (o.oangle x (x - y)).sign = -(o.oangle x y).sign

Tactic:
rw [← o.oangle_sign_smul_sub_right x y 1, one_smul]

Goal state after:
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
⊢ ↑(∠ p₂ p₃ p₁) = ↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃))

Tactic:
angle_eq_arccos_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)

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
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ ↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃)) = ↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃))
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case refine_1
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
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x ↦ (↑x.1, p₅, x.2 +ᵥ ↑x.1)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p ↦ ∡ p.1 p.2.1 p.2.2) s
q : P
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
hq : q ∈ line[ℝ, p₁, p₂]
⊢ q -ᵥ q - r • (p₂ -ᵥ p₁) ≠ 0

Tactic:
vsub_self,

Goal state after:
case refine_1
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
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x ↦ (↑x.1, p₅, x.2 +ᵥ ↑x.1)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p ↦ ∡ p.1 p.2.1 p.2.2) s
q : P
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
hq : q ∈ line[ℝ, p₁, p₂]
⊢ 0 - r • (p₂ -ᵥ p₁) ≠ 0
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ p₁ ∈ Sphere.ofDiameter p₁ p₂

Tactic:
by simp [Sphere.ofDiameter, mem_sphere, inv_mul_eq_div]

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

Goal state before:
pp: case inr
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
h₂ : p₁ ≠ p₂
h : 2 • ∡ p₂ (↑((orthogonalProjection line[ℝ, p₁, p₂]) p)) p = 2 • ∡ p (↑((orthogonalProjection line[ℝ, p₁, p₂]) p)) p₃
h' : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = p₁
hp : p ≠ ↑((orthogonalProjection line[ℝ, p₁, p₂]) p)
hpm : p ∉ line[ℝ, p₁, p₂]
⊢ dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)

Tactic:
rw [two_zsmul_oangle_orthogonalProjection_self _ hpm (right_mem_affineSpan_pair _ _ _)
          (h'.symm ▸ h₂.symm), eq_comm, oangle, Real.Angle.two_zsmul_eq_pi_iff, h'] at h

Goal state after:
case inr
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
h₂ : p₁ ≠ p₂
h : o.oangle (p -ᵥ p₁) (p₃ -ᵥ p₁) = ↑(Real.pi / 2) ∨ o.oangle (p -ᵥ p₁) (p₃ -ᵥ p₁) = ↑(-Real.pi / 2)
h' : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = p₁
hp : p ≠ ↑((orthogonalProjection line[ℝ, p₁, p₂]) p)
hpm : p ∉ line[ℝ, p₁, p₂]
⊢ dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
Module: Mathlib.Geometry.Euclidean.Sphere.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
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : Fin 3 → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
hf0 : f 0 = 0
hfi : Function.Injective f
⊢ False

Tactic:
simp_rw [← hsd 0, hf0, zero_smul, zero_vadd, dist_smul_vadd_eq_dist (p 0) c hv0] at hsd

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 : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : Fin 3 → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hf0 : f 0 = 0
hfi : Function.Injective f
hsd : ∀ (i : Fin 3), f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
⊢ False
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 • (s.center -ᵥ s.center) = q -ᵥ s.center
hp : p = s.center
⊢ p = q ∨ q = s.center

Tactic:
vsub_self,

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 : r • 0 = q -ᵥ s.center
hp : p = s.center
⊢ p = q ∨ q = s.center
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

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
as : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥as
inst✝ : as.direction.HasOrthogonalProjection
⊢ dist s.center ↑((orthogonalProjection as) s.center) = s.radius ↔
    s.IsTangentAt (↑((orthogonalProjection as) s.center)) as

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · refine ⟨?_, orthogonalProjection_mem _, fun p hp ↦ ?_⟩
    · rwa [mem_sphere']
    · rw [mem_orthRadius_iff_inner_left]
      exact orthogonalProjection_vsub_mem_direction_orthogonal as s.center _
        (vsub_orthogonalProjection_mem_direction s.center hp)
  · rw [dist_orthogonalProjection_eq_infDist, h.isTangent.infDist_eq_radius]

Goal state after:
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 : P
hp : dist p s.center = s.radius
p' : P
⊢ p' ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) ↔ p' ∈ {p}

Tactic:
simp only [Set.mem_inter_iff, Metric.mem_sphere, mem_coe', SetLike.mem_coe, Set.mem_singleton_iff]

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 : P
hp : dist p s.center = s.radius
p' : P
⊢ p' ∈ s ∧ p' ∈ s.orthRadius p ↔ p' = p
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case h₁
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₁ p₂ : P
x✝ : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
⊢ ‖p₂ -ᵥ s.center‖ = ‖s.center -ᵥ p₁‖

Tactic:
simp_rw [← dist_eq_norm_vsub, mem_sphere'.1 h₁, mem_sphere.1 h₂]

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

Goal state before:
pp: case inl.inr.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 : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : ¬(ℝ ∙ (p -ᵥ s.center))ᗮ = ⊥
hn : ¬Subsingleton V
hnf : Module.finrank ℝ V ≠ 1
v : V
hvm : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
hv0 : v ≠ 0
⊢ (‖√(s.radius ^ 2 - dist p s.center ^ 2)‖ / ‖v‖ * ‖v‖) ^ 2 = s.radius ^ 2 - dist p s.center ^ 2

Tactic:
div_mul_cancel₀ _ (norm_ne_zero_iff.2 hv0)

Goal state after:
case inl.inr.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 : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : ¬(ℝ ∙ (p -ᵥ s.center))ᗮ = ⊥
hn : ¬Subsingleton V
hnf : Module.finrank ℝ V ≠ 1
v : V
hvm : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
hv0 : v ≠ 0
⊢ ‖√(s.radius ^ 2 - dist p s.center ^ 2)‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

Goal state before:
pp: case refine_1
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₃
hd :
  dist (incenter t) ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t ∅)) =
    dist (incenter t) ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t ∅))
⊢ t.points i₁ ∈ Set.range (faceOpposite t i₃).points

Tactic:
simp
    grind

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

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
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₃
hd :
  dist (incenter t) ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t ∅)) =
    dist (incenter t) ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t ∅))
⊢ t.points i₁ ∈ Set.range (faceOpposite t i₂).points

Tactic:
simp
    grind

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

Goal state before:
pp: case refine_1
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₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t {i₁}))
⊢ t.points i₁ ∈ Set.range (faceOpposite t i₃).points

Tactic:
simp
    grind

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

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
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₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t {i₁}))
⊢ t.points i₁ ∈ Set.range (faceOpposite t i₂).points

Tactic:
simp
    grind

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

Goal state before:
pp: case refine_1
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₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points))) (excenter t {i₁}))
⊢ t.points i₂ ∈ Set.range (faceOpposite t i₃).points

Tactic:
simp
    grind

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

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
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₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points))) (excenter t {i₁}))
⊢ t.points i₂ ∈ Set.range (faceOpposite t i₁).points

Tactic:
simp
    grind

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ : V
hy✝ : y✝ ≠ 0
hx✝ : x✝ ≠ 0
hxy : x✝ ≠ y✝
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)

Tactic:
simp [field, mul_assoc, sin_angle_mul_norm_mul_norm]

Goal state after: