awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : DecidableEq ι
S : Finset ι
p : ι → Ideal R
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
hM : IsTorsionBySet R M (↑(⨅ i ∈ S, p i) : Set R)
apply : Eq.{u_2 + 1} (α := Submodule R M) (⨆ t ∈ (↑S : Set ι), torsionBySet R M (↑(p t) : Set R)) ⊤
⊢ Eq.{u_2 + 1} (α := Submodule R M) (⨆ (i : ↥S), torsionBySet R M (↑(p (↑i : ι)) : Set R)) ⊤

Tactic:
apply (iSup_subtype'' ↑S fun i => torsionBySet R M <| p i).trans

Premises used: iSup_subtype'', SetLike.coe, Submodule.torsionBySet, Eq.trans
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : DecidableEq ι
S : Finset ι
p : ι → Ideal R
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
hM : IsTorsionBySet R M (↑(⨅ i ∈ S, p i) : Set R)
⊢ Eq.{u_2 + 1} (α := Submodule R M) (⨆ t ∈ (↑S : Set ι), torsionBySet R M (↑(p t) : Set R)) ⊤

Tactic:
apply (iSup_torsionBySet_ideal_eq_torsionBySet_iInf hp).trans <|
        (Module.isTorsionBySet_iff_torsionBySet_eq_top _).mp hM

Premises used: Module.isTorsionBySet_iff_torsionBySet_eq_top, Iff.mp, Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf, Eq.trans
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : DecidableEq ι
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
hM : IsTorsionBy R M (∏ i ∈ S, q i)
⊢ IsTorsionBySet R M (↑(⨅ a ∈ S, Ideal.span {q a}) : Set R)

Tactic:
rw [← Module.isTorsionBySet_span_singleton_iff, Ideal.submodule_span_eq, ←
    Ideal.finset_inf_span_singleton _ _ hq, Finset.inf_eq_iInf] at hM

Premises used: Ideal.submodule_span_eq, Module.isTorsionBySet_span_singleton_iff, Ideal.finset_inf_span_singleton, Finset.inf_eq_iInf
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : DecidableEq ι
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
hM : IsTorsionBySet R M (↑(⨅ a ∈ S, Ideal.span {q a}) : Set R)
⊢ DirectSum.IsInternal (S := Submodule R M) fun (i : ↥S) ↦ torsionBySet R M (↑(Ideal.span {q (↑i : ι)}) : Set R)

Tactic:
torsionBySet_isInternal
      (fun i hi j hj ij => (Ideal.sup_eq_top_iff_isCoprime (q i) _).mpr <| hq hi hj ij) hM

Premises used: Iff.mpr, Ideal.sup_eq_top_iff_isCoprime, Submodule.torsionBySet_isInternal
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : DecidableEq ι
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
hM : IsTorsionBySet R M (↑(⨅ a ∈ S, Ideal.span {q a}) : Set R)
h :
  ∀ (x : ↥S),
    Eq (α := Submodule R M) (torsionBy R M (q (↑x : ι))) (torsionBySet R M (↑(Ideal.span {q (↑x : ι)}) : Set R))
⊢ DirectSum.IsInternal (S := Submodule R M) fun (i : ↥S) ↦ torsionBy R M (q (↑i : ι))

Tactic:
convert!
    torsionBySet_isInternal
      (fun i hi j hj ij => (Ideal.sup_eq_top_iff_isCoprime (q i) _).mpr <| hq hi hj ij) hM

Premises used: Iff.mpr, Ideal.sup_eq_top_iff_isCoprime, Submodule.torsionBySet_isInternal
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : DecidableEq ι
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
hM : IsTorsionBySet R M (↑(⨅ a ∈ S, Ideal.span {q a}) : Set R)
x : ↥S
⊢ Eq (α := Submodule R M) (torsionBy R M (q (↑x : ι))) (torsionBySet R M (↑(Ideal.span {q (↑x : ι)}) : Set R))

Tactic:
(torsionBySet_span_singleton_eq _ (R := R) (M := M)).symm

Premises used: Submodule.torsionBySet_span_singleton_eq, Eq.symm
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : DecidableEq ι
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
hM : IsTorsionBySet R M (↑(⨅ a ∈ S, Ideal.span {q a}) : Set R)
x : ↥S
⊢ Eq (α := Submodule R M) (torsionBy R M (q (↑x : ι))) (torsionBySet R M (↑(Ideal.span {q (↑x : ι)}) : Set R))

Tactic:
exact (torsionBySet_span_singleton_eq _ (R := R) (M := M)).symm

Premises used: Submodule.torsionBySet_span_singleton_eq, Eq.symm
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
r : R
hM : IsTorsionBySet R M (↑I : Set R)
b : R ⧸ I
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hM : (↑I : Set R) ⊆ (↑(annihilator R M) : Set R)) (b : R ⧸ I),
    LE.le.{u_1} (α := AddSubgroup R) (Submodule.toAddSubgroup I) (AddMonoidHom.ker (M := M →+ M) (smulAddHom R M))
⊢ LE.le.{u_1} (α := AddSubgroup R) (Submodule.toAddSubgroup I) (AddMonoidHom.ker (M := M →+ M) (smulAddHom R M))

Tactic:
rwa [isTorsionBySet_iff_subset_annihilator] at hM

Premises used: Module.isTorsionBySet_iff_subset_annihilator
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
r : R
hM : IsTorsionBy R M r
rwa rwa₁ rwa₂ rwa₃ : ∀ (hM : IsTorsionBySet R M (↑(R ∙ r) : Set R)), IsTorsionBySet R M (↑(Ideal.span {r}) : Set R)
⊢ IsTorsionBySet R M (↑(Ideal.span {r}) : Set R)

Tactic:
rwa [← isTorsionBySet_span_singleton_iff r] at hM

Premises used: Module.isTorsionBySet_span_singleton_iff
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
r : R
hM : IsTorsionBy R M r
rwa rwa₁ rwa₂ rwa₃ : ∀ (hM : IsTorsionBySet R M (↑(R ∙ r) : Set R)), IsTorsionBySet R M (↑(Ideal.span {r}) : Set R)
⊢ IsTorsionBySet R M (↑(Ideal.span {r}) : Set R)

Tactic:
finally
  rwa [← isTorsionBySet_span_singleton_iff r] at hM
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : I.IsTwoSided
hM : IsTorsionBySet R M (↑I : Set R)
b : R
x : M
⊢ HSMul.hSMul (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) b : R ⧸ I) x = b • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
inst_3 : Ideal.IsTwoSided (α := R) (Ideal.span {r})
hM : IsTorsionBy R M r
b : R
x : M
⊢ HSMul.hSMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
      ((Ideal.Quotient.mk (Ideal.span {r}) : (a : R) → R ⧸ Ideal.span {r}) b :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
      x =
    b • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
r : R
inst_3 : I.IsTwoSided
hM : IsTorsionBySet R M (↑I : Set R)
S : Type u_3
inst_4 : SMul S R
inst_5 : SMul S M
inst_6 : IsScalarTower S R M
inst_7 : IsScalarTower S R R
⊢ IsScalarTower.{u_3, u_1, u_2} S (R ⧸ I) M

Tactic:
@IsScalarTower.mk S (R ⧸ I) M _ hM.hasSMul _
    (fun b d x => Quotient.inductionOn' d fun c => (smul_assoc b c x :))

Premises used: Quotient.inductionOn', IsScalarTower.mk
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : I.IsTwoSided
hM : IsTorsionBySet R M (↑I : Set R)
⊢ IsSemisimpleModule.{u_1, u_2} (R ⧸ I) M ↔ IsSemisimpleModule R M

Tactic:
letI := hM.module
  (hM.semilinearMap.isSemisimpleModule_iff_of_bijective Function.bijective_id).symm

Premises used: Function.bijective_id, Module.IsTorsionBySet.semilinearMap, LinearMap.isSemisimpleModule_iff_of_bijective, Iff.symm
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
r : R
h : Ideal.IsTwoSided (α := R) (Ideal.span {r})
hM : IsTorsionBy R M r
rwa rwa₁ rwa₂ rwa₃ : ∀ (hM : IsTorsionBySet R M (↑(R ∙ r) : Set R)), IsTorsionBySet R M (↑(Ideal.span {r}) : Set R)
⊢ IsTorsionBySet R M (↑(Ideal.span {r}) : Set R)

Tactic:
rwa [← isTorsionBySet_span_singleton_iff] at hM

Premises used: Module.isTorsionBySet_span_singleton_iff
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
r : R
h : Ideal.IsTwoSided (α := R) (Ideal.span {r})
hM : IsTorsionBy R M r
rwa rwa₁ rwa₂ rwa₃ : ∀ (hM : IsTorsionBySet R M (↑(R ∙ r) : Set R)), IsTorsionBySet R M (↑(Ideal.span {r}) : Set R)
⊢ IsTorsionBySet R M (↑(Ideal.span {r}) : Set R)

Tactic:
finally
  rwa [← isTorsionBySet_span_singleton_iff] at hM
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
r : R
⊢ IsTorsionBy.{u_1, u_2} R (M ⧸ N) r ↔ ∀ (x : M), r • x ∈ N

Tactic:
Iff.trans N.mkQ_surjective.forall <| forall_congr' fun _ =>
    Submodule.Quotient.mk_eq_zero N

Premises used: Function.Surjective.forall, forall_congr', Iff.trans, Submodule.mkQ_surjective, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
r : R
h : IsTorsionBy R M r
⊢ IsTorsionBy.{u_1, u_2} R (M ⧸ N) r

Tactic:
(isTorsionBy_quotient_iff N r).mpr fun x => @h x ▸ N.zero_mem

Premises used: Iff.mpr, Eq.rec, Submodule.zero_mem, Module.isTorsionBy_quotient_iff, Eq.symm
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
s : Set R
⊢ IsTorsionBySet.{u_1, u_2} R (M ⧸ N) s ↔ ∀ (x : M), ∀ r ∈ s, r • x ∈ N

Tactic:
Iff.trans N.mkQ_surjective.forall <| forall_congr' fun _ =>
    Iff.trans Subtype.forall <| forall₂_congr fun _ _ =>
      Submodule.Quotient.mk_eq_zero N

Premises used: Function.Surjective.forall, Subtype.forall, forall₂_congr, forall_congr', Iff.trans, Submodule.mkQ_surjective, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
s : Set R
h : IsTorsionBySet R M s
⊢ IsTorsionBySet.{u_1, u_2} R (M ⧸ N) s

Tactic:
(isTorsionBySet_quotient_iff N s).mpr fun x r h' => @h x ⟨r, h'⟩ ▸ N.zero_mem

Premises used: Iff.mpr, Eq.rec, Submodule.zero_mem, Module.isTorsionBySet_quotient_iff, Eq.symm
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set R
⊢ IsTorsionBySet.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) s ⊤) s

Tactic:
(isTorsionBySet_quotient_iff _ _).mpr fun _ _ h =>
    mem_set_smul_of_mem_mem h mem_top

Premises used: Iff.mpr, Submodule.mem_set_smul_of_mem_mem, Module.isTorsionBySet_quotient_iff, Submodule.mem_top
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
⊢ IsTorsionBySet.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤) (↑I : Set R)

Tactic:
(isTorsionBySet_quotient_iff _ _).mpr fun _ _ h => smul_mem_smul h ⟨⟩

Premises used: Iff.mpr, Module.isTorsionBySet_quotient_iff, Submodule.smul_mem_smul, True.intro
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : I.IsTwoSided
r : R
m : M
⊢ HSMul.hSMul (α := R ⧸ I) (β := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
      ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) r : R ⧸ I) (Submodule.Quotient.mk m) =
    Submodule.Quotient.mk (r • m)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Quot.map, Quotient.map', rfl
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
⊢ IsTorsionBy.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) r ⊤) r

Tactic:
(isTorsionBy_quotient_iff _ _).mpr (Submodule.smul_mem_pointwise_smul · r ⊤ ⟨⟩)

Premises used: Iff.mpr, Submodule.smul_mem_pointwise_smul, Module.isTorsionBy_quotient_iff, Top.top, True.intro
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
b : R
x : ↥(torsionBySet R M (↑I : Set R))
⊢ HSMul.hSMul (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) b : R ⧸ I) x = b • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : SMul S R
inst_4 : SMul S M
inst_5 : IsScalarTower S R M
inst_6 : IsScalarTower S R R
⊢ IsScalarTower.{u_3, u_1, u_2} S (R ⧸ I) ↥(torsionBySet R M (↑I : Set R))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
a b : R
x : ↥(torsionBy R M a)
⊢ HSMul.hSMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {a}))
      ((Ideal.Quotient.mk (Ideal.span {a}) : (a_1 : R) → R ⧸ Ideal.span {a}) b :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.span {a}))
      x =
    b • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
a b : R
x : ↥(torsionBy R M a)
⊢ HSMul.hSMul (α := HasQuotient.Quotient R (B := Ideal R) (R ∙ a))
      ((Ideal.Quotient.mk (R ∙ a) : (a_1 : R) → R ⧸ R ∙ a) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a)) x =
    b • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
a : R
S : Type u_3
inst_3 : SMul S R
inst_4 : SMul S M
inst_5 : IsScalarTower S R M
inst_6 : IsScalarTower S R R
⊢ IsScalarTower.{u_3, u_1, u_2} S (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
a : R
p : Submodule R ↥(torsionBy R M a)
c : HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)
b : R
x : ↥(torsionBy R M a)
⊢ x ∈ (↑p : Set ↥(torsionBy R M a)) →
    HSMul.hSMul (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a))
        (Quot.mk (⇑(R ∙ a).quotientRel : R → R → Prop) b) x ∈
      (↑p : Set ↥(torsionBy R M a))

Tactic:
p.smul_mem b

Premises used: Set.Mem, Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
a : R
p : Submodule R ↥(torsionBy R M a)
c : HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)
b : R
⊢ ∀ {x : ↥(torsionBy R M a)},
    x ∈ (↑p : Set ↥(torsionBy R M a)) →
      HSMul.hSMul (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a))
          (Quot.mk (⇑(R ∙ a).quotientRel : R → R → Prop) b) x ∈
        (↑p : Set ↥(torsionBy R M a))

Tactic:
exact p.smul_mem b

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
a : R
x : Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a)
h :
  ∀ (x_1 : ↥(torsionBy R M a)),
    Membership.mem (γ := Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a))
        ((fun (p : Submodule R ↥(torsionBy R M a)) ↦
            { carrier := (↑p : Set ↥(torsionBy R M a)), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ :
              Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a) })
          (Function.Embedding.toFun
            (RelEmbedding.toEmbedding (r :=
              fun
                (x1 x2 :
                  Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a)) ↦
              x1 ≤ x2) (s := fun (x1 x2 : Submodule R ↥(torsionBy R M a)) ↦ x1 ≤ x2)
              (restrictScalarsEmbedding R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a)))
            x))
        x_1 ↔
      x_1 ∈ x
⊢ (fun (p : Submodule R ↥(torsionBy R M a)) ↦
        { carrier := (↑p : Set ↥(torsionBy R M a)), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ :
          Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a) })
      (Function.Embedding.toFun
        (RelEmbedding.toEmbedding (r :=
          fun (x1 x2 : Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a)) ↦
          x1 ≤ x2) (s := fun (x1 x2 : Submodule R ↥(torsionBy R M a)) ↦ x1 ≤ x2)
          (restrictScalarsEmbedding R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a)))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
a : R
x : Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a)
x_1 : ↥(torsionBy R M a)
⊢ Membership.mem (γ := Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a))
      ((fun (p : Submodule R ↥(torsionBy R M a)) ↦
          { carrier := (↑p : Set ↥(torsionBy R M a)), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ :
            Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a) })
        (Function.Embedding.toFun
          (RelEmbedding.toEmbedding (r :=
            fun
              (x1 x2 : Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a)) ↦
            x1 ≤ x2) (s := fun (x1 x2 : Submodule R ↥(torsionBy R M a)) ↦ x1 ≤ x2)
            (restrictScalarsEmbedding R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a)))
          x))
      x_1 ↔
    x_1 ∈ x

Tactic:
simp [restrictScalarsEmbedding]

Premises used: Submodule.restrictScalarsEmbedding
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
a : R
x : Submodule R ↥(torsionBy R M a)
h :
  ∀ (x_1 : ↥(torsionBy R M a)),
    Membership.mem (γ := Submodule R ↥(torsionBy R M a))
        (Function.Embedding.toFun (α :=
          Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a))
          (RelEmbedding.toEmbedding (r :=
            fun
              (x1 x2 : Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a)) ↦
            x1 ≤ x2) (s := fun (x1 x2 : Submodule R ↥(torsionBy R M a)) ↦ x1 ≤ x2)
            (restrictScalarsEmbedding R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a)))
          ((fun (p : Submodule R ↥(torsionBy R M a)) ↦
              { carrier := (↑p : Set ↥(torsionBy R M a)), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ :
                Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a) })
            x))
        x_1 ↔
      x_1 ∈ x
⊢ Function.Embedding.toFun (α :=
      Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a))
      (RelEmbedding.toEmbedding (r :=
        fun (x1 x2 : Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a)) ↦
        x1 ≤ x2) (s := fun (x1 x2 : Submodule R ↥(torsionBy R M a)) ↦ x1 ≤ x2)
        (restrictScalarsEmbedding R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a)))
      ((fun (p : Submodule R ↥(torsionBy R M a)) ↦
          { carrier := (↑p : Set ↥(torsionBy R M a)), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ :
            Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a) })
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
a : R
x : Submodule R ↥(torsionBy R M a)
x_1 : ↥(torsionBy R M a)
⊢ Membership.mem (γ := Submodule R ↥(torsionBy R M a))
      (Function.Embedding.toFun (α :=
        Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a))
        (RelEmbedding.toEmbedding (r :=
          fun (x1 x2 : Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a)) ↦
          x1 ≤ x2) (s := fun (x1 x2 : Submodule R ↥(torsionBy R M a)) ↦ x1 ≤ x2)
          (restrictScalarsEmbedding R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a)))
        ((fun (p : Submodule R ↥(torsionBy R M a)) ↦
            { carrier := (↑p : Set ↥(torsionBy R M a)), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ :
              Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a)) ↥(torsionBy R M a) })
          x))
      x_1 ↔
    x_1 ∈ x

Tactic:
simp [restrictScalarsEmbedding]

Premises used: Submodule.restrictScalarsEmbedding
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M_1 : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module.Finite R M
I : Ideal R
⊢ Module.Finite.{u_1, u_3} (R ⧸ I) (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)

Tactic:
Module.Finite.of_restrictScalars_finite R _ _

Premises used: Module.Finite.of_restrictScalars_finite
-- 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 : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
x : M
⊢ Membership.mem (γ := Submodule R M) (torsion' R M S) x ↔ ∃ (a : S), a • x = 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- 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
⊢ Membership.mem (γ := Submodule R M) (torsion R M) x ↔ ∃ (a : ↥R⁰), a • x = 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- 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 : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
s : S
x : ↥(torsion' R M S)
obtain :
  ∀ (x : M) (a : S) (h : a • x = 0),
    Membership.mem (γ := Submodule R M) (torsion' R M S)
      (s • (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (torsion' R M S) x) x ⋯) : M))
⊢ Membership.mem (γ := Submodule R M) (torsion' R M S) (s • (↑x : M))

Tactic:
obtain ⟨x, a, h⟩ := 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
s : S
x : M
a : S
h : a • x = 0
h₁ : a • s • (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (torsion' R M S) x) x ⋯) : M) = 0
⊢ Membership.mem (γ := Submodule R M) (torsion' R M S)
    (s • (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (torsion' R M S) x) x ⋯) : M))

Tactic:
use a
-- 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 : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
s : S
x : M
a : S
h : a • x = 0
h₁ : a • s • x = 0
⊢ a • s • (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (torsion' R M S) x) x ⋯) : M) = 0

Tactic:
dsimp