awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : x ∈ comap f S
⊢ r • x ∈ comap f (I • S)
have hx₁ : Membership.mem (α := M') S ((f : (a : M) → M') x : M')
Tactic: rw [Submodule.mem_comap] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : Membership.mem (α := M') S ((f : (a : M) → M') x : M')
⊢ Membership.mem (α := M') (I • S) ((f : (a : M) → M') (r • x) : M')
have rw : HSMul.hSMul (β := M') r ((f : (a : M) → M') x : M') ∈ I • S
Tactic: rw [f.map_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{v + 1, w + 1} (α := M) (β := M') (⇑f : (a : M) → M')
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
⊢ comap f (I • p) = I • comap f p
have refine : comap f (I • p) ≤ I • comap f p
Tactic: refine le_antisymm ?_ (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{v + 1, w + 1} (α := M) (β := M') (⇑f : (a : M) → M')
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
| comap f (I • p)
have rw : comap f (map f (I • comap f p))
Tactic: rw [← Submodule.map_comap_eq_self hp, ← Submodule.map_smul'']
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{v + 1, w + 1} (α := M) (β := M') (⇑f : (a : M) → M')
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
⊢ comap f (I • p) ≤ I • comap f p
have conv_lhs : comap f (map f (I • comap f p)) ≤ I • comap f p
Tactic: conv_lhs => rw [← Submodule.map_comap_eq_self hp, ← Submodule.map_smul'']
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{v + 1, w + 1} (α := M) (β := M') (⇑f : (a : M) → M')
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
⊢ comap f (map f (I • comap f p)) ≤ I • comap f p
have rw : I • comap f p ≤ I • comap f p
Tactic: rw [Submodule.comap_map_eq_of_injective hf]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
m x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (R ∙ m)
m1 m2 : M
h : ∃ y ∈ I, y • m = m1
h_1 : ∃ y ∈ I, y • m = m2
y1 : R
hyi1 : y1 ∈ I
hy1 : y1 • m = m1
y2 : R
hyi2 : y2 ∈ I
hy2 : y2 • m = m2
⊢ (y1 + y2) • m = m1 + m2
have rw : y1 • m + y2 • m = m1 + m2
Tactic: rw [add_smul, hy1, hy2]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
m x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (R ∙ m)
m1 m2 : M
h : ∃ y ∈ I, y • m = m1
h_1 : ∃ y ∈ I, y • m = m2
y1 : R
hyi1 : y1 ∈ I
hy1 : y1 • m = m1
y2 : R
hyi2 : y2 ∈ I
hy2 : y2 • m = m2
rw : y1 • m + y2 • m = m1 + m2
⊢ (y1 + y2) • m = m1 + m2
have rw₁ : m1 + y2 • m = m1 + m2
Tactic: rw [add_smul, hy1, hy2]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
m x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I (R ∙ m)
m1 m2 : M
h : ∃ y ∈ I, y • m = m1
h_1 : ∃ y ∈ I, y • m = m2
y1 : R
hyi1 : y1 ∈ I
hy1 : y1 • m = m1
y2 : R
hyi2 : y2 ∈ I
hy2 : y2 • m = m2
rw : y1 • m + y2 • m = m1 + m2
rw₁ : m1 + y2 • m = m1 + m2
⊢ (y1 + y2) • m = m1 + m2
have rw₂ : m1 + m2 = m1 + m2
Tactic: rw [add_smul, hy1, hy2]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
m : M
hm : Membership.mem (γ := Submodule R M) (span R T) m
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) (r • m)
have revert : ∀ (r : R) (hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r),
  Membership.mem (γ := Submodule R M) (span R (S • T)) (r • m)
Tactic: revert r
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (span R T) m_1
m : M
hm : m ∈ T
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) (HSMul.hSMul.{u, v, v} (α := R) 0 m)
have rw : Membership.mem (γ := Submodule R M) (span R (S • T)) 0
Tactic: rw [zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (span R T) m_1
m : M
hm : m ∈ T
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
x x_1 : R
h : Membership.mem (γ := Submodule R R) (span R S) x
h_1 : Membership.mem (γ := Submodule R R) (span R S) x_1
h₁ : Membership.mem (γ := Submodule R M) (span R (S • T)) (x • m)
h₂ : Membership.mem (γ := Submodule R M) (span R (S • T)) (x_1 • m)
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) ((x + x_1) • m)
have rw : Membership.mem (γ := Submodule R M) (span R (S • T)) (x • m + x_1 • m)
Tactic: rw [add_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (span R T) m_1
m : M
hm : m ∈ T
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
x x_1 : R
h_1 : Membership.mem (γ := Submodule R R) (span R S) x_1
h : Membership.mem (γ := Submodule R M) (span R (S • T)) (x_1 • m)
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) ((x • x_1) • m)
have rw : Membership.mem (γ := Submodule R M) (span R (S • T)) (x • x_1 • m)
Tactic: rw [smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m : M
hm : Membership.mem (γ := Submodule R M) (span R T) m
x : R
h : Membership.mem (γ := Submodule R R) (Ideal.span S) x
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) (HSMul.hSMul (β := M) x 0)
have rw : Membership.mem (γ := Submodule R M) (span R (S • T)) 0
Tactic: rw [smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m : M
hm : Membership.mem (γ := Submodule R M) (span R T) m
x x_1 : M
h : Membership.mem (γ := Submodule R M) (span R T) x
h_1 : Membership.mem (γ := Submodule R M) (span R T) x_1
h₁ :
  ∀ (r : R) (hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r),
    Membership.mem (γ := Submodule R M) (span R (S • T)) (r • x)
h₂ :
  ∀ (r : R) (hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r),
    Membership.mem (γ := Submodule R M) (span R (S • T)) (r • x_1)
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) (r • (x + x_1))
have rw : Membership.mem (γ := Submodule R M) (span R (S • T)) (r • x + r • x_1)
Tactic: rw [smul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set R
T : Set M
inst_3 : Ideal.IsTwoSided (Ideal.span S)
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (span R T) m_1
r' : R
m : M
hm : Membership.mem (γ := Submodule R M) (span R T) m
mem :
  ∀ (r : R) (hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r),
    Membership.mem (γ := Submodule R M) (span R (S • T)) (r • m)
r : R
hr : Membership.mem (γ := Submodule R R) (Ideal.span S) r
⊢ Membership.mem (γ := Submodule R M) (span R (S • T)) (r • r' • m)
have rw : Membership.mem (γ := Submodule R M) (span R (S • T)) ((r * r') • m)
Tactic: rw [← mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
s : Set M
x : M
⊢ x ∈ HSMul.hSMul (β := Submodule R M) I (span R s) ↔ Membership.mem (γ := Submodule R M) (span R ((↑I : Set R) • s)) x
have rw : Ideal.IsTwoSided (Ideal.span (↑I : Set R)) →
  ∀ {s : Set M} {x : M},
    x ∈ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.span (↑I : Set R)) (span R s) ↔
      Membership.mem (γ := Submodule R M) (span R ((↑(Ideal.span (↑I : Set R)) : Set R) • s)) x
Tactic: rw [← I.span_eq] at *
Cleared hypotheses: inst_3, s, x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
inst_3 : Ideal.IsTwoSided (Ideal.span (↑I : Set R))
s : Set M
x : M
⊢ x ∈ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.span (↑I : Set R)) (span R s) ↔
    Membership.mem (γ := Submodule R M) (span R ((↑(Ideal.span (↑I : Set R)) : Set R) • s)) x
have rw : Membership.mem (γ := Submodule R M) (span R ((↑I : Set R) • s)) x ↔
  Membership.mem (γ := Submodule R M) (span R ((↑(Ideal.span (↑I : Set R)) : Set R) • s)) x
Tactic: rw [Submodule.span_smul_span, I.span_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
inst_3 : Ideal.IsTwoSided (Ideal.span (↑I : Set R))
s : Set M
x : M
rw :
  Membership.mem (γ := Submodule R M) (span R ((↑I : Set R) • s)) x ↔
    Membership.mem (γ := Submodule R M) (span R ((↑(Ideal.span (↑I : Set R)) : Set R) • s)) x
⊢ x ∈ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.span (↑I : Set R)) (span R s) ↔
    Membership.mem (γ := Submodule R M) (span R ((↑(Ideal.span (↑I : Set R)) : Set R) • s)) x
have rw₁ : Membership.mem (γ := Submodule R M) (span R ((↑I : Set R) • s)) x ↔
  Membership.mem (γ := Submodule R M) (span R ((↑I : Set R) • s)) x
Tactic: rw [Submodule.span_smul_span, I.span_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
have mp : 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: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 :
  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
⊢ 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
have mpr : (∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
    (a.sum fun (i : ι) (c : R) ↦ c • f i) = x) →
  x ∈ HSMul.hSMul (β := Submodule R M) I (span R (Set.range f))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
have 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
Tactic: refine fun hx => span_induction ?_ ?_ ?_ ?_ (mem_smul_span.mp hx)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ 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
have 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
Tactic: refine fun hx => span_induction ?_ ?_ ?_ ?_ (mem_smul_span.mp hx)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ 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
have 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
Tactic: refine fun hx => span_induction ?_ ?_ ?_ ?_ (mem_smul_span.mp hx)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ 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
have 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
Tactic: refine fun hx => span_induction ?_ ?_ ?_ ?_ (mem_smul_span.mp hx)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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))
have mp : ∀ (j : ι), Membership.mem (α := R) I ((Finsupp.single i y : (a : ι) → R) j : R)
Tactic: refine ⟨Finsupp.single i y, fun j => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
⊢ ∃ (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))
have 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))
Tactic: refine ⟨Finsupp.single i y, fun j => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 ι
⊢ Membership.mem (α := R) I ((Finsupp.single i y : (a : ι) → R) j : R)
have mp : (if i = j then y else 0) ∈ I
Tactic: rw [Finsupp.single_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 ι
⊢ (if i = j then y else 0) ∈ I
have pos : i = j → y ∈ I
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ (if i = j then y else 0) ∈ I
have neg : ¬i = j → 0 ∈ I
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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))
have mp : Eq.{v + 1} (α := M) ((fun (i : ι) (y : R) ↦ y • f i) i 0) 0
Tactic: refine @Finsupp.sum_single_index ι R M _ _ i _ (fun i y => y • f i) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
have mp : ∀ (a : ι), HSMul.hSMul.{u, v, v} (α := R) 0 (f a) = 0
Tactic: refine ⟨ax + ay, fun i => I.add_mem (hax i) (hay i), Finsupp.sum_add_index' ?_ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ ∃ (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)
have mp₁ : ∀ (a : ι) (b₁ b₂ : R), (b₁ + b₂) • f a = b₁ • f a + b₂ • f a
Tactic: refine ⟨ax + ay, fun i => I.add_mem (hax i) (hay i), Finsupp.sum_add_index' ?_ ?_⟩