-- 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_1 : C →ₐ[A] D
f : B → D
map_one' : f 1 = 1
map_mul' :
  ∀ (x y : B),
    { toFun := f, map_one' := map_one' : OneHom B D }.toFun (x * y) =
      { toFun := f, map_one' := map_one' : OneHom B D }.toFun x *
        { toFun := f, map_one' := map_one' : OneHom B D }.toFun y
map_zero' : (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun 0 = 0
map_add' :
  ∀ (x y : B),
    (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun (x + y) =
      (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun x +
        (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun y
commutes' :
  ∀ (r : A),
    (↑(↑{ toFun := f, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add' :
                    B →+* D } :
                B →* D) :
            OneHom B D).toFun
        ((algebraMap A B : (a : A) → B) r) =
      (algebraMap A D : (a : A) → D) r
g : C → D
map_one'_1 : g 1 = 1
map_mul'_1 :
  ∀ (x y : C),
    { toFun := g, map_one' := map_one'_1 : OneHom C D }.toFun (x * y) =
      { toFun := g, map_one' := map_one'_1 : OneHom C D }.toFun x *
        { toFun := g, map_one' := map_one'_1 : OneHom C D }.toFun y
map_zero'_1 : (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun 0 = 0
map_add'_1 :
  ∀ (x y : C),
    (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun (x + y) =
      (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun x +
        (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun y
hg :
  ∀ (r : B),
    (↑(↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1 :
                    C →+* D } :
                C →* D) :
            OneHom C D).toFun
        ((algebraMap B C : (a : B) → C) r) =
      (algebraMap B D : (a : B) → D) r
obtain :
  ∀ (map_one' : Eq.{u_6 + 1} (α := D) ((fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x)) 1) 1)
    (map_mul' :
      ∀ (x y : B),
        OneHom.toFun { toFun := fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x), map_one' := map_one' } (x * y) =
          HMul.hMul (α := D)
            (OneHom.toFun
              { toFun := fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x), map_one' := map_one' : OneHom B D } x)
            (OneHom.toFun
              { toFun := fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x), map_one' := map_one' : OneHom B D } y))
    (map_zero' :
      (↑{ toFun := fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x), map_one' := map_one', map_mul' := map_mul' :
                  B →* D } :
              OneHom B D).toFun
          0 =
        0)
    (map_add' :
      ∀ (x y : B),
        (↑{ toFun := fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x), map_one' := map_one', map_mul' := map_mul' :
                    B →* D } :
                OneHom B D).toFun
            (x + y) =
          (↑{ toFun := fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x), map_one' := map_one', map_mul' := map_mul' :
                      B →* D } :
                  OneHom B D).toFun
              x +
            (↑{ toFun := fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x), map_one' := map_one',
                      map_mul' := map_mul' : 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', map_mul' := map_mul',
                        map_zero' := map_zero', map_add' := map_add' : 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'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1,
                        map_add' := map_add'_1 : 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', map_mul' := map_mul',
              map_zero' := map_zero', map_add' := map_add', commutes' := commutes' }
            { toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1,
              map_add' := map_add'_1, 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', map_mul' := map_mul',
          map_zero' := map_zero', map_add' := map_add', commutes' := commutes' }
        { toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1,
          commutes' := hg : C →ₐ[B] D })
⊢ 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 := f, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
            commutes' := commutes' }
          { toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1,
            map_add' := map_add'_1, commutes' := hg : C →ₐ[B] D })))
    (Sigma.mk (β := fun (f : B →ₐ[A] D) ↦ C →ₐ[B] D)
      { toFun := f, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
        commutes' := commutes' }
      { toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1,
        commutes' := hg : C →ₐ[B] D })

Tactic:
obtain rfl : f = fun x => g (algebraMap B C x) := by
      ext x
      exact (hg x).symm

Premises used: Algebra.algebraMap, DFunLike.coe, rfl