-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma Subgraph.IsPerfectMatching.symmDiff_isCycles
    {M : Subgraph G} {M' : Subgraph G'} (hM : M.IsPerfectMatching)
    (hM' : M'.IsPerfectMatching) : (M.spanningCoe ∆ M'.spanningCoe).IsCycles

Proof state:
case pos
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
w' : V
hw' : (fun w => M'.Adj v w) w' ∧ ∀ (y : V), (fun w => M'.Adj v w) y → y = w'
hww' : w = w'
⊢ (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
    ∃ x y, ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}

Tactic:
simp_all [← imp_iff_not_or, hww']

Result:
no goals

Proof state:
case neg.h
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
w' : V
hw' : (fun w => M'.Adj v w) w' ∧ ∀ (y : V), (fun w => M'.Adj v w) y → y = w'
hww' : ¬w = w'
⊢ ∃ x y, ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}

Tactic:
use w, w'

Result:
case h
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
w' : V
hw' : (fun w => M'.Adj v w) w' ∧ ∀ (y : V), (fun w => M'.Adj v w) y → y = w'
hww' : ¬w = w'
⊢ ¬w = w' ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {w, w'}

Proof state:
case intro.intro
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
w' : V
hw' : (fun w => M'.Adj v w) w' ∧ ∀ (y : V), (fun w => M'.Adj v w) y → y = w'
⊢ ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).Nonempty → ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).ncard = 2

Tactic:
simp only [symmDiff_def, Set.ncard_eq_two, ne_eq, imp_iff_not_or, Set.not_nonempty_iff_eq_empty,
  Set.eq_empty_iff_forall_not_mem, SimpleGraph.mem_neighborSet, SimpleGraph.sup_adj, sdiff_adj,
  spanningCoe_adj, not_or, not_and, not_not]

Result:
case intro.intro
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
w' : V
hw' : (fun w => M'.Adj v w) w' ∧ ∀ (y : V), (fun w => M'.Adj v w) y → y = w'
⊢ (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
    ∃ x y, ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}

Proof state:
case h
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
w' : V
hw' : (fun w => M'.Adj v w) w' ∧ ∀ (y : V), (fun w => M'.Adj v w) y → y = w'
hww' : ¬w = w'
⊢ ¬w = w' ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {w, w'}

Tactic:
aesop

Result:
no goals

Proof state:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v : V
⊢ ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).Nonempty → ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).ncard = 2

Tactic:
obtain ⟨w, hw⟩ := hM.1 (hM.2 v)

Result:
case intro
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
⊢ ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).Nonempty → ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).ncard = 2

Proof state:
case intro
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
⊢ ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).Nonempty → ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).ncard = 2

Tactic:
obtain ⟨w', hw'⟩ := hM'.1 (hM'.2 v)

Result:
case intro.intro
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
w' : V
hw' : (fun w => M'.Adj v w) w' ∧ ∀ (y : V), (fun w => M'.Adj v w) y → y = w'
⊢ ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).Nonempty → ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).ncard = 2

Proof state:
case intro.intro
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
w' : V
hw' : (fun w => M'.Adj v w) w' ∧ ∀ (y : V), (fun w => M'.Adj v w) y → y = w'
⊢ (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
    ∃ x y, ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}

Tactic:
by_cases hww' : w = w'

Result:
case pos
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
w' : V
hw' : (fun w => M'.Adj v w) w' ∧ ∀ (y : V), (fun w => M'.Adj v w) y → y = w'
hww' : w = w'
⊢ (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
    ∃ x y, ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}

case neg
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
w' : V
hw' : (fun w => M'.Adj v w) w' ∧ ∀ (y : V), (fun w => M'.Adj v w) y → y = w'
hww' : ¬w = w'
⊢ (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
    ∃ x y, ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}

Proof state:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
⊢ (M.spanningCoe ∆ M'.spanningCoe).IsCycles

Tactic:
intro v

Result:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v : V
⊢ ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).Nonempty → ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).ncard = 2

Proof state:
case neg
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
w' : V
hw' : (fun w => M'.Adj v w) w' ∧ ∀ (y : V), (fun w => M'.Adj v w) y → y = w'
hww' : ¬w = w'
⊢ (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
    ∃ x y, ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}

Tactic:
right

Result:
case neg.h
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
w' : V
hw' : (fun w => M'.Adj v w) w' ∧ ∀ (y : V), (fun w => M'.Adj v w) y → y = w'
hww' : ¬w = w'
⊢ ∃ x y, ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}