Theorem: exists_prime_factors_of_exists_multiset (Kaplanski4/Kaplanski.lean)

State before:
R : Type u_1
inst✝ : CommMonoidWithZero R
a : R
h : ∃ l, ∃ (_ : ∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod l = a
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
rcases h with ⟨l ,hl, hl₂⟩
State after:
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
a : R
l : Multiset R
hl : ∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}
hl₂ : Multiset.prod l = a
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a

State before:
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
a : R
l : Multiset R
hl : ∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}
hl₂ : Multiset.prod l = a
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
revert a hl hl₂
State after:
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ ∀ (a : R),
    (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
      Multiset.prod l = a → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a

State before:
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ ∀ (a : R),
    (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
      Multiset.prod l = a → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
refine' l.induction (p := fun l => ∀ a, (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
  l.prod = a → ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod a) _ _
State after:
case intro.intro.refine'_1
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ (fun l =>
      ∀ (a : R),
        (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
          Multiset.prod l = a → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a)
    0

case intro.intro.refine'_2
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    (fun l =>
          ∀ (a : R),
            (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
              Multiset.prod l = a → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a)
        s →
      (fun l =>
          ∀ (a : R),
            (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
              Multiset.prod l = a → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a)
        (a ::ₘ s)

State before:
case intro.intro.refine'_1
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ (fun l =>
      ∀ (a : R),
        (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
          Multiset.prod l = a → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a)
    0
Tactic:
simp only [Multiset.not_mem_zero, Set.mem_setOf_eq, IsEmpty.forall_iff, forall_const,
  Multiset.prod_zero, forall_true_left, forall_eq']
State after:
case intro.intro.refine'_1
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) 1

State before:
case intro.intro.refine'_1
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) 1
Tactic:
use 0
State after:
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ (∀ b ∈ 0, Prime b) ∧ Associated (Multiset.prod 0) 1

State before:
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ (∀ b ∈ 0, Prime b) ∧ Associated (Multiset.prod 0) 1
Tactic:
simp only [Multiset.not_mem_zero, IsEmpty.forall_iff, forall_const, Multiset.prod_zero,
  true_and]
State after:
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ Associated 1 1

State before:
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ Associated 1 1
Tactic:
exact Associated.refl 1
State after:
no goals

State before:
case intro.intro.refine'_2
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    (fun l =>
          ∀ (a : R),
            (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
              Multiset.prod l = a → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a)
        s →
      (fun l =>
          ∀ (a : R),
            (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
              Multiset.prod l = a → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a)
        (a ::ₘ s)
Tactic:
simp only [Set.mem_setOf_eq, forall_apply_eq_imp_iff, Multiset.mem_cons, forall_eq_or_imp,
  Multiset.prod_cons, and_imp, forall_apply_eq_imp_iff₂]
State after:
case intro.intro.refine'_2
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    ((∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)) →
      IsUnit a ∨ Prime a →
        (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)

State before:
case intro.intro.refine'_2
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    ((∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)) →
      IsUnit a ∨ Prime a →
        (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)
Tactic:
intros a s hind ha hs
State after:
case intro.intro.refine'_2
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
ha : IsUnit a ∨ Prime a
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)

State before:
case intro.intro.refine'_2
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
ha : IsUnit a ∨ Prime a
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)
Tactic:
rcases ha with ha₁ | ha₂
State after:
case intro.intro.refine'_2.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₁ : IsUnit a
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)

case intro.intro.refine'_2.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₂ : Prime a
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)

State before:
case intro.intro.refine'_2.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₁ : IsUnit a
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)
Tactic:
rcases (hind hs) with ⟨f, hf, hf₂⟩
State after:
case intro.intro.refine'_2.inl.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₁ : IsUnit a
f : Multiset R
hf : ∀ b ∈ f, Prime b
hf₂ : Associated (Multiset.prod f) (Multiset.prod s)
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)

State before:
case intro.intro.refine'_2.inl.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₁ : IsUnit a
f : Multiset R
hf : ∀ b ∈ f, Prime b
hf₂ : Associated (Multiset.prod f) (Multiset.prod s)
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)
Tactic:
exact ⟨f, hf, (associated_isUnit_mul_right_iff ha₁).2 hf₂⟩
State after:
no goals

State before:
case intro.intro.refine'_2.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₂ : Prime a
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)
Tactic:
rcases (hind hs) with ⟨f, hf, hf₂⟩
State after:
case intro.intro.refine'_2.inr.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₂ : Prime a
f : Multiset R
hf : ∀ b ∈ f, Prime b
hf₂ : Associated (Multiset.prod f) (Multiset.prod s)
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)

State before:
case intro.intro.refine'_2.inr.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₂ : Prime a
f : Multiset R
hf : ∀ b ∈ f, Prime b
hf₂ : Associated (Multiset.prod f) (Multiset.prod s)
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)
Tactic:
refine' ⟨f.cons a, Multiset.forall_mem_cons.2 ⟨ha₂, hf⟩, _⟩
State after:
case intro.intro.refine'_2.inr.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₂ : Prime a
f : Multiset R
hf : ∀ b ∈ f, Prime b
hf₂ : Associated (Multiset.prod f) (Multiset.prod s)
⊢ Associated (Multiset.prod (a ::ₘ f)) (a * Multiset.prod s)

State before:
case intro.intro.refine'_2.inr.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₂ : Prime a
f : Multiset R
hf : ∀ b ∈ f, Prime b
hf₂ : Associated (Multiset.prod f) (Multiset.prod s)
⊢ Associated (Multiset.prod (a ::ₘ f)) (a * Multiset.prod s)
Tactic:
rw [Multiset.prod_cons]
State after:
case intro.intro.refine'_2.inr.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₂ : Prime a
f : Multiset R
hf : ∀ b ∈ f, Prime b
hf₂ : Associated (Multiset.prod f) (Multiset.prod s)
⊢ Associated (a * Multiset.prod f) (a * Multiset.prod s)

State before:
case intro.intro.refine'_2.inr.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₂ : Prime a
f : Multiset R
hf : ∀ b ∈ f, Prime b
hf₂ : Associated (Multiset.prod f) (Multiset.prod s)
⊢ Associated (a * Multiset.prod f) (a * Multiset.prod s)
Tactic:
exact Associated.mul_left a hf₂
State after:
no goals