Module: Mathlib.Algebra.Star.StarRingHom

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Star B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Star C
inst✝¹ : NonUnitalNonAssocSemiring D
inst✝ : Star D
f : A → B
map_mul'✝¹ : ∀ (x y : A), f (x * y) = f x * f y
map_zero'✝¹ : { toFun := f, map_mul' := map_mul'✝¹ }.toFun 0 = 0
map_add'✝¹ :
  ∀ (x y : A),
    { toFun := f, map_mul' := map_mul'✝¹ }.toFun (x + y) =
      { toFun := f, map_mul' := map_mul'✝¹ }.toFun x + { toFun := f, map_mul' := map_mul'✝¹ }.toFun y
map_star'✝¹ :
  ∀ (a : A),
    { toFun := f, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun (star a) =
      star ({ toFun := f, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun a)
g : A → B
map_mul'✝ : ∀ (x y : A), g (x * y) = g x * g y
map_zero'✝ : { toFun := g, map_mul' := map_mul'✝ }.toFun 0 = 0
map_add'✝ :
  ∀ (x y : A),
    { toFun := g, map_mul' := map_mul'✝ }.toFun (x + y) =
      { toFun := g, map_mul' := map_mul'✝ }.toFun x + { toFun := g, map_mul' := map_mul'✝ }.toFun y
map_star'✝ :
  ∀ (a : A),
    { toFun := g, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun (star a) =
      star ({ toFun := g, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun a)
h :
  (fun f ↦ f.toFun)
      { toFun := f, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹,
        map_star' := map_star'✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := g, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝, map_star' := map_star'✝ }
⊢ { toFun := f, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹, map_star' := map_star'✝¹ } =
    { toFun := g, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝, map_star' := map_star'✝ }

Tactic:
;

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Star B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Star C
inst✝¹ : NonUnitalNonAssocSemiring D
inst✝ : Star D
f : A → B
map_mul'✝¹ : ∀ (x y : A), f (x * y) = f x * f y
map_zero'✝¹ : { toFun := f, map_mul' := map_mul'✝¹ }.toFun 0 = 0
map_add'✝¹ :
  ∀ (x y : A),
    { toFun := f, map_mul' := map_mul'✝¹ }.toFun (x + y) =
      { toFun := f, map_mul' := map_mul'✝¹ }.toFun x + { toFun := f, map_mul' := map_mul'✝¹ }.toFun y
map_star'✝¹ :
  ∀ (a : A),
    { toFun := f, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun (star a) =
      star ({ toFun := f, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun a)
g : A → B
map_mul'✝ : ∀ (x y : A), g (x * y) = g x * g y
map_zero'✝ : { toFun := g, map_mul' := map_mul'✝ }.toFun 0 = 0
map_add'✝ :
  ∀ (x y : A),
    { toFun := g, map_mul' := map_mul'✝ }.toFun (x + y) =
      { toFun := g, map_mul' := map_mul'✝ }.toFun x + { toFun := g, map_mul' := map_mul'✝ }.toFun y
map_star'✝ :
  ∀ (a : A),
    { toFun := g, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun (star a) =
      star ({ toFun := g, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun a)
h :
  (fun f ↦ f.toFun)
      { toFun := f, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹,
        map_star' := map_star'✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := g, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝, map_star' := map_star'✝ }
⊢ { toFun := f, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹, map_star' := map_star'✝¹ } =
    { toFun := g, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝, map_star' := map_star'✝ }