awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
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 := ⋯ }
i j : ℕ
b : α j
h : i ≤ j
h_1 :
  ¬Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) j b ∧
    ∀ (a : ℕ) (b_1 : α a),
      Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b) ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 →
        Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) j b →
          ¬Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 = Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b) →
            Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 = Sigma.mk (β := fun (a : ℕ) ↦ α a) j b
hne : ¬Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) j b
h' :
  ∀ (a : ℕ) (b_1 : α a),
    Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b) ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 →
      Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) j b →
        ¬Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 = Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b) →
          Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 = Sigma.mk (β := fun (a : ℕ) ↦ α a) j b
hle' : i + 1 ≤ j
⊢ π ⋯ ((Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) (π hle' b)).snd (β := fun (i : ℕ) ↦ α i)) =
    (Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b)).snd (β := fun (i : ℕ) ↦ α i)
have rw : π sorry b = (Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b)).snd (β := fun (i : ℕ) ↦ α i)
Tactic: rw [π_trans]
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
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 := ⋯ }
i : ℕ
b : α (i + 1)
h : i ≤ i + 1
⊢ ¬Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b ∧
    ∀ (a : ℕ) (b_1 : α a),
      Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b) ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 →
        Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b →
          ¬Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 = Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b) →
            Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 = Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b
have refine_2 : ∀ (a : ℕ) (b_1 : α a),
  Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b) ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 →
    Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b →
      ¬Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 = Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b) →
        Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 = Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b
Tactic: refine ⟨fun h ↦ by simp at h, ?_⟩
-- Lean 4 proof step from Mathlib.Order.KonigLemma (hypothesis)
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 := ⋯ }
i : ℕ
b : α (i + 1)
h : i ≤ i + 1
j : ℕ
hij : i ≤ j
hji : j ≤ i + 1
hcb : π hij (π hji b) = π h b
hne : ¬Sigma.mk (β := fun (a : ℕ) ↦ α a) j (π hji b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b)
⊢ Sigma.mk (β := fun (a : ℕ) ↦ α a) j (π hji b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b
have hne₁ : i ≠ j
Tactic: replace hne := show i ≠ j by rintro rfl; contradiction
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
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 := ⋯ }
i : ℕ
b : α (i + 1)
h : i ≤ i + 1
j : ℕ
hij : i ≤ j
hji : j ≤ i + 1
hcb : π hij (π hji b) = π h b
hne : i ≠ j
⊢ Sigma.mk (β := fun (a : ℕ) ↦ α a) j (π hji b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b
have refine_2 : ∀ (hij : i ≤ i + 1) (hji : i + 1 ≤ i + 1) (hcb : π hij (π hji b) = π h b) (hne : i ≠ i + 1),
  Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) (π hji b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b
Tactic: obtain rfl := hji.antisymm (hij.lt_of_ne hne)
Cleared hypotheses: j, hij, hji, hcb, hne
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
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 := ⋯ }
i : ℕ
b : α (i + 1)
h hij : i ≤ i + 1
hji : i + 1 ≤ i + 1
hcb : π hij (π hji b) = π h b
hne : i ≠ i + 1
⊢ Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) (π hji b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b
have refine_2 : Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b = Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b
Tactic: rw [π_refl]
-- Lean 4 proof step from Mathlib.Order.KonigLemma (hypothesis)
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 := ⋯ }
⊢ ∃ (f : (i : ℕ) → α i), ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i
have hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
Tactic: have hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.1 + 1 = b.1 := by
    simp only [αs, covBy_iff_lt_and_eq_or_eq, lt_iff_le_and_ne, ne_eq, Sigma.forall, and_assoc,
      and_congr_right_iff, or_iff_not_imp_left]
    rintro i a j b ⟨h : i ≤ j, rfl : π h b = a⟩
    refine ⟨fun ⟨hne, h'⟩ ↦ ?_, ?_⟩
    · have hle' : i + 1 ≤ j := h.lt_of_ne <| by rintro rfl; simp [π_refl] at hne
      exact congr_arg Sigma.fst <| h' (i + 1) (π hle' b) ⟨by simp, by rw [π_trans]⟩ ⟨hle', by simp⟩
        (fun h ↦ by simp at h)
    rintro rfl
    refine ⟨fun h ↦ by simp at h, ?_⟩
    rintro j c ⟨hij : i ≤ j, hcb : π _ c = π _ b⟩ ⟨hji : j ≤ i + 1, rfl : π hji b = c⟩ hne
    replace hne := show i ≠ j by rintro rfl; contradiction
    obtain rfl := hji.antisymm (hij.lt_of_ne hne)
    rw [π_refl]
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
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
have 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
Tactic: simp_rw [isStronglyAtomic_iff, lt_iff_le_and_ne, hcovby]
-- Lean 4 proof step from Mathlib.Order.KonigLemma (hypothesis)
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
⊢ ∃ (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
have hle : i + 1 ≤ j
Tactic: have hle : i + 1 ≤ j := hij.lt_of_ne (by rintro rfl; simp [← h2, π_refl] at hne)
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
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 + 1) (π hle b)).snd (β := fun (i : ℕ) ↦ α i)) =
    (Sigma.mk (β := fun (i : ℕ) ↦ α i) i a).snd (β := fun (i : ℕ) ↦ α i)
have rw : π sorry b = (Sigma.mk (β := fun (i : ℕ) ↦ α i) i a).snd (β := fun (i : ℕ) ↦ α i)
Tactic: rw [π_trans, ← h2]
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
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)
⊢ π ⋯ ((Sigma.mk (β := fun (i : ℕ) ↦ α i) (i + 1) (π hle b)).snd (β := fun (i : ℕ) ↦ α i)) =
    (Sigma.mk (β := fun (i : ℕ) ↦ α i) i a).snd (β := fun (i : ℕ) ↦ α i)
have rw₁ : π sorry b = (Sigma.mk (β := fun (i : ℕ) ↦ α i) i (π hij b)).snd (β := fun (i : ℕ) ↦ α i)
Tactic: rw [π_trans, ← h2]
-- Lean 4 proof step from Mathlib.Order.KonigLemma (hypothesis)
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)
⊢ ∃ (f : (i : ℕ) → α i), ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i
have this : 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⟩⟩
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
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), a₀.fst (β := fun (i : ℕ) ↦ α i) = 0 ∧ (Ici a₀).Infinite
have obtain : ∀ (a₀ : α 0)
  (ha₀ :
    Infinite.{u_1 + 1} (↑(preimage (β := α 0) (fun (a : αs) ↦ π sorry (a.snd (β := fun (i : ℕ) ↦ α i))) {a₀}) : Type u_1)),
  ∃ (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)
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
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
have refine : preimage (β := α 0) (fun (a : αs) ↦ π sorry (a.snd (β := fun (i : ℕ) ↦ α i))) {a₀} ⊆
  Ici (Sigma.mk (β := fun (i : ℕ) ↦ α i) 0 a₀)
Tactic: refine ⟨⟨0, a₀⟩, rfl, (infinite_coe_iff.1 ha₀).mono ?_⟩
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
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)
⊢ preimage (β := α 0) (fun (a : αs) ↦ π ⋯ (a.snd (β := fun (i : ℕ) ↦ α i))) {a₀} ⊆
    Ici (Sigma.mk (β := fun (i : ℕ) ↦ α i) 0 a₀)
have simp : ∀ (a : ℕ) (b : α a), π sorry b = a₀ → Sigma.mk (β := fun (i : ℕ) ↦ α i) 0 a₀ ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) a b
Tactic: simp only [αs, subset_def, mem_preimage, mem_singleton_iff, mem_Ici, Sigma.forall]
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
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
⊢ ∃ (f : (i : ℕ) → α i), ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i
have 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
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⟩
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
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}
have 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) | π sorry b = a})
Tactic: refine fun ⟨i, a⟩ ↦ ((hfin i a).image (fun b ↦ ⟨_, b⟩)).subset ?_
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
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
⊢ 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})
have 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)),
        π sorry x = a ∧ Sigma.mk (β := fun (i : ℕ) ↦ α i) (i + 1) x = Sigma.mk (β := fun (a : ℕ) ↦ α a) a_1 b
Tactic: simp only [αs, hcovby, subset_def, mem_setOf_eq, mem_image, and_imp, Sigma.forall]
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
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)
⊢ π ⋯ (π ⋯ b) = a
have rwa : π sorry b = a
Tactic: rwa [π_trans]