α✝ : Type ?u.142517
β✝ : Type ?u.142520
γ : Type ?u.142523
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal
α : Type u_1
x✝³ : α → α → Prop
x✝² : IsWellOrder α x✝³
β : Type u_1
x✝¹ : β → β → Prop
x✝ : IsWellOrder β x✝¹
⊢ IsEmpty (β × α) ↔ IsEmpty α ∨ IsEmpty β
α✝ : Type ?u.142517
β✝ : Type ?u.142520
γ : Type ?u.142523
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal
α : Type u_1
x✝³ : α → α → Prop
x✝² : IsWellOrder α x✝³
β : Type u_1
x✝¹ : β → β → Prop
x✝ : IsWellOrder β x✝¹
⊢ type x✝³ * type x✝¹ = 0 ↔ type x✝³ = 0 ∨ type x✝¹ = 0
simp_rw [← type_prod_lex, type_eq_zero_iff_isEmpty]
α✝ : Type ?u.142517
β✝ : Type ?u.142520
γ : Type ?u.142523
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal
α : Type u_1
x✝³ : α → α → Prop
x✝² : IsWellOrder α x✝³
β : Type u_1
x✝¹ : β → β → Prop
x✝ : IsWellOrder β x✝¹
⊢ IsEmpty (β × α) ↔ IsEmpty β ∨ IsEmpty α
α✝ : Type ?u.142517
β✝ : Type ?u.142520
γ : Type ?u.142523
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal
α : Type u_1
x✝³ : α → α → Prop
x✝² : IsWellOrder α x✝³
β : Type u_1
x✝¹ : β → β → Prop
x✝ : IsWellOrder β x✝¹
⊢ IsEmpty (β × α) ↔ IsEmpty α ∨ IsEmpty β
rw [or_comm]
no goals
α✝ : Type ?u.142517
β✝ : Type ?u.142520
γ : Type ?u.142523
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal
α : Type u_1
x✝³ : α → α → Prop
x✝² : IsWellOrder α x✝³
β : Type u_1
x✝¹ : β → β → Prop
x✝ : IsWellOrder β x✝¹
⊢ IsEmpty (β × α) ↔ IsEmpty β ∨ IsEmpty α
exact isEmpty_prod