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

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
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
h : dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
hc : Collinear ℝ {p', ↑((orthogonalProjection s₁) p), ↑((orthogonalProjection s₂) p)}
h₁ : ↑((orthogonalProjection s₁) p) ∈ line[ℝ, p', ↑((orthogonalProjection s₂) p)]
h₁' : ↑((orthogonalProjection s₁) p) ∈ s₁ ⊓ s₂
h₁'' : ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection (s₁ ⊓ s₂)) p)
h₂ : ↑((orthogonalProjection s₂) p) ∈ line[ℝ, p', ↑((orthogonalProjection s₁) p)]
h₂' : ↑((orthogonalProjection s₂) p) ∈ s₁ ⊓ s₂
h₂'' : ↑((orthogonalProjection s₂) p) = ↑((orthogonalProjection (s₁ ⊓ s₂)) p)
⊢ ↑((orthogonalProjection (s₁ ⊓ s₂)) p) = ↑((orthogonalProjection s₂) p)

Tactic:
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
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
h : dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
hc : Collinear ℝ {p', ↑((orthogonalProjection s₁) p), ↑((orthogonalProjection s₂) p)}
h₁ : ↑((orthogonalProjection s₁) p) ∈ line[ℝ, p', ↑((orthogonalProjection s₂) p)]
h₁' : ↑((orthogonalProjection s₁) p) ∈ s₁ ⊓ s₂
h₁'' : ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection (s₁ ⊓ s₂)) p)
h₂ : ↑((orthogonalProjection s₂) p) ∈ line[ℝ, p', ↑((orthogonalProjection s₁) p)]
h₂' : ↑((orthogonalProjection s₂) p) ∈ s₁ ⊓ s₂
h₂'' : ↑((orthogonalProjection s₂) p) = ↑((orthogonalProjection (s₁ ⊓ s₂)) p)
⊢ ↑((orthogonalProjection (s₁ ⊓ s₂)) p) = ↑((orthogonalProjection (s₁ ⊓ s₂)) p)
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

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
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
h₂ : p₁ ≠ p₂
h : 2 • ∡ p₂ p₁ p = 2 • ∡ p p₁ p₃
h' : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = p₁
⊢ dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)

Tactic:
obtain rfl | hp := eq_or_ne p p₁

Goal state after:
case inl
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
h₂ : p ≠ p₂
h : 2 • ∡ p₂ p p = 2 • ∡ p p p₃
h' : ↑((orthogonalProjection line[ℝ, p, p₂]) p) = p
⊢ dist p ↑((orthogonalProjection line[ℝ, p, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p, p₃]) p)

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₂ p₁ p = 2 • ∡ p p₁ p₃
h' : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = p₁
hp : p ≠ p₁
⊢ dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

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
s : Sphere P
p q : P
h : s.orthRadius p ≤ s.orthRadius q
h' : (ℝ ∙ (p -ᵥ s.center))ᗮ ≤ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
hp : ⟪p -ᵥ s.center, r • (p -ᵥ s.center)⟫ - r * ⟪p -ᵥ s.center, r • (p -ᵥ s.center)⟫ = 0
⊢ p = q ∨ q = s.center

Tactic:
real_inner_smul_right,

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
s : Sphere P
p q : P
h : s.orthRadius p ≤ s.orthRadius q
h' : (ℝ ∙ (p -ᵥ s.center))ᗮ ≤ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
hp : r * ⟪p -ᵥ s.center, p -ᵥ s.center⟫ - r * (r * ⟪p -ᵥ s.center, p -ᵥ s.center⟫) = 0
⊢ p = q ∨ q = 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 : Sphere P
as : AffineSubspace ℝ P
⊢ s.radius = 0 ∧ s.center ∈ as → s.IsTangentAt s.center as

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

Goal state after:
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 : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
⊢ 0 ≤ ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫

Tactic:
rcases inner_pos_or_eq_of_dist_le_radius hp₁ hp₂ with (h | rfl)

Goal state after:
case inl
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
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
⊢ 0 ≤ ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫

case 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
hp₁ : p₁ ∈ s
hp₂ : dist p₁ s.center ≤ s.radius
⊢ 0 ≤ ⟪p₁ -ᵥ p₁, p₁ -ᵥ s.center⟫
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case inr.refine_1
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
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
h : s.center ∈ line[ℝ, p₁, p₂]
⊢ Collinear ℝ {p₁, s.center, p₂}

pp: case inr.refine_2
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
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
h : s.center ∈ line[ℝ, p₁, p₂]
⊢ dist s.center s.center ≤ s.radius

Tactic:
· rw [Set.insert_comm]; exact collinear_insert_of_mem_affineSpan_pair h

Goal state after:
case inr.refine_2
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
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
h : s.center ∈ line[ℝ, p₁, p₂]
⊢ dist s.center s.center ≤ s.radius
Module: Mathlib.Geometry.Euclidean.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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
⊢ (s.height i)⁻¹ ≠ 0

Tactic:
· simp [(s.height_pos i).ne']

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

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
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
⊢ 2 • o.oangle (-(x - y)) (-(x - z)) = 2 • o.oangle (y - x) (z - x)

Tactic:
neg_sub,

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
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
⊢ 2 • o.oangle (y - x) (-(x - z)) = 2 • o.oangle (y - x) (z - x)
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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
⊢ ∑ i, (s.height i)⁻¹ ^ 2 • (s.points i -ᵥ s.altitudeFoot i) = 0

Tactic:
suffices ∀ i, i ≠ 0 →
      ∑ j, ⟪s.points i -ᵥ s.points 0, (s.height j)⁻¹ ^ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫ = 0 by
    rw [← Submodule.mem_bot ℝ,
      ← Submodule.inf_orthogonal_eq_bot (vectorSpan ℝ (Set.range s.points))]
    refine ⟨Submodule.sum_smul_mem _ _ fun i hi ↦
              vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan
                (mem_affineSpan _ (Set.mem_range_self _))
                (altitudeFoot_mem_affineSpan  _ _),
            ?_⟩
    rw [vectorSpan_range_eq_span_range_vsub_right_ne _ _ 0, Submodule.span_range_eq_iSup,
      ← Submodule.iInf_orthogonal, Submodule.coe_iInf, Set.mem_iInter]
    intro i
    rcases i with ⟨i, hi⟩
    simpa only [SetLike.mem_coe, Submodule.mem_orthogonal_singleton_iff_inner_right, inner_sum]
      using this i hi
  intro i hi
  rw [← Finset.add_sum_erase _ _ (Finset.mem_univ 0),
    ← Finset.add_sum_erase _ _ (Finset.mem_erase.2 ⟨hi, Finset.mem_univ _⟩), ← add_assoc]
  convert! add_zero _
  · convert! Finset.sum_const_zero with j hj
    rw [real_inner_smul_right]
    convert! mul_zero _
    rw [← Submodule.mem_orthogonal_singleton_iff_inner_right]
    refine SetLike.le_def.1 (Submodule.orthogonal_le ?_)
      (vsub_orthogonalProjection_mem_direction_orthogonal _ _)
    rw [Submodule.span_singleton_le_iff_mem, direction_affineSpan]
    simp only [Finset.mem_erase, Finset.mem_univ, and_true] at hj
    refine vsub_mem_vectorSpan _ ?_ ?_ <;>
      simp only [range_faceOpposite_points, Set.mem_image]
    · exact ⟨i, hj.1.symm, rfl⟩
    · exact ⟨0, hj.2.symm, rfl⟩
  · rw [inner_smul_right, inner_smul_right, inner_vsub_vsub_altitudeFoot_eq_height_sq _ hi,
      ← neg_vsub_eq_vsub_rev, inner_neg_left, inner_vsub_vsub_altitudeFoot_eq_height_sq _ hi.symm,
      mul_neg, inv_pow]
    simp [height]

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ (s.height i)⁻¹ -
      ∑ x with x ≠ i,
        -(⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ / (s.height i * s.height x) *
            (s.height x)⁻¹) =
    0

Tactic:
rw [Finset.sum_neg_distrib, sub_neg_eq_add, Finset.filter_ne',
    Finset.sum_erase_eq_sub (Finset.mem_univ _), real_inner_self_eq_norm_mul_norm,
    ← dist_eq_norm_vsub]

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ (s.height i)⁻¹ +
      (∑ x,
          ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ / (s.height i * s.height x) *
            (s.height x)⁻¹ -
        dist (s.points i) (s.altitudeFoot i) * dist (s.points i) (s.altitudeFoot i) / (s.height i * s.height i) *
          (s.height i)⁻¹) =
    0
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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
h :
  ∑ i_1,
      (dist (s.points i) (s.altitudeFoot i))⁻¹ *
        ((dist (s.points i_1) (s.altitudeFoot i_1))⁻¹ ^ 2 *
          ⟪s.points i -ᵥ s.altitudeFoot i, s.points i_1 -ᵥ s.altitudeFoot i_1⟫) =
    0
⊢ ∑ x,
      ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ /
          (dist (s.points i) (s.altitudeFoot i) * dist (s.points x) (s.altitudeFoot x)) *
        (dist (s.points x) (s.altitudeFoot x))⁻¹ =
    0

Tactic:
convert! h using 2 with j

Goal state after:
case a
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
h :
  ∑ i_1,
      (dist (s.points i) (s.altitudeFoot i))⁻¹ *
        ((dist (s.points i_1) (s.altitudeFoot i_1))⁻¹ ^ 2 *
          ⟪s.points i -ᵥ s.altitudeFoot i, s.points i_1 -ᵥ s.altitudeFoot i_1⟫) =
    0
j : Fin (n + 1)
a✝ : j ∈ Finset.univ
⊢ ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ /
        (dist (s.points i) (s.altitudeFoot i) * dist (s.points j) (s.altitudeFoot j)) *
      (dist (s.points j) (s.altitudeFoot j))⁻¹ =
    (dist (s.points i) (s.altitudeFoot i))⁻¹ *
      ((dist (s.points j) (s.altitudeFoot j))⁻¹ ^ 2 * ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫)
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
n : ℕ
inst✝¹ : NeZero n
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
h : j ∈ {k | k ≠ i}
⊢ s.excenterWeightsUnnorm {i} j = (s.height j)⁻¹

Tactic:
· rw [Finset.mem_filter_univ] at h
    simp [excenterWeightsUnnorm, h]

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
h : ‖x‖ = ‖y‖
⊢ ⟪x, -(y - x)⟫ / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)

Tactic:
neg_sub,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ = ‖y‖
⊢ ⟪x, x - y⟫ / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
r : ℝ
hr : r • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center
⊢ ((«o».oangle (midpoint ℝ p₁ p₂ -ᵥ p₁) (r • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) + (midpoint ℝ p₁ p₂ -ᵥ p₁))).tan / 2) •
        («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ
      midpoint ℝ p₁ p₂ =
    r • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂

Tactic:
nth_rw 1 [show p₂ -ᵥ p₁ = (2 : ℝ) • (midpoint ℝ p₁ p₂ -ᵥ p₁) by simp]

Goal state after:
V : Type u_3
P : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
r : ℝ
hr : r • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center
⊢ ((«o».oangle (midpoint ℝ p₁ p₂ -ᵥ p₁)
              (r • («o».rotation ↑(π / 2)) (2 • (midpoint ℝ p₁ p₂ -ᵥ p₁)) + (midpoint ℝ p₁ p₂ -ᵥ p₁))).tan /
          2) •
        («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ
      midpoint ℝ p₁ p₂ =
    r • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖-(y - x)‖)
hxy : ¬x = y
⊢ ‖x‖ = ‖y‖

Tactic:
neg_sub,

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖x - y‖)
hxy : ¬x = y
⊢ ‖x‖ = ‖y‖
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ = 0
hx0 : ¬x = 0
hy0 : y = 0
⊢ ‖x‖ = ‖y‖

Tactic:
rw [hy0, norm_zero, h]

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

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
a b c p x : P
hx : Sbtw ℝ a x c
hxb : SameRay ℝ (x -ᵥ p) (b -ᵥ p)
hb : b ≠ p
hpx : p ≠ x
r : ℝ
hr : 0 < r
hrb : r • (x -ᵥ p) = b -ᵥ p
hab : ∠ a p b = ∠ a p x
hbc : ∠ b p c = ∠ x p c
⊢ ∠ a p x + ∠ b p c = ∠ a p c

Tactic:
hbc

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
a b c p x : P
hx : Sbtw ℝ a x c
hxb : SameRay ℝ (x -ᵥ p) (b -ᵥ p)
hb : b ≠ p
hpx : p ≠ x
r : ℝ
hr : 0 < r
hrb : r • (x -ᵥ p) = b -ᵥ p
hab : ∠ a p b = ∠ a p x
hbc : ∠ b p c = ∠ x p c
⊢ ∠ a p x + ∠ x p c = ∠ a p c
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 0 ≤ 1 - ⟪x, ⟪y, x⟫ • y⟫

Tactic:
real_inner_smul_right,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 0 ≤ 1 - ⟪y, x⟫ * ⟪x, y⟫
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ⟪x, ‖ortho y x‖⁻¹ • ortho y x⟫ ^ 2 + ⟪x, y⟫ ^ 2 = 1

Tactic:
real_inner_smul_right,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ (‖ortho y x‖⁻¹ * ⟪x, ortho y x⟫) ^ 2 + ⟪x, y⟫ ^ 2 = 1
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H1 : ‖x - ⟪y, x⟫ • y‖ ≠ 0
⊢ (1 - ⟪y, x⟫ * ⟪x, y⟫) ^ 2 + (⟪x, x⟫ - ⟪x, ⟪y, x⟫ • y⟫ - (⟪⟪y, x⟫ • y, x⟫ - ⟪⟪y, x⟫ • y, ⟪y, x⟫ • y⟫)) * ⟪x, y⟫ ^ 2 =
    ⟪x, x⟫ - ⟪x, ⟪y, x⟫ • y⟫ - (⟪⟪y, x⟫ • y, x⟫ - ⟪⟪y, x⟫ • y, ⟪y, x⟫ • y⟫)

Tactic:
real_inner_smul_right,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H1 : ‖x - ⟪y, x⟫ • y‖ ≠ 0
⊢ (1 - ⟪y, x⟫ * ⟪x, y⟫) ^ 2 + (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫ - (⟪⟪y, x⟫ • y, x⟫ - ⟪⟪y, x⟫ • y, ⟪y, x⟫ • y⟫)) * ⟪x, y⟫ ^ 2 =
    ⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫ - (⟪⟪y, x⟫ • y, x⟫ - ⟪⟪y, x⟫ • y, ⟪y, x⟫ • y⟫)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H1 : ‖x - ⟪y, x⟫ • y‖ ≠ 0
⊢ (1 - ⟪y, x⟫ * ⟪x, y⟫) ^ 2 + (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫ - (⟪y, x⟫ * ⟪y, x⟫ - ⟪⟪y, x⟫ • y, ⟪y, x⟫ • y⟫)) * ⟪x, y⟫ ^ 2 =
    ⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫ - (⟪y, x⟫ * ⟪y, x⟫ - ⟪⟪y, x⟫ • y, ⟪y, x⟫ • y⟫)

Tactic:
real_inner_smul_right,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H1 : ‖x - ⟪y, x⟫ • y‖ ≠ 0
⊢ (1 - ⟪y, x⟫ * ⟪x, y⟫) ^ 2 + (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫ - (⟪y, x⟫ * ⟪y, x⟫ - ⟪y, x⟫ * ⟪⟪y, x⟫ • y, y⟫)) * ⟪x, y⟫ ^ 2 =
    ⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫ - (⟪y, x⟫ * ⟪y, x⟫ - ⟪y, x⟫ * ⟪⟪y, x⟫ • y, y⟫)
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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
⊢ (∃ r, ∀ (i : Fin (n + 1)), (s.signedInfDist i) p = r) ↔ p = s.incenter

Tactic:
convert! s.exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter hp (signs := ∅)
  · simp
  · simp [excenterExists_empty]

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

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ x = ⟪x, y⟫ • y + ⟪x, ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)⟫ • ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)

Tactic:
real_inner_smul_right,

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ x = ⟪x, y⟫ • y + (‖x - ⟪y, x⟫ • y‖⁻¹ * ⟪x, x - ⟪y, x⟫ • y⟫) • ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ x = ⟪x, y⟫ • y + (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪x, ⟪y, x⟫ • y⟫)) • ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)

Tactic:
real_inner_smul_right,

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ x = ⟪x, y⟫ • y + (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) • ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - ⟪x, y⟫ ^ 2 ≠ 0
⊢ 1 - ⟪x, ⟪x, y⟫ • y⟫ - (⟪⟪x, y⟫ • y, x⟫ - ⟪⟪x, y⟫ • y, ⟪x, y⟫ • y⟫) = 1 - ⟪x, y⟫ ^ 2

Tactic:
real_inner_smul_right,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - ⟪x, y⟫ ^ 2 ≠ 0
⊢ 1 - ⟪x, y⟫ * ⟪x, y⟫ - (⟪⟪x, y⟫ • y, x⟫ - ⟪⟪x, y⟫ • y, ⟪x, y⟫ • y⟫) = 1 - ⟪x, y⟫ ^ 2
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - ⟪x, y⟫ ^ 2 ≠ 0
⊢ 1 - ⟪x, y⟫ ^ 2 - (⟪x, y⟫ * ⟪y, x⟫ - ⟪x, y⟫ * ⟪y, ⟪x, y⟫ • y⟫) = 1 - ⟪x, y⟫ ^ 2

Tactic:
real_inner_smul_right,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - ⟪x, y⟫ ^ 2 ≠ 0
⊢ 1 - ⟪x, y⟫ ^ 2 - (⟪x, y⟫ * ⟪y, x⟫ - ⟪x, y⟫ * (⟪x, y⟫ * ⟪y, y⟫)) = 1 - ⟪x, y⟫ ^ 2
Module: Mathlib.Geometry.Euclidean.Triangle

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₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
by_cases h : p₂ = p₁
  · rw [h, angle_self_left]
    linarith [Real.pi_pos]
  · rcases hne with hne | hne | hne <;>
      rcases hne.lt_or_gt with hne | hne <;>
      linarith [angle_add_angle_add_angle_eq_pi p₃ h]

Goal state after: