[GOAL]
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
[PROOFSTEP]
rintro ⟨⟨⟨⟨f, _⟩, _⟩, _⟩, _⟩ ⟨⟨⟨⟨g, _⟩, _⟩, _⟩, _⟩ h
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk
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) = m • f x
map_zero'✝¹ : MulActionHom.toFun { toFun := f, map_smul' := map_smul'✝¹ } 0 = 0
map_add'✝¹ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := f, map_smul' := map_smul'✝¹ } (x + y) =
      MulActionHom.toFun { toFun := f, map_smul' := map_smul'✝¹ } x +
        MulActionHom.toFun { toFun := f, map_smul' := map_smul'✝¹ } y
map_mul'✝¹ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
            map_add' := map_add'✝¹ }.toMulActionHom
        (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
              map_add' := map_add'✝¹ }.toMulActionHom
          x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
              map_add' := map_add'✝¹ }.toMulActionHom
          y
map_star'✝¹ :
  ∀ (a : A),
    MulActionHom.toFun
        {
              toDistribMulActionHom :=
                { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
                  map_add' := map_add'✝¹ },
              map_mul' := map_mul'✝¹ }.toDistribMulActionHom.toMulActionHom
        (star a) =
      star
        (MulActionHom.toFun
          {
                toDistribMulActionHom :=
                  { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
                    map_add' := map_add'✝¹ },
                map_mul' := map_mul'✝¹ }.toDistribMulActionHom.toMulActionHom
          a)
g : A → B
map_smul'✝ : ∀ (m : R) (x : A), g (m • x) = m • g x
map_zero'✝ : MulActionHom.toFun { toFun := g, map_smul' := map_smul'✝ } 0 = 0
map_add'✝ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := g, map_smul' := map_smul'✝ } (x + y) =
      MulActionHom.toFun { toFun := g, map_smul' := map_smul'✝ } x +
        MulActionHom.toFun { toFun := g, map_smul' := map_smul'✝ } y
map_mul'✝ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
            map_add' := map_add'✝ }.toMulActionHom
        (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
              map_add' := map_add'✝ }.toMulActionHom
          x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
              map_add' := map_add'✝ }.toMulActionHom
          y
map_star'✝ :
  ∀ (a : A),
    MulActionHom.toFun
        {
              toDistribMulActionHom :=
                { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
                  map_add' := map_add'✝ },
              map_mul' := map_mul'✝ }.toDistribMulActionHom.toMulActionHom
        (star a) =
      star
        (MulActionHom.toFun
          {
                toDistribMulActionHom :=
                  { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
                    map_add' := map_add'✝ },
                map_mul' := map_mul'✝ }.toDistribMulActionHom.toMulActionHom
          a)
h :
  (fun f => f.toFun)
      {
        toNonUnitalAlgHom :=
          {
            toDistribMulActionHom :=
              { toMulActionHom := { 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)
      {
        toNonUnitalAlgHom :=
          {
            toDistribMulActionHom :=
              { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
                map_add' := map_add'✝ },
            map_mul' := map_mul'✝ },
        map_star' := map_star'✝ }
⊢ {
      toNonUnitalAlgHom :=
        {
          toDistribMulActionHom :=
            { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
              map_add' := map_add'✝¹ },
          map_mul' := map_mul'✝¹ },
      map_star' := map_star'✝¹ } =
    {
      toNonUnitalAlgHom :=
        {
          toDistribMulActionHom :=
            { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
              map_add' := map_add'✝ },
          map_mul' := map_mul'✝ },
      map_star' := map_star'✝ }
[PROOFSTEP]
congr
[GOAL]
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 →⋆ₙₐ[R] B
h₁ : ∀ (m : R) (x : A), ↑f (m • x) = m • ↑f x
h₂ : MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } 0 = 0
h₃ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } (x + y) =
      MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } y
h₄ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom y
h₅ :
  ∀ (a : A),
    MulActionHom.toFun
        {
              toDistribMulActionHom :=
                { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
              map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom
        (star a) =
      star
        (MulActionHom.toFun
          {
                toDistribMulActionHom :=
                  { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
                map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom
          a)
⊢ {
      toNonUnitalAlgHom :=
        {
          toDistribMulActionHom :=
            { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
          map_mul' := h₄ },
      map_star' := h₅ } =
    f
[PROOFSTEP]
ext
[GOAL]
case h
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 →⋆ₙₐ[R] B
h₁ : ∀ (m : R) (x : A), ↑f (m • x) = m • ↑f x
h₂ : MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } 0 = 0
h₃ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } (x + y) =
      MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } y
h₄ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom y
h₅ :
  ∀ (a : A),
    MulActionHom.toFun
        {
              toDistribMulActionHom :=
                { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
              map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom
        (star a) =
      star
        (MulActionHom.toFun
          {
                toDistribMulActionHom :=
                  { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
                map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom
          a)
x✝ : A
⊢ ↑{
          toNonUnitalAlgHom :=
            {
              toDistribMulActionHom :=
                { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
              map_mul' := h₄ },
          map_star' := h₅ }
      x✝ =
    ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
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 : B →⋆ₙₐ[R] C
g : A →⋆ₙₐ[R] B
src✝ : A →ₙₐ[R] C := NonUnitalAlgHom.comp f.toNonUnitalAlgHom g.toNonUnitalAlgHom
⊢ ∀ (a : A),
    MulActionHom.toFun
        { toDistribMulActionHom := src✝.toDistribMulActionHom,
              map_mul' :=
                (_ :
                  ∀ (x y : A),
                    MulActionHom.toFun src✝.toMulActionHom (x * y) =
                      MulActionHom.toFun src✝.toMulActionHom x *
                        MulActionHom.toFun src✝.toMulActionHom y) }.toDistribMulActionHom.toMulActionHom
        (star a) =
      star
        (MulActionHom.toFun
          { toDistribMulActionHom := src✝.toDistribMulActionHom,
                map_mul' :=
                  (_ :
                    ∀ (x y : A),
                      MulActionHom.toFun src✝.toMulActionHom (x * y) =
                        MulActionHom.toFun src✝.toMulActionHom x *
                          MulActionHom.toFun src✝.toMulActionHom y) }.toDistribMulActionHom.toMulActionHom
          a)
[PROOFSTEP]
simp only [map_star, NonUnitalAlgHom.toFun_eq_coe, eq_self_iff_true, NonUnitalAlgHom.coe_comp, coe_toNonUnitalAlgHom,
  Function.comp_apply, forall_const]
[GOAL]
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✝³ : StarAddMonoid A
inst✝² : NonUnitalNonAssocSemiring B
inst✝¹ : DistribMulAction R B
inst✝ : StarAddMonoid B
src✝ : A →ₙₐ[R] B := 0
⊢ ∀ (a : A),
    MulActionHom.toFun
        { toDistribMulActionHom := src✝.toDistribMulActionHom,
              map_mul' :=
                (_ :
                  ∀ (x y : A),
                    MulActionHom.toFun src✝.toMulActionHom (x * y) =
                      MulActionHom.toFun src✝.toMulActionHom x *
                        MulActionHom.toFun src✝.toMulActionHom y) }.toDistribMulActionHom.toMulActionHom
        (star a) =
      star
        (MulActionHom.toFun
          { toDistribMulActionHom := src✝.toDistribMulActionHom,
                map_mul' :=
                  (_ :
                    ∀ (x y : A),
                      MulActionHom.toFun src✝.toMulActionHom (x * y) =
                        MulActionHom.toFun src✝.toMulActionHom x *
                          MulActionHom.toFun src✝.toMulActionHom y) }.toDistribMulActionHom.toMulActionHom
          a)
[PROOFSTEP]
simp
[GOAL]
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
⊢ Function.Injective fun f => f.toFun
[PROOFSTEP]
rintro ⟨⟨⟨⟨⟨f, _⟩, _⟩, _⟩, _⟩, _⟩ ⟨⟨⟨⟨⟨g, _⟩, _⟩, _⟩, _⟩, _⟩ h
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk.mk.mk
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),
    OneHom.toFun { toFun := f, map_one' := map_one'✝¹ } (x * y) =
      OneHom.toFun { toFun := f, map_one' := map_one'✝¹ } x * OneHom.toFun { toFun := f, map_one' := map_one'✝¹ } y
map_zero'✝¹ : OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) 0 = 0
map_add'✝¹ :
  ∀ (x y : A),
    OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) y
commutes'✝¹ :
  ∀ (r : R),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
              map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ })
        (↑(algebraMap R A) r) =
      ↑(algebraMap R B) r
map_star'✝¹ :
  ∀ (x : A),
    OneHom.toFun
        (↑↑↑{
                toRingHom :=
                  { toMonoidHom := { toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
                    map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
                commutes' := commutes'✝¹ })
        (star x) =
      star
        (OneHom.toFun
          (↑↑↑{
                  toRingHom :=
                    { toMonoidHom := { toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
                      map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
                  commutes' := commutes'✝¹ })
          x)
g : A → B
map_one'✝ : g 1 = 1
map_mul'✝ :
  ∀ (x y : A),
    OneHom.toFun { toFun := g, map_one' := map_one'✝ } (x * y) =
      OneHom.toFun { toFun := g, map_one' := map_one'✝ } x * OneHom.toFun { toFun := g, map_one' := map_one'✝ } y
map_zero'✝ : OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) 0 = 0
map_add'✝ :
  ∀ (x y : A),
    OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) y
commutes'✝ :
  ∀ (r : R),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
              map_zero' := map_zero'✝, map_add' := map_add'✝ })
        (↑(algebraMap R A) r) =
      ↑(algebraMap R B) r
map_star'✝ :
  ∀ (x : A),
    OneHom.toFun
        (↑↑↑{
                toRingHom :=
                  { toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
                    map_zero' := map_zero'✝, map_add' := map_add'✝ },
                commutes' := commutes'✝ })
        (star x) =
      star
        (OneHom.toFun
          (↑↑↑{
                  toRingHom :=
                    { toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
                      map_zero' := map_zero'✝, map_add' := map_add'✝ },
                  commutes' := commutes'✝ })
          x)
h :
  (fun f => f.toFun)
      {
        toAlgHom :=
          {
            toRingHom :=
              { toMonoidHom := { toOneHom := { 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.toFun)
      {
        toAlgHom :=
          {
            toRingHom :=
              { toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
                map_zero' := map_zero'✝, map_add' := map_add'✝ },
            commutes' := commutes'✝ },
        map_star' := map_star'✝ }
⊢ {
      toAlgHom :=
        {
          toRingHom :=
            { toMonoidHom := { toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
              map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
          commutes' := commutes'✝¹ },
      map_star' := map_star'✝¹ } =
    {
      toAlgHom :=
        {
          toRingHom :=
            { toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
              map_zero' := map_zero'✝, map_add' := map_add'✝ },
          commutes' := commutes'✝ },
      map_star' := map_star'✝ }
[PROOFSTEP]
congr
[GOAL]
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 →⋆ₐ[R] B
h₁ : ↑f 1 = 1
h₂ :
  ∀ (x y : A),
    OneHom.toFun { toFun := ↑f, map_one' := h₁ } (x * y) =
      OneHom.toFun { toFun := ↑f, map_one' := h₁ } x * OneHom.toFun { toFun := ↑f, map_one' := h₁ } y
h₃ : OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0
h₄ :
  ∀ (x y : A),
    OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) y
h₅ :
  ∀ (r : R),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
              map_add' := h₄ })
        (↑(algebraMap R A) r) =
      ↑(algebraMap R B) r
h₆ :
  ∀ (x : A),
    OneHom.toFun
        (↑↑↑{
                toRingHom :=
                  { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                    map_add' := h₄ },
                commutes' := h₅ })
        (star x) =
      star
        (OneHom.toFun
          (↑↑↑{
                  toRingHom :=
                    { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                      map_add' := h₄ },
                  commutes' := h₅ })
          x)
⊢ {
      toAlgHom :=
        {
          toRingHom :=
            { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
              map_add' := h₄ },
          commutes' := h₅ },
      map_star' := h₆ } =
    f
[PROOFSTEP]
ext
[GOAL]
case h
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 →⋆ₐ[R] B
h₁ : ↑f 1 = 1
h₂ :
  ∀ (x y : A),
    OneHom.toFun { toFun := ↑f, map_one' := h₁ } (x * y) =
      OneHom.toFun { toFun := ↑f, map_one' := h₁ } x * OneHom.toFun { toFun := ↑f, map_one' := h₁ } y
h₃ : OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0
h₄ :
  ∀ (x y : A),
    OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) y
h₅ :
  ∀ (r : R),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
              map_add' := h₄ })
        (↑(algebraMap R A) r) =
      ↑(algebraMap R B) r
h₆ :
  ∀ (x : A),
    OneHom.toFun
        (↑↑↑{
                toRingHom :=
                  { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                    map_add' := h₄ },
                commutes' := h₅ })
        (star x) =
      star
        (OneHom.toFun
          (↑↑↑{
                  toRingHom :=
                    { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                      map_add' := h₄ },
                  commutes' := h₅ })
          x)
x✝ : A
⊢ ↑{
          toAlgHom :=
            {
              toRingHom :=
                { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                  map_add' := h₄ },
              commutes' := h₅ },
          map_star' := h₆ }
      x✝ =
    ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
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 : B →⋆ₐ[R] C
g : A →⋆ₐ[R] B
src✝ : A →ₐ[R] C := AlgHom.comp f.toAlgHom g.toAlgHom
⊢ ∀ (x : A),
    OneHom.toFun
        (↑↑↑{ toRingHom := ↑src✝,
                commutes' := (_ : ∀ (r : R), OneHom.toFun (↑↑↑src✝) (↑(algebraMap R A) r) = ↑(algebraMap R C) r) })
        (star x) =
      star
        (OneHom.toFun
          (↑↑↑{ toRingHom := ↑src✝,
                  commutes' := (_ : ∀ (r : R), OneHom.toFun (↑↑↑src✝) (↑(algebraMap R A) r) = ↑(algebraMap R C) r) })
          x)
[PROOFSTEP]
simp only [map_star, AlgHom.toFun_eq_coe, AlgHom.coe_comp, coe_toAlgHom, Function.comp_apply, eq_self_iff_true,
  forall_const]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
src✝ : A →ₙₐ[R] B × C := NonUnitalAlgHom.prod f.toNonUnitalAlgHom g.toNonUnitalAlgHom
x : A
⊢ MulActionHom.toFun
      { toDistribMulActionHom := src✝.toDistribMulActionHom,
            map_mul' :=
              (_ :
                ∀ (x y : A),
                  MulActionHom.toFun src✝.toMulActionHom (x * y) =
                    MulActionHom.toFun src✝.toMulActionHom x *
                      MulActionHom.toFun src✝.toMulActionHom y) }.toDistribMulActionHom.toMulActionHom
      (star x) =
    star
      (MulActionHom.toFun
        { toDistribMulActionHom := src✝.toDistribMulActionHom,
              map_mul' :=
                (_ :
                  ∀ (x y : A),
                    MulActionHom.toFun src✝.toMulActionHom (x * y) =
                      MulActionHom.toFun src✝.toMulActionHom x *
                        MulActionHom.toFun src✝.toMulActionHom y) }.toDistribMulActionHom.toMulActionHom
        x)
[PROOFSTEP]
simp [map_star, Prod.star_def]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
⊢ comp (fst R B C) (prod f g) = f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x✝ : A
⊢ ↑(comp (fst R B C) (prod f g)) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
⊢ comp (snd R B C) (prod f g) = g
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x✝ : A
⊢ ↑(comp (snd R B C) (prod f g)) x✝ = ↑g x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : (A →⋆ₙₐ[R] B) × (A →⋆ₙₐ[R] C)
⊢ (fun f => (comp (fst R B C) f, comp (snd R B C) f)) ((fun f => prod f.fst f.snd) f) = f
[PROOFSTEP]
ext
[GOAL]
case h₁.h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : (A →⋆ₙₐ[R] B) × (A →⋆ₙₐ[R] C)
x✝ : A
⊢ ↑((fun f => (comp (fst R B C) f, comp (snd R B C) f)) ((fun f => prod f.fst f.snd) f)).fst x✝ = ↑f.fst x✝
[PROOFSTEP]
rfl
[GOAL]
case h₂.h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : (A →⋆ₙₐ[R] B) × (A →⋆ₙₐ[R] C)
x✝ : A
⊢ ↑((fun f => (comp (fst R B C) f, comp (snd R B C) f)) ((fun f => prod f.fst f.snd) f)).snd x✝ = ↑f.snd x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₙₐ[R] B × C
⊢ (fun f => prod f.fst f.snd) ((fun f => (comp (fst R B C) f, comp (snd R B C) f)) f) = f
[PROOFSTEP]
ext
[GOAL]
case h.h₁
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₙₐ[R] B × C
x✝ : A
⊢ (↑((fun f => prod f.fst f.snd) ((fun f => (comp (fst R B C) f, comp (snd R B C) f)) f)) x✝).fst = (↑f x✝).fst
[PROOFSTEP]
rfl
[GOAL]
case h.h₂
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₙₐ[R] B × C
x✝ : A
⊢ (↑((fun f => prod f.fst f.snd) ((fun f => (comp (fst R B C) f, comp (snd R B C) f)) f)) x✝).snd = (↑f x✝).snd
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
src✝ : A →ₐ[R] B × C := AlgHom.prod f.toAlgHom g.toAlgHom
x : A
⊢ OneHom.toFun
      (↑↑↑{ toRingHom := ↑src✝,
              commutes' := (_ : ∀ (r : R), OneHom.toFun (↑↑↑src✝) (↑(algebraMap R A) r) = ↑(algebraMap R (B × C)) r) })
      (star x) =
    star
      (OneHom.toFun
        (↑↑↑{ toRingHom := ↑src✝,
                commutes' :=
                  (_ : ∀ (r : R), OneHom.toFun (↑↑↑src✝) (↑(algebraMap R A) r) = ↑(algebraMap R (B × C)) r) })
        x)
[PROOFSTEP]
simp [Prod.star_def, map_star]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
⊢ comp (fst R B C) (prod f g) = f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x✝ : A
⊢ ↑(comp (fst R B C) (prod f g)) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
⊢ comp (snd R B C) (prod f g) = g
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x✝ : A
⊢ ↑(comp (snd R B C) (prod f g)) x✝ = ↑g x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : (A →⋆ₐ[R] B) × (A →⋆ₐ[R] C)
⊢ (fun f => (comp (fst R B C) f, comp (snd R B C) f)) ((fun f => prod f.fst f.snd) f) = f
[PROOFSTEP]
ext
[GOAL]
case h₁.h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : (A →⋆ₐ[R] B) × (A →⋆ₐ[R] C)
x✝ : A
⊢ ↑((fun f => (comp (fst R B C) f, comp (snd R B C) f)) ((fun f => prod f.fst f.snd) f)).fst x✝ = ↑f.fst x✝
[PROOFSTEP]
rfl
[GOAL]
case h₂.h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : (A →⋆ₐ[R] B) × (A →⋆ₐ[R] C)
x✝ : A
⊢ ↑((fun f => (comp (fst R B C) f, comp (snd R B C) f)) ((fun f => prod f.fst f.snd) f)).snd x✝ = ↑f.snd x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₐ[R] B × C
⊢ (fun f => prod f.fst f.snd) ((fun f => (comp (fst R B C) f, comp (snd R B C) f)) f) = f
[PROOFSTEP]
ext
[GOAL]
case h.h₁
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₐ[R] B × C
x✝ : A
⊢ (↑((fun f => prod f.fst f.snd) ((fun f => (comp (fst R B C) f, comp (snd R B C) f)) f)) x✝).fst = (↑f x✝).fst
[PROOFSTEP]
rfl
[GOAL]
case h.h₂
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₐ[R] B × C
x✝ : A
⊢ (↑((fun f => prod f.fst f.snd) ((fun f => (comp (fst R B C) f, comp (snd R B C) f)) f)) x✝).snd = (↑f x✝).snd
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Star A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Star B
hF : StarAlgEquivClass F R A B
f : F
r : R
⊢ ↑f (↑(algebraMap R A) r) = ↑(algebraMap R B) r
[PROOFSTEP]
simp only [Algebra.algebraMap_eq_smul_one, map_smul, map_one]
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
f g : A ≃⋆ₐ[R] B
h₁ : (fun f => f.toFun) f = (fun f => f.toFun) g
h₂ : (fun f => f.invFun) f = (fun f => f.invFun) g
⊢ f = g
[PROOFSTEP]
rcases f with ⟨⟨⟨_, _, _⟩, _⟩, _⟩
[GOAL]
case mk.mk.mk
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
g : A ≃⋆ₐ[R] B
toFun✝ : A → B
invFun✝ : B → A
left_inv✝ : Function.LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
map_mul'✝ :
  ∀ (x y : A),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : A),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_star'✝ :
  ∀ (a : A),
    Equiv.toFun
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
        (star a) =
      star
        (Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          a)
map_smul'✝ :
  ∀ (r : R) (a : A),
    Equiv.toFun
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
        (r • a) =
      r •
        Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          a
h₁ :
  (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        map_star' := map_star'✝, map_smul' := map_smul'✝ } =
    (fun f => f.toFun) g
h₂ :
  (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        map_star' := map_star'✝, map_smul' := map_smul'✝ } =
    (fun f => f.invFun) g
⊢ {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
          map_mul' := map_mul'✝, map_add' := map_add'✝ },
      map_star' := map_star'✝, map_smul' := map_smul'✝ } =
    g
[PROOFSTEP]
rcases g with ⟨⟨⟨_, _, _⟩, _⟩, _⟩
[GOAL]
case mk.mk.mk.mk.mk.mk
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
toFun✝¹ : A → B
invFun✝¹ : B → A
left_inv✝¹ : Function.LeftInverse invFun✝¹ toFun✝¹
right_inv✝¹ : Function.RightInverse invFun✝¹ toFun✝¹
map_mul'✝¹ :
  ∀ (x y : A),
    Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x * y) =
      Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x *
        Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
map_add'✝¹ :
  ∀ (x y : A),
    Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x + y) =
      Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x +
        Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
map_star'✝¹ :
  ∀ (a : A),
    Equiv.toFun
        { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
            map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
        (star a) =
      star
        (Equiv.toFun
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
              map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
          a)
map_smul'✝¹ :
  ∀ (r : R) (a : A),
    Equiv.toFun
        { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
            map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
        (r • a) =
      r •
        Equiv.toFun
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
              map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
          a
toFun✝ : A → B
invFun✝ : B → A
left_inv✝ : Function.LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
map_mul'✝ :
  ∀ (x y : A),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : A),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_star'✝ :
  ∀ (a : A),
    Equiv.toFun
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
        (star a) =
      star
        (Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          a)
map_smul'✝ :
  ∀ (r : R) (a : A),
    Equiv.toFun
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
        (r • a) =
      r •
        Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          a
h₁ :
  (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
            map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
        map_star' := map_star'✝¹, map_smul' := map_smul'✝¹ } =
    (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        map_star' := map_star'✝, map_smul' := map_smul'✝ }
h₂ :
  (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
            map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
        map_star' := map_star'✝¹, map_smul' := map_smul'✝¹ } =
    (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        map_star' := map_star'✝, map_smul' := map_smul'✝ }
⊢ {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
          map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
      map_star' := map_star'✝¹, map_smul' := map_smul'✝¹ } =
    {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
          map_mul' := map_mul'✝, map_add' := map_add'✝ },
      map_star' := map_star'✝, map_smul' := map_smul'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e : A ≃⋆ₐ[R] B
src✝ : B ≃+* A := RingEquiv.symm e.toRingEquiv
b : B
⊢ Equiv.toFun
      { toEquiv := src✝.toEquiv,
          map_mul' :=
            (_ :
              ∀ (x y : B), Equiv.toFun src✝.toEquiv (x * y) = Equiv.toFun src✝.toEquiv x * Equiv.toFun src✝.toEquiv y),
          map_add' :=
            (_ :
              ∀ (x y : B),
                Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }.toEquiv
      (star b) =
    star
      (Equiv.toFun
        { toEquiv := src✝.toEquiv,
            map_mul' :=
              (_ :
                ∀ (x y : B),
                  Equiv.toFun src✝.toEquiv (x * y) = Equiv.toFun src✝.toEquiv x * Equiv.toFun src✝.toEquiv y),
            map_add' :=
              (_ :
                ∀ (x y : B),
                  Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }.toEquiv
        b)
[PROOFSTEP]
simpa only [apply_inv_apply, inv_apply_apply] using congr_arg (inv e) (map_star e (inv e b)).symm
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e : A ≃⋆ₐ[R] B
src✝ : B ≃+* A := RingEquiv.symm e.toRingEquiv
r : R
b : B
⊢ Equiv.toFun
      { toEquiv := src✝.toEquiv,
          map_mul' :=
            (_ :
              ∀ (x y : B), Equiv.toFun src✝.toEquiv (x * y) = Equiv.toFun src✝.toEquiv x * Equiv.toFun src✝.toEquiv y),
          map_add' :=
            (_ :
              ∀ (x y : B),
                Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }.toEquiv
      (r • b) =
    r •
      Equiv.toFun
        { toEquiv := src✝.toEquiv,
            map_mul' :=
              (_ :
                ∀ (x y : B),
                  Equiv.toFun src✝.toEquiv (x * y) = Equiv.toFun src✝.toEquiv x * Equiv.toFun src✝.toEquiv y),
            map_add' :=
              (_ :
                ∀ (x y : B),
                  Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }.toEquiv
        b
[PROOFSTEP]
simpa only [apply_inv_apply, inv_apply_apply] using congr_arg (inv e) (map_smul e r (inv e b)).symm
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e : A ≃⋆ₐ[R] B
⊢ symm (symm e) = e
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e : A ≃⋆ₐ[R] B
a✝ : A
⊢ ↑(symm (symm e)) a✝ = ↑e a✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e₁ : A ≃⋆ₐ[R] B
e₂ : B ≃⋆ₐ[R] C
src✝ : A ≃+* C := RingEquiv.trans e₁.toRingEquiv e₂.toRingEquiv
a : A
⊢ Equiv.toFun e₂.toEquiv (Equiv.toFun e₁.toEquiv (star a)) = star (Equiv.toFun e₂.toEquiv (Equiv.toFun e₁.toEquiv a))
[PROOFSTEP]
rw [e₁.map_star', e₂.map_star']
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e₁ : A ≃⋆ₐ[R] B
e₂ : B ≃⋆ₐ[R] C
src✝ : A ≃+* C := RingEquiv.trans e₁.toRingEquiv e₂.toRingEquiv
r : R
a : A
⊢ Equiv.toFun e₂.toEquiv (Equiv.toFun e₁.toEquiv (r • a)) = r • Equiv.toFun e₂.toEquiv (Equiv.toFun e₁.toEquiv a)
[PROOFSTEP]
rw [e₁.map_smul', e₂.map_smul']
