awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
simp_rw : 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

Tactic:
simp_rw [← not_le, ← or_iff_not_imp_left]

Premises used: not_le, Classical.or_iff_not_imp_left
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
⊢ a ≤ 0 ∨ 0 ≤ a

Tactic:
have := le_total a 0
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
⊢ b ≤ 0 ∨ 0 ≤ b

Tactic:
have := le_total b 0
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
a b c : R
h : c < 0
⊢ c * a ≤ c * b ↔ b ≤ a

Tactic:
(strictAnti_mul_left h).le_iff_ge

Premises used: strictAnti_mul_left, StrictAnti.le_iff_ge
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
a b c : R
h : c < 0
⊢ a * c ≤ b * c ↔ b ≤ a

Tactic:
(strictAnti_mul_right h).le_iff_ge

Premises used: strictAnti_mul_right, StrictAnti.le_iff_ge
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
a b c : R
h : c < 0
⊢ c * a < c * b ↔ b < a

Tactic:
(strictAnti_mul_left h).lt_iff_gt

Premises used: strictAnti_mul_left, StrictAnti.lt_iff_gt
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
a b c : R
h : c < 0
⊢ a * c < b * c ↔ b < a

Tactic:
(strictAnti_mul_right h).lt_iff_gt

Premises used: strictAnti_mul_right, StrictAnti.lt_iff_gt
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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 : c * a < c * b
hc : c ≤ 0
⊢ b < a

Tactic:
(antitone_mul_left hc).reflect_lt h

Premises used: antitone_mul_left, Antitone.reflect_lt
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : a * c < b * c
hc : c ≤ 0
⊢ b < a

Tactic:
(antitone_mul_right hc).reflect_lt h

Premises used: Antitone.reflect_lt, antitone_mul_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightReflectLT R
inst_5 : AddRightStrictMono R
a : R
ha : a < 0
b c : R
⊢ cmp (a * b) (a * c) = cmp c b

Tactic:
(strictAnti_mul_left ha).cmp_map_eq b c

Premises used: StrictAnti.cmp_map_eq, strictAnti_mul_left
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightReflectLT R
inst_5 : AddRightStrictMono R
a : R
ha : a < 0
b c : R
⊢ cmp (b * a) (c * a) = cmp c b

Tactic:
(strictAnti_mul_right ha).cmp_map_eq b c

Premises used: strictAnti_mul_right, StrictAnti.cmp_map_eq
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
mpr : a ≠ 0 → 0 < a * a
⊢ 0 < a * a ↔ a ≠ 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
⊢ LT.lt.{u} (α := R) 0 0

Tactic:
rw [mul_zero] at h

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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 : LT.lt.{u} (α := R) 0 0
⊢ False

Tactic:
h.false

Premises used: LT.lt.false
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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 : LT.lt.{u} (α := R) 0 0
⊢ False

Tactic:
exact h.false

Premises used: LT.lt.false
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
mpr₁ : ∀ (h : 0 < a), 0 < a * a
⊢ 0 < a * a

Tactic:
rcases h.lt_or_gt with h | h

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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_1 : a ≠ 0
h : a < 0
⊢ 0 < a * a

Tactic:
mul_pos_of_neg_of_neg h h

Premises used: mul_pos_of_neg_of_neg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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_1 : a ≠ 0
h : 0 < a
⊢ 0 < a * a

Tactic:
mul_pos h h

Premises used: mul_pos
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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_1 : a ≠ 0
h : a < 0
⊢ 0 < a * a

Tactic:
exacts [mul_pos_of_neg_of_neg h h, mul_pos h h]

Premises used: mul_pos, mul_pos_of_neg_of_neg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
a b : R
h : a * b ≤ 0
hb : b < 0
⊢ 0 ≤ a

Tactic:
le_of_not_gt fun ha => absurd h (mul_pos_of_neg_of_neg ha hb).not_ge

Premises used: le_of_not_gt, absurd, LT.lt.not_ge, mul_pos_of_neg_of_neg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
a b : R
h : a * b ≤ 0
ha : a < 0
⊢ 0 ≤ b

Tactic:
le_of_not_gt fun hb => absurd h (mul_pos_of_neg_of_neg ha hb).not_ge

Premises used: le_of_not_gt, absurd, LT.lt.not_ge, mul_pos_of_neg_of_neg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
a b : R
h : a * b < 0
hb : b ≤ 0
⊢ 0 < a

Tactic:
lt_of_not_ge fun ha => absurd h (mul_nonneg_of_nonpos_of_nonpos ha hb).not_gt

Premises used: lt_of_not_ge, mul_nonneg_of_nonpos_of_nonpos, absurd, LE.le.not_gt
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
a b : R
h : a * b < 0
ha : a ≤ 0
⊢ 0 < b

Tactic:
lt_of_not_ge fun hb => absurd h (mul_nonneg_of_nonpos_of_nonpos ha hb).not_gt

Premises used: lt_of_not_ge, mul_nonneg_of_nonpos_of_nonpos, absurd, LE.le.not_gt
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : MulPosMono R
inst_5 : AddRightMono R
inst_6 : AddRightReflectLE R
hab : a * b < 0
⊢ a < 0 ↔ 0 < b

Tactic:
⟨pos_of_mul_neg_right hab ∘ le_of_lt, neg_of_mul_neg_left hab ∘ le_of_lt⟩

Premises used: neg_of_mul_neg_left, le_of_lt, Function.comp, Iff.intro, pos_of_mul_neg_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : MulPosMono R
inst_5 : AddRightMono R
inst_6 : AddRightReflectLE R
hab : a * b < 0
⊢ 0 < a ↔ b < 0

Tactic:
⟨neg_of_mul_neg_right hab ∘ le_of_lt, pos_of_mul_neg_left hab ∘ le_of_lt⟩

Premises used: pos_of_mul_neg_left, neg_of_mul_neg_right, le_of_lt, Function.comp, Iff.intro
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
inr : ∀ (ha : a < 0), 0 ≤ HPow.hPow (β := ℕ) a 2
⊢ 0 ≤ HPow.hPow (β := ℕ) a 2

Tactic:
obtain ha | ha := le_or_gt 0 a

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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 : 0 ≤ a
⊢ 0 ≤ HPow.hPow (β := ℕ) a 2

Tactic:
pow_succ_nonneg ha _

Premises used: pow_succ_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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 : 0 ≤ a
⊢ 0 ≤ HPow.hPow (β := ℕ) a 2

Tactic:
exact pow_succ_nonneg ha _

Premises used: pow_succ_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
inr : ∀ (b : R) (hab : 0 = a + b), 0 ≤ HPow.hPow (β := ℕ) a 2
⊢ 0 ≤ HPow.hPow (β := ℕ) a 2

Tactic:
obtain ⟨b, hab⟩ := exists_add_of_le ha.le

Premises used: LT.lt.le, ExistsAddOfLE.exists_add_of_le
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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 < b

Tactic:
have hb : 0 < b := not_le.1 fun hb ↦ (add_neg_of_neg_of_nonpos ha hb).ne' hab
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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 (β := ℕ) b 2

Tactic:
pow_succ_nonneg hb.le _

Premises used: pow_succ_nonneg, LT.lt.le
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
rw₂ rw₃ : HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) b 2
⊢ HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) b 2 + a * (a + b)

Tactic:
rw [← hab, mul_zero, add_zero]

Premises used: MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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)
rw₅ 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

Tactic:
rw [add_mul, mul_add, sq, sq, add_comm, add_assoc]

Premises used: add_mul, add_assoc, sq, add_comm, mul_add
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
rw₂ rw₃ : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) a 2
⊢ HPow.hPow (β := ℕ) a 2 + (a + b) * b = HPow.hPow (β := ℕ) a 2

Tactic:
rw [← hab, zero_mul, add_zero]

Premises used: MulZeroClass.zero_mul, add_zero
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
b₃ : HPow.hPow (β := ℕ) a 2 + (a + b) * b = HPow.hPow (β := ℕ) a 2
⊢ 0 ≤ 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]

Premises used: pow_succ_nonneg, LT.lt.le, HAdd.hAdd
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
trans₁ : HPow.hPow (β := ℕ) r 2 = 0 ↔ r = 0
⊢ HPow.hPow (β := ℕ) r 2 ≤ 0 ↔ r = 0

Tactic:
trans r ^ 2 = 0
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
rw₁ rw₂ : HPow.hPow (β := ℕ) r 2 ≤ 0 ↔ HPow.hPow (β := ℕ) r 2 ≤ 0
⊢ HPow.hPow (β := ℕ) r 2 ≤ 0 ↔ HPow.hPow (β := ℕ) r 2 = 0

Tactic:
rw [le_antisymm_iff, and_iff_left (sq_nonneg r)]

Premises used: and_iff_left, le_antisymm_iff, sq_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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

Tactic:
sq_eq_zero_iff

Premises used: sq_eq_zero_iff
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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

Tactic:
exact sq_eq_zero_iff

Premises used: sq_eq_zero_iff
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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 ≤ a * a

Tactic:
simpa only [sq] using sq_nonneg a

Premises used: sq, sq_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
α : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
⊢ LE.le.{u} (α := R) 0 1

Tactic:
simpa only [one_mul] using mul_self_nonneg (1 : R)

Premises used: mul_self_nonneg, OfNat.ofNat, one_mul
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
hb : 0 ≤ b * b
⊢ a * a + b * b = 0 ↔ a = 0 ∧ b = 0

Tactic:
rw [add_eq_zero_iff_of_nonneg, mul_self_eq_zero (M₀ := R), mul_self_eq_zero (M₀ := R)]

Premises used: mul_self_eq_zero, add_eq_zero_iff_of_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
⊢ 0 ≤ a * a

Tactic:
apply mul_self_nonneg

Premises used: mul_self_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
⊢ 0 ≤ b * b

Tactic:
apply mul_self_nonneg

Premises used: mul_self_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
h : a * a + b * b = 0
⊢ a = 0

Tactic:
(mul_self_add_mul_self_eq_zero.mp h).left

Premises used: mul_self_add_mul_self_eq_zero, And.left, Iff.mp
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
neg : ∀ (ha : a ≤ 0), 0 < a
⊢ 0 < a

Tactic:
by_cases! ha : 0 < a
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
ha : 0 < a
⊢ 0 < a

Tactic:
ha
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
ha : 0 < a
⊢ 0 < a

Tactic:
exact ha
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
ha : a ≤ 0
⊢ 0 < a

Tactic:
grind [mul_le_mul_of_nonpos_left hbc ha]

Premises used: mul_le_mul_of_nonpos_left
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddLeftMono R
inst_5 : AddRightReflectLE R
h : b * a < c * a
hbc : b ≤ c
pos : ∀ (ha : 0 < a), 0 < a
neg : ∀ (ha : a ≤ 0), 0 < a
⊢ 0 < a

Tactic:
by_cases! ha : 0 < a
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddLeftMono R
inst_5 : AddRightReflectLE R
h : b * a < c * a
hbc : b ≤ c
ha : 0 < a
⊢ 0 < a

Tactic:
ha
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddLeftMono R
inst_5 : AddRightReflectLE R
h : b * a < c * a
hbc : b ≤ c
ha : 0 < a
⊢ 0 < a

Tactic:
exact ha
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddLeftMono R
inst_5 : AddRightReflectLE R
h : b * a < c * a
hbc : b ≤ c
ha : a ≤ 0
⊢ 0 < a

Tactic:
grind [mul_le_mul_of_nonpos_right hbc ha]

Premises used: mul_le_mul_of_nonpos_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
a d : R
inst_2 : PosMulMono R
inst_3 : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
c0 : 0 ≤ a
b0 : 0 ≤ max d b
h₁ : b ≤ max d b
h₂ : a ≤ max c a
⊢ b * a ≤ max d b * max c a

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
a d : R
inst_2 : PosMulMono R
inst_3 : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
⊢ 0 ≤ a

Tactic:
ha
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
a d : R
inst_2 : PosMulMono R
inst_3 : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
⊢ 0 ≤ max d b

Tactic:
hd.trans <| le_max_left d b

Premises used: LE.le.trans, le_max_left
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
a d : R
inst_2 : PosMulMono R
inst_3 : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
⊢ b ≤ max d b

Tactic:
le_max_right d b

Premises used: le_max_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
a d : R
inst_2 : PosMulMono R
inst_3 : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
⊢ a ≤ max c a

Tactic:
le_max_right c a

Premises used: le_max_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
a d : R
inst_2 : PosMulMono R
inst_3 : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
⊢ 0 ≤ a

Tactic:
exacts [ha, hd.trans <| le_max_left d b, le_max_right d b, le_max_right c a]

Premises used: le_max_right, LE.le.trans, le_max_left
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
a d : R
inst_2 : PosMulMono R
inst_3 : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
ba : b * a ≤ max d b * max c a
cd : c * d ≤ max a c * max b d
⊢ a * b ≤ max a c * max d b

Tactic:
simpa [mul_comm, max_comm] using ba

Premises used: mul_comm, max_comm
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
a d : R
inst_2 : PosMulMono R
inst_3 : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
ba : b * a ≤ max d b * max c a
cd : c * d ≤ max a c * max b d
⊢ d * c ≤ max a c * max d b

Tactic:
simpa [mul_comm, max_comm] using cd

Premises used: mul_comm, max_comm
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
a b : R
⊢ 2 * a * b ≤ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2

Tactic:
simpa [fn_min_add_fn_max (fun x ↦ x * x), sq, two_mul, add_mul]
    using mul_add_mul_le_mul_add_mul (@min_le_max _ _ a b) (@min_le_max _ _ a b)

Premises used: add_mul, HMul.hMul, min_le_max, fn_min_add_fn_max, two_mul, sq, mul_add_mul_le_mul_add_mul
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
a b : R
rw : 4 * (a * b) = 2 * a * b + 2 * a * b
rw₁ : HAdd.hAdd (α := R) 2 2 * (a * b) = 2 * a * b + 2 * a * b
rw₂ : 2 * (a * b) + 2 * (a * b) = 2 * a * b + 2 * a * b
rw₃ rw₄ : 2 * (a * b) + 2 * (a * b) = 2 * (a * b) + 2 * (a * b)
⊢ 4 * a * b = 2 * a * b + 2 * a * b

Tactic:
rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]

Premises used: add_mul, mul_assoc, Eq.symm, two_add_two_eq_four
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
a b : R
bc : 2 * a * b ≤ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2
⊢ 2 * a * b + 2 * a * b ≤ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b

Tactic:
gcongr