Theorem: Matroid.Iso.symm_symm (Matroid/Old/_Equiv.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
⊢ e.symm.symm = e
Tactic:
cases e
State after:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
toPartialEquiv✝ : PartialEquiv α β
source_eq'✝ : toPartialEquiv✝.source = M.E
target_eq'✝ : toPartialEquiv✝.target = N.E
setOf_base_eq'✝ : setOf N.Base = image ↑toPartialEquiv✝ '' setOf M.Base
⊢ { toPartialEquiv := toPartialEquiv✝, source_eq' := source_eq'✝, target_eq' := target_eq'✝,
          setOf_base_eq' := setOf_base_eq'✝ }.symm.symm =
    { toPartialEquiv := toPartialEquiv✝, source_eq' := source_eq'✝, target_eq' := target_eq'✝,
      setOf_base_eq' := setOf_base_eq'✝ }

State before:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
toPartialEquiv✝ : PartialEquiv α β
source_eq'✝ : toPartialEquiv✝.source = M.E
target_eq'✝ : toPartialEquiv✝.target = N.E
setOf_base_eq'✝ : setOf N.Base = image ↑toPartialEquiv✝ '' setOf M.Base
⊢ { toPartialEquiv := toPartialEquiv✝, source_eq' := source_eq'✝, target_eq' := target_eq'✝,
          setOf_base_eq' := setOf_base_eq'✝ }.symm.symm =
    { toPartialEquiv := toPartialEquiv✝, source_eq' := source_eq'✝, target_eq' := target_eq'✝,
      setOf_base_eq' := setOf_base_eq'✝ }
Tactic:
rfl
State after:
no goals