awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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 : ℕ
s : Simplex ℝ P n
he : s.Equilateral
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ π / 3 < π / 2
have linarith : π / 2 ≤ π / 3 → 2 / 2 = 1
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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 : ℕ
s : Simplex ℝ P n
he : s.Equilateral
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
linarith : π / 2 ≤ π / 3 → 2 / 2 = 1
⊢ π / 3 < π / 2
have linarith₁ : π / 2 ≤ π / 3 → HMul.hMul (α := ℝ) 3 2 = 6
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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 : ℕ
s : Simplex ℝ P n
he : s.Equilateral
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
linarith : π / 2 ≤ π / 3 → 2 / 2 = 1
linarith₁ : π / 2 ≤ π / 3 → HMul.hMul (α := ℝ) 3 2 = 6
⊢ π / 3 < π / 2
have linarith₂ : π / 2 ≤ π / 3 → 3 / 3 = 1
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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 : ℕ
s : Simplex ℝ P n
he : s.Equilateral
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
linarith : π / 2 ≤ π / 3 → 2 / 2 = 1
linarith₁ : π / 2 ≤ π / 3 → HMul.hMul (α := ℝ) 3 2 = 6
linarith₂ : π / 2 ≤ π / 3 → 3 / 3 = 1
⊢ π / 3 < π / 2
have linarith₃ : π / 2 ≤ π / 3 → HMul.hMul (α := ℝ) 2 3 = 6
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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 : ℕ
s : Simplex ℝ P n
he : s.Equilateral
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
linarith : π / 2 ≤ π / 3 → 2 / 2 = 1
linarith₁ : π / 2 ≤ π / 3 → HMul.hMul (α := ℝ) 3 2 = 6
linarith₂ : π / 2 ≤ π / 3 → 3 / 3 = 1
linarith₃ : π / 2 ≤ π / 3 → HMul.hMul (α := ℝ) 2 3 = 6
⊢ π / 3 < π / 2
have linarith₄ : π / 2 ≤ π / 3 → GT.gt (α := ℝ) 6 0
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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 : ℕ
s : Simplex ℝ P n
he : s.Equilateral
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
linarith : π / 2 ≤ π / 3 → 2 / 2 = 1
linarith₁ : π / 2 ≤ π / 3 → HMul.hMul (α := ℝ) 3 2 = 6
linarith₂ : π / 2 ≤ π / 3 → 3 / 3 = 1
linarith₃ : π / 2 ≤ π / 3 → HMul.hMul (α := ℝ) 2 3 = 6
linarith₄ : π / 2 ≤ π / 3 → GT.gt (α := ℝ) 6 0
⊢ π / 3 < π / 2
have linarith₅ : π / 2 ≤ π / 3 → 3 * π - 2 * π + (0 - π) = 0
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
i : Fin (n + 1)
⊢ dist (s.points i) s.centroid = (↑n : ℝ) * dist s.centroid (s.faceOppositeCentroid i)
have simp_rw : ‖s.points i -ᵥ s.centroid‖ = (↑n : ℝ) * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖
Tactic: simp_rw [dist_eq_norm_vsub, s.point_vsub_centroid_eq_smul_vsub i, norm_smul, Real.norm_natCast]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
i : Fin (n + 1)
simp_rw : ‖s.points i -ᵥ s.centroid‖ = (↑n : ℝ) * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖
⊢ dist (s.points i) s.centroid = (↑n : ℝ) * dist s.centroid (s.faceOppositeCentroid i)
have simp_rw₁ : ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.centroid -ᵥ s.faceOppositeCentroid i)‖ =
  (↑n : ℝ) * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖
Tactic: simp_rw [dist_eq_norm_vsub, s.point_vsub_centroid_eq_smul_vsub i, norm_smul, Real.norm_natCast]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
i : Fin (n + 1)
simp_rw : ‖s.points i -ᵥ s.centroid‖ = (↑n : ℝ) * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖
simp_rw₁ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.centroid -ᵥ s.faceOppositeCentroid i)‖ =
    (↑n : ℝ) * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖
⊢ dist (s.points i) s.centroid = (↑n : ℝ) * dist s.centroid (s.faceOppositeCentroid i)
have simp_rw₂ : norm (E := ℝ) (↑n : ℝ) * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖ = (↑n : ℝ) * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖
Tactic: simp_rw [dist_eq_norm_vsub, s.point_vsub_centroid_eq_smul_vsub i, norm_smul, Real.norm_natCast]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
i : Fin (n + 1)
⊢ dist (s.points i) (s.faceOppositeCentroid i) =
    HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * dist s.centroid (s.faceOppositeCentroid i)
have simp_rw : ‖HAdd.hAdd (α := ℝ) (↑n : ℝ) 1‖ * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖ =
  HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖
Tactic: simp_rw [dist_eq_norm_vsub, s.point_vsub_faceOppositeCentroid_eq_smul_vsub i,
    norm_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
i : Fin (n + 1)
⊢ ‖HAdd.hAdd (α := ℝ) (↑n : ℝ) 1‖ * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖ =
    HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖
have norm_cast : (↑(n + 1) : ℝ) * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖ = (↑(n + 1) : ℝ) * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
⊢ Simplex.AcuteAngled t ↔
    ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
      ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
have refine : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2 →
  ∀ (h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2) (h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2)
    (h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2), Simplex.AcuteAngled t
Tactic: refine ⟨fun h ↦ ⟨h _ _ _ (by decide) (by decide) (by decide),
                   h _ _ _ (by decide) (by decide) (by decide),
                   h _ _ _ (by decide) (by decide) (by decide)⟩,
          fun ⟨h012, h120, h201⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
⊢ Simplex.AcuteAngled t
have h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
Tactic: have h210 := angle_comm (t.points 0) _ _ ▸ h012
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
⊢ Simplex.AcuteAngled t
have h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
Tactic: have h021 := angle_comm (t.points 1) _ _ ▸ h120
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
⊢ Simplex.AcuteAngled t
have h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
Tactic: have h102 := angle_comm (t.points 2) _ _ ▸ h201
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₁ i₂ i₃ : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∠ (t.points i₁) (t.points i₂) (t.points i₃) < π / 2
have 0 : ∀ (h₁₂ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩ ≠ i₂)
  (h₁₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩ ≠ i₃),
  ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₂)
      (t.points i₃) <
    π / 2
Tactic: fin_cases i₁
Cleared hypotheses: i₁, h₁₂, h₁₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₁ i₂ i₃ : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
0 :
  ∀ (h₁₂ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ ≠ i₂)
    (h₁₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ ≠ i₃),
    ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₂)
        (t.points i₃) <
      π / 2
⊢ ∠ (t.points i₁) (t.points i₂) (t.points i₃) < π / 2
have 1 : ∀ (h₁₂ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩ ≠ i₂)
  (h₁₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩ ≠ i₃),
  ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₂)
      (t.points i₃) <
    π / 2
Tactic: fin_cases i₁
Cleared hypotheses: i₁, h₁₂, h₁₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₁ i₂ i₃ : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
0 :
  ∀ (h₁₂ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ ≠ i₂)
    (h₁₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ ≠ i₃),
    ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₂)
        (t.points i₃) <
      π / 2
1 :
  ∀ (h₁₂ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ ≠ i₂)
    (h₁₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ ≠ i₃),
    ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₂)
        (t.points i₃) <
      π / 2
⊢ ∠ (t.points i₁) (t.points i₂) (t.points i₃) < π / 2
have 2 : ∀ (h₁₂ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩ ≠ i₂)
  (h₁₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩ ≠ i₃),
  ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₂)
      (t.points i₃) <
    π / 2
Tactic: fin_cases i₁
Cleared hypotheses: i₁, h₁₂, h₁₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₂ i₃ : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₂₃ : i₂ ≠ i₃
h₁₂ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ ≠ i₂
h₁₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ ≠ i₃
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₂)
      (t.points i₃) <
    π / 2
have 0 : ∀ (h₂₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩ ≠ i₃)
  (h₁₂ :
    Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩)),
  ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₃) <
    π / 2
Tactic: fin_cases i₂
Cleared hypotheses: i₂, h₂₃, h₁₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₂ i₃ : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₂₃ : i₂ ≠ i₃
h₁₂ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ ≠ i₂
h₁₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ ≠ i₃
0 :
  ∀ (h₂₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ ≠ i₃)
    (h₁₂ :
      Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)),
    ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points i₃) <
      π / 2
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₂)
      (t.points i₃) <
    π / 2
have 0₁ : ∀ (h₂₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩ ≠ i₃)
  (h₁₂ :
    Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩)),
  ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₃) <
    π / 2
Tactic: fin_cases i₂
Cleared hypotheses: i₂, h₂₃, h₁₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₂ i₃ : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₂₃ : i₂ ≠ i₃
h₁₂ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ ≠ i₂
h₁₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ ≠ i₃
0 :
  ∀ (h₂₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ ≠ i₃)
    (h₁₂ :
      Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)),
    ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points i₃) <
      π / 2
h_1 :
  ∀ (h₂₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ ≠ i₃)
    (h₁₂ :
      Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)),
    ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points i₃) <
      π / 2
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₂)
      (t.points i₃) <
    π / 2
have 0₁ : ∀ (h₂₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩ ≠ i₃)
  (h₁₂ :
    Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩)),
  ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₃) <
    π / 2
Tactic: fin_cases i₂
Cleared hypotheses: i₂, h₂₃, h₁₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₂ i₃ : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₂₃ : i₂ ≠ i₃
h₁₂ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ ≠ i₂
h₁₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ ≠ i₃
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₂)
      (t.points i₃) <
    π / 2
have 1 : ∀ (h₂₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩ ≠ i₃)
  (h₁₂ :
    Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩)),
  ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₃) <
    π / 2
Tactic: fin_cases i₂
Cleared hypotheses: i₂, h₂₃, h₁₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Simplex (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
t : Triangle ℝ P
h :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₂ i₃ : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₂₃ : i₂ ≠ i₃
h₁₂ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ ≠ i₂
h₁₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ ≠ i₃
1 :
  ∀ (h₂₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ ≠ i₃)
    (h₁₂ :
      Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)),
    ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points i₃) <
      π / 2
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₂)
      (t.points i₃) <
    π / 2
have 1₁ : ∀ (h₂₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩ ≠ i₃)
  (h₁₂ :
    Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩)),
  ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₃) <
    π / 2
Tactic: fin_cases i₂
Cleared hypotheses: i₂, h₂₃, h₁₂