-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring A
inst_1 : CommSemiring C
inst_2 : CommSemiring D
inst_3 : Algebra A C
inst_4 : Algebra A D
inst_5 : CommSemiring B
inst_6 : Algebra A B
inst_7 : Algebra B C
inst_8 : IsScalarTower A B C
f : C →ₐ[A] D
g : C → D
map_one' : g 1 = 1
map_mul' :
  ∀ (x y : C),
    { toFun := g, map_one' := map_one' : OneHom C D }.toFun (x * y) =
      { toFun := g, map_one' := map_one' : OneHom C D }.toFun x *
        { toFun := g, map_one' := map_one' : OneHom C D }.toFun y
map_zero' : (↑{ toFun := g, map_one' := map_one', map_mul' := map_mul' : C →* D } : OneHom C D).toFun 0 = 0
map_add' :
  ∀ (x y : C),
    (↑{ toFun := g, map_one' := map_one', map_mul' := map_mul' : C →* D } : OneHom C D).toFun (x + y) =
      (↑{ toFun := g, map_one' := map_one', map_mul' := map_mul' : C →* D } : OneHom C D).toFun x +
        (↑{ toFun := g, map_one' := map_one', map_mul' := map_mul' : C →* D } : OneHom C D).toFun y
map_one'_1 : Eq.{u_6 + 1} (α := D) ((fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x)) 1) 1
map_mul'_1 :
  ∀ (x y : B),
    OneHom.toFun { toFun := fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x), map_one' := map_one'_1 } (x * y) =
      HMul.hMul (α := D)
        (OneHom.toFun
          { toFun := fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x), map_one' := map_one'_1 : OneHom B D } x)
        (OneHom.toFun
          { toFun := fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x), map_one' := map_one'_1 : OneHom B D } y)
map_zero'_1 :
  (↑{ toFun := fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x), map_one' := map_one'_1, map_mul' := map_mul'_1 :
              B →* D } :
          OneHom B D).toFun
      0 =
    0
map_add'_1 :
  ∀ (x y : B),
    (↑{ toFun := fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x), map_one' := map_one'_1, map_mul' := map_mul'_1 :
                B →* D } :
            OneHom B D).toFun
        (x + y) =
      (↑{ toFun := fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x), map_one' := map_one'_1, map_mul' := map_mul'_1 :
                  B →* D } :
              OneHom B D).toFun
          x +
        (↑{ toFun := fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x), map_one' := map_one'_1,
                  map_mul' := map_mul'_1 : B →* D } :
              OneHom B D).toFun
          y
commutes' :
  ∀ (r : A),
    (↑(↑{ toFun := fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x), map_one' := map_one'_1, map_mul' := map_mul'_1,
                    map_zero' := map_zero'_1, map_add' := map_add'_1 : B →+* D } :
                B →* D) :
            OneHom B D).toFun
        ((algebraMap A B : (a : A) → B) r) =
      (algebraMap A D : (a : A) → D) r
hg :
  ∀ (r : B),
    (↑(↑{ toFun := g, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add' :
                    C →+* D } :
                C →* D) :
            OneHom C D).toFun
        ((algebraMap B C : (a : B) → C) r) =
      (algebraMap B D : (a : B) → D) r
⊢ Eq (α := (f : B →ₐ[A] D) × (C →ₐ[B] D))
    ((fun (f : C →ₐ[A] D) ↦
        (Sigma.mk (β := fun (f : B →ₐ[A] D) ↦ C →ₐ[B] D) (AlgHom.restrictDomain B f) (AlgHom.extendScalars B f) :
          (f : B →ₐ[A] D) × (C →ₐ[B] D)))
      ((fun (fg : (f : B →ₐ[A] D) × (C →ₐ[B] D)) ↦
          let x := fg.fst (β := fun (f : B →ₐ[A] D) ↦ C →ₐ[B] D).toAlgebra;
          (AlgHom.restrictScalars A (fg.snd (β := fun (f : B →ₐ[A] D) ↦ C →ₐ[B] D)) : C →ₐ[A] D))
        (Sigma.mk (β := fun (f : B →ₐ[A] D) ↦ C →ₐ[B] D)
          { toFun := fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x), map_one' := map_one'_1, map_mul' := map_mul'_1,
            map_zero' := map_zero'_1, map_add' := map_add'_1, commutes' := commutes' }
          { toFun := g, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
            commutes' := hg : C →ₐ[B] D })))
    (Sigma.mk (β := fun (f : B →ₐ[A] D) ↦ C →ₐ[B] D)
      { toFun := fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x), map_one' := map_one'_1, map_mul' := map_mul'_1,
        map_zero' := map_zero'_1, map_add' := map_add'_1, commutes' := commutes' }
      { toFun := g, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
        commutes' := hg : C →ₐ[B] D })

Tactic:
rfl