case intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
s : Submonoid R
a : R
ha : a ≠ 0
hfac : ∀ (b : R), b ∈ factors a → b ∈ s
hunit : ∀ (c : Rˣ), ↑c ∈ s
c : Rˣ
hc : Multiset.prod (factors a) * ↑c = a
⊢ a ∈ s
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
s : Submonoid R
a : R
ha : a ≠ 0
hfac : ∀ (b : R), b ∈ factors a → b ∈ s
hunit : ∀ (c : Rˣ), ↑c ∈ s
⊢ a ∈ s
rcases(factors_spec a ha).2 with ⟨c, hc⟩
case intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
s : Submonoid R
a : R
ha : a ≠ 0
hfac : ∀ (b : R), b ∈ factors a → b ∈ s
hunit : ∀ (c : Rˣ), ↑c ∈ s
c : Rˣ
hc : Multiset.prod (factors a) * ↑c = a
⊢ Multiset.prod (factors a) * ↑c ∈ s
case intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
s : Submonoid R
a : R
ha : a ≠ 0
hfac : ∀ (b : R), b ∈ factors a → b ∈ s
hunit : ∀ (c : Rˣ), ↑c ∈ s
c : Rˣ
hc : Multiset.prod (factors a) * ↑c = a
⊢ a ∈ s
rw [← hc]
no goals
case intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
s : Submonoid R
a : R
ha : a ≠ 0
hfac : ∀ (b : R), b ∈ factors a → b ∈ s
hunit : ∀ (c : Rˣ), ↑c ∈ s
c : Rˣ
hc : Multiset.prod (factors a) * ↑c = a
⊢ Multiset.prod (factors a) * ↑c ∈ s
exact mul_mem (multiset_prod_mem _ hfac) (hunit _)