awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : NoAccidental t
x y z : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
hxz : (graph t).Adj x z
hyz : (graph t).Adj y z
a : α
b : β
c : γ
habc : Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c} {x, y, z}
hab : (graph t).Adj (in₀ a) (in₁ b)
hac : (graph t).Adj (in₀ a) (in₂ c)
hbc : (graph t).Adj (in₁ b) (in₂ c)
c' : γ
hc' : (a, b, c') ∈ t
b' : β
hb' : (a, b', c) ∈ t
⊢ (a, b, c) ∈ t
have refine_1 : ∀ (a' : α) (ha' : (a', b, c) ∈ t), (a, b, c) ∈ t
Tactic: obtain ⟨a', ha'⟩ := in₁₂_iff.1 hbc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : NoAccidental t
x y z : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
hxz : (graph t).Adj x z
hyz : (graph t).Adj y z
a : α
b : β
c : γ
habc : Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c} {x, y, z}
hab : (graph t).Adj (in₀ a) (in₁ b)
hac : (graph t).Adj (in₀ a) (in₂ c)
hbc : (graph t).Adj (in₁ b) (in₂ c)
c' : γ
hc' : (a, b, c') ∈ t
b' : β
hb' : (a, b', c) ∈ t
a' : α
ha' : (a', b, c) ∈ t
⊢ (a, b, c) ∈ t
have refine_1 : ∀ (ha' : (a, b, c) ∈ t), (a, b, c) ∈ t
Tactic: obtain rfl | rfl | rfl := NoAccidental.eq_or_eq_or_eq ha' hb' hc'
Cleared hypotheses: a', ha'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : ExplicitDisjoint t
x : Finset (α ⊕ β ⊕ γ)
⊢ x ∈ (↑(map toTriangle t) : Set (Finset (α ⊕ β ⊕ γ))) →
    ∀ ⦃y : Finset (α ⊕ β ⊕ γ)⦄,
      y ∈ (↑(map toTriangle t) : Set (Finset (α ⊕ β ⊕ γ))) →
        x ≠ y → (fun (x y : Finset (α ⊕ β ⊕ γ)) ↦ ((↑x : Set (α ⊕ β ⊕ γ)) ∩ (↑y : Set (α ⊕ β ⊕ γ))).Subsingleton) x y
have simp : ∀ (x_1 : α) (x_2 : β) (x_3 : γ),
  (x_1, x_2, x_3) ∈ t →
    (toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x_1, x_2, x_3) = x →
      ∀ ⦃y : Finset (α ⊕ β ⊕ γ)⦄ (x_4 : α) (x_5 : β) (x_6 : γ),
        (x_4, x_5, x_6) ∈ t →
          (toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x_4, x_5, x_6) = y →
            ¬x = y → ((↑x : Set (α ⊕ β ⊕ γ)) ∩ (↑y : Set (α ⊕ β ⊕ γ))).Subsingleton
Tactic: simp only [Finset.coe_map, Set.mem_image, Finset.mem_coe, Prod.exists, Ne,
    forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' :
  ¬Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x, y, z) : Finset (α ⊕ β ⊕ γ))
⊢ ((↑((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ)) : Set (α ⊕ β ⊕ γ)) ∩
      (↑((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x, y, z) : Finset (α ⊕ β ⊕ γ)) :
        Set (α ⊕ β ⊕ γ))).Subsingleton
have this : (a, b, c) ≠ (x, y, z)
Tactic: have := ne_of_apply_ne _ h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' :
  ¬Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x, y, z) : Finset (α ⊕ β ⊕ γ))
this : (a, b, c) ≠ (x, y, z)
⊢ ((↑((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ)) : Set (α ⊕ β ⊕ γ)) ∩
      (↑((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x, y, z) : Finset (α ⊕ β ⊕ γ)) :
        Set (α ⊕ β ⊕ γ))).Subsingleton
have this₁ : a = x → b = y → ¬c = z
Tactic: simp only [Ne, Prod.mk_inj, not_and] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' :
  ¬Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x, y, z) : Finset (α ⊕ β ⊕ γ))
this : a = x → b = y → ¬c = z
⊢ ¬(a = x ∧ b = y) ∧ ¬(a = x ∧ c = z) ∧ ¬(b = y ∧ c = z)
have refine_1 : ¬(a = x ∧ b = y)
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' :
  ¬Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x, y, z) : Finset (α ⊕ β ⊕ γ))
this : a = x → b = y → ¬c = z
refine_1 : ¬(a = x ∧ b = y)
⊢ ¬(a = x ∧ b = y) ∧ ¬(a = x ∧ c = z) ∧ ¬(b = y ∧ c = z)
have refine_2 : ¬(a = x ∧ c = z)
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' :
  ¬Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x, y, z) : Finset (α ⊕ β ⊕ γ))
this : a = x → b = y → ¬c = z
refine_1 : ¬(a = x ∧ b = y)
refine_2 : ¬(a = x ∧ c = z)
⊢ ¬(a = x ∧ b = y) ∧ ¬(a = x ∧ c = z) ∧ ¬(b = y ∧ c = z)
have refine_3 : ¬(b = y ∧ c = z)
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : NoAccidental t
⊢ (graph t).cliqueSet 3 = (⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) '' (↑t : Set (α × β × γ))
have h : ∀ (x : Finset (α ⊕ β ⊕ γ)),
  x ∈ (graph t).cliqueSet 3 ↔
    Membership.mem (γ := Set (Finset (α ⊕ β ⊕ γ)))
      ((⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) '' (↑t : Set (α × β × γ))) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : Fintype α
inst_4 : Fintype β
inst_5 : Fintype γ
inst_6 : NoAccidental t
⊢ (↑((graph t).cliqueFinset 3) : Set (Finset (α ⊕ β ⊕ γ))) =
    (↑(image (⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) t) : Set (Finset (α ⊕ β ⊕ γ)))
have push_cast : (graph t).cliqueSet 3 = (⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) '' (↑t : Set (α × β × γ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : Fintype α
inst_4 : Fintype β
inst_5 : Fintype γ
inst_6 : NoAccidental t
⊢ #((graph t).cliqueFinset 3) = #t
have rw : #(map toTriangle t) = #t
Tactic: rw [cliqueFinset_eq_map, card_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : Fintype α
inst_4 : Fintype β
inst_5 : Fintype γ
inst_6 : NoAccidental t
rw : #(map toTriangle t) = #t
⊢ #((graph t).cliqueFinset 3) = #t
have rw₁ : #t = #t
Tactic: rw [cliqueFinset_eq_map, card_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : ExplicitDisjoint t
inst_1 : NoAccidental t
⊢ (graph t).LocallyLinear
have refine_1 : (graph t).EdgeDisjointTriangles
Tactic: refine ⟨?_, fun x y hxy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : ExplicitDisjoint t
inst_1 : NoAccidental t
refine_1 : (graph t).EdgeDisjointTriangles
⊢ (graph t).LocallyLinear
have refine_2 : ∀ (x y : α ⊕ β ⊕ γ) (hxy : (graph t).Adj x y), ∃ (s : Finset (α ⊕ β ⊕ γ)), (graph t).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s
Tactic: refine ⟨?_, fun x y hxy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : ExplicitDisjoint t
inst_1 : NoAccidental t
⊢ ((graph t).cliqueSet 3).Pairwise fun (x y : Finset (α ⊕ β ⊕ γ)) ↦
    ((↑x : Set (α ⊕ β ⊕ γ)) ∩ (↑y : Set (α ⊕ β ⊕ γ))).Subsingleton
have h : (graph t).cliqueSet 3 = (↑(map toTriangle t) : Set (Finset (α ⊕ β ⊕ γ)))
Tactic: convert! map_toTriangle_disjoint t
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : ExplicitDisjoint t
inst_1 : NoAccidental t
⊢ (graph t).cliqueSet 3 = (↑(map toTriangle t) : Set (Finset (α ⊕ β ⊕ γ)))
have h : (⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) '' (↑t : Set (α × β × γ)) =
  (↑(map toTriangle t) : Set (Finset (α ⊕ β ⊕ γ)))
Tactic: rw [cliqueSet_eq_image, coe_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : ExplicitDisjoint t
inst_1 : NoAccidental t
h :
  (⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) '' (↑t : Set (α × β × γ)) =
    (↑(map toTriangle t) : Set (Finset (α ⊕ β ⊕ γ)))
⊢ (graph t).cliqueSet 3 = (↑(map toTriangle t) : Set (Finset (α ⊕ β ⊕ γ)))
have h₁ : Eq (α := Set (Finset (α ⊕ β ⊕ γ))) ((⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) '' (↑t : Set (α × β × γ)))
  ((⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) '' (↑t : Set (α × β × γ)))
Tactic: rw [cliqueSet_eq_image, coe_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : ExplicitDisjoint t
inst_1 : NoAccidental t
x y : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
⊢ ∃ (s : Finset (α ⊕ β ⊕ γ)), (graph t).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s
have refine_2 : ∀ (z : α × β × γ) (hz : z ∈ t)
  (hxy :
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) x ∧
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) y),
  ∃ (s : Finset (α ⊕ β ⊕ γ)), (graph t).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s
Tactic: obtain ⟨z, hz, hxy⟩ := exists_mem_toTriangle hxy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : ExplicitDisjoint t
inst_1 : NoAccidental t
⊢ (graph t).LocallyLinear
have refine_1 : (graph t).EdgeDisjointTriangles
Tactic: classical
  refine ⟨?_, fun x y hxy ↦ ?_⟩
  · unfold EdgeDisjointTriangles
    convert! map_toTriangle_disjoint t
    rw [cliqueSet_eq_image, coe_map]
  · obtain ⟨z, hz, hxy⟩ := exists_mem_toTriangle hxy
    exact ⟨_, toTriangle_is3Clique hz, hxy⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : ExplicitDisjoint t
inst_1 : NoAccidental t
refine_1 : (graph t).EdgeDisjointTriangles
⊢ (graph t).LocallyLinear
have refine_2 : ∀ (x y : α ⊕ β ⊕ γ) (hxy : (graph t).Adj x y), ∃ (s : Finset (α ⊕ β ⊕ γ)), (graph t).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s
Tactic: classical
  refine ⟨?_, fun x y hxy ↦ ?_⟩
  · unfold EdgeDisjointTriangles
    convert! map_toTriangle_disjoint t
    rw [cliqueSet_eq_image, coe_map]
  · obtain ⟨z, hz, hxy⟩ := exists_mem_toTriangle hxy
    exact ⟨_, toTriangle_is3Clique hz, hxy⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
⊢ ∃ (G' : SimpleGraph V), G'.IsAlternating M.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
have refine_1 : ∀ (u' : V) (hu'x : u' ≠ x) (hadj : p.toSubgraph.spanningCoe.Adj a u'), M.spanningCoe.Adj a u'
Tactic: refine ⟨p.toSubgraph.spanningCoe ⊔ edge x a, (hcalt.spanningCoe p.toSubgraph).sup_edge (by simpa)
    (fun u' hu'x hadj ↦ ?_) aux, ?_, ?_, by aesop, sup_le_iff.mpr ⟨hle, fun v w hvw ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
refine_1 : ∀ (u' : V) (hu'x : u' ≠ x) (hadj : p.toSubgraph.spanningCoe.Adj a u'), M.spanningCoe.Adj a u'
⊢ ∃ (G' : SimpleGraph V), G'.IsAlternating M.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
have refine_2 : (p.toSubgraph.spanningCoe ⊔ edge x a).IsCycles
Tactic: refine ⟨p.toSubgraph.spanningCoe ⊔ edge x a, (hcalt.spanningCoe p.toSubgraph).sup_edge (by simpa)
    (fun u' hu'x hadj ↦ ?_) aux, ?_, ?_, by aesop, sup_le_iff.mpr ⟨hle, fun v w hvw ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
refine_1 : ∀ (u' : V) (hu'x : u' ≠ x) (hadj : p.toSubgraph.spanningCoe.Adj a u'), M.spanningCoe.Adj a u'
refine_2 : (p.toSubgraph.spanningCoe ⊔ edge x a).IsCycles
⊢ ∃ (G' : SimpleGraph V), G'.IsAlternating M.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
have refine_3 : ¬(p.toSubgraph.spanningCoe ⊔ edge x a).Adj x b
Tactic: refine ⟨p.toSubgraph.spanningCoe ⊔ edge x a, (hcalt.spanningCoe p.toSubgraph).sup_edge (by simpa)
    (fun u' hu'x hadj ↦ ?_) aux, ?_, ?_, by aesop, sup_le_iff.mpr ⟨hle, fun v w hvw ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
refine_1 : ∀ (u' : V) (hu'x : u' ≠ x) (hadj : p.toSubgraph.spanningCoe.Adj a u'), M.spanningCoe.Adj a u'
refine_2 : (p.toSubgraph.spanningCoe ⊔ edge x a).IsCycles
refine_3 : ¬(p.toSubgraph.spanningCoe ⊔ edge x a).Adj x b
⊢ ∃ (G' : SimpleGraph V), G'.IsAlternating M.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
have refine_4 : ∀ (v w : V) (hvw : (edge x a).Adj v w), (G ⊔ edge a c).Adj v w
Tactic: refine ⟨p.toSubgraph.spanningCoe ⊔ edge x a, (hcalt.spanningCoe p.toSubgraph).sup_edge (by simpa)
    (fun u' hu'x hadj ↦ ?_) aux, ?_, ?_, by aesop, sup_le_iff.mpr ⟨hle, fun v w hvw ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
⊢ (p.toSubgraph.spanningCoe ⊔ edge x a).IsCycles
have refine_2 : ∀ (hadj : s(x, a) ∈ p.edges), False
Tactic: refine hp.isCycles_spanningCoe_toSubgraph_sup_edge hgadj.ne.symm fun hadj ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
Goal:
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
hadj : s(x, a) ∈ p.edges
⊢ False
have hadj₁ : p.toSubgraph.Adj x a
Tactic: rw [← Walk.mem_edges_toSubgraph, Subgraph.mem_edgeSet] at hadj
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
Goal:
V : Type u_1
G G' : SimpleGraph V
inst : Finite V
u : Set V
h : G ≤ G'
ht :
  u.ncard <
    Set.ncard (α :=
      ConnectedComponent (V := (↑(Set.univ \ u) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ u) :
          SimpleGraph (↑(Subgraph.verts (G := G') (Subgraph.deleteVerts ⊤ u)) : Type u_1)))
      (oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u)))
⊢ u.ncard <
    Set.ncard (α :=
      ConnectedComponent (V := (↑(Set.univ \ u) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ u) :
          SimpleGraph (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)))
      (oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u)))
have this : Set.ncard (α :=
    ConnectedComponent (V := (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1))
      (Subgraph.coe (Subgraph.deleteVerts ⊤ u)))
    (oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) ≤
  Set.ncard (α :=
    ConnectedComponent (V := (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1))
      (Subgraph.coe (Subgraph.deleteVerts ⊤ u)))
    (oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u)))
Tactic: have := ncard_oddComponents_mono _ (Subgraph.deleteVerts_mono' (G := G) (G' := G') u h)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
⊢ ∃ (M : G.Subgraph), M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts
have hrep : ConnectedComponent.Represents
  (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents)
  G.deleteUniversalVerts.coe.oddComponents
Tactic: have hrep := ConnectedComponent.Represents.image_out G.deleteUniversalVerts.coe.oddComponents
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents
    (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
⊢ (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) ''
        Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents).ncard ≤
    G.universalVerts.ncard
have h₁ : Set.ncard (α :=
    ConnectedComponent (V := (↑(verts (G := G) (deleteVerts ⊤ G.universalVerts)) : Type u_1))
      (Subgraph.coe (deleteVerts ⊤ G.universalVerts)))
    (oddComponents (Subgraph.coe (deleteVerts ⊤ G.universalVerts))) ≤
  G.universalVerts.ncard
Tactic: simp only [IsTutteViolator, not_lt] at h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h_1 : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents
    (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
h :
  Set.ncard (α :=
      ConnectedComponent (V := (↑(verts (G := G) (deleteVerts ⊤ G.universalVerts)) : Type u_1))
        (Subgraph.coe (deleteVerts ⊤ G.universalVerts)))
      (oddComponents (Subgraph.coe (deleteVerts ⊤ G.universalVerts))) ≤
    G.universalVerts.ncard
⊢ (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) ''
        Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents).ncard ≤
    G.universalVerts.ncard
have rwa : (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents).ncard ≤
  G.universalVerts.ncard
Tactic: rwa [Set.ncard_image_of_injective _ Subtype.val_injective, hrep.ncard_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h_1 : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents
    (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
h :
  Set.ncard (α :=
      ConnectedComponent (V := (↑(verts (G := G) (deleteVerts ⊤ G.universalVerts)) : Type u_1))
        (Subgraph.coe (deleteVerts ⊤ G.universalVerts)))
      (oddComponents (Subgraph.coe (deleteVerts ⊤ G.universalVerts))) ≤
    G.universalVerts.ncard
rwa :
  (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents).ncard ≤
    G.universalVerts.ncard
rwa₁ : Type u_1
⊢ (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) ''
        Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents).ncard ≤
    G.universalVerts.ncard
have rwa₂ : Set { x : V // x ∈ G.deleteUniversalVerts.verts }
Tactic: rwa [Set.ncard_image_of_injective _ Subtype.val_injective, hrep.ncard_eq]
Cleared hypotheses: h