-- Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean
lemma Subgraph.IsMatching.exists_of_universalVerts [Finite V] {s : Set V}
    (h : Disjoint G.universalVerts s) (hc : s.ncard ≤ G.universalVerts.ncard) :
    ∃ t ⊆ G.universalVerts, ∃ (M : Subgraph G), M.verts = s ∪ t ∧ M.IsMatching

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
⊢ ∃ t ⊆ G.universalVerts, ∃ M, M.verts = s ∪ t ∧ M.IsMatching

Tactic:
obtain ⟨t, ht⟩ := Set.exists_subset_card_eq hc

Result:
case intro
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
⊢ ∃ t ⊆ G.universalVerts, ∃ M, M.verts = s ∪ t ∧ M.IsMatching

Proof state:
case intro.intro
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
f : ↑s ≃ ↑t
⊢ ∃ M, M.verts = s ∪ t ∧ M.IsMatching

Tactic:
letI hd := Set.disjoint_of_subset_left ht.1 h

Result:
case intro.intro
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
f : ↑s ≃ ↑t
hd : Disjoint t s := Set.disjoint_of_subset_left ht.left h
⊢ ∃ M, M.verts = s ∪ t ∧ M.IsMatching

Proof state:
case intro.intro
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
f : ↑s ≃ ↑t
hd : Disjoint t s := Set.disjoint_of_subset_left ht.left h
⊢ ∃ M, M.verts = s ∪ t ∧ M.IsMatching

Tactic:
have hadj (v : s) : G.Adj v (f v) := ht.1 (f v).2 (hd.ne_of_mem (f v).2 v.2)

Result:
case intro.intro
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
f : ↑s ≃ ↑t
hd : Disjoint t s := Set.disjoint_of_subset_left ht.left h
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
⊢ ∃ M, M.verts = s ∪ t ∧ M.IsMatching

Proof state:
case intro.intro
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
f : ↑s ≃ ↑t
hd : Disjoint t s := Set.disjoint_of_subset_left ht.left h
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
⊢ ∃ M, M.verts = s ∪ t ∧ M.IsMatching

Tactic:
exact Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv hd.symm f hadj

Result:
no goals

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
⊢ ∃ t ⊆ G.universalVerts, ∃ M, M.verts = s ∪ t ∧ M.IsMatching

Tactic:
refine ⟨t, ht.1, ?_⟩

Result:
case intro
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
⊢ ∃ M, M.verts = s ∪ t ∧ M.IsMatching

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
⊢ ∃ M, M.verts = s ∪ t ∧ M.IsMatching

Tactic:
obtain ⟨f⟩ : Nonempty (s ≃ t) := by
  rw [← Cardinal.eq, ← t.cast_ncard t.toFinite, ← s.cast_ncard s.toFinite, ht.2]

Result:
case intro.intro
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
f : ↑s ≃ ↑t
⊢ ∃ M, M.verts = s ∪ t ∧ M.IsMatching

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
⊢ Nonempty (↑s ≃ ↑t)

Tactic:
rw [← Cardinal.eq, ← t.cast_ncard t.toFinite, ← s.cast_ncard s.toFinite, ht.2]

Result:
no goals