a b c : Ordinal
h : IsLimit c
this : (bsup c fun x x_1 => (fun x x_2 => x + x_2) b x) = (fun x x_1 => x + x_1) b c
⊢ a < b + c ↔ ∃ c', c' < c ∧ a < b + c'
a b c : Ordinal
h : IsLimit c
⊢ a < b + c ↔ ∃ c', c' < c ∧ a < b + c'
have := IsNormal.bsup_eq.{u, u} (add_isNormal b) h
a b c : Ordinal
h : IsLimit c
this : (bsup c fun x x_1 => b + x) = b + c
⊢ a < b + c ↔ ∃ c', c' < c ∧ a < b + c'
a b c : Ordinal
h : IsLimit c
this : (bsup c fun x x_1 => (fun x x_2 => x + x_2) b x) = (fun x x_1 => x + x_1) b c
⊢ a < b + c ↔ ∃ c', c' < c ∧ a < b + c'
dsimp only at this
no goals
a b c : Ordinal
h : IsLimit c
this : (bsup c fun x x_1 => b + x) = b + c
⊢ a < b + c ↔ ∃ c', c' < c ∧ a < b + c'
rw [← this, lt_bsup, bex_def]