awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M_1 : Type ?u.229890
N : Type ?u.230178
inst : Ring R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
ι_1 : Sort ?u.230453
inst_5 : Finite ι_1
ι : Type u_1
M : ι → Type u_2
inst_6 : (i : ι) → AddCommGroup (M i)
inst_7 : (i : ι) → Module.{u_3, u_2} R (M i)
inst_8 : ∀ (i : ι), FinitePresentation.{u_3, u_2} R (M i)
inst_9 : Finite ι
refine_1 :
  ∀ {N : Type u_2} {N' : Type (max u_2 u_1)} [inst_10 : AddCommGroup N] [inst_11 : AddCommGroup N']
    [inst_12 : Module R N] [inst_13 : Module R N'] (a : N ≃ₗ[R] N'),
    (fun (N : Type u_2) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N inst_10 inst_12 →
      (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N' inst_11 inst_13
refine_2 :
  ∀ {N N' : Type (max u_2 u_1)} [inst_10 : AddCommGroup N] [inst_11 : AddCommGroup N'] [inst_12 : Module R N]
    [inst_13 : Module R N'] (a : N ≃ₗ[R] N'),
    (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N inst_10 inst_12 →
      (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N' inst_11 inst_13
refine_3 : FinitePresentation R PUnit.{u_2 + 1}
refine_4 :
  ∀ {N : Type u_2} {N' : Type (max u_2 u_1)} [inst_10 : AddCommGroup N] [inst_11 : AddCommGroup N']
    [inst_12 : Module R N] [inst_13 : Module R N'],
    (fun (N : Type u_2) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N inst_10 inst_12 →
      (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N' inst_11
          inst_13 →
        (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) (N × N')
          Prod.instAddCommGroup Prod.instModule
⊢ FinitePresentation R ((i : ι) → M i)

Tactic:
refine Module.pi_induction' (motive := fun N _ _ ↦ Module.FinitePresentation R N)
      (motive' := fun N _ _ ↦ Module.FinitePresentation R N) R ?_ ?_ ?_ ?_ M inferInstance

Premises used: inferInstance, Module.FinitePresentation, Module.pi_induction'
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M_1 : Type ?u.229890
N : Type ?u.230178
inst : Ring R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
ι_1 : Sort ?u.230453
inst_5 : Finite ι_1
ι : Type u_1
M : ι → Type u_2
inst_6 : (i : ι) → AddCommGroup (M i)
inst_7 : (i : ι) → Module.{u_3, u_2} R (M i)
inst_8 : ∀ (i : ι), FinitePresentation.{u_3, u_2} R (M i)
inst_9 : Finite ι
N_1 : Type u_2
N' : Type (max u_2 u_1)
inst_10 : AddCommGroup N_1
inst_11 : AddCommGroup N'
inst_12 : Module R N_1
inst_13 : Module R N'
⊢ ∀ (a : N_1 ≃ₗ[R] N'),
    (fun (N : Type u_2) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N_1 inst_10 inst_12 →
      (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N' inst_11 inst_13

Tactic:
fun e (hN : Module.FinitePresentation _ _) ↦ .of_equiv e

Premises used: Module.FinitePresentation.of_equiv
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M_1 : Type ?u.229890
N : Type ?u.230178
inst : Ring R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
ι_1 : Sort ?u.230453
inst_5 : Finite ι_1
ι : Type u_1
M : ι → Type u_2
inst_6 : (i : ι) → AddCommGroup (M i)
inst_7 : (i : ι) → Module.{u_3, u_2} R (M i)
inst_8 : ∀ (i : ι), FinitePresentation.{u_3, u_2} R (M i)
inst_9 : Finite ι
⊢ ∀ {N : Type u_2} {N' : Type (max u_2 u_1)} [inst_10 : AddCommGroup N] [inst_11 : AddCommGroup N']
    [inst_12 : Module R N] [inst_13 : Module R N'] (a : N ≃ₗ[R] N'),
    (fun (N : Type u_2) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N inst_10 inst_12 →
      (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N' inst_11 inst_13

Tactic:
exact fun e (hN : Module.FinitePresentation _ _) ↦ .of_equiv e
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M_1 : Type ?u.229890
N : Type ?u.230178
inst : Ring R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
ι_1 : Sort ?u.230453
inst_5 : Finite ι_1
ι : Type u_1
M : ι → Type u_2
inst_6 : (i : ι) → AddCommGroup (M i)
inst_7 : (i : ι) → Module.{u_3, u_2} R (M i)
inst_8 : ∀ (i : ι), FinitePresentation.{u_3, u_2} R (M i)
inst_9 : Finite ι
N_1 N' : Type (max u_2 u_1)
inst_10 : AddCommGroup N_1
inst_11 : AddCommGroup N'
inst_12 : Module R N_1
inst_13 : Module R N'
⊢ ∀ (a : N_1 ≃ₗ[R] N'),
    (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N_1 inst_10
        inst_12 →
      (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N' inst_11 inst_13

Tactic:
fun e (hN : Module.FinitePresentation _ _) ↦ .of_equiv e

Premises used: Module.FinitePresentation.of_equiv
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M_1 : Type ?u.229890
N : Type ?u.230178
inst : Ring R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
ι_1 : Sort ?u.230453
inst_5 : Finite ι_1
ι : Type u_1
M : ι → Type u_2
inst_6 : (i : ι) → AddCommGroup (M i)
inst_7 : (i : ι) → Module.{u_3, u_2} R (M i)
inst_8 : ∀ (i : ι), FinitePresentation.{u_3, u_2} R (M i)
inst_9 : Finite ι
⊢ ∀ {N N' : Type (max u_2 u_1)} [inst_10 : AddCommGroup N] [inst_11 : AddCommGroup N'] [inst_12 : Module R N]
    [inst_13 : Module R N'] (a : N ≃ₗ[R] N'),
    (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N inst_10 inst_12 →
      (fun (N : Type (max u_2 u_1)) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) N' inst_11 inst_13

Tactic:
exact fun e (hN : Module.FinitePresentation _ _) ↦ .of_equiv e
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M_1 : Type ?u.229890
N : Type ?u.230178
inst : Ring R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
ι_1 : Sort ?u.230453
inst_5 : Finite ι_1
ι : Type u_1
M : ι → Type u_2
inst_6 : (i : ι) → AddCommGroup (M i)
inst_7 : (i : ι) → Module.{u_3, u_2} R (M i)
inst_8 : ∀ (i : ι), FinitePresentation.{u_3, u_2} R (M i)
inst_9 : Finite ι
⊢ (fun (N : Type u_2) (x : AddCommGroup N) (x_1 : Module R N) ↦ FinitePresentation R N) PUnit.{u_2 + 1}
    PUnit.addCommGroup PUnit.module

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M_1 : Type ?u.229890
N_1 : Type ?u.230178
inst : Ring R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N_1
inst_4 : Module R N_1
ι_1 : Sort ?u.230453
inst_5 : Finite ι_1
ι : Type u_1
M : ι → Type u_2
inst_6 : (i : ι) → AddCommGroup (M i)
inst_7 : (i : ι) → Module.{u_3, u_2} R (M i)
inst_8 : ∀ (i : ι), FinitePresentation.{u_3, u_2} R (M i)
inst_9 : Finite ι
N : Type u_2
N' : Type (max u_2 u_1)
inst_10 : AddCommGroup N
inst_11 : AddCommGroup N'
inst_12 : Module R N
inst_13 : Module R N'
hN : FinitePresentation R N
hN' : FinitePresentation R N'
⊢ FinitePresentation R (N × N')

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FinitePresentation R S
inst_8 : FinitePresentation S M
obtain : ∀ (n : ℕ) (K : Submodule S (Fin n → S)) (e : M ≃ₗ[S] (Fin n → S) ⧸ K) (hK : K.FG), FinitePresentation R M
⊢ FinitePresentation R M

Tactic:
obtain ⟨n, K, e, hK⟩ := Module.FinitePresentation.exists_fin S M

Premises used: Module.FinitePresentation.exists_fin
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FinitePresentation R S
inst_8 : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (Fin n → S) M :=
  (↑R :
      {S M : Type u_1} →
        {M₂ : Type u_3} →
          [inst : Semiring R] →
            [inst_9 : Semiring S] →
              [inst_10 : AddCommMonoid M] →
                [inst_11 : AddCommMonoid M₂] →
                  [inst_12 : Module R M] →
                    [inst_13 : Module R M₂] →
                      [inst_14 : Module S M] →
                        [inst_15 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ)
⊢ FinitePresentation R M

Tactic:
Module.finitePresentation_of_surjective f (fun m ↦ ?_) ?_

Premises used: Module.finitePresentation_of_surjective
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FinitePresentation R S
inst_8 : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (Fin n → S) M :=
  (↑R :
      {S M : Type u_1} →
        {M₂ : Type u_3} →
          [inst : Semiring R] →
            [inst_9 : Semiring S] →
              [inst_10 : AddCommMonoid M] →
                [inst_11 : AddCommMonoid M₂] →
                  [inst_12 : Module R M] →
                    [inst_13 : Module R M₂] →
                      [inst_14 : Module S M] →
                        [inst_15 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ)
refine_1 : ∀ (m : M), ∃ (a : Fin n → S), (f : (a : Fin n → S) → M) a = m
refine_2 : f.ker.FG
⊢ FinitePresentation R M

Tactic:
refine Module.finitePresentation_of_surjective f (fun m ↦ ?_) ?_

Premises used: Module.finitePresentation_of_surjective
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FinitePresentation R S
inst_8 : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (Fin n → S) M :=
  (↑R :
      {S M : Type u_1} →
        {M₂ : Type u_3} →
          [inst : Semiring R] →
            [inst_9 : Semiring S] →
              [inst_10 : AddCommMonoid M] →
                [inst_11 : AddCommMonoid M₂] →
                  [inst_12 : Module R M] →
                    [inst_13 : Module R M₂] →
                      [inst_14 : Module S M] →
                        [inst_15 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ)
m : M
refine_1 :
  ∀ (a : Fin n → S)
    (ha :
      Eq (α := (Fin n → S) ⧸ K) ((K.mkQ : (a : Fin n → S) → (Fin n → S) ⧸ K) a : (Fin n → S) ⧸ K)
        ((e : (a : M) → (Fin n → S) ⧸ K) m : (Fin n → S) ⧸ K)),
    ∃ (a : Fin n → S), (f : (a : Fin n → S) → M) a = m
⊢ ∃ (a : Fin n → S), (f : (a : Fin n → S) → M) a = m

Tactic:
obtain ⟨a, ha⟩ := K.mkQ_surjective (e m)

Premises used: Submodule.mkQ_surjective, DFunLike.coe
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FinitePresentation R S
inst_8 : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (Fin n → S) M :=
  (↑R :
      {S M : Type u_1} →
        {M₂ : Type u_3} →
          [inst : Semiring R] →
            [inst_9 : Semiring S] →
              [inst_10 : AddCommMonoid M] →
                [inst_11 : AddCommMonoid M₂] →
                  [inst_12 : Module R M] →
                    [inst_13 : Module R M₂] →
                      [inst_14 : Module S M] →
                        [inst_15 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ)
m : M
a : Fin n → S
ha :
  Eq (α := (Fin n → S) ⧸ K) ((K.mkQ : (a : Fin n → S) → (Fin n → S) ⧸ K) a : (Fin n → S) ⧸ K)
    ((e : (a : M) → (Fin n → S) ⧸ K) m : (Fin n → S) ⧸ K)
⊢ (f : (a : Fin n → S) → M) a = m

Tactic:
simp [f, ha]
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FinitePresentation R S
inst_8 : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (Fin n → S) M :=
  (↑R :
      {S M : Type u_1} →
        {M₂ : Type u_3} →
          [inst : Semiring R] →
            [inst_9 : Semiring S] →
              [inst_10 : AddCommMonoid M] →
                [inst_11 : AddCommMonoid M₂] →
                  [inst_12 : Module R M] →
                    [inst_13 : Module R M₂] →
                      [inst_14 : Module S M] →
                        [inst_15 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ)
m : M
a : Fin n → S
ha :
  Eq (α := (Fin n → S) ⧸ K) ((K.mkQ : (a : Fin n → S) → (Fin n → S) ⧸ K) a : (Fin n → S) ⧸ K)
    ((e : (a : M) → (Fin n → S) ⧸ K) m : (Fin n → S) ⧸ K)
⊢ ∃ (a : Fin n → S), (f : (a : Fin n → S) → M) a = m

Tactic:
exact ⟨a, by simp [f, ha]⟩
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FinitePresentation R S
inst_8 : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (Fin n → S) M :=
  (↑R :
      {S M : Type u_1} →
        {M₂ : Type u_3} →
          [inst : Semiring R] →
            [inst_9 : Semiring S] →
              [inst_10 : AddCommMonoid M] →
                [inst_11 : AddCommMonoid M₂] →
                  [inst_12 : Module R M] →
                    [inst_13 : Module R M₂] →
                      [inst_14 : Module S M] →
                        [inst_15 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ)
⊢ ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ).ker.FG

Tactic:
simpa
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FinitePresentation R S
inst_8 : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (Fin n → S) M :=
  (↑R :
      {S M : Type u_1} →
        {M₂ : Type u_3} →
          [inst : Semiring R] →
            [inst_9 : Semiring S] →
              [inst_10 : AddCommMonoid M] →
                [inst_11 : AddCommMonoid M₂] →
                  [inst_12 : Module R M] →
                    [inst_13 : Module R M₂] →
                      [inst_14 : Module S M] →
                        [inst_15 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ)
⊢ Module.Finite S ↥(Submodule.restrictScalars R ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ).ker)

Tactic:
have : Module.Finite S
        (Submodule.restrictScalars R (LinearMap.ker (e.symm.toLinearMap ∘ₗ K.mkQ))) :=
      .of_fg <| show (LinearMap.ker (e.symm.toLinearMap ∘ₗ K.mkQ)).FG by simpa
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FinitePresentation R S
inst_8 : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (Fin n → S) M :=
  (↑R :
      {S M : Type u_1} →
        {M₂ : Type u_3} →
          [inst : Semiring R] →
            [inst_9 : Semiring S] →
              [inst_10 : AddCommMonoid M] →
                [inst_11 : AddCommMonoid M₂] →
                  [inst_12 : Module R M] →
                    [inst_13 : Module R M₂] →
                      [inst_14 : Module S M] →
                        [inst_15 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ)
this : Module.Finite S ↥(Submodule.restrictScalars R ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ).ker)
refine_2 : Module.Finite.{u_2, u_1} R ↥(Submodule.restrictScalars R ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ).ker)
⊢ f.ker.FG

Tactic:
simp only [f, LinearMap.ker_restrictScalars, ← Module.Finite.iff_fg]

Premises used: LinearMap.ker_restrictScalars, Module.Finite.iff_fg
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FinitePresentation R S
inst_8 : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (Fin n → S) M :=
  (↑R :
      {S M : Type u_1} →
        {M₂ : Type u_3} →
          [inst : Semiring R] →
            [inst_9 : Semiring S] →
              [inst_10 : AddCommMonoid M] →
                [inst_11 : AddCommMonoid M₂] →
                  [inst_12 : Module R M] →
                    [inst_13 : Module R M₂] →
                      [inst_14 : Module S M] →
                        [inst_15 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ)
this : Module.Finite S ↥(Submodule.restrictScalars R ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ).ker)
⊢ Module.Finite.{u_2, u_1} R ↥(Submodule.restrictScalars R ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ).ker)

Tactic:
Module.Finite.trans S _

Premises used: Module.Finite.trans
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FinitePresentation R S
inst_8 : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : LinearMap.{u_2, u_2, u_1, u_3} (RingHom.id R) (Fin n → S) M :=
  (↑R :
      {S M : Type u_1} →
        {M₂ : Type u_3} →
          [inst : Semiring R] →
            [inst_9 : Semiring S] →
              [inst_10 : AddCommMonoid M] →
                [inst_11 : AddCommMonoid M₂] →
                  [inst_12 : Module R M] →
                    [inst_13 : Module R M₂] →
                      [inst_14 : Module S M] →
                        [inst_15 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ)
this : Module.Finite S ↥(Submodule.restrictScalars R ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ).ker)
⊢ Module.Finite.{u_2, u_1} R ↥(Submodule.restrictScalars R ((↑e.symm : (Fin n → S) ⧸ K →ₗ[S] M) ∘ₗ K.mkQ).ker)

Tactic:
exact Module.Finite.trans S _

Premises used: Module.Finite.trans
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_3
N : Type ?u.260520
N' : Type ?u.260786
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst_7 : IsLocalizedModule S f
A : Type u_1
inst_8 : CommRing A
inst_9 : Algebra R A
inst_10 : Module.FinitePresentation R M
obtain :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)),
    Module.FinitePresentation A (A ⊗[R] M)
⊢ Module.FinitePresentation A (A ⊗[R] M)

Tactic:
obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M

Premises used: Module.Finite.exists_fin'
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_3
N : Type ?u.260520
N' : Type ?u.260786
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
f_1 : N →ₗ[R] N'
inst_7 : IsLocalizedModule S f_1
A : Type u_1
inst_8 : CommRing A
inst_9 : Algebra R A
inst_10 : Module.FinitePresentation R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
⊢ Module.FinitePresentation A (A ⊗[R] (Fin n → R))

Tactic:
have inst := Module.finitePresentation_of_projective A (A ⊗[R] (Fin n → R))
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_3
N : Type ?u.260520
N' : Type ?u.260786
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : AddCommGroup N'
inst_7 : Module R N'
S : Submonoid R
f_1 : N →ₗ[R] N'
inst_8 : IsLocalizedModule S f_1
A : Type u_1
inst_9 : CommRing A
inst_10 : Algebra R A
inst_11 : Module.FinitePresentation R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
inst : Module.FinitePresentation A (A ⊗[R] (Fin n → R))
apply : Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.ker (LinearMap.baseChange A f))
⊢ Module.FinitePresentation A (A ⊗[R] M)

Tactic:
apply Module.finitePresentation_of_surjective (f.baseChange A)
    (LinearMap.lTensor_surjective A hf)

Premises used: LinearMap.baseChange, LinearMap.lTensor_surjective, Module.finitePresentation_of_surjective
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_3
N : Type ?u.260520
N' : Type ?u.260786
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : AddCommGroup N'
inst_7 : Module R N'
S : Submonoid R
f_1 : N →ₗ[R] N'
inst_8 : IsLocalizedModule S f_1
A : Type u_1
inst_9 : CommRing A
inst_10 : Algebra R A
inst_11 : Module.FinitePresentation R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
inst : Module.FinitePresentation A (A ⊗[R] (Fin n → R))
⊢ Function.Exact (M := A ⊗[R] ↥f.ker) (N := A ⊗[R] (Fin n → R)) (P := A ⊗[R] M)
    (⇑(LinearMap.baseChange A f.ker.subtype) : (a : A ⊗[R] ↥f.ker) → A ⊗[R] (Fin n → R))
    (⇑(LinearMap.baseChange A f) : (a : A ⊗[R] (Fin n → R)) → A ⊗[R] M)

Tactic:
have : Function.Exact ((LinearMap.ker f).subtype.baseChange A) (f.baseChange A) :=
    lTensor_exact A f.exact_subtype_ker_map hf