mathlib-initiative/mathlib-tactics huggingface dataset:
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₂ ∈ 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₂ ∈ Metric.sphere (Affine.Simplex.circumsphere t₁).center (Affine.Simplex.circumsphere t₁).radius
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 + ∠ x p c = ∠ a p c

Tactic:
]

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.Circumcenter

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

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.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)
⊢ s.exradius signs = s.exradius signs

Tactic:
]

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

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
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₄
⊢ Cospherical {p₂, p₃, p₄} ∨ Collinear ℝ {p₂, p₃, p₄}

Tactic:
]

Goal state after:
case pos
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₄
⊢ Cospherical {p₂, p₃, p₄} ∨ Collinear ℝ {p₂, p₃, p₄}
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 p : P
h : ∠ b p c = π
⊢ (dist a p * dist a p + dist b p * dist b p - 2 * dist a p * dist b p * Real.cos (π - ∠ a p c)) * dist c p +
      (dist a p * dist a p + dist c p * dist c p - 2 * dist a p * dist c p * Real.cos (∠ a p c)) * dist b p =
    dist b c * (dist a p ^ 2 + dist b p * dist c p)

Tactic:
Real.cos_pi_sub,

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 p : P
h : ∠ b p c = π
⊢ (dist a p * dist a p + dist b p * dist b p - 2 * dist a p * dist b p * -Real.cos (∠ a p c)) * dist c p +
      (dist a p * dist a p + dist c p * dist c p - 2 * dist a p * dist c p * Real.cos (∠ a p c)) * dist b p =
    dist b c * (dist a p ^ 2 + dist b p * dist c 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))
i : Fin (n + 1)
p : P
ht : (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points))
⊢ ↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points))) (s.exsphere signs).center) =
    ↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points))) (s.exsphere signs).center)

Tactic:
]

Goal state after:
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 p : P
h : ∠ b p c = π
⊢ (dist a p * dist a p + dist b p * dist b p - 2 * dist a p * dist b p * -Real.cos (∠ a p c)) * dist c p +
      (dist a p * dist a p + dist c p * dist c p - 2 * dist a p * dist c p * Real.cos (∠ a p c)) * dist b p =
    (dist b p + dist c p) * (dist a p ^ 2 + dist b p * dist c 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
a b c p : P
h : ∠ b p c = π
⊢ (dist a p * dist a p + dist b p * dist b p - 2 * dist a p * dist b p * -Real.cos (∠ a p c)) * dist c p +
      (dist a p * dist a p + dist c p * dist c p - 2 * dist a p * dist c p * Real.cos (∠ a p c)) * dist b p =
    (dist b p + dist c p) * (dist a p ^ 2 + dist b p * dist c 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
i : Fin (n + 1)
⊢ s.pointsWithCircumcenter (pointIndex i) =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (pointWeightsWithCircumcenter 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 : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ s.pointsWithCircumcenter (pointIndex i) =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (pointWeightsWithCircumcenter i)
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₄}
⊢ Cospherical {p₂, p₃, p₄}

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₄}
⊢ Cospherical {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
hf : Fact (Module.finrank ℝ V = n)
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ n - 1 + 1 = n

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
hf : Fact (Module.finrank ℝ V = n)
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ n - 1 + 1 = n
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 := ⋯ }
⊢ ∃ s, {p₂, p₃, p₄} ⊆ Metric.sphere s.center s.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 := ⋯ }
⊢ ∃ s, {p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius
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 : P
hbc : ¬b = c
m : P := midpoint ℝ b c
this : dist b c ≠ 0
hm :
  dist a b ^ 2 * (2⁻¹ * dist b c) + dist a c ^ 2 * (2⁻¹ * dist b c) =
    dist b c * (dist a (midpoint ℝ b c) ^ 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))
⊢ 2 / dist b c * (dist b c * (dist a (midpoint ℝ b c) ^ 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))) =
    2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2)

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
a b c : P
hbc : ¬b = c
m : P := midpoint ℝ b c
this : dist b c ≠ 0
hm :
  dist a b ^ 2 * (2⁻¹ * dist b c) + dist a c ^ 2 * (2⁻¹ * dist b c) =
    dist b c * (dist a (midpoint ℝ b c) ^ 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))
⊢ 2 / dist b c * (dist b c * (dist a (midpoint ℝ b c) ^ 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))) =
    2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2)
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₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : ¬p₁ = p₄
⊢ Collinear ℝ {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
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₄
⊢ Collinear ℝ {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))
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
i : Fin (n + 1)
⊢ (s.signedInfDist i) ((Finset.affineCombination ℝ Finset.univ s.points) w) = (if i ∈ signs then -1 else 1) * r

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
i : Fin (n + 1)
⊢ (s.signedInfDist i) ((Finset.affineCombination ℝ Finset.univ s.points) w) = (if i ∈ signs then -1 else 1) * r
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₄}
⊢ Collinear ℝ {p₁, p₂, p₃, p₄}

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₄
hc' : Collinear ℝ {p₁, p₃, p₄}
⊢ Collinear ℝ {p₁, p₂, p₃, p₄}
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₄}
⊢ Collinear ℝ {p₂, p₁, p₄}

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₄
hc' : Collinear ℝ {p₁, p₃, p₄}
⊢ Collinear ℝ {p₂, p₁, p₄}
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
⊢ (r * dist a b) ^ 2 + (r * dist c b) ^ 2 - 2 * (r * dist a b) * (r * dist c b) * Real.cos (∠ a b c) =
    r ^ 2 * (dist a b ^ 2 + dist c b ^ 2 - 2 * dist a b * dist c b * Real.cos (∠ a b c))

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
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
⊢ (r * dist a b) ^ 2 + (r * dist c b) ^ 2 - 2 * (r * dist a b) * (r * dist c b) * Real.cos (∠ a b c) =
    r ^ 2 * (dist a b ^ 2 + dist c b ^ 2 - 2 * dist a b * dist c b * Real.cos (∠ a b c))
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.pointsWithCircumcenter circumcenterIndex =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (circumcenterWeightsWithCircumcenter n)

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
⊢ s.pointsWithCircumcenter circumcenterIndex =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (circumcenterWeightsWithCircumcenter n)
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
⊢ x - ⟪y, x⟫ • y = x - ⟪y, x⟫ • y

Tactic:
]

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 : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ⟪x, y⟫ * ⟪x, y⟫ ≤ 1

Tactic:
]

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⟫ ≤ 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
⊢ 1 ≤ 1

Tactic:
]

Goal state after:
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
⊢ 0 = 0

Tactic:
]

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
⊢ 0 = 0

pp: case hw
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ y ∈ ℝ ∙ y

Tactic:
]

Goal state after:
case hw
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ 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
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
i : Fin (n + 1)
h' : w i = (if i ∈ signs then -1 else 1) * r / s.height i
⊢ w i = r * ((if i ∈ signs then -1 else 1) * (s.height 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
i : Fin (n + 1)
h' : w i = (if i ∈ signs then -1 else 1) * r / s.height i
⊢ w i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ (#(if i₁ ∈ univ then {i₁} else ∅) + #(if i₂ ∈ univ then {i₂} else ∅)) • 1 + #{x | ¬(x = i₁ ∨ x = i₂)} • 0 + -1 = 1

pp: n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ Disjoint (if i₁ ∈ univ then {i₁} else ∅) (if i₂ ∈ univ then {i₂} else ∅)

Tactic:
]

Goal state after:
n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ (#(if i₁ ∈ univ then {i₁} else ∅) + #(if i₂ ∈ univ then {i₂} else ∅)) • 1 + #{x | ¬(x = i₁ ∨ x = i₂)} • 0 + -1 = 1

n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ Disjoint (if i₁ ∈ univ then {i₁} else ∅) (if i₂ ∈ univ then {i₂} else ∅)
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
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
hab'₁ : a' = b'
⊢ r * dist c b = r * dist c b

Tactic:
]

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 : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) ^ 2 + ⟪x, y⟫ ^ 2 = 1

Tactic:
]

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⟫ - ⟪y, x⟫ * ⟪x, y⟫)) ^ 2 + ⟪x, y⟫ ^ 2 = 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
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
⊢ 0 ≤ dist a' b'

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
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
⊢ 0 ≤ dist a' b'
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
h₁ : ¬x = y
h₂ : ¬x = -y
⊢ (‖x - ⟪y, x⟫ • y‖⁻¹ * (1 ^ 2 - ⟪y, x⟫ * ⟪x, y⟫)) ^ 2 + ⟪x, y⟫ ^ 2 = 1

Tactic:
]

Goal state after:
case neg
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
⊢ (‖x - ⟪y, x⟫ • y‖⁻¹ * (1 ^ 2 - ⟪y, x⟫ * ⟪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
i : Fin (n + 1)
h' : w i = (if i ∈ signs then -1 else 1) * r / s.height i
⊢ r *
      ((if i ∈ signs then -1 else 1) *
        (dist (s.points i)
            ↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points))) (s.points i)))⁻¹) =
    r *
      ((if i ∈ signs then -1 else 1) *
        (dist (s.points i)
            ↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points))) (s.points i)))⁻¹)

Tactic:
]

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

Tactic:
]

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