awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
simp_rw :
  ∀ (a b : αs),
    a ≤ b ∧ a ≠ b →
      ∃ (x_1 : αs), (a ≤ x_1 ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = x_1.fst (β := fun (i : ℕ) ↦ α i)) ∧ x_1 ≤ b
⊢ IsStronglyAtomic αs

Tactic:
simp_rw [isStronglyAtomic_iff, lt_iff_le_and_ne, hcovby]

Premises used: isStronglyAtomic_iff, lt_iff_le_and_ne
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
i : ℕ
a b : α i
hne : Sigma.mk (β := fun (i : ℕ) ↦ α i) i a ≠ Sigma.mk (β := fun (i : ℕ) ↦ α i) i b
hij : i ≤ i
h2 : π hij b = a
⊢ False

Tactic:
simp [← h2, π_refl] at hne
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
i : ℕ
a : α i
j : ℕ
b : α j
hne : Sigma.mk (β := fun (i : ℕ) ↦ α i) i a ≠ Sigma.mk (β := fun (i : ℕ) ↦ α i) j b
hij : i ≤ j
h2 : π hij b = a
⊢ i + 1 ≤ j

Tactic:
have hle : i + 1 ≤ j := hij.lt_of_ne (by rintro rfl; simp [← h2, π_refl] at hne)
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
i : ℕ
a : α i
j : ℕ
b : α j
hne : Sigma.mk (β := fun (i : ℕ) ↦ α i) i a ≠ Sigma.mk (β := fun (i : ℕ) ↦ α i) j b
hij : i ≤ j
h2 : π hij b = a
hle : i + 1 ≤ j
⊢ (Sigma.mk (β := fun (i : ℕ) ↦ α i) i a).fst (β := fun (i : ℕ) ↦ α i) ≤
    (Sigma.mk (β := fun (i : ℕ) ↦ α i) (i + 1) (π hle b)).fst (β := fun (i : ℕ) ↦ α i)

Tactic:
simp
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
i : ℕ
a : α i
j : ℕ
b : α j
hne : Sigma.mk (β := fun (i : ℕ) ↦ α i) i a ≠ Sigma.mk (β := fun (i : ℕ) ↦ α i) j b
hij : i ≤ j
h2 : π hij b = a
hle : i + 1 ≤ j
rw : π ⋯ b = (Sigma.mk (β := fun (i : ℕ) ↦ α i) i a).snd (β := fun (i : ℕ) ↦ α i)
rw₁ rw₂ : π ⋯ b = (Sigma.mk (β := fun (i : ℕ) ↦ α i) i (π hij b)).snd (β := fun (i : ℕ) ↦ α i)
⊢ π ⋯ ((Sigma.mk (β := fun (i : ℕ) ↦ α i) (i + 1) (π hle b)).snd (β := fun (i : ℕ) ↦ α i)) =
    (Sigma.mk (β := fun (i : ℕ) ↦ α i) i a).snd (β := fun (i : ℕ) ↦ α i)

Tactic:
rw [π_trans, ← h2]
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
i : ℕ
a : α i
j : ℕ
b : α j
hne : Sigma.mk (β := fun (i : ℕ) ↦ α i) i a ≠ Sigma.mk (β := fun (i : ℕ) ↦ α i) j b
hij : i ≤ j
h2 : π hij b = a
hle : i + 1 ≤ j
⊢ (Sigma.mk (β := fun (i : ℕ) ↦ α i) i a).fst (β := fun (i : ℕ) ↦ α i) + 1 =
    (Sigma.mk (β := fun (i : ℕ) ↦ α i) (i + 1) (π hle b)).fst (β := fun (i : ℕ) ↦ α i)

Tactic:
simp
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
i : ℕ
a : α i
j : ℕ
b : α j
hne : Sigma.mk (β := fun (i : ℕ) ↦ α i) i a ≠ Sigma.mk (β := fun (i : ℕ) ↦ α i) j b
hij : i ≤ j
h2 : π hij b = a
hle : i + 1 ≤ j
⊢ π hle ((Sigma.mk (β := fun (i : ℕ) ↦ α i) j b).snd (β := fun (i : ℕ) ↦ α i)) =
    (Sigma.mk (β := fun (i : ℕ) ↦ α i) (i + 1) (π hle b)).snd (β := fun (i : ℕ) ↦ α i)

Tactic:
simp
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
i : ℕ
a : α i
j : ℕ
b : α j
hne : Sigma.mk (β := fun (i : ℕ) ↦ α i) i a ≠ Sigma.mk (β := fun (i : ℕ) ↦ α i) j b
hij : i ≤ j
h2 : π hij b = a
hle : i + 1 ≤ j
⊢ ∃ (x_1 : αs),
    (Sigma.mk (β := fun (i : ℕ) ↦ α i) i a ≤ x_1 ∧
        (Sigma.mk (β := fun (i : ℕ) ↦ α i) i a).fst (β := fun (i : ℕ) ↦ α i) + 1 = x_1.fst (β := fun (i : ℕ) ↦ α i)) ∧
      x_1 ≤ Sigma.mk (β := fun (i : ℕ) ↦ α i) j b

Tactic:
exact ⟨⟨_, π hle b⟩, ⟨⟨by simp, by rw [π_trans, ← h2]⟩, by simp⟩, ⟨hle, by simp⟩⟩
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
⊢ IsStronglyAtomic αs

Tactic:
have : IsStronglyAtomic αs := by
    simp_rw [isStronglyAtomic_iff, lt_iff_le_and_ne, hcovby]
    rintro ⟨i, a⟩ ⟨j, b⟩ ⟨⟨hij : i ≤ j, h2 : π hij b = a⟩, hne⟩
    have hle : i + 1 ≤ j := hij.lt_of_ne (by rintro rfl; simp [← h2, π_refl] at hne)
    exact ⟨⟨_, π hle b⟩, ⟨⟨by simp, by rw [π_trans, ← h2]⟩, by simp⟩, ⟨hle, by simp⟩⟩
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
this : IsStronglyAtomic αs
obtain :
  ∀ (a₀ : α 0)
    (ha₀ :
      Infinite.{u_1 + 1}
        (↑(preimage (β := α 0) (fun (a : αs) ↦ π ⋯ (a.snd (β := fun (i : ℕ) ↦ α i))) {a₀}) : Type u_1)),
    ∃ (a₀ : αs), a₀.fst (β := fun (i : ℕ) ↦ α i) = 0 ∧ (Ici a₀).Infinite
⊢ ∃ (a₀ : αs), a₀.fst (β := fun (i : ℕ) ↦ α i) = 0 ∧ (Ici a₀).Infinite

Tactic:
obtain ⟨a₀, ha₀⟩ := Finite.exists_infinite_fiber (fun (a : αs) ↦ π zero_le a.2)

Premises used: zero_le, Sigma.snd, Finite.exists_infinite_fiber
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
this : IsStronglyAtomic αs
a₀ : α 0
ha₀ : Infinite.{u_1 + 1} (↑(preimage (β := α 0) (fun (a : αs) ↦ π ⋯ (a.snd (β := fun (i : ℕ) ↦ α i))) {a₀}) : Type u_1)
⊢ ∃ (a₀ : αs), a₀.fst (β := fun (i : ℕ) ↦ α i) = 0 ∧ (Ici a₀).Infinite

Tactic:
⟨⟨0, a₀⟩, rfl, (infinite_coe_iff.1 ha₀).mono ?_⟩

Premises used: Set.Infinite.mono, Set.infinite_coe_iff, And.intro, Exists.intro, Iff.mp, Sigma.mk, OfNat.ofNat, rfl
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
this : IsStronglyAtomic αs
a₀ : α 0
ha₀ : Infinite.{u_1 + 1} (↑(preimage (β := α 0) (fun (a : αs) ↦ π ⋯ (a.snd (β := fun (i : ℕ) ↦ α i))) {a₀}) : Type u_1)
refine :
  preimage (β := α 0) (fun (a : αs) ↦ π ⋯ (a.snd (β := fun (i : ℕ) ↦ α i))) {a₀} ⊆
    Ici (Sigma.mk (β := fun (i : ℕ) ↦ α i) 0 a₀)
⊢ ∃ (a₀ : αs), a₀.fst (β := fun (i : ℕ) ↦ α i) = 0 ∧ (Ici a₀).Infinite

Tactic:
refine ⟨⟨0, a₀⟩, rfl, (infinite_coe_iff.1 ha₀).mono ?_⟩
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
this : IsStronglyAtomic αs
a₀ : α 0
ha₀ : Infinite.{u_1 + 1} (↑(preimage (β := α 0) (fun (a : αs) ↦ π ⋯ (a.snd (β := fun (i : ℕ) ↦ α i))) {a₀}) : Type u_1)
simp : ∀ (a : ℕ) (b : α a), π ⋯ b = a₀ → Sigma.mk (β := fun (i : ℕ) ↦ α i) 0 a₀ ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) a b
⊢ preimage (β := α 0) (fun (a : αs) ↦ π ⋯ (a.snd (β := fun (i : ℕ) ↦ α i))) {a₀} ⊆
    Ici (Sigma.mk (β := fun (i : ℕ) ↦ α i) 0 a₀)

Tactic:
simp only [αs, subset_def, mem_preimage, mem_singleton_iff, mem_Ici, Sigma.forall]

Premises used: Set.subset_def, Sigma.forall, Set.mem_singleton_iff, Set.mem_Ici, Set.mem_preimage
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
this : IsStronglyAtomic αs
a₀ : α 0
ha₀ : Infinite.{u_1 + 1} (↑(preimage (β := α 0) (fun (a : αs) ↦ π ⋯ (a.snd (β := fun (i : ℕ) ↦ α i))) {a₀}) : Type u_1)
⊢ ∀ (a : ℕ) (b : α a), π ⋯ b = a₀ → Sigma.mk (β := fun (i : ℕ) ↦ α i) 0 a₀ ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) a b

Tactic:
fun i x h ↦ ⟨zero_le, h⟩

Premises used: zero_le, Exists.intro
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
this : IsStronglyAtomic αs
a₀ : α 0
ha₀ : Infinite.{u_1 + 1} (↑(preimage (β := α 0) (fun (a : αs) ↦ π ⋯ (a.snd (β := fun (i : ℕ) ↦ α i))) {a₀}) : Type u_1)
⊢ ∀ (a : ℕ) (b : α a), π ⋯ b = a₀ → Sigma.mk (β := fun (i : ℕ) ↦ α i) 0 a₀ ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) a b

Tactic:
exact fun i x h ↦ ⟨zero_le, h⟩
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
this : IsStronglyAtomic αs
obtain :
  ∀ (a₀ : αs) (ha₀ : a₀.fst (β := fun (i : ℕ) ↦ α i) = 0) (ha₀inf : (Ici a₀).Infinite),
    ∃ (f : (i : ℕ) → α i), ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i
⊢ ∃ (f : (i : ℕ) → α i), ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i

Tactic:
obtain ⟨a₀, ha₀, ha₀inf⟩ : ∃ a₀ : αs, a₀.1 = 0 ∧ (Ici a₀).Infinite := by
    obtain ⟨a₀, ha₀⟩ := Finite.exists_infinite_fiber (fun (a : αs) ↦ π zero_le a.2)
    refine ⟨⟨0, a₀⟩, rfl, (infinite_coe_iff.1 ha₀).mono ?_⟩
    simp only [αs, subset_def, mem_preimage, mem_singleton_iff, mem_Ici, Sigma.forall]
    exact fun i x h ↦ ⟨zero_le, h⟩
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst (β := fun (i : ℕ) ↦ α i) = 0
ha₀inf : (Ici a₀).Infinite
⊢ ∀ (a : αs), Set.Finite.{u_1} (α := αs) {x_1 : αs | a ⋖ x_1}

Tactic:
fun ⟨i, a⟩ ↦ ((hfin i a).image (fun b ↦ ⟨_, b⟩)).subset ?_

Premises used: CovBy, setOf, Set.Finite, Set.Finite.subset, Set.Finite.image, _private.0.exists_seq_forall_proj_of_forall_finite.match_13
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst (β := fun (i : ℕ) ↦ α i) = 0
ha₀inf : (Ici a₀).Infinite
refine :
  ∀ (x_1 : αs) (i : ℕ) (a : α i),
    Subset.{u_1} (α := Set αs) {x_2 : αs | Sigma.mk (β := fun (i : ℕ) ↦ α i) i a ⋖ x_2}
      ((fun (b : α (i + 1)) ↦ Sigma.mk (β := fun (i : ℕ) ↦ α i) (i + 1) b) '' {b : α (i + 1) | π ⋯ b = a})
⊢ ∀ (a : αs), Set.Finite.{u_1} (α := αs) {x_1 : αs | a ⋖ x_1}

Tactic:
refine fun ⟨i, a⟩ ↦ ((hfin i a).image (fun b ↦ ⟨_, b⟩)).subset ?_
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst (β := fun (i : ℕ) ↦ α i) = 0
ha₀inf : (Ici a₀).Infinite
x_1 : αs
i : ℕ
a : α i
simp :
  ∀ (a_1 : ℕ) (b : α a_1),
    Sigma.mk (β := fun (i : ℕ) ↦ α i) i a ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) a_1 b →
      i + 1 = a_1 →
        ∃ (x : α (i + 1)),
          π ⋯ x = a ∧ Sigma.mk (β := fun (i : ℕ) ↦ α i) (i + 1) x = Sigma.mk (β := fun (a : ℕ) ↦ α a) a_1 b
⊢ Subset.{u_1} (α := Set αs) {x_2 : αs | Sigma.mk (β := fun (i : ℕ) ↦ α i) i a ⋖ x_2}
    ((fun (b : α (i + 1)) ↦ Sigma.mk (β := fun (i : ℕ) ↦ α i) (i + 1) b) '' {b : α (i + 1) | π ⋯ b = a})

Tactic:
simp only [αs, hcovby, subset_def, mem_setOf_eq, mem_image, and_imp, Sigma.forall]

Premises used: Set.subset_def, and_imp, Set.mem_image, Sigma.forall, Set.mem_setOf_eq
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst (β := fun (i : ℕ) ↦ α i) = 0
ha₀inf : (Ici a₀).Infinite
x_1 : αs
i : ℕ
a : α i
j : ℕ
b : α j
h : Sigma.mk (β := fun (i : ℕ) ↦ α i) i a ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) j b
hj : i + 1 = j
w :
  (Sigma.mk (β := fun (i : ℕ) ↦ α i) i a).fst (β := fun (i : ℕ) ↦ α i) ≤
    (Sigma.mk (β := fun (a : ℕ) ↦ α a) j b).fst (β := fun (i : ℕ) ↦ α i)
h_1 :
  π w ((Sigma.mk (β := fun (a : ℕ) ↦ α a) j b).snd (β := fun (i : ℕ) ↦ α i)) =
    (Sigma.mk (β := fun (i : ℕ) ↦ α i) i a).snd (β := fun (i : ℕ) ↦ α i)
rwa rwa₁ rwa₂ rwa₃ : π ⋯ b = a
⊢ π ⋯ (π ⋯ b) = a

Tactic:
rwa [π_trans]
-- Module: Mathlib.Order.KonigLemma
Goal:
α : ℕ → Type u_1
inst : Finite.{u_1 + 1} (α 0)
inst_1 : ∀ (i : ℕ), Nonempty.{u_1 + 1} (α i)
π : {i j : ℕ} → (hij : i ≤ j) → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x : PartialOrder αs :=
  { le := fun (a b : αs) ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst (β := fun (i : ℕ) ↦ α i) = 0
ha₀inf : (Ici a₀).Infinite
x_1 : αs
i : ℕ
a : α i
j : ℕ
b : α j
h : Sigma.mk (β := fun (i : ℕ) ↦ α i) i a ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) j b
hj : i + 1 = j
w :
  (Sigma.mk (β := fun (i : ℕ) ↦ α i) i a).fst (β := fun (i : ℕ) ↦ α i) ≤
    (Sigma.mk (β := fun (a : ℕ) ↦ α a) j b).fst (β := fun (i : ℕ) ↦ α i)
h_1 :
  π w ((Sigma.mk (β := fun (a : ℕ) ↦ α a) j b).snd (β := fun (i : ℕ) ↦ α i)) =
    (Sigma.mk (β := fun (i : ℕ) ↦ α i) i a).snd (β := fun (i : ℕ) ↦ α i)
refl :
  ∀ (b : α (i + 1)),
    Sigma.mk (β := fun (i : ℕ) ↦ α i) i a ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b →
      ∀
        (w :
          (Sigma.mk (β := fun (i : ℕ) ↦ α i) i a).fst (β := fun (i : ℕ) ↦ α i) ≤
            (Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b).fst (β := fun (i : ℕ) ↦ α i)),
        π w ((Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b).snd (β := fun (i : ℕ) ↦ α i)) =
            (Sigma.mk (β := fun (i : ℕ) ↦ α i) i a).snd (β := fun (i : ℕ) ↦ α i) →
          Sigma.mk (β := fun (i : ℕ) ↦ α i) (i + 1) (π ⋯ b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b
⊢ Sigma.mk (β := fun (i : ℕ) ↦ α i) (i + 1) (π ⋯ b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) j b

Tactic:
cases hj