-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
protected lemma IsMatching.map {G' : SimpleGraph W} {M : Subgraph G} (f : G →g G')
    (hf : Injective f) (hM : M.IsMatching) : (M.map f).IsMatching

Proof state:
case h.intro.intro.intro.intro.refl
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective ⇑f
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun w => M.Adj v w) v' ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = v'
w' : V
hw : M.Adj v w'
hw' : f v = f v
⊢ f w' = f v'

Tactic:
rw [hv'.2 w' hw]

Result:
no goals

Proof state:
case h.intro.intro.intro.intro
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective ⇑f
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun w => M.Adj v w) v' ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = v'
w w' : V
hw : M.Adj w w'
hw' : f w = f v
⊢ f w' = f v'

Tactic:
cases hf hw'.symm

Result:
case h.intro.intro.intro.intro.refl
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective ⇑f
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun w => M.Adj v w) v' ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = v'
w' : V
hw : M.Adj v w'
hw' : f v = f v
⊢ f w' = f v'

Proof state:
case intro.intro.intro
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective ⇑f
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun w => M.Adj v w) v' ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = v'
⊢ ∃! w, (Subgraph.map f M).Adj (f v) w

Tactic:
use f v'

Result:
case h
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective ⇑f
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun w => M.Adj v w) v' ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = v'
⊢ (fun w => (Subgraph.map f M).Adj (f v) w) (f v') ∧ ∀ (y : W), (fun w => (Subgraph.map f M).Adj (f v) w) y → y = f v'

Proof state:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective ⇑f
hM : M.IsMatching
⊢ (Subgraph.map f M).IsMatching

Tactic:
rintro _ ⟨v, hv, rfl⟩

Result:
case intro.intro
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective ⇑f
hM : M.IsMatching
v : V
hv : v ∈ M.verts
⊢ ∃! w, (Subgraph.map f M).Adj (f v) w

Proof state:
case h
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective ⇑f
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun w => M.Adj v w) v' ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = v'
⊢ ∀ (y : W), (fun w => (Subgraph.map f M).Adj (f v) w) y → y = f v'

Tactic:
rintro _ ⟨w, w', hw, hw', rfl⟩

Result:
case h.intro.intro.intro.intro
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective ⇑f
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun w => M.Adj v w) v' ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = v'
w w' : V
hw : M.Adj w w'
hw' : f w = f v
⊢ f w' = f v'

Proof state:
case intro.intro
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective ⇑f
hM : M.IsMatching
v : V
hv : v ∈ M.verts
⊢ ∃! w, (Subgraph.map f M).Adj (f v) w

Tactic:
obtain ⟨v', hv'⟩ := hM hv

Result:
case intro.intro.intro
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective ⇑f
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun w => M.Adj v w) v' ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = v'
⊢ ∃! w, (Subgraph.map f M).Adj (f v) w

Proof state:
case h
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective ⇑f
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun w => M.Adj v w) v' ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = v'
⊢ (fun w => (Subgraph.map f M).Adj (f v) w) (f v') ∧ ∀ (y : W), (fun w => (Subgraph.map f M).Adj (f v) w) y → y = f v'

Tactic:
refine ⟨⟨v, v', hv'.1, rfl, rfl⟩, ?_⟩

Result:
case h
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective ⇑f
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun w => M.Adj v w) v' ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = v'
⊢ ∀ (y : W), (fun w => (Subgraph.map f M).Adj (f v) w) y → y = f v'