awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
d : ℕ
x y a b : ℤ
h₁ : (↑d : ℤ) ∣ x
h₂ : (↑d : ℤ) ∣ y
h₃ : x * a + y * b = (↑d : ℤ)
⊢ (↑(x.gcd y) : ℤ) ∣ x * a

Tactic:
exact (Int.gcd_dvd_left ..).mul_right _

Premises used: Dvd.dvd.mul_right, Int.gcd_dvd_left
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
d : ℕ
x y a b : ℤ
h₁ : (↑d : ℤ) ∣ x
h₂ : (↑d : ℤ) ∣ y
h₃ : x * a + y * b = (↑d : ℤ)
⊢ (↑(x.gcd y) : ℤ) ∣ y * b

Tactic:
(Int.gcd_dvd_right ..).mul_right _

Premises used: Dvd.dvd.mul_right, Int.gcd_dvd_right
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
d : ℕ
x y a b : ℤ
h₁ : (↑d : ℤ) ∣ x
h₂ : (↑d : ℤ) ∣ y
h₃ : x * a + y * b = (↑d : ℤ)
⊢ (↑(x.gcd y) : ℤ) ∣ y * b

Tactic:
exact (Int.gcd_dvd_right ..).mul_right _

Premises used: Dvd.dvd.mul_right, Int.gcd_dvd_right
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
x y : ℕ
h : y % x = 0
⊢ x.gcd y = x

Tactic:
Nat.gcd_eq_left (Nat.dvd_of_mod_eq_zero h)

Premises used: Nat.gcd_eq_left, Nat.dvd_of_mod_eq_zero
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
x y : ℕ
h : x % y = 0
⊢ x.gcd y = y

Tactic:
Nat.gcd_eq_right (Nat.dvd_of_mod_eq_zero h)

Premises used: Nat.dvd_of_mod_eq_zero, Nat.gcd_eq_right
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
rw : Int.gcd (↑x : ℤ) (↑y : ℤ) = d
⊢ x.gcd y = d

Tactic:
rw [← Int.gcd_natCast_natCast]

Premises used: Int.gcd_natCast_natCast
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
apply : HMul.hMul (α := ℤ) (↑x : ℤ) (↑a : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (-(↑b : ℤ)) = (↑d : ℤ)
⊢ Int.gcd (↑x : ℤ) (↑y : ℤ) = d

Tactic:
apply int_gcd_helper' a (-b)
    (Int.natCast_dvd_natCast.mpr (Nat.dvd_of_mod_eq_zero hu))
    (Int.natCast_dvd_natCast.mpr (Nat.dvd_of_mod_eq_zero hv))

Premises used: Iff.mpr, Tactic.NormNum.int_gcd_helper', Nat.cast, Nat.dvd_of_mod_eq_zero, Neg.neg, Int.natCast_dvd_natCast
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
rw : HMul.hMul (α := ℤ) (↑x : ℤ) (↑a : ℤ) = HMul.hMul (α := ℤ) (↑y : ℤ) (↑b : ℤ) + (↑d : ℤ)
⊢ HMul.hMul (α := ℤ) (↑x : ℤ) (↑a : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (-(↑b : ℤ)) = (↑d : ℤ)

Tactic:
rw [mul_neg, ← sub_eq_add_neg, sub_eq_iff_eq_add']

Premises used: sub_eq_add_neg, sub_eq_iff_eq_add', mul_neg
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ HMul.hMul (α := ℤ) (↑x : ℤ) (↑a : ℤ) = HMul.hMul (α := ℤ) (↑y : ℤ) (↑b : ℤ) + (↑d : ℤ)

Tactic:
mod_cast h

Premises used: Nat.cast_mul._simp_1, HMul.hMul, congrArg, Nat.cast_add._simp_1, cast, Nat.cast, HAdd.hAdd, congr, Nat.cast_inj._simp_1, congrFun', Eq.symm, Eq, Eq.trans
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ HMul.hMul (α := ℤ) (↑x : ℤ) (↑a : ℤ) = HMul.hMul (α := ℤ) (↑y : ℤ) (↑b : ℤ) + (↑d : ℤ)

Tactic:
exact mod_cast h
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : y * b = x * a + d
⊢ x.gcd y = d

Tactic:
(Nat.gcd_comm _ _).trans <| nat_gcd_helper_2 _ _ _ _ _ hv hu h

Premises used: Tactic.NormNum.nat_gcd_helper_2, Nat.gcd_comm, Eq.trans
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
x y a b : ℕ
h : y * b = x * a + 1
⊢ x.gcd y = 1

Tactic:
nat_gcd_helper_1 1 _ _ _ _ (Nat.mod_one _) (Nat.mod_one _) h

Premises used: Nat.mod_one, Tactic.NormNum.nat_gcd_helper_1, OfNat.ofNat
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
x y a b : ℕ
h : x * a = y * b + 1
⊢ x.gcd y = 1

Tactic:
nat_gcd_helper_2 1 _ _ _ _ (Nat.mod_one _) (Nat.mod_one _) h

Premises used: Nat.mod_one, Tactic.NormNum.nat_gcd_helper_2, OfNat.ofNat
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
x y d m : ℕ
hd : x.gcd y = d
d0 : d.beq 0 = false
dm : x * y = d * m
rw : d * x.lcm y = x * y
rw₁ : x.gcd y * x.lcm y = x * y
rw₂ rw₃ : x * y = x * y
⊢ d * x.lcm y = d * m

Tactic:
rw [← dm, ← hd, Nat.gcd_mul_lcm]

Premises used: Nat.gcd_mul_lcm
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
x y : ℤ
x' y' d : ℕ
hx : x.natAbs = x'
hy : y.natAbs = y'
h : x'.gcd y' = d
subst_vars : x.gcd y = x.natAbs.gcd y.natAbs
⊢ x.gcd y = d

Tactic:
subst_vars
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
x y : ℤ
rw rw₁ : x.natAbs.gcd y.natAbs = x.natAbs.gcd y.natAbs
⊢ x.gcd y = x.natAbs.gcd y.natAbs

Tactic:
rw [Int.gcd_def]

Premises used: Int.gcd_def
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
x y : ℤ
x' y' d : ℕ
hx : x.natAbs = x'
hy : y.natAbs = y'
h : x'.lcm y' = d
subst_vars : x.lcm y = x.natAbs.lcm y.natAbs
⊢ x.lcm y = d

Tactic:
subst_vars
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
x y : ℤ
rw rw₁ : x.natAbs.lcm y.natAbs = x.natAbs.lcm y.natAbs
⊢ x.lcm y = x.natAbs.lcm y.natAbs

Tactic:
rw [Int.lcm_def]

Premises used: Int.lcm_def
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
n : ℤ
d : ℕ
hi : Invertible (α := ℚ) (↑d : ℚ)
h : n.natAbs.gcd d = 1
out : (HMul.hMul (α := ℚ) (↑n : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).num = (↑n : ℤ)
⊢ IsInt (HMul.hMul (α := ℚ) (↑n : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).num n

Tactic:
constructor
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
n : ℤ
d : ℕ
hi : Invertible (α := ℚ) (↑d : ℚ)
h : n.natAbs.gcd d = 1
⊢ d ≠ 0

Tactic:
simpa using hi.ne_zero

Premises used: Invertible.ne_zero
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
n : ℤ
d : ℕ
hi : Invertible (α := ℚ) (↑d : ℚ)
h : n.natAbs.gcd d = 1
⊢ 0 < d

Tactic:
have : 0 < d := Nat.pos_iff_ne_zero.mpr <| by simpa using hi.ne_zero
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
n : ℤ
d : ℕ
hi : Invertible (α := ℚ) (↑d : ℚ)
h : n.natAbs.gcd d = 1
this : 0 < d
out :
  Rat.num (↑n : ℚ) * Rat.num (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _) /
      (↑((Rat.num (↑n : ℚ) * Rat.num (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).natAbs.gcd
            (Rat.den (↑n : ℚ) * Rat.den (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _))) :
        ℤ) =
    (↑n : ℤ)
out₁ :
  Rat.num (↑n : ℚ) * Rat.num (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _) /
      (↑((Rat.num (↑n : ℚ) * Rat.num (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).natAbs.gcd
            (1 * Rat.den (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _))) :
        ℤ) =
    (↑n : ℤ)
out₂ :
  Rat.num (↑n : ℚ) * Rat.num (↑d : ℚ)⁻¹ /
      (↑((Rat.num (↑n : ℚ) * Rat.num (↑d : ℚ)⁻¹).natAbs.gcd (1 * Rat.den (↑d : ℚ)⁻¹)) : ℤ) =
    (↑n : ℤ)
out₃ :
  Rat.num (↑n : ℚ) * Rat.num (↑d : ℚ)⁻¹ / (↑((Rat.num (↑n : ℚ) * Rat.num (↑d : ℚ)⁻¹).natAbs.gcd (1 * d)) : ℤ) = (↑n : ℤ)
out₄ : Rat.num (↑n : ℚ) * 1 / (↑((Rat.num (↑n : ℚ) * 1).natAbs.gcd (1 * d)) : ℤ) = (↑n : ℤ)
out₅ : n * 1 / (↑((n * 1).natAbs.gcd (1 * d)) : ℤ) = (↑n : ℤ)
out₆ : n * 1 / (↑((n * 1).natAbs.gcd d) : ℤ) = (↑n : ℤ)
out₇ : n / (↑(n.natAbs.gcd d) : ℤ) = (↑n : ℤ)
out₈ : n / (↑1 : ℤ) = (↑n : ℤ)
out₉ : n / 1 = (↑n : ℤ)
out₁₀ : n = (↑n : ℤ)
⊢ (HMul.hMul (α := ℚ) (↑n : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).num = (↑n : ℤ)

Tactic:
simp_rw [Rat.mul_num, Rat.den_intCast, invOf_eq_inv,
      Rat.inv_natCast_den_of_pos this, Rat.inv_natCast_num_of_pos this,
      Rat.num_intCast, one_mul, mul_one, h, Nat.cast_one, Int.ediv_one, Int.cast_id]

Premises used: Rat.inv_natCast_num_of_pos, Int.ediv_one, Rat.den_intCast, Rat.inv_natCast_den_of_pos, Int.cast_id, invOf_eq_inv, mul_one, Rat.mul_num, Nat.cast_one, one_mul, Rat.num_intCast
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
n : ℤ
d : ℕ
hi : Invertible (α := ℚ) (↑d : ℚ)
h : n.natAbs.gcd d = 1
out : (HMul.hMul (α := ℚ) (↑n : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).den = (↑d : ℕ)
⊢ IsNat (HMul.hMul (α := ℚ) (↑n : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).den d

Tactic:
constructor
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
n : ℤ
d : ℕ
hi : Invertible (α := ℚ) (↑d : ℚ)
h : n.natAbs.gcd d = 1
this : 0 < d
out :
  Rat.den (↑n : ℚ) * Rat.den (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _) /
      (Rat.num (↑n : ℚ) * Rat.num (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).natAbs.gcd
        (Rat.den (↑n : ℚ) * Rat.den (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)) =
    (↑d : ℕ)
out₁ :
  1 * Rat.den (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _) /
      (Rat.num (↑n : ℚ) * Rat.num (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).natAbs.gcd
        (1 * Rat.den (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)) =
    (↑d : ℕ)
out₂ : 1 * Rat.den (↑d : ℚ)⁻¹ / (Rat.num (↑n : ℚ) * Rat.num (↑d : ℚ)⁻¹).natAbs.gcd (1 * Rat.den (↑d : ℚ)⁻¹) = (↑d : ℕ)
out₃ : 1 * d / (Rat.num (↑n : ℚ) * Rat.num (↑d : ℚ)⁻¹).natAbs.gcd (1 * d) = (↑d : ℕ)
out₄ : 1 * d / (Rat.num (↑n : ℚ) * 1).natAbs.gcd (1 * d) = (↑d : ℕ)
out₅ : 1 * d / (n * 1).natAbs.gcd (1 * d) = (↑d : ℕ)
out₆ : d / (n * 1).natAbs.gcd d = (↑d : ℕ)
out₇ : d / n.natAbs.gcd d = (↑d : ℕ)
out₈ : d / n.natAbs.gcd d = d
out₉ : d / 1 = d
⊢ (HMul.hMul (α := ℚ) (↑n : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).den = (↑d : ℕ)

Tactic:
simp_rw [Rat.mul_den, Rat.den_intCast, invOf_eq_inv,
      Rat.inv_natCast_den_of_pos this, Rat.inv_natCast_num_of_pos this,
      Rat.num_intCast, one_mul, mul_one, Nat.cast_id, h, Nat.div_one]

Premises used: Nat.cast_id, Rat.inv_natCast_num_of_pos, Rat.den_intCast, Nat.div_one, Rat.inv_natCast_den_of_pos, invOf_eq_inv, mul_one, Rat.mul_den, one_mul, Rat.num_intCast
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
a b : α
a' b' : ℕ
ha : IsNat a a'
hb : IsNat b b'
h : b'.ble a' = true
⊢ ¬a < b

Tactic:
not_lt_of_ge (isNat_le_true hb ha h)

Premises used: Mathlib.Meta.NormNum.isNat_le_true, not_lt_of_ge
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num num_1 da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h : decide (num.mul db ≤ num_1.mul da) = true
⊢ LE.le.{u_1} (α := α) (↑(num.mul db) : α) (↑(num_1.mul da) : α)

Tactic:
have h := (Nat.cast_le (α := α)).mpr <| of_decide_eq_true h
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num num_1 da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num.mul db ≤ num_1.mul da) = true
h : LE.le.{u_1} (α := α) (↑(num.mul db) : α) (↑(num_1.mul da) : α)
⊢ LE.le.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)

Tactic:
have ha : 0 ≤ ⅟(da : α) := invOf_nonneg.mpr <| Nat.cast_nonneg da
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num num_1 da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num.mul db ≤ num_1.mul da) = true
h : LE.le.{u_1} (α := α) (↑(num.mul db) : α) (↑(num_1.mul da) : α)
ha : LE.le.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
⊢ LE.le.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)

Tactic:
have hb : 0 ≤ ⅟(db : α) := invOf_nonneg.mpr <| Nat.cast_nonneg db
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num num_1 da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num.mul db ≤ num_1.mul da) = true
h : LE.le.{u_1} (α := α) (↑(num.mul db) : α) (↑(num_1.mul da) : α)
ha : LE.le.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
hb : LE.le.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      HMul.hMul (α := α) (↑(num.mul db) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) ≤
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      HMul.hMul (α := α) (↑(num_1.mul da) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)

Tactic:
have h := (mul_le_mul_of_nonneg_left · hb) <| mul_le_mul_of_nonneg_right h ha
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num num_1 da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num.mul db ≤ num_1.mul da) = true
h_2 : LE.le.{u_1} (α := α) (↑(num.mul db) : α) (↑(num_1.mul da) : α)
ha : LE.le.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
hb : LE.le.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
h :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      HMul.hMul (α := α) (↑(num.mul db) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) ≤
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      HMul.hMul (α := α) (↑(num_1.mul da) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
⊢ HMul.hMul (α := α) (↑(num.mul db) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ ≤
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      HMul.hMul (α := α) (↑(num_1.mul da) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)

Tactic:
rw [← mul_assoc, Nat.commute_cast] at h

Premises used: Nat.commute_cast, mul_assoc
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num num_1 da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num.mul db ≤ num_1.mul da) = true
h_2 : LE.le.{u_1} (α := α) (↑(num.mul db) : α) (↑(num_1.mul da) : α)
ha : LE.le.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
hb : LE.le.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
h :
  HMul.hMul (α := α) (↑(num.mul db) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ ≤
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      HMul.hMul (α := α) (↑(num_1.mul da) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) ≤
    HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) (↑num_1 : α)

Tactic:
simp only [Nat.mul_eq, Nat.cast_mul, mul_invOf_cancel_right'] at h

Premises used: Nat.cast_mul, Nat.mul_eq, mul_invOf_cancel_right'
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num num_1 da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num.mul db ≤ num_1.mul da) = true
h_2 : LE.le.{u_1} (α := α) (↑(num.mul db) : α) (↑(num_1.mul da) : α)
ha : LE.le.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
hb : LE.le.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
h :
  HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) ≤
    HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) (↑num_1 : α)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (h :
      HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) ≤
        HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)),
    HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) ≤
      HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) ≤
    HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)

Tactic:
rwa [Nat.commute_cast] at h

Premises used: Nat.commute_cast
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Nontrivial α
num num_1 da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h : decide (num * db < num_1 * da) = true
⊢ LT.lt.{u_1} (α := α) (↑(num * db) : α) (↑(num_1 * da) : α)

Tactic:
have h := (Nat.cast_lt (α := α)).mpr <| of_decide_eq_true h
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Nontrivial α
num num_1 da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num * db < num_1 * da) = true
h : LT.lt.{u_1} (α := α) (↑(num * db) : α) (↑(num_1 * da) : α)
⊢ LT.lt.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)

Tactic:
have ha : 0 < ⅟(da : α) := pos_invOf_of_invertible_cast da
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Nontrivial α
num num_1 da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num * db < num_1 * da) = true
h : LT.lt.{u_1} (α := α) (↑(num * db) : α) (↑(num_1 * da) : α)
ha : LT.lt.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
⊢ LT.lt.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)

Tactic:
have hb : 0 < ⅟(db : α) := pos_invOf_of_invertible_cast db
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Nontrivial α
num num_1 da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num * db < num_1 * da) = true
h : LT.lt.{u_1} (α := α) (↑(num * db) : α) (↑(num_1 * da) : α)
ha : LT.lt.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
hb : LT.lt.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      HMul.hMul (α := α) (↑(num * db) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) <
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      HMul.hMul (α := α) (↑(num_1 * da) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)

Tactic:
have h := (mul_lt_mul_of_pos_left · hb) <| mul_lt_mul_of_pos_right h ha
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Nontrivial α
num num_1 da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num * db < num_1 * da) = true
h_2 : LT.lt.{u_1} (α := α) (↑(num * db) : α) (↑(num_1 * da) : α)
ha : LT.lt.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
hb : LT.lt.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
h :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      HMul.hMul (α := α) (↑(num * db) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) <
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      HMul.hMul (α := α) (↑(num_1 * da) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
⊢ HMul.hMul (α := α) (↑(num * db) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ <
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      HMul.hMul (α := α) (↑(num_1 * da) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)

Tactic:
rw [← mul_assoc, Nat.commute_cast] at h

Premises used: Nat.commute_cast, mul_assoc
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Nontrivial α
num num_1 da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num * db < num_1 * da) = true
h_2 : LT.lt.{u_1} (α := α) (↑(num * db) : α) (↑(num_1 * da) : α)
ha : LT.lt.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
hb : LT.lt.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
h :
  HMul.hMul (α := α) (↑(num * db) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ <
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      HMul.hMul (α := α) (↑(num_1 * da) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) <
    HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) (↑num_1 : α)

Tactic:
simp only [Nat.cast_mul, mul_invOf_cancel_right'] at h

Premises used: Nat.cast_mul, mul_invOf_cancel_right'
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Nontrivial α
num num_1 da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num * db < num_1 * da) = true
h_2 : LT.lt.{u_1} (α := α) (↑(num * db) : α) (↑(num_1 * da) : α)
ha : LT.lt.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
hb : LT.lt.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
h :
  HMul.hMul (α := α) (↑(num * db) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ <
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      HMul.hMul (α := α) (↑(num_1 * da) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) <
    HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) (↑num_1 : α)

Tactic:
simp? at h says simp only [Nat.cast_mul, mul_invOf_cancel_right'] at h

Premises used: Nat.cast_mul, mul_invOf_cancel_right'