awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Equiv.Opposite
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module S M
σ : RingHom.{u_1, u_2} Rᵐᵒᵖ S
f g : LinearMap.{u_1, u_2, u_1, u_3} (R := Rᵐᵒᵖ) (S := S) σ R M
h : Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) 1 : M) ((g : (a : R) → M) 1 : M)
x : R
rw : Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) (1 * x) : M) ((g : (a : R) → M) (1 * x) : M)
rw₁ :
  Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) (HSMul.hSMul (β := R) (MulOpposite.op x) 1) : M)
    ((g : (a : R) → M) (HSMul.hSMul (β := R) (MulOpposite.op x) 1) : M)
rw₂ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M) ((σ : (a : Rᵐᵒᵖ) → S) (MulOpposite.op x) : S)
      ((f : (a : R) → M) 1 : M) =
    (g : (a : R) → M) (HSMul.hSMul (β := R) (MulOpposite.op x) 1)
rw₃ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M) ((σ : (a : Rᵐᵒᵖ) → S) (MulOpposite.op x) : S)
      ((g : (a : R) → M) 1 : M) =
    (g : (a : R) → M) (HSMul.hSMul (β := R) (MulOpposite.op x) 1)
rw₄ rw₅ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M) ((σ : (a : Rᵐᵒᵖ) → S) (MulOpposite.op x) : S)
      ((g : (a : R) → M) 1 : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M) ((σ : (a : Rᵐᵒᵖ) → S) (MulOpposite.op x) : S)
      ((g : (a : R) → M) 1 : M)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) x : M) ((g : (a : R) → M) x : M)

Tactic:
rw [← one_mul x, ← op_smul_eq_mul, f.map_smulₛₗ, h, g.map_smulₛₗ]

Premises used: op_smul_eq_mul, LinearMap.map_smulₛₗ, one_mul
-- Module: Mathlib.Algebra.Module.Equiv.Opposite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{v + 1} (α := (a : M) → Mᵐᵒᵖ) (⇑(opLinearEquiv R) : (a : M) → Mᵐᵒᵖ) op

Tactic:
rfl

Premises used: rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Module.Equiv.Opposite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{v + 1} (α := (a : Mᵐᵒᵖ) → M) (⇑(LinearEquiv.symm (opLinearEquiv R)) : (a : Mᵐᵒᵖ) → M) unop

Tactic:
rfl

Premises used: MulOpposite, MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Opposite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{v + 1} (α := (a : M) → Mᵐᵒᵖ) (⇑(↑(opLinearEquiv R) : M →ₗ[R] Mᵐᵒᵖ) : (a : M) → Mᵐᵒᵖ) op

Tactic:
rfl

Premises used: rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Module.Equiv.Opposite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{v + 1} (α := (a : Mᵐᵒᵖ) → M) (⇑(↑(LinearEquiv.symm (opLinearEquiv R)) : Mᵐᵒᵖ →ₗ[R] M) : (a : Mᵐᵒᵖ) → M) unop

Tactic:
rfl

Premises used: MulOpposite, MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Opposite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{v + 1} (α := M ≃+ Mᵐᵒᵖ) (LinearEquiv.toAddEquiv (opLinearEquiv R)) opAddEquiv

Tactic:
rfl

Premises used: MulOpposite.opEquiv, MulOpposite, MulOpposite.opAddEquiv, MulOpposite.unop, rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Module.Equiv.Opposite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := M ≃+ Mᵐᵒᵖ) (↑(opLinearEquiv R) : M ≃+ Mᵐᵒᵖ) opAddEquiv

Tactic:
rfl

Premises used: MulOpposite.opEquiv, MulOpposite, MulOpposite.opAddEquiv, MulOpposite.unop, rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Module.Equiv.Opposite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{v + 1} (α := Mᵐᵒᵖ ≃+ M) (LinearEquiv.toAddEquiv (LinearEquiv.symm (opLinearEquiv R))) (AddEquiv.symm opAddEquiv)

Tactic:
rfl

Premises used: MulOpposite, MulOpposite.unop, Equiv.symm, rfl, AddEquiv.symm, MulOpposite.op
-- Module: Mathlib.Algebra.Module.Equiv.Opposite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := Mᵐᵒᵖ ≃+ M) (↑(LinearEquiv.symm (opLinearEquiv R)) : Mᵐᵒᵖ ≃+ M) (AddEquiv.symm opAddEquiv)

Tactic:
rfl

Premises used: MulOpposite, AddEquivClass.toAddEquiv, MulOpposite.unop, Equiv.symm, EquivLike.toEquiv, rfl, AddEquiv.symm, MulOpposite.op
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Module.FinitePresentation R M
obtain :
  ∀ (s : Finset M) (hs₁ : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤),
    Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) →
      Module.Finite R M
⊢ Module.Finite R M

Tactic:
obtain ⟨s, hs₁, _⟩ := h
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset M
hs₁ : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
right :
  Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
⊢ Module.Finite R M

Tactic:
⟨s, hs₁⟩

Premises used: Module.Finite.of_fg_top, Exists.intro
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset M
hs₁ : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
right :
  Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
⊢ Module.Finite R M

Tactic:
exact ⟨s, hs₁⟩
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u
M : Type u_1
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
fp : FinitePresentation R M
ι : Finset M
hι₁ : Eq (α := Submodule R M) (Submodule.span R (↑ι : Set M)) ⊤
hι₂ :
  Submodule.FG (M := Finsupp.{u_1, u} (↥ι) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ ι))))
⊢ ∃ (n : ℕ) (K : Submodule R (Fin n → R)) (x : M ≃ₗ[R] (Fin n → R) ⧸ K), K.FG

Tactic:
⟨_, LinearMap.ker (linearCombination R Subtype.val ∘ₗ
    (lcongr ι.equivFin (.refl ..) ≪≫ₗ linearEquivFunOnFinite R R _).symm.toLinearMap),
    (LinearMap.quotKerEquivOfSurjective _ <| LinearMap.range_eq_top.mp ?_).symm, ?_⟩

Premises used: LinearEquiv.symm, Finset.equivFin, LinearMap.ker, Finsupp.linearEquivFunOnFinite, Finsupp.lcongr, LinearMap.range_eq_top, LinearMap.comp, LinearEquiv.toLinearMap, LinearMap.quotKerEquivOfSurjective, Exists.intro, Iff.mp, LinearEquiv.refl, Finsupp.linearCombination, Subtype.val, LinearEquiv.trans
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u
M : Type u_1
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
fp : FinitePresentation R M
ι : Finset M
hι₁ : Eq (α := Submodule R M) (Submodule.span R (↑ι : Set M)) ⊤
hι₂ :
  Submodule.FG (M := Finsupp.{u_1, u} (↥ι) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ ι))))
refine_1 :
  Eq (α := Submodule R M)
    (LinearMap.range
      (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ ι)) ∘ₗ
        (↑(LinearEquiv.symm (lcongr ι.equivFin (LinearEquiv.refl R R) ≪≫ₗ linearEquivFunOnFinite R R (Fin ι.card))) :
          (Fin ι.card → R) →ₗ[R] ↥ι →₀ R)))
    ⊤
refine_2 :
  (LinearMap.ker
      (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ ι)) ∘ₗ
        (↑(LinearEquiv.symm (lcongr ι.equivFin (LinearEquiv.refl R R) ≪≫ₗ linearEquivFunOnFinite R R (Fin ι.card))) :
          (Fin ι.card → R) →ₗ[R] ↥ι →₀ R))).FG
⊢ ∃ (n : ℕ) (K : Submodule R (Fin n → R)) (x : M ≃ₗ[R] (Fin n → R) ⧸ K), K.FG

Tactic:
refine ⟨_, LinearMap.ker (linearCombination R Subtype.val ∘ₗ
    (lcongr ι.equivFin (.refl ..) ≪≫ₗ linearEquivFunOnFinite R R _).symm.toLinearMap),
    (LinearMap.quotKerEquivOfSurjective _ <| LinearMap.range_eq_top.mp ?_).symm, ?_⟩
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u
M : Type u_1
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
fp : FinitePresentation R M
ι : Finset M
hι₁ : Eq (α := Submodule R M) (Submodule.span R (↑ι : Set M)) ⊤
hι₂ :
  Submodule.FG (M := Finsupp.{u_1, u} (↥ι) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ ι))))
⊢ Eq (α := Submodule R M)
    (LinearMap.range
      (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ ι)) ∘ₗ
        (↑(LinearEquiv.symm (lcongr ι.equivFin (LinearEquiv.refl R R) ≪≫ₗ linearEquivFunOnFinite R R (Fin ι.card))) :
          (Fin ι.card → R) →ₗ[R] ↥ι →₀ R)))
    ⊤

Tactic:
simpa [range_linearCombination] using hι₁

Premises used: Finsupp.range_linearCombination
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u
M : Type u_1
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
fp : FinitePresentation R M
ι : Finset M
hι₁ : Eq (α := Submodule R M) (Submodule.span R (↑ι : Set M)) ⊤
hι₂ :
  Submodule.FG (M := Finsupp.{u_1, u} (↥ι) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ ι))))
⊢ (LinearMap.ker
      (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ ι)) ∘ₗ
        (↑(LinearEquiv.symm (lcongr ι.equivFin (LinearEquiv.refl R R) ≪≫ₗ linearEquivFunOnFinite R R (Fin ι.card))) :
          (Fin ι.card → R) →ₗ[R] ↥ι →₀ R))).FG

Tactic:
simpa [LinearMap.ker_comp, Submodule.comap_equiv_eq_map_symm] using hι₂.map _

Premises used: Submodule.comap_equiv_eq_map_symm, Submodule.FG.map, LinearMap.ker_comp
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u
M : Type u_1
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FinitePresentation R M
inst_4 : Small.{v, u} R
⊢ ∃ (L : Type v) (x : AddCommGroup L) (x_1 : Module R L) (K : Submodule R L) (x_2 :
    LinearEquiv.{u, u, u_1, v} (RingHom.id R) M (L ⧸ K)), Free R L ∧ Module.Finite R L ∧ K.FG

Tactic:
have ⟨_n, _K, e, fg⟩ := Module.FinitePresentation.exists_fin R M
  let es := Shrink.linearEquiv
  ⟨_, inferInstance, inferInstance, _, e ≪≫ₗ Submodule.Quotient.equiv _ _ (es ..).symm rfl,
    .of_equiv (es ..).symm, .equiv (es ..).symm, fg.map (es ..).symm.toLinearMap⟩

Premises used: LinearEquiv.symm, Submodule.FG.map, Exists, inferInstance, Module.FinitePresentation.exists_fin, Submodule.Quotient.equiv, _private.0.Module.FinitePresentation.equiv_quotient.match_1, Submodule.FG, Module.Free, And, LinearEquiv.toLinearMap, And.intro, Module.Free.of_equiv, Exists.intro, Shrink.linearEquiv, Module.Finite, Shrink, Submodule.map, Module.Finite.equiv, LinearEquiv.trans, rfl
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
h : Module.Finite R M
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⟩ := h
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
⊢ FinitePresentation R M

Tactic:
⟨s, hs, IsNoetherian.noetherian _⟩

Premises used: IsNoetherian.noetherian, Module.FinitePresentation.mk, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
⊢ FinitePresentation R M

Tactic:
exact ⟨s, hs, IsNoetherian.noetherian _⟩
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
⊢ FinitePresentation R M ↔ Module.Finite R M

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ finitePresentation_of_finite R M⟩

Premises used: inferInstance, Iff.intro, Module.finitePresentation_of_finite
-- 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 : Free R M
inst_6 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
i : Free.ChooseBasisIndex R M
⊢ Membership.mem.{u_3, u_3} (α := N) (γ := Finset N)
    (Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯)
    ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M) : N)

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 : Free R M
inst_6 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M →
  ↥(Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯) :=
  fun (i : Free.ChooseBasisIndex R M) ↦
    Subtype.mk (p := fun (x : N) ↦
      Membership.mem (γ := Finset N)
        (Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)
        x)
      ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) ⋯
x_1 :
  ↥(Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯)
x : N
hx :
  Membership.mem (γ := Finset N)
    (Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯)
    x
⊢ ∃ (a : Free.ChooseBasisIndex R M), (l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) a : M) = x

Tactic:
simpa using hx
-- 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 : Free R M
inst_6 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M →
  ↥(Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯) :=
  fun (i : Free.ChooseBasisIndex R M) ↦
    Subtype.mk (p := fun (x : N) ↦
      Membership.mem (γ := Finset N)
        (Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)
        x)
      ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) ⋯
x_1 :
  ↥(Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯)
x : N
hx :
  Membership.mem (γ := Finset N)
    (Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯)
    x
obtain :
  ∀ (y : Free.ChooseBasisIndex R M)
    (hx :
      Membership.mem.{u_3, u_3} (α := N) (γ := Finset N)
        (Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)
        ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) y : M) : N)),
    ∃ (a : Free.ChooseBasisIndex R M),
      π a =
        Subtype.mk (p := fun (x : N) ↦
          Membership.mem (γ := Finset N)
            (Set.Finite.toFinset (s :=
              Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
                (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
              ⋯)
            x)
          ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) y : M)) hx
⊢ ∃ (a : Free.ChooseBasisIndex R M),
    π a =
      Subtype.mk (p := fun (x : N) ↦
        Membership.mem (γ := Finset N)
          (Set.Finite.toFinset (s :=
            Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
              (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
            ⋯)
          x)
        x hx

Tactic:
obtain ⟨y, rfl⟩ : ∃ a, l (b a) = x := by simpa using hx

Premises used: rfl
-- 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 : Free R M
inst_6 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M →
  ↥(Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯) :=
  fun (i : Free.ChooseBasisIndex R M) ↦
    Subtype.mk (p := fun (x : N) ↦
      Membership.mem (γ := Finset N)
        (Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)
        x)
      ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) ⋯
x :
  ↥(Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯)
y : Free.ChooseBasisIndex R M
hx :
  Membership.mem.{u_3, u_3} (α := N) (γ := Finset N)
    (Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯)
    ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) y : M) : N)
⊢ ∃ (a : Free.ChooseBasisIndex R M),
    π a =
      Subtype.mk (p := fun (x : N) ↦
        Membership.mem (γ := Finset N)
          (Set.Finite.toFinset (s :=
            Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
              (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
            ⋯)
          x)
        ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) y : M)) hx

Tactic:
⟨y, rfl⟩

Premises used: Exists.intro, rfl
-- 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 : Free R M
inst_6 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M →
  ↥(Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯) :=
  fun (i : Free.ChooseBasisIndex R M) ↦
    Subtype.mk (p := fun (x : N) ↦
      Membership.mem (γ := Finset N)
        (Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)
        x)
      ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) ⋯
x :
  ↥(Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯)
y : Free.ChooseBasisIndex R M
hx :
  Membership.mem.{u_3, u_3} (α := N) (γ := Finset N)
    (Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯)
    ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) y : M) : N)
⊢ ∃ (a : Free.ChooseBasisIndex R M),
    π a =
      Subtype.mk (p := fun (x : N) ↦
        Membership.mem (γ := Finset N)
          (Set.Finite.toFinset (s :=
            Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
              (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
            ⋯)
          x)
        ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) y : M)) hx

Tactic:
exact ⟨y, rfl⟩
-- 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 : Free R M
inst_6 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M →
  ↥(Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯) :=
  fun (i : Free.ChooseBasisIndex R M) ↦
    Subtype.mk (p := fun (x : N) ↦
      Membership.mem (γ := Finset N)
        (Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)
        x)
      ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) ⋯
this : Function.Surjective π
choose :
  ∀
    (σ :
      (b :
          ↥(Set.Finite.toFinset (s :=
              Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
                (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
              ⋯)) →
        Free.ChooseBasisIndex R M)
    (hσ :
      ∀
        (b_1 :
          ↥(Set.Finite.toFinset (s :=
              Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
                (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
              ⋯)),
        π (σ b_1) = b_1),
    FinitePresentation R N
⊢ FinitePresentation R N

Tactic:
choose σ hσ using this