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)
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)
refl refl₁ : 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) (i + 1) b

Tactic:
rw [π_refl]
-- 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
⊢ ∀ (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

Tactic:
exact fun j b ⟨_, _⟩ hj ↦ ⟨π hj.le b, by rwa [π_trans], by cases hj; rw [π_refl]⟩
-- 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:
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]⟩
-- 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_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}
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
⊢ ∃ (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

Premises used: exists_orderEmbedding_covby_of_forall_covby_finite
-- 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_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
rw₁ rw₂ : 0 = Nat.zero
⊢ Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) Nat.zero) = Nat.zero

Tactic:
rw [hf0, ha₀]
-- 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_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
rw₁ rw₂ : i + 1 = i.succ
⊢ Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i.succ) = i.succ

Tactic:
rw [← (hcovby.1 (hf i)).2, ih]

Premises used: And.right, Iff.mp
-- 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_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 : ℕ), 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])
-- 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_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 : ℕ
rw : α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))
⊢ α i

Tactic:
rw [← hr i]
-- 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_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 : ℕ
⊢ α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))

Tactic:
exact (f i).2

Premises used: Sigma.snd, DFunLike.coe
-- 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_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
refine :
  ∀ (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
⊢ ∃ (f : (i : ℕ) → α i), ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i

Tactic:
refine ⟨fun i ↦ by rw [← hr i]; exact (f i).2, fun i j hij ↦ ?_⟩
-- 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_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
⊢ Eq (α := α (Sigma.fst (β := 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)))
    (Sigma.snd (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))

Tactic:
(f.monotone hij).2

Premises used: OrderEmbedding.monotone
-- 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_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))
h₄ :
  α i = α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)) →
    HEq.{u_1 + 1} (α := α i) ((fun (i : ℕ) ↦ Eq.mpr ⋯ (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))
⊢ π 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

Tactic:
convert! (f.monotone hij).2

Premises used: OrderEmbedding.monotone
-- 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_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
⊢ i = Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)

Tactic:
simp [hr]
-- 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_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
e_1 : α i = α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))
⊢ i = Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i)

Tactic:
simp [hr]
-- 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_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
e_1 : α i = α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))
⊢ j = Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) j)

Tactic:
simp [hr]
-- 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_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
e_1 : α i = α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))
e_2 : 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))

Tactic:
simp [hr]
-- 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_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
e_1 : α i = α (Sigma.fst (β := fun (i : ℕ) ↦ α i) ((f : (a : ℕ) → αs) i))
⊢ HEq.{u_1 + 1} (α := α i) ((fun (i : ℕ) ↦ Eq.mpr ⋯ (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:
simp [hr]
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ height (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) x : αᵒᵈ) = coheight x

Tactic:
rfl

Premises used: rfl, Order.coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : αᵒᵈ
⊢ height (α := α) ((OrderDual.ofDual : (a : αᵒᵈ) → α) x : α) = coheight x

Tactic:
rfl

Premises used: OrderDual, rfl, Order.coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ coheight (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) x : αᵒᵈ) = height x

Tactic:
rfl

Premises used: OrderDual, rfl, Order.coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : αᵒᵈ
⊢ coheight (α := α) ((OrderDual.ofDual : (a : αᵒᵈ) → α) x : α) = height x

Tactic:
rfl

Premises used: rfl, Order.coheight