-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.FaithfullyFlat A B
I : Ideal A
inj :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := A ⧸ I) (β :=
    HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))
    (⇑((↑A :
              {S : Type u_2} →
                {M : Type (max u_1 u_2)} →
                  {M₂ : Type u_2} →
                    [inst : Semiring A] →
                      [inst_4 : Semiring S] →
                        [inst_5 : AddCommMonoid M] →
                          [inst_6 : AddCommMonoid M₂] →
                            [inst_7 : Module A M] →
                              [inst_8 : Module A M₂] →
                                [inst_9 : Module S M] →
                                  [inst_10 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
            (AlgEquiv.toLinearMap (AlgEquiv.symm (quotIdealMapEquivTensorQuot B I))) ∘ₗ
          (TensorProduct.mk A B (A ⧸ I) : (a : B) → A ⧸ I →ₗ[A] B ⊗[A] (A ⧸ I)) 1) :
      (a : A ⧸ I) → B ⧸ map (algebraMap A B) I)
x : A
hx :
  Eq.{u_2 + 1} (α := HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))
    ((Quotient.mk (map (F := A →+* B) (algebraMap A B) I) : (a : B) → B ⧸ map (algebraMap A B) I)
        ((algebraMap A B : (a : A) → B) x) :
      HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))
    (0 : HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))
⊢ Eq.{u_2 + 1} (α := HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))
    ((((↑A :
                  {S : Type u_2} →
                    {M : Type (max u_1 u_2)} →
                      {M₂ : Type u_2} →
                        [inst : Semiring A] →
                          [inst_4 : Semiring S] →
                            [inst_5 : AddCommMonoid M] →
                              [inst_6 : AddCommMonoid M₂] →
                                [inst_7 : Module A M] →
                                  [inst_8 : Module A M₂] →
                                    [inst_9 : Module S M] →
                                      [inst_10 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
                (AlgEquiv.toLinearMap (AlgEquiv.symm (quotIdealMapEquivTensorQuot B I))) ∘ₗ
              (TensorProduct.mk A B (A ⧸ I) : (a : B) → A ⧸ I →ₗ[A] B ⊗[A] (A ⧸ I)) 1 :
            LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id A) (A ⧸ I)
              (HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))) :
          (a : A ⧸ I) → B ⧸ map (algebraMap A B) I)
        ((Quotient.mk I : (a : A) → A ⧸ I) x) :
      HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))
    ((((↑A :
                  {S : Type u_2} →
                    {M : Type (max u_1 u_2)} →
                      {M₂ : Type u_2} →
                        [inst : Semiring A] →
                          [inst_4 : Semiring S] →
                            [inst_5 : AddCommMonoid M] →
                              [inst_6 : AddCommMonoid M₂] →
                                [inst_7 : Module A M] →
                                  [inst_8 : Module A M₂] →
                                    [inst_9 : Module S M] →
                                      [inst_10 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
                (AlgEquiv.toLinearMap (AlgEquiv.symm (quotIdealMapEquivTensorQuot B I))) ∘ₗ
              (TensorProduct.mk A B (A ⧸ I) : (a : B) → A ⧸ I →ₗ[A] B ⊗[A] (A ⧸ I)) 1 :
            LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id A) (A ⧸ I)
              (HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))) :
          (a : A ⧸ I) → B ⧸ map (algebraMap A B) I)
        0 :
      HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))
have this : Eq.{u_2 + 1} (α := HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))
  ((((↑A :
                {S : Type u_2} →
                  {M : Type (max u_1 u_2)} →
                    {M₂ : Type u_2} →
                      [inst : Semiring A] →
                        [inst_4 : Semiring S] →
                          [inst_5 : AddCommMonoid M] →
                            [inst_6 : AddCommMonoid M₂] →
                              [inst_7 : Module A M] →
                                [inst_8 : Module A M₂] →
                                  [inst_9 : Module S M] →
                                    [inst_10 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
              (↑(↑(AlgEquiv.symm (quotIdealMapEquivTensorQuot B I)) : B ⊗[A] (A ⧸ I) ≃ₗ[B] B ⧸ map (algebraMap A B) I) :
                B ⊗[A] (A ⧸ I) →ₗ[B] B ⧸ map (algebraMap A B) I) ∘ₗ
            (TensorProduct.mk A B (A ⧸ I) : (a : B) → A ⧸ I →ₗ[A] B ⊗[A] (A ⧸ I)) 1 :
          LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id A) (A ⧸ I)
            (HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))) :
        (a : A ⧸ I) → B ⧸ map (algebraMap A B) I)
      ((Quotient.mk I : (a : A) → A ⧸ I) x) :
    HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))
  (0 : HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))
Tactic: have : ((quotIdealMapEquivTensorQuot B I).symm.toLinearEquiv.toLinearMap.restrictScalars _ ∘ₗ
      TensorProduct.mk A B (A ⧸ I) 1) x = 0 := by
    simp [← Algebra.algebraMap_eq_smul_one, hx]