awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α) (@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 α
a b : α
na nb da db : ℕ
ha : IsNNRat a na da
hb : IsNNRat b nb db
h : decide (nb * da < na * db) = true
⊢ ¬a ≤ b

Tactic:
not_le_of_gt (isNNRat_lt_true hb ha h)

Premises used: not_le_of_gt, Mathlib.Meta.NormNum.isNNRat_lt_true
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
na nb da db : ℕ
ha : IsNNRat a na da
hb : IsNNRat b nb db
h : decide (nb * da ≤ na * db) = true
⊢ ¬a < b

Tactic:
not_lt_of_ge (isNNRat_le_true hb ha h)

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

Tactic:
have h := Int.cast_mono (R := α) <| of_decide_eq_true h
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num num_1 : ℤ
da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num.mul (Int.ofNat db) ≤ num_1.mul (Int.ofNat da)) = true
h : LE.le.{u_1} (α := α) (↑(num.mul (Int.ofNat db)) : α) (↑(num_1.mul (Int.ofNat 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 : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num num_1 : ℤ
da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num.mul (Int.ofNat db) ≤ num_1.mul (Int.ofNat da)) = true
h : LE.le.{u_1} (α := α) (↑(num.mul (Int.ofNat db)) : α) (↑(num_1.mul (Int.ofNat 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 : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num num_1 : ℤ
da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num.mul (Int.ofNat db) ≤ num_1.mul (Int.ofNat da)) = true
h : LE.le.{u_1} (α := α) (↑(num.mul (Int.ofNat db)) : α) (↑(num_1.mul (Int.ofNat 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 (Int.ofNat db)) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) ≤
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      HMul.hMul (α := α) (↑(num_1.mul (Int.ofNat 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 : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num num_1 : ℤ
da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num.mul (Int.ofNat db) ≤ num_1.mul (Int.ofNat da)) = true
h_2 : LE.le.{u_1} (α := α) (↑(num.mul (Int.ofNat db)) : α) (↑(num_1.mul (Int.ofNat 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 (Int.ofNat db)) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) ≤
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      HMul.hMul (α := α) (↑(num_1.mul (Int.ofNat da)) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
⊢ HMul.hMul (α := α) (↑(num.mul (Int.ofNat 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 (Int.ofNat da)) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)

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

Premises used: mul_assoc, Int.commute_cast
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num num_1 : ℤ
da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num.mul (Int.ofNat db) ≤ num_1.mul (Int.ofNat da)) = true
h_2 : LE.le.{u_1} (α := α) (↑(num.mul (Int.ofNat db)) : α) (↑(num_1.mul (Int.ofNat 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 (Int.ofNat 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 (Int.ofNat 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 [Int.ofNat_eq_natCast, Int.mul_def, Int.cast_mul, Int.cast_natCast,
      mul_invOf_cancel_right'] at h

Premises used: Int.cast_natCast, Int.mul_def, Int.ofNat_eq_natCast, Int.cast_mul, mul_invOf_cancel_right'
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num num_1 : ℤ
da db : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h_1 : decide (num.mul (Int.ofNat db) ≤ num_1.mul (Int.ofNat da)) = true
h_2 : LE.le.{u_1} (α := α) (↑(num.mul (Int.ofNat db)) : α) (↑(num_1.mul (Int.ofNat 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 [Int.commute_cast] at h

Premises used: Int.commute_cast
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Ring α
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} (α := α) ((fun (x : ℤ) ↦ ((↑x : α) : α)) (num * (↑db : ℤ)))
    ((fun (x : ℤ) ↦ ((↑x : α) : α)) (num_1 * (↑da : ℤ)))

Tactic:
have h := Int.cast_strictMono (R := α) <| of_decide_eq_true h
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Ring α
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} (α := α) ((fun (x : ℤ) ↦ ((↑x : α) : α)) (num * (↑db : ℤ)))
    ((fun (x : ℤ) ↦ ((↑x : α) : α)) (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 : Ring α
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} (α := α) ((fun (x : ℤ) ↦ ((↑x : α) : α)) (num * (↑db : ℤ)))
    ((fun (x : ℤ) ↦ ((↑x : α) : α)) (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 : Ring α
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} (α := α) ((fun (x : ℤ) ↦ ((↑x : α) : α)) (num * (↑db : ℤ)))
    ((fun (x : ℤ) ↦ ((↑x : α) : α)) (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 (α := α) ((fun (x : ℤ) ↦ ((↑x : α) : α)) (num * (↑db : ℤ)))
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) <
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      HMul.hMul (α := α) ((fun (x : ℤ) ↦ ((↑x : α) : α)) (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 : Ring α
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} (α := α) ((fun (x : ℤ) ↦ ((↑x : α) : α)) (num * (↑db : ℤ)))
    ((fun (x : ℤ) ↦ ((↑x : α) : α)) (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 (α := α) ((fun (x : ℤ) ↦ ((↑x : α) : α)) (num * (↑db : ℤ)))
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) <
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      HMul.hMul (α := α) ((fun (x : ℤ) ↦ ((↑x : α) : α)) (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 (α := α) ((fun (x : ℤ) ↦ ((↑x : α) : α)) (num_1 * (↑da : ℤ)))
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)

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

Premises used: mul_assoc, Int.commute_cast
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Ring α
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} (α := α) ((fun (x : ℤ) ↦ ((↑x : α) : α)) (num * (↑db : ℤ)))
    ((fun (x : ℤ) ↦ ((↑x : α) : α)) (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 (α := α) ((fun (x : ℤ) ↦ ((↑x : α) : α)) (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 [Int.cast_mul, Int.cast_natCast, mul_invOf_cancel_right'] at h

Premises used: Int.cast_natCast, Int.cast_mul, mul_invOf_cancel_right'
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Ring α
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} (α := α) ((fun (x : ℤ) ↦ ((↑x : α) : α)) (num * (↑db : ℤ)))
    ((fun (x : ℤ) ↦ ((↑x : α) : α)) (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 (α := α) ((fun (x : ℤ) ↦ ((↑x : α) : α)) (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 [Int.cast_mul, Int.cast_natCast, mul_invOf_cancel_right'] at h

Premises used: Int.cast_natCast, Int.cast_mul, mul_invOf_cancel_right'
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Ring α
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} (α := α) ((fun (x : ℤ) ↦ ((↑x : α) : α)) (num * (↑db : ℤ)))
    ((fun (x : ℤ) ↦ ((↑x : α) : α)) (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 : α) (@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 [Int.commute_cast] at h

Premises used: Int.commute_cast
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Nontrivial α
a b : α
na nb : ℤ
da db : ℕ
ha : IsRat a na da
hb : IsRat b nb db
h : decide (nb * (↑da : ℤ) < na * (↑db : ℤ)) = true
⊢ ¬a ≤ b

Tactic:
not_le_of_gt (isRat_lt_true hb ha h)

Premises used: Mathlib.Meta.NormNum.isRat_lt_true, not_le_of_gt
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
na nb : ℤ
da db : ℕ
ha : IsRat a na da
hb : IsRat b nb db
h : decide (nb * (↑da : ℤ) ≤ na * (↑db : ℤ)) = true
⊢ ¬a < b

Tactic:
not_lt_of_ge (isRat_le_true hb ha h)

Premises used: Mathlib.Meta.NormNum.isRat_le_true, not_lt_of_ge
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : CharZero α
a b : α
a' b' : ℕ
ha : IsNat a a'
hb : IsNat b b'
h : a'.ble b' = false
⊢ ¬a ≤ b

Tactic:
not_le_of_gt (isNat_lt_true hb ha h)

Premises used: Mathlib.Meta.NormNum.isNat_lt_true, not_le_of_gt
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : Nontrivial α
a b : α
a' b' : ℤ
ha : IsInt a a'
hb : IsInt b b'
h : decide (b' < a') = true
⊢ ¬a ≤ b

Tactic:
not_le_of_gt (isInt_lt_true hb ha h)

Premises used: Mathlib.Meta.NormNum.isInt_lt_true, not_le_of_gt
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
a b : α
a' b' : ℤ
ha : IsInt a a'
hb : IsInt b b'
h : decide (b' ≤ a') = true
⊢ ¬a < b

Tactic:
not_lt_of_ge (isInt_le_true hb ha h)

Premises used: Mathlib.Meta.NormNum.isInt_le_true, not_lt_of_ge
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
«$u_1» «$u» : Level
«$α» : Type u
«$lα» : LE «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» «$nb» : ℕ
«$fst» : Semiring «$α»
«$fst_1» : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»

Tactic:
infer_instance
-- Module: Mathlib.Tactic.NormNum.Ineq
Goal:
«$u_1» «$u» : Level
«$α» : Type u
«$lα» : LT «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» «$nb» : ℕ
«$fst» : Semiring «$α»
«$fst_1» : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»

Tactic:
infer_instance
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
n num : ℤ
n_1 denom : ℕ
inv : Invertible (α := ℚ) (↑denom : ℚ)
h :
  HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑n_1 : ℚ) =
    HMul.hMul (α := ℚ) (↑num : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : ℚ) _)
rw : IsRat (HDiv.hDiv (α := ℚ) (↑(↑n : ℤ) : ℚ) (↑(↑n_1 : ℕ) : ℚ)) num denom
⊢ IsRat (mkRat (↑n : ℤ) (↑n_1 : ℕ)) num denom

Tactic:
rw [Rat.mkRat_eq_div]

Premises used: Rat.mkRat_eq_div
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
n num : ℤ
n_1 denom : ℕ
inv : Invertible (α := ℚ) (↑denom : ℚ)
h :
  HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑n_1 : ℚ) =
    HMul.hMul (α := ℚ) (↑num : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : ℚ) _)
⊢ IsRat (HDiv.hDiv (α := ℚ) (↑(↑n : ℤ) : ℚ) (↑(↑n_1 : ℕ) : ℚ)) num denom

Tactic:
⟨_, h⟩

Premises used: Mathlib.Meta.NormNum.IsRat.mk
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
n num : ℤ
n_1 denom : ℕ
inv : Invertible (α := ℚ) (↑denom : ℚ)
h :
  HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑n_1 : ℚ) =
    HMul.hMul (α := ℚ) (↑num : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : ℚ) _)
⊢ IsRat (HDiv.hDiv (α := ℚ) (↑(↑n : ℤ) : ℚ) (↑(↑n_1 : ℕ) : ℚ)) num denom

Tactic:
exact ⟨_, h⟩
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
R : Type u_1
inst : DivisionRing R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑(↑n : ℚ) : R) (↑n : R)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
R : Type u_1
inst : DivisionRing R
n : ℤ
⊢ Eq.{u_1 + 1} (α := R) (↑(↑n : ℚ) : R) (↑n : R)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
num denom : ℕ
qi : ℚ
invOf_mul_self : qi * (↑denom : ℚ) = 1
mul_invOf_self : (↑denom : ℚ) * qi = 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : qi * (↑denom : ℚ) = 1
⊢ HMul.hMul (α := R) (↑qi : R) (↑denom : R) = 1

Tactic:
norm_cast
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
num denom : ℕ
qi : ℚ
invOf_mul_self : qi * (↑denom : ℚ) = 1
mul_invOf_self : (↑denom : ℚ) * qi = 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑denom : ℚ) * qi = 1
⊢ HMul.hMul (α := R) (↑denom : R) (↑qi : R) = 1

Tactic:
norm_cast
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
num denom : ℕ
qi : ℚ
invOf_mul_self : qi * (↑denom : ℚ) = 1
mul_invOf_self : (↑denom : ℚ) * qi = 1
simp : (↑((↑num : ℚ) * qi) : R) = HMul.hMul (α := R) (↑num : R) (↑qi : R)
⊢ (↑(HMul.hMul (α := ℚ) (↑num : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : ℚ) _)) : R) =
    HMul.hMul (α := R) (↑num : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : R) _)

Tactic:
simp only
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
num denom : ℕ
qi : ℚ
invOf_mul_self : qi * (↑denom : ℚ) = 1
mul_invOf_self : (↑denom : ℚ) * qi = 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑num : ℚ) * qi = (↑num : ℚ) * qi
⊢ (↑((↑num : ℚ) * qi) : R) = HMul.hMul (α := R) (↑num : R) (↑qi : R)

Tactic:
norm_cast
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
num : ℤ
denom : ℕ
qi : ℚ
invOf_mul_self : qi * (↑denom : ℚ) = 1
mul_invOf_self : (↑denom : ℚ) * qi = 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : qi * (↑denom : ℚ) = 1
⊢ HMul.hMul (α := R) (↑qi : R) (↑denom : R) = 1

Tactic:
norm_cast