α : Type ?u.327023
β : Type ?u.327026
γ : Type ?u.327029
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : lsub f = 0
i : ι
⊢ False
α : Type ?u.327023
β : Type ?u.327026
γ : Type ?u.327029
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
⊢ lsub f = 0 ↔ IsEmpty ι
refine' ⟨fun h => ⟨fun i => _⟩, fun h => @lsub_empty _ h _⟩
α : Type ?u.327023
β : Type ?u.327026
γ : Type ?u.327029
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : lsub f = 0
i : ι
this : 0 < lsub f
⊢ False
α : Type ?u.327023
β : Type ?u.327026
γ : Type ?u.327029
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : lsub f = 0
i : ι
⊢ False
have := @lsub_pos.{_, v} _ ⟨i⟩ f
α : Type ?u.327023
β : Type ?u.327026
γ : Type ?u.327029
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : lsub f = 0
i : ι
this : 0 < 0
⊢ False
α : Type ?u.327023
β : Type ?u.327026
γ : Type ?u.327029
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : lsub f = 0
i : ι
this : 0 < lsub f
⊢ False
rw [h] at this
no goals
α : Type ?u.327023
β : Type ?u.327026
γ : Type ?u.327029
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : lsub f = 0
i : ι
this : 0 < 0
⊢ False
exact this.false