awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ Membership.mem (γ := Ideal R) (annihilator R (M × M')) x ↔
    Membership.mem (γ := Ideal R) (annihilator R M ⊓ annihilator R M') x
have h₃ : (∀ (a : M) (b : M'), (x • a, x • b) = 0) ↔ (∀ (m : M), x • m = 0) ∧ ∀ (m : M'), x • m = 0
Tactic: simp_rw [Ideal.mem_inf, mem_annihilator,
    Prod.forall, Prod.smul_mk, Prod.mk_eq_zero, forall_and_left, ← forall_and_right]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ Membership.mem (γ := Ideal R) (annihilator R (M × M')) x ↔
    Membership.mem (γ := Ideal R) (annihilator R M ⊓ annihilator R M') x
have h₄ : (∀ (a : M) (b : M'), x • a = 0 ∧ x • b = 0) ↔ (∀ (m : M), x • m = 0) ∧ ∀ (m : M'), x • m = 0
Tactic: simp_rw [Ideal.mem_inf, mem_annihilator,
    Prod.forall, Prod.smul_mk, Prod.mk_eq_zero, forall_and_left, ← forall_and_right]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ Membership.mem (γ := Ideal R) (annihilator R (M × M')) x ↔
    Membership.mem (γ := Ideal R) (annihilator R M ⊓ annihilator R M') x
have h₅ : (∀ (a : M), x • a = 0 ∧ ∀ (x_1 : M'), x • x_1 = 0) ↔ (∀ (m : M), x • m = 0) ∧ ∀ (m : M'), x • m = 0
Tactic: simp_rw [Ideal.mem_inf, mem_annihilator,
    Prod.forall, Prod.smul_mk, Prod.mk_eq_zero, forall_and_left, ← forall_and_right]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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 ι
⊢ Eq (α := Ideal R) (annihilator R (ι →₀ M)) (annihilator R M)
have h : ∀ (r : R), Membership.mem (γ := Ideal R) (annihilator R (ι →₀ M)) r ↔ Membership.mem (γ := Ideal R) (annihilator R M) r
Tactic: ext r
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ Membership.mem (γ := Ideal R) (annihilator R (ι →₀ M)) r ↔ Membership.mem (γ := Ideal R) (annihilator R M) r
have h : (∀ (m : ι →₀ M), r • m = 0) ↔ ∀ (m : M), r • m = 0
Tactic: simp_rw [mem_annihilator]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ (∀ (m : ι →₀ M), r • m = 0) ↔ ∀ (m : M), r • m = 0
have h : (∀ (m : ι →₀ M), r • m = 0) → ∀ (m : M), r • m = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ (∀ (m : ι →₀ M), r • m = 0) ↔ ∀ (m : M), r • m = 0
have h₁ : (∀ (m : M), r • m = 0) → ∀ (m : ι →₀ M), r • m = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
have h₁ : ∀ (i : ι) (m : M), r • m = 0
Tactic: refine Nonempty.elim ‹_› fun i : ι ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
have h₁ : ∀ (i : ι), Eq.{u_2 + 1} (α := M) ((r • m : (a : ι) → M) i : M) ((0 : (a : ι) → M) i : M)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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)
⊢ Eq (α := Ideal R) (annihilator R (Π₀ (i : ι), M i)) (⨅ (i : ι), annihilator.{u_1, u_5} R (M i))
have 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
Tactic: ext r
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ Membership.mem (γ := Ideal R) (annihilator R (Π₀ (i : ι), M i)) r ↔
    Membership.mem (γ := Ideal R) (⨅ (i : ι), annihilator.{u_1, u_5} R (M i)) r
have h : (∀ (m : Π₀ (i : ι), M i), r • m = 0) ↔ ∀ (i : ι) (m : M i), r • m = 0
Tactic: simp only [mem_annihilator, Ideal.mem_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ (∀ (m : Π₀ (i : ι), M i), r • m = 0) ↔ ∀ (i : ι) (m : M i), r • m = 0
have h : (∀ (m : Π₀ (i : ι), M i), r • m = 0) → ∀ (i : ι) (m : M i), r • m = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ (∀ (m : Π₀ (i : ι), M i), r • m = 0) ↔ ∀ (i : ι) (m : M i), r • m = 0
have h₁ : (∀ (i : ι) (m : M i), r • m = 0) → ∀ (m : Π₀ (i : ι), M i), r • m = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ r • m = 0
have h₁ : ∀ (i : ι), (r • m : (a : ι) → M a) i = (0 : (a : ι) → M a) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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)
⊢ Eq (α := Ideal R) (annihilator R ((i : ι) → M i)) (⨅ (i : ι), annihilator.{u_1, u_5} R (M i))
have 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
Tactic: ext r
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ Membership.mem (γ := Ideal R) (annihilator R ((i : ι) → M i)) r ↔
    Membership.mem (γ := Ideal R) (⨅ (i : ι), annihilator.{u_1, u_5} R (M i)) r
have h : (∀ (m : (i : ι) → M i), r • m = 0) ↔ ∀ (i : ι) (m : M i), r • m = 0
Tactic: simp only [mem_annihilator, Ideal.mem_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ (∀ (m : (i : ι) → M i), r • m = 0) ↔ ∀ (i : ι) (m : M i), r • m = 0
have h : (∀ (m : (i : ι) → M i), r • m = 0) → ∀ (i : ι) (m : M i), r • m = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ (∀ (m : (i : ι) → M i), r • m = 0) ↔ ∀ (i : ι) (m : M i), r • m = 0
have h₁ : (∀ (i : ι) (m : M i), r • m = 0) → ∀ (m : (i : ι) → M i), r • m = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ r • m = 0
have h₁ : ∀ (i : ι), (r • m) i = 0 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = 0
have 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
Tactic: simp_rw [annihilator, Module.mem_annihilator, Subtype.forall, Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ HSMul.hSMul (β := M) x 0 = 0
have rw : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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 = ⊥
have rw : Eq (α := Ideal R) (Module.annihilator.{u_1, u_2} R ↥N) ⊤ ↔ N = ⊥
Tactic: rw [annihilator, Module.annihilator_eq_top_iff, Submodule.subsingleton_iff_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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 = ⊥
⊢ N.annihilator = ⊤ ↔ N = ⊥
have rw₁ : Subsingleton.{u_2 + 1} ↥N ↔ N = ⊥
Tactic: rw [annihilator, Module.annihilator_eq_top_iff, Submodule.subsingleton_iff_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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 = ⊥
⊢ N.annihilator = ⊤ ↔ N = ⊥
have rw₂ : N = ⊥ ↔ N = ⊥
Tactic: rw [annihilator, Module.annihilator_eq_top_iff, Submodule.subsingleton_iff_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ r • (m₁ + m₂) = 0
have simp_rw₂ : r • m₁ + r • m₂ = 0
Tactic: simp_rw [smul_add, h₁, h₂, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ r • (m₁ + m₂) = 0
have simp_rw₃ : 0 + r • m₂ = 0
Tactic: simp_rw [smul_add, h₁, h₂, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ r • (m₁ + m₂) = 0
have simp_rw₄ : HAdd.hAdd (α := M) 0 0 = 0
Tactic: simp_rw [smul_add, h₁, h₂, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ (N ⊔ P).annihilator = N.annihilator ⊓ P.annihilator
have rw : annihilator (M := M) (sSup {N, P}) = N.annihilator ⊓ P.annihilator
Tactic: rw [← sSup_pair, sSup_eq_iSup, iSup_subtype', annihilator_iSup, ← iInf_pair, iInf_subtype']
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ (N ⊔ P).annihilator = N.annihilator ⊓ P.annihilator
have 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
Tactic: rw [← sSup_pair, sSup_eq_iSup, iSup_subtype', annihilator_iSup, ← iInf_pair, iInf_subtype']
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ (N ⊔ P).annihilator = N.annihilator ⊓ P.annihilator
have 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
Tactic: rw [← sSup_pair, sSup_eq_iSup, iSup_subtype', annihilator_iSup, ← iInf_pair, iInf_subtype']
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ (N ⊔ P).annihilator = N.annihilator ⊓ P.annihilator
have rw₃ : ⨅ (i : Subtype (Membership.mem (γ := Set (Submodule R M)) {N, P})), (↑i : Submodule R M).annihilator =
  N.annihilator ⊓ P.annihilator
Tactic: rw [← sSup_pair, sSup_eq_iSup, iSup_subtype', annihilator_iSup, ← iInf_pair, iInf_subtype']
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ (N ⊔ P).annihilator = N.annihilator ⊓ P.annihilator
have 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)
Tactic: rw [← sSup_pair, sSup_eq_iSup, iSup_subtype', annihilator_iSup, ← iInf_pair, iInf_subtype']
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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)
⊢ (N ⊔ P).annihilator = N.annihilator ⊓ P.annihilator
have 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)
Tactic: rw [← sSup_pair, sSup_eq_iSup, iSup_subtype', annihilator_iSup, ← iInf_pair, iInf_subtype']
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ I ≤ N.annihilator ↔ I • N = ⊥
have simp_rw : (∀ ⦃x : R⦄, x ∈ I → ∀ n ∈ N, x • n = 0) ↔ ∀ r ∈ I, ∀ n ∈ N, Membership.mem (γ := Submodule R M) ⊥ (r • n)
Tactic: simp_rw [← le_bot_iff, smul_le, SetLike.le_def, mem_annihilator]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ Membership.mem (γ := Ideal R) (annihilator (span R s)) r ↔ ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
have rw : (∀ (n : M), Membership.mem (γ := Submodule R M) (span R s) n → r • n = 0) ↔ ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
Tactic: rw [Submodule.mem_annihilator]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ (∀ (n : M), Membership.mem (γ := Submodule R M) (span R s) n → r • n = 0) ↔ ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
have mp : (∀ (n : M), Membership.mem (γ := Submodule R M) (span R s) n → r • n = 0) → ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
mp :
  (∀ (n : M), Membership.mem (γ := Submodule R M) (span R s) n → r • n = 0) → ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
⊢ (∀ (n : M), Membership.mem (γ := Submodule R M) (span R s) n → r • n = 0) ↔ ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
have mpr : (∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0) → ∀ (n : M), Membership.mem (γ := Submodule R M) (span R s) n → r • n = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
⊢ r • n = 0
have mpr : ∀ (x : M) (h : x ∈ s), r • x = 0
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
mpr : ∀ (x : M) (h : x ∈ s), r • x = 0
⊢ r • n = 0
have mpr₁ : HSMul.hSMul (β := M) r 0 = 0
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
mpr : ∀ (x : M) (h : x ∈ s), r • x = 0
mpr₁ : HSMul.hSMul (β := M) r 0 = 0
⊢ r • n = 0
have mpr₂ : ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
  (hy : Membership.mem (γ := Submodule R M) (span R s) y), r • x = 0 → r • y = 0 → r • (x + y) = 0
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
mpr : ∀ (x : M) (h : x ∈ s), r • x = 0
mpr₁ : HSMul.hSMul (β := M) r 0 = 0
mpr₂ :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R M) (span R s) y), r • x = 0 → r • y = 0 → r • (x + y) = 0
⊢ r • n = 0
have mpr₃ : ∀ (a : R) (x : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x), r • x = 0 → r • a • x = 0
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
x y : M
hx_1 : Membership.mem (γ := Submodule R M) (span R s) x
hy_1 : Membership.mem (γ := Submodule R M) (span R s) y
hx : r • x = 0
hy : r • y = 0
⊢ r • (x + y) = 0
have mpr : r • x + r • y = 0
Tactic: rw [smul_add, hx, hy, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
x y : M
hx_1 : Membership.mem (γ := Submodule R M) (span R s) x
hy_1 : Membership.mem (γ := Submodule R M) (span R s) y
hx : r • x = 0
hy : r • y = 0
mpr : r • x + r • y = 0
⊢ r • (x + y) = 0
have mpr₁ : 0 + r • y = 0
Tactic: rw [smul_add, hx, hy, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
x y : M
hx_1 : Membership.mem (γ := Submodule R M) (span R s) x
hy_1 : Membership.mem (γ := Submodule R M) (span R s) y
hx : r • x = 0
hy : r • y = 0
mpr : r • x + r • y = 0
mpr₁ : 0 + r • y = 0
⊢ r • (x + y) = 0
have mpr₂ : HAdd.hAdd (α := M) 0 0 = 0
Tactic: rw [smul_add, hx, hy, zero_add]