no goals
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
⊢ a :: l₁ ~ b :: l₂
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
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
⊢ a :: l₁ ~ b :: l₂
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
⊢ a :: l₁ ~ b :: l₂
have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
⊢ a :: l₁ ~ b :: l₂
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
⊢ a :: l₁ ~ b :: l₂
have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
ha : a ∈ b :: l₂
⊢ a :: l₁ ~ b :: l₂
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
⊢ a :: l₁ ~ b :: l₂
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 _ _)
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: List.erase (b :: l₂) a
⊢ a :: l₁ ~ b :: l₂
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
ha : a ∈ b :: l₂
⊢ a :: l₁ ~ b :: l₂
have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: List.erase (b :: l₂) a
hl : prod l₁ = prod (List.erase (b :: l₂) a)
⊢ a :: l₁ ~ b :: l₂
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: List.erase (b :: l₂) a
⊢ a :: l₁ ~ b :: l₂
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]
no goals
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: List.erase (b :: l₂) a
hl : prod l₁ = prod (List.erase (b :: l₂) a)
⊢ a :: l₁ ~ b :: l₂
exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
⊢ a ∣ a * prod l₁
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
⊢ a ∣ prod (a :: l₁)
rw [prod_cons]
no goals
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
⊢ a ∣ a * prod l₁
exact dvd_mul_right _ _
no goals
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: List.erase (b :: l₂) a
⊢ a * prod l₁ = a * prod (List.erase (b :: l₂) a)
rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]