awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
⊢ ∀ (x y : ⨁ (i : ι), A i),
    (toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R) (x * y) =
      HMul.hMul (α := R) (β := R) ((toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R) x : R)
        ((toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R) y : R)
have rw : AddMonoidHom.compr₂ AddMonoidHom.mul (toAddMonoid (β := A) f) =
  (AddMonoidHom.comp AddMonoidHom.mul (toAddMonoid (β := A) f)).compl₂ (toAddMonoid (β := A) f)
Tactic: rw [(toAddMonoid f).map_mul_iff]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
⊢ AddMonoidHom.compr₂ AddMonoidHom.mul (toAddMonoid (β := A) f) =
    (AddMonoidHom.comp AddMonoidHom.mul (toAddMonoid (β := A) f)).compl₂ (toAddMonoid (β := A) f)
have refine : ∀ (xi : ι) (xv : A xi),
  Eq (α := (⨁ (i : ι), A i) →+ R)
    ((AddMonoidHom.comp (AddMonoidHom.compr₂ AddMonoidHom.mul (toAddMonoid (β := A) f)) (of A xi) :
          (a : A xi) → (⨁ (i : ι), A i) →+ R)
        xv :
      (⨁ (i : ι), A i) →+ R)
    ((((AddMonoidHom.comp AddMonoidHom.mul (toAddMonoid (β := A) f)).compl₂ (toAddMonoid (β := A) f)).comp (of A xi) :
          (a : A xi) → (⨁ (i : ι), A i) →+ R)
        xv :
      (⨁ (i : ι), A i) →+ R)
Tactic: refine DirectSum.addHom_ext' (fun xi ↦ AddMonoidHom.ext (fun xv ↦ ?_))
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
xi : ι
xv : A xi
⊢ Eq (α := (⨁ (i : ι), A i) →+ R)
    ((AddMonoidHom.comp (AddMonoidHom.compr₂ AddMonoidHom.mul (toAddMonoid (β := A) f)) (of A xi) :
          (a : A xi) → (⨁ (i : ι), A i) →+ R)
        xv :
      (⨁ (i : ι), A i) →+ R)
    ((((AddMonoidHom.comp AddMonoidHom.mul (toAddMonoid (β := A) f)).compl₂ (toAddMonoid (β := A) f)).comp (of A xi) :
          (a : A xi) → (⨁ (i : ι), A i) →+ R)
        xv :
      (⨁ (i : ι), A i) →+ R)
have refine : ∀ (yi : ι) (yv : A yi),
  Eq.{u_3 + 1} (α := R)
    ((AddMonoidHom.comp
            ((AddMonoidHom.comp (AddMonoidHom.compr₂ AddMonoidHom.mul (toAddMonoid (β := A) f)) (of A xi) :
                (a : A xi) → (⨁ (i : ι), A i) →+ R)
              xv)
            (of A yi) :
          (a : A yi) → R)
        yv :
      R)
    ((AddMonoidHom.comp
            ((((AddMonoidHom.comp AddMonoidHom.mul (toAddMonoid (β := A) f)).compl₂ (toAddMonoid (β := A) f)).comp
                  (of A xi) :
                (a : A xi) → (⨁ (i : ι), A i) →+ R)
              xv)
            (of A yi) :
          (a : A yi) → R)
        yv :
      R)
Tactic: refine DirectSum.addHom_ext' (fun yi ↦ AddMonoidHom.ext (fun yv ↦ ?_))
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
xi : ι
xv : A xi
yi : ι
yv : A yi
⊢ Eq.{u_3 + 1} (α := R)
    ((AddMonoidHom.comp
            ((AddMonoidHom.comp (AddMonoidHom.compr₂ AddMonoidHom.mul (toAddMonoid (β := A) f)) (of A xi) :
                (a : A xi) → (⨁ (i : ι), A i) →+ R)
              xv)
            (of A yi) :
          (a : A yi) → R)
        yv :
      R)
    ((AddMonoidHom.comp
            ((((AddMonoidHom.comp AddMonoidHom.mul (toAddMonoid (β := A) f)).compl₂ (toAddMonoid (β := A) f)).comp
                  (of A xi) :
                (a : A xi) → (⨁ (i : ι), A i) →+ R)
              xv)
            (of A yi) :
          (a : A yi) → R)
        yv :
      R)
have toAddMonoid : (toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R)
    (HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i) ((of A xi : (a : A xi) → ⨁ (i : ι), A i) xv : ⨁ (i : ι), A i)
      ((of A yi : (a : A yi) → ⨁ (i : ι), A i) yv : ⨁ (i : ι), A i)) =
  HMul.hMul (α := R) (β := R)
    ((toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R) ((of A xi : (a : A xi) → ⨁ (i : ι), A i) xv : ⨁ (i : ι), A i) :
      R)
    ((toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R) ((of A yi : (a : A yi) → ⨁ (i : ι), A i) yv : ⨁ (i : ι), A i) :
      R)
Tactic: change
        toAddMonoid f (of A xi xv * of A yi yv) =
          toAddMonoid f (of A xi xv) * toAddMonoid f (of A yi yv)
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
xi : ι
xv : A xi
yi : ι
yv : A yi
⊢ (toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R)
      (HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
        ((of A xi : (a : A xi) → ⨁ (i : ι), A i) xv : ⨁ (i : ι), A i)
        ((of A yi : (a : A yi) → ⨁ (i : ι), A i) yv : ⨁ (i : ι), A i)) =
    HMul.hMul (α := R) (β := R)
      ((toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R)
          ((of A xi : (a : A xi) → ⨁ (i : ι), A i) xv : ⨁ (i : ι), A i) :
        R)
      ((toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R)
          ((of A yi : (a : A yi) → ⨁ (i : ι), A i) yv : ⨁ (i : ι), A i) :
        R)
have simp_rw : (f (xi + yi) : (a : A (xi + yi)) → R) (GradedMonoid.GMul.mul (A := A) xv yv) =
  HMul.hMul (α := R) (β := R) ((f xi : (a : A xi) → R) xv : R) ((f yi : (a : A yi) → R) yv : R)
Tactic: simp_rw [of_mul_of, toAddMonoid_of]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
F : (⨁ (i : ι), A i) →+* R
⊢ Eq.{u_3 + 1} (α := R)
    ((AddMonoidHom.comp (↑F : (⨁ (i : ι), A i) →+ R) (of A 0) : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R)
    (1 : R)
have simp : Eq.{u_3 + 1} (α := R)
  (((↑F : (⨁ (i : ι), A i) →+ R) : (a : ⨁ (i : ι), A i) → R)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A)) : ⨁ (i : ι), A i) :
    R)
  (1 : R)
Tactic: simp only [AddMonoidHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
F : (⨁ (i : ι), A i) →+* R
⊢ Eq.{u_3 + 1} (α := R)
    (((↑F : (⨁ (i : ι), A i) →+ R) : (a : ⨁ (i : ι), A i) → R)
        ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A)) : ⨁ (i : ι), A i) :
      R)
    (1 : R)
have rw : Eq.{u_3 + 1} (α := R)
  (((↑F : (⨁ (i : ι), A i) →+ R) : (a : ⨁ (i : ι), A i) → R)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A)) : ⨁ (i : ι), A i) :
    R)
  ((F : (a : ⨁ (i : ι), A i) → R) 1 : R)
Tactic: rw [← F.map_one]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
F : (⨁ (i : ι), A i) →+* R
i j : ι
ai : A i
aj : A j
⊢ (AddMonoidHom.comp (↑F : (⨁ (i : ι), A i) →+ R) (of A (i + j)) : (a : A (i + j)) → R)
      (GradedMonoid.GMul.mul (A := A) ai aj) =
    HMul.hMul (α := R) (β := R) ((AddMonoidHom.comp (↑F : (⨁ (i : ι), A i) →+ R) (of A i) : (a : A i) → R) ai : R)
      ((AddMonoidHom.comp (↑F : (⨁ (i : ι), A i) →+ R) (of A j) : (a : A j) → R) aj : R)
have simp : (F : (a : ⨁ (i : ι), A i) → R)
    ((of A (i + j) : (a : A (i + j)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj) : ⨁ (i : ι), A i) =
  HMul.hMul (α := R) (β := R)
    ((F : (a : ⨁ (i : ι), A i) → R) ((of A i : (a : A i) → ⨁ (i : ι), A i) ai : ⨁ (i : ι), A i) : R)
    ((F : (a : ⨁ (i : ι), A i) → R) ((of A j : (a : A j) → ⨁ (i : ι), A i) aj : ⨁ (i : ι), A i) : R)
Tactic: simp only [AddMonoidHom.comp_apply, AddMonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
F : (⨁ (i : ι), A i) →+* R
i j : ι
ai : A i
aj : A j
⊢ (F : (a : ⨁ (i : ι), A i) → R)
      ((of A (i + j) : (a : A (i + j)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj) : ⨁ (i : ι), A i) =
    HMul.hMul (α := R) (β := R)
      ((F : (a : ⨁ (i : ι), A i) → R) ((of A i : (a : A i) → ⨁ (i : ι), A i) ai : ⨁ (i : ι), A i) : R)
      ((F : (a : ⨁ (i : ι), A i) → R) ((of A j : (a : A j) → ⨁ (i : ι), A i) aj : ⨁ (i : ι), A i) : R)
have rw : Eq.{u_3 + 1} (α := R)
  ((F : (a : ⨁ (i : ι), A i) → R)
      ((of A (i + j) : (a : A (i + j)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj) : ⨁ (i : ι), A i) :
    R)
  ((F : (a : ⨁ (i : ι), A i) → R)
      (HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i) ((of A i : (a : A i) → ⨁ (i : ι), A i) ai : ⨁ (i : ι), A i)
        ((of A j : (a : A j) → ⨁ (i : ι), A i) aj : ⨁ (i : ι), A i)) :
    R)
Tactic: rw [← F.map_mul (of A i ai), of_mul_of ai]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
F : (⨁ (i : ι), A i) →+* R
i j : ι
ai : A i
aj : A j
rw :
  Eq.{u_3 + 1} (α := R)
    ((F : (a : ⨁ (i : ι), A i) → R)
        ((of A (i + j) : (a : A (i + j)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj) : ⨁ (i : ι), A i) :
      R)
    ((F : (a : ⨁ (i : ι), A i) → R)
        (HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
          ((of A i : (a : A i) → ⨁ (i : ι), A i) ai : ⨁ (i : ι), A i)
          ((of A j : (a : A j) → ⨁ (i : ι), A i) aj : ⨁ (i : ι), A i)) :
      R)
⊢ (F : (a : ⨁ (i : ι), A i) → R)
      ((of A (i + j) : (a : A (i + j)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj) : ⨁ (i : ι), A i) =
    HMul.hMul (α := R) (β := R)
      ((F : (a : ⨁ (i : ι), A i) → R) ((of A i : (a : A i) → ⨁ (i : ι), A i) ai : ⨁ (i : ι), A i) : R)
      ((F : (a : ⨁ (i : ι), A i) → R) ((of A j : (a : A j) → ⨁ (i : ι), A i) aj : ⨁ (i : ι), A i) : R)
have rw₁ : Eq.{u_3 + 1} (α := R)
  ((F : (a : ⨁ (i : ι), A i) → R)
      ((of A (i + j) : (a : A (i + j)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj) : ⨁ (i : ι), A i) :
    R)
  ((F : (a : ⨁ (i : ι), A i) → R)
      ((of A (i + j) : (a : A (i + j)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj) : ⨁ (i : ι), A i) :
    R)
Tactic: rw [← F.map_mul (of A i ai), of_mul_of ai]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
F : (⨁ (i : ι), A i) →+* R
⊢ (fun
          (f :
            { f : {i : ι} → AddMonoidHom.{u_2, u_3} (A i) R //
              Eq.{u_3 + 1} (α := R) ((f : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R) ∧
                ∀ {i j : ι} (ai : A i) (aj : A j),
                  (f : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
                    HMul.hMul (α := R) (β := R) ((f : (a : A i) → R) ai : R) ((f : (a : A j) → R) aj : R) }) ↦
        (toSemiring (A := A) (fun (x : ι) ↦ (↑f : {i : ι} → A i →+ R)) ⋯ ⋯ : (⨁ (i : ι), A i) →+* R))
      ((fun (F : (⨁ (i : ι), A i) →+* R) ↦
          Subtype.mk (p := fun (f : {i : ι} → AddMonoidHom.{u_2, u_3} (A i) R) ↦
            Eq.{u_3 + 1} (α := R) ((f : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R) ∧
              ∀ {i j : ι} (ai : A i) (aj : A j),
                (f : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
                  HMul.hMul (α := R) (β := R) ((f : (a : A i) → R) ai : R) ((f : (a : A j) → R) aj : R))
            (fun {i : ι} ↦ AddMonoidHom.comp (↑F : (⨁ (i : ι), A i) →+ R) (of A i)) ⋯)
        F) =
    F
have a : Eq (α := (⨁ (i : ι), A i) →+ R)
  ((fun (f : (⨁ (i : ι), A i) →+* R) ↦ ((↑f : (⨁ (i : ι), A i) →+ R) : (⨁ (i : ι), A i) →+ R))
    ((fun
          (f :
            { f : {i : ι} → AddMonoidHom.{u_2, u_3} (A i) R //
              Eq.{u_3 + 1} (α := R) ((f : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R) ∧
                ∀ {i j : ι} (ai : A i) (aj : A j),
                  (f : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
                    HMul.hMul (α := R) (β := R) ((f : (a : A i) → R) ai : R) ((f : (a : A j) → R) aj : R) }) ↦
        (toSemiring (A := A) (fun (x : ι) ↦ (↑f : {i : ι} → A i →+ R)) sorry sorry : (⨁ (i : ι), A i) →+* R))
      ((fun (F : (⨁ (i : ι), A i) →+* R) ↦
          Subtype.mk (p := fun (f : {i : ι} → AddMonoidHom.{u_2, u_3} (A i) R) ↦
            Eq.{u_3 + 1} (α := R) ((f : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R) ∧
              ∀ {i j : ι} (ai : A i) (aj : A j),
                (f : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
                  HMul.hMul (α := R) (β := R) ((f : (a : A i) → R) ai : R) ((f : (a : A j) → R) aj : R))
            (fun {i : ι} ↦ AddMonoidHom.comp (↑F : (⨁ (i : ι), A i) →+ R) (of A i)) sorry)
        F)))
  ((fun (f : (⨁ (i : ι), A i) →+* R) ↦ ((↑f : (⨁ (i : ι), A i) →+ R) : (⨁ (i : ι), A i) →+ R)) F)
Tactic: apply RingHom.coe_addMonoidHom_injective
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
R : Type u_2
inst_1 : AddMonoid ι
inst_2 : Semiring R
i j : ι
a b : R
⊢ HMul.hMul (α := ⨁ (i : ι), R) (β := ⨁ (i : ι), R)
      (((of.{u_1, u_2} (fun (x : ι) ↦ R) i : R →+ ⨁ (i : ι), R) : (a : R) → ⨁ (i : ι), R) a : ⨁ (i : ι), R)
      (((of.{u_1, u_2} (fun (x : ι) ↦ R) j : R →+ ⨁ (i : ι), R) : (a : R) → ⨁ (i : ι), R) b : ⨁ (i : ι), R) =
    ((of.{u_1, u_2} (fun (i : ι) ↦ R) (i + j) : R →+ ⨁ (i : ι), R) : (a : R) → ⨁ (i : ι), R) (a * b)
have rw : Eq (α := ⨁ (x : ι), R)
  (((of.{u_1, u_2} (fun (x : ι) ↦ R) (i + j) : R →+ ⨁ (i : ι), R) : (a : R) → ⨁ (i : ι), R)
      (@GradedMonoid.GMul.mul _ (fun (x : ι) ↦ R) AddSemigroup.toAdd _ i j a b) :
    ⨁ (i : ι), R)
  (((of.{u_1, u_2} (fun (i : ι) ↦ R) (i + j) : R →+ ⨁ (i : ι), R) : (a : R) → ⨁ (i : ι), R) (a * b) : ⨁ (i : ι), R)
Tactic: rw [DirectSum.of_mul_of, Mul.gMul_mul]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
R : Type u_2
inst_1 : AddMonoid ι
inst_2 : Semiring R
i j : ι
a b : R
rw :
  Eq (α := ⨁ (x : ι), R)
    (((of.{u_1, u_2} (fun (x : ι) ↦ R) (i + j) : R →+ ⨁ (i : ι), R) : (a : R) → ⨁ (i : ι), R)
        (@GradedMonoid.GMul.mul _ (fun (x : ι) ↦ R) AddSemigroup.toAdd _ i j a b) :
      ⨁ (i : ι), R)
    (((of.{u_1, u_2} (fun (i : ι) ↦ R) (i + j) : R →+ ⨁ (i : ι), R) : (a : R) → ⨁ (i : ι), R) (a * b) : ⨁ (i : ι), R)
⊢ HMul.hMul (α := ⨁ (i : ι), R) (β := ⨁ (i : ι), R)
      (((of.{u_1, u_2} (fun (x : ι) ↦ R) i : R →+ ⨁ (i : ι), R) : (a : R) → ⨁ (i : ι), R) a : ⨁ (i : ι), R)
      (((of.{u_1, u_2} (fun (x : ι) ↦ R) j : R →+ ⨁ (i : ι), R) : (a : R) → ⨁ (i : ι), R) b : ⨁ (i : ι), R) =
    ((of.{u_1, u_2} (fun (i : ι) ↦ R) (i + j) : R →+ ⨁ (i : ι), R) : (a : R) → ⨁ (i : ι), R) (a * b)
have rw₁ : Eq (α := ⨁ (x : ι), R)
  (((of.{u_1, u_2} (fun (x : ι) ↦ R) (i + j) : R →+ ⨁ (i : ι), R) : (a : R) → ⨁ (i : ι), R) (a * b) : ⨁ (i : ι), R)
  (((of.{u_1, u_2} (fun (i : ι) ↦ R) (i + j) : R →+ ⨁ (i : ι), R) : (a : R) → ⨁ (i : ι), R) (a * b) : ⨁ (i : ι), R)
Tactic: rw [DirectSum.of_mul_of, Mul.gMul_mul]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : Semigroup α
b c a : α
h : b ∣ c
⊢ a * b ∣ a * c
have obtain : ∀ (d : α), a * b ∣ a * (b * d)
Tactic: obtain ⟨d, rfl⟩ := h
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : Semigroup α
b a d : α
⊢ a * b ∣ a * (b * d)
have h : a * (b * d) = a * b * d
Tactic: use d
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : Semigroup α
b a d : α
⊢ a * (b * d) = a * b * d
have h : a * (b * d) = a * (b * d)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
h : a = b
⊢ a ∣ b
have rw : b ∣ b
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : Monoid α
m n : ℕ
a : α
h : m ≤ n
⊢ a ^ n = a ^ m * a ^ (n - m)
have rw : a ^ n = a ^ (m + (n - m))
Tactic: rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : Monoid α
m n : ℕ
a : α
h : m ≤ n
rw : a ^ n = a ^ (m + (n - m))
⊢ a ^ n = a ^ m * a ^ (n - m)
have rw₁ : a ^ n = a ^ (n - m + m)
Tactic: rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : Monoid α
m n : ℕ
a : α
h : m ≤ n
rw : a ^ n = a ^ (m + (n - m))
rw₁ : a ^ n = a ^ (n - m + m)
⊢ a ^ n = a ^ m * a ^ (n - m)
have rw₂ : a ^ n = a ^ n
Tactic: rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
hab : a ∣ b
n : ℕ
h : n + 1 ≠ 0
⊢ a ∣ b ^ (n + 1)
have rw : a ∣ b * b ^ n
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : CommSemigroup α
a b : α
h : a ∣ b
c : α
⊢ a ∣ c * b
have rw : a ∣ b * c
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : CommSemigroup α
inst_1 : DecompositionMonoid α
k m n : α
⊢ k ∣ m * n ↔ ∃ (d₁ : α), ∃ (d₂ : α), d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂
have refine : (∃ (d₁ : α), ∃ (d₂ : α), d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂) → k ∣ m * n
Tactic: refine ⟨exists_dvd_and_dvd_of_dvd_mul, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
h : a ∣ b
n : ℕ
h_1 : a ^ n ∣ b ^ n
⊢ a ^ (n + 1) ∣ b ^ (n + 1)
have succ : a ^ n * a ∣ b ^ n * b
Tactic: rw [pow_succ, pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
h : a ∣ b
n : ℕ
⊢ a ^ n ∣ b ^ n
have zero : HPow.hPow (β := ℕ) a 0 ∣ HPow.hPow (β := ℕ) b 0
Tactic: induction n with
  | zero => simp
  | succ =>
    rw [pow_succ, pow_succ]
    gcongr
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
h : a ∣ b
n : ℕ
zero : HPow.hPow (β := ℕ) a 0 ∣ HPow.hPow (β := ℕ) b 0
⊢ a ^ n ∣ b ^ n
have succ : ∀ (n : ℕ), a ^ n ∣ b ^ n → a ^ (n + 1) ∣ b ^ (n + 1)
Tactic: induction n with
  | zero => simp
  | succ =>
    rw [pow_succ, pow_succ]
    gcongr
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
m n : ℕ
hab : a ∣ b
hmn : m ≤ n
⊢ a ^ m ∣ b ^ n
have trans : a ^ m ∣ a ^ n
Tactic: trans (a ^ n)
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
m n : ℕ
hab : a ∣ b
hmn : m ≤ n
trans : a ^ m ∣ a ^ n
⊢ a ^ m ∣ b ^ n
have trans₁ : a ^ n ∣ b ^ n
Tactic: trans (a ^ n)
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
m n : ℕ
hab : a ∣ b
hmn : m ≤ n
⊢ a ^ m ∣ b ^ n
have trans : a ^ m ∣ a ^ n
Tactic: trans (a ^ n) <;> [gcongr; apply_rules [pow_dvd_pow_of_dvd]]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
m n : ℕ
hab : a ∣ b
hmn : m ≤ n
trans : a ^ m ∣ a ^ n
⊢ a ^ m ∣ b ^ n
have trans₁ : a ^ n ∣ b ^ n
Tactic: trans (a ^ n) <;> [gcongr; apply_rules [pow_dvd_pow_of_dvd]]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Prod (goal)
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : Semigroup G₁
inst_1 : Semigroup G₂
x y : G₁ × G₂
⊢ x ∣ y ↔ x.1 ∣ y.1 ∧ x.2 ∣ y.2
have mk : ∀ (fst : G₁) (snd : G₂), (fst, snd) ∣ y ↔ (fst, snd).1 ∣ y.1 ∧ (fst, snd).2 ∣ y.2
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Prod (goal)
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : Semigroup G₁
inst_1 : Semigroup G₂
y : G₁ × G₂
fst : G₁
snd : G₂
⊢ (fst, snd) ∣ y ↔ (fst, snd).1 ∣ y.1 ∧ (fst, snd).2 ∣ y.2
have mk : ∀ (fst_1 : G₁) (snd_1 : G₂),
  (fst, snd) ∣ (fst_1, snd_1) ↔ (fst, snd).1 ∣ (fst_1, snd_1).1 ∧ (fst, snd).2 ∣ (fst_1, snd_1).2
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Prod (goal)
Goal:
ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
G : ι → Type u_4
inst : Semigroup G₁
inst_1 : Semigroup G₂
inst_2 : (i : ι) → Semigroup (G i)
inst_3 : DecompositionMonoid G₁
inst_4 : DecompositionMonoid G₂
a b c : G₁ × G₂
h : a ∣ b * c
⊢ ∃ (a₁ : G₁ × G₂), ∃ (a₂ : G₁ × G₂), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
have simp_rw : ∀ (h : a.1 ∣ (b * c).1 ∧ a.2 ∣ (b * c).2),
  ∃ (a₁ : G₁ × G₂), ∃ (a₂ : G₁ × G₂), (a₁.1 ∣ b.1 ∧ a₁.2 ∣ b.2) ∧ (a₂.1 ∣ c.1 ∧ a₂.2 ∣ c.2) ∧ a = a₁ * a₂
Tactic: simp_rw [prod_dvd_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Prod (goal)
Goal:
ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
G : ι → Type u_4
inst : Semigroup G₁
inst_1 : Semigroup G₂
inst_2 : (i : ι) → Semigroup (G i)
inst_3 : DecompositionMonoid G₁
inst_4 : DecompositionMonoid G₂
a b c : G₁ × G₂
h : a.1 ∣ (b * c).1 ∧ a.2 ∣ (b * c).2
⊢ ∃ (a₁ : G₁ × G₂), ∃ (a₂ : G₁ × G₂), (a₁.1 ∣ b.1 ∧ a₁.2 ∣ b.2) ∧ (a₂.1 ∣ c.1 ∧ a₂.2 ∣ c.2) ∧ a = a₁ * a₂
have obtain : ∀ (a₁ a₁' : G₁) (h₁ : a₁ ∣ b.1) (h₁' : a₁' ∣ c.1) (eq₁ : a.1 = a₁ * a₁'),
  ∃ (a₁ : G₁ × G₂), ∃ (a₂ : G₁ × G₂), (a₁.1 ∣ b.1 ∧ a₁.2 ∣ b.2) ∧ (a₂.1 ∣ c.1 ∧ a₂.2 ∣ c.2) ∧ a = a₁ * a₂
Tactic: obtain ⟨a₁, a₁', h₁, h₁', eq₁⟩ := DecompositionMonoid.primal a.1 h.1