case h₁
ι : Type u_1
ι' : Type ?u.81
α : ι → Type u_2
β : ι → Type ?u.91
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i✝ j : ι
a : α i✝
i : ι
⊢ range (Sigma.mk i) ⊆ Sigma.fst ⁻¹' {i}

case h₂
ι : Type u_1
ι' : Type ?u.81
α : ι → Type u_2
β : ι → Type ?u.91
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i✝ j : ι
a : α i✝
i : ι
⊢ Sigma.fst ⁻¹' {i} ⊆ range (Sigma.mk i)
ι : Type u_1
ι' : Type ?u.81
α : ι → Type u_2
β : ι → Type ?u.91
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i✝ j : ι
a : α i✝
i : ι
⊢ range (Sigma.mk i) = Sigma.fst ⁻¹' {i}
apply Subset.antisymm
case h₁.intro
ι : Type u_1
ι' : Type ?u.81
α : ι → Type u_2
β : ι → Type ?u.91
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i✝ j : ι
a : α i✝
i : ι
b : α i
⊢ { fst := i, snd := b } ∈ Sigma.fst ⁻¹' {i}
case h₁
ι : Type u_1
ι' : Type ?u.81
α : ι → Type u_2
β : ι → Type ?u.91
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i✝ j : ι
a : α i✝
i : ι
⊢ range (Sigma.mk i) ⊆ Sigma.fst ⁻¹' {i}
rintro _ ⟨b, rfl⟩
no goals
case h₁.intro
ι : Type u_1
ι' : Type ?u.81
α : ι → Type u_2
β : ι → Type ?u.91
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i✝ j : ι
a : α i✝
i : ι
b : α i
⊢ { fst := i, snd := b } ∈ Sigma.fst ⁻¹' {i}
simp
case h₂.mk.refl
ι : Type u_1
ι' : Type ?u.81
α : ι → Type u_2
β : ι → Type ?u.91
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : ι
y : α x
⊢ { fst := x, snd := y } ∈ range (Sigma.mk { fst := x, snd := y }.fst)
case h₂
ι : Type u_1
ι' : Type ?u.81
α : ι → Type u_2
β : ι → Type ?u.91
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i✝ j : ι
a : α i✝
i : ι
⊢ Sigma.fst ⁻¹' {i} ⊆ range (Sigma.mk i)
rintro ⟨x, y⟩ (rfl | _)
no goals
case h₂.mk.refl
ι : Type u_1
ι' : Type ?u.81
α : ι → Type u_2
β : ι → Type ?u.91
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : ι
y : α x
⊢ { fst := x, snd := y } ∈ range (Sigma.mk { fst := x, snd := y }.fst)
exact mem_range_self y