case inl
α : Type ?u.221106
β : Type ?u.221109
γ : Type ?u.221112
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
l : IsLimit a
b0 : 0 < 0
⊢ IsLimit (a * 0)

case inr.inl.intro
α : Type ?u.221106
β : Type ?u.221109
γ : Type ?u.221112
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
l : IsLimit a
b : Ordinal
b0 : 0 < succ b
⊢ IsLimit (a * succ b)

case inr.inr
α : Type ?u.221106
β : Type ?u.221109
γ : Type ?u.221112
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
l : IsLimit a
b0 : 0 < b
lb : IsLimit b
⊢ IsLimit (a * b)
α : Type ?u.221106
β : Type ?u.221109
γ : Type ?u.221112
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
l : IsLimit a
b0 : 0 < b
⊢ IsLimit (a * b)
rcases zero_or_succ_or_limit b with (rfl | ⟨b, rfl⟩ | lb)
no goals
case inl
α : Type ?u.221106
β : Type ?u.221109
γ : Type ?u.221112
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
l : IsLimit a
b0 : 0 < 0
⊢ IsLimit (a * 0)
exact b0.false.elim
case inr.inl.intro
α : Type ?u.221106
β : Type ?u.221109
γ : Type ?u.221112
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
l : IsLimit a
b : Ordinal
b0 : 0 < succ b
⊢ IsLimit (a * b + a)
case inr.inl.intro
α : Type ?u.221106
β : Type ?u.221109
γ : Type ?u.221112
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
l : IsLimit a
b : Ordinal
b0 : 0 < succ b
⊢ IsLimit (a * succ b)
rw [mul_succ]
no goals
case inr.inl.intro
α : Type ?u.221106
β : Type ?u.221109
γ : Type ?u.221112
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
l : IsLimit a
b : Ordinal
b0 : 0 < succ b
⊢ IsLimit (a * b + a)
exact add_isLimit _ l
no goals
case inr.inr
α : Type ?u.221106
β : Type ?u.221109
γ : Type ?u.221112
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
l : IsLimit a
b0 : 0 < b
lb : IsLimit b
⊢ IsLimit (a * b)
exact mul_isLimit l.pos lb