Module: Mathlib.Geometry.Euclidean.Angle.Incenter

Goal state before:
pp: case inl
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)
t : Triangle ℝ P
i₂ i₃ : Fin 3
h₂₃ : i₂ ≠ i₃
p : P
h₁ : dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₂).orthogonalProjectionSpan p)
hp : p ∈ affineSpan ℝ (Set.range t.points)
i : Fin (2 + 1)
h₁₂ : i ≠ i₂
h₁₃ : i ≠ i₃
h₂ : dist p ↑((faceOpposite t i).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p)
⊢ dist p ↑((faceOpposite t i).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p)

pp: case inr.inl
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)
t : Triangle ℝ P
i₁ i₃ : Fin 3
h₁₃ : i₁ ≠ i₃
p : P
h₂ : dist p ↑((faceOpposite t i₁).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p)
hp : p ∈ affineSpan ℝ (Set.range t.points)
i : Fin (2 + 1)
h₁₂ : i₁ ≠ i
h₂₃ : i ≠ i₃
h₁ : dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i).orthogonalProjectionSpan p)
⊢ dist p ↑((faceOpposite t i).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p)

pp: case inr.inr
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)
t : Triangle ℝ P
i₁ i₂ : Fin 3
h₁₂ : i₁ ≠ i₂
p : P
hp : p ∈ affineSpan ℝ (Set.range t.points)
i : Fin (2 + 1)
h₁₃ : i₁ ≠ i
h₂₃ : i₂ ≠ i
h₁ : dist p ↑((faceOpposite t i).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₂).orthogonalProjectionSpan p)
h₂ : dist p ↑((faceOpposite t i₁).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i).orthogonalProjectionSpan p)
⊢ dist p ↑((faceOpposite t i).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i).orthogonalProjectionSpan p)

Tactic:
<;>

Goal state after:
case inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₂ i₃ : Fin 3
h₂₃ : i₂ ≠ i₃
p : P
h₁ : dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₂).orthogonalProjectionSpan p)
hp : p ∈ affineSpan ℝ (Set.range t.points)
i : Fin (2 + 1)
h₁₂ : i ≠ i₂
h₁₃ : i ≠ i₃
h₂ : dist p ↑((faceOpposite t i).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p)
⊢ dist p ↑((faceOpposite t i).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p)

case inr.inl
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)
t : Triangle ℝ P
i₁ i₃ : Fin 3
h₁₃ : i₁ ≠ i₃
p : P
h₂ : dist p ↑((faceOpposite t i₁).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p)
hp : p ∈ affineSpan ℝ (Set.range t.points)
i : Fin (2 + 1)
h₁₂ : i₁ ≠ i
h₂₃ : i ≠ i₃
h₁ : dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i).orthogonalProjectionSpan p)
⊢ dist p ↑((faceOpposite t i).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p)

case inr.inr
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)
t : Triangle ℝ P
i₁ i₂ : Fin 3
h₁₂ : i₁ ≠ i₂
p : P
hp : p ∈ affineSpan ℝ (Set.range t.points)
i : Fin (2 + 1)
h₁₃ : i₁ ≠ i
h₂₃ : i₂ ≠ i
h₁ : dist p ↑((faceOpposite t i).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₂).orthogonalProjectionSpan p)
h₂ : dist p ↑((faceOpposite t i₁).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i).orthogonalProjectionSpan p)
⊢ dist p ↑((faceOpposite t i).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i).orthogonalProjectionSpan p)