[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ torsionOf R M 0 = ⊤
[PROOFSTEP]
simp [torsionOf]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ torsionOf R M m = ⊤ ↔ m = 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h => by simp [h]⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
h : m = 0
⊢ torsionOf R M m = ⊤
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
h : torsionOf R M m = ⊤
⊢ m = 0
[PROOFSTEP]
rw [← one_smul R m, ← mem_torsionOf_iff m (1 : R), h]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
h : torsionOf R M m = ⊤
⊢ 1 ∈ ⊤
[PROOFSTEP]
exact Submodule.mem_top
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
⊢ torsionOf R M m = ⊥ ↔ m ≠ 0
[PROOFSTEP]
refine' ⟨fun h contra => _, fun h => (Submodule.eq_bot_iff _).mpr fun r hr => _⟩
[GOAL]
case refine'_1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : torsionOf R M m = ⊥
contra : m = 0
⊢ False
[PROOFSTEP]
rw [contra, torsionOf_zero] at h
[GOAL]
case refine'_1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : ⊤ = ⊥
contra : m = 0
⊢ False
[PROOFSTEP]
exact bot_ne_top.symm h
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : m ≠ 0
r : R
hr : r ∈ torsionOf R M m
⊢ r = 0
[PROOFSTEP]
rw [mem_torsionOf_iff, smul_eq_zero] at hr
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : m ≠ 0
r : R
hr : r = 0 ∨ m = 0
⊢ r = 0
[PROOFSTEP]
tauto
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hv : CompleteLattice.Independent fun i => Submodule.span R {v i}
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
⊢ LinearIndependent R v
[PROOFSTEP]
refine' linearIndependent_iff_not_smul_mem_span.mpr fun i r hi => _
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hv : CompleteLattice.Independent fun i => Submodule.span R {v i}
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
⊢ r = 0
[PROOFSTEP]
replace hv := CompleteLattice.independent_def.mp hv i
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Disjoint (Submodule.span R {v i}) (⨆ (j : ι) (_ : j ≠ i), Submodule.span R {v j})
⊢ r = 0
[PROOFSTEP]
simp only [iSup_subtype', ← Submodule.span_range_eq_iSup, disjoint_iff] at hv
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
⊢ r = 0
[PROOFSTEP]
have : r • v i ∈ ⊥ := by
  rw [← hv, Submodule.mem_inf]
  refine' ⟨Submodule.mem_span_singleton.mpr ⟨r, rfl⟩, _⟩
  convert hi
  ext
  simp
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
⊢ r • v i ∈ ⊥
[PROOFSTEP]
rw [← hv, Submodule.mem_inf]
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
⊢ r • v i ∈ Submodule.span R {v i} ∧ r • v i ∈ Submodule.span R (Set.range fun i_1 => v ↑i_1)
[PROOFSTEP]
refine' ⟨Submodule.mem_span_singleton.mpr ⟨r, rfl⟩, _⟩
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
⊢ r • v i ∈ Submodule.span R (Set.range fun i_1 => v ↑i_1)
[PROOFSTEP]
convert hi
[GOAL]
case h.e'_5.h.e'_6
R✝ : Type u_1
M✝ : Type u_2
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
⊢ (Set.range fun i_1 => v ↑i_1) = v '' (Set.univ \ {i})
[PROOFSTEP]
ext
[GOAL]
case h.e'_5.h.e'_6.h
R✝ : Type u_1
M✝ : Type u_2
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
x✝ : M
⊢ (x✝ ∈ Set.range fun i_1 => v ↑i_1) ↔ x✝ ∈ v '' (Set.univ \ {i})
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
this : r • v i ∈ ⊥
⊢ r = 0
[PROOFSTEP]
rw [← Submodule.mem_bot R, ← h_ne_zero i]
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
this : r • v i ∈ ⊥
⊢ r ∈ torsionOf R M (v i)
[PROOFSTEP]
simpa using this
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type w
inst✝¹ : CommMonoid S
inst✝ : DistribMulAction S M
⊢ ∀ {a b : M}, a ∈ {x | ∃ a, a • x = 0} → b ∈ {x | ∃ a, a • x = 0} → a + b ∈ {x | ∃ a, a • x = 0}
[PROOFSTEP]
intro x y ⟨a, hx⟩ ⟨b, hy⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type w
inst✝¹ : CommMonoid S
inst✝ : DistribMulAction S M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
⊢ x + y ∈ {x | ∃ a, a • x = 0}
[PROOFSTEP]
use b * a
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type w
inst✝¹ : CommMonoid S
inst✝ : DistribMulAction S M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
⊢ (b * a) • (x + y) = 0
[PROOFSTEP]
rw [smul_add, mul_smul, mul_comm, mul_smul, hx, hy, smul_zero, smul_zero, add_zero]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type w
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
src✝ : AddSubmonoid M := torsion'AddSubMonoid M S
a : R
x : M
x✝ : x ∈ { toAddSubsemigroup := src✝.toAddSubsemigroup, zero_mem' := (_ : 0 ∈ src✝.carrier) }.toAddSubsemigroup.carrier
b : S
h : b • x = 0
⊢ b • a • x = 0
[PROOFSTEP]
rw [smul_comm, h, smul_zero]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
x : M
⊢ x ∈ torsionBySet R M s ↔ ∀ (a : ↑s), ↑a • x = 0
[PROOFSTEP]
refine' ⟨fun h ⟨a, ha⟩ => mem_sInf.mp h _ (Set.mem_image_of_mem _ ha), fun h => mem_sInf.mpr _⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
x : M
h : ∀ (a : ↑s), ↑a • x = 0
⊢ ∀ (p : Submodule R M), p ∈ torsionBy R M '' s → x ∈ p
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a✝ : R
x : M
h : ∀ (a : ↑s), ↑a • x = 0
a : R
ha : a ∈ s
⊢ x ∈ torsionBy R M a
[PROOFSTEP]
exact h ⟨a, ha⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
⊢ torsionBySet R M {a} = torsionBy R M a
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
x : M
⊢ x ∈ torsionBySet R M {a} ↔ x ∈ torsionBy R M a
[PROOFSTEP]
simp only [mem_torsionBySet_iff, SetCoe.forall, Subtype.coe_mk, Set.mem_singleton_iff, forall_eq, mem_torsionBy_iff]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
⊢ torsionBySet R M s = torsionBySet R M ↑(Ideal.span s)
[PROOFSTEP]
refine le_antisymm (fun x hx => ?_) (torsionBySet_le_torsionBySet_of_subset subset_span)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
x : M
hx : x ∈ torsionBySet R M s
⊢ x ∈ torsionBySet R M ↑(Ideal.span s)
[PROOFSTEP]
rw [mem_torsionBySet_iff] at hx ⊢
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ ∀ (a : ↑↑(Ideal.span s)), ↑a • x = 0
[PROOFSTEP]
suffices Ideal.span s ≤ Ideal.torsionOf R M x by
  rintro ⟨a, ha⟩
  exact this ha
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
this : Ideal.span s ≤ Ideal.torsionOf R M x
⊢ ∀ (a : ↑↑(Ideal.span s)), ↑a • x = 0
[PROOFSTEP]
rintro ⟨a, ha⟩
[GOAL]
case mk
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a✝ : R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
this : Ideal.span s ≤ Ideal.torsionOf R M x
a : R
ha : a ∈ ↑(Ideal.span s)
⊢ ↑{ val := a, property := ha } • x = 0
[PROOFSTEP]
exact this ha
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ Ideal.span s ≤ Ideal.torsionOf R M x
[PROOFSTEP]
rw [Ideal.span_le]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ s ⊆ ↑(Ideal.torsionOf R M x)
[PROOFSTEP]
exact fun a ha => hx ⟨a, ha⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a✝ a b : R
dvd : a ∣ b
⊢ torsionBy R M a ≤ torsionBy R M b
[PROOFSTEP]
rw [← torsionBySet_span_singleton_eq, ← torsionBySet_singleton_eq]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a✝ a b : R
dvd : a ∣ b
⊢ torsionBySet R M ↑(span R {a}) ≤ torsionBySet R M {b}
[PROOFSTEP]
apply torsionBySet_le_torsionBySet_of_subset
[GOAL]
case st
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a✝ a b : R
dvd : a ∣ b
⊢ {b} ⊆ ↑(span R {a})
[PROOFSTEP]
rintro c (rfl : c = b)
[GOAL]
case st
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a✝ a c : R
dvd : a ∣ c
⊢ c ∈ ↑(span R {a})
[PROOFSTEP]
exact Ideal.mem_span_singleton.mpr dvd
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
x✝ : M
h : x✝ ∈ torsionBy R M 1
⊢ x✝ ∈ ⊥
[PROOFSTEP]
rw [mem_torsionBy_iff, one_smul] at h
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
x✝ : M
h : x✝ = 0
⊢ x✝ ∈ ⊥
[PROOFSTEP]
exact h
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
⊢ torsionBySet R M Set.univ = ⊥
[PROOFSTEP]
rw [eq_bot_iff, ← torsionBy_one, ← torsionBySet_singleton_eq]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
⊢ torsionBySet R M Set.univ ≤ torsionBySet R M {1}
[PROOFSTEP]
exact torsionBySet_le_torsionBySet_of_subset fun _ _ => trivial
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
⊢ IsTorsionBySet R M {a} ↔ IsTorsionBy R M a
[PROOFSTEP]
refine' ⟨fun h x => @h _ ⟨_, Set.mem_singleton _⟩, fun h x => _⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
h : IsTorsionBy R M a
x : M
⊢ ∀ ⦃a_1 : ↑{a}⦄, ↑a_1 • x = 0
[PROOFSTEP]
rintro ⟨b, rfl : b = a⟩
[GOAL]
case mk
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
b : R
h : IsTorsionBy R M b
⊢ ↑{ val := b, property := (_ : b = b) } • x = 0
[PROOFSTEP]
exact @h _
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
h : torsionBySet R M s = ⊤
x : M
⊢ ∀ ⦃a : ↑s⦄, ↑a • x = 0
[PROOFSTEP]
rw [← mem_torsionBySet_iff, h]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
h : torsionBySet R M s = ⊤
x : M
⊢ x ∈ ⊤
[PROOFSTEP]
trivial
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
⊢ IsTorsionBy R M a ↔ torsionBy R M a = ⊤
[PROOFSTEP]
rw [← torsionBySet_singleton_eq, ← isTorsionBySet_singleton_iff, isTorsionBySet_iff_torsionBySet_eq_top]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
⊢ IsTorsionBySet R M s ↔ IsTorsionBySet R M ↑(Ideal.span s)
[PROOFSTEP]
rw [isTorsionBySet_iff_torsionBySet_eq_top, isTorsionBySet_iff_torsionBySet_eq_top, torsionBySet_eq_torsionBySet_span]
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
⊢ ⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(p i) = torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
[PROOFSTEP]
cases' S.eq_empty_or_nonempty with h h
[GOAL]
case inl
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : S = ∅
⊢ ⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(p i) = torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
[PROOFSTEP]
simp only [h]
  -- Porting note: converts were not cooperating
[GOAL]
case inl
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : S = ∅
⊢ ⨆ (i : ι) (_ : i ∈ ∅), torsionBySet R M ↑(p i) = torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ ∅), p i)
[PROOFSTEP]
convert iSup_emptyset (f := fun i => torsionBySet R M (p i))
[GOAL]
case h.e'_2.h.e'_4.h.pq.a.a
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : S = ∅
x✝ : ι
⊢ x✝ ∈ ∅ ↔ x✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
case h.e'_3
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : S = ∅
⊢ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ ∅), p i) = ⊥
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
⊢ ⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(p i) = torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inr.a
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
⊢ ⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(p i) ≤ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
[PROOFSTEP]
apply iSup_le _
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
⊢ ∀ (i : ι), ⨆ (_ : i ∈ S), torsionBySet R M ↑(p i) ≤ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
[PROOFSTEP]
intro i
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
i : ι
⊢ ⨆ (_ : i ∈ S), torsionBySet R M ↑(p i) ≤ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
[PROOFSTEP]
apply iSup_le _
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
i : ι
⊢ i ∈ S → torsionBySet R M ↑(p i) ≤ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
[PROOFSTEP]
intro is
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
i : ι
is : i ∈ S
⊢ torsionBySet R M ↑(p i) ≤ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
[PROOFSTEP]
apply torsionBySet_le_torsionBySet_of_subset
[GOAL]
case st
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
i : ι
is : i ∈ S
⊢ ↑(⨅ (i : ι) (_ : i ∈ S), p i) ⊆ ↑(p i)
[PROOFSTEP]
exact (iInf_le (fun i => ⨅ _ : i ∈ S, p i) i).trans (iInf_le _ is)
[GOAL]
case inr.a
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
⊢ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i) ≤ ⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(p i)
[PROOFSTEP]
intro x hx
[GOAL]
case inr.a
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : x ∈ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
⊢ x ∈ ⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(p i)
[PROOFSTEP]
rw [mem_iSup_finset_iff_exists_sum]
[GOAL]
case inr.a
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : x ∈ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
⊢ ∃ μ, ∑ i in S, ↑(μ i) = x
[PROOFSTEP]
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)
[GOAL]
case inr.a.intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : x ∈ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
⊢ ∃ μ, ∑ i in S, ↑(μ i) = x
[PROOFSTEP]
refine' ⟨fun i => ⟨(μ i : R) • x, _⟩, _⟩
[GOAL]
case inr.a.intro.refine'_1
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : x ∈ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
⊢ ↑(μ i) • x ∈ torsionBySet R M ↑(p i)
[PROOFSTEP]
rw [mem_torsionBySet_iff] at hx ⊢
[GOAL]
case inr.a.intro.refine'_1
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
⊢ ∀ (a : ↑↑(p i)), ↑a • ↑(μ i) • x = 0
[PROOFSTEP]
rintro ⟨a, ha⟩
[GOAL]
case inr.a.intro.refine'_1.mk
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a✝ : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ ↑{ val := a, property := ha } • ↑(μ i) • x = 0
[PROOFSTEP]
rw [smul_smul]
[GOAL]
case inr.a.intro.refine'_1.mk
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a✝ : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ (↑{ val := a, property := ha } * ↑(μ i)) • x = 0
[PROOFSTEP]
suffices : a * μ i ∈ ⨅ i ∈ S, p i
[GOAL]
case inr.a.intro.refine'_1.mk
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a✝ : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
this : a * ↑(μ i) ∈ ⨅ (i : ι) (_ : i ∈ S), p i
⊢ (↑{ val := a, property := ha } * ↑(μ i)) • x = 0
case this
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a✝ : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ a * ↑(μ i) ∈ ⨅ (i : ι) (_ : i ∈ S), p i
[PROOFSTEP]
exact hx ⟨_, this⟩
[GOAL]
case this
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a✝ : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ a * ↑(μ i) ∈ ⨅ (i : ι) (_ : i ∈ S), p i
[PROOFSTEP]
rw [mem_iInf]
[GOAL]
case this
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a✝ : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ ∀ (i_1 : ι), a * ↑(μ i) ∈ ⨅ (_ : i_1 ∈ S), p i_1
[PROOFSTEP]
intro j
[GOAL]
case this
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a✝ : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
⊢ a * ↑(μ i) ∈ ⨅ (_ : j ∈ S), p j
[PROOFSTEP]
rw [mem_iInf]
[GOAL]
case this
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a✝ : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
⊢ j ∈ S → a * ↑(μ i) ∈ p j
[PROOFSTEP]
intro hj
[GOAL]
case this
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a✝ : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
⊢ a * ↑(μ i) ∈ p j
[PROOFSTEP]
by_cases ij : j = i
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a✝ : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : j = i
⊢ a * ↑(μ i) ∈ p j
[PROOFSTEP]
rw [ij]
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a✝ : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : j = i
⊢ a * ↑(μ i) ∈ p i
[PROOFSTEP]
exact Ideal.mul_mem_right _ _ ha
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a✝ : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : ¬j = i
⊢ a * ↑(μ i) ∈ p j
[PROOFSTEP]
have := coe_mem (μ i)
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a✝ : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : ¬j = i
this : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j
⊢ a * ↑(μ i) ∈ p j
[PROOFSTEP]
simp only [mem_iInf] at this
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a✝ : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : ¬j = i
this : ∀ (i_1 : ι), i_1 ∈ S → i_1 ≠ i → ↑(μ i) ∈ p i_1
⊢ a * ↑(μ i) ∈ p j
[PROOFSTEP]
exact Ideal.mul_mem_left _ _ (this j hj ij)
[GOAL]
case inr.a.intro.refine'_2
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : x ∈ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
⊢ ∑ i in S, ↑((fun i => { val := ↑(μ i) • x, property := (_ : ↑(μ i) • x ∈ torsionBySet R M ↑(p i)) }) i) = x
[PROOFSTEP]
rw [← Finset.sum_smul, hμ, one_smul]
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
⊢ Disjoint ((fun i => torsionBySet R M ↑(p i)) i) (Finset.sup T fun i => torsionBySet R M ↑(p i))
[PROOFSTEP]
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]
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
⊢ (fun i => torsionBySet R M ↑(p i)) i ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i) = ⊥
[PROOFSTEP]
have := GaloisConnection.u_inf (b₁ := OrderDual.toDual (p i)) (b₂ := OrderDual.toDual (⨅ i ∈ T, p i)) (torsion_gc R M)
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(↑OrderDual.ofDual (↑OrderDual.toDual (p i) ⊓ ↑OrderDual.toDual (⨅ (i : ι) (_ : i ∈ T), p i))) =
    torsionBySet R M ↑(↑OrderDual.ofDual (↑OrderDual.toDual (p i))) ⊓
      torsionBySet R M ↑(↑OrderDual.ofDual (↑OrderDual.toDual (⨅ (i : ι) (_ : i ∈ T), p i)))
⊢ (fun i => torsionBySet R M ↑(p i)) i ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i) = ⊥
[PROOFSTEP]
dsimp at this ⊢
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(p i ⊔ ⨅ (i : ι) (_ : i ∈ T), p i) =
    torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i)
⊢ torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i) = ⊥
[PROOFSTEP]
rw [← this, Ideal.sup_iInf_eq_top, top_coe, torsionBySet_univ]
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(p i ⊔ ⨅ (i : ι) (_ : i ∈ T), p i) =
    torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i)
⊢ ∀ (i_1 : ι), i_1 ∈ T → p i ⊔ p i_1 = ⊤
[PROOFSTEP]
intro j hj
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(p i ⊔ ⨅ (i : ι) (_ : i ∈ T), p i) =
    torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i)
j : ι
hj : j ∈ T
⊢ p i ⊔ p j = ⊤
[PROOFSTEP]
apply hp hi (hT hj)
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(p i ⊔ ⨅ (i : ι) (_ : i ∈ T), p i) =
    torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i)
j : ι
hj : j ∈ T
⊢ i ≠ j
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(p i ⊔ ⨅ (i : ι) (_ : i ∈ T), p i) =
    torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i)
hj : i ∈ T
⊢ False
[PROOFSTEP]
exact hiT hj
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
inst✝ : DecidableEq ι
⊢ ⨆ (i : ι) (_ : i ∈ S), torsionBy R M (q i) = torsionBy R M (∏ i in S, q i)
[PROOFSTEP]
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]
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
inst✝ : DecidableEq ι
⊢ ⨆ (i : ι) (_ : i ∈ S), torsionBy R M (q i) = ⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(Ideal.span {q i})
case hp
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
inst✝ : DecidableEq ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
[PROOFSTEP]
congr
[GOAL]
case e_s
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
inst✝ : DecidableEq ι
⊢ (fun i => ⨆ (_ : i ∈ S), torsionBy R M (q i)) = fun i => ⨆ (_ : i ∈ S), torsionBySet R M ↑(Ideal.span {q i})
case hp
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
inst✝ : DecidableEq ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
[PROOFSTEP]
ext : 1
[GOAL]
case e_s.h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
inst✝ : DecidableEq ι
x✝ : ι
⊢ ⨆ (_ : x✝ ∈ S), torsionBy R M (q x✝) = ⨆ (_ : x✝ ∈ S), torsionBySet R M ↑(Ideal.span {q x✝})
case hp
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
inst✝ : DecidableEq ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
[PROOFSTEP]
congr
[GOAL]
case e_s.h.e_s
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
inst✝ : DecidableEq ι
x✝ : ι
⊢ (fun h => torsionBy R M (q x✝)) = fun h => torsionBySet R M ↑(Ideal.span {q x✝})
case hp
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
inst✝ : DecidableEq ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
[PROOFSTEP]
ext : 1
[GOAL]
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
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
inst✝ : DecidableEq ι
x✝¹ : ι
x✝ : x✝¹ ∈ S
⊢ torsionBy R M (q x✝¹) = torsionBySet R M ↑(Ideal.span {q x✝¹})
case hp
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
inst✝ : DecidableEq ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
[PROOFSTEP]
exact (torsionBySet_span_singleton_eq _).symm
[GOAL]
case hp
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
inst✝ : DecidableEq ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
[PROOFSTEP]
exact fun i hi j hj ij => (Ideal.sup_eq_top_iff_isCoprime _ _).mpr (hq hi hj ij)
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
inst✝ : DecidableEq ι
⊢ Finset.SupIndep S fun i => torsionBy R M (q i)
[PROOFSTEP]
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
[GOAL]
case h.e'_6.h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
inst✝ : DecidableEq ι
x✝ : ι
⊢ torsionBy R M (q x✝) = torsionBySet R M ↑(Ideal.span {q x✝})
[PROOFSTEP]
exact (torsionBySet_span_singleton_eq (R := R) (M := M) _).symm
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
p : ι → Ideal R
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
hM : Module.IsTorsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
⊢ ⨆ (i : { x // x ∈ S }), torsionBySet R M ↑(p ↑i) = ⊤
[PROOFSTEP]
apply (iSup_subtype'' ↑S fun i => torsionBySet R M <| p i).trans
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
p : ι → Ideal R
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
hM : Module.IsTorsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
⊢ ⨆ (t : ι) (_ : t ∈ ↑S), torsionBySet R M ↑(p t) = ⊤
[PROOFSTEP]
apply (iSup_torsionBySet_ideal_eq_torsionBySet_iInf hp).trans <| (Module.isTorsionBySet_iff_torsionBySet_eq_top _).mp hM
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
hM : Module.IsTorsionBy R M (∏ i in S, q i)
⊢ DirectSum.IsInternal fun i => torsionBy R M (q ↑i)
[PROOFSTEP]
rw [← Module.isTorsionBySet_span_singleton_iff, Ideal.submodule_span_eq, ← Ideal.finset_inf_span_singleton _ _ hq,
  Finset.inf_eq_iInf] at hM
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
hM : Module.IsTorsionBySet R M ↑(⨅ (a : ι) (_ : a ∈ S), Ideal.span {q a})
⊢ DirectSum.IsInternal fun i => torsionBy R M (q ↑i)
[PROOFSTEP]
convert torsionBySet_isInternal (fun i hi j hj ij => (Ideal.sup_eq_top_iff_isCoprime (q i) _).mpr <| hq hi hj ij) hM
[GOAL]
case h.e'_8.h
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
hM : Module.IsTorsionBySet R M ↑(⨅ (a : ι) (_ : a ∈ S), Ideal.span {q a})
x✝ : { x // x ∈ S }
⊢ torsionBy R M (q ↑x✝) = torsionBySet R M ↑(Ideal.span {q ↑x✝})
[PROOFSTEP]
exact (torsionBySet_span_singleton_eq _ (R := R) (M := M)).symm
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hM : IsTorsionBySet R M ↑I
b : R ⧸ I
x : M
b₁ b₂ : R
h : Setoid.r b₁ b₂
⊢ b₁ • x = b₂ • x
[PROOFSTEP]
have : (-b₁ + b₂) • x = 0 := @hM x ⟨_, QuotientAddGroup.leftRel_apply.mp h⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hM : IsTorsionBySet R M ↑I
b : R ⧸ I
x : M
b₁ b₂ : R
h : Setoid.r b₁ b₂
this : (-b₁ + b₂) • x = 0
⊢ b₁ • x = b₂ • x
[PROOFSTEP]
rw [add_smul, neg_smul, neg_add_eq_zero] at this
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hM : IsTorsionBySet R M ↑I
b : R ⧸ I
x : M
b₁ b₂ : R
h : Setoid.r b₁ b₂
this : b₁ • x = b₂ • x
⊢ b₁ • x = b₂ • x
[PROOFSTEP]
exact this
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hM : IsTorsionBySet R M ↑I
x : M ⧸ I • ⊤
r : ↑↑I
⊢ ↑r • x = 0
[PROOFSTEP]
induction x using Quotient.inductionOn
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hM : IsTorsionBySet R M ↑I
r : ↑↑I
a✝ : M
⊢ ↑r • Quotient.mk (Submodule.quotientRel (I • ⊤)) a✝ = 0
[PROOFSTEP]
refine' (Submodule.Quotient.mk_eq_zero _).mpr (Submodule.smul_mem_smul r.prop _)
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hM : IsTorsionBySet R M ↑I
r : ↑↑I
a✝ : M
⊢ a✝ ∈ ⊤
[PROOFSTEP]
trivial
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
s : S
x : { x // x ∈ torsion' R M S }
⊢ s • ↑x ∈ torsion' R M S
[PROOFSTEP]
obtain ⟨x, a, h⟩ := x
[GOAL]
case mk.intro
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
s : S
x : M
a : S
h : a • x = 0
⊢ s • ↑{ val := x, property := (_ : ∃ a, a • x = 0) } ∈ torsion' R M S
[PROOFSTEP]
use a
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
s : S
x : M
a : S
h : a • x = 0
⊢ a • s • ↑{ val := x, property := (_ : ∃ a, a • x = 0) } = 0
[PROOFSTEP]
dsimp
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
s : S
x : M
a : S
h : a • x = 0
⊢ a • s • x = 0
[PROOFSTEP]
rw [smul_comm, h, smul_zero]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
h : torsion' R M S = ⊤
x : M
⊢ ∃ a, a • x = 0
[PROOFSTEP]
rw [← @mem_torsion'_iff R, h]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
h : torsion' R M S = ⊤
x : M
⊢ x ∈ ⊤
[PROOFSTEP]
trivial
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ ↑(annihilator ⊤) ∩ ↑R⁰ ≠ ∅
[PROOFSTEP]
obtain ⟨S, hS⟩ := ‹Module.Finite R M›.out
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ↑(annihilator ⊤) ∩ ↑R⁰ ≠ ∅
[PROOFSTEP]
refine' Set.Nonempty.ne_empty ⟨_, _, (∏ x in S, (@hM x).choose : R⁰).prop⟩
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ↑(∏ x in S, Exists.choose (_ : ∃ a, a • x = 0)) ∈ ↑(annihilator ⊤)
[PROOFSTEP]
rw [Submonoid.coe_finset_prod, SetLike.mem_coe, ← hS, mem_annihilator_span]
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ∀ (n : ↑↑S), (∏ i in S, ↑(Exists.choose (_ : ∃ a, a • i = 0))) • ↑n = 0
[PROOFSTEP]
intro n
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
n : ↑↑S
⊢ (∏ i in S, ↑(Exists.choose (_ : ∃ a, a • i = 0))) • ↑n = 0
[PROOFSTEP]
letI := Classical.decEq M
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
n : ↑↑S
this : DecidableEq M := Classical.decEq M
⊢ (∏ i in S, ↑(Exists.choose (_ : ∃ a, a • i = 0))) • ↑n = 0
[PROOFSTEP]
rw [← Finset.prod_erase_mul _ _ n.prop, mul_smul, ← Submonoid.smul_def, (@hM n).choose_spec, smul_zero]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ ↑(torsion R M) = {x | annihilator (span R {x}) ≠ ⊥}
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
⊢ x ∈ ↑(torsion R M) ↔ x ∈ {x | annihilator (span R {x}) ≠ ⊥}
[PROOFSTEP]
simp_rw [Submodule.ne_bot_iff, mem_annihilator, mem_span_singleton]
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
⊢ x ∈ ↑(torsion R M) ↔ x ∈ {x | ∃ x_1, (∀ (n : M), (∃ a, a • x = n) → x_1 • n = 0) ∧ x_1 ≠ 0}
[PROOFSTEP]
exact
  ⟨fun ⟨a, hax⟩ =>
    ⟨a, fun _ ⟨b, hb⟩ => by rw [← hb, smul_comm, ← Submonoid.smul_def, hax, smul_zero], nonZeroDivisors.coe_ne_zero _⟩,
    fun ⟨a, hax, ha⟩ => ⟨⟨_, mem_nonZeroDivisors_of_ne_zero ha⟩, hax x ⟨1, one_smul _ _⟩⟩⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
x✝² : x ∈ ↑(torsion R M)
a : { x // x ∈ R⁰ }
hax : a • x = 0
x✝¹ : M
x✝ : ∃ a, a • x = x✝¹
b : R
hb : b • x = x✝¹
⊢ ↑a • x✝¹ = 0
[PROOFSTEP]
rw [← hb, smul_comm, ← Submonoid.smul_def, hax, smul_zero]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ NoZeroSMulDivisors R M ↔ torsion R M = ⊥
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ NoZeroSMulDivisors R M → torsion R M = ⊥
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ torsion R M = ⊥ → NoZeroSMulDivisors R M
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : NoZeroSMulDivisors R M
⊢ torsion R M = ⊥
[PROOFSTEP]
haveI : NoZeroSMulDivisors R M := h
[GOAL]
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
⊢ torsion R M = ⊥
[PROOFSTEP]
rw [eq_bot_iff]
[GOAL]
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
⊢ torsion R M ≤ ⊥
[PROOFSTEP]
rintro x ⟨a, hax⟩
[GOAL]
case mp.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
x : M
a : { x // x ∈ R⁰ }
hax : a • x = 0
⊢ x ∈ ⊥
[PROOFSTEP]
change (a : R) • x = 0 at hax
[GOAL]
case mp.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
x : M
a : { x // x ∈ R⁰ }
hax : ↑a • x = 0
⊢ x ∈ ⊥
[PROOFSTEP]
cases' eq_zero_or_eq_zero_of_smul_eq_zero hax with h0 h0
[GOAL]
case mp.intro.inl
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
x : M
a : { x // x ∈ R⁰ }
hax : ↑a • x = 0
h0 : ↑a = 0
⊢ x ∈ ⊥
[PROOFSTEP]
exfalso
[GOAL]
case mp.intro.inl.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
x : M
a : { x // x ∈ R⁰ }
hax : ↑a • x = 0
h0 : ↑a = 0
⊢ False
[PROOFSTEP]
exact nonZeroDivisors.coe_ne_zero a h0
[GOAL]
case mp.intro.inr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
x : M
a : { x // x ∈ R⁰ }
hax : ↑a • x = 0
h0 : x = 0
⊢ x ∈ ⊥
[PROOFSTEP]
exact h0
[GOAL]
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
⊢ NoZeroSMulDivisors R M
[PROOFSTEP]
exact
  {
    eq_zero_or_eq_zero_of_smul_eq_zero := fun {a} {x} hax =>
      by
      by_cases ha : a = 0
      · left
        exact ha
      · right
        rw [← mem_bot R, ← h]
        exact ⟨⟨a, mem_nonZeroDivisors_of_ne_zero ha⟩, hax⟩ }
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
a : R
x : M
hax : a • x = 0
⊢ a = 0 ∨ x = 0
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
a : R
x : M
hax : a • x = 0
ha : a = 0
⊢ a = 0 ∨ x = 0
[PROOFSTEP]
left
[GOAL]
case pos.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
a : R
x : M
hax : a • x = 0
ha : a = 0
⊢ a = 0
[PROOFSTEP]
exact ha
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
a : R
x : M
hax : a • x = 0
ha : ¬a = 0
⊢ a = 0 ∨ x = 0
[PROOFSTEP]
right
[GOAL]
case neg.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
a : R
x : M
hax : a • x = 0
ha : ¬a = 0
⊢ x = 0
[PROOFSTEP]
rw [← mem_bot R, ← h]
[GOAL]
case neg.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
a : R
x : M
hax : a • x = 0
ha : ¬a = 0
⊢ x ∈ torsion R M
[PROOFSTEP]
exact ⟨⟨a, mem_nonZeroDivisors_of_ne_zero ha⟩, hax⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : { x // x ∈ R⁰ }
hax : a • Quotient.mk'' x = 0
⊢ Quotient.mk'' x ∈ ⊥
[PROOFSTEP]
rw [Quotient.mk''_eq_mk, ← Quotient.mk_smul, Quotient.mk_eq_zero] at hax
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : { x // x ∈ R⁰ }
hax : a • x ∈ torsion R M
⊢ Quotient.mk'' x ∈ ⊥
[PROOFSTEP]
rw [mem_bot, Quotient.mk''_eq_mk, Quotient.mk_eq_zero]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : { x // x ∈ R⁰ }
hax : a • x ∈ torsion R M
⊢ x ∈ torsion R M
[PROOFSTEP]
cases' hax with b h
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a b : { x // x ∈ R⁰ }
h : b • a • x = 0
⊢ x ∈ torsion R M
[PROOFSTEP]
exact ⟨b * a, (mul_smul _ _ _).trans h⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
⊢ IsTorsion' M { x // x ∈ Submonoid.powers p } ↔ ∀ (x : M), ∃ n, p ^ n • x = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
⊢ IsTorsion' M { x // x ∈ Submonoid.powers p } → ∀ (x : M), ∃ n, p ^ n • x = 0
[PROOFSTEP]
intro h x
[GOAL]
case mp
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M { x // x ∈ Submonoid.powers p }
x : M
⊢ ∃ n, p ^ n • x = 0
[PROOFSTEP]
let ⟨⟨a, ⟨n, hn⟩⟩, hx⟩ := @h x
[GOAL]
case mp
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M { x // x ∈ Submonoid.powers p }
x : M
a : R
n : ℕ
hn : (fun x x_1 => x ^ x_1) p n = a
hx : { val := a, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) p y = a) } • x = 0
⊢ ∃ n, p ^ n • x = 0
[PROOFSTEP]
dsimp at hn
[GOAL]
case mp
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M { x // x ∈ Submonoid.powers p }
x : M
a : R
n : ℕ
hn : p ^ n = a
hx : { val := a, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) p y = a) } • x = 0
⊢ ∃ n, p ^ n • x = 0
[PROOFSTEP]
use n
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M { x // x ∈ Submonoid.powers p }
x : M
a : R
n : ℕ
hn : p ^ n = a
hx : { val := a, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) p y = a) } • x = 0
⊢ p ^ n • x = 0
[PROOFSTEP]
rw [hn]
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M { x // x ∈ Submonoid.powers p }
x : M
a : R
n : ℕ
hn : p ^ n = a
hx : { val := a, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) p y = a) } • x = 0
⊢ a • x = 0
[PROOFSTEP]
apply hx
[GOAL]
case mpr
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
⊢ (∀ (x : M), ∃ n, p ^ n • x = 0) → IsTorsion' M { x // x ∈ Submonoid.powers p }
[PROOFSTEP]
intro h x
[GOAL]
case mpr
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : ∀ (x : M), ∃ n, p ^ n • x = 0
x : M
⊢ ∃ a, a • x = 0
[PROOFSTEP]
let ⟨n, hn⟩ := h x
[GOAL]
case mpr
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : ∀ (x : M), ∃ n, p ^ n • x = 0
x : M
n : ℕ
hn : p ^ n • x = 0
⊢ ∃ a, a • x = 0
[PROOFSTEP]
exact ⟨⟨_, ⟨n, rfl⟩⟩, hn⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion' M { x // x ∈ Submonoid.powers p }
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : span R (Set.range s) = ⊤
⊢ ∃ j, IsTorsionBy R M (p ^ pOrder hM (s j))
[PROOFSTEP]
let oj := List.argmax (fun i => pOrder hM <| s i) (List.finRange d)
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion' M { x // x ∈ Submonoid.powers p }
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : span R (Set.range s) = ⊤
oj : Option (Fin d) := List.argmax (fun i => pOrder hM (s i)) (List.finRange d)
⊢ ∃ j, IsTorsionBy R M (p ^ pOrder hM (s j))
[PROOFSTEP]
have hoj : oj.isSome :=
  Option.ne_none_iff_isSome.mp fun eq_none => hd <| List.finRange_eq_nil.mp <| List.argmax_eq_none.mp eq_none
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion' M { x // x ∈ Submonoid.powers p }
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : span R (Set.range s) = ⊤
oj : Option (Fin d) := List.argmax (fun i => pOrder hM (s i)) (List.finRange d)
hoj : Option.isSome oj = true
⊢ ∃ j, IsTorsionBy R M (p ^ pOrder hM (s j))
[PROOFSTEP]
use Option.get _ hoj
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion' M { x // x ∈ Submonoid.powers p }
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : span R (Set.range s) = ⊤
oj : Option (Fin d) := List.argmax (fun i => pOrder hM (s i)) (List.finRange d)
hoj : Option.isSome oj = true
⊢ IsTorsionBy R M (p ^ pOrder hM (s (Option.get oj hoj)))
[PROOFSTEP]
rw [isTorsionBy_iff_torsionBy_eq_top, eq_top_iff, ← hs, Submodule.span_le, Set.range_subset_iff]
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion' M { x // x ∈ Submonoid.powers p }
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : span R (Set.range s) = ⊤
oj : Option (Fin d) := List.argmax (fun i => pOrder hM (s i)) (List.finRange d)
hoj : Option.isSome oj = true
⊢ ∀ (y : Fin d), s y ∈ ↑(torsionBy R M (p ^ pOrder hM (s (Option.get oj hoj))))
[PROOFSTEP]
intro i
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion' M { x // x ∈ Submonoid.powers p }
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : span R (Set.range s) = ⊤
oj : Option (Fin d) := List.argmax (fun i => pOrder hM (s i)) (List.finRange d)
hoj : Option.isSome oj = true
i : Fin d
⊢ s i ∈ ↑(torsionBy R M (p ^ pOrder hM (s (Option.get oj hoj))))
[PROOFSTEP]
change (p ^ pOrder hM (s (Option.get oj hoj))) • s i = 0
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion' M { x // x ∈ Submonoid.powers p }
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : span R (Set.range s) = ⊤
oj : Option (Fin d) := List.argmax (fun i => pOrder hM (s i)) (List.finRange d)
hoj : Option.isSome oj = true
i : Fin d
⊢ p ^ pOrder hM (s (Option.get oj hoj)) • s i = 0
[PROOFSTEP]
have : pOrder hM (s i) ≤ pOrder hM (s <| Option.get _ hoj) :=
  List.le_of_mem_argmax (List.mem_finRange i) (Option.get_mem hoj)
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion' M { x // x ∈ Submonoid.powers p }
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : span R (Set.range s) = ⊤
oj : Option (Fin d) := List.argmax (fun i => pOrder hM (s i)) (List.finRange d)
hoj : Option.isSome oj = true
i : Fin d
this : pOrder hM (s i) ≤ pOrder hM (s (Option.get oj hoj))
⊢ p ^ pOrder hM (s (Option.get oj hoj)) • s i = 0
[PROOFSTEP]
rw [← Nat.sub_add_cancel this, pow_add, mul_smul, pow_pOrder_smul, smul_zero]
[GOAL]
R✝ : Type u_1
M : Type u_2
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
⊢ torsionBy R (R ⧸ Submodule.span R {a * b}) a = Submodule.span R {↑(mk (Submodule.span R {a * b})) b}
[PROOFSTEP]
ext x
[GOAL]
case h
R✝ : Type u_1
M : Type u_2
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R ⧸ Submodule.span R {a * b}
⊢ x ∈ torsionBy R (R ⧸ Submodule.span R {a * b}) a ↔ x ∈ Submodule.span R {↑(mk (Submodule.span R {a * b})) b}
[PROOFSTEP]
rw [mem_torsionBy_iff, Submodule.mem_span_singleton]
[GOAL]
case h
R✝ : Type u_1
M : Type u_2
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R ⧸ Submodule.span R {a * b}
⊢ a • x = 0 ↔ ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = x
[PROOFSTEP]
obtain ⟨x, rfl⟩ := mk_surjective x
[GOAL]
case h.intro
R✝ : Type u_1
M : Type u_2
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
⊢ a • ↑(mk (Submodule.span R {a * b})) x = 0 ↔
    ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
[PROOFSTEP]
constructor
[GOAL]
case h.intro.mp
R✝ : Type u_1
M : Type u_2
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
⊢ a • ↑(mk (Submodule.span R {a * b})) x = 0 →
    ∃ a_2, a_2 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
[PROOFSTEP]
intro h
[GOAL]
case h.intro.mpr
R✝ : Type u_1
M : Type u_2
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
⊢ (∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x) →
    a • ↑(mk (Submodule.span R {a * b})) x = 0
[PROOFSTEP]
intro h
[GOAL]
case h.intro.mp
R✝ : Type u_1
M : Type u_2
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : a • ↑(mk (Submodule.span R {a * b})) x = 0
⊢ ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
[PROOFSTEP]
rw [← mk_eq_mk, ← Quotient.mk_smul, Quotient.mk_eq_zero, Submodule.mem_span_singleton] at h
[GOAL]
case h.intro.mp
R✝ : Type u_1
M : Type u_2
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : ∃ a_1, a_1 • (a * b) = a • x
⊢ ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
[PROOFSTEP]
obtain ⟨c, h⟩ := h
[GOAL]
case h.intro.mp.intro
R✝ : Type u_1
M : Type u_2
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c • (a * b) = a • x
⊢ ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
[PROOFSTEP]
rw [smul_eq_mul, smul_eq_mul, mul_comm, mul_assoc, mul_cancel_left_mem_nonZeroDivisors ha, mul_comm] at h
[GOAL]
case h.intro.mp.intro
R✝ : Type u_1
M : Type u_2
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c * b = x
⊢ ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
[PROOFSTEP]
use c
[GOAL]
case h
R✝ : Type u_1
M : Type u_2
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c * b = x
⊢ c • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
[PROOFSTEP]
rw [← h, ← mk_eq_mk, ← Quotient.mk_smul, smul_eq_mul, mk_eq_mk]
[GOAL]
case h.intro.mpr
R✝ : Type u_1
M : Type u_2
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
⊢ a • ↑(mk (Submodule.span R {a * b})) x = 0
[PROOFSTEP]
obtain ⟨c, h⟩ := h
[GOAL]
case h.intro.mpr.intro
R✝ : Type u_1
M : Type u_2
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
⊢ a • ↑(mk (Submodule.span R {a * b})) x = 0
[PROOFSTEP]
rw [← h, smul_comm, ← mk_eq_mk, ← Quotient.mk_smul, (Quotient.mk_eq_zero _).mpr <| mem_span_singleton_self _, smul_zero]
[GOAL]
R : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
⊢ IsTorsion M ↔ Module.IsTorsion ℕ M
[PROOFSTEP]
refine' ⟨fun h x => _, fun h x => _⟩
[GOAL]
case refine'_1
R : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
h : IsTorsion M
x : M
⊢ ∃ a, a • x = 0
[PROOFSTEP]
obtain ⟨n, h0, hn⟩ := (isOfFinAddOrder_iff_nsmul_eq_zero x).mp (h x)
[GOAL]
case refine'_1.intro.intro
R : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
h : IsTorsion M
x : M
n : ℕ
h0 : 0 < n
hn : n • x = 0
⊢ ∃ a, a • x = 0
[PROOFSTEP]
exact ⟨⟨n, mem_nonZeroDivisors_of_ne_zero <| ne_of_gt h0⟩, hn⟩
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
h : Module.IsTorsion ℕ M
x : M
⊢ IsOfFinAddOrder x
[PROOFSTEP]
rw [isOfFinAddOrder_iff_nsmul_eq_zero]
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
h : Module.IsTorsion ℕ M
x : M
⊢ ∃ n, 0 < n ∧ n • x = 0
[PROOFSTEP]
obtain ⟨n, hn⟩ := @h x
[GOAL]
case refine'_2.intro
R : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
h : Module.IsTorsion ℕ M
x : M
n : { x // x ∈ ℕ⁰ }
hn : n • x = 0
⊢ ∃ n, 0 < n ∧ n • x = 0
[PROOFSTEP]
refine' ⟨n, Nat.pos_of_ne_zero (nonZeroDivisors.coe_ne_zero _), hn⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝ : AddCommGroup M
⊢ IsTorsion M ↔ Module.IsTorsion ℤ M
[PROOFSTEP]
refine' ⟨fun h x => _, fun h x => _⟩
[GOAL]
case refine'_1
R : Type u_1
M : Type u_2
inst✝ : AddCommGroup M
h : IsTorsion M
x : M
⊢ ∃ a, a • x = 0
[PROOFSTEP]
obtain ⟨n, h0, hn⟩ := (isOfFinAddOrder_iff_nsmul_eq_zero x).mp (h x)
[GOAL]
case refine'_1.intro.intro
R : Type u_1
M : Type u_2
inst✝ : AddCommGroup M
h : IsTorsion M
x : M
n : ℕ
h0 : 0 < n
hn : n • x = 0
⊢ ∃ a, a • x = 0
[PROOFSTEP]
exact ⟨⟨n, mem_nonZeroDivisors_of_ne_zero <| ne_of_gt <| Int.coe_nat_pos.mpr h0⟩, (coe_nat_zsmul _ _).trans hn⟩
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝ : AddCommGroup M
h : Module.IsTorsion ℤ M
x : M
⊢ IsOfFinAddOrder x
[PROOFSTEP]
rw [isOfFinAddOrder_iff_nsmul_eq_zero]
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝ : AddCommGroup M
h : Module.IsTorsion ℤ M
x : M
⊢ ∃ n, 0 < n ∧ n • x = 0
[PROOFSTEP]
obtain ⟨n, hn⟩ := @h x
[GOAL]
case refine'_2.intro
R : Type u_1
M : Type u_2
inst✝ : AddCommGroup M
h : Module.IsTorsion ℤ M
x : M
n : { x // x ∈ ℤ⁰ }
hn : n • x = 0
⊢ ∃ n, 0 < n ∧ n • x = 0
[PROOFSTEP]
exact exists_nsmul_eq_zero_of_zsmul_eq_zero (nonZeroDivisors.coe_ne_zero n) hn


[GOAL]
α : Type u
inst✝ : AddZeroClass α
⊢ unop 0 = 0
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : AddMonoid α
⊢ unop 0 = 0
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : AddMonoidWithOne α
src✝² : AddMonoid αᵐᵒᵖ := addMonoid α
src✝¹ : One αᵐᵒᵖ := one α
src✝ : NatCast αᵐᵒᵖ := natCast α
⊢ op ↑0 = 0
[PROOFSTEP]
rw [Nat.cast_zero, op_zero]
[GOAL]
α : Type u
inst✝ : AddMonoidWithOne α
src✝² : AddMonoid αᵐᵒᵖ := addMonoid α
src✝¹ : One αᵐᵒᵖ := one α
src✝ : NatCast αᵐᵒᵖ := natCast α
⊢ ∀ (n : ℕ), op ↑(n + 1) = op ↑n + 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : SubNegMonoid α
⊢ unop 0 = 0
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : AddGroup α
⊢ unop 0 = 0
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : AddGroupWithOne α
src✝¹ : AddMonoidWithOne αᵐᵒᵖ := addMonoidWithOne α
src✝ : AddGroup αᵐᵒᵖ := addGroup α
n : ℕ
⊢ op ↑↑n = op ↑n
[PROOFSTEP]
rw [Int.cast_ofNat]
[GOAL]
α : Type u
inst✝ : AddGroupWithOne α
src✝¹ : AddMonoidWithOne αᵐᵒᵖ := addMonoidWithOne α
src✝ : AddGroup αᵐᵒᵖ := addGroup α
n : ℕ
⊢ op ↑(Int.negSucc n) = op (-unop (op ↑(n + 1)))
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : DivInvMonoid α
src✝¹ : Monoid αᵐᵒᵖ := monoid α
src✝ : Inv αᵐᵒᵖ := inv α
n : ℕ
x : αᵐᵒᵖ
⊢ unop ((fun n x => op (unop x ^ n)) (Int.ofNat (Nat.succ n)) x) =
    unop (x * (fun n x => op (unop x ^ n)) (Int.ofNat n) x)
[PROOFSTEP]
simp only [Int.ofNat_eq_coe]
[GOAL]
α : Type u
inst✝ : DivInvMonoid α
src✝¹ : Monoid αᵐᵒᵖ := monoid α
src✝ : Inv αᵐᵒᵖ := inv α
n : ℕ
x : αᵐᵒᵖ
⊢ unop (op (unop x ^ ↑(Nat.succ n))) = unop (x * op (unop x ^ ↑n))
[PROOFSTEP]
rw [unop_op, zpow_ofNat, pow_succ', unop_mul, unop_op, zpow_ofNat]
[GOAL]
α : Type u
inst✝ : DivInvMonoid α
x y : α
⊢ op (x / y) = (op y)⁻¹ * op x
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u
inst✝ : Mul α
a x y : α
⊢ SemiconjBy (op a) (op y) (op x) ↔ SemiconjBy a x y
[PROOFSTEP]
simp only [SemiconjBy, ← op_mul, op_inj, eq_comm]
[GOAL]
α : Type u
inst✝ : Mul α
a x y : αᵐᵒᵖ
⊢ SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y
[PROOFSTEP]
conv_rhs => rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]
[GOAL]
α : Type u
inst✝ : Mul α
a x y : αᵐᵒᵖ
| SemiconjBy a x y
[PROOFSTEP]
rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]
[GOAL]
α : Type u
inst✝ : Mul α
a x y : αᵐᵒᵖ
| SemiconjBy a x y
[PROOFSTEP]
rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]
[GOAL]
α : Type u
inst✝ : Mul α
a x y : αᵐᵒᵖ
| SemiconjBy a x y
[PROOFSTEP]
rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]
[GOAL]
α : Type u
inst✝ : MulOneClass α
⊢ unop 1 = 1
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : Monoid α
⊢ unop 1 = 1
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : CommMonoid α
⊢ unop 1 = 1
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : DivInvMonoid α
⊢ unop 1 = 1
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : Group α
⊢ unop 1 = 1
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : CommGroup α
⊢ unop 1 = 1
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : AddCommMonoidWithOne α
src✝² : AddCommMonoid αᵃᵒᵖ := addCommMonoid α
src✝¹ : One αᵃᵒᵖ := one
src✝ : NatCast αᵃᵒᵖ := natCast α
⊢ op ↑0 = 0
[PROOFSTEP]
rw [Nat.cast_zero, op_zero]
[GOAL]
α : Type u
inst✝ : AddCommMonoidWithOne α
src✝² : AddCommMonoid αᵃᵒᵖ := addCommMonoid α
src✝¹ : One αᵃᵒᵖ := one
src✝ : NatCast αᵃᵒᵖ := natCast α
⊢ ∀ (n : ℕ), op ↑(n + 1) = op ↑n + 1
[PROOFSTEP]
simp [add_comm]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
hf : ∀ (x y : M), Commute (↑f x) (↑f y)
x y : M
⊢ (op ∘ ↑f) (x * y) = (op ∘ ↑f) x * (op ∘ ↑f) y
[PROOFSTEP]
simp [(hf x y).eq]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
hf : ∀ (x y : M), Commute (↑f x) (↑f y)
x y : M
⊢ OneHom.toFun { toFun := op ∘ ↑f, map_one' := (_ : op (↑f 1) = op 1) } (x * y) =
    OneHom.toFun { toFun := op ∘ ↑f, map_one' := (_ : op (↑f 1) = op 1) } x *
      OneHom.toFun { toFun := op ∘ ↑f, map_one' := (_ : op (↑f 1) = op 1) } y
[PROOFSTEP]
simp [(hf x y).eq]
[GOAL]
α : Type u
M : Type ?u.46725
inst✝ : Monoid M
x : Mᵐᵒᵖˣ
⊢ ↑((fun X =>
          MulOpposite.rec'
            (fun u =>
              { val := op ↑u, inv := op ↑u⁻¹, val_inv := (_ : op ↑u * op ↑u⁻¹ = 1),
                inv_val := (_ : op ↑u⁻¹ * op ↑u = 1) })
            X)
        ((fun u =>
            op
              { val := unop ↑u, inv := unop ↑u⁻¹, val_inv := (_ : unop ↑u * unop ↑u⁻¹ = 1),
                inv_val := (_ : unop ↑u⁻¹ * unop ↑u = 1) })
          x)) =
    ↑x
[PROOFSTEP]
simp
[GOAL]
α : Type u
M : Type ?u.46725
inst✝ : Monoid M
x : Mˣᵐᵒᵖ
⊢ ↑(unop
        ((fun u =>
            op
              { val := unop ↑u, inv := unop ↑u⁻¹, val_inv := (_ : unop ↑u * unop ↑u⁻¹ = 1),
                inv_val := (_ : unop ↑u⁻¹ * unop ↑u = 1) })
          ((fun X =>
              MulOpposite.rec'
                (fun u =>
                  { val := op ↑u, inv := op ↑u⁻¹, val_inv := (_ : op ↑u * op ↑u⁻¹ = 1),
                    inv_val := (_ : op ↑u⁻¹ * op ↑u = 1) })
                X)
            x))) =
    ↑(unop x)
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u
α : Type ?u.65550
β : Type ?u.65553
inst✝¹ : Mul α
inst✝ : Mul β
f : αᵐᵒᵖ ≃* βᵐᵒᵖ
x : α
⊢ (unop ∘ ↑(symm f) ∘ MulOpposite.op) ((unop ∘ ↑f ∘ MulOpposite.op) x) = x
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
α : Type ?u.65550
β : Type ?u.65553
inst✝¹ : Mul α
inst✝ : Mul β
f : αᵐᵒᵖ ≃* βᵐᵒᵖ
x : β
⊢ (unop ∘ ↑f ∘ MulOpposite.op) ((unop ∘ ↑(symm f) ∘ MulOpposite.op) x) = x
[PROOFSTEP]
simp


[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
mul_left_inv : ∀ (a : G), a⁻¹ * a = 1
a : G
⊢ a * 1 = a
[PROOFSTEP]
have mul_right_inv : ∀ a, a * a⁻¹ = 1 := fun a =>
  calc
    a * a⁻¹ = 1 * (a * a⁻¹) := (one_mul _).symm
    _ = ((a * a⁻¹)⁻¹ * (a * a⁻¹)) * (a * a⁻¹) := by rw [mul_left_inv]
    _ = (a * a⁻¹)⁻¹ * (a * ((a⁻¹ * a) * a⁻¹)) := by simp only [assoc]
    _ = 1 := by rw [mul_left_inv, one_mul, mul_left_inv]
[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
mul_left_inv : ∀ (a : G), a⁻¹ * a = 1
a✝ a : G
⊢ 1 * (a * a⁻¹) = (a * a⁻¹)⁻¹ * (a * a⁻¹) * (a * a⁻¹)
[PROOFSTEP]
rw [mul_left_inv]
[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
mul_left_inv : ∀ (a : G), a⁻¹ * a = 1
a✝ a : G
⊢ (a * a⁻¹)⁻¹ * (a * a⁻¹) * (a * a⁻¹) = (a * a⁻¹)⁻¹ * (a * (a⁻¹ * a * a⁻¹))
[PROOFSTEP]
simp only [assoc]
[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
mul_left_inv : ∀ (a : G), a⁻¹ * a = 1
a✝ a : G
⊢ (a * a⁻¹)⁻¹ * (a * (a⁻¹ * a * a⁻¹)) = 1
[PROOFSTEP]
rw [mul_left_inv, one_mul, mul_left_inv]
[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
mul_left_inv : ∀ (a : G), a⁻¹ * a = 1
a : G
mul_right_inv : ∀ (a : G), a * a⁻¹ = 1
⊢ a * 1 = a
[PROOFSTEP]
rw [← mul_left_inv a, ← assoc, mul_right_inv a, one_mul]
[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_right_inv : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * a * 1 = a⁻¹ * a * (a⁻¹ * a * (a⁻¹ * a)⁻¹)
[PROOFSTEP]
rw [mul_right_inv]
[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_right_inv : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * a * (a⁻¹ * a * (a⁻¹ * a)⁻¹) = a⁻¹ * (a * a⁻¹) * a * (a⁻¹ * a)⁻¹
[PROOFSTEP]
simp only [assoc]
[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_right_inv : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * (a * a⁻¹) * a * (a⁻¹ * a)⁻¹ = 1
[PROOFSTEP]
rw [mul_right_inv, mul_one, mul_right_inv]
[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_right_inv : ∀ (a : G), a * a⁻¹ = 1
mul_left_inv : ∀ (a : G), a⁻¹ * a = 1
a : G
⊢ 1 * a = a
[PROOFSTEP]
rw [← mul_right_inv a, assoc, mul_left_inv, mul_one]


[GOAL]
α : Type u
β : Type v
inst✝ : Finite α
⊢ α ≃ Additive α
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
inst✝ : Finite α
⊢ α ≃ Multiplicative α
[PROOFSTEP]
rfl