-- Lean 4 proof step from Mathlib.RingTheory.RingInvo (goal)
Goal:
F : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : EquivLike F R Rᵐᵒᵖ
tE : R ≃ Rᵐᵒᵖ
map_mul' : ∀ (x y : R), tE.toFun (x * y) = tE.toFun x * tE.toFun y
map_add' : ∀ (x y : R), tE.toFun (x + y) = tE.toFun x + tE.toFun y
involution' :
  ∀ (x : R),
    MulOpposite.unop
        ({ toEquiv := tE, map_mul' := map_mul', map_add' := map_add' : R ≃+* Rᵐᵒᵖ }.toFun
          (MulOpposite.unop ({ toEquiv := tE, map_mul' := map_mul', map_add' := map_add' : R ≃+* Rᵐᵒᵖ }.toFun x))) =
      x
tF : R ≃ Rᵐᵒᵖ
map_mul'_1 : ∀ (x y : R), tF.toFun (x * y) = tF.toFun x * tF.toFun y
map_add'_1 : ∀ (x y : R), tF.toFun (x + y) = tF.toFun x + tF.toFun y
involution'_1 :
  ∀ (x : R),
    MulOpposite.unop
        ({ toEquiv := tF, map_mul' := map_mul'_1, map_add' := map_add'_1 : R ≃+* Rᵐᵒᵖ }.toFun
          (MulOpposite.unop ({ toEquiv := tF, map_mul' := map_mul'_1, map_add' := map_add'_1 : R ≃+* Rᵐᵒᵖ }.toFun x))) =
      x
h₁ :
  { toEquiv := tE, map_mul' := map_mul', map_add' := map_add', involution' := involution' : RingInvo R }.toFun =
    { toEquiv := tF, map_mul' := map_mul'_1, map_add' := map_add'_1, involution' := involution'_1 : RingInvo R }.toFun
h₂ :
  { toEquiv := tE, map_mul' := map_mul', map_add' := map_add', involution' := involution' : RingInvo R }.invFun =
    { toEquiv := tF, map_mul' := map_mul'_1, map_add' := map_add'_1, involution' := involution'_1 : RingInvo R }.invFun
⊢ { toEquiv := tE, map_mul' := map_mul', map_add' := map_add', involution' := involution' : RingInvo R } =
    { toEquiv := tF, map_mul' := map_mul'_1, map_add' := map_add'_1, involution' := involution'_1 }
have mk : ∀ (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 : 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' :
    ∀ (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' :
    ∀ (x : R),
      MulOpposite.unop
          ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
                map_add' := map_add' : R ≃+* Rᵐᵒᵖ }.toFun
            (MulOpposite.unop
              ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, 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',
          map_add' := map_add', involution' := involution' : RingInvo R }.toFun =
      { toEquiv := tF, map_mul' := map_mul'_1, map_add' := map_add'_1, involution' := involution'_1 :
          RingInvo R }.toFun)
  (h₂ :
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
          map_add' := map_add', involution' := involution' : RingInvo R }.invFun =
      { toEquiv := tF, map_mul' := map_mul'_1, map_add' := map_add'_1, involution' := involution'_1 :
          RingInvo R }.invFun),
  { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
      map_add' := map_add', involution' := involution' : RingInvo R } =
    { toEquiv := tF, map_mul' := map_mul'_1, map_add' := map_add'_1, involution' := involution'_1 }
Tactic: cases tE
Cleared hypotheses: tE, map_mul', map_add', involution', h₁, h₂