Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝²⁴ : Monoid M
N : Type u_2
inst✝²³ : Monoid N
P : Type u_3
inst✝²² : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst✝²¹ : Monoid A
inst✝²⁰ : MulDistribMulAction M A
B : Type u_5
inst✝¹⁹ : Monoid B
inst✝¹⁸ : MulDistribMulAction N B
B₁ : Type u_6
inst✝¹⁷ : Monoid B₁
inst✝¹⁶ : MulDistribMulAction M B₁
C : Type u_7
inst✝¹⁵ : Monoid C
inst✝¹⁴ : MulDistribMulAction P C
A' : Type u_8
inst✝¹³ : Group A'
inst✝¹² : MulDistribMulAction M A'
B' : Type u_9
inst✝¹¹ : Group B'
inst✝¹⁰ : MulDistribMulAction N B'
R : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_11
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_12
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction N S
S' : Type u_13
inst✝³ : Ring S'
inst✝² : MulSemiringAction N S'
T : Type u_14
inst✝¹ : Semiring T
inst✝ : MulSemiringAction P T
g : R →ₑ+*[φ] S
tF : R →ₑ[⇑φ] S
map_zero'✝ : tF.toFun 0 = 0
map_add'✝ : ∀ (x y : R), tF.toFun (x + y) = tF.toFun x + tF.toFun y
map_one'✝ : { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : R),
    { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun (x * y) =
      { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun x *
        { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun y
h :
  (fun m ↦ m.toFun)
      { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝, map_one' := map_one'✝,
        map_mul' := map_mul'✝ } =
    (fun m ↦ m.toFun) g
⊢ { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝, map_one' := map_one'✝,
      map_mul' := map_mul'✝ } =
    g

Tactic:
;

Goal state after:
M : Type u_1
inst✝²⁴ : Monoid M
N : Type u_2
inst✝²³ : Monoid N
P : Type u_3
inst✝²² : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst✝²¹ : Monoid A
inst✝²⁰ : MulDistribMulAction M A
B : Type u_5
inst✝¹⁹ : Monoid B
inst✝¹⁸ : MulDistribMulAction N B
B₁ : Type u_6
inst✝¹⁷ : Monoid B₁
inst✝¹⁶ : MulDistribMulAction M B₁
C : Type u_7
inst✝¹⁵ : Monoid C
inst✝¹⁴ : MulDistribMulAction P C
A' : Type u_8
inst✝¹³ : Group A'
inst✝¹² : MulDistribMulAction M A'
B' : Type u_9
inst✝¹¹ : Group B'
inst✝¹⁰ : MulDistribMulAction N B'
R : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_11
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_12
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction N S
S' : Type u_13
inst✝³ : Ring S'
inst✝² : MulSemiringAction N S'
T : Type u_14
inst✝¹ : Semiring T
inst✝ : MulSemiringAction P T
g : R →ₑ+*[φ] S
tF : R →ₑ[⇑φ] S
map_zero'✝ : tF.toFun 0 = 0
map_add'✝ : ∀ (x y : R), tF.toFun (x + y) = tF.toFun x + tF.toFun y
map_one'✝ : { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : R),
    { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun (x * y) =
      { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun x *
        { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun y
h :
  (fun m ↦ m.toFun)
      { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝, map_one' := map_one'✝,
        map_mul' := map_mul'✝ } =
    (fun m ↦ m.toFun) g
⊢ { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝, map_one' := map_one'✝,
      map_mul' := map_mul'✝ } =
    g