awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' G'' : SimpleGraph V
halt : G.IsAlternating G'
h : G'' ≤ G
⊢ G''.IsAlternating G'

Tactic:
fun _ _ _ hww' hvw hvw' ↦ halt hww' (h hvw) (h hvw')

Premises used: SimpleGraph.IsAlternating
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
v w w' : V
hww' : w ≠ w'
hvw : H.Adj v w
hvv' : H.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
halt hww' hvw.adj_sub hvv'.adj_sub

Premises used: SimpleGraph.Subgraph.Adj.adj_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
v w w' : V
hww' : w ≠ w'
hvw : H.Adj v w
hvv' : H.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
exact halt hww' hvw.adj_sub hvv'.adj_sub

Premises used: SimpleGraph.Subgraph.Adj.adj_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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
pos : ∀ (hadj : G.Adj u x), (G ⊔ edge u x).IsAlternating G'
neg : ∀ (hadj : ¬G.Adj u x), (G ⊔ edge u x).IsAlternating G'
⊢ (G ⊔ edge u x).IsAlternating G'

Tactic:
by_cases hadj : G.Adj u x

Premises used: SimpleGraph.Adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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
pos pos₁ pos₂ pos₃ : G.IsAlternating G'
⊢ (G ⊔ edge u x).IsAlternating G'

Tactic:
rwa [sup_edge_of_adj G hadj]

Premises used: SimpleGraph.sup_edge_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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'
hvw : (G ⊔ edge u x).Adj v w
hvv' : (G ⊔ edge u x).Adj v w'
⊢ G.Adj v w ∨ (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w

Tactic:
simp only [sup_adj, edge_adj] at hvw hvv'

Premises used: SimpleGraph.sup_adj, SimpleGraph.edge_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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'
hvw : (G ⊔ edge u x).Adj v w
hvv' : (G ⊔ edge u x).Adj v w'
hvw₁ : G.Adj v w ∨ (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
⊢ G.Adj v w' ∨ (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'

Tactic:
simp only [sup_adj, edge_adj] at hvw hvv'

Premises used: SimpleGraph.sup_adj, SimpleGraph.edge_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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'
hvw : G.Adj v w ∨ (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
hvv' : G.Adj v w' ∨ (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
neg : ∀ (hl : G.Adj v w), G'.Adj v w ↔ ¬G'.Adj v w'
neg₁ : ∀ (hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w), G'.Adj v w ↔ ¬G'.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
obtain hl | hr := hvw
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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'
hvv' : G.Adj v w' ∨ (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
hl : G.Adj v w
neg : ∀ (h1 : G.Adj v w'), G'.Adj v w ↔ ¬G'.Adj v w'
neg₁ : ∀ (h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'), G'.Adj v w ↔ ¬G'.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
obtain h1 | h2 := hvv'
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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'
hvv' : G.Adj v w' ∨ (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
neg : ∀ (h1 : G.Adj v w'), G'.Adj v w ↔ ¬G'.Adj v w'
neg₁ : ∀ (h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'), G'.Adj v w ↔ ¬G'.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
obtain h1 | h2 := hvv'
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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
h1 : G.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
halt hww' hl h1
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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
h1 : G.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
exact halt hww' hl h1
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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'
neg : G'.Adj v w ↔ ¬G'.Adj u x
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

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

Premises used: SimpleGraph.adj_congr_of_sym2
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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'
neg : G'.Adj v w
⊢ G'.Adj v w ↔ ¬G'.Adj u x

Tactic:
simp only [hnadj, not_false_eq_true, iff_true]

Premises used: iff_true, not_false_eq_true
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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'
neg :
  ∀ (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
neg₁ : ∀ (h2r1 : v = x) (h2r2 : w' = u), G'.Adj v w
⊢ G'.Adj v w

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

Premises used: And.left, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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:
(hx' _ hww' hl.symm).symm

Premises used: SimpleGraph.Adj.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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

Premises used: SimpleGraph.Adj.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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'
⊢ s(v, w) = s(u, x)

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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'
neg : G'.Adj u x ↔ ¬G'.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

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

Premises used: SimpleGraph.adj_congr_of_sym2
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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'
neg : G'.Adj v w'
⊢ G'.Adj u x ↔ ¬G'.Adj v w'

Tactic:
simp only [hnadj, false_iff, not_not]

Premises used: Classical.not_not, false_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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'
neg :
  ∀ (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'
neg₁ : ∀ (hrr1 : v = x) (hrr2 : w = u), G'.Adj v w'
⊢ G'.Adj v w'

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

Premises used: And.left, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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:
(hx' _ hww'.symm h1.symm).symm

Premises used: SimpleGraph.Adj.symm, Ne.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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

Premises used: SimpleGraph.Adj.symm, Ne.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
rw : ∀ (v : V), ∃! w : V, Adj (G := M.spanningCoe ∆ G') ⊤ v w
⊢ IsPerfectMatching.{u_1} (V := V) (G := M.spanningCoe ∆ G') ⊤

Tactic:
rw [Subgraph.isPerfectMatching_iff]

Premises used: SimpleGraph.Subgraph.isPerfectMatching_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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
obtain :
  ∀ (w : V) (hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w),
    ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w
⊢ ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w

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

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
pos : ∀ (h : G'.Adj v w), ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w
neg : ∀ (h : ¬G'.Adj v w), ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w
⊢ ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w

Tactic:
by_cases h : G'.Adj v w

Premises used: SimpleGraph.Adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
h : G'.Adj v w
pos : ∀ (w' : V) (hw' : w ≠ w' ∧ G'.Adj v w'), ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w
⊢ ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w

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

Premises used: SimpleGraph.IsCycles.other_adj_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ 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

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ 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:
have hmadj : M.Adj v w ↔ ¬M.Adj v w' := by simpa using hG' hw'.1 h hw'.2
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ 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'
h₁ :
  (fun (w : V) ↦ Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w) w' ∧
    ∀ (y : V), (fun (w : V) ↦ Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w) y → y = w'
⊢ ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w

Tactic:
use w'
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ 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'
h₁ : ∀ (y : V), M.Adj v y ∧ ¬G'.Adj v y ∨ G'.Adj v y ∧ ¬M.Adj v y → y = w'
⊢ (fun (w : V) ↦ Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w) w' ∧
    ∀ (y : V), (fun (w : V) ↦ Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w) y → y = w'

Tactic:
simp only [Subgraph.top_adj, SimpleGraph.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]

Premises used: and_self, not_true_eq_false, SimpleGraph.sup_adj, SimpleGraph.sdiff_adj, And.right, And.left, Iff.mp, SimpleGraph.Subgraph.top_adj, SimpleGraph.Subgraph.spanningCoe_adj, not_false_eq_true, or_true, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ 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:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ 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
h₁ : ∀ (w'' : V) (hw'' : y ≠ w'' ∧ G'.Adj v w''), y = w'
⊢ y = w'

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

Premises used: And.left, SimpleGraph.IsCycles.other_adj_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ 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''
h₁ : ∀ (hc : y ≠ w'), False
⊢ y = w'

Tactic:
by_contra! hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ 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

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ 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]
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
h : ¬G'.Adj v w
h₁ :
  (fun (w : V) ↦ Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w) w ∧
    ∀ (y : V), (fun (w : V) ↦ Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w) y → y = w
⊢ ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w

Tactic:
use w
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
h : ¬G'.Adj v w
h₁ : ∀ (y : V), M.Adj v y ∧ ¬G'.Adj v y ∨ G'.Adj v y ∧ ¬M.Adj v y → y = w
⊢ (fun (w : V) ↦ Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w) w ∧
    ∀ (y : V), (fun (w : V) ↦ Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w) y → y = w

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

Premises used: and_self, not_true_eq_false, SimpleGraph.sup_adj, SimpleGraph.sdiff_adj, And.left, SimpleGraph.Subgraph.top_adj, or_false, SimpleGraph.Subgraph.spanningCoe_adj, not_false_eq_true, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ 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:
hw.2 _ hl.1

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ 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

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
h : ¬G'.Adj v w
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
h₁ : ∀ (w' : V) (hw' : y ≠ w' ∧ G'.Adj v w'), y = w
⊢ y = w

Tactic:
have ⟨w', hw'⟩ := hG'cyc.other_adj_of_adj hr.1
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ 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

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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 : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ 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]
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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'
obtain :
  ∀ (v1 : V) (hm1 : M.Adj v v1) (hv1 : ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = v1),
    M.spanningCoe.Adj v w ↔ ¬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)

Premises used: And.right, And.left