case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.82270
ι : Sort ?u.82273
ι' : Sort ?u.82276
f : ι → α
s t : Set α
x₁ : α
x₂ : β
h : Sum.inr x₂ = Sum.inl x₁
⊢ Sum.inl x₁ ∈ ⊥
α : Type u_1
β : Type u_2
γ : Type ?u.82270
ι : Sort ?u.82273
ι' : Sort ?u.82276
f : ι → α
s t : Set α
⊢ range Sum.inl ⊓ range Sum.inr ≤ ⊥
rintro y ⟨⟨x₁, rfl⟩, ⟨x₂, h⟩⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.82270
ι : Sort ?u.82273
ι' : Sort ?u.82276
f : ι → α
s t : Set α
x₁ : α
x₂ : β
h : Sum.inr x₂ = Sum.inl x₁
⊢ Sum.inl x₁ ∈ ⊥
exact Sum.noConfusion h
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.82270
ι : Sort ?u.82273
ι' : Sort ?u.82276
f : ι → α
s t : Set α
⊢ ⊤ ≤ range Sum.inl ⊔ range Sum.inr
rintro (x | y) - <;> [left; right] <;> exact mem_range_self _