awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)
hb₁ : Bijective b
hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V)
this : (p₁ ∪ Set.range fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) = Set.univ
v : V
h_1 : v ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).verts
h_2 : v ∉ p₁
h :
  ∀ (x : (↑p₁ : Type u_1)),
    ((fun (a : (↑p₁ : Type u_1)) ↦ b a = Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) v ⋯) x ∧
        ∀ (y : (↑p₁ : Type u_1)),
          (fun (a : (↑p₁ : Type u_1)) ↦ b a = Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) v ⋯) y → y = x) →
      ∃! w : V, ∃ (h : w ∈ p₁), (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w ⋯)) : V) = v
⊢ ∃! w : V, ∃ (h : w ∈ p₁), (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w ⋯)) : V) = v

Tactic:
obtain ⟨x, _⟩ := hb₁.existsUnique ⟨v, by grind⟩

Premises used: Function.Bijective.existsUnique, Subtype.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)
hb₁ : Bijective b
hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V)
this : (p₁ ∪ Set.range fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) = Set.univ
v : V
h : v ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).verts
h_1 : v ∉ p₁
x : (↑p₁ : Type u_1)
h_2 :
  (fun (a : (↑p₁ : Type u_1)) ↦ b a = Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) v ⋯) x ∧
    ∀ (y : (↑p₁ : Type u_1)), (fun (a : (↑p₁ : Type u_1)) ↦ b a = Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) v ⋯) y → y = x
⊢ (fun (w : V) ↦ ∃ (h : w ∈ p₁), (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w ⋯)) : V) = v) (↑x : V) ∧
    ∀ (y : V),
      (fun (w : V) ↦ ∃ (h : w ∈ p₁), (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w ⋯)) : V) = v) y → y = (↑x : V)

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)
hb₁ : Bijective b
hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V)
this : (p₁ ∪ Set.range fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) = Set.univ
v : V
h : v ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).verts
h_1 : v ∉ p₁
x : (↑p₁ : Type u_1)
h_2 :
  (fun (a : (↑p₁ : Type u_1)) ↦ b a = Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) v ⋯) x ∧
    ∀ (y : (↑p₁ : Type u_1)), (fun (a : (↑p₁ : Type u_1)) ↦ b a = Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) v ⋯) y → y = x
⊢ ∃! w : V, ∃ (h : w ∈ p₁), (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w ⋯)) : V) = v

Tactic:
exact ⟨x, by grind⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
β : Type u_2
inst_1 : DecidableEq β
H : SimpleGraph β
a b : α
p : G.Walk a b
f : G →g H
hf : Bijective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hp : p.IsHamiltonian
⊢ (Walk.map f p).IsHamiltonian

Tactic:
simp [IsHamiltonian, hf.surjective.forall, hf.injective, hp _]

Premises used: Function.Surjective.forall, Function.Bijective.injective, Function.Bijective.surjective, SimpleGraph.Walk.IsHamiltonian
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
hp : p.IsHamiltonian
c : α
⊢ c ∈ p.support

Tactic:
p.support.one_le_count_iff.mp <| hp c |>.symm.le

Premises used: Eq.le, List.one_le_count_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
hp : p.IsHamiltonian
⊢ p.IsPath

Tactic:
IsPath.mk' <| List.nodup_iff_count_le_one.2 <| (le_of_eq <| hp ·)

Premises used: Iff.mpr, le_of_eq, List.nodup_iff_count_le_one, SimpleGraph.Walk.IsPath.mk'
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
hp : p.IsPath
hp' : ∀ (w : α), w ∈ p.support
⊢ p.IsHamiltonian

Tactic:
fun _ ↦
  le_antisymm (List.nodup_iff_count_le_one.1 hp.support_nodup _) (List.count_pos_iff.2 (hp' _))

Premises used: Iff.mpr, List.count_pos_iff, le_antisymm, Iff.mp, SimpleGraph.Walk.IsPath.support_nodup, List.nodup_iff_count_le_one, SimpleGraph.Walk.IsHamiltonian
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
hp : p.IsPath
⊢ p.IsHamiltonian ↔ ∀ (w : α), w ∈ p.support

Tactic:
⟨(·.mem_support), hp.isHamiltonian_of_mem⟩

Premises used: SimpleGraph.Walk.IsPath.isHamiltonian_of_mem, SimpleGraph.Walk.IsHamiltonian.mem_support, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Subsingleton α
v : α
rw : List.count v [a] = 1
rw₁ : List.count a [a] = 1
rw₂ rw₃ : Eq (α := ℕ) 1 1
⊢ List.count v p.support = 1

Tactic:
rw [nil_iff_support_eq.mp p.nil_of_subsingleton, Subsingleton.elim v a, List.count_singleton_self]

Premises used: SimpleGraph.Walk.nil_iff_support_eq, SimpleGraph.Walk.nil_of_subsingleton, List.count_singleton_self, Iff.mp, Subsingleton.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
hp : p.IsHamiltonian
have : ∀ (this : Fintype α), Finite α
⊢ Finite α

Tactic:
have := hp.fintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
hp : p.IsHamiltonian
this : Fintype α
⊢ Finite α

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
h : Infinite α
contrapose! : ∀ (h : p.IsHamiltonian), Finite α
⊢ ¬p.IsHamiltonian

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
h : p.IsHamiltonian
⊢ Finite α

Tactic:
h.finite

Premises used: SimpleGraph.Walk.IsHamiltonian.finite
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
h : p.IsHamiltonian
⊢ Finite α

Tactic:
exact h.finite

Premises used: SimpleGraph.Walk.IsHamiltonian.finite
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Fintype α
hp : p.IsHamiltonian
⊢ p.support.toFinset = univ

Tactic:
simp [eq_univ_iff_forall, hp]

Premises used: Finset.eq_univ_iff_forall
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
hp : p.IsHamiltonian
⊢ Eq.{u_1 + 1} (α := Set α) {v : α | v ∈ p.support} Set.univ

Tactic:
Set.eq_univ_iff_forall.mpr hp.mem_support

Premises used: Iff.mpr, Set.eq_univ_iff_forall, SimpleGraph.Walk.IsHamiltonian.mem_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Fintype α
hp : p.IsHamiltonian
rw : p.support.length = Fintype.card α
rw₁ : ∑ a_1 ∈ p.support.toFinset, List.count a_1 p.support = Fintype.card α
rw₂ : ∑ x ∈ p.support.toFinset, 1 = Fintype.card α
rw₃ : #p.support.toFinset = Fintype.card α
rw₄ : card.{u_1} (α := α) univ = Fintype.card α
rw₅ rw₆ : Fintype.card α = Fintype.card α
⊢ p.length + 1 = Fintype.card α

Tactic:
rw [← length_support, ← List.sum_toFinset_count_eq_length, Finset.sum_congr rfl fun _ _ ↦ hp _,
      ← card_eq_sum_ones, hp.toFinset_support, card_univ]

Premises used: Finset.card_univ, List.sum_toFinset_count_eq_length, Finset.card_eq_sum_ones, SimpleGraph.Walk.length_support, SimpleGraph.Walk.IsHamiltonian.toFinset_support, Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Fintype α
hp : p.IsHamiltonian
have : ∀ (this : Inhabited α), p.support.length = Fintype.card α
⊢ p.support.length = Fintype.card α

Tactic:
have : Inhabited α := ⟨a⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Fintype α
hp : p.IsHamiltonian
this : Inhabited α
⊢ p.support.length = Fintype.card α

Tactic:
grind [Fintype.card_ne_zero, length_eq]

Premises used: Fintype.card_ne_zero, SimpleGraph.Walk.IsHamiltonian.length_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
⊢ p.IsHamiltonian ↔ Bijective p.support.get

Tactic:
p.support.get_bijective_iff.symm

Premises used: List.get_bijective_iff, SimpleGraph.Walk.IsHamiltonian, Iff.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
hp : p.IsHamiltonian
⊢ Surjective p.getVert

Tactic:
.of_comp <| p.getVert_comp_val_eq_get_support ▸
    isHamiltonian_iff_support_get_bijective.mp hp |>.surjective

Premises used: Function.Surjective.of_comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
β : Type u_2
H : SimpleGraph β
a b : α
p : G.Walk a b
f : G →g H
hp : p.IsHamiltonian
h : (Walk.map f p).IsPath
rw : Set.InjOn.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) {v : α | v ∈ p.support}
⊢ Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
rw [← Set.injOn_univ, ← hp.setOf_support]

Premises used: SimpleGraph.Walk.IsHamiltonian.setOf_support, Set.injOn_univ
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
β : Type u_2
H : SimpleGraph β
a b : α
p : G.Walk a b
f : G →g H
hp : p.IsHamiltonian
h : (Walk.map f p).IsPath
⊢ Set.InjOn.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) {v : α | v ∈ p.support}

Tactic:
h.injOn_support_of_isPath_map

Premises used: SimpleGraph.Walk.IsPath.injOn_support_of_isPath_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
β : Type u_2
H : SimpleGraph β
a b : α
p : G.Walk a b
f : G →g H
hp : p.IsHamiltonian
h : (Walk.map f p).IsPath
⊢ Set.InjOn.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) {v : α | v ∈ p.support}

Tactic:
exact h.injOn_support_of_isPath_map

Premises used: SimpleGraph.Walk.IsPath.injOn_support_of_isPath_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Fintype α
pos : ∀ (h : IsEmpty α), p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1
neg : ∀ (h : Nonempty α), p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1
⊢ p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1

Tactic:
by_cases! h : IsEmpty α

Premises used: IsEmpty
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Fintype α
h : IsEmpty α
⊢ p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1

Tactic:
h.elim' a

Premises used: IsEmpty.elim'
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Fintype α
h : IsEmpty α
⊢ p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1

Tactic:
exact h.elim' a

Premises used: IsEmpty.elim'
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Fintype α
h : Nonempty α
⊢ p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1

Tactic:
⟨fun h ↦ ⟨h.isPath, h.length_eq⟩, fun ⟨hp, h⟩ ↦ ?_⟩

Premises used: _private.0.SimpleGraph.Walk.isHamiltonian_iff_isPath_and_length_eq.match_1, SimpleGraph.Walk.IsHamiltonian.isPath, And.intro, Iff.intro, SimpleGraph.Walk.IsHamiltonian.length_eq, SimpleGraph.Walk.IsHamiltonian
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Fintype α
h : Nonempty α
neg : p.IsPath ∧ p.length = Fintype.card α - 1 → ∀ (hp : p.IsPath) (h : p.length = Fintype.card α - 1), p.IsHamiltonian
⊢ p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1

Tactic:
refine ⟨fun h ↦ ⟨h.isPath, h.length_eq⟩, fun ⟨hp, h⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Fintype α
h_1 : Nonempty α
h_2 : p.IsPath ∧ p.length = Fintype.card α - 1
hp : p.IsPath
h : p.length = Fintype.card α - 1
⊢ Injective.{1, u_1 + 1} (β := α) fun (x : Fin p.support.length) ↦ p.support.get x

Tactic:
have := p.isPath_iff_injective_get_support.mp hp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Fintype α
h_1 : Nonempty α
h_2 : p.IsPath ∧ p.length = Fintype.card α - 1
hp : p.IsPath
h : p.length = Fintype.card α - 1
this : Injective.{1, u_1 + 1} (β := α) fun (x : Fin p.support.length) ↦ p.support.get x
⊢ p.IsHamiltonian

Tactic:
isHamiltonian_iff_support_get_bijective.mpr ⟨this, this.surjective_of_finite ?_⟩

Premises used: Iff.mpr, Function.Injective.surjective_of_finite, SimpleGraph.Walk.isHamiltonian_iff_support_get_bijective, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Fintype α
h_1 : Nonempty α
h_2 : p.IsPath ∧ p.length = Fintype.card α - 1
hp : p.IsPath
h : p.length = Fintype.card α - 1
this : Injective.{1, u_1 + 1} (β := α) fun (x : Fin p.support.length) ↦ p.support.get x
neg : Fin p.support.length ≃ α
⊢ p.IsHamiltonian

Tactic:
refine isHamiltonian_iff_support_get_bijective.mpr ⟨this, this.surjective_of_finite ?_⟩

Premises used: Iff.mpr, Function.Injective.surjective_of_finite, SimpleGraph.Walk.isHamiltonian_iff_support_get_bijective, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Fintype α
h_1 : Nonempty α
h_2 : p.IsPath ∧ p.length = Fintype.card α - 1
hp : p.IsPath
h : p.length = Fintype.card α - 1
this : Injective.{1, u_1 + 1} (β := α) fun (x : Fin p.support.length) ↦ p.support.get x
neg : Fintype.card α = p.support.length
⊢ Fin p.support.length ≃ α

Tactic:
refine (Fintype.equivFinOfCardEq ?_).symm

Premises used: Fintype.equivFinOfCardEq, Equiv.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Fintype α
h_1 : Nonempty α
h_2 : p.IsPath ∧ p.length = Fintype.card α - 1
hp : p.IsPath
h : p.length = Fintype.card α - 1
this : Injective.{1, u_1 + 1} (β := α) fun (x : Fin p.support.length) ↦ p.support.get x
neg : Fintype.card α = p.length + 1
neg₁ : Fintype.card α = Fintype.card α - 1 + 1
⊢ Fintype.card α = p.support.length

Tactic:
simp_rw [length_support, h, Nat.sub_one_add_one Fintype.card_ne_zero]

Premises used: SimpleGraph.Walk.length_support, Nat.sub_one_add_one, Fintype.card_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
⊢ p.IsCycle

Tactic:
hp.toIsCycle

Premises used: SimpleGraph.Walk.IsHamiltonianCycle.toIsCycle
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
β : Type u_2
inst_1 : DecidableEq β
H : SimpleGraph β
a : α
f : G →g H
p : G.Walk a a
hf : Bijective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hp : p.IsHamiltonianCycle
simp : ∀ (x : α), List.count ((f : (a : α) → β) x) (Walk.map f p).tail.support = 1
⊢ (Walk.map f p).tail.IsHamiltonian

Tactic:
simp only [IsHamiltonian, hf.surjective.forall]

Premises used: Function.Surjective.forall, Function.Bijective.surjective, SimpleGraph.Walk.IsHamiltonian
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
β : Type u_2
inst_1 : DecidableEq β
H : SimpleGraph β
a : α
f : G →g H
p : G.Walk a a
hf : Bijective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hp : p.IsHamiltonianCycle
x : α
nil :
  ∀ (hp : IsHamiltonianCycle.{u_1} (α := α) (G := G) (a := a) Walk.nil),
    List.count ((f : (a : α) → β) x)
        (support (u := snd (u := (f : (a : α) → β) a) (Walk.map f Walk.nil)) (tail (Walk.map f Walk.nil))) =
      1
cons :
  ∀ {v : α} (y : G.Adj a v) (p : G.Walk v a) (hp : (Walk.cons y p).IsHamiltonianCycle),
    List.count ((f : (a : α) → β) x) (Walk.map f (Walk.cons y p)).tail.support = 1
⊢ List.count ((f : (a : α) → β) x) (Walk.map f p).tail.support = 1

Tactic:
rcases p with (_ | ⟨y, p⟩)
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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 : α
hp : IsHamiltonianCycle.{u_1} (α := α) (G := G) (a := a) nil
__IsCycle : IsCycle (u := (f : (a : α) → β) a) (Walk.map f nil) := ⋯
⊢ List.count ((f : (a : α) → β) x)
      (support (u := snd (u := (f : (a : α) → β) a) (Walk.map f nil)) (tail (Walk.map f nil))) =
    1

Tactic:
cases hp.ne_nil rfl

Premises used: SimpleGraph.Walk.IsHamiltonianCycle.toIsCycle, SimpleGraph.Walk.IsCircuit.ne_nil, SimpleGraph.Walk.IsCycle.isCircuit, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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 : (Walk.cons y p).IsHamiltonianCycle
__IsCycle : (Walk.map f (Walk.cons y p)).IsCycle := ⋯
cons : List.count.{u_2} (α := β) ((f : (a : α) → β) x : β) (List.map (⇑f : (a : α) → β) p.support : List β) = 1
⊢ List.count ((f : (a : α) → β) x) (Walk.map f (Walk.cons y p)).tail.support = 1

Tactic:
simp only [map_cons, getVert_cons_succ, tail_cons, support_copy, support_map]

Premises used: SimpleGraph.Walk.support_copy, SimpleGraph.Walk.tail_cons, SimpleGraph.Walk.getVert_cons_succ, SimpleGraph.Walk.map_cons, SimpleGraph.Walk.support_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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 : (Walk.cons y p).IsHamiltonianCycle
__IsCycle : (Walk.map f (Walk.cons y p)).IsCycle := ⋯
cons : List.count x p.support = 1
⊢ List.count.{u_2} (α := β) ((f : (a : α) → β) x : β) (List.map (⇑f : (a : α) → β) p.support : List β) = 1

Tactic:
rw [List.count_map_of_injective _ _ hf.injective]

Premises used: Function.Bijective.injective, List.count_map_of_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
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 x p.support = 1

Tactic:
simpa using hp.isHamiltonian_tail x

Premises used: SimpleGraph.Walk.IsHamiltonianCycle.isHamiltonian_tail
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
⊢ Finite α

Tactic:
hp.isHamiltonian_tail.finite

Premises used: SimpleGraph.Walk.IsHamiltonianCycle.isHamiltonian_tail, SimpleGraph.Walk.IsHamiltonian.finite
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
h : Infinite α
contrapose! : ∀ (h : p.IsHamiltonianCycle), Finite α
⊢ ¬p.IsHamiltonianCycle

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
h : p.IsHamiltonianCycle
⊢ Finite α

Tactic:
h.finite

Premises used: SimpleGraph.Walk.IsHamiltonianCycle.finite
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
h : p.IsHamiltonianCycle
⊢ Finite α

Tactic:
exact h.finite

Premises used: SimpleGraph.Walk.IsHamiltonianCycle.finite
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
⊢ p.IsHamiltonianCycle ↔ p.IsCycle ∧ p.tail.IsHamiltonian

Tactic:
⟨fun ⟨h, h'⟩ ↦ ⟨h, h'⟩, fun ⟨h, h'⟩ ↦ ⟨h, h'⟩⟩

Premises used: _private.0.SimpleGraph.Walk.isHamiltonianCycle_isCycle_and_isHamiltonian_tail.match_2, SimpleGraph.Walk.IsCycle, SimpleGraph.Walk.IsHamiltonianCycle.mk, And, SimpleGraph.Walk.IsHamiltonianCycle, And.intro, Iff.intro, SimpleGraph.Walk.tail, SimpleGraph.Walk.IsHamiltonian, _private.0.SimpleGraph.Walk.isHamiltonianCycle_isCycle_and_isHamiltonian_tail.match_1
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
⊢ p.IsHamiltonianCycle ↔ p.IsCycle ∧ ∀ (a_1 : α), List.count a_1 p.support.tail = 1

Tactic:
simp +contextual [isHamiltonianCycle_isCycle_and_isHamiltonian_tail,
    IsHamiltonian, support_tail_of_not_nil, IsCycle.not_nil]

Premises used: SimpleGraph.Walk.isHamiltonianCycle_isCycle_and_isHamiltonian_tail, SimpleGraph.Walk.support_tail_of_not_nil, SimpleGraph.Walk.IsHamiltonian, SimpleGraph.Walk.IsCycle.not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
b : α
⊢ b ∈ p.support

Tactic:
List.mem_of_mem_tail <|
    support_tail_of_not_nil p hp.1.not_nil ▸ hp.isHamiltonian_tail.mem_support _

Premises used: SimpleGraph.Walk.IsHamiltonianCycle.isHamiltonian_tail, Eq.rec, SimpleGraph.Walk.IsHamiltonianCycle.toIsCycle, SimpleGraph.Walk.IsHamiltonian.mem_support, List.mem_of_mem_tail, SimpleGraph.Walk.support_tail_of_not_nil, 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 α
hp : p.IsHamiltonianCycle
rw : 1 ≤ Fintype.card α
⊢ p.length = Fintype.card α

Tactic:
rw [← length_tail_add_one hp.not_nil, hp.isHamiltonian_tail.length_eq, Nat.sub_add_cancel]

Premises used: SimpleGraph.Walk.length_tail_add_one, SimpleGraph.Walk.IsHamiltonianCycle.isHamiltonian_tail, SimpleGraph.Walk.IsHamiltonianCycle.toIsCycle, Nat.sub_add_cancel, SimpleGraph.Walk.IsHamiltonian.length_eq, 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 α
hp : p.IsHamiltonianCycle
rw : Nonempty α
⊢ 1 ≤ Fintype.card α

Tactic:
rw [Nat.succ_le_iff, Fintype.card_pos_iff]

Premises used: Nat.succ_le_iff, Fintype.card_pos_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst_1 : Fintype α
hp : p.IsHamiltonianCycle
⊢ Nonempty α

Tactic:
⟨a⟩

Premises used: Nonempty.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst_1 : Fintype α
hp : p.IsHamiltonianCycle
⊢ Nonempty α

Tactic:
exact ⟨a⟩