-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsMatching.coeSubgraph {G' : Subgraph G} {M : Subgraph G'.coe} (hM : M.IsMatching) :
    M.coeSubgraph.IsMatching

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w => M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w => M.Adj ⟨v✝, ⋯⟩ w) y → y = w
⊢ ∃! w, (Subgraph.coeSubgraph M).Adj v✝ w

Tactic:
use w

Result:
case h
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w => M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w => M.Adj ⟨v✝, ⋯⟩ w) y → y = w
⊢ (fun w => (Subgraph.coeSubgraph M).Adj v✝ w) ↑w ∧ ∀ (y : V), (fun w => (Subgraph.coeSubgraph M).Adj v✝ w) y → y = ↑w

Proof state:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
⊢ ∃! w, (Subgraph.coeSubgraph M).Adj v✝ w

Tactic:
obtain ⟨w, hw⟩ := hM <| Set.mem_of_mem_image_val <| M.verts_coeSubgraph.symm ▸ hv

Result:
case intro
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w => M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w => M.Adj ⟨v✝, ⋯⟩ w) y → y = w
⊢ ∃! w, (Subgraph.coeSubgraph M).Adj v✝ w

Proof state:
case h.refine_2
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w => M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w => M.Adj ⟨v✝, ⋯⟩ w) y → y = w
y : V
hy : (fun w => (Subgraph.coeSubgraph M).Adj v✝ w) y
⊢ y = ↑w

Tactic:
obtain ⟨_, hw', hvw⟩ := (coeSubgraph_adj _ _ _).mp hy

Result:
case h.refine_2.intro.intro
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w => M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w => M.Adj ⟨v✝, ⋯⟩ w) y → y = w
y : V
hy : (fun w => (Subgraph.coeSubgraph M).Adj v✝ w) y
w✝ : v✝ ∈ G'.verts
hw' : y ∈ G'.verts
hvw : M.Adj ⟨v✝, w✝⟩ ⟨y, hw'⟩
⊢ y = ↑w

Proof state:
case h.refine_1
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w => M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w => M.Adj ⟨v✝, ⋯⟩ w) y → y = w
⊢ (fun w => (Subgraph.coeSubgraph M).Adj v✝ w) ↑w

Tactic:
obtain ⟨v, hv⟩ := (Set.mem_image _ _ _).mp <| M.verts_coeSubgraph.symm ▸ hv

Result:
case h.refine_1.intro
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv✝ : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w => M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w => M.Adj ⟨v✝, ⋯⟩ w) y → y = w
v : { x // x ∈ G'.verts }
hv : v ∈ M.verts ∧ ↑v = v✝
⊢ (Subgraph.coeSubgraph M).Adj v✝ ↑w

Proof state:
case h.refine_2.intro.intro
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w => M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w => M.Adj ⟨v✝, ⋯⟩ w) y → y = w
y : V
hy : (fun w => (Subgraph.coeSubgraph M).Adj v✝ w) y
w✝ : v✝ ∈ G'.verts
hw' : y ∈ G'.verts
hvw : M.Adj ⟨v✝, w✝⟩ ⟨y, hw'⟩
⊢ y = ↑w

Tactic:
rw [← hw.2 ⟨y, hw'⟩ hvw]

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
⊢ (Subgraph.coeSubgraph M).IsMatching

Tactic:
intro _ hv

Result:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
⊢ ∃! w, (Subgraph.coeSubgraph M).Adj v✝ w

Proof state:
case h.refine_1.intro
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv✝ : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w => M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w => M.Adj ⟨v✝, ⋯⟩ w) y → y = w
v : { x // x ∈ G'.verts }
hv : v ∈ M.verts ∧ ↑v = v✝
⊢ ∃ (h : v✝ ∈ G'.verts), M.Adj ⟨v✝, ⋯⟩ w

Tactic:
exact ⟨hv.2 ▸ v.2, hw.1⟩

Result:
no goals

Proof state:
case h
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w => M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w => M.Adj ⟨v✝, ⋯⟩ w) y → y = w
⊢ (fun w => (Subgraph.coeSubgraph M).Adj v✝ w) ↑w ∧ ∀ (y : V), (fun w => (Subgraph.coeSubgraph M).Adj v✝ w) y → y = ↑w

Tactic:
refine ⟨?_, fun y hy => ?_⟩

Result:
case h.refine_1
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w => M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w => M.Adj ⟨v✝, ⋯⟩ w) y → y = w
⊢ (fun w => (Subgraph.coeSubgraph M).Adj v✝ w) ↑w

case h.refine_2
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w => M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w => M.Adj ⟨v✝, ⋯⟩ w) y → y = w
y : V
hy : (fun w => (Subgraph.coeSubgraph M).Adj v✝ w) y
⊢ y = ↑w

Proof state:
case h.refine_1.intro
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv✝ : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w => M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w => M.Adj ⟨v✝, ⋯⟩ w) y → y = w
v : { x // x ∈ G'.verts }
hv : v ∈ M.verts ∧ ↑v = v✝
⊢ (Subgraph.coeSubgraph M).Adj v✝ ↑w

Tactic:
simp only [coeSubgraph_adj, Subtype.coe_eta, Subtype.coe_prop, exists_const]

Result:
case h.refine_1.intro
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv✝ : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w => M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w => M.Adj ⟨v✝, ⋯⟩ w) y → y = w
v : { x // x ∈ G'.verts }
hv : v ∈ M.verts ∧ ↑v = v✝
⊢ ∃ (h : v✝ ∈ G'.verts), M.Adj ⟨v✝, ⋯⟩ w