awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.DirectSum.Ring
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 :
  { 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) }
xi : ι
xv : A xi
⊢ Eq.{u_3 + 1} (α := 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)) ⋯)
                ((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))
                  f)) :
            {i : ι} → A i →+ R) :
          (a : A xi) → R)
        xv :
      R)
    (((↑f : {i : ι} → A i →+ R) : (a : A xi) → R) xv : R)

Tactic:
exact toAddMonoid_of (fun _ => f.1) xi xv

Premises used: Subtype.val, DirectSum.toAddMonoid_of
-- Module: Mathlib.Algebra.DirectSum.Ring
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
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)) ⋯ ⋯ : (⨁ (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)))
    ((fun (f : (⨁ (i : ι), A i) →+* R) ↦ ((↑f : (⨁ (i : ι), A i) →+ R) : (⨁ (i : ι), A i) →+ R)) F)
⊢ (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

Tactic:
apply RingHom.coe_addMonoidHom_injective

Premises used: RingHom.coe_addMonoidHom_injective
-- Module: Mathlib.Algebra.DirectSum.Ring
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 (α := (⨁ (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)) ⋯ ⋯ : (⨁ (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)))
    ((fun (f : (⨁ (i : ι), A i) →+* R) ↦ ((↑f : (⨁ (i : ι), A i) →+ R) : (⨁ (i : ι), A i) →+ R)) F)

Tactic:
DirectSum.addHom_ext' (fun xi ↦ AddMonoidHom.ext (fun xv ↦ ?_))

Premises used: AddMonoidHom.ext, DirectSum.addHom_ext'
-- Module: Mathlib.Algebra.DirectSum.Ring
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
xi : ι
xv : A xi
⊢ Eq.{u_3 + 1} (α := R)
    ((AddMonoidHom.comp
            ((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)) ⋯ ⋯ : (⨁ (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)))
            (of A xi) :
          (a : A xi) → R)
        xv :
      R)
    ((AddMonoidHom.comp ((fun (f : (⨁ (i : ι), A i) →+* R) ↦ ((↑f : (⨁ (i : ι), A i) →+ R) : (⨁ (i : ι), A i) →+ R)) F)
            (of A xi) :
          (a : A xi) → R)
        xv :
      R)

Tactic:
simp only [DirectSum.toAddMonoid_of, AddMonoidHom.comp_apply, toSemiring_coe_addMonoidHom]

Premises used: DirectSum.toSemiring_coe_addMonoidHom, AddMonoidHom.comp_apply, DirectSum.toAddMonoid_of
-- Module: Mathlib.Algebra.DirectSum.Ring
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [DirectSum.of_mul_of, Mul.gMul_mul]

Premises used: DirectSum.of_mul_of, Mul.gMul_mul
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Semigroup α
a b c : α
h : a * c = b
⊢ a ∣ b

Tactic:
Exists.intro c h.symm

Premises used: Exists.intro, Eq.symm
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Semigroup α
a b : α
h : a ∣ b
⊢ ∃ (c : α), b = a * c

Tactic:
h
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Semigroup α
a b : α
⊢ a ∣ b ↔ ∃ (c : α), b = a * c

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Semigroup α
P : Prop
a b : α
H₁ : a ∣ b
H₂ : ∀ (c : α), b = a * c → P
⊢ P

Tactic:
Exists.elim H₁ H₂

Premises used: Exists.elim
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Semigroup α
a b c : α
⊢ IsTrans α Dvd.dvd

Tactic:
⟨fun _ _ _ => dvd_trans⟩

Premises used: IsTrans.mk, dvd_trans
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Semigroup α
a b : α
⊢ a ∣ a * b

Tactic:
Dvd.intro b rfl

Premises used: Dvd.intro, rfl
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Semigroup α
a b : α
h : a ∣ b
c : α
⊢ a ∣ b * c

Tactic:
h.trans (dvd_mul_right b c)

Premises used: dvd_mul_right, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Semigroup α
a b c : α
h : a * b ∣ c
⊢ a ∣ c

Tactic:
(dvd_mul_right a b).trans h

Premises used: dvd_mul_right, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Semigroup α
inst_1 : DecompositionMonoid α
b c a : α
H : a ∣ b * c
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
DecompositionMonoid.primal a H

Premises used: DecompositionMonoid.primal
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Semigroup α
b c a : α
h : b ∣ c
obtain : ∀ (d : α), a * b ∣ a * (b * d)
⊢ a * b ∣ a * c

Tactic:
obtain ⟨d, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Semigroup α
b a d : α
h : a * (b * d) = a * b * d
⊢ a * b ∣ a * (b * d)

Tactic:
use d
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Semigroup α
b a d : α
h h₁ : a * (b * d) = a * (b * d)
⊢ a * (b * d) = a * b * d

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Semigroup α
a b c : α
h : IsLeftRegular a
⊢ a * b ∣ a * c ↔ b ∣ c

Tactic:
⟨fun dvd ↦ have ⟨d, eq⟩ := dvd; ⟨d, h (eq.trans <| mul_assoc ..)⟩, mul_dvd_mul_left a⟩

Premises used: Dvd.dvd, mul_assoc, _private.0.IsLeftRegular.dvd_cancel_left.match_1, mul_dvd_mul_left, Iff.intro, Exists.intro, Eq.trans
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Monoid α
a : α
⊢ a ∣ a

Tactic:
Dvd.intro 1 (mul_one a)

Premises used: Dvd.intro, mul_one, OfNat.ofNat
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Monoid α
⊢ ∀ {a : α}, a ∣ a

Tactic:
fun {a} => dvd_refl a

Premises used: dvd_refl
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Monoid α
a b c : α
m n : ℕ
⊢ Std.Refl fun (x1 x2 : α) ↦ x1 ∣ x2

Tactic:
⟨dvd_refl⟩

Premises used: Std.Refl.mk, dvd_refl
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Monoid α
a : α
⊢ 1 ∣ a

Tactic:
Dvd.intro a (one_mul a)

Premises used: Dvd.intro, one_mul
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Monoid α
a b : α
h : a = b
rw rw₁ : b ∣ b
⊢ a ∣ b

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Divisibility.Basic
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)
rw₂ rw₃ : a ^ n = a ^ n
⊢ a ^ n = a ^ m * a ^ (n - m)

Tactic:
rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]

Premises used: pow_add, Nat.sub_add_cancel, Nat.add_comm
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Monoid α
a b : α
hab : a ∣ b
n : ℕ
h : n + 1 ≠ 0
rw : a ∣ b * b ^ n
⊢ a ∣ b ^ (n + 1)

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Monoid α
a b : α
hab : a ∣ b
n : ℕ
h : n + 1 ≠ 0
⊢ a ∣ b * b ^ n

Tactic:
hab.mul_right _

Premises used: Dvd.dvd.mul_right
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Monoid α
a b : α
hab : a ∣ b
n : ℕ
h : n + 1 ≠ 0
⊢ a ∣ b * b ^ n

Tactic:
exact hab.mul_right _

Premises used: Dvd.dvd.mul_right
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : Monoid α
a : α
n : ℕ
hn : n ≠ 0
⊢ a ∣ a ^ n

Tactic:
dvd_rfl.pow hn

Premises used: Dvd.dvd.pow, dvd_rfl
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommSemigroup α
a b c : α
h : c * a = b
⊢ a * c = b

Tactic:
rw [mul_comm] at h

Premises used: mul_comm
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommSemigroup α
a b c : α
h : a * c = b
⊢ a * c = b

Tactic:
apply h
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommSemigroup α
a b : α
h : a ∣ b
⊢ ∃ (c : α), b = c * a

Tactic:
Dvd.elim h fun c => fun H1 : b = a * c => Exists.intro c (Eq.trans H1 (mul_comm a c))

Premises used: Dvd.elim, Exists.intro, mul_comm, Eq.trans
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommSemigroup α
a c : α
⊢ a ∣ c * a

Tactic:
⟨c, mul_comm _ _⟩

Premises used: Exists.intro, mul_comm
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommSemigroup α
a c : α
⊢ a ∣ c * a

Tactic:
exact ⟨c, mul_comm _ _⟩
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommSemigroup α
a b : α
P : Prop
h₁ : a ∣ b
h₂ : ∀ (c : α), b = c * a → P
⊢ P

Tactic:
Exists.elim (exists_eq_mul_left_of_dvd h₁) fun c => fun h₃ : b = c * a => h₂ c h₃

Premises used: exists_eq_mul_left_of_dvd, Exists.elim
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommSemigroup α
a b : α
⊢ a ∣ b * a

Tactic:
Dvd.intro b (mul_comm a b)

Premises used: Dvd.intro, mul_comm
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommSemigroup α
a b : α
h : a ∣ b
c : α
rw : a ∣ b * c
⊢ a ∣ c * b

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommSemigroup α
a b : α
h : a ∣ b
c : α
⊢ a ∣ b * c

Tactic:
h.mul_right _

Premises used: Dvd.dvd.mul_right
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommSemigroup α
a b : α
h : a ∣ b
c : α
⊢ a ∣ b * c

Tactic:
exact h.mul_right _

Premises used: Dvd.dvd.mul_right
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommSemigroup α
a c e f : α
⊢ a * e * (c * f) = a * c * (e * f)

Tactic:
simp
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommSemigroup α
a b c : α
h : a * b ∣ c
d : α
ceq : c = a * b * d
⊢ b * (a * d) = c

Tactic:
simp [ceq]
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommSemigroup α
inst_1 : DecompositionMonoid α
k m n : α
⊢ k ∣ m * n ↔ ∃ (d₁ : α), ∃ (d₂ : α), d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂

Tactic:
⟨exists_dvd_and_dvd_of_dvd_mul, ?_⟩

Premises used: exists_dvd_and_dvd_of_dvd_mul, Iff.intro
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommSemigroup α
inst_1 : DecompositionMonoid α
k m n : α
refine : (∃ (d₁ : α), ∃ (d₂ : α), d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂) → k ∣ m * n
⊢ k ∣ m * n ↔ ∃ (d₁ : α), ∃ (d₂ : α), d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂

Tactic:
refine ⟨exists_dvd_and_dvd_of_dvd_mul, ?_⟩
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommSemigroup α
inst_1 : DecompositionMonoid α
m n d₁ d₂ : α
hy : d₁ ∣ m
hz : d₂ ∣ n
⊢ d₁ * d₂ ∣ m * n

Tactic:
gcongr
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
h : a ∣ b
c : α
⊢ a * c ∣ b * c

Tactic:
gcongr
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
h : a ∣ b
⊢ HPow.hPow (β := ℕ) a 0 ∣ HPow.hPow (β := ℕ) b 0

Tactic:
simp
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
h : a ∣ b
n : ℕ
h_1 : a ^ n ∣ b ^ n
succ : a ^ n * a ∣ b ^ n * b
⊢ a ^ (n + 1) ∣ b ^ (n + 1)

Tactic:
rw [pow_succ, pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
h : a ∣ b
n : ℕ
h_1 : a ^ n ∣ b ^ n
⊢ a ^ n * a ∣ b ^ n * b

Tactic:
gcongr
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
h : a ∣ b
n : ℕ
zero : HPow.hPow (β := ℕ) a 0 ∣ HPow.hPow (β := ℕ) b 0
succ : ∀ (n : ℕ), a ^ n ∣ b ^ n → a ^ (n + 1) ∣ b ^ (n + 1)
⊢ a ^ n ∣ b ^ n

Tactic:
induction n with
  | zero => simp
  | succ =>
    rw [pow_succ, pow_succ]
    gcongr

Premises used: pow_succ
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
m n : ℕ
hab : a ∣ b
hmn : m ≤ n
trans : a ^ m ∣ a ^ n
trans₁ : a ^ n ∣ b ^ n
⊢ a ^ m ∣ b ^ n

Tactic:
trans (a ^ n)

Premises used: HPow.hPow
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
m n : ℕ
hab : a ∣ b
hmn : m ≤ n
⊢ a ^ m ∣ a ^ n

Tactic:
gcongr
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
m n : ℕ
hab : a ∣ b
hmn : m ≤ n
⊢ a ^ n ∣ b ^ n

Tactic:
apply_rules [pow_dvd_pow_of_dvd]

Premises used: pow_dvd_pow_of_dvd
-- Module: Mathlib.Algebra.Divisibility.Basic
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
m n : ℕ
hab : a ∣ b
hmn : m ≤ n
trans : a ^ m ∣ a ^ n
trans₁ : a ^ n ∣ b ^ n
trans₂ : a ^ m ∣ a ^ n
trans₃ : a ^ n ∣ b ^ n
⊢ a ^ m ∣ b ^ n

Tactic:
trans (a ^ n) <;> [gcongr; apply_rules [pow_dvd_pow_of_dvd]]

Premises used: pow_dvd_pow_of_dvd, HPow.hPow
-- Module: Mathlib.Algebra.Divisibility.Hom
Goal:
M : Type u_1
N : Type u_2
inst : Semigroup M
inst_1 : Semigroup N
f : M →ₙ* N
a b : M
⊢ a ∣ b → Dvd.dvd.{u_2} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)

Tactic:
_root_.map_dvd f

Premises used: map_dvd
-- Module: Mathlib.Algebra.Divisibility.Hom
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
f : M →* N
a b : M
⊢ a ∣ b → Dvd.dvd.{u_2} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)

Tactic:
_root_.map_dvd f

Premises used: map_dvd
-- Module: Mathlib.Algebra.Divisibility.Prod
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : Semigroup G₁
inst_1 : Semigroup G₂
x y : G₁ × G₂
mk : ∀ (fst : G₁) (snd : G₂), (fst, snd) ∣ y ↔ (fst, snd).1 ∣ y.1 ∧ (fst, snd).2 ∣ y.2
⊢ x ∣ y ↔ x.1 ∣ y.1 ∧ x.2 ∣ y.2

Tactic:
cases x
-- Module: Mathlib.Algebra.Divisibility.Prod
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : Semigroup G₁
inst_1 : Semigroup G₂
y : G₁ × G₂
fst : G₁
snd : G₂
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
⊢ (fst, snd) ∣ y ↔ (fst, snd).1 ∣ y.1 ∧ (fst, snd).2 ∣ y.2

Tactic:
cases y
-- Module: Mathlib.Algebra.Divisibility.Prod
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : Semigroup G₁
inst_1 : Semigroup G₂
fst : G₁
snd : G₂
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:
simp only [dvd_def, Prod.exists, Prod.mk_mul_mk, Prod.mk.injEq,
    exists_and_left, exists_and_right]

Premises used: dvd_def, exists_and_left, exists_and_right, Prod.mk.injEq, Prod.mk_mul_mk, Prod.exists
-- Module: Mathlib.Algebra.Divisibility.Prod
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : Semigroup G₁
inst_1 : Semigroup G₂
x₁ y₁ : G₁
x₂ y₂ : G₂
⊢ (x₁, x₂) ∣ (y₁, y₂) ↔ x₁ ∣ y₁ ∧ x₂ ∣ y₂

Tactic:
prod_dvd_iff

Premises used: prod_dvd_iff
-- Module: Mathlib.Algebra.Divisibility.Prod
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
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₂
⊢ ∃ (a₁ : G₁ × G₂), ∃ (a₂ : G₁ × G₂), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
simp_rw [prod_dvd_iff] at h ⊢

Premises used: prod_dvd_iff
-- Module: Mathlib.Algebra.Divisibility.Prod
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
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₂
⊢ ∃ (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

Premises used: DecompositionMonoid.primal, Prod.fst, And.left
-- Module: Mathlib.Algebra.Divisibility.Prod
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₁ a₁' : G₁
h₁ : a₁ ∣ b.1
h₁' : a₁' ∣ c.1
eq₁ : a.1 = a₁ * a₁'
obtain :
  ∀ (a₂ a₂' : G₂) (h₂ : a₂ ∣ b.2) (h₂' : a₂' ∣ c.2) (eq₂ : a.2 = 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₂
⊢ ∃ (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.2 h.2

Premises used: DecompositionMonoid.primal, And.right, Prod.snd