awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hmax : ∀ (I : Ideal R), ¬P I → ∃ (I : Ideal R), Maximal (fun (x : Ideal R) ↦ ¬P x) I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I_1 : Ideal R
hI_1 : ¬P I_1
I : Ideal R
hI : Maximal (fun (x : Ideal R) ↦ ¬P x) I
⊢ False

Tactic:
hI.prop <| hprime I (hP.isPrime_of_maximal_not hI)

Premises used: Maximal.prop, Ideal.IsOka.isPrime_of_maximal_not
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hmax : ∀ (I : Ideal R), ¬P I → ∃ (I : Ideal R), Maximal (fun (x : Ideal R) ↦ ¬P x) I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I_1 : Ideal R
hI_1 : ¬P I_1
I : Ideal R
hI : Maximal (fun (x : Ideal R) ↦ ¬P x) I
⊢ False

Tactic:
exact hI.prop <| hprime I (hP.isPrime_of_maximal_not hI)

Premises used: Maximal.prop, Ideal.IsOka.isPrime_of_maximal_not
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hchain : ∀ C ⊆ {I : Ideal R | ¬P I}, IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
⊢ ∀ (I : Ideal R), P I

Tactic:
forall_of_forall_prime hP (fun I hI ↦ ?_) hprime

Premises used: Ideal.IsOka.forall_of_forall_prime
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hchain : ∀ C ⊆ {I : Ideal R | ¬P I}, IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
refine : ∀ (I : Ideal R) (hI : ¬P I), ∃ (I : Ideal R), Maximal (fun (x : Ideal R) ↦ ¬P x) I
⊢ ∀ (I : Ideal R), P I

Tactic:
refine forall_of_forall_prime hP (fun I hI ↦ ?_) hprime

Premises used: Ideal.IsOka.forall_of_forall_prime
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hchain : ∀ C ⊆ {I : Ideal R | ¬P I}, IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I : Ideal R
hI : ¬P I
⊢ ∃ (M : Ideal R), I ≤ M ∧ Maximal (fun (x : Ideal R) ↦ ¬P x) M

Tactic:
zorn_le_nonempty₀ {I | ¬P I} (fun C hC₁ hC₂ J hJ ↦ ⟨sSup C, ?_, fun _ ↦ le_sSup⟩) I hI

Premises used: Set.Mem, setOf, And.intro, zorn_le_nonempty₀, Exists.intro, le_sSup, Not, SupSet.sSup
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hchain : ∀ C ⊆ {I : Ideal R | ¬P I}, IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I : Ideal R
hI : ¬P I
refine :
  ∀ (C : Set (Ideal R)) (hC₁ : C ⊆ {I : Ideal R | ¬P I}) (hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C)
    (J : Ideal R) (hJ : J ∈ C), Membership.mem (γ := Set (Ideal R)) {I : Ideal R | ¬P I} (sSup C)
⊢ ∃ (M : Ideal R), I ≤ M ∧ Maximal (fun (x : Ideal R) ↦ ¬P x) M

Tactic:
refine zorn_le_nonempty₀ {I | ¬P I} (fun C hC₁ hC₂ J hJ ↦ ⟨sSup C, ?_, fun _ ↦ le_sSup⟩) I hI

Premises used: setOf, And.intro, zorn_le_nonempty₀, Exists.intro, le_sSup, Not, SupSet.sSup
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hchain : ∀ C ⊆ {I : Ideal R | ¬P I}, IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I : Ideal R
hI : ¬P I
C : Set (Ideal R)
hC₁ : C ⊆ {I : Ideal R | ¬P I}
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
J : Ideal R
hJ : J ∈ C
H : P (sSup C)
obtain : ∀ (w : Ideal R) (h₁ : w ∈ C) (h₂ : P w), False
⊢ False

Tactic:
obtain ⟨_, h₁, h₂⟩ := hchain C hC₁ hC₂ J hJ H
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hchain : ∀ C ⊆ {I : Ideal R | ¬P I}, IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I : Ideal R
hI : ¬P I
C : Set (Ideal R)
hC₁ : C ⊆ {I : Ideal R | ¬P I}
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
J : Ideal R
hJ : J ∈ C
H : P (sSup C)
w : Ideal R
h₁ : w ∈ C
h₂ : P w
⊢ False

Tactic:
hC₁ h₁ h₂
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hchain : ∀ C ⊆ {I : Ideal R | ¬P I}, IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I : Ideal R
hI : ¬P I
C : Set (Ideal R)
hC₁ : C ⊆ {I : Ideal R | ¬P I}
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
J : Ideal R
hJ : J ∈ C
H : P (sSup C)
w : Ideal R
h₁ : w ∈ C
h₂ : P w
⊢ False

Tactic:
exact hC₁ h₁ h₂
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hchain : ∀ C ⊆ {I : Ideal R | ¬P I}, IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I : Ideal R
hI : ¬P I
obtain :
  ∀ (M : Ideal R),
    I ≤ M → ∀ (hM : Maximal (fun (x : Ideal R) ↦ ¬P x) M), ∃ (I : Ideal R), Maximal (fun (x : Ideal R) ↦ ¬P x) I
⊢ ∃ (I : Ideal R), Maximal (fun (x : Ideal R) ↦ ¬P x) I

Tactic:
obtain ⟨M, _, hM⟩ : ∃ M, I ≤ M ∧ Maximal (¬P ·) M := by
    refine zorn_le_nonempty₀ {I | ¬P I} (fun C hC₁ hC₂ J hJ ↦ ⟨sSup C, ?_, fun _ ↦ le_sSup⟩) I hI
    intro H
    obtain ⟨_, h₁, h₂⟩ := hchain C hC₁ hC₂ J hJ H
    exact hC₁ h₁ h₂
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hchain : ∀ C ⊆ {I : Ideal R | ¬P I}, IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I : Ideal R
hI : ¬P I
M : Ideal R
left : I ≤ M
hM : Maximal (fun (x : Ideal R) ↦ ¬P x) M
⊢ ∃ (I : Ideal R), Maximal (fun (x : Ideal R) ↦ ¬P x) I

Tactic:
⟨M, hM⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.Ideal.Oka
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hchain : ∀ C ⊆ {I : Ideal R | ¬P I}, IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I : Ideal R
hI : ¬P I
M : Ideal R
left : I ≤ M
hM : Maximal (fun (x : Ideal R) ↦ ¬P x) M
⊢ ∃ (I : Ideal R), Maximal (fun (x : Ideal R) ↦ ¬P x) I

Tactic:
exact ⟨M, hM⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
x : R'
h : x ∈ s
⊢ x • n ∈ s • N

Tactic:
mem_set_smul_of_mem_mem h hn

Premises used: Submodule.mem_set_smul_of_mem_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
x : R'
h : x ∈ s
⊢ x • n ∈ s • N

Tactic:
exact mem_set_smul_of_mem_mem h hn

Premises used: Submodule.mem_set_smul_of_mem_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
zero : 0 ∈ s • N
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R') 0 n ∈ s • N

Tactic:
rw [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
⊢ 0 ∈ s • N

Tactic:
Submodule.zero_mem _

Premises used: Submodule.zero_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
⊢ 0 ∈ s • N

Tactic:
exact Submodule.zero_mem _

Premises used: Submodule.zero_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
x y : R'
hx : Membership.mem (γ := Submodule R' R') (span R' s) x
hy : Membership.mem (γ := Submodule R' R') (span R' s) y
ihr : x • n ∈ s • N
ihs : y • n ∈ s • N
add : x • n + y • n ∈ s • N
⊢ (x + y) • n ∈ s • N

Tactic:
rw [add_smul]

Premises used: add_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
x y : R'
hx : Membership.mem (γ := Submodule R' R') (span R' s) x
hy : Membership.mem (γ := Submodule R' R') (span R' s) y
ihr : x • n ∈ s • N
ihs : y • n ∈ s • N
⊢ x • n + y • n ∈ s • N

Tactic:
Submodule.add_mem _ ihr ihs

Premises used: Submodule.add_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
x y : R'
hx : Membership.mem (γ := Submodule R' R') (span R' s) x
hy : Membership.mem (γ := Submodule R' R') (span R' s) y
ihr : x • n ∈ s • N
ihs : y • n ∈ s • N
⊢ x • n + y • n ∈ s • N

Tactic:
exact Submodule.add_mem _ ihr ihs

Premises used: Submodule.add_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a x : R'
hr : Membership.mem (γ := Submodule R' R') (span R' s) x
h : x • n ∈ s • N
⊢ ∃ (c : R' →₀ R'), (↑c.support : Set R') ⊆ s ∧ (c.sum fun (mi r : R') ↦ r • mi) = x

Tactic:
rw [mem_span_set] at hr

Premises used: Submodule.mem_span_set
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a x : R'
hr : Membership.mem (γ := Submodule R' R') (span R' s) x
h : x • n ∈ s • N
hr₁ : ∃ (c : R' →₀ R'), (↑c.support : Set R') ⊆ s ∧ (c.sum fun (mi r : R') ↦ r • mi) = x
⊢ x • n ∈ s • N

Tactic:
rw [mem_span_set] at hr

Premises used: Submodule.mem_span_set
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a x : R'
hr : ∃ (c : R' →₀ R'), (↑c.support : Set R') ⊆ s ∧ (c.sum fun (mi r : R') ↦ r • mi) = x
h : x • n ∈ s • N
smul :
  ∀ (c : R' →₀ R') (hc : (↑c.support : Set R') ⊆ s),
    HSMul.hSMul (α := R') (c.sum fun (mi r : R') ↦ r • mi) n ∈ s • N →
      HSMul.hSMul (β := R') a (c.sum fun (mi r : R') ↦ r • mi) • n ∈ s • N
⊢ (a • x) • n ∈ s • N

Tactic:
obtain ⟨c, hc, rfl⟩ := hr

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a : R'
c : R' →₀ R'
hc : (↑c.support : Set R') ⊆ s
h : HSMul.hSMul (α := R') (c.sum fun (mi r : R') ↦ r • mi) n ∈ s • N
smul : ∑ i ∈ c.support, (a • HSMul.hSMul (α := R') ((c : (a : R') → R') i : R') i) • n ∈ s • N
⊢ HSMul.hSMul (β := R') a (c.sum fun (mi r : R') ↦ r • mi) • n ∈ s • N

Tactic:
rw [Finsupp.sum, Finset.smul_sum, Finset.sum_smul]

Premises used: Finset.sum_smul, Finsupp.sum, Finset.smul_sum
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a : R'
c : R' →₀ R'
hc : (↑c.support : Set R') ⊆ s
h : HSMul.hSMul (α := R') (c.sum fun (mi r : R') ↦ r • mi) n ∈ s • N
⊢ ∑ i ∈ c.support, (a • HSMul.hSMul (α := R') ((c : (a : R') → R') i : R') i) • n ∈ s • N

Tactic:
Submodule.sum_mem _ fun i hi => ?_

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a : R'
c : R' →₀ R'
hc : (↑c.support : Set R') ⊆ s
h : HSMul.hSMul (α := R') (c.sum fun (mi r : R') ↦ r • mi) n ∈ s • N
smul : ∀ (i : R') (hi : i ∈ c.support), (a • HSMul.hSMul (α := R') ((c : (a : R') → R') i : R') i) • n ∈ s • N
⊢ ∑ i ∈ c.support, (a • HSMul.hSMul (α := R') ((c : (a : R') → R') i : R') i) • n ∈ s • N

Tactic:
refine Submodule.sum_mem _ fun i hi => ?_

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a : R'
c : R' →₀ R'
hc : (↑c.support : Set R') ⊆ s
h : HSMul.hSMul (α := R') (c.sum fun (mi r : R') ↦ r • mi) n ∈ s • N
i : R'
hi : i ∈ c.support
smul : i • HMul.hMul (β := R') a ((c : (a : R') → R') i : R') • n ∈ s • N
⊢ (a • HSMul.hSMul (α := R') ((c : (a : R') → R') i : R') i) • n ∈ s • N

Tactic:
rw [← mul_smul, smul_eq_mul, mul_comm, mul_smul]

Premises used: mul_comm, smul_eq_mul, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a : R'
c : R' →₀ R'
hc : (↑c.support : Set R') ⊆ s
h : HSMul.hSMul (α := R') (c.sum fun (mi r : R') ↦ r • mi) n ∈ s • N
i : R'
hi : i ∈ c.support
⊢ i • HMul.hMul (β := R') a ((c : (a : R') → R') i : R') • n ∈ s • N

Tactic:
mem_set_smul_of_mem_mem (hc hi) <| Submodule.smul_mem _ _ hn

Premises used: Set.Mem, Submodule.mem_set_smul_of_mem_mem, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a : R'
c : R' →₀ R'
hc : (↑c.support : Set R') ⊆ s
h : HSMul.hSMul (α := R') (c.sum fun (mi r : R') ↦ r • mi) n ∈ s • N
i : R'
hi : i ∈ c.support
⊢ i • HMul.hMul (β := R') a ((c : (a : R') → R') i : R') • n ∈ s • N

Tactic:
exact mem_set_smul_of_mem_mem (hc hi) <| Submodule.smul_mem _ _ hn

Premises used: Submodule.mem_set_smul_of_mem_mem, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hr : r ∈ (↑(Ideal.span s) : Set R')
hn : n ∈ N
mem : ∀ (x : R') (h : x ∈ s), x • n ∈ s • N
zero : HSMul.hSMul.{u_1, u_2, u_2} (α := R') 0 n ∈ s • N
add :
  ∀ (x y : R'),
    Membership.mem (γ := Submodule R' R') (span R' s) x →
      Membership.mem (γ := Submodule R' R') (span R' s) y →
        ∀ (ihr : x • n ∈ s • N) (ihs : y • n ∈ s • N), (x + y) • n ∈ s • N
smul : ∀ (a x : R') (hr : Membership.mem (γ := Submodule R' R') (span R' s) x), x • n ∈ s • N → (a • x) • n ∈ s • N
⊢ r • n ∈ s • N

Tactic:
induction hr using Submodule.span_induction with
        | mem _ h => exact mem_set_smul_of_mem_mem h hn
        | zero => rw [zero_smul]; exact Submodule.zero_mem _
        | add _ _ _ _ ihr ihs => rw [add_smul]; exact Submodule.add_mem _ ihr ihs
        | smul _ _ hr =>
          rw [mem_span_set] at hr
          obtain ⟨c, hc, rfl⟩ := hr
          rw [Finsupp.sum, Finset.smul_sum, Finset.sum_smul]
          refine Submodule.sum_mem _ fun i hi => ?_
          rw [← mul_smul, smul_eq_mul, mul_comm, mul_smul]
          exact mem_set_smul_of_mem_mem (hc hi) <| Submodule.smul_mem _ _ hn

Premises used: Finset.sum_smul, Submodule.sum_mem, Finsupp.sum, Submodule.mem_span_set, zero_smul, Submodule.smul, add_smul, Submodule.zero_mem, Finset.smul_sum, mul_comm, Submodule.zero, smul_eq_mul, Submodule.add, SemigroupAction.mul_smul, rfl, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
M : Type u_1
inst : AddCommGroup M
a : M
h :
  ∀ (i : M),
    Membership.mem (γ := AddSubgroup M) (toAddSubgroup (module_M := AddCommGroup.toIntModule M) (ℤ ∙ a)) i ↔
      Membership.mem (γ := AddSubgroup M) (AddSubgroup.zmultiples a) i
⊢ Eq (α := AddSubgroup M) (toAddSubgroup (module_M := AddCommGroup.toIntModule M) (ℤ ∙ a)) (AddSubgroup.zmultiples a)

Tactic:
ext i
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
M : Type u_1
inst : AddCommGroup M
a i : M
⊢ Membership.mem (γ := AddSubgroup M) (toAddSubgroup (module_M := AddCommGroup.toIntModule M) (ℤ ∙ a)) i ↔
    Membership.mem (γ := AddSubgroup M) (AddSubgroup.zmultiples a) i

Tactic:
simp [Submodule.mem_span_singleton, AddSubgroup.mem_zmultiples_iff]

Premises used: Submodule.mem_span_singleton, AddSubgroup.mem_zmultiples_iff
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
a : ℤ
⊢ Eq (α := AddSubgroup ℤ) (toAddSubgroup (Ideal.span {a})) (AddSubgroup.zmultiples a)

Tactic:
Submodule.span_singleton_toAddSubgroup_eq_zmultiples _

Premises used: Submodule.span_singleton_toAddSubgroup_eq_zmultiples
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
⊢ I • J = I * J

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
⊢ I • N ≤ N

Tactic:
smul_le.2 fun r _ _ ↦ N.smul_mem r

Premises used: Iff.mpr, Set.Mem, Submodule.smul_le, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
f : R →ₗ[R] M
y : R
hy : y ∈ (↑I : Set R)
rw : HSMul.hSMul (β := M) y ((f : (a : R) → M) 1 : M) ∈ HSMul.hSMul (β := Submodule R M) I ⊤
⊢ Membership.mem (α := M) (HSMul.hSMul (β := Submodule R M) I ⊤) ((f : (a : R) → M) y : M)

Tactic:
rw [← mul_one y, ← smul_eq_mul, f.map_smul]

Premises used: LinearMap.map_smul, smul_eq_mul, mul_one
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
f : R →ₗ[R] M
y : R
hy : y ∈ (↑I : Set R)
⊢ HSMul.hSMul (β := M) y ((f : (a : R) → M) 1 : M) ∈ HSMul.hSMul (β := Submodule R M) I ⊤

Tactic:
smul_mem_smul hy mem_top

Premises used: Set.Mem, Submodule.smul_mem_smul, Submodule.mem_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
f : R →ₗ[R] M
y : R
hy : y ∈ (↑I : Set R)
⊢ HSMul.hSMul (β := M) y ((f : (a : R) → M) 1 : M) ∈ HSMul.hSMul (β := Submodule R M) I ⊤

Tactic:
exact smul_mem_smul hy mem_top

Premises used: Submodule.smul_mem_smul, Submodule.mem_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
⊢ HSMul.hSMul.{u, v, v} (α := Ideal R) ⊤ N = N

Tactic:
le_antisymm smul_le_right fun r hri => one_smul R r ▸ smul_mem_smul mem_top hri

Premises used: Eq.rec, Submodule.smul_le_right, one_smul, le_antisymm, Submodule.smul_mem_smul, Submodule.mem_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I J : Ideal R
N : Submodule R M
⊢ (I * J) • N = I • J • N

Tactic:
Submodule.smul_assoc _ _ _

Premises used: Set.Mem, Submodule.smul_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Submodule R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
x : M
H : ∀ (r : (↑s : Type u)), (↑r : R) • x ∈ M'
this : LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M'
rw : Membership.mem (α := M) M' ((LinearMap.toSpanSingleton R M x : (a : R) → M) 1 : M)
⊢ x ∈ M'

Tactic:
rw [← LinearMap.toSpanSingleton_apply_one R M x]

Premises used: LinearMap.toSpanSingleton_apply_one
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Submodule R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
x : M
H : ∀ (r : (↑s : Type u)), (↑r : R) • x ∈ M'
this : LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M'
⊢ Membership.mem (α := M) M' ((LinearMap.toSpanSingleton R M x : (a : R) → M) 1 : M)

Tactic:
this (LinearMap.mem_range_self _ 1)

Premises used: LinearMap.mem_range_self, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Submodule R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
x : M
H : ∀ (r : (↑s : Type u)), (↑r : R) • x ∈ M'
this : LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M'
⊢ Membership.mem (α := M) M' ((LinearMap.toSpanSingleton R M x : (a : R) → M) 1 : M)

Tactic:
exact this (LinearMap.mem_range_self _ 1)

Premises used: LinearMap.mem_range_self, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Submodule R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
x : M
H : ∀ (r : (↑s : Type u)), (↑r : R) • x ∈ M'
suffices : LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M'
⊢ x ∈ M'

Tactic:
suffices LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M' by
    rw [← LinearMap.toSpanSingleton_apply_one R M x]
    exact this (LinearMap.mem_range_self _ 1)
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Submodule R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
x : M
H : ∀ (r : (↑s : Type u)), (↑r : R) • x ∈ M'
rw : s ⊆ (↑(comap (LinearMap.toSpanSingleton R M x) M') : Set R)
⊢ LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M'

Tactic:
rw [LinearMap.range_eq_map, ← hs, map_le_iff_le_comap, Ideal.span, span_le]

Premises used: Ideal.span, LinearMap.range_eq_map, Submodule.map_le_iff_le_comap, Submodule.span_le
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Submodule R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
x : M
H : ∀ (r : (↑s : Type u)), (↑r : R) • x ∈ M'
⊢ s ⊆ (↑(comap (LinearMap.toSpanSingleton R M x) M') : Set R)

Tactic:
fun r hr ↦ H ⟨r, hr⟩

Premises used: Set.Mem, setOf, Set.Subset, Subtype.mk, Set.preimage
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Submodule R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
x : M
H : ∀ (r : (↑s : Type u)), (↑r : R) • x ∈ M'
⊢ s ⊆ (↑(comap (LinearMap.toSpanSingleton R M x) M') : Set R)

Tactic:
exact fun r hr ↦ H ⟨r, hr⟩

Premises used: Subtype.mk
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
⊢ map f (I • N) = I • map f N

Tactic:
le_antisymm
    (map_le_iff_le_comap.2 <|
      smul_le.2 fun r hr n hn =>
        show f (r • n) ∈ I • N.map f from
          (f.map_smul r n).symm ▸ smul_mem_smul hr (mem_map_of_mem hn)) <|
    smul_le.2 fun r hr _ hn =>
      let ⟨p, hp, hfp⟩ := mem_map.1 hn
      hfp ▸ f.map_smul r p ▸ mem_map_of_mem (smul_mem_smul hr hp)

Premises used: Iff.mpr, Submodule.mem_map, Membership.mem, Eq.rec, _private.0.Submodule.map_smul''.match_1, le_antisymm, LinearMap.map_smul, Iff.mp, Submodule.smul_le, HSMul.hSMul, Submodule.mem_map_of_mem, Submodule.smul_mem_smul, Submodule.map, Submodule.map_le_iff_le_comap, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
rw : I • map N.subtype ⊤ = I • N
rw₁ : I • N.subtype.range = I • N
rw₂ rw₃ : I • N = I • N
⊢ map N.subtype (HSMul.hSMul (β := Submodule R ↥N) I ⊤) = I • N

Tactic:
rw [Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype]

Premises used: Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype