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

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).IsAlternating M.spanningCoe

Tactic:
intro v w w' hww' hvw hvw'

Result:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w w' : V
hww' : w ≠ w'
hvw : (M.spanningCoe ∆ M'.spanningCoe).Adj v w
hvw' : (M.spanningCoe ∆ M'.spanningCoe).Adj v w'
⊢ M.spanningCoe.Adj v w ↔ ¬M.spanningCoe.Adj v w'

Proof state:
case intro.intro.intro.intro
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w w' : V
hww' : w ≠ w'
hvw : (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).Adj v w
hvw' : (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).Adj v w'
v1 : V
hm1 : M.Adj v v1
hv1 : ∀ (y : V), M.Adj v y → y = v1
v2 : V
hm2 : M'.Adj v v2
hv2 : ∀ (y : V), M'.Adj v y → y = v2
⊢ M.spanningCoe.Adj v w ↔ ¬M.spanningCoe.Adj v w'

Tactic:
aesop

Result:
no goals

Proof state:
case intro.intro.intro.intro
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w w' : V
hww' : w ≠ w'
hvw : (M.spanningCoe ∆ M'.spanningCoe).Adj v w
hvw' : (M.spanningCoe ∆ M'.spanningCoe).Adj v w'
v1 : V
hm1 : M.Adj v v1
hv1 : ∀ (y : V), (fun w => M.Adj v w) y → y = v1
v2 : V
hm2 : M'.Adj v v2
hv2 : ∀ (y : V), (fun w => M'.Adj v w) y → y = v2
⊢ M.spanningCoe.Adj v w ↔ ¬M.spanningCoe.Adj v w'

Tactic:
simp only [symmDiff_def] at *

Result:
case intro.intro.intro.intro
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w w' : V
hww' : w ≠ w'
hvw : (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).Adj v w
hvw' : (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).Adj v w'
v1 : V
hm1 : M.Adj v v1
hv1 : ∀ (y : V), M.Adj v y → y = v1
v2 : V
hm2 : M'.Adj v v2
hv2 : ∀ (y : V), M'.Adj v y → y = v2
⊢ M.spanningCoe.Adj v w ↔ ¬M.spanningCoe.Adj v 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 w' : V
hww' : w ≠ w'
hvw : (M.spanningCoe ∆ M'.spanningCoe).Adj v w
hvw' : (M.spanningCoe ∆ M'.spanningCoe).Adj v w'
v1 : V
hm1 : M.Adj v v1
hv1 : ∀ (y : V), (fun w => M.Adj v w) y → y = v1
⊢ M.spanningCoe.Adj v w ↔ ¬M.spanningCoe.Adj v w'

Tactic:
obtain ⟨v2, hm2, hv2⟩ := hM'.1 (hM'.2 v)

Result:
case intro.intro.intro.intro
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w w' : V
hww' : w ≠ w'
hvw : (M.spanningCoe ∆ M'.spanningCoe).Adj v w
hvw' : (M.spanningCoe ∆ M'.spanningCoe).Adj v w'
v1 : V
hm1 : M.Adj v v1
hv1 : ∀ (y : V), (fun w => M.Adj v w) y → y = v1
v2 : V
hm2 : M'.Adj v v2
hv2 : ∀ (y : V), (fun w => M'.Adj v w) y → y = v2
⊢ M.spanningCoe.Adj v w ↔ ¬M.spanningCoe.Adj v w'

Proof state:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w w' : V
hww' : w ≠ w'
hvw : (M.spanningCoe ∆ M'.spanningCoe).Adj v w
hvw' : (M.spanningCoe ∆ M'.spanningCoe).Adj v w'
⊢ M.spanningCoe.Adj v w ↔ ¬M.spanningCoe.Adj v w'

Tactic:
obtain ⟨v1, hm1, hv1⟩ := 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 w' : V
hww' : w ≠ w'
hvw : (M.spanningCoe ∆ M'.spanningCoe).Adj v w
hvw' : (M.spanningCoe ∆ M'.spanningCoe).Adj v w'
v1 : V
hm1 : M.Adj v v1
hv1 : ∀ (y : V), (fun w => M.Adj v w) y → y = v1
⊢ M.spanningCoe.Adj v w ↔ ¬M.spanningCoe.Adj v w'