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
⊢ (fun f ↦ ⟨AlgHom.domRestrict B f, AlgHom.extendScalars B f⟩)
      ((fun fg ↦
          let x := fg.fst.toAlgebra;
          AlgHom.restrictScalars A fg.snd)
        ⟨{ 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'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝,
            commutes' := hg }⟩) =
    ⟨{ 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'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝,
        commutes' := hg }⟩

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

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
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
map_one'✝ : (fun x ↦ g ((algebraMap B C) x)) 1 = 1
map_mul'✝ :
  ∀ (x y : B),
    { toFun := fun x ↦ g ((algebraMap B C) x), map_one' := map_one'✝ }.toFun (x * y) =
      { toFun := fun x ↦ g ((algebraMap B C) x), map_one' := map_one'✝ }.toFun x *
        { toFun := fun x ↦ g ((algebraMap B C) x), map_one' := map_one'✝ }.toFun y
map_zero'✝ : (↑{ toFun := fun x ↦ g ((algebraMap B C) x), map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun 0 = 0
map_add'✝ :
  ∀ (x y : B),
    (↑{ toFun := fun x ↦ g ((algebraMap B C) x), map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun (x + y) =
      (↑{ toFun := fun x ↦ g ((algebraMap B C) x), map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun x +
        (↑{ toFun := fun x ↦ g ((algebraMap B C) x), map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun y
commutes'✝ :
  ∀ (r : A),
    (↑↑{ toFun := fun x ↦ g ((algebraMap B C) x), 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
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
⊢ (fun f ↦ ⟨AlgHom.domRestrict B f, AlgHom.extendScalars B f⟩)
      ((fun fg ↦
          let x := fg.fst.toAlgebra;
          AlgHom.restrictScalars A fg.snd)
        ⟨{ toFun := fun x ↦ g ((algebraMap 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'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹,
            map_add' := map_add'✝¹, commutes' := hg }⟩) =
    ⟨{ toFun := fun x ↦ g ((algebraMap 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'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹,
        commutes' := hg }⟩