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
ι : 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 : ∀ (i_1 : ι), Membership.mem (γ := Submodule R R) (⨅ (_ : i_1 ∈ S), p i_1) (a * (↑(μ i) : R))
⊢ Membership.mem (γ := Ideal R) (⨅ i ∈ S, p i) (a * (↑(μ i) : R))

Tactic:
rw [mem_iInf]

Premises used: Submodule.mem_iInf
-- 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)
j : ι
inr : ∀ (i_1 : j ∈ S), a * (↑(μ i) : R) ∈ p j
⊢ Membership.mem (γ := Submodule R R) (⨅ (_ : j ∈ S), p j) (a * (↑(μ i) : R))

Tactic:
rw [mem_iInf]

Premises used: Submodule.mem_iInf
-- 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)
j : ι
hj : j ∈ S
pos : ∀ (ij : j = i), a * (↑(μ i) : R) ∈ p j
neg : ∀ (ij : ¬j = i), a * (↑(μ i) : R) ∈ p j
⊢ a * (↑(μ i) : R) ∈ p j

Tactic:
by_cases ij : j = i
-- 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)
j : ι
hj : j ∈ S
ij : j = i
pos : a * (↑(μ i) : R) ∈ p i
⊢ a * (↑(μ i) : R) ∈ p j

Tactic:
rw [ij]
-- 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)
j : ι
hj : j ∈ S
ij : j = i
⊢ a * (↑(μ i) : R) ∈ p i

Tactic:
Ideal.mul_mem_right _ _ ha

Premises used: Set.Mem, Ideal.mul_mem_right
-- 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)
j : ι
hj : j ∈ S
ij : j = i
⊢ a * (↑(μ i) : R) ∈ p i

Tactic:
exact Ideal.mul_mem_right _ _ ha

Premises used: Ideal.mul_mem_right
-- 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)
j : ι
hj : j ∈ S
ij : ¬j = i
⊢ Membership.mem (γ := Submodule R R) (⨅ j ∈ S, ⨅ (_ : j ≠ i), p j) (↑(μ i) : R)

Tactic:
have := coe_mem (μ i)
-- 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)
j : ι
hj : j ∈ S
ij : ¬j = i
this : Membership.mem (γ := Submodule R R) (⨅ j ∈ S, ⨅ (_ : j ≠ i), p j) (↑(μ i) : R)
⊢ ∀ (i_1 : ι) (i_2 : i_1 ∈ S) (i_3 : i_1 ≠ i), (↑(μ i) : R) ∈ p i_1

Tactic:
simp only [mem_iInf] at this

Premises used: Submodule.mem_iInf
-- 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)
j : ι
hj : j ∈ S
ij : ¬j = i
this : ∀ (i_1 : ι) (i_2 : i_1 ∈ S) (i_3 : i_1 ≠ i), (↑(μ i) : R) ∈ p i_1
⊢ a * (↑(μ i) : R) ∈ p j

Tactic:
Ideal.mul_mem_left _ _ (this j hj ij)

Premises used: Set.Mem, Ideal.mul_mem_left
-- 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)
j : ι
hj : j ∈ S
ij : ¬j = i
this : ∀ (i_1 : ι) (i_2 : i_1 ∈ S) (i_3 : i_1 ≠ i), (↑(μ i) : R) ∈ p i_1
⊢ a * (↑(μ i) : R) ∈ p j

Tactic:
exact Ideal.mul_mem_left _ _ (this j hj ij)

Premises used: Ideal.mul_mem_left
-- 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 : 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
inr₂ inr₃ : 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

Tactic:
rw [← Finset.sum_smul, hμ, one_smul]

Premises used: Finset.sum_smul, one_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
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))
refine_1 : (↑⊤ : Set (Fin 2)).Pairwise fun (i j : Fin 2) ↦ map i ⊔ map j = ⊤
⊢ 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 := ⊤) ?_
-- 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
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) (⨆ (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
-- 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
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))
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))
⊢ Eq (α := Submodule R M) (torsionBySet R M (↑P : Set R) ⊔ torsionBySet R M (↑Q : Set R))
    (torsionBySet R M (↑(P ⊓ Q) : Set R))

Tactic:
simpa [Finset.top_eq_univ, Fin.univ_succ, Fin.isValue, coe_iInf, this] using heq

Premises used: Finset.top_eq_univ, Submodule.coe_iInf, Fin.univ_succ, Fin.isValue
-- 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
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
⊢ (↑⊤ : Set (Fin 2)).Pairwise fun (i j : Fin 2) ↦ map i ⊔ map j = ⊤

Tactic:
simp_all [Set.pairwise_pair, Fin.univ_succ, map, sup_comm]

Premises used: Set.pairwise_pair, Fin.univ_succ, sup_comm
-- 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 = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
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))
    ⊥
⊢ 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))

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]

Premises used: disjoint_iff, Finset.sup_eq_iSup, Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf
-- 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 = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
⊢ 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)
-- 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 = ⊤
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))
rw : ∀ i_1 ∈ T, p i ⊔ p i_1 = ⊤
⊢ Eq (α := Submodule R M) (torsionBySet R M (↑(p i) : Set R) ⊓ torsionBySet R M (↑(⨅ i ∈ T, p i) : Set R)) ⊥

Tactic:
rw [← this, Ideal.sup_iInf_eq_top, top_coe, torsionBySet_univ]

Premises used: Ideal.sup_iInf_eq_top, Submodule.torsionBySet_univ, Submodule.top_coe
-- 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 = ⊤
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
apply : i ≠ j
⊢ p i ⊔ p j = ⊤

Tactic:
apply hp hi (hT hj)
-- 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 = ⊤
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))
hj : i ∈ T
⊢ False

Tactic:
hiT hj
-- 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 = ⊤
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))
hj : i ∈ T
⊢ False

Tactic:
exact hiT hj
-- 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
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))
refine_1 : (↑⊤ : Set (Fin 2)).Pairwise fun (i j : Fin 2) ↦ map i ⊔ map j = ⊤
⊢ 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 := ⊤) ?_
-- 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
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 : 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:
simpa [Finset.top_eq_univ, Fin.isValue, map] using heq

Premises used: Finset.top_eq_univ, Fin.isValue
-- 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
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
⊢ (↑⊤ : Set (Fin 2)).Pairwise fun (i j : Fin 2) ↦ map i ⊔ map j = ⊤

Tactic:
aesop (add norm [Fin.univ_succ, Set.pairwise_pair, map, sup_comm])

Premises used: Set.pairwise_pair, Fin.univ_succ, sup_comm
-- 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
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))
rw₁ : (↑S : Set ι).Pairwise fun (i j : ι) ↦ Eq (α := Ideal R) (Ideal.span {q i} ⊔ Ideal.span {q j}) ⊤
⊢ Eq (α := Submodule R M) (⨆ 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]

Premises used: Ideal.submodule_span_eq, Ideal.finset_inf_span_singleton, Submodule.torsionBySet_span_singleton_eq, Finset.inf_eq_iInf, Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf
-- 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
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
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)
⊢ 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:
congr
-- 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
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
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))
⊢ 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:
ext : 1
-- 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
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
x : ι
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)
⊢ 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:
congr
-- 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
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
x : ι
e_s : x ∈ S → Eq (α := Submodule R M) (torsionBy R M (q x)) (torsionBySet R M (↑(Ideal.span {q x}) : Set R))
⊢ 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:
ext : 1
-- 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
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
x : ι
h : 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 _).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 : 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 : ι
h : 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 _).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 : 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)
⊢ (↑S : Set ι).Pairwise fun (i j : ι) ↦ Eq (α := Ideal R) (Ideal.span {q i} ⊔ Ideal.span {q j}) ⊤

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

Premises used: Iff.mpr, Ideal.sup_eq_top_iff_isCoprime, Set.Pairwise
-- 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
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
⊢ (↑S : Set ι).Pairwise fun (i j : ι) ↦ Eq (α := Ideal R) (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)

Premises used: Iff.mpr, Ideal.sup_eq_top_iff_isCoprime
-- 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
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
⊢ Finset.SupIndep.{u_2, u_3} (α := Submodule R M) S fun (i : ι) ↦ torsionBySet R M (↑(Ideal.span {q i}) : Set R)

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

Premises used: Iff.mpr, Submodule.supIndep_torsionBySet_ideal, Ideal.sup_eq_top_iff_isCoprime
-- 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
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
h : ∀ (x : ι), Eq (α := Submodule R M) (torsionBy R M (q x)) (torsionBySet R M (↑(Ideal.span {q x}) : Set R))
⊢ Finset.SupIndep.{u_2, u_3} (α := Submodule R M) S fun (i : ι) ↦ torsionBy R M (q i)

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

Premises used: Iff.mpr, Submodule.supIndep_torsionBySet_ideal, Ideal.sup_eq_top_iff_isCoprime
-- 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
S : Finset ι
q : ι → R
hq : (↑S : Set ι).Pairwise (IsCoprime on q)
x : ι
⊢ 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 : 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 (α := 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