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 : π / 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₂
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
hne : ∠ p₁ p₂ p₃ < ∠ p₂ 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₂
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
hne : ∠ p₁ p₂ p₃ < ∠ p₂ 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₂
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]
-- 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 : π / 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₂
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
hne : ∠ p₂ p₃ p₁ < ∠ p₁ 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₂
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
hne : ∠ p₂ p₃ p₁ < ∠ p₁ 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₃) = 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₂
⊢ ∠ 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₂
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ < ∠ p₃ 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₂
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ < ∠ p₃ 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₂
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ < ∠ p₃ 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₂
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]
-- 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 : π / 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₂
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₁ 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₂
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₁ 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₃) = 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₂
⊢ ∠ 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₂
h : ¬p₂ = p₁
hne_1 : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₂ p₃ p₁ < ∠ p₃ 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₂
h : ¬p₂ = p₁
hne_1 : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₂ p₃ p₁ < ∠ p₃ 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₂
h : ¬p₂ = p₁
hne_1 : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₂ p₃ p₁ < ∠ p₃ 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₃ →
  2 * (∠ 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₂
h : ¬p₂ = p₁
hne_1 : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₂ p₃ p₁ < ∠ p₃ 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
linarith₃ :
  π / 3 ≤ ∠ p₁ p₂ p₃ →
    2 * (∠ 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
⊢ ∠ p₁ p₂ p₃ < π / 3
have linarith₄ : π / 3 ≤ ∠ p₁ p₂ p₃ → 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₁
⊢ ∠ 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₂
h : ¬p₂ = p₁
hne_1 : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₂ 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₂
h : ¬p₂ = p₁
hne_1 : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₂ 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₂
h : ¬p₂ = p₁
hne_1 : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₂ 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₃ →
  2 * (∠ 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₂
h : ¬p₂ = p₁
hne_1 : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₂ 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
linarith₃ :
  π / 3 ≤ ∠ p₁ p₂ p₃ →
    2 * (∠ 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
⊢ ∠ p₁ p₂ p₃ < π / 3
have linarith₄ : π / 3 ≤ ∠ p₁ p₂ p₃ → GT.gt (α := ℝ) 2 0
Tactic: linarith [angle_add_angle_add_angle_eq_pi p₃ h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (hypothesis)
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
⊢ Eq.{u_1 + 1} (α := Measure X) μHE[0] μH[0]
have heq : Eq (α := Set (EuclideanSpace ℝ (Fin 0))) {0}
  (parallelepiped (ι := Fin 0) (⇑basis : (a : Fin 0) → EuclideanSpace ℝ (Fin 0)))
Tactic: have heq : ({0} : Set (EuclideanSpace ℝ (Fin 0))) = parallelepiped basis := by
    simp [parallelepiped]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (hypothesis)
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq :
  Eq (α := Set (EuclideanSpace ℝ (Fin 0))) {0}
    (parallelepiped (ι := Fin 0) (⇑basis : (a : Fin 0) → EuclideanSpace ℝ (Fin 0)))
⊢ Eq.{u_1 + 1} (α := Measure X) μHE[0] μH[0]
have h : volume =
  HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
    (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)]
Tactic: obtain h := isAddLeftInvariant_eq_smul (volume : Measure (EuclideanSpace ℝ (Fin 0))) μH[(0 : ℕ)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (hypothesis)
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq :
  Eq (α := Set (EuclideanSpace ℝ (Fin 0))) {0}
    (parallelepiped (ι := Fin 0) (⇑basis : (a : Fin 0) → EuclideanSpace ℝ (Fin 0)))
h :
  volume =
    HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
      (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)]
⊢ Eq.{u_1 + 1} (α := Measure X) μHE[0] μH[0]
have h₁ : Eq (α := ENNReal)
  ((HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
          (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)] :
        (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal)
      {0} :
    ENNReal)
  ((volume : (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal) {0} : ENNReal)
Tactic: obtain h := congr($h.symm {0})
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq :
  Eq (α := Set (EuclideanSpace ℝ (Fin 0))) {0}
    (parallelepiped (ι := Fin 0) (⇑basis : (a : Fin 0) → EuclideanSpace ℝ (Fin 0)))
h_1 :
  volume =
    HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
      (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)]
h :
  Eq (α := ENNReal)
    ((HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
            (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)] :
          (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal)
        {0} :
      ENNReal)
    ((volume : (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal) {0} : ENNReal)
| ((volume : (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal) {0} : ENNReal)
have rw : 1
Tactic: rw [heq, OrthonormalBasis.volume_parallelepiped]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (hypothesis)
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq :
  Eq (α := Set (EuclideanSpace ℝ (Fin 0))) {0}
    (parallelepiped (ι := Fin 0) (⇑basis : (a : Fin 0) → EuclideanSpace ℝ (Fin 0)))
h_1 :
  volume =
    HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
      (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)]
h :
  Eq (α := ENNReal)
    ((HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
            (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)] :
          (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal)
        {0} :
      ENNReal)
    ((volume : (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal) {0} : ENNReal)
⊢ Eq.{u_1 + 1} (α := Measure X) μHE[0] μH[0]
have h₁ : Eq (α := ENNReal)
  ((HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
          (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)] :
        (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal)
      {0} :
    ENNReal)
  (1 : ENNReal)
Tactic: conv_rhs at h => rw [heq, OrthonormalBasis.volume_parallelepiped]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (hypothesis)
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq :
  Eq (α := Set (EuclideanSpace ℝ (Fin 0))) {0}
    (parallelepiped (ι := Fin 0) (⇑basis : (a : Fin 0) → EuclideanSpace ℝ (Fin 0)))
h_1 :
  volume =
    HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
      (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)]
h :
  Eq (α := ENNReal)
    ((HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin 0)))
            (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[(↑0 : ℝ)]) μH[(↑0 : ℝ)] :
          (a : Set (EuclideanSpace ℝ (Fin 0))) → ENNReal)
        {0} :
      ENNReal)
    (1 : ENNReal)
⊢ Eq.{u_1 + 1} (α := Measure X) μHE[0] μH[0]
have h₁ : addHaarScalarFactor (G := EuclideanSpace ℝ (Fin 0)) volume μH[0] = 1
Tactic: simp_rw [CharP.cast_eq_zero, smul_apply, hausdorffMeasure_zero_singleton, ENNReal.smul_def,
    smul_eq_mul, mul_one, ENNReal.coe_eq_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (hypothesis)
Goal:
d : ℕ
h0 : addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)] = 0
⊢ False
have h : volume =
  HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin d)))
    (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)]) μH[(↑d : ℝ)]
Tactic: obtain h := isAddLeftInvariant_eq_smul (volume : Measure (EuclideanSpace ℝ (Fin d))) μH[d]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (hypothesis)
Goal:
d : ℕ
h0 : addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)] = 0
h :
  volume =
    HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin d)))
      (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)]) μH[(↑d : ℝ)]
⊢ False
have h₁ : Eq (α := ENNReal)
  ((volume : (a : Set (EuclideanSpace ℝ (Fin d))) → ENNReal)
      (parallelepiped (ι := Fin (finrank ℝ (EuclideanSpace ℝ (Fin d))))
        (⇑(stdOrthonormalBasis ℝ (EuclideanSpace ℝ (Fin d))) :
          (a : Fin (finrank ℝ (EuclideanSpace ℝ (Fin d)))) → EuclideanSpace ℝ (Fin d))) :
    ENNReal)
  ((HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin d)))
          (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)]) μH[(↑d : ℝ)] :
        (a : Set (EuclideanSpace ℝ (Fin d))) → ENNReal)
      (parallelepiped (ι := Fin (finrank ℝ (EuclideanSpace ℝ (Fin d))))
        (⇑(stdOrthonormalBasis ℝ (EuclideanSpace ℝ (Fin d))) :
          (a : Fin (finrank ℝ (EuclideanSpace ℝ (Fin d)))) → EuclideanSpace ℝ (Fin d))) :
    ENNReal)
Tactic: obtain h := congr($h (parallelepiped (stdOrthonormalBasis ℝ (EuclideanSpace ℝ (Fin d)))))
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℕ
h : d₁ < d₂
s : Set X
⊢ Eq (α := ENNReal)
      ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₂)) volume μH[(↑d₂ : ℝ)])
              μH[(↑d₂ : ℝ)] :
            (a : Set X) → ENNReal)
          s :
        ENNReal)
      (0 : ENNReal) ∨
    Eq (α := ENNReal)
      ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₁)) volume μH[(↑d₁ : ℝ)])
              μH[(↑d₁ : ℝ)] :
            (a : Set X) → ENNReal)
          s :
        ENNReal)
      (⊤ : ENNReal)
have inl : ∀ (h : Eq (α := ENNReal) (((μH[(↑d₂ : ℝ)] : Measure X) : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)),
  Eq (α := ENNReal)
      ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₂)) volume μH[(↑d₂ : ℝ)])
              μH[(↑d₂ : ℝ)] :
            (a : Set X) → ENNReal)
          s :
        ENNReal)
      (0 : ENNReal) ∨
    Eq (α := ENNReal)
      ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₁)) volume μH[(↑d₁ : ℝ)])
              μH[(↑d₁ : ℝ)] :
            (a : Set X) → ENNReal)
          s :
        ENNReal)
      (⊤ : ENNReal)
Tactic: obtain h | h := hausdorffMeasure_zero_or_top (show (d₁ : ℝ) < d₂ by simpa using h) s