awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
m : M
refine_1 : ∀ (h : Eq (α := Ideal R) (torsionOf R M m) ⊥) (contra : m = 0), False
refine_2 : ∀ (h : m ≠ 0) (r : R) (hr : Membership.mem (γ := Submodule R R) (torsionOf R M m) r), r = 0
⊢ Eq (α := Ideal R) (torsionOf R M m) ⊥ ↔ m ≠ 0

Tactic:
refine ⟨fun h contra => ?_, fun h => (Submodule.eq_bot_iff _).mpr fun r hr => ?_⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
m : M
h : Eq (α := Ideal R) (torsionOf R M m) ⊥
contra : m = 0
⊢ Eq.{u_1 + 1} (α := Ideal R) ⊤ ⊥

Tactic:
rw [contra, torsionOf_zero] at h

Premises used: Ideal.torsionOf_zero
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
m : M
h : Eq (α := Ideal R) (torsionOf R M m) ⊥
contra : m = 0
h₁ : Eq.{u_1 + 1} (α := Ideal R) ⊤ ⊥
⊢ m = 0

Tactic:
rw [contra, torsionOf_zero] at h

Premises used: Ideal.torsionOf_zero
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
m : M
h : Eq.{u_1 + 1} (α := Ideal R) ⊤ ⊥
contra : m = 0
⊢ False

Tactic:
bot_ne_top.symm h

Premises used: Ne.symm, bot_ne_top
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
m : M
h : Eq.{u_1 + 1} (α := Ideal R) ⊤ ⊥
contra : m = 0
⊢ False

Tactic:
exact bot_ne_top.symm h

Premises used: Ne.symm, bot_ne_top
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
m : M
h : m ≠ 0
r : R
hr : Membership.mem (γ := Submodule R R) (torsionOf R M m) r
⊢ r = 0 ∨ m = 0

Tactic:
rw [mem_torsionOf_iff, smul_eq_zero] at hr

Premises used: Ideal.mem_torsionOf_iff, smul_eq_zero
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
m : M
h : m ≠ 0
r : R
hr : r = 0 ∨ m = 0
refine_2 : ∀ (hr : r = 0), r = 0
refine_2₁ : ∀ (hr : m = 0), r = 0
refine_2₂ refine_2₃ : ∀ (hr : r = 0), r = 0
⊢ r = 0

Tactic:
tauto
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Eq (α := Ideal R) (Submodule.annihilator (M := M) (R ∙ x)) (torsionOf R M x)

Tactic:
simpa [torsionOf] using Submodule.annihilator_span_singleton x

Premises used: Submodule.annihilator_span_singleton, Ideal.torsionOf
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h :
  ∀ (r : R),
    Membership.mem (γ := Ideal R) (annihilator R M) r ↔ Membership.mem (γ := Ideal R) (⨅ (x : M), torsionOf R M x) r
⊢ Eq (α := Ideal R) (annihilator R M) (⨅ (x : M), torsionOf R M x)

Tactic:
ext r
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
⊢ Membership.mem (γ := Ideal R) (annihilator R M) r ↔ Membership.mem (γ := Ideal R) (⨅ (x : M), torsionOf R M x) r

Tactic:
simp [Module.mem_annihilator]

Premises used: Module.mem_annihilator
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
hv : iSupIndep.{u_3 + 1, u_5} (α := Submodule R M) fun (i : ι) ↦ R ∙ v i
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
⊢ LinearIndependent R v

Tactic:
linearIndependent_iff_eq_zero_of_smul_mem_span.mpr fun i r hi => ?_

Premises used: Iff.mpr, linearIndependent_iff_eq_zero_of_smul_mem_span
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
hv : iSupIndep.{u_3 + 1, u_5} (α := Submodule R M) fun (i : ι) ↦ R ∙ v i
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
refine :
  ∀ (i : ι) (r : R) (hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)),
    r = 0
⊢ LinearIndependent R v

Tactic:
refine linearIndependent_iff_eq_zero_of_smul_mem_span.mpr fun i r hi => ?_

Premises used: Iff.mpr, linearIndependent_iff_eq_zero_of_smul_mem_span
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
hv : iSupIndep.{u_3 + 1, u_5} (α := Submodule R M) fun (i : ι) ↦ R ∙ v i
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
⊢ Disjoint (α := Submodule R M) (R ∙ v i) (⨆ (j : ι), ⨆ (_ : j ≠ i), R ∙ v j)

Tactic:
replace hv := iSupIndep_def.mp hv i
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv : Disjoint (α := Submodule R M) (R ∙ v i) (⨆ (j : ι), ⨆ (_ : j ≠ i), R ∙ v j)
⊢ Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥

Tactic:
simp only [iSup_subtype', ← Submodule.span_range_eq_iSup (ι := Subtype _), disjoint_iff] at hv

Premises used: iSup_subtype', disjoint_iff, Submodule.span_range_eq_iSup
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv :
  Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥
rw :
  Membership.mem (γ := Submodule R M) (R ∙ v i) (r • v i) ∧
    Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι)))
      (r • v i)
⊢ Membership.mem (γ := Submodule R M) ⊥ (r • v i)

Tactic:
rw [← hv, Submodule.mem_inf]

Premises used: Submodule.mem_inf
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv :
  Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥
⊢ Membership.mem (γ := Submodule R M) (R ∙ v i) (r • v i) ∧
    Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι)))
      (r • v i)

Tactic:
⟨Submodule.mem_span_singleton.mpr ⟨r, rfl⟩, ?_⟩

Premises used: Iff.mpr, Submodule.mem_span_singleton, And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv :
  Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥
refine :
  Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι)))
    (r • v i)
⊢ Membership.mem (γ := Submodule R M) (R ∙ v i) (r • v i) ∧
    Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι)))
      (r • v i)

Tactic:
refine ⟨Submodule.mem_span_singleton.mpr ⟨r, rfl⟩, ?_⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv :
  Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)

Tactic:
hi
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv :
  Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥
h : (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι)) = v '' (Set.univ \ {i})
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι)))
    (r • v i)

Tactic:
convert! hi
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv :
  Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥
h :
  ∀ (x : M),
    Membership.mem (γ := Set M) (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι)) x ↔
      x ∈ v '' (Set.univ \ {i})
⊢ (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι)) = v '' (Set.univ \ {i})

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv :
  Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥
x : M
⊢ Membership.mem (γ := Set M) (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι)) x ↔
    x ∈ v '' (Set.univ \ {i})

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv :
  Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥
⊢ Membership.mem (γ := Submodule R M) ⊥ (r • v i)

Tactic:
have : r • v i ∈ (⊥ : Submodule R M) := by
    rw [← hv, Submodule.mem_inf]
    refine ⟨Submodule.mem_span_singleton.mpr ⟨r, rfl⟩, ?_⟩
    convert! hi
    ext
    simp
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv :
  Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥
this : Membership.mem (γ := Submodule R M) ⊥ (r • v i)
rw : Membership.mem (γ := Submodule R R) (torsionOf R M (v i)) r
⊢ r = 0

Tactic:
rw [← Submodule.mem_bot R, ← h_ne_zero i]

Premises used: Submodule.mem_bot
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_ne_zero : ∀ (i : ι), Eq (α := Ideal R) (torsionOf R M (v i)) ⊥
i : ι
r : R
hi : Membership.mem (γ := Submodule R M) (Submodule.span R (v '' (Set.univ \ {i}))) (r • v i)
hv :
  Eq (α := Submodule R M) (R ∙ v i ⊓ Submodule.span R (Set.range fun (i_1 : { i_1 : ι // i_1 ≠ i }) ↦ v (↑i_1 : ι))) ⊥
this : Membership.mem (γ := Submodule R M) ⊥ (r • v i)
⊢ Membership.mem (γ := Submodule R R) (torsionOf R M (v i)) r

Tactic:
simpa using this
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
a : R
⊢ ((quotTorsionOfEquivSpanSingleton R M x :
          LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id R) (HasQuotient.Quotient R (B := Ideal R) (torsionOf R M x))
            ↥(R ∙ x)) :
        (a : R ⧸ torsionOf R M x) → ↥(R ∙ x))
      (Submodule.Quotient.mk a) =
    HSMul.hSMul (β := ↥(R ∙ x)) a
      (Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ x) x_1) x ⋯)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
x y : M
this :
  ∀ (a : S) (hx : a • x = 0),
    Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} y →
      Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} (x + y)
⊢ Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} x →
    Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} y →
      Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} (x + y)

Tactic:
⟨a,hx⟩
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
this : ∀ (b : S) (hy : b • y = 0), Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} (x + y)
⊢ Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} y →
    Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} (x + y)

Tactic:
⟨b,hy⟩
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
h : (b * a) • (x + y) = 0
⊢ Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} (x + y)

Tactic:
use b * a
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
h : (b * a) • x + (b * a) • y = 0
h₁ : b • a • x + (b * a) • y = 0
h₂ : b • a • x + (a * b) • y = 0
h₃ : b • a • x + a • b • y = 0
h₄ : HSMul.hSMul (β := M) b 0 + a • b • y = 0
h₅ : HSMul.hSMul (β := M) b 0 + HSMul.hSMul (β := M) a 0 = 0
h₆ : 0 + HSMul.hSMul (β := M) a 0 = 0
h₇ : HAdd.hAdd (α := M) 0 0 = 0
h₈ h₉ : Eq.{u_2 + 1} (α := M) 0 0
⊢ (b * a) • (x + y) = 0

Tactic:
rw [smul_add, mul_smul, mul_comm, mul_smul, hx, hy, smul_zero, smul_zero, add_zero]

Premises used: smul_zero, mul_comm, add_zero, SemigroupAction.mul_smul, smul_add
-- 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
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
a : R
x : M
h_1 : Membership.mem (γ := Set M) {x : M | ∃ (a : S), a • x = 0} x
b : S
h : b • x = 0
rw : a • b • x = 0
rw₁ : HSMul.hSMul (β := M) a 0 = 0
rw₂ rw₃ : Eq.{u_2 + 1} (α := M) 0 0
⊢ b • a • x = 0

Tactic:
rw [smul_comm, h, smul_zero]

Premises used: smul_zero, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ IsTorsionBySet R M (↑(annihilator R M) : Set R)

Tactic:
fun _ r ↦ Module.mem_annihilator.mp r.2 _

Premises used: Module.mem_annihilator, Iff.mp, Subtype.property
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : R
rw : (∀ ⦃x : M⦄, a • x = 0) ↔ Membership.mem (γ := Ideal R) (annihilator R M) a
rw₁ rw₂ : (∀ ⦃x : M⦄, a • x = 0) ↔ ∀ (m : M), a • m = 0
⊢ IsTorsionBy R M a ↔ Membership.mem (γ := Ideal R) (annihilator R M) a

Tactic:
rw [IsTorsionBy, mem_annihilator]

Premises used: Module.mem_annihilator, Module.IsTorsionBy
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
simp_rw : (∀ ⦃x : M⦄ ⦃a : (↑s : Type u_1)⦄, (↑a : R) • x = 0) ↔ ∀ x ∈ s, ∀ (m : M), x • m = 0
⊢ IsTorsionBySet R M s ↔ s ⊆ (↑(annihilator R M) : Set R)

Tactic:
simp_rw [IsTorsionBySet, Set.subset_def, SetLike.mem_coe, mem_annihilator]

Premises used: Module.mem_annihilator, Module.IsTorsionBySet, Set.subset_def, SetLike.mem_coe
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
rw : (∀ (b : (↑s : Type u_1)) (a : M), (↑b : R) • a = 0) ↔ ∀ x ∈ s, ∀ (m : M), x • m = 0
rw₁ rw₂ :
  (∀ (x : R) (h : x ∈ s) (a : M), (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) x h) : R) • a = 0) ↔
    ∀ x ∈ s, ∀ (m : M), x • m = 0
⊢ (∀ ⦃x : M⦄ ⦃a : (↑s : Type u_1)⦄, (↑a : R) • x = 0) ↔ ∀ x ∈ s, ∀ (m : M), x • m = 0

Tactic:
rw [forall_comm, SetCoe.forall]

Premises used: forall_comm, SetCoe.forall
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_2
M : Type u_1
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
⊢ IsSMulRegular M r ↔ Eq (α := Submodule R M) (Submodule.torsionBy R M r) ⊥

Tactic:
(DistribSMul.toLinearMap R M r).ker_eq_bot.symm

Premises used: LinearMap.ker_eq_bot, Submodule.torsionBy, IsSMulRegular, Iff.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
a : R
x : ↥(torsionBy R M a)
⊢ a • x = 0

Tactic:
Subtype.ext x.prop

Premises used: Subtype.prop, Subtype.ext
-- 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
a : R
x : ↥(torsionBy R M a)
⊢ a • (↑x : M) = 0

Tactic:
x.prop

Premises used: Set.Mem, setOf, Set.preimage, Subtype.prop, Set.singleton
-- 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
a : R
x : M
⊢ Membership.mem (γ := Submodule R M) (torsionBy R M a) x ↔ a • x = 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.singleton
-- 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
s : Set R
x : M
⊢ Membership.mem (γ := Submodule R M) (torsionBySet R M s) x ↔ ∀ (a : (↑s : Type u_1)), (↑a : R) • x = 0

Tactic:
⟨fun h ⟨a, ha⟩ => mem_sInf.mp h _ (Set.mem_image_of_mem _ ha), fun h => mem_sInf.mpr ?_⟩

Premises used: Iff.mpr, Submodule.torsionBy, Set.mem_image_of_mem, Iff.intro, Iff.mp, Submodule.mem_sInf, HSMul.hSMul, OfNat.ofNat, Subtype.val, Eq, _private.0.Submodule.mem_torsionBySet_iff.match_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
s : Set R
x : M
refine :
  ∀ (h : ∀ (a : (↑s : Type u_1)), (↑a : R) • x = 0) (p : Submodule R M),
    Membership.mem (γ := Set (Submodule R M)) (torsionBy R M '' s) p → x ∈ p
⊢ Membership.mem (γ := Submodule R M) (torsionBySet R M s) x ↔ ∀ (a : (↑s : Type u_1)), (↑a : R) • x = 0

Tactic:
refine ⟨fun h ⟨a, ha⟩ => mem_sInf.mp h _ (Set.mem_image_of_mem _ ha), fun h => mem_sInf.mpr ?_⟩
-- 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
s : Set R
x : M
h : ∀ (a : (↑s : Type u_1)), (↑a : R) • x = 0
a : R
ha : a ∈ s
⊢ Membership.mem (γ := Submodule R M) (torsionBy R M a) x

Tactic:
h ⟨a, ha⟩

Premises used: Set.Mem, setOf, Subtype.mk, Set.preimage, Set.singleton
-- 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
s : Set R
x : M
h : ∀ (a : (↑s : Type u_1)), (↑a : R) • x = 0
a : R
ha : a ∈ s
⊢ Membership.mem (γ := Submodule R M) (torsionBy R M a) x

Tactic:
exact h ⟨a, ha⟩

Premises used: Subtype.mk
-- 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
a : R
h :
  ∀ (x : M),
    Membership.mem (γ := Submodule R M) (torsionBySet R M {a}) x ↔
      Membership.mem (γ := Submodule R M) (torsionBy R M a) x
⊢ Eq (α := Submodule R M) (torsionBySet R M {a}) (torsionBy R M a)

Tactic:
ext x
-- 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
a : R
x : M
⊢ Membership.mem (γ := Submodule R M) (torsionBySet R M {a}) x ↔ Membership.mem (γ := Submodule R M) (torsionBy R M a) x

Tactic:
simp only [mem_torsionBySet_iff, SetCoe.forall, Set.mem_singleton_iff, forall_eq,
    mem_torsionBy_iff]

Premises used: Submodule.mem_torsionBySet_iff, forall_eq, Set.mem_singleton_iff, Submodule.mem_torsionBy_iff, SetCoe.forall
-- 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
s t : Set R
st : s ⊆ t
⊢ LE.le (α := Submodule R M) (torsionBySet R M t) (torsionBySet R M s)

Tactic:
sInf_le_sInf fun _ ⟨a, ha, h⟩ => ⟨a, st ha, h⟩

Premises used: Set.Mem, Submodule.torsionBy, sInf_le_sInf, Membership.mem, And.intro, Exists.intro, Set.image, _private.0.Submodule.torsionBySet_le_torsionBySet_of_subset.match_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
i j : ℕ
h : i ≤ j
I : Ideal R
⊢ LE.le (α := Submodule R M) (torsionBySet R M (↑(I ^ i) : Set R)) (torsionBySet R M (↑(I ^ j) : Set R))

Tactic:
torsionBySet_le_torsionBySet_of_subset (Ideal.pow_le_pow_right h)

Premises used: Submodule.torsionBySet_le_torsionBySet_of_subset, Ideal.pow_le_pow_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
s : Set R
⊢ Eq (α := Submodule R M) (torsionBySet R M s) (torsionBySet R M (↑(Ideal.span s) : Set R))

Tactic:
le_antisymm (fun x hx => ?_) (torsionBySet_le_torsionBySet_of_subset subset_span)

Premises used: Submodule.torsionBySet_le_torsionBySet_of_subset, le_antisymm, Submodule.subset_span
-- 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
s : Set R
refine :
  ∀ (x : M) (hx : Membership.mem (γ := Submodule R M) (torsionBySet R M s) x),
    Membership.mem (γ := Submodule R M) (torsionBySet R M (↑(Ideal.span s) : Set R)) x
⊢ Eq (α := Submodule R M) (torsionBySet R M s) (torsionBySet R M (↑(Ideal.span s) : Set R))

Tactic:
refine le_antisymm (fun x hx => ?_) (torsionBySet_le_torsionBySet_of_subset subset_span)

Premises used: Submodule.torsionBySet_le_torsionBySet_of_subset, le_antisymm, Submodule.subset_span