case mp
ι : Type u_1
ι' : Type ?u.6266
α : ι → Type u_2
β : ι → Type ?u.6276
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : (i : ι) × α i
⊢ x ∈ Set.Sigma {i} t → x ∈ Sigma.mk i '' t i

case mpr
ι : Type u_1
ι' : Type ?u.6266
α : ι → Type u_2
β : ι → Type ?u.6276
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : (i : ι) × α i
⊢ x ∈ Sigma.mk i '' t i → x ∈ Set.Sigma {i} t
ι : Type u_1
ι' : Type ?u.6266
α : ι → Type u_2
β : ι → Type ?u.6276
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : (i : ι) × α i
⊢ x ∈ Set.Sigma {i} t ↔ x ∈ Sigma.mk i '' t i
constructor
case mp.mk
ι : Type u_1
ι' : Type ?u.6266
α : ι → Type u_2
β : ι → Type ?u.6276
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j✝ : ι
a✝ : α i
j : ι
a : α j
⊢ { fst := j, snd := a } ∈ Set.Sigma {i} t → { fst := j, snd := a } ∈ Sigma.mk i '' t i
case mp
ι : Type u_1
ι' : Type ?u.6266
α : ι → Type u_2
β : ι → Type ?u.6276
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : (i : ι) × α i
⊢ x ∈ Set.Sigma {i} t → x ∈ Sigma.mk i '' t i
obtain ⟨j, a⟩ := x
case mp.mk.intro
ι : Type u_1
ι' : Type ?u.6266
α : ι → Type u_2
β : ι → Type ?u.6276
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
j✝ j : ι
a✝ : α j
ha : { fst := j, snd := a✝ }.snd ∈ t { fst := j, snd := a✝ }.fst
a : α j
⊢ { fst := j, snd := a✝ } ∈ Sigma.mk j '' t j
case mp.mk
ι : Type u_1
ι' : Type ?u.6266
α : ι → Type u_2
β : ι → Type ?u.6276
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j✝ : ι
a✝ : α i
j : ι
a : α j
⊢ { fst := j, snd := a } ∈ Set.Sigma {i} t → { fst := j, snd := a } ∈ Sigma.mk i '' t i
rintro ⟨rfl : j = i, ha⟩
no goals
case mp.mk.intro
ι : Type u_1
ι' : Type ?u.6266
α : ι → Type u_2
β : ι → Type ?u.6276
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
j✝ j : ι
a✝ : α j
ha : { fst := j, snd := a✝ }.snd ∈ t { fst := j, snd := a✝ }.fst
a : α j
⊢ { fst := j, snd := a✝ } ∈ Sigma.mk j '' t j
exact mem_image_of_mem _ ha
case mpr.intro.intro
ι : Type u_1
ι' : Type ?u.6266
α : ι → Type u_2
β : ι → Type ?u.6276
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a b : α i
hb : b ∈ t i
⊢ { fst := i, snd := b } ∈ Set.Sigma {i} t
case mpr
ι : Type u_1
ι' : Type ?u.6266
α : ι → Type u_2
β : ι → Type ?u.6276
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : (i : ι) × α i
⊢ x ∈ Sigma.mk i '' t i → x ∈ Set.Sigma {i} t
rintro ⟨b, hb, rfl⟩
no goals
case mpr.intro.intro
ι : Type u_1
ι' : Type ?u.6266
α : ι → Type u_2
β : ι → Type ?u.6276
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a b : α i
hb : b ∈ t i
⊢ { fst := i, snd := b } ∈ Set.Sigma {i} t
exact ⟨rfl, hb⟩