awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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
⊢ 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 (Int.ofNat db)) : α) (↑(num_1.mul (Int.ofNat da)) : α)
Tactic: have h := Int.cast_mono (R := α) <| of_decide_eq_true h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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)) : α)
⊢ 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 : 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 : α) _)
⊢ 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 : 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 : α) _)
⊢ 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 (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
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) ≤
    HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _)
have 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 : α) _)
Tactic: rw [← mul_assoc, Int.commute_cast] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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 (α := α) (↑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 [Int.ofNat_eq_natCast, Int.mul_def, Int.cast_mul, Int.cast_natCast,
      mul_invOf_cancel_right'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (goal)
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 : α)
⊢ 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 [Int.commute_cast] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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
⊢ 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} (α := α) ((fun (x : ℤ) ↦ ((↑x : α) : α)) (num * (↑db : ℤ)))
  ((fun (x : ℤ) ↦ ((↑x : α) : α)) (num_1 * (↑da : ℤ)))
Tactic: have h := Int.cast_strictMono (R := α) <| of_decide_eq_true h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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 : ℤ)))
⊢ 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 : 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 : α) _)
⊢ 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 : 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 : α) _)
⊢ 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 (α := α) ((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
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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 : α) (@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 (α := α) ((fun (x : ℤ) ↦ ((↑x : α) : α)) (num_1 * (↑da : ℤ)))
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
Tactic: rw [← mul_assoc, Int.commute_cast] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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 (α := α) (↑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 [Int.cast_mul, Int.cast_natCast, mul_invOf_cancel_right'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (hypothesis)
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 (α := α) (↑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 [Int.cast_mul, Int.cast_natCast, mul_invOf_cancel_right'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Ineq (goal)
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 : α)
⊢ 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 [Int.commute_cast] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Inv (goal)
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 (mkRat (↑n : ℤ) (↑n_1 : ℕ)) num denom
have rw : IsRat (HDiv.hDiv (α := ℚ) (↑(↑n : ℤ) : ℚ) (↑(↑n_1 : ℕ) : ℚ)) num denom
Tactic: rw [Rat.mkRat_eq_div]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Inv (goal)
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
⊢ (↑(HMul.hMul (α := ℚ) (↑num : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : ℚ) _)) : R) =
    HMul.hMul (α := R) (↑num : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : R) _)
have simp : (↑((↑num : ℚ) * qi) : R) = HMul.hMul (α := R) (↑num : R) (↑qi : R)
Tactic: simp only
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Inv (goal)
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
⊢ (↑((↑num : ℚ) * qi) : R) = HMul.hMul (α := R) (↑num : R) (↑qi : R)
have norm_cast : (↑num : ℚ) * qi = (↑num : ℚ) * qi
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Inv (goal)
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
⊢ (↑(HMul.hMul (α := ℚ) (↑num : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : ℚ) _)) : R) =
    HMul.hMul (α := R) (↑num : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : R) _)
have simp : (↑((↑num : ℚ) * qi) : R) = HMul.hMul (α := R) (↑num : R) (↑qi : R)
Tactic: simp only
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Inv (goal)
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
⊢ (↑((↑num : ℚ) * qi) : R) = HMul.hMul (α := R) (↑num : R) (↑qi : R)
have norm_cast : (↑num : ℚ) * qi = (↑num : ℚ) * qi
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Inv (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
inst_1 : CharZero α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
⊢ IsNNRat (HMul.hMul (α := α) (↑n.succ : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹ d
    n.succ
have have : ∀ (this : Invertible (α := α) (↑n.succ : α)),
  IsNNRat (HMul.hMul (α := α) (↑n.succ : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹ d
    n.succ
Tactic: have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Inv (goal)
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
⊢ IsRat
    (HMul.hMul (α := α) (↑(Int.ofNat n.succ) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
    (Int.ofNat d) n.succ
have have : ∀ (this : Invertible (α := α) (↑n.succ : α)),
  IsRat
    (HMul.hMul (α := α) (↑(Int.ofNat n.succ) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
    (Int.ofNat d) n.succ
Tactic: have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Inv (goal)
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
⊢ IsRat
    (HMul.hMul (α := α) (↑(Int.negOfNat n.succ) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
    (Int.negOfNat d) n.succ
have simp : IsRat
  (HMul.hMul (α := α) (↑(-Int.ofNat n.succ) : α)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
  (-Int.ofNat d) n.succ
Tactic: simp only [Int.negOfNat_eq]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Inv (goal)
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
⊢ IsRat
    (HMul.hMul (α := α) (↑(-Int.ofNat n.succ) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
    (-Int.ofNat d) n.succ
have have : ∀ (this : Invertible (α := α) (↑n.succ : α)),
  IsRat
    (HMul.hMul (α := α) (↑(-Int.ofNat n.succ) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
    (-Int.ofNat d) n.succ
Tactic: have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))