-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsPerfectMatching.symmDiff_of_isAlternating (hM : M.IsPerfectMatching)
    (hG' : G'.IsAlternating M.spanningCoe) (hG'cyc : G'.IsCycles) :
    (⊤ : Subgraph (M.spanningCoe ∆ G')).IsPerfectMatching

Proof state:
case h.inl
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
y : V
hl : M.Adj v y ∧ ¬G'.Adj v y
⊢ y = w'

Tactic:
aesop

Result:
no goals

Proof state:
case h.inr
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
⊢ y = w'

Tactic:
obtain ⟨w'', hw''⟩ := hG'cyc.other_adj_of_adj hr.1

Result:
case h.inr.intro
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
w'' : V
hw'' : y ≠ w'' ∧ G'.Adj v w''
⊢ y = w'

Proof state:
case pos.intro
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
⊢ ∃! w, ⊤.Adj v w

Tactic:
use w'

Result:
case h
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
⊢ (fun w => ⊤.Adj v w) w' ∧ ∀ (y : V), (fun w => ⊤.Adj v w) y → y = w'

Proof state:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
⊢ ⊤.IsPerfectMatching

Tactic:
rw [Subgraph.isPerfectMatching_iff]

Result:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
⊢ ∀ (v : V), ∃! w, ⊤.Adj v w

Proof state:
case h
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
⊢ ∀ (y : V), M.Adj v y ∧ ¬G'.Adj v y ∨ G'.Adj v y ∧ ¬M.Adj v y → y = w'

Tactic:
rintro y (hl | hr)

Result:
case h.inl
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
y : V
hl : M.Adj v y ∧ ¬G'.Adj v y
⊢ y = w'

case h.inr
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
⊢ y = w'

Proof state:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
⊢ M.Adj v w ↔ ¬M.Adj v w'

Tactic:
simpa using hG' hw'.1 h hw'.2

Result:
no goals

Proof state:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
⊢ ∀ (v : V), ∃! w, ⊤.Adj v w

Tactic:
intro v

Result:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v : V
⊢ ∃! w, ⊤.Adj v w

Proof state:
case intro
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
⊢ ∃! w, ⊤.Adj v w

Tactic:
by_cases h : G'.Adj v w

Result:
case pos
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
h : G'.Adj v w
⊢ ∃! w, ⊤.Adj v w

case neg
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
h : ¬G'.Adj v w
⊢ ∃! w, ⊤.Adj v w

Proof state:
case h
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
h : ¬G'.Adj v w
⊢ ∀ (y : V), M.Adj v y ∧ ¬G'.Adj v y ∨ G'.Adj v y ∧ ¬M.Adj v y → y = w

Tactic:
rintro y (hl | hr)

Result:
case h.inl
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
h : ¬G'.Adj v w
y : V
hl : M.Adj v y ∧ ¬G'.Adj v y
⊢ y = w

case h.inr
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
h : ¬G'.Adj v w
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
⊢ y = w

Proof state:
case h.inl
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
h : ¬G'.Adj v w
y : V
hl : M.Adj v y ∧ ¬G'.Adj v y
⊢ y = w

Tactic:
exact hw.2 _ hl.1

Result:
no goals