-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsAlternating.sup_edge {u x : V} (halt : G.IsAlternating G') (hnadj : ¬G'.Adj u x)
    (hu' : ∀ u', u' ≠ u → G.Adj x u' → G'.Adj x u')
    (hx' : ∀ x', x' ≠ x → G.Adj x' u → G'.Adj x' u) : (G ⊔ edge u x).IsAlternating G'

Proof state:
case neg.inl.inr
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
rw [G'.adj_congr_of_sym2 (by aesop : s(v, w') = s(u, x))]

Result:
case neg.inl.inr
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ G'.Adj v w ↔ ¬G'.Adj u x

Proof state:
case neg.inr.inl.inl.intro
V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
v w w' : V
hww' : w ≠ w'
h1 : G.Adj v w'
hnadj : ¬G'.Adj v w
hu' : ∀ (u' : V), u' ≠ v → G.Adj w u' → G'.Adj w u'
hx' : ∀ (x' : V), x' ≠ w → G.Adj x' v → G'.Adj x' v
hadj : ¬G.Adj v w
hr : (v = v ∧ w = w ∨ v = w ∧ w = v) ∧ v ≠ w
⊢ G'.Adj v w'

Tactic:
exact (hx' _ hww'.symm h1.symm).symm

Result:
no goals

Proof state:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ s(v, w') = s(u, x)

Tactic:
aesop

Result:
no goals

Proof state:
case neg.inl.inr.inl.intro
V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
hnadj : ¬G'.Adj v w'
hu' : ∀ (u' : V), u' ≠ v → G.Adj w' u' → G'.Adj w' u'
hx' : ∀ (x' : V), x' ≠ w' → G.Adj x' v → G'.Adj x' v
hadj : ¬G.Adj v w'
h2 : (v = v ∧ w' = w' ∨ v = w' ∧ w' = v) ∧ v ≠ w'
⊢ G'.Adj v w

Tactic:
exact (hx' _ hww' hl.symm).symm

Result:
no goals

Proof state:
case neg.inr.inl
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
⊢ G'.Adj v w'

Tactic:
rcases hr.1 with ⟨hrl1, hrl2⟩ | ⟨hrr1, hrr2⟩

Result:
case neg.inr.inl.inl.intro
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
hrl1 : v = u
hrl2 : w = x
⊢ G'.Adj v w'

case neg.inr.inl.inr.intro
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
hrr1 : v = x
hrr2 : w = u
⊢ G'.Adj v w'

Proof state:
case neg.inl.inr
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ G'.Adj v w

Tactic:
rcases h2.1 with ⟨h2l1, h2l2⟩ | ⟨h2r1,h2r2⟩

Result:
case neg.inl.inr.inl.intro
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
h2l1 : v = u
h2l2 : w' = x
⊢ G'.Adj v w

case neg.inl.inr.inr.intro
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
h2r1 : v = x
h2r2 : w' = u
⊢ G'.Adj v w

Proof state:
case neg.inr.inl
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
rw [G'.adj_congr_of_sym2 (by aesop : s(v, w) = s(u, x))]

Result:
case neg.inr.inl
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
⊢ G'.Adj u x ↔ ¬G'.Adj v w'

Proof state:
case neg.inr.inl.inl.intro
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
hrl1 : v = u
hrl2 : w = x
⊢ G'.Adj v w'

Tactic:
subst hrl1 hrl2

Result:
case neg.inr.inl.inl.intro
V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
v w w' : V
hww' : w ≠ w'
h1 : G.Adj v w'
hnadj : ¬G'.Adj v w
hu' : ∀ (u' : V), u' ≠ v → G.Adj w u' → G'.Adj w u'
hx' : ∀ (x' : V), x' ≠ w → G.Adj x' v → G'.Adj x' v
hadj : ¬G.Adj v w
hr : (v = v ∧ w = w ∨ v = w ∧ w = v) ∧ v ≠ w
⊢ G'.Adj v w'

Proof state:
case neg.inl.inr
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ G'.Adj v w ↔ ¬G'.Adj u x

Tactic:
simp only [hnadj, not_false_eq_true, iff_true]

Result:
case neg.inl.inr
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ G'.Adj v w

Proof state:
case neg.inr.inl.inr.intro
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
hrr1 : v = x
hrr2 : w = u
⊢ G'.Adj v w'

Tactic:
aesop

Result:
no goals