Theorem: Submonoid.closure_mem_of_prod_mem (Kaplanski4/Kaplanski.lean)

State before:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
⊢ ∀ (x y : R), x * y ∈ closure {r | IsUnit r ∨ Prime r} → x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
intros a b hab
State after:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
a b : R
hab : a * b ∈ closure {r | IsUnit r ∨ Prime r}
⊢ a ∈ closure {r | IsUnit r ∨ Prime r}

State before:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
a b : R
hab : a * b ∈ closure {r | IsUnit r ∨ Prime r}
⊢ a ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
obtain ⟨m, hm⟩ := exists_multiset_of_mem_closure hab
State after:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
a b : R
hab : a * b ∈ closure {r | IsUnit r ∨ Prime r}
m : Multiset R
hm : ∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b
⊢ a ∈ closure {r | IsUnit r ∨ Prime r}

State before:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
a b : R
hab : a * b ∈ closure {r | IsUnit r ∨ Prime r}
m : Multiset R
hm : ∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b
⊢ a ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
revert a b hm
State after:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
⊢ ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b) → a ∈ closure {r | IsUnit r ∨ Prime r}

State before:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
⊢ ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b) → a ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
refine m.induction (p := fun m ↦ ∀ a b, a * b ∈ closure {r | IsUnit r ∨ Prime r} →
  (∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), m.prod = a * b) →
  a ∈ closure {r | IsUnit r ∨ Prime r}) (fun _ _ _ hprod => subset_closure (Set.mem_def.2 ?_)) ?_
State after:
case intro.refine_1
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
x✝² x✝¹ : R
x✝ : x✝² * x✝¹ ∈ closure {r | IsUnit r ∨ Prime r}
hprod : ∃ (_ : ∀ y ∈ 0, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod 0 = x✝² * x✝¹
⊢ {r | IsUnit r ∨ Prime r} x✝²

case intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    (fun m =>
          ∀ (a b : R),
            a * b ∈ closure {r | IsUnit r ∨ Prime r} →
              (∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b) →
                a ∈ closure {r | IsUnit r ∨ Prime r})
        s →
      (fun m =>
          ∀ (a b : R),
            a * b ∈ closure {r | IsUnit r ∨ Prime r} →
              (∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b) →
                a ∈ closure {r | IsUnit r ∨ Prime r})
        (a ::ₘ s)

State before:
case intro.refine_1
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
x✝² x✝¹ : R
x✝ : x✝² * x✝¹ ∈ closure {r | IsUnit r ∨ Prime r}
hprod : ∃ (_ : ∀ y ∈ 0, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod 0 = x✝² * x✝¹
⊢ {r | IsUnit r ∨ Prime r} x✝²
Tactic:
left
State after:
case intro.refine_1.h
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
x✝² x✝¹ : R
x✝ : x✝² * x✝¹ ∈ closure {r | IsUnit r ∨ Prime r}
hprod : ∃ (_ : ∀ y ∈ 0, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod 0 = x✝² * x✝¹
⊢ IsUnit x✝²

State before:
case intro.refine_1.h
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
x✝² x✝¹ : R
x✝ : x✝² * x✝¹ ∈ closure {r | IsUnit r ∨ Prime r}
hprod : ∃ (_ : ∀ y ∈ 0, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod 0 = x✝² * x✝¹
⊢ IsUnit x✝²
Tactic:
exact isUnit_of_mul_eq_one _ _ hprod.2.symm
State after:
no goals

State before:
case intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    (fun m =>
          ∀ (a b : R),
            a * b ∈ closure {r | IsUnit r ∨ Prime r} →
              (∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b) →
                a ∈ closure {r | IsUnit r ∨ Prime r})
        s →
      (fun m =>
          ∀ (a b : R),
            a * b ∈ closure {r | IsUnit r ∨ Prime r} →
              (∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b) →
                a ∈ closure {r | IsUnit r ∨ Prime r})
        (a ::ₘ s)
Tactic:
simp only [exists_prop, and_imp, Multiset.prod_cons, Multiset.mem_cons, forall_eq_or_imp]
State after:
case intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    (∀ (a b : R),
        a * b ∈ closure {r | IsUnit r ∨ Prime r} →
          (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}) →
      ∀ (a_2 b : R),
        a_2 * b ∈ closure {r | IsUnit r ∨ Prime r} →
          a ∈ {r | IsUnit r ∨ Prime r} →
            (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) →
              a * Multiset.prod s = a_2 * b → a_2 ∈ closure {r | IsUnit r ∨ Prime r}

State before:
case intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    (∀ (a b : R),
        a * b ∈ closure {r | IsUnit r ∨ Prime r} →
          (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}) →
      ∀ (a_2 b : R),
        a_2 * b ∈ closure {r | IsUnit r ∨ Prime r} →
          a ∈ {r | IsUnit r ∨ Prime r} →
            (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) →
              a * Multiset.prod s = a_2 * b → a_2 ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
intros _ s hind x y _ ha hs hprod
State after:
case intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
ha : a✝¹ ∈ {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

State before:
case intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
ha : a✝¹ ∈ {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
rcases ha with ha₁ | ha₂
State after:
case intro.refine_2.inl
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

State before:
case intro.refine_2.inl
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
rcases ha₁.exists_right_inv with ⟨k, hk⟩
State after:
case intro.refine_2.inl.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

State before:
case intro.refine_2.inl.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
refine hind x (y*k) ?_ hs ?_
State after:
case intro.refine_2.inl.intro.refine_1
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ x * (y * k) ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inl.intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ Multiset.prod s = x * (y * k)

State before:
case intro.refine_2.inl.intro.refine_1
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ x * (y * k) ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inl.intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ Multiset.prod s = x * (y * k)
Tactic:
simp only [← mul_assoc, ← hprod, ← Multiset.prod_cons, mul_comm]
State after:
case intro.refine_2.inl.intro.refine_1
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ Multiset.prod (k ::ₘ a✝¹ ::ₘ s) ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inl.intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ Multiset.prod s = x * (y * k)

State before:
case intro.refine_2.inl.intro.refine_1
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ Multiset.prod (k ::ₘ a✝¹ ::ₘ s) ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inl.intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ Multiset.prod s = x * (y * k)
Tactic:
refine multiset_prod_mem _ _ (Multiset.forall_mem_cons.2 ⟨subset_closure (Set.mem_def.2 ?_),
  Multiset.forall_mem_cons.2 ⟨subset_closure (Set.mem_def.2 ?_), (fun t ht =>
  subset_closure (hs t ht))⟩⟩)
State after:
case intro.refine_2.inl.intro.refine_1.refine_1
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ {r | IsUnit r ∨ Prime r} k

case intro.refine_2.inl.intro.refine_1.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ {r | IsUnit r ∨ Prime r} a✝¹

case intro.refine_2.inl.intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ Multiset.prod s = x * (y * k)

State before:
case intro.refine_2.inl.intro.refine_1.refine_1
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ {r | IsUnit r ∨ Prime r} k

case intro.refine_2.inl.intro.refine_1.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ {r | IsUnit r ∨ Prime r} a✝¹

case intro.refine_2.inl.intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ Multiset.prod s = x * (y * k)
Tactic:
left
State after:
case intro.refine_2.inl.intro.refine_1.refine_1.h
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ IsUnit k

case intro.refine_2.inl.intro.refine_1.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ {r | IsUnit r ∨ Prime r} a✝¹

case intro.refine_2.inl.intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ Multiset.prod s = x * (y * k)

State before:
case intro.refine_2.inl.intro.refine_1.refine_1.h
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ IsUnit k

case intro.refine_2.inl.intro.refine_1.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ {r | IsUnit r ∨ Prime r} a✝¹

case intro.refine_2.inl.intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ Multiset.prod s = x * (y * k)
Tactic:
exact isUnit_of_mul_eq_one_right _ _ hk
State after:
case intro.refine_2.inl.intro.refine_1.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ {r | IsUnit r ∨ Prime r} a✝¹

case intro.refine_2.inl.intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ Multiset.prod s = x * (y * k)

State before:
case intro.refine_2.inl.intro.refine_1.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ {r | IsUnit r ∨ Prime r} a✝¹

case intro.refine_2.inl.intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ Multiset.prod s = x * (y * k)
Tactic:
left
State after:
case intro.refine_2.inl.intro.refine_1.refine_2.h
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ IsUnit a✝¹

case intro.refine_2.inl.intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ Multiset.prod s = x * (y * k)

State before:
case intro.refine_2.inl.intro.refine_1.refine_2.h
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ IsUnit a✝¹

case intro.refine_2.inl.intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ Multiset.prod s = x * (y * k)
Tactic:
exact ha₁
State after:
case intro.refine_2.inl.intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ Multiset.prod s = x * (y * k)

State before:
case intro.refine_2.inl.intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ Multiset.prod s = x * (y * k)
Tactic:
rw [← mul_one s.prod, ← hk, ← mul_assoc, ← mul_assoc, mul_eq_mul_right_iff, mul_comm]
State after:
case intro.refine_2.inl.intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ a✝¹ * Multiset.prod s = x * y ∨ k = 0

State before:
case intro.refine_2.inl.intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ a✝¹ * Multiset.prod s = x * y ∨ k = 0
Tactic:
left
State after:
case intro.refine_2.inl.intro.refine_2.h
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ a✝¹ * Multiset.prod s = x * y

State before:
case intro.refine_2.inl.intro.refine_2.h
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ a✝¹ * Multiset.prod s = x * y
Tactic:
exact hprod
State after:
no goals

State before:
case intro.refine_2.inr
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
rcases ha₂.dvd_mul.1 (Dvd.intro _ hprod) with ⟨c, hc⟩ | ⟨c, hc⟩
State after:
case intro.refine_2.inr.inl.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : x = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

State before:
case intro.refine_2.inr.inl.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : x = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
rw [hc]
State after:
case intro.refine_2.inr.inl.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : x = a✝¹ * c
⊢ a✝¹ * c ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

State before:
case intro.refine_2.inr.inl.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : x = a✝¹ * c
⊢ a✝¹ * c ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
rw [hc, mul_assoc] at hprod
State after:
case intro.refine_2.inr.inl.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ a✝¹ * c ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

State before:
case intro.refine_2.inr.inl.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ a✝¹ * c ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
refine' Submonoid.mul_mem _ (subset_closure (Set.mem_def.2 _))
  (hind _ _ _ hs (mul_left_cancel₀ ha₂.ne_zero hprod))
State after:
case intro.refine_2.inr.inl.intro.refine'_1
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ {r | IsUnit r ∨ Prime r} a✝¹

case intro.refine_2.inr.inl.intro.refine'_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ c * y ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

State before:
case intro.refine_2.inr.inl.intro.refine'_1
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ {r | IsUnit r ∨ Prime r} a✝¹

case intro.refine_2.inr.inl.intro.refine'_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ c * y ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
right
State after:
case intro.refine_2.inr.inl.intro.refine'_1.h
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ Prime a✝¹

case intro.refine_2.inr.inl.intro.refine'_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ c * y ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

State before:
case intro.refine_2.inr.inl.intro.refine'_1.h
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ Prime a✝¹

case intro.refine_2.inr.inl.intro.refine'_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ c * y ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
exact ha₂
State after:
case intro.refine_2.inr.inl.intro.refine'_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ c * y ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

State before:
case intro.refine_2.inr.inl.intro.refine'_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ c * y ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
rw [← mul_left_cancel₀ ha₂.ne_zero hprod]
State after:
case intro.refine_2.inr.inl.intro.refine'_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ Multiset.prod s ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

State before:
case intro.refine_2.inr.inl.intro.refine'_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ Multiset.prod s ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
exact multiset_prod_mem _ _ (fun t ht => subset_closure (hs t ht))
State after:
case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

State before:
case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
rw [hc, mul_comm x _, mul_assoc, mul_comm c _] at hprod
State after:
case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (x * c)
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

State before:
case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (x * c)
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
refine' hind x c _ hs (mul_left_cancel₀ ha₂.ne_zero hprod)
State after:
case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (x * c)
hc : y = a✝¹ * c
⊢ x * c ∈ closure {r | IsUnit r ∨ Prime r}

State before:
case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (x * c)
hc : y = a✝¹ * c
⊢ x * c ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
rw [← mul_left_cancel₀ ha₂.ne_zero hprod]
State after:
case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (x * c)
hc : y = a✝¹ * c
⊢ Multiset.prod s ∈ closure {r | IsUnit r ∨ Prime r}

State before:
case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (x * c)
hc : y = a✝¹ * c
⊢ Multiset.prod s ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
exact multiset_prod_mem _ _ (fun t ht => subset_closure (hs t ht))
State after:
no goals