α : Type ?u.70093
r : α → α → Prop
a✝ o✝ : Ordinal
f✝ : (b : Ordinal) → b < o✝ → Ordinal
a o o' : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
g : (b : Ordinal) → b < o' → Ordinal
hg : IsFundamentalSequence o o' g
i : Ordinal
hi : i < o'
⊢ g i hi < blsub o' g
α : Type ?u.70093
r : α → α → Prop
a✝ o✝ : Ordinal
f✝ : (b : Ordinal) → b < o✝ → Ordinal
a o o' : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
g : (b : Ordinal) → b < o' → Ordinal
hg : IsFundamentalSequence o o' g
i : Ordinal
hi : i < o'
⊢ g i hi < o
rw [← hg.2.2]
no goals
α : Type ?u.70093
r : α → α → Prop
a✝ o✝ : Ordinal
f✝ : (b : Ordinal) → b < o✝ → Ordinal
a o o' : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
g : (b : Ordinal) → b < o' → Ordinal
hg : IsFundamentalSequence o o' g
i : Ordinal
hi : i < o'
⊢ g i hi < blsub o' g
apply lt_blsub
case refine'_1
α : Type ?u.70093
r : α → α → Prop
a✝ o✝ : Ordinal
f✝ : (b : Ordinal) → b < o✝ → Ordinal
a o o' : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
g : (b : Ordinal) → b < o' → Ordinal
hg : IsFundamentalSequence o o' g
⊢ o' ≤ ord (cof a)

case refine'_2
α : Type ?u.70093
r : α → α → Prop
a✝ o✝ : Ordinal
f✝ : (b : Ordinal) → b < o✝ → Ordinal
a o o' : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
g : (b : Ordinal) → b < o' → Ordinal
hg : IsFundamentalSequence o o' g
⊢ (blsub o' fun i hi => f (g i hi) (_ : g i hi < o)) = a
α : Type ?u.70093
r : α → α → Prop
a✝ o✝ : Ordinal
f✝ : (b : Ordinal) → b < o✝ → Ordinal
a o o' : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
g : (b : Ordinal) → b < o' → Ordinal
hg : IsFundamentalSequence o o' g
⊢ IsFundamentalSequence a o' fun i hi => f (g i hi) (_ : g i hi < o)
refine' ⟨_, @fun i j _ _ h => hf.2.1 _ _ (hg.2.1 _ _ h), _⟩
case refine'_1
α : Type ?u.70093
r : α → α → Prop
a✝ o✝ : Ordinal
f✝ : (b : Ordinal) → b < o✝ → Ordinal
a o o' : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
g : (b : Ordinal) → b < o' → Ordinal
hg : IsFundamentalSequence o o' g
⊢ o' ≤ o
case refine'_1
α : Type ?u.70093
r : α → α → Prop
a✝ o✝ : Ordinal
f✝ : (b : Ordinal) → b < o✝ → Ordinal
a o o' : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
g : (b : Ordinal) → b < o' → Ordinal
hg : IsFundamentalSequence o o' g
⊢ o' ≤ ord (cof a)
rw [hf.cof_eq]
no goals
case refine'_1
α : Type ?u.70093
r : α → α → Prop
a✝ o✝ : Ordinal
f✝ : (b : Ordinal) → b < o✝ → Ordinal
a o o' : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
g : (b : Ordinal) → b < o' → Ordinal
hg : IsFundamentalSequence o o' g
⊢ o' ≤ o
exact hg.1.trans (ord_cof_le o)
case refine'_2
α : Type ?u.70093
r : α → α → Prop
a✝ o✝ : Ordinal
f✝ : (b : Ordinal) → b < o✝ → Ordinal
a o o' : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
g : (b : Ordinal) → b < o' → Ordinal
hg : IsFundamentalSequence o o' g
⊢ blsub o f = a

case refine'_2.hg
α : Type ?u.70093
r : α → α → Prop
a✝ o✝ : Ordinal
f✝ : (b : Ordinal) → b < o✝ → Ordinal
a o o' : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
g : (b : Ordinal) → b < o' → Ordinal
hg : IsFundamentalSequence o o' g
⊢ (blsub o' fun i hi => g i hi) = o
case refine'_2
α : Type ?u.70093
r : α → α → Prop
a✝ o✝ : Ordinal
f✝ : (b : Ordinal) → b < o✝ → Ordinal
a o o' : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
g : (b : Ordinal) → b < o' → Ordinal
hg : IsFundamentalSequence o o' g
⊢ (blsub o' fun i hi => f (g i hi) (_ : g i hi < o)) = a
rw [@blsub_comp.{u, u, u} o _ f (@IsFundamentalSequence.monotone _ _ f hf)]
case refine'_2.hg
α : Type ?u.70093
r : α → α → Prop
a✝ o✝ : Ordinal
f✝ : (b : Ordinal) → b < o✝ → Ordinal
a o o' : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
g : (b : Ordinal) → b < o' → Ordinal
hg : IsFundamentalSequence o o' g
⊢ (blsub o' fun i hi => g i hi) = o
case refine'_2
α : Type ?u.70093
r : α → α → Prop
a✝ o✝ : Ordinal
f✝ : (b : Ordinal) → b < o✝ → Ordinal
a o o' : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
g : (b : Ordinal) → b < o' → Ordinal
hg : IsFundamentalSequence o o' g
⊢ blsub o f = a

case refine'_2.hg
α : Type ?u.70093
r : α → α → Prop
a✝ o✝ : Ordinal
f✝ : (b : Ordinal) → b < o✝ → Ordinal
a o o' : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
g : (b : Ordinal) → b < o' → Ordinal
hg : IsFundamentalSequence o o' g
⊢ (blsub o' fun i hi => g i hi) = o
exact hf.2.2
no goals
case refine'_2.hg
α : Type ?u.70093
r : α → α → Prop
a✝ o✝ : Ordinal
f✝ : (b : Ordinal) → b < o✝ → Ordinal
a o o' : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
g : (b : Ordinal) → b < o' → Ordinal
hg : IsFundamentalSequence o o' g
⊢ (blsub o' fun i hi => g i hi) = o
exact hg.2.2