Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
R' : Type u_2
R'' : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing R''
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R R''
inst✝² : Algebra R' R''
inst✝¹ : IsScalarTower R R' R''
inst✝ : Algebra R S
e : R' ⊗[R] S
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.rTensor S (ofId R' R'')
ψ : R'' ⊗[R] S →ₐ[R''] R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}) :=
  TensorProduct.lift (ofId R'' (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e})))
    ((AlgHom.restrictScalars R TensorProduct.includeRight).comp
      ((Ideal.Quotient.mkₐ R (Ideal.span {e})).comp TensorProduct.includeRight))
    ⋯
hψφ :
  (AlgHom.restrictScalars R' ψ).comp φ =
    (AlgHom.restrictScalars R' TensorProduct.includeRight).comp (Ideal.Quotient.mkₐ R' (Ideal.span {e}))
heψ : Ideal.span {φ e} ≤ RingHom.ker ψ
x✝ : S
⊢ ((AlgHom.restrictScalars R
            (((AlgHom.restrictScalars R'
                      ((Ideal.Quotient.liftₐ (Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e}) ψ heψ).comp
                        (TensorProduct.lift
                          (ofId R'' (R'' ⊗[R] S ⧸ Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e}))
                          (Ideal.quotientMapₐ (Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e}) φ ⋯) ⋯))).comp
                  TensorProduct.includeRight).comp
              (Ideal.Quotient.mkₐ R' (Ideal.span {e})))).comp
        TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            (((AlgHom.restrictScalars R' (AlgHom.id R'' (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e})))).comp
                  TensorProduct.includeRight).comp
              (Ideal.Quotient.mkₐ R' (Ideal.span {e})))).comp
        TensorProduct.includeRight)
      x✝

Tactic:
;

Goal state after:
R : Type u_1
R' : Type u_2
R'' : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing R''
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R R''
inst✝² : Algebra R' R''
inst✝¹ : IsScalarTower R R' R''
inst✝ : Algebra R S
e : R' ⊗[R] S
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.rTensor S (ofId R' R'')
ψ : R'' ⊗[R] S →ₐ[R''] R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}) :=
  TensorProduct.lift (ofId R'' (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e})))
    ((AlgHom.restrictScalars R TensorProduct.includeRight).comp
      ((Ideal.Quotient.mkₐ R (Ideal.span {e})).comp TensorProduct.includeRight))
    ⋯
hψφ :
  (AlgHom.restrictScalars R' ψ).comp φ =
    (AlgHom.restrictScalars R' TensorProduct.includeRight).comp (Ideal.Quotient.mkₐ R' (Ideal.span {e}))
heψ : Ideal.span {φ e} ≤ RingHom.ker ψ
x✝ : S
⊢ ((AlgHom.restrictScalars R
            (((AlgHom.restrictScalars R'
                      ((Ideal.Quotient.liftₐ (Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e}) ψ heψ).comp
                        (TensorProduct.lift
                          (ofId R'' (R'' ⊗[R] S ⧸ Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e}))
                          (Ideal.quotientMapₐ (Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e}) φ ⋯) ⋯))).comp
                  TensorProduct.includeRight).comp
              (Ideal.Quotient.mkₐ R' (Ideal.span {e})))).comp
        TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            (((AlgHom.restrictScalars R' (AlgHom.id R'' (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e})))).comp
                  TensorProduct.includeRight).comp
              (Ideal.Quotient.mkₐ R' (Ideal.span {e})))).comp
        TensorProduct.includeRight)
      x✝