awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
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)
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have obtain : ∀ (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)), ∃ (M : G.Subgraph), M.IsPerfectMatching
Tactic: classical
  obtain ⟨b, hb₁, hb₂⟩ := exists_bijective_of_forall_ncard_le h₁ h₂
  use hall_subgraph (fun v ↦ b v) (fun v ↦ h₁.disjoint.notMem_of_mem_right (b v).property) hb₂
  have : p₁ ∪ Set.range (fun v ↦ (b v).1) = Set.univ := by
    rw [Set.range_comp', hb₁.surjective.range_eq, Subtype.coe_image_univ]
    exact union_eq_univ_of_forall_ncard_le h₁ h₂
  refine ⟨fun v _ ↦ ?_, Subgraph.isSpanning_iff.mpr this⟩
  simp only [dite_else_false]
  split
  · exact existsUnique_eq'
  · obtain ⟨x, _⟩ := hb₁.existsUnique ⟨v, by grind⟩
    exact ⟨x, by grind⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
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)
obtain :
  ∀ (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)), ∃ (M : G.Subgraph), M.IsPerfectMatching
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have h : ∀ (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)),
  (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) sorry hb₂).IsPerfectMatching
Tactic: classical
  obtain ⟨b, hb₁, hb₂⟩ := exists_bijective_of_forall_ncard_le h₁ h₂
  use hall_subgraph (fun v ↦ b v) (fun v ↦ h₁.disjoint.notMem_of_mem_right (b v).property) hb₂
  have : p₁ ∪ Set.range (fun v ↦ (b v).1) = Set.univ := by
    rw [Set.range_comp', hb₁.surjective.range_eq, Subtype.coe_image_univ]
    exact union_eq_univ_of_forall_ncard_le h₁ h₂
  refine ⟨fun v _ ↦ ?_, Subgraph.isSpanning_iff.mpr this⟩
  simp only [dite_else_false]
  split
  · exact existsUnique_eq'
  · obtain ⟨x, _⟩ := hb₁.existsUnique ⟨v, by grind⟩
    exact ⟨x, by grind⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
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)
obtain :
  ∀ (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)), ∃ (M : G.Subgraph), M.IsPerfectMatching
h :
  ∀ (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)),
    (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).IsPerfectMatching
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have h₃ : ∀ (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),
  (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) sorry hb₂).IsPerfectMatching
Tactic: classical
  obtain ⟨b, hb₁, hb₂⟩ := exists_bijective_of_forall_ncard_le h₁ h₂
  use hall_subgraph (fun v ↦ b v) (fun v ↦ h₁.disjoint.notMem_of_mem_right (b v).property) hb₂
  have : p₁ ∪ Set.range (fun v ↦ (b v).1) = Set.univ := by
    rw [Set.range_comp', hb₁.surjective.range_eq, Subtype.coe_image_univ]
    exact union_eq_univ_of_forall_ncard_le h₁ h₂
  refine ⟨fun v _ ↦ ?_, Subgraph.isSpanning_iff.mpr this⟩
  simp only [dite_else_false]
  split
  · exact existsUnique_eq'
  · obtain ⟨x, _⟩ := hb₁.existsUnique ⟨v, by grind⟩
    exact ⟨x, by grind⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
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)
obtain :
  ∀ (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)), ∃ (M : G.Subgraph), M.IsPerfectMatching
h :
  ∀ (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)),
    (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).IsPerfectMatching
h₃ :
  ∀ (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),
    (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).IsPerfectMatching
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have h₄ : ∀ (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 ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) sorry hb₂).verts,
    ∃! w : V, (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) sorry hb₂).Adj v w
Tactic: classical
  obtain ⟨b, hb₁, hb₂⟩ := exists_bijective_of_forall_ncard_le h₁ h₂
  use hall_subgraph (fun v ↦ b v) (fun v ↦ h₁.disjoint.notMem_of_mem_right (b v).property) hb₂
  have : p₁ ∪ Set.range (fun v ↦ (b v).1) = Set.univ := by
    rw [Set.range_comp', hb₁.surjective.range_eq, Subtype.coe_image_univ]
    exact union_eq_univ_of_forall_ncard_le h₁ h₂
  refine ⟨fun v _ ↦ ?_, Subgraph.isSpanning_iff.mpr this⟩
  simp only [dite_else_false]
  split
  · exact existsUnique_eq'
  · obtain ⟨x, _⟩ := hb₁.existsUnique ⟨v, by grind⟩
    exact ⟨x, by grind⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
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)
obtain :
  ∀ (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)), ∃ (M : G.Subgraph), M.IsPerfectMatching
h :
  ∀ (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)),
    (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).IsPerfectMatching
h₃ :
  ∀ (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),
    (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).IsPerfectMatching
h₄ :
  ∀ (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 ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).verts,
      ∃! w : V, (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).Adj v w
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have h₅ : ∀ (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 ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) sorry hb₂).verts,
    ∃! w : V,
      if h : v ∈ p₁ then (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v sorry)) : V) = w
      else ∃ (h : w ∈ p₁), (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w sorry)) : V) = v
Tactic: classical
  obtain ⟨b, hb₁, hb₂⟩ := exists_bijective_of_forall_ncard_le h₁ h₂
  use hall_subgraph (fun v ↦ b v) (fun v ↦ h₁.disjoint.notMem_of_mem_right (b v).property) hb₂
  have : p₁ ∪ Set.range (fun v ↦ (b v).1) = Set.univ := by
    rw [Set.range_comp', hb₁.surjective.range_eq, Subtype.coe_image_univ]
    exact union_eq_univ_of_forall_ncard_le h₁ h₂
  refine ⟨fun v _ ↦ ?_, Subgraph.isSpanning_iff.mpr this⟩
  simp only [dite_else_false]
  split
  · exact existsUnique_eq'
  · obtain ⟨x, _⟩ := hb₁.existsUnique ⟨v, by grind⟩
    exact ⟨x, by grind⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
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)
obtain :
  ∀ (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)), ∃ (M : G.Subgraph), M.IsPerfectMatching
h :
  ∀ (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)),
    (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).IsPerfectMatching
h₃ :
  ∀ (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),
    (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).IsPerfectMatching
h₄ :
  ∀ (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 ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).verts,
      ∃! w : V, (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).Adj v w
h₅ :
  ∀ (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 ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).verts,
      ∃! w : V,
        if h : v ∈ p₁ then (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v ⋯)) : V) = w
        else ∃ (h : w ∈ p₁), (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w ⋯)) : V) = v
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have h₆ : ∀ (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 ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) sorry hb₂).verts,
    ∀ (h : v ∈ p₁), ∃! w : V, (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v sorry)) : V) = w
Tactic: classical
  obtain ⟨b, hb₁, hb₂⟩ := exists_bijective_of_forall_ncard_le h₁ h₂
  use hall_subgraph (fun v ↦ b v) (fun v ↦ h₁.disjoint.notMem_of_mem_right (b v).property) hb₂
  have : p₁ ∪ Set.range (fun v ↦ (b v).1) = Set.univ := by
    rw [Set.range_comp', hb₁.surjective.range_eq, Subtype.coe_image_univ]
    exact union_eq_univ_of_forall_ncard_le h₁ h₂
  refine ⟨fun v _ ↦ ?_, Subgraph.isSpanning_iff.mpr this⟩
  simp only [dite_else_false]
  split
  · exact existsUnique_eq'
  · obtain ⟨x, _⟩ := hb₁.existsUnique ⟨v, by grind⟩
    exact ⟨x, by grind⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Subsingleton α
v : α
⊢ List.count v p.support = 1
have rw : List.count v [a] = 1
Tactic: rw [nil_iff_support_eq.mp p.nil_of_subsingleton, Subsingleton.elim v a, List.count_singleton_self]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
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
⊢ List.count v p.support = 1
have rw₁ : List.count a [a] = 1
Tactic: rw [nil_iff_support_eq.mp p.nil_of_subsingleton, Subsingleton.elim v a, List.count_singleton_self]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
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
⊢ List.count v p.support = 1
have rw₂ : Eq (α := ℕ) 1 1
Tactic: rw [nil_iff_support_eq.mp p.nil_of_subsingleton, Subsingleton.elim v a, List.count_singleton_self]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
hp : p.IsHamiltonian
⊢ Finite α
have have : ∀ (this : Fintype α), Finite α
Tactic: have := hp.fintype
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
h : Infinite α
⊢ ¬p.IsHamiltonian
have contrapose! : ∀ (h : p.IsHamiltonian), 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 b : α
p : G.Walk a b
inst_1 : Fintype α
hp : p.IsHamiltonian
⊢ p.length + 1 = Fintype.card α
have rw : p.support.length = 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
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 α
⊢ p.length + 1 = Fintype.card α
have rw₁ : ∑ a_1 ∈ p.support.toFinset, List.count a_1 p.support = 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
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 α
⊢ p.length + 1 = Fintype.card α
have rw₂ : ∑ x ∈ p.support.toFinset, 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
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 α
⊢ p.length + 1 = Fintype.card α
have rw₃ : #p.support.toFinset = 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
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 α
⊢ p.length + 1 = Fintype.card α
have rw₄ : card.{u_1} (α := α) univ = 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
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 α
⊢ p.length + 1 = Fintype.card α
have rw₅ : Fintype.card α = 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Fintype α
hp : p.IsHamiltonian
⊢ p.support.length = Fintype.card α
have have : ∀ (this : Inhabited α), p.support.length = Fintype.card α
Tactic: have : Inhabited α := ⟨a⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
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
⊢ Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
have rw : Set.InjOn.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) {v : α | v ∈ p.support}
Tactic: rw [← Set.injOn_univ, ← hp.setOf_support]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
Goal:
α : Type u_1
inst : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst_1 : Fintype α
⊢ p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1
have pos : ∀ (h : IsEmpty α), p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1
Tactic: by_cases! h : IsEmpty α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
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
⊢ p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1
have neg : ∀ (h : Nonempty α), p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1
Tactic: by_cases! h : IsEmpty α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
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
have neg : p.IsPath ∧ p.length = Fintype.card α - 1 → ∀ (hp : p.IsPath) (h : p.length = Fintype.card α - 1), p.IsHamiltonian
Tactic: refine ⟨fun h ↦ ⟨h.isPath, h.length_eq⟩, fun ⟨hp, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (hypothesis)
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
⊢ p.IsHamiltonian
have this : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
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
have neg : Fin p.support.length ≃ α
Tactic: refine isHamiltonian_iff_support_get_bijective.mpr ⟨this, this.surjective_of_finite ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
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
⊢ Fin p.support.length ≃ α
have neg : Fintype.card α = p.support.length
Tactic: refine (Fintype.equivFinOfCardEq ?_).symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
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
⊢ Fintype.card α = p.support.length
have neg : Fintype.card α = p.length + 1
Tactic: simp_rw [length_support, h, Nat.sub_one_add_one Fintype.card_ne_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hamiltonian (goal)
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
⊢ Fintype.card α = p.support.length
have neg₁ : Fintype.card α = Fintype.card α - 1 + 1
Tactic: simp_rw [length_support, h, Nat.sub_one_add_one Fintype.card_ne_zero]
-- 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
p : G.Walk a a
hf : Bijective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hp : p.IsHamiltonianCycle
⊢ (Walk.map f p).tail.IsHamiltonian
have simp : ∀ (x : α), List.count ((f : (a : α) → β) x) (Walk.map f p).tail.support = 1
Tactic: simp only [IsHamiltonian, hf.surjective.forall]
-- 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
p : G.Walk a a
hf : Bijective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hp : p.IsHamiltonianCycle
x : α
⊢ List.count ((f : (a : α) → β) x) (Walk.map f p).tail.support = 1
have nil : ∀ (hp : IsHamiltonianCycle.{u_1} (α := α) (G := G) (a := a) nil),
  List.count ((f : (a : α) → β) x)
      (support (u := snd (u := (f : (a : α) → β) a) (Walk.map f nil)) (tail (Walk.map f nil))) =
    1
Tactic: rcases p with (_ | ⟨y, p⟩)
Cleared hypotheses: p, hp
-- 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
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
⊢ List.count ((f : (a : α) → β) x) (Walk.map f p).tail.support = 1
have cons : ∀ {v : α} (y : G.Adj a v) (p : G.Walk v a) (hp : (cons y p).IsHamiltonianCycle),
  List.count ((f : (a : α) → β) x) (Walk.map f (cons y p)).tail.support = 1
Tactic: rcases p with (_ | ⟨y, p⟩)
Cleared hypotheses: p, hp
-- 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 ((f : (a : α) → β) x) (Walk.map f (cons y p)).tail.support = 1
have cons : List.count.{u_2} (α := β) ((f : (a : α) → β) x : β) (List.map (⇑f : (a : α) → β) p.support : List β) = 1
Tactic: simp only [map_cons, getVert_cons_succ, tail_cons, support_copy, support_map]