awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
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
hM1xb₁ : M1.Adj x b
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have hM2ac₁ : M2.Adj a c
Tactic: simp only [not_not] at hM1xb hM2ac
Cleared hypotheses: hM1xb, hM2ac
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
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
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have hM1nac : ¬M1.Adj a c
Tactic: have hM1nac : ¬M1.Adj a c := fun h ↦ by simpa [hnGac, edge_adj, hnac, hxa.ne, hnbc.symm, hab.ne]
    using h.adj_sub
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
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
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
Tactic: have hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = (G ⊔ edge a c) ⊔ edge x b := by grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
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
this :
  ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have obtain : ∀ (G' : SimpleGraph V) (hG' : G'.IsAlternating M2.spanningCoe) (hG'cyc : G'.IsCycles) (hG'xb : ¬G'.Adj x b)
  (hnG'ac : G'.Adj a c) (hle : G' ≤ G ⊔ edge a c), ∃ (M : G.Subgraph), M.IsPerfectMatching
Tactic: obtain ⟨G', hG', hG'cyc, hG'xb, hnG'ac, hle⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
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
G' : SimpleGraph V
hG' : G'.IsAlternating M2.spanningCoe
hG'cyc : G'.IsCycles
hG'xb : ¬G'.Adj x b
hnG'ac : G'.Adj a c
hle : G' ≤ G ⊔ edge a c
⊢ M2.spanningCoe ∆ G' ≤ G
have apply : Disjoint (M2.spanningCoe ∆ G') (edge a c)
Tactic: apply Disjoint.left_le_of_le_sup_right (symmDiff_le (le_sup_of_le_right M2.spanningCoe_le)
        (le_sup_of_le_right hle))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
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
G' : SimpleGraph V
hG' : G'.IsAlternating M2.spanningCoe
hG'cyc : G'.IsCycles
hG'xb : ¬G'.Adj x b
hnG'ac : G'.Adj a c
hle : G' ≤ G ⊔ edge a c
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have this : M2.spanningCoe ∆ G' ≤ G
Tactic: have : M2.spanningCoe ∆ G' ≤ G := by
      apply Disjoint.left_le_of_le_sup_right (symmDiff_le (le_sup_of_le_right M2.spanningCoe_le)
        (le_sup_of_le_right hle))
      simp [disjoint_edge, symmDiff_def, hM2ac, hnG'ac]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
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
G' : SimpleGraph V
hG' : G'.IsAlternating M2.spanningCoe
hG'cyc : G'.IsCycles
hG'xb : ¬G'.Adj x b
hnG'ac : G'.Adj a c
hle : G' ≤ G ⊔ edge a c
this : M2.spanningCoe ∆ G' ≤ G
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have h : (toSubgraph (M2.spanningCoe ∆ G') this).IsPerfectMatching
Tactic: use (G.toSubgraph (symmDiff M2.spanningCoe G') this)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
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
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have neg : ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
Tactic: suffices ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧
      G'.Adj a c ∧ G' ≤ G ⊔ edge a c by
    obtain ⟨G', hG', hG'cyc, hG'xb, hnG'ac, hle⟩ := this
    have : M2.spanningCoe ∆ G' ≤ G := by
      apply Disjoint.left_le_of_le_sup_right (symmDiff_le (le_sup_of_le_right M2.spanningCoe_le)
        (le_sup_of_le_right hle))
      simp [disjoint_edge, symmDiff_def, hM2ac, hnG'ac]
    use (G.toSubgraph (symmDiff M2.spanningCoe G') this)
    apply hM2.symmDiff_of_isAlternating hG' hG'cyc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
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
⊢ ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
have hcalt : cycles.IsAlternating M2.spanningCoe
Tactic: have hcalt : cycles.IsAlternating M2.spanningCoe := hM1.isAlternating_symmDiff_right hM2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
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
⊢ ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
have hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
Tactic: have hcycles := Subgraph.IsPerfectMatching.symmDiff_isCycles hM1 hM2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
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
⊢ ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
have hcac : cycles.Adj a c
Tactic: have hcac : cycles.Adj a c := by simp [cycles, symmDiff_def, hM2ac, hM1nac]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
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
⊢ ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
have hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
Tactic: have hM1sub := Subgraph.spanningCoe_le M1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
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
⊢ ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
have hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
Tactic: have hM2sub := Subgraph.spanningCoe_le M2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
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
⊢ (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x b
have refine : cycles ≤ G ⊔ edge a c ⊔ edge x b
Tactic: refine le_trans (spanningCoe_induce_le cycles (cycles.connectedComponentMk c).supp) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
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
⊢ cycles ≤ G ⊔ edge a c ⊔ edge x b
have simp : M1.spanningCoe ∆ M2.spanningCoe ≤ G ⊔ edge x b ⊔ (G ⊔ edge a c)
Tactic: simp only [← hsupG, cycles]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
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
⊢ ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
have induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
  G ⊔ edge a c ⊔ edge x b
Tactic: have induce_le : ((cycles.connectedComponentMk c).toSimpleGraph).spanningCoe ≤
      (G ⊔ edge a c) ⊔ edge x b := by
    refine le_trans (spanningCoe_induce_le cycles (cycles.connectedComponentMk c).supp) ?_
    simp only [← hsupG, cycles]
    exact le_trans (by apply symmDiff_le_sup) (sup_le_sup hM1sub hM2sub)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
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
⊢ ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
have pos : ∀ (hxc : x ∉ (cycles.connectedComponentMk c).supp),
  ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
Tactic: by_cases! hxc : x ∉ (cycles.connectedComponentMk c).supp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
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
pos :
  ∀ (hxc : x ∉ (cycles.connectedComponentMk c).supp),
    ∃ (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
have neg : ∀ (hxc : x ∈ (cycles.connectedComponentMk c).supp),
  ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
Tactic: by_cases! hxc : x ∉ (cycles.connectedComponentMk c).supp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
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
⊢ ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
have h : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s :=
        (↑(cycles.connectedComponentMk c) : Set V)).IsAlternating
    M2.spanningCoe ∧
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)).IsCycles ∧
    ¬(cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)).Adj x
          b ∧
      (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)).Adj a
          c ∧
        (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
          G ⊔ edge a c
Tactic: use (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
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
⊢ (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s :=
          (↑(cycles.connectedComponentMk c) : Set V)).IsAlternating
      M2.spanningCoe ∧
    (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s :=
          (↑(cycles.connectedComponentMk c) : Set V)).IsCycles ∧
      ¬(cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)).Adj x
            b ∧
        (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)).Adj
            a c ∧
          (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
            G ⊔ edge a c
have h : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)).IsCycles ∧
  ¬(cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)).Adj x b ∧
    (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)).Adj a
        c ∧
      (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
        G ⊔ edge a c
Tactic: refine ⟨hcalt.mono (spanningCoe_induce_le cycles (cycles.connectedComponentMk c).supp), ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
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
⊢ (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)).IsCycles ∧
    ¬(cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)).Adj x
          b ∧
      (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)).Adj a
          c ∧
        (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
          G ⊔ edge a c
have h : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)).IsCycles ∧
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c
Tactic: simp only [ConnectedComponent.adj_spanningCoe_toSimpleGraph, hxc, hcac, false_and,
      not_false_eq_true, ConnectedComponent.mem_supp_iff, ConnectedComponent.eq, and_true,
      true_and, hcac.reachable]