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 := ⋯ }
i j : ℕ
b : α j
h : i ≤ j
⊢ (¬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) ↔
    i + 1 = j

Tactic:
⟨fun ⟨hne, h'⟩ ↦ ?_, ?_⟩

Premises used: HAdd.hAdd, Iff.intro, OfNat.ofNat, Eq, _private.0.exists_seq_forall_proj_of_forall_finite.match_9
-- 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 := ⋯ }
i j : ℕ
b : α j
h : i ≤ j
refine_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),
      i + 1 = j
refine_2 :
  i + 1 = j →
    ¬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
⊢ (¬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) ↔
    i + 1 = j

Tactic:
refine ⟨fun ⟨hne, 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 := ⋯ }
i : ℕ
b : α i
h : i ≤ i
h_1 :
  ¬Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) i 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 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 b
hne : ¬Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) i 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) i 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 b
⊢ False

Tactic:
simp [π_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 := ⋯ }
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
⊢ i + 1 ≤ j

Tactic:
have hle' : i + 1 ≤ j := h.lt_of_ne <| by rintro rfl; simp [π_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 := ⋯ }
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 (π h b)).fst (β := fun (i : ℕ) ↦ α i) ≤
    (Sigma.mk (β := fun (a : ℕ) ↦ α a) (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 := ⋯ }
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
rw rw₁ : π ⋯ b = (Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b)).snd (β := fun (i : ℕ) ↦ α i)
⊢ π ⋯ ((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)

Tactic:
rw [π_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 := ⋯ }
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
⊢ π hle' ((Sigma.mk (β := fun (a : ℕ) ↦ α a) j b).snd (β := fun (i : ℕ) ↦ α i)) =
    (Sigma.mk (β := fun (a : ℕ) ↦ α a) (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 := ⋯ }
i j : ℕ
b : α j
h_1 : i ≤ j
h_2 :
  ¬Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h_1 b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) j b ∧
    ∀ (a : ℕ) (b_1 : α a),
      Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h_1 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_1 b) →
            Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 = Sigma.mk (β := fun (a : ℕ) ↦ α a) j b
hne : ¬Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h_1 b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) j b
h' :
  ∀ (a : ℕ) (b_1 : α a),
    Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h_1 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_1 b) →
          Sigma.mk (β := fun (a : ℕ) ↦ α a) a b_1 = Sigma.mk (β := fun (a : ℕ) ↦ α a) j b
hle' : i + 1 ≤ j
h : Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) (π hle' b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h_1 b)
⊢ False

Tactic:
simp at 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 := ⋯ }
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
⊢ i + 1 = j

Tactic:
exact congr_arg Sigma.fst <| h' (i + 1) (π hle' b) ⟨by simp, by rw [π_trans]⟩ ⟨hle', by simp⟩
        (fun h ↦ by simp at h)

Premises used: Sigma.fst, congr_arg, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- 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 := ⋯ }
i : ℕ
b : α (i + 1)
h_1 : i ≤ i + 1
h : Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h_1 b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b
⊢ False

Tactic:
simp at 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 := ⋯ }
i : ℕ
b : α (i + 1)
h : i ≤ i + 1
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
⊢ ¬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

Tactic:
refine ⟨fun h ↦ by simp at 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 := ⋯ }
i : ℕ
b : α (i + 1)
h : i ≤ i + 1
hij : i ≤ i
hji : i ≤ i + 1
hcb : π hij (π hji b) = π h b
hne : ¬Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π hji b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) i (π h b)
⊢ False

Tactic:
contradiction
-- 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 := ⋯ }
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)
⊢ i ≠ j

Tactic:
replace hne := show i ≠ j by rintro rfl; contradiction
-- 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 := ⋯ }
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
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
⊢ Sigma.mk (β := fun (a : ℕ) ↦ α a) j (π hji b) = Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b

Tactic:
obtain rfl := hji.antisymm (hij.lt_of_ne hne)

Premises used: LE.le.antisymm, LE.le.lt_of_ne, 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 := ⋯ }
i : ℕ
b : α (i + 1)
h hij : i ≤ i + 1
hji : i + 1 ≤ i + 1
hcb : π hij (π hji b) = π h b
hne : i ≠ i + 1
refine_2 refine_2₁ : Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b = Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) b
⊢ Sigma.mk (β := fun (a : ℕ) ↦ α a) (i + 1) (π hji 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 := ⋯ }
⊢ ∀ {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]