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₁
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₁
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 →
  ∠ 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₃
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
⊢ π / 3 < ∠ p₁ p₂ p₃
have pos : ∀ (h : p₂ = p₁), π / 3 < ∠ p₁ p₂ p₃
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₁), π / 3 < ∠ p₁ p₂ p₃
⊢ π / 3 < ∠ p₁ p₂ p₃
have neg : ∀ (h : ¬p₂ = p₁), π / 3 < ∠ p₁ p₂ p₃
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₁
⊢ π / 3 < ∠ p₁ p₂ p₃
have pos : π / 3 < π / 2
Tactic: rw [h, angle_self_left]
-- 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₁
⊢ π / 3 < π / 2
have linarith : π / 2 ≤ π / 3 → 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₃ : 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₁
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.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₁
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.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₁
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.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₁
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.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₁
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.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₁
⊢ π / 3 < ∠ p₁ p₂ p₃
have neg : ∀ (hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁), π / 3 < ∠ p₁ p₂ p₃
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₁), π / 3 < ∠ p₁ p₂ p₃
⊢ π / 3 < ∠ p₁ p₂ p₃
have neg₁ : ∀ (hne : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂), π / 3 < ∠ p₁ p₂ p₃
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₁), π / 3 < ∠ p₁ p₂ p₃
neg₁ : ∀ (hne : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂), π / 3 < ∠ p₁ p₂ p₃
⊢ π / 3 < ∠ p₁ p₂ p₃
have neg₂ : ∀ (hne : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂), π / 3 < ∠ p₁ p₂ p₃
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₁
⊢ π / 3 < ∠ p₁ p₂ p₃
have neg : ∀ (hne : ∠ p₁ p₂ p₃ < ∠ p₂ p₃ p₁), π / 3 < ∠ p₁ p₂ p₃
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₁), π / 3 < ∠ p₁ p₂ p₃
⊢ π / 3 < ∠ p₁ p₂ p₃
have neg₁ : ∀ (hne : ∠ p₂ p₃ p₁ < ∠ p₁ p₂ p₃), π / 3 < ∠ p₁ p₂ p₃
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₂
⊢ π / 3 < ∠ p₁ p₂ p₃
have neg : ∀ (hne : ∠ p₁ p₂ p₃ < ∠ p₃ p₁ p₂), π / 3 < ∠ p₁ p₂ p₃
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₂), π / 3 < ∠ p₁ p₂ p₃
⊢ π / 3 < ∠ p₁ p₂ p₃
have neg₁ : ∀ (hne : ∠ p₃ p₁ p₂ < ∠ p₁ p₂ p₃), π / 3 < ∠ p₁ p₂ p₃
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₂
⊢ π / 3 < ∠ p₁ p₂ p₃
have neg : ∀ (hne : ∠ p₂ p₃ p₁ < ∠ p₃ p₁ p₂), π / 3 < ∠ p₁ p₂ p₃
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₂), π / 3 < ∠ p₁ p₂ p₃
⊢ π / 3 < ∠ p₁ p₂ p₃
have neg₁ : ∀ (hne : ∠ p₃ p₁ p₂ < ∠ p₂ p₃ p₁), π / 3 < ∠ p₁ p₂ p₃
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₁
⊢ π / 3 < ∠ p₁ p₂ p₃
have linarith : ∠ p₁ p₂ p₃ ≤ π / 3 → 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₃
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 → ∠ 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₃
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
hne : ∠ p₂ p₃ p₁ < ∠ p₁ p₂ p₃
⊢ π / 3 < ∠ p₁ p₂ p₃
have linarith : ∠ p₁ p₂ p₃ ≤ π / 3 → 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₃
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 →
  ∠ 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₂
⊢ π / 3 < ∠ p₁ p₂ p₃
have linarith : ∠ p₁ p₂ p₃ ≤ π / 3 → 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₃
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 → ∠ 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₃
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₁ p₂ p₃
⊢ π / 3 < ∠ p₁ p₂ p₃
have linarith : ∠ p₁ p₂ p₃ ≤ π / 3 → 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₃
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 →
  ∠ 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₂
⊢ π / 3 < ∠ p₁ p₂ p₃
have linarith : ∠ p₁ p₂ p₃ ≤ π / 3 → 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₃
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₃
h : ¬p₂ = p₁
hne_1 : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₂ p₃ p₁
⊢ π / 3 < ∠ p₁ p₂ p₃
have linarith : ∠ p₁ p₂ p₃ ≤ π / 3 → 3 / 3 = 1
Tactic: linarith [angle_add_angle_add_angle_eq_pi p₃ h]