awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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
hij :
  ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
⊢ Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)

Tactic:
simp_all
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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 :
  ![t.points i₁, t.points i₂, t.points 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)
⊢ AffineIndependent ℝ ![t.points i₁, t.points i₂, t.points i₃]

Tactic:
convert!
      t.independent.comp_embedding
        ⟨![i₁, i₂, i₃], by
          intro i j hij
          fin_cases i <;> fin_cases j <;> simp_all⟩

Premises used: AffineIndependent.comp_embedding, Function.Embedding.mk, Matrix.vecEmpty, Affine.Simplex.independent, Matrix.vecCons
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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 :
  ∀ (i : Fin (Nat.succ 0).succ.succ),
    ![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
⊢ ![t.points i₁, t.points i₂, t.points 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)

Tactic:
ext i
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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, ⋯⟩)
h₂ :
  ![t.points i₁, t.points i₂, t.points i₃]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : 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) ⟨2, ⋯⟩)
⊢ ![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

Tactic:
fin_cases i
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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
⊢ ![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, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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
⊢ ![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, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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
⊢ ![t.points i₁, t.points i₂, t.points i₃]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : 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) ⟨2, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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
⊢ 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
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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₃]
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)
⊢ 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₃))

Tactic:
rw [orthogonalProjectionSpan, orthogonalProjectionSpan,
    ← dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq ha]

Premises used: Affine.Simplex.orthogonalProjectionSpan, EuclideanGeometry.dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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₃]
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)
⊢ 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:
simp only [range_faceOpposite_points]

Premises used: Affine.Simplex.range_faceOpposite_points
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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₃]
⊢ Eq (α := Set (Fin 3)) {i₃}ᶜ {i₁, i₂}

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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₃]
⊢ Eq (α := Set (Fin 3)) {i₂}ᶜ {i₁, i₃}

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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₂)
rw₃ : dist (excenter t signs) (touchpoint t signs i₂) = dist (excenter t signs) (touchpoint t signs i₂)
i₄ : Fin (HAdd.hAdd (α := ℕ) 2 1)
rw₄ : dist (excenter t signs) (touchpoint t signs i₂) = dist (excenter t signs) (touchpoint t signs i₂)
i₅ : Fin (HAdd.hAdd (α := ℕ) 2 1)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₂) (t.points i₁) (excenter t signs)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (excenter t signs) (t.points i₁) (t.points 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]

Premises used: Affine.Simplex.ExcenterExists.dist_excenter_eq_dist_excenter, Affine.Simplex.touchpoint, Affine.Triangle.excenterExists, Affine.Triangle.dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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₃
rw : ∡ (touchpoint t ∅ i₃) (t.points i₁) (incenter t) = ∡ (incenter t) (t.points i₁) (touchpoint t ∅ i₂)
⊢ ∡ (t.points i₂) (t.points i₁) (incenter t) = ∡ (incenter t) (t.points i₁) (t.points i₃)

Tactic:
rw [← (t.sbtw_touchpoint_empty h₁₃ h₁₂ h₂₃.symm).oangle_eq_left,
    ← (t.sbtw_touchpoint_empty h₁₂ h₁₃ h₂₃).oangle_eq_right]

Premises used: Ne.symm, Sbtw.oangle_eq_right, Affine.Triangle.sbtw_touchpoint_empty, Sbtw.oangle_eq_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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₃
⊢ dist (incenter t) (touchpoint t ∅ i₃) = dist (incenter t) (touchpoint t ∅ i₂)

Tactic:
have hd := t.dist_incenter_eq_dist_incenter i₃ i₂
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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₂)
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)
⊢ ∡ (touchpoint t ∅ i₃) (t.points i₁) (incenter t) = ∡ (incenter t) (t.points i₁) (touchpoint t ∅ i₂)

Tactic:
simp_rw [touchpoint, orthogonalProjectionSpan] at hd ⊢

Premises used: Affine.Simplex.orthogonalProjectionSpan, Affine.Simplex.touchpoint
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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)
⊢ ∡
      (↑((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:
oangle_eq_of_dist_orthogonalProjection_eq (mem_affineSpan _ ?_) (mem_affineSpan _ ?_)
    (t.touchpoint_empty_injective.ne h₂₃.symm) hd

Premises used: Affine.Simplex.touchpoint_empty_injective, Set.Mem, Affine.Simplex.incenter, Function.Injective.ne, mem_affineSpan, Ne.symm, EuclideanGeometry.oangle_eq_of_dist_orthogonalProjection_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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)
refine_1 : ∃ (x : Fin 3), ¬x = i₃ ∧ t.points x = t.points i₁
⊢ t.points i₁ ∈ Set.range (faceOpposite t i₃).points

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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)
⊢ ∃ (x : Fin 3), ¬x = i₃ ∧ t.points x = t.points i₁

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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)
refine_2 : ∃ (x : Fin 3), ¬x = i₂ ∧ t.points x = t.points i₁
⊢ t.points i₁ ∈ Set.range (faceOpposite t i₂).points

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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)
⊢ ∃ (x : Fin 3), ¬x = i₂ ∧ t.points x = t.points i₁

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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₃
rw : ∡ (touchpoint t {i₁} i₃) (t.points i₁) (excenter t {i₁}) = ∡ (excenter t {i₁}) (t.points i₁) (touchpoint t {i₁} i₂)
⊢ ∡ (t.points i₂) (t.points i₁) (excenter t {i₁}) = ∡ (excenter t {i₁}) (t.points i₁) (t.points 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]

Premises used: Affine.Triangle.touchpoint_singleton_sbtw, Ne.symm, Sbtw.oangle_eq_right, Sbtw.symm, Sbtw.oangle_eq_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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₃
⊢ 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₂
-- Module: Mathlib.Geometry.Euclidean.Angle.Incenter
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₂)
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)
⊢ ∡ (touchpoint t {i₁} i₃) (t.points i₁) (excenter t {i₁}) = ∡ (excenter t {i₁}) (t.points i₁) (touchpoint t {i₁} i₂)

Tactic:
simp_rw [touchpoint, orthogonalProjectionSpan] at hd ⊢

Premises used: Affine.Simplex.orthogonalProjectionSpan, Affine.Simplex.touchpoint