case mp
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
⊢ IsLimit b ∨ b = 0 ∧ IsLimit a

case mpr
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit b ∨ b = 0 ∧ IsLimit a
⊢ IsLimit (a + b)
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
⊢ IsLimit (a + b) ↔ IsLimit b ∨ b = 0 ∧ IsLimit a
constructor <;> intro h
case mpr.inl
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit b
⊢ IsLimit (a + b)

case mpr.inr.intro
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
h : IsLimit a
⊢ IsLimit (a + 0)
case mpr
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit b ∨ b = 0 ∧ IsLimit a
⊢ IsLimit (a + b)
rcases h with (h | ⟨rfl, h⟩)
case mpr.inr.intro
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
h : IsLimit a
⊢ IsLimit (a + 0)
case mpr.inl
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit b
⊢ IsLimit (a + b)

case mpr.inr.intro
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
h : IsLimit a
⊢ IsLimit (a + 0)
exact add_isLimit a h
no goals
case mpr.inr.intro
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
h : IsLimit a
⊢ IsLimit (a + 0)
simpa only [add_zero]
case pos
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
h' : b = 0
⊢ IsLimit b ∨ b = 0 ∧ IsLimit a

case neg
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
h' : ¬b = 0
⊢ IsLimit b ∨ b = 0 ∧ IsLimit a
case mp
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
⊢ IsLimit b ∨ b = 0 ∧ IsLimit a
by_cases h' : b = 0
case neg.h
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
h' : ¬b = 0
⊢ IsLimit b
case neg
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
h' : ¬b = 0
⊢ IsLimit b ∨ b = 0 ∧ IsLimit a
left
case neg.h
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
h' : ¬b = 0
⊢ IsLimit (a + b - a)
case neg.h
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
h' : ¬b = 0
⊢ IsLimit b
rw [← add_sub_cancel a b]
case neg.h
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
h' : ¬b = 0
⊢ a < a + b
case neg.h
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
h' : ¬b = 0
⊢ IsLimit (a + b - a)
apply sub_isLimit h
case neg.h
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
h' : ¬b = 0
this : a + 0 < a + b
⊢ a < a + b

case this
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
h' : ¬b = 0
⊢ a + 0 < a + b
case neg.h
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
h' : ¬b = 0
⊢ a < a + b
suffices : a + 0 < a + b
case this
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
h' : ¬b = 0
⊢ a + 0 < a + b
case neg.h
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
h' : ¬b = 0
this : a + 0 < a + b
⊢ a < a + b

case this
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
h' : ¬b = 0
⊢ a + 0 < a + b
simpa only [add_zero] using this
no goals
case this
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
h' : ¬b = 0
⊢ a + 0 < a + b
rwa [add_lt_add_iff_left, Ordinal.pos_iff_ne_zero]
case pos
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit a
h' : b = 0
⊢ IsLimit b ∨ b = 0 ∧ IsLimit a
case pos
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit (a + b)
h' : b = 0
⊢ IsLimit b ∨ b = 0 ∧ IsLimit a
rw [h', add_zero] at h
case pos.h
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit a
h' : b = 0
⊢ b = 0 ∧ IsLimit a
case pos
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit a
h' : b = 0
⊢ IsLimit b ∨ b = 0 ∧ IsLimit a
right
no goals
case pos.h
α : Type ?u.248176
β : Type ?u.248179
γ : Type ?u.248182
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : IsLimit a
h' : b = 0
⊢ b = 0 ∧ IsLimit a
exact ⟨h', h⟩