[GOAL]
R : Type u_1
inst✝¹ inst✝ : Semiring R
e f : RingInvo R
h₁ : (fun f => f.toFun) e = (fun f => f.toFun) f
h₂ : (fun f => f.invFun) e = (fun f => f.invFun) f
⊢ e = f
[PROOFSTEP]
rcases e with ⟨⟨tE, _⟩, _⟩
[GOAL]
case mk.mk
R : Type u_1
inst✝¹ inst✝ : Semiring R
f : RingInvo R
tE : R ≃ Rᵐᵒᵖ
map_mul'✝ : ∀ (x y : R), Equiv.toFun tE (x * y) = Equiv.toFun tE x * Equiv.toFun tE y
map_add'✝ : ∀ (x y : R), Equiv.toFun tE (x + y) = Equiv.toFun tE x + Equiv.toFun tE y
involution'✝ :
  ∀ (x : R),
    MulOpposite.unop
        (Equiv.toFun { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          (MulOpposite.unop (Equiv.toFun { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv x))) =
      x
h₁ :
  (fun f => f.toFun)
      { toRingEquiv := { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }, involution' := involution'✝ } =
    (fun f => f.toFun) f
h₂ :
  (fun f => f.invFun)
      { toRingEquiv := { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }, involution' := involution'✝ } =
    (fun f => f.invFun) f
⊢ { toRingEquiv := { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }, involution' := involution'✝ } = f
[PROOFSTEP]
rcases f with ⟨⟨tF, _⟩, _⟩
[GOAL]
case mk.mk.mk.mk
R : Type u_1
inst✝¹ inst✝ : Semiring R
tE : R ≃ Rᵐᵒᵖ
map_mul'✝¹ : ∀ (x y : R), Equiv.toFun tE (x * y) = Equiv.toFun tE x * Equiv.toFun tE y
map_add'✝¹ : ∀ (x y : R), Equiv.toFun tE (x + y) = Equiv.toFun tE x + Equiv.toFun tE y
involution'✝¹ :
  ∀ (x : R),
    MulOpposite.unop
        (Equiv.toFun { toEquiv := tE, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
          (MulOpposite.unop
            (Equiv.toFun { toEquiv := tE, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv x))) =
      x
tF : R ≃ Rᵐᵒᵖ
map_mul'✝ : ∀ (x y : R), Equiv.toFun tF (x * y) = Equiv.toFun tF x * Equiv.toFun tF y
map_add'✝ : ∀ (x y : R), Equiv.toFun tF (x + y) = Equiv.toFun tF x + Equiv.toFun tF y
involution'✝ :
  ∀ (x : R),
    MulOpposite.unop
        (Equiv.toFun { toEquiv := tF, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          (MulOpposite.unop (Equiv.toFun { toEquiv := tF, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv x))) =
      x
h₁ :
  (fun f => f.toFun)
      { toRingEquiv := { toEquiv := tE, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
        involution' := involution'✝¹ } =
    (fun f => f.toFun)
      { toRingEquiv := { toEquiv := tF, map_mul' := map_mul'✝, map_add' := map_add'✝ }, involution' := involution'✝ }
h₂ :
  (fun f => f.invFun)
      { toRingEquiv := { toEquiv := tE, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
        involution' := involution'✝¹ } =
    (fun f => f.invFun)
      { toRingEquiv := { toEquiv := tF, map_mul' := map_mul'✝, map_add' := map_add'✝ }, involution' := involution'✝ }
⊢ { toRingEquiv := { toEquiv := tE, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }, involution' := involution'✝¹ } =
    { toRingEquiv := { toEquiv := tF, map_mul' := map_mul'✝, map_add' := map_add'✝ }, involution' := involution'✝ }
[PROOFSTEP]
cases tE
[GOAL]
case mk.mk.mk.mk.mk
R : Type u_1
inst✝¹ inst✝ : Semiring R
tF : R ≃ Rᵐᵒᵖ
map_mul'✝¹ : ∀ (x y : R), Equiv.toFun tF (x * y) = Equiv.toFun tF x * Equiv.toFun tF y
map_add'✝¹ : ∀ (x y : R), Equiv.toFun tF (x + y) = Equiv.toFun tF x + Equiv.toFun tF y
involution'✝¹ :
  ∀ (x : R),
    MulOpposite.unop
        (Equiv.toFun { toEquiv := tF, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
          (MulOpposite.unop
            (Equiv.toFun { toEquiv := tF, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv 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),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : R),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
involution'✝ :
  ∀ (x : R),
    MulOpposite.unop
        (Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          (MulOpposite.unop
            (Equiv.toFun
              { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
                  map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
              x))) =
      x
h₁ :
  (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        involution' := involution'✝ } =
    (fun f => f.toFun)
      { toRingEquiv := { toEquiv := tF, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }, involution' := involution'✝¹ }
h₂ :
  (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        involution' := involution'✝ } =
    (fun f => f.invFun)
      { toRingEquiv := { toEquiv := tF, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }, involution' := involution'✝¹ }
⊢ {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
          map_mul' := map_mul'✝, map_add' := map_add'✝ },
      involution' := involution'✝ } =
    { toRingEquiv := { toEquiv := tF, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }, involution' := involution'✝¹ }
[PROOFSTEP]
cases tF
[GOAL]
case mk.mk.mk.mk.mk.mk
R : Type u_1
inst✝¹ inst✝ : Semiring R
toFun✝¹ : R → Rᵐᵒᵖ
invFun✝¹ : Rᵐᵒᵖ → R
left_inv✝¹ : Function.LeftInverse invFun✝¹ toFun✝¹
right_inv✝¹ : Function.RightInverse invFun✝¹ toFun✝¹
map_mul'✝¹ :
  ∀ (x y : R),
    Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x * y) =
      Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x *
        Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
map_add'✝¹ :
  ∀ (x y : R),
    Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x + y) =
      Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x +
        Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
involution'✝¹ :
  ∀ (x : R),
    MulOpposite.unop
        (Equiv.toFun
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
              map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
          (MulOpposite.unop
            (Equiv.toFun
              { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
                  map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
              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),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : R),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
involution'✝ :
  ∀ (x : R),
    MulOpposite.unop
        (Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          (MulOpposite.unop
            (Equiv.toFun
              { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
                  map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
              x))) =
      x
h₁ :
  (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
            map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
        involution' := involution'✝¹ } =
    (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        involution' := involution'✝ }
h₂ :
  (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
            map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
        involution' := involution'✝¹ } =
    (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        involution' := involution'✝ }
⊢ {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
          map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
      involution' := involution'✝¹ } =
    {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
          map_mul' := map_mul'✝, map_add' := map_add'✝ },
      involution' := involution'✝ }
[PROOFSTEP]
congr
