-- Mathlib/Algebra/Module/Torsion.lean
theorem iSup_torsionBy_eq_torsionBy_prod (hq : (S : Set ι).Pairwise <| (IsCoprime on q)) :
    ⨆ i ∈ S, torsionBy R M (q i) = torsionBy R M (∏ i ∈ S, q i)

Proof state:
case e_s.h.e_s
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
x✝ : ι
⊢ (fun h => torsionBy R M (q x✝)) = fun h => torsionBySet R M ↑(Ideal.span {q x✝})

Tactic:
ext : 1

Result:
case e_s.h.e_s.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
x✝¹ : ι
x✝ : x✝¹ ∈ S
⊢ torsionBy R M (q x✝¹) = torsionBySet R M ↑(Ideal.span {q x✝¹})

Proof state:
case e_s.h.e_s.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
x✝¹ : ι
x✝ : x✝¹ ∈ S
⊢ torsionBy R M (q x✝¹) = torsionBySet R M ↑(Ideal.span {q x✝¹})

Tactic:
exact (torsionBySet_span_singleton_eq _).symm

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ (↑S).Pairwise fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤

Tactic:
exact fun i hi j hj ij => (Ideal.sup_eq_top_iff_isCoprime _ _).mpr (hq hi hj ij)

Result:
no goals

Proof state:
case e_s.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
x✝ : ι
⊢ ⨆ (_ : x✝ ∈ S), torsionBy R M (q x✝) = ⨆ (_ : x✝ ∈ S), torsionBySet R M ↑(Ideal.span {q x✝})

Tactic:
congr

Result:
case e_s.h.e_s
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
x✝ : ι
⊢ (fun h => torsionBy R M (q x✝)) = fun h => torsionBySet R M ↑(Ideal.span {q x✝})

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ ⨆ i ∈ S, torsionBy R M (q i) = ⨆ i ∈ S, torsionBySet R M ↑(Ideal.span {q i})

Tactic:
congr

Result:
case e_s
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ (fun i => ⨆ (_ : i ∈ S), torsionBy R M (q i)) = fun i => ⨆ (_ : i ∈ S), torsionBySet R M ↑(Ideal.span {q i})

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ ⨆ i ∈ S, torsionBy R M (q i) = torsionBy R M (∏ i ∈ S, q i)

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]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ ⨆ i ∈ S, torsionBy R M (q i) = ⨆ i ∈ S, torsionBySet R M ↑(Ideal.span {q i})

R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ (↑S).Pairwise fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤

Proof state:
case e_s
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ (fun i => ⨆ (_ : i ∈ S), torsionBy R M (q i)) = fun i => ⨆ (_ : i ∈ S), torsionBySet R M ↑(Ideal.span {q i})

Tactic:
ext : 1

Result:
case e_s.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
x✝ : ι
⊢ ⨆ (_ : x✝ ∈ S), torsionBy R M (q x✝) = ⨆ (_ : x✝ ∈ S), torsionBySet R M ↑(Ideal.span {q x✝})