Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: case mk
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
tG : R →ₑ[⇑φ] S
map_zero'✝¹ : tG.toFun 0 = 0
map_add'✝¹ : ∀ (x y : R), tG.toFun (x + y) = tG.toFun x + tG.toFun y
map_one'✝¹ : { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun 1 = 1
map_mul'✝¹ :
  ∀ (x y : R),
    { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun (x * y) =
      { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun x *
        { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun y
toFun✝ : R → S
map_smul'✝ : ∀ (m : M) (x : R), toFun✝ (m • x) = φ m • toFun✝ x
map_zero'✝ : { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun 0 = 0
map_add'✝ :
  ∀ (x y : R),
    { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun (x + y) =
      { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun x + { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun y
map_one'✝ : { toFun := toFun✝, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : R),
    { toFun := toFun✝, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun x *
        { toFun := toFun✝, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun y
h :
  (fun m ↦ m.toFun)
      { toFun := toFun✝, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝, map_one' := map_one'✝,
        map_mul' := map_mul'✝ } =
    (fun m ↦ m.toFun)
      { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹, map_one' := map_one'✝¹,
        map_mul' := map_mul'✝¹ }
⊢ { toFun := toFun✝, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝, map_one' := map_one'✝,
      map_mul' := map_mul'✝ } =
    { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹, map_one' := map_one'✝¹,
      map_mul' := map_mul'✝¹ }

Tactic:
;

Goal state after:
case mk
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
tG : R →ₑ[⇑φ] S
map_zero'✝¹ : tG.toFun 0 = 0
map_add'✝¹ : ∀ (x y : R), tG.toFun (x + y) = tG.toFun x + tG.toFun y
map_one'✝¹ : { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun 1 = 1
map_mul'✝¹ :
  ∀ (x y : R),
    { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun (x * y) =
      { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun x *
        { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun y
toFun✝ : R → S
map_smul'✝ : ∀ (m : M) (x : R), toFun✝ (m • x) = φ m • toFun✝ x
map_zero'✝ : { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun 0 = 0
map_add'✝ :
  ∀ (x y : R),
    { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun (x + y) =
      { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun x + { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun y
map_one'✝ : { toFun := toFun✝, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : R),
    { toFun := toFun✝, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun x *
        { toFun := toFun✝, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun y
h :
  (fun m ↦ m.toFun)
      { toFun := toFun✝, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝, map_one' := map_one'✝,
        map_mul' := map_mul'✝ } =
    (fun m ↦ m.toFun)
      { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹, map_one' := map_one'✝¹,
        map_mul' := map_mul'✝¹ }
⊢ { toFun := toFun✝, map_smul' := map_smul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝, map_one' := map_one'✝,
      map_mul' := map_mul'✝ } =
    { toMulActionHom := tG, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹, map_one' := map_one'✝¹,
      map_mul' := map_mul'✝¹ }