-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsMatching.exists_of_disjoint_sets_of_equiv {s t : Set V} (h : Disjoint s t)
    (f : s ≃ t) (hadj : ∀ v : s, G.Adj v (f v)) :
    ∃ M : Subgraph G, M.verts = s ∪ t ∧ M.IsMatching

Proof state:
case h
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hl : v ∈ s
⊢ ∀ (y : V), (↑(f ⟨v, ⋯⟩) = y ∨ ∃ (h : y ∈ s), ↑(f ⟨y, h⟩) = v) → y = ↑(f ⟨v, hl⟩)

Tactic:
rintro y (rfl | ⟨hys, rfl⟩)

Result:
case h.inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hl : v ∈ s
⊢ ↑(f ⟨v, ⋯⟩) = ↑(f ⟨v, hl⟩)

case h.inr.intro
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
y : V
hys : y ∈ s
hl : ↑(f ⟨y, hys⟩) ∈ s
⊢ y = ↑(f ⟨↑(f ⟨y, hys⟩), hl⟩)

Proof state:
case h.inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hr : v ∈ t
⊢ ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v

Tactic:
use f.symm ⟨v, hr⟩

Result:
case h
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hr : v ∈ t
⊢ (fun w => (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) ↑(f.symm ⟨v, hr⟩) ∧
    ∀ (y : V), (fun w => (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) y → y = ↑(f.symm ⟨v, hr⟩)

Proof state:
case h
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
⊢ { verts := s ∪ t, Adj := fun v w => (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v, adj_sub := ⋯,
          edge_vert := ⋯, symm := ⋯ }.verts =
      s ∪ t ∧
    { verts := s ∪ t, Adj := fun v w => (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v, adj_sub := ⋯,
        edge_vert := ⋯, symm := ⋯ }.IsMatching

Tactic:
simp only [Subgraph.IsMatching, Set.mem_union, true_and]

Result:
case h
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
⊢ ∀ ⦃v : V⦄, v ∈ s ∨ v ∈ t → ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v

Proof state:
case h.inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hl : v ∈ s
⊢ ↑(f ⟨v, ⋯⟩) = ↑(f ⟨v, hl⟩)

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
s t : Set V
h✝ : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v w : V
h : (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v
⊢ G.Adj v w

Tactic:
obtain (⟨hv, rfl⟩ | ⟨hw, rfl⟩) := h

Result:
case inl.intro
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hv : v ∈ s
⊢ G.Adj v ↑(f ⟨v, hv⟩)

case inr.intro
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
w : V
hw : w ∈ s
⊢ G.Adj (↑(f ⟨w, hw⟩)) w

Proof state:
case h
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hr : v ∈ t
⊢ ∀ (y : V), ((∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = y) ∨ ∃ (h : y ∈ s), ↑(f ⟨y, h⟩) = v) → y = ↑(f.symm ⟨v, hr⟩)

Tactic:
rintro y (⟨hy, rfl⟩ | ⟨hy, rfl⟩)

Result:
case h.inl.intro
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hr : v ∈ t
hy : v ∈ s
⊢ ↑(f ⟨v, hy⟩) = ↑(f.symm ⟨v, hr⟩)

case h.inr.intro
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
y : V
hy : y ∈ s
hr : ↑(f ⟨y, hy⟩) ∈ t
⊢ y = ↑(f.symm ⟨↑(f ⟨y, hy⟩), hr⟩)

Proof state:
case h.inr.intro
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
y : V
hy : y ∈ s
hr : ↑(f ⟨y, hy⟩) ∈ t
⊢ y = ↑(f.symm ⟨↑(f ⟨y, hy⟩), hr⟩)

Tactic:
simp

Result:
no goals

Proof state:
case h
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hl : v ∈ s
⊢ (fun w => (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) ↑(f ⟨v, hl⟩) ∧
    ∀ (y : V), (fun w => (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) y → y = ↑(f ⟨v, hl⟩)

Tactic:
simp only [hl, exists_const, true_or, exists_true_left, true_and]

Result:
case h
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hl : v ∈ s
⊢ ∀ (y : V), (↑(f ⟨v, ⋯⟩) = y ∨ ∃ (h : y ∈ s), ↑(f ⟨y, h⟩) = v) → y = ↑(f ⟨v, hl⟩)

Proof state:
case h
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hv : v ∈ s ∨ v ∈ t
⊢ ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v

Tactic:
rcases hv with hl | hr

Result:
case h.inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hl : v ∈ s
⊢ ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v

case h.inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hr : v ∈ t
⊢ ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v

Proof state:
case h
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hr : v ∈ t
⊢ (fun w => (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) ↑(f.symm ⟨v, hr⟩) ∧
    ∀ (y : V), (fun w => (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) y → y = ↑(f.symm ⟨v, hr⟩)

Tactic:
simp only [Subtype.coe_eta, Equiv.apply_symm_apply, Subtype.coe_prop, exists_const, or_true,
  true_and]

Result:
case h
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hr : v ∈ t
⊢ ∀ (y : V), ((∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = y) ∨ ∃ (h : y ∈ s), ↑(f ⟨y, h⟩) = v) → y = ↑(f.symm ⟨v, hr⟩)

Proof state:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
⊢ ∀ {v w : V}, (fun v w => (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) v w → v ∈ s ∪ t

Tactic:
aesop

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
⊢ ∀ {v w : V}, (fun v w => (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) v w → G.Adj v w

Tactic:
intro v w h

Result:
V : Type u_1
G : SimpleGraph V
s t : Set V
h✝ : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v w : V
h : (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v
⊢ G.Adj v w

Proof state:
case h.inr.intro
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
y : V
hys : y ∈ s
hl : ↑(f ⟨y, hys⟩) ∈ s
⊢ y = ↑(f ⟨↑(f ⟨y, hys⟩), hl⟩)

Tactic:
exact (h.ne_of_mem hl (f ⟨y, hys⟩).coe_prop rfl).elim

Result:
no goals

Proof state:
case h.inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hl : v ∈ s
⊢ ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v

Tactic:
use f ⟨v, hl⟩

Result:
case h
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hl : v ∈ s
⊢ (fun w => (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) ↑(f ⟨v, hl⟩) ∧
    ∀ (y : V), (fun w => (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) y → y = ↑(f ⟨v, hl⟩)