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 := ⋯ }
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)
⊢ Sigma.mk (β := fun (i : ℕ) ↦ α i) (i + 1) (π ⋯ b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) j b
have 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) (π sorry b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b
Tactic: cases hj
Cleared hypotheses: j, b, h, hj, w, h_1
-- 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
b : α (i + 1)
h : 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)
h_1 :
  π 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
have refl : Sigma.mk (β := fun (i : ℕ) ↦ α i) (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 := ⋯ }
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
⊢ ∃ (f : (i : ℕ) → α i), ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i
have hfin₁ : ∀ (a : αs), Set.Finite.{u_1} (α := αs) {x_1 : αs | a ⋖ x_1}
Tactic: have hfin : ∀ (a : αs), {x | a ⋖ x}.Finite := by
    refine fun ⟨i, a⟩ ↦ ((hfin i a).image (fun b ↦ ⟨_, b⟩)).subset ?_
    simp only [αs, hcovby, subset_def, mem_setOf_eq, mem_image, and_imp, Sigma.forall]
    exact fun j b ⟨_, _⟩ hj ↦ ⟨π hj.le b, by rwa [π_trans], by cases hj; 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_1 : ∀ (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
hfin : ∀ (a : αs), Set.Finite.{u_1} (α := αs) {x_1 : αs | a ⋖ x_1}
⊢ ∃ (f : (i : ℕ) → α i), ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i
have obtain : ∀ (f : ℕ ↪o αs) (hf0 : (f : (a : ℕ) → αs) 0 = a₀)
  (hf : ∀ (i : ℕ), CovBy (α := αs) ((f : (a : ℕ) → αs) i : αs) ((f : (a : ℕ) → αs) (i + 1) : αs)),
  ∃ (f : (i : ℕ) → α i), ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i
Tactic: obtain ⟨f, hf0, hf⟩ := exists_orderEmbedding_covby_of_forall_covby_finite hfin ha₀inf
-- 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_1 : ∀ (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
hfin : ∀ (a : αs), Set.Finite.{u_1} (α := αs) {x_1 : αs | a ⋖ x_1}
f : ℕ ↪o αs
hf0 : (f : (a : ℕ) → αs) 0 = a₀
hf : ∀ (i : ℕ), CovBy (α := αs) ((f : (a : ℕ) → αs) i : αs) ((f : (a : ℕ) → αs) (i + 1) : αs)
rw : a₀.fst (β := fun (i : ℕ) ↦ α i) = Nat.zero
⊢ Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) Nat.zero) = Nat.zero
have rw₁ : 0 = Nat.zero
Tactic: rw [hf0, ha₀]
-- 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_1 : ∀ (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
hfin : ∀ (a : αs), Set.Finite.{u_1} (α := αs) {x_1 : αs | a ⋖ x_1}
f : ℕ ↪o αs
hf0 : (f : (a : ℕ) → αs) 0 = a₀
hf : ∀ (i : ℕ), CovBy (α := αs) ((f : (a : ℕ) → αs) i : αs) ((f : (a : ℕ) → αs) (i + 1) : αs)
i : ℕ
ih : Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i) = i
⊢ Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i.succ) = i.succ
have rw : HAdd.hAdd (α := ℕ) (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)) 1 = i.succ
Tactic: rw [← (hcovby.1 (hf i)).2, ih]
-- 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_1 : ∀ (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
hfin : ∀ (a : αs), Set.Finite.{u_1} (α := αs) {x_1 : αs | a ⋖ x_1}
f : ℕ ↪o αs
hf0 : (f : (a : ℕ) → αs) 0 = a₀
hf : ∀ (i : ℕ), CovBy (α := αs) ((f : (a : ℕ) → αs) i : αs) ((f : (a : ℕ) → αs) (i + 1) : αs)
i : ℕ
ih : Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i) = i
rw : HAdd.hAdd (α := ℕ) (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)) 1 = i.succ
⊢ Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i.succ) = i.succ
have rw₁ : i + 1 = i.succ
Tactic: rw [← (hcovby.1 (hf i)).2, ih]
-- 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_1 : ∀ (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
hfin : ∀ (a : αs), Set.Finite.{u_1} (α := αs) {x_1 : αs | a ⋖ x_1}
f : ℕ ↪o αs
hf0 : (f : (a : ℕ) → αs) 0 = a₀
hf : ∀ (i : ℕ), CovBy (α := αs) ((f : (a : ℕ) → αs) i : αs) ((f : (a : ℕ) → αs) (i + 1) : αs)
⊢ ∃ (f : (i : ℕ) → α i), ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i
have hr : ∀ (i : ℕ), Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i) = i
Tactic: have hr : ∀ i, (f i).1 = i :=
    Nat.rec (by rw [hf0, ha₀]) (fun i ih ↦ by rw [← (hcovby.1 (hf i)).2, ih])
-- 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_1 : ∀ (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
hfin : ∀ (a : αs), Set.Finite.{u_1} (α := αs) {x_1 : αs | a ⋖ x_1}
f : ℕ ↪o αs
hf0 : (f : (a : ℕ) → αs) 0 = a₀
hf : ∀ (i : ℕ), CovBy (α := αs) ((f : (a : ℕ) → αs) i : αs) ((f : (a : ℕ) → αs) (i + 1) : αs)
hr : ∀ (i : ℕ), Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i) = i
i : ℕ
⊢ α i
have rw : α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))
Tactic: rw [← hr i]
-- 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_1 : ∀ (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
hfin : ∀ (a : αs), Set.Finite.{u_1} (α := αs) {x_1 : αs | a ⋖ x_1}
f : ℕ ↪o αs
hf0 : (f : (a : ℕ) → αs) 0 = a₀
hf : ∀ (i : ℕ), CovBy (α := αs) ((f : (a : ℕ) → αs) i : αs) ((f : (a : ℕ) → αs) (i + 1) : αs)
hr : ∀ (i : ℕ), Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i) = i
⊢ ∃ (f : (i : ℕ) → α i), ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i
have refine : ∀ (i j : ℕ) (hij : i ≤ j),
  π hij ((fun (i : ℕ) ↦ Eq.mpr sorry (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))) j) =
    (fun (i : ℕ) ↦ Eq.mpr sorry (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))) i
Tactic: refine ⟨fun i ↦ by rw [← hr i]; exact (f i).2, fun i j hij ↦ ?_⟩
-- 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_1 : ∀ (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
hfin : ∀ (a : αs), Set.Finite.{u_1} (α := αs) {x_1 : αs | a ⋖ x_1}
f : ℕ ↪o αs
hf0 : (f : (a : ℕ) → αs) 0 = a₀
hf : ∀ (i : ℕ), CovBy (α := αs) ((f : (a : ℕ) → αs) i : αs) ((f : (a : ℕ) → αs) (i + 1) : αs)
hr : ∀ (i : ℕ), Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i) = i
i j : ℕ
hij : i ≤ j
⊢ π hij ((fun (i : ℕ) ↦ Eq.mpr ⋯ (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))) j) =
    (fun (i : ℕ) ↦ Eq.mpr ⋯ (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))) i
have h : i = Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)
Tactic: convert! (f.monotone hij).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_1 : ∀ (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
hfin : ∀ (a : αs), Set.Finite.{u_1} (α := αs) {x_1 : αs | a ⋖ x_1}
f : ℕ ↪o αs
hf0 : (f : (a : ℕ) → αs) 0 = a₀
hf : ∀ (i : ℕ), CovBy (α := αs) ((f : (a : ℕ) → αs) i : αs) ((f : (a : ℕ) → αs) (i + 1) : αs)
hr : ∀ (i : ℕ), Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i) = i
i j : ℕ
hij : i ≤ j
h : i = Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)
⊢ π hij ((fun (i : ℕ) ↦ Eq.mpr ⋯ (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))) j) =
    (fun (i : ℕ) ↦ Eq.mpr ⋯ (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))) i
have h₁ : α i = α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)) →
  i = Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)
Tactic: convert! (f.monotone hij).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_1 : ∀ (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
hfin : ∀ (a : αs), Set.Finite.{u_1} (α := αs) {x_1 : αs | a ⋖ x_1}
f : ℕ ↪o αs
hf0 : (f : (a : ℕ) → αs) 0 = a₀
hf : ∀ (i : ℕ), CovBy (α := αs) ((f : (a : ℕ) → αs) i : αs) ((f : (a : ℕ) → αs) (i + 1) : αs)
hr : ∀ (i : ℕ), Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i) = i
i j : ℕ
hij : i ≤ j
h : i = Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)
h₁ :
  α i = α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)) →
    i = Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)
⊢ π hij ((fun (i : ℕ) ↦ Eq.mpr ⋯ (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))) j) =
    (fun (i : ℕ) ↦ Eq.mpr ⋯ (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))) i
have h₂ : α i = α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)) →
  j = Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) j)
Tactic: convert! (f.monotone hij).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_1 : ∀ (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
hfin : ∀ (a : αs), Set.Finite.{u_1} (α := αs) {x_1 : αs | a ⋖ x_1}
f : ℕ ↪o αs
hf0 : (f : (a : ℕ) → αs) 0 = a₀
hf : ∀ (i : ℕ), CovBy (α := αs) ((f : (a : ℕ) → αs) i : αs) ((f : (a : ℕ) → αs) (i + 1) : αs)
hr : ∀ (i : ℕ), Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i) = i
i j : ℕ
hij : i ≤ j
h : i = Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)
h₁ :
  α i = α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)) →
    i = Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)
h₂ :
  α i = α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)) →
    j = Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) j)
⊢ π hij ((fun (i : ℕ) ↦ Eq.mpr ⋯ (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))) j) =
    (fun (i : ℕ) ↦ Eq.mpr ⋯ (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))) i
have h₃ : α i = α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)) →
  j = Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) j) →
    HEq.{u_1 + 1} (α := α j) ((fun (i : ℕ) ↦ Eq.mpr sorry (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))) j)
      (β := α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) j)))
      (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) j))
Tactic: convert! (f.monotone hij).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_1 : ∀ (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
hfin : ∀ (a : αs), Set.Finite.{u_1} (α := αs) {x_1 : αs | a ⋖ x_1}
f : ℕ ↪o αs
hf0 : (f : (a : ℕ) → αs) 0 = a₀
hf : ∀ (i : ℕ), CovBy (α := αs) ((f : (a : ℕ) → αs) i : αs) ((f : (a : ℕ) → αs) (i + 1) : αs)
hr : ∀ (i : ℕ), Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i) = i
i j : ℕ
hij : i ≤ j
h : i = Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)
h₁ :
  α i = α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)) →
    i = Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)
h₂ :
  α i = α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)) →
    j = Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) j)
h₃ :
  α i = α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)) →
    j = Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) j) →
      HEq.{u_1 + 1} (α := α j) ((fun (i : ℕ) ↦ Eq.mpr ⋯ (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))) j)
        (β := α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) j)))
        (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) j))
⊢ π hij ((fun (i : ℕ) ↦ Eq.mpr ⋯ (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))) j) =
    (fun (i : ℕ) ↦ Eq.mpr ⋯ (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))) i
have h₄ : α i = α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)) →
  HEq.{u_1 + 1} (α := α i) ((fun (i : ℕ) ↦ Eq.mpr sorry (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))) i)
    (β := α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)))
    (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))
Tactic: convert! (f.monotone hij).2
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
⊢ height a ≤ n ↔
    ∀ ⦃p : LTSeries α⦄,
      RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          a →
        (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
          n
have rw : ⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          a),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
    n ↔
  ∀ ⦃p : LTSeries α⦄,
    RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p ≤
        a →
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n
Tactic: rw [height, iSup₂_le_iff]