-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem copy_eq (e : PartialEquiv α β) (f : α → β) (hf : ⇑e = f) (g : β → α) (hg : ⇑e.symm = g)
    (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t) :
    e.copy f hf g hg s hs t ht = e

Proof state:
case mk
α : Type u_1
β : Type u_2
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'✝ }.copy
      ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }
      ⋯
      ↑{ 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'✝ }.source
      ⋯
      { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.target
      ⋯ =
    { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
      map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
f : α → β
hf : ↑e = f
g : β → α
hg : ↑e.symm = g
s : Set α
hs : e.source = s
t : Set β
ht : e.target = t
⊢ e.copy f hf g hg s hs t ht = e

Tactic:
substs f g s t

Result:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ e.copy ↑e ⋯ ↑e.symm ⋯ e.source ⋯ e.target ⋯ = e

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ e.copy ↑e ⋯ ↑e.symm ⋯ e.source ⋯ e.target ⋯ = e

Tactic:
cases e

Result:
case mk
α : Type u_1
β : Type u_2
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'✝ }.copy
      ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }
      ⋯
      ↑{ 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'✝ }.source
      ⋯
      { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.target
      ⋯ =
    { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
      map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }