-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
h₁ :
  dist p
      (↑(((faceOpposite t i₃).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            p) :
        P) =
    dist p
      (↑(((faceOpposite t i₂).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₂).points)))
            p) :
        P)
h₂ :
  dist p
      (↑(((faceOpposite t i₁).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₁).points)))
            p) :
        P) =
    dist p
      (↑(((faceOpposite t i₃).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            p) :
        P)
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) p
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
h : i = i₁ ∨ i = i₂ ∨ i = i₃
inl :
  ∀ (h₁₂ : i ≠ i₂) (h₁₃ : i ≠ i₃)
    (h₂ :
      dist p
          (↑(((faceOpposite t i).orthogonalProjectionSpan :
                  (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i).points)))
                p) :
            P) =
        dist p
          (↑(((faceOpposite t i₃).orthogonalProjectionSpan :
                  (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
                p) :
            P)),
    dist p
        (↑(((faceOpposite t i).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i).points)))
              p) :
          P) =
      dist p
        (↑(((faceOpposite t i₃).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
              p) :
          P)
⊢ dist p
      (↑(((faceOpposite t i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i).points)))
            p) :
        P) =
    dist p
      (↑(((faceOpposite t i₃).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            p) :
        P)
have inr : ∀ (h₁₂ : i₁ ≠ i) (h₂₃ : i ≠ i₃)
  (h₁ :
    dist p
        (↑(((faceOpposite t i₃).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
              p) :
          P) =
      dist p
        (↑(((faceOpposite t i).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i).points)))
              p) :
          P)),
  dist p
      (↑(((faceOpposite t i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i).points)))
            p) :
        P) =
    dist p
      (↑(((faceOpposite t i₃).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            p) :
        P)
Tactic: rcases h with rfl | rfl | rfl
Cleared hypotheses: i₂, h₁₂, h₂₃, h₁, h