Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: case mk.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'
toFun✝¹ : A → B
map_smul'✝¹ : ∀ (m : M) (x : A), toFun✝¹ (m • x) = φ m • toFun✝¹ x
map_one'✝¹ : { toFun := toFun✝¹, map_smul' := map_smul'✝¹ }.toFun 1 = 1
map_mul'✝¹ :
  ∀ (x y : A),
    { 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
toFun✝ : A → B
map_smul'✝ : ∀ (m : M) (x : A), toFun✝ (m • x) = φ m • toFun✝ x
map_one'✝ : { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : A),
    { 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
h :
  (fun m ↦ m.toFun) { toFun := toFun✝¹, map_smul' := map_smul'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun m ↦ m.toFun) { toFun := toFun✝, map_smul' := map_smul'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ { toFun := toFun✝¹, map_smul' := map_smul'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    { toFun := toFun✝, map_smul' := map_smul'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }

Tactic:
;

Goal state after:
case mk.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'
toFun✝¹ : A → B
map_smul'✝¹ : ∀ (m : M) (x : A), toFun✝¹ (m • x) = φ m • toFun✝¹ x
map_one'✝¹ : { toFun := toFun✝¹, map_smul' := map_smul'✝¹ }.toFun 1 = 1
map_mul'✝¹ :
  ∀ (x y : A),
    { 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
toFun✝ : A → B
map_smul'✝ : ∀ (m : M) (x : A), toFun✝ (m • x) = φ m • toFun✝ x
map_one'✝ : { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : A),
    { 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
h :
  (fun m ↦ m.toFun) { toFun := toFun✝¹, map_smul' := map_smul'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun m ↦ m.toFun) { toFun := toFun✝, map_smul' := map_smul'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ { toFun := toFun✝¹, map_smul' := map_smul'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    { toFun := toFun✝, map_smul' := map_smul'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }