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₃
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)

Tactic:
oangle_eq_of_dist_orthogonalProjection_eq (mem_affineSpan _ ?_) (mem_affineSpan _ ?_)
    ((t.excenterExists_singleton i₁).touchpoint_injective.ne h₂₃.symm) hd

Premises used: Set.Mem, Function.Injective.ne, mem_affineSpan, Ne.symm, EuclideanGeometry.oangle_eq_of_dist_orthogonalProjection_eq, Affine.Simplex.ExcenterExists.touchpoint_injective, Affine.Simplex.excenterExists_singleton
-- 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₁})
      (↑((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
refine_2 : 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)

Tactic:
refine oangle_eq_of_dist_orthogonalProjection_eq (mem_affineSpan _ ?_) (mem_affineSpan _ ?_)
    ((t.excenterExists_singleton i₁).touchpoint_injective.ne h₂₃.symm) hd

Premises used: Function.Injective.ne, mem_affineSpan, Ne.symm, EuclideanGeometry.oangle_eq_of_dist_orthogonalProjection_eq, Affine.Simplex.ExcenterExists.touchpoint_injective, Affine.Simplex.excenterExists_singleton
-- 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₁})
      (↑((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 : ∃ (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 (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)
⊢ ∃ (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 (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_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 (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)
⊢ ∃ (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₃) + (↑π : Real.Angle)

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]

Premises used: Sbtw.oangle_eq_add_pi_left, Affine.Triangle.sbtw_touchpoint_singleton, Affine.Triangle.touchpoint_singleton_sbtw, Ne.symm, add_left_inj, Sbtw.oangle_eq_right, Sbtw.symm, Affine.Simplex.excenterExists_singleton, Affine.Simplex.ExcenterExists.excenter_ne_point
-- 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
-- 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₁})
      (↑((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)

Tactic:
oangle_eq_of_dist_orthogonalProjection_eq (mem_affineSpan _ ?_) (mem_affineSpan _ ?_)
    ((t.excenterExists_singleton i₁).touchpoint_injective.ne h₁₃.symm) hd

Premises used: Set.Mem, Function.Injective.ne, mem_affineSpan, Ne.symm, EuclideanGeometry.oangle_eq_of_dist_orthogonalProjection_eq, Affine.Simplex.ExcenterExists.touchpoint_injective, Affine.Simplex.excenterExists_singleton
-- 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₁})
      (↑((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
refine_2 : 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)

Tactic:
refine oangle_eq_of_dist_orthogonalProjection_eq (mem_affineSpan _ ?_) (mem_affineSpan _ ?_)
    ((t.excenterExists_singleton i₁).touchpoint_injective.ne h₁₃.symm) hd

Premises used: Function.Injective.ne, mem_affineSpan, Ne.symm, EuclideanGeometry.oangle_eq_of_dist_orthogonalProjection_eq, Affine.Simplex.ExcenterExists.touchpoint_injective, Affine.Simplex.excenterExists_singleton
-- 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₁})
      (↑((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 : ∃ (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 (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)
⊢ ∃ (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 (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_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 (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)
⊢ ∃ (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₃
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₁))
⊢ 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₁

Premises used: 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₃
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₁))
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)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₃) (t.points i₂) p) = HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁))

Tactic:
rw [← dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃] at h₁

Premises used: 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₃
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₁))
⊢ 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₂

Premises used: Ne.symm, 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₃
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) ⊤ p

Tactic:
AffineSubspace.mem_top ℝ V p

Premises used: Real, AffineSubspace.mem_top
-- 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₁ :
  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)
h : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) ⊤
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) p

Tactic:
convert! AffineSubspace.mem_top ℝ V p

Premises used: Real, AffineSubspace.mem_top