awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
hlc' : 0 ≤ (↑(↑1 : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff
h : Even P.natDegree
⊢ 0 < (↑(↑1 : ℤ) : ℝ) * eval x P
have push_cast : ∀ (hlc' : 0 ≤ 1 * (P.comp (-X)).leadingCoeff), 0 < 1 * eval x P
Tactic: push_cast at hlc' ⊢
Cleared hypotheses: hlc'
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
h : Even P.natDegree
hlc' : 0 ≤ 1 * (P.comp (-X)).leadingCoeff
⊢ 0 < 1 * eval x P
have rw : ∀ (hlc' : 0 ≤ (P.comp (-X)).leadingCoeff), 0 < eval x P
Tactic: rw [one_mul] at hlc' ⊢
Cleared hypotheses: hlc'
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (hypothesis)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
h : Even P.natDegree
hlc' : 0 ≤ (P.comp (-X)).leadingCoeff
⊢ 0 < eval x P
have this : 0 < eval (-x) (P.comp (-X))
Tactic: have := zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg hroots' hlc'
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
hlc' : 0 ≤ (↑(↑(Int.negOnePow (↑(P.comp (-X)).natDegree : ℤ)) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff
h : Odd P.natDegree
⊢ 0 < (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
have rw : ∀ (hlc' : 0 ≤ (↑(↑(-1) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff) (h : Odd P.natDegree), 0 < (↑(↑(-1) : ℤ) : ℝ) * eval x P
Tactic: rw [Int.negOnePow_odd] at hlc' ⊢
Cleared hypotheses: hlc', h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
hlc' : 0 ≤ (↑(↑(Int.negOnePow (↑(P.comp (-X)).natDegree : ℤ)) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff
h : Odd P.natDegree
rw :
  ∀ (hlc' : 0 ≤ (↑(↑(-1) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff) (h : Odd P.natDegree),
    0 < (↑(↑(-1) : ℤ) : ℝ) * eval x P
⊢ 0 < (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
have hn : ∀ (hlc' : 0 ≤ (↑(↑(-1) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff) (h : Odd P.natDegree), Odd (α := ℤ) (↑P.natDegree : ℤ)
Tactic: rw [Int.negOnePow_odd] at hlc' ⊢
Cleared hypotheses: hlc', h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
hlc' : 0 ≤ (↑(↑(Int.negOnePow (↑(P.comp (-X)).natDegree : ℤ)) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff
h : Odd P.natDegree
rw :
  ∀ (hlc' : 0 ≤ (↑(↑(-1) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff) (h : Odd P.natDegree),
    0 < (↑(↑(-1) : ℤ) : ℝ) * eval x P
hn :
  ∀ (hlc' : 0 ≤ (↑(↑(-1) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff) (h : Odd P.natDegree), Odd (α := ℤ) (↑P.natDegree : ℤ)
⊢ 0 < (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
have hn₁ : Odd (α := ℤ) (↑(P.comp (-X)).natDegree : ℤ)
Tactic: rw [Int.negOnePow_odd] at hlc' ⊢
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
hlc' : 0 ≤ (↑(↑(-1) : ℤ) : ℝ) * (P.comp (-X)).leadingCoeff
h : Odd P.natDegree
⊢ 0 < (↑(↑(-1) : ℤ) : ℝ) * eval x P
have push_cast : ∀ (hlc' : 0 ≤ -1 * (P.comp (-X)).leadingCoeff), 0 < -1 * eval x P
Tactic: push_cast at hlc' ⊢
Cleared hypotheses: hlc'
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
h : Odd P.natDegree
hlc' : 0 ≤ -1 * (P.comp (-X)).leadingCoeff
⊢ 0 < -1 * eval x P
have rw : ∀ (hlc' : 0 ≤ -(P.comp (-X)).leadingCoeff), 0 < -eval x P
Tactic: rw [neg_one_mul] at hlc' ⊢
Cleared hypotheses: hlc'
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (hypothesis)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ) (hy : (P.comp (-X)).IsRoot y), y < -x
h : Odd P.natDegree
hlc' : 0 ≤ -(P.comp (-X)).leadingCoeff
⊢ 0 < -eval x P
have this : eval (-x) (P.comp (-X)) < 0
Tactic: have := eval_lt_zero_of_roots_lt_of_leadingCoeff_nonpos hroots' (nonpos_of_neg_nonneg hlc')
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : 0 ≤ P.leadingCoeff
⊢ 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
have pos : ∀ (hroots' : ∃ (y : ℝ), P.IsRoot y ∧ y ≤ x), 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
Tactic: by_cases! hroots' : ∃ y, P.IsRoot y ∧ y ≤ x
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : 0 ≤ P.leadingCoeff
pos : ∀ (hroots' : ∃ (y : ℝ), P.IsRoot y ∧ y ≤ x), 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
⊢ 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
have neg : ∀ (hroots' : ∀ (y : ℝ) (_ : P.IsRoot y), x < y), 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
Tactic: by_cases! hroots' : ∃ y, P.IsRoot y ∧ y ≤ x
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∃ (y : ℝ), P.IsRoot y ∧ y ≤ x
⊢ 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
have pos : ∀ (y : ℝ) (hroot : P.IsRoot y) (hle : y ≤ x), 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
Tactic: obtain ⟨y, hroot, hle⟩ := hroots'
Cleared hypotheses: hroots'
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : 0 ≤ P.leadingCoeff
y : ℝ
hroot : P.IsRoot y
hle : y ≤ x
⊢ 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
have pos : 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval y P
Tactic: rw [eq_of_ge_of_le hle (hroots y hroot), hroot, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : 0 ≤ P.leadingCoeff
y : ℝ
hroot : P.IsRoot y
hle : y ≤ x
pos : 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval y P
⊢ 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
have pos₁ : 0 ≤ HMul.hMul (α := ℝ) (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) 0
Tactic: rw [eq_of_ge_of_le hle (hroots y hroot), hroot, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : 0 ≤ P.leadingCoeff
y : ℝ
hroot : P.IsRoot y
hle : y ≤ x
pos : 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval y P
pos₁ : 0 ≤ HMul.hMul (α := ℝ) (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) 0
⊢ 0 ≤ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P
have pos₂ : LE.le (α := ℝ) 0 0
Tactic: rw [eq_of_ge_of_le hle (hroots y hroot), hroot, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
this : 0 < (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)
⊢ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P < 0
have apply : 0 < -((↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P)
Tactic: apply neg_pos.mp
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
⊢ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P < 0
have suffices : 0 < (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)
Tactic: suffices 0 < Int.negOnePow (-P).natDegree * (-P).eval x by apply neg_pos.mp; simpa
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
⊢ 0 < (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)
have refine_1 : ∀ (y : ℝ) (hy : (-P).IsRoot y), P.IsRoot y
Tactic: refine zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg (fun y hy => hroots y ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
refine_1 : ∀ (y : ℝ) (hy : (-P).IsRoot y), P.IsRoot y
⊢ 0 < (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)
have refine_2 : 0 ≤ (-P).leadingCoeff
Tactic: refine zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg (fun y hy => hroots y ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ P.IsRoot y
have refine_1 : eval y P = 0
Tactic: rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
refine_1 : eval y P = 0
⊢ P.IsRoot y
have refine_1₁ : eval y P = -0
Tactic: rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
refine_1 : eval y P = 0
refine_1₁ : eval y P = -0
⊢ P.IsRoot y
have refine_1₂ : -eval y P = 0
Tactic: rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
refine_1 : eval y P = 0
refine_1₁ : eval y P = -0
refine_1₂ : -eval y P = 0
⊢ P.IsRoot y
have refine_1₃ : eval y (-P) = 0
Tactic: rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
⊢ 0 ≤ (-P).leadingCoeff
have refine_2 : 0 ≤ -P.leadingCoeff
Tactic: rwa [leadingCoeff_neg, le_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
refine_2 : 0 ≤ -P.leadingCoeff
⊢ 0 ≤ (-P).leadingCoeff
have refine_2₁ : P.leadingCoeff ≤ -0
Tactic: rwa [leadingCoeff_neg, le_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
this : 0 ≤ (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)
⊢ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P ≤ 0
have apply : 0 ≤ -((↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P)
Tactic: apply neg_nonneg.mp
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
⊢ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P ≤ 0
have suffices : 0 ≤ (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)
Tactic: suffices 0 ≤ Int.negOnePow (-P).natDegree * (-P).eval x by apply neg_nonneg.mp; simpa
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
⊢ 0 ≤ (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)
have refine_1 : ∀ (y : ℝ) (hy : (-P).IsRoot y), P.IsRoot y
Tactic: refine zero_le_negOnePow_mul_eval_of_le_roots_of_leadingCoeff_nonneg (fun y hy => hroots y ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
refine_1 : ∀ (y : ℝ) (hy : (-P).IsRoot y), P.IsRoot y
⊢ 0 ≤ (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)
have refine_2 : 0 ≤ (-P).leadingCoeff
Tactic: refine zero_le_negOnePow_mul_eval_of_le_roots_of_leadingCoeff_nonneg (fun y hy => hroots y ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ P.IsRoot y
have refine_1 : eval y P = 0
Tactic: rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
refine_1 : eval y P = 0
⊢ P.IsRoot y
have refine_1₁ : eval y P = -0
Tactic: rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
refine_1 : eval y P = 0
refine_1₁ : eval y P = -0
⊢ P.IsRoot y
have refine_1₂ : -eval y P = 0
Tactic: rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
refine_1 : eval y P = 0
refine_1₁ : eval y P = -0
refine_1₂ : -eval y P = 0
⊢ P.IsRoot y
have refine_1₃ : eval y (-P) = 0
Tactic: rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Order (goal)
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
⊢ 0 ≤ (-P).leadingCoeff
have refine_2 : 0 ≤ -P.leadingCoeff
Tactic: rwa [leadingCoeff_neg, neg_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
x y : ℍ
r : ℝ
⊢ ⟪r • x, y⟫ = HMul.hMul (α := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) ⟪x, y⟫
have simp : r * x.re * y.re + r * x.imI * y.imI + r * x.imJ * y.imJ + r * x.imK * y.imK =
  r * (x.re * y.re + x.imI * y.imI + x.imJ * y.imJ + x.imK * y.imK)
Tactic: simp [inner_def]
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
a : ℍ
⊢ (normSq : (a : ℍ) → ℝ) a = ‖a‖ * ‖a‖
have rw : ⟪a, a⟫ = ‖a‖ * ‖a‖
Tactic: rw [← inner_self, real_inner_self_eq_norm_mul_norm]
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
a : ℍ
rw : ⟪a, a⟫ = ‖a‖ * ‖a‖
⊢ (normSq : (a : ℍ) → ℝ) a = ‖a‖ * ‖a‖
have rw₁ : ‖a‖ * ‖a‖ = ‖a‖ * ‖a‖
Tactic: rw [← inner_self, real_inner_self_eq_norm_mul_norm]
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
⊢ norm (E := ℍ) 1 = 1
have rw : √(inner ℝ (E := ℍ) 1 1) = 1
Tactic: rw [norm_eq_sqrt_real_inner, inner_self, normSq.map_one, Real.sqrt_one]
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
rw : √(inner ℝ (E := ℍ) 1 1) = 1
⊢ norm (E := ℍ) 1 = 1
have rw₁ : √((normSq : (a : ℍ) → ℝ) 1) = 1
Tactic: rw [norm_eq_sqrt_real_inner, inner_self, normSq.map_one, Real.sqrt_one]
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
rw : √(inner ℝ (E := ℍ) 1 1) = 1
rw₁ : √((normSq : (a : ℍ) → ℝ) 1) = 1
⊢ norm (E := ℍ) 1 = 1
have rw₂ : √1 = 1
Tactic: rw [norm_eq_sqrt_real_inner, inner_self, normSq.map_one, Real.sqrt_one]
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
rw : √(inner ℝ (E := ℍ) 1 1) = 1
rw₁ : √((normSq : (a : ℍ) → ℝ) 1) = 1
rw₂ : √1 = 1
⊢ norm (E := ℍ) 1 = 1
have rw₃ : Eq (α := ℝ) 1 1
Tactic: rw [norm_eq_sqrt_real_inner, inner_self, normSq.map_one, Real.sqrt_one]
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
a : ℝ
⊢ norm (E := ℍ) (↑a : ℍ) = ‖a‖
have rw : √(inner ℝ (E := ℍ) (↑a : ℍ) (↑a : ℍ)) = ‖a‖
Tactic: rw [norm_eq_sqrt_real_inner, inner_self, normSq_coe, Real.sqrt_sq_eq_abs, Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
a : ℝ
rw : √(inner ℝ (E := ℍ) (↑a : ℍ) (↑a : ℍ)) = ‖a‖
⊢ norm (E := ℍ) (↑a : ℍ) = ‖a‖
have rw₁ : √((normSq : (a : ℍ) → ℝ) (↑a : ℍ)) = ‖a‖
Tactic: rw [norm_eq_sqrt_real_inner, inner_self, normSq_coe, Real.sqrt_sq_eq_abs, Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
a : ℝ
rw : √(inner ℝ (E := ℍ) (↑a : ℍ) (↑a : ℍ)) = ‖a‖
rw₁ : √((normSq : (a : ℍ) → ℝ) (↑a : ℍ)) = ‖a‖
⊢ norm (E := ℍ) (↑a : ℍ) = ‖a‖
have rw₂ : √(HPow.hPow (β := ℕ) a 2) = ‖a‖
Tactic: rw [norm_eq_sqrt_real_inner, inner_self, normSq_coe, Real.sqrt_sq_eq_abs, Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
a : ℝ
rw : √(inner ℝ (E := ℍ) (↑a : ℍ) (↑a : ℍ)) = ‖a‖
rw₁ : √((normSq : (a : ℍ) → ℝ) (↑a : ℍ)) = ‖a‖
rw₂ : √(HPow.hPow (β := ℕ) a 2) = ‖a‖
⊢ norm (E := ℍ) (↑a : ℍ) = ‖a‖
have rw₃ : |a| = ‖a‖
Tactic: rw [norm_eq_sqrt_real_inner, inner_self, normSq_coe, Real.sqrt_sq_eq_abs, Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
a : ℝ
rw : √(inner ℝ (E := ℍ) (↑a : ℍ) (↑a : ℍ)) = ‖a‖
rw₁ : √((normSq : (a : ℍ) → ℝ) (↑a : ℍ)) = ‖a‖
rw₂ : √(HPow.hPow (β := ℕ) a 2) = ‖a‖
rw₃ : |a| = ‖a‖
⊢ norm (E := ℍ) (↑a : ℍ) = ‖a‖
have rw₄ : |a| = |a|
Tactic: rw [norm_eq_sqrt_real_inner, inner_self, normSq_coe, Real.sqrt_sq_eq_abs, Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
a : ℍ
⊢ ‖star a‖ = ‖a‖
have simp_rw : √⟪star a, star a⟫ = √⟪a, a⟫
Tactic: simp_rw [norm_eq_sqrt_real_inner, inner_self, normSq_star]
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
a : ℍ
simp_rw : √⟪star a, star a⟫ = √⟪a, a⟫
⊢ ‖star a‖ = ‖a‖
have simp_rw₁ : √((normSq : (a : ℍ) → ℝ) (star a)) = √((normSq : (a : ℍ) → ℝ) a)
Tactic: simp_rw [norm_eq_sqrt_real_inner, inner_self, normSq_star]
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
z w : ℂ
⊢ (↑(z + w) : ℍ) = (↑z : ℍ) + (↑w : ℍ)
have a : (↑(z + w) : ℍ).re = ((↑z : ℍ) + (↑w : ℍ)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
z w : ℂ
a : (↑(z + w) : ℍ).re = ((↑z : ℍ) + (↑w : ℍ)).re
⊢ (↑(z + w) : ℍ) = (↑z : ℍ) + (↑w : ℍ)
have a₁ : (↑(z + w) : ℍ).imI = ((↑z : ℍ) + (↑w : ℍ)).imI
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
z w : ℂ
a : (↑(z + w) : ℍ).re = ((↑z : ℍ) + (↑w : ℍ)).re
a₁ : (↑(z + w) : ℍ).imI = ((↑z : ℍ) + (↑w : ℍ)).imI
⊢ (↑(z + w) : ℍ) = (↑z : ℍ) + (↑w : ℍ)
have a₂ : (↑(z + w) : ℍ).imJ = ((↑z : ℍ) + (↑w : ℍ)).imJ
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
z w : ℂ
a : (↑(z + w) : ℍ).re = ((↑z : ℍ) + (↑w : ℍ)).re
a₁ : (↑(z + w) : ℍ).imI = ((↑z : ℍ) + (↑w : ℍ)).imI
a₂ : (↑(z + w) : ℍ).imJ = ((↑z : ℍ) + (↑w : ℍ)).imJ
⊢ (↑(z + w) : ℍ) = (↑z : ℍ) + (↑w : ℍ)
have a₃ : (↑(z + w) : ℍ).imK = ((↑z : ℍ) + (↑w : ℍ)).imK
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
z w : ℂ
⊢ (↑(z * w) : ℍ) = (↑z : ℍ) * (↑w : ℍ)
have a : (↑(z * w) : ℍ).re = ((↑z : ℍ) * (↑w : ℍ)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
z w : ℂ
a : (↑(z * w) : ℍ).re = ((↑z : ℍ) * (↑w : ℍ)).re
⊢ (↑(z * w) : ℍ) = (↑z : ℍ) * (↑w : ℍ)
have a₁ : (↑(z * w) : ℍ).imI = ((↑z : ℍ) * (↑w : ℍ)).imI
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
z w : ℂ
a : (↑(z * w) : ℍ).re = ((↑z : ℍ) * (↑w : ℍ)).re
a₁ : (↑(z * w) : ℍ).imI = ((↑z : ℍ) * (↑w : ℍ)).imI
⊢ (↑(z * w) : ℍ) = (↑z : ℍ) * (↑w : ℍ)
have a₂ : (↑(z * w) : ℍ).imJ = ((↑z : ℍ) * (↑w : ℍ)).imJ
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
z w : ℂ
a : (↑(z * w) : ℍ).re = ((↑z : ℍ) * (↑w : ℍ)).re
a₁ : (↑(z * w) : ℍ).imI = ((↑z : ℍ) * (↑w : ℍ)).imI
a₂ : (↑(z * w) : ℍ).imJ = ((↑z : ℍ) * (↑w : ℍ)).imJ
⊢ (↑(z * w) : ℍ) = (↑z : ℍ) * (↑w : ℍ)
have a₃ : (↑(z * w) : ℍ).imK = ((↑z : ℍ) * (↑w : ℍ)).imK
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
r : ℝ
z : ℂ
⊢ r • (↑z : ℍ) = (↑r : ℍ) * (↑z : ℍ)
have a : (r • (↑z : ℍ)).re = ((↑r : ℍ) * (↑z : ℍ)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
r : ℝ
z : ℂ
a : (r • (↑z : ℍ)).re = ((↑r : ℍ) * (↑z : ℍ)).re
⊢ r • (↑z : ℍ) = (↑r : ℍ) * (↑z : ℍ)
have a₁ : (r • (↑z : ℍ)).imI = ((↑r : ℍ) * (↑z : ℍ)).imI
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
r : ℝ
z : ℂ
a : (r • (↑z : ℍ)).re = ((↑r : ℍ) * (↑z : ℍ)).re
a₁ : (r • (↑z : ℍ)).imI = ((↑r : ℍ) * (↑z : ℍ)).imI
⊢ r • (↑z : ℍ) = (↑r : ℍ) * (↑z : ℍ)
have a₂ : (r • (↑z : ℍ)).imJ = ((↑r : ℍ) * (↑z : ℍ)).imJ
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
r : ℝ
z : ℂ
a : (r • (↑z : ℍ)).re = ((↑r : ℍ) * (↑z : ℍ)).re
a₁ : (r • (↑z : ℍ)).imI = ((↑r : ℍ) * (↑z : ℍ)).imI
a₂ : (r • (↑z : ℍ)).imJ = ((↑r : ℍ) * (↑z : ℍ)).imJ
⊢ r • (↑z : ℍ) = (↑r : ℍ) * (↑z : ℍ)
have a₃ : (r • (↑z : ℍ)).imK = ((↑r : ℍ) * (↑z : ℍ)).imK
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
x : ℍ
⊢ norm (E := WithLp 2 (Fin 4 → ℝ)) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x) : WithLp 2 (Fin 4 → ℝ)) = ‖x‖
have rw : √(inner ℝ (E := ℝ) (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 0 : ℝ)
            (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 0 : ℝ) +
          inner ℝ (E := ℝ) (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 1 : ℝ)
            (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 1 : ℝ) +
        inner ℝ (E := ℝ) (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 2 : ℝ)
          (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 2 : ℝ) +
      inner ℝ (E := ℝ) (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 3 : ℝ)
        (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 3 : ℝ)) =
  √(HPow.hPow (β := ℕ) x.re 2 + HPow.hPow (β := ℕ) x.imI 2 + HPow.hPow (β := ℕ) x.imJ 2 + HPow.hPow (β := ℕ) x.imK 2)
Tactic: rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner, inner_self, normSq_def', PiLp.inner_apply,
    Fin.sum_univ_four]
-- Lean 4 proof step from Mathlib.Analysis.Quaternion (goal)
Goal:
x : ℍ
⊢ √(inner ℝ (E := ℝ) (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 0 : ℝ)
              (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 0 : ℝ) +
            inner ℝ (E := ℝ) (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 1 : ℝ)
              (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 1 : ℝ) +
          inner ℝ (E := ℝ) (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 2 : ℝ)
            (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 2 : ℝ) +
        inner ℝ (E := ℝ) (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 3 : ℝ)
          (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 3 : ℝ)) =
    √(HPow.hPow (β := ℕ) x.re 2 + HPow.hPow (β := ℕ) x.imI 2 + HPow.hPow (β := ℕ) x.imJ 2 + HPow.hPow (β := ℕ) x.imK 2)
have simp_rw : √(HPow.hPow (α := ℝ) (β := ℕ) ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x 0 : ℝ) 2 +
          HPow.hPow (α := ℝ) (β := ℕ) ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x 1 : ℝ) 2 +
        HPow.hPow (α := ℝ) (β := ℕ) ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x 2 : ℝ) 2 +
      HPow.hPow (α := ℝ) (β := ℕ) ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x 3 : ℝ) 2) =
  √(HPow.hPow (β := ℕ) x.re 2 + HPow.hPow (β := ℕ) x.imI 2 + HPow.hPow (β := ℕ) x.imJ 2 + HPow.hPow (β := ℕ) x.imK 2)
Tactic: simp_rw [RCLike.inner_apply, starRingEnd_apply, star_trivial, ← sq]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : Module ℝ E
inst_4 : IsScalarTower ℝ K E
r : ℝ
x : E
⊢ r • x = HSMul.hSMul.{u_1, u_2, u_2} (α := K) (↑r : K) x
have rw : r • x = HSMul.hSMul (β := K) r 1 • x
Tactic: rw [RCLike.ofReal_alg, smul_one_smul]