awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic (hypothesis)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
E : Type u_3
inst : MetricSpace E
inst_1 : Subsingleton V
x : E
u v : V
ha : G.Adj u v
⊢ dist.{u_3} (α := E) (({ toFun := fun (x_1 : V) ↦ x, inj' := ⋯ : V ↪ E } : (a : V) → E) u : E)
      (({ toFun := fun (x_1 : V) ↦ x, inj' := ⋯ : V ↪ E } : (a : V) → E) v : E) =
    1
have this : G.Adj v v
Tactic: have := Subsingleton.elim u v ▸ ha
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
G : SimpleGraph V
c : Set V
⊢ G.IsIndepSet cᶜ ↔ G.IsVertexCover c
have refine : ∀ (hi : G.IsIndepSet cᶜ) (v w : V) (hadj : G.Adj v w), v ∈ c ∨ w ∈ c
Tactic: refine ⟨fun hi v w hadj ↦ ?_, by grind [IsVertexCover, Set.Pairwise]⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
G : SimpleGraph V
c : Set V
hi : G.IsIndepSet cᶜ
v w : V
hadj : G.Adj v w
⊢ v ∈ c ∨ w ∈ c
have by_contra! : ∀ (hh : v ∉ c ∧ w ∉ c), False
Tactic: by_contra! hh
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
⊢ ∃ (s : Set V), s.encard = G.vertexCoverNum ∧ G.IsVertexCover s
have this : Nonempty.{max 1 (u_1 + 1)} { s : Set V // G.IsVertexCover s }
Tactic: have : Nonempty {s : Set V // IsVertexCover G s} := nonempty_subtype.mpr ⟨Set.univ, by simp⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
G : SimpleGraph V
this : Nonempty.{max 1 (u_1 + 1)} { s : Set V // G.IsVertexCover s }
⊢ ∃ (s : Set V), s.encard = G.vertexCoverNum ∧ G.IsVertexCover s
have obtain : ∀ (s : { s : Set V // G.IsVertexCover s })
  (hs : (↑s : Set V).encard = ⨅ (x : { s : Set V // G.IsVertexCover s }), (↑x : Set V).encard),
  ∃ (s : Set V), s.encard = G.vertexCoverNum ∧ G.IsVertexCover s
Tactic: obtain ⟨s, hs⟩ := @ENat.exists_eq_iInf _ this (·.val.encard)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
G : SimpleGraph V
n : ℕ
h₁ : G.vertexCoverNum ≤ (↑n : ℕ∞)
h₂ : (↑n : ℕ∞) ≤ ENat.card V
⊢ ∃ (s : Set V), s.encard = (↑n : ℕ∞) ∧ G.IsVertexCover s
have obtain : ∀ (s : Set V) (hs₁ : s.encard = G.vertexCoverNum) (hs₂ : G.IsVertexCover s),
  ∃ (s : Set V), s.encard = (↑n : ℕ∞) ∧ G.IsVertexCover s
Tactic: obtain ⟨s, hs₁, hs₂⟩ := vertexCoverNum_exists G
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
G : SimpleGraph V
n : ℕ
h₁ : G.vertexCoverNum ≤ (↑n : ℕ∞)
h₂ : (↑n : ℕ∞) ≤ ENat.card V
s : Set V
hs₁ : s.encard = G.vertexCoverNum
hs₂ : G.IsVertexCover s
⊢ ∃ (s : Set V), s.encard = (↑n : ℕ∞) ∧ G.IsVertexCover s
have obtain : ∀ (r : Set V) (hr₁ : s ⊆ r),
  r ⊆ Set.univ → ∀ (hr₃ : r.encard = (↑n : ℕ∞)), ∃ (s : Set V), s.encard = (↑n : ℕ∞) ∧ G.IsVertexCover s
Tactic: obtain ⟨r, hr₁, _, hr₃⟩ :=
    Set.exists_superset_subset_encard_eq (by simp) (le_of_eq_of_le hs₁ h₁) (Set.encard_univ _ ▸ h₂)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.vertexCoverNum = 0 ↔ G = ⊥
have refine : ∀ (h : G.vertexCoverNum = 0), G = ⊥
Tactic: refine ⟨fun h ↦ ?_, by simp_all⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.vertexCoverNum ≤ ENat.card V - 1
have a : Nontrivial V
Tactic: nontriviality V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : Nontrivial V
⊢ G.vertexCoverNum ≤ ENat.card V - 1
have obtain : ∀ (x : V), G.vertexCoverNum ≤ ENat.card V - 1
Tactic: obtain ⟨x⟩ := not_subsingleton_iff_nontrivial.mp (not_subsingleton V) |>.to_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : Nontrivial V
x : V
⊢ G.vertexCoverNum ≤ ENat.card V - 1
have refine : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ G.vertexCoverNum), (↑n : ℕ∞) ≤ ENat.card V - 1
Tactic: refine ENat.forall_natCast_le_iff_le.mp fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
h : Nontrivial V
x : V
n : ℕ
hn : (↑n : ℕ∞) ≤ G.vertexCoverNum
⊢ (↑n : ℕ∞) ≤ ENat.card V - 1
have hn₁ : ∀ (i : Set V) (i_1 : G.IsVertexCover i), (↑n : ℕ∞) ≤ i.encard
Tactic: simp only [vertexCoverNum, le_iInf_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
h : Nontrivial V
x : V
n : ℕ
hn : ∀ (i : Set V) (i_1 : G.IsVertexCover i), (↑n : ℕ∞) ≤ i.encard
⊢ (↑n : ℕ∞) ≤ ENat.card V - 1
have this : (↑n : ℕ∞) ≤ Set.encard (α := V) (Set.univ \ {x})
Tactic: have := hn (Set.univ \ {x}) (by grind [IsVertexCover, Adj.ne'])
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Nonempty V
inst_1 : Finite V
⊢ G.vertexCoverNum < ENat.card V
have refine : G.vertexCoverNum + 1 ≤ ENat.card V
Tactic: refine (ENat.add_one_le_iff vertexCoverNum_ne_top_of_finite).mp ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Nonempty V
inst_1 : Finite V
⊢ G.vertexCoverNum + 1 ≤ ENat.card V
have grw : HSub.hSub (α := ℕ∞) (↑(Nat.card V) : ℕ∞) 1 + 1 ≤ (↑(Nat.card V) : ℕ∞)
Tactic: grw [vertexCoverNum_le_card_sub_one, ENat.card_eq_coe_natCard]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Nonempty V
inst_1 : Finite V
⊢ HSub.hSub (α := ℕ∞) (↑(Nat.card V) : ℕ∞) 1 + 1 ≤ (↑(Nat.card V) : ℕ∞)
have enat_to_nat : Nat.card V - 1 + 1 ≤ Nat.card V
Tactic: enat_to_nat
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.vertexCoverNum ≤ G.edgeSet.encard
have pos : ∀ (h' : G.edgeSet = ∅), G.vertexCoverNum ≤ G.edgeSet.encard
Tactic: by_cases h' : G.edgeSet = ∅
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
G : SimpleGraph V
pos : ∀ (h' : G.edgeSet = ∅), G.vertexCoverNum ≤ G.edgeSet.encard
⊢ G.vertexCoverNum ≤ G.edgeSet.encard
have neg : ∀ (h' : ¬G.edgeSet = ∅), G.vertexCoverNum ≤ G.edgeSet.encard
Tactic: by_cases h' : G.edgeSet = ∅
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h' : ¬G.edgeSet = ∅
⊢ G.vertexCoverNum ≤ G.edgeSet.encard
have neg : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ G.vertexCoverNum), (↑n : ℕ∞) ≤ G.edgeSet.encard
Tactic: refine ENat.forall_natCast_le_iff_le.mp fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
h' : ¬G.edgeSet = ∅
n : ℕ
hn : (↑n : ℕ∞) ≤ G.vertexCoverNum
⊢ (↑n : ℕ∞) ≤ G.edgeSet.encard
have hn₁ : ∀ (i : Set V) (i_1 : G.IsVertexCover i), (↑n : ℕ∞) ≤ i.encard
Tactic: simp only [vertexCoverNum, le_iInf_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
h' : ¬G.edgeSet = ∅
n : ℕ
hn : ∀ (i : Set V) (i_1 : G.IsVertexCover i), (↑n : ℕ∞) ≤ i.encard
⊢ (↑n : ℕ∞) ≤ G.edgeSet.encard
have this : (↑n : ℕ∞) ≤ Set.encard (α := V) ((fun (x : Sym2 V) ↦ (Quot.out (r := Sym2.Rel V) x).1) '' G.edgeSet)
Tactic: have := hn ((·.out.1) '' G.edgeSet)
    (fun v w _ ↦ by grind [Sym2.out_fst_mem s(v, w), mem_edgeSet])
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (hypothesis)
Goal:
V : Type u_1
⊢ (completeGraph V).vertexCoverNum = ENat.card V - 1
have a : Nontrivial V
Tactic: nontriviality V using tsub_eq_zero_of_le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
h : Nontrivial V
⊢ (completeGraph V).vertexCoverNum = ENat.card V - 1
have refine_1 : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ (completeGraph V).vertexCoverNum), (↑n : ℕ∞) ≤ ENat.card V - 1
Tactic: refine ENat.eq_of_forall_natCast_le_iff fun n ↦ ⟨fun hn ↦ ?_, fun hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
h : Nontrivial V
refine_1 : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ (completeGraph V).vertexCoverNum), (↑n : ℕ∞) ≤ ENat.card V - 1
⊢ (completeGraph V).vertexCoverNum = ENat.card V - 1
have refine_2 : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ ENat.card V - 1), (↑n : ℕ∞) ≤ (completeGraph V).vertexCoverNum
Tactic: refine ENat.eq_of_forall_natCast_le_iff fun n ↦ ⟨fun hn ↦ ?_, fun hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ (completeGraph V).vertexCoverNum
⊢ (↑n : ℕ∞) ≤ ENat.card V - 1
have refine_1 : (completeGraph V).vertexCoverNum ≤ ENat.card V - 1
Tactic: grw [hn, vertexCoverNum_le_card_sub_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ (completeGraph V).vertexCoverNum
refine_1 : (completeGraph V).vertexCoverNum ≤ ENat.card V - 1
⊢ (↑n : ℕ∞) ≤ ENat.card V - 1
have refine_1₁ : ENat.card V - 1 ≤ ENat.card V - 1
Tactic: grw [hn, vertexCoverNum_le_card_sub_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
⊢ (↑n : ℕ∞) ≤ (completeGraph V).vertexCoverNum
have refine_2 : ∀ (hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)), False
Tactic: by_contra! hh
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
⊢ HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
have grw : ENat.card V - 1 ≤ ENat.card V + 1
Tactic: grw [tsub_le_iff_right, hn]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (hypothesis)
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
⊢ False
have this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
Tactic: have : n - 1 ≤ ENat.card V := by
    grw [tsub_le_iff_right, hn]
    simp [add_assoc, one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
⊢ False
have refine_2 : ∀ (t : Set V) (ht₁ : t.encard = (↑(n - 1) : ℕ∞)) (ht₂ : (completeGraph V).IsVertexCover t), False
Tactic: obtain ⟨t, ht₁, ht₂⟩ := exists_of_le_vertexCoverNum (n - 1) (ENat.le_sub_one_of_lt hh) this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
⊢ 1 < (Set.univ \ t).encard
have refine : HAdd.hAdd (α := ℕ∞) 1 1 ≤ (Set.univ \ t).encard
Tactic: refine ENat.add_one_le_iff (by simp) |>.mp ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
⊢ HAdd.hAdd (α := ℕ∞) 1 1 ≤ (Set.univ \ t).encard
have rw : HAdd.hAdd (α := ℕ∞) 1 1 ≤ ENat.card V - t.encard
Tactic: rw [Set.encard_diff (by simp) (Set.finite_of_encard_eq_coe ht₁), Set.encard_univ]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
⊢ HAdd.hAdd (α := ℕ∞) 1 1 ≤ ENat.card V - t.encard
have refine : t.encard + HAdd.hAdd (α := ℕ∞) 1 1 ≤ ENat.card V
Tactic: refine ENat.le_sub_of_add_le_left (by simp [ht₁]) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
⊢ t.encard + HAdd.hAdd (α := ℕ∞) 1 1 ≤ ENat.card V
have refine : t.encard ≤ ENat.card V - HAdd.hAdd (α := ℕ∞) 1 1
Tactic: refine add_le_of_le_tsub_right_of_le (Order.add_one_le_of_lt ENat.one_lt_card) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
⊢ t.encard ≤ ENat.card V - HAdd.hAdd (α := ℕ∞) 1 1
have grw : ENat.card V - 1 - (↑1 : ℕ∞) ≤ ENat.card V - HAdd.hAdd (α := ℕ∞) 1 1
Tactic: grw [ht₁, ENat.coe_sub, hn]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (hypothesis)
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
⊢ False
have this₁ : 1 < (Set.univ \ t).encard
Tactic: have : 1 < (Set.univ \ t).encard := by
    refine ENat.add_one_le_iff (by simp) |>.mp ?_
    rw [Set.encard_diff (by simp) (Set.finite_of_encard_eq_coe ht₁), Set.encard_univ]
    refine ENat.le_sub_of_add_le_left (by simp [ht₁]) ?_
    refine add_le_of_le_tsub_right_of_le (Order.add_one_le_of_lt ENat.one_lt_card) ?_
    grw [ht₁, ENat.coe_sub, hn]
    simp [add_assoc, one_add_one_eq_two, le_tsub_add]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this_1 : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
this : 1 < (Set.univ \ t).encard
⊢ False
have refine_2 : ∀ (a b : V), a ∈ Set.univ \ t → b ∈ Set.univ \ t → ∀ (hne : a ≠ b), False
Tactic: obtain ⟨a, b, _, _, hne⟩ := Set.one_lt_encard_iff.mp <| this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (hypothesis)
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this_1 : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
this : 1 < (Set.univ \ t).encard
a b : V
left : a ∈ Set.univ \ t
left_1 : b ∈ Set.univ \ t
hne : a ≠ b
⊢ False
have this₁ : a ∈ t ∨ b ∈ t
Tactic: have := @ht₂ a b (by simp [hne])
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
⊢ G.vertexCoverNum ≤ H.vertexCoverNum
have have : ∀ (f : G →g H) (hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)),
  G.vertexCoverNum ≤ H.vertexCoverNum
Tactic: have ⟨f, hf⟩ := h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
⊢ G.vertexCoverNum ≤ H.vertexCoverNum
have obtain : ∀ (s : Set W) (hs₁ : s.encard = H.vertexCoverNum) (hs₂ : H.IsVertexCover s), G.vertexCoverNum ≤ H.vertexCoverNum
Tactic: obtain ⟨s, hs₁, hs₂⟩ := vertexCoverNum_exists H
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (hypothesis)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
⊢ G.vertexCoverNum ≤ H.vertexCoverNum
have this : IsAntichain H.Adj sᶜ
Tactic: have := H.isIndepSet_iff_isAntichain_adj.mp <| isIndepSet_compl_iff_isVertexCover.mpr hs₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (hypothesis)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
this : IsAntichain H.Adj sᶜ
⊢ G.vertexCoverNum ≤ H.vertexCoverNum
have this₁ : IsAntichain G.Adj ((⇑f : (a : V) → W) ⁻¹' sᶜ)
Tactic: have : IsAntichain G.Adj (f ⁻¹' sᶜ) := this.preimage hf (fun _ _ hadj ↦ f.map_rel' hadj)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (hypothesis)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
this_1 : IsAntichain H.Adj sᶜ
this : IsAntichain G.Adj ((⇑f : (a : V) → W) ⁻¹' sᶜ)
⊢ G.vertexCoverNum ≤ H.vertexCoverNum
have this₁ : G.IsVertexCover ((⇑f : (a : V) → W) ⁻¹' s)
Tactic: have : G.IsVertexCover (f ⁻¹' s) :=
    isIndepSet_compl_iff_isVertexCover.mp <| G.isIndepSet_iff_isAntichain_adj.mpr this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.VertexCover (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
this_1 : IsAntichain H.Adj sᶜ
this_2 : IsAntichain G.Adj ((⇑f : (a : V) → W) ⁻¹' sᶜ)
this : G.IsVertexCover ((⇑f : (a : V) → W) ⁻¹' s)
⊢ G.vertexCoverNum ≤ H.vertexCoverNum
have grw : Set.encard.{u_1} (α := V) ((⇑f : (a : V) → W) ⁻¹' s) ≤ s.encard
Tactic: grw [this.vertexCoverNum_le, ← hs₁]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support ≠ []
have nil : Ne.{u + 1} (α := List V) (support (G := G) (u := u) nil) []
Tactic: cases p
Cleared hypotheses: v, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : Ne.{u + 1} (α := List V) (support (G := G) (u := u) Walk.nil) []
⊢ p.support ≠ []
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (cons h p).support ≠ []
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
⊢ p.support.head ⋯ = a
have nil : List.head (support (G := G) (u := a) nil) sorry = a
Tactic: cases p
Cleared hypotheses: b, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
nil : List.head (support (G := G) (u := a) Walk.nil) ⋯ = a
⊢ p.support.head ⋯ = a
have cons : ∀ {v : V} (h : G.Adj a v) (p : G.Walk v b), (cons h p).support.head sorry = a
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
⊢ p.support.getLast ⋯ = b
have nil : ∀ {u : V}, List.getLast (support (G := G) (u := u) nil) sorry = u
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
nil : ∀ {u : V}, List.getLast (support (G := G) (u := u) Walk.nil) ⋯ = u
⊢ p.support.getLast ⋯ = b
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w), p.support.getLast sorry = w → (cons h p).support.getLast sorry = w
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u :: p.support.tail = p.support
have nil : u :: List.tail (support (G := G) (u := u) nil) = support (G := G) (u := u) nil
Tactic: cases p
Cleared hypotheses: v, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : u :: List.tail (support (G := G) (u := u) Walk.nil) = support (G := G) (u := u) Walk.nil
⊢ u :: p.support.tail = p.support
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), u :: (cons h p).support.tail = (cons h p).support
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support = u :: p.support.tail
have nil : support (G := G) (u := u) nil = u :: List.tail (support (G := G) (u := u) nil)
Tactic: cases p
Cleared hypotheses: v, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : support (G := G) (u := u) Walk.nil = u :: List.tail (support (G := G) (u := u) Walk.nil)
⊢ p.support = u :: p.support.tail
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (cons h p).support = u :: (cons h p).support.tail
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u ∈ p.support
have nil : Membership.mem (γ := List V) (support (G := G) (u := u) nil) u
Tactic: cases p
Cleared hypotheses: v, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : Membership.mem (γ := List V) (support (G := G) (u := u) Walk.nil) u
⊢ u ∈ p.support
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), u ∈ (cons h p).support
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ v ∈ p.support
have nil : ∀ {u : V}, Membership.mem (γ := List V) (support (G := G) (u := u) nil) u
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : ∀ {u : V}, Membership.mem (γ := List V) (support (G := G) (u := u) Walk.nil) u
⊢ v ∈ p.support
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w), w ∈ p.support → w ∈ (cons h p).support
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support ↔ w = u ∨ w ∈ p.support.tail
have nil : Membership.mem (γ := List V) (support (G := G) (u := u) nil) w ↔
  w = u ∨ Membership.mem (γ := List V) (List.tail (support (G := G) (u := u) nil)) w
Tactic: cases p
Cleared hypotheses: v, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
nil :
  Membership.mem (γ := List V) (support (G := G) (u := u) Walk.nil) w ↔
    w = u ∨ Membership.mem (γ := List V) (List.tail (support (G := G) (u := u) Walk.nil)) w
⊢ w ∈ p.support ↔ w = u ∨ w ∈ p.support.tail
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), w ∈ (cons h p).support ↔ w = u ∨ w ∈ (cons h p).support.tail
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : u ≠ v
p : G.Walk u v
⊢ v ∈ p.support.tail
have obtain : ∀ (w : V) (w_1 : G.Adj u w) (w_2 : G.Walk w v), v ∈ (cons w_1 w_2).support.tail
Tactic: obtain ⟨_, _, _, rfl⟩ := exists_eq_cons_of_ne h p
Cleared hypotheses: p