awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
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 : ℕ)
⊢ (HMul.hMul (α := ℚ) (↑n : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).den = (↑d : ℕ)
have out₆ : d / (n * 1).natAbs.gcd d = (↑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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
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 : ℕ)
⊢ (HMul.hMul (α := ℚ) (↑n : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).den = (↑d : ℕ)
have out₇ : d / n.natAbs.gcd d = (↑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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
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 : ℕ)
⊢ (HMul.hMul (α := ℚ) (↑n : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).den = (↑d : ℕ)
have out₈ : d / n.natAbs.gcd d = 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
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
⊢ (HMul.hMul (α := ℚ) (↑n : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).den = (↑d : ℕ)
have out₉ : d / 1 = 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) ≤
    HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
have h₁ : LE.le.{u_1} (α := α) (↑(num.mul db) : α) (↑(num_1.mul da) : α)
Tactic: have h := (Nat.cast_le (α := α)).mpr <| of_decide_eq_true h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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) : α)
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) ≤
    HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
have ha : LE.le.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
Tactic: have ha : 0 ≤ ⅟(da : α) := invOf_nonneg.mpr <| Nat.cast_nonneg da
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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 : α) _)
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) ≤
    HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
have hb : LE.le.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
Tactic: have hb : 0 ≤ ⅟(db : α) := invOf_nonneg.mpr <| Nat.cast_nonneg db
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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 : α) _)
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) ≤
    HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
have 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 : α) _)
Tactic: have h := (mul_le_mul_of_nonneg_left · hb) <| mul_le_mul_of_nonneg_right h ha
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) ≤
    HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
have 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 : α) _)
Tactic: rw [← mul_assoc, Nat.commute_cast] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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 (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (goal)
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 : α)
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) ≤
    HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
have 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 : α) _)
Tactic: rwa [Nat.commute_cast] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) <
    HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
have h₁ : LT.lt.{u_1} (α := α) (↑(num * db) : α) (↑(num_1 * da) : α)
Tactic: have h := (Nat.cast_lt (α := α)).mpr <| of_decide_eq_true h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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) : α)
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) <
    HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
have ha : LT.lt.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
Tactic: have ha : 0 < ⅟(da : α) := pos_invOf_of_invertible_cast da
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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 : α) _)
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) <
    HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
have hb : LT.lt.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
Tactic: have hb : 0 < ⅟(db : α) := pos_invOf_of_invertible_cast db
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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 : α) _)
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) <
    HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
have 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 : α) _)
Tactic: have h := (mul_lt_mul_of_pos_left · hb) <| mul_lt_mul_of_pos_right h ha
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) <
    HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
have 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 : α) _)
Tactic: rw [← mul_assoc, Nat.commute_cast] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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 (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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 (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (goal)
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 : α)
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) <
    HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
have 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 : α) _)
Tactic: rwa [Nat.commute_cast] at h
Cleared hypotheses: h