Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := ⋯
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ ∀ x ∈ p ::ₘ fx, Irreducible x

pp: case a
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := ⋯
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ ∀ x ∈ fa + fb, Irreducible x

pp: case a
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := ⋯
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ (p ::ₘ fx).prod ~ᵤ (fa + fb).prod

Tactic:
· exact fun i hi => (Multiset.mem_cons.1 hi).elim (fun hip => hip.symm ▸ hpi) (hfx.1 _)

Goal state after:
case a
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := ⋯
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ ∀ x ∈ fa + fb, Irreducible x

case a
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := ⋯
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ (p ::ₘ fx).prod ~ᵤ (fa + fb).prod