awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
h : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
obtain :
  ∀ (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))))),
    l.ker.FG
obtain₁ :
  ∀ (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)),
    l.ker.FG
obtain₂ :
  ∀ (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))), l.ker.FG
⊢ l.ker.FG
have obtain₃ : ∀ (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 = ⊤), l.ker.FG
Tactic: classical
  obtain ⟨s, hs, hs'⟩ := h
  have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → N)) :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hs])
  obtain ⟨f, hf⟩ : ∃ f : (s →₀ R) →ₗ[R] M, l ∘ₗ f = (Finsupp.linearCombination R Subtype.val) := by
    choose f hf using show _ from hl
    exact ⟨Finsupp.linearCombination R (fun i ↦ f i), by ext; simp [hf]⟩
  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⟩
  apply Submodule.fg_of_fg_map_of_fg_inf_ker (LinearMap.range f).mkQ
  · rw [this]
    exact Module.Finite.fg_top
  · rw [Submodule.ker_mkQ, inf_comm, ← Submodule.map_comap_eq, ← LinearMap.ker_comp, hf]
    exact hs'.map f
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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_3} (R := R) (M := M) ⊤
have hs1 : (Submodule.map l ⊤).FG
Tactic: apply Submodule.fg_of_fg_map_of_fg_inf_ker l
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
⊢ Submodule.FG.{u_1, u_3} (R := R) (M := M) ⊤
have hs2 : (⊤ ⊓ l.ker).FG
Tactic: apply Submodule.fg_of_fg_map_of_fg_inf_ker l
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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.map l ⊤).FG
have hs1 : Submodule.FG.{u_1, u_2} (R := R) (M := N) ⊤
Tactic: rw [Submodule.map_top, LinearMap.range_eq_top.mpr hl]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
⊢ (⊤ ⊓ l.ker).FG
have hs2 : Module.Finite.{u_1, u_3} R ↥l.ker
Tactic: rw [top_inf_eq, ← Module.Finite.iff_fg]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
⊢ FinitePresentation R M
have obtain : ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set 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
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
have refine : Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
  (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
Tactic: refine ⟨s, hs, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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))
⊢ π.range = ⊤
have rw : Eq.{u_3 + 1} (α := Submodule R M) (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) ⊤
Tactic: rw [range_linearCombination, Subtype.range_val, ← hs]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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)) ⊤
⊢ π.range = ⊤
have rw₂ : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) (Submodule.span R (↑s : Set M))
Tactic: rw [range_linearCombination, Subtype.range_val, ← hs]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
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))
⊢ Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
have H : 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])
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
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)
⊢ Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
have inst : Module.Finite R ↥(l ∘ₗ π).ker
Tactic: have inst : Module.Finite R (LinearMap.ker (l ∘ₗ π)) :=
    .of_fg <| Module.FinitePresentation.fg_ker _ (hl.comp H)
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
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 ⋯
⊢ Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
have e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
Tactic: have e : π ∘ₗ Submodule.subtype _ = Submodule.subtype _ ∘ₗ f := by ext; rfl
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
⊢ Function.Surjective (α := ↥(l ∘ₗ π).ker) (β := ↥l.ker) (⇑f : (a : ↥(l ∘ₗ π).ker) → ↥l.ker)
have rw : f.range = ⊤
Tactic: rw [← LinearMap.range_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
⊢ f.range = ⊤
have a : Submodule.map l.ker.subtype f.range = Submodule.map l.ker.subtype ⊤
Tactic: apply Submodule.map_injective_of_injective (Submodule.injective_subtype _)
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
⊢ Submodule.map l.ker.subtype f.range = Submodule.map l.ker.subtype ⊤
have a : Submodule.map l.ker.subtype f.range = l.ker.subtype.range
Tactic: rw [Submodule.map_top, Submodule.range_subtype, ← LinearMap.range_comp, ← e,
      LinearMap.range_comp, Submodule.range_subtype, LinearMap.ker_comp,
      Submodule.map_comap_eq_of_surjective H]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
a : Submodule.map l.ker.subtype f.range = l.ker.subtype.range
⊢ Submodule.map l.ker.subtype f.range = Submodule.map l.ker.subtype ⊤
have a₁ : Submodule.map l.ker.subtype f.range = l.ker
Tactic: rw [Submodule.map_top, Submodule.range_subtype, ← LinearMap.range_comp, ← e,
      LinearMap.range_comp, Submodule.range_subtype, LinearMap.ker_comp,
      Submodule.map_comap_eq_of_surjective H]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
a : Submodule.map l.ker.subtype f.range = l.ker.subtype.range
a₁ : Submodule.map l.ker.subtype f.range = l.ker
⊢ Submodule.map l.ker.subtype f.range = Submodule.map l.ker.subtype ⊤
have a₂ : (l.ker.subtype ∘ₗ f).range = l.ker
Tactic: rw [Submodule.map_top, Submodule.range_subtype, ← LinearMap.range_comp, ← e,
      LinearMap.range_comp, Submodule.range_subtype, LinearMap.ker_comp,
      Submodule.map_comap_eq_of_surjective H]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
a : Submodule.map l.ker.subtype f.range = l.ker.subtype.range
a₁ : Submodule.map l.ker.subtype f.range = l.ker
a₂ : (l.ker.subtype ∘ₗ f).range = l.ker
⊢ Submodule.map l.ker.subtype f.range = Submodule.map l.ker.subtype ⊤
have a₃ : (π ∘ₗ (l ∘ₗ π).ker.subtype).range = l.ker
Tactic: rw [Submodule.map_top, Submodule.range_subtype, ← LinearMap.range_comp, ← e,
      LinearMap.range_comp, Submodule.range_subtype, LinearMap.ker_comp,
      Submodule.map_comap_eq_of_surjective H]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
a : Submodule.map l.ker.subtype f.range = l.ker.subtype.range
a₁ : Submodule.map l.ker.subtype f.range = l.ker
a₂ : (l.ker.subtype ∘ₗ f).range = l.ker
a₃ : (π ∘ₗ (l ∘ₗ π).ker.subtype).range = l.ker
⊢ Submodule.map l.ker.subtype f.range = Submodule.map l.ker.subtype ⊤
have a₄ : Submodule.map π (l ∘ₗ π).ker.subtype.range = l.ker
Tactic: rw [Submodule.map_top, Submodule.range_subtype, ← LinearMap.range_comp, ← e,
      LinearMap.range_comp, Submodule.range_subtype, LinearMap.ker_comp,
      Submodule.map_comap_eq_of_surjective H]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
a : Submodule.map l.ker.subtype f.range = l.ker.subtype.range
a₁ : Submodule.map l.ker.subtype f.range = l.ker
a₂ : (l.ker.subtype ∘ₗ f).range = l.ker
a₃ : (π ∘ₗ (l ∘ₗ π).ker.subtype).range = l.ker
a₄ : Submodule.map π (l ∘ₗ π).ker.subtype.range = l.ker
⊢ Submodule.map l.ker.subtype f.range = Submodule.map l.ker.subtype ⊤
have a₅ : Submodule.map π (l ∘ₗ π).ker = l.ker
Tactic: rw [Submodule.map_top, Submodule.range_subtype, ← LinearMap.range_comp, ← e,
      LinearMap.range_comp, Submodule.range_subtype, LinearMap.ker_comp,
      Submodule.map_comap_eq_of_surjective H]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
a : Submodule.map l.ker.subtype f.range = l.ker.subtype.range
a₁ : Submodule.map l.ker.subtype f.range = l.ker
a₂ : (l.ker.subtype ∘ₗ f).range = l.ker
a₃ : (π ∘ₗ (l ∘ₗ π).ker.subtype).range = l.ker
a₄ : Submodule.map π (l ∘ₗ π).ker.subtype.range = l.ker
a₅ : Submodule.map π (l ∘ₗ π).ker = l.ker
⊢ Submodule.map l.ker.subtype f.range = Submodule.map l.ker.subtype ⊤
have a₆ : Submodule.map π (Submodule.comap π l.ker) = l.ker
Tactic: rw [Submodule.map_top, Submodule.range_subtype, ← LinearMap.range_comp, ← e,
      LinearMap.range_comp, Submodule.range_subtype, LinearMap.ker_comp,
      Submodule.map_comap_eq_of_surjective H]