-- Lean 4 proof step from Mathlib.RingTheory.AlgebraTower (goal)
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
⊢ 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 })
have 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 })
Tactic: obtain rfl : f = fun x => g (algebraMap B C x) := by
      ext x
      exact (hg x).symm
Cleared hypotheses: f, map_one', map_mul', map_zero', map_add', commutes', hg