Theorem: Ideal.IsPrime.mem_of_prod_mem (FormalisingMathematics2024/Solutions/Section14UFDsAndPIDsEtc/Sheet3.lean)

State before:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
⊢ Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
Tactic:
refine L.induction_on ?_ ?_
State after:
case refine_1
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
⊢ Multiset.prod 0 ∈ P → ∃ x ∈ 0, x ∈ P

case refine_2
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    (Multiset.prod s ∈ P → ∃ x ∈ s, x ∈ P) → Multiset.prod (a ::ₘ s) ∈ P → ∃ x ∈ a ::ₘ s, x ∈ P

State before:
case refine_1
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
⊢ Multiset.prod 0 ∈ P → ∃ x ∈ 0, x ∈ P
Tactic:
intro h
State after:
case refine_1
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
h : Multiset.prod 0 ∈ P
⊢ ∃ x ∈ 0, x ∈ P

State before:
case refine_1
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
h : Multiset.prod 0 ∈ P
⊢ ∃ x ∈ 0, x ∈ P
Tactic:
rw [Multiset.prod_zero] at h
State after:
case refine_1
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
h : 1 ∈ P
⊢ ∃ x ∈ 0, x ∈ P

State before:
case refine_1
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
h : 1 ∈ P
⊢ ∃ x ∈ 0, x ∈ P
Tactic:
cases hP.not_one_mem h
State after:
no goals

State before:
case refine_2
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    (Multiset.prod s ∈ P → ∃ x ∈ s, x ∈ P) → Multiset.prod (a ::ₘ s) ∈ P → ∃ x ∈ a ::ₘ s, x ∈ P
Tactic:
intro a L IH h
State after:
case refine_2
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : Multiset.prod (a ::ₘ L) ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P

State before:
case refine_2
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : Multiset.prod (a ::ₘ L) ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P
Tactic:
simp only [Multiset.prod_cons] at h
State after:
case refine_2
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P

State before:
case refine_2
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P
Tactic:
rcases hP.mem_or_mem h with (ha | hL)
State after:
case refine_2.inl
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
ha : a ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P

case refine_2.inr
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
hL : Multiset.prod L ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P

State before:
case refine_2.inl
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
ha : a ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P
Tactic:
exact ⟨a, by simp, ha⟩
State after:
no goals

State before:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
ha : a ∈ P
⊢ a ∈ a ::ₘ L
Tactic:
simp
State after:
no goals

State before:
case refine_2.inr
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
hL : Multiset.prod L ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P
Tactic:
obtain ⟨x, hxL, hxP⟩ := IH hL
State after:
case refine_2.inr.intro.intro
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
hL : Multiset.prod L ∈ P
x : R
hxL : x ∈ L
hxP : x ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P

State before:
case refine_2.inr.intro.intro
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
hL : Multiset.prod L ∈ P
x : R
hxL : x ∈ L
hxP : x ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P
Tactic:
exact ⟨x, Multiset.mem_cons_of_mem hxL, hxP⟩
State after:
no goals