awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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
have 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) 𝔪 ⊤)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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))
⊢ N = ⊤
have this₁ : 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]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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) 𝔪 ⊤
⊢ ∃ (a : k ⊗[R] M), (f : (a : k ⊗[R] M) → M ⧸ 𝔪 • ⊤) a = x
have 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) 𝔪 ⊤)
Tactic: obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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) 𝔪 ⊤)
      (((HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ : (a : M) → M ⧸ 𝔪 • ⊤) x :
        M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
have 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) 𝔪 ⊤)
Tactic: rw [← this, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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
⊢ N = ⊤
have hf : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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 ⧸ 𝔪 • ⊤)
⊢ N = ⊤
have 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 ⊤
Tactic: apply_fun Submodule.map f at hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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 ⊤
⊢ N = ⊤
have mp : ∀ (hN : Submodule.map (f ∘ₗ (TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N = Submodule.map f ⊤), N = ⊤
Tactic: rwa [← Submodule.map_comp, this, Submodule.map_top, LinearMap.range_eq_top.2 hf,
      map_mkQ_eq_top] at hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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 = ⊤
⊢ N = ⊤
have mp₁ : ∀ (hN : Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = Submodule.map f ⊤), N = ⊤
Tactic: rwa [← Submodule.map_comp, this, Submodule.map_top, LinearMap.range_eq_top.2 hf,
      map_mkQ_eq_top] at hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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 = ⊤
⊢ N = ⊤
have mp₂ : ∀ (hN : Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = f.range), N = ⊤
Tactic: rwa [← Submodule.map_comp, this, Submodule.map_top, LinearMap.range_eq_top.2 hf,
      map_mkQ_eq_top] at hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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 = ⊤
⊢ N = ⊤
have mp₃ : ∀ (hN : Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤), N = ⊤
Tactic: rwa [← Submodule.map_comp, this, Submodule.map_top, LinearMap.range_eq_top.2 hf,
      map_mkQ_eq_top] at hN
Cleared hypotheses: hN