awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
refine_1 :
  ∀ (h : G.CliqueFreeOn s 2) (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ s),
    a ≠ b → ∀ (hab : G.Adj a b), (↑{a, b} : Set α) ⊆ s
⊢ G.CliqueFreeOn s 2 ↔ s.Pairwise G.Adjᶜ
have refine_2 : s.Pairwise G.Adjᶜ → G.CliqueFreeOn s 2
Tactic: classical
  refine ⟨fun h a ha b hb _ hab => h ?_ ⟨by simpa [hab.ne], card_pair hab.ne⟩, ?_⟩
  · push_cast
    exact Set.insert_subset_iff.2 ⟨ha, Set.singleton_subset_iff.2 hb⟩
  simp only [CliqueFreeOn, isNClique_iff, card_eq_two, not_and, not_exists]
  rintro h t hst ht a b hab rfl
  simp only [coe_insert, coe_singleton, Set.insert_subset_iff, Set.singleton_subset_iff] at hst
  refine h hst.1 hst.2 hab (ht ?_ ?_ hab) <;> simp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
refine_1 :
  ∀ (h : G.CliqueFreeOn s 2) (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ s),
    a ≠ b → ∀ (hab : G.Adj a b), (↑{a, b} : Set α) ⊆ s
refine_2 refine_2₁ : s.Pairwise G.Adjᶜ → G.CliqueFreeOn s 2
⊢ G.CliqueFreeOn s 2 ↔ s.Pairwise G.Adjᶜ
have refine_2₂ : s.Pairwise G.Adjᶜ →
  ∀ ⦃t : Finset α⦄, (↑t : Set α) ⊆ s → G.IsClique (↑t : Set α) → ∀ (x x_1 : α), x ≠ x_1 → ¬t = {x, x_1}
Tactic: classical
  refine ⟨fun h a ha b hb _ hab => h ?_ ⟨by simpa [hab.ne], card_pair hab.ne⟩, ?_⟩
  · push_cast
    exact Set.insert_subset_iff.2 ⟨ha, Set.singleton_subset_iff.2 hb⟩
  simp only [CliqueFreeOn, isNClique_iff, card_eq_two, not_and, not_exists]
  rintro h t hst ht a b hab rfl
  simp only [coe_insert, coe_singleton, Set.insert_subset_iff, Set.singleton_subset_iff] at hst
  refine h hst.1 hst.2 hab (ht ?_ ?_ hab) <;> simp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
refine_1 :
  ∀ (h : G.CliqueFreeOn s 2) (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ s),
    a ≠ b → ∀ (hab : G.Adj a b), (↑{a, b} : Set α) ⊆ s
refine_2 refine_2₁ : s.Pairwise G.Adjᶜ → G.CliqueFreeOn s 2
refine_2₂ :
  s.Pairwise G.Adjᶜ →
    ∀ ⦃t : Finset α⦄, (↑t : Set α) ⊆ s → G.IsClique (↑t : Set α) → ∀ (x x_1 : α), x ≠ x_1 → ¬t = {x, x_1}
⊢ G.CliqueFreeOn s 2 ↔ s.Pairwise G.Adjᶜ
have refine_2₃ : ∀ (h : s.Pairwise G.Adjᶜ) (a b : α) (hab : a ≠ b) (hst : (↑{a, b} : Set α) ⊆ s) (ht : G.IsClique (↑{a, b} : Set α)),
  False
Tactic: classical
  refine ⟨fun h a ha b hb _ hab => h ?_ ⟨by simpa [hab.ne], card_pair hab.ne⟩, ?_⟩
  · push_cast
    exact Set.insert_subset_iff.2 ⟨ha, Set.singleton_subset_iff.2 hb⟩
  simp only [CliqueFreeOn, isNClique_iff, card_eq_two, not_and, not_exists]
  rintro h t hst ht a b hab rfl
  simp only [coe_insert, coe_singleton, Set.insert_subset_iff, Set.singleton_subset_iff] at hst
  refine h hst.1 hst.2 hab (ht ?_ ?_ hab) <;> simp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
refine_1 :
  ∀ (h : G.CliqueFreeOn s 2) (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ s),
    a ≠ b → ∀ (hab : G.Adj a b), (↑{a, b} : Set α) ⊆ s
refine_2 refine_2₁ : s.Pairwise G.Adjᶜ → G.CliqueFreeOn s 2
refine_2₂ :
  s.Pairwise G.Adjᶜ →
    ∀ ⦃t : Finset α⦄, (↑t : Set α) ⊆ s → G.IsClique (↑t : Set α) → ∀ (x x_1 : α), x ≠ x_1 → ¬t = {x, x_1}
refine_2₃ :
  ∀ (h : s.Pairwise G.Adjᶜ) (a b : α) (hab : a ≠ b) (hst : (↑{a, b} : Set α) ⊆ s) (ht : G.IsClique (↑{a, b} : Set α)),
    False
⊢ G.CliqueFreeOn s 2 ↔ s.Pairwise G.Adjᶜ
have refine_2₄ : ∀ (h : s.Pairwise G.Adjᶜ) (a b : α) (hab : a ≠ b) (ht : G.IsClique (↑{a, b} : Set α)) (hst : a ∈ s ∧ b ∈ s), False
Tactic: classical
  refine ⟨fun h a ha b hb _ hab => h ?_ ⟨by simpa [hab.ne], card_pair hab.ne⟩, ?_⟩
  · push_cast
    exact Set.insert_subset_iff.2 ⟨ha, Set.singleton_subset_iff.2 hb⟩
  simp only [CliqueFreeOn, isNClique_iff, card_eq_two, not_and, not_exists]
  rintro h t hst ht a b hab rfl
  simp only [coe_insert, coe_singleton, Set.insert_subset_iff, Set.singleton_subset_iff] at hst
  refine h hst.1 hst.2 hab (ht ?_ ?_ hab) <;> simp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
⊢ G.CliqueFreeOn (s ∩ G.neighborSet a) n
have refine : ∀ (t : Finset α) (hts : (↑t : Set α) ⊆ s ∩ G.neighborSet a) (ht : G.IsNClique n t), (↑(insert a t) : Set α) ⊆ s
Tactic: refine fun t hts ht => hs ?_ (ht.insert fun b hb => (hts hb).2)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
t : Finset α
hts : (↑t : Set α) ⊆ s ∩ G.neighborSet a
ht : G.IsNClique n t
⊢ (↑(insert a t) : Set α) ⊆ s
have push_cast : insert a (↑t : Set α) ⊆ s
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
⊢ G.CliqueFreeOn (s ∩ G.neighborSet a) n
have refine : ∀ (t : Finset α) (hts : (↑t : Set α) ⊆ s ∩ G.neighborSet a) (ht : G.IsNClique n t), (↑(insert a t) : Set α) ⊆ s
Tactic: classical
  refine fun t hts ht => hs ?_ (ht.insert fun b hb => (hts hb).2)
  push_cast
  exact Set.insert_subset_iff.2 ⟨ha, hts.trans Set.inter_subset_left⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
refine : ∀ (t : Finset α) (hts : (↑t : Set α) ⊆ s ∩ G.neighborSet a) (ht : G.IsNClique n t), (↑(insert a t) : Set α) ⊆ s
⊢ G.CliqueFreeOn (s ∩ G.neighborSet a) n
have refine₁ : ∀ (t : Finset α) (hts : (↑t : Set α) ⊆ s ∩ G.neighborSet a) (ht : G.IsNClique n t), insert a (↑t : Set α) ⊆ s
Tactic: classical
  refine fun t hts ht => hs ?_ (ht.insert fun b hb => (hts hb).2)
  push_cast
  exact Set.insert_subset_iff.2 ⟨ha, hts.trans Set.inter_subset_left⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.cliqueSet n = ∅ ↔ G.CliqueFree n
have simp_rw : G.cliqueSet n = ∅ ↔ ∀ (t : Finset α), ¬G.IsNClique n t
Tactic: simp_rw [CliqueFree, Set.eq_empty_iff_forall_notMem, mem_cliqueSet_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
simp_rw : G.cliqueSet n = ∅ ↔ ∀ (t : Finset α), ¬G.IsNClique n t
⊢ G.cliqueSet n = ∅ ↔ G.CliqueFree n
have simp_rw₁ : (∀ (x : Finset α), x ∉ G.cliqueSet n) ↔ ∀ (t : Finset α), ¬G.IsNClique n t
Tactic: simp_rw [CliqueFree, Set.eq_empty_iff_forall_notMem, mem_cliqueSet_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
⊢ cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n = map f '' G.cliqueSet n
have h : ∀ (s : Finset β),
  Membership.mem (γ := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n) s ↔
    s ∈ map f '' G.cliqueSet n
Tactic: ext s
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset β
⊢ Membership.mem (γ := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n) s ↔
    s ∈ map f '' G.cliqueSet n
have h : Membership.mem (γ := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n) s → s ∈ map f '' G.cliqueSet n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset β
h :
  Membership.mem (γ := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n) s →
    s ∈ map f '' G.cliqueSet n
⊢ Membership.mem (γ := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n) s ↔
    s ∈ map f '' G.cliqueSet n
have h₁ : s ∈ map f '' G.cliqueSet n → Membership.mem (γ := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n) s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
⊢ map f (s.preimage (⇑f : (a : α) → β) ⋯) = s
have rw : ∀ x ∈ s, Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x
Tactic: rw [map_eq_image, image_preimage, filter_true_of_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
a : β
ha : a ∈ s
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a
have obtain : ∀ (b : β) (hb : b ∈ s) (hba : b ≠ a),
  Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a
Tactic: obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hba : b ≠ a
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a
have obtain : ∀ (c w : α),
  G.Adj c w →
    ∀ (hc : (f : (a : α) → β) c = a),
      (f : (a : α) → β) w = b → Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a
Tactic: obtain ⟨-, c, _, _, hc, _⟩ := hs ha hb hba.symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
⊢ map f (s.preimage (⇑f : (a : α) → β) ⋯) = s
have rw : image (⇑f : (a : α) → β) (s.preimage (⇑f : (a : α) → β) sorry) = s
Tactic: classical
      rw [map_eq_image, image_preimage, filter_true_of_mem]
      rintro a ha
      obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a
      obtain ⟨-, c, _, _, hc, _⟩ := hs ha hb hba.symm
      exact ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
rw : image (⇑f : (a : α) → β) (s.preimage (⇑f : (a : α) → β) ⋯) = s
⊢ map f (s.preimage (⇑f : (a : α) → β) ⋯) = s
have rw₁ : {x ∈ s | Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x} = s
Tactic: classical
      rw [map_eq_image, image_preimage, filter_true_of_mem]
      rintro a ha
      obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a
      obtain ⟨-, c, _, _, hc, _⟩ := hs ha hb hba.symm
      exact ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
rw : image (⇑f : (a : α) → β) (s.preimage (⇑f : (a : α) → β) ⋯) = s
rw₁ : {x ∈ s | Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x} = s
⊢ map f (s.preimage (⇑f : (a : α) → β) ⋯) = s
have rw₂ : s = s
Tactic: classical
      rw [map_eq_image, image_preimage, filter_true_of_mem]
      rintro a ha
      obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a
      obtain ⟨-, c, _, _, hc, _⟩ := hs ha hb hba.symm
      exact ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
rw : image (⇑f : (a : α) → β) (s.preimage (⇑f : (a : α) → β) ⋯) = s
rw₁ : {x ∈ s | Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x} = s
rw₂ : s = s
⊢ map f (s.preimage (⇑f : (a : α) → β) ⋯) = s
have rw₃ : ∀ x ∈ s, Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x
Tactic: classical
      rw [map_eq_image, image_preimage, filter_true_of_mem]
      rintro a ha
      obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a
      obtain ⟨-, c, _, _, hc, _⟩ := hs ha hb hba.symm
      exact ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
rw : image (⇑f : (a : α) → β) (s.preimage (⇑f : (a : α) → β) ⋯) = s
rw₁ : {x ∈ s | Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x} = s
rw₂ : s = s
rw₃ : ∀ x ∈ s, Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x
rw₄ : s = s
rw₅ rw₆ rw₇ :
  ∀ (a : β) (ha : a ∈ s), Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a
⊢ map f (s.preimage (⇑f : (a : α) → β) ⋯) = s
have rw₈ : ∀ (a : β) (ha : a ∈ s) (b : β) (hb : b ∈ s) (hba : b ≠ a),
  Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a
Tactic: classical
      rw [map_eq_image, image_preimage, filter_true_of_mem]
      rintro a ha
      obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a
      obtain ⟨-, c, _, _, hc, _⟩ := hs ha hb hba.symm
      exact ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
rw : image (⇑f : (a : α) → β) (s.preimage (⇑f : (a : α) → β) ⋯) = s
rw₁ : {x ∈ s | Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x} = s
rw₂ : s = s
rw₃ : ∀ x ∈ s, Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x
rw₄ : s = s
rw₅ rw₆ rw₇ :
  ∀ (a : β) (ha : a ∈ s), Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a
rw₈ :
  ∀ (a : β) (ha : a ∈ s) (b : β) (hb : b ∈ s) (hba : b ≠ a),
    Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a
⊢ map f (s.preimage (⇑f : (a : α) → β) ⋯) = s
have rw₉ : ∀ (a : β) (ha : a ∈ s) (b : β) (hb : b ∈ s) (hba : b ≠ a) (c w : α),
  G.Adj c w →
    ∀ (hc : (f : (a : α) → β) c = a),
      (f : (a : α) → β) w = b → Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a
Tactic: classical
      rw [map_eq_image, image_preimage, filter_true_of_mem]
      rintro a ha
      obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a
      obtain ⟨-, c, _, _, hc, _⟩ := hs ha hb hba.symm
      exact ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
⊢ s ∈ map f '' G.cliqueSet #s
have hs' : map f (s.preimage (⇑f : (a : α) → β) sorry) = s
Tactic: have hs' : (s.preimage f f.injective.injOn).map f = s := by
      classical
      rw [map_eq_image, image_preimage, filter_true_of_mem]
      rintro a ha
      obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a
      obtain ⟨-, c, _, _, hc, _⟩ := hs ha hb hba.symm
      exact ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
hs' : map f (s.preimage (⇑f : (a : α) → β) ⋯) = s
⊢ #(s.preimage (⇑f : (a : α) → β) ⋯) = #s
have rw : #(map f (s.preimage (⇑f : (a : α) → β) sorry)) = #s
Tactic: rw [← card_map f, hs']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
hs' : map f (s.preimage (⇑f : (a : α) → β) ⋯) = s
rw : #(map f (s.preimage (⇑f : (a : α) → β) ⋯)) = #s
⊢ #(s.preimage (⇑f : (a : α) → β) ⋯) = #s
have rw₁ : #s = #s
Tactic: rw [← card_map f, hs']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
hs' : map f (s.preimage (⇑f : (a : α) → β) ⋯) = s
⊢ s ∈ map f '' G.cliqueSet #s
have h : G.IsClique (↑(s.preimage (⇑f : (a : α) → β) sorry) : Set α)
Tactic: refine ⟨s.preimage f f.injective.injOn, ⟨?_, by rw [← card_map f, hs']⟩, hs'⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
hs' : map f (s.preimage (⇑f : (a : α) → β) ⋯) = s
⊢ G.IsClique (↑(s.preimage (⇑f : (a : α) → β) ⋯) : Set α)
have h : G.IsClique ((⇑f : (a : α) → β) ⁻¹' (↑s : Set β))
Tactic: rw [coe_preimage]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
n : ℕ
⊢ cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) n = map e.toEmbedding '' G.cliqueSet n
have inl : cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) 1 = map e.toEmbedding '' G.cliqueSet 1
Tactic: obtain rfl | hn := eq_or_ne n 1
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
n : ℕ
inl : cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) 1 = map e.toEmbedding '' G.cliqueSet 1
⊢ cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) n = map e.toEmbedding '' G.cliqueSet n
have inr : ∀ (hn : n ≠ 1), cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) n = map e.toEmbedding '' G.cliqueSet n
Tactic: obtain rfl | hn := eq_or_ne n 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
⊢ cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) 1 = map e.toEmbedding '' G.cliqueSet 1
have inl : ∀ (x : Finset β),
  Membership.mem (γ := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) 1) x ↔
    x ∈ map e.toEmbedding '' G.cliqueSet 1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
⊢ BddAbove (α := ℕ) {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}
have have : ∀ (this : Fintype α), BddAbove (α := ℕ) {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}
Tactic: have := ofFinite α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
this : Fintype α
⊢ BddAbove (α := ℕ) {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}
have h : Membership.mem (γ := Set ℕ) (upperBounds {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}) (Fintype.card α)
Tactic: use card α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
this : Fintype α
y : ℕ
s : Finset α
syc : G.IsNClique y s
⊢ y ≤ Fintype.card α
have syc₁ : G.IsClique (↑s : Set α) ∧ #s = y
Tactic: rw [isNClique_iff] at syc
Cleared hypotheses: syc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
this : Fintype α
y : ℕ
s : Finset α
syc : G.IsClique (↑s : Set α) ∧ #s = y
⊢ y ≤ Fintype.card α
have h : #s ≤ Fintype.card α
Tactic: rw [← syc.right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_3
G : SimpleGraph α
⊢ ∃ (s : Finset α), G.IsNClique G.cliqueNum s
have pos : ∀ (h : BddAbove (α := ℕ) {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}), ∃ (s : Finset α), G.IsNClique G.cliqueNum s
Tactic: by_cases h : BddAbove {n | ∃ s, G.IsNClique n s}
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_3
G : SimpleGraph α
pos : ∀ (h : BddAbove (α := ℕ) {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}), ∃ (s : Finset α), G.IsNClique G.cliqueNum s
⊢ ∃ (s : Finset α), G.IsNClique G.cliqueNum s
have neg : ∀ (h : ¬BddAbove (α := ℕ) {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}), ∃ (s : Finset α), G.IsNClique G.cliqueNum s
Tactic: by_cases h : BddAbove {n | ∃ s, G.IsNClique n s}
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
⊢ t ≤ (↑s : Set α)
have by_contra : ∀ (hc : ¬t ≤ (↑s : Set α)), False
Tactic: by_contra hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
hc : ¬t ≤ (↑s : Set α)
⊢ False
have have : ∀ (fint : Fintype (↑t : Type u_3)), False
Tactic: have fint := ofFinite t
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
hc : ¬t ≤ (↑s : Set α)
fint : Fintype (↑t : Type u_3)
a : s = t.toFinset
⊢ False
have M₁ : G.IsMaximumClique t.toFinset
Tactic: subst a
Cleared hypotheses: s, M, hsub, hc, a
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
hc : ¬t ≤ (↑s : Set α)
fint : Fintype (↑t : Type u_3)
a : s = t.toFinset
M₁ : G.IsMaximumClique t.toFinset
⊢ False
have hsub₁ : (↑t.toFinset : Set α) ≤ t
Tactic: subst a
Cleared hypotheses: s, M, hsub, hc, a
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
hc : ¬t ≤ (↑s : Set α)
fint : Fintype (↑t : Type u_3)
a : s = t.toFinset
M₁ : G.IsMaximumClique t.toFinset
hsub₁ : (↑t.toFinset : Set α) ≤ t
⊢ False
have hc₁ : ¬t ≤ (↑t.toFinset : Set α)
Tactic: subst a
Cleared hypotheses: s, M, hsub, hc, a
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
hc : ¬t ≤ (↑s : Set α)
fint : Fintype (↑t : Type u_3)
⊢ False
have ne : s ≠ t.toFinset
Tactic: have ne : s ≠ t.toFinset := fun a ↦ by subst a; simp_all[Set.coe_toFinset, not_true_eq_false]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
hc : ¬t ≤ (↑s : Set α)
fint : Fintype (↑t : Type u_3)
ne : s ≠ t.toFinset
⊢ False
have hle : #t.toFinset ≤ #s
Tactic: have hle : #t.toFinset ≤ #s := M.maximum t.toFinset (by simp [Set.coe_toFinset, ht])
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
hc : ¬t ≤ (↑s : Set α)
fint : Fintype (↑t : Type u_3)
ne : s ≠ t.toFinset
hle : #t.toFinset ≤ #s
⊢ False
have hlt : #s < #t.toFinset
Tactic: have hlt : #s < #t.toFinset :=
        card_lt_card (ssubset_of_ne_of_subset ne (Set.subset_toFinset.mpr hsub))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
sm : G.IsMaximumClique s
⊢ #s = G.cliqueNum
have sc : G.IsClique (↑s : Set α)
Tactic: obtain ⟨sc, sm⟩ := sm
Cleared hypotheses: sm