-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
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 (α := A ⧸ I) ((Quotient.mk I : (a : A) → A ⧸ I) x : A ⧸ I) (0 : A ⧸ I)
have a : 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))
Tactic: apply inj