awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P Q : Ideal R
hc : P ⊔ Q = ⊤
map : Fin 2 → Ideal R :=
  fun (x : Fin 2) ↦
    match (motive := Fin 2 → Ideal R) x with
    | 0 => P
    | 1 => Q
⊢ Eq (α := Submodule R M) (torsionBySet R M (↑P : Set R) ⊔ torsionBySet R M (↑Q : Set R))
    (torsionBySet R M (↑(P ⊓ Q) : Set R))
have refine_2 : ∀
  (heq :
    Eq (α := Submodule R M)
      (⨆ (i : Fin 2), ⨆ (_ : Membership.mem (γ := Finset (Fin 2)) ⊤ i), torsionBySet R M (↑(map i) : Set R))
      (torsionBySet R M (↑(⨅ (i : Fin 2), ⨅ (_ : Membership.mem (γ := Finset (Fin 2)) ⊤ i), map i) : Set R))),
  Eq (α := Submodule R M) (torsionBySet R M (↑P : Set R) ⊔ torsionBySet R M (↑Q : Set R))
    (torsionBySet R M (↑(P ⊓ Q) : Set R))
Tactic: have heq := Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf
    (p := map) (M := M) (S := ⊤) ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P Q : Ideal R
hc : P ⊔ Q = ⊤
map : Fin 2 → Ideal R :=
  fun (x : Fin 2) ↦
    match (motive := Fin 2 → Ideal R) x with
    | 0 => P
    | 1 => Q
refine_2 :
  ∀
    (heq :
      Eq (α := Submodule R M)
        (⨆ (i : Fin 2), ⨆ (_ : Membership.mem (γ := Finset (Fin 2)) ⊤ i), torsionBySet R M (↑(map i) : Set R))
        (torsionBySet R M (↑(⨅ (i : Fin 2), ⨅ (_ : Membership.mem (γ := Finset (Fin 2)) ⊤ i), map i) : Set R))),
    Eq (α := Submodule R M) (torsionBySet R M (↑P : Set R) ⊔ torsionBySet R M (↑Q : Set R))
      (torsionBySet R M (↑(P ⊓ Q) : Set R))
⊢ Eq (α := Submodule R M) (torsionBySet R M (↑P : Set R) ⊔ torsionBySet R M (↑Q : Set R))
    (torsionBySet R M (↑(P ⊓ Q) : Set R))
have refine_1 : (↑⊤ : Set (Fin 2)).Pairwise fun (i j : Fin 2) ↦ map i ⊔ map j = ⊤
Tactic: have heq := Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf
    (p := map) (M := M) (S := ⊤) ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P Q : Ideal R
hc : P ⊔ Q = ⊤
map : Fin 2 → Ideal R :=
  fun (x : Fin 2) ↦
    match (motive := Fin 2 → Ideal R) x with
    | 0 => P
    | 1 => Q
heq :
  Eq (α := Submodule R M)
    (⨆ (i : Fin 2), ⨆ (_ : Membership.mem (γ := Finset (Fin 2)) ⊤ i), torsionBySet R M (↑(map i) : Set R))
    (torsionBySet R M (↑(⨅ (i : Fin 2), ⨅ (_ : Membership.mem (γ := Finset (Fin 2)) ⊤ i), map i) : Set R))
⊢ Eq (α := Submodule R M) (torsionBySet R M (↑P : Set R) ⊔ torsionBySet R M (↑Q : Set R))
    (torsionBySet R M (↑(P ⊓ Q) : Set R))
have this : Eq (α := Submodule R M) (⨆ (i : Fin 2), ⨆ (_ : i = 0 ∨ i = 1), torsionBySet R M (↑(map i) : Set R))
  (torsionBySet R M (↑(map 0) : Set R) ⊔ torsionBySet R M (↑(map 1) : Set R))
Tactic: have : ⨆ i, ⨆ (_ : i = 0 ∨ i = 1), torsionBySet R M ↑(map i) =
        torsionBySet R M ↑(map 0) ⊔ torsionBySet R M ↑(map 1) := iSup_pair
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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 = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
⊢ Disjoint.{u_2} (α := Submodule R M) ((fun (i : ι) ↦ (torsionBySet R M (↑(p i) : Set R) : Submodule R M)) i)
    (T.sup fun (i : ι) ↦ torsionBySet R M (↑(p i) : Set R))
have rw : Eq (α := Submodule R M)
  ((fun (i : ι) ↦ (torsionBySet R M (↑(p i) : Set R) : Submodule R M)) i ⊓ torsionBySet R M (↑(⨅ i ∈ T, p i) : Set R)) ⊥
Tactic: rw [disjoint_iff, Finset.sup_eq_iSup,
    iSup_torsionBySet_ideal_eq_torsionBySet_iInf fun i hi j hj ij => hp (hT hi) (hT hj) ij]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (hypothesis)
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 = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
⊢ Eq (α := Submodule R M)
    ((fun (i : ι) ↦ (torsionBySet R M (↑(p i) : Set R) : Submodule R M)) i ⊓ torsionBySet R M (↑(⨅ i ∈ T, p i) : Set R))
    ⊥
have this : Eq (α := Submodule R M)
  (torsionBySet R M
    (↑((OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R)
            ((OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) (p i) ⊓
              (OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) (⨅ i ∈ T, p i)) :
          Ideal R) :
      Set R))
  (torsionBySet R M
      (↑((OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) ((OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) (p i)) :
            Ideal R) :
        Set R) ⊓
    torsionBySet R M
      (↑((OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R)
            ((OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) (⨅ i ∈ T, p i))) :
        Set R))
Tactic: have := GaloisConnection.u_inf
    (b₁ := OrderDual.toDual (p i)) (b₂ := OrderDual.toDual (⨅ i ∈ T, p i)) (torsion_gc R M)
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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 = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
this :
  Eq (α := Submodule R M) (torsionBySet R M (↑(p i ⊔ ⨅ i ∈ T, p i) : Set R))
    (torsionBySet R M (↑(p i) : Set R) ⊓ torsionBySet R M (↑(⨅ i ∈ T, p i) : Set R))
⊢ Eq (α := Submodule R M) (torsionBySet R M (↑(p i) : Set R) ⊓ torsionBySet R M (↑(⨅ i ∈ T, p i) : Set R)) ⊥
have rw : ∀ i_1 ∈ T, p i ⊔ p i_1 = ⊤
Tactic: rw [← this, Ideal.sup_iInf_eq_top, top_coe, torsionBySet_univ]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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 = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
this :
  Eq (α := Submodule R M) (torsionBySet R M (↑(p i ⊔ ⨅ i ∈ T, p i) : Set R))
    (torsionBySet R M (↑(p i) : Set R) ⊓ torsionBySet R M (↑(⨅ i ∈ T, p i) : Set R))
j : ι
hj : j ∈ T
⊢ p i ⊔ p j = ⊤
have apply : i ≠ j
Tactic: apply hp hi (hT hj)
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P Q : Ideal R
hc : P ⊔ Q = ⊤
map : Fin 2 → Ideal R :=
  fun (x : Fin 2) ↦
    match (motive := Fin 2 → Ideal R) x with
    | 0 => P
    | 1 => Q
⊢ Disjoint (α := Submodule R M) (torsionBySet R M (↑P : Set R)) (torsionBySet R M (↑Q : Set R))
have refine_2 : ∀ (heq : Finset.SupIndep.{u_2, 0} (α := Submodule R M) ⊤ fun (i : Fin 2) ↦ torsionBySet R M (↑(map i) : Set R)),
  Disjoint (α := Submodule R M) (torsionBySet R M (↑P : Set R)) (torsionBySet R M (↑Q : Set R))
Tactic: have heq := Submodule.supIndep_torsionBySet_ideal (p := map) (M := M) (S := ⊤) ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P Q : Ideal R
hc : P ⊔ Q = ⊤
map : Fin 2 → Ideal R :=
  fun (x : Fin 2) ↦
    match (motive := Fin 2 → Ideal R) x with
    | 0 => P
    | 1 => Q
refine_2 :
  ∀ (heq : Finset.SupIndep.{u_2, 0} (α := Submodule R M) ⊤ fun (i : Fin 2) ↦ torsionBySet R M (↑(map i) : Set R)),
    Disjoint (α := Submodule R M) (torsionBySet R M (↑P : Set R)) (torsionBySet R M (↑Q : Set R))
⊢ Disjoint (α := Submodule R M) (torsionBySet R M (↑P : Set R)) (torsionBySet R M (↑Q : Set R))
have refine_1 : (↑⊤ : Set (Fin 2)).Pairwise fun (i j : Fin 2) ↦ map i ⊔ map j = ⊤
Tactic: have heq := Submodule.supIndep_torsionBySet_ideal (p := map) (M := M) (S := ⊤) ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
⊢ Eq (α := Submodule R M) (⨆ i ∈ S, torsionBy R M (q i)) (torsionBy R M (∏ i ∈ S, q i))
have rw : Eq.{u_2 + 1} (α := Submodule R M) (⨆ i ∈ S, torsionBy R M (q i))
  (⨆ i ∈ S, torsionBySet R M (↑(Ideal.span {q i}) : Set R))
Tactic: rw [← torsionBySet_span_singleton_eq, Ideal.submodule_span_eq, ←
    Ideal.finset_inf_span_singleton _ _ hq, Finset.inf_eq_iInf, ←
    iSup_torsionBySet_ideal_eq_torsionBySet_iInf]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
rw :
  Eq.{u_2 + 1} (α := Submodule R M) (⨆ i ∈ S, torsionBy R M (q i))
    (⨆ i ∈ S, torsionBySet R M (↑(Ideal.span {q i}) : Set R))
⊢ Eq (α := Submodule R M) (⨆ i ∈ S, torsionBy R M (q i)) (torsionBy R M (∏ i ∈ S, q i))
have rw₁ : (↑S : Set ι).Pairwise fun (i j : ι) ↦ Eq (α := Ideal R) (Ideal.span {q i} ⊔ Ideal.span {q j}) ⊤
Tactic: rw [← torsionBySet_span_singleton_eq, Ideal.submodule_span_eq, ←
    Ideal.finset_inf_span_singleton _ _ hq, Finset.inf_eq_iInf, ←
    iSup_torsionBySet_ideal_eq_torsionBySet_iInf]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
⊢ Eq.{u_2 + 1} (α := Submodule R M) (⨆ i ∈ S, torsionBy R M (q i))
    (⨆ i ∈ S, torsionBySet R M (↑(Ideal.span {q i}) : Set R))
have e_s : Eq (α := ι → Submodule R M) (fun (i : ι) ↦ ⨆ (_ : i ∈ S), torsionBy R M (q i)) fun (i : ι) ↦
  ⨆ (_ : i ∈ S), torsionBySet R M (↑(Ideal.span {q i}) : Set R)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
⊢ Eq (α := ι → Submodule R M) (fun (i : ι) ↦ ⨆ (_ : i ∈ S), torsionBy R M (q i)) fun (i : ι) ↦
    ⨆ (_ : i ∈ S), torsionBySet R M (↑(Ideal.span {q i}) : Set R)
have e_s : ∀ (x : ι),
  Eq.{u_2 + 1} (α := Submodule R M) (⨆ (_ : x ∈ S), torsionBy R M (q x))
    (⨆ (_ : x ∈ S), torsionBySet R M (↑(Ideal.span {q x}) : Set R))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
x : ι
⊢ Eq.{u_2 + 1} (α := Submodule R M) (⨆ (_ : x ∈ S), torsionBy R M (q x))
    (⨆ (_ : x ∈ S), torsionBySet R M (↑(Ideal.span {q x}) : Set R))
have e_s : Eq.{u_2 + 1} (α := x ∈ S → Submodule R M) (fun (h : x ∈ S) ↦ torsionBy R M (q x)) fun (h : x ∈ S) ↦
  torsionBySet R M (↑(Ideal.span {q x}) : Set R)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
x : ι
⊢ Eq.{u_2 + 1} (α := x ∈ S → Submodule R M) (fun (h : x ∈ S) ↦ torsionBy R M (q x)) fun (h : x ∈ S) ↦
    torsionBySet R M (↑(Ideal.span {q x}) : Set R)
have e_s : x ∈ S → Eq (α := Submodule R M) (torsionBy R M (q x)) (torsionBySet R M (↑(Ideal.span {q x}) : Set R))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
⊢ Finset.SupIndep.{u_2, u_3} (α := Submodule R M) S fun (i : ι) ↦ torsionBy R M (q i)
have h : ∀ (x : ι), Eq (α := Submodule R M) (torsionBy R M (q x)) (torsionBySet R M (↑(Ideal.span {q x}) : Set R))
Tactic: convert!
    supIndep_torsionBySet_ideal (M := M) fun i hi j hj ij =>
      (Ideal.sup_eq_top_iff_isCoprime (q i) _).mpr <| hq hi hj ij
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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) (⨆ (i : ↥S), torsionBySet R M (↑(p (↑i : ι)) : Set R)) ⊤
have apply : Eq.{u_2 + 1} (α := Submodule R M) (⨆ t ∈ (↑S : Set ι), torsionBySet R M (↑(p t) : Set R)) ⊤
Tactic: apply (iSup_subtype'' ↑S fun i => torsionBySet R M <| p i).trans
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (hypothesis)
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)
⊢ DirectSum.IsInternal (S := Submodule R M) fun (i : ↥S) ↦ torsionBy R M (q (↑i : ι))
have hM₁ : 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
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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) ↦ torsionBy R M (q (↑i : ι))
have h : ∀ (x : ↥S), Eq (α := Submodule R M) (torsionBy R M (q (↑x : ι))) (torsionBySet R M (↑(Ideal.span {q (↑x : ι)}) : Set R))
Tactic: convert!
    torsionBySet_isInternal
      (fun i hi j hj ij => (Ideal.sup_eq_top_iff_isCoprime (q i) _).mpr <| hq hi hj ij) hM
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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
⊢ LE.le.{u_1} (α := AddSubgroup R) (Submodule.toAddSubgroup I) (AddMonoidHom.ker (M := M →+ M) (smulAddHom R M))
have 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))
Tactic: rwa [isTorsionBySet_iff_subset_annihilator] at hM
Cleared hypotheses: hM, b
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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
⊢ IsTorsionBySet R M (↑(Ideal.span {r}) : Set R)
have rwa : ∀ (hM : IsTorsionBySet R M (↑(R ∙ r) : Set R)), IsTorsionBySet R M (↑(Ideal.span {r}) : Set R)
Tactic: rwa [← isTorsionBySet_span_singleton_iff r] at hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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
⊢ IsTorsionBySet R M (↑(Ideal.span {r}) : Set R)
have rwa : ∀ (hM : IsTorsionBySet R M (↑(R ∙ r) : Set R)), IsTorsionBySet R M (↑(Ideal.span {r}) : Set R)
Tactic: finally
  rwa [← isTorsionBySet_span_singleton_iff r] at hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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
⊢ IsTorsionBySet R M (↑(Ideal.span {r}) : Set R)
have rwa : ∀ (hM : IsTorsionBySet R M (↑(R ∙ r) : Set R)), IsTorsionBySet R M (↑(Ideal.span {r}) : Set R)
Tactic: rwa [← isTorsionBySet_span_singleton_iff] at hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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
⊢ IsTorsionBySet R M (↑(Ideal.span {r}) : Set R)
have rwa : ∀ (hM : IsTorsionBySet R M (↑(R ∙ r) : Set R)), IsTorsionBySet R M (↑(Ideal.span {r}) : Set R)
Tactic: finally
  rwa [← isTorsionBySet_span_singleton_iff] at hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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)
⊢ (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
have 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' := sorry, zero_mem' := sorry, smul_mem' := sorry :
            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: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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)
⊢ 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
have 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' := sorry, zero_mem' := sorry, smul_mem' := sorry :
              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: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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)
⊢ Membership.mem (γ := Submodule R M) (torsion' R M S) (s • (↑x : M))
have 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 sorry) : M))
Tactic: obtain ⟨x, a, h⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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
⊢ 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))
have h₁ : a • s • (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (torsion' R M S) x) x sorry) : M) = 0
Tactic: use a
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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
⊢ a • s • (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (torsion' R M S) x) x ⋯) : M) = 0
have h₁ : a • s • x = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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
⊢ a • s • x = 0
have h₁ : s • a • x = 0
Tactic: rw [smul_comm, h, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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₁ : s • a • x = 0
⊢ a • s • x = 0
have h₂ : HSMul.hSMul (β := M) s 0 = 0
Tactic: rw [smul_comm, h, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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₁ : s • a • x = 0
h₂ : HSMul.hSMul (β := M) s 0 = 0
⊢ a • s • x = 0
have h₃ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [smul_comm, h, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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
h : Eq (α := Submodule R M) (torsion' R M S) ⊤
x : M
⊢ ∃ (a : S), a • x = 0
have rw : Membership.mem (γ := Submodule R M) ⊤ x
Tactic: rw [← @mem_torsion'_iff R, h]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
hM : IsTorsion R M
⊢ ((↑(annihilator.{u_1, u_2} (M := M) ⊤) : Set R) ∩ (↑R⁰ : Set R)).Nonempty
have obtain : ∀ (S : Finset M) (hS : Eq (α := Submodule R M) (span R (↑S : Set M)) ⊤),
  ((↑(annihilator.{u_1, u_2} (M := M) ⊤) : Set R) ∩ (↑R⁰ : Set R)).Nonempty
Tactic: obtain ⟨S, hS⟩ := ‹Module.Finite R M›.fg_top