awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
Goal:
R : Type u_2
M : Type u_3
inst : AddCommGroup M
inst_1 : Ring R
inst_2 : Module R M
l : NF R M
⊢ (-l).eval = -l.eval
have simp : Eq.{u_3 + 1} (α := M) (sum (map ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (-x.1, x.2)) l))
  (sum (map ((fun (x : M) ↦ -x) ∘ fun (x : R × M) ↦ x.1 • x.2) l))
Tactic: simp +instances only [NF.eval, List.map_map, List.sum_neg, NF.instNeg]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
Goal:
R : Type u_2
M : Type u_3
inst : AddCommGroup M
inst_1 : Ring R
inst_2 : Module R M
l : NF R M
⊢ Eq.{u_3 + 1} (α := M) (sum (map ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (-x.1, x.2)) l))
    (sum (map ((fun (x : M) ↦ -x) ∘ fun (x : R × M) ↦ x.1 • x.2) l))
have e_a : Eq (α := R × M → M) ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (-x.1, x.2))
  ((fun (x : M) ↦ -x) ∘ fun (x : R × M) ↦ x.1 • x.2)
Tactic: congr
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
Goal:
R : Type u_2
M : Type u_3
inst : AddCommGroup M
inst_1 : Ring R
inst_2 : Module R M
l : NF R M
⊢ Eq (α := R × M → M) ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (-x.1, x.2))
    ((fun (x : M) ↦ -x) ∘ fun (x : R × M) ↦ x.1 • x.2)
have e_a : ∀ (p : R × M),
  Eq.{u_3 + 1} (α := M) (((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (-x.1, x.2)) p)
    (((fun (x : M) ↦ -x) ∘ fun (x : R × M) ↦ x.1 • x.2) p)
Tactic: ext p
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : AddCommGroup M
inst_1 : Semiring S
inst_2 : Module S M
inst_3 : Ring R
inst_4 : Module R M
l : NF R M
l₀ : NF S M
hl : l.eval = l₀.eval
x : M
h : x = l₀.eval
⊢ -x = (-l).eval
have rw : -l₀.eval = (-l).eval
Tactic: rw [h, ← hl, eval_neg]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : AddCommGroup M
inst_1 : Semiring S
inst_2 : Module S M
inst_3 : Ring R
inst_4 : Module R M
l : NF R M
l₀ : NF S M
hl : l.eval = l₀.eval
x : M
h : x = l₀.eval
rw : -l₀.eval = (-l).eval
⊢ -x = (-l).eval
have rw₁ : -l.eval = (-l).eval
Tactic: rw [h, ← hl, eval_neg]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : AddCommGroup M
inst_1 : Semiring S
inst_2 : Module S M
inst_3 : Ring R
inst_4 : Module R M
l : NF R M
l₀ : NF S M
hl : l.eval = l₀.eval
x : M
h : x = l₀.eval
rw : -l₀.eval = (-l).eval
rw₁ : -l.eval = (-l).eval
⊢ -x = (-l).eval
have rw₂ : -l.eval = -l.eval
Tactic: rw [h, ← hl, eval_neg]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
Goal:
R : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
l : NF R M
x : M
h :
  x =
    sum
      (map
        (fun (x : R × M) ↦
          match (motive := R × M → M) x with
          | (r, x) => r • x)
        l)
r : R
⊢ sum
      (map
        (fun (x : R × M) ↦
          match (motive := R × M → M) x with
          | (r, x) => r • x)
        (r • l)) =
    r • x
have simp : Eq.{u_3 + 1} (α := M) (sum (map ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (r * x.1, x.2)) l))
  (sum (map ((fun (x : M) ↦ r • x) ∘ fun (x : R × M) ↦ x.1 • x.2) l))
Tactic: simp only [h, smul_sum, map_map, NF.smul_apply]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
Goal:
R : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
l : NF R M
x : M
h :
  x =
    sum
      (map
        (fun (x : R × M) ↦
          match (motive := R × M → M) x with
          | (r, x) => r • x)
        l)
r : R
⊢ Eq.{u_3 + 1} (α := M) (sum (map ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (r * x.1, x.2)) l))
    (sum (map ((fun (x : M) ↦ r • x) ∘ fun (x : R × M) ↦ x.1 • x.2) l))
have e_a : Eq (α := R × M → M) ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (r * x.1, x.2))
  ((fun (x : M) ↦ r • x) ∘ fun (x : R × M) ↦ x.1 • x.2)
Tactic: congr
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
Goal:
R : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
l : NF R M
x : M
h :
  x =
    sum
      (map
        (fun (x : R × M) ↦
          match (motive := R × M → M) x with
          | (r, x) => r • x)
        l)
r : R
⊢ Eq (α := R × M → M) ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (r * x.1, x.2))
    ((fun (x : M) ↦ r • x) ∘ fun (x : R × M) ↦ x.1 • x.2)
have e_a : ∀ (p : R × M),
  Eq.{u_3 + 1} (α := M) (((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (r * x.1, x.2)) p)
    (((fun (x : M) ↦ r • x) ∘ fun (x : R × M) ↦ x.1 • x.2) p)
Tactic: ext p
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : Semiring R₀
inst_4 : Module R₀ M
inst_5 : Semiring S
inst_6 : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ s • x = (r • l).eval
have h : l.eval = l.eval
Tactic: rw [← hs, hx, ← hl, eval_smul]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
Goal:
R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : Semiring R₁
inst_4 : Module R₁ M
inst_5 : Semiring R₂
inst_6 : Module R₂ M
l₁ l₂ : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁'.eval
hx₂ : x₂ = l₂'.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval = l₂.eval
⊢ x₁ = x₂
have rw : l₁'.eval = x₂
Tactic: rw [hx₁, hx₂, ← h₁, ← h₂, h]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
Goal:
R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : Semiring R₁
inst_4 : Module R₁ M
inst_5 : Semiring R₂
inst_6 : Module R₂ M
l₁ l₂ : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁'.eval
hx₂ : x₂ = l₂'.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval = l₂.eval
rw : l₁'.eval = x₂
⊢ x₁ = x₂
have rw₁ : l₁'.eval = l₂'.eval
Tactic: rw [hx₁, hx₂, ← h₁, ← h₂, h]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
Goal:
R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : Semiring R₁
inst_4 : Module R₁ M
inst_5 : Semiring R₂
inst_6 : Module R₂ M
l₁ l₂ : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁'.eval
hx₂ : x₂ = l₂'.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval = l₂.eval
rw : l₁'.eval = x₂
rw₁ : l₁'.eval = l₂'.eval
⊢ x₁ = x₂
have rw₂ : l₁.eval = l₂'.eval
Tactic: rw [hx₁, hx₂, ← h₁, ← h₂, h]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
Goal:
R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : Semiring R₁
inst_4 : Module R₁ M
inst_5 : Semiring R₂
inst_6 : Module R₂ M
l₁ l₂ : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁'.eval
hx₂ : x₂ = l₂'.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval = l₂.eval
rw : l₁'.eval = x₂
rw₁ : l₁'.eval = l₂'.eval
rw₂ : l₁.eval = l₂'.eval
rw₃ : l₁.eval = l₂.eval
⊢ x₁ = x₂
have rw₄ : l₂.eval = l₂.eval
Tactic: rw [hx₁, hx₂, ← h₁, ← h₂, h]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : Algebra S R
inst_3 : AddMonoid M
inst_4 : SMul S M
inst_5 : MulAction R M
inst_6 : IsScalarTower S R M
l : NF S M
⊢ (algebraMap R l).eval = l.eval
have simp : Eq.{u_3 + 1} (α := M)
  (sum (map ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : S × M) ↦ ((Algebra.algebraMap S R : (a : S) → R) x.1, x.2)) l))
  (sum (map (fun (x : S × M) ↦ x.1 • x.2) l))
Tactic: simp only [NF.eval, algebraMap, map_map]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : Algebra S R
inst_3 : AddMonoid M
inst_4 : SMul S M
inst_5 : MulAction R M
inst_6 : IsScalarTower S R M
l : NF S M
⊢ Eq.{u_3 + 1} (α := M)
    (sum (map ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : S × M) ↦ ((Algebra.algebraMap S R : (a : S) → R) x.1, x.2)) l))
    (sum (map (fun (x : S × M) ↦ x.1 • x.2) l))
have e_a : Eq (α := S × M → M)
  ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : S × M) ↦ ((Algebra.algebraMap S R : (a : S) → R) x.1, x.2))
  fun (x : S × M) ↦ x.1 • x.2
Tactic: congr
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : Algebra S R
inst_3 : AddMonoid M
inst_4 : SMul S M
inst_5 : MulAction R M
inst_6 : IsScalarTower S R M
l : NF S M
⊢ Eq (α := S × M → M)
    ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : S × M) ↦ ((Algebra.algebraMap S R : (a : S) → R) x.1, x.2))
    fun (x : S × M) ↦ x.1 • x.2
have e_a : ∀ (x : S × M),
  ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : S × M) ↦ ((Algebra.algebraMap S R : (a : S) → R) x.1, x.2)) x = x.1 • x.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : Lattice α
inst_2 : IsOrderedRing α
a : α
na : ℕ
pa : IsNat a na
⊢ IsNat |a| na
have rw : IsNat.{u_1} (α := α) (↑na : α) na
Tactic: rw [pa.out, Nat.abs_cast]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : Lattice α
inst_2 : IsOrderedRing α
a : α
na : ℕ
pa : IsNat a na
⊢ IsNat.{u_1} (α := α) (↑na : α) na
have out : Eq.{u_1 + 1} (α := α) (↑na : α) (↑na : α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : Lattice α
inst_2 : IsOrderedRing α
a : α
na : ℕ
pa : IsInt a (Int.negOfNat na)
⊢ IsNat |a| na
have rw : IsNat.{u_1} (α := α) |(↑(Int.negOfNat na) : α)| na
Tactic: rw [pa.out]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : Lattice α
inst_2 : IsOrderedRing α
a : α
na : ℕ
pa : IsInt a (Int.negOfNat na)
⊢ IsNat.{u_1} (α := α) |(↑(Int.negOfNat na) : α)| na
have out : Eq.{u_1 + 1} (α := α) |(↑(Int.negOfNat na) : α)| (↑na : α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Abs (goal)
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
num den : ℕ
ra : IsNNRat a num den
⊢ IsNNRat |a| num den
have obtain : ∀ (ha1 : Invertible (α := α) (↑den : α)),
  IsNNRat |HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)| num
    den
Tactic: obtain ⟨ha1, rfl⟩ := ra
Cleared hypotheses: a, ra
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Abs (goal)
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible (α := α) (↑den : α)
⊢ IsNNRat |HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)| num
    den
have refine : 0 ≤ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)
Tactic: refine ⟨ha1, abs_of_nonneg ?_⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Abs (goal)
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible (α := α) (↑den : α)
⊢ 0 ≤ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)
have ha : LE.le.{u_1} (α := α) 0 (↑num : α)
Tactic: apply mul_nonneg
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Abs (goal)
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible (α := α) (↑den : α)
ha : LE.le.{u_1} (α := α) 0 (↑num : α)
⊢ 0 ≤ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)
have hb : LE.le.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)
Tactic: apply mul_nonneg
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Abs (goal)
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
num den : ℕ
ra : IsRat a (Int.negOfNat num) den
⊢ IsNNRat |a| num den
have obtain : ∀ (ha1 : Invertible (α := α) (↑den : α)),
  IsNNRat
    |HMul.hMul (α := α) (↑(Int.negOfNat num) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)|
    num den
Tactic: obtain ⟨ha1, rfl⟩ := ra
Cleared hypotheses: a, ra
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Abs (goal)
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible (α := α) (↑den : α)
⊢ IsNNRat
    |HMul.hMul (α := α) (↑(Int.negOfNat num) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)|
    num den
have simp : IsNNRat |HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)| num den
Tactic: simp only [Int.cast_negOfNat, neg_mul, abs_neg]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
Goal:
α : Type u_1
inst : Semiring α
k : ℕ
b c : α
hc1 : c * ((↑k : α) * b) = 1
hc2 : (↑k : α) * b * c = 1
⊢ Invertible b
have hc1₁ : c * (↑k : α) * b = 1
Tactic: rw [← mul_assoc] at hc1
Cleared hypotheses: hc1, hc2
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Basic (hypothesis)
Goal:
α : Type u_1
inst : Semiring α
k : ℕ
b c : α
hc1 : c * (↑k : α) * b = 1
hc2 : (↑k : α) * b * c = 1
⊢ Invertible b
have hc2₁ : b * (c * (↑k : α)) = 1
Tactic: rw [Nat.cast_commute k, mul_assoc, Nat.cast_commute k] at hc2
Cleared hypotheses: hc2
-- 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 * db + nb * da = 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 * db + nb * da = 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 * db + nb * da = 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 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 : 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 : α)
⊢ 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 * 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 : 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 : α) (@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 [Nat.cast_add, Nat.cast_mul, ← 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 : 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 : α) _
⊢ 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₂