awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c d : R
inst_2 : AddLeftReflectLT R
inst_3 : ExistsAddOfLE R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftStrictMono R
hba : b < a
hdc : d < c
⊢ a * d + b * c < a * c + b * d
have rw : b * c + a * d < b * d + a * c
Tactic: rw [add_comm (a * d), add_comm (a * c)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
hab : 0 ≤ a * b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
have refine : ¬(¬(0 ≤ a ∧ 0 ≤ b) ∧ ¬(a ≤ 0 ∧ b ≤ 0))
Tactic: refine Decidable.or_iff_not_not_and_not.2 ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
hab : 0 ≤ a * b
⊢ ¬(¬(0 ≤ a ∧ 0 ≤ b) ∧ ¬(a ≤ 0 ∧ b ≤ 0))
have simp : (0 ≤ a → b < 0) → ¬(a ≤ 0 → 0 < b)
Tactic: simp only [not_and, not_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ False
have apply : a * b < 0
Tactic: apply not_lt_of_ge hab _
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ a * b < 0
have inl : ∀ (ha : 0 < a), a * b < 0
Tactic: rcases lt_trichotomy 0 a with (ha | rfl | ha)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
inl : ∀ (ha : 0 < a), a * b < 0
⊢ a * b < 0
have inr : ∀ (hab : 0 ≤ 0 * b) (ab : LE.le.{u} (α := R) 0 0 → b < 0) (nab : LE.le.{u} (α := R) 0 0 → 0 < b), 0 * b < 0
Tactic: rcases lt_trichotomy 0 a with (ha | rfl | ha)
Cleared hypotheses: a, hab, ab, nab
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
inl : ∀ (ha : 0 < a), a * b < 0
inr : ∀ (hab : 0 ≤ 0 * b) (ab : LE.le.{u} (α := R) 0 0 → b < 0) (nab : LE.le.{u} (α := R) 0 0 → 0 < b), 0 * b < 0
⊢ a * b < 0
have inr₁ : ∀ (ha : a < 0), a * b < 0
Tactic: rcases lt_trichotomy 0 a with (ha | rfl | ha)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
b c : R
inst_2 : PosMulStrictMono R
h : 0 < c
⊢ 0 ≤ c * b ↔ 0 ≤ b
have h₁ : 0 = c * 0
Tactic: convert! mul_le_mul_iff_right₀ h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
⊢ a = 0 ∨ 0 < a ∧ 0 ≤ b
have this : 0 ≤ a
Tactic: have : 0 ≤ a := by simpa only [pow_zero, mul_one] using h 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
this : 0 ≤ a
⊢ a = 0 ∨ 0 < a ∧ 0 ≤ b
have refine : ∀ (ha : 0 < a), 0 ≤ a * b
Tactic: refine this.eq_or_lt'.imp_right fun ha ↦ ⟨ha, nonneg_of_mul_nonneg_right ?_ ha⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
a b c : R
⊢ 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a
have rw : (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ 0 ≤ b * c ∨ 0 ≤ c * a
Tactic: rw [mul_nonneg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ 0 ≤ b * c ∨ 0 ≤ c * a
have rw : (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c * a
Tactic: rw [mul_nonneg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c * a
have rw : (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
Tactic: rw [mul_nonneg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
a b c : R
⊢ 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a
have iterate : (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
Tactic: iterate 3 rw [mul_nonneg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
have or_a : 0 ≤ a ∨ a ≤ 0
Tactic: have or_a := le_total 0 a
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
a b c : R
or_a : 0 ≤ a ∨ a ≤ 0
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
have or_b : 0 ≤ b ∨ b ≤ 0
Tactic: have or_b := le_total 0 b
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
a b c : R
or_a : 0 ≤ a ∨ a ≤ 0
or_b : 0 ≤ b ∨ b ≤ 0
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
have or_c : 0 ≤ c ∨ c ≤ 0
Tactic: have or_c := le_total 0 c
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
⊢ 0 ≤ a * b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)
have refine : 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)
Tactic: refine mul_nonneg_iff.trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)
have simp_rw : 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)
Tactic: simp_rw [← not_le, ← or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)
have this : a ≤ 0 ∨ 0 ≤ a
Tactic: have := le_total a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
this : a ≤ 0 ∨ 0 ≤ a
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)
have this₁ : b ≤ 0 ∨ 0 ≤ b
Tactic: have := le_total b 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftStrictMono R
inst_6 : AddLeftReflectLT R
a : R
⊢ 0 < a * a ↔ a ≠ 0
have mp : 0 < a * a → a ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftStrictMono R
inst_6 : AddLeftReflectLT R
a : R
mp : 0 < a * a → a ≠ 0
⊢ 0 < a * a ↔ a ≠ 0
have mpr : a ≠ 0 → 0 < a * a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftStrictMono R
inst_6 : AddLeftReflectLT R
h : 0 < HMul.hMul (α := R) 0 0
⊢ False
have h₁ : LT.lt.{u} (α := R) 0 0
Tactic: rw [mul_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftStrictMono R
inst_6 : AddLeftReflectLT R
a : R
h : a ≠ 0
⊢ 0 < a * a
have mpr : ∀ (h : a < 0), 0 < a * a
Tactic: rcases h.lt_or_gt with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftStrictMono R
inst_6 : AddLeftReflectLT R
a : R
h : a ≠ 0
mpr : ∀ (h : a < 0), 0 < a * a
⊢ 0 < a * a
have mpr₁ : ∀ (h : 0 < a), 0 < a * a
Tactic: rcases h.lt_or_gt with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
⊢ 0 ≤ HPow.hPow (β := ℕ) a 2
have inl : ∀ (ha : 0 ≤ a), 0 ≤ HPow.hPow (β := ℕ) a 2
Tactic: obtain ha | ha := le_or_gt 0 a
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
inl : ∀ (ha : 0 ≤ a), 0 ≤ HPow.hPow (β := ℕ) a 2
⊢ 0 ≤ HPow.hPow (β := ℕ) a 2
have inr : ∀ (ha : a < 0), 0 ≤ HPow.hPow (β := ℕ) a 2
Tactic: obtain ha | ha := le_or_gt 0 a
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
ha : a < 0
⊢ 0 ≤ HPow.hPow (β := ℕ) a 2
have inr : ∀ (b : R) (hab : 0 = a + b), 0 ≤ HPow.hPow (β := ℕ) a 2
Tactic: obtain ⟨b, hab⟩ := exists_add_of_le ha.le
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
⊢ 0 ≤ HPow.hPow (β := ℕ) a 2
have hb : 0 < b
Tactic: have hb : 0 < b := not_le.1 fun hb ↦ (add_neg_of_neg_of_nonpos ha hb).ne' hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) b 2 + a * (a + b)
have rw : HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) b 2 + a * 0
Tactic: rw [← hab, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
rw : HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) b 2 + a * 0
⊢ HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) b 2 + a * (a + b)
have rw₁ : HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) b 2 + 0
Tactic: rw [← hab, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
rw : HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) b 2 + a * 0
rw₁ : HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) b 2 + 0
⊢ HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) b 2 + a * (a + b)
have rw₂ : HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) b 2
Tactic: rw [← hab, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ HPow.hPow (β := ℕ) b 2 + a * (a + b) = HPow.hPow (β := ℕ) a 2 + (a + b) * b
have rw : HPow.hPow (β := ℕ) b 2 + a * (a + b) = HPow.hPow (β := ℕ) a 2 + (a * b + b * b)
Tactic: rw [add_mul, mul_add, sq, sq, add_comm, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
rw : HPow.hPow (β := ℕ) b 2 + a * (a + b) = HPow.hPow (β := ℕ) a 2 + (a * b + b * b)
⊢ HPow.hPow (β := ℕ) b 2 + a * (a + b) = HPow.hPow (β := ℕ) a 2 + (a + b) * b
have rw₁ : HPow.hPow (β := ℕ) b 2 + (a * a + a * b) = HPow.hPow (β := ℕ) a 2 + (a * b + b * b)
Tactic: rw [add_mul, mul_add, sq, sq, add_comm, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
rw : HPow.hPow (β := ℕ) b 2 + a * (a + b) = HPow.hPow (β := ℕ) a 2 + (a * b + b * b)
rw₁ : HPow.hPow (β := ℕ) b 2 + (a * a + a * b) = HPow.hPow (β := ℕ) a 2 + (a * b + b * b)
⊢ HPow.hPow (β := ℕ) b 2 + a * (a + b) = HPow.hPow (β := ℕ) a 2 + (a + b) * b
have rw₂ : b * b + (a * a + a * b) = HPow.hPow (β := ℕ) a 2 + (a * b + b * b)
Tactic: rw [add_mul, mul_add, sq, sq, add_comm, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
rw : HPow.hPow (β := ℕ) b 2 + a * (a + b) = HPow.hPow (β := ℕ) a 2 + (a * b + b * b)
rw₁ : HPow.hPow (β := ℕ) b 2 + (a * a + a * b) = HPow.hPow (β := ℕ) a 2 + (a * b + b * b)
rw₂ : b * b + (a * a + a * b) = HPow.hPow (β := ℕ) a 2 + (a * b + b * b)
⊢ HPow.hPow (β := ℕ) b 2 + a * (a + b) = HPow.hPow (β := ℕ) a 2 + (a + b) * b
have rw₃ : b * b + (a * a + a * b) = a * a + (a * b + b * b)
Tactic: rw [add_mul, mul_add, sq, sq, add_comm, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
rw : HPow.hPow (β := ℕ) b 2 + a * (a + b) = HPow.hPow (β := ℕ) a 2 + (a * b + b * b)
rw₁ : HPow.hPow (β := ℕ) b 2 + (a * a + a * b) = HPow.hPow (β := ℕ) a 2 + (a * b + b * b)
rw₂ : b * b + (a * a + a * b) = HPow.hPow (β := ℕ) a 2 + (a * b + b * b)
rw₃ : b * b + (a * a + a * b) = a * a + (a * b + b * b)
⊢ HPow.hPow (β := ℕ) b 2 + a * (a + b) = HPow.hPow (β := ℕ) a 2 + (a + b) * b
have rw₄ : a * a + a * b + b * b = a * a + (a * b + b * b)
Tactic: rw [add_mul, mul_add, sq, sq, add_comm, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
rw : HPow.hPow (β := ℕ) b 2 + a * (a + b) = HPow.hPow (β := ℕ) a 2 + (a * b + b * b)
rw₁ : HPow.hPow (β := ℕ) b 2 + (a * a + a * b) = HPow.hPow (β := ℕ) a 2 + (a * b + b * b)
rw₂ : b * b + (a * a + a * b) = HPow.hPow (β := ℕ) a 2 + (a * b + b * b)
rw₃ : b * b + (a * a + a * b) = a * a + (a * b + b * b)
rw₄ : a * a + a * b + b * b = a * a + (a * b + b * b)
⊢ HPow.hPow (β := ℕ) b 2 + a * (a + b) = HPow.hPow (β := ℕ) a 2 + (a + b) * b
have rw₅ : a * a + (a * b + b * b) = a * a + (a * b + b * b)
Tactic: rw [add_mul, mul_add, sq, sq, add_comm, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ HPow.hPow (β := ℕ) a 2 + (a + b) * b = HPow.hPow (β := ℕ) a 2
have rw : HPow.hPow (β := ℕ) a 2 + 0 * b = HPow.hPow (β := ℕ) a 2
Tactic: rw [← hab, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
rw : HPow.hPow (β := ℕ) a 2 + 0 * b = HPow.hPow (β := ℕ) a 2
⊢ HPow.hPow (β := ℕ) a 2 + (a + b) * b = HPow.hPow (β := ℕ) a 2
have rw₁ : HPow.hPow (β := ℕ) a 2 + 0 = HPow.hPow (β := ℕ) a 2
Tactic: rw [← hab, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
rw : HPow.hPow (β := ℕ) a 2 + 0 * b = HPow.hPow (β := ℕ) a 2
rw₁ : HPow.hPow (β := ℕ) a 2 + 0 = HPow.hPow (β := ℕ) a 2
⊢ HPow.hPow (β := ℕ) a 2 + (a + b) * b = HPow.hPow (β := ℕ) a 2
have rw₂ : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) a 2
Tactic: rw [← hab, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ 0 ≤ HPow.hPow (β := ℕ) a 2
have b₁ : HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) b 2 + a * (a + b)
Tactic: calc
    0 ≤ b ^ 2 := pow_succ_nonneg hb.le _
    _ = b ^ 2 + a * (a + b) := by rw [← hab, mul_zero, add_zero]
    _ = a ^ 2 + (a + b) * b := by rw [add_mul, mul_add, sq, sq, add_comm, add_assoc]
    _ = a ^ 2 := by rw [← hab, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
b₁ : HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) b 2 + a * (a + b)
⊢ 0 ≤ HPow.hPow (β := ℕ) a 2
have b₂ : HPow.hPow (β := ℕ) b 2 + a * (a + b) = HPow.hPow (β := ℕ) a 2 + (a + b) * b
Tactic: calc
    0 ≤ b ^ 2 := pow_succ_nonneg hb.le _
    _ = b ^ 2 + a * (a + b) := by rw [← hab, mul_zero, add_zero]
    _ = a ^ 2 + (a + b) * b := by rw [add_mul, mul_add, sq, sq, add_comm, add_assoc]
    _ = a ^ 2 := by rw [← hab, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
b₁ : HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) b 2 + a * (a + b)
b₂ : HPow.hPow (β := ℕ) b 2 + a * (a + b) = HPow.hPow (β := ℕ) a 2 + (a + b) * b
⊢ 0 ≤ HPow.hPow (β := ℕ) a 2
have b₃ : HPow.hPow (β := ℕ) a 2 + (a + b) * b = HPow.hPow (β := ℕ) a 2
Tactic: calc
    0 ≤ b ^ 2 := pow_succ_nonneg hb.le _
    _ = b ^ 2 + a * (a + b) := by rw [← hab, mul_zero, add_zero]
    _ = a ^ 2 + (a + b) * b := by rw [add_mul, mul_add, sq, sq, add_comm, add_assoc]
    _ = a ^ 2 := by rw [← hab, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
inst_5 : NoZeroDivisors R
r : R
⊢ HPow.hPow (β := ℕ) r 2 ≤ 0 ↔ r = 0
have trans : HPow.hPow (β := ℕ) r 2 ≤ 0 ↔ HPow.hPow (β := ℕ) r 2 = 0
Tactic: trans r ^ 2 = 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
inst_5 : NoZeroDivisors R
r : R
trans : HPow.hPow (β := ℕ) r 2 ≤ 0 ↔ HPow.hPow (β := ℕ) r 2 = 0
⊢ HPow.hPow (β := ℕ) r 2 ≤ 0 ↔ r = 0
have trans₁ : HPow.hPow (β := ℕ) r 2 = 0 ↔ r = 0
Tactic: trans r ^ 2 = 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
inst_5 : NoZeroDivisors R
r : R
⊢ HPow.hPow (β := ℕ) r 2 ≤ 0 ↔ HPow.hPow (β := ℕ) r 2 = 0
have rw : HPow.hPow (β := ℕ) r 2 ≤ 0 ↔ HPow.hPow (β := ℕ) r 2 ≤ 0 ∧ 0 ≤ HPow.hPow (β := ℕ) r 2
Tactic: rw [le_antisymm_iff, and_iff_left (sq_nonneg r)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
inst_5 : NoZeroDivisors R
r : R
rw : HPow.hPow (β := ℕ) r 2 ≤ 0 ↔ HPow.hPow (β := ℕ) r 2 ≤ 0 ∧ 0 ≤ HPow.hPow (β := ℕ) r 2
⊢ HPow.hPow (β := ℕ) r 2 ≤ 0 ↔ HPow.hPow (β := ℕ) r 2 = 0
have rw₁ : HPow.hPow (β := ℕ) r 2 ≤ 0 ↔ HPow.hPow (β := ℕ) r 2 ≤ 0
Tactic: rw [le_antisymm_iff, and_iff_left (sq_nonneg r)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : NoZeroDivisors R
inst_3 : ExistsAddOfLE R
inst_4 : PosMulMono R
inst_5 : AddLeftMono R
⊢ a * a + b * b = 0 ↔ a = 0 ∧ b = 0
have ha : 0 ≤ a * a
Tactic: rw [add_eq_zero_iff_of_nonneg, mul_self_eq_zero (M₀ := R), mul_self_eq_zero (M₀ := R)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : NoZeroDivisors R
inst_3 : ExistsAddOfLE R
inst_4 : PosMulMono R
inst_5 : AddLeftMono R
ha : 0 ≤ a * a
⊢ a * a + b * b = 0 ↔ a = 0 ∧ b = 0
have hb : 0 ≤ b * b
Tactic: rw [add_eq_zero_iff_of_nonneg, mul_self_eq_zero (M₀ := R), mul_self_eq_zero (M₀ := R)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : a * b < a * c
hbc : b ≤ c
⊢ 0 < a
have pos : ∀ (ha : 0 < a), 0 < a
Tactic: by_cases! ha : 0 < a
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : a * b < a * c
hbc : b ≤ c
pos : ∀ (ha : 0 < a), 0 < a
⊢ 0 < a
have neg : ∀ (ha : a ≤ 0), 0 < a
Tactic: by_cases! ha : 0 < a