awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
x : M
hx : Membership.mem (γ := Submodule R M) (torsionBySet R M s) x
rw : ∀ (hx : ∀ (a : (↑s : Type u_1)), (↑a : R) • x = 0) (a : (↑(↑(Ideal.span s) : Set R) : Type u_1)), (↑a : R) • x = 0
⊢ Membership.mem (γ := Submodule R M) (torsionBySet R M (↑(Ideal.span s) : Set R)) x

Tactic:
rw [mem_torsionBySet_iff] at hx ⊢

Premises used: Submodule.mem_torsionBySet_iff
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
x : M
hx : ∀ (a : (↑s : Type u_1)), (↑a : R) • x = 0
this : LE.le (α := Ideal R) (Ideal.span s) (Ideal.torsionOf R M x)
a : R
ha : a ∈ (↑(Ideal.span s) : Set R)
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑(Ideal.span s) : Set R)) a ha) : R) • x = 0

Tactic:
this ha

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
x : M
hx : ∀ (a : (↑s : Type u_1)), (↑a : R) • x = 0
this : LE.le (α := Ideal R) (Ideal.span s) (Ideal.torsionOf R M x)
a : R
ha : a ∈ (↑(Ideal.span s) : Set R)
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑(Ideal.span s) : Set R)) a ha) : R) • x = 0

Tactic:
exact this ha
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
x : M
hx : ∀ (a : (↑s : Type u_1)), (↑a : R) • x = 0
suffices : LE.le (α := Ideal R) (Ideal.span s) (Ideal.torsionOf R M x)
⊢ ∀ (a : (↑(↑(Ideal.span s) : Set R) : Type u_1)), (↑a : R) • x = 0

Tactic:
suffices Ideal.span s ≤ Ideal.torsionOf R M x by
    rintro ⟨a, ha⟩
    exact this ha
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
x : M
hx : ∀ (a : (↑s : Type u_1)), (↑a : R) • x = 0
rw : s ⊆ (↑(Ideal.torsionOf R M x) : Set R)
⊢ LE.le (α := Ideal R) (Ideal.span s) (Ideal.torsionOf R M x)

Tactic:
rw [Ideal.span_le]

Premises used: Ideal.span_le
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
x : M
hx : ∀ (a : (↑s : Type u_1)), (↑a : R) • x = 0
⊢ s ⊆ (↑(Ideal.torsionOf R M x) : Set R)

Tactic:
fun a ha => hx ⟨a, ha⟩

Premises used: Set.Mem, setOf, Set.Subset, Subtype.mk, Set.preimage, Set.singleton
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
x : M
hx : ∀ (a : (↑s : Type u_1)), (↑a : R) • x = 0
⊢ s ⊆ (↑(Ideal.torsionOf R M x) : Set R)

Tactic:
exact fun a ha => hx ⟨a, ha⟩

Premises used: Subtype.mk
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : R
⊢ Eq (α := Submodule R M) (torsionBySet R M (↑(R ∙ a) : Set R)) (torsionBy R M a)

Tactic:
(torsionBySet_eq_torsionBySet_span _).symm.trans <| torsionBySet_singleton_eq _

Premises used: Submodule.torsionBySet_singleton_eq, Submodule.torsionBySet_eq_torsionBySet_span, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : R
⊢ Eq (α := Submodule R M) (torsionBySet R M (↑(Ideal.span {a}) : Set R)) (torsionBy R M a)

Tactic:
torsionBySet_span_singleton_eq a

Premises used: Submodule.torsionBySet_span_singleton_eq
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : R
dvd : a ∣ b
rw : LE.le (α := Submodule R M) (torsionBySet R M (↑(R ∙ a) : Set R)) (torsionBySet R M {b})
⊢ LE.le (α := Submodule R M) (torsionBy R M a) (torsionBy R M b)

Tactic:
rw [← torsionBySet_span_singleton_eq, ← torsionBySet_singleton_eq]

Premises used: Submodule.torsionBySet_singleton_eq, Submodule.torsionBySet_span_singleton_eq
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : R
dvd : a ∣ b
st : {b} ⊆ (↑(R ∙ a) : Set R)
⊢ LE.le (α := Submodule R M) (torsionBySet R M (↑(R ∙ a) : Set R)) (torsionBySet R M {b})

Tactic:
apply torsionBySet_le_torsionBySet_of_subset

Premises used: Submodule.torsionBySet_le_torsionBySet_of_subset
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a c : R
dvd : a ∣ c
⊢ c ∈ (↑(R ∙ a) : Set R)

Tactic:
Ideal.mem_span_singleton.mpr dvd

Premises used: Iff.mpr, Set.Mem, Ideal.mem_span_singleton
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a c : R
dvd : a ∣ c
⊢ c ∈ (↑(R ∙ a) : Set R)

Tactic:
exact Ideal.mem_span_singleton.mpr dvd

Premises used: Iff.mpr, Ideal.mem_span_singleton
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
h : Membership.mem (γ := Submodule R M) (torsionBy R M 1) x
⊢ x = 0

Tactic:
rw [mem_torsionBy_iff, one_smul] at h

Premises used: one_smul, Submodule.mem_torsionBy_iff
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
h : x = 0
⊢ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
h

Premises used: Set.Mem, setOf, Set.singleton
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
h : x = 0
⊢ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
exact h
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw : LE.le (α := Submodule R M) (torsionBySet R M Set.univ) (torsionBySet R M {1})
⊢ Eq (α := Submodule R M) (torsionBySet R M Set.univ) ⊥

Tactic:
rw [eq_bot_iff, ← torsionBy_one, ← torsionBySet_singleton_eq]

Premises used: Submodule.torsionBySet_singleton_eq, Submodule.torsionBy_one, eq_bot_iff
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ LE.le (α := Submodule R M) (torsionBySet R M Set.univ) (torsionBySet R M {1})

Tactic:
torsionBySet_le_torsionBySet_of_subset fun _ _ => trivial

Premises used: trivial, Submodule.torsionBySet_le_torsionBySet_of_subset
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ LE.le (α := Submodule R M) (torsionBySet R M Set.univ) (torsionBySet R M {1})

Tactic:
exact torsionBySet_le_torsionBySet_of_subset fun _ _ => trivial

Premises used: trivial, Submodule.torsionBySet_le_torsionBySet_of_subset
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set R
h : s ⊆ t
ht : IsTorsionBySet R M t
⊢ IsTorsionBySet R M s

Tactic:
fun m r ↦ @ht m ⟨r, h r.2⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : R
⊢ IsTorsionBySet R M {a} ↔ IsTorsionBy R M a

Tactic:
⟨fun h x => @h _ ⟨_, Set.mem_singleton _⟩, fun h x => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : R
refine : ∀ (h : IsTorsionBy R M a) (x : M) ⦃a_1 : (↑{a} : Type u_1)⦄, (↑a_1 : R) • x = 0
⊢ IsTorsionBySet R M {a} ↔ IsTorsionBy R M a

Tactic:
refine ⟨fun h x => @h _ ⟨_, Set.mem_singleton _⟩, fun h x => ?_⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
b : R
h : IsTorsionBy R M b
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) {b} x) b ⋯) : R) • x = 0

Tactic:
@h _
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
b : R
h : IsTorsionBy R M b
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) {b} x) b ⋯) : R) • x = 0

Tactic:
exact @h _
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
⊢ IsTorsionBySet R M s ↔ IsTorsionBySet R M (↑(Ideal.span s) : Set R)

Tactic:
simpa only [isTorsionBySet_iff_subset_annihilator] using Ideal.span_le.symm

Premises used: Ideal.span_le, Module.isTorsionBySet_iff_subset_annihilator, Iff.symm
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : R
⊢ IsTorsionBySet R M (↑(R ∙ a) : Set R) ↔ IsTorsionBy R M a

Tactic:
(isTorsionBySet_iff_is_torsion_by_span _).symm.trans <| isTorsionBySet_singleton_iff _

Premises used: Module.isTorsionBySet_singleton_iff, Module.isTorsionBySet_iff_is_torsion_by_span, Iff.trans, Iff.symm
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
h : Eq (α := Submodule R M) (torsionBySet R M s) ⊤
x : M
rw : Membership.mem (γ := Submodule R M) ⊤ x
⊢ ∀ ⦃a : (↑s : Type u_1)⦄, (↑a : R) • x = 0

Tactic:
rw [← mem_torsionBySet_iff, h]

Premises used: Submodule.mem_torsionBySet_iff
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
h : Eq (α := Submodule R M) (torsionBySet R M s) ⊤
x : M
⊢ Membership.mem (γ := Submodule R M) ⊤ x

Tactic:
trivial
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : R
rw : IsTorsionBy R M a ↔ Eq (α := Submodule R M) (torsionBySet R M {a}) ⊤
rw₁ : IsTorsionBySet R M {a} ↔ Eq (α := Submodule R M) (torsionBySet R M {a}) ⊤
rw₂ rw₃ : Eq (α := Submodule R M) (torsionBySet R M {a}) ⊤ ↔ Eq (α := Submodule R M) (torsionBySet R M {a}) ⊤
⊢ IsTorsionBy R M a ↔ Eq (α := Submodule R M) (torsionBy R M a) ⊤

Tactic:
rw [← torsionBySet_singleton_eq, ← isTorsionBySet_singleton_iff,
    isTorsionBySet_iff_torsionBySet_eq_top]

Premises used: Submodule.torsionBySet_singleton_eq, Module.isTorsionBySet_iff_torsionBySet_eq_top, Module.isTorsionBySet_singleton_iff
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : R
⊢ IsTorsionBy R M a ↔ Membership.mem (γ := Submodule R R) (LinearMap.ker (M₂ := M →ₗ[R] M) (LinearMap.lsmul R M)) a

Tactic:
Iff.symm LinearMap.ext_iff

Premises used: LinearMap.ext_iff, Iff.symm
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
⊢ IsTorsionBySet.{u_1, u_2} R (↥(torsionBySet R M s)) s

Tactic:
fun ⟨_, hx⟩ a => Subtype.ext <| (mem_torsionBySet_iff _ _).mp hx a

Premises used: Submodule.mem_torsionBySet_iff, _private.0.Submodule.torsionBySet_isTorsionBySet.match_1, Iff.mp, HSMul.hSMul, OfNat.ofNat, Subtype.val, Eq, Subtype.ext
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : R
⊢ IsTorsionBy.{u_1, u_2} R (↥(torsionBy R M a)) a

Tactic:
smul_torsionBy a

Premises used: Submodule.smul_torsionBy
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
⊢ IsTorsion.{u_1, u_2} R ↥(torsionBy R M a)

Tactic:
(⟨⟨a, ha⟩, smul_torsionBy _ ·⟩)

Premises used: Subtype.mk, Exists.intro, Submodule.smul_torsionBy
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : NoZeroDivisors R
inst_4 : Nontrivial R
I : Ideal R
hbot : I ≠ ⊥
⊢ IsTorsion.{u_1, u_2} R ↥(torsionBySet R M (↑I : Set R))

Tactic:
aesop (add norm Submodule.eq_bot_iff)

Premises used: Submodule.eq_bot_iff
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : R
⊢ Eq.{u_2 + 1} (α := Submodule R ↥(torsionBy R M a)) (torsionBy R (↥(torsionBy R M a)) a) ⊤

Tactic:
(isTorsionBy_iff_torsionBy_eq_top a).mp <| torsionBy_isTorsionBy a

Premises used: Iff.mp, Submodule.torsionBy_isTorsionBy, Module.isTorsionBy_iff_torsionBy_eq_top
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
⊢ Eq.{u_2 + 1} (α := Submodule R ↥(torsionBySet R M s)) (torsionBySet R (↥(torsionBySet R M s)) s) ⊤

Tactic:
(isTorsionBySet_iff_torsionBySet_eq_top s).mp <| torsionBySet_isTorsionBySet s

Premises used: Module.isTorsionBySet_iff_torsionBySet_eq_top, Iff.mp, Submodule.torsionBySet_isTorsionBySet
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ GaloisConnection.{u_2, u_1} (α := Submodule R M) annihilator fun (I : (Ideal R)ᵒᵈ) ↦
    torsionBySet R M (↑((OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) I : Ideal R) : Set R)

Tactic:
fun _ _ =>
  ⟨fun h x hx => (mem_torsionBySet_iff _ _).mpr fun ⟨_, ha⟩ => mem_annihilator.mp (h ha) x hx,
    fun h a ha => mem_annihilator.mpr fun _ hx => (mem_torsionBySet_iff _ _).mp (h hx) ⟨a, ha⟩⟩

Premises used: Iff.mpr, OrderDual.ofDual, Submodule.mem_torsionBySet_iff, Submodule.mem_annihilator, Subtype.mk, _private.0.Submodule.torsion_gc.match_1, SetLike.coe, Iff.intro, Iff.mp, HSMul.hSMul, OfNat.ofNat, Subtype.val, Eq, DFunLike.coe, GaloisConnection
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
inl :
  ∀ (h : S = ∅),
    Eq (α := Submodule R M) (⨆ i ∈ S, torsionBySet R M (↑(p i) : Set R)) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R))
inr :
  ∀ (h : S.Nonempty),
    Eq (α := Submodule R M) (⨆ i ∈ S, torsionBySet R M (↑(p i) : Set R)) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R))
⊢ Eq (α := Submodule R M) (⨆ i ∈ S, torsionBySet R M (↑(p i) : Set R)) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R))

Tactic:
rcases S.eq_empty_or_nonempty with h | h

Premises used: Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
h : S = ∅
⊢ Eq (α := Submodule R M) (⨆ i ∈ S, torsionBySet R M (↑(p i) : Set R)) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R))

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
h : S.Nonempty
inr :
  LE.le (α := Submodule R M) (⨆ i ∈ S, torsionBySet R M (↑(p i) : Set R)) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R))
inr₁ :
  LE.le (α := Submodule R M) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R)) (⨆ i ∈ S, torsionBySet R M (↑(p i) : Set R))
⊢ Eq (α := Submodule R M) (⨆ i ∈ S, torsionBySet R M (↑(p i) : Set R)) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
h : S.Nonempty
apply :
  ∀ (i : ι),
    LE.le (α := Submodule R M) (⨆ (_ : i ∈ S), torsionBySet R M (↑(p i) : Set R))
      (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R))
⊢ LE.le (α := Submodule R M) (⨆ i ∈ S, torsionBySet R M (↑(p i) : Set R)) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R))

Tactic:
apply iSup_le _

Premises used: iSup_le
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
h : S.Nonempty
i : ι
apply :
  ∀ (i_1 : i ∈ S),
    LE.le (α := Submodule R M) (torsionBySet R M (↑(p i) : Set R)) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R))
⊢ LE.le (α := Submodule R M) (⨆ (_ : i ∈ S), torsionBySet R M (↑(p i) : Set R))
    (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R))

Tactic:
apply iSup_le _

Premises used: iSup_le
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
h : S.Nonempty
i : ι
is : i ∈ S
st : (↑(⨅ i ∈ S, p i) : Set R) ⊆ (↑(p i) : Set R)
⊢ LE.le (α := Submodule R M) (torsionBySet R M (↑(p i) : Set R)) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R))

Tactic:
apply torsionBySet_le_torsionBySet_of_subset

Premises used: Submodule.torsionBySet_le_torsionBySet_of_subset
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
h : S.Nonempty
i : ι
is : i ∈ S
⊢ (↑(⨅ i ∈ S, p i) : Set R) ⊆ (↑(p i) : Set R)

Tactic:
(iInf_le (fun i => ⨅ _ : i ∈ S, p i) i).trans (iInf_le _ is)

Premises used: iInf, Set.Mem, Set.Subset, LE.le.trans, iInf_le
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
h : S.Nonempty
i : ι
is : i ∈ S
⊢ (↑(⨅ i ∈ S, p i) : Set R) ⊆ (↑(p i) : Set R)

Tactic:
exact (iInf_le (fun i => ⨅ _ : i ∈ S, p i) i).trans (iInf_le _ is)

Premises used: iInf, LE.le.trans, iInf_le
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : Membership.mem (γ := Submodule R M) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R)) x
inr : ∃ (μ : (i : ι) → ↥(torsionBySet R M (↑(p i) : Set R))), ∑ i ∈ S, (↑(μ i) : M) = x
⊢ Membership.mem (γ := Submodule R M) (⨆ i ∈ S, torsionBySet R M (↑(p i) : Set R)) x

Tactic:
rw [mem_iSup_finset_iff_exists_sum]

Premises used: Submodule.mem_iSup_finset_iff_exists_sum
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : Membership.mem (γ := Submodule R M) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R)) x
inr :
  ∀ (μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)) (hμ : Eq.{u_1 + 1} (α := R) (∑ i ∈ S, (↑(μ i) : R)) 1),
    ∃ (μ : (i : ι) → ↥(torsionBySet R M (↑(p i) : Set R))), ∑ i ∈ S, (↑(μ i) : M) = x
⊢ ∃ (μ : (i : ι) → ↥(torsionBySet R M (↑(p i) : Set R))), ∑ i ∈ S, (↑(μ i) : M) = x

Tactic:
obtain ⟨μ, hμ⟩ :=
      (mem_iSup_finset_iff_exists_sum _ _).mp
        ((Ideal.eq_top_iff_one _).mp <| (Ideal.iSup_iInf_eq_top_iff_pairwise h _).mpr hp)

Premises used: Iff.mpr, Ideal.iSup_iInf_eq_top_iff_pairwise, Ideal.eq_top_iff_one, Submodule.mem_iSup_finset_iff_exists_sum, Iff.mp
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : Membership.mem (γ := Submodule R M) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R)) x
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : Eq.{u_1 + 1} (α := R) (∑ i ∈ S, (↑(μ i) : R)) 1
⊢ ∃ (μ : (i : ι) → ↥(torsionBySet R M (↑(p i) : Set R))), ∑ i ∈ S, (↑(μ i) : M) = x

Tactic:
⟨fun i => ⟨(μ i : R) • x, ?_⟩, ?_⟩

Premises used: Subtype.mk, Exists.intro, HSMul.hSMul, Subtype.val
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : Membership.mem (γ := Submodule R M) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R)) x
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : Eq.{u_1 + 1} (α := R) (∑ i ∈ S, (↑(μ i) : R)) 1
inr : ∀ (i : ι), Membership.mem (γ := Submodule R M) (torsionBySet R M (↑(p i) : Set R)) ((↑(μ i) : R) • x)
inr₁ :
  ∑ i ∈ S,
      (↑((fun (i : ι) ↦
              (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (torsionBySet R M (↑(p i) : Set R)) x)
                  ((↑(μ i) : R) • x) ⋯ :
                ↥(torsionBySet R M (↑(p i) : Set R))))
            i) :
        M) =
    x
⊢ ∃ (μ : (i : ι) → ↥(torsionBySet R M (↑(p i) : Set R))), ∑ i ∈ S, (↑(μ i) : M) = x

Tactic:
refine ⟨fun i => ⟨(μ i : R) • x, ?_⟩, ?_⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : Membership.mem (γ := Submodule R M) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R)) x
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : Eq.{u_1 + 1} (α := R) (∑ i ∈ S, (↑(μ i) : R)) 1
i : ι
inr :
  ∀ (hx : ∀ (a : (↑(↑(⨅ i ∈ S, p i) : Set R) : Type u_1)), (↑a : R) • x = 0)
    (μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)) (hμ : Eq.{u_1 + 1} (α := R) (∑ i ∈ S, (↑(μ i) : R)) 1) (i : ι)
    (a : (↑(↑(p i) : Set R) : Type u_1)), (↑a : R) • (↑(μ i) : R) • x = 0
⊢ Membership.mem (γ := Submodule R M) (torsionBySet R M (↑(p i) : Set R)) ((↑(μ i) : R) • x)

Tactic:
rw [mem_torsionBySet_iff] at hx ⊢

Premises used: Submodule.mem_torsionBySet_iff
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : (↑(↑(⨅ i ∈ S, p i) : Set R) : Type u_1)), (↑a : R) • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : Eq.{u_1 + 1} (α := R) (∑ i ∈ S, (↑(μ i) : R)) 1
i : ι
a : R
ha : a ∈ (↑(p i) : Set R)
inr : ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑(p i) : Set R)) a ha) : R) * (↑(μ i) : R)) • x = 0
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑(p i) : Set R)) a ha) : R) • (↑(μ i) : R) • x = 0

Tactic:
rw [smul_smul]

Premises used: smul_smul
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : (↑(↑(⨅ i ∈ S, p i) : Set R) : Type u_1)), (↑a : R) • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : Eq.{u_1 + 1} (α := R) (∑ i ∈ S, (↑(μ i) : R)) 1
i : ι
a : R
ha : a ∈ (↑(p i) : Set R)
inr : Membership.mem (γ := Ideal R) (⨅ i ∈ S, p i) (a * (↑(μ i) : R))
⊢ ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑(p i) : Set R)) a ha) : R) * (↑(μ i) : R)) • x = 0

Tactic:
suffices a * μ i ∈ ⨅ i ∈ S, p i from hx ⟨_, this⟩