-- Mathlib/Data/List/Prime.lean
theorem perm_of_prod_eq_prod :
    ∀ {l₁ l₂ : List M}, l₁.prod = l₂.prod → (∀ p ∈ l₁, Prime p) → (∀ p ∈ l₂, Prime p) → Perm l₁ l₂
  | [], [], _, _, _ => Perm.nil
  | [], a :: l, h₁, _, h₃ =>
    have ha : a ∣ 1 := prod_nil (M := M) ▸ h₁.symm ▸ (prod_cons (l := l)).symm ▸ dvd_mul_right _ _
    absurd ha (Prime.not_dvd_one (h₃ a (mem_cons_self _ _)))
  | a :: l, [], h₁, h₂, _ =>
    have ha : a ∣ 1 := prod_nil (M := M) ▸ h₁ ▸ (prod_cons (l := l)).symm ▸ dvd_mul_right _ _
    absurd ha (Prime.not_dvd_one (h₂ a (mem_cons_self _ _)))
  | a :: l₁, b :: l₂, h, hl₁, hl₂ => by
    classical
      have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)
      have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)
      have ha : a ∈ b :: l₂ :=
        mem_list_primes_of_dvd_prod (hl₁ a (mem_cons_self _ _)) hl₂
          (h ▸ by rw [prod_cons]; exact dvd_mul_right _ _)
      have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha
      have hl : prod l₁ = prod ((b :: l₂).erase a) :=
        (mul_right_inj' (hl₁ a (mem_cons_self _ _)).ne_zero).1 <| by
          rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
      exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm

Proof state:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ p ∈ a :: l₁, Prime p
hl₂ : ∀ p ∈ b :: l₂, Prime p
hl₁' : ∀ p ∈ l₁, Prime p
hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p
ha : a ∈ b :: l₂
⊢ a :: l₁ ~ b :: l₂

Tactic:
have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha

Result:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ p ∈ a :: l₁, Prime p
hl₂ : ∀ p ∈ b :: l₂, Prime p
hl₁' : ∀ p ∈ l₁, Prime p
hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
⊢ a :: l₁ ~ b :: l₂

Proof state:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ p ∈ a :: l₁, Prime p
hl₂ : ∀ p ∈ b :: l₂, Prime p
⊢ a :: l₁ ~ b :: l₂

Tactic:
have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)

Result:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ p ∈ a :: l₁, Prime p
hl₂ : ∀ p ∈ b :: l₂, Prime p
hl₁' : ∀ p ∈ l₁, Prime p
⊢ a :: l₁ ~ b :: l₂

Proof state:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ p ∈ a :: l₁, Prime p
hl₂ : ∀ p ∈ b :: l₂, Prime p
hl₁' : ∀ p ∈ l₁, Prime p
hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
⊢ a * l₁.prod = a * ((b :: l₂).erase a).prod

Tactic:
rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ p ∈ a :: l₁, Prime p
hl₂ : ∀ p ∈ b :: l₂, Prime p
hl₁' : ∀ p ∈ l₁, Prime p
hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
hl : l₁.prod = ((b :: l₂).erase a).prod
⊢ a :: l₁ ~ b :: l₂

Tactic:
exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ p ∈ a :: l₁, Prime p
hl₂ : ∀ p ∈ b :: l₂, Prime p
⊢ a :: l₁ ~ b :: l₂

Tactic:
classical
  have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)
  have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)
  have ha : a ∈ b :: l₂ :=
    mem_list_primes_of_dvd_prod (hl₁ a (mem_cons_self _ _)) hl₂
      (h ▸ by rw [prod_cons]; exact dvd_mul_right _ _)
  have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha
  have hl : prod l₁ = prod ((b :: l₂).erase a) :=
    (mul_right_inj' (hl₁ a (mem_cons_self _ _)).ne_zero).1 <| by
      rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
  exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ p ∈ a :: l₁, Prime p
hl₂ : ∀ p ∈ b :: l₂, Prime p
hl₁' : ∀ p ∈ l₁, Prime p
hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p
⊢ a :: l₁ ~ b :: l₂

Tactic:
have ha : a ∈ b :: l₂ :=
  mem_list_primes_of_dvd_prod (hl₁ a (mem_cons_self _ _)) hl₂
    (h ▸ by rw [prod_cons]; exact dvd_mul_right _ _)

Result:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ p ∈ a :: l₁, Prime p
hl₂ : ∀ p ∈ b :: l₂, Prime p
hl₁' : ∀ p ∈ l₁, Prime p
hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p
ha : a ∈ b :: l₂
⊢ a :: l₁ ~ b :: l₂

Proof state:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ p ∈ a :: l₁, Prime p
hl₂ : ∀ p ∈ b :: l₂, Prime p
hl₁' : ∀ p ∈ l₁, Prime p
hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p
⊢ a ∣ (a :: l₁).prod

Tactic:
rw [prod_cons]

Result:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ p ∈ a :: l₁, Prime p
hl₂ : ∀ p ∈ b :: l₂, Prime p
hl₁' : ∀ p ∈ l₁, Prime p
hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p
⊢ a ∣ a * l₁.prod

Proof state:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ p ∈ a :: l₁, Prime p
hl₂ : ∀ p ∈ b :: l₂, Prime p
hl₁' : ∀ p ∈ l₁, Prime p
hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p
⊢ a ∣ a * l₁.prod

Tactic:
exact dvd_mul_right _ _

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ p ∈ a :: l₁, Prime p
hl₂ : ∀ p ∈ b :: l₂, Prime p
hl₁' : ∀ p ∈ l₁, Prime p
⊢ a :: l₁ ~ b :: l₂

Tactic:
have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)

Result:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ p ∈ a :: l₁, Prime p
hl₂ : ∀ p ∈ b :: l₂, Prime p
hl₁' : ∀ p ∈ l₁, Prime p
hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p
⊢ a :: l₁ ~ b :: l₂

Proof state:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ p ∈ a :: l₁, Prime p
hl₂ : ∀ p ∈ b :: l₂, Prime p
hl₁' : ∀ p ∈ l₁, Prime p
hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
⊢ a :: l₁ ~ b :: l₂

Tactic:
have hl : prod l₁ = prod ((b :: l₂).erase a) :=
  (mul_right_inj' (hl₁ a (mem_cons_self _ _)).ne_zero).1 <| by
    rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]

Result:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ p ∈ a :: l₁, Prime p
hl₂ : ∀ p ∈ b :: l₂, Prime p
hl₁' : ∀ p ∈ l₁, Prime p
hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
hl : l₁.prod = ((b :: l₂).erase a).prod
⊢ a :: l₁ ~ b :: l₂