awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
x' : V
hx' : Membership.mem (γ := Finset V) {x, b} x'
hx'p : x' ∈ p'.support
htw : ∀ (t : V), Membership.mem (γ := Finset V) {x, b} t → t ∈ (p'.takeUntil x' hx'p).support → t = x'
h : ¬a = x'
⊢ ¬(p'.takeUntil x' hx'p).Nil

Tactic:
rw [Walk.nil_takeUntil]

Premises used: SimpleGraph.Walk.nil_takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
x' : V
hx' : Membership.mem (γ := Finset V) {x, b} x'
hx'p : x' ∈ p'.support
htw : ∀ (t : V), Membership.mem (γ := Finset V) {x, b} t → t ∈ (p'.takeUntil x' hx'p).support → t = x'
⊢ ¬a = x'

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
x' : V
hx' : Membership.mem (γ := Finset V) {x, b} x'
hx'p : x' ∈ p'.support
htw : ∀ (t : V), Membership.mem (γ := Finset V) {x, b} t → t ∈ (p'.takeUntil x' hx'p).support → t = x'
⊢ (p'.takeUntil x' hx'p).toSubgraph.Adj a (p'.takeUntil x' hx'p).snd

Tactic:
have : (p'.takeUntil x' hx'p).toSubgraph.Adj a (p'.takeUntil x' hx'p).snd := by
      apply Walk.toSubgraph_adj_snd
      rw [Walk.nil_takeUntil]
      grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this_1 : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
x' : V
hx' : Membership.mem (γ := Finset V) {x, b} x'
hx'p : x' ∈ p'.support
htw : ∀ (t : V), Membership.mem (γ := Finset V) {x, b} t → t ∈ (p'.takeUntil x' hx'p).support → t = x'
this : (p'.takeUntil x' hx'p).toSubgraph.Adj a (p'.takeUntil x' hx'p).snd
refine_1 : x' ≠ a
⊢ (p'.takeUntil x' hx'p).toSubgraph.Adj a c

Tactic:
rwa [Walk.snd_takeUntil, hp'.2.1] at this

Premises used: SimpleGraph.Walk.snd_takeUntil, And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this_1 : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
x' : V
hx' : Membership.mem (γ := Finset V) {x, b} x'
hx'p : x' ∈ p'.support
htw : ∀ (t : V), Membership.mem (γ := Finset V) {x, b} t → t ∈ (p'.takeUntil x' hx'p).support → t = x'
this : (p'.takeUntil x' hx'p).toSubgraph.Adj a (p'.takeUntil x' hx'p).snd
⊢ x' = x ∨ x' = b

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton] at hx'

Premises used: Finset.mem_singleton, Finset.mem_insert
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
a b c : V
M2 : (G ⊔ edge a c).Subgraph
hab : G.Adj a b
hnGac : ¬G.Adj a c
hnac : a ≠ c
hnbc : b ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this_1 : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x' b).Subgraph
hxa : G.Adj x' a
hnGxb : ¬G.Adj x' b
hnxb : x' ≠ b
hnxc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x' b
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x' b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x' b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x' b
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x' b
hxc : x' ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
hx'p : x' ∈ p'.support
htw : ∀ (t : V), Membership.mem (γ := Finset V) {x', b} t → t ∈ (p'.takeUntil x' hx'p).support → t = x'
this : (p'.takeUntil x' hx'p).toSubgraph.Adj a (p'.takeUntil x' hx'p).snd
⊢ x' ≠ a

Tactic:
hxa.ne

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this_1 : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
hx'p : x' ∈ p'.support
htw : ∀ (t : V), Membership.mem (γ := Finset V) {x, x'} t → t ∈ (p'.takeUntil x' hx'p).support → t = x'
this : (p'.takeUntil x' hx'p).toSubgraph.Adj a (p'.takeUntil x' hx'p).snd
⊢ x' ≠ a

Tactic:
hab.ne.symm

Premises used: SimpleGraph.Adj.ne, Ne.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
a b c : V
M2 : (G ⊔ edge a c).Subgraph
hab : G.Adj a b
hnGac : ¬G.Adj a c
hnac : a ≠ c
hnbc : b ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this_1 : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x' b).Subgraph
hxa : G.Adj x' a
hnGxb : ¬G.Adj x' b
hnxb : x' ≠ b
hnxc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x' b
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x' b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x' b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x' b
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x' b
hxc : x' ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
hx'p : x' ∈ p'.support
htw : ∀ (t : V), Membership.mem (γ := Finset V) {x', b} t → t ∈ (p'.takeUntil x' hx'p).support → t = x'
this : (p'.takeUntil x' hx'p).toSubgraph.Adj a (p'.takeUntil x' hx'p).snd
⊢ x' ≠ a

Tactic:
exacts [hxa.ne, hab.ne.symm]

Premises used: SimpleGraph.Adj.ne, Ne.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
neg :
  ∀ (x' : V) (hx' : Membership.mem (γ := Finset V) {x, b} x') (p : cycles.Walk a x') (hp : p.IsPath)
    (hpac : p.toSubgraph.Adj a c) (hnpxb : ¬p.toSubgraph.Adj x b),
    ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
⊢ ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c

Tactic:
obtain ⟨x', hx', p, hp, hpac, hnpxb⟩ :
      ∃ x' ∈ ({x, b} : Finset V), ∃ (p : cycles.Walk a x'), p.IsPath ∧
        p.toSubgraph.Adj a c ∧ ¬p.toSubgraph.Adj x b := by
    obtain ⟨p, hp⟩ := hcycles.exists_cycle_toSubgraph_verts_eq_connectedComponentSupp hacc
      ⟨_, hcac⟩
    obtain ⟨p', hp'⟩ := hp.1.exists_isCycle_snd_verts_eq (by
      rwa [hp.1.adj_toSubgraph_iff_of_isCycles hcycles (hp.2 ▸ hacc)])
    obtain ⟨x', hx', hx'p, htw⟩ := Walk.exists_mem_support_forall_mem_support_imp_eq {x, b} <| by
      use x
      simp only [Finset.mem_filter, Finset.mem_insert, Finset.mem_singleton, true_or, true_and]
      rwa [← @Walk.mem_verts_toSubgraph, hp'.2.2, hp.2]
    refine ⟨x', hx', p'.takeUntil x' hx'p, hp'.1.isPath_takeUntil hx'p, ?_, fun h ↦ ?_⟩; swap
    · simp [htw _ (by simp) (Walk.mem_support_of_adj_toSubgraph h.symm),
        htw _ (by simp) (Walk.mem_support_of_adj_toSubgraph h)] at hnxb
    have : (p'.takeUntil x' hx'p).toSubgraph.Adj a (p'.takeUntil x' hx'p).snd := by
      apply Walk.toSubgraph_adj_snd
      rw [Walk.nil_takeUntil]
      grind
    rwa [Walk.snd_takeUntil, hp'.2.1] at this
    simp only [Finset.mem_insert, Finset.mem_singleton] at hx'
    obtain rfl | rfl := hx'
    exacts [hxa.ne, hab.ne.symm]

Premises used: Insert.insert, Singleton.singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
x' : V
hx' : Membership.mem (γ := Finset V) {x, b} x'
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
⊢ ¬p.toSubgraph.spanningCoe.Adj x b

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
x' : V
hx' : Membership.mem (γ := Finset V) {x, b} x'
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
rw : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
⊢ p.toSubgraph.spanningCoe ≤ G ⊔ edge a c

Tactic:
rw [← sdiff_edge _ (by simpa : ¬p.toSubgraph.spanningCoe.Adj x b), sdiff_le_iff']

Premises used: sdiff_le_iff', SimpleGraph.sdiff_edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
x' : V
hx' : Membership.mem (γ := Finset V) {x, b} x'
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
v w : V
hvw : p.toSubgraph.spanningCoe.Adj v w
a₁ : (M1.spanningCoe ⊔ M2.spanningCoe).Adj v w
⊢ (G ⊔ edge a c ⊔ edge x b).Adj v w

Tactic:
apply hsupG ▸ sup_le_sup hM1sub hM2sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
x' : V
hx' : Membership.mem (γ := Finset V) {x, b} x'
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
v w : V
hvw : p.toSubgraph.spanningCoe.Adj v w
⊢ cycles.Adj v w

Tactic:
have := p.toSubgraph.spanningCoe_le hvw
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this_1 : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
x' : V
hx' : Membership.mem (γ := Finset V) {x, b} x'
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
v w : V
hvw : p.toSubgraph.spanningCoe.Adj v w
this : (M1.spanningCoe \ M2.spanningCoe ⊔ M2.spanningCoe \ M1.spanningCoe).Adj v w
⊢ (M1.spanningCoe ⊔ M2.spanningCoe).Adj v w

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
x' : V
hx' : Membership.mem (γ := Finset V) {x, b} x'
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
⊢ p.toSubgraph.spanningCoe ≤ G ⊔ edge a c

Tactic:
have hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c := by
    rw [← sdiff_edge _ (by simpa : ¬p.toSubgraph.spanningCoe.Adj x b), sdiff_le_iff']
    intro v w hvw
    apply hsupG ▸ sup_le_sup hM1sub hM2sub
    have := p.toSubgraph.spanningCoe_le hvw
    simp only [cycles, symmDiff_def] at this
    aesop