awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne_1 : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₂ p₃ p₁
linarith : ∠ p₁ p₂ p₃ ≤ π / 3 → 3 / 3 = 1
⊢ π / 3 < ∠ p₁ p₂ p₃
have linarith₁ : ∠ p₁ p₂ p₃ ≤ π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
Tactic: linarith [angle_add_angle_add_angle_eq_pi p₃ h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne_1 : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₂ p₃ p₁
linarith : ∠ p₁ p₂ p₃ ≤ π / 3 → 3 / 3 = 1
linarith₁ : ∠ p₁ p₂ p₃ ≤ π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
⊢ π / 3 < ∠ p₁ p₂ p₃
have linarith₂ : ∠ p₁ p₂ p₃ ≤ π / 3 → GT.gt (α := ℝ) 3 0
Tactic: linarith [angle_add_angle_add_angle_eq_pi p₃ h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne_1 : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₂ p₃ p₁
linarith : ∠ p₁ p₂ p₃ ≤ π / 3 → 3 / 3 = 1
linarith₁ : ∠ p₁ p₂ p₃ ≤ π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : ∠ p₁ p₂ p₃ ≤ π / 3 → GT.gt (α := ℝ) 3 0
⊢ π / 3 < ∠ p₁ p₂ p₃
have linarith₃ : ∠ p₁ p₂ p₃ ≤ π / 3 →
  2 * (∠ p₂ p₃ p₁ - ∠ p₁ p₂ p₃) + (∠ p₃ p₁ p₂ - ∠ p₂ p₃ p₁) + (3 * ∠ p₁ p₂ p₃ - 1 * π) +
      -(∠ p₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ p₁ p₂ - π) =
    0
Tactic: linarith [angle_add_angle_add_angle_eq_pi p₃ h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne_1 : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₂ p₃ p₁
linarith : ∠ p₁ p₂ p₃ ≤ π / 3 → 3 / 3 = 1
linarith₁ : ∠ p₁ p₂ p₃ ≤ π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : ∠ p₁ p₂ p₃ ≤ π / 3 → GT.gt (α := ℝ) 3 0
linarith₃ :
  ∠ p₁ p₂ p₃ ≤ π / 3 →
    2 * (∠ p₂ p₃ p₁ - ∠ p₁ p₂ p₃) + (∠ p₃ p₁ p₂ - ∠ p₂ p₃ p₁) + (3 * ∠ p₁ p₂ p₃ - 1 * π) +
        -(∠ p₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ p₁ p₂ - π) =
      0
⊢ π / 3 < ∠ p₁ p₂ p₃
have linarith₄ : ∠ p₁ p₂ p₃ ≤ π / 3 → GT.gt (α := ℝ) 2 0
Tactic: linarith [angle_add_angle_add_angle_eq_pi p₃ h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hnd : p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃
⊢ ∠ p₁ p₂ p₃ ≤ π / 3
have pos : ∀ (h : p₂ = p₁), ∠ p₁ p₂ p₃ ≤ π / 3
Tactic: by_cases h : p₂ = p₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hnd : p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃
pos : ∀ (h : p₂ = p₁), ∠ p₁ p₂ p₃ ≤ π / 3
⊢ ∠ p₁ p₂ p₃ ≤ π / 3
have neg : ∀ (h : ¬p₂ = p₁), ∠ p₁ p₂ p₃ ≤ π / 3
Tactic: by_cases h : p₂ = p₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hnd : p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃
h : p₂ = p₁
⊢ ∠ p₁ p₂ p₃ ≤ π / 3
have pos : ∀ (h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂) (h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂) (hnd : p₂ ≠ p₂ ∨ p₂ ≠ p₃ ∨ p₂ ≠ p₃),
  ∠ p₂ p₂ p₃ ≤ π / 3
Tactic: subst h
Cleared hypotheses: p₁, h₂₃₁, h₃₁₂, hnd, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂
h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂
hnd : p₂ ≠ p₂ ∨ p₂ ≠ p₃ ∨ p₂ ≠ p₃
⊢ ∠ p₂ p₂ p₃ ≤ π / 3
have pos : ∀ (h₂₃₁ : π / 2 ≤ 0) (hnd : ¬p₂ = p₃), π / 2 ≤ π / 3
Tactic: simp_all [angle_self_of_ne]
Cleared hypotheses: h₂₃₁, h₃₁₂, hnd
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : π / 2 ≤ 0
hnd : ¬p₂ = p₃
⊢ π / 2 ≤ π / 3
have linarith : π / 3 < π / 2 → 3 / 3 = 1
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : π / 2 ≤ 0
hnd : ¬p₂ = p₃
linarith : π / 3 < π / 2 → 3 / 3 = 1
⊢ π / 2 ≤ π / 3
have linarith₁ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 2 3 = 6
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : π / 2 ≤ 0
hnd : ¬p₂ = p₃
linarith : π / 3 < π / 2 → 3 / 3 = 1
linarith₁ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 2 3 = 6
⊢ π / 2 ≤ π / 3
have linarith₂ : π / 3 < π / 2 → 2 / 2 = 1
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : π / 2 ≤ 0
hnd : ¬p₂ = p₃
linarith : π / 3 < π / 2 → 3 / 3 = 1
linarith₁ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 2 3 = 6
linarith₂ : π / 3 < π / 2 → 2 / 2 = 1
⊢ π / 2 ≤ π / 3
have linarith₃ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 3 2 = 6
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : π / 2 ≤ 0
hnd : ¬p₂ = p₃
linarith : π / 3 < π / 2 → 3 / 3 = 1
linarith₁ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 2 3 = 6
linarith₂ : π / 3 < π / 2 → 2 / 2 = 1
linarith₃ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 3 2 = 6
⊢ π / 2 ≤ π / 3
have linarith₄ : π / 3 < π / 2 → GT.gt (α := ℝ) 6 0
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : π / 2 ≤ 0
hnd : ¬p₂ = p₃
linarith : π / 3 < π / 2 → 3 / 3 = 1
linarith₁ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 2 3 = 6
linarith₂ : π / 3 < π / 2 → 2 / 2 = 1
linarith₃ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 3 2 = 6
linarith₄ : π / 3 < π / 2 → GT.gt (α := ℝ) 6 0
linarith₅ : π / 3 < π / 2 → 2 / 2 = 1
⊢ π / 2 ≤ π / 3
have linarith₆ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : π / 2 ≤ 0
hnd : ¬p₂ = p₃
linarith : π / 3 < π / 2 → 3 / 3 = 1
linarith₁ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 2 3 = 6
linarith₂ : π / 3 < π / 2 → 2 / 2 = 1
linarith₃ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 3 2 = 6
linarith₄ : π / 3 < π / 2 → GT.gt (α := ℝ) 6 0
linarith₅ : π / 3 < π / 2 → 2 / 2 = 1
linarith₆ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ π / 2 ≤ π / 3
have linarith₇ : π / 3 < π / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : π / 2 ≤ 0
hnd : ¬p₂ = p₃
linarith : π / 3 < π / 2 → 3 / 3 = 1
linarith₁ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 2 3 = 6
linarith₂ : π / 3 < π / 2 → 2 / 2 = 1
linarith₃ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 3 2 = 6
linarith₄ : π / 3 < π / 2 → GT.gt (α := ℝ) 6 0
linarith₅ : π / 3 < π / 2 → 2 / 2 = 1
linarith₆ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : π / 3 < π / 2 → GT.gt (α := ℝ) 2 0
⊢ π / 2 ≤ π / 3
have linarith₈ : π / 3 < π / 2 → 1 * π - HMul.hMul (α := ℝ) 2 0 + (2 * π - 3 * π) = 0
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hnd : p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃
h : ¬p₂ = p₁
⊢ ∠ p₁ p₂ p₃ ≤ π / 3
have linarith : π / 3 < ∠ p₁ p₂ p₃ → 3 / 3 = 1
Tactic: linarith [angle_add_angle_add_angle_eq_pi p₃ h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hnd : p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃
h : ¬p₂ = p₁
linarith : π / 3 < ∠ p₁ p₂ p₃ → 3 / 3 = 1
⊢ ∠ p₁ p₂ p₃ ≤ π / 3
have linarith₁ : π / 3 < ∠ p₁ p₂ p₃ → HMul.hMul (α := ℝ) 1 3 = 3
Tactic: linarith [angle_add_angle_add_angle_eq_pi p₃ h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hnd : p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃
h : ¬p₂ = p₁
linarith : π / 3 < ∠ p₁ p₂ p₃ → 3 / 3 = 1
linarith₁ : π / 3 < ∠ p₁ p₂ p₃ → HMul.hMul (α := ℝ) 1 3 = 3
⊢ ∠ p₁ p₂ p₃ ≤ π / 3
have linarith₂ : π / 3 < ∠ p₁ p₂ p₃ → GT.gt (α := ℝ) 3 0
Tactic: linarith [angle_add_angle_add_angle_eq_pi p₃ h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hnd : p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃
h : ¬p₂ = p₁
linarith : π / 3 < ∠ p₁ p₂ p₃ → 3 / 3 = 1
linarith₁ : π / 3 < ∠ p₁ p₂ p₃ → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π / 3 < ∠ p₁ p₂ p₃ → GT.gt (α := ℝ) 3 0
⊢ ∠ p₁ p₂ p₃ ≤ π / 3
have linarith₃ : π / 3 < ∠ p₁ p₂ p₃ →
  ∠ p₁ p₂ p₃ - ∠ p₂ p₃ p₁ + (∠ p₁ p₂ p₃ - ∠ p₃ p₁ p₂) + (1 * π - 3 * ∠ p₁ p₂ p₃) +
      (∠ p₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ p₁ p₂ - π) =
    0
Tactic: linarith [angle_add_angle_add_angle_eq_pi p₃ h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
⊢ ∠ p₁ p₂ p₃ < π / 3
have pos : ∀ (h : p₂ = p₁), ∠ p₁ p₂ p₃ < π / 3
Tactic: by_cases h : p₂ = p₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
pos : ∀ (h : p₂ = p₁), ∠ p₁ p₂ p₃ < π / 3
⊢ ∠ p₁ p₂ p₃ < π / 3
have neg : ∀ (h : ¬p₂ = p₁), ∠ p₁ p₂ p₃ < π / 3
Tactic: by_cases h : p₂ = p₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : p₂ = p₁
⊢ ∠ p₁ p₂ p₃ < π / 3
have pos : ∀ (h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂) (h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂)
  (hne : ∠ p₂ p₂ p₃ ≠ ∠ p₂ p₃ p₂ ∨ ∠ p₂ p₂ p₃ ≠ ∠ p₃ p₂ p₂ ∨ ∠ p₂ p₃ p₂ ≠ ∠ p₃ p₂ p₂), ∠ p₂ p₂ p₃ < π / 3
Tactic: subst h
Cleared hypotheses: p₁, h₂₃₁, h₃₁₂, hne, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂
h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂
hne : ∠ p₂ p₂ p₃ ≠ ∠ p₂ p₃ p₂ ∨ ∠ p₂ p₂ p₃ ≠ ∠ p₃ p₂ p₂ ∨ ∠ p₂ p₃ p₂ ≠ ∠ p₃ p₂ p₂
⊢ ∠ p₂ p₂ p₃ < π / 3
have pos : ∀ (h₂₃ : p₂ = p₃), ∠ p₂ p₂ p₃ < π / 3
Tactic: by_cases h₂₃ : p₂ = p₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂
h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂
hne : ∠ p₂ p₂ p₃ ≠ ∠ p₂ p₃ p₂ ∨ ∠ p₂ p₂ p₃ ≠ ∠ p₃ p₂ p₂ ∨ ∠ p₂ p₃ p₂ ≠ ∠ p₃ p₂ p₂
pos : ∀ (h₂₃ : p₂ = p₃), ∠ p₂ p₂ p₃ < π / 3
⊢ ∠ p₂ p₂ p₃ < π / 3
have neg : ∀ (h₂₃ : ¬p₂ = p₃), ∠ p₂ p₂ p₃ < π / 3
Tactic: by_cases h₂₃ : p₂ = p₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂
h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂
hne : ∠ p₂ p₂ p₃ ≠ ∠ p₂ p₃ p₂ ∨ ∠ p₂ p₂ p₃ ≠ ∠ p₃ p₂ p₂ ∨ ∠ p₂ p₃ p₂ ≠ ∠ p₃ p₂ p₂
h₂₃ : p₂ = p₃
⊢ ∠ p₂ p₂ p₃ < π / 3
have pos : ∀ (h₂₃₁ h₃₁₂ : ∠ p₂ p₂ p₂ ≤ ∠ p₂ p₂ p₂)
  (hne : ∠ p₂ p₂ p₂ ≠ ∠ p₂ p₂ p₂ ∨ ∠ p₂ p₂ p₂ ≠ ∠ p₂ p₂ p₂ ∨ ∠ p₂ p₂ p₂ ≠ ∠ p₂ p₂ p₂), ∠ p₂ p₂ p₂ < π / 3
Tactic: subst h₂₃
Cleared hypotheses: p₃, h₂₃₁, h₃₁₂, hne, h₂₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂
h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂
hne : ∠ p₂ p₂ p₃ ≠ ∠ p₂ p₃ p₂ ∨ ∠ p₂ p₂ p₃ ≠ ∠ p₃ p₂ p₂ ∨ ∠ p₂ p₃ p₂ ≠ ∠ p₃ p₂ p₂
h₂₃ : ¬p₂ = p₃
⊢ ∠ p₂ p₂ p₃ < π / 3
have neg : ∀ (h₂₃₁ : π / 2 ≤ 0) (h₂₃ : ¬p₂ = p₃), π / 2 < π / 3
Tactic: simp_all [angle_self_of_ne]
Cleared hypotheses: h₂₃₁, h₃₁₂, hne, h₂₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : π / 2 ≤ 0
h₂₃ : ¬p₂ = p₃
⊢ π / 2 < π / 3
have linarith : π / 3 ≤ π / 2 → 3 / 3 = 1
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : π / 2 ≤ 0
h₂₃ : ¬p₂ = p₃
linarith : π / 3 ≤ π / 2 → 3 / 3 = 1
⊢ π / 2 < π / 3
have linarith₁ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 2 3 = 6
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : π / 2 ≤ 0
h₂₃ : ¬p₂ = p₃
linarith : π / 3 ≤ π / 2 → 3 / 3 = 1
linarith₁ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 2 3 = 6
⊢ π / 2 < π / 3
have linarith₂ : π / 3 ≤ π / 2 → 2 / 2 = 1
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : π / 2 ≤ 0
h₂₃ : ¬p₂ = p₃
linarith : π / 3 ≤ π / 2 → 3 / 3 = 1
linarith₁ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 2 3 = 6
linarith₂ : π / 3 ≤ π / 2 → 2 / 2 = 1
⊢ π / 2 < π / 3
have linarith₃ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 3 2 = 6
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : π / 2 ≤ 0
h₂₃ : ¬p₂ = p₃
linarith : π / 3 ≤ π / 2 → 3 / 3 = 1
linarith₁ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 2 3 = 6
linarith₂ : π / 3 ≤ π / 2 → 2 / 2 = 1
linarith₃ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 3 2 = 6
⊢ π / 2 < π / 3
have linarith₄ : π / 3 ≤ π / 2 → GT.gt (α := ℝ) 6 0
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : π / 2 ≤ 0
h₂₃ : ¬p₂ = p₃
linarith : π / 3 ≤ π / 2 → 3 / 3 = 1
linarith₁ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 2 3 = 6
linarith₂ : π / 3 ≤ π / 2 → 2 / 2 = 1
linarith₃ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 3 2 = 6
linarith₄ : π / 3 ≤ π / 2 → GT.gt (α := ℝ) 6 0
linarith₅ : π / 3 ≤ π / 2 → 2 / 2 = 1
⊢ π / 2 < π / 3
have linarith₆ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : π / 2 ≤ 0
h₂₃ : ¬p₂ = p₃
linarith : π / 3 ≤ π / 2 → 3 / 3 = 1
linarith₁ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 2 3 = 6
linarith₂ : π / 3 ≤ π / 2 → 2 / 2 = 1
linarith₃ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 3 2 = 6
linarith₄ : π / 3 ≤ π / 2 → GT.gt (α := ℝ) 6 0
linarith₅ : π / 3 ≤ π / 2 → 2 / 2 = 1
linarith₆ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ π / 2 < π / 3
have linarith₇ : π / 3 ≤ π / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₂ p₃ : P
h₂₃₁ : π / 2 ≤ 0
h₂₃ : ¬p₂ = p₃
linarith : π / 3 ≤ π / 2 → 3 / 3 = 1
linarith₁ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 2 3 = 6
linarith₂ : π / 3 ≤ π / 2 → 2 / 2 = 1
linarith₃ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 3 2 = 6
linarith₄ : π / 3 ≤ π / 2 → GT.gt (α := ℝ) 6 0
linarith₅ : π / 3 ≤ π / 2 → 2 / 2 = 1
linarith₆ : π / 3 ≤ π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : π / 3 ≤ π / 2 → GT.gt (α := ℝ) 2 0
⊢ π / 2 < π / 3
have linarith₈ : π / 3 ≤ π / 2 → 1 * π - HMul.hMul (α := ℝ) 2 0 + (0 - π) = 0
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
⊢ ∠ p₁ p₂ p₃ < π / 3
have neg : ∀ (hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁), ∠ p₁ p₂ p₃ < π / 3
Tactic: rcases hne with hne | hne | hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
neg : ∀ (hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁), ∠ p₁ p₂ p₃ < π / 3
⊢ ∠ p₁ p₂ p₃ < π / 3
have neg₁ : ∀ (hne : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂), ∠ p₁ p₂ p₃ < π / 3
Tactic: rcases hne with hne | hne | hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
neg : ∀ (hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁), ∠ p₁ p₂ p₃ < π / 3
neg₁ : ∀ (hne : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂), ∠ p₁ p₂ p₃ < π / 3
⊢ ∠ p₁ p₂ p₃ < π / 3
have neg₂ : ∀ (hne : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂), ∠ p₁ p₂ p₃ < π / 3
Tactic: rcases hne with hne | hne | hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
⊢ ∠ p₁ p₂ p₃ < π / 3
have neg : ∀ (hne : ∠ p₁ p₂ p₃ < ∠ p₂ p₃ p₁), ∠ p₁ p₂ p₃ < π / 3
Tactic: rcases hne.lt_or_gt with hne | hne
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
neg : ∀ (hne : ∠ p₁ p₂ p₃ < ∠ p₂ p₃ p₁), ∠ p₁ p₂ p₃ < π / 3
⊢ ∠ p₁ p₂ p₃ < π / 3
have neg₁ : ∀ (hne : ∠ p₂ p₃ p₁ < ∠ p₁ p₂ p₃), ∠ p₁ p₂ p₃ < π / 3
Tactic: rcases hne.lt_or_gt with hne | hne
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
⊢ ∠ p₁ p₂ p₃ < π / 3
have neg : ∀ (hne : ∠ p₁ p₂ p₃ < ∠ p₃ p₁ p₂), ∠ p₁ p₂ p₃ < π / 3
Tactic: rcases hne.lt_or_gt with hne | hne
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
neg : ∀ (hne : ∠ p₁ p₂ p₃ < ∠ p₃ p₁ p₂), ∠ p₁ p₂ p₃ < π / 3
⊢ ∠ p₁ p₂ p₃ < π / 3
have neg₁ : ∀ (hne : ∠ p₃ p₁ p₂ < ∠ p₁ p₂ p₃), ∠ p₁ p₂ p₃ < π / 3
Tactic: rcases hne.lt_or_gt with hne | hne
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
⊢ ∠ p₁ p₂ p₃ < π / 3
have neg : ∀ (hne : ∠ p₂ p₃ p₁ < ∠ p₃ p₁ p₂), ∠ p₁ p₂ p₃ < π / 3
Tactic: rcases hne.lt_or_gt with hne | hne
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
neg : ∀ (hne : ∠ p₂ p₃ p₁ < ∠ p₃ p₁ p₂), ∠ p₁ p₂ p₃ < π / 3
⊢ ∠ p₁ p₂ p₃ < π / 3
have neg₁ : ∀ (hne : ∠ p₃ p₁ p₂ < ∠ p₂ p₃ p₁), ∠ p₁ p₂ p₃ < π / 3
Tactic: rcases hne.lt_or_gt with hne | hne
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
hne : ∠ p₁ p₂ p₃ < ∠ p₂ p₃ p₁
⊢ ∠ p₁ p₂ p₃ < π / 3
have linarith : π / 3 ≤ ∠ p₁ p₂ p₃ → 3 / 3 = 1
Tactic: linarith [angle_add_angle_add_angle_eq_pi p₃ h]