awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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 ∈ (↑t2 : Set M)
⊢ Membership.mem (γ := Submodule R M) (span R (↑t2 : Set M)) x

Tactic:
have : x ∈ span R t2 := subset_span hx
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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 ∈ (↑t2 : Set M)
this : Membership.mem (γ := Submodule R M) (span R (↑t2 : Set M)) x
⊢ x ∈ s ⊓ f.ker

Tactic:
rw [ht2] at this
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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 ∈ (↑t2 : Set M)
this : x ∈ s ⊓ f.ker
⊢ x ∈ (↑s : Set M)

Tactic:
this.1

Premises used: And.left
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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 ∈ (↑t2 : Set M)
this : x ∈ s ⊓ f.ker
⊢ x ∈ (↑s : Set M)

Tactic:
exact this.1

Premises used: And.left
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
⊢ ∃ y ∈ s, Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) y : P) ((f : (a : M) → P) x : P)

Tactic:
⟨x, hx, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
⊢ ∃ y ∈ s, Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) y : P) ((f : (a : M) → P) x : P)

Tactic:
exact ⟨x, hx, rfl⟩
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
⊢ Membership.mem (α := P) (map f s) ((f : (a : M) → P) x : P)

Tactic:
have : f x ∈ s.map f := by
    rw [mem_map]
    exact ⟨x, hx, rfl⟩
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
this : Membership.mem (α := P) (map f s) ((f : (a : M) → P) x : P)
⊢ ∃ (l : P →₀ R),
    Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l ∧
      Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)

Tactic:
rw [← ht1, ← Set.image_id (t1 : Set P), Finsupp.mem_span_image_iff_linearCombination] at this

Premises used: SetLike.coe, Finsupp.mem_span_image_iff_linearCombination, Set.image_id
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
this :
  ∃ (l : P →₀ R),
    Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l ∧
      Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
a :
  ∀ (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)) ⊔ span R (↑t2 : Set M)) x
⊢ Membership.mem (γ := Submodule R M) (span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M)) x

Tactic:
rcases this with ⟨l, hl1, hl2⟩
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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)) ⊔ span R (↑t2 : Set M)) x

Tactic:
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 _ _⟩

Premises used: Iff.mpr, HSub.hSub, Finsupp.lmapDomain, id, LinearMap.toAddHom, add_sub_cancel, And.intro, Exists.intro, Submodule.mem_sup, Finsupp.linearCombination, DFunLike.coe, AddHom.toFun
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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))
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))
⊢ Membership.mem (γ := Submodule R M) (span R (g '' (↑t1 : Set P)) ⊔ span R (↑t2 : Set M)) x

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 _ _⟩

Premises used: Iff.mpr, HSub.hSub, Finsupp.lmapDomain, id, LinearMap.toAddHom, add_sub_cancel, And.intro, Exists.intro, Submodule.mem_sup, Finsupp.linearCombination, DFunLike.coe, AddHom.toFun
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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_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)
⊢ 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))

Tactic:
rw [← Set.image_id (g '' ↑t1), Finsupp.mem_span_image_iff_linearCombination]

Premises used: SetLike.coe, Set.image, Finsupp.mem_span_image_iff_linearCombination, Set.image_id
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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)

Tactic:
⟨_, ?_, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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 (α := 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)
⊢ ∃ (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:
refine ⟨_, ?_, rfl⟩
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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 :
  ∀ (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)
⊢ 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⟩
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
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)
⊢ 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:
rw [← Finsupp.lmapDomain_supported _ _ g, mem_map]

Premises used: Submodule.mem_map, Finsupp.lmapDomain_supported
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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)

Tactic:
⟨l, hl1, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
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)
⊢ ∃ (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:
refine ⟨l, hl1, ?_⟩
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
⊢ 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:
rfl
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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) ∈
      f.ker
⊢ 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:
rw [ht2, mem_inf]

Premises used: Submodule.mem_inf
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
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
⊢ 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:
constructor
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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 (α := M) s
    ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : 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) ∈
    s

Tactic:
apply s.sub_mem hx

Premises used: Submodule.sub_mem
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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
a₂ : ∀ (b : M) (m₁ m₂ : R), (m₁ + m₂) • id b = m₁ • id b + m₂ • id b
⊢ 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:
rw [Finsupp.linearCombination_apply, Finsupp.lmapDomain_apply, Finsupp.sum_mapDomain_index]

Premises used: Finsupp.sum_mapDomain_index, Finsupp.linearCombination_apply, Finsupp.lmapDomain_apply
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
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

Tactic:
s.sum_mem ?_

Premises used: Set.Mem, Submodule.sum_mem, Finsupp.sum