case refine'_1
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
⊢ o ≤ ord (cof (f a))

case refine'_2
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
⊢ (blsub o fun b hb => f (g b hb)) = f a
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
⊢ IsFundamentalSequence (f a) o fun b hb => f (g b hb)
refine' ⟨_, @fun i j _ _ h => hf.strictMono (hg.2.1 _ _ h), _⟩
case refine'_1.intro.intro.intro
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
⊢ o ≤ ord (cof (f a))
case refine'_1
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
⊢ o ≤ ord (cof (f a))
rcases exists_lsub_cof (f a) with ⟨ι, f', hf', hι⟩
case refine'_1.intro.intro.intro
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
⊢ cof a ≤ (#ι)
case refine'_1.intro.intro.intro
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
⊢ o ≤ ord (cof (f a))
rw [← hg.cof_eq, ord_le_ord, ← hι]
case refine'_1.intro.intro.intro
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
⊢ (lsub fun i => sInf {b | f' i ≤ f b}) = a
case refine'_1.intro.intro.intro
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
⊢ cof a ≤ (#ι)
suffices (lsub.{u, u} fun i => sInf { b : Ordinal | f' i ≤ f b }) = a by
  rw [← this]
  apply cof_lsub_le
case refine'_1.intro.intro.intro
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
H : ∀ (i : ι), ∃ b, b < a ∧ f' i ≤ f b
⊢ (lsub fun i => sInf {b | f' i ≤ f b}) = a
case refine'_1.intro.intro.intro
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
⊢ (lsub fun i => sInf {b | f' i ≤ f b}) = a
have H : ∀ i, ∃ b < a, f' i ≤ f b := fun i => by
  have := lt_lsub.{u, u} f' i
  rw [hf', ← IsNormal.blsub_eq.{u, u} hf ha, lt_blsub_iff] at this
  simpa using this
case refine'_1.intro.intro.intro.refine'_1
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
H : ∀ (i : ι), ∃ b, b < a ∧ f' i ≤ f b
i : ι
⊢ sInf {b | f' i ≤ f b} < a

case refine'_1.intro.intro.intro.refine'_2
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
H : ∀ (i : ι), ∃ b, b < a ∧ f' i ≤ f b
b : Ordinal
hb : b < a
⊢ b < lsub fun i => sInf {b | f' i ≤ f b}
case refine'_1.intro.intro.intro
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
H : ∀ (i : ι), ∃ b, b < a ∧ f' i ≤ f b
⊢ (lsub fun i => sInf {b | f' i ≤ f b}) = a
refine' (lsub_le fun i => _).antisymm (le_of_forall_lt fun b hb => _)
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
this : (lsub fun i => sInf {b | f' i ≤ f b}) = a
⊢ cof (lsub fun i => sInf {b | f' i ≤ f b}) ≤ (#ι)
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
this : (lsub fun i => sInf {b | f' i ≤ f b}) = a
⊢ cof a ≤ (#ι)
rw [← this]
no goals
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
this : (lsub fun i => sInf {b | f' i ≤ f b}) = a
⊢ cof (lsub fun i => sInf {b | f' i ≤ f b}) ≤ (#ι)
apply cof_lsub_le
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
i : ι
this : f' i < lsub f'
⊢ ∃ b, b < a ∧ f' i ≤ f b
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
i : ι
⊢ ∃ b, b < a ∧ f' i ≤ f b
have := lt_lsub.{u, u} f' i
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
i : ι
this : ∃ i_1 hi, f' i ≤ f i_1
⊢ ∃ b, b < a ∧ f' i ≤ f b
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
i : ι
this : f' i < lsub f'
⊢ ∃ b, b < a ∧ f' i ≤ f b
rw [hf', ← IsNormal.blsub_eq.{u, u} hf ha, lt_blsub_iff] at this
no goals
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
i : ι
this : ∃ i_1 hi, f' i ≤ f i_1
⊢ ∃ b, b < a ∧ f' i ≤ f b
simpa using this
case refine'_1.intro.intro.intro.refine'_1.intro.intro
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
H : ∀ (i : ι), ∃ b, b < a ∧ f' i ≤ f b
i : ι
b : Ordinal
hb : b < a
hb' : f' i ≤ f b
⊢ sInf {b | f' i ≤ f b} < a
case refine'_1.intro.intro.intro.refine'_1
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
H : ∀ (i : ι), ∃ b, b < a ∧ f' i ≤ f b
i : ι
⊢ sInf {b | f' i ≤ f b} < a
rcases H i with ⟨b, hb, hb'⟩
no goals
case refine'_1.intro.intro.intro.refine'_1.intro.intro
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
H : ∀ (i : ι), ∃ b, b < a ∧ f' i ≤ f b
i : ι
b : Ordinal
hb : b < a
hb' : f' i ≤ f b
⊢ sInf {b | f' i ≤ f b} < a
exact lt_of_le_of_lt (csInf_le' hb') hb
case refine'_1.intro.intro.intro.refine'_2
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
H : ∀ (i : ι), ∃ b, b < a ∧ f' i ≤ f b
b : Ordinal
hb : b < a
this : f b < f a
⊢ b < lsub fun i => sInf {b | f' i ≤ f b}
case refine'_1.intro.intro.intro.refine'_2
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
H : ∀ (i : ι), ∃ b, b < a ∧ f' i ≤ f b
b : Ordinal
hb : b < a
⊢ b < lsub fun i => sInf {b | f' i ≤ f b}
have := hf.strictMono hb
case refine'_1.intro.intro.intro.refine'_2
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
H : ∀ (i : ι), ∃ b, b < a ∧ f' i ≤ f b
b : Ordinal
hb : b < a
this : ∃ i, f b ≤ f' i
⊢ b < lsub fun i => sInf {b | f' i ≤ f b}
case refine'_1.intro.intro.intro.refine'_2
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
H : ∀ (i : ι), ∃ b, b < a ∧ f' i ≤ f b
b : Ordinal
hb : b < a
this : f b < f a
⊢ b < lsub fun i => sInf {b | f' i ≤ f b}
rw [← hf', lt_lsub_iff] at this
case refine'_1.intro.intro.intro.refine'_2.intro
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
H : ∀ (i : ι), ∃ b, b < a ∧ f' i ≤ f b
b : Ordinal
hb : b < a
i : ι
hi : f b ≤ f' i
⊢ b < lsub fun i => sInf {b | f' i ≤ f b}
case refine'_1.intro.intro.intro.refine'_2
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
H : ∀ (i : ι), ∃ b, b < a ∧ f' i ≤ f b
b : Ordinal
hb : b < a
this : ∃ i, f b ≤ f' i
⊢ b < lsub fun i => sInf {b | f' i ≤ f b}
cases' this with i hi
case refine'_1.intro.intro.intro.refine'_2.intro.intro.intro
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
H : ∀ (i : ι), ∃ b, b < a ∧ f' i ≤ f b
b✝ : Ordinal
hb✝ : b✝ < a
i : ι
hi : f b✝ ≤ f' i
b : Ordinal
left✝ : b < a
hb : f' i ≤ f b
⊢ b✝ < lsub fun i => sInf {b | f' i ≤ f b}
case refine'_1.intro.intro.intro.refine'_2.intro
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
H : ∀ (i : ι), ∃ b, b < a ∧ f' i ≤ f b
b : Ordinal
hb : b < a
i : ι
hi : f b ≤ f' i
⊢ b < lsub fun i => sInf {b | f' i ≤ f b}
rcases H i with ⟨b, _, hb⟩
no goals
case refine'_1.intro.intro.intro.refine'_2.intro.intro.intro
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
H : ∀ (i : ι), ∃ b, b < a ∧ f' i ≤ f b
b✝ : Ordinal
hb✝ : b✝ < a
i : ι
hi : f b✝ ≤ f' i
b : Ordinal
left✝ : b < a
hb : f' i ≤ f b
⊢ b✝ < lsub fun i => sInf {b | f' i ≤ f b}
exact
  ((le_csInf_iff'' ⟨b, by exact hb⟩).2 fun c hc =>
    hf.strictMono.le_iff_le.1 (hi.trans hc)).trans_lt (lt_lsub _ i)
no goals
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
ι : Type u
f' : ι → Ordinal
hf' : lsub f' = f a
hι : (#ι) = cof (f a)
H : ∀ (i : ι), ∃ b, b < a ∧ f' i ≤ f b
b✝ : Ordinal
hb✝ : b✝ < a
i : ι
hi : f b✝ ≤ f' i
b : Ordinal
left✝ : b < a
hb : f' i ≤ f b
⊢ b ∈ fun c =>
    Quot.lift
      (fun a₁ =>
        Quotient.lift
          ((fun x x_1 =>
              match x with
              | { α := α, r := r, wo := wo } =>
                match x_1 with
                | { α := α_1, r := s, wo := wo } => Nonempty (r ≼i s))
            a₁)
          (_ :
            ∀ (a b : WellOrder),
              a ≈ b →
                (match a₁ with
                  | { α := α, r := r, wo := wo } =>
                    match a with
                    | { α := α_1, r := s, wo := wo } => Nonempty (r ≼i s)) =
                  match a₁ with
                  | { α := α, r := r, wo := wo } =>
                    match b with
                    | { α := α_1, r := s, wo := wo } => Nonempty (r ≼i s))
          (f c))
      (_ :
        ∀ (a b : WellOrder),
          a ≈ b →
            (fun a₁ =>
                  Quotient.lift
                    (fun x =>
                      match a₁ with
                      | { α := α, r := r, wo := wo } =>
                        match x with
                        | { α := α_1, r := s, wo := wo } => Nonempty (r ≼i s))
                    (_ :
                      ∀ (a b : WellOrder),
                        a ≈ b →
                          (fun x x_1 =>
                                match x with
                                | { α := α, r := r, wo := wo } =>
                                  match x_1 with
                                  | { α := α_1, r := s, wo := wo } => Nonempty (r ≼i s))
                              a₁ a =
                            (fun x x_1 =>
                                match x with
                                | { α := α, r := r, wo := wo } =>
                                  match x_1 with
                                  | { α := α_1, r := s, wo := wo } => Nonempty (r ≼i s))
                              a₁ b)
                    (f c))
                a =
              (fun a₁ =>
                  Quotient.lift
                    (fun x =>
                      match a₁ with
                      | { α := α, r := r, wo := wo } =>
                        match x with
                        | { α := α_1, r := s, wo := wo } => Nonempty (r ≼i s))
                    (_ :
                      ∀ (a b : WellOrder),
                        a ≈ b →
                          (fun x x_1 =>
                                match x with
                                | { α := α, r := r, wo := wo } =>
                                  match x_1 with
                                  | { α := α_1, r := s, wo := wo } => Nonempty (r ≼i s))
                              a₁ a =
                            (fun x x_1 =>
                                match x with
                                | { α := α, r := r, wo := wo } =>
                                  match x_1 with
                                  | { α := α_1, r := s, wo := wo } => Nonempty (r ≼i s))
                              a₁ b)
                    (f c))
                b)
      (f' i)
exact hb
case refine'_2
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
⊢ (blsub a fun b x => f b) = f a
case refine'_2
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
⊢ (blsub o fun b hb => f (g b hb)) = f a
rw [@blsub_comp.{u, u, u} a _ (fun b _ => f b) (@fun i j _ _ h => hf.strictMono.monotone h) g
    hg.2.2]
no goals
case refine'_2
α : Type ?u.94822
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a o : Ordinal
ha : IsLimit a
g : (b : Ordinal) → b < o → Ordinal
hg : IsFundamentalSequence a o g
⊢ (blsub a fun b x => f b) = f a
exact IsNormal.blsub_eq.{u, u} hf ha