awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
inst_4 : Module.Finite R M
hN :
  Eq (α := Submodule R (k ⊗[R] M))
    (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) ⊤
this_1 : Module.{u_1, u_2} k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this : IsScalarTower.{u_1, u_1, u_2} R k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) := ⋯
f : k ⊗[R] M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤ :=
  AlgebraTensorModule.lift
    ((↑R :
        {S M : Type u_1} →
          {M₂ : Type u_2} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := k)
      ((LinearEquiv.symm
            (LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)) :
          (a : M →ₗ[R] M ⧸ 𝔪 • ⊤) → k →ₗ[k] M →ₗ[R] M ⧸ 𝔪 • ⊤)
        (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ))
h :
  ∀ (x : M),
    Eq (α := M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
      ((f ∘ₗ (TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1 : (a : M) → M ⧸ 𝔪 • ⊤) x :
        M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
      (((HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ : (a : M) → M ⧸ 𝔪 • ⊤) x :
        M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
⊢ f ∘ₗ (TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1 =
    (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ

Tactic:
ext
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
inst_4 : Module.Finite R M
hN :
  Eq (α := Submodule R (k ⊗[R] M))
    (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) ⊤
this_1 : Module.{u_1, u_2} k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this : IsScalarTower.{u_1, u_1, u_2} R k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) := ⋯
f : k ⊗[R] M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤ :=
  AlgebraTensorModule.lift
    ((↑R :
        {S M : Type u_1} →
          {M₂ : Type u_2} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := k)
      ((LinearEquiv.symm
            (LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)) :
          (a : M →ₗ[R] M ⧸ 𝔪 • ⊤) → k →ₗ[k] M →ₗ[R] M ⧸ 𝔪 • ⊤)
        (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ))
x : M
⊢ Eq (α := M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
    ((f ∘ₗ (TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1 : (a : M) → M ⧸ 𝔪 • ⊤) x :
      M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
    (((HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ : (a : M) → M ⧸ 𝔪 • ⊤) x :
      M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)

Tactic:
simp [f]
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
inst_4 : Module.Finite R M
hN :
  Eq (α := Submodule R (k ⊗[R] M))
    (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) ⊤
this_1 : Module.{u_1, u_2} k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this : IsScalarTower.{u_1, u_1, u_2} R k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) := ⋯
f : k ⊗[R] M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤ :=
  AlgebraTensorModule.lift
    ((↑R :
        {S M : Type u_1} →
          {M₂ : Type u_2} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := k)
      ((LinearEquiv.symm
            (LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)) :
          (a : M →ₗ[R] M ⧸ 𝔪 • ⊤) → k →ₗ[k] M →ₗ[R] M ⧸ 𝔪 • ⊤)
        (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ))
⊢ f ∘ₗ (TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1 =
    (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ

Tactic:
have : f.comp (TensorProduct.mk R k M 1) = Submodule.mkQ (𝔪 • ⊤) := by ext; simp [f]
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
inst_4 : Module.Finite R M
hN :
  Eq (α := Submodule R (k ⊗[R] M))
    (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) ⊤
this_1 : Module.{u_1, u_2} k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) := ⋯
f : k ⊗[R] M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤ :=
  AlgebraTensorModule.lift
    ((↑R :
        {S M : Type u_1} →
          {M₂ : Type u_2} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := k)
      ((LinearEquiv.symm
            (LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)) :
          (a : M →ₗ[R] M ⧸ 𝔪 • ⊤) → k →ₗ[k] M →ₗ[R] M ⧸ 𝔪 • ⊤)
        (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ))
this :
  f ∘ₗ (TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1 =
    (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ
x : M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤
obtain :
  ∀ (x : M),
    ∃ (a : k ⊗[R] M),
      Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
        ((f : (a : k ⊗[R] M) → M ⧸ 𝔪 • ⊤) a : M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
        (((HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ : (a : M) → M ⧸ 𝔪 • ⊤) x :
          M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
⊢ ∃ (a : k ⊗[R] M), (f : (a : k ⊗[R] M) → M ⧸ 𝔪 • ⊤) a = x

Tactic:
obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x

Premises used: Submodule.mkQ_surjective, rfl
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
inst_4 : Module.Finite R M
hN :
  Eq (α := Submodule R (k ⊗[R] M))
    (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) ⊤
this_1 : Module.{u_1, u_2} k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) := ⋯
f : k ⊗[R] M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤ :=
  AlgebraTensorModule.lift
    ((↑R :
        {S M : Type u_1} →
          {M₂ : Type u_2} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := k)
      ((LinearEquiv.symm
            (LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)) :
          (a : M →ₗ[R] M ⧸ 𝔪 • ⊤) → k →ₗ[k] M →ₗ[R] M ⧸ 𝔪 • ⊤)
        (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ))
this :
  f ∘ₗ (TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1 =
    (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ
x : M
rw :
  ∃ (a : k ⊗[R] M),
    Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
      ((f : (a : k ⊗[R] M) → M ⧸ 𝔪 • ⊤) a : M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
      ((f : (a : k ⊗[R] M) → M ⧸ 𝔪 • ⊤)
          (((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1 : (a : M) → k ⊗[R] M) x) :
        M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
⊢ ∃ (a : k ⊗[R] M),
    Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
      ((f : (a : k ⊗[R] M) → M ⧸ 𝔪 • ⊤) a : M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
      (((HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ : (a : M) → M ⧸ 𝔪 • ⊤) x :
        M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)

Tactic:
rw [← this, LinearMap.comp_apply]

Premises used: LinearMap.comp_apply
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
inst_4 : Module.Finite R M
hN :
  Eq (α := Submodule R (k ⊗[R] M))
    (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) ⊤
this_1 : Module.{u_1, u_2} k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) := ⋯
f : k ⊗[R] M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤ :=
  AlgebraTensorModule.lift
    ((↑R :
        {S M : Type u_1} →
          {M₂ : Type u_2} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := k)
      ((LinearEquiv.symm
            (LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)) :
          (a : M →ₗ[R] M ⧸ 𝔪 • ⊤) → k →ₗ[k] M →ₗ[R] M ⧸ 𝔪 • ⊤)
        (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ))
this :
  f ∘ₗ (TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1 =
    (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ
x : M
⊢ ∃ (a : k ⊗[R] M),
    Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
      ((f : (a : k ⊗[R] M) → M ⧸ 𝔪 • ⊤) a : M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
      ((f : (a : k ⊗[R] M) → M ⧸ 𝔪 • ⊤)
          (((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1 : (a : M) → k ⊗[R] M) x) :
        M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
inst_4 : Module.Finite R M
hN :
  Eq (α := Submodule R (k ⊗[R] M))
    (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) ⊤
this_1 : Module.{u_1, u_2} k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) := ⋯
f : k ⊗[R] M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤ :=
  AlgebraTensorModule.lift
    ((↑R :
        {S M : Type u_1} →
          {M₂ : Type u_2} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := k)
      ((LinearEquiv.symm
            (LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)) :
          (a : M →ₗ[R] M ⧸ 𝔪 • ⊤) → k →ₗ[k] M →ₗ[R] M ⧸ 𝔪 • ⊤)
        (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ))
this :
  f ∘ₗ (TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1 =
    (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ
x : M
⊢ ∃ (a : k ⊗[R] M),
    Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
      ((f : (a : k ⊗[R] M) → M ⧸ 𝔪 • ⊤) a : M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
      ((f : (a : k ⊗[R] M) → M ⧸ 𝔪 • ⊤)
          (((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1 : (a : M) → k ⊗[R] M) x) :
        M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
inst_4 : Module.Finite R M
hN :
  Eq (α := Submodule R (k ⊗[R] M))
    (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) ⊤
this_1 : Module.{u_1, u_2} k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) := ⋯
f : k ⊗[R] M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤ :=
  AlgebraTensorModule.lift
    ((↑R :
        {S M : Type u_1} →
          {M₂ : Type u_2} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := k)
      ((LinearEquiv.symm
            (LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)) :
          (a : M →ₗ[R] M ⧸ 𝔪 • ⊤) → k →ₗ[k] M →ₗ[R] M ⧸ 𝔪 • ⊤)
        (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ))
this :
  f ∘ₗ (TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1 =
    (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ
⊢ Surjective (α := k ⊗[R] M) (β := M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
    (⇑f : (a : k ⊗[R] M) → M ⧸ 𝔪 • ⊤)

Tactic:
have hf : Function.Surjective f := by
      intro x; obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x
      rw [← this, LinearMap.comp_apply]; exact ⟨_, rfl⟩
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
inst_4 : Module.Finite R M
hN :
  Eq (α := Submodule R (k ⊗[R] M))
    (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) ⊤
this_1 : Module.{u_1, u_2} k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) := ⋯
f : k ⊗[R] M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤ :=
  AlgebraTensorModule.lift
    ((↑R :
        {S M : Type u_1} →
          {M₂ : Type u_2} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := k)
      ((LinearEquiv.symm
            (LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)) :
          (a : M →ₗ[R] M ⧸ 𝔪 • ⊤) → k →ₗ[k] M →ₗ[R] M ⧸ 𝔪 • ⊤)
        (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ))
this :
  f ∘ₗ (TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1 =
    (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ
hf :
  Surjective (α := k ⊗[R] M) (β := M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
    (⇑f : (a : k ⊗[R] M) → M ⧸ 𝔪 • ⊤)
⊢ Submodule.map f (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) =
    Submodule.map f ⊤

Tactic:
apply_fun Submodule.map f at hN

Premises used: Submodule.map
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
inst_4 : Module.Finite R M
this_1 : Module.{u_1, u_2} k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) := ⋯
f : k ⊗[R] M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤ :=
  AlgebraTensorModule.lift
    ((↑R :
        {S M : Type u_1} →
          {M₂ : Type u_2} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := k)
      ((LinearEquiv.symm
            (LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)) :
          (a : M →ₗ[R] M ⧸ 𝔪 • ⊤) → k →ₗ[k] M →ₗ[R] M ⧸ 𝔪 • ⊤)
        (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ))
this :
  f ∘ₗ (TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1 =
    (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ
hf :
  Surjective (α := k ⊗[R] M) (β := M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
    (⇑f : (a : k ⊗[R] M) → M ⧸ 𝔪 • ⊤)
hN :
  Submodule.map f (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) =
    Submodule.map f ⊤
mp : ∀ (hN : Submodule.map (f ∘ₗ (TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N = Submodule.map f ⊤), N = ⊤
mp₁ : ∀ (hN : Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = Submodule.map f ⊤), N = ⊤
mp₂ : ∀ (hN : Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = f.range), N = ⊤
mp₃ : ∀ (hN : Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤), N = ⊤
mp₄ mp₅ mp₆ mp₇ : ∀ (hN : N = ⊤), N = ⊤
⊢ N = ⊤

Tactic:
rwa [← Submodule.map_comp, this, Submodule.map_top, LinearMap.range_eq_top.2 hf,
      map_mkQ_eq_top] at hN

Premises used: Iff.mpr, Submodule.map_top, Submodule.map_comp, LinearMap.range_eq_top, IsLocalRing.map_mkQ_eq_top
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : Module.Finite R M
mpr :
  Surjective (α := M) (β := k ⊗[R] M) (⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M)
⊢ Eq (α := Submodule R (k ⊗[R] M))
    (Submodule.map (R := R) (M := M) (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) ⊤)
    ⊤

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

Premises used: Submodule.map_top, LinearMap.range_eq_top
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : Module.Finite R M
⊢ Surjective (α := M) (β := k ⊗[R] M) (⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M)

Tactic:
TensorProduct.mk_surjective R M k Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective, IsLocalRing.ResidueField, TensorProduct.mk_surjective
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : Module.Finite R M
⊢ Surjective (α := M) (β := k ⊗[R] M) (⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M)

Tactic:
exact TensorProduct.mk_surjective R M k Ideal.Quotient.mk_surjective