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 : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
rw : (∀ (b : (↑s : Type u_1)) (a : M), (↑b : R) • a = 0) ↔ ∀ x ∈ s, ∀ (m : M), x • m = 0
⊢ (∀ ⦃x : M⦄ ⦃a : (↑s : Type u_1)⦄, (↑a : R) • x = 0) ↔ ∀ x ∈ s, ∀ (m : M), x • m = 0
have rw₁ : (∀ (x : R) (h : x ∈ s) (a : M), (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) x h) : R) • a = 0) ↔
  ∀ x ∈ s, ∀ (m : M), x • m = 0
Tactic: rw [forall_comm, SetCoe.forall]
-- 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 : Set R
x : M
⊢ Membership.mem (γ := Submodule R M) (torsionBySet R M s) x ↔ ∀ (a : (↑s : Type u_1)), (↑a : R) • x = 0
have refine : ∀ (h : ∀ (a : (↑s : Type u_1)), (↑a : R) • x = 0) (p : Submodule R M),
  Membership.mem (γ := Set (Submodule R M)) (torsionBy R M '' s) p → x ∈ p
Tactic: refine ⟨fun h ⟨a, ha⟩ => mem_sInf.mp h _ (Set.mem_image_of_mem _ ha), fun h => mem_sInf.mpr ?_⟩
-- 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
a : R
⊢ Eq (α := Submodule R M) (torsionBySet R M {a}) (torsionBy R M a)
have h : ∀ (x : M),
  Membership.mem (γ := Submodule R M) (torsionBySet R M {a}) x ↔ Membership.mem (γ := Submodule R M) (torsionBy R M a) x
Tactic: ext 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 : Set R
⊢ Eq (α := Submodule R M) (torsionBySet R M s) (torsionBySet R M (↑(Ideal.span s) : Set R))
have refine : ∀ (x : M) (hx : Membership.mem (γ := Submodule R M) (torsionBySet R M s) x),
  Membership.mem (γ := Submodule R M) (torsionBySet R M (↑(Ideal.span s) : Set R)) x
Tactic: refine le_antisymm (fun x hx => ?_) (torsionBySet_le_torsionBySet_of_subset subset_span)
-- 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 : Set R
x : M
hx : Membership.mem (γ := Submodule R M) (torsionBySet R M s) x
⊢ Membership.mem (γ := Submodule R M) (torsionBySet R M (↑(Ideal.span s) : Set R)) x
have rw : ∀ (hx : ∀ (a : (↑s : Type u_1)), (↑a : R) • x = 0) (a : (↑(↑(Ideal.span s) : Set R) : Type u_1)), (↑a : R) • x = 0
Tactic: rw [mem_torsionBySet_iff] at hx ⊢
Cleared hypotheses: hx
-- 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 : Set R
x : M
hx : ∀ (a : (↑s : Type u_1)), (↑a : R) • x = 0
⊢ ∀ (a : (↑(↑(Ideal.span s) : Set R) : Type u_1)), (↑a : R) • x = 0
have suffices : LE.le (α := Ideal R) (Ideal.span s) (Ideal.torsionOf R M x)
Tactic: suffices Ideal.span s ≤ Ideal.torsionOf R M x by
    rintro ⟨a, ha⟩
    exact this ha
-- 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 : Set R
x : M
hx : ∀ (a : (↑s : Type u_1)), (↑a : R) • x = 0
⊢ LE.le (α := Ideal R) (Ideal.span s) (Ideal.torsionOf R M x)
have rw : s ⊆ (↑(Ideal.torsionOf R M x) : Set R)
Tactic: rw [Ideal.span_le]
-- 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
a b : R
dvd : a ∣ b
⊢ LE.le (α := Submodule R M) (torsionBy R M a) (torsionBy R M b)
have rw : LE.le (α := Submodule R M) (torsionBySet R M (↑(R ∙ a) : Set R)) (torsionBySet R M {b})
Tactic: rw [← torsionBySet_span_singleton_eq, ← torsionBySet_singleton_eq]
-- 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
a b : R
dvd : a ∣ b
⊢ LE.le (α := Submodule R M) (torsionBySet R M (↑(R ∙ a) : Set R)) (torsionBySet R M {b})
have st : {b} ⊆ (↑(R ∙ a) : Set R)
Tactic: apply torsionBySet_le_torsionBySet_of_subset
-- 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
x : M
h : Membership.mem (γ := Submodule R M) (torsionBy R M 1) x
⊢ Membership.mem (γ := Submodule R M) ⊥ x
have h₁ : x = 0
Tactic: rw [mem_torsionBy_iff, one_smul] at h
Cleared hypotheses: 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
⊢ Eq (α := Submodule R M) (torsionBySet R M Set.univ) ⊥
have rw : LE.le (α := Submodule R M) (torsionBySet R M Set.univ) (torsionBySet R M {1})
Tactic: rw [eq_bot_iff, ← torsionBy_one, ← torsionBySet_singleton_eq]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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
have refine : ∀ (h : IsTorsionBy R M a) (x : M) ⦃a_1 : (↑{a} : Type u_1)⦄, (↑a_1 : R) • x = 0
Tactic: refine ⟨fun h x => @h _ ⟨_, Set.mem_singleton _⟩, fun h 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 : Set R
h : Eq (α := Submodule R M) (torsionBySet R M s) ⊤
x : M
⊢ ∀ ⦃a : (↑s : Type u_1)⦄, (↑a : R) • x = 0
have rw : Membership.mem (γ := Submodule R M) ⊤ x
Tactic: rw [← mem_torsionBySet_iff, 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
a : R
⊢ IsTorsionBy R M a ↔ Eq (α := Submodule R M) (torsionBy R M a) ⊤
have rw : IsTorsionBy R M a ↔ Eq (α := Submodule R M) (torsionBySet R M {a}) ⊤
Tactic: rw [← torsionBySet_singleton_eq, ← isTorsionBySet_singleton_iff,
    isTorsionBySet_iff_torsionBySet_eq_top]
-- 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
a : R
rw : IsTorsionBy R M a ↔ Eq (α := Submodule R M) (torsionBySet R M {a}) ⊤
⊢ IsTorsionBy R M a ↔ Eq (α := Submodule R M) (torsionBy R M a) ⊤
have rw₁ : IsTorsionBySet R M {a} ↔ Eq (α := Submodule R M) (torsionBySet R M {a}) ⊤
Tactic: rw [← torsionBySet_singleton_eq, ← isTorsionBySet_singleton_iff,
    isTorsionBySet_iff_torsionBySet_eq_top]
-- 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
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}) ⊤
⊢ IsTorsionBy R M a ↔ Eq (α := Submodule R M) (torsionBy R M a) ⊤
have rw₂ : Eq (α := Submodule R M) (torsionBySet R M {a}) ⊤ ↔ Eq (α := Submodule R M) (torsionBySet R M {a}) ⊤
Tactic: rw [← torsionBySet_singleton_eq, ← isTorsionBySet_singleton_iff,
    isTorsionBySet_iff_torsionBySet_eq_top]
-- 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 = ⊤
⊢ Eq (α := Submodule R M) (⨆ i ∈ S, torsionBySet R M (↑(p i) : Set R)) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R))
have 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))
Tactic: rcases S.eq_empty_or_nonempty with h | 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
ι : 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))
⊢ Eq (α := Submodule R M) (⨆ i ∈ S, torsionBySet R M (↑(p i) : Set R)) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R))
have 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))
Tactic: rcases S.eq_empty_or_nonempty with h | 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
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S : Set ι).Pairwise fun (i j : ι) ↦ p i ⊔ p j = ⊤
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))
have inr : 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 le_antisymm
-- 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 = ⊤
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))
⊢ Eq (α := Submodule R M) (⨆ i ∈ S, torsionBySet R M (↑(p i) : Set R)) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R))
have inr₁ : LE.le (α := Submodule R M) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R)) (⨆ i ∈ S, torsionBySet R M (↑(p i) : Set R))
Tactic: apply le_antisymm
-- 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 = ⊤
h : S.Nonempty
⊢ LE.le (α := Submodule R M) (⨆ i ∈ S, torsionBySet R M (↑(p i) : Set R)) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R))
have 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))
Tactic: apply iSup_le _
-- 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 = ⊤
h : S.Nonempty
i : ι
⊢ LE.le (α := Submodule R M) (⨆ (_ : i ∈ S), torsionBySet R M (↑(p i) : Set R))
    (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R))
have 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))
Tactic: apply iSup_le _
-- 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 = ⊤
h : S.Nonempty
i : ι
is : i ∈ S
⊢ LE.le (α := Submodule R M) (torsionBySet R M (↑(p i) : Set R)) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R))
have st : (↑(⨅ i ∈ S, p i) : Set R) ⊆ (↑(p i) : Set R)
Tactic: apply torsionBySet_le_torsionBySet_of_subset
-- 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 = ⊤
h : S.Nonempty
x : M
hx : Membership.mem (γ := Submodule R M) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R)) x
⊢ Membership.mem (γ := Submodule R M) (⨆ i ∈ S, torsionBySet R M (↑(p i) : Set R)) x
have inr : ∃ (μ : (i : ι) → ↥(torsionBySet R M (↑(p i) : Set R))), ∑ i ∈ S, (↑(μ i) : M) = x
Tactic: rw [mem_iSup_finset_iff_exists_sum]
-- 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 = ⊤
h : S.Nonempty
x : M
hx : Membership.mem (γ := Submodule R M) (torsionBySet R M (↑(⨅ i ∈ S, p i) : Set R)) x
⊢ ∃ (μ : (i : ι) → ↥(torsionBySet R M (↑(p i) : Set R))), ∑ i ∈ S, (↑(μ i) : M) = x
have 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
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)
-- 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 = ⊤
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
have inr : ∀ (i : ι), Membership.mem (γ := Submodule R M) (torsionBySet R M (↑(p i) : Set R)) ((↑(μ i) : R) • x)
Tactic: refine ⟨fun i => ⟨(μ i : R) • 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
ι : 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)
⊢ ∃ (μ : (i : ι) → ↥(torsionBySet R M (↑(p i) : Set R))), ∑ i ∈ S, (↑(μ i) : M) = x
have 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) sorry :
              ↥(torsionBySet R M (↑(p i) : Set R))))
          i) :
      M) =
  x
Tactic: refine ⟨fun i => ⟨(μ i : R) • 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
ι : 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 : ι
⊢ Membership.mem (γ := Submodule R M) (torsionBySet R M (↑(p i) : Set R)) ((↑(μ i) : R) • x)
have 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
Tactic: rw [mem_torsionBySet_iff] at hx ⊢
Cleared hypotheses: hx, μ, hμ, i
-- 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 = ⊤
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)
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑(p i) : Set R)) a ha) : R) • (↑(μ i) : R) • x = 0
have inr : ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑(p i) : Set R)) a ha) : R) * (↑(μ i) : R)) • x = 0
Tactic: rw [smul_smul]
-- 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 = ⊤
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)
⊢ ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑(p i) : Set R)) a ha) : R) * (↑(μ i) : R)) • x = 0
have inr : Membership.mem (γ := Ideal R) (⨅ i ∈ S, p i) (a * (↑(μ i) : R))
Tactic: suffices a * μ i ∈ ⨅ i ∈ S, p i from hx ⟨_, this⟩
-- 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 = ⊤
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)
⊢ Membership.mem (γ := Ideal R) (⨅ i ∈ S, p i) (a * (↑(μ i) : R))
have inr : ∀ (i_1 : ι), Membership.mem (γ := Submodule R R) (⨅ (_ : i_1 ∈ S), p i_1) (a * (↑(μ i) : R))
Tactic: rw [mem_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
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)
j : ι
⊢ Membership.mem (γ := Submodule R R) (⨅ (_ : j ∈ S), p j) (a * (↑(μ i) : R))
have inr : ∀ (i_1 : j ∈ S), a * (↑(μ i) : R) ∈ p j
Tactic: rw [mem_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
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)
j : ι
hj : j ∈ S
⊢ a * (↑(μ i) : R) ∈ p j
have pos : ∀ (ij : j = i), a * (↑(μ i) : R) ∈ p j
Tactic: by_cases ij : j = i
-- 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 = ⊤
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)
j : ι
hj : j ∈ S
pos : ∀ (ij : j = i), a * (↑(μ i) : R) ∈ p j
⊢ a * (↑(μ i) : R) ∈ p j
have neg : ∀ (ij : ¬j = i), a * (↑(μ i) : R) ∈ p j
Tactic: by_cases ij : j = i
-- 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 = ⊤
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)
j : ι
hj : j ∈ S
ij : j = i
⊢ a * (↑(μ i) : R) ∈ p j
have pos : a * (↑(μ i) : R) ∈ p i
Tactic: rw [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 = ⊤
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)
j : ι
hj : j ∈ S
ij : ¬j = i
⊢ a * (↑(μ i) : R) ∈ p j
have this : Membership.mem (γ := Submodule R R) (⨅ j ∈ S, ⨅ (_ : j ≠ i), p j) (↑(μ i) : R)
Tactic: have := coe_mem (μ i)
-- 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 = ⊤
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)
j : ι
hj : j ∈ S
ij : ¬j = i
this : Membership.mem (γ := Submodule R R) (⨅ j ∈ S, ⨅ (_ : j ≠ i), p j) (↑(μ i) : R)
⊢ a * (↑(μ i) : R) ∈ p j
have this₁ : ∀ (i_1 : ι) (i_2 : i_1 ∈ S) (i_3 : i_1 ≠ i), (↑(μ i) : R) ∈ p i_1
Tactic: simp only [mem_iInf] at this
Cleared hypotheses: this
-- 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 = ⊤
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 ∈ 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
have inr : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (∑ i ∈ S, (↑(μ i) : R)) x = x
Tactic: rw [← Finset.sum_smul, hμ, one_smul]
-- 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 = ⊤
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 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (∑ i ∈ S, (↑(μ i) : R)) x = x
⊢ ∑ 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
have inr₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 x = x
Tactic: rw [← Finset.sum_smul, hμ, one_smul]
-- 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 = ⊤
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 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (∑ i ∈ S, (↑(μ i) : R)) x = x
inr₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 x = x
⊢ ∑ 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
have inr₂ : x = x
Tactic: rw [← Finset.sum_smul, hμ, one_smul]