Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : Monoid R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : DistribMulAction R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : DistribMulAction R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : DistribMulAction R C
inst✝³ : Star C
inst✝² : NonUnitalNonAssocSemiring D
inst✝¹ : DistribMulAction R D
inst✝ : Star D
⊢ Function.Injective fun f ↦ f.toFun

Tactic:
rintro ⟨⟨⟨⟨f, _⟩, _⟩, _⟩, _⟩ ⟨⟨⟨⟨g, _⟩, _⟩, _⟩, _⟩ h

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