awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
i j : Ordinal.{u}
h_1 : i < type r'
h : j < type r'
h_2 : i < j
⊢ r
    ((hrr'.toEmbedding (r := r') (s := r) : (a : { i : ι // ∀ (j : ι), r j i → f j < f i }) → ι)
      ((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
          (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) i h_1) :
        { i : ι // ∀ (j : ι), r j i → f j < f i }))
    ((hrr'.toEmbedding (r := r') (s := r) : (a : { i : ι // ∀ (j : ι), r j i → f j < f i }) → ι)
      ((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
          (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) j h) :
        { i : ι // ∀ (j : ι), r j i → f j < f i }))
have refine_2 : r'
  ((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
    (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) i h_1))
  ((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
    (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) j h))
Tactic: rwa [hrr'.2, @enum_lt_enum _ r']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
i j : Ordinal.{u}
h_1 : i < type r'
h : j < type r'
h_2 : i < j
refine_2 :
  r'
    ((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) i h_1))
    ((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) j h))
⊢ r
    ((hrr'.toEmbedding (r := r') (s := r) : (a : { i : ι // ∀ (j : ι), r j i → f j < f i }) → ι)
      ((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
          (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) i h_1) :
        { i : ι // ∀ (j : ι), r j i → f j < f i }))
    ((hrr'.toEmbedding (r := r') (s := r) : (a : { i : ι // ∀ (j : ι), r j i → f j < f i }) → ι)
      ((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
          (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) j h) :
        { i : ι // ∀ (j : ι), r j i → f j < f i }))
have refine_2₁ : Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) i h_1 <
  Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) j h
Tactic: rwa [hrr'.2, @enum_lt_enum _ r']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
⊢ a ≤
    (type r').blsub fun (i : Ordinal.{u}) (x : i < type r') ↦
      f
        (↑((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
              (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) i x)) :
          ι)
have refine_3 : ∀ (i : ι),
  f i <
    (type r').blsub fun (i : Ordinal.{u}) (x : i < type r') ↦
      f
        (↑((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
              (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) i x)) :
          ι)
Tactic: rw [← hf, lsub_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h :
  ∃ (i' : Ordinal.{u}) (hi' : i' < type r'),
    f i ≤ bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι)) i' hi'
⊢ f i <
    (type r').blsub fun (i : Ordinal.{u}) (x : i < type r') ↦
      f
        (↑((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
              (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) i x)) :
          ι)
have rcases : ∀ (i' : Ordinal.{u}) (hi' : i' < type r')
  (hfg : f i ≤ bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι)) i' hi'),
  f i <
    (type r').blsub fun (i : Ordinal.{u}) (x : i < type r') ↦
      f
        (↑((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
              (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) i x)) :
          ι)
Tactic: rcases h with ⟨i', hi', hfg⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
i : ι
⊢ f i <
    (type r').blsub fun (i : Ordinal.{u}) (x : i < type r') ↦
      f
        (↑((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
              (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) i x)) :
          ι)
have refine_3 : ∃ (i' : Ordinal.{u}) (hi' : i' < type r'),
  f i ≤ bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι)) i' hi'
Tactic: suffices h : ∃ i' hi', f i ≤ bfamilyOfFamily' r' (fun i => f i) i' hi' by
      rcases h with ⟨i', hi', hfg⟩
      exact hfg.trans_lt (lt_blsub _ _ _)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
i : ι
⊢ ∃ (i' : Ordinal.{u}) (hi' : i' < type r'),
    f i ≤ bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι)) i' hi'
have pos : ∀ (h : ∀ (j : ι), r j i → f j < f i),
  ∃ (i' : Ordinal.{u}) (hi' : i' < type r'),
    f i ≤ bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι)) i' hi'
Tactic: by_cases! h : ∀ j, r j i → f j < f i
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
i : ι
pos :
  ∀ (h : ∀ (j : ι), r j i → f j < f i),
    ∃ (i' : Ordinal.{u}) (hi' : i' < type r'),
      f i ≤ bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι)) i' hi'
⊢ ∃ (i' : Ordinal.{u}) (hi' : i' < type r'),
    f i ≤ bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι)) i' hi'
have neg : ∀ (h : ∃ (j : ι), r j i ∧ f i ≤ f j),
  ∃ (i' : Ordinal.{u}) (hi' : i' < type r'),
    f i ≤ bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι)) i' hi'
Tactic: by_cases! h : ∀ j, r j i → f j < f i
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∀ (j : ι), r j i → f j < f i
⊢ ∃ (i' : Ordinal.{u}) (hi' : i' < type r'),
    f i ≤ bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι)) i' hi'
have pos : f i ≤
  bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι))
    (((typein r').toRelEmbedding (r := r') (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) :
        (a : { i : ι // ∀ (j : ι), r j i → f j < f i }) → Ordinal.{u})
      (Subtype.mk (p := fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i) i h))
    sorry
Tactic: refine ⟨typein r' ⟨i, h⟩, typein_lt_type _ _, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∀ (j : ι), r j i → f j < f i
⊢ f i ≤
    bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι))
      (((typein r').toRelEmbedding (r := r') (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) :
          (a : { i : ι // ∀ (j : ι), r j i → f j < f i }) → Ordinal.{u})
        (Subtype.mk (p := fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i) i h))
      ⋯
have pos : f i ≤ f i
Tactic: rw [bfamilyOfFamily'_typein]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (hypothesis)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∃ (j : ι), r j i ∧ f i ≤ f j
⊢ ∃ (i' : Ordinal.{u}) (hi' : i' < type r'),
    f i ≤ bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι)) i' hi'
have hji : r (WellFounded.min (r := r) sorry (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h) i
Tactic: obtain ⟨hji, hij⟩ := wo.wf.min_mem _ h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (hypothesis)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∃ (j : ι), r j i ∧ f i ≤ f j
hji : r (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h) i
⊢ ∃ (i' : Ordinal.{u}) (hi' : i' < type r'),
    f i ≤ bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι)) i' hi'
have hij : f i ≤ f (WellFounded.min (r := r) sorry (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h)
Tactic: obtain ⟨hji, hij⟩ := wo.wf.min_mem _ h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∃ (j : ι), r j i ∧ f i ≤ f j
hji : r (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h)
⊢ ∃ (i' : Ordinal.{u}) (hi' : i' < type r'),
    f i ≤ bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι)) i' hi'
have neg : ∀ (k : ι) (hkj : r k (WellFounded.min (r := r) sorry (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h)), f k < f i
Tactic: refine ⟨typein r' ⟨_, fun k hkj => lt_of_lt_of_le ?_ hij⟩, typein_lt_type _ _, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∃ (j : ι), r j i ∧ f i ≤ f j
hji : r (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h)
neg : ∀ (k : ι) (hkj : r k (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h)), f k < f i
⊢ ∃ (i' : Ordinal.{u}) (hi' : i' < type r'),
    f i ≤ bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι)) i' hi'
have neg₁ : f i ≤
  bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι))
    (((typein r').toRelEmbedding (r := r') (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) :
        (a : { i : ι // ∀ (j : ι), r j i → f j < f i }) → Ordinal.{u})
      (Subtype.mk (p := fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i)
        (WellFounded.min (r := r) sorry (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h) sorry))
    sorry
Tactic: refine ⟨typein r' ⟨_, fun k hkj => lt_of_lt_of_le ?_ hij⟩, typein_lt_type _ _, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∃ (j : ι), r j i ∧ f i ≤ f j
hji : r (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h)
k : ι
hkj : r k (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h)
⊢ f k < f i
have neg : ∀ (H : f i ≤ f k), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∃ (j : ι), r j i ∧ f i ≤ f j
hji : r (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h)
⊢ f i ≤
    bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι))
      (((typein r').toRelEmbedding (r := r') (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) :
          (a : { i : ι // ∀ (j : ι), r j i → f j < f i }) → Ordinal.{u})
        (Subtype.mk (p := fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i)
          (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h) ⋯))
      ⋯
have neg : f i ≤
  f
    (↑(Subtype.mk (p := fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i)
          (WellFounded.min (r := r) sorry (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h) sorry) :
      ι)
Tactic: rwa [bfamilyOfFamily'_typein]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
⊢ (f a).IsFundamentalSequence o fun (b : Ordinal.{u}) (hb : b < o) ↦ f (g b hb)
have refine_1 : o ≤ (f a).cof.ord
Tactic: refine ⟨?_, @fun i j _ _ h => hf.strictMono (hg.2.1 _ _ h), ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
refine_1 : o ≤ (f a).cof.ord
⊢ (f a).IsFundamentalSequence o fun (b : Ordinal.{u}) (hb : b < o) ↦ f (g b hb)
have refine_2 : (o.blsub fun (b : Ordinal.{u}) (hb : b < o) ↦ f (g b hb)) = f a
Tactic: refine ⟨?_, @fun i j _ _ h => hf.strictMono (hg.2.1 _ _ h), ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
⊢ (o.blsub fun (b : Ordinal.{u}) (hb : b < o) ↦ f (g b hb)) = f a
have refine_2 : (a.blsub fun (b : Ordinal.{u}) (x : b < a) ↦ f b) = f a
Tactic: rw [@blsub_comp.{u, u, u} a _ (fun b _ => f b) (@fun i j _ _ h => hf.strictMono.monotone h) g
        hg.2.2]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
n : ℕ
⊢ (↑n : ONote).repr = (↑n : Ordinal.{0})
have zero : (↑0 : ONote).repr = (↑0 : Ordinal.{0})
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
n : ℕ
zero : (↑0 : ONote).repr = (↑0 : Ordinal.{0})
⊢ (↑n : ONote).repr = (↑n : Ordinal.{0})
have succ : ∀ (n : ℕ), (↑(n + 1) : ONote).repr = (↑(n + 1) : Ordinal.{0})
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
⊢ ω ^ e.repr ≤ (e.oadd n a).repr
have refine : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0})
Tactic: refine le_trans ?_ le_self_add
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h : (e₁.oadd n₁ a₁).cmp (e₂.oadd n₂ a₂) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
have revert : ∀ (h : (e₁.oadd n₁ a₁).cmp (e₂.oadd n₂ a₂) = Ordering.eq), e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
⊢ ∀ (h : (e₁.cmp e₂).then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
    e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
have lt : ∀ (h₁ : e₁.cmp e₂ = Ordering.lt)
  (h : Ordering.lt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
  e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
Tactic: cases h₁ : cmp e₁ e₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
lt :
  ∀ (h₁ : e₁.cmp e₂ = Ordering.lt)
    (h : Ordering.lt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
    e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
⊢ ∀ (h : (e₁.cmp e₂).then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
    e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
have eq : ∀ (h₁ : e₁.cmp e₂ = Ordering.eq)
  (h : Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
  e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
Tactic: cases h₁ : cmp e₁ e₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
lt :
  ∀ (h₁ : e₁.cmp e₂ = Ordering.lt)
    (h : Ordering.lt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
    e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
eq :
  ∀ (h₁ : e₁.cmp e₂ = Ordering.eq)
    (h : Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
    e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
⊢ ∀ (h : (e₁.cmp e₂).then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
    e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
have gt : ∀ (h₁ : e₁.cmp e₂ = Ordering.gt)
  (h : Ordering.gt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
  e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
Tactic: cases h₁ : cmp e₁ e₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₂ = Ordering.eq
h : Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
have eq : ∀ (h₁ : e₁.cmp e₁ = Ordering.eq), e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
Tactic: obtain rfl := eq_of_cmp_eq h₁
Cleared hypotheses: e₂, h₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h : Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq
h₁ : e₁.cmp e₁ = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
have eq : ∀ (h : Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
  e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
⊢ ∀ (h : Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
    e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
have eq : ∀ (h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.lt)
  (h : Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂)) = Ordering.eq), e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
Tactic: cases h₂ : _root_.cmp (n₁ : ℕ) n₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
eq :
  ∀ (h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.lt)
    (h : Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂)) = Ordering.eq), e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
⊢ ∀ (h : Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
    e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
have eq₁ : ∀ (h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.eq)
  (h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂)) = Ordering.eq), e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
Tactic: cases h₂ : _root_.cmp (n₁ : ℕ) n₂