awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) b : 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) b : 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) b : N)
h₁ : (g : (a : N) → M) ((f : (a : M) → N) p : N) = p
h₂ : (g : (a : N) → M) ((f : (a : M) → N) b : N) = b
⊢ p ∣ b

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) b : 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) b : N)
⊢ (g : (a : N) → M) ((f : (a : M) → N) b : N) = b

Tactic:
apply hinv
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoidWithZero M
inst_1 : CommMonoidWithZero N
p : M
E : Type u_5
inst_2 : EquivLike E M N
inst_3 : MulEquivClass E M N
e_1 : E
e : M ≃* N := (↑e_1 : M ≃* N)
a : M
⊢ (e.symm : (a : N) → M) ((e : (a : M) → N) a : N) = a

Tactic:
simp
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoidWithZero M
inst_1 : CommMonoidWithZero N
p : M
E : Type u_5
inst_2 : EquivLike E M N
inst_3 : MulEquivClass E M N
e_1 : E
e : M ≃* N := (↑e_1 : M ≃* N)
h : Prime p
a : N
⊢ (e : (a : M) → N) ((e.symm : (a : N) → M) a : M) = a

Tactic:
simp
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoidWithZero M
inst_1 : CommMonoidWithZero N
p : M
E : Type u_5
inst_2 : EquivLike E M N
inst_3 : MulEquivClass E M N
e_1 : E
e : M ≃* N := (↑e_1 : M ≃* N)
⊢ Prime.{u_2} (M := N) ((e_1 : (a : M) → N) p : N) ↔ Prime p

Tactic:
exact ⟨comap_prime e e.symm fun a => by simp,
    fun h => (comap_prime e.symm e fun a => by simp) <| (e.symm_apply_apply p).substr h⟩
-- Module: Mathlib.Algebra.Prime.Lemmas
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
inl : ∀ (h : p ∣ a), p ∣ a ∨ a ∣ b
inr : ∀ (x : M) (hc : p * b = a * (p * x)), p ∣ a ∨ a ∣ b
⊢ p ∣ a ∨ a ∣ b

Tactic:
rcases hp.2.2 a c (hc ▸ dvd_mul_right _ _) with (h | ⟨x, rfl⟩)

Premises used: Eq.rec, And.right, dvd_mul_right, rfl
-- Module: Mathlib.Algebra.Prime.Lemmas
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
h : p ∣ a
⊢ p ∣ a ∨ a ∣ b

Tactic:
Or.inl h

Premises used: Or.inl
-- Module: Mathlib.Algebra.Prime.Lemmas
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
h : p ∣ a
⊢ p ∣ a ∨ a ∣ b

Tactic:
exact Or.inl h

Premises used: Or.inl
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
a b x : M
hc : p * b = a * (p * x)
⊢ b = a * x

Tactic:
rw [mul_left_comm, mul_right_inj' hp.ne_zero] at hc

Premises used: mul_left_comm, Prime.ne_zero, mul_right_inj'
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
a b x : M
hc : b = a * x
⊢ p ∣ a ∨ a ∣ b

Tactic:
Or.inr (hc.symm ▸ dvd_mul_right _ _)

Premises used: Eq.rec, dvd_mul_right, Eq.symm, Or.inr
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
a b x : M
hc : b = a * x
⊢ p ∣ a ∨ a ∣ b

Tactic:
exact Or.inr (hc.symm ▸ dvd_mul_right _ _)

Premises used: Or.inr
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
hp : Prime p
h : ¬p ∣ a
h' : HPow.hPow (β := ℕ) p 0 ∣ a * b
zero : 1 ∣ b
⊢ HPow.hPow (β := ℕ) p 0 ∣ b

Tactic:
rw [pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
hp : Prime p
h : ¬p ∣ a
h' : HPow.hPow (β := ℕ) p 0 ∣ a * b
⊢ 1 ∣ b

Tactic:
one_dvd b

Premises used: one_dvd
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
hp : Prime p
h : ¬p ∣ a
h' : HPow.hPow (β := ℕ) p 0 ∣ a * b
⊢ 1 ∣ b

Tactic:
exact one_dvd b

Premises used: one_dvd
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
ih : ∀ (h' : p ^ n ∣ a * b), p ^ n ∣ b
h' : p ^ (n + 1) ∣ a * b
succ :
  ∀ (c : M) (ih : ∀ (h' : p ^ n ∣ a * (p ^ n * c)), p ^ n ∣ p ^ n * c) (h' : p ^ (n + 1) ∣ a * (p ^ n * c)),
    p ^ (n + 1) ∣ p ^ n * c
⊢ p ^ (n + 1) ∣ b

Tactic:
obtain ⟨c, rfl⟩ := ih (dvd_trans (pow_dvd_pow p n.le_succ) h')

Premises used: pow_dvd_pow, Nat.le_succ, dvd_trans, rfl
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
c : M
ih : ∀ (h' : p ^ n ∣ a * (p ^ n * c)), p ^ n ∣ p ^ n * c
h' : p ^ (n + 1) ∣ a * (p ^ n * c)
succ : p ^ n * p ∣ p ^ n * c
⊢ p ^ (n + 1) ∣ p ^ n * c

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
c : M
ih : ∀ (h' : p ^ n ∣ a * (p ^ n * c)), p ^ n ∣ p ^ n * c
h' : p ^ (n + 1) ∣ a * (p ^ n * c)
apply : p ∣ a * c
⊢ p ^ n * p ∣ p ^ n * c

Tactic:
apply mul_dvd_mul_left _ ((hp.dvd_or_dvd _).resolve_left h)

Premises used: Prime.dvd_or_dvd, mul_dvd_mul_left, Or.resolve_left
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
c : M
ih : ∀ (h' : p ^ n ∣ a * (p ^ n * c)), p ^ n ∣ p ^ n * c
h' : p ^ (n + 1) ∣ a * (p ^ n * c)
rwa : p ^ n * p ∣ p ^ n * (a * c)
rwa₁ : p ^ (n + 1) ∣ p ^ n * (a * c)
rwa₂ rwa₃ rwa₄ rwa₅ : p ^ (n + 1) ∣ a * (p ^ n * c)
⊢ p ∣ a * c

Tactic:
rwa [← mul_dvd_mul_iff_left (pow_ne_zero n hp.ne_zero), ← pow_succ, mul_left_comm]

Premises used: pow_succ, pow_ne_zero, mul_left_comm, mul_dvd_mul_iff_left, Prime.ne_zero
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
hp : Prime p
n : ℕ
h : ¬p ∣ a
h' : p ^ n ∣ a * b
zero : ∀ (h' : HPow.hPow (β := ℕ) p 0 ∣ a * b), HPow.hPow (β := ℕ) p 0 ∣ b
succ : ∀ (n : ℕ) (ih : ∀ (h' : p ^ n ∣ a * b), p ^ n ∣ b) (h' : p ^ (n + 1) ∣ a * b), p ^ (n + 1) ∣ b
⊢ p ^ n ∣ b

Tactic:
induction n with
  | zero =>
    rw [pow_zero]
    exact one_dvd b
  | succ n ih =>
    obtain ⟨c, rfl⟩ := ih (dvd_trans (pow_dvd_pow p n.le_succ) h')
    rw [pow_succ]
    apply mul_dvd_mul_left _ ((hp.dvd_or_dvd _).resolve_left h)
    rwa [← mul_dvd_mul_iff_left (pow_ne_zero n hp.ne_zero), ← pow_succ, mul_left_comm]

Premises used: Prime.dvd_or_dvd, pow_succ, pow_ne_zero, mul_dvd_mul_left, Or.resolve_left, mul_left_comm, pow_zero, mul_dvd_mul_iff_left, one_dvd, Prime.ne_zero, rfl
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
hp : Prime p
n : ℕ
h : ¬p ∣ b
h' : p ^ n ∣ a * b
⊢ p ^ n ∣ b * a

Tactic:
rw [mul_comm] at h'

Premises used: mul_comm
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
hp : Prime p
n : ℕ
h : ¬p ∣ b
h' : p ^ n ∣ b * a
⊢ p ^ n ∣ a

Tactic:
hp.pow_dvd_of_dvd_mul_left n h h'

Premises used: Prime.pow_dvd_of_dvd_mul_left
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
hp : Prime p
n : ℕ
h : ¬p ∣ b
h' : p ^ n ∣ b * a
⊢ p ^ n ∣ a

Tactic:
exact hp.pow_dvd_of_dvd_mul_left n h h'

Premises used: Prime.pow_dvd_of_dvd_mul_left
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ b
inl : ∀ (H : p ∣ a ^ n.succ), p ∣ a
inr : ∀ (hbdiv : p ∣ b ^ n), p ∣ a
⊢ p ∣ a

Tactic:
rcases hp.dvd_or_dvd ((dvd_pow_self p (Nat.succ_ne_zero n)).trans hpow) with H | hbdiv

Premises used: Prime.dvd_or_dvd, dvd_pow_self, Nat.succ_ne_zero, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ b
H : p ∣ a ^ n.succ
⊢ p ∣ a

Tactic:
hp.dvd_of_dvd_pow H

Premises used: Prime.dvd_of_dvd_pow
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ b
H : p ∣ a ^ n.succ
⊢ p ∣ a

Tactic:
exact hp.dvd_of_dvd_pow H

Premises used: Prime.dvd_of_dvd_pow
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ b
hbdiv : p ∣ b ^ n
inr :
  ∀ (x : M) (hpow : p ^ n.succ ∣ a ^ n.succ * (p * x) ^ n) (hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x)
    (hbdiv : p ∣ (p * x) ^ n), p ∣ a
⊢ p ∣ a

Tactic:
obtain ⟨x, rfl⟩ := hp.dvd_of_dvd_pow hbdiv

Premises used: Prime.dvd_of_dvd_pow, rfl
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hpow : p ^ n.succ ∣ a ^ n.succ * (p * x) ^ n
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
inr : ∀ (y : M) (hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y), p ∣ a
⊢ p ∣ a

Tactic:
obtain ⟨y, hy⟩ := hpow
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ a ^ n.succ * x ^ n = p * y

Tactic:
mul_left_cancel₀ (pow_ne_zero n hp.ne_zero) ?_

Premises used: pow_ne_zero, mul_left_cancel₀, Prime.ne_zero
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
refine : p ^ n * (a ^ n.succ * x ^ n) = p ^ n * (p * y)
⊢ a ^ n.succ * x ^ n = p * y

Tactic:
refine mul_left_cancel₀ (pow_ne_zero n hp.ne_zero) ?_

Premises used: pow_ne_zero, mul_left_cancel₀, Prime.ne_zero
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
rw : p ^ n * (a ^ n.succ * x ^ n) = p ^ n * p * y
rw₁ : p ^ n * (a ^ n.succ * x ^ n) = p ^ (n + 1) * y
rw₂ : p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * (p * x) ^ n
rw₃ : p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * (p ^ n * x ^ n)
rw₄ : p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * p ^ n * x ^ n
rw₅ : p ^ n * (a ^ n.succ * x ^ n) = p ^ n * a ^ n.succ * x ^ n
rw₆ rw₇ : p ^ n * (a ^ n.succ * x ^ n) = p ^ n * (a ^ n.succ * x ^ n)
⊢ p ^ n * (a ^ n.succ * x ^ n) = p ^ n * (p * y)

Tactic:
rw [← mul_assoc _ p, ← pow_succ, ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n),
      mul_assoc]

Premises used: pow_succ, mul_assoc, HPow.hPow, mul_comm, mul_pow, Nat.succ
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ a ^ n.succ * x ^ n = p * y

Tactic:
have : a ^ n.succ * x ^ n = p * y := by
    refine mul_left_cancel₀ (pow_ne_zero n hp.ne_zero) ?_
    rw [← mul_assoc _ p, ← pow_succ, ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n),
      mul_assoc]
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
this : a ^ n.succ * x ^ n = p * y
⊢ p ∣ a

Tactic:
hp.dvd_of_dvd_pow ((hp.dvd_or_dvd ⟨_, this⟩).resolve_right fun hdvdx => hb ?_)

Premises used: Prime.dvd_or_dvd, Exists.intro, Or.resolve_right, Prime.dvd_of_dvd_pow
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
this : a ^ n.succ * x ^ n = p * y
inr : ∀ (hdvdx : p ∣ x ^ n), HPow.hPow (β := ℕ) p 2 ∣ p * x
⊢ p ∣ a

Tactic:
refine hp.dvd_of_dvd_pow ((hp.dvd_or_dvd ⟨_, this⟩).resolve_right fun hdvdx => hb ?_)

Premises used: Prime.dvd_or_dvd, Exists.intro, Or.resolve_right, Prime.dvd_of_dvd_pow
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
this : a ^ n.succ * x ^ n = p * y
hdvdx : p ∣ x ^ n
inr :
  ∀ (z : M) (hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * (p * z)) (hbdiv : p ∣ (p * (p * z)) ^ n)
    (hy : a ^ n.succ * (p * (p * z)) ^ n = p ^ n.succ * y) (this : a ^ n.succ * (p * z) ^ n = p * y)
    (hdvdx : p ∣ (p * z) ^ n), HPow.hPow (β := ℕ) p 2 ∣ p * (p * z)
⊢ HPow.hPow (β := ℕ) p 2 ∣ p * x

Tactic:
obtain ⟨z, rfl⟩ := hp.dvd_of_dvd_pow hdvdx

Premises used: Prime.dvd_of_dvd_pow, rfl
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
y z : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ n.succ * (p * (p * z)) ^ n = p ^ n.succ * y
this : a ^ n.succ * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
inr : p * p ∣ p * p * z
⊢ HPow.hPow (β := ℕ) p 2 ∣ p * (p * z)

Tactic:
rw [pow_two, ← mul_assoc]

Premises used: pow_two, mul_assoc
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
y z : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ n.succ * (p * (p * z)) ^ n = p ^ n.succ * y
this : a ^ n.succ * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
⊢ p * p ∣ p * p * z

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
y z : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ n.succ * (p * (p * z)) ^ n = p ^ n.succ * y
this : a ^ n.succ * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
⊢ p * p ∣ p * p * z

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p x y : M
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
rw : ¬p ∣ y → p ^ (i + 1) ∣ x
⊢ p ^ (i + 1) ∣ x ∨ p ∣ y

Tactic:
rw [or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p x y : M
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
⊢ ¬p ∣ y → p ^ (i + 1) ∣ x

Tactic:
fun a ↦ Prime.pow_dvd_of_dvd_mul_right h (i + 1) a hxy

Premises used: Prime.pow_dvd_of_dvd_mul_right, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p x y : M
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
⊢ ¬p ∣ y → p ^ (i + 1) ∣ x

Tactic:
exact fun a ↦ Prime.pow_dvd_of_dvd_mul_right h (i + 1) a hxy

Premises used: Prime.pow_dvd_of_dvd_mul_right, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
a b : M
k l : ℕ
h : p ^ k ∣ a
h_1 : p ^ l ∣ b
h_2 : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
⊢ p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)

Tactic:
simpa [mul_comm, pow_add, hx, hy, mul_assoc, mul_left_comm] using hz

Premises used: mul_assoc, pow_add, mul_left_comm, mul_comm
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
a b : M
k l : ℕ
h_1 : p ^ k ∣ a
h_2 : p ^ l ∣ b
h_3 : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : x * y = p * z) (hp0 : p ^ (k + l) ≠ 0), x * y = p * z
⊢ x * y = p * z

Tactic:
rwa [mul_right_inj' hp0] at h

Premises used: mul_right_inj'
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
a b : M
k l : ℕ
h_1 : p ^ k ∣ a
h_2 : p ^ l ∣ b
h_3 : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
hpd : p ∣ x * y
h_4 : p ∣ x
d : M
hd : x = p * d
⊢ a = p ^ (k + 1) * d

Tactic:
simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]

Premises used: pow_succ, mul_assoc, mul_left_comm, mul_comm
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
a b : M
k l : ℕ
h_1 : p ^ k ∣ a
h_2 : p ^ l ∣ b
h_3 : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
hpd : p ∣ x * y
h_4 : p ∣ y
d : M
hd : y = p * d
⊢ b = p ^ (l + 1) * d

Tactic:
simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]

Premises used: pow_succ, mul_assoc, mul_left_comm, mul_comm
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
⊢ ¬IsSquare p

Tactic:
hp.irreducible.not_isSquare

Premises used: Prime.irreducible, Irreducible.not_isSquare
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
a : M
ha : IsSquare a
⊢ ¬Prime a

Tactic:
fun h => h.not_isSquare ha

Premises used: Prime.not_isSquare, Not
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
a : M
n : ℕ
hn : n ≠ 1
⊢ ¬Prime (a ^ n)

Tactic:
fun hp =>
  not_irreducible_pow hn hp.irreducible

Premises used: Prime.irreducible, not_irreducible_pow, Not
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p q : M
h : DvdNotUnit p q
hq : Irreducible q
obtain : p ≠ 0 → ∀ (x : M) (hx : ¬IsUnit x) (hx' : q = p * x), IsUnit p
⊢ IsUnit p

Tactic:
obtain ⟨_, x, hx, hx'⟩ := h
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p q : M
hq : Irreducible q
left : p ≠ 0
x : M
hx : ¬IsUnit x
hx' : q = p * x
⊢ IsUnit p

Tactic:
((irreducible_iff.1 hq).right hx').resolve_right hx

Premises used: And.right, Iff.mp, irreducible_iff, Or.resolve_right
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p q : M
hq : Irreducible q
left : p ≠ 0
x : M
hx : ¬IsUnit x
hx' : q = p * x
⊢ IsUnit p

Tactic:
exact ((irreducible_iff.1 hq).right hx').resolve_right hx

Premises used: And.right, Iff.mp, irreducible_iff, Or.resolve_right
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p q : M
hp : ¬IsUnit p
h : DvdNotUnit p q
⊢ ¬Irreducible q

Tactic:
mt h.isUnit_of_irreducible_right hp

Premises used: mt, DvdNotUnit.isUnit_of_irreducible_right
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p q : M
hp : DvdNotUnit p q
obtain : ∀ (x : M) (hx : ¬IsUnit x), ¬IsUnit (p * x)
⊢ ¬IsUnit q

Tactic:
obtain ⟨-, x, hx, rfl⟩ := hp

Premises used: rfl
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p x : M
hx : ¬IsUnit x
⊢ ¬IsUnit (p * x)

Tactic:
fun hc => hx (isUnit_iff_dvd_one.mpr (dvd_of_mul_left_dvd (isUnit_iff_dvd_one.mp hc)))

Premises used: Iff.mpr, dvd_of_mul_left_dvd, Iff.mp, Not, isUnit_iff_dvd_one
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p x : M
hx : ¬IsUnit x
⊢ ¬IsUnit (p * x)

Tactic:
exact fun hc => hx (isUnit_iff_dvd_one.mpr (dvd_of_mul_left_dvd (isUnit_iff_dvd_one.mp hc)))

Premises used: Iff.mpr, dvd_of_mul_left_dvd, Iff.mp, isUnit_iff_dvd_one
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p q : M
h : DvdNotUnit p q
by_contra : ∀ (hcontra : p = q), False
⊢ p ≠ q

Tactic:
by_contra hcontra
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p q : M
h : DvdNotUnit p q
hcontra : p = q
obtain : ∀ (hp : p ≠ 0) (x : M) (hx' : ¬IsUnit x) (hx'' : q = p * x), False
⊢ False

Tactic:
obtain ⟨hp, x, hx', hx''⟩ := h
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p q : M
hcontra : p = q
hp : p ≠ 0
x : M
hx' : ¬IsUnit x
hx'' : q = p * x
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
⊢ Function.Injective.{1, u_1 + 1} (β := M) fun (n : ℕ) ↦ q ^ n

Tactic:
.of_lt_imp_ne fun n m h => DvdNotUnit.ne ⟨pow_ne_zero n hq', q ^ (m - n), ?_, ?_⟩

Premises used: HSub.hSub, Function.Injective.of_lt_imp_ne, pow_ne_zero, HPow.hPow, DvdNotUnit.ne, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Prime.Lemmas
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
refine_1 : ∀ (n m : ℕ) (h : n < m), ¬IsUnit (q ^ (m - n))
refine_2 : ∀ (n m : ℕ) (h : n < m), q ^ m = q ^ n * q ^ (m - n)
⊢ Function.Injective.{1, u_1 + 1} (β := M) fun (n : ℕ) ↦ q ^ n

Tactic:
refine .of_lt_imp_ne fun n m h => DvdNotUnit.ne ⟨pow_ne_zero n hq', q ^ (m - n), ?_, ?_⟩