awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
β : Type u_2
inst_1 : DecidableEq β
H : SimpleGraph β
a : α
f : G →g H
hf : Bijective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
x v : α
y : G.Adj a v
p : G.Walk v a
hp : (cons y p).IsHamiltonianCycle
__IsCycle : (Walk.map f (cons y p)).IsCycle := ⋯
⊢ List.count.{u_2} (α := β) ((f : (a : α) → β) x : β) (List.map (⇑f : (a : α) → β) p.support : List β) = 1
have cons : List.count x p.support = 1
Tactic: rw [List.count_map_of_injective _ _ hf.injective]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
h : Infinite α
⊢ ¬p.IsHamiltonianCycle
have contrapose! : ∀ (h : p.IsHamiltonianCycle), Finite α
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst_1 : Fintype α
hp : p.IsHamiltonianCycle
⊢ p.length = Fintype.card α
have rw : 1 ≤ Fintype.card α
Tactic: rw [← length_tail_add_one hp.not_nil, hp.isHamiltonian_tail.length_eq, Nat.sub_add_cancel]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst_1 : Fintype α
hp : p.IsHamiltonianCycle
⊢ 1 ≤ Fintype.card α
have rw : Nonempty α
Tactic: rw [Nat.succ_le_iff, Fintype.card_pos_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
⊢ List.count a p.support = 2
have rw : List.count a (a :: p.support.tail) = 2
Tactic: rw [← cons_tail_support, List.count_cons_self,
    ← support_tail_of_not_nil _ hp.1.not_nil, hp.isHamiltonian_tail]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
rw : List.count a (a :: p.support.tail) = 2
⊢ List.count a p.support = 2
have rw₁ : List.count a p.support.tail + 1 = 2
Tactic: rw [← cons_tail_support, List.count_cons_self,
    ← support_tail_of_not_nil _ hp.1.not_nil, hp.isHamiltonian_tail]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
rw : List.count a (a :: p.support.tail) = 2
rw₁ : List.count a p.support.tail + 1 = 2
⊢ List.count a p.support = 2
have rw₂ : List.count a p.tail.support + 1 = 2
Tactic: rw [← cons_tail_support, List.count_cons_self,
    ← support_tail_of_not_nil _ hp.1.not_nil, hp.isHamiltonian_tail]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
rw : List.count a (a :: p.support.tail) = 2
rw₁ : List.count a p.support.tail + 1 = 2
rw₂ : List.count a p.tail.support + 1 = 2
⊢ List.count a p.support = 2
have rw₃ : HAdd.hAdd (α := ℕ) 1 1 = 2
Tactic: rw [← cons_tail_support, List.count_cons_self,
    ← support_tail_of_not_nil _ hp.1.not_nil, hp.isHamiltonian_tail]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
h : a ≠ b
⊢ List.count b p.support = 1
have rw : List.count b (a :: p.tail.support) = 1
Tactic: rw [← cons_support_tail hp.1.not_nil, List.count_cons_of_ne h, hp.isHamiltonian_tail]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
h : a ≠ b
rw : List.count b (a :: p.tail.support) = 1
⊢ List.count b p.support = 1
have rw₁ : List.count b p.tail.support = 1
Tactic: rw [← cons_support_tail hp.1.not_nil, List.count_cons_of_ne h, hp.isHamiltonian_tail]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
h : a ≠ b
rw : List.count b (a :: p.tail.support) = 1
rw₁ : List.count b p.tail.support = 1
⊢ List.count b p.support = 1
have rw₂ : Eq (α := ℕ) 1 1
Tactic: rw [← cons_support_tail hp.1.not_nil, List.count_cons_of_ne h, hp.isHamiltonian_tail]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst_1 : Fintype α
⊢ p.IsHamiltonianCycle ↔ p.IsCycle ∧ p.length = Fintype.card α
have refine : p.IsCycle ∧ p.length = Fintype.card α → ∀ (h₁ : p.IsCycle) (h₂ : p.length = Fintype.card α), p.tail.IsHamiltonian
Tactic: refine ⟨fun h ↦ ⟨h.isCycle, h.length_eq⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst_1 : Fintype α
h : p.IsCycle ∧ p.length = Fintype.card α
h₁ : p.IsCycle
h₂ : p.length = Fintype.card α
⊢ p.tail.IsHamiltonian
have refine : p.tail.length = Fintype.card α - 1
Tactic: refine isHamiltonian_iff_isPath_and_length_eq.mpr ⟨h₁.isPath_tail, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a v : α
p : G.Walk a a
hv : v ∈ p.support
⊢ (p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle
have inl : Infinite α → ((p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle)
Tactic: cases (finite_or_infinite α).symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a v : α
p : G.Walk a a
hv : v ∈ p.support
inl : Infinite α → ((p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle)
⊢ (p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle
have inr : Finite α → ((p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle)
Tactic: cases (finite_or_infinite α).symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a v : α
p : G.Walk a a
hv : v ∈ p.support
h : Finite α
⊢ (p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle
have inr : ∀ (val : Fintype α), (p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
inst_2 : Nontrivial α
hG : G.IsHamiltonian
v : α
⊢ ∃ (p : G.Walk v v), p.IsHamiltonianCycle
have obtain : ∀ (u : α) (p : G.Walk u u) (hp : p.IsHamiltonianCycle), ∃ (p : G.Walk v v), p.IsHamiltonianCycle
Tactic: obtain ⟨u, p, hp⟩ := hG Fintype.one_lt_card.ne'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
hG : G.IsHamiltonian
a b : α
⊢ G.Reachable a b
have inl : G.Reachable a a
Tactic: obtain rfl | hab := eq_or_ne a b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
hG : G.IsHamiltonian
a b : α
inl : G.Reachable a a
⊢ G.Reachable a b
have inr : ∀ (hab : a ≠ b), G.Reachable a b
Tactic: obtain rfl | hab := eq_or_ne a b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
⊢ G.Reachable a b
have this : Nontrivial α
Tactic: have : Nontrivial α := ⟨a, b, hab⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
this : Nontrivial α
⊢ G.Reachable a b
have inr : ∀ (w : α) (p : G.Walk w w) (hp : p.IsHamiltonianCycle), G.Reachable a b
Tactic: obtain ⟨_, p, hp⟩ := hG Fintype.one_lt_card.ne'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
this : Nontrivial α
w : α
p : G.Walk w w
hp : p.IsHamiltonianCycle
⊢ G.Reachable a b
have a_mem : a ∈ p.support
Tactic: have a_mem := hp.mem_support a
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
this : Nontrivial α
w : α
p : G.Walk w w
hp : p.IsHamiltonianCycle
a_mem : a ∈ p.support
⊢ G.Reachable a b
have b_mem : b ∈ p.support
Tactic: have b_mem := hp.mem_support b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
h : Fintype.card α = 2
hG : G.IsHamiltonian
⊢ False
have have : ∀ (v : α) (p : G.Walk v v) (hp : p.IsHamiltonianCycle), False
Tactic: have ⟨v, p, hp⟩ := hG <| by lia
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h : Fintype.card α ≠ 1
hG : IsHamiltonian.{u_1} (α := α) ⊥
⊢ False
have have : ∀ (v : α) (p : Walk ⊥ v v) (hp : p.IsHamiltonianCycle), False
Tactic: have ⟨v, p, hp⟩ := hG h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
e : Sym2 α
he : G.IsBridge e
⊢ ¬G.IsHamiltonian
have h : ∀ (u v : α) (he : G.IsBridge s(u, v)), ¬G.IsHamiltonian
Tactic: induction e with | h u v
Cleared hypotheses: e, he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
u v : α
he : G.IsBridge s(u, v)
⊢ ¬G.IsHamiltonian
have this : Nontrivial α
Tactic: have := he.nontrivial
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
u v : α
he : G.IsBridge s(u, v)
this : Nontrivial α
hG : G.IsHamiltonian
⊢ False
have h : ∀ (p : G.Walk u u) (hp : p.IsHamiltonianCycle), False
Tactic: obtain ⟨p, hp⟩ := hG.exists_isHamiltonianCycle u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
u v : α
he : G.IsBridge s(u, v)
this : Nontrivial α
hG : G.IsHamiltonian
p : G.Walk u u
hp : p.IsHamiltonianCycle
⊢ False
have h : ∀ (huv : (G.deleteEdges {s(u, v)}).Reachable p.snd v), (G.deleteEdges {s(u, v)}).Reachable (u, v).1 p.snd
Tactic: refine hp.isHamiltonian_tail.isPath.isTrail.not_mem_support_of_not_reachable
    (fun huv ↦ he.2 <| .trans ?_ huv) he.2 (hp.isHamiltonian_tail.mem_support v)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
u v : α
he : G.IsBridge s(u, v)
this : Nontrivial α
hG : G.IsHamiltonian
p : G.Walk u u
hp : p.IsHamiltonianCycle
huv : (G.deleteEdges {s(u, v)}).Reachable p.snd v
⊢ (G.deleteEdges {s(u, v)}).Reachable (u, v).1 p.snd
have h : (u, v).1 ∈ p.support
Tactic: apply hp.isTrail.isEdgeReachable_two
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
u v : α
he : G.IsBridge s(u, v)
this : Nontrivial α
hG : G.IsHamiltonian
p : G.Walk u u
hp : p.IsHamiltonianCycle
huv : (G.deleteEdges {s(u, v)}).Reachable p.snd v
h : (u, v).1 ∈ p.support
⊢ (G.deleteEdges {s(u, v)}).Reachable (u, v).1 p.snd
have h₁ : p.snd ∈ p.support
Tactic: apply hp.isTrail.isEdgeReachable_two
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
u v : α
he : G.IsBridge s(u, v)
this : Nontrivial α
hG : G.IsHamiltonian
p : G.Walk u u
hp : p.IsHamiltonianCycle
huv : (G.deleteEdges {s(u, v)}).Reachable p.snd v
h : (u, v).1 ∈ p.support
h₁ : p.snd ∈ p.support
⊢ (G.deleteEdges {s(u, v)}).Reachable (u, v).1 p.snd
have h₂ : Set.encard (α := Sym2 α) {s(u, v)} < (↑2 : ℕ∞)
Tactic: apply hp.isTrail.isEdgeReachable_two
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Finset α
⊢ ¬(hasse α).IsNClique 3 s
have this : ∀ (hc : (hasse α).IsClique (↑s : Set α)) (hcard : s.card = 3), False
Tactic: ⟨hc, hcard⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Finset α
hc : (hasse α).IsClique (↑s : Set α)
hcard : s.card = 3
⊢ False
have obtain : ∀ (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hc : (hasse α).IsClique (↑{a, b, c} : Set α))
  (hcard : Finset.card (α := α) {a, b, c} = 3), False
Tactic: obtain ⟨a, b, c, hab, hac, hbc, rfl⟩ := s.card_eq_three.mp hcard
Cleared hypotheses: s, hc, hcard
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique (↑{a, b, c} : Set α)
hcard : Finset.card (α := α) {a, b, c} = 3
⊢ False
have this : (hasse α).Adj a b
Tactic: have := hc (by simp) (by simp) hab
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique (↑{a, b, c} : Set α)
hcard : Finset.card (α := α) {a, b, c} = 3
this : (hasse α).Adj a b
⊢ False
have this₁ : (hasse α).Adj b c
Tactic: have := hc (by simp) (by simp) hbc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique (↑{a, b, c} : Set α)
hcard : Finset.card (α := α) {a, b, c} = 3
this_1 : (hasse α).Adj a b
this : (hasse α).Adj b c
⊢ False
have this₁ : (hasse α).Adj a c
Tactic: have := hc (by simp) (by simp) hac
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ (hasse α).CliqueFree 3
have intro : ∀ (s : Finset α), ¬(hasse α).IsNClique 3 s
Tactic: classical
  intro s ⟨hc, hcard⟩
  obtain ⟨a, b, c, hab, hac, hbc, rfl⟩ := s.card_eq_three.mp hcard
  have := hc (by simp) (by simp) hab
  have := hc (by simp) (by simp) hbc
  have := hc (by simp) (by simp) hac
  grind [hasse_adj, CovBy]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
inst : Preorder α
intro : ∀ (s : Finset α), ¬(hasse α).IsNClique 3 s
⊢ (hasse α).CliqueFree 3
have intro₁ : ∀ (s : Finset α) (hc : (hasse α).IsClique (↑s : Set α)) (hcard : s.card = 3), False
Tactic: classical
  intro s ⟨hc, hcard⟩
  obtain ⟨a, b, c, hab, hac, hbc, rfl⟩ := s.card_eq_three.mp hcard
  have := hc (by simp) (by simp) hab
  have := hc (by simp) (by simp) hbc
  have := hc (by simp) (by simp) hac
  grind [hasse_adj, CovBy]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
inst : Preorder α
intro : ∀ (s : Finset α), ¬(hasse α).IsNClique 3 s
intro₁ : ∀ (s : Finset α) (hc : (hasse α).IsClique (↑s : Set α)) (hcard : s.card = 3), False
⊢ (hasse α).CliqueFree 3
have intro₂ : ∀ (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hc : (hasse α).IsClique (↑{a, b, c} : Set α))
  (hcard : Finset.card (α := α) {a, b, c} = 3), False
Tactic: classical
  intro s ⟨hc, hcard⟩
  obtain ⟨a, b, c, hab, hac, hbc, rfl⟩ := s.card_eq_three.mp hcard
  have := hc (by simp) (by simp) hab
  have := hc (by simp) (by simp) hbc
  have := hc (by simp) (by simp) hac
  grind [hasse_adj, CovBy]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
inst : Preorder α
intro : ∀ (s : Finset α), ¬(hasse α).IsNClique 3 s
intro₁ : ∀ (s : Finset α) (hc : (hasse α).IsClique (↑s : Set α)) (hcard : s.card = 3), False
intro₂ :
  ∀ (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hc : (hasse α).IsClique (↑{a, b, c} : Set α))
    (hcard : Finset.card (α := α) {a, b, c} = 3), False
⊢ (hasse α).CliqueFree 3
have intro₃ : ∀ (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hc : (hasse α).IsClique (↑{a, b, c} : Set α))
  (hcard : Finset.card (α := α) {a, b, c} = 3) (this : (hasse α).Adj a b), False
Tactic: classical
  intro s ⟨hc, hcard⟩
  obtain ⟨a, b, c, hab, hac, hbc, rfl⟩ := s.card_eq_three.mp hcard
  have := hc (by simp) (by simp) hab
  have := hc (by simp) (by simp) hbc
  have := hc (by simp) (by simp) hac
  grind [hasse_adj, CovBy]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
inst : Preorder α
intro : ∀ (s : Finset α), ¬(hasse α).IsNClique 3 s
intro₁ : ∀ (s : Finset α) (hc : (hasse α).IsClique (↑s : Set α)) (hcard : s.card = 3), False
intro₂ :
  ∀ (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hc : (hasse α).IsClique (↑{a, b, c} : Set α))
    (hcard : Finset.card (α := α) {a, b, c} = 3), False
intro₃ :
  ∀ (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hc : (hasse α).IsClique (↑{a, b, c} : Set α))
    (hcard : Finset.card (α := α) {a, b, c} = 3) (this : (hasse α).Adj a b), False
⊢ (hasse α).CliqueFree 3
have intro₄ : ∀ (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hc : (hasse α).IsClique (↑{a, b, c} : Set α))
  (hcard : Finset.card (α := α) {a, b, c} = 3) (this : (hasse α).Adj a b) (this : (hasse α).Adj b c), False
Tactic: classical
  intro s ⟨hc, hcard⟩
  obtain ⟨a, b, c, hab, hac, hbc, rfl⟩ := s.card_eq_three.mp hcard
  have := hc (by simp) (by simp) hab
  have := hc (by simp) (by simp) hbc
  have := hc (by simp) (by simp) hac
  grind [hasse_adj, CovBy]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
inst : Preorder α
intro : ∀ (s : Finset α), ¬(hasse α).IsNClique 3 s
intro₁ : ∀ (s : Finset α) (hc : (hasse α).IsClique (↑s : Set α)) (hcard : s.card = 3), False
intro₂ :
  ∀ (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hc : (hasse α).IsClique (↑{a, b, c} : Set α))
    (hcard : Finset.card (α := α) {a, b, c} = 3), False
intro₃ :
  ∀ (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hc : (hasse α).IsClique (↑{a, b, c} : Set α))
    (hcard : Finset.card (α := α) {a, b, c} = 3) (this : (hasse α).Adj a b), False
intro₄ :
  ∀ (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hc : (hasse α).IsClique (↑{a, b, c} : Set α))
    (hcard : Finset.card (α := α) {a, b, c} = 3) (this : (hasse α).Adj a b) (this : (hasse α).Adj b c), False
⊢ (hasse α).CliqueFree 3
have intro₅ : ∀ (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hc : (hasse α).IsClique (↑{a, b, c} : Set α))
  (hcard : Finset.card (α := α) {a, b, c} = 3) (this : (hasse α).Adj a b) (this : (hasse α).Adj b c)
  (this : (hasse α).Adj a c), False
Tactic: classical
  intro s ⟨hc, hcard⟩
  obtain ⟨a, b, c, hab, hac, hbc, rfl⟩ := s.card_eq_three.mp hcard
  have := hc (by simp) (by simp) hab
  have := hc (by simp) (by simp) hbc
  have := hc (by simp) (by simp) hac
  grind [hasse_adj, CovBy]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
⊢ hasse (α × β) = hasse α □ hasse β
have Adj : ∀ (x y : α × β), Adj (hasse (α × β)) x y ↔ (hasse α □ hasse β).Adj x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
⊢ Adj (hasse (α × β)) x y ↔ (hasse α □ hasse β).Adj x y
have Adj : Adj (hasse (α × β)) x y ↔ (hasse α).Adj x.1 y.1 ∧ x.2 = y.2 ∨ (hasse β).Adj x.2 y.2 ∧ x.1 = y.1
Tactic: simp_rw [boxProd_adj, hasse_adj, Prod.covBy_iff, or_and_right, @eq_comm _ y.1, @eq_comm _ y.2,
    or_or_or_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
Adj : SimpleGraph.Adj (hasse (α × β)) x y ↔ (hasse α).Adj x.1 y.1 ∧ x.2 = y.2 ∨ (hasse β).Adj x.2 y.2 ∧ x.1 = y.1
⊢ SimpleGraph.Adj (hasse (α × β)) x y ↔ (hasse α □ hasse β).Adj x y
have Adj₁ : x ⋖ y ∨ y ⋖ x ↔ (x.1 ⋖ y.1 ∨ y.1 ⋖ x.1) ∧ x.2 = y.2 ∨ (x.2 ⋖ y.2 ∨ y.2 ⋖ x.2) ∧ x.1 = y.1
Tactic: simp_rw [boxProd_adj, hasse_adj, Prod.covBy_iff, or_and_right, @eq_comm _ y.1, @eq_comm _ y.2,
    or_or_or_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
Adj : SimpleGraph.Adj (hasse (α × β)) x y ↔ (hasse α).Adj x.1 y.1 ∧ x.2 = y.2 ∨ (hasse β).Adj x.2 y.2 ∧ x.1 = y.1
Adj₁ : x ⋖ y ∨ y ⋖ x ↔ (x.1 ⋖ y.1 ∨ y.1 ⋖ x.1) ∧ x.2 = y.2 ∨ (x.2 ⋖ y.2 ∨ y.2 ⋖ x.2) ∧ x.1 = y.1
⊢ SimpleGraph.Adj (hasse (α × β)) x y ↔ (hasse α □ hasse β).Adj x y
have Adj₂ : (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1) ∨ y.1 ⋖ x.1 ∧ y.2 = x.2 ∨ y.2 ⋖ x.2 ∧ y.1 = x.1 ↔
  (x.1 ⋖ y.1 ∨ y.1 ⋖ x.1) ∧ x.2 = y.2 ∨ (x.2 ⋖ y.2 ∨ y.2 ⋖ x.2) ∧ x.1 = y.1
Tactic: simp_rw [boxProd_adj, hasse_adj, Prod.covBy_iff, or_and_right, @eq_comm _ y.1, @eq_comm _ y.2,
    or_or_or_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
Adj : SimpleGraph.Adj (hasse (α × β)) x y ↔ (hasse α).Adj x.1 y.1 ∧ x.2 = y.2 ∨ (hasse β).Adj x.2 y.2 ∧ x.1 = y.1
Adj₁ : x ⋖ y ∨ y ⋖ x ↔ (x.1 ⋖ y.1 ∨ y.1 ⋖ x.1) ∧ x.2 = y.2 ∨ (x.2 ⋖ y.2 ∨ y.2 ⋖ x.2) ∧ x.1 = y.1
Adj₂ :
  (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1) ∨ y.1 ⋖ x.1 ∧ y.2 = x.2 ∨ y.2 ⋖ x.2 ∧ y.1 = x.1 ↔
    (x.1 ⋖ y.1 ∨ y.1 ⋖ x.1) ∧ x.2 = y.2 ∨ (x.2 ⋖ y.2 ∨ y.2 ⋖ x.2) ∧ x.1 = y.1
⊢ SimpleGraph.Adj (hasse (α × β)) x y ↔ (hasse α □ hasse β).Adj x y
have Adj₃ : (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1) ∨ y.1 ⋖ x.1 ∧ y.2 = x.2 ∨ y.2 ⋖ x.2 ∧ y.1 = x.1 ↔
  (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ y.1 ⋖ x.1 ∧ x.2 = y.2) ∨ x.2 ⋖ y.2 ∧ x.1 = y.1 ∨ y.2 ⋖ x.2 ∧ x.1 = y.1
Tactic: simp_rw [boxProd_adj, hasse_adj, Prod.covBy_iff, or_and_right, @eq_comm _ y.1, @eq_comm _ y.2,
    or_or_or_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hasse (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
Adj : SimpleGraph.Adj (hasse (α × β)) x y ↔ (hasse α).Adj x.1 y.1 ∧ x.2 = y.2 ∨ (hasse β).Adj x.2 y.2 ∧ x.1 = y.1
Adj₁ : x ⋖ y ∨ y ⋖ x ↔ (x.1 ⋖ y.1 ∨ y.1 ⋖ x.1) ∧ x.2 = y.2 ∨ (x.2 ⋖ y.2 ∨ y.2 ⋖ x.2) ∧ x.1 = y.1
Adj₂ :
  (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1) ∨ y.1 ⋖ x.1 ∧ y.2 = x.2 ∨ y.2 ⋖ x.2 ∧ y.1 = x.1 ↔
    (x.1 ⋖ y.1 ∨ y.1 ⋖ x.1) ∧ x.2 = y.2 ∨ (x.2 ⋖ y.2 ∨ y.2 ⋖ x.2) ∧ x.1 = y.1
Adj₃ :
  (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1) ∨ y.1 ⋖ x.1 ∧ y.2 = x.2 ∨ y.2 ⋖ x.2 ∧ y.1 = x.1 ↔
    (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ y.1 ⋖ x.1 ∧ x.2 = y.2) ∨ x.2 ⋖ y.2 ∧ x.1 = y.1 ∨ y.2 ⋖ x.2 ∧ x.1 = y.1
⊢ SimpleGraph.Adj (hasse (α × β)) x y ↔ (hasse α □ hasse β).Adj x y
have Adj₄ : (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1) ∨ y.1 ⋖ x.1 ∧ y.2 = x.2 ∨ y.2 ⋖ x.2 ∧ x.1 = y.1 ↔
  (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ y.1 ⋖ x.1 ∧ x.2 = y.2) ∨ x.2 ⋖ y.2 ∧ x.1 = y.1 ∨ y.2 ⋖ x.2 ∧ x.1 = y.1
Tactic: simp_rw [boxProd_adj, hasse_adj, Prod.covBy_iff, or_and_right, @eq_comm _ y.1, @eq_comm _ y.2,
    or_or_or_comm]