awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
sm : G.IsMaximumClique s
sc : G.IsClique (↑s : Set α)
⊢ #s = G.cliqueNum
have sm₁ : ∀ (t : Finset α), G.IsClique (↑t : Set α) → #t ≤ #s
Tactic: obtain ⟨sc, sm⟩ := sm
Cleared hypotheses: sm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
sc : G.IsClique (↑s : Set α)
sm : ∀ (t : Finset α), G.IsClique (↑t : Set α) → #t ≤ #s
⊢ #s = G.cliqueNum
have obtain : ∀ (t : Finset α) (tc : G.IsClique (↑t : Set α)) (tcard : #t = G.cliqueNum), #s = G.cliqueNum
Tactic: obtain ⟨t, tc, tcard⟩ := G.exists_isNClique_cliqueNum
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
⊢ ∃ (s : Finset α), G.IsMaximumClique s
have obtain : ∀ (s : Finset α) (snc : G.IsNClique G.cliqueNum s), ∃ (s : Finset α), G.IsMaximumClique s
Tactic: obtain ⟨s, snc⟩ := G.exists_isNClique_cliqueNum
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
n : ℕ
⊢ G.cliqueFinset n = ∅ ↔ G.CliqueFree n
have simp_rw : G.cliqueFinset n = ∅ ↔ ∀ (t : Finset α), ¬G.IsNClique n t
Tactic: simp_rw [CliqueFree, eq_empty_iff_forall_notMem, mem_cliqueFinset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
n : ℕ
simp_rw : G.cliqueFinset n = ∅ ↔ ∀ (t : Finset α), ¬G.IsNClique n t
⊢ G.cliqueFinset n = ∅ ↔ G.CliqueFree n
have simp_rw₁ : (∀ (x : Finset α), x ∉ G.cliqueFinset n) ↔ ∀ (t : Finset α), ¬G.IsNClique n t
Tactic: simp_rw [CliqueFree, eq_empty_iff_forall_notMem, mem_cliqueFinset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
n : ℕ
⊢ #(G.cliqueFinset n) ≤ (Fintype.card α).choose n
have rw : #(G.cliqueFinset n) ≤ Finset.card.{u_1} (α := Finset α) (powersetCard n univ)
Tactic: rw [← card_univ, ← card_powersetCard]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
n : ℕ
⊢ #(G.cliqueFinset n) ≤ Finset.card.{u_1} (α := Finset α) (powersetCard n univ)
have refine : ∀ s ∈ G.cliqueFinset n, Membership.mem (γ := Finset (Finset α)) (powersetCard n univ) s
Tactic: refine card_mono fun s => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
n : ℕ
inst_3 : Fintype β
inst_4 : DecidableEq β
f : α ↪ β
hn : n ≠ 1
⊢ (↑(cliqueFinset (SimpleGraph.map (⇑f : (a : α) → β) G) n) : Set (Finset β)) =
    (↑(map { toFun := map f, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) }
          (G.cliqueFinset n)) :
      Set (Finset β))
have simp_rw : cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n =
  (↑(map { toFun := map f, inj' := sorry : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) }
        (G.cliqueFinset n)) :
    Set (Finset β))
Tactic: simp_rw [coe_cliqueFinset, cliqueSet_map hn, coe_map, coe_cliqueFinset, Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
n : ℕ
inst_3 : Fintype β
inst_4 : DecidableEq β
f : α ↪ β
hn : n ≠ 1
simp_rw :
  cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n =
    (↑(map { toFun := map f, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) }
          (G.cliqueFinset n)) :
      Set (Finset β))
⊢ (↑(cliqueFinset (SimpleGraph.map (⇑f : (a : α) → β) G) n) : Set (Finset β)) =
    (↑(map { toFun := map f, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) }
          (G.cliqueFinset n)) :
      Set (Finset β))
have simp_rw₁ : map f '' G.cliqueSet n =
  (↑(map { toFun := map f, inj' := sorry : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) }
        (G.cliqueFinset n)) :
    Set (Finset β))
Tactic: simp_rw [coe_cliqueFinset, cliqueSet_map hn, coe_map, coe_cliqueFinset, Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
n : ℕ
inst_3 : Fintype β
inst_4 : DecidableEq β
f : α ↪ β
hn : n ≠ 1
simp_rw :
  cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n =
    (↑(map { toFun := map f, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) }
          (G.cliqueFinset n)) :
      Set (Finset β))
simp_rw₁ :
  map f '' G.cliqueSet n =
    (↑(map { toFun := map f, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) }
          (G.cliqueFinset n)) :
      Set (Finset β))
⊢ (↑(cliqueFinset (SimpleGraph.map (⇑f : (a : α) → β) G) n) : Set (Finset β)) =
    (↑(map { toFun := map f, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) }
          (G.cliqueFinset n)) :
      Set (Finset β))
have simp_rw₂ : map f '' G.cliqueSet n =
  (⇑{ toFun := map f, inj' := sorry : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) } :
      (a : Finset α) → Finset β) ''
    (↑(G.cliqueFinset n) : Set (Finset α))
Tactic: simp_rw [coe_cliqueFinset, cliqueSet_map hn, coe_map, coe_cliqueFinset, Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
n : ℕ
inst_3 : Fintype β
inst_4 : DecidableEq β
f : α ↪ β
hn : n ≠ 1
simp_rw :
  cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n =
    (↑(map { toFun := map f, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) }
          (G.cliqueFinset n)) :
      Set (Finset β))
simp_rw₁ :
  map f '' G.cliqueSet n =
    (↑(map { toFun := map f, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) }
          (G.cliqueFinset n)) :
      Set (Finset β))
simp_rw₂ :
  map f '' G.cliqueSet n =
    (⇑{ toFun := map f, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) } :
        (a : Finset α) → Finset β) ''
      (↑(G.cliqueFinset n) : Set (Finset α))
⊢ (↑(cliqueFinset (SimpleGraph.map (⇑f : (a : α) → β) G) n) : Set (Finset β)) =
    (↑(map { toFun := map f, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) }
          (G.cliqueFinset n)) :
      Set (Finset β))
have simp_rw₃ : map f '' G.cliqueSet n =
  (⇑{ toFun := map f, inj' := sorry : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) } :
      (a : Finset α) → Finset β) ''
    G.cliqueSet n
Tactic: simp_rw [coe_cliqueFinset, cliqueSet_map hn, coe_map, coe_cliqueFinset, Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
inst_3 : Fintype β
inst_4 : DecidableEq β
e : α ≃ β
n : ℕ
⊢ (↑(cliqueFinset (SimpleGraph.map (⇑e : (a : α) → β) G) n) : Set (Finset β)) =
    (↑(map { toFun := map e.toEmbedding, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) }
          (G.cliqueFinset n)) :
      Set (Finset β))
have push_cast : Eq.{u_2 + 1} (α := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) n)
  ((⇑{ toFun := map e.toEmbedding, inj' := sorry : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) } :
      (a : Finset α) → Finset β) ''
    G.cliqueSet n)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
he : e ∈ G.edgeSet
⊢ Set.Nonempty.{u_1} (α := α) {b : α | b ∈ sᶜ ∧ b ∈ e}
have mk : ∀ (v w : α) (he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet),
  Set.Nonempty.{u_1} (α := α) {b : α | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)}
Tactic: obtain ⟨v, w⟩ := e
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
⊢ Set.Nonempty.{u_1} (α := α) {b : α | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)}
have mk : ∀ (c : Eq.{u_1 + 1} (α := Set α) {b : α | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} ∅), False
Tactic: by_contra! c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : Eq.{u_1 + 1} (α := Set α) {b : α | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} ∅
⊢ False
have mk : (v, w).1 ∈ s
Tactic: refine indA ?_ ?_ he.ne he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : Eq.{u_1 + 1} (α := Set α) {b : α | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} ∅
mk : (v, w).1 ∈ s
⊢ False
have mk₁ : (v, w).2 ∈ s
Tactic: refine indA ?_ ?_ he.ne he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
⊢ G.IsIndepSet (G.neighborSet v)
have by_contra : ∀ (nind : ¬G.IsIndepSet (G.neighborSet v)), False
Tactic: by_contra nind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
nind : ¬G.IsIndepSet (G.neighborSet v)
⊢ False
have nind₁ : ¬∀ ⦃x : α⦄, x ∈ G.neighborSet v → ∀ ⦃y : α⦄, y ∈ G.neighborSet v → x ≠ y → ¬G.Adj x y
Tactic: rw [IsIndepSet, Set.Pairwise] at nind
Cleared hypotheses: nind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
nind : ¬∀ ⦃x : α⦄, x ∈ G.neighborSet v → ∀ ⦃y : α⦄, y ∈ G.neighborSet v → x ≠ y → ¬G.Adj x y
⊢ False
have nind₁ : ∃ x ∈ G.neighborSet v, ∃ y ∈ G.neighborSet v, x ≠ y ∧ G.Adj x y
Tactic: push Not at nind
Cleared hypotheses: nind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
nind : ∃ x ∈ G.neighborSet v, ∃ y ∈ G.neighborSet v, x ≠ y ∧ G.Adj x y
⊢ False
have nind₁ : ∃ (x : α), G.Adj v x ∧ ∃ (y : α), G.Adj v y ∧ x ≠ y ∧ G.Adj x y
Tactic: simp_rw [mem_neighborSet] at nind
Cleared hypotheses: nind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
nind : ∃ (x : α), G.Adj v x ∧ ∃ (y : α), G.Adj v y ∧ x ≠ y ∧ G.Adj x y
⊢ False
have obtain : ∀ (j : α) (avj : G.Adj v j) (k : α) (avk : G.Adj v k), j ≠ k → ∀ (ajk : G.Adj j k), False
Tactic: obtain ⟨j, avj, k, avk, _, ajk⟩ := nind
Cleared hypotheses: nind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
⊢ G.IsIndepSet (G.neighborSet v)
have by_contra : ¬G.IsIndepSet (G.neighborSet v) → False
Tactic: classical
  by_contra nind
  rw [IsIndepSet, Set.Pairwise] at nind
  push Not at nind
  simp_rw [mem_neighborSet] at nind
  obtain ⟨j, avj, k, avk, _, ajk⟩ := nind
  exact h {v, j, k} (is3Clique_triple_iff.mpr (by simp [avj, avk, ajk]))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
by_contra by_contra₁ by_contra₂ : ∀ (nind : ¬G.IsIndepSet (G.neighborSet v)), False
⊢ G.IsIndepSet (G.neighborSet v)
have by_contra₃ : ∀ (nind : ¬∀ ⦃x : α⦄, x ∈ G.neighborSet v → ∀ ⦃y : α⦄, y ∈ G.neighborSet v → x ≠ y → ¬G.Adj x y), False
Tactic: classical
  by_contra nind
  rw [IsIndepSet, Set.Pairwise] at nind
  push Not at nind
  simp_rw [mem_neighborSet] at nind
  obtain ⟨j, avj, k, avk, _, ajk⟩ := nind
  exact h {v, j, k} (is3Clique_triple_iff.mpr (by simp [avj, avk, ajk]))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
by_contra by_contra₁ by_contra₂ : ∀ (nind : ¬G.IsIndepSet (G.neighborSet v)), False
by_contra₃ : ∀ (nind : ¬∀ ⦃x : α⦄, x ∈ G.neighborSet v → ∀ ⦃y : α⦄, y ∈ G.neighborSet v → x ≠ y → ¬G.Adj x y), False
⊢ G.IsIndepSet (G.neighborSet v)
have by_contra₄ : ∀ (nind : ∃ x ∈ G.neighborSet v, ∃ y ∈ G.neighborSet v, x ≠ y ∧ G.Adj x y), False
Tactic: classical
  by_contra nind
  rw [IsIndepSet, Set.Pairwise] at nind
  push Not at nind
  simp_rw [mem_neighborSet] at nind
  obtain ⟨j, avj, k, avk, _, ajk⟩ := nind
  exact h {v, j, k} (is3Clique_triple_iff.mpr (by simp [avj, avk, ajk]))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
by_contra by_contra₁ by_contra₂ : ∀ (nind : ¬G.IsIndepSet (G.neighborSet v)), False
by_contra₃ : ∀ (nind : ¬∀ ⦃x : α⦄, x ∈ G.neighborSet v → ∀ ⦃y : α⦄, y ∈ G.neighborSet v → x ≠ y → ¬G.Adj x y), False
by_contra₄ : ∀ (nind : ∃ x ∈ G.neighborSet v, ∃ y ∈ G.neighborSet v, x ≠ y ∧ G.Adj x y), False
⊢ G.IsIndepSet (G.neighborSet v)
have by_contra₅ : ∀ (nind : ∃ (x : α), G.Adj v x ∧ ∃ (y : α), G.Adj v y ∧ x ≠ y ∧ G.Adj x y), False
Tactic: classical
  by_contra nind
  rw [IsIndepSet, Set.Pairwise] at nind
  push Not at nind
  simp_rw [mem_neighborSet] at nind
  obtain ⟨j, avj, k, avk, _, ajk⟩ := nind
  exact h {v, j, k} (is3Clique_triple_iff.mpr (by simp [avj, avk, ajk]))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
by_contra by_contra₁ by_contra₂ : ∀ (nind : ¬G.IsIndepSet (G.neighborSet v)), False
by_contra₃ : ∀ (nind : ¬∀ ⦃x : α⦄, x ∈ G.neighborSet v → ∀ ⦃y : α⦄, y ∈ G.neighborSet v → x ≠ y → ¬G.Adj x y), False
by_contra₄ : ∀ (nind : ∃ x ∈ G.neighborSet v, ∃ y ∈ G.neighborSet v, x ≠ y ∧ G.Adj x y), False
by_contra₅ : ∀ (nind : ∃ (x : α), G.Adj v x ∧ ∃ (y : α), G.Adj v y ∧ x ≠ y ∧ G.Adj x y), False
⊢ G.IsIndepSet (G.neighborSet v)
have by_contra₆ : ∀ (j : α) (avj : G.Adj v j) (k : α) (avk : G.Adj v k), j ≠ k → ∀ (ajk : G.Adj j k), False
Tactic: classical
  by_contra nind
  rw [IsIndepSet, Set.Pairwise] at nind
  push Not at nind
  simp_rw [mem_neighborSet] at nind
  obtain ⟨j, avj, k, avk, _, ajk⟩ := nind
  exact h {v, j, k} (is3Clique_triple_iff.mpr (by simp [avj, avk, ajk]))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
⊢ Gᶜ.IsNClique n s ↔ G.IsNIndepSet n s
have rw : Gᶜ.IsNClique n s ↔ G.IsIndepSet (↑s : Set α) ∧ #s = n
Tactic: rw [isNIndepSet_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
⊢ Gᶜ.IsNIndepSet n s ↔ G.IsNClique n s
have rw : Gᶜ.IsNIndepSet n s ↔ G.IsClique (↑s : Set α) ∧ #s = n
Tactic: rw [isNClique_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
t : Finset α
tc : G.IsIndepSet (↑t : Set α)
⊢ #t ≤ G.indepNum
have tc₁ : Gᶜ.IsClique (↑t : Set α)
Tactic: rw [← isClique_compl] at tc
Cleared hypotheses: tc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
t : Finset α
tc : Gᶜ.IsClique (↑t : Set α)
⊢ #t ≤ G.indepNum
have simp_rw : #t ≤ sSup {n : ℕ | ∃ (s : Finset α), Gᶜ.IsNClique n s}
Tactic: simp_rw [indepNum, ← isNClique_compl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_3
G : SimpleGraph α
⊢ ∃ (s : Finset α), G.IsNIndepSet G.indepNum s
have simp_rw : ∃ (s : Finset α), Gᶜ.IsNClique (sSup {n : ℕ | ∃ (s : Finset α), Gᶜ.IsNClique n s}) s
Tactic: simp_rw [indepNum, ← isNClique_compl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumIndepSet s
⊢ Maximal G.IsIndepSet (↑s : Set α)
have rw : Maximal Gᶜ.IsClique (↑s : Set α)
Tactic: rw [← isMaximalClique_compl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumIndepSet s
⊢ Maximal Gᶜ.IsClique (↑s : Set α)
have M₁ : Gᶜ.IsMaximumClique s
Tactic: rw [← isMaximumClique_compl] at M
Cleared hypotheses: M
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
t : Finset α
tmc : G.IsMaximumIndepSet t
⊢ #t = G.indepNum
have tmc₁ : Gᶜ.IsMaximumClique t
Tactic: rw [← isMaximumClique_compl] at tmc
Cleared hypotheses: tmc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
t : Finset α
tmc : Gᶜ.IsMaximumClique t
⊢ #t = G.indepNum
have simp_rw : #t = sSup {n : ℕ | ∃ (s : Finset α), Gᶜ.IsNClique n s}
Tactic: simp_rw [indepNum, ← isNClique_compl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n : ℕ
u v : Fin n
⊢ (pathGraph n).Adj u v →
    Ne (α := Bool) ((fun (u : Fin n) ↦ decide ((↑u : ℕ) % 2 = 0)) u) ((fun (u : Fin n) ↦ decide ((↑u : ℕ) % 2 = 0)) v)
have rw : (↑u : ℕ) + 1 = (↑v : ℕ) ∨ (↑v : ℕ) + 1 = (↑u : ℕ) →
  Ne (α := Bool) ((fun (u : Fin n) ↦ decide ((↑u : ℕ) % 2 = 0)) u) ((fun (u : Fin n) ↦ decide ((↑u : ℕ) % 2 = 0)) v)
Tactic: rw [pathGraph_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n : ℕ
h : 2 ≤ n
v w : Fin 2
⊢ Eq (α := Fin n) ((fun (v : Fin 2) ↦ (⟨(↑v : ℕ), ⋯⟩ : Fin n)) v) ((fun (v : Fin 2) ↦ (⟨(↑v : ℕ), ⋯⟩ : Fin n)) w) →
    v = w
have rw : (↑v : ℕ) = (↑w : ℕ) → v = w
Tactic: rw [Fin.mk.injEq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (hypothesis)
Goal:
n : ℕ
h : 2 ≤ n
⊢ (pathGraph n).chromaticNumber = 2
have hc : (pathGraph n).Colorable (Fintype.card Bool)
Tactic: have hc := (pathGraph.bicoloring n).colorable
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
⊢ (pathGraph n).chromaticNumber = 2
have a : (pathGraph n).chromaticNumber ≤ 2
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
a : (pathGraph n).chromaticNumber ≤ 2
⊢ (pathGraph n).chromaticNumber = 2
have a₁ : 2 ≤ (pathGraph n).chromaticNumber
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (hypothesis)
Goal:
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
⊢ 2 ≤ (pathGraph n).chromaticNumber
have hadj : (pathGraph n).Adj ⟨0, sorry⟩ ⟨1, h⟩
Tactic: have hadj : (pathGraph n).Adj ⟨0, Nat.zero_lt_of_lt h⟩ ⟨1, h⟩ := by simp [pathGraph_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u_1 v_1 u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true)
⊢ Even (Walk.cons h p).length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
have cons : ¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
Tactic: simp only [Walk.length_cons, Nat.even_add_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u_1 v_1 u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true)
⊢ ¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true
have rw : ¬Eq (α := Bool) ((c : (a : α) → Bool) u : Bool) ((c : (a : α) → Bool) v : Bool)
Tactic: rw [← not_iff, ← Bool.eq_iff_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u_1 v_1 u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true)
⊢ ¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
have this : ¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true
Tactic: have : ¬ c u = true ↔ c v = true := by
      rw [← not_iff, ← Bool.eq_iff_iff]
      exact c.valid h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u_1 v_1 u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true)
this : ¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true
⊢ ¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
have cons : Even p.length →
  ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true → (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
Tactic: tauto
Cleared hypotheses: ih, this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u_1 v_1 u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true)
this : ¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true
cons :
  Even p.length →
    ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬(c : (a : α) → Bool) u = true →
        (c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
⊢ ¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
have cons₁ : Even p.length →
  ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
    ¬¬(c : (a : α) → Bool) u = true →
      ¬(c : (a : α) → Bool) v = true →
        (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
Tactic: tauto
Cleared hypotheses: ih, this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u_1 v_1 u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true)
this : ¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true
cons :
  Even p.length →
    ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬(c : (a : α) → Bool) u = true →
        (c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₁ :
  Even p.length →
    ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬¬(c : (a : α) → Bool) u = true →
        ¬(c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
⊢ ¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
have cons₂ : ¬Even p.length →
  ¬((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true → (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
Tactic: tauto
Cleared hypotheses: ih, this