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₃
p : P
i : Fin (Nat.succ 0).succ.succ
h :
  ![t.points i₁, t.points i₂, t.points i₃]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    Function.comp (α := Fin (Nat.succ 0).succ.succ) t.points
      (⇑{ toFun := ![i₁, i₂, i₃], inj' := ⋯ : Fin (Nat.succ 0).succ.succ ↪ Fin 3 } :
        (a : Fin (Nat.succ 0).succ.succ) → Fin 3)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ ![t.points i₁, t.points i₂, t.points i₃] i =
    (t.points ∘
        (⇑{ toFun := ![i₁, i₂, i₃], inj' := ⋯ : Fin (Nat.succ 0).succ.succ ↪ Fin 3 } :
          (a : Fin (Nat.succ 0).succ.succ) → Fin 3))
      i
have h₁ : ![t.points i₁, t.points i₂, t.points i₃]
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  Function.comp (α := Fin (Nat.succ 0).succ.succ) t.points
    (⇑{ toFun := ![i₁, i₂, i₃], inj' := sorry : Fin (Nat.succ 0).succ.succ ↪ Fin 3 } :
      (a : Fin (Nat.succ 0).succ.succ) → Fin 3)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: 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₃
p : P
i : Fin (Nat.succ 0).succ.succ
h :
  ![t.points i₁, t.points i₂, t.points i₃]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    Function.comp (α := Fin (Nat.succ 0).succ.succ) t.points
      (⇑{ toFun := ![i₁, i₂, i₃], inj' := ⋯ : Fin (Nat.succ 0).succ.succ ↪ Fin 3 } :
        (a : Fin (Nat.succ 0).succ.succ) → Fin 3)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₁ :
  ![t.points i₁, t.points i₂, t.points i₃]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    Function.comp (α := Fin (Nat.succ 0).succ.succ) t.points
      (⇑{ toFun := ![i₁, i₂, i₃], inj' := ⋯ : Fin (Nat.succ 0).succ.succ ↪ Fin 3 } :
        (a : Fin (Nat.succ 0).succ.succ) → Fin 3)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ ![t.points i₁, t.points i₂, t.points i₃] i =
    (t.points ∘
        (⇑{ toFun := ![i₁, i₂, i₃], inj' := ⋯ : Fin (Nat.succ 0).succ.succ ↪ Fin 3 } :
          (a : Fin (Nat.succ 0).succ.succ) → Fin 3))
      i
have h₂ : ![t.points i₁, t.points i₂, t.points i₃]
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  Function.comp (α := Fin (Nat.succ 0).succ.succ) t.points
    (⇑{ toFun := ![i₁, i₂, i₃], inj' := sorry : Fin (Nat.succ 0).succ.succ ↪ Fin 3 } :
      (a : Fin (Nat.succ 0).succ.succ) → Fin 3)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- 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
⊢ 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) ↔
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₂) (t.points i₁) p) = HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₁) (t.points i₃))
have ha : AffineIndependent ℝ ![t.points i₁, t.points i₂, t.points i₃]
Tactic: have ha : AffineIndependent ℝ ![t.points i₁, t.points i₂, t.points i₃] := by
    convert!
      t.independent.comp_embedding
        ⟨![i₁, i₂, i₃], by
          intro i j hij
          fin_cases i <;> fin_cases j <;> simp_all⟩
    ext i
    fin_cases i <;> rfl
-- 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
ha : AffineIndependent ℝ ![t.points i₁, t.points i₂, t.points 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) ↔
    HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₂) (t.points i₁) p) = HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₁) (t.points i₃))
have rw : dist p
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            p) :
        P) =
    dist p
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₂).points)))
            p) :
        P) ↔
  dist p
      (↑((orthogonalProjection (affineSpan ℝ {t.points i₁, t.points i₂}) :
              (a : P) → ↥(affineSpan ℝ {t.points i₁, t.points i₂}))
            p) :
        P) =
    dist p
      (↑((orthogonalProjection (affineSpan ℝ {t.points i₁, t.points i₃}) :
              (a : P) → ↥(affineSpan ℝ {t.points i₁, t.points i₃}))
            p) :
        P)
Tactic: rw [orthogonalProjectionSpan, orthogonalProjectionSpan,
    ← dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq ha]
-- 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
ha : AffineIndependent ℝ ![t.points i₁, t.points i₂, t.points i₃]
⊢ dist p
        (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points)) :
                (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
              p) :
          P) =
      dist p
        (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points)) :
                (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₂).points)))
              p) :
          P) ↔
    dist p
        (↑((orthogonalProjection (affineSpan ℝ {t.points i₁, t.points i₂}) :
                (a : P) → ↥(affineSpan ℝ {t.points i₁, t.points i₂}))
              p) :
          P) =
      dist p
        (↑((orthogonalProjection (affineSpan ℝ {t.points i₁, t.points i₃}) :
                (a : P) → ↥(affineSpan ℝ {t.points i₁, t.points i₃}))
              p) :
          P)
have simp : dist p
      (↑((orthogonalProjection (affineSpan ℝ (t.points '' {i₃}ᶜ)) : (a : P) → ↥(affineSpan ℝ (t.points '' {i₃}ᶜ))) p) :
        P) =
    dist p
      (↑((orthogonalProjection (affineSpan ℝ (t.points '' {i₂}ᶜ)) : (a : P) → ↥(affineSpan ℝ (t.points '' {i₂}ᶜ))) p) :
        P) ↔
  dist p
      (↑((orthogonalProjection (affineSpan ℝ {t.points i₁, t.points i₂}) :
              (a : P) → ↥(affineSpan ℝ {t.points i₁, t.points i₂}))
            p) :
        P) =
    dist p
      (↑((orthogonalProjection (affineSpan ℝ {t.points i₁, t.points i₃}) :
              (a : P) → ↥(affineSpan ℝ {t.points i₁, t.points i₃}))
            p) :
        P)
Tactic: simp only [range_faceOpposite_points]
-- 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₃
signs : Finset (Fin 3)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₂) (t.points i₁) (excenter t signs)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (excenter t signs) (t.points i₁) (t.points i₃))
have rw : dist (excenter t signs)
    (↑(((faceOpposite t i₃).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
          (excenter t signs)) :
      P) =
  dist (excenter t signs)
    (↑(((faceOpposite t i₂).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₂).points)))
          (excenter t signs)) :
      P)
Tactic: rw [← dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃,
    ← touchpoint, ← touchpoint, (t.excenterExists signs).dist_excenter_eq_dist_excenter]
-- 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₃
signs : Finset (Fin 3)
rw :
  dist (excenter t signs)
      (↑(((faceOpposite t i₃).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            (excenter t signs)) :
        P) =
    dist (excenter t signs)
      (↑(((faceOpposite t i₂).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₂).points)))
            (excenter t signs)) :
        P)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₂) (t.points i₁) (excenter t signs)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (excenter t signs) (t.points i₁) (t.points i₃))
have rw₁ : dist (excenter t signs) (touchpoint t signs i₃) =
  dist (excenter t signs)
    (↑(((faceOpposite t i₂).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₂).points)))
          (excenter t signs)) :
      P)
Tactic: rw [← dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃,
    ← touchpoint, ← touchpoint, (t.excenterExists signs).dist_excenter_eq_dist_excenter]
-- 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₃
signs : Finset (Fin 3)
rw :
  dist (excenter t signs)
      (↑(((faceOpposite t i₃).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            (excenter t signs)) :
        P) =
    dist (excenter t signs)
      (↑(((faceOpposite t i₂).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₂).points)))
            (excenter t signs)) :
        P)
rw₁ :
  dist (excenter t signs) (touchpoint t signs i₃) =
    dist (excenter t signs)
      (↑(((faceOpposite t i₂).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₂).points)))
            (excenter t signs)) :
        P)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₂) (t.points i₁) (excenter t signs)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (excenter t signs) (t.points i₁) (t.points i₃))
have rw₂ : dist (excenter t signs) (touchpoint t signs i₃) = dist (excenter t signs) (touchpoint t signs i₂)
Tactic: rw [← dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃,
    ← touchpoint, ← touchpoint, (t.excenterExists signs).dist_excenter_eq_dist_excenter]
-- 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₃
signs : Finset (Fin 3)
rw :
  dist (excenter t signs)
      (↑(((faceOpposite t i₃).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            (excenter t signs)) :
        P) =
    dist (excenter t signs)
      (↑(((faceOpposite t i₂).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₂).points)))
            (excenter t signs)) :
        P)
rw₁ :
  dist (excenter t signs) (touchpoint t signs i₃) =
    dist (excenter t signs)
      (↑(((faceOpposite t i₂).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₂).points)))
            (excenter t signs)) :
        P)
rw₂ : dist (excenter t signs) (touchpoint t signs i₃) = dist (excenter t signs) (touchpoint t signs i₂)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₂) (t.points i₁) (excenter t signs)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (excenter t signs) (t.points i₁) (t.points i₃))
have rw₃ : dist (excenter t signs) (touchpoint t signs i₂) = dist (excenter t signs) (touchpoint t signs i₂)
Tactic: rw [← dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃,
    ← touchpoint, ← touchpoint, (t.excenterExists signs).dist_excenter_eq_dist_excenter]
-- 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₁) (incenter t) = ∡ (incenter t) (t.points i₁) (t.points i₃)
have rw : ∡ (touchpoint t ∅ i₃) (t.points i₁) (incenter t) = ∡ (incenter t) (t.points i₁) (touchpoint t ∅ i₂)
Tactic: rw [← (t.sbtw_touchpoint_empty h₁₃ h₁₂ h₂₃.symm).oangle_eq_left,
    ← (t.sbtw_touchpoint_empty h₁₂ h₁₃ h₂₃).oangle_eq_right]
-- 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₃) (t.points i₁) (incenter t) = ∡ (incenter t) (t.points i₁) (touchpoint t ∅ i₂)
have hd : dist (incenter t) (touchpoint t ∅ i₃) = dist (incenter t) (touchpoint t ∅ i₂)
Tactic: have hd := t.dist_incenter_eq_dist_incenter 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 (incenter t) (touchpoint t ∅ i₃) = dist (incenter t) (touchpoint t ∅ i₂)
⊢ ∡ (touchpoint t ∅ i₃) (t.points i₁) (incenter t) = ∡ (incenter t) (t.points i₁) (touchpoint t ∅ i₂)
have simp_rw : ∡
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
          (excenter t ∅)) :
      P)
    (t.points i₁) (incenter t) =
  ∡ (incenter t) (t.points i₁)
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₂).points)))
          (excenter t ∅)) :
      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 (incenter t)
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            (excenter t ∅)) :
        P) =
    dist (incenter t)
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₂).points)))
            (excenter t ∅)) :
        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 (incenter t)
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            (excenter t ∅)) :
        P) =
    dist (incenter t)
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₂).points)))
            (excenter t ∅)) :
        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₃)
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_left,
    (t.touchpoint_singleton_sbtw h₁₂ h₁₃ h₂₃).symm.oangle_eq_right]
-- 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