awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.JordanHolder (hypothesis)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
ht :
  last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
hs₁0 :
  s₁.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    0
this :
  ∀ (x : X),
    x ∈ s₁ ↔
      x =
        last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s₁
⊢ s₁ = s₂
have this₁ : ∀ (x : X),
  x ∈ s₂ ↔
    x =
      last (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        s₂
Tactic: have : ∀ x, x ∈ s₂ ↔ x = s₂.last := fun x =>
    ⟨fun hx =>
      subsingleton_of_length_eq_zero
        (length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero hb ht
          hs₁0) hx s₂.last_mem,
      fun hx => hx.symm ▸ s₂.last_mem⟩
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
ht :
  last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
hs₁0 :
  s₁.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    0
this_1 :
  ∀ (x : X),
    x ∈ s₁ ↔
      x =
        last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s₁
this :
  ∀ (x : X),
    x ∈ s₂ ↔
      x =
        last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s₂
⊢ s₁ = s₂
have h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
ht :
  last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
hle :
  s₁.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    0
⊢ s₁.Equivalent s₂
have zero : s₂.Equivalent s₂
Tactic: rw [eq_of_head_eq_head_of_last_eq_last_of_length_eq_zero hb ht hle]
-- Lean 4 proof step from Mathlib.Order.JordanHolder (hypothesis)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s₁ s₂ : CompositionSeries X)
    (hb :
      head (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s₁ =
        head (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s₂)
    (ht :
      last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s₁ =
        last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s₂)
    (hle :
      s₁.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) =
        n),
    s₁.Equivalent s₂
s₁ s₂ : CompositionSeries X
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
ht :
  last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
hle :
  s₁.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    n + 1
⊢ s₁.Equivalent s₂
have h0s₂ : 0 <
  s₂.length (r :=
    {x : X × X |
      match (motive := X × X → Prop) x with
      | (x, y) => @IsMaximal _ inst _ x y})
Tactic: have h0s₂ : 0 < s₂.length :=
      length_pos_of_head_eq_head_of_last_eq_last_of_length_pos hb ht (hle.symm ▸ Nat.succ_pos _)
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
ht :
  last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
⊢ s₁.Equivalent s₂
have induction : ∀ (x : ℕ)
  (hle :
    s₁.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) =
      x),
  s₁.Equivalent s₂
Tactic: induction hle : s₁.length generalizing s₁ s₂ with
  | zero => rw [eq_of_head_eq_head_of_last_eq_last_of_length_eq_zero hb ht hle]
  | succ n ih =>
    have h0s₂ : 0 < s₂.length :=
      length_pos_of_head_eq_head_of_last_eq_last_of_length_pos hb ht (hle.symm ▸ Nat.succ_pos _)
    rcases exists_last_eq_snoc_equivalent s₁ s₂.eraseLast.last
        (ht.symm ▸ isMaximal_eraseLast_last h0s₂)
        (hb.symm ▸ s₂.head_eraseLast ▸ head_le_of_mem (last_mem _)) with
      ⟨t, htb, htl, htt, hteq⟩
    have := ih t s₂.eraseLast (by simp [htb, ← hb]) htt (Nat.succ_inj.1 (htl.trans hle))
    refine hteq.trans ?_
    conv_rhs => rw [eq_snoc_eraseLast h0s₂]
    simp only [ht]
    exact Equivalent.snoc this (by simpa [htt] using (isMaximal_eraseLast_last h0s₂).iso_refl)
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : IsStronglyAtomic α
b : α
hfin : ∀ (a : α), Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
hb : (Ici b).Infinite
⊢ ∃ (f : ℕ ↪o α),
    (f : (a : ℕ) → α) 0 = b ∧ ∀ (i : ℕ), CovBy (α := α) ((f : (a : ℕ) → α) i : α) ((f : (a : ℕ) → α) (i + 1) : α)
have obtain : ∀ (f : ℕ → α) (hf : f 0 = b ∧ ∀ (i : ℕ), f i ⋖ f (i + 1)),
  ∃ (f : ℕ ↪o α),
    (f : (a : ℕ) → α) 0 = b ∧ ∀ (i : ℕ), CovBy (α := α) ((f : (a : ℕ) → α) i : α) ((f : (a : ℕ) → α) (i + 1) : α)
Tactic: obtain ⟨f, hf⟩ := exists_seq_covby_of_forall_covby_finite hfin hb
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : IsStronglyAtomic α
inst_2 : GradeMinOrder ℕ α
inst_3 : OrderBot α
inst_4 : Infinite α
hfin : ∀ (a : α), Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
⊢ ∃ (f : ℕ ↪o α),
    Eq (α := α) ((f : (a : ℕ) → α) 0 : α) (⊥ : α) ∧
      (∀ (i : ℕ), CovBy (α := α) ((f : (a : ℕ) → α) i : α) ((f : (a : ℕ) → α) (i + 1) : α)) ∧
        ∀ (i : ℕ), grade ℕ (α := α) ((f : (a : ℕ) → α) i : α) = i
have obtain : ∀ (f : ℕ ↪o α) (h0 : Eq (α := α) ((f : (a : ℕ) → α) 0 : α) (⊥ : α))
  (hf : ∀ (i : ℕ), CovBy (α := α) ((f : (a : ℕ) → α) i : α) ((f : (a : ℕ) → α) (i + 1) : α)),
  ∃ (f : ℕ ↪o α),
    Eq (α := α) ((f : (a : ℕ) → α) 0 : α) (⊥ : α) ∧
      (∀ (i : ℕ), CovBy (α := α) ((f : (a : ℕ) → α) i : α) ((f : (a : ℕ) → α) (i + 1) : α)) ∧
        ∀ (i : ℕ), grade ℕ (α := α) ((f : (a : ℕ) → α) i : α) = i
Tactic: obtain ⟨f, h0, hf⟩ := exists_orderEmbedding_covby_of_forall_covby_finite_of_bot hfin
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : IsStronglyAtomic α
inst_2 : GradeMinOrder ℕ α
inst_3 : OrderBot α
inst_4 : Infinite α
hfin : ∀ (a : α), Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
f : ℕ ↪o α
h0 : Eq (α := α) ((f : (a : ℕ) → α) 0 : α) (⊥ : α)
hf : ∀ (i : ℕ), CovBy (α := α) ((f : (a : ℕ) → α) i : α) ((f : (a : ℕ) → α) (i + 1) : α)
⊢ ∃ (f : ℕ ↪o α),
    Eq (α := α) ((f : (a : ℕ) → α) 0 : α) (⊥ : α) ∧
      (∀ (i : ℕ), CovBy (α := α) ((f : (a : ℕ) → α) i : α) ((f : (a : ℕ) → α) (i + 1) : α)) ∧
        ∀ (i : ℕ), grade ℕ (α := α) ((f : (a : ℕ) → α) i : α) = i
have refine : ∀ (i : ℕ), grade ℕ (α := α) ((f : (a : ℕ) → α) i : α) = i
Tactic: refine ⟨f, h0, hf, fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : IsStronglyAtomic α
inst_2 : GradeMinOrder ℕ α
inst_3 : OrderBot α
inst_4 : Infinite α
hfin : ∀ (a : α), Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
f : ℕ ↪o α
h0 : Eq (α := α) ((f : (a : ℕ) → α) 0 : α) (⊥ : α)
hf : ∀ (i : ℕ), CovBy (α := α) ((f : (a : ℕ) → α) i : α) ((f : (a : ℕ) → α) (i + 1) : α)
i : ℕ
⊢ grade ℕ (α := α) ((f : (a : ℕ) → α) i : α) = i
have zero : grade ℕ (α := α) ((f : (a : ℕ) → α) 0 : α) = 0
Tactic: induction i with
  | zero => simp [h0]
  | succ i ih => simpa [Order.covBy_iff_add_one_eq, ih, eq_comm] using CovBy.grade ℕ <| hf i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Order.KonigLemma (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : IsStronglyAtomic α
inst_2 : GradeMinOrder ℕ α
inst_3 : OrderBot α
inst_4 : Infinite α
hfin : ∀ (a : α), Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
f : ℕ ↪o α
h0 : Eq (α := α) ((f : (a : ℕ) → α) 0 : α) (⊥ : α)
hf : ∀ (i : ℕ), CovBy (α := α) ((f : (a : ℕ) → α) i : α) ((f : (a : ℕ) → α) (i + 1) : α)
i : ℕ
zero : grade ℕ (α := α) ((f : (a : ℕ) → α) 0 : α) = 0
⊢ grade ℕ (α := α) ((f : (a : ℕ) → α) i : α) = i
have succ : ∀ (i : ℕ) (ih : grade ℕ (α := α) ((f : (a : ℕ) → α) i : α) = i),
  grade ℕ (α := α) ((f : (a : ℕ) → α) (i + 1) : α) = i + 1
Tactic: induction i with
  | zero => simp [h0]
  | succ i ih => simpa [Order.covBy_iff_add_one_eq, ih, eq_comm] using CovBy.grade ℕ <| hf i
Cleared hypotheses: 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 : ∀ (i : ℕ) (a : α i), Set.Finite.{u_1} (α := α (i + 1)) {b : α (i + 1) | π ⋯ b = a}
αs : Type u_1 := (i : ℕ) × α i
x x_1 c : αs
h :
  ∃ (h : x.fst (β := fun (i : ℕ) ↦ α i) ≤ x_1.fst (β := fun (i : ℕ) ↦ α i)),
    π h (x_1.snd (β := fun (i : ℕ) ↦ α i)) = x.snd (β := fun (i : ℕ) ↦ α i)
h' :
  ∃ (h : x_1.fst (β := fun (i : ℕ) ↦ α i) ≤ c.fst (β := fun (i : ℕ) ↦ α i)),
    π h (c.snd (β := fun (i : ℕ) ↦ α i)) = x_1.snd (β := fun (i : ℕ) ↦ α i)
⊢ π ⋯ (c.snd (β := fun (i : ℕ) ↦ α i)) = x.snd (β := fun (i : ℕ) ↦ α i)
have rw : π (j := x_1.fst (β := fun (i : ℕ) ↦ α i)) sorry (π sorry (c.snd (β := fun (i : ℕ) ↦ α i))) = x.snd (β := fun (i : ℕ) ↦ α i)
Tactic: rw [← π_trans h.1 h'.1 c.2, h'.2, h.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 x_1 c : αs
h :
  ∃ (h : x.fst (β := fun (i : ℕ) ↦ α i) ≤ x_1.fst (β := fun (i : ℕ) ↦ α i)),
    π h (x_1.snd (β := fun (i : ℕ) ↦ α i)) = x.snd (β := fun (i : ℕ) ↦ α i)
h' :
  ∃ (h : x_1.fst (β := fun (i : ℕ) ↦ α i) ≤ c.fst (β := fun (i : ℕ) ↦ α i)),
    π h (c.snd (β := fun (i : ℕ) ↦ α i)) = x_1.snd (β := fun (i : ℕ) ↦ α i)
rw : π (j := x_1.fst (β := fun (i : ℕ) ↦ α i)) ⋯ (π ⋯ (c.snd (β := fun (i : ℕ) ↦ α i))) = x.snd (β := fun (i : ℕ) ↦ α i)
⊢ π ⋯ (c.snd (β := fun (i : ℕ) ↦ α i)) = x.snd (β := fun (i : ℕ) ↦ α i)
have rw₁ : π sorry (x_1.snd (β := fun (i : ℕ) ↦ α i)) = x.snd (β := fun (i : ℕ) ↦ α i)
Tactic: rw [← π_trans h.1 h'.1 c.2, h'.2, h.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 x_1 c : αs
h :
  ∃ (h : x.fst (β := fun (i : ℕ) ↦ α i) ≤ x_1.fst (β := fun (i : ℕ) ↦ α i)),
    π h (x_1.snd (β := fun (i : ℕ) ↦ α i)) = x.snd (β := fun (i : ℕ) ↦ α i)
h' :
  ∃ (h : x_1.fst (β := fun (i : ℕ) ↦ α i) ≤ c.fst (β := fun (i : ℕ) ↦ α i)),
    π h (c.snd (β := fun (i : ℕ) ↦ α i)) = x_1.snd (β := fun (i : ℕ) ↦ α i)
rw : π (j := x_1.fst (β := fun (i : ℕ) ↦ α i)) ⋯ (π ⋯ (c.snd (β := fun (i : ℕ) ↦ α i))) = x.snd (β := fun (i : ℕ) ↦ α i)
rw₁ : π ⋯ (x_1.snd (β := fun (i : ℕ) ↦ α i)) = x.snd (β := fun (i : ℕ) ↦ α i)
⊢ π ⋯ (c.snd (β := fun (i : ℕ) ↦ α i)) = x.snd (β := fun (i : ℕ) ↦ α i)
have rw₂ : x.snd (β := fun (i : ℕ) ↦ α i) = x.snd (β := fun (i : ℕ) ↦ α i)
Tactic: rw [← π_trans h.1 h'.1 c.2, h'.2, h.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 := ⋯ }
⊢ ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)
have simp : ∀ (a : ℕ) (b : α a) (a_1 : ℕ) (b_1 : α a_1),
  Sigma.mk (β := fun (a : ℕ) ↦ α a) a b ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) a_1 b_1 →
    ((¬Sigma.mk (β := fun (a : ℕ) ↦ α a) a b = Sigma.mk (β := fun (a : ℕ) ↦ α a) a_1 b_1 ∧
        ∀ (a_3 : ℕ) (b_2 : α a_3),
          Sigma.mk (β := fun (a : ℕ) ↦ α a) a b ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) a_3 b_2 →
            Sigma.mk (β := fun (a : ℕ) ↦ α a) a_3 b_2 ≤ Sigma.mk (β := fun (a : ℕ) ↦ α a) a_1 b_1 →
              ¬Sigma.mk (β := fun (a : ℕ) ↦ α a) a_3 b_2 = Sigma.mk (β := fun (a : ℕ) ↦ α a) a b →
                Sigma.mk (β := fun (a : ℕ) ↦ α a) a_3 b_2 = Sigma.mk (β := fun (a : ℕ) ↦ α a) a_1 b_1) ↔
      a + 1 = a_1)
Tactic: 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]
-- 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
⊢ (¬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
have 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
Tactic: refine ⟨fun ⟨hne, 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 := ⋯ }
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
⊢ (¬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
have 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
Tactic: refine ⟨fun ⟨hne, 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 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
have hle' : i + 1 ≤ j
Tactic: have hle' : i + 1 ≤ j := h.lt_of_ne <| by rintro rfl; simp [π_refl] at hne