awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * (↑db : ℤ) + nb * (↑da : ℤ) = (↑k : ℤ) * nc
h₂_1 : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₁ :
  HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _) +
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) =
    HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₂ :
  HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _) =
    HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
⊢ HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) +
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have eq : HMul.hMul (α := α) (↑nc : α) (↑k : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
    @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ =
  HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
Tactic: rw [h₁, h₂, Nat.cast_commute]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
α : Type u_1
inst : Ring α
num : ℤ
denom : ℕ
h : Invertible (α := α) (↑denom : α)
⊢ -HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _) =
    HMul.hMul (α := α) (↑num.neg : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)
have rw : HMul.hMul (α := α) (↑(-num) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _) =
  HMul.hMul (α := α) (↑num.neg : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)
Tactic: rw [← neg_mul, ← Int.cast_neg]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
α : Type u_1
inst : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul (↑db : ℤ)).sub (nb.mul (↑da : ℤ)) = Int.mul (↑k : ℤ) nc
h₂ : da.mul db = k.mul dc
⊢ IsRat (f a b) nc dc
have rw : IsRat (a + -b) nc dc
Tactic: rw [hf, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
α : Type u_1
inst : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul (↑db : ℤ)).sub (nb.mul (↑da : ℤ)) = Int.mul (↑k : ℤ) nc
h₂ : da.mul db = k.mul dc
⊢ IsRat (a + -b) nc dc
have refine : (na.mul (↑db : ℤ)).add ((-nb).mul (↑da : ℤ)) = Int.mul (↑k : ℤ) nc
Tactic: refine isRat_add rfl ra (isRat_neg (n' := -nb) rfl rb rfl) (k := k) (nc := nc) ?_ h₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
α : Type u_1
inst : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul (↑db : ℤ)).sub (nb.mul (↑da : ℤ)) = Int.mul (↑k : ℤ) nc
h₂ : da.mul db = k.mul dc
⊢ (na.mul (↑db : ℤ)).add ((-nb).mul (↑da : ℤ)) = Int.mul (↑k : ℤ) nc
have rw : (na.mul (↑db : ℤ)).add (-(nb * (↑da : ℤ))) = Int.mul (↑k : ℤ) nc
Tactic: rw [show Int.mul (-nb) _ = _ from neg_mul ..]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * nb = k * nc
h₂ : da * db = k * dc
⊢ IsNNRat
    (HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
    nc dc
have have : ∀ (this : Invertible (α := α) (↑(da * db) : α)),
  IsNNRat
    (HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
    nc dc
Tactic: have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da:α) db
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * nb = k * nc
h₂ : da * db = k * dc
this : Invertible (α := α) (↑(da * db) : α)
⊢ IsNNRat
    (HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
    nc dc
have have : ∀ (this : Invertible (α := α) (↑dc : α)),
  IsNNRat
    (HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
    nc dc
Tactic: have := invertibleOfMul' (α := α) h₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * nb = k * nc
h₂ : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
⊢ IsNNRat
    (HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
    nc dc
have refine : HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
    HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) =
  HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
Tactic: refine ⟨this, ?_⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * nb = k * nc
h₂ : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
⊢ HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have H : ∀ (a : α),
  a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
Tactic: have H := (Nat.cast_commute (α := α) da db).invOf_left.invOf_right.right_comm
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * nb = k * nc
h₂ : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
⊢ HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have h₃ : Eq.{u_1 + 1} (α := α) (↑(na * nb) : α) (↑(k * nc) : α)
Tactic: have h₁ := congr_arg (Nat.cast (R := α)) h₁
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * nb = k * nc
h₂ : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₁ : Eq.{u_1 + 1} (α := α) (↑(na * nb) : α) (↑(k * nc) : α)
⊢ HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have h₃ : HMul.hMul (α := α) (↑na : α) (↑nb : α) = HMul.hMul (α := α) (↑k : α) (↑nc : α)
Tactic: simp only [Nat.cast_mul] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * nb = k * nc
h₂ : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₁ : HMul.hMul (α := α) (↑na : α) (↑nb : α) = HMul.hMul (α := α) (↑k : α) (↑nc : α)
⊢ HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have simp : HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ =
  HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
Tactic: simp only [← mul_assoc, (Nat.cast_commute (α := α) da nb).invOf_left.right_comm, h₁]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * nb = k * nc
h₂ : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₁ : HMul.hMul (α := α) (↑na : α) (↑nb : α) = HMul.hMul (α := α) (↑k : α) (↑nc : α)
⊢ HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have h₃ : Eq.{u_1 + 1} (α := α)
  ((fun (x : ℕ) ↦
      HMul.hMul (α := α) (↑nc : α) (↑x : α) *
        (HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) *
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _))
    (da * db))
  ((fun (x : ℕ) ↦
      HMul.hMul (α := α) (↑nc : α) (↑x : α) *
        (HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) *
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _))
    (k * dc))
Tactic: have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * nb = k * nc
h₂_1 : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₁ : HMul.hMul (α := α) (↑na : α) (↑nb : α) = HMul.hMul (α := α) (↑k : α) (↑nc : α)
h₂ :
  Eq.{u_1 + 1} (α := α)
    ((fun (x : ℕ) ↦
        HMul.hMul (α := α) (↑nc : α) (↑x : α) *
          (HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
              (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) *
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _))
      (da * db))
    ((fun (x : ℕ) ↦
        HMul.hMul (α := α) (↑nc : α) (↑x : α) *
          (HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
              (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) *
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _))
      (k * dc))
⊢ HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have h₃ : HMul.hMul (α := α) (↑nc : α) (↑da : α) * (↑db : α) *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _ =
  HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
Tactic: simp only [Nat.cast_mul, ← mul_assoc] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * nb = k * nc
h₂_1 : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₁ : HMul.hMul (α := α) (↑na : α) (↑nb : α) = HMul.hMul (α := α) (↑k : α) (↑nc : α)
h₂ :
  HMul.hMul (α := α) (↑nc : α) (↑da : α) * (↑db : α) *
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _ =
    HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
⊢ HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have h₃ : HMul.hMul (α := α) (↑nc : α) (↑da : α) * (↑db : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _ =
  HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
Tactic: rw [H] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * nb = k * nc
h₂_1 : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₁ : HMul.hMul (α := α) (↑na : α) (↑nb : α) = HMul.hMul (α := α) (↑k : α) (↑nc : α)
h₂ :
  HMul.hMul (α := α) (↑nc : α) (↑da : α) * (↑db : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _ =
    HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
⊢ HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have h₃ : HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _) =
  HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
Tactic: simp only [mul_invOf_cancel_right'] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * nb = k * nc
h₂_1 : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₁ : HMul.hMul (α := α) (↑na : α) (↑nb : α) = HMul.hMul (α := α) (↑k : α) (↑nc : α)
h₂ :
  HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _) =
    HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
⊢ HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
have rw : HMul.hMul (α := α) (↑nc : α) (↑k : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ =
  HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
Tactic: rw [h₂, Nat.cast_commute]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * nb = (↑k : ℤ) * nc
h₂ : da * db = k * dc
⊢ IsRat
    (HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
    nc dc
have have : ∀ (this : Invertible (α := α) (↑(da * db) : α)),
  IsRat
    (HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
    nc dc
Tactic: have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da:α) db
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * nb = (↑k : ℤ) * nc
h₂ : da * db = k * dc
this : Invertible (α := α) (↑(da * db) : α)
⊢ IsRat
    (HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
    nc dc
have have : ∀ (this : Invertible (α := α) (↑dc : α)),
  IsRat
    (HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
    nc dc
Tactic: have := invertibleOfMul' (α := α) h₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (goal)
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * nb = (↑k : ℤ) * nc
h₂ : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
⊢ IsRat
    (HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
    nc dc
have refine : HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
    HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) =
  HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)
Tactic: refine ⟨this, ?_⟩