awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
x : M
obtain :
  ∀ (y : Finsupp.{u_3, u_1} (↥s) R)
    (hy :
      Eq.{u_3 + 1} (α := N) ((linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)) : (a : ↥s →₀ R) → N) y : N)
        ((l : (a : M) → N) x : N)),
    Membership.mem (α := M ⧸ f.range) (Submodule.map f.range.mkQ l.ker)
      ((f.range.mkQ : (a : M) → M ⧸ f.range) x : M ⧸ f.range)
⊢ Membership.mem (α := M ⧸ f.range) (Submodule.map f.range.mkQ l.ker)
    ((f.range.mkQ : (a : M) → M ⧸ f.range) x : M ⧸ f.range)

Tactic:
obtain ⟨y, hy⟩ := H (l x)

Premises used: DFunLike.coe
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
x : M
y : Finsupp.{u_3, u_1} (↥s) R
hy :
  Eq.{u_3 + 1} (α := N) ((linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)) : (a : ↥s →₀ R) → N) y : N)
    ((l : (a : M) → N) x : N)
⊢ Eq.{u_3 + 1} (α := N) ((l : (a : M) → N) (HSub.hSub (β := M) x ((f : (a : ↥s →₀ R) → M) y : M)) : N) (0 : N)

Tactic:
rw [← hf, LinearMap.comp_apply, eq_comm, ← sub_eq_zero, ← map_sub] at hy

Premises used: map_sub, sub_eq_zero, LinearMap.comp_apply, eq_comm
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
x : M
y : Finsupp.{u_3, u_1} (↥s) R
hy : Eq.{u_3 + 1} (α := N) ((l : (a : M) → N) (HSub.hSub (β := M) x ((f : (a : ↥s →₀ R) → M) y : M)) : N) (0 : N)
⊢ Eq (α := M ⧸ f.range)
    ((f.range.mkQ : (a : M) → M ⧸ f.range) (HSub.hSub (β := M) x ((f : (a : ↥s →₀ R) → M) y : M)) : M ⧸ f.range)
    ((f.range.mkQ : (a : M) → M ⧸ f.range) x : M ⧸ f.range)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
x : M
y : Finsupp.{u_3, u_1} (↥s) R
hy : Eq.{u_3 + 1} (α := N) ((l : (a : M) → N) (HSub.hSub (β := M) x ((f : (a : ↥s →₀ R) → M) y : M)) : N) (0 : N)
⊢ Membership.mem (α := M ⧸ f.range) (Submodule.map f.range.mkQ l.ker)
    ((f.range.mkQ : (a : M) → M ⧸ f.range) x : M ⧸ f.range)

Tactic:
exact ⟨_, hy, by simp⟩
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
⊢ Submodule.map f.range.mkQ l.ker = ⊤

Tactic:
have : (LinearMap.ker l).map (LinearMap.range f).mkQ = ⊤ := by
    rw [← top_le_iff]
    rintro x -
    obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x
    obtain ⟨y, hy⟩ := H (l x)
    rw [← hf, LinearMap.comp_apply, eq_comm, ← sub_eq_zero, ← map_sub] at hy
    exact ⟨_, hy, by simp⟩
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
this : Submodule.map f.range.mkQ l.ker = ⊤
hs1 : (Submodule.map f.range.mkQ l.ker).FG
hs2 : (l.ker ⊓ f.range.mkQ.ker).FG
⊢ l.ker.FG

Tactic:
apply Submodule.fg_of_fg_map_of_fg_inf_ker (LinearMap.range f).mkQ

Premises used: LinearMap.range, Submodule.mkQ, Submodule.fg_of_fg_map_of_fg_inf_ker
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
this : Submodule.map f.range.mkQ l.ker = ⊤
hs1 : Submodule.FG.{u_1, u_2} (R := R) (M := M ⧸ f.range) ⊤
⊢ (Submodule.map f.range.mkQ l.ker).FG

Tactic:
rw [this]
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
this : Submodule.map f.range.mkQ l.ker = ⊤
⊢ Submodule.FG.{u_1, u_2} (R := R) (M := M ⧸ f.range) ⊤

Tactic:
Module.Finite.fg_top

Premises used: Module.Finite.fg_top
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
this : Submodule.map f.range.mkQ l.ker = ⊤
⊢ Submodule.FG.{u_1, u_2} (R := R) (M := M ⧸ f.range) ⊤

Tactic:
exact Module.Finite.fg_top

Premises used: Module.Finite.fg_top
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
this : Submodule.map f.range.mkQ l.ker = ⊤
hs2 : (Submodule.map f (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))).FG
⊢ (l.ker ⊓ f.range.mkQ.ker).FG

Tactic:
rw [Submodule.ker_mkQ, inf_comm, ← Submodule.map_comap_eq, ← LinearMap.ker_comp, hf]

Premises used: Submodule.map_comap_eq, LinearMap.ker_comp, inf_comm, Submodule.ker_mkQ
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
this : Submodule.map f.range.mkQ l.ker = ⊤
⊢ (Submodule.map f (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))).FG

Tactic:
hs'.map f

Premises used: Submodule.FG.map
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
s : Finset N
hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤
hs' :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))
H :
  Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
    (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)
f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M
hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))
this : Submodule.map f.range.mkQ l.ker = ⊤
⊢ (Submodule.map f (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))).FG

Tactic:
exact hs'.map f

Premises used: Submodule.FG.map
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FinitePresentation R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
⊢ l.ker.FG ↔ FinitePresentation R N

Tactic:
⟨finitePresentation_of_surjective l hl, fun _ ↦ fg_ker l hl⟩

Premises used: Module.FinitePresentation.fg_ker, Module.finitePresentation_of_surjective, Iff.intro
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_6 : FinitePresentation.{u_1, u_3} R ↥l.ker
hs1 : (Submodule.map l ⊤).FG
hs2 : (⊤ ⊓ l.ker).FG
⊢ Submodule.FG.{u_1, u_3} (R := R) (M := M) ⊤

Tactic:
apply Submodule.fg_of_fg_map_of_fg_inf_ker l

Premises used: Submodule.fg_of_fg_map_of_fg_inf_ker
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_6 : FinitePresentation.{u_1, u_3} R ↥l.ker
hs1 : Submodule.FG.{u_1, u_2} (R := R) (M := N) ⊤
⊢ (Submodule.map l ⊤).FG

Tactic:
rw [Submodule.map_top, LinearMap.range_eq_top.mpr hl]

Premises used: Iff.mpr, Submodule.map_top, LinearMap.range_eq_top
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_6 : FinitePresentation.{u_1, u_3} R ↥l.ker
⊢ Submodule.FG.{u_1, u_2} (R := R) (M := N) ⊤

Tactic:
Module.Finite.fg_top

Premises used: Module.Finite.fg_top
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_6 : FinitePresentation.{u_1, u_3} R ↥l.ker
⊢ Submodule.FG.{u_1, u_2} (R := R) (M := N) ⊤

Tactic:
exact Module.Finite.fg_top

Premises used: Module.Finite.fg_top
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_6 : FinitePresentation.{u_1, u_3} R ↥l.ker
hs2 : Module.Finite.{u_1, u_3} R ↥l.ker
⊢ (⊤ ⊓ l.ker).FG

Tactic:
rw [top_inf_eq, ← Module.Finite.iff_fg]

Premises used: top_inf_eq, Module.Finite.iff_fg
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_6 : FinitePresentation.{u_1, u_3} R ↥l.ker
⊢ Module.Finite.{u_1, u_3} R ↥l.ker

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_6 : FinitePresentation.{u_1, u_3} R ↥l.ker
obtain : ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤), FinitePresentation R M
⊢ FinitePresentation R M

Tactic:
obtain ⟨s, hs⟩ : (⊤ : Submodule R M).FG := by
    apply Submodule.fg_of_fg_map_of_fg_inf_ker l
    · rw [Submodule.map_top, LinearMap.range_eq_top.mpr hl]; exact Module.Finite.fg_top
    · rw [top_inf_eq, ← Module.Finite.iff_fg]; infer_instance

Premises used: Submodule.FG, Top.top
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_6 : FinitePresentation.{u_1, u_3} R ↥l.ker
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
⊢ FinitePresentation R M

Tactic:
⟨s, hs, ?_⟩

Premises used: Module.FinitePresentation.mk, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_6 : FinitePresentation.{u_1, u_3} R ↥l.ker
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
refine :
  Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
⊢ FinitePresentation R M

Tactic:
refine ⟨s, hs, ?_⟩
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_6 : FinitePresentation.{u_1, u_3} R ↥l.ker
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
π : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
rw :
  Eq.{u_3 + 1} (α := Submodule R M) (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) ⊤
rw₁ : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
rw₂ rw₃ : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) (Submodule.span R (↑s : Set M))
⊢ π.range = ⊤

Tactic:
rw [range_linearCombination, Subtype.range_val, ← hs]

Premises used: Subtype.range_val, Finsupp.range_linearCombination
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_6 : FinitePresentation.{u_1, u_3} R ↥l.ker
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
π : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
⊢ Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := M) (⇑π : (a : ↥s →₀ R) → M)

Tactic:
have H : Function.Surjective π :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hs])
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_6 : FinitePresentation.{u_1, u_3} R ↥l.ker
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
π : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
H : Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := M) (⇑π : (a : ↥s →₀ R) → M)
⊢ Module.Finite R ↥(l ∘ₗ π).ker

Tactic:
have inst : Module.Finite R (LinearMap.ker (l ∘ₗ π)) :=
    .of_fg <| Module.FinitePresentation.fg_ker _ (hl.comp H)
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst_1 : Ring R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_7 : FinitePresentation.{u_1, u_3} R ↥l.ker
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
π : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
H : Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := M) (⇑π : (a : ↥s →₀ R) → M)
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
h :
  ∀ (x : ↥(l ∘ₗ π).ker),
    Eq.{u_3 + 1} (α := M) ((π ∘ₗ (l ∘ₗ π).ker.subtype : (a : ↥(l ∘ₗ π).ker) → M) x : M)
      ((l.ker.subtype ∘ₗ f : (a : ↥(l ∘ₗ π).ker) → M) x : M)
⊢ π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f

Tactic:
ext
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst_1 : Ring R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_7 : FinitePresentation.{u_1, u_3} R ↥l.ker
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
π : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
H : Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := M) (⇑π : (a : ↥s →₀ R) → M)
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
x : ↥(l ∘ₗ π).ker
⊢ Eq.{u_3 + 1} (α := M) ((π ∘ₗ (l ∘ₗ π).ker.subtype : (a : ↥(l ∘ₗ π).ker) → M) x : M)
    ((l.ker.subtype ∘ₗ f : (a : ↥(l ∘ₗ π).ker) → M) x : M)

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_3
N : Type u_2
inst_1 : Ring R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_3 + 1, u_2 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
inst_7 : FinitePresentation.{u_1, u_3} R ↥l.ker
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
π : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M := linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
H : Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := M) (⇑π : (a : ↥s →₀ R) → M)
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
⊢ π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f

Tactic:
have e : π ∘ₗ Submodule.subtype _ = Submodule.subtype _ ∘ₗ f := by ext; rfl