Module: Mathlib.RingTheory.RingInvo

Goal state before:
pp: case mk.mk
F : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : EquivLike F R Rᵐᵒᵖ
toFun✝¹ : R → Rᵐᵒᵖ
invFun✝¹ : Rᵐᵒᵖ → R
left_inv✝¹ : Function.LeftInverse invFun✝¹ toFun✝¹
right_inv✝¹ : Function.RightInverse invFun✝¹ toFun✝¹
map_mul'✝¹ :
  ∀ (x y : R),
    { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun (x * y) =
      { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun x *
        { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun y
map_add'✝¹ :
  ∀ (x y : R),
    { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun (x + y) =
      { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun x +
        { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun y
involution'✝¹ :
  ∀ (x : R),
    MulOpposite.unop
        ({ toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹,
              map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toFun
          (MulOpposite.unop
            ({ toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹,
                  map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toFun
              x))) =
      x
toFun✝ : R → Rᵐᵒᵖ
invFun✝ : Rᵐᵒᵖ → R
left_inv✝ : Function.LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
map_mul'✝ :
  ∀ (x y : R),
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun (x * y) =
      { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun x *
        { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun y
map_add'✝ :
  ∀ (x y : R),
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun (x + y) =
      { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun x +
        { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun y
involution'✝ :
  ∀ (x : R),
    MulOpposite.unop
        ({ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
              map_add' := map_add'✝ }.toFun
          (MulOpposite.unop
            ({ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝,
                  map_mul' := map_mul'✝, map_add' := map_add'✝ }.toFun
              x))) =
      x
h₁ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹, map_mul' := map_mul'✝¹,
        map_add' := map_add'✝¹, involution' := involution'✝¹ }.toFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_add' := map_add'✝, involution' := involution'✝ }.toFun
h₂ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹, map_mul' := map_mul'✝¹,
        map_add' := map_add'✝¹, involution' := involution'✝¹ }.invFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_add' := map_add'✝, involution' := involution'✝ }.invFun
⊢ { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹, map_mul' := map_mul'✝¹,
      map_add' := map_add'✝¹, involution' := involution'✝¹ } =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
      map_add' := map_add'✝, involution' := involution'✝ }

Tactic:
congr

Goal state after: