Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case zero.zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
⊢ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun (0 * 0) =
    { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun 0 *
      { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun 0

pp: case zero.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
a✝ : α
⊢ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun (0 * ↑a✝) =
    { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun 0 *
      { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun ↑a✝

pp: case coe.zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
a✝ : α
⊢ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun (↑a✝ * 0) =
    { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun ↑a✝ *
      { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun 0

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
a✝¹ a✝ : α
⊢ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun (↑a✝¹ * ↑a✝) =
    { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun ↑a✝¹ *
      { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun ↑a✝

Tactic:
<;>

Goal state after:
case zero.zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
⊢ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun (0 * 0) =
    { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun 0 *
      { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun 0

case zero.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
a✝ : α
⊢ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun (0 * ↑a✝) =
    { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun 0 *
      { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun ↑a✝

case coe.zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
a✝ : α
⊢ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun (↑a✝ * 0) =
    { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun ↑a✝ *
      { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun 0

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
a✝¹ a✝ : α
⊢ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun (↑a✝¹ * ↑a✝) =
    { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun ↑a✝¹ *
      { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun ↑a✝