awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 * 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 _ 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 : α) (@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₂
Cleared hypotheses: h₁, 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 * 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 (α := α) (↑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 (α := α) (↑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₂
Cleared hypotheses: h₁, 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 * 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 α
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
⊢ 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 * (↑db : ℤ) + nb * (↑da : ℤ) = (↑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 * (↑db : ℤ) + nb * (↑da : ℤ) = (↑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 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 : α) _)
Tactic: use this
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
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 : α)
⊢ 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 : 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 : α) _
⊢ 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} (α := α)
  ((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₁
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
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 : α) (@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 : α) (↑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₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
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₁ :
  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 : α) _
⊢ 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} (α := α)
  ((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 : 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 : α) (↑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 _ 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 : α) (@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₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
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 : α) (↑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 (α := α) (↑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 (α := α) (↑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₂
Cleared hypotheses: h₁, h₂