-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem ext {e e' : PartialEquiv α β} (h : ∀ x, e x = e' x)
    (hsymm : ∀ x, e.symm x = e'.symm x) (hs : e.source = e'.source) : e = e'

Proof state:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
⊢ e = e'

Tactic:
have A : (e : α → β) = e' := by
  ext x
  exact h x

Result:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
A : ↑e = ↑e'
⊢ e = e'

Proof state:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
A : ↑e = ↑e'
B : ↑e.symm = ↑e'.symm
I : ↑e '' e.source = e.target
I' : ↑e' '' e'.source = e'.target
⊢ e = e'

Tactic:
rw [A, hs, I'] at I

Result:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
A : ↑e = ↑e'
B : ↑e.symm = ↑e'.symm
I : e'.target = e.target
I' : ↑e' '' e'.source = e'.target
⊢ e = e'

Proof state:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
⊢ ↑e = ↑e'

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
x : α
⊢ ↑e x = ↑e' x

Proof state:
case mk.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✝ : α → β
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
I' :
  ↑{ 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'✝ }.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
h :
  ∀ (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'✝¹ }
        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'✝ }
        x
hsymm :
  ∀ (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'✝¹ }.symm
        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'✝ }.symm
        x
hs :
  { 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'✝ }.source
A :
  ↑{ 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'✝ }
B :
  ↑{ 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
I :
  { 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'✝¹ }.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'✝¹ } =
    { 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:
simp_all

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
A : ↑e = ↑e'
B : ↑e.symm = ↑e'.symm
⊢ e = e'

Tactic:
have I : e '' e.source = e.target := e.image_source_eq_target

Result:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
A : ↑e = ↑e'
B : ↑e.symm = ↑e'.symm
I : ↑e '' e.source = e.target
⊢ e = e'

Proof state:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
A : ↑e = ↑e'
⊢ ↑e.symm = ↑e'.symm

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
A : ↑e = ↑e'
x : β
⊢ ↑e.symm x = ↑e'.symm x

Proof state:
case h
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
x : α
⊢ ↑e x = ↑e' x

Tactic:
exact h x

Result:
no goals