awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t
x : β
hxt : x ∈ t
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x
have refine_2 : ∀ (y : β) (hyt : y ∈ t) (hyne : y ≠ x),
  Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x
Tactic: obtain ⟨y, hyt, hyne⟩ := ht.exists_ne x
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t
x : β
hxt : x ∈ t
y : β
hyt : y ∈ t
hyne : y ≠ x
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x
have refine_2 : ∀ (u v : α) (hyt : Membership.mem (α := β) t ((f : (a : α) → β) u : β))
  (hxt : Membership.mem (α := β) t ((f : (a : α) → β) v : β))
  (hyne : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) u : β) ((f : (a : α) → β) v : β)),
  Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    ((f : (a : α) → β) v : β)
Tactic: obtain ⟨-, u, v, -, rfl, rfl⟩ := h hyt hxt hyne
Cleared hypotheses: x, hxt, y, hyt, hyne
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t ↔
    t.Subsingleton ∨ ∃ (s : Set α), G.IsClique s ∧ (⇑f : (a : α) → β) '' s = t
have inl : ∀ (ht : t.Subsingleton),
  IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t ↔
    t.Subsingleton ∨ ∃ (s : Set α), G.IsClique s ∧ (⇑f : (a : α) → β) '' s = t
Tactic: obtain (ht | ht) := t.subsingleton_or_nontrivial
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
inl :
  ∀ (ht : t.Subsingleton),
    IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t ↔
      t.Subsingleton ∨ ∃ (s : Set α), G.IsClique s ∧ (⇑f : (a : α) → β) '' s = t
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t ↔
    t.Subsingleton ∨ ∃ (s : Set α), G.IsClique s ∧ (⇑f : (a : α) → β) '' s = t
have inr : ∀ (ht : t.Nontrivial),
  IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t ↔
    t.Subsingleton ∨ ∃ (s : Set α), G.IsClique s ∧ (⇑f : (a : α) → β) '' s = t
Tactic: obtain (ht | ht) := t.subsingleton_or_nontrivial
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
⊢ IsClique.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) ((⇑f : (a : α) → β) '' s) ↔ G.IsClique s
have rw : (s.Subsingleton ∨
    ∃ (s_1 : Set α), G.IsClique s_1 ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' s_1) ((⇑f : (a : α) → β) '' s)) ↔
  G.IsClique s
Tactic: rw [isClique_map_iff, f.injective.subsingleton_image_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
⊢ (s.Subsingleton ∨
      ∃ (s_1 : Set α),
        G.IsClique s_1 ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' s_1) ((⇑f : (a : α) → β) '' s)) ↔
    G.IsClique s
have inl : ∀ (hs : s.Subsingleton),
  (s.Subsingleton ∨
      ∃ (s_1 : Set α),
        G.IsClique s_1 ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' s_1) ((⇑f : (a : α) → β) '' s)) ↔
    G.IsClique s
Tactic: obtain (hs | hs) := s.subsingleton_or_nontrivial
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
inl :
  ∀ (hs : s.Subsingleton),
    (s.Subsingleton ∨
        ∃ (s_1 : Set α),
          G.IsClique s_1 ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' s_1) ((⇑f : (a : α) → β) '' s)) ↔
      G.IsClique s
⊢ (s.Subsingleton ∨
      ∃ (s_1 : Set α),
        G.IsClique s_1 ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' s_1) ((⇑f : (a : α) → β) '' s)) ↔
    G.IsClique s
have inr : ∀ (hs : s.Nontrivial),
  (s.Subsingleton ∨
      ∃ (s_1 : Set α),
        G.IsClique s_1 ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' s_1) ((⇑f : (a : α) → β) '' s)) ↔
    G.IsClique s
Tactic: obtain (hs | hs) := s.subsingleton_or_nontrivial
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) ↔ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
have mp : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) → ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
mp :
  IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) → ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) ↔ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
have mpr : (∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t) → IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) → ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
have mp : (∃ (s : Set α), G.IsClique s ∧ (⇑f : (a : α) → β) '' s = (↑t : Set β)) →
  ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
Tactic: rw [isClique_map_iff_of_nontrivial (by simpa)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
s : Set α
hs : G.IsClique s
hst : (⇑f : (a : α) → β) '' s = (↑t : Set β)
⊢ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
have mp : ∀ (s : Finset α) (hs : G.IsClique (↑s : Set α)) (hst : (⇑f : (a : α) → β) '' (↑s : Set α) = (↑t : Set β)),
  ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
Tactic: obtain ⟨s, rfl⟩ := Set.Finite.exists_finset_coe <|
      (show s.Finite from Set.Finite.of_finite_image (by simp [hst]) f.injective.injOn)
Cleared hypotheses: s, hs, hst
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) ↔
    #t ≤ 1 ∨ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
have inl : ∀ (ht : #t ≤ 1),
  IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) ↔
    #t ≤ 1 ∨ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
Tactic: obtain (ht | ht) := le_or_gt #t 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
inl :
  ∀ (ht : #t ≤ 1),
    IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) ↔
      #t ≤ 1 ∨ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) ↔
    #t ≤ 1 ∨ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
have inr : ∀ (ht : 1 < #t),
  IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) ↔
    #t ≤ 1 ∨ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
Tactic: obtain (ht | ht) := le_or_gt #t 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : #t ≤ 1
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) ↔
    #t ≤ 1 ∨ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
have inl : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β)
Tactic: simp only [ht, true_or, iff_true]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) ↔
    #t ≤ 1 ∨ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
have inr : (∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t) ↔
  ¬1 < #t ∨ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
Tactic: rw [isClique_map_finset_iff_of_nontrivial, ← not_lt]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
inr :
  (∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t) ↔
    ¬1 < #t ∨ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) ↔
    #t ≤ 1 ∨ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
have inr₁ : t.Nontrivial
Tactic: rw [isClique_map_finset_iff_of_nontrivial, ← not_lt]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set (↑F : Type u_1)
c : (S.induce F).coe.IsClique A
⊢ G.IsClique (Subtype.val (p := fun (x : α) ↦ x ∈ F) '' A)
have simp : ∀ ⦃x : α⦄,
  (∃ (x_1 : x ∈ F), Subtype.mk (p := fun (a : α) ↦ a ∈ F) x sorry ∈ A) →
    ∀ ⦃y : α⦄, (∃ (x : y ∈ F), Subtype.mk (p := fun (a : α) ↦ a ∈ F) y sorry ∈ A) → x ≠ y → G.Adj x y
Tactic: simp only [Set.Pairwise, Set.mem_image, Subtype.exists, exists_and_right, exists_eq_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set (↑F : Type u_1)
c : (S.induce F).coe.IsClique A
x : α
⊢ (∃ (x_1 : x ∈ F), Subtype.mk (p := fun (a : α) ↦ a ∈ F) x ⋯ ∈ A) →
    ∀ ⦃y : α⦄, (∃ (x : y ∈ F), Subtype.mk (p := fun (a : α) ↦ a ∈ F) y ⋯ ∈ A) → x ≠ y → G.Adj x y
have this : ∀ (w : x ∈ F) (ainA : Subtype.mk (p := fun (a : α) ↦ a ∈ F) x sorry ∈ A) ⦃y : α⦄,
  (∃ (x : y ∈ F), Subtype.mk (p := fun (a : α) ↦ a ∈ F) y sorry ∈ A) → x ≠ y → G.Adj x y
Tactic: ⟨_, ainA⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set (↑F : Type u_1)
c : (S.induce F).coe.IsClique A
x : α
w : x ∈ F
ainA : Subtype.mk (p := fun (a : α) ↦ a ∈ F) x ⋯ ∈ A
y : α
⊢ (∃ (x : y ∈ F), Subtype.mk (p := fun (a : α) ↦ a ∈ F) y ⋯ ∈ A) → x ≠ y → G.Adj x y
have this : ∀ (w : y ∈ F) (binA : Subtype.mk (p := fun (a : α) ↦ a ∈ F) y sorry ∈ A), x ≠ y → G.Adj x y
Tactic: ⟨_, binA⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
hc : (G ⊔ edge v w).IsClique s
x : α
hx : x ∈ s \ {v}
y : α
hy : y ∈ s \ {v}
hxy : x ≠ y
⊢ G.Adj x y
have this : (G ⊔ edge v w).Adj x y
Tactic: have := hc hx.1 hy.1 hxy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ (G ⊔ edge v w).Adj x y
have pos : ∀ (h' : x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w}), (G ⊔ edge v w).Adj x y
Tactic: by_cases h' : x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w}
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
pos : ∀ (h' : x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w}), (G ⊔ edge v w).Adj x y
⊢ (G ⊔ edge v w).Adj x y
have neg : ∀ (h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})), (G ⊔ edge v w).Adj x y
Tactic: by_cases h' : x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w}
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w}
⊢ (G ⊔ edge v w).Adj x y
have pos : ∀ (hx : x ∈ s \ {v}) (hy : y ∈ s \ {v}), (G ⊔ edge v w).Adj x y
Tactic: obtain (⟨hx, hy⟩ | ⟨hx, hy⟩) := h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w}
pos : ∀ (hx : x ∈ s \ {v}) (hy : y ∈ s \ {v}), (G ⊔ edge v w).Adj x y
⊢ (G ⊔ edge v w).Adj x y
have pos₁ : ∀ (hx : x ∈ s \ {w}) (hy : y ∈ s \ {w}), (G ⊔ edge v w).Adj x y
Tactic: obtain (⟨hx, hy⟩ | ⟨hx, hy⟩) := h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})
⊢ Sym2.ToRel {s(v, w)} x y
have pos : x = v → Sym2.ToRel {s(v, w)} x y
Tactic: by_cases x = v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})
pos : x = v → Sym2.ToRel {s(v, w)} x y
⊢ Sym2.ToRel {s(v, w)} x y
have neg : ¬x = v → Sym2.ToRel {s(v, w)} x y
Tactic: by_cases x = v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : Copy.{u_2, u_1} (α := β) ⊤ G
x : α
⊢ Membership.mem (γ := Set α) (Set.range.{u_1, u_2 + 1} (ι := β) (⇑f : (a : β) → α)) x →
    ∀ ⦃y : α⦄, Membership.mem (γ := Set α) (Set.range.{u_1, u_2 + 1} (ι := β) (⇑f : (a : β) → α)) y → x ≠ y → G.Adj x y
have this : ∀ (w : β) (h : (f : (a : β) → α) w = x) ⦃y : α⦄,
  Membership.mem (γ := Set α) (Set.range.{u_1, u_2 + 1} (ι := β) (⇑f : (a : β) → α)) y → x ≠ y → G.Adj x y
Tactic: ⟨_, h⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : Copy.{u_2, u_1} (α := β) ⊤ G
x : α
w : β
h : (f : (a : β) → α) w = x
y : α
⊢ Membership.mem (γ := Set α) (Set.range.{u_1, u_2 + 1} (ι := β) (⇑f : (a : β) → α)) y → x ≠ y → G.Adj x y
have this : ∀ (w : β) (h' : (f : (a : β) → α) w = y), x ≠ y → G.Adj x y
Tactic: ⟨_, h'⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : Copy.{u_2, u_1} (α := β) ⊤ G
x : α
w : β
h : (f : (a : β) → α) w = x
y : α
w_1 : β
h' : (f : (a : β) → α) w_1 = y
nh : x ≠ y
⊢ G.Adj x y
have rw : ∀ (nh : Ne.{u_1 + 1} (α := α) ((f.topEmbedding : (a : β) → α) w : α) ((f.topEmbedding : (a : β) → α) w_1 : α)),
  G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
Tactic: rw [← h, ← Copy.topEmbedding_apply, ← h', ← Copy.topEmbedding_apply] at nh ⊢
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : Copy.{u_2, u_1} (α := β) ⊤ G
x : α
w : β
h : (f : (a : β) → α) w = x
y : α
w_1 : β
h' : (f : (a : β) → α) w_1 = y
nh : Ne.{u_1 + 1} (α := α) ((f.topEmbedding : (a : β) → α) w : α) ((f.topEmbedding : (a : β) → α) w_1 : α)
⊢ G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
have rwa : ∀
  (nh :
    Ne.{u_1 + 1} (α := α) ((f.topEmbedding.toEmbedding (r := Adj ⊤) (s := G.Adj) : (a : β) → α) w : α)
      ((f.topEmbedding.toEmbedding (r := Adj ⊤) (s := G.Adj) : (a : β) → α) w_1 : α)),
  G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
Tactic: rwa [← f.topEmbedding.coe_toEmbedding, (f.topEmbedding.apply_eq_iff_eq _ _).ne,
    ← top_adj, ← f.topEmbedding.map_adj_iff] at nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : Copy.{u_2, u_1} (α := β) ⊤ G
x : α
w : β
h : (f : (a : β) → α) w = x
y : α
w_1 : β
h' : (f : (a : β) → α) w_1 = y
nh : Ne.{u_1 + 1} (α := α) ((f.topEmbedding : (a : β) → α) w : α) ((f.topEmbedding : (a : β) → α) w_1 : α)
rwa :
  ∀
    (nh :
      Ne.{u_1 + 1} (α := α) ((f.topEmbedding.toEmbedding (r := Adj ⊤) (s := G.Adj) : (a : β) → α) w : α)
        ((f.topEmbedding.toEmbedding (r := Adj ⊤) (s := G.Adj) : (a : β) → α) w_1 : α)),
    G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
⊢ G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
have rwa₁ : ∀ (nh : w ≠ w_1), G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
Tactic: rwa [← f.topEmbedding.coe_toEmbedding, (f.topEmbedding.apply_eq_iff_eq _ _).ne,
    ← top_adj, ← f.topEmbedding.map_adj_iff] at nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : Copy.{u_2, u_1} (α := β) ⊤ G
x : α
w : β
h : (f : (a : β) → α) w = x
y : α
w_1 : β
h' : (f : (a : β) → α) w_1 = y
nh : Ne.{u_1 + 1} (α := α) ((f.topEmbedding : (a : β) → α) w : α) ((f.topEmbedding : (a : β) → α) w_1 : α)
rwa :
  ∀
    (nh :
      Ne.{u_1 + 1} (α := α) ((f.topEmbedding.toEmbedding (r := Adj ⊤) (s := G.Adj) : (a : β) → α) w : α)
        ((f.topEmbedding.toEmbedding (r := Adj ⊤) (s := G.Adj) : (a : β) → α) w_1 : α)),
    G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
rwa₁ : ∀ (nh : w ≠ w_1), G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
⊢ G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
have rwa₂ : ∀ (nh : Adj ⊤ w w_1), G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
Tactic: rwa [← f.topEmbedding.coe_toEmbedding, (f.topEmbedding.apply_eq_iff_eq _ _).ne,
    ← top_adj, ← f.topEmbedding.map_adj_iff] at nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : Copy.{u_2, u_1} (α := β) ⊤ G
x : α
w : β
h : (f : (a : β) → α) w = x
y : α
w_1 : β
h' : (f : (a : β) → α) w_1 = y
nh : Ne.{u_1 + 1} (α := α) ((f.topEmbedding : (a : β) → α) w : α) ((f.topEmbedding : (a : β) → α) w_1 : α)
rwa :
  ∀
    (nh :
      Ne.{u_1 + 1} (α := α) ((f.topEmbedding.toEmbedding (r := Adj ⊤) (s := G.Adj) : (a : β) → α) w : α)
        ((f.topEmbedding.toEmbedding (r := Adj ⊤) (s := G.Adj) : (a : β) → α) w_1 : α)),
    G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
rwa₁ : ∀ (nh : w ≠ w_1), G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
rwa₂ : ∀ (nh : Adj ⊤ w w_1), G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
⊢ G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
have rwa₃ : ∀ (nh : G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)),
  G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
Tactic: rwa [← f.topEmbedding.coe_toEmbedding, (f.topEmbedding.apply_eq_iff_eq _ _).ne,
    ← top_adj, ← f.topEmbedding.map_adj_iff] at nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
h : G ≤ H
⊢ G.IsNClique n s → H.IsNClique n s
have simp_rw : G.IsClique (↑s : Set α) ∧ #s = n → H.IsClique (↑s : Set α) ∧ #s = n
Tactic: simp_rw [isNClique_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
s : Finset α
h : G.IsNClique n s
f : α ↪ β
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑(map f s) : Set β)
have rw : IsClique.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) ((⇑f : (a : α) → β) '' (↑s : Set α))
Tactic: rw [coe_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ IsNClique (SimpleGraph.map (⇑f : (a : α) → β) G) n t ↔ ∃ (s : Finset α), G.IsNClique n s ∧ map f s = t
have rw : (∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t) ∧ #t = n ↔ ∃ (s : Finset α), G.IsNClique n s ∧ map f s = t
Tactic: rw [isNClique_iff, isClique_map_finset_iff, or_and_right,
    or_iff_right (by rintro ⟨h', rfl⟩; exact h'.not_gt hn)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t) ∧ #t = n ↔ ∃ (s : Finset α), G.IsNClique n s ∧ map f s = t
have mp : (∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t) ∧ #t = n → ∃ (s : Finset α), G.IsNClique n s ∧ map f s = t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
mp :
  (∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t) ∧ #t = n → ∃ (s : Finset α), G.IsNClique n s ∧ map f s = t
⊢ (∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t) ∧ #t = n ↔ ∃ (s : Finset α), G.IsNClique n s ∧ map f s = t
have mpr : (∃ (s : Finset α), G.IsNClique n s ∧ map f s = t) → (∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t) ∧ #t = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
n : ℕ
s : Finset α
⊢ IsNClique ⊥ n s ↔ n ≤ 1 ∧ #s = n
have rw : (↑s : Set α).Subsingleton ∧ #s = n ↔ n ≤ 1 ∧ #s = n
Tactic: rw [isNClique_iff, isClique_bot_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
n : ℕ
s : Finset α
⊢ (↑s : Set α).Subsingleton ∧ #s = n ↔ n ≤ 1 ∧ #s = n
have refine : #s = n → ((↑s : Set α).Subsingleton ↔ n ≤ 1)
Tactic: refine and_congr_left ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ G.IsNClique 0 s ↔ s = ∅
have simp : s = ∅ → G.IsClique (↑s : Set α)
Tactic: simp only [isNClique_iff, Finset.card_eq_zero, and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ G.IsNClique 1 s ↔ ∃ (a : α), s = {a}
have simp : (∃ (a : α), s = {a}) → G.IsClique (↑s : Set α)
Tactic: simp only [isNClique_iff, card_eq_one, and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ G.IsNClique (n + 1) (insert a s)
have isClique : G.IsClique (↑(insert a s) : Set α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
isClique : G.IsClique (↑(insert a s) : Set α)
⊢ G.IsNClique (n + 1) (insert a s)
have card_eq : #(insert a s) = n + 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ G.IsClique (↑(insert a s) : Set α)
have isClique : G.IsClique (insert a (↑s : Set α))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ #(insert a s) = n + 1
have card_eq : #s + 1 = n + 1
Tactic: rw [card_insert_of_notMem fun ha => (h _ ha).ne rfl, hs.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
card_eq : #s + 1 = n + 1
⊢ #(insert a s) = n + 1
have card_eq₁ : n + 1 = n + 1
Tactic: rw [card_insert_of_notMem fun ha => (h _ ha).ne rfl, hs.2]