-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Quotient (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
M : Type u_4
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
N : Type u_5
inst_9 : AddCommGroup N
inst_10 : Module R N
inst_11 : Module B N
inst_12 : IsScalarTower R B N
n : Submodule B N
m : A
x : TensorProduct.{u_1, u_4, u_5} R M (N ⧸ n)
zero :
  (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n) :
        (a : M ⊗[R] (N ⧸ Submodule.restrictScalars R n)) →
          M ⊗[R] N ⧸ (TensorProduct.map LinearMap.id (Submodule.restrictScalars R n).subtype).range)
      (HSMul.hSMul (β := TensorProduct.{u_1, u_4, u_5} R M (N ⧸ n)) m 0) =
    HSMul.hSMul (α := A) (β :=
      HasQuotient.Quotient (M ⊗[R] N) (B := Submodule A (M ⊗[R] N))
        (LinearMap.range (R := A) (M := TensorProduct.{u_1, u_4, u_5} R M ↥n) (τ₁₂ := RingHom.id A)
          (((lTensor A M : (↥n →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_4, u_5} R M ↥n →ₗ[A] M ⊗[R] N) :
              (a : ↥n →ₗ[R] N) → M ⊗[R] ↥n →ₗ[A] M ⊗[R] N)
            ((↑R :
                {S : Type u_3} →
                  {M M₂ : Type u_5} →
                    [inst : Semiring R] →
                      [inst_13 : Semiring S] →
                        [inst_14 : AddCommMonoid M] →
                          [inst_15 : AddCommMonoid M₂] →
                            [inst_16 : Module R M] →
                              [inst_17 : Module R M₂] →
                                [inst_18 : Module S M] →
                                  [inst_19 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              n.subtype))))
      ((RingHom.id A : (a : A) → A) m : A)
      ((TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n) :
          (a : M ⊗[R] (N ⧸ Submodule.restrictScalars R n)) →
            M ⊗[R] N ⧸ (TensorProduct.map LinearMap.id (Submodule.restrictScalars R n).subtype).range)
        0)
add :
  ∀ (x y : TensorProduct.{u_1, u_4, u_5} R M (N ⧸ n))
    (hx :
      (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n) :
            (a : M ⊗[R] (N ⧸ Submodule.restrictScalars R n)) →
              M ⊗[R] N ⧸ (TensorProduct.map LinearMap.id (Submodule.restrictScalars R n).subtype).range)
          (m • x) =
        HSMul.hSMul (α := A) (β :=
          HasQuotient.Quotient (M ⊗[R] N) (B := Submodule A (M ⊗[R] N))
            (LinearMap.range (R := A) (M := TensorProduct.{u_1, u_4, u_5} R M ↥n) (τ₁₂ := RingHom.id A)
              (((lTensor A M : (↥n →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_4, u_5} R M ↥n →ₗ[A] M ⊗[R] N) :
                  (a : ↥n →ₗ[R] N) → M ⊗[R] ↥n →ₗ[A] M ⊗[R] N)
                ((↑R :
                    {S : Type u_3} →
                      {M M₂ : Type u_5} →
                        [inst : Semiring R] →
                          [inst_13 : Semiring S] →
                            [inst_14 : AddCommMonoid M] →
                              [inst_15 : AddCommMonoid M₂] →
                                [inst_16 : Module R M] →
                                  [inst_17 : Module R M₂] →
                                    [inst_18 : Module S M] →
                                      [inst_19 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  n.subtype))))
          ((RingHom.id A : (a : A) → A) m : A)
          ((TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n) :
                (a : M ⊗[R] (N ⧸ Submodule.restrictScalars R n)) →
                  M ⊗[R] N ⧸ (TensorProduct.map LinearMap.id (Submodule.restrictScalars R n).subtype).range)
              x :
            HasQuotient.Quotient (M ⊗[R] N) (B := Submodule R (M ⊗[R] N))
              (LinearMap.range (M := TensorProduct.{u_1, u_4, u_5} R M ↥(Submodule.restrictScalars R n))
                (TensorProduct.map LinearMap.id (Submodule.subtype (Submodule.restrictScalars R n))))))
    (hy :
      (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n) :
            (a : M ⊗[R] (N ⧸ Submodule.restrictScalars R n)) →
              M ⊗[R] N ⧸ (TensorProduct.map LinearMap.id (Submodule.restrictScalars R n).subtype).range)
          (m • y) =
        HSMul.hSMul (α := A) (β :=
          HasQuotient.Quotient (M ⊗[R] N) (B := Submodule A (M ⊗[R] N))
            (LinearMap.range (R := A) (M := TensorProduct.{u_1, u_4, u_5} R M ↥n) (τ₁₂ := RingHom.id A)
              (((lTensor A M : (↥n →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_4, u_5} R M ↥n →ₗ[A] M ⊗[R] N) :
                  (a : ↥n →ₗ[R] N) → M ⊗[R] ↥n →ₗ[A] M ⊗[R] N)
                ((↑R :
                    {S : Type u_3} →
                      {M M₂ : Type u_5} →
                        [inst : Semiring R] →
                          [inst_13 : Semiring S] →
                            [inst_14 : AddCommMonoid M] →
                              [inst_15 : AddCommMonoid M₂] →
                                [inst_16 : Module R M] →
                                  [inst_17 : Module R M₂] →
                                    [inst_18 : Module S M] →
                                      [inst_19 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  n.subtype))))
          ((RingHom.id A : (a : A) → A) m : A)
          ((TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n) :
                (a : M ⊗[R] (N ⧸ Submodule.restrictScalars R n)) →
                  M ⊗[R] N ⧸ (TensorProduct.map LinearMap.id (Submodule.restrictScalars R n).subtype).range)
              y :
            HasQuotient.Quotient (M ⊗[R] N) (B := Submodule R (M ⊗[R] N))
              (LinearMap.range (M := TensorProduct.{u_1, u_4, u_5} R M ↥(Submodule.restrictScalars R n))
                (TensorProduct.map LinearMap.id (Submodule.subtype (Submodule.restrictScalars R n)))))),
    (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n) :
          (a : M ⊗[R] (N ⧸ Submodule.restrictScalars R n)) →
            M ⊗[R] N ⧸ (TensorProduct.map LinearMap.id (Submodule.restrictScalars R n).subtype).range)
        (m • (x + y)) =
      HSMul.hSMul (α := A) (β :=
        HasQuotient.Quotient (M ⊗[R] N) (B := Submodule A (M ⊗[R] N))
          (LinearMap.range (R := A) (M := TensorProduct.{u_1, u_4, u_5} R M ↥n) (τ₁₂ := RingHom.id A)
            (((lTensor A M : (↥n →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_4, u_5} R M ↥n →ₗ[A] M ⊗[R] N) :
                (a : ↥n →ₗ[R] N) → M ⊗[R] ↥n →ₗ[A] M ⊗[R] N)
              ((↑R :
                  {S : Type u_3} →
                    {M M₂ : Type u_5} →
                      [inst : Semiring R] →
                        [inst_13 : Semiring S] →
                          [inst_14 : AddCommMonoid M] →
                            [inst_15 : AddCommMonoid M₂] →
                              [inst_16 : Module R M] →
                                [inst_17 : Module R M₂] →
                                  [inst_18 : Module S M] →
                                    [inst_19 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                n.subtype))))
        ((RingHom.id A : (a : A) → A) m : A)
        ((TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n) :
              (a : M ⊗[R] (N ⧸ Submodule.restrictScalars R n)) →
                M ⊗[R] N ⧸ (TensorProduct.map LinearMap.id (Submodule.restrictScalars R n).subtype).range)
            (x + y) :
          HasQuotient.Quotient (M ⊗[R] N) (B := Submodule R (M ⊗[R] N))
            (LinearMap.range (M := TensorProduct.{u_1, u_4, u_5} R M ↥(Submodule.restrictScalars R n))
              (TensorProduct.map LinearMap.id (Submodule.subtype (Submodule.restrictScalars R n)))))
⊢ (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n) :
        (a : M ⊗[R] (N ⧸ Submodule.restrictScalars R n)) →
          M ⊗[R] N ⧸ (TensorProduct.map LinearMap.id (Submodule.restrictScalars R n).subtype).range)
      (m • x) =
    HSMul.hSMul (α := A) (β :=
      HasQuotient.Quotient (M ⊗[R] N) (B := Submodule A (M ⊗[R] N))
        (LinearMap.range (R := A) (M := TensorProduct.{u_1, u_4, u_5} R M ↥n) (τ₁₂ := RingHom.id A)
          (((lTensor A M : (↥n →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_4, u_5} R M ↥n →ₗ[A] M ⊗[R] N) :
              (a : ↥n →ₗ[R] N) → M ⊗[R] ↥n →ₗ[A] M ⊗[R] N)
            ((↑R :
                {S : Type u_3} →
                  {M M₂ : Type u_5} →
                    [inst : Semiring R] →
                      [inst_13 : Semiring S] →
                        [inst_14 : AddCommMonoid M] →
                          [inst_15 : AddCommMonoid M₂] →
                            [inst_16 : Module R M] →
                              [inst_17 : Module R M₂] →
                                [inst_18 : Module S M] →
                                  [inst_19 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              n.subtype))))
      ((RingHom.id A : (a : A) → A) m : A)
      ((TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n) :
            (a : M ⊗[R] (N ⧸ Submodule.restrictScalars R n)) →
              M ⊗[R] N ⧸ (TensorProduct.map LinearMap.id (Submodule.restrictScalars R n).subtype).range)
          x :
        HasQuotient.Quotient (M ⊗[R] N) (B := Submodule R (M ⊗[R] N))
          (LinearMap.range (M := TensorProduct.{u_1, u_4, u_5} R M ↥(Submodule.restrictScalars R n))
            (TensorProduct.map LinearMap.id (Submodule.subtype (Submodule.restrictScalars R n)))))
have tmul : ∀ (x : M) (y : N ⧸ n),
  (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n) :
        (a : M ⊗[R] (N ⧸ Submodule.restrictScalars R n)) →
          M ⊗[R] N ⧸ (TensorProduct.map LinearMap.id (Submodule.restrictScalars R n).subtype).range)
      (HSMul.hSMul (β := TensorProduct.{u_1, u_4, u_5} R M (N ⧸ n)) m (x ⊗ₜ[R] y)) =
    HSMul.hSMul (α := A) (β :=
      HasQuotient.Quotient (M ⊗[R] N) (B := Submodule A (M ⊗[R] N))
        (LinearMap.range (R := A) (M := TensorProduct.{u_1, u_4, u_5} R M ↥n) (τ₁₂ := RingHom.id A)
          (((lTensor A M : (↥n →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_4, u_5} R M ↥n →ₗ[A] M ⊗[R] N) :
              (a : ↥n →ₗ[R] N) → M ⊗[R] ↥n →ₗ[A] M ⊗[R] N)
            ((↑R :
                {S : Type u_3} →
                  {M M₂ : Type u_5} →
                    [inst : Semiring R] →
                      [inst_13 : Semiring S] →
                        [inst_14 : AddCommMonoid M] →
                          [inst_15 : AddCommMonoid M₂] →
                            [inst_16 : Module R M] →
                              [inst_17 : Module R M₂] →
                                [inst_18 : Module S M] →
                                  [inst_19 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              n.subtype))))
      ((RingHom.id A : (a : A) → A) m : A)
      ((TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n) :
            (a : M ⊗[R] (N ⧸ Submodule.restrictScalars R n)) →
              M ⊗[R] N ⧸ (TensorProduct.map LinearMap.id (Submodule.restrictScalars R n).subtype).range)
          (x ⊗ₜ[R] y) :
        HasQuotient.Quotient (M ⊗[R] N) (B := Submodule R (M ⊗[R] N))
          (LinearMap.range (M := TensorProduct.{u_1, u_4, u_5} R M ↥(Submodule.restrictScalars R n))
            (TensorProduct.map LinearMap.id (Submodule.subtype (Submodule.restrictScalars R n)))))
Tactic: induction x with
    | zero => simp
    | add x y hx hy => simp [hx, hy]
    | tmul x y =>
      obtain ⟨y, rfl⟩ := Submodule.Quotient.mk_surjective _ y
      rw [smul_tmul']
      rfl
Cleared hypotheses: x