mathlib-initiative/mathlib-tactics huggingface dataset:
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₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ |(∡ p₁ p₂ p₃).sin| = (∡ p₃ p₁ s.center).cos

Tactic:
← Real.Angle.abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi
    (two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi hp₁ hp₂ hp₃ hp₁p₂.symm hp₂p₃ hp₁p₃),

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₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ |(∡ p₃ p₁ s.center).cos| = (∡ p₃ p₁ s.center).cos
Module: Mathlib.Geometry.Euclidean.Incenter

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
h : s.excenterWeights signs₁ = s.excenterWeights signs₂
hn₁ : ∑ i, s.excenterWeightsUnnorm signs₁ i ≠ 0
hn₂ : ∑ i, s.excenterWeightsUnnorm signs₂ i ≠ 0
hs : SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ = -SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹
hi :
  ∀ (i : Fin (n + 1)),
    -SignType.sign (s.excenterWeightsUnnorm signs₁ i) = SignType.sign (s.excenterWeightsUnnorm signs₂ i)
⊢ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ

Tactic:
simp only [excenterWeightsUnnorm, sign_mul, inv_pos, height_pos, sign_pos, mul_one] at hi

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
h : s.excenterWeights signs₁ = s.excenterWeights signs₂
hn₁ : ∑ i, s.excenterWeightsUnnorm signs₁ i ≠ 0
hn₂ : ∑ i, s.excenterWeightsUnnorm signs₂ i ≠ 0
hs : SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ = -SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹
hi : ∀ (i : Fin (n + 1)), -SignType.sign (if i ∈ signs₁ then -1 else 1) = SignType.sign (if i ∈ signs₂ then -1 else 1)
⊢ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ
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
h : angle (x - y) y = angle (x - y) (x - y + y) + angle y (x - y + y)
⊢ angle x y + angle x (x - y) + angle y (y - x) = π

Tactic:
sub_add_cancel

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
h : angle (x - y) y = angle (x - y) x + angle y x
⊢ angle x y + angle x (x - y) + angle y (y - 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
signs₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
⊢ (Finset.affineCombination ℝ Finset.univ s.points) (s.excenterWeights signs₁) = s.excenter signs₂ ↔
    signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ

Tactic:
h₂.affineCombination_eq_excenter_iff (s.sum_excenterWeights_eq_one_iff.2 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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
⊢ s.excenterWeights signs₁ = s.excenterWeights signs₂ ↔ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ
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
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).circumcenter = f s.circumcenter

Tactic:
eq_comm

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ f s.circumcenter = (s.map f.toAffineMap ⋯).circumcenter
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
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).circumradius = s.circumradius

Tactic:
eq_comm

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ s.circumradius = (s.map f.toAffineMap ⋯).circumradius
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₂ p₃ p₁ + ∠ p₃ p₁ p₂) = π

Tactic:
add_comm,

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₃ p₁ + ∠ p₃ p₁ p₂ + ∠ p₁ p₂ p₃ = π
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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ ↑(s.restrict S hS).circumcenter = s.circumcenter

Tactic:
eq_comm

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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ s.circumcenter = ↑(s.restrict S hS).circumcenter
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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ (s.restrict S hS).circumradius = s.circumradius

Tactic:
eq_comm

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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ s.circumradius = (s.restrict S hS).circumradius
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ ∑ i, f i = ∑ i, f ((pointIndexEmbedding n) i) + f circumcenterIndex

Tactic:
add_comm,

Goal state after:
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ ∑ i, f i = f circumcenterIndex + ∑ i, f ((pointIndexEmbedding n) i)
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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ dist (s.excenter signs) ↑((s.faceOpposite i).orthogonalProjectionSpan (s.excenter signs)) = s.exradius signs

Tactic:
← touchpoint,

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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ dist (s.excenter signs) (s.touchpoint signs i) = s.exradius signs
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
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
hab₁ : a = b
⊢ r * dist a b = 0

Tactic:
dist_eq_zero.mpr hab₁,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
hab₁ : a = b
⊢ r * 0 = 0
Module: Mathlib.Geometry.Euclidean.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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
r : ℝ
h : ∀ (i : Fin (n + 1)), |(s.signedInfDist i) p| = r
h' : ∀ (i : Fin (n + 1)), (s.signedInfDist i) p = r ∨ (s.signedInfDist i) p = -r
⊢ s.ExcenterExists {i | (s.signedInfDist i) p = -r} ∧ p = s.excenter {i | (s.signedInfDist i) p = -r}

Tactic:
apply (s.exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter hp).1

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
r : ℝ
h : ∀ (i : Fin (n + 1)), |(s.signedInfDist i) p| = r
h' : ∀ (i : Fin (n + 1)), (s.signedInfDist i) p = r ∨ (s.signedInfDist i) p = -r
⊢ ∃ r_1, ∀ (i : Fin (n + 1)), (s.signedInfDist i) p = (if i ∈ {i | (s.signedInfDist i) p = -r} then -1 else 1) * r_1
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
H : 1 - ⟪x, y⟫ ^ 2 ≠ 0
⊢ x = ⟪y, x⟫ • y + ((1 - ⟪y, x⟫ ^ 2) / ⟪x - ⟪y, x⟫ • y, x - ⟪y, x⟫ • y⟫) • (x - ⟪y, x⟫ • y)

Tactic:
have H0 : ⟪x - ⟪x, y⟫ • y, x - ⟪x, y⟫ • y⟫ = 1 - ⟪x, y⟫ ^ 2 := by
    rw [inner_sub_left, inner_sub_right, inner_sub_right, inner_self_eq_one_of_norm_eq_one hx,
      real_inner_smul_right, ← sq, real_inner_smul_left, real_inner_smul_left,
      real_inner_smul_right, inner_self_eq_one_of_norm_eq_one hy, real_inner_comm y x]
    ring

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
H : 1 - ⟪x, y⟫ ^ 2 ≠ 0
H0 : ⟪x - ⟪x, y⟫ • y, x - ⟪x, y⟫ • y⟫ = 1 - ⟪x, y⟫ ^ 2
⊢ x = ⟪y, x⟫ • y + ((1 - ⟪y, x⟫ ^ 2) / ⟪x - ⟪y, x⟫ • y, x - ⟪y, x⟫ • y⟫) • (x - ⟪y, x⟫ • y)
Module: Mathlib.Geometry.Euclidean.Incenter

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
hs :
  SignType.sign
      (s.touchpointWeights signs i j * ‖s.points j -ᵥ ↑((s.faceOpposite j).orthogonalProjectionSpan (s.points j))‖) =
    SignType.sign (s.excenterWeights signs j)
⊢ SignType.sign ‖s.points j -ᵥ ↑((s.faceOpposite j).orthogonalProjectionSpan (s.points j))‖ = 1

Tactic:
rw [sign_eq_one_iff, ← dist_eq_norm_vsub]

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
hs :
  SignType.sign
      (s.touchpointWeights signs i j * ‖s.points j -ᵥ ↑((s.faceOpposite j).orthogonalProjectionSpan (s.points j))‖) =
    SignType.sign (s.excenterWeights signs j)
⊢ 0 < dist (s.points j) ↑((s.faceOpposite j).orthogonalProjectionSpan (s.points j))
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
hz : z = 0
hx : x ≠ 0
⊢ angle z x = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)

Tactic:
add_comm,

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
hz : z = 0
hx : x ≠ 0
⊢ angle z x = angle z (kx • x + kz • z) + angle x (kx • x + kz • z)
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
⊢ ‖z + y‖ = ‖z - y‖

Tactic:
eq_comm

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
⊢ ‖z - y‖ = ‖z + y‖
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
r : P
⊢ b -ᵥ r = m -ᵥ r + (b -ᵥ midpoint ℝ a b)

Tactic:
add_comm,

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
r : P
⊢ b -ᵥ r = b -ᵥ midpoint ℝ a b + (m -ᵥ r)
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₂
⊢ -(∑ i,
            ∑ i₂_1,
              (if i = i₁ ∨ i = i₂ then (↑(n + 1))⁻¹ else 0) *
                  (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
                (dist (s.points i) (s.pointsWithCircumcenter i₂_1) *
                  dist (s.points i) (s.pointsWithCircumcenter i₂_1)) +
          ∑ i₂_1,
            -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
              (dist s.circumcenter (s.pointsWithCircumcenter i₂_1) *
                dist s.circumcenter (s.pointsWithCircumcenter i₂_1))) /
      2 =
    0

Tactic:
← sum_subset fs.subset_univ _

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,
            ∑ i₂_1,
              (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
                  (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
                (dist (s.points x) (s.pointsWithCircumcenter i₂_1) *
                  dist (s.points x) (s.pointsWithCircumcenter i₂_1)) +
          ∑ i₂_1,
            -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
              (dist s.circumcenter (s.pointsWithCircumcenter i₂_1) *
                dist s.circumcenter (s.pointsWithCircumcenter i₂_1))) /
      2 =
    0

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 ∈ univ,
    x ∉ fs →
      ∑ i₂_1,
          (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
              (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
            (dist (s.points x) (s.pointsWithCircumcenter i₂_1) * dist (s.points x) (s.pointsWithCircumcenter i₂_1)) =
        0
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,
            (∑ x_1,
                (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
                    ((if x_1 = i₁ then 1 else 0) - if x_1 = i₂ then 1 else 0) *
                  (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) * (0 - 0) *
                (dist (s.points x) s.circumcenter * dist (s.points x) s.circumcenter)) +
          (∑ x,
              -2 / ↑(n + 1) * ((if x = i₁ then 1 else 0) - if x = i₂ then 1 else 0) *
                (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points x)) +
            -2 / ↑(n + 1) * (0 - 0) * (dist s.circumcenter s.circumcenter * dist s.circumcenter s.circumcenter))) /
      2 =
    0

Tactic:
← sum_subset fs.subset_univ _

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) *
                    ((if x_1 = i₁ then 1 else 0) - if x_1 = i₂ then 1 else 0) *
                  (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) * (0 - 0) *
                (dist (s.points x) s.circumcenter * dist (s.points x) s.circumcenter)) +
          (∑ x ∈ fs,
              -2 / ↑(n + 1) * ((if x = i₁ then 1 else 0) - if x = i₂ then 1 else 0) *
                (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points x)) +
            -2 / ↑(n + 1) * (0 - 0) * (dist s.circumcenter s.circumcenter * dist s.circumcenter s.circumcenter))) /
      2 =
    0

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 ∈ univ,
    x ∉ fs →
      -2 / ↑(n + 1) * ((if x = i₁ then 1 else 0) - if x = i₂ then 1 else 0) *
          (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points 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
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)
⊢ p₂ ∈ line[ℝ, p₁, p]

Tactic:
simp [hp₁p₂_sbtw.wbtw.collinear.mem_affineSpan_of_mem_of_ne _ _ _ hp₁p₂_sbtw.left_ne]

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

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
p : P
hp : p ∈ s
v : V
p' : P
hp' : p' ∈ AffineSubspace.mk' p (ℝ ∙ v)
h : p' ∈ s
⊢ p' = p ∨ p' = s.secondInter p v

Tactic:
rw [AffineSubspace.mem_mk', Submodule.mem_span_singleton] at hp'

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 : Sphere P
p : P
hp : p ∈ s
v : V
p' : P
hp' : ∃ a, a • v = p' -ᵥ p
h : p' ∈ s
⊢ p' = p ∨ p' = s.secondInter p v
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)
i₁ i₂ : Fin (n + 3)
⊢ ∀ u ∈ ℝ ∙ (s.points i₁ -ᵥ s.points i₂), ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, u⟫ = 0

Tactic:
intro v

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)
i₁ i₂ : Fin (n + 3)
v : V
⊢ v ∈ ℝ ∙ (s.points i₁ -ᵥ s.points i₂) → ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, v⟫ = 0
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

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
s : Sphere P
p p' : P
hp : p ∈ s
hp' : dist p' s.center ≤ s.radius
h : ¬p' = p
he : ⟪p -ᵥ p', p -ᵥ s.center⟫ = 0
⊢ False

Tactic:
eq_comm

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
s : Sphere P
p p' : P
hp : p ∈ s
hp' : dist p' s.center ≤ s.radius
h : ¬p' = p
he : 0 = ⟪p -ᵥ p', p -ᵥ s.center⟫
⊢ False
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

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
p p' : P
hp : p ∈ s
hp' : dist p' s.center < s.radius
⊢ p' ≠ s.secondInter p (p' -ᵥ p)

Tactic:
rintro h
    rw [h, mem_sphere.1 ((Sphere.secondInter_mem _).2 hp)] at hp'
    exact lt_irrefl _ hp'

Goal state after: