-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem trans_symm_eq_symm_trans_symm : (e.trans e').symm = e'.symm.trans e.symm

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ (e.trans e').symm = e'.symm.trans e.symm

Tactic:
cases e

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
e' : PartialEquiv β γ
toFun✝ : α → β
invFun✝ : β → α
source✝ : Set α
target✝ : Set β
map_source'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → toFun✝ x ∈ target✝
map_target'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → invFun✝ x ∈ source✝
left_inv'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → invFun✝ (toFun✝ x) = x
right_inv'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → toFun✝ (invFun✝ x) = x
⊢ ({ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
            map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.trans
        e').symm =
    e'.symm.trans
      { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.symm

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
toFun✝¹ : α → β
invFun✝¹ : β → α
source✝¹ : Set α
target✝¹ : Set β
map_source'✝¹ : ∀ ⦃x : α⦄, x ∈ source✝¹ → toFun✝¹ x ∈ target✝¹
map_target'✝¹ : ∀ ⦃x : β⦄, x ∈ target✝¹ → invFun✝¹ x ∈ source✝¹
left_inv'✝¹ : ∀ ⦃x : α⦄, x ∈ source✝¹ → invFun✝¹ (toFun✝¹ x) = x
right_inv'✝¹ : ∀ ⦃x : β⦄, x ∈ target✝¹ → toFun✝¹ (invFun✝¹ x) = x
toFun✝ : β → γ
invFun✝ : γ → β
source✝ : Set β
target✝ : Set γ
map_source'✝ : ∀ ⦃x : β⦄, x ∈ source✝ → toFun✝ x ∈ target✝
map_target'✝ : ∀ ⦃x : γ⦄, x ∈ target✝ → invFun✝ x ∈ source✝
left_inv'✝ : ∀ ⦃x : β⦄, x ∈ source✝ → invFun✝ (toFun✝ x) = x
right_inv'✝ : ∀ ⦃x : γ⦄, x ∈ target✝ → toFun✝ (invFun✝ x) = x
⊢ ({ toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
            map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ }.trans
        { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }).symm =
    { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
            map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.symm.trans
      { toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
          map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ }.symm

Tactic:
rfl

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
e' : PartialEquiv β γ
toFun✝ : α → β
invFun✝ : β → α
source✝ : Set α
target✝ : Set β
map_source'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → toFun✝ x ∈ target✝
map_target'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → invFun✝ x ∈ source✝
left_inv'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → invFun✝ (toFun✝ x) = x
right_inv'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → toFun✝ (invFun✝ x) = x
⊢ ({ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
            map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.trans
        e').symm =
    e'.symm.trans
      { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.symm

Tactic:
cases e'

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
toFun✝¹ : α → β
invFun✝¹ : β → α
source✝¹ : Set α
target✝¹ : Set β
map_source'✝¹ : ∀ ⦃x : α⦄, x ∈ source✝¹ → toFun✝¹ x ∈ target✝¹
map_target'✝¹ : ∀ ⦃x : β⦄, x ∈ target✝¹ → invFun✝¹ x ∈ source✝¹
left_inv'✝¹ : ∀ ⦃x : α⦄, x ∈ source✝¹ → invFun✝¹ (toFun✝¹ x) = x
right_inv'✝¹ : ∀ ⦃x : β⦄, x ∈ target✝¹ → toFun✝¹ (invFun✝¹ x) = x
toFun✝ : β → γ
invFun✝ : γ → β
source✝ : Set β
target✝ : Set γ
map_source'✝ : ∀ ⦃x : β⦄, x ∈ source✝ → toFun✝ x ∈ target✝
map_target'✝ : ∀ ⦃x : γ⦄, x ∈ target✝ → invFun✝ x ∈ source✝
left_inv'✝ : ∀ ⦃x : β⦄, x ∈ source✝ → invFun✝ (toFun✝ x) = x
right_inv'✝ : ∀ ⦃x : γ⦄, x ∈ target✝ → toFun✝ (invFun✝ x) = x
⊢ ({ toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
            map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ }.trans
        { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }).symm =
    { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
            map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.symm.trans
      { toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
          map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ }.symm