awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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
rw₃ rw₄ : HAdd.hAdd (α := ℕ) 1 1 = 2
⊢ List.count a p.support = 2

Tactic:
rw [← cons_tail_support, List.count_cons_self,
    ← support_tail_of_not_nil _ hp.1.not_nil, hp.isHamiltonian_tail]

Premises used: SimpleGraph.Walk.IsHamiltonianCycle.isHamiltonian_tail, SimpleGraph.Walk.IsHamiltonianCycle.toIsCycle, SimpleGraph.Walk.cons_tail_support, SimpleGraph.Walk.support_tail_of_not_nil, List.count_cons_self, SimpleGraph.Walk.IsCycle.not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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
rw₂ rw₃ : Eq (α := ℕ) 1 1
⊢ List.count b p.support = 1

Tactic:
rw [← cons_support_tail hp.1.not_nil, List.count_cons_of_ne h, hp.isHamiltonian_tail]

Premises used: SimpleGraph.Walk.IsHamiltonianCycle.isHamiltonian_tail, List.count_cons_of_ne, SimpleGraph.Walk.IsHamiltonianCycle.toIsCycle, SimpleGraph.Walk.cons_support_tail, SimpleGraph.Walk.IsCycle.not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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 α

Tactic:
⟨fun h ↦ ⟨h.isCycle, h.length_eq⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩

Premises used: SimpleGraph.Walk.IsHamiltonianCycle.isCycle, _private.0.SimpleGraph.Walk.isHamiltonianCycle_iff_isCycle_and_length_eq.match_1, SimpleGraph.Walk.IsHamiltonianCycle.length_eq, SimpleGraph.Walk.IsHamiltonianCycle.mk, SimpleGraph.Walk.IsHamiltonianCycle, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst_1 : Fintype α
refine :
  p.IsCycle ∧ p.length = Fintype.card α → ∀ (h₁ : p.IsCycle) (h₂ : p.length = Fintype.card α), p.tail.IsHamiltonian
⊢ p.IsHamiltonianCycle ↔ p.IsCycle ∧ p.length = Fintype.card α

Tactic:
refine ⟨fun h ↦ ⟨h.isCycle, h.length_eq⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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

Tactic:
isHamiltonian_iff_isPath_and_length_eq.mpr ⟨h₁.isPath_tail, ?_⟩

Premises used: Iff.mpr, SimpleGraph.Walk.isHamiltonian_iff_isPath_and_length_eq, And.intro, SimpleGraph.Walk.IsCycle.isPath_tail
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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 α
refine : p.tail.length = Fintype.card α - 1
⊢ p.tail.IsHamiltonian

Tactic:
refine isHamiltonian_iff_isPath_and_length_eq.mpr ⟨h₁.isPath_tail, ?_⟩

Premises used: Iff.mpr, SimpleGraph.Walk.isHamiltonian_iff_isPath_and_length_eq, And.intro, SimpleGraph.Walk.IsCycle.isPath_tail
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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.length = Fintype.card α - 1

Tactic:
grind [length_tail_add_one, IsCycle.not_nil]

Premises used: SimpleGraph.Walk.length_tail_add_one, SimpleGraph.Walk.IsCycle.not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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)
inr : Finite α → ((p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle)
⊢ (p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle

Tactic:
cases (finite_or_infinite α).symm

Premises used: finite_or_infinite, Or.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a v : α
p : G.Walk a a
hv : v ∈ p.support
h : Infinite α
⊢ (p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a v : α
p : G.Walk a a
hv : v ∈ p.support
h : Finite α
inr : ∀ (val : Fintype α), (p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle
⊢ (p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a v : α
p : G.Walk a a
hv : v ∈ p.support
h : Finite α
val : Fintype α
⊢ (p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle

Tactic:
simp [isHamiltonianCycle_iff_isCycle_and_length_eq]

Premises used: SimpleGraph.Walk.isHamiltonianCycle_iff_isCycle_and_length_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
inst_2 : Nontrivial α
hG : G.IsHamiltonian
v : α
obtain : ∀ (u : α) (p : G.Walk u u) (hp : p.IsHamiltonianCycle), ∃ (p : G.Walk v v), p.IsHamiltonianCycle
⊢ ∃ (p : G.Walk v v), p.IsHamiltonianCycle

Tactic:
obtain ⟨u, p, hp⟩ := hG Fintype.one_lt_card.ne'

Premises used: Fintype.one_lt_card, LT.lt.ne'
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
inst_2 : Nontrivial α
hG : G.IsHamiltonian
v u : α
p : G.Walk u u
hp : p.IsHamiltonianCycle
⊢ (p.rotate v ⋯).IsHamiltonianCycle

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
inst_2 : Nontrivial α
hG : G.IsHamiltonian
v u : α
p : G.Walk u u
hp : p.IsHamiltonianCycle
⊢ ∃ (p : G.Walk v v), p.IsHamiltonianCycle

Tactic:
exact ⟨p.rotate v <| hp.mem_support _, by simpa⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
H : SimpleGraph α
hGH : G ≤ H
hG : G.IsHamiltonian
⊢ H.IsHamiltonian

Tactic:
fun hα ↦ let ⟨_, p, hp⟩ := hG hα; ⟨_, p.map <| .ofLE hGH, hp.map bijective_id⟩

Premises used: SimpleGraph.Walk.map, Function.bijective_id, _private.0.SimpleGraph.IsHamiltonian.mono.match_1, Exists, SimpleGraph.Walk.IsHamiltonianCycle, SimpleGraph.IsHamiltonian, Exists.intro, SimpleGraph.Hom.ofLE, SimpleGraph.Walk.IsHamiltonianCycle.map, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
hG : G.IsHamiltonian
a b : α
inl : G.Reachable a a
inr : ∀ (hab : a ≠ b), G.Reachable a b
⊢ G.Reachable a b

Tactic:
obtain rfl | hab := eq_or_ne a b

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
hG : G.IsHamiltonian
a : α
⊢ G.Reachable a a

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
⊢ Nontrivial α

Tactic:
have : Nontrivial α := ⟨a, b, hab⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
this : Nontrivial α
inr : ∀ (w : α) (p : G.Walk w w) (hp : p.IsHamiltonianCycle), G.Reachable a b
⊢ G.Reachable a b

Tactic:
obtain ⟨_, p, hp⟩ := hG Fintype.one_lt_card.ne'

Premises used: Fintype.one_lt_card, LT.lt.ne'
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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 ∈ p.support

Tactic:
have a_mem := hp.mem_support a
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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
⊢ b ∈ p.support

Tactic:
have b_mem := hp.mem_support b
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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
b_mem : b ∈ p.support
⊢ G.Reachable a b

Tactic:
((p.takeUntil a a_mem).reverse.append <| p.takeUntil b b_mem).reachable

Premises used: SimpleGraph.Walk.reachable, SimpleGraph.Walk.takeUntil, SimpleGraph.Walk.reverse, SimpleGraph.Walk.append
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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
b_mem : b ∈ p.support
⊢ G.Reachable a b

Tactic:
exact ((p.takeUntil a a_mem).reverse.append <| p.takeUntil b b_mem).reachable

Premises used: SimpleGraph.Walk.reachable, SimpleGraph.Walk.takeUntil, SimpleGraph.Walk.reverse, SimpleGraph.Walk.append
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
h : Fintype.card α = 1
⊢ G.IsHamiltonian

Tactic:
(· h |>.elim)

Premises used: False.elim, SimpleGraph.IsHamiltonian
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
h : Fintype.card α = 2
hG : G.IsHamiltonian
⊢ Fintype.card α ≠ 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
h : Fintype.card α = 2
hG : G.IsHamiltonian
have : ∀ (v : α) (p : G.Walk v v) (hp : p.IsHamiltonianCycle), False
⊢ False

Tactic:
have ⟨v, p, hp⟩ := hG <| by lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
h : Fintype.card α = 2
hG : G.IsHamiltonian
v : α
p : G.Walk v v
hp : p.IsHamiltonianCycle
⊢ False

Tactic:
grind [hp.three_le_length, hp.length_eq]

Premises used: SimpleGraph.Walk.IsHamiltonianCycle.length_eq, SimpleGraph.Walk.IsHamiltonianCycle.toIsCycle, SimpleGraph.Walk.IsCycle.three_le_length
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h : Fintype.card α ≠ 1
hG : IsHamiltonian.{u_1} (α := α) ⊥
have : ∀ (v : α) (p : Walk ⊥ v v) (hp : p.IsHamiltonianCycle), False
⊢ False

Tactic:
have ⟨v, p, hp⟩ := hG h
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h : Fintype.card α ≠ 1
hG : IsHamiltonian.{u_1} (α := α) ⊥
v : α
p : Walk ⊥ v v
hp : p.IsHamiltonianCycle
⊢ False

Tactic:
p.adj_snd hp.not_nil

Premises used: SimpleGraph.Walk.IsHamiltonianCycle.toIsCycle, SimpleGraph.Walk.adj_snd, SimpleGraph.Walk.IsCycle.not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h : Fintype.card α ≠ 1
hG : IsHamiltonian.{u_1} (α := α) ⊥
v : α
p : Walk ⊥ v v
hp : p.IsHamiltonianCycle
⊢ False

Tactic:
exact p.adj_snd hp.not_nil

Premises used: SimpleGraph.Walk.IsHamiltonianCycle.toIsCycle, SimpleGraph.Walk.adj_snd, SimpleGraph.Walk.IsCycle.not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
inst_2 : Unique α
⊢ G.IsHamiltonian

Tactic:
of_card_eq_one <| Fintype.card_unique

Premises used: Fintype.card_unique, SimpleGraph.IsHamiltonian.of_card_eq_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
e : Sym2 α
he : G.IsBridge e
h : ∀ (u v : α) (he : G.IsBridge s(u, v)), ¬G.IsHamiltonian
⊢ ¬G.IsHamiltonian

Tactic:
induction e with | h u v
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
u v : α
he : G.IsBridge s(u, v)
⊢ Nontrivial α

Tactic:
have := he.nontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
inst_1 : Fintype α
u v : α
he : G.IsBridge s(u, v)
this : Nontrivial α
hG : G.IsHamiltonian
h : ∀ (p : G.Walk u u) (hp : p.IsHamiltonianCycle), False
⊢ False

Tactic:
obtain ⟨p, hp⟩ := hG.exists_isHamiltonianCycle u

Premises used: SimpleGraph.IsHamiltonian.exists_isHamiltonianCycle
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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

Tactic:
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)

Premises used: SimpleGraph.Walk.IsPath.isTrail, SimpleGraph.Walk.IsHamiltonianCycle.isHamiltonian_tail, SimpleGraph.Walk.IsHamiltonian.isPath, SimpleGraph.Reachable.trans, SimpleGraph.Walk.IsHamiltonian.mem_support, And.right, SimpleGraph.Walk.IsTrail.not_mem_support_of_not_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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
h : ∀ (huv : (G.deleteEdges {s(u, v)}).Reachable p.snd v), (G.deleteEdges {s(u, v)}).Reachable (u, v).1 p.snd
⊢ False

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)

Premises used: SimpleGraph.Walk.IsPath.isTrail, SimpleGraph.Walk.IsHamiltonianCycle.isHamiltonian_tail, SimpleGraph.Walk.IsHamiltonian.isPath, SimpleGraph.Reachable.trans, SimpleGraph.Walk.IsHamiltonian.mem_support, And.right, SimpleGraph.Walk.IsTrail.not_mem_support_of_not_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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
h₂ : Set.encard (α := Sym2 α) {s(u, v)} < (↑2 : ℕ∞)
⊢ (G.deleteEdges {s(u, v)}).Reachable (u, v).1 p.snd

Tactic:
apply hp.isTrail.isEdgeReachable_two

Premises used: SimpleGraph.Walk.IsTrail.isEdgeReachable_two, SimpleGraph.Walk.IsCircuit.isTrail, SimpleGraph.Walk.IsHamiltonianCycle.toIsCycle, SimpleGraph.Walk.IsCycle.isCircuit
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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
⊢ (u, v).1 ∈ p.support

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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
⊢ p.snd ∈ p.support

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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
⊢ Set.encard (α := Sym2 α) {s(u, v)} < (↑2 : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ (hasse α).Adj a b ↔ a ⋖ b ∨ b ⋖ a

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
a b : α
⊢ ∀ {a b : αᵒᵈ}, (hasse α).Adj ((ofDual : (a : αᵒᵈ) → α) a) ((ofDual : (a : αᵒᵈ) → α) b) ↔ Adj (hasse αᵒᵈ) a b

Tactic:
simp [or_comm]

Premises used: or_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
α : Type u_1
inst : Preorder α
a : αᵒᵈ
⊢ Eq (α := α) ((hasseDualIso : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Eq (α := αᵒᵈ) ((Iso.symm hasseDualIso : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
α : Type u_1
inst : Preorder α
s : Finset α
this : ∀ (hc : (hasse α).IsClique (↑s : Set α)) (hcard : s.card = 3), False
⊢ ¬(hasse α).IsNClique 3 s

Tactic:
⟨hc, hcard⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
α : Type u_1
inst : Preorder α
s : Finset α
hc : (hasse α).IsClique (↑s : Set α)
hcard : s.card = 3
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
⊢ False

Tactic:
obtain ⟨a, b, c, hab, hac, hbc, rfl⟩ := s.card_eq_three.mp hcard

Premises used: Iff.mp, Finset.card_eq_three, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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
⊢ a ∈ (↑{a, b, c} : Set α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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
⊢ b ∈ (↑{a, b, c} : Set α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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
⊢ (hasse α).Adj a b

Tactic:
have := hc (by simp) (by simp) hab
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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
⊢ b ∈ (↑{a, b, c} : Set α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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
⊢ c ∈ (↑{a, b, c} : Set α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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
⊢ (hasse α).Adj b c

Tactic:
have := hc (by simp) (by simp) hbc
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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
⊢ a ∈ (↑{a, b, c} : Set α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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
⊢ c ∈ (↑{a, b, c} : Set α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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
⊢ (hasse α).Adj a c

Tactic:
have := hc (by simp) (by simp) hac
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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_2 : (hasse α).Adj b c
this : (hasse α).Adj a c
⊢ False

Tactic:
grind [hasse_adj, CovBy]

Premises used: CovBy, SimpleGraph.hasse_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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
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
⊢ (hasse α).CliqueFree 3

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]

Premises used: CovBy, SimpleGraph.hasse_adj, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
Adj : ∀ (x y : α × β), SimpleGraph.Adj (hasse (α × β)) x y ↔ (hasse α □ hasse β).Adj x y
⊢ hasse (α × β) = hasse α □ hasse β

Tactic:
ext x y
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
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
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
Adj₅ :
  (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1) ∨ y.1 ⋖ x.1 ∧ x.2 = y.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
⊢ SimpleGraph.Adj (hasse (α × β)) x y ↔ (hasse α □ hasse β).Adj x y

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]

Premises used: or_or_or_comm, eq_comm, Prod.covBy_iff, SimpleGraph.hasse_adj, SimpleGraph.boxProd_adj, or_and_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Hasse
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
a b : α
rw : ReflTransGen (hasse α).Adj a b
⊢ (hasse α).Reachable a b

Tactic:
rw [reachable_iff_reflTransGen]

Premises used: SimpleGraph.reachable_iff_reflTransGen