case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ↑(annihilator ⊤) ∩ ↑R⁰ ≠ ∅
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ ↑(annihilator ⊤) ∩ ↑R⁰ ≠ ∅
obtain ⟨S, hS⟩ := ‹Module.Finite R M›.out
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ↑(∏ x in S, Exists.choose (_ : ∃ a, a • x = 0)) ∈ ↑(annihilator ⊤)
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ↑(annihilator ⊤) ∩ ↑R⁰ ≠ ∅
refine' Set.Nonempty.ne_empty ⟨_, _, (∏ x in S, (@hM x).choose : R⁰).prop⟩
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ∀ (n : ↑↑S), (∏ i in S, ↑(Exists.choose (_ : ∃ a, a • i = 0))) • ↑n = 0
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ↑(∏ x in S, Exists.choose (_ : ∃ a, a • x = 0)) ∈ ↑(annihilator ⊤)
rw [Submonoid.coe_finset_prod, SetLike.mem_coe, ← hS, mem_annihilator_span]
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
n : ↑↑S
⊢ (∏ i in S, ↑(Exists.choose (_ : ∃ a, a • i = 0))) • ↑n = 0
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ∀ (n : ↑↑S), (∏ i in S, ↑(Exists.choose (_ : ∃ a, a • i = 0))) • ↑n = 0
intro n
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
n : ↑↑S
this : DecidableEq M := Classical.decEq M
⊢ (∏ i in S, ↑(Exists.choose (_ : ∃ a, a • i = 0))) • ↑n = 0
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
n : ↑↑S
⊢ (∏ i in S, ↑(Exists.choose (_ : ∃ a, a • i = 0))) • ↑n = 0
letI := Classical.decEq M
no goals
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
n : ↑↑S
this : DecidableEq M := Classical.decEq M
⊢ (∏ i in S, ↑(Exists.choose (_ : ∃ a, a • i = 0))) • ↑n = 0
rw [← Finset.prod_erase_mul _ _ n.prop, mul_smul, ← Submonoid.smul_def, (@hM n).choose_spec,
  smul_zero]