-- Mathlib/Algebra/GroupWithZero/Divisibility.lean
theorem IsPrimal.mul {α} [CancelCommMonoidWithZero α] {m n : α}
    (hm : IsPrimal m) (hn : IsPrimal n) : IsPrimal (m * n)

Proof state:
case inr.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : CancelCommMonoidWithZero α
n : α
hn : IsPrimal n
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
h : a₁ * a₂ * n ∣ a₁ * b * (a₂ * c)
⊢ ∃ a₁_1 a₂_1, a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * n = a₁_1 * a₂_1

Tactic:
rw [mul_mul_mul_comm, mul_dvd_mul_iff_left h0] at h

Result:
case inr.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : CancelCommMonoidWithZero α
n : α
hn : IsPrimal n
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
h : n ∣ b * c
⊢ ∃ a₁_1 a₂_1, a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * n = a₁_1 * a₂_1

Proof state:
case inr.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : CancelCommMonoidWithZero α
n : α
hn : IsPrimal n
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
h : n ∣ b * c
⊢ ∃ a₁_1 a₂_1, a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * n = a₁_1 * a₂_1

Tactic:
obtain ⟨a₁', a₂', h₁, h₂, rfl⟩ := hn h

Result:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : CancelCommMonoidWithZero α
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
a₁' a₂' : α
h₁ : a₁' ∣ b
h₂ : a₂' ∣ c
hn : IsPrimal (a₁' * a₂')
h : a₁' * a₂' ∣ b * c
⊢ ∃ a₁_1 a₂_1, a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * (a₁' * a₂') = a₁_1 * a₂_1

Proof state:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : CancelCommMonoidWithZero α
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
a₁' a₂' : α
h₁ : a₁' ∣ b
h₂ : a₂' ∣ c
hn : IsPrimal (a₁' * a₂')
h : a₁' * a₂' ∣ b * c
⊢ ∃ a₁_1 a₂_1, a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * (a₁' * a₂') = a₁_1 * a₂_1

Tactic:
exact ⟨a₁ * a₁', a₂ * a₂', mul_dvd_mul_left _ h₁, mul_dvd_mul_left _ h₂, mul_mul_mul_comm _ _ _ _⟩

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝ : CancelCommMonoidWithZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
h0 : m ≠ 0
⊢ IsPrimal (m * n)

Tactic:
intro b c h

Result:
case inr
α : Type u_2
inst✝ : CancelCommMonoidWithZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
h0 : m ≠ 0
b c : α
h : m * n ∣ b * c
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ m * n = a₁ * a₂

Proof state:
case inr
α : Type u_2
inst✝ : CancelCommMonoidWithZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
h0 : m ≠ 0
b c : α
h : m * n ∣ b * c
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ m * n = a₁ * a₂

Tactic:
obtain ⟨a₁, a₂, ⟨b, rfl⟩, ⟨c, rfl⟩, rfl⟩ := hm (dvd_of_mul_right_dvd h)

Result:
case inr.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : CancelCommMonoidWithZero α
n : α
hn : IsPrimal n
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
h : a₁ * a₂ * n ∣ a₁ * b * (a₂ * c)
⊢ ∃ a₁_1 a₂_1, a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * n = a₁_1 * a₂_1

Proof state:
α : Type u_2
inst✝ : CancelCommMonoidWithZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
⊢ IsPrimal (m * n)

Tactic:
obtain rfl | h0 := eq_or_ne m 0

Result:
case inl
α : Type u_2
inst✝ : CancelCommMonoidWithZero α
n : α
hn : IsPrimal n
hm : IsPrimal 0
⊢ IsPrimal (0 * n)

case inr
α : Type u_2
inst✝ : CancelCommMonoidWithZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
h0 : m ≠ 0
⊢ IsPrimal (m * n)

Proof state:
case inl
α : Type u_2
inst✝ : CancelCommMonoidWithZero α
n : α
hn : IsPrimal n
hm : IsPrimal 0
⊢ IsPrimal (0 * n)

Tactic:
rwa [zero_mul]

Result:
no goals