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₁_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 (α := α) (↑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₂

Premises used: mul_assoc, 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 * 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 (α := α) (↑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₂
-- 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 * 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 (α := α) (↑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₂

Premises used: 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 * 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 : α) _
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 : α) _
⊢ 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:
rw [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 * 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 (α := α) (↑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:
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, Nat.cast, Commute.invOf_left, Commute.right_comm, Nat.cast_commute, mul_invOf_cancel_right'
-- 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 * nb = (↑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 * nb = (↑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 * nb = (↑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 * 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

Tactic:
⟨this, ?_⟩

Premises used: Mathlib.Meta.NormNum.IsRat.mk
-- 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 * nb = (↑k : ℤ) * nc
h₂ : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
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 : α) _)
⊢ IsRat
    (HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) *
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
    nc dc

Tactic:
refine ⟨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 * nb = (↑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 * 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 : α) _
⊢ Eq.{u_1 + 1} (α := α) (↑(na * nb) : α) (↑((↑k : ℤ) * nc) : α)

Tactic:
have h₁ := congr_arg (Int.cast (R := α)) 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 * 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 : α) (↑nb : α) = HMul.hMul (α := α) (↑k : α) (↑nc : α)

Tactic:
simp only [Int.cast_mul, Int.cast_natCast] at h₁

Premises used: Int.cast_natCast, Int.cast_mul
-- 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 * 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 : α)
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 : α) _)
⊢ 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:
simp only [← mul_assoc, (Nat.cast_commute (α := α) da nb).invOf_left.right_comm, h₁]

Premises used: Int.cast, mul_assoc, 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₁_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 : α)
⊢ 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 : Ring α
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 (α := α) (↑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₂

Premises used: mul_assoc, Nat.cast_mul
-- 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 * 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 (α := α) (↑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₂
-- 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 * 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 (α := α) (↑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₂

Premises used: mul_invOf_cancel_right'