awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
hk : k = k'
hn : n = n'
hkm'₁ : k < m'
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
have hq₁ : q = trinomial k m' n' (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
Tactic: subst hk
Cleared hypotheses: k', hkm', hq, hk
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' n' : ℕ
hmn' : m' < n'
x y z : ℤˣ
hn : n = n'
hkm' : k < m'
hq : q = trinomial k m' n' (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
have hmn'₁ : m' < n
Tactic: subst hn
Cleared hypotheses: n', hmn', hn, hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' n' : ℕ
hmn' : m' < n'
x y z : ℤˣ
hn : n = n'
hkm' : k < m'
hq : q = trinomial k m' n' (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
hmn'₁ : m' < n
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
have hq₁ : q = trinomial k m' n (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
Tactic: subst hn
Cleared hypotheses: n', hmn', hn, hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
have inl : ∀ (h1 : (↑y : ℤ) = (↑v : ℤ)), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Tactic: rcases eq_or_eq_neg_of_sq_eq_sq (y : ℤ) (v : ℤ)
      ((Int.isUnit_sq y.isUnit).trans (Int.isUnit_sq v.isUnit).symm) with
    (h1 | h1)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
inl : ∀ (h1 : (↑y : ℤ) = (↑v : ℤ)), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
have inr : ∀ (h1 : (↑y : ℤ) = -(↑v : ℤ)), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Tactic: rcases eq_or_eq_neg_of_sq_eq_sq (y : ℤ) (v : ℤ)
      ((Int.isUnit_sq y.isUnit).trans (Int.isUnit_sq v.isUnit).symm) with
    (h1 | h1)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
h1 : (↑y : ℤ) = (↑v : ℤ)
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
have hq₁ : q = trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ)
Tactic: rw [h1] at hq
Cleared hypotheses: hq, h1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ)
h1 : (↑y : ℤ) = (↑v : ℤ)
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
have inl : ∀ (h2 : q = p), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Tactic: rcases irreducible_aux3 hkm hmn hkm' hmn' u v w x z hp hq hpq with (h2 | h2)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (↑v : ℤ) (↑z : ℤ)
h1 : (↑y : ℤ) = (↑v : ℤ)
inl : ∀ (h2 : q = p), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
have inl₁ : ∀ (h2 : q = p.mirror), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Tactic: rcases irreducible_aux3 hkm hmn hkm' hmn' u v w x z hp hq hpq with (h2 | h2)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (↑y : ℤ) (↑z : ℤ)
h1 : (↑y : ℤ) = -(↑v : ℤ)
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
have hq₁ : q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)
Tactic: rw [h1] at hq
Cleared hypotheses: hq, h1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)
h1 : (↑y : ℤ) = -(↑v : ℤ)
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
have inr : ∀
  (hp :
    p =
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
          HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n))
  (m' : ℕ) (x y z : ℤˣ) (hkm' : k < m') (hmn' : m' < n) (hq : q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ))
  (h1 : (↑y : ℤ) = -(↑v : ℤ)), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Tactic: rw [trinomial_def] at hp
Cleared hypotheses: hp, m', x, y, z, hkm', hmn', hq, h1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp :
  p =
    HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)
h1 : (↑y : ℤ) = -(↑v : ℤ)
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
have inr : ∀
  (hp :
    -p =
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑u : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
          HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑v : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑w : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n))
  (m' : ℕ) (x y z : ℤˣ) (hkm' : k < m') (hmn' : m' < n) (hq : q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ))
  (h1 : (↑y : ℤ) = -(↑v : ℤ)), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Tactic: rw [← neg_inj, neg_add, neg_add, ← neg_mul, ← neg_mul, ← neg_mul, ← C_neg, ← C_neg, ← C_neg]
      at hp
Cleared hypotheses: hp, m', x, y, z, hkm', hmn', hq, h1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp :
  -p =
    HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑u : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑v : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑w : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)
h1 : (↑y : ℤ) = -(↑v : ℤ)
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
have inr : ∀ (hpq : -p * (-p).mirror = q * q.mirror) (k m n : ℕ) (hkm : k < m) (hmn : m < n) (u v w : ℤˣ)
  (hp :
    -p =
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑u : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
          HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑v : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑w : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n))
  (m' : ℕ) (x y z : ℤˣ) (hkm' : k < m') (hmn' : m' < n) (hq : q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ))
  (h1 : (↑y : ℤ) = -(↑v : ℤ)), q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Tactic: rw [← neg_mul_neg, ← mirror_neg] at hpq
Cleared hypotheses: hpq, k, m, n, hkm, hmn, u, v, w, hp, m', x, y, z, hkm', hmn', hq, h1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : -p * (-p).mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp :
  -p =
    HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑u : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑v : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑w : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)
h1 : (↑y : ℤ) = -(↑v : ℤ)
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
have inr : ∀ (hpq : -p * (-p).mirror = -p * (-p).mirror) (hq : -p = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)),
  -p = p ∨ -p = -p ∨ -p = p.mirror ∨ -p = -p.mirror
Tactic: rcases irreducible_aux3 hkm hmn hkm' hmn' (-u) (-v) (-w) x z hp hq hpq with (rfl | rfl)
Cleared hypotheses: q, hpq, hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : -p * (-p).mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp :
  -p =
    HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑u : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑v : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (-(↑w : ℤ)) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)
h1 : (↑y : ℤ) = -(↑v : ℤ)
inr :
  ∀ (hpq : -p * (-p).mirror = -p * (-p).mirror) (hq : -p = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)),
    -p = p ∨ -p = -p ∨ -p = p.mirror ∨ -p = -p.mirror
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
have inr₁ : ∀ (hpq : -p * (-p).mirror = (-p).mirror * (-p).mirror.mirror)
  (hq : (-p).mirror = trinomial k m' n (↑x : ℤ) (-(↑v : ℤ)) (↑z : ℤ)),
  (-p).mirror = p ∨ (-p).mirror = -p ∨ (-p).mirror = p.mirror ∨ (-p).mirror = -p.mirror
Tactic: rcases irreducible_aux3 hkm hmn hkm' hmn' (-u) (-v) (-w) x z hp hq hpq with (rfl | rfl)
Cleared hypotheses: q, hpq, hq
-- Lean 4 proof step from Mathlib.Algebra.PresentedMonoid.Basic (goal)
Goal:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
⊢ Eq (α := Submonoid (PresentedMonoid rels)) (closure (range (of rels))) ⊤
have rw : ∀ (x : PresentedMonoid rels), Membership.mem (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels))) x
Tactic: rw [Submonoid.eq_top_iff']
-- Lean 4 proof step from Mathlib.Algebra.PresentedMonoid.Basic (goal)
Goal:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x : PresentedMonoid rels
⊢ Membership.mem (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels))) x
have h : ∀ (a : FreeMonoid α),
  Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) a : PresentedMonoid rels)
Tactic: induction x with | _ a
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.PresentedMonoid.Basic (goal)
Goal:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
a : FreeMonoid α
⊢ Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) a : PresentedMonoid rels)
have h : Membership.mem (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
  ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) 1)
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
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.PresentedMonoid.Basic (goal)
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)
⊢ Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) a : PresentedMonoid rels)
have h₁ : ∀ (x : α),
  Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) (FreeMonoid.of x) : 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
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.PresentedMonoid.Basic (goal)
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)
⊢ Membership.mem (α := PresentedMonoid rels) (γ := Submonoid (PresentedMonoid rels)) (closure (range (of rels)))
    ((mk rels : (a : FreeMonoid α) → PresentedMonoid rels) a : PresentedMonoid rels)
have 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)
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
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.PresentedMonoid.Basic (goal)
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)
⊢ φ = ψ
have 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 _)
-- Lean 4 proof step from Mathlib.Algebra.Prime.Defs (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ HPow.hPow (β := ℕ) a 0
⊢ p ∣ a
have h₁ : p ∣ 1
Tactic: rw [pow_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Prime.Defs (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ 1
⊢ p ∣ a
have this : IsUnit p
Tactic: have := isUnit_of_dvd_one h
-- Lean 4 proof step from Mathlib.Algebra.Prime.Defs (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ 1
this : IsUnit p
⊢ p ∣ a
have this₁ : ¬IsUnit p
Tactic: have := not_unit hp
-- Lean 4 proof step from Mathlib.Algebra.Prime.Defs (hypothesis)
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
have h₁ : p ∣ a * a ^ n
Tactic: rw [pow_succ'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Prime.Defs (goal)
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
⊢ p ∣ a
have succ : ∀ (dvd_a : p ∣ a), p ∣ a
Tactic: rcases dvd_or_dvd hp h with dvd_a | dvd_pow
-- Lean 4 proof step from Mathlib.Algebra.Prime.Defs (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
h : p ∣ a ^ n
⊢ p ∣ a
have zero : ∀ (h : p ∣ HPow.hPow (β := ℕ) a 0), 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
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Prime.Defs (goal)
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
⊢ p ∣ a
have succ : ∀ (n : ℕ) (ih : ∀ (h : p ∣ a ^ n), p ∣ a) (h : p ∣ a ^ (n + 1)), 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
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Prime.Defs (goal)
Goal:
M : Type u_1
inst : Monoid M
p : M
hp : Irreducible p
q' : M
hq : Irreducible (p * q')
⊢ p * q' ∣ p
have rw : p ∣ p
Tactic: rw [IsUnit.mul_right_dvd (Or.resolve_left (of_irreducible_mul hq) hp.not_isUnit)]
-- Lean 4 proof step from Mathlib.Algebra.Prime.Defs (goal)
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
⊢ a_1 ∣ a ∨ a_1 ∣ b
have 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
Tactic: obtain ⟨d₁, d₂, h₁, h₂, rfl⟩ := primal dvd
Cleared hypotheses: a_1, irr, primal, dvd
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
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
⊢ (f : (a : M) → N) p ∣ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)
have h₁ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) = (f : (a : M) → N) (a * b)
Tactic: convert! map_dvd f h
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
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
⊢ p ∣ a ∨ p ∣ b
have refine_1 : Dvd.dvd.{u_2} (α := N) ((f : (a : M) → N) p : N) ((f : (a : M) → N) a : N) → p ∣ a
Tactic: refine
        (hp.2.2 (f a) (f b) <| by
              convert! map_dvd f h
              simp).imp
          ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
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
⊢ p ∣ a ∨ p ∣ b
have refine_2 : Dvd.dvd.{u_2} (α := N) ((f : (a : M) → N) p : N) ((f : (a : M) → N) b : N) → p ∣ b
Tactic: refine
        (hp.2.2 (f a) (f b) <| by
              convert! map_dvd f h
              simp).imp
          ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
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)
⊢ p ∣ a
have h₁ : (g : (a : N) → M) ((f : (a : M) → N) p : N) = p
Tactic: convert! ← map_dvd g h
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
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
⊢ p ∣ a
have h₂ : (g : (a : N) → M) ((f : (a : M) → N) a : N) = a
Tactic: convert! ← map_dvd g h
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
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) b : N)
⊢ p ∣ b
have h₁ : (g : (a : N) → M) ((f : (a : M) → N) p : N) = p
Tactic: convert! ← map_dvd g h
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
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) b : N)
h₁ : (g : (a : N) → M) ((f : (a : M) → N) p : N) = p
⊢ p ∣ b
have h₂ : (g : (a : N) → M) ((f : (a : M) → N) b : N) = b
Tactic: convert! ← map_dvd g h
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
a b c : M
hc : p * b = a * c
⊢ p ∣ a ∨ a ∣ b
have inl : ∀ (h : p ∣ a), p ∣ a ∨ a ∣ b
Tactic: rcases hp.2.2 a c (hc ▸ dvd_mul_right _ _) with (h | ⟨x, rfl⟩)