awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.JordanHolder
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₂
x : X
⊢ x ∈ s₁ ↔ x ∈ s₂

Tactic:
simp [*]
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
x : X
hm :
  @IsMaximal _ inst _ x
    (last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s)
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s ≤
    x
hn :
  s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    0
⊢ ∃ (t : CompositionSeries X),
    head (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          t =
        head (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s ∧
      t.length (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y}) +
            1 =
          0 ∧
        ∃ (htx :
          last (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y})
              t =
            x),
          s.Equivalent
            (snoc (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y})
              t
              (last (r :=
                {x : X × X |
                  match (motive := X × X → Prop) x with
                  | (x, y) => @IsMaximal _ inst _ x y})
                s)
              ⋯)

Tactic:
(ne_of_gt (lt_of_le_of_lt hb (lt_of_isMaximal hm))
      (subsingleton_of_length_eq_zero hn s.last_mem s.head_mem)).elim

Premises used: lt_of_le_of_lt, RelSeries.last_mem, False.elim, ne_of_gt, JordanHolderLattice.lt_of_isMaximal, RelSeries.head_mem, RelSeries.subsingleton_of_length_eq_zero
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
x : X
hm :
  @IsMaximal _ inst _ x
    (last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s)
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s ≤
    x
hn :
  s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    0
⊢ ∃ (t : CompositionSeries X),
    head (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          t =
        head (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s ∧
      t.length (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y}) +
            1 =
          0 ∧
        ∃ (htx :
          last (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y})
              t =
            x),
          s.Equivalent
            (snoc (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y})
              t
              (last (r :=
                {x : X × X |
                  match (motive := X × X → Prop) x with
                  | (x, y) => @IsMaximal _ inst _ x y})
                s)
              ⋯)

Tactic:
exact (ne_of_gt (lt_of_le_of_lt hb (lt_of_isMaximal hm))
      (subsingleton_of_length_eq_zero hn s.last_mem s.head_mem)).elim

Premises used: lt_of_le_of_lt, RelSeries.last_mem, False.elim, ne_of_gt, JordanHolderLattice.lt_of_isMaximal, RelSeries.head_mem, RelSeries.subsingleton_of_length_eq_zero
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X)
    (hm :
      @IsMaximal _ inst _ x
        (last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s))
    (hb :
      head (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s ≤
        x)
    (hn :
      s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) =
        n),
    ∃ (t : CompositionSeries X),
      head (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            t =
          head (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s ∧
        t.length (r :=
                {x : X × X |
                  match (motive := X × X → Prop) x with
                  | (x, y) => @IsMaximal _ inst _ x y}) +
              1 =
            n ∧
          ∃ (htx :
            last (r :=
                {x : X × X |
                  match (motive := X × X → Prop) x with
                  | (x, y) => @IsMaximal _ inst _ x y})
                t =
              x),
            s.Equivalent
              (snoc (r :=
                {x : X × X |
                  match (motive := X × X → Prop) x with
                  | (x, y) => @IsMaximal _ inst _ x y})
                t
                (last (r :=
                  {x : X × X |
                    match (motive := X × X → Prop) x with
                    | (x, y) => @IsMaximal _ inst _ x y})
                  s)
                ⋯)
s : CompositionSeries X
x : X
hm :
  @IsMaximal _ inst _ x
    (last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s)
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s ≤
    x
hn :
  s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    n + 1
⊢ 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 := hn.symm ▸ Nat.succ_pos _
-- Module: Mathlib.Order.JordanHolder
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
zero zero₁ : s₂.Equivalent s₂
⊢ s₁.Equivalent s₂

Tactic:
rw [eq_of_head_eq_head_of_last_eq_last_of_length_eq_zero hb ht hle]

Premises used: CompositionSeries.eq_of_head_eq_head_of_last_eq_last_of_length_eq_zero
-- Module: Mathlib.Order.JordanHolder
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
⊢ 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 _)
-- Module: Mathlib.Order.JordanHolder
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₂
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₂
⊢ 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)

Premises used: RelSeries.length
-- Module: Mathlib.Order.KonigLemma
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : IsStronglyAtomic α
b : α
hfin : ∀ (a : α), Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
hb : (Ici b).Infinite
h : ∀ (a : { a : α // (Ici a).Infinite }), ∃ (b : α), (↑a : α) ⋖ b ∧ (Ici b).Infinite := ⋯
ks : ℕ → { a : α // (Ici a).Infinite } :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ { a : α // (Ici a).Infinite })
      (Subtype.mk (p := fun (a : α) ↦ (Ici a).Infinite) b hb)
      (fun (x : ℕ) (a : { a : α // (Ici a).Infinite }) ↦
        Subtype.mk (p := fun (a : α) ↦ (Ici a).Infinite) (⋯.choose (p := fun (b : α) ↦ (↑a : α) ⋖ b ∧ (Ici b).Infinite))
          ⋯)
      t
⊢ (fun (i : ℕ) ↦ (↑(ks i) : α)) 0 = b

Tactic:
simp [ks]
-- Module: Mathlib.Order.KonigLemma
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : IsStronglyAtomic α
b : α
hfin : ∀ (a : α), Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
hb : (Ici b).Infinite
h : ∀ (a : { a : α // (Ici a).Infinite }), ∃ (b : α), (↑a : α) ⋖ b ∧ (Ici b).Infinite := ⋯
ks : ℕ → { a : α // (Ici a).Infinite } :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ { a : α // (Ici a).Infinite })
      (Subtype.mk (p := fun (a : α) ↦ (Ici a).Infinite) b hb)
      (fun (x : ℕ) (a : { a : α // (Ici a).Infinite }) ↦
        Subtype.mk (p := fun (a : α) ↦ (Ici a).Infinite) (⋯.choose (p := fun (b : α) ↦ (↑a : α) ⋖ b ∧ (Ici b).Infinite))
          ⋯)
      t
i : ℕ
⊢ CovBy.{u_1} (α := α) ((fun (i : ℕ) ↦ (↑(ks i) : α)) i) ((fun (i : ℕ) ↦ (↑(ks i) : α)) (i + 1))

Tactic:
simpa using (h (ks i)).choose_spec.1

Premises used: Exists.choose_spec, And.left
-- Module: Mathlib.Order.KonigLemma
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : IsStronglyAtomic α
b : α
hfin : ∀ (a : α), Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
hb : (Ici b).Infinite
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) : α)
⊢ ∃ (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

Premises used: exists_seq_covby_of_forall_covby_finite
-- Module: Mathlib.Order.KonigLemma
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : IsStronglyAtomic α
b : α
hfin : ∀ (a : α), Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
hb : (Ici b).Infinite
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:
⟨OrderEmbedding.ofStrictMono f (strictMono_nat_of_lt_succ (fun i ↦ (hf.2 i).lt)), hf⟩

Premises used: strictMono_nat_of_lt_succ, And.right, OrderEmbedding.ofStrictMono, Exists.intro, CovBy.lt
-- Module: Mathlib.Order.KonigLemma
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : IsStronglyAtomic α
b : α
hfin : ∀ (a : α), Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
hb : (Ici b).Infinite
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:
exact ⟨OrderEmbedding.ofStrictMono f (strictMono_nat_of_lt_succ (fun i ↦ (hf.2 i).lt)), hf⟩
-- Module: Mathlib.Order.KonigLemma
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : IsStronglyAtomic α
inst_2 : OrderBot α
inst_3 : Infinite α
hfin : ∀ (a : α), Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
⊢ Set.Infinite.{u_1} (α := α) (Ici ⊥)

Tactic:
simpa using infinite_univ

Premises used: Set.infinite_univ
-- Module: Mathlib.Order.KonigLemma
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}
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
⊢ ∃ (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

Premises used: exists_orderEmbedding_covby_of_forall_covby_finite_of_bot
-- Module: Mathlib.Order.KonigLemma
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

Tactic:
⟨f, h0, hf, fun i ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.KonigLemma
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) : α)
refine : ∀ (i : ℕ), grade ℕ (α := α) ((f : (a : ℕ) → α) i : α) = i
⊢ ∃ (f : ℕ ↪o α),
    Eq (α := α) ((f : (a : ℕ) → α) 0 : α) (⊥ : α) ∧
      (∀ (i : ℕ), CovBy (α := α) ((f : (a : ℕ) → α) i : α) ((f : (a : ℕ) → α) (i + 1) : α)) ∧
        ∀ (i : ℕ), grade ℕ (α := α) ((f : (a : ℕ) → α) i : α) = i

Tactic:
refine ⟨f, h0, hf, fun i ↦ ?_⟩
-- Module: Mathlib.Order.KonigLemma
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) : α)
⊢ grade ℕ (α := α) ((f : (a : ℕ) → α) 0 : α) = 0

Tactic:
simp [h0]
-- Module: Mathlib.Order.KonigLemma
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 : ℕ
ih : grade ℕ (α := α) ((f : (a : ℕ) → α) i : α) = i
⊢ grade ℕ (α := α) ((f : (a : ℕ) → α) (i + 1) : α) = i + 1

Tactic:
simpa [Order.covBy_iff_add_one_eq, ih, eq_comm] using CovBy.grade ℕ <| hf i

Premises used: Order.covBy_iff_add_one_eq, eq_comm, Nat, CovBy.grade
-- Module: Mathlib.Order.KonigLemma
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
succ :
  ∀ (i : ℕ) (ih : grade ℕ (α := α) ((f : (a : ℕ) → α) i : α) = i),
    grade ℕ (α := α) ((f : (a : ℕ) → α) (i + 1) : α) = i + 1
⊢ grade ℕ (α := α) ((f : (a : ℕ) → α) i : α) = i

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

Premises used: Order.covBy_iff_add_one_eq, eq_comm, Nat, CovBy.grade
-- 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 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)
rw₂ rw₃ : x.snd (β := fun (i : ℕ) ↦ α i) = x.snd (β := fun (i : ℕ) ↦ α i)
⊢ π ⋯ (c.snd (β := fun (i : ℕ) ↦ α i)) = x.snd (β := fun (i : ℕ) ↦ α i)

Tactic:
rw [← π_trans h.1 h'.1 c.2, h'.2, h.2]

Premises used: Sigma.snd
-- 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
⊢ ∀ (a b : αs),
    (∃ (h : a.fst (β := fun (i : ℕ) ↦ α i) ≤ b.fst (β := fun (i : ℕ) ↦ α i)),
        π h (b.snd (β := fun (i : ℕ) ↦ α i)) = a.snd (β := fun (i : ℕ) ↦ α i)) →
      (∃ (h : b.fst (β := fun (i : ℕ) ↦ α i) ≤ a.fst (β := fun (i : ℕ) ↦ α i)),
          π h (a.snd (β := fun (i : ℕ) ↦ α i)) = b.snd (β := fun (i : ℕ) ↦ α i)) →
        a = b

Tactic:
grind
-- 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 := ⋯ }
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)
⊢ ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst (β := fun (i : ℕ) ↦ α i) + 1 = b.fst (β := fun (i : ℕ) ↦ α i)

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]

Premises used: lt_iff_le_and_ne, Sigma.forall, and_congr_right_iff, ne_eq, covBy_iff_lt_and_eq_or_eq, Classical.or_iff_not_imp_left, and_assoc