awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
a :
  Membership.mem (γ := Submodule R M) (span R (g '' (↑t1 : Set P)))
    (AddHom.toFun (M := M →₀ R) (LinearMap.toAddHom (linearCombination R id))
      ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l))
⊢ Membership.mem (γ := Submodule R M) (span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M)) x
have a₁ : Membership.mem (γ := Submodule R M) (span R (↑t2 : Set M))
  (HSub.hSub (β := M) x
    ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M))
Tactic: refine
    mem_sup.2
      ⟨(linearCombination R id).toFun ((lmapDomain R R g : (P →₀ R) → M →₀ R) l), ?_,
        x - linearCombination R id ((lmapDomain R R g : (P →₀ R) → M →₀ R) l), ?_,
        add_sub_cancel _ _⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ Membership.mem (γ := Submodule R M) (span R (g '' (↑t1 : Set P)))
    (AddHom.toFun (M := M →₀ R) (LinearMap.toAddHom (linearCombination R id))
      ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l))
have a : ∃ (l_1 : M →₀ R),
  Membership.mem (γ := Submodule R (M →₀ R)) (supported R R (g '' (↑t1 : Set P))) l_1 ∧
    Eq.{u_2 + 1} (α := M) ((linearCombination R id : (a : M →₀ R) → M) l_1 : M)
      (AddHom.toFun (M := M →₀ R) (LinearMap.toAddHom (linearCombination R id))
          ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l) :
        M)
Tactic: rw [← Set.image_id (g '' ↑t1), Finsupp.mem_span_image_iff_linearCombination]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ ∃ (l_1 : M →₀ R),
    Membership.mem (γ := Submodule R (M →₀ R)) (supported R R (g '' (↑t1 : Set P))) l_1 ∧
      Eq.{u_2 + 1} (α := M) ((linearCombination R id : (a : M →₀ R) → M) l_1 : M)
        (AddHom.toFun (M := M →₀ R) (LinearMap.toAddHom (linearCombination R id))
            ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l) :
          M)
have a : Membership.mem (α := M →₀ R) (γ := Submodule R (M →₀ R)) (supported R R (g '' (↑t1 : Set P)))
  ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R)
Tactic: refine ⟨_, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ Membership.mem (α := M →₀ R) (γ := Submodule R (M →₀ R)) (supported R R (g '' (↑t1 : Set P)))
    ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R)
have a : ∀ (this : Inhabited P),
  Membership.mem (α := M →₀ R) (γ := Submodule R (M →₀ R)) (supported R R (g '' (↑t1 : Set P)))
    ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R)
Tactic: haveI : Inhabited P := ⟨0⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this_3 : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
this : Inhabited P
⊢ Membership.mem (α := M →₀ R) (γ := Submodule R (M →₀ R)) (supported R R (g '' (↑t1 : Set P)))
    ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R)
have a : ∃ (y : P →₀ R),
  Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) y ∧
    Eq (α := M →₀ R) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) y : M →₀ R)
      ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R)
Tactic: rw [← Finsupp.lmapDomain_supported _ _ g, mem_map]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this_3 : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
this : Inhabited P
⊢ ∃ (y : P →₀ R),
    Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) y ∧
      Eq (α := M →₀ R) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) y : M →₀ R)
        ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R)
have a : Eq (α := M →₀ R) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R)
  ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R)
Tactic: refine ⟨l, hl1, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ Membership.mem (γ := Submodule R M) (span R (↑t2 : Set M))
    (HSub.hSub (β := M) x
      ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M))
have a : HSub.hSub (β := M) x
      ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M) ∈
    s ∧
  HSub.hSub (β := M) x
      ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M) ∈
    f.ker
Tactic: rw [ht2, mem_inf]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ HSub.hSub (β := M) x
        ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M) ∈
      s ∧
    HSub.hSub (β := M) x
        ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M) ∈
      f.ker
have a : HSub.hSub (β := M) x
    ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M) ∈
  s
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
a :
  HSub.hSub (β := M) x
      ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M) ∈
    s
⊢ HSub.hSub (β := M) x
        ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M) ∈
      s ∧
    HSub.hSub (β := M) x
        ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M) ∈
      f.ker
have a₁ : HSub.hSub (β := M) x
    ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M) ∈
  f.ker
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ HSub.hSub (β := M) x
      ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M) ∈
    s
have a : Membership.mem (α := M) s
  ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M)
Tactic: apply s.sub_mem hx
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ Membership.mem (α := M) s
    ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M)
have a : (l.sum fun (a : P) (m : R) ↦ m • id (g a)) ∈ s
Tactic: rw [Finsupp.linearCombination_apply, Finsupp.lmapDomain_apply, Finsupp.sum_mapDomain_index]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
a : (l.sum fun (a : P) (m : R) ↦ m • id (g a)) ∈ s
⊢ Membership.mem (α := M) s
    ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M)
have a₁ : ∀ (b : M), HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (id b) = 0
Tactic: rw [Finsupp.linearCombination_apply, Finsupp.lmapDomain_apply, Finsupp.sum_mapDomain_index]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
a : (l.sum fun (a : P) (m : R) ↦ m • id (g a)) ∈ s
a₁ : ∀ (b : M), HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (id b) = 0
⊢ Membership.mem (α := M) s
    ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M)
have a₂ : ∀ (b : M) (m₁ m₂ : R), (m₁ + m₂) • id b = m₁ • id b + m₂ • id b
Tactic: rw [Finsupp.linearCombination_apply, Finsupp.lmapDomain_apply, Finsupp.sum_mapDomain_index]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ (l.sum fun (a : P) (m : R) ↦ m • id (g a)) ∈ s
have a : ∀ c ∈ l.support, (fun (a : P) (m : R) ↦ m • id (g a)) c ((l : (a : P) → R) c) ∈ s
Tactic: refine s.sum_mem ?_
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ HSub.hSub (β := M) x
      ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M) ∈
    f.ker
have a : HSub.hSub (α := P) (β := P) ((linearCombination R id : (a : P →₀ R) → P) l : P)
    ((f : (a : M) → P)
        ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M) :
      P) =
  0
Tactic: rw [LinearMap.mem_ker, f.map_sub, ← hl2]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ HSub.hSub (α := P) (β := P) ((linearCombination R id : (a : P →₀ R) → P) l : P)
      ((f : (a : M) → P)
          ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M) :
        P) =
    0
have a : HSub.hSub (α := P) (β := P) (l.sum fun (i : P) (a : R) ↦ a • id i : P)
    ((f : (a : M) → P) ((mapDomain g l).sum fun (i : M) (a : R) ↦ a • id i) : P) =
  0
Tactic: rw [Finsupp.linearCombination_apply, Finsupp.linearCombination_apply, Finsupp.lmapDomain_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ HSub.hSub (α := P) (β := P) (l.sum fun (i : P) (a : R) ↦ a • id i : P)
      ((f : (a : M) → P) ((mapDomain g l).sum fun (i : M) (a : R) ↦ a • id i) : P) =
    0
have a : HSub.hSub (α := P) (∑ a ∈ l.support, HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) a : R) (id a))
    (∑ x ∈ l.support, (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) x : R) (id (g x)))) =
  0
Tactic: rw [Finsupp.sum_mapDomain_index, Finsupp.sum, Finsupp.sum, map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
a :
  HSub.hSub (α := P) (∑ a ∈ l.support, HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) a : R) (id a))
      (∑ x ∈ l.support, (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) x : R) (id (g x)))) =
    0
⊢ HSub.hSub (α := P) (β := P) (l.sum fun (i : P) (a : R) ↦ a • id i : P)
      ((f : (a : M) → P) ((mapDomain g l).sum fun (i : M) (a : R) ↦ a • id i) : P) =
    0
have a₁ : ∀ (b : M), HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (id b) = 0
Tactic: rw [Finsupp.sum_mapDomain_index, Finsupp.sum, Finsupp.sum, map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
a :
  HSub.hSub (α := P) (∑ a ∈ l.support, HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) a : R) (id a))
      (∑ x ∈ l.support, (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) x : R) (id (g x)))) =
    0
a₁ : ∀ (b : M), HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (id b) = 0
⊢ HSub.hSub (α := P) (β := P) (l.sum fun (i : P) (a : R) ↦ a • id i : P)
      ((f : (a : M) → P) ((mapDomain g l).sum fun (i : M) (a : R) ↦ a • id i) : P) =
    0
have a₂ : ∀ (b : M) (m₁ m₂ : R), (m₁ + m₂) • id b = m₁ • id b + m₂ • id b
Tactic: rw [Finsupp.sum_mapDomain_index, Finsupp.sum, Finsupp.sum, map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Finsupp (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ HSub.hSub (α := P) (∑ a ∈ l.support, HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) a : R) (id a))
      (∑ x ∈ l.support, (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) x : R) (id (g x)))) =
    0
have a : Eq (α := P) (∑ a ∈ l.support, HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) a : R) (id a))
  (∑ x ∈ l.support, (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) x : R) (id (g x))))
Tactic: rw [sub_eq_zero]