-- 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.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''
hc : y ≠ w'
⊢ False

Tactic:
simp_all [show M.Adj v y ↔ ¬M.Adj v w' from by simpa using hG' hc hr.1 hw'.2]

Result:
no goals

Proof state:
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

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
⊢ (fun w => ⊤.Adj v w) w ∧ ∀ (y : V), (fun w => ⊤.Adj v w) y → y = w

Proof state:
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

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

Result:
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'
⊢ ∃! 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
⊢ (fun w => ⊤.Adj v w) w ∧ ∀ (y : V), (fun w => ⊤.Adj v w) y → y = w

Tactic:
simp only [Subgraph.top_adj, sup_adj, sdiff_adj, Subgraph.spanningCoe_adj, hw.1, h,
  not_false_eq_true, and_self, not_true_eq_false, or_false, true_and]

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
⊢ ∀ (y : V), M.Adj v y ∧ ¬G'.Adj v y ∨ G'.Adj v y ∧ ¬M.Adj v y → y = w

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
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
w' : V
hw' : y ≠ w' ∧ G'.Adj v w'
⊢ y = w

Tactic:
simp_all [show M.Adj v y ↔ ¬M.Adj v w' from by simpa using hG' hw'.1 hr.1 hw'.2]

Result:
no goals

Proof state:
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'

Tactic:
by_contra! hc

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''
hc : y ≠ w'
⊢ False

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'
⊢ (fun w => ⊤.Adj v w) w' ∧ ∀ (y : V), (fun w => ⊤.Adj v w) y → y = w'

Tactic:
simp only [Subgraph.top_adj, sup_adj, sdiff_adj, Subgraph.spanningCoe_adj, hmadj.mp hw.1, hw'.2,
  not_true_eq_false, and_self, not_false_eq_true, or_true, true_and]

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'
⊢ ∀ (y : V), M.Adj v y ∧ ¬G'.Adj v y ∨ 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'
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''
hc : y ≠ w'
⊢ M.Adj v y ↔ ¬M.Adj v w'

Tactic:
simpa using hG' hc hr.1 hw'.2

Result:
no goals

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'
⊢ ∃! w, ⊤.Adj v w

Tactic:
have hmadj :  M.Adj v w ↔ ¬M.Adj v w' := by simpa using hG' hw'.1 h hw'.2

Result:
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

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
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
w' : V
hw' : y ≠ w' ∧ G'.Adj v w'
⊢ M.Adj v y ↔ ¬M.Adj v w'

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

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
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
⊢ y = w

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

Result:
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
w' : V
hw' : y ≠ w' ∧ G'.Adj v w'
⊢ 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 : V
⊢ ∃! w, ⊤.Adj v w

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

Result:
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