awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
two_mul_le_add_sq _ _

Premises used: two_mul_le_add_sq
-- 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:
exact two_mul_le_add_sq _ _

Premises used: two_mul_le_add_sq
-- 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 rw₁ :
  HPow.hPow (β := ℕ) a 2 + 2 * a * b + HPow.hPow (β := ℕ) b 2 =
    HPow.hPow (β := ℕ) a 2 + 2 * a * b + HPow.hPow (β := ℕ) b 2
⊢ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b =
    HPow.hPow (β := ℕ) a 2 + 2 * a * b + HPow.hPow (β := ℕ) b 2

Tactic:
rw [add_right_comm]

Premises used: add_right_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
⊢ HPow.hPow (β := ℕ) a 2 + 2 * a * b + HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) (a + b) 2

Tactic:
(add_sq a b).symm

Premises used: add_sq, Eq.symm
-- 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
calc : 4 * a * b = 2 * a * b + 2 * a * b
calc₁ : 2 * a * b + 2 * a * b ≤ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
calc₂ :
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b =
    HPow.hPow (β := ℕ) a 2 + 2 * a * b + HPow.hPow (β := ℕ) b 2
⊢ 4 * a * b ≤ HPow.hPow (β := ℕ) (a + b) 2

Tactic:
calc 4 * a * b
    _ = 2 * a * b + 2 * a * b := by rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]
    _ ≤ a ^ 2 + b ^ 2 + 2 * a * b := by gcongr; exact two_mul_le_add_sq _ _
    _ = a ^ 2 + 2 * a * b + b ^ 2 := by rw [add_right_comm]
    _ = (a + b) ^ 2 := (add_sq a b).symm

Premises used: add_sq, HAdd.hAdd, Eq.symm
-- 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 : PosMulStrictMono R
inst_5 : AddLeftReflectLE R
inst_6 : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : HPow.hPow (β := ℕ) r 2 ≤ a * b
apply : 2 * r * (2 * r) ≤ (a + b) * (a + b)
⊢ 2 * r ≤ a + b

Tactic:
apply nonneg_le_nonneg_of_sq_le_sq (Left.add_nonneg ha hb)

Premises used: nonneg_le_nonneg_of_sq_le_sq, Left.add_nonneg
-- 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 : PosMulStrictMono R
inst_5 : AddLeftReflectLE R
inst_6 : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : HPow.hPow (β := ℕ) r 2 ≤ a * b
rw : 4 * HPow.hPow (β := ℕ) r 2 ≤ (a + b) * (a + b)
⊢ 2 * r * (2 * r) ≤ (a + b) * (a + b)

Tactic:
rw [mul_mul_mul_comm, ← pow_two r, two_mul, two_add_two_eq_four]

Premises used: pow_two, mul_mul_mul_comm, two_mul, 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 : PosMulStrictMono R
inst_5 : AddLeftReflectLE R
inst_6 : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : HPow.hPow (β := ℕ) r 2 ≤ a * b
grw : 4 * (a * b) ≤ (a + b) * (a + b)
grw₁ : 4 * a * b ≤ (a + b) * (a + b)
grw₂ : HPow.hPow (β := ℕ) (a + b) 2 ≤ (a + b) * (a + b)
grw₃ grw₄ : (a + b) * (a + b) ≤ (a + b) * (a + b)
⊢ 4 * HPow.hPow (β := ℕ) r 2 ≤ (a + b) * (a + b)

Tactic:
grw [mul_le_mul_of_nonneg_left ht zero_le_four, ← mul_assoc, four_mul_le_sq_add a b, sq]

Premises used: mul_assoc, four_mul_le_sq_add, zero_le_four, sq, mul_le_mul_of_nonneg_left
-- 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 : PosMulStrictMono R
inst_5 : AddLeftReflectLE R
inst_6 : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : HPow.hPow (β := ℕ) r 2 = a * b
⊢ 2 * r ≤ a + b

Tactic:
two_mul_le_add_of_sq_le_mul ha hb ht.le

Premises used: Eq.le, two_mul_le_add_of_sq_le_mul
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLT R
inst_5 : AddLeftStrictMono R
rw : 0 < -(a * b) ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₁ : 0 < a * -b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₂ : 0 < a ∧ 0 < -b ∨ a < 0 ∧ -b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₃ : 0 < a ∧ b < 0 ∨ a < 0 ∧ -b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₄ rw₅ : 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
rw [← neg_pos, neg_mul_eq_mul_neg, mul_pos_iff (R := R), neg_pos, neg_lt_zero]

Premises used: neg_pos, mul_pos_iff, neg_lt_zero, neg_mul_eq_mul_neg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
rw : 0 ≤ -(a * b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₁ : 0 ≤ a * -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₂ : 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₃ : 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₄ rw₅ : 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
rw [← neg_nonneg, neg_mul_eq_mul_neg, mul_nonneg_iff (R := R), neg_nonneg, neg_nonpos]

Premises used: mul_nonneg_iff, neg_nonpos, neg_nonneg, neg_mul_eq_mul_neg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftMono R
inst_5 : AddLeftReflectLE R
rw : (0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
⊢ 0 ≤ a * b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Tactic:
rw [← neg_mul_neg, mul_nonneg_iff_pos_imp_nonneg (R := R)]

Premises used: mul_nonneg_iff_pos_imp_nonneg, neg_mul_neg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftMono R
inst_5 : AddLeftReflectLE R
⊢ (0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Tactic:
simp only [neg_pos, neg_nonneg]

Premises used: neg_pos, neg_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftMono R
inst_5 : AddLeftReflectLE R
rw : (0 < a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ a) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
⊢ a * b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
rw [← neg_nonneg, ← mul_neg, mul_nonneg_iff_pos_imp_nonneg (R := R)]

Premises used: mul_nonneg_iff_pos_imp_nonneg, neg_nonneg, mul_neg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftMono R
inst_5 : AddLeftReflectLE R
⊢ (0 < a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ a) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
simp only [neg_pos, neg_nonneg]

Premises used: neg_pos, neg_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftMono R
inst_5 : AddLeftReflectLE R
rw : (0 < -a → 0 ≤ b) ∧ (0 < b → 0 ≤ -a) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
⊢ a * b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
rw [← neg_nonneg, ← neg_mul, mul_nonneg_iff_pos_imp_nonneg (R := R)]

Premises used: mul_nonneg_iff_pos_imp_nonneg, neg_nonneg, neg_mul
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftMono R
inst_5 : AddLeftReflectLE R
⊢ (0 < -a → 0 ≤ b) ∧ (0 < b → 0 ≤ -a) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
simp only [neg_pos, neg_nonneg]

Premises used: neg_pos, neg_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
inst_2 : ZeroLEOneClass R
inst_3 : NeZero.{u} (R := R) 1
inst_4 : AddLeftStrictMono R
⊢ LT.lt.{u} (α := R) (-1) 0

Tactic:
neg_lt_zero.2 zero_lt_one

Premises used: Iff.mpr, neg_lt_zero, zero_lt_one
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
inst_2 : ZeroLEOneClass R
inst_3 : NeZero.{u} (R := R) 1
inst_4 : AddLeftStrictMono R
a : R
⊢ a - 1 < a

Tactic:
sub_lt_iff_lt_add.2 <| lt_add_one a

Premises used: Iff.mpr, lt_add_one, sub_lt_iff_lt_add
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosMono R
inst_3 : PosMulMono R
inst_4 : AddLeftMono R
h₁ : a ≤ b
h₂ : -a ≤ b
⊢ a * a ≤ b * b

Tactic:
(le_total 0 a).elim (mul_self_le_mul_self · h₁) fun h ↦
    (neg_mul_neg a a).symm.trans_le <|
      mul_le_mul h₂ h₂ (neg_nonneg.2 h) <| (neg_nonneg.2 h).trans h₂

Premises used: Iff.mpr, mul_self_le_mul_self, Eq.trans_le, le_total, neg_nonneg, mul_le_mul, neg_mul_neg, LE.le.trans, Or.elim, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : 0 ≤ x - a ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₁ : a ≤ x ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₂ : a ≤ x ∧ b ≤ x ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₃ : a ≤ x ∧ b ≤ x ∨ x ≤ a ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₄ : a ≤ x ∧ b ≤ x ∨ x ≤ a ∧ x ≤ b ↔ x ≤ a ∨ b ≤ x
rw₅ : b ≤ x ∨ x ≤ a ∧ x ≤ b ↔ x ≤ a ∨ b ≤ x
rw₆ : b ≤ x ∨ x ≤ a ↔ x ≤ a ∨ b ≤ x
rw₇ rw₈ : x ≤ a ∨ b ≤ x ↔ x ≤ a ∨ b ≤ x
⊢ 0 ≤ (x - a) * (x - b) ↔ x ≤ a ∨ b ≤ x

Tactic:
rw [mul_nonneg_iff, sub_nonneg, sub_nonneg, sub_nonpos, sub_nonpos,
    and_iff_right_of_imp h.trans, and_iff_left_of_imp h.trans', or_comm]

Premises used: and_iff_left_of_imp, mul_nonneg_iff, LE.le.trans, sub_nonpos, or_comm, sub_nonneg, and_iff_right_of_imp, LE.le.trans'
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : b ≤ x ∧ x ≤ a → a ≤ x ∧ x ≤ b
⊢ (x - a) * (x - b) ≤ 0 ↔ a ≤ x ∧ x ≤ b

Tactic:
rw [mul_nonpos_iff, sub_nonneg, sub_nonneg, sub_nonpos, sub_nonpos, or_iff_left_iff_imp, and_comm]

Premises used: or_iff_left_iff_imp, and_comm, mul_nonpos_iff, sub_nonpos, sub_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
⊢ b ≤ x ∧ x ≤ a → a ≤ x ∧ x ≤ b

Tactic:
And.imp h.trans h.trans'

Premises used: And.imp, LE.le.trans, LE.le.trans'
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
⊢ b ≤ x ∧ x ≤ a → a ≤ x ∧ x ≤ b

Tactic:
exact And.imp h.trans h.trans'

Premises used: And.imp, LE.le.trans, LE.le.trans'
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : 0 < x - a ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₁ : a < x ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₂ : a < x ∧ b < x ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₃ : a < x ∧ b < x ∨ x < a ∧ x - b < 0 ↔ x < a ∨ b < x
rw₄ : a < x ∧ b < x ∨ x < a ∧ x < b ↔ x < a ∨ b < x
rw₅ : b < x ∨ x < a ∧ x < b ↔ x < a ∨ b < x
rw₆ : b < x ∨ x < a ↔ x < a ∨ b < x
rw₇ rw₈ : x < a ∨ b < x ↔ x < a ∨ b < x
⊢ 0 < (x - a) * (x - b) ↔ x < a ∨ b < x

Tactic:
rw [mul_pos_iff, sub_pos, sub_pos, sub_neg, sub_neg, and_iff_right_of_imp h.trans_lt,
    and_iff_left_of_imp h.trans_lt', or_comm]

Premises used: sub_neg, sub_pos, and_iff_left_of_imp, mul_pos_iff, LE.le.trans_lt', or_comm, LE.le.trans_lt, and_iff_right_of_imp
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : b < x ∧ x < a → a < x ∧ x < b
⊢ (x - a) * (x - b) < 0 ↔ a < x ∧ x < b

Tactic:
rw [mul_neg_iff, sub_pos, sub_pos, sub_neg, sub_neg, or_iff_left_iff_imp, and_comm]

Premises used: sub_neg, sub_pos, or_iff_left_iff_imp, and_comm, mul_neg_iff
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
⊢ b < x ∧ x < a → a < x ∧ x < b

Tactic:
And.imp h.trans_lt h.trans_lt'

Premises used: And.imp, LE.le.trans_lt', LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
⊢ b < x ∧ x < a → a < x ∧ x < b

Tactic:
exact And.imp h.trans_lt h.trans_lt'

Premises used: And.imp, LE.le.trans_lt', LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a : ℤ
ha : 0 ≤ a
b : ℕ
⊢ 0 ≤ mkRat a b

Tactic:
simpa using divInt_nonneg ha (Int.natCast_nonneg _)

Premises used: Rat.divInt_nonneg, Int.natCast_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
m : ℕ
s : Bool
e : ℕ
rw : 0 ≤ if s = true then normalize (↑m : ℤ) (HPow.hPow (α := ℕ) 10 e) ⋯ else (↑(m * HPow.hPow (α := ℕ) 10 e) : ℚ)
⊢ 0 ≤ Rat.ofScientific m s e

Tactic:
rw [Rat.ofScientific]

Premises used: Rat.ofScientific
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
m : ℕ
s : Bool
e : ℕ
false :
  0 ≤
    if Bool.false = Bool.true then normalize (↑m : ℤ) (HPow.hPow (α := ℕ) 10 e) ⋯
    else (↑(m * HPow.hPow (α := ℕ) 10 e) : ℚ)
true :
  0 ≤
    if Bool.true = Bool.true then normalize (↑m : ℤ) (HPow.hPow (α := ℕ) 10 e) ⋯
    else (↑(m * HPow.hPow (α := ℕ) 10 e) : ℚ)
⊢ 0 ≤ if s = Bool.true then normalize (↑m : ℤ) (HPow.hPow (α := ℕ) 10 e) ⋯ else (↑(m * HPow.hPow (α := ℕ) 10 e) : ℚ)

Tactic:
cases s
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
m e : ℕ
⊢ ¬false = true

Tactic:
decide
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
m e : ℕ
⊢ LE.le (α := ℚ) 0 (↑(m * HPow.hPow (α := ℕ) 10 e) : ℚ)

Tactic:
num_nonneg.mp <| Int.natCast_nonneg _

Premises used: Iff.mp, Rat.num_nonneg, Int.natCast_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
m e : ℕ
⊢ LE.le (α := ℚ) 0 (↑(m * HPow.hPow (α := ℕ) 10 e) : ℚ)

Tactic:
exact num_nonneg.mp <| Int.natCast_nonneg _

Premises used: Iff.mp, Rat.num_nonneg, Int.natCast_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
m e : ℕ
⊢ 0 ≤ if true = true then normalize (↑m : ℤ) (HPow.hPow (α := ℕ) 10 e) ⋯ else (↑(m * HPow.hPow (α := ℕ) 10 e) : ℚ)

Tactic:
grind [normalize_eq_mkRat, Rat.mkRat_nonneg]

Premises used: Rat.normalize_eq_mkRat, Rat.mkRat_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
K : Type u_1
inst : NNRatCast K
m : ℕ
b : Bool
d : ℕ
⊢ Eq.{u_1 + 1} (α := K) (OfScientific.ofScientific m b d)
    (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) (OfScientific.ofScientific m b d) ⋯) : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
K : Type u_1
inst : NNRatCast K
m : ℕ
s : Bool
e : ℕ
⊢ Eq.{u_1 + 1} (α := K) (↑(OfScientific.ofScientific m s e) : K) (OfScientific.ofScientific m s e)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
rw : 0 ≤ c /. d - a /. b ↔ 0 ≤ c * b - a * d
⊢ a /. b ≤ c /. d ↔ a * d ≤ c * b

Tactic:
rw [Rat.le_iff_sub_nonneg, ← Int.sub_nonneg]

Premises used: Rat.le_iff_sub_nonneg, Int.sub_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ 0 ≤ c /. d - a /. b ↔ 0 ≤ c * b - a * d

Tactic:
simp [sub_eq_add_neg, ne_of_gt b0, ne_of_gt d0, Int.mul_pos d0 b0]

Premises used: Int.mul_pos, sub_eq_add_neg, ne_of_gt
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a b : ℚ
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
Std.LawfulOrderLT.lt_iff a b

Premises used: Std.LawfulOrderLT.lt_iff
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a : ℤ
b : ℕ
hb : b ≠ 0
⊢ LT.lt (α := ℤ) 0 (↑b : ℤ)

Tactic:
simpa using Nat.pos_of_ne_zero hb

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a : ℤ
b : ℕ
hb : b ≠ 0
⊢ 0 < mkRat a b ↔ 0 < a

Tactic:
grind [mkRat_nonneg_iff, Rat.mkRat_eq_zero]

Premises used: Rat.mkRat_nonneg_iff, Rat.mkRat_eq_zero
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a : ℤ
ha : 0 < a
b : ℕ
hb : b ≠ 0
⊢ 0 < mkRat a b

Tactic:
(mkRat_pos_iff a hb).mpr ha

Premises used: Iff.mpr, Rat.mkRat_pos_iff
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a : ℤ
b : ℕ
hb : b ≠ 0
⊢ mkRat a b ≤ 0 ↔ a ≤ 0

Tactic:
grind [mkRat_pos_iff]

Premises used: Rat.mkRat_pos_iff
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a : ℤ
ha : a ≤ 0
b : ℕ
inl : mkRat a 0 ≤ 0
inr : ∀ (hb : b ≠ 0), mkRat a b ≤ 0
⊢ mkRat a b ≤ 0

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a : ℤ
ha : a ≤ 0
⊢ mkRat a 0 ≤ 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a : ℤ
ha : a ≤ 0
b : ℕ
hb : b ≠ 0
⊢ mkRat a b ≤ 0

Tactic:
(mkRat_nonpos_iff a hb).mpr ha

Premises used: Iff.mpr, Rat.mkRat_nonpos_iff
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a : ℤ
ha : a ≤ 0
b : ℕ
hb : b ≠ 0
⊢ mkRat a b ≤ 0

Tactic:
exact (mkRat_nonpos_iff a hb).mpr ha

Premises used: Iff.mpr, Rat.mkRat_nonpos_iff
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a : ℤ
b : ℕ
hb : b ≠ 0
⊢ mkRat a b < 0 ↔ a < 0

Tactic:
grind [mkRat_nonneg_iff]

Premises used: Rat.mkRat_nonneg_iff
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a : ℤ
ha : a < 0
b : ℕ
hb : b ≠ 0
⊢ mkRat a b < 0

Tactic:
(mkRat_neg_iff a hb).mpr ha

Premises used: Iff.mpr, Rat.mkRat_neg_iff
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a : ℚ
⊢ a.num ≤ 0 ↔ a ≤ 0

Tactic:
simp +instances [Int.le_iff_lt_or_eq, instLE, Rat.blt]

Premises used: Int.le_iff_lt_or_eq, Rat.blt, Rat.instLE
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a : ℚ
⊢ 0 < a.num ↔ 0 < a

Tactic:
lt_iff_lt_of_le_iff_le num_nonpos

Premises used: Rat.num_nonpos, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a : ℚ
⊢ a.num < 0 ↔ a < 0

Tactic:
lt_iff_lt_of_le_iff_le num_nonneg

Premises used: Rat.num_nonneg, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
simp :
  HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ∧
      ¬HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ↔
    a * d ≤ c * b ∧ ¬c * b ≤ a * d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) < HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ↔ a * d < c * b

Tactic:
simp only [lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
h₁ : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ↔ a * d ≤ c * b
h₂ : ¬HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ↔ ¬c * b ≤ a * d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ∧
      ¬HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ↔
    a * d ≤ c * b ∧ ¬c * b ≤ a * d

Tactic:
apply and_congr

Premises used: and_congr
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ↔ a * d ≤ c * b

Tactic:
simp [div_def', Rat.divInt_le_divInt b_pos d_pos]

Premises used: Rat.div_def', Rat.divInt_le_divInt
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ¬HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ↔ ¬c * b ≤ a * d

Tactic:
simp [div_def', Rat.divInt_le_divInt d_pos b_pos]

Premises used: Rat.div_def', Rat.divInt_le_divInt
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
q : ℚ
⊢ q.num ≤ (↑q.den : ℤ) ↔ q ≤ 1

Tactic:
simp [Rat.le_iff]

Premises used: Rat.le_iff
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
q : ℚ
⊢ q.num < (↑q.den : ℤ) ↔ q < 1

Tactic:
simp [Rat.lt_iff]

Premises used: Rat.lt_iff
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
q : ℚ
⊢ |q| = (↑q.num.natAbs : ℤ) /. (↑q.den : ℤ)

Tactic:
grind [abs_of_nonpos, neg_def, Rat.num_nonneg, abs_of_nonneg, num_divInt_den]

Premises used: Rat.num_divInt_den, abs_of_nonpos, abs_of_nonneg, Rat.num_nonneg, Rat.neg_def
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
q : ℚ
⊢ |q| = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }

Tactic:
ext ?_ ?_

Premises used: Rat.ext
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
q : ℚ
refine_1 : |q|.num = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }.num
refine_2 : |q|.den = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }.den
⊢ |q| = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }

Tactic:
refine ext ?_ ?_

Premises used: Rat.ext
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
q : ℚ
⊢ |q|.num = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }.num

Tactic:
simp [Int.abs_eq_natAbs, abs_def,
      ← Rat.mk_eq_divInt (num := q.num.natAbs) (nz := q.den_ne_zero) (c := q.reduced)]

Premises used: Rat.mk_eq_divInt, Rat.abs_def, Int.abs_eq_natAbs
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
q : ℚ
⊢ |q|.den = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }.den

Tactic:
simp [Int.abs_eq_natAbs, abs_def,
      ← Rat.mk_eq_divInt (num := q.num.natAbs) (nz := q.den_ne_zero) (c := q.reduced)]

Premises used: Rat.mk_eq_divInt, Rat.abs_def, Int.abs_eq_natAbs
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
q : ℚ
rw rw₁ : { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ : ℚ }.num = |q.num|
⊢ |q|.num = |q.num|

Tactic:
rw [abs_def']

Premises used: Rat.abs_def'
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat
Goal:
q : ℚ
rw rw₁ : { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ : ℚ }.den = q.den
⊢ |q|.den = q.den

Tactic:
rw [abs_def']

Premises used: Rat.abs_def'
-- Module: Mathlib.Algebra.Order.Ring.Units
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
rw :
  ∃ (a : Rˣ),
    ∀ (b : Rˣ),
      Xor (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) (b * a))
        (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) b)
⊢ Subgroup.index (G := Rˣ) (posSubgroup R) = 2

Tactic:
rw [Subgroup.index_eq_two_iff]

Premises used: Subgroup.index_eq_two_iff
-- Module: Mathlib.Algebra.Order.Ring.Units
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
⊢ ∃ (a : Rˣ),
    ∀ (b : Rˣ),
      Xor (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) (b * a))
        (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) b)

Tactic:
⟨-1, fun a ↦ ?_⟩

Premises used: Exists.intro, OfNat.ofNat, Neg.neg