mathlib-initiative/mathlib-tactics huggingface dataset:
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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).circumradius = s.circumradius

Tactic:
[

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).circumradius = s.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
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₂ p₃ p₁
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ 2 • o.oangle (-(p₂ -ᵥ p₁)) (-(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁))) = 2 • o.oangle (-(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁))) (-(p₃ -ᵥ p₁))

Tactic:
[

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✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₂ p₃ p₁
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ 2 • o.oangle (-(p₂ -ᵥ p₁)) (-(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁))) = 2 • o.oangle (-(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁))) (-(p₃ -ᵥ p₁))
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))
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
h : (s.restrict S hS).ExcenterExists signs
i : Fin (n + 1)
this : Nonempty ↥S
⊢ ↑((s.restrict S hS).touchpoint signs i) = s.touchpoint signs i

Tactic:
exact (h.touchpoint_map S.subtypeₐᵢ i).symm

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

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
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
hn' : ¬Collinear ℝ {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }
⊢ {p₁, p₂, p₃, p₄} ⊆ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius

Tactic:
[

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
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
hn' : ¬Collinear ℝ {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }
⊢ {p₁, p₂, p₃, p₄} ⊆ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius
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₁ i₂ : Fin (n + 1)
⊢ dist (s.excenter signs) (s.touchpoint signs i₁) = dist (s.excenter signs) (s.touchpoint signs i₂)

Tactic:
[

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₁ i₂ : Fin (n + 1)
⊢ dist (s.excenter signs) (s.touchpoint signs i₁) = dist (s.excenter signs) (s.touchpoint signs i₂)
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)
⊢ circumcenterIndex ∉ Finset.map (pointIndexEmbedding n) univ

Tactic:
[

Goal state after:
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ circumcenterIndex ∉ Finset.map (pointIndexEmbedding n) univ
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : p₁ = p₄
hl : ¬Collinear ℝ {p₂, p₃, p₄}
t : Affine.Triangle ℝ P := { points := ![p₂, p₃, p₄], independent := ⋯ }
⊢ {p₂, p₃, p₄} ⊆ Metric.sphere (Affine.Simplex.circumsphere t).center (Affine.Simplex.circumsphere t).radius

Tactic:
[

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : p₁ = p₄
hl : ¬Collinear ℝ {p₂, p₃, p₄}
t : Affine.Triangle ℝ P := { points := ![p₂, p₃, p₄], independent := ⋯ }
⊢ {p₂, p₃, p₄} ⊆ Metric.sphere (Affine.Simplex.circumsphere t).center (Affine.Simplex.circumsphere t).radius
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: n : ℕ
fs : Finset (Fin (n + 1))
h : fs.Nonempty
⊢ ∑ i, centroidWeightsWithCircumcenter fs i = 1

Tactic:
[

Goal state after:
n : ℕ
fs : Finset (Fin (n + 1))
h : fs.Nonempty
⊢ ∑ i, centroidWeightsWithCircumcenter fs i = 1
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
fs : Finset (Fin (n + 1))
⊢ Finset.centroid ℝ fs s.points =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (centroidWeightsWithCircumcenter fs)

Tactic:
[

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
fs : Finset (Fin (n + 1))
⊢ Finset.centroid ℝ fs s.points =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (centroidWeightsWithCircumcenter fs)
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : ¬p₁ = p₄
hc' : Collinear ℝ {p₁, p₃, p₄}
⊢ Cospherical {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}

Tactic:
refine Or.inr ?_

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : ¬p₁ = p₄
hc' : Collinear ℝ {p₁, p₃, p₄}
⊢ Collinear ℝ {p₁, p₂, p₃, p₄}
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
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : ∑ i, w i = 1
hp : (Finset.affineCombination ℝ Finset.univ s.points) w ∈ affineSpan ℝ (Set.range s.points)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i) ((Finset.affineCombination ℝ Finset.univ s.points) w) = (if i ∈ signs then -1 else 1) * r
h' : ∀ (i : Fin (n + 1)), w i * ‖s.points i -ᵥ s.altitudeFoot i‖ = (if i ∈ signs then -1 else 1) * r
⊢ s.ExcenterExists signs ∧ (Finset.affineCombination ℝ Finset.univ s.points) w = s.excenter signs

Tactic:
[

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
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : ∑ i, w i = 1
hp : (Finset.affineCombination ℝ Finset.univ s.points) w ∈ affineSpan ℝ (Set.range s.points)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i) ((Finset.affineCombination ℝ Finset.univ s.points) w) = (if i ∈ signs then -1 else 1) * r
h' : ∀ (i : Fin (n + 1)), w i * ‖s.points i -ᵥ s.altitudeFoot i‖ = (if i ∈ signs then -1 else 1) * r
⊢ s.ExcenterExists signs ∧ (Finset.affineCombination ℝ Finset.univ s.points) w = s.excenter signs
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : ¬Collinear ℝ {p₁, p₂, p₄}
⊢ Cospherical {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}

Tactic:
exact Or.inl (cospherical_of_two_zsmul_oangle_eq_of_not_collinear h hc)

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
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : ∑ i, w i = 1
hp : (Finset.affineCombination ℝ Finset.univ s.points) w ∈ affineSpan ℝ (Set.range s.points)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i) ((Finset.affineCombination ℝ Finset.univ s.points) w) = (if i ∈ signs then -1 else 1) * r
h' : ∀ (i : Fin (n + 1)), w i * dist (s.points i) (s.altitudeFoot i) = (if i ∈ signs then -1 else 1) * r
⊢ ∀ (i : Fin (n + 1)), w i = r * s.excenterWeightsUnnorm signs i

Tactic:
[

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))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : ∑ i, w i = 1
hp : (Finset.affineCombination ℝ Finset.univ s.points) w ∈ affineSpan ℝ (Set.range s.points)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i) ((Finset.affineCombination ℝ Finset.univ s.points) w) = (if i ∈ signs then -1 else 1) * r
h' : ∀ (i : Fin (n + 1)), w i * dist (s.points i) (s.altitudeFoot i) = (if i ∈ signs then -1 else 1) * r
⊢ ∀ (i : Fin (n + 1)), w i = r * s.excenterWeightsUnnorm signs i
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ ∑ i, reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ i = 1

Tactic:
[

Goal state after:
n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ ∑ i, reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ i = 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
hy : ‖y‖ = 1
⊢ ortho y x = x - ⟪y, x⟫ • y

Tactic:
ortho,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : ‖y‖ = 1
⊢ x - (ℝ ∙ y).starProjection x = 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
⊢ 0 ≤ ⟪x, x - ⟪y, x⟫ • y⟫

Tactic:
inner_sub_right,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 0 ≤ ⟪x, x⟫ - ⟪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
⊢ ⟪y, ortho y x⟫ = 0

Tactic:
ortho,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ⟪y, x - (ℝ ∙ y).starProjection x⟫ = 0
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 - ⟪y, x⟫ • y‖⁻¹ * ⟪x, x - ⟪y, x⟫ • y⟫) ^ 2 + ⟪x, y⟫ ^ 2 = 1

Tactic:
inner_sub_right,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪x, ⟪y, x⟫ • y⟫)) ^ 2 + ⟪x, y⟫ ^ 2 = 1
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))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : ∑ i, w i = 1
hp : (Finset.affineCombination ℝ Finset.univ s.points) w ∈ affineSpan ℝ (Set.range s.points)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i) ((Finset.affineCombination ℝ Finset.univ s.points) w) = (if i ∈ signs then -1 else 1) * r
h' : ∀ (i : Fin (n + 1)), w i * dist (s.points i) (s.altitudeFoot i) = (if i ∈ signs then -1 else 1) * r
h'' : ∀ (i : Fin (n + 1)), w i = r * s.excenterWeightsUnnorm signs i
⊢ w = s.excenterWeights signs

Tactic:
[

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))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : ∑ i, w i = 1
hp : (Finset.affineCombination ℝ Finset.univ s.points) w ∈ affineSpan ℝ (Set.range s.points)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i) ((Finset.affineCombination ℝ Finset.univ s.points) w) = (if i ∈ signs then -1 else 1) * r
h' : ∀ (i : Fin (n + 1)), w i * dist (s.points i) (s.altitudeFoot i) = (if i ∈ signs then -1 else 1) * r
h'' : ∀ (i : Fin (n + 1)), w i = r * s.excenterWeightsUnnorm signs i
⊢ w = s.excenterWeights signs
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⟫ • y⟫ - ⟪⟪y, x⟫ • y, x - ⟪y, x⟫ • y⟫) * ⟪x, y⟫ ^ 2 =
    ⟪x, x - ⟪y, x⟫ • y⟫ - ⟪⟪y, x⟫ • y, x - ⟪y, x⟫ • y⟫

Tactic:
inner_sub_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⟫ - ⟪x, ⟪y, x⟫ • y⟫ - ⟪⟪y, x⟫ • y, x - ⟪y, x⟫ • y⟫) * ⟪x, y⟫ ^ 2 =
    ⟪x, x⟫ - ⟪x, ⟪y, x⟫ • y⟫ - ⟪⟪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
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⟫) * ⟪x, y⟫ ^ 2 =
    ⟪x, x⟫ - ⟪x, ⟪y, x⟫ • y⟫ - ⟪⟪y, x⟫ • y, x - ⟪y, x⟫ • y⟫

Tactic:
inner_sub_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⟫ - ⟪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⟫)
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:
[

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)
⊢ ∑ 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
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)), dist p ↑((s.faceOpposite i).orthogonalProjectionSpan p) = r) ↔
    ∃ signs, s.ExcenterExists signs ∧ p = s.excenter signs

Tactic:
[

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
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
⊢ (∃ r, ∀ (i : Fin (n + 1)), dist p ↑((s.faceOpposite i).orthogonalProjectionSpan p) = r) ↔
    ∃ signs, s.ExcenterExists signs ∧ p = s.excenter signs
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 - ⟪y, x⟫ • y⟫) • ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)

Tactic:
inner_sub_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⟫ - ⟪x, ⟪y, 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
⊢ ⟪x, x - ⟪x, y⟫ • y⟫ - ⟪⟪x, y⟫ • y, x - ⟪x, y⟫ • y⟫ = 1 - ⟪x, y⟫ ^ 2

Tactic:
inner_sub_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
⊢ ⟪x, x⟫ - ⟪x, ⟪x, y⟫ • y⟫ - ⟪⟪x, y⟫ • y, x - ⟪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
⊢ ⟪x, x⟫ - ⟪x, ⟪x, y⟫ • y⟫ - ⟪⟪x, y⟫ • y, x - ⟪x, y⟫ • y⟫ = 1 - ⟪x, y⟫ ^ 2

Tactic:
inner_sub_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
⊢ ⟪x, x⟫ - ⟪x, ⟪x, y⟫ • y⟫ - (⟪⟪x, y⟫ • y, x⟫ - ⟪⟪x, y⟫ • y, ⟪x, y⟫ • y⟫) = 1 - ⟪x, y⟫ ^ 2
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : p₂ = p₁
⊢ π / 3 ≤ ∠ p₁ p₂ p₃

pp: case neg
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₃
h : ¬p₂ = p₁
⊢ π / 3 ≤ ∠ p₁ p₂ p₃

Tactic:
· rw [h, angle_self_left]
    linarith [Real.pi_pos]

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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
⊢ π / 3 ≤ ∠ p₁ p₂ p₃
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
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₂
h : p₂ = p₁
⊢ π / 3 < ∠ p₁ p₂ p₃

pp: case neg
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₂
h : ¬p₂ = p₁
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
· rw [h, angle_self_left]
    linarith [Real.pi_pos]

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
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₂
h : ¬p₂ = p₁
⊢ π / 3 < ∠ p₁ p₂ p₃
Module: Mathlib.Topology.MetricSpace.Congruence

Goal state before:
pp: ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ Congruent v₁ v₂ ↔ Pairwise fun i₁ i₂ ↦ nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)

Tactic:
[

Goal state after:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ Congruent v₁ v₂ ↔ Pairwise fun i₁ i₂ ↦ nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)
Module: Mathlib.Topology.MetricSpace.Congruence

Goal state before:
pp: ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ Congruent v₁ v₂ ↔ Pairwise fun i₁ i₂ ↦ dist (v₁ i₁) (v₁ i₂) = dist (v₂ i₁) (v₂ i₂)

Tactic:
[

Goal state after:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ Congruent v₁ v₂ ↔ Pairwise fun i₁ i₂ ↦ dist (v₁ i₁) (v₁ i₂) = dist (v₂ i₁) (v₂ i₂)