Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: 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✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f✝ : C →ₐ[A] D
f : B → D
map_one'✝¹ : f 1 = 1
map_mul'✝¹ :
  ∀ (x y : B),
    { toFun := f, map_one' := map_one'✝¹ }.toFun (x * y) =
      { toFun := f, map_one' := map_one'✝¹ }.toFun x * { toFun := f, map_one' := map_one'✝¹ }.toFun y
map_zero'✝¹ : (↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun 0 = 0
map_add'✝¹ :
  ∀ (x y : B),
    (↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun (x + y) =
      (↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun x +
        (↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun y
commutes'✝ :
  ∀ (r : A),
    (↑↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹,
                map_add' := map_add'✝¹ }).toFun
        ((algebraMap A B) r) =
      (algebraMap A D) r
g : C → D
map_one'✝ : g 1 = 1
map_mul'✝ :
  ∀ (x y : C),
    { toFun := g, map_one' := map_one'✝ }.toFun (x * y) =
      { toFun := g, map_one' := map_one'✝ }.toFun x * { toFun := g, map_one' := map_one'✝ }.toFun y
map_zero'✝ : (↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun 0 = 0
map_add'✝ :
  ∀ (x y : C),
    (↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun (x + y) =
      (↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun x +
        (↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun y
hg :
  ∀ (r : B),
    (↑↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝,
                map_add' := map_add'✝ }).toFun
        ((algebraMap B C) r) =
      (algebraMap B D) r
⊢ f = fun x ↦ g ((algebraMap B C) x)

Tactic:
ext x

Goal state after:
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✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f✝ : C →ₐ[A] D
f : B → D
map_one'✝¹ : f 1 = 1
map_mul'✝¹ :
  ∀ (x y : B),
    { toFun := f, map_one' := map_one'✝¹ }.toFun (x * y) =
      { toFun := f, map_one' := map_one'✝¹ }.toFun x * { toFun := f, map_one' := map_one'✝¹ }.toFun y
map_zero'✝¹ : (↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun 0 = 0
map_add'✝¹ :
  ∀ (x y : B),
    (↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun (x + y) =
      (↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun x +
        (↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun y
commutes'✝ :
  ∀ (r : A),
    (↑↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹,
                map_add' := map_add'✝¹ }).toFun
        ((algebraMap A B) r) =
      (algebraMap A D) r
g : C → D
map_one'✝ : g 1 = 1
map_mul'✝ :
  ∀ (x y : C),
    { toFun := g, map_one' := map_one'✝ }.toFun (x * y) =
      { toFun := g, map_one' := map_one'✝ }.toFun x * { toFun := g, map_one' := map_one'✝ }.toFun y
map_zero'✝ : (↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun 0 = 0
map_add'✝ :
  ∀ (x y : C),
    (↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun (x + y) =
      (↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun x +
        (↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun y
hg :
  ∀ (r : B),
    (↑↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝,
                map_add' := map_add'✝ }).toFun
        ((algebraMap B C) r) =
      (algebraMap B D) r
x : B
⊢ f x = g ((algebraMap B C) x)