awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₃
hd :
  dist (excenter t {i₁})
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            (excenter t {i₁})) :
        P) =
    dist (excenter t {i₁})
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₂).points)))
            (excenter t {i₁})) :
        P)
⊢ t.points i₁ ∈ Set.range (faceOpposite t i₃).points
have refine_1 : ∃ (x : Fin 3), ¬x = i₃ ∧ t.points x = t.points i₁
Tactic: simp
-- 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₃
hd :
  dist (excenter t {i₁})
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            (excenter t {i₁})) :
        P) =
    dist (excenter t {i₁})
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₂).points)))
            (excenter t {i₁})) :
        P)
⊢ t.points i₁ ∈ Set.range (faceOpposite t i₂).points
have refine_2 : ∃ (x : Fin 3), ¬x = i₂ ∧ t.points x = t.points i₁
Tactic: simp
-- 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₃
⊢ ∡ (t.points i₁) (t.points i₂) (excenter t {i₁}) = ∡ (excenter t {i₁}) (t.points i₂) (t.points i₃) + (↑π : Real.Angle)
have rw : ∡ (touchpoint t {i₁} i₃) (t.points i₂) (excenter t {i₁}) = ∡ (excenter t {i₁}) (t.points i₂) (touchpoint t {i₁} i₁)
Tactic: rw [(t.touchpoint_singleton_sbtw h₁₃ h₁₂ h₂₃.symm).symm.oangle_eq_add_pi_left
        ((t.excenterExists_singleton _).excenter_ne_point _),
    ← (t.sbtw_touchpoint_singleton h₁₂.symm h₂₃ h₁₃).oangle_eq_right, add_left_inj]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (hypothesis)
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₃
⊢ ∡ (touchpoint t {i₁} i₃) (t.points i₂) (excenter t {i₁}) = ∡ (excenter t {i₁}) (t.points i₂) (touchpoint t {i₁} i₁)
have hd : dist (excenter t {i₁}) (touchpoint t {i₁} i₃) = dist (excenter t {i₁}) (touchpoint t {i₁} i₁)
Tactic: have hd := (t.excenterExists_singleton i₁).dist_excenter_eq_dist_excenter i₃ i₁
-- 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₃
hd : dist (excenter t {i₁}) (touchpoint t {i₁} i₃) = dist (excenter t {i₁}) (touchpoint t {i₁} i₁)
⊢ ∡ (touchpoint t {i₁} i₃) (t.points i₂) (excenter t {i₁}) = ∡ (excenter t {i₁}) (t.points i₂) (touchpoint t {i₁} i₁)
have simp_rw : ∡
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
          (excenter t {i₁})) :
      P)
    (t.points i₂) (excenter t {i₁}) =
  ∡ (excenter t {i₁}) (t.points i₂)
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₁).points)))
          (excenter t {i₁})) :
      P)
Tactic: simp_rw [touchpoint, orthogonalProjectionSpan] at hd ⊢
-- 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₃
hd :
  dist (excenter t {i₁})
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            (excenter t {i₁})) :
        P) =
    dist (excenter t {i₁})
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₁).points)))
            (excenter t {i₁})) :
        P)
⊢ ∡
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            (excenter t {i₁})) :
        P)
      (t.points i₂) (excenter t {i₁}) =
    ∡ (excenter t {i₁}) (t.points i₂)
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₁).points)))
            (excenter t {i₁})) :
        P)
have refine_1 : t.points i₂ ∈ Set.range (faceOpposite t i₃).points
Tactic: refine oangle_eq_of_dist_orthogonalProjection_eq (mem_affineSpan _ ?_) (mem_affineSpan _ ?_)
    ((t.excenterExists_singleton i₁).touchpoint_injective.ne h₁₃.symm) hd
-- 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₃
hd :
  dist (excenter t {i₁})
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            (excenter t {i₁})) :
        P) =
    dist (excenter t {i₁})
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₁).points)))
            (excenter t {i₁})) :
        P)
refine_1 : t.points i₂ ∈ Set.range (faceOpposite t i₃).points
⊢ ∡
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            (excenter t {i₁})) :
        P)
      (t.points i₂) (excenter t {i₁}) =
    ∡ (excenter t {i₁}) (t.points i₂)
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₁).points)))
            (excenter t {i₁})) :
        P)
have refine_2 : t.points i₂ ∈ Set.range (faceOpposite t i₁).points
Tactic: refine oangle_eq_of_dist_orthogonalProjection_eq (mem_affineSpan _ ?_) (mem_affineSpan _ ?_)
    ((t.excenterExists_singleton i₁).touchpoint_injective.ne h₁₃.symm) hd
-- 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₃
hd :
  dist (excenter t {i₁})
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            (excenter t {i₁})) :
        P) =
    dist (excenter t {i₁})
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₁).points)))
            (excenter t {i₁})) :
        P)
⊢ t.points i₂ ∈ Set.range (faceOpposite t i₃).points
have refine_1 : ∃ (x : Fin 3), ¬x = i₃ ∧ t.points x = t.points i₂
Tactic: simp
-- 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₃
hd :
  dist (excenter t {i₁})
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            (excenter t {i₁})) :
        P) =
    dist (excenter t {i₁})
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₁).points)))
            (excenter t {i₁})) :
        P)
⊢ t.points i₂ ∈ Set.range (faceOpposite t i₁).points
have refine_2 : ∃ (x : Fin 3), ¬x = i₁ ∧ t.points x = t.points i₂
Tactic: simp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (hypothesis)
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₁ : HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₂) (t.points i₁) p) = HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₁) (t.points i₃))
h₂ : HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₃) (t.points i₂) p) = HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁))
⊢ ∃ (signs : Finset (Fin 3)), p = excenter t signs
have 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)
Tactic: rw [← dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (hypothesis)
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₂ : HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₃) (t.points i₂) p) = HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁))
⊢ ∃ (signs : Finset (Fin 3)), p = excenter t signs
have 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)
Tactic: rw [← dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq h₂₃ h₁₂.symm h₁₃.symm]
    at h₂
Cleared hypotheses: h₂
-- 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)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) p
have h : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) ⊤
Tactic: convert! AffineSubspace.mem_top ℝ V p
-- 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)
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) ⊤
have h : Fintype.card (Fin (HAdd.hAdd (α := ℕ) 2 1)) = finrank ℝ V + 1
Tactic: rw [t.independent.affineSpan_eq_top_iff_card_eq_finrank_add_one]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (hypothesis)
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)
⊢ ∃ (signs : Finset (Fin 3)), p = excenter t signs
have hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) p
Tactic: have hp : p ∈ affineSpan ℝ (Set.range t.points) := by
    convert! AffineSubspace.mem_top ℝ V p
    rw [t.independent.affineSpan_eq_top_iff_card_eq_finrank_add_one]
    simp [hd2.out]
-- 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
⊢ ∃ (r : ℝ),
    ∀ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)),
      dist p
          (↑(((faceOpposite t i).orthogonalProjectionSpan :
                  (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i).points)))
                p) :
            P) =
        r
have refine : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)),
  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: refine ⟨dist p ((faceOpposite t i₃).orthogonalProjectionSpan p), ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (hypothesis)
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)
⊢ 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 h : i = i₁ ∨ i = i₂ ∨ i = i₃
Tactic: have h : i = i₁ ∨ i = i₂ ∨ i = i₃ := by clear! p t; decide +revert
-- 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₃
⊢ 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 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)
Tactic: rcases h with rfl | rfl | rfl
Cleared hypotheses: i₁, h₁₂, h₁₃, h₂, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (hypothesis)
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
⊢ ∃ (signs : Finset (Fin 3)), p = excenter t signs
have hr : ∃ (r : ℝ),
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)),
    dist p
        (↑(((faceOpposite t i).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i).points)))
              p) :
          P) =
      r
Tactic: have hr : ∃ r : ℝ, ∀ i, dist p ((t.faceOpposite i).orthogonalProjectionSpan p) = r := by
    refine ⟨dist p ((faceOpposite t i₃).orthogonalProjectionSpan p), ?_⟩
    intro i
    have h : i = i₁ ∨ i = i₂ ∨ i = i₃ := by clear! p t; decide +revert
    rcases h with rfl | rfl | rfl <;> grind