Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
toNPow✝¹ : NPow M
npow_zero✝¹ : ∀ (x : M), x ^ 0 = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsRightCancelMul✝¹ : IsRightCancelMul M
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
toNPow✝ : NPow M
npow_zero✝ : ∀ (x : M), x ^ 0 = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsRightCancelMul✝ : IsRightCancelMul M
h :
  { toSemigroup := toSemigroup✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, toNPow := toNPow✝¹,
        npow_zero := npow_zero✝¹, npow_succ := npow_succ✝¹, toIsRightCancelMul := toIsRightCancelMul✝¹ }.toMonoid =
    { toSemigroup := toSemigroup✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝, toNPow := toNPow✝,
        npow_zero := npow_zero✝, npow_succ := npow_succ✝, toIsRightCancelMul := toIsRightCancelMul✝ }.toMonoid
⊢ { toSemigroup := toSemigroup✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, toNPow := toNPow✝¹,
      npow_zero := npow_zero✝¹, npow_succ := npow_succ✝¹, toIsRightCancelMul := toIsRightCancelMul✝¹ } =
    { toSemigroup := toSemigroup✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝, toNPow := toNPow✝,
      npow_zero := npow_zero✝, npow_succ := npow_succ✝, toIsRightCancelMul := toIsRightCancelMul✝ }

Tactic:
congr

Goal state after:
case e_toSemigroup
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
toNPow✝¹ : NPow M
npow_zero✝¹ : ∀ (x : M), x ^ 0 = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsRightCancelMul✝¹ : IsRightCancelMul M
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
toNPow✝ : NPow M
npow_zero✝ : ∀ (x : M), x ^ 0 = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsRightCancelMul✝ : IsRightCancelMul M
h :
  { toSemigroup := toSemigroup✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, toNPow := toNPow✝¹,
        npow_zero := npow_zero✝¹, npow_succ := npow_succ✝¹, toIsRightCancelMul := toIsRightCancelMul✝¹ }.toMonoid =
    { toSemigroup := toSemigroup✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝, toNPow := toNPow✝,
        npow_zero := npow_zero✝, npow_succ := npow_succ✝, toIsRightCancelMul := toIsRightCancelMul✝ }.toMonoid
⊢ toSemigroup✝¹ = toSemigroup✝

case e_toOne
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
toNPow✝¹ : NPow M
npow_zero✝¹ : ∀ (x : M), x ^ 0 = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsRightCancelMul✝¹ : IsRightCancelMul M
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
toNPow✝ : NPow M
npow_zero✝ : ∀ (x : M), x ^ 0 = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsRightCancelMul✝ : IsRightCancelMul M
h :
  { toSemigroup := toSemigroup✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, toNPow := toNPow✝¹,
        npow_zero := npow_zero✝¹, npow_succ := npow_succ✝¹, toIsRightCancelMul := toIsRightCancelMul✝¹ }.toMonoid =
    { toSemigroup := toSemigroup✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝, toNPow := toNPow✝,
        npow_zero := npow_zero✝, npow_succ := npow_succ✝, toIsRightCancelMul := toIsRightCancelMul✝ }.toMonoid
⊢ toOne✝¹ = toOne✝

case e_toNPow
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
toNPow✝¹ : NPow M
npow_zero✝¹ : ∀ (x : M), x ^ 0 = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsRightCancelMul✝¹ : IsRightCancelMul M
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
toNPow✝ : NPow M
npow_zero✝ : ∀ (x : M), x ^ 0 = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsRightCancelMul✝ : IsRightCancelMul M
h :
  { toSemigroup := toSemigroup✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, toNPow := toNPow✝¹,
        npow_zero := npow_zero✝¹, npow_succ := npow_succ✝¹, toIsRightCancelMul := toIsRightCancelMul✝¹ }.toMonoid =
    { toSemigroup := toSemigroup✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝, toNPow := toNPow✝,
        npow_zero := npow_zero✝, npow_succ := npow_succ✝, toIsRightCancelMul := toIsRightCancelMul✝ }.toMonoid
⊢ toNPow✝¹ = toNPow✝