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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ (p' : P),
        Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) p' ∧
          Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₂).points)) p' ∧
            ∠ p p'
                (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
                      p) :
                  P) =
              ∠ p p'
                (↑(((s.faceOpposite i₂).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₂).points)))
                      p) :
                  P)
refine :
  ∀ (i : Fin (n + 1)),
    dist p
        (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
              p) :
          P) =
      dist p
        (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
              p) :
          P)
⊢ ∃ (r : ℝ),
    ∀ (i : Fin (n + 1)),
      dist p
          (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                  (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                p) :
            P) =
        r

Tactic:
refine ⟨dist p ((s.faceOpposite i₁).orthogonalProjectionSpan p), ?_⟩
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ (p' : P),
        Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) p' ∧
          Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₂).points)) p' ∧
            ∠ p p'
                (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
                      p) :
                  P) =
              ∠ p p'
                (↑(((s.faceOpposite i₂).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₂).points)))
                      p) :
                  P)
i : Fin (n + 1)
pos :
  ∀ (hi : i = i₁),
    dist p
        (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
              p) :
          P) =
      dist p
        (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
              p) :
          P)
neg :
  ∀ (hi : ¬i = i₁),
    dist p
        (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
              p) :
          P) =
      dist p
        (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
              p) :
          P)
⊢ dist p
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            p) :
        P) =
    dist p
      (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
            p) :
        P)

Tactic:
by_cases hi : 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ (p' : P),
        Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) p' ∧
          Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₂).points)) p' ∧
            ∠ p p'
                (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
                      p) :
                  P) =
              ∠ p p'
                (↑(((s.faceOpposite i₂).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₂).points)))
                      p) :
                  P)
i : Fin (n + 1)
hi : i = i₁
pos pos₁ :
  dist p
      (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
            p) :
        P) =
    dist p
      (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
            p) :
        P)
⊢ dist p
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            p) :
        P) =
    dist p
      (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
            p) :
        P)

Tactic:
rw [hi]
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ (p' : P),
        Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) p' ∧
          Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₂).points)) p' ∧
            ∠ p p'
                (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
                      p) :
                  P) =
              ∠ p p'
                (↑(((s.faceOpposite i₂).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₂).points)))
                      p) :
                  P)
i : Fin (n + 1)
hi : ¬i = i₁
neg :
  ∀ (p' : P) (hp'₁ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) p')
    (hp'₂ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i).points)) p')
    (ha :
      ∠ p p'
          (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
                  (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
                p) :
            P) =
        ∠ p p'
          (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                  (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                p) :
            P)),
    dist p
        (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
              p) :
          P) =
      dist p
        (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
              p) :
          P)
⊢ dist p
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            p) :
        P) =
    dist p
      (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
            p) :
        P)

Tactic:
obtain ⟨p', hp'₁, hp'₂, ha⟩ := h i hi
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ (p' : P),
        Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) p' ∧
          Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₂).points)) p' ∧
            ∠ p p'
                (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
                      p) :
                  P) =
              ∠ p p'
                (↑(((s.faceOpposite i₂).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₂).points)))
                      p) :
                  P)
i : Fin (n + 1)
hi : ¬i = i₁
p' : P
hp'₁ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) p'
hp'₂ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i).points)) p'
ha :
  ∠ p p'
      (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
            p) :
        P) =
    ∠ p p'
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            p) :
        P)
⊢ dist p
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            p) :
        P) =
    dist p
      (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
            p) :
        P)

Tactic:
((dist_orthogonalProjection_eq_iff_angle_eq hp'₁ hp'₂).2 ha).symm

Premises used: Iff.mpr, Set.Mem, EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq, Eq.symm
-- 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ (p' : P),
        Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) p' ∧
          Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₂).points)) p' ∧
            ∠ p p'
                (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
                      p) :
                  P) =
              ∠ p p'
                (↑(((s.faceOpposite i₂).orthogonalProjectionSpan :
                        (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₂).points)))
                      p) :
                  P)
i : Fin (n + 1)
hi : ¬i = i₁
p' : P
hp'₁ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) p'
hp'₂ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i).points)) p'
ha :
  ∠ p p'
      (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
            p) :
        P) =
    ∠ p p'
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            p) :
        P)
⊢ dist p
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            p) :
        P) =
    dist p
      (↑(((s.faceOpposite i₁).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i₁).points)))
            p) :
        P)

Tactic:
exact ((dist_orthogonalProjection_eq_iff_angle_eq hp'₁ hp'₂).2 ha).symm

Premises used: Iff.mpr, EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq, Eq.symm
-- 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 j : Fin (Nat.succ 0).succ.succ
hij : ![i₁, i₂, i₃] i = ![i₁, i₂, i₃] j
0 :
  ∀
    (hij :
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
        ![i₁, i₂, i₃] j),
    (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩ = j
1 :
  ∀
    (hij :
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
        ![i₁, i₂, i₃] j),
    (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩ = j
2 :
  ∀
    (hij :
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
        ![i₁, i₂, i₃] j),
    (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩ = j
⊢ i = j

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
j : Fin (Nat.succ 0).succ.succ
hij : ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) = ![i₁, i₂, i₃] j
0 :
  ∀
    (hij :
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
        ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)),
    Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h :
  ∀
    (hij :
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
        ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)),
    Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
h_1 :
  ∀
    (hij :
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : 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) ⟨0, ⋯⟩)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
⊢ (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩ = j

Tactic:
fin_cases j
-- 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
j : Fin (Nat.succ 0).succ.succ
hij : ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) = ![i₁, i₂, i₃] j
1 :
  ∀
    (hij :
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
        ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)),
    Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h :
  ∀
    (hij :
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
        ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)),
    Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
h_1 :
  ∀
    (hij :
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : 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) ⟨1, ⋯⟩)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
⊢ (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩ = j

Tactic:
fin_cases j
-- 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
j : Fin (Nat.succ 0).succ.succ
hij : ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) = ![i₁, i₂, i₃] j
2 :
  ∀
    (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) ⟨0, ⋯⟩)),
    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) ⟨0, ⋯⟩)
h :
  ∀
    (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) ⟨1, ⋯⟩)),
    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) ⟨1, ⋯⟩)
h_1 :
  ∀
    (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, ⋯⟩)
⊢ (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩ = j

Tactic:
fin_cases j
-- 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) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)

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
hij :
  ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)

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
hij :
  ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : 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) ⟨0, ⋯⟩)
    ((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
hij :
  ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)

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
hij :
  ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)

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
hij :
  ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : 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) ⟨1, ⋯⟩)
    ((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
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) ⟨0, ⋯⟩)
⊢ 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) ⟨0, ⋯⟩)

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
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) ⟨1, ⋯⟩)
⊢ 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) ⟨1, ⋯⟩)

Tactic:
simp_all