awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Similarity (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
h2 : c' = b'
h_dist_cb : c = b
pos : ∠ a b b = ∠ a' b' c'
⊢ ∠ a b c = ∠ a' b' c'
have pos₁ : ∠ a b b = ∠ a' b' b'
Tactic: simp_rw [h_dist_cb, h2, angle_self_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Similarity (hypothesis)
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
⊢ ∠ a b c = ∠ a' b' c'
have h_cos₁ : Real.cos (∠ a' b' c') = Real.cos (∠ a b c)
Tactic: rw [mul_right_inj' heq] at h_cos
Cleared hypotheses: h_cos, h_cos', heq
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Similarity (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : Real.cos (∠ a' b' c') = Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
⊢ ∠ a b c = ∠ a' b' c'
have neg : ∀ (h_cos : ∠ a' b' c' = ∠ a b c), ∠ a b c = ∠ a' b' c'
Tactic: apply Real.injOn_cos at h_cos
Cleared hypotheses: h_cos
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Similarity (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : Real.cos (∠ a' b' c') = Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
neg : ∀ (h_cos : ∠ a' b' c' = ∠ a b c), ∠ a b c = ∠ a' b' c'
⊢ ∠ a b c = ∠ a' b' c'
have a₁ : ∠ a' b' c' ∈ Set.Icc 0 Real.pi
Tactic: apply Real.injOn_cos at h_cos
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Similarity (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : Real.cos (∠ a' b' c') = Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
neg : ∀ (h_cos : ∠ a' b' c' = ∠ a b c), ∠ a b c = ∠ a' b' c'
a₁ : ∠ a' b' c' ∈ Set.Icc 0 Real.pi
⊢ ∠ a b c = ∠ a' b' c'
have a₂ : ∠ a b c ∈ Set.Icc 0 Real.pi
Tactic: apply Real.injOn_cos at h_cos
-- 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₃
⊢ ∠ (s.points i₁) (s.points i₂) (s.points i₃) = π / 3
have 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
Tactic: rcases he with ⟨r, hr⟩
Cleared hypotheses: he
-- 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
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
⊢ ∠ (s.points i₁) (s.points i₂) (s.points i₃) = π / 3
have 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
Tactic: rw [angle, InnerProductGeometry.angle,
    real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two]
-- 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
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
⊢ 0 ≤ π / 3
have linarith : π / 3 < 0 → 3 / 3 = 1
Tactic: linarith [Real.pi_nonneg]
-- 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
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
⊢ 0 ≤ π / 3
have linarith₁ : π / 3 < 0 → HMul.hMul (α := ℝ) 1 3 = 3
Tactic: linarith [Real.pi_nonneg]
-- 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
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
⊢ 0 ≤ π / 3
have linarith₂ : π / 3 < 0 → GT.gt (α := ℝ) 3 0
Tactic: linarith [Real.pi_nonneg]
-- 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
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
⊢ 0 ≤ π / 3
have linarith₃ : π / 3 < 0 → 1 * π - HMul.hMul (α := ℝ) 3 0 + (0 - π) = 0
Tactic: linarith [Real.pi_nonneg]
-- 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
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
⊢ π / 3 ≤ π
have linarith : π < π / 3 → 3 / 3 = 1
Tactic: linarith [Real.pi_nonneg]
-- 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
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
⊢ π / 3 ≤ π
have linarith₁ : π < π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
Tactic: linarith [Real.pi_nonneg]
-- 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
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
⊢ π / 3 ≤ π
have linarith₂ : π < π / 3 → GT.gt (α := ℝ) 3 0
Tactic: linarith [Real.pi_nonneg]
-- 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
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
⊢ π / 3 ≤ π
have linarith₃ : π < π / 3 → 3 * π - 1 * π + 2 * (0 - π) = 0
Tactic: linarith [Real.pi_nonneg]
-- 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
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
⊢ π / 3 ≤ π
have linarith₄ : π < π / 3 → GT.gt (α := ℝ) 2 0
Tactic: linarith [Real.pi_nonneg]
-- 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
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
⊢ 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
have 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)
Tactic: refine Real.arccos_eq_of_eq_cos (by linarith [Real.pi_nonneg]) (by linarith [Real.pi_nonneg]) ?_
-- 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
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
⊢ (‖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)
have simp : (r * r + r * r - r * r) / 2 / (r * r) = 1 / 2
Tactic: simp only [vsub_sub_vsub_cancel_right, ← dist_eq_norm_vsub, hr _ _ h₁₂, hr _ _ h₁₃,
    hr _ _ h₂₃.symm, Real.cos_pi_div_three]
-- 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
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
⊢ False
have hr₁ : dist (s.points i₁) (s.points i₂) = 0
Tactic: replace hr := hr _ _ h₁₂
Cleared hypotheses: hr
-- 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
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
⊢ False
have hr₁ : s.points i₁ = s.points i₂
Tactic: rw [dist_eq_zero] at hr
Cleared hypotheses: hr
-- 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
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 * r + r * r - r * r) / 2 / (r * r) = 1 / 2
have hr0 : 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)
-- 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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).AcuteAngled ↔ s.AcuteAngled
have 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
Tactic: refine ⟨fun h {i₁ i₂ i₃} h₁₂ h₁₃ h₂₃ ↦ ?_, fun h {i₁ i₂ i₃} h₁₂ 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
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
⊢ (s.reindex e).AcuteAngled ↔ s.AcuteAngled
have 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
Tactic: refine ⟨fun h {i₁ i₂ i₃} h₁₂ h₁₃ h₂₃ ↦ ?_, fun h {i₁ i₂ i₃} h₁₂ 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
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₃) < π / 2
have 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₃))
Tactic: convert! h (i₁ := e i₁) (i₂ := e i₂) (i₃ := e i₃) ?_ ?_ ?_ using 1
-- 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
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₃))
⊢ ∠ (s.points i₁) (s.points i₂) (s.points i₃) < π / 2
have 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))
Tactic: convert! h (i₁ := e i₁) (i₂ := e i₂) (i₃ := e i₃) ?_ ?_ ?_ using 1
-- 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
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))
⊢ ∠ (s.points i₁) (s.points i₂) (s.points i₃) < π / 2
have 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))
Tactic: convert! h (i₁ := e i₁) (i₂ := e i₂) (i₃ := e i₃) ?_ ?_ ?_ using 1
-- 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
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))
⊢ ∠ (s.points i₁) (s.points i₂) (s.points i₃) < π / 2
have 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))
Tactic: convert! h (i₁ := e i₁) (i₂ := e i₂) (i₃ := e i₃) ?_ ?_ ?_ using 1
-- 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
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.reindex e).points i₁) ((s.reindex e).points i₂) ((s.reindex e).points i₃) < π / 2
have 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))
Tactic: convert! h (i₁ := e.symm i₁) (i₂ := e.symm i₂) (i₃ := e.symm i₃) ?_ ?_ ?_ using 1
-- 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
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))
⊢ ∠ ((s.reindex e).points i₁) ((s.reindex e).points i₂) ((s.reindex e).points i₃) < π / 2
have 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))
Tactic: convert! h (i₁ := e.symm i₁) (i₂ := e.symm i₂) (i₃ := e.symm i₃) ?_ ?_ ?_ using 1
-- 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
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))
⊢ ∠ ((s.reindex e).points i₁) ((s.reindex e).points i₂) ((s.reindex e).points i₃) < π / 2
have 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))
Tactic: convert! h (i₁ := e.symm i₁) (i₂ := e.symm i₂) (i₃ := e.symm i₃) ?_ ?_ ?_ using 1
-- 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₃
⊢ ∠ (s.points i₁) (s.points i₂) (s.points i₃) < π / 2
have rw : π / 3 < π / 2
Tactic: rw [he.angle_eq_pi_div_three h₁₂ h₁₃ h₂₃]