awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Simplex
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₃
rcases :
  ∀ (r : ℝ) (hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r),
    ∠ (s.points i₁) (s.points i₂) (s.points i₃) = π / 3
⊢ ∠ (s.points i₁) (s.points i₂) (s.points i₃) = π / 3

Tactic:
rcases he with ⟨r, hr⟩
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r
rw :
  Real.arccos
      ((‖s.points i₁ -ᵥ s.points i₂‖ * ‖s.points i₁ -ᵥ s.points i₂‖ +
              ‖s.points i₃ -ᵥ s.points i₂‖ * ‖s.points i₃ -ᵥ s.points i₂‖ -
            ‖s.points i₁ -ᵥ s.points i₂ - (s.points i₃ -ᵥ s.points i₂)‖ *
              ‖s.points i₁ -ᵥ s.points i₂ - (s.points i₃ -ᵥ s.points i₂)‖) /
          2 /
        (‖s.points i₁ -ᵥ s.points i₂‖ * ‖s.points i₃ -ᵥ s.points i₂‖)) =
    π / 3
⊢ ∠ (s.points i₁) (s.points i₂) (s.points i₃) = π / 3

Tactic:
rw [angle, InnerProductGeometry.angle,
    real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two]

Premises used: InnerProductGeometry.angle, real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r
linarith : π / 3 < 0 → 3 / 3 = 1
linarith₁ : π / 3 < 0 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π / 3 < 0 → GT.gt (α := ℝ) 3 0
linarith₃ : π / 3 < 0 → 1 * π - HMul.hMul (α := ℝ) 3 0 + (0 - π) = 0
⊢ 0 ≤ π / 3

Tactic:
linarith [Real.pi_nonneg]

Premises used: Real.pi_nonneg
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r
linarith : π < π / 3 → 3 / 3 = 1
linarith₁ : π < π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π < π / 3 → GT.gt (α := ℝ) 3 0
linarith₃ : π < π / 3 → 3 * π - 1 * π + 2 * (0 - π) = 0
linarith₄ : π < π / 3 → GT.gt (α := ℝ) 2 0
⊢ π / 3 ≤ π

Tactic:
linarith [Real.pi_nonneg]

Premises used: Real.pi_nonneg
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r
refine :
  (‖s.points i₁ -ᵥ s.points i₂‖ * ‖s.points i₁ -ᵥ s.points i₂‖ +
            ‖s.points i₃ -ᵥ s.points i₂‖ * ‖s.points i₃ -ᵥ s.points i₂‖ -
          ‖s.points i₁ -ᵥ s.points i₂ - (s.points i₃ -ᵥ s.points i₂)‖ *
            ‖s.points i₁ -ᵥ s.points i₂ - (s.points i₃ -ᵥ s.points i₂)‖) /
        2 /
      (‖s.points i₁ -ᵥ s.points i₂‖ * ‖s.points i₃ -ᵥ s.points i₂‖) =
    Real.cos (π / 3)
⊢ Real.arccos
      ((‖s.points i₁ -ᵥ s.points i₂‖ * ‖s.points i₁ -ᵥ s.points i₂‖ +
              ‖s.points i₃ -ᵥ s.points i₂‖ * ‖s.points i₃ -ᵥ s.points i₂‖ -
            ‖s.points i₁ -ᵥ s.points i₂ - (s.points i₃ -ᵥ s.points i₂)‖ *
              ‖s.points i₁ -ᵥ s.points i₂ - (s.points i₃ -ᵥ s.points i₂)‖) /
          2 /
        (‖s.points i₁ -ᵥ s.points i₂‖ * ‖s.points i₃ -ᵥ s.points i₂‖)) =
    π / 3

Tactic:
refine Real.arccos_eq_of_eq_cos (by linarith [Real.pi_nonneg]) (by linarith [Real.pi_nonneg]) ?_

Premises used: Real.arccos_eq_of_eq_cos
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r
simp : (r * r + r * r - r * r) / 2 / (r * r) = 1 / 2
⊢ (‖s.points i₁ -ᵥ s.points i₂‖ * ‖s.points i₁ -ᵥ s.points i₂‖ +
            ‖s.points i₃ -ᵥ s.points i₂‖ * ‖s.points i₃ -ᵥ s.points i₂‖ -
          ‖s.points i₁ -ᵥ s.points i₂ - (s.points i₃ -ᵥ s.points i₂)‖ *
            ‖s.points i₁ -ᵥ s.points i₂ - (s.points i₃ -ᵥ s.points i₂)‖) /
        2 /
      (‖s.points i₁ -ᵥ s.points i₂‖ * ‖s.points i₃ -ᵥ s.points i₂‖) =
    Real.cos (π / 3)

Tactic:
simp only [vsub_sub_vsub_cancel_right, ← dist_eq_norm_vsub, hr _ _ h₁₂, hr _ _ h₁₃,
    hr _ _ h₂₃.symm, Real.cos_pi_div_three]

Premises used: Ne.symm, vsub_sub_vsub_cancel_right, dist_eq_norm_vsub, Real.cos_pi_div_three
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = 0
⊢ dist (s.points i₁) (s.points i₂) = 0

Tactic:
replace hr := hr _ _ h₁₂
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hr : dist (s.points i₁) (s.points i₂) = 0
⊢ s.points i₁ = s.points i₂

Tactic:
rw [dist_eq_zero] at hr

Premises used: dist_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hr : s.points i₁ = s.points i₂
⊢ False

Tactic:
h₁₂ (s.independent.injective hr)

Premises used: AffineIndependent.injective, Affine.Simplex.independent
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hr : s.points i₁ = s.points i₂
⊢ False

Tactic:
exact h₁₂ (s.independent.injective hr)

Premises used: AffineIndependent.injective, Affine.Simplex.independent
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r
⊢ r ≠ 0

Tactic:
have hr0 : r ≠ 0 := by
    rintro rfl
    replace hr := hr _ _ h₁₂
    rw [dist_eq_zero] at hr
    exact h₁₂ (s.independent.injective hr)
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r
hr0 : r ≠ 0
⊢ (r * r + r * r - r * r) / 2 / (r * r) = 1 / 2

Tactic:
field
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).AcuteAngled ↔ s.AcuteAngled

Tactic:
⟨fun h {i₁ i₂ i₃} h₁₂ h₁₃ h₂₃ ↦ ?_, fun h {i₁ i₂ i₃} h₁₂ h₁₃ h₂₃ ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
refine_1 :
  ∀ (h : (s.reindex e).AcuteAngled) {i₁ i₂ i₃ : Fin (m + 1)} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃),
    ∠ (s.points i₁) (s.points i₂) (s.points i₃) < π / 2
refine_2 :
  ∀ (h : s.AcuteAngled) {i₁ i₂ i₃ : Fin (n + 1)} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃),
    ∠ ((s.reindex e).points i₁) ((s.reindex e).points i₂) ((s.reindex e).points i₃) < π / 2
⊢ (s.reindex e).AcuteAngled ↔ s.AcuteAngled

Tactic:
refine ⟨fun h {i₁ i₂ i₃} h₁₂ h₁₃ h₂₃ ↦ ?_, fun h {i₁ i₂ i₃} h₁₂ h₁₃ h₂₃ ↦ ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).AcuteAngled
i₁ i₂ i₃ : Fin (m + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∠ ((s.reindex e).points ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₁))
      ((s.reindex e).points ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₂))
      ((s.reindex e).points ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₃)) <
    π / 2

Tactic:
h (i₁ := e i₁) (i₂ := e i₂) (i₃ := e i₃) ?_ ?_ ?_

Premises used: DFunLike.coe
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).AcuteAngled
i₁ i₂ i₃ : Fin (m + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁ :
  ∠ (s.points i₁) (s.points i₂) (s.points i₃) =
    ∠ ((s.reindex e).points ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₁))
      ((s.reindex e).points ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₂))
      ((s.reindex e).points ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₃))
refine_1 :
  Ne (α := Fin (n + 1)) ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₁ : Fin (n + 1))
    ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₂ : Fin (n + 1))
refine_1₁ :
  Ne (α := Fin (n + 1)) ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₁ : Fin (n + 1))
    ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₃ : Fin (n + 1))
refine_1₂ :
  Ne (α := Fin (n + 1)) ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₂ : Fin (n + 1))
    ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₃ : Fin (n + 1))
⊢ ∠ (s.points i₁) (s.points i₂) (s.points i₃) < π / 2

Tactic:
convert! h (i₁ := e i₁) (i₂ := e i₂) (i₃ := e i₃) ?_ ?_ ?_ using 1

Premises used: DFunLike.coe
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).AcuteAngled
i₁ i₂ i₃ : Fin (m + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∠ (s.points i₁) (s.points i₂) (s.points i₃) =
    ∠ ((s.reindex e).points ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₁))
      ((s.reindex e).points ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₂))
      ((s.reindex e).points ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₃))

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).AcuteAngled
i₁ i₂ i₃ : Fin (m + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Ne (α := Fin (n + 1)) ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₁ : Fin (n + 1))
    ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₂ : Fin (n + 1))

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).AcuteAngled
i₁ i₂ i₃ : Fin (m + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Ne (α := Fin (n + 1)) ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₁ : Fin (n + 1))
    ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₃ : Fin (n + 1))

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).AcuteAngled
i₁ i₂ i₃ : Fin (m + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Ne (α := Fin (n + 1)) ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₂ : Fin (n + 1))
    ((e : (a : Fin (m + 1)) → Fin (n + 1)) i₃ : Fin (n + 1))

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : s.AcuteAngled
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∠ (s.points ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i₁))
      (s.points ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i₂))
      (s.points ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i₃)) <
    π / 2

Tactic:
h (i₁ := e.symm i₁) (i₂ := e.symm i₂) (i₃ := e.symm i₃) ?_ ?_ ?_

Premises used: Equiv.symm, DFunLike.coe
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : s.AcuteAngled
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
refine_2 :
  Ne (α := Fin (m + 1)) ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i₁ : Fin (m + 1))
    ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i₂ : Fin (m + 1))
refine_2₁ :
  Ne (α := Fin (m + 1)) ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i₁ : Fin (m + 1))
    ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i₃ : Fin (m + 1))
refine_2₂ :
  Ne (α := Fin (m + 1)) ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i₂ : Fin (m + 1))
    ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i₃ : Fin (m + 1))
⊢ ∠ ((s.reindex e).points i₁) ((s.reindex e).points i₂) ((s.reindex e).points i₃) < π / 2

Tactic:
convert! h (i₁ := e.symm i₁) (i₂ := e.symm i₂) (i₃ := e.symm i₃) ?_ ?_ ?_ using 1

Premises used: Equiv.symm, DFunLike.coe
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : s.AcuteAngled
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Ne (α := Fin (m + 1)) ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i₁ : Fin (m + 1))
    ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i₂ : Fin (m + 1))

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : s.AcuteAngled
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Ne (α := Fin (m + 1)) ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i₁ : Fin (m + 1))
    ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i₃ : Fin (m + 1))

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : s.AcuteAngled
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Ne (α := Fin (m + 1)) ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i₂ : Fin (m + 1))
    ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i₃ : Fin (m + 1))

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Simplex
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₃
rw : π / 3 < π / 2
⊢ ∠ (s.points i₁) (s.points i₂) (s.points i₃) < π / 2

Tactic:
rw [he.angle_eq_pi_div_three h₁₂ h₁₃ h₂₃]

Premises used: Affine.Simplex.Equilateral.angle_eq_pi_div_three
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
linarith₅ : π / 2 ≤ π / 3 → 3 * π - 2 * π + (0 - π) = 0
⊢ π / 3 < π / 2

Tactic:
linarith [Real.pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Geometry.Euclidean.Simplex
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‖
simp_rw₂ :
  norm (E := ℝ) (↑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)

Tactic:
simp_rw [dist_eq_norm_vsub, s.point_vsub_centroid_eq_smul_vsub i, norm_smul, Real.norm_natCast]

Premises used: norm_smul, Real.norm_natCast, Affine.Simplex.point_vsub_centroid_eq_smul_vsub, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Simplex
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 :
  ‖HAdd.hAdd (α := ℝ) (↑n : ℝ) 1‖ * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖ =
    HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖
⊢ dist (s.points i) (s.faceOppositeCentroid i) =
    HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * dist s.centroid (s.faceOppositeCentroid i)

Tactic:
simp_rw [dist_eq_norm_vsub, s.point_vsub_faceOppositeCentroid_eq_smul_vsub i,
    norm_smul]

Premises used: norm_smul, Affine.Simplex.point_vsub_faceOppositeCentroid_eq_smul_vsub, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Simplex
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)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  (↑(n + 1) : ℝ) * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖ = (↑(n + 1) : ℝ) * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖
⊢ ‖HAdd.hAdd (α := ℝ) (↑n : ℝ) 1‖ * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖ =
    HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖s.centroid -ᵥ s.faceOppositeCentroid i‖

Tactic:
norm_cast
-- Module: Mathlib.Geometry.Euclidean.Simplex
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 : Simplex.AcuteAngled t
⊢ Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 1

Tactic:
decide
-- Module: Mathlib.Geometry.Euclidean.Simplex
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 : Simplex.AcuteAngled t
⊢ Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 2

Tactic:
decide
-- Module: Mathlib.Geometry.Euclidean.Simplex
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 : Simplex.AcuteAngled t
⊢ Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 2

Tactic:
decide
-- Module: Mathlib.Geometry.Euclidean.Simplex
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 : Simplex.AcuteAngled t
⊢ Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 0

Tactic:
decide
-- Module: Mathlib.Geometry.Euclidean.Simplex
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 : Simplex.AcuteAngled t
⊢ Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 0

Tactic:
decide
-- Module: Mathlib.Geometry.Euclidean.Simplex
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 : Simplex.AcuteAngled t
⊢ Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 1

Tactic:
decide
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
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
⊢ 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

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⟩ ↦ ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
⊢ ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2

Tactic:
have h210 := angle_comm (t.points 0) _ _ ▸ h012
-- Module: Mathlib.Geometry.Euclidean.Simplex
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
⊢ ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2

Tactic:
have h021 := angle_comm (t.points 1) _ _ ▸ h120