a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ ∀ (i : Ordinal) (h : i < a ♯ b),
    f i h <
      max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b))
        (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))

a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) ≤ blsub (a ♯ b) f

a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) ≤ blsub (a ♯ b) f
a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ blsub (a ♯ b) f =
    max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))
apply (blsub_le_iff.2 fun i h => _).antisymm (max_le _ _)
a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
i : Ordinal
h : i < a ♯ b
⊢ f i h <
    max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))

a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) ≤ blsub (a ♯ b) f

a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) ≤ blsub (a ♯ b) f
a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ ∀ (i : Ordinal) (h : i < a ♯ b),
    f i h <
      max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b))
        (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))

a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) ≤ blsub (a ♯ b) f

a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) ≤ blsub (a ♯ b) f
intro i h
no goals
a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) ≤ blsub (a ♯ b) f

a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) ≤ blsub (a ♯ b) f
all_goals
  apply blsub_le_of_brange_subset.{u, u, v}
  rintro c ⟨d, hd, rfl⟩
  apply mem_brange_self
case inl.intro.intro
a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
i : Ordinal
h : i < a ♯ b
a' : Ordinal
ha' : a' < a
hi : i ≤ a' ♯ b
⊢ f i h <
    max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))

case inr.intro.intro
a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
i : Ordinal
h : i < a ♯ b
b' : Ordinal
hb' : b' < b
hi : i ≤ a ♯ b'
⊢ f i h <
    max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))
a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
i : Ordinal
h : i < a ♯ b
⊢ f i h <
    max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))
rcases lt_nadd_iff.1 h with (⟨a', ha', hi⟩ | ⟨b', hb', hi⟩)
no goals
case inl.intro.intro
a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
i : Ordinal
h : i < a ♯ b
a' : Ordinal
ha' : a' < a
hi : i ≤ a' ♯ b
⊢ f i h <
    max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))
exact lt_max_of_lt_left ((hf h (nadd_lt_nadd_right ha' b) hi).trans_lt (lt_blsub _ _ ha'))
no goals
case inr.intro.intro
a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
i : Ordinal
h : i < a ♯ b
b' : Ordinal
hb' : b' < b
hi : i ≤ a ♯ b'
⊢ f i h <
    max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))
exact lt_max_of_lt_right ((hf h (nadd_lt_nadd_left hb' a) hi).trans_lt (lt_blsub _ _ hb'))
a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (brange b fun a_1 ha => (fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) a_1 ha) ⊆
    brange (a ♯ b) fun a_1 ha => f a_1 ha
a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) ≤ blsub (a ♯ b) f
apply blsub_le_of_brange_subset.{u, u, v}
case intro.intro
a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
d : Ordinal
hd : d < b
⊢ (fun a_1 ha => (fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) a_1 ha) d hd ∈ brange (a ♯ b) fun a_1 ha => f a_1 ha
a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (brange b fun a_1 ha => (fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) a_1 ha) ⊆
    brange (a ♯ b) fun a_1 ha => f a_1 ha
rintro c ⟨d, hd, rfl⟩
no goals
case intro.intro
a b c : Ordinal
f : (c : Ordinal) → c < a ♯ b → Ordinal
hf : ∀ {i j : Ordinal} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
d : Ordinal
hd : d < b
⊢ (fun a_1 ha => (fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) a_1 ha) d hd ∈ brange (a ♯ b) fun a_1 ha => f a_1 ha
apply mem_brange_self