awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x y : FreeMonoid α
h : rels x y
⊢ Eq (α := PresentedMonoid rels) ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) x : PresentedMonoid rels)
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) y : PresentedMonoid rels)

Tactic:
mk_eq_mk_iff.2 (.of _ _ h)

Premises used: Iff.mpr, PresentedMonoid.mk_eq_mk_iff, ConGen.Rel.of
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
rw : ∀ (x : PresentedMonoid rels), Membership.mem (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels))) x
⊢ Eq (α := Submonoid (PresentedMonoid rels)) (closure (range (of rels))) ⊤

Tactic:
rw [Submonoid.eq_top_iff']

Premises used: Submonoid.eq_top_iff'
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x : PresentedMonoid rels
h :
  ∀ (a : FreeMonoid α),
    Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
      ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) a : PresentedMonoid rels)
⊢ Membership.mem (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels))) x

Tactic:
induction x with | _ a
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
⊢ Membership.mem (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) 1)

Tactic:
Submonoid.one_mem _

Premises used: Set.Mem, Submonoid.one_mem
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
⊢ Membership.mem (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) 1)

Tactic:
exact Submonoid.one_mem _

Premises used: Submonoid.one_mem
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x : α
⊢ Membership.mem (α := PresentedMonoid rels) (range (of rels))
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) (FreeMonoid.of x) : PresentedMonoid rels)

Tactic:
simp [range, of]

Premises used: PresentedMonoid.of, Set.range
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x : α
⊢ Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) (FreeMonoid.of x) : PresentedMonoid rels)

Tactic:
exact subset_closure <| by simp [range, of]

Premises used: Submonoid.subset_closure
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x y : FreeMonoid α
hx :
  Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) x : PresentedMonoid rels)
hy :
  Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) y : PresentedMonoid rels)
⊢ Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) (x * y) : PresentedMonoid rels)

Tactic:
Submonoid.mul_mem _ hx hy

Premises used: Submonoid.mul_mem, Set.Mem, Quotient.map₂
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x y : FreeMonoid α
hx :
  Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) x : PresentedMonoid rels)
hy :
  Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) y : PresentedMonoid rels)
⊢ Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) (x * y) : PresentedMonoid rels)

Tactic:
exact Submonoid.mul_mem _ hx hy

Premises used: Submonoid.mul_mem
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
a : FreeMonoid α
h :
  Membership.mem (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) 1)
h₁ :
  ∀ (x : α),
    Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
      ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) (FreeMonoid.of x) : PresentedMonoid rels)
h₂ :
  ∀ (x y : FreeMonoid α)
    (hx :
      Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
        ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) x : PresentedMonoid rels))
    (hy :
      Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
        ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) y : PresentedMonoid rels)),
    Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
      ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) (x * y) : PresentedMonoid rels)
⊢ Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) a : PresentedMonoid rels)

Tactic:
induction a with
  | one => exact Submonoid.one_mem _
  | of x => exact subset_closure <| by simp [range, of]
  | mul x y hx hy => exact Submonoid.mul_mem _ hx hy

Premises used: Submonoid.mul, PresentedMonoid.of, Submonoid.one_mem, Submonoid.one, Submonoid.subset_closure
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
⊢ Function.Surjective (α := FreeMonoid α) (β := PresentedMonoid rels)
    (⇑(mk rels) : (a : FreeMonoid α) → PresentedMonoid rels)

Tactic:
fun x ↦ PresentedMonoid.inductionOn x fun a ↦ .intro a rfl

Premises used: PresentedMonoid.inductionOn, Function.Surjective
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α : Type u_3
M : Type u_4
inst : Monoid M
f : α → M
rels : FreeMonoid α → FreeMonoid α → Prop
h :
  ∀ (a b : FreeMonoid α),
    rels a b →
      Eq.{u_4 + 1} (α := M)
        ((((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_3, u_4} (FreeMonoid α) M) :
              (a : FreeMonoid α) → M)
            a :
          M)
        ((((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_3, u_4} (FreeMonoid α) M) :
              (a : FreeMonoid α) → M)
            b :
          M)
g : MonoidHom.{u_3, u_4} (Con.Quotient (conGen rels)) M
hg : ∀ (a : α), (g : (a : (conGen rels).Quotient) → M) (of rels a) = f a
⊢ g = lift f (rels := rels) h

Tactic:
Con.lift_unique (Con.conGen_le h) g (FreeMonoid.hom_eq hg)

Premises used: PresentedMonoid.lift, Con.conGen_le, Con.lift_unique, FreeMonoid.hom_eq
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α : Type u_3
M : Type u_4
inst : Monoid M
f : α → M
rels : FreeMonoid α → FreeMonoid α → Prop
h :
  ∀ (a b : FreeMonoid α),
    rels a b →
      Eq.{u_4 + 1} (α := M)
        ((((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_3, u_4} (FreeMonoid α) M) :
              (a : FreeMonoid α) → M)
            a :
          M)
        ((((FreeMonoid.lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_3, u_4} (FreeMonoid α) M) :
              (a : FreeMonoid α) → M)
            b :
          M)
x : α
⊢ (lift f (rels := rels) h : (a : PresentedMonoid rels) → M) (of rels x) = f x

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, Con.liftOn, rfl
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α : Type u_2
M : Type u_3
inst : Monoid M
rels : FreeMonoid α → FreeMonoid α → Prop
φ ψ : MonoidHom.{u_2, u_3} (PresentedMonoid rels) M
hx :
  ∀ (x : α),
    Eq.{u_3 + 1} (α := M) ((φ : (a : PresentedMonoid rels) → M) (of rels x) : M)
      ((ψ : (a : PresentedMonoid rels) → M) (of rels x) : M)
apply :
  EqOn.{u_2, u_3} (β := M) (⇑φ : (a : PresentedMonoid rels) → M) (⇑ψ : (a : PresentedMonoid rels) → M) (range (of rels))
⊢ φ = ψ

Tactic:
apply MonoidHom.eq_of_eqOn_denseM (closure_range_of _)

Premises used: PresentedMonoid.closure_range_of, MonoidHom.eq_of_eqOn_denseM
-- Module: Mathlib.Algebra.PresentedMonoid.Basic
Goal:
α : Type u_2
M : Type u_3
inst : Monoid M
rels : FreeMonoid α → FreeMonoid α → Prop
φ ψ : MonoidHom.{u_2, u_3} (PresentedMonoid rels) M
hx :
  ∀ (x : α),
    Eq.{u_3 + 1} (α := M) ((φ : (a : PresentedMonoid rels) → M) (of rels x) : M)
      ((ψ : (a : PresentedMonoid rels) → M) (of rels x) : M)
⊢ EqOn.{u_2, u_3} (β := M) (⇑φ : (a : PresentedMonoid rels) → M) (⇑ψ : (a : PresentedMonoid rels) → M) (range (of rels))

Tactic:
grind [Set.eqOn_range]

Premises used: Set.eqOn_range
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
⊢ p ≠ 0

Tactic:
hp.1

Premises used: And.left
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
⊢ ¬IsUnit p

Tactic:
hp.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
⊢ ¬p ∣ 1

Tactic:
mt (isUnit_of_dvd_one ·) hp.not_unit

Premises used: mt, Prime.not_unit, isUnit_of_dvd_one
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
⊢ p ≠ 1

Tactic:
fun h => hp.2.1 (h.symm ▸ isUnit_one)

Premises used: Eq.rec, And.right, isUnit_one, And.left, Eq.symm, Not
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a b : M
h : p ∣ a * b
⊢ p ∣ a ∨ p ∣ b

Tactic:
hp.2.2 a b h

Premises used: And.right
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a b : M
⊢ p ∣ a * b ↔ p ∣ a ∨ p ∣ b

Tactic:
⟨hp.dvd_or_dvd, (Or.elim · (dvd_mul_of_dvd_left · _) (dvd_mul_of_dvd_right · _))⟩

Premises used: dvd_mul_of_dvd_left, dvd_mul_of_dvd_right, Prime.dvd_or_dvd, Iff.intro, Or.elim
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
⊢ IsPrimal p

Tactic:
fun _a _b dvd ↦ (hp.dvd_or_dvd dvd).elim
  (fun h ↦ ⟨p, 1, h, one_dvd _, (mul_one p).symm⟩) fun h ↦ ⟨1, p, one_dvd _, h, (one_mul p).symm⟩

Premises used: IsPrimal, Prime.dvd_or_dvd, one_dvd, And.intro, Exists.intro, mul_one, Or.elim, OfNat.ofNat, Eq.symm, one_mul
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a b : M
ha : ¬p ∣ a
hb : ¬p ∣ b
⊢ ¬p ∣ a * b

Tactic:
hp.dvd_mul.not.mpr <| not_or.mpr ⟨ha, hb⟩

Premises used: Iff.mpr, Prime.dvd_mul, Iff.not, not_or, And.intro
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ HPow.hPow (β := ℕ) a 0
⊢ p ∣ 1

Tactic:
rw [pow_zero] at h

Premises used: pow_zero
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ 1
⊢ IsUnit p

Tactic:
have := isUnit_of_dvd_one h
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ 1
this : IsUnit p
⊢ ¬IsUnit p

Tactic:
have := not_unit hp
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ 1
this_1 : IsUnit p
this : ¬IsUnit p
⊢ p ∣ a

Tactic:
contradiction
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : ∀ (h : p ∣ a ^ n), p ∣ a
h : p ∣ a ^ (n + 1)
⊢ p ∣ a * a ^ n

Tactic:
rw [pow_succ'] at h

Premises used: pow_succ'
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : ∀ (h : p ∣ a ^ n), p ∣ a
h : p ∣ a * a ^ n
succ : ∀ (dvd_a : p ∣ a), p ∣ a
succ₁ : ∀ (dvd_pow : p ∣ a ^ n), p ∣ a
⊢ p ∣ a

Tactic:
rcases dvd_or_dvd hp h with dvd_a | dvd_pow

Premises used: Prime.dvd_or_dvd, dvd_pow
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : ∀ (h : p ∣ a ^ n), p ∣ a
h : p ∣ a * a ^ n
dvd_a : p ∣ a
⊢ p ∣ a

Tactic:
assumption
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : ∀ (h : p ∣ a ^ n), p ∣ a
h : p ∣ a * a ^ n
dvd_pow : p ∣ a ^ n
⊢ p ∣ a

Tactic:
ih dvd_pow
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : ∀ (h : p ∣ a ^ n), p ∣ a
h : p ∣ a * a ^ n
dvd_pow : p ∣ a ^ n
⊢ p ∣ a

Tactic:
exact ih dvd_pow
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
h : p ∣ a ^ n
zero : ∀ (h : p ∣ HPow.hPow (β := ℕ) a 0), p ∣ a
succ : ∀ (n : ℕ) (ih : ∀ (h : p ∣ a ^ n), p ∣ a) (h : p ∣ a ^ (n + 1)), p ∣ a
⊢ p ∣ a

Tactic:
induction n with
  | zero =>
    rw [pow_zero] at h
    have := isUnit_of_dvd_one h
    have := not_unit hp
    contradiction
  | succ n ih =>
    rw [pow_succ'] at h
    rcases dvd_or_dvd hp h with dvd_a | dvd_pow
    · assumption
    · exact ih dvd_pow

Premises used: Prime.dvd_or_dvd, dvd_pow, pow_zero, pow_succ'
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
hn : n ≠ 0
⊢ p ∣ a ^ n ↔ p ∣ a

Tactic:
⟨hp.dvd_of_dvd_pow, (dvd_pow · hn)⟩

Premises used: dvd_pow, Iff.intro, Prime.dvd_of_dvd_pow
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
⊢ ¬Prime.{u_1} (M := M) 0

Tactic:
fun h => h.ne_zero rfl

Premises used: Prime.ne_zero, Not, rfl
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
⊢ ¬Prime.{u_1} (M := M) 1

Tactic:
fun h => h.not_unit isUnit_one

Premises used: Prime.not_unit, isUnit_one, Not
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoid M
p u : M
hp : Irreducible p
hu : IsUnit u
⊢ ¬p ∣ u

Tactic:
mt (isUnit_of_dvd_unit · hu) hp.not_isUnit

Premises used: isUnit_of_dvd_unit, Irreducible.not_isUnit, mt
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoid M
p : M
hp : Irreducible p
⊢ ¬p ∣ 1

Tactic:
hp.not_dvd_isUnit isUnit_one

Premises used: Irreducible.not_dvd_isUnit, isUnit_one
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoid M
p : M
u : Mˣ
hp : Irreducible p
⊢ ¬p ∣ (↑u : M)

Tactic:
hp.not_dvd_isUnit u.isUnit

Premises used: Irreducible.not_dvd_isUnit, Units.isUnit
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : Monoid M
p : M
hp : Irreducible p
q' : M
hq : Irreducible (p * q')
rw rw₁ : p ∣ p
⊢ p * q' ∣ p

Tactic:
rw [IsUnit.mul_right_dvd (Or.resolve_left (of_irreducible_mul hq) hp.not_isUnit)]

Premises used: Irreducible.not_isUnit, Or.resolve_left, of_irreducible_mul, IsUnit.mul_right_dvd
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : Monoid M
p q : M
hp : Irreducible p
hq : Irreducible q
⊢ p ∣ q ↔ q ∣ p

Tactic:
⟨hp.dvd_symm hq, hq.dvd_symm hp⟩

Premises used: Irreducible.dvd_symm, Iff.intro
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a_1 : M
irr : Irreducible a_1
primal : IsPrimal a_1
a b : M
dvd : a_1 ∣ a * b
obtain :
  ∀ (d₁ d₂ : M) (h₁ : d₁ ∣ a) (h₂ : d₂ ∣ b) (irr : Irreducible (d₁ * d₂)) (primal : IsPrimal (d₁ * d₂))
    (dvd : d₁ * d₂ ∣ a * b), d₁ * d₂ ∣ a ∨ d₁ * d₂ ∣ b
⊢ a_1 ∣ a ∨ a_1 ∣ b

Tactic:
obtain ⟨d₁, d₂, h₁, h₂, rfl⟩ := primal dvd

Premises used: rfl
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a b d₁ d₂ : M
h₁ : d₁ ∣ a
h₂ : d₂ ∣ b
irr : Irreducible (d₁ * d₂)
primal : IsPrimal (d₁ * d₂)
dvd : d₁ * d₂ ∣ a * b
⊢ d₁ * d₂ ∣ a ∨ d₁ * d₂ ∣ b

Tactic:
(of_irreducible_mul irr).symm.imp (·.mul_right_dvd.mpr h₁) (·.mul_left_dvd.mpr h₂)

Premises used: Or.symm, of_irreducible_mul, Or.imp
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a b d₁ d₂ : M
h₁ : d₁ ∣ a
h₂ : d₂ ∣ b
irr : Irreducible (d₁ * d₂)
primal : IsPrimal (d₁ * d₂)
dvd : d₁ * d₂ ∣ a * b
⊢ d₁ * d₂ ∣ a ∨ d₁ * d₂ ∣ b

Tactic:
exact (of_irreducible_mul irr).symm.imp (·.mul_right_dvd.mpr h₁) (·.mul_left_dvd.mpr h₂)

Premises used: Or.symm, of_irreducible_mul, Or.imp
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : DecompositionMonoid M
a : M
irr : Irreducible a
⊢ Prime a

Tactic:
irr.prime_of_isPrimal (DecompositionMonoid.primal a)

Premises used: Irreducible.prime_of_isPrimal, DecompositionMonoid.primal
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
a b : M
hp : Prime (a * b)
⊢ IsUnit a ∨ IsUnit b

Tactic:
(hp.dvd_or_dvd dvd_rfl).symm.imp
      (isUnit_of_dvd_one <| (mul_dvd_mul_iff_right <| right_ne_zero_of_mul hp.ne_zero).mp <|
        dvd_mul_of_dvd_right · _)
      (isUnit_of_dvd_one <| (mul_dvd_mul_iff_left <| left_ne_zero_of_mul hp.ne_zero).mp <|
        dvd_mul_of_dvd_left · _)

Premises used: dvd_mul_of_dvd_left, dvd_mul_of_dvd_right, Prime.dvd_or_dvd, mul_dvd_mul_iff_right, right_ne_zero_of_mul, mul_dvd_mul_iff_left, Or.symm, isUnit_of_dvd_one, left_ne_zero_of_mul, Prime.ne_zero, Iff.mp, dvd_rfl, Or.imp, OfNat.ofNat
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
a b : M
hp : Prime (a * b)
⊢ IsUnit a ∨ IsUnit b

Tactic:
exact (hp.dvd_or_dvd dvd_rfl).symm.imp
      (isUnit_of_dvd_one <| (mul_dvd_mul_iff_right <| right_ne_zero_of_mul hp.ne_zero).mp <|
        dvd_mul_of_dvd_right · _)
      (isUnit_of_dvd_one <| (mul_dvd_mul_iff_left <| left_ne_zero_of_mul hp.ne_zero).mp <|
        dvd_mul_of_dvd_left · _)

Premises used: dvd_mul_of_dvd_left, dvd_mul_of_dvd_right, Prime.dvd_or_dvd, mul_dvd_mul_iff_right, right_ne_zero_of_mul, mul_dvd_mul_iff_left, Or.symm, isUnit_of_dvd_one, left_ne_zero_of_mul, Prime.ne_zero, Iff.mp, dvd_rfl, Or.imp, OfNat.ofNat
-- Module: Mathlib.Algebra.Prime.Defs
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : DecompositionMonoid M
a : M
⊢ Irreducible a ↔ Prime a

Tactic:
⟨Irreducible.prime, Prime.irreducible⟩

Premises used: Prime.irreducible, Iff.intro, Irreducible.prime
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoidWithZero M
inst_1 : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidWithZeroHomClass F M N
inst_4 : FunLike G N M
inst_5 : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), (g : (a : N) → M) ((f : (a : M) → N) a : N) = a
hp : Prime.{u_2} (M := N) ((f : (a : M) → N) p : N)
h : p = 0
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) p : N) (0 : N)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoidWithZero M
inst_1 : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidWithZeroHomClass F M N
inst_4 : FunLike G N M
inst_5 : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), (g : (a : N) → M) ((f : (a : M) → N) a : N) = a
hp : Prime.{u_2} (M := N) ((f : (a : M) → N) p : N)
a b : M
h : p ∣ a * b
⊢ Dvd.dvd.{u_2} (α := N) ((f : (a : M) → N) p : N) ((f : (a : M) → N) (a * b) : N)

Tactic:
map_dvd f h

Premises used: map_dvd
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoidWithZero M
inst_1 : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidWithZeroHomClass F M N
inst_4 : FunLike G N M
inst_5 : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), (g : (a : N) → M) ((f : (a : M) → N) a : N) = a
hp : Prime.{u_2} (M := N) ((f : (a : M) → N) p : N)
a b : M
h : p ∣ a * b
h₁ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) = (f : (a : M) → N) (a * b)
⊢ (f : (a : M) → N) p ∣ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)

Tactic:
convert! map_dvd f h

Premises used: map_dvd
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoidWithZero M
inst_1 : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidWithZeroHomClass F M N
inst_4 : FunLike G N M
inst_5 : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), (g : (a : N) → M) ((f : (a : M) → N) a : N) = a
hp : Prime.{u_2} (M := N) ((f : (a : M) → N) p : N)
a b : M
h : p ∣ a * b
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) = (f : (a : M) → N) (a * b)

Tactic:
simp
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoidWithZero M
inst_1 : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidWithZeroHomClass F M N
inst_4 : FunLike G N M
inst_5 : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), (g : (a : N) → M) ((f : (a : M) → N) a : N) = a
hp : Prime.{u_2} (M := N) ((f : (a : M) → N) p : N)
a b : M
h : p ∣ a * b
refine_1 : Dvd.dvd.{u_2} (α := N) ((f : (a : M) → N) p : N) ((f : (a : M) → N) a : N) → p ∣ a
refine_2 : Dvd.dvd.{u_2} (α := N) ((f : (a : M) → N) p : N) ((f : (a : M) → N) b : N) → p ∣ b
⊢ p ∣ a ∨ p ∣ b

Tactic:
refine
        (hp.2.2 (f a) (f b) <| by
              convert! map_dvd f h
              simp).imp
          ?_ ?_

Premises used: And.right, Or.imp, DFunLike.coe
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoidWithZero M
inst_1 : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidWithZeroHomClass F M N
inst_4 : FunLike G N M
inst_5 : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), (g : (a : N) → M) ((f : (a : M) → N) a : N) = a
hp : Prime.{u_2} (M := N) ((f : (a : M) → N) p : N)
a b : M
h_1 : p ∣ a * b
h : Dvd.dvd.{u_2} (α := N) ((f : (a : M) → N) p : N) ((f : (a : M) → N) a : N)
⊢ Dvd.dvd.{u_1} (α := M) ((g : (a : N) → M) ((f : (a : M) → N) p : N) : M)
    ((g : (a : N) → M) ((f : (a : M) → N) a : N) : M)

Tactic:
map_dvd g h

Premises used: map_dvd
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoidWithZero M
inst_1 : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidWithZeroHomClass F M N
inst_4 : FunLike G N M
inst_5 : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), (g : (a : N) → M) ((f : (a : M) → N) a : N) = a
hp : Prime.{u_2} (M := N) ((f : (a : M) → N) p : N)
a b : M
h_1 : p ∣ a * b
h : Dvd.dvd.{u_2} (α := N) ((f : (a : M) → N) p : N) ((f : (a : M) → N) a : N)
h₁ : (g : (a : N) → M) ((f : (a : M) → N) p : N) = p
h₂ : (g : (a : N) → M) ((f : (a : M) → N) a : N) = a
⊢ p ∣ a

Tactic:
convert! ← map_dvd g h

Premises used: map_dvd
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoidWithZero M
inst_1 : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidWithZeroHomClass F M N
inst_4 : FunLike G N M
inst_5 : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), (g : (a : N) → M) ((f : (a : M) → N) a : N) = a
hp : Prime.{u_2} (M := N) ((f : (a : M) → N) p : N)
a b : M
h_1 : p ∣ a * b
h : Dvd.dvd.{u_2} (α := N) ((f : (a : M) → N) p : N) ((f : (a : M) → N) a : N)
⊢ (g : (a : N) → M) ((f : (a : M) → N) p : N) = p

Tactic:
apply hinv
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoidWithZero M
inst_1 : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidWithZeroHomClass F M N
inst_4 : FunLike G N M
inst_5 : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), (g : (a : N) → M) ((f : (a : M) → N) a : N) = a
hp : Prime.{u_2} (M := N) ((f : (a : M) → N) p : N)
a b : M
h_1 : p ∣ a * b
h : Dvd.dvd.{u_2} (α := N) ((f : (a : M) → N) p : N) ((f : (a : M) → N) a : N)
⊢ (g : (a : N) → M) ((f : (a : M) → N) a : N) = a

Tactic:
apply hinv