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
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)
⊢ 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)
have 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)
Tactic: by_cases hi : 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
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₁
⊢ 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)
have 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)
Tactic: rw [hi]
-- 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
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₁
⊢ 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)
have 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)
Tactic: obtain ⟨p', hp'₁, hp'₂, ha⟩ := h i hi
-- 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 j : Fin (Nat.succ 0).succ.succ
hij : ![i₁, i₂, i₃] i = ![i₁, i₂, i₃] j
⊢ i = j
have 0 : ∀
  (hij :
    ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) = ![i₁, i₂, i₃] j),
  (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩ = j
Tactic: fin_cases i
Cleared hypotheses: i, hij
-- 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 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
⊢ i = j
have 1 : ∀
  (hij :
    ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) = ![i₁, i₂, i₃] j),
  (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩ = j
Tactic: fin_cases i
Cleared hypotheses: i, hij
-- 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 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
⊢ i = j
have 2 : ∀
  (hij :
    ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) = ![i₁, i₂, i₃] j),
  (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩ = j
Tactic: fin_cases i
Cleared hypotheses: i, hij
-- 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
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
⊢ (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩ = j
have 0 : ∀
  (hij :
    ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)),
  Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
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, ⋯⟩)
⊢ (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩ = j
have 0₁ : ∀
  (hij :
    ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)),
  Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
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, ⋯⟩)
⊢ (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩ = j
have 0₁ : ∀
  (hij :
    ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)),
  Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
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
⊢ (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩ = j
have 1 : ∀
  (hij :
    ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)),
  Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
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, ⋯⟩)
⊢ (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩ = j
have 1₁ : ∀
  (hij :
    ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)),
  Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
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, ⋯⟩)
⊢ (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩ = j
have 1₁ : ∀
  (hij :
    ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)),
  Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
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
⊢ (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩ = j
have 2 : ∀
  (hij :
    ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)),
  Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
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, ⋯⟩)
⊢ (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩ = j
have 2₁ : ∀
  (hij :
    ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)),
  Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
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, ⋯⟩)
⊢ (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩ = j
have 2₁ : ∀
  (hij :
    ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
      ![i₁, i₂, i₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)),
  Eq (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
⊢ AffineIndependent ℝ ![t.points i₁, t.points i₂, t.points i₃]
have h : ![t.points i₁, t.points i₂, t.points i₃] =
  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)
Tactic: convert!
      t.independent.comp_embedding
        ⟨![i₁, i₂, i₃], by
          intro i j hij
          fin_cases i <;> fin_cases j <;> simp_all⟩
-- 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
⊢ ![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)
have 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' := sorry : Fin (Nat.succ 0).succ.succ ↪ Fin 3 } :
          (a : Fin (Nat.succ 0).succ.succ) → Fin 3))
      i
Tactic: ext 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
⊢ ![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) (⟨0, 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) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i