mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ s.exsphere ∅ᶜ = s.insphere

Tactic:
exsphere_compl,

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
⊢ s.exsphere ∅ = s.insphere
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
⊢ Real.cos (angle x y) = Real.cos (angle x (x + y) + angle y (y + x))

Tactic:
Real.cos_add,

Goal state after:
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
⊢ Real.cos (angle x y) =
    Real.cos (angle x (x + y)) * Real.cos (angle y (y + x)) - Real.sin (angle x (x + y)) * Real.sin (angle y (y + x))
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
⊢ Real.cos (angle x y) = Real.cos (angle x (x + y) + angle y (y + x))

Tactic:
rw [Real.cos_add, cos_angle, cos_angle, cos_angle, sin_angle_add hx (by grind),
      sin_angle_add hy (by grind), mul_comm ⟪y, y⟫ ⟪x, x⟫, real_inner_comm x y, add_comm y x]
    have : x + y ≠ 0 := by grind
    simp only [field] -- non-recursive `field_simp`
    rw [Real.sq_sqrt (sub_nonneg_of_le (real_inner_mul_inner_self_le x y))]
    simp only [← real_inner_self_eq_norm_sq, inner_add_right, inner_add_left, real_inner_comm]
    ring

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

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
hne : Nonempty ι
inst✝ : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
⊢ ∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius

Tactic:
by
  cases nonempty_fintype ι
  induction hn : Fintype.card ι generalizing ι with
  | zero =>
    exfalso
    have h := Fintype.card_pos_iff.2 hne
    lia
  | succ m hm =>
    rcases m with - | m
    · rw [Fintype.card_eq_one_iff] at hn
      obtain ⟨i, hi⟩ := hn
      have : Unique ι := ⟨⟨i⟩, hi⟩
      use ⟨p i, 0⟩
      simp only [Set.range_unique, AffineSubspace.mem_affineSpan_singleton]
      constructor
      · simp_rw [hi default, Set.singleton_subset_iff]
        exact ⟨⟨⟩, by simp only [Metric.sphere_zero, Set.mem_singleton_iff]⟩
      · rintro ⟨cc, cr⟩
        rintro ⟨rfl, hdist⟩
        replace hdist : 0 = cr := by simpa using hdist
        rw [hi default, hdist]
    · have i := hne.some
      let ι2 := { x // x ≠ i }
      classical
      have hc : Fintype.card ι2 = m + 1 := by
        rw [Fintype.card_of_subtype {x | x ≠ i}]
        · rw [Finset.filter_not, Finset.filter_eq' _ i, if_pos (Finset.mem_univ _),
            Finset.card_sdiff, Finset.card_univ, hn]
          simp
        · simp
      have : Nonempty ι2 := Fintype.card_pos_iff.1 (hc.symm ▸ Nat.zero_lt_succ _)
      have ha2 : AffineIndependent ℝ fun i2 : ι2 => p i2 := ha.subtype _
      replace hm := hm ha2 _ hc
      have hr : Set.range p = insert (p i) (Set.range fun i2 : ι2 => p i2) := by
        change _ = insert _ (Set.range fun i2 : { x | x ≠ i } => p i2)
        rw [← Set.image_eq_range, ← Set.image_univ, ← Set.image_insert_eq]
        congr with j
        simp [Classical.em]
      rw [hr, ← affineSpan_insert_affineSpan]
      refine existsUnique_dist_eq_of_insert (Set.range_nonempty _) (subset_affineSpan ℝ _) ?_ hm
      convert! ha.notMem_affineSpan_sdiff i Set.univ
      change (Set.range fun i2 : { x | x ≠ i } => p i2) = _
      rw [← Set.image_eq_range]
      congr 1 with j
      simp

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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
h : i ≠ j
⊢ 0 < s.excenterWeights {j} i

Tactic:
← sign_eq_one_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
n : ℕ
inst✝¹ : NeZero n
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
h : i ≠ j
⊢ SignType.sign (s.excenterWeights {j} i) = 1
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 : P
h : Sbtw ℝ p p₁ p₂
⊢ ∠ p₃ p₁ p = ∠ p₁ p₃ p₂ + ∠ p₃ p₂ p₁

Tactic:
by
  linarith [angle_add_angle_eq_pi_of_angle_eq_pi p₃ h.angle₁₂₃_eq_pi,
    angle_add_angle_add_angle_eq_pi p₃ h.right_ne.symm, angle_comm p₃ p₁ p₂]

Goal state after:
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 : |⟪y, x⟫| * 1 = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H2 : x = ⟪y, x⟫ • y
⊢ False

Tactic:
mul_one

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : |⟪y, x⟫| = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H2 : x = ⟪y, x⟫ • y
⊢ False
Module: Mathlib.Geometry.Euclidean.Circumcenter

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 : ℕ
s : Simplex ℝ P n
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ i,
        (centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n +
                centroidWeightsWithCircumcenter {i₁, i₂} -
              reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
            (pointIndex i) •
          (s.pointsWithCircumcenter (pointIndex i) -ᵥ Classical.choice ⋯) +
      (centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n +
              centroidWeightsWithCircumcenter {i₁, i₂} -
            reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
          circumcenterIndex •
        (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) =
    0

Tactic:
Pi.sub_apply,

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 : ℕ
s : Simplex ℝ P n
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ x,
        ((centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n +
                centroidWeightsWithCircumcenter {i₁, i₂})
              (pointIndex x) -
            reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ (pointIndex x)) •
          (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) +
      ((centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n +
              centroidWeightsWithCircumcenter {i₁, i₂})
            circumcenterIndex -
          reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ circumcenterIndex) •
        (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) =
    0
Module: Mathlib.Geometry.Euclidean.Circumcenter

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 : ℕ
s : Simplex ℝ P n
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ x,
        ((centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n) (pointIndex x) +
              centroidWeightsWithCircumcenter {i₁, i₂} (pointIndex x) -
            reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ (pointIndex x)) •
          (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) +
      ((centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n) circumcenterIndex +
            centroidWeightsWithCircumcenter {i₁, i₂} circumcenterIndex -
          reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ circumcenterIndex) •
        (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) =
    0

Tactic:
Pi.sub_apply,

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 : ℕ
s : Simplex ℝ P n
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ x,
        (centroidWeightsWithCircumcenter {i₁, i₂} (pointIndex x) -
                circumcenterWeightsWithCircumcenter n (pointIndex x) +
              centroidWeightsWithCircumcenter {i₁, i₂} (pointIndex x) -
            reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ (pointIndex x)) •
          (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) +
      (centroidWeightsWithCircumcenter {i₁, i₂} circumcenterIndex -
              circumcenterWeightsWithCircumcenter n circumcenterIndex +
            centroidWeightsWithCircumcenter {i₁, i₂} circumcenterIndex -
          reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ circumcenterIndex) •
        (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) =
    0
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
⊢ Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z)

Tactic:
Real.cos_add,

Goal state after:
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
⊢ Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) ≤ Real.cos (angle x z)
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
t : Triangle ℝ P
signs : Finset (Fin 3)
⊢ Simplex.excenter t signs = Simplex.incenter t ∨ ∃ i, Simplex.excenter t signs = Simplex.excenter t {i}

Tactic:
have h : signs = ∅ ∨ signs = Finset.univ ∨ ∃ i, signs = {i} ∨ signs = {i}ᶜ := by decide +revert

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
signs : Finset (Fin 3)
h : signs = ∅ ∨ signs = Finset.univ ∨ ∃ i, signs = {i} ∨ signs = {i}ᶜ
⊢ Simplex.excenter t signs = Simplex.incenter t ∨ ∃ i, Simplex.excenter t signs = Simplex.excenter t {i}
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case pointIndex
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
i : Fin (n + 2 + 1)
⊢ mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ (pointIndex i) =
    (mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ) (pointIndex i)

Tactic:
Pi.sub_apply,

Goal state after:
case pointIndex
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
i : Fin (n + 2 + 1)
⊢ mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ (pointIndex i) =
    mongePointWeightsWithCircumcenter n (pointIndex i) - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ (pointIndex i)
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ ∑ i, (mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ) i = 0

Tactic:
Pi.sub_apply,

Goal state after:
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ ∑ x, (mongePointWeightsWithCircumcenter n x - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ x) = 0
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : p ∈ line[ℝ, a, b]
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|

Tactic:
iterate 4 rw [dist_eq_norm_vsub V]

Goal state after:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : p ∈ line[ℝ, a, b]
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |‖b -ᵥ q‖ ^ 2 - ‖p -ᵥ q‖ ^ 2|
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ -(∑ x ∈ fs,
            (∑ i,
                (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
                    (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) (pointIndex i) *
                  (dist (s.points x) (s.points i) * dist (s.points x) (s.points i)) +
              (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
                  (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) circumcenterIndex *
                (dist (s.points x) s.circumcenter * dist (s.points x) s.circumcenter)) +
          (∑ i,
              -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) (pointIndex i) *
                (dist s.circumcenter (s.points i) * dist s.circumcenter (s.points i)) +
            -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) circumcenterIndex *
              (dist s.circumcenter s.circumcenter * dist s.circumcenter s.circumcenter))) /
      2 =
    0

Tactic:
Pi.sub_apply,

Goal state after:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ -(∑ x ∈ fs,
            (∑ x_1,
                (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
                    (pointWeightsWithCircumcenter i₁ (pointIndex x_1) -
                      pointWeightsWithCircumcenter i₂ (pointIndex x_1)) *
                  (dist (s.points x) (s.points x_1) * dist (s.points x) (s.points x_1)) +
              (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
                  (pointWeightsWithCircumcenter i₁ circumcenterIndex -
                    pointWeightsWithCircumcenter i₂ circumcenterIndex) *
                (dist (s.points x) s.circumcenter * dist (s.points x) s.circumcenter)) +
          (∑ x,
              -2 / ↑(n + 1) *
                  (pointWeightsWithCircumcenter i₁ (pointIndex x) - pointWeightsWithCircumcenter i₂ (pointIndex x)) *
                (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points x)) +
            -2 / ↑(n + 1) *
                (pointWeightsWithCircumcenter i₁ circumcenterIndex -
                  pointWeightsWithCircumcenter i₂ circumcenterIndex) *
              (dist s.circumcenter s.circumcenter * dist s.circumcenter s.circumcenter))) /
      2 =
    0
Module: Mathlib.Geometry.Euclidean.MongePoint

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 : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ mk' (Finset.centroid ℝ {i₁, i₂}ᶜ (s.reindex e).points) (ℝ ∙ ((s.points ∘ ⇑e.symm) i₁ -ᵥ (s.points ∘ ⇑e.symm) i₂))ᗮ ⊓
      affineSpan ℝ (Set.range (s.reindex e).points) =
    mk' (Finset.centroid ℝ {e.symm i₁, e.symm i₂}ᶜ s.points) (ℝ ∙ (s.points (e.symm i₁) -ᵥ s.points (e.symm i₂)))ᗮ ⊓
      affineSpan ℝ (Set.range s.points)

Tactic:
reindex_range_points,

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 : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ mk' (Finset.centroid ℝ {i₁, i₂}ᶜ (s.reindex e).points) (ℝ ∙ ((s.points ∘ ⇑e.symm) i₁ -ᵥ (s.points ∘ ⇑e.symm) i₂))ᗮ ⊓
      affineSpan ℝ (Set.range s.points) =
    mk' (Finset.centroid ℝ {e.symm i₁, e.symm i₂}ᶜ s.points) (ℝ ∙ (s.points (e.symm i₁) -ᵥ s.points (e.symm i₂)))ᗮ ⊓
      affineSpan ℝ (Set.range s.points)
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ {p₁, p, p₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
⊢ Cospherical {p₁, p₂, p₃, p₄}

Tactic:
let s_isom : AffineIsometry ℝ S P := S.subtypeₐᵢ

Goal state after:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ {p₁, p, p₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := S.subtypeₐᵢ
⊢ Cospherical {p₁, p₂, p₃, p₄}
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: P : Type u_2
inst✝ : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
⊢ s.power p = 0 ↔ p ∈ s

Tactic:
rw [power, mem_sphere, sub_eq_zero, pow_left_inj₀ dist_nonneg hr two_ne_zero]

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

Goal state before:
pp: case a
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : Real.cos (∠ a' b' c') = Real.cos (∠ a b c)
h_cos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
⊢ ∠ a' b' c' ∈ Set.Icc 0 Real.pi

pp: case a
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : Real.cos (∠ a' b' c') = Real.cos (∠ a b c)
h_cos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
⊢ ∠ a b c ∈ Set.Icc 0 Real.pi

Tactic:
grind [angle_nonneg, angle_le_pi]

Goal state after:
case a
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : Real.cos (∠ a' b' c') = Real.cos (∠ a b c)
h_cos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
⊢ ∠ a b c ∈ Set.Icc 0 Real.pi
Module: Mathlib.Geometry.Euclidean.Similarity

Goal state before:
pp: case a
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : Real.cos (∠ a' b' c') = Real.cos (∠ a b c)
h_cos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
⊢ ∠ a b c ∈ Set.Icc 0 Real.pi

Tactic:
grind [angle_nonneg, angle_le_pi]

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

Goal state before:

Tactic:
grind [angle_nonneg, angle_le_pi]

Goal state after: