-- Module: Mathlib.RingTheory.RingInvo
Goal:
F : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : EquivLike F R Rᵐᵒᵖ
tF : R ≃ Rᵐᵒᵖ
map_mul' : ∀ (x y : R), tF.toFun (x * y) = tF.toFun x * tF.toFun y
map_add' : ∀ (x y : R), tF.toFun (x + y) = tF.toFun x + tF.toFun y
involution' :
  ∀ (x : R),
    MulOpposite.unop
        ({ toEquiv := tF, map_mul' := map_mul', map_add' := map_add' : R ≃+* Rᵐᵒᵖ }.toFun
          (MulOpposite.unop ({ toEquiv := tF, map_mul' := map_mul', map_add' := map_add' : R ≃+* Rᵐᵒᵖ }.toFun x))) =
      x
toFun : R → Rᵐᵒᵖ
invFun : Rᵐᵒᵖ → R
left_inv : Function.LeftInverse invFun toFun
right_inv : Function.RightInverse invFun toFun
map_mul'_1 :
  ∀ (x y : R),
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : R ≃ Rᵐᵒᵖ }.toFun (x * y) =
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : R ≃ Rᵐᵒᵖ }.toFun x *
        { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : R ≃ Rᵐᵒᵖ }.toFun y
map_add'_1 :
  ∀ (x y : R),
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : R ≃ Rᵐᵒᵖ }.toFun (x + y) =
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : R ≃ Rᵐᵒᵖ }.toFun x +
        { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : R ≃ Rᵐᵒᵖ }.toFun y
involution'_1 :
  ∀ (x : R),
    MulOpposite.unop
        ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul'_1,
              map_add' := map_add'_1 : R ≃+* Rᵐᵒᵖ }.toFun
          (MulOpposite.unop
            ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul'_1,
                  map_add' := map_add'_1 : R ≃+* Rᵐᵒᵖ }.toFun
              x))) =
      x
h₁ :
  { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul'_1,
        map_add' := map_add'_1, involution' := involution'_1 : RingInvo R }.toFun =
    { toEquiv := tF, map_mul' := map_mul', map_add' := map_add', involution' := involution' : RingInvo R }.toFun
h₂ :
  { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul'_1,
        map_add' := map_add'_1, involution' := involution'_1 : RingInvo R }.invFun =
    { toEquiv := tF, map_mul' := map_mul', map_add' := map_add', involution' := involution' : RingInvo R }.invFun
mk :
  ∀ (toFun_1 : R → Rᵐᵒᵖ) (invFun_1 : Rᵐᵒᵖ → R) (left_inv_1 : Function.LeftInverse invFun_1 toFun_1)
    (right_inv_1 : Function.RightInverse invFun_1 toFun_1)
    (map_mul' :
      ∀ (x y : R),
        { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : R ≃ Rᵐᵒᵖ }.toFun
            (x * y) =
          { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : R ≃ Rᵐᵒᵖ }.toFun
              x *
            { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : R ≃ Rᵐᵒᵖ }.toFun
              y)
    (map_add' :
      ∀ (x y : R),
        { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : R ≃ Rᵐᵒᵖ }.toFun
            (x + y) =
          { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : R ≃ Rᵐᵒᵖ }.toFun
              x +
            { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : R ≃ Rᵐᵒᵖ }.toFun
              y)
    (involution' :
      ∀ (x : R),
        MulOpposite.unop
            ({ toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1,
                  map_mul' := map_mul', map_add' := map_add' : R ≃+* Rᵐᵒᵖ }.toFun
              (MulOpposite.unop
                ({ toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1,
                      map_mul' := map_mul', map_add' := map_add' : R ≃+* Rᵐᵒᵖ }.toFun
                  x))) =
          x)
    (h₁ :
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul'_1,
            map_add' := map_add'_1, involution' := involution'_1 : RingInvo R }.toFun =
        { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1, map_mul' := map_mul',
            map_add' := map_add', involution' := involution' : RingInvo R }.toFun)
    (h₂ :
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul'_1,
            map_add' := map_add'_1, involution' := involution'_1 : RingInvo R }.invFun =
        { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1, map_mul' := map_mul',
            map_add' := map_add', involution' := involution' : RingInvo R }.invFun),
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul'_1,
        map_add' := map_add'_1, involution' := involution'_1 : RingInvo R } =
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1, 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'_1,
      map_add' := map_add'_1, involution' := involution'_1 : RingInvo R } =
    { toEquiv := tF, map_mul' := map_mul', map_add' := map_add', involution' := involution' }

Tactic:
cases tF