awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : R
h : ∀ (m : M), x • m = 0
m : M'
obtain : ∀ (m : M), HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M') = 0
⊢ x • m = 0

Tactic:
obtain ⟨m, rfl⟩ := hf m

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : R
h : ∀ (m : M), x • m = 0
m : M
rw : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (x • m) : M') (0 : M')
rw₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') 0 : M') (0 : M')
rw₂ rw₃ : Eq.{u_3 + 1} (α := M') 0 0
⊢ HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M') = 0

Tactic:
rw [← map_smul, h, f.map_zero]

Premises used: LinearMap.map_zero, map_smul
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
e : M ≃ₗ[R] M'
⊢ Eq (α := Ideal R) (Module.annihilator R M) (Module.annihilator R M')

Tactic:
(e.annihilator_le_of_surjective e.surjective).antisymm (e.annihilator_le_of_injective e.injective)

Premises used: LinearEquiv.surjective, LE.le.antisymm, LinearMap.annihilator_le_of_injective, LinearEquiv.toLinearMap, LinearMap.annihilator_le_of_surjective, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₀ : Type u_4
inst_3 : CommSemiring R₀
inst_4 : Module R₀ M
inst_5 : Algebra R₀ R
inst_6 : IsScalarTower R₀ R M
h :
  ∀ (x : R₀),
    Membership.mem (γ := Ideal R₀) (Ideal.comap (F := R₀ →+* R) (algebraMap R₀ R) (annihilator R M)) x ↔
      Membership.mem (γ := Ideal R₀) (annihilator R₀ M) x
⊢ Eq (α := Ideal R₀) (Ideal.comap (F := R₀ →+* R) (algebraMap R₀ R) (annihilator R M)) (annihilator R₀ M)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₀ : Type u_4
inst_3 : CommSemiring R₀
inst_4 : Module R₀ M
inst_5 : Algebra R₀ R
inst_6 : IsScalarTower R₀ R M
x : R₀
⊢ Membership.mem (γ := Ideal R₀) (Ideal.comap (F := R₀ →+* R) (algebraMap R₀ R) (annihilator R M)) x ↔
    Membership.mem (γ := Ideal R₀) (annihilator R₀ M) x

Tactic:
simp [mem_annihilator]

Premises used: Module.mem_annihilator
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_4
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : LE.le (α := Ideal R) (annihilator R M) ⊥ ↔ FaithfulSMul R M
⊢ Eq (α := Ideal R) (annihilator R M) ⊥ ↔ FaithfulSMul R M

Tactic:
rw [← le_bot_iff]

Premises used: le_bot_iff
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_4
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ LE.le (α := Ideal R) (annihilator R M) ⊥ ↔ FaithfulSMul R M

Tactic:
⟨fun H ↦ ⟨fun {r s} H' ↦ ?_⟩, fun ⟨H⟩ {a} ha ↦ ?_⟩

Premises used: _private.0.Module.annihilator_eq_bot.match_1, Membership.mem, Bot.bot, FaithfulSMul.mk, Iff.intro
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_4
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
refine_1 : ∀ (H : LE.le (α := Ideal R) (annihilator R M) ⊥) {r s : R} (H' : ∀ (a : M), r • a = s • a), r = s
refine_2 :
  FaithfulSMul R M →
    ∀ {a : R} (ha : Membership.mem (γ := Submodule R R) (annihilator R M) a)
      (H : ∀ {m₁ m₂ : R}, (∀ (a : M), m₁ • a = m₂ • a) → m₁ = m₂), Membership.mem (γ := Submodule R R) ⊥ a
⊢ LE.le (α := Ideal R) (annihilator R M) ⊥ ↔ FaithfulSMul R M

Tactic:
refine ⟨fun H ↦ ⟨fun {r s} H' ↦ ?_⟩, fun ⟨H⟩ {a} ha ↦ ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_4
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
H : LE.le (α := Ideal R) (annihilator R M) ⊥
r s : R
H' : ∀ (a : M), r • a = s • a
refine_1 : r - s = 0
⊢ r = s

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_4
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
H : LE.le (α := Ideal R) (annihilator R M) ⊥
r s : R
H' : ∀ (a : M), r • a = s • a
⊢ ∀ (m : M), (r - s) • m = 0

Tactic:
simp only [sub_smul, H', sub_self, implies_true]

Premises used: sub_self, sub_smul, implies_true
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_4
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
H : LE.le (α := Ideal R) (annihilator R M) ⊥
r s : R
H' : ∀ (a : M), r • a = s • a
⊢ r - s = 0

Tactic:
exact H (Module.mem_annihilator (r := r - s).mpr
      (by simp only [sub_smul, H', sub_self, implies_true]))

Premises used: Iff.mpr, Module.mem_annihilator
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_4
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h : FaithfulSMul R M
a : R
ha : Membership.mem (γ := Submodule R R) (annihilator R M) a
H : ∀ {m₁ m₂ : R}, (∀ (a : M), m₁ • a = m₂ • a) → m₁ = m₂
⊢ ∀ (a_1 : M), a • a_1 = HSMul.hSMul.{u_4, u_5, u_5} (α := R) 0 a_1

Tactic:
simp [Module.mem_annihilator.mp ha]

Premises used: Module.mem_annihilator, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_4
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h : FaithfulSMul R M
a : R
ha : Membership.mem (γ := Submodule R R) (annihilator R M) a
H : ∀ {m₁ m₂ : R}, (∀ (a : M), m₁ • a = m₂ • a) → m₁ = m₂
⊢ Membership.mem (γ := Submodule R R) ⊥ a

Tactic:
exact @H a 0 (by simp [Module.mem_annihilator.mp ha])
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Eq (α := Ideal R) (annihilator R M) ⊤
m m' : M
rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m'
⊢ m = m'

Tactic:
rw [← one_smul R m, ← one_smul R m']

Premises used: one_smul
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Eq (α := Ideal R) (annihilator R M) ⊤
m m' : M
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m'

Tactic:
simp_rw [mem_annihilator.mp (h ▸ Submodule.mem_top)]

Premises used: Module.mem_annihilator, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
h :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) (annihilator R (M × M')) x ↔
      Membership.mem (γ := Ideal R) (annihilator R M ⊓ annihilator R M') x
⊢ Eq (α := Ideal R) (annihilator R (M × M')) (annihilator R M ⊓ annihilator R M')

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
x : R
h :
  Membership.mem (γ := Ideal R) (annihilator R (M × M')) x ↔
    Membership.mem (γ := Ideal R) (annihilator R M) x ∧ Membership.mem (γ := Ideal R) (annihilator R M') x
h₁ : (∀ (m : M × M'), x • m = 0) ↔ (∀ (m : M), x • m = 0) ∧ ∀ (m : M'), x • m = 0
h₂ : (∀ (a : M) (b : M'), x • (a, b) = 0) ↔ (∀ (m : M), x • m = 0) ∧ ∀ (m : M'), x • m = 0
h₃ : (∀ (a : M) (b : M'), (x • a, x • b) = 0) ↔ (∀ (m : M), x • m = 0) ∧ ∀ (m : M'), x • m = 0
h₄ : (∀ (a : M) (b : M'), x • a = 0 ∧ x • b = 0) ↔ (∀ (m : M), x • m = 0) ∧ ∀ (m : M'), x • m = 0
h₅ : (∀ (a : M), x • a = 0 ∧ ∀ (x_1 : M'), x • x_1 = 0) ↔ (∀ (m : M), x • m = 0) ∧ ∀ (m : M'), x • m = 0
⊢ Membership.mem (γ := Ideal R) (annihilator R (M × M')) x ↔
    Membership.mem (γ := Ideal R) (annihilator R M ⊓ annihilator R M') x

Tactic:
simp_rw [Ideal.mem_inf, mem_annihilator,
    Prod.forall, Prod.smul_mk, Prod.mk_eq_zero, forall_and_left, ← forall_and_right]

Premises used: Module.mem_annihilator, forall_and_left, forall_and_right, Prod.mk_eq_zero, Ideal.mem_inf, Prod.forall, Prod.smul_mk
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
inst_3 : Nonempty ι
h :
  ∀ (r : R),
    Membership.mem (γ := Ideal R) (annihilator R (ι →₀ M)) r ↔ Membership.mem (γ := Ideal R) (annihilator R M) r
⊢ Eq (α := Ideal R) (annihilator R (ι →₀ M)) (annihilator R M)

Tactic:
ext r
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
inst_3 : Nonempty ι
r : R
h : (∀ (m : ι →₀ M), r • m = 0) ↔ ∀ (m : M), r • m = 0
⊢ Membership.mem (γ := Ideal R) (annihilator R (ι →₀ M)) r ↔ Membership.mem (γ := Ideal R) (annihilator R M) r

Tactic:
simp_rw [mem_annihilator]

Premises used: Module.mem_annihilator
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
inst_3 : Nonempty ι
r : R
h : (∀ (m : ι →₀ M), r • m = 0) → ∀ (m : M), r • m = 0
h₁ : (∀ (m : M), r • m = 0) → ∀ (m : ι →₀ M), r • m = 0
⊢ (∀ (m : ι →₀ M), r • m = 0) ↔ ∀ (m : M), r • m = 0

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
inst_3 : Nonempty ι
r : R
h : ∀ (m : ι →₀ M), r • m = 0
⊢ ∀ (m : M), r • m = 0

Tactic:
Nonempty.elim ‹_› fun i : ι ↦ ?_

Premises used: Nonempty.elim
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
inst_3 : Nonempty ι
r : R
h : ∀ (m : ι →₀ M), r • m = 0
h₁ : ∀ (i : ι) (m : M), r • m = 0
⊢ ∀ (m : M), r • m = 0

Tactic:
refine Nonempty.elim ‹_› fun i : ι ↦ ?_

Premises used: Nonempty.elim
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
inst_3 : Nonempty ι
r : R
h : ∀ (m : ι →₀ M), r • m = 0
i : ι
⊢ ∀ (m : M), r • m = 0

Tactic:
simpa using fun m ↦ congr($(h (Finsupp.single i m)) i)

Premises used: congrArg, id, DFunLike.coe, Finsupp.single
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
inst_3 : Nonempty ι
r : R
h : ∀ (m : M), r • m = 0
m : ι →₀ M
h₁ : ∀ (i : ι), Eq.{u_2 + 1} (α := M) ((r • m : (a : ι) → M) i : M) ((0 : (a : ι) → M) i : M)
⊢ r • m = 0

Tactic:
ext i
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
inst_3 : Nonempty ι
r : R
h : ∀ (m : M), r • m = 0
m : ι →₀ M
i : ι
⊢ Eq.{u_2 + 1} (α := M) ((r • m : (a : ι) → M) i : M) ((0 : (a : ι) → M) i : M)

Tactic:
h _
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
inst_3 : Nonempty ι
r : R
h : ∀ (m : M), r • m = 0
m : ι →₀ M
i : ι
⊢ Eq.{u_2 + 1} (α := M) ((r • m : (a : ι) → M) i : M) ((0 : (a : ι) → M) i : M)

Tactic:
exact h _
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
M : ι → Type u_5
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
h :
  ∀ (r : R),
    Membership.mem (γ := Ideal R) (annihilator R (Π₀ (i : ι), M i)) r ↔
      Membership.mem (γ := Ideal R) (⨅ (i : ι), annihilator.{u_1, u_5} R (M i)) r
⊢ Eq (α := Ideal R) (annihilator R (Π₀ (i : ι), M i)) (⨅ (i : ι), annihilator.{u_1, u_5} R (M i))

Tactic:
ext r
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
M : ι → Type u_5
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
r : R
h : (∀ (m : Π₀ (i : ι), M i), r • m = 0) ↔ ∀ (i : ι) (m : M i), r • m = 0
⊢ Membership.mem (γ := Ideal R) (annihilator R (Π₀ (i : ι), M i)) r ↔
    Membership.mem (γ := Ideal R) (⨅ (i : ι), annihilator.{u_1, u_5} R (M i)) r

Tactic:
simp only [mem_annihilator, Ideal.mem_iInf]

Premises used: Module.mem_annihilator, Ideal.mem_iInf
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
M : ι → Type u_5
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
r : R
h : (∀ (m : Π₀ (i : ι), M i), r • m = 0) → ∀ (i : ι) (m : M i), r • m = 0
h₁ : (∀ (i : ι) (m : M i), r • m = 0) → ∀ (m : Π₀ (i : ι), M i), r • m = 0
⊢ (∀ (m : Π₀ (i : ι), M i), r • m = 0) ↔ ∀ (i : ι) (m : M i), r • m = 0

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
M : ι → Type u_5
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
r : R
h : ∀ (m : Π₀ (i : ι), M i), r • m = 0
i : ι
m : M i
⊢ r • m = 0

Tactic:
simpa using DFunLike.congr_fun (h (DFinsupp.single i m)) i

Premises used: DFunLike.congr_fun, DFinsupp.single
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
M : ι → Type u_5
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
r : R
h : ∀ (m : Π₀ (i : ι), M i), r • m = 0
i : ι
m : M i
⊢ r • m = 0

Tactic:
classical simpa using DFunLike.congr_fun (h (DFinsupp.single i m)) i
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
M : ι → Type u_5
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
m : Π₀ (i : ι), M i
h₁ : ∀ (i : ι), (r • m : (a : ι) → M a) i = (0 : (a : ι) → M a) i
⊢ r • m = 0

Tactic:
ext i
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
M : ι → Type u_5
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
m : Π₀ (i : ι), M i
i : ι
⊢ (r • m : (a : ι) → M a) i = (0 : (a : ι) → M a) i

Tactic:
h i _
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
M : ι → Type u_5
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
m : Π₀ (i : ι), M i
i : ι
⊢ (r • m : (a : ι) → M a) i = (0 : (a : ι) → M a) i

Tactic:
exact h i _
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
M : ι → Type u_5
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
h :
  ∀ (r : R),
    Membership.mem (γ := Ideal R) (annihilator R ((i : ι) → M i)) r ↔
      Membership.mem (γ := Ideal R) (⨅ (i : ι), annihilator.{u_1, u_5} R (M i)) r
⊢ Eq (α := Ideal R) (annihilator R ((i : ι) → M i)) (⨅ (i : ι), annihilator.{u_1, u_5} R (M i))

Tactic:
ext r
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
M : ι → Type u_5
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
r : R
h : (∀ (m : (i : ι) → M i), r • m = 0) ↔ ∀ (i : ι) (m : M i), r • m = 0
⊢ Membership.mem (γ := Ideal R) (annihilator R ((i : ι) → M i)) r ↔
    Membership.mem (γ := Ideal R) (⨅ (i : ι), annihilator.{u_1, u_5} R (M i)) r

Tactic:
simp only [mem_annihilator, Ideal.mem_iInf]

Premises used: Module.mem_annihilator, Ideal.mem_iInf
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
M : ι → Type u_5
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
r : R
h : (∀ (m : (i : ι) → M i), r • m = 0) → ∀ (i : ι) (m : M i), r • m = 0
h₁ : (∀ (i : ι) (m : M i), r • m = 0) → ∀ (m : (i : ι) → M i), r • m = 0
⊢ (∀ (m : (i : ι) → M i), r • m = 0) ↔ ∀ (i : ι) (m : M i), r • m = 0

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
M : ι → Type u_5
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
r : R
h : ∀ (m : (i : ι) → M i), r • m = 0
i : ι
m : M i
⊢ r • m = 0

Tactic:
simpa using congr_fun (h (Pi.single i m)) i

Premises used: Pi.single, congr_fun
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
M : ι → Type u_5
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
r : R
h : ∀ (m : (i : ι) → M i), r • m = 0
i : ι
m : M i
⊢ r • m = 0

Tactic:
classical simpa using congr_fun (h (Pi.single i m)) i
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
M : ι → Type u_5
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
m : (i : ι) → M i
h₁ : ∀ (i : ι), (r • m) i = 0 i
⊢ r • m = 0

Tactic:
ext i
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
M : ι → Type u_5
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
m : (i : ι) → M i
i : ι
⊢ (r • m) i = 0 i

Tactic:
h i _
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
M : ι → Type u_5
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
m : (i : ι) → M i
i : ι
⊢ (r • m) i = 0 i

Tactic:
exact h i _
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := Ideal R) (annihilator.{u_1, u_2} (M := M) ⊤) (Module.annihilator R M)

Tactic:
topEquiv.annihilator_eq

Premises used: Submodule.topEquiv, LinearEquiv.annihilator_eq
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
r : R
simp_rw :
  (∀ (a : M) (b : a ∈ N), (↑(r • Subtype.mk (p := fun (a : M) ↦ a ∈ N) a b) : M) = (↑0 : M)) ↔ ∀ n ∈ N, r • n = 0
⊢ r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = 0

Tactic:
simp_rw [annihilator, Module.mem_annihilator, Subtype.forall, Subtype.ext_iff]

Premises used: Module.mem_annihilator, Subtype.forall, Subtype.ext_iff, Submodule.annihilator
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
r : R
⊢ (∀ (a : M) (b : a ∈ N), (↑(r • Subtype.mk (p := fun (a : M) ↦ a ∈ N) a b) : M) = (↑0 : M)) ↔ ∀ n ∈ N, r • n = 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : R
h : Membership.mem (γ := Submodule R R) ⊤ x
rw rw₁ : Eq.{u_2 + 1} (α := M) 0 0
⊢ HSMul.hSMul (β := M) x 0 = 0

Tactic:
rw [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
rw : Eq (α := Ideal R) (Module.annihilator.{u_1, u_2} R ↥N) ⊤ ↔ N = ⊥
rw₁ : Subsingleton.{u_2 + 1} ↥N ↔ N = ⊥
rw₂ rw₃ : N = ⊥ ↔ N = ⊥
⊢ N.annihilator = ⊤ ↔ N = ⊥

Tactic:
rw [annihilator, Module.annihilator_eq_top_iff, Submodule.subsingleton_iff_eq_bot]

Premises used: Submodule.subsingleton_iff_eq_bot, Module.annihilator_eq_top_iff, Submodule.annihilator
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N P : Submodule R M
h : N ≤ P
⊢ P.annihilator ≤ N.annihilator

Tactic:
fun _ hrp =>
  mem_annihilator.2 fun n hn => mem_annihilator.1 hrp n <| h hn

Premises used: Iff.mpr, Set.Mem, Submodule.mem_annihilator, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Sort w
f : ι → Submodule R M
r : R
H : Membership.mem (γ := Submodule R R) (⨅ (i : ι), (f i).annihilator) r
n : M
hn : Membership.mem (γ := Submodule R M) (⨆ (i : ι), f i) n
m₁ m₂ : M
h₁ : (fun (x : M) ↦ r • x = 0) m₁
h₂ : (fun (x : M) ↦ r • x = 0) m₂
simp_rw simp_rw₁ : r • (m₁ + m₂) = 0
simp_rw₂ : r • m₁ + r • m₂ = 0
simp_rw₃ : 0 + r • m₂ = 0
simp_rw₄ : HAdd.hAdd (α := M) 0 0 = 0
⊢ r • (m₁ + m₂) = 0

Tactic:
simp_rw [smul_add, h₁, h₂, add_zero]

Premises used: add_zero, smul_add
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N P : Submodule R M
rw : annihilator (M := M) (sSup {N, P}) = N.annihilator ⊓ P.annihilator
rw₁ :
  annihilator.{u_1, u_2} (M := M)
      (⨆ (a : Submodule R M), ⨆ (_ : Membership.mem (γ := Set (Submodule R M)) {N, P} a), a) =
    N.annihilator ⊓ P.annihilator
rw₂ :
  annihilator.{u_1, u_2} (M := M)
      (⨆ (x : Subtype (Membership.mem (γ := Set (Submodule R M)) {N, P})), (↑x : Submodule R M)) =
    N.annihilator ⊓ P.annihilator
rw₃ :
  ⨅ (i : Subtype (Membership.mem (γ := Set (Submodule R M)) {N, P})), (↑i : Submodule R M).annihilator =
    N.annihilator ⊓ P.annihilator
rw₄ :
  Eq.{u_1 + 1} (α := Ideal R)
    (⨅ (i : Subtype (Membership.mem (γ := Set (Submodule R M)) {N, P})), (↑i : Submodule R M).annihilator)
    (⨅ (x : Submodule R M), ⨅ (_ : Membership.mem (γ := Set (Submodule R M)) {N, P} x), x.annihilator)
rw₅ rw₆ :
  Eq.{u_1 + 1} (α := Ideal R)
    (⨅ (i : Subtype (Membership.mem (γ := Set (Submodule R M)) {N, P})), (↑i : Submodule R M).annihilator)
    (⨅ (x : Subtype (Membership.mem (γ := Set (Submodule R M)) {N, P})), (↑x : Submodule R M).annihilator)
⊢ (N ⊔ P).annihilator = N.annihilator ⊓ P.annihilator

Tactic:
rw [← sSup_pair, sSup_eq_iSup, iSup_subtype', annihilator_iSup, ← iInf_pair, iInf_subtype']

Premises used: Submodule.annihilator_iSup, iSup_subtype', iInf_subtype', sSup_eq_iSup, sSup_pair, iInf_pair
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
I : Ideal R
simp_rw : (∀ ⦃x : R⦄, x ∈ I → ∀ n ∈ N, x • n = 0) ↔ ∀ r ∈ I, ∀ n ∈ N, Membership.mem (γ := Submodule R M) ⊥ (r • n)
⊢ I ≤ N.annihilator ↔ I • N = ⊥

Tactic:
simp_rw [← le_bot_iff, smul_le, SetLike.le_def, mem_annihilator]

Premises used: le_bot_iff, SetLike.le_def, Submodule.mem_annihilator, Submodule.smul_le
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
I : Ideal R
⊢ (∀ ⦃x : R⦄, x ∈ I → ∀ n ∈ N, x • n = 0) ↔ ∀ r ∈ I, ∀ n ∈ N, Membership.mem (γ := Submodule R M) ⊥ (r • n)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
⊢ N.annihilator • N = ⊥

Tactic:
eq_bot_iff.2 (smul_le.2 fun _ => mem_annihilator.1)

Premises used: Iff.mpr, Submodule.mem_annihilator, Iff.mp, Submodule.smul_le, eq_bot_iff
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : Semiring R
I : Ideal R
⊢ annihilator I * I = ⊥

Tactic:
annihilator_smul I

Premises used: Submodule.annihilator_smul
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
r : R
⊢ r ∈ N.annihilator ↔ N ≤ comap (HSMul.hSMul (β := M →ₗ[R] M) r LinearMap.id) ⊥

Tactic:
mem_annihilator.trans ⟨fun H n hn => (mem_bot R).2 <| H n hn, fun H _ hn => (mem_bot R).1 <| H hn⟩

Premises used: Iff.mpr, Submodule.mem_bot, Submodule.mem_annihilator, Iff.intro, Iff.mp, Iff.trans
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
r : R
rw :
  (∀ (n : M), Membership.mem (γ := Submodule R M) (span R s) n → r • n = 0) ↔ ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
⊢ Membership.mem (γ := Ideal R) (annihilator (span R s)) r ↔ ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0

Tactic:
rw [Submodule.mem_annihilator]

Premises used: Submodule.mem_annihilator