awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid M) (closure S) m
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    Eq (α := R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a :
        R[M])
      ((of R M : (a : M) → R[M]) 1 : R[M])

Tactic:
⟨1, map_one _⟩

Premises used: map_one, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid M) (closure S) m
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    Eq (α := R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a :
        R[M])
      ((of R M : (a : M) → R[M]) 1 : R[M])

Tactic:
exact ⟨1, map_one _⟩
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid M) (closure S) m
m₁ m₂ : M
hx : Membership.mem (γ := Submonoid M) (closure S) m₁
hy : Membership.mem (γ := Submonoid M) (closure S) m₂
P₁ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₁ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₁ :
      R[M])
    ((of R M : (a : M) → R[M]) m₁ : R[M])
P₂ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₂ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₂ :
      R[M])
    ((of R M : (a : M) → R[M]) m₂ : R[M])
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    Eq (α := R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a :
        R[M])
      ((of R M : (a : M) → R[M]) (m₁ * m₂) : R[M])

Tactic:
exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]⟩
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
f g : R[M]
ihf :
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      f
ihg :
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      g
hadd :
  ∀ (P : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
      ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a =
        HAdd.hAdd (α := R[M])
          (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                  fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
                (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
              P :
            R[M])
          g
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      f + g

Tactic:
rcases ihf with ⟨P, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
g : R[M]
ihg :
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      g
P : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hadd :
  ∀ (Q : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
      ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a =
        HAdd.hAdd (α := R[M]) (β := R[M])
          (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                  fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
                (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
              P :
            R[M])
          (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                  fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
                (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
              Q :
            R[M])
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      HAdd.hAdd (α := R[M])
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            P :
          R[M])
        g

Tactic:
rcases ihg with ⟨Q, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
P Q : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      HAdd.hAdd (α := R[M]) (β := R[M])
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            P :
          R[M])
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            Q :
          R[M])

Tactic:
⟨P + Q, map_add _ _ _⟩

Premises used: map_add, HAdd.hAdd, Exists.intro
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
P Q : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      HAdd.hAdd (α := R[M]) (β := R[M])
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            P :
          R[M])
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            Q :
          R[M])

Tactic:
exact ⟨P + Q, map_add _ _ _⟩
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
r : R
f : R[M]
ih :
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      f
hsmul :
  ∀ (P : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
      ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a =
        HSMul.hSMul (β := R[M]) r
          (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                  fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
                (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
              P :
            R[M])
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      r • f

Tactic:
rcases ih with ⟨P, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
r : R
P : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      HSMul.hSMul (β := R[M]) r
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            P :
          R[M])

Tactic:
⟨r • P, map_smul _ _ _⟩

Premises used: Exists.intro, HSMul.hSMul, map_smul
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
r : R
P : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        a =
      HSMul.hSMul (β := R[M]) r
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            P :
          R[M])

Tactic:
exact ⟨r • P, map_smul _ _ _⟩
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommRing R
inst_2 : Monoid.FG M
⊢ FiniteType R R[M]

Tactic:
(AddMonoidAlgebra.finiteType_of_fg R (Additive M)).equiv (toAdditiveAlgEquiv R M).symm

Premises used: AlgEquiv.symm, Additive, AddMonoidAlgebra.finiteType_of_fg, MonoidAlgebra.toAdditiveAlgEquiv, Algebra.FiniteType.equiv
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommRing R
inst_2 : Nontrivial R
h : FiniteType R R[M]
⊢ Monoid.FG M

Tactic:
finiteType_iff_fg.1 h

Premises used: MonoidAlgebra.finiteType_iff_fg, Iff.mp
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
G : Type u_3
inst : Group G
inst_1 : CommRing R
inst_2 : Nontrivial R
⊢ FiniteType R R[G] ↔ Group.FG G

Tactic:
simpa [Group.fg_iff_monoid_fg] using finiteType_iff_fg

Premises used: MonoidAlgebra.finiteType_iff_fg, Group.fg_iff_monoid_fg
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
⊢ OrzechProperty R

Tactic:
⟨fun {M} _ _ _ {N} f hf ↦ ?_⟩

Premises used: OrzechProperty.mk
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
refine :
  ∀ {M : Type u_1} (x : AddCommMonoid M) (x_1 : Module R M),
    Module.Finite R M →
      ∀ {N : Submodule R M} (f : ↥N →ₗ[R] M) (hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)),
        Function.Injective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
⊢ OrzechProperty R

Tactic:
refine ⟨fun {M} _ _ _ {N} f hf ↦ ?_⟩
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x : AddCommMonoid M
x_1 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
⊢ Function.Injective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)

Tactic:
LinearMap.ker_eq_bot.1 <| LinearMap.ker_eq_bot'.2 fun n hn ↦ ?_

Premises used: Iff.mpr, LinearMap.ker_eq_bot, LinearMap.ker_eq_bot', Iff.mp
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x : AddCommMonoid M
x_1 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
refine : ∀ (n : ↥N) (hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)), n = 0
⊢ Function.Injective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)

Tactic:
refine LinearMap.ker_eq_bot.1 <| LinearMap.ker_eq_bot'.2 fun n hn ↦ ?_

Premises used: Iff.mpr, LinearMap.ker_eq_bot, LinearMap.ker_eq_bot', Iff.mp
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x : AddCommMonoid M
x_1 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
obtain : ∀ (k : ℕ) (mj : Fin k → M) (hmj : Eq (α := Submodule R M) (span R (Set.range mj)) ⊤), n = 0
⊢ n = 0

Tactic:
obtain ⟨k, mj, hmj⟩ := exists_fin (R := R) (M := M)

Premises used: Module.Finite.exists_fin
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x : AddCommMonoid M
x_1 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj : Eq (α := Submodule R M) (span R (Set.range mj)) ⊤
⊢ Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)

Tactic:
rw [← surjective_piEquiv_apply_iff] at hmj

Premises used: Module.surjective_piEquiv_apply_iff
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x : AddCommMonoid M
x_1 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
obtain :
  ∀ (b : Fin k → R)
    (hb :
      Eq (α := M)
        ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
              (a : Fin k → R) → M)
            b :
          M)
        ((i : (a : ↥N) → M) n : M)),
    n = 0
⊢ n = 0

Tactic:
obtain ⟨b, hb⟩ := hmj (i n)

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x : AddCommMonoid M
x_1 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
b : Fin k → R
hb :
  Eq (α := M)
    ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
          (a : Fin k → R) → M)
        b :
      M)
    ((i : (a : ↥N) → M) n : M)
choose : ∀ (nj : (j : Fin k) → ↥N) (hnj : ∀ (j : Fin k), (f : (a : ↥N) → M) (nj j) = mj j), n = 0
⊢ n = 0

Tactic:
choose nj hnj using fun j ↦ hf (mj j)
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x : AddCommMonoid M
x_1 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
b : Fin k → R
hb :
  Eq (α := M)
    ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
          (a : Fin k → R) → M)
        b :
      M)
    ((i : (a : ↥N) → M) n : M)
nj : (j : Fin k) → ↥N
hnj : ∀ (j : Fin k), (f : (a : ↥N) → M) (nj j) = mj j
choose :
  ∀ (c : (j : Fin k) → Fin k → R)
    (hc :
      ∀ (j : Fin k),
        Eq (α := M)
          ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
                (a : Fin k → R) → M)
              (c j) :
            M)
          ((i : (a : ↥N) → M) (nj j) : M)),
    n = 0
⊢ n = 0

Tactic:
choose c hc using fun j ↦ hmj (i (nj j))

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x : AddCommMonoid M
x_1 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
b : Fin k → R
hb :
  Eq (α := M)
    ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
          (a : Fin k → R) → M)
        b :
      M)
    ((i : (a : ↥N) → M) n : M)
nj : (j : Fin k) → ↥N
hnj : ∀ (j : Fin k), (f : (a : ↥N) → M) (nj j) = mj j
c : (j : Fin k) → Fin k → R
hc :
  ∀ (j : Fin k),
    Eq (α := M)
      ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
            (a : Fin k → R) → M)
          (c j) :
        M)
      ((i : (a : ↥N) → M) (nj j) : M)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
⊢ IsNoetherianRing.{u_1} ↥A

Tactic:
haveI : IsNoetherianRing A := is_noetherian_subring_closure _
    (.union (Set.finite_range _) (Set.finite_range _))
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
inst : CommRing R
M : Type u_1
x : AddCommMonoid M
x_1 : Module R M
h : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
this_1 : AddCommGroup M := addCommMonoidToAddCommGroup R
this_2 : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective (α := ↥N) (β := M) (⇑i : (a : ↥N) → M) := ⋯
n : ↥N
hn : Eq (α := M) ((f : (a : ↥N) → M) n : M) (0 : M)
k : ℕ
mj : Fin k → M
hmj :
  Surjective (α := Fin k → R) (β := M)
    (⇑((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
      (a : Fin k → R) → M)
b : Fin k → R
hb :
  Eq (α := M)
    ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
          (a : Fin k → R) → M)
        b :
      M)
    ((i : (a : ↥N) → M) n : M)
nj : (j : Fin k) → ↥N
hnj : ∀ (j : Fin k), (f : (a : ↥N) → M) (nj j) = mj j
c : (j : Fin k) → Fin k → R
hc :
  ∀ (j : Fin k),
    Eq (α := M)
      ((((Module.piEquiv (Fin k) R M : (a : Fin k → M) → (Fin k → R) →ₗ[R] M) mj : (Fin k → R) →ₗ[R] M) :
            (a : Fin k → R) → M)
          (c j) :
        M)
      ((i : (a : ↥N) → M) (nj j) : M)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this : IsNoetherianRing.{u_1} ↥A
⊢ Module.Finite.{u_1, u_1} ↥A ↥M'

Tactic:
haveI : Module.Finite A M' := span_of_finite A (Set.finite_range _)