awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * db + nb * da = k * nc
h₂ : da * db = k * dc
this : Invertible (α := α) (↑(da * db) : α)
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
⊢ 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₂
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * db + nb * da = k * nc
h₂ : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
eq :
  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 : α) _)
⊢ IsNNRat
    (HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) +
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
    nc dc

Tactic:
use this
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * db + nb * da = k * nc
h₂ : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
⊢ ∀ (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
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * db + nb * da = 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 : α) _
⊢ Eq.{u_1 + 1} (α := α)
    ((fun (x : ℕ) ↦
        (↑x : α) *
          HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
      (na * db + nb * da))
    ((fun (x : ℕ) ↦
        (↑x : α) *
          HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
      (k * nc))

Tactic:
have h₁ := congr_arg (↑· * (⅟↑da * ⅟↑db : α)) h₁
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * db + nb * da = 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} (α := α)
    ((fun (x : ℕ) ↦
        (↑x : α) *
          HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
      (na * db + nb * da))
    ((fun (x : ℕ) ↦
        (↑x : α) *
          HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
      (k * nc))
⊢ HMul.hMul (α := α) (↑na : α) (↑db : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ +
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) =
    HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _

Tactic:
simp only [Nat.cast_add, Nat.cast_mul, ← mul_assoc,
    add_mul, mul_invOf_cancel_right] at h₁

Premises used: add_mul, mul_assoc, mul_invOf_cancel_right, Nat.cast_add, Nat.cast_mul
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * db + nb * da = 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 : α) (↑db : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ +
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) =
    HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _
⊢ 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₂
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Semiring α
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 : α) (↑db : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ +
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) =
    HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _
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 (α := α) (↑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 : α) _

Tactic:
simp only [H, mul_invOf_cancel_right', Nat.cast_mul, ← mul_assoc] at h₁ h₂

Premises used: mul_assoc, Nat.cast_mul, mul_invOf_cancel_right'
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Semiring α
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 : α) (↑db : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ +
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) =
    HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _
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))
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 : α) _
⊢ 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 : α) _

Tactic:
simp only [H, mul_invOf_cancel_right', Nat.cast_mul, ← mul_assoc] at h₁ h₂

Premises used: mul_assoc, Nat.cast_mul, mul_invOf_cancel_right'
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Semiring α
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 : α) _
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 : α) _
⊢ 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:
rw [h₁, h₂, Nat.cast_commute]

Premises used: Nat.cast_commute
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Semiring α
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 (α := α) (↑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:
simp only [mul_invOf_cancel_right,
    (Nat.cast_commute (α := α) da dc).invOf_left.invOf_right.right_comm,
    (Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]

Premises used: Commute.invOf_right, mul_invOf_cancel_right, Nat.cast, Commute.invOf_left, Commute.right_comm, Nat.cast_commute
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * (↑db : ℤ) + nb * (↑da : ℤ) = (↑k : ℤ) * nc
h₂ : da * db = k * dc
⊢ Invertible (α := α) (↑(da * db) : α)

Tactic:
simpa using invertibleMul (da:α) db

Premises used: Nat.cast, invertibleMul
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * (↑db : ℤ) + nb * (↑da : ℤ) = (↑k : ℤ) * nc
h₂ : da * db = k * dc
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
⊢ 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
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * (↑db : ℤ) + nb * (↑da : ℤ) = (↑k : ℤ) * nc
h₂ : da * db = k * dc
this : Invertible (α := α) (↑(da * db) : α)
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
⊢ 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₂
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * (↑db : ℤ) + nb * (↑da : ℤ) = (↑k : ℤ) * nc
h₂ : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
eq :
  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 : α) _)
⊢ IsRat
    (HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) +
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
    nc dc

Tactic:
use this
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * (↑db : ℤ) + nb * (↑da : ℤ) = (↑k : ℤ) * nc
h₂ : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
⊢ ∀ (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
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * (↑db : ℤ) + nb * (↑da : ℤ) = (↑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 : α) _
⊢ Eq.{u_1 + 1} (α := α)
    ((fun (x : ℤ) ↦
        (↑x : α) *
          HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
      (na * (↑db : ℤ) + nb * (↑da : ℤ)))
    ((fun (x : ℤ) ↦
        (↑x : α) *
          HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
      ((↑k : ℤ) * nc))

Tactic:
have h₁ := congr_arg (↑· * (⅟↑da * ⅟↑db : α)) h₁
-- Module: Mathlib.Tactic.NormNum.Basic
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₂ : 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} (α := α)
    ((fun (x : ℤ) ↦
        (↑x : α) *
          HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
      (na * (↑db : ℤ) + nb * (↑da : ℤ)))
    ((fun (x : ℤ) ↦
        (↑x : α) *
          HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
      ((↑k : ℤ) * nc))
⊢ HMul.hMul (α := α) (↑na : α) (↑db : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ +
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _) =
    HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _

Tactic:
simp only [Int.cast_add, Int.cast_mul, Int.cast_natCast, ← mul_assoc,
    add_mul, mul_invOf_cancel_right] at h₁

Premises used: add_mul, Int.cast_natCast, mul_assoc, mul_invOf_cancel_right, Int.cast_add, Int.cast_mul