awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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'
⊢ ∃ (o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}), a.IsFundamentalSequence o f

Tactic:
⟨_, _, hrr'.ordinal_type_le.trans ?_, @fun i j _ h _ => (enum r' ⟨j, h⟩).prop _ ?_,
      le_antisymm (blsub_le fun i hi => lsub_le_iff.1 hf.le _) ?_⟩

Premises used: Eq.le, Ordinal.blsub_le, Subtype.mk, le_antisymm, Ordinal.lsub_le_iff, Subtype.prop, RelEmbedding.ordinal_type_le, And.intro, Exists.intro, Iff.mp, Ordinal.enum, LE.le.trans, Subtype.val, DFunLike.coe
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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'
refine_1 : type r ≤ a.cof.ord
refine_2 :
  ∀ (i j : Ordinal.{u}) (x : i < type r') (h : j < type r'),
    i < j →
      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 x)) :
          ι)
        (↑((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)) :
          ι)
refine_3 :
  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)) :
          ι)
⊢ ∃ (o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}), a.IsFundamentalSequence o f

Tactic:
refine
    ⟨_, _, hrr'.ordinal_type_le.trans ?_, @fun i j _ h _ => (enum r' ⟨j, h⟩).prop _ ?_,
      le_antisymm (blsub_le fun i hi => lsub_le_iff.1 hf.le _) ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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'
refine_1 : type r ≤ (#ι).ord
refine_1₁ refine_1₂ : type r ≤ type r
⊢ type r ≤ a.cof.ord

Tactic:
rw [← hι, hr]
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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
    ((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 }))
⊢ 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:
change r (hrr'.1 _) (hrr'.1 _)

Premises used: RelEmbedding.toEmbedding, DFunLike.coe
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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))
refine_2₁ refine_2₂ refine_2₃ 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
⊢ 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 }))

Tactic:
rwa [hrr'.2, @enum_lt_enum _ r']

Premises used: Ordinal.enum_lt_enum, RelEmbedding.map_rel_iff'
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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'
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)) :
            ι)
⊢ 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)) :
          ι)

Tactic:
rw [← hf, lsub_le_iff]

Premises used: Ordinal.lsub_le_iff
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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'
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)) :
            ι)
⊢ 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⟩
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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'
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:
hfg.trans_lt (lt_blsub _ _ _)

Premises used: Ordinal.lt_blsub, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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'
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:
exact hfg.trans_lt (lt_blsub _ _ _)

Premises used: Ordinal.lt_blsub, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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 : ι
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'
⊢ 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:
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 _ _ _)
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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'
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'
⊢ ∃ (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
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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'

Tactic:
⟨typein r' ⟨i, h⟩, typein_lt_type _ _, ?_⟩

Premises used: PrincipalSeg.toRelEmbedding, Ordinal.typein_lt_type, Subtype.mk, Exists.intro, DFunLike.coe, Ordinal.typein
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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
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))
      ⋯
⊢ ∃ (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:
refine ⟨typein r' ⟨i, h⟩, typein_lt_type _ _, ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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
pos pos₁ : f i ≤ 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))
      ⋯

Tactic:
rw [bfamilyOfFamily'_typein]

Premises used: Ordinal.bfamilyOfFamily'_typein
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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
⊢ r (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h) i

Tactic:
obtain ⟨hji, hij⟩ := wo.wf.min_mem _ h

Premises used: WellFounded.min_mem, IsWellFounded.wf
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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
⊢ f i ≤ f (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h)

Tactic:
obtain ⟨hji, hij⟩ := wo.wf.min_mem _ h

Premises used: WellFounded.min_mem, IsWellFounded.wf
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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'

Tactic:
⟨typein r' ⟨_, fun k hkj => lt_of_lt_of_le ?_ hij⟩, typein_lt_type _ _, ?_⟩

Premises used: PrincipalSeg.toRelEmbedding, Ordinal.typein_lt_type, Subtype.mk, Exists.intro, DFunLike.coe, lt_of_lt_of_le, Ordinal.typein
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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
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) ⋯ (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'

Tactic:
refine ⟨typein r' ⟨_, fun k hkj => lt_of_lt_of_le ?_ hij⟩, typein_lt_type _ _, ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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)
neg : ∀ (H : f i ≤ f k), False
⊢ f k < f i

Tactic:
by_contra! H
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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)
H : f i ≤ f k
⊢ False

Tactic:
(wo.wf.not_lt_min {j | r j i ∧ f i ≤ f j} ⟨IsTrans.trans _ _ _ hkj hji, H⟩) hkj

Premises used: setOf, IsTrans.trans, LE.le, IsWellFounded.wf, And, And.intro, WellFounded.not_lt_min
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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)
H : f i ≤ f k
⊢ False

Tactic:
exact (wo.wf.not_lt_min {j | r j i ∧ f i ≤ f j} ⟨IsTrans.trans _ _ _ hkj hji, H⟩) hkj

Premises used: setOf, IsTrans.trans, LE.le, IsWellFounded.wf, And, And.intro, WellFounded.not_lt_min