Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Star A
inst✝⁸ : Semiring B
inst✝⁷ : Algebra R B
inst✝⁶ : Star B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Star C
inst✝² : Semiring D
inst✝¹ : Algebra R D
inst✝ : Star D
f : A → B
map_one'✝¹ : f 1 = 1
map_mul'✝¹ :
  ∀ (x y : A),
    { 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 : A),
    (↑{ 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 : R),
    (↑↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹,
                map_add' := map_add'✝¹ }).toFun
        ((algebraMap R A) r) =
      (algebraMap R B) r
map_star'✝¹ :
  ∀ (x : A),
    (↑↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹,
                  commutes' := commutes'✝¹ }.toRingHom).toFun
        (star x) =
      star
        ((↑↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹,
                    map_add' := map_add'✝¹, commutes' := commutes'✝¹ }.toRingHom).toFun
          x)
g : A → B
map_one'✝ : g 1 = 1
map_mul'✝ :
  ∀ (x y : A),
    { 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 : A),
    (↑{ 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
commutes'✝ :
  ∀ (r : R),
    (↑↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝,
                map_add' := map_add'✝ }).toFun
        ((algebraMap R A) r) =
      (algebraMap R B) r
map_star'✝ :
  ∀ (x : A),
    (↑↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝,
                  commutes' := commutes'✝ }.toRingHom).toFun
        (star x) =
      star
        ((↑↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝,
                    commutes' := commutes'✝ }.toRingHom).toFun
          x)
h :
  (fun f ↦ (↑↑f.toRingHom).toFun)
      { toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹,
        commutes' := commutes'✝¹, map_star' := map_star'✝¹ } =
    (fun f ↦ (↑↑f.toRingHom).toFun)
      { toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝,
        commutes' := commutes'✝, map_star' := map_star'✝ }
⊢ { toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹,
      commutes' := commutes'✝¹, map_star' := map_star'✝¹ } =
    { toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝,
      commutes' := commutes'✝, map_star' := map_star'✝ }

Tactic:
;

Goal state after:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Star A
inst✝⁸ : Semiring B
inst✝⁷ : Algebra R B
inst✝⁶ : Star B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Star C
inst✝² : Semiring D
inst✝¹ : Algebra R D
inst✝ : Star D
f : A → B
map_one'✝¹ : f 1 = 1
map_mul'✝¹ :
  ∀ (x y : A),
    { 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 : A),
    (↑{ 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 : R),
    (↑↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹,
                map_add' := map_add'✝¹ }).toFun
        ((algebraMap R A) r) =
      (algebraMap R B) r
map_star'✝¹ :
  ∀ (x : A),
    (↑↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹,
                  commutes' := commutes'✝¹ }.toRingHom).toFun
        (star x) =
      star
        ((↑↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹,
                    map_add' := map_add'✝¹, commutes' := commutes'✝¹ }.toRingHom).toFun
          x)
g : A → B
map_one'✝ : g 1 = 1
map_mul'✝ :
  ∀ (x y : A),
    { 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 : A),
    (↑{ 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
commutes'✝ :
  ∀ (r : R),
    (↑↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝,
                map_add' := map_add'✝ }).toFun
        ((algebraMap R A) r) =
      (algebraMap R B) r
map_star'✝ :
  ∀ (x : A),
    (↑↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝,
                  commutes' := commutes'✝ }.toRingHom).toFun
        (star x) =
      star
        ((↑↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝,
                    commutes' := commutes'✝ }.toRingHom).toFun
          x)
h :
  (fun f ↦ (↑↑f.toRingHom).toFun)
      { toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹,
        commutes' := commutes'✝¹, map_star' := map_star'✝¹ } =
    (fun f ↦ (↑↑f.toRingHom).toFun)
      { toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝,
        commutes' := commutes'✝, map_star' := map_star'✝ }
⊢ { toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹,
      commutes' := commutes'✝¹, map_star' := map_star'✝¹ } =
    { toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝,
      commutes' := commutes'✝, map_star' := map_star'✝ }