awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
⊢ x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f)) →
    ∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
      (a.sum fun (i : ι) (c : R) ↦ c • f i) = x

Tactic:
fun hx => span_induction ?_ ?_ ?_ ?_ (mem_smul_span.mp hx)

Premises used: Submodule.span_induction, Submodule.mem_smul_span, Iff.mp
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
mp :
  ∀ (hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))) (x : M) (h : x ∈ (↑I : Set R) • Set.range f),
    ∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
      (a.sum fun (i : ι) (c : R) ↦ c • f i) = x
mp₁ :
  ∀ (hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))),
    ∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
      Eq.{v + 1} (α := M) (a.sum fun (i : ι) (c : R) ↦ c • f i) 0
mp₂ :
  ∀ (hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))) (x y : M)
    (hx : Membership.mem (γ := Submodule R M) (span R ((↑I : Set R) • Set.range f)) x)
    (hy : Membership.mem (γ := Submodule R M) (span R ((↑I : Set R) • Set.range f)) y),
    (∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
        (a.sum fun (i : ι) (c : R) ↦ c • f i) = x) →
      (∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
          (a.sum fun (i : ι) (c : R) ↦ c • f i) = y) →
        ∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
          (a.sum fun (i : ι) (c : R) ↦ c • f i) = x + y
mp₃ :
  ∀ (hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))) (a : R) (x : M)
    (hx : Membership.mem (γ := Submodule R M) (span R ((↑I : Set R) • Set.range f)) x),
    (∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
        (a.sum fun (i : ι) (c : R) ↦ c • f i) = x) →
      ∃ (a_2 : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a_2 : (a : ι) → R) i : R)),
        (a_2.sum fun (i : ι) (c : R) ↦ c • f i) = a • x
⊢ x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f)) →
    ∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
      (a.sum fun (i : ι) (c : R) ↦ c • f i) = x

Tactic:
refine fun hx => span_induction ?_ ?_ ?_ ?_ (mem_smul_span.mp hx)
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
y : R
hy : y ∈ (↑I : Set R)
i : ι
⊢ ∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
    Eq.{v + 1} (α := M) (a.sum fun (i : ι) (c : R) ↦ c • f i) ((fun (x1 : R) (x2 : M) ↦ x1 • x2) y (f i))

Tactic:
⟨Finsupp.single i y, fun j => ?_, ?_⟩

Premises used: Exists.intro, Finsupp.single
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
y : R
hy : y ∈ (↑I : Set R)
i : ι
mp : ∀ (j : ι), Membership.mem (α := R) I ((Finsupp.single i y : (a : ι) → R) j : R)
mp₁ :
  Eq.{v + 1} (α := M) (Finsupp.sum (Finsupp.single i y) fun (i : ι) (c : R) ↦ c • f i)
    ((fun (x1 : R) (x2 : M) ↦ x1 • x2) y (f i))
⊢ ∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
    Eq.{v + 1} (α := M) (a.sum fun (i : ι) (c : R) ↦ c • f i) ((fun (x1 : R) (x2 : M) ↦ x1 • x2) y (f i))

Tactic:
refine ⟨Finsupp.single i y, fun j => ?_, ?_⟩
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
y : R
hy : y ∈ (↑I : Set R)
i j : ι
this : DecidableEq ι := Classical.decEq ι
mp : (if i = j then y else 0) ∈ I
⊢ Membership.mem (α := R) I ((Finsupp.single i y : (a : ι) → R) j : R)

Tactic:
rw [Finsupp.single_apply]

Premises used: Finsupp.single_apply
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
y : R
hy : y ∈ (↑I : Set R)
i j : ι
this : DecidableEq ι := Classical.decEq ι
pos : i = j → y ∈ I
neg : ¬i = j → 0 ∈ I
⊢ (if i = j then y else 0) ∈ I

Tactic:
split_ifs
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
y : R
hy : y ∈ (↑I : Set R)
i j : ι
this : DecidableEq ι := Classical.decEq ι
h : i = j
⊢ y ∈ I

Tactic:
assumption
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
y : R
hy : y ∈ (↑I : Set R)
i j : ι
this : DecidableEq ι := Classical.decEq ι
h : ¬i = j
⊢ 0 ∈ I

Tactic:
I.zero_mem

Premises used: Ideal.zero_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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
y : R
hy : y ∈ (↑I : Set R)
i j : ι
this : DecidableEq ι := Classical.decEq ι
h : ¬i = j
⊢ 0 ∈ I

Tactic:
exact I.zero_mem

Premises used: Ideal.zero_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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
y : R
hy : y ∈ (↑I : Set R)
i : ι
⊢ Eq.{v + 1} (α := M) (Finsupp.sum (Finsupp.single i y) fun (i : ι) (c : R) ↦ c • f i)
    ((fun (x1 : R) (x2 : M) ↦ x1 • x2) y (f i))

Tactic:
@Finsupp.sum_single_index ι R M _ _ i _ (fun i y => y • f i) ?_

Premises used: Finsupp.sum_single_index
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
y : R
hy : y ∈ (↑I : Set R)
i : ι
mp : Eq.{v + 1} (α := M) ((fun (i : ι) (y : R) ↦ y • f i) i 0) 0
⊢ Eq.{v + 1} (α := M) (Finsupp.sum (Finsupp.single i y) fun (i : ι) (c : R) ↦ c • f i)
    ((fun (x1 : R) (x2 : M) ↦ x1 • x2) y (f i))

Tactic:
refine @Finsupp.sum_single_index ι R M _ _ i _ (fun i y => y • f i) ?_

Premises used: Finsupp.sum_single_index
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
y : R
hy : y ∈ (↑I : Set R)
i : ι
⊢ Eq.{v + 1} (α := M) ((fun (i : ι) (y : R) ↦ y • f i) i 0) 0

Tactic:
simp
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
⊢ ∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
    Eq.{v + 1} (α := M) (a.sum fun (i : ι) (c : R) ↦ c • f i) 0

Tactic:
⟨0, fun _ => I.zero_mem, Finsupp.sum_zero_index⟩

Premises used: Ideal.zero_mem, Exists.intro, Finsupp.sum_zero_index, 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
I : Ideal R
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
⊢ ∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
    Eq.{v + 1} (α := M) (a.sum fun (i : ι) (c : R) ↦ c • f i) 0

Tactic:
exact ⟨0, fun _ => I.zero_mem, Finsupp.sum_zero_index⟩
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
ax : ι →₀ R
hax : ∀ (i : ι), Membership.mem (α := R) I ((ax : (a : ι) → R) i : R)
ay : ι →₀ R
hay : ∀ (i : ι), Membership.mem (α := R) I ((ay : (a : ι) → R) i : R)
⊢ ∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
    (a.sum fun (i : ι) (c : R) ↦ c • f i) =
      HAdd.hAdd (α := M) (ax.sum fun (i : ι) (c : R) ↦ c • f i) (ay.sum fun (i : ι) (c : R) ↦ c • f i)

Tactic:
⟨ax + ay, fun i => I.add_mem (hax i) (hay i), Finsupp.sum_add_index' ?_ ?_⟩

Premises used: Finsupp.sum_add_index', Ideal.add_mem, HAdd.hAdd, Exists.intro
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
ax : ι →₀ R
hax : ∀ (i : ι), Membership.mem (α := R) I ((ax : (a : ι) → R) i : R)
ay : ι →₀ R
hay : ∀ (i : ι), Membership.mem (α := R) I ((ay : (a : ι) → R) i : R)
mp : ∀ (a : ι), HSMul.hSMul.{u, v, v} (α := R) 0 (f a) = 0
mp₁ : ∀ (a : ι) (b₁ b₂ : R), (b₁ + b₂) • f a = b₁ • f a + b₂ • f a
⊢ ∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
    (a.sum fun (i : ι) (c : R) ↦ c • f i) =
      HAdd.hAdd (α := M) (ax.sum fun (i : ι) (c : R) ↦ c • f i) (ay.sum fun (i : ι) (c : R) ↦ c • f i)

Tactic:
refine ⟨ax + ay, fun i => I.add_mem (hax i) (hay i), Finsupp.sum_add_index' ?_ ?_⟩
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
ax : ι →₀ R
hax : ∀ (i : ι), Membership.mem (α := R) I ((ax : (a : ι) → R) i : R)
ay : ι →₀ R
hay : ∀ (i : ι), Membership.mem (α := R) I ((ay : (a : ι) → R) i : R)
a : ι
⊢ HSMul.hSMul.{u, v, v} (α := R) 0 (f a) = 0

Tactic:
simp only [zero_smul, add_smul]

Premises used: zero_smul, add_smul
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
ax : ι →₀ R
hax : ∀ (i : ι), Membership.mem (α := R) I ((ax : (a : ι) → R) i : R)
ay : ι →₀ R
hay : ∀ (i : ι), Membership.mem (α := R) I ((ay : (a : ι) → R) i : R)
a : ι
b₁ b₂ : R
⊢ (b₁ + b₂) • f a = b₁ • f a + b₂ • f a

Tactic:
simp only [zero_smul, add_smul]

Premises used: zero_smul, add_smul
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
c : R
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
⊢ ∃ (a_1 : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a_1 : (a : ι) → R) i : R)),
    (a_1.sum fun (i : ι) (c : R) ↦ c • f i) = HSMul.hSMul (β := M) c (a.sum fun (i : ι) (c : R) ↦ c • f i)

Tactic:
⟨c • a, fun i => I.mul_mem_left c (ha i), ?_⟩

Premises used: Exists.intro, HSMul.hSMul, Ideal.mul_mem_left
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
c : R
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
mp : ((c • a).sum fun (i : ι) (c : R) ↦ c • f i) = HSMul.hSMul (β := M) c (a.sum fun (i : ι) (c : R) ↦ c • f i)
⊢ ∃ (a_1 : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a_1 : (a : ι) → R) i : R)),
    (a_1.sum fun (i : ι) (c : R) ↦ c • f i) = HSMul.hSMul (β := M) c (a.sum fun (i : ι) (c : R) ↦ c • f i)

Tactic:
refine ⟨c • a, fun i => I.mul_mem_left c (ha i), ?_⟩
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
c : R
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
mp : Eq.{v + 1} (α := M) (a.sum fun (i : ι) (a : R) ↦ (c * a) • f i) (a.sum fun (a : ι) (b : R) ↦ c • b • f a)
mp₁ : ∀ (i : ι), HSMul.hSMul.{u, v, v} (α := R) 0 (f i) = 0
⊢ ((c • a).sum fun (i : ι) (c : R) ↦ c • f i) = HSMul.hSMul (β := M) c (a.sum fun (i : ι) (c : R) ↦ c • f i)

Tactic:
rw [Finsupp.sum_smul_index, Finsupp.smul_sum]

Premises used: Finsupp.sum_smul_index, Finsupp.smul_sum
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
c : R
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
⊢ Eq.{v + 1} (α := M) (a.sum fun (i : ι) (a : R) ↦ (c * a) • f i) (a.sum fun (a : ι) (b : R) ↦ c • b • f a)

Tactic:
simp only [zero_smul, mul_smul]

Premises used: zero_smul, SemigroupAction.mul_smul
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
c : R
a : ι →₀ R
ha : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)
i : ι
⊢ HSMul.hSMul.{u, v, v} (α := R) 0 (f i) = 0

Tactic:
simp only [zero_smul, mul_smul]

Premises used: zero_smul, SemigroupAction.mul_smul
-- 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
inst_3 : I.IsTwoSided
ι : Type u_4
s : Set ι
f : ι → M
x : M
rw :
  x ∈ HSMul.hSMul (β := Submodule R M) I (span R (f '' s)) ↔
    x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range fun (i : (↑s : Type u_4)) ↦ f (↑i : ι)))
rw₁ rw₂ :
  x ∈ HSMul.hSMul (β := Submodule R M) I (span R (f '' s)) ↔ x ∈ HSMul.hSMul (β := Submodule R M) I (span R (f '' s))
⊢ x ∈ HSMul.hSMul (β := Submodule R M) I (span R (f '' s)) ↔
    ∃ (a : Finsupp.{u_4, u} (↑s : Type u_4) R) (_ :
      ∀ (i : (↑s : Type u_4)), Membership.mem (α := R) I ((a : (a : (↑s : Type u_4)) → R) i : R)),
      (a.sum fun (i : (↑s : Type u_4)) (c : R) ↦ c • f (↑i : ι)) = x

Tactic:
rw [← Submodule.mem_ideal_smul_span_iff_exists_sum, ← Set.image_eq_range]

Premises used: Submodule.mem_ideal_smul_span_iff_exists_sum, Set.image_eq_range
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
⊢ I • N = map₂ (LinearMap.lsmul R M) I N

Tactic:
le_antisymm (smul_le.mpr fun _m hm _n ↦ Submodule.apply_mem_map₂ _ hm)
    (map₂_le.mpr fun _m hm _n ↦ smul_mem_smul hm)

Premises used: Iff.mpr, LinearMap.lsmul, Submodule.apply_mem_map₂, le_antisymm, Submodule.map₂_le, Submodule.smul_le, Submodule.smul_mem_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
N : Submodule R M
rw : span R (HSMul.hSMul (α := Set R) {r} (↑N : Set M))
| HSMul.hSMul (α := Ideal R) (Ideal.span {r}) N

Tactic:
rw [← span_eq N, span_smul_span]

Premises used: Submodule.span_eq, Submodule.span_smul_span
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
N : Submodule R M
conv_lhs : span R (HSMul.hSMul (α := Set R) {r} (↑N : Set M)) = r • N
⊢ HSMul.hSMul (α := Ideal R) (Ideal.span {r}) N = r • N

Tactic:
conv_lhs => rw [← span_eq N, span_smul_span]

Premises used: Submodule.span_eq, Submodule.span_smul_span
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
N : Submodule R M
⊢ span R (HSMul.hSMul (α := Set R) {r} (↑N : Set M)) = r • N

Tactic:
simpa using span_eq (r • N)

Premises used: Submodule.span_eq, HSMul.hSMul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : CommSemiring 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)), ∃ (n : ℕ), (↑r : R) ^ n • x ∈ M'
choose : ∀ (f : (r : (↑s : Type u)) → ℕ) (hf : ∀ (r : (↑s : Type u)), (↑r : R) ^ f r • x ∈ M'), x ∈ M'
⊢ x ∈ M'

Tactic:
choose f hf using H
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : CommSemiring 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
f : (r : (↑s : Type u)) → ℕ
hf : ∀ (r : (↑s : Type u)), (↑r : R) ^ f r • x ∈ M'
H : ∀ (r : (↑(Set.range fun (x : (↑s : Type u)) ↦ (↑x : R) ^ f x) : Type u)), (↑r : R) • x ∈ M'
⊢ x ∈ M'

Tactic:
apply M'.mem_of_span_top_of_smul_mem _ (Ideal.span_range_pow_eq_top s hs f)

Premises used: Submodule.mem_of_span_top_of_smul_mem, Ideal.span_range_pow_eq_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : CommSemiring 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
f : (r : (↑s : Type u)) → ℕ
hf : ∀ (r : (↑s : Type u)), (↑r : R) ^ f r • x ∈ M'
r : (↑s : Type u)
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) (Set.range fun (x : (↑s : Type u)) ↦ (↑x : R) ^ f x) x)
            ((fun (x : (↑s : Type u)) ↦ (↑x : R) ^ f x) r) ⋯) :
        R) •
      x ∈
    M'

Tactic:
hf r

Premises used: Set.Mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
inst : CommSemiring 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
f : (r : (↑s : Type u)) → ℕ
hf : ∀ (r : (↑s : Type u)), (↑r : R) ^ f r • x ∈ M'
r : (↑s : Type u)
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) (Set.range fun (x : (↑s : Type u)) ↦ (↑x : R) ^ f x) x)
            ((fun (x : (↑s : Type u)) ↦ (↑x : R) ^ f x) r) ⋯) :
        R) •
      x ∈
    M'

Tactic:
exact hf r
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
M : Type v
M' : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
r : R
N : Submodule R M
f : M →ₗ[R] M'
simp_rw : map f (HSMul.hSMul (α := Ideal R) (Ideal.span {r}) N) = HSMul.hSMul (α := Ideal R) (Ideal.span {r}) (map f N)
⊢ map f (r • N) = r • map f N

Tactic:
simp_rw [← ideal_span_singleton_smul, map_smul'']

Premises used: Submodule.ideal_span_singleton_smul, Submodule.map_smul''
-- 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
inst : Semiring R
⊢ Eq.{u + 1} (α := Ideal R) 0 ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
⊢ s.sum f = s.sup f

Tactic:
rfl

Premises used: Finset.fold, Finset.sup, rfl, Multiset.fold
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
rw : Eq (α := Ideal R) (R ∙ 1) ⊤
rw₁ : Eq (α := Ideal R) (span {1}) ⊤
rw₂ rw₃ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
⊢ Eq.{u + 1} (α := Ideal R) 1 ⊤

Tactic:
rw [Submodule.one_eq_span, ← Ideal.span, Ideal.span_singleton_one]

Premises used: Ideal.span_singleton_one, Ideal.span, Submodule.one_eq_span
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
rw : I + J = ⊤ ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
rw₁ : 1 ∈ I + J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
rw₂ : 1 ∈ I ⊔ J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
rw₃ rw₄ : (∃ y ∈ I, ∃ z ∈ J, y + z = 1) ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
⊢ I + J = 1 ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1

Tactic:
rw [one_eq_top, eq_top_iff_one, add_eq_sup, Submodule.mem_sup]

Premises used: Ideal.one_eq_top, Ideal.eq_top_iff_one, Ideal.add_eq_sup, Submodule.mem_sup
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
r s : R
hr : r ∈ I
hs : s ∈ J
⊢ r * s ∈ I * J

Tactic:
Submodule.smul_mem_smul hr hs

Premises used: Set.Mem, Submodule.smul_mem_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : n ≠ 0
⊢ HPow.hPow (α := Ideal R) ⊥ n = ⊥

Tactic:
Submodule.bot_pow hn

Premises used: Submodule.bot_pow
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
x : R
hx : x ∈ I
n : ℕ
⊢ x ^ n ∈ I ^ n

Tactic:
Submodule.pow_mem_pow _ hx _

Premises used: Set.Mem, Submodule.pow_mem_pow
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
⊢ I * J ≤ K ↔ ∀ r ∈ I, ∀ s ∈ J, r * s ∈ K

Tactic:
Submodule.smul_le

Premises used: Set.Mem, Submodule.smul_le
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
⊢ I * J ≤ J

Tactic:
mul_le.2 fun _ _ _ => J.mul_mem_left _

Premises used: Iff.mpr, Ideal.mul_le, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
⊢ I ⊔ J * I = I

Tactic:
sup_eq_left.2 mul_le_left

Premises used: Iff.mpr, sup_eq_left, Ideal.mul_le_left
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
⊢ J * I ⊔ I = I

Tactic:
sup_eq_right.2 mul_le_left

Premises used: Iff.mpr, Ideal.mul_le_left, sup_eq_right
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : I.IsTwoSided
⊢ I * J ≤ I

Tactic:
mul_le.2 fun _ hr _ _ ↦ I.mul_mem_right _ hr

Premises used: Iff.mpr, Ideal.mul_le, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : I.IsTwoSided
⊢ I ⊔ I * J = I

Tactic:
sup_eq_left.2 mul_le_right

Premises used: Iff.mpr, Ideal.mul_le_right, sup_eq_left
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
inst_1 : I.IsTwoSided
⊢ I * J ⊔ I = I

Tactic:
sup_eq_right.2 mul_le_right

Premises used: Iff.mpr, Ideal.mul_le_right, sup_eq_right
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K : Ideal R
⊢ I * J * K = I * (J * K)

Tactic:
Submodule.smul_assoc I J K

Premises used: Set.Mem, Submodule.smul_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
⊢ I * ⊥ = ⊥

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
⊢ ⊥ * I = ⊥

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I : Ideal R
⊢ ⊤ * I = I

Tactic:
Submodule.top_smul I

Premises used: Submodule.top_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : Semiring R
I J K L : Ideal R
hik : I ≤ K
hjl : J ≤ L
⊢ I * J ≤ K * L

Tactic:
Submodule.smul_mono hik hjl

Premises used: Submodule.smul_mono, Set.Mem