α : Type ?u.70717
r : α → α → Prop
a : Ordinal
h : ∃ o f, IsFundamentalSequence a o f
⊢ ∃ f, IsFundamentalSequence a (ord (cof a)) f

case h
α : Type ?u.70717
r : α → α → Prop
a : Ordinal
⊢ ∃ o f, IsFundamentalSequence a o f
α : Type ?u.70717
r : α → α → Prop
a : Ordinal
⊢ ∃ f, IsFundamentalSequence a (ord (cof a)) f
suffices h : ∃ o f, IsFundamentalSequence a o f
case h.intro.intro.intro
α : Type ?u.70717
r : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
⊢ ∃ o f, IsFundamentalSequence a o f
case h
α : Type ?u.70717
r : α → α → Prop
a : Ordinal
⊢ ∃ o f, IsFundamentalSequence a o f
rcases exists_lsub_cof a with ⟨ι, f, hf, hι⟩
case h.intro.intro.intro.intro.intro
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
⊢ ∃ o f, IsFundamentalSequence a o f
case h.intro.intro.intro
α : Type ?u.70717
r : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
⊢ ∃ o f, IsFundamentalSequence a o f
rcases ord_eq ι with ⟨r, wo, hr⟩
case h.intro.intro.intro.intro.intro
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this : IsWellOrder ι r
⊢ ∃ o f, IsFundamentalSequence a o f
case h.intro.intro.intro.intro.intro
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
⊢ ∃ o f, IsFundamentalSequence a o f
haveI := wo
case h.intro.intro.intro.intro.intro
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
⊢ ∃ o f, IsFundamentalSequence a o f
case h.intro.intro.intro.intro.intro
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this : IsWellOrder ι r
⊢ ∃ o f, IsFundamentalSequence a o f
let r' := Subrel r { i | ∀ j, r j i → f j < f i }
case h.intro.intro.intro.intro.intro
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
⊢ ∃ o f, IsFundamentalSequence a o f
case h.intro.intro.intro.intro.intro
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
⊢ ∃ o f, IsFundamentalSequence a o f
let hrr' : r' ↪r r := Subrel.relEmbedding _ _
case h.intro.intro.intro.intro.intro
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
⊢ ∃ o f, IsFundamentalSequence a o f
case h.intro.intro.intro.intro.intro
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
⊢ ∃ o f, IsFundamentalSequence a o f
haveI := hrr'.isWellOrder
case h.intro.intro.intro.intro.intro.refine'_1
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
⊢ type r ≤ ord (cof a)

case h.intro.intro.intro.intro.intro.refine'_2
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
i j : Ordinal
x✝¹ : i < type r'
h : j < type r'
x✝ : i < j
⊢ r ↑(enum r' i x✝¹) ↑(enum r' j h)

case h.intro.intro.intro.intro.intro.refine'_3
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
⊢ a ≤ blsub (type r') fun j h => f ↑(enum r' j h)
case h.intro.intro.intro.intro.intro
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
⊢ ∃ o f, IsFundamentalSequence a o f
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 _) _⟩
case intro.intro
α : Type ?u.70717
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
⊢ ∃ f, IsFundamentalSequence a (ord (cof a)) f
α : Type ?u.70717
r : α → α → Prop
a : Ordinal
h : ∃ o f, IsFundamentalSequence a o f
⊢ ∃ f, IsFundamentalSequence a (ord (cof a)) f
rcases h with ⟨o, f, hf⟩
no goals
case intro.intro
α : Type ?u.70717
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
⊢ ∃ f, IsFundamentalSequence a (ord (cof a)) f
exact ⟨_, hf.ord_cof⟩
no goals
case h.intro.intro.intro.intro.intro.refine'_1
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
⊢ type r ≤ ord (cof a)
rw [← hι, hr]
case h.intro.intro.intro.intro.intro.refine'_2
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
i j : Ordinal
x✝¹ : i < type r'
h : j < type r'
x✝ : i < j
⊢ r (↑hrr'.toEmbedding (enum r' i x✝¹)) (↑hrr'.toEmbedding (enum r' j h))
case h.intro.intro.intro.intro.intro.refine'_2
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
i j : Ordinal
x✝¹ : i < type r'
h : j < type r'
x✝ : i < j
⊢ r ↑(enum r' i x✝¹) ↑(enum r' j h)
change r (hrr'.1 _) (hrr'.1 _)
no goals
case h.intro.intro.intro.intro.intro.refine'_2
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
i j : Ordinal
x✝¹ : i < type r'
h : j < type r'
x✝ : i < j
⊢ r (↑hrr'.toEmbedding (enum r' i x✝¹)) (↑hrr'.toEmbedding (enum r' j h))
rwa [hrr'.2, @enum_lt_enum _ r']
case h.intro.intro.intro.intro.intro.refine'_3
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
⊢ ∀ (i : ι), f i < blsub (type r') fun j h => f ↑(enum r' j h)
case h.intro.intro.intro.intro.intro.refine'_3
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
⊢ a ≤ blsub (type r') fun j h => f ↑(enum r' j h)
rw [← hf, lsub_le_iff]
case h.intro.intro.intro.intro.intro.refine'_3
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
i : ι
⊢ f i < blsub (type r') fun j h => f ↑(enum r' j h)
case h.intro.intro.intro.intro.intro.refine'_3
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
⊢ ∀ (i : ι), f i < blsub (type r') fun j h => f ↑(enum r' j h)
intro i
case h.intro.intro.intro.intro.intro.refine'_3
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
i : ι
h : ∃ i' hi', f i ≤ bfamilyOfFamily' r' (fun i => f ↑i) i' hi'
⊢ f i < blsub (type r') fun j h => f ↑(enum r' j h)

case h
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
i : ι
⊢ ∃ i' hi', f i ≤ bfamilyOfFamily' r' (fun i => f ↑i) i' hi'
case h.intro.intro.intro.intro.intro.refine'_3
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
i : ι
⊢ f i < blsub (type r') fun j h => f ↑(enum r' j h)
suffices h : ∃ i' hi', f i ≤ bfamilyOfFamily' r' (fun i => f i) i' hi'
case pos
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {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' hi', f i ≤ bfamilyOfFamily' r' (fun i => f ↑i) i' hi'

case neg
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {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' hi', f i ≤ bfamilyOfFamily' r' (fun i => f ↑i) i' hi'
case h
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
i : ι
⊢ ∃ i' hi', f i ≤ bfamilyOfFamily' r' (fun i => f ↑i) i' hi'
by_cases h : ∀ j, r j i → f j < f i
case h.intro.intro.intro.intro.intro.refine'_3.intro.intro
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
i : ι
i' : Ordinal
hi' : i' < type r'
hfg : f i ≤ bfamilyOfFamily' r' (fun i => f ↑i) i' hi'
⊢ f i < blsub (type r') fun j h => f ↑(enum r' j h)
case h.intro.intro.intro.intro.intro.refine'_3
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
i : ι
h : ∃ i' hi', f i ≤ bfamilyOfFamily' r' (fun i => f ↑i) i' hi'
⊢ f i < blsub (type r') fun j h => f ↑(enum r' j h)
rcases h with ⟨i', hi', hfg⟩
no goals
case h.intro.intro.intro.intro.intro.refine'_3.intro.intro
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}
this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'
i : ι
i' : Ordinal
hi' : i' < type r'
hfg : f i ≤ bfamilyOfFamily' r' (fun i => f ↑i) i' hi'
⊢ f i < blsub (type r') fun j h => f ↑(enum r' j h)
exact hfg.trans_lt (lt_blsub _ _ _)
case pos
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {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 => f ↑i) (typein r' { val := i, property := h })
      (_ : typein r' { val := i, property := h } < type r')
case pos
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {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' hi', f i ≤ bfamilyOfFamily' r' (fun i => f ↑i) i' hi'
refine' ⟨typein r' ⟨i, h⟩, typein_lt_type _ _, _⟩
no goals
case pos
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {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 => f ↑i) (typein r' { val := i, property := h })
      (_ : typein r' { val := i, property := h } < type r')
rw [bfamilyOfFamily'_typein]
case neg
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {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' hi', f i ≤ bfamilyOfFamily' r' (fun i => f ↑i) i' hi'
case neg
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {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' hi', f i ≤ bfamilyOfFamily' r' (fun i => f ↑i) i' hi'
push_neg  at h
case neg.intro
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {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 (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h)
⊢ ∃ i' hi', f i ≤ bfamilyOfFamily' r' (fun i => f ↑i) i' hi'
case neg
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {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' hi', f i ≤ bfamilyOfFamily' r' (fun i => f ↑i) i' hi'
cases' wo.wf.min_mem _ h with hji hij
case neg.intro.refine'_1
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {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 (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h)
k : ι
hkj : r k (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h)
⊢ f k < f i

case neg.intro.refine'_2
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {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 (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h)
⊢ f i ≤
    bfamilyOfFamily' r' (fun i => f ↑i)
      (typein r'
        { val := WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h,
          property :=
            (_ :
              ∀ (k : ι),
                r k (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h) →
                  f k < f (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h)) })
      (_ :
        typein r'
            { val := WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h,
              property :=
                (_ :
                  ∀ (k : ι),
                    r k (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h) →
                      f k < f (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h)) } <
          type r')
case neg.intro
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {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 (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h)
⊢ ∃ i' hi', f i ≤ bfamilyOfFamily' r' (fun i => f ↑i) i' hi'
refine' ⟨typein r' ⟨_, fun k hkj => lt_of_lt_of_le _ hij⟩, typein_lt_type _ _, _⟩
case neg.intro.refine'_1
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {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 (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h)
k : ι
hkj : r k (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h)
H : f i ≤ f k
⊢ False
case neg.intro.refine'_1
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {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 (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h)
k : ι
hkj : r k (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h)
⊢ f k < f i
by_contra' H
no goals
case neg.intro.refine'_1
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {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 (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h)
k : ι
hkj : r k (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h)
H : f i ≤ f k
⊢ False
exact (wo.wf.not_lt_min _ h ⟨IsTrans.trans _ _ _ hkj hji, H⟩) hkj
no goals
case neg.intro.refine'_2
α : Type ?u.70717
r✝ : α → α → Prop
a : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = a
hι : (#ι) = cof a
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : ord (#ι) = type r
this✝ : IsWellOrder ι r
r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop :=
  Subrel r {i | ∀ (j : ι), r j i → f j < f i}
hrr' : r' ↪r r := Subrel.relEmbedding r {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 (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h)
⊢ f i ≤
    bfamilyOfFamily' r' (fun i => f ↑i)
      (typein r'
        { val := WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h,
          property :=
            (_ :
              ∀ (k : ι),
                r k (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h) →
                  f k < f (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h)) })
      (_ :
        typein r'
            { val := WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h,
              property :=
                (_ :
                  ∀ (k : ι),
                    r k (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h) →
                      f k < f (WellFounded.min (_ : WellFounded r) (fun x => r x i ∧ f i ≤ f x) h)) } <
          type r')
rwa [bfamilyOfFamily'_typein]