case h
α : Type ?u.161812
β : Type ?u.161815
γ : Type ?u.161818
ι✝ : Sort ?u.161821
ι' : Sort ?u.161824
ι₂ : Sort ?u.161827
κ : ι✝ → Sort ?u.161832
κ₁ : ι✝ → Sort ?u.161837
κ₂ : ι✝ → Sort ?u.161842
κ' : ι' → Sort ?u.161847
ι : Type u_1
σ : ι → Type u_2
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ (x ∈ ⋃ (i : ι), Sigma.mk i '' (Sigma.mk i ⁻¹' s)) ↔ x ∈ s
α : Type ?u.161812
β : Type ?u.161815
γ : Type ?u.161818
ι✝ : Sort ?u.161821
ι' : Sort ?u.161824
ι₂ : Sort ?u.161827
κ : ι✝ → Sort ?u.161832
κ₁ : ι✝ → Sort ?u.161837
κ₂ : ι✝ → Sort ?u.161842
κ' : ι' → Sort ?u.161847
ι : Type u_1
σ : ι → Type u_2
s : Set (Sigma σ)
⊢ (⋃ (i : ι), Sigma.mk i '' (Sigma.mk i ⁻¹' s)) = s
ext x
case h
α : Type ?u.161812
β : Type ?u.161815
γ : Type ?u.161818
ι✝ : Sort ?u.161821
ι' : Sort ?u.161824
ι₂ : Sort ?u.161827
κ : ι✝ → Sort ?u.161832
κ₁ : ι✝ → Sort ?u.161837
κ₂ : ι✝ → Sort ?u.161842
κ' : ι' → Sort ?u.161847
ι : Type u_1
σ : ι → Type u_2
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ (∃ i x_1, { fst := i, snd := x_1 } ∈ s ∧ { fst := i, snd := x_1 } = x) ↔ x ∈ s
case h
α : Type ?u.161812
β : Type ?u.161815
γ : Type ?u.161818
ι✝ : Sort ?u.161821
ι' : Sort ?u.161824
ι₂ : Sort ?u.161827
κ : ι✝ → Sort ?u.161832
κ₁ : ι✝ → Sort ?u.161837
κ₂ : ι✝ → Sort ?u.161842
κ' : ι' → Sort ?u.161847
ι : Type u_1
σ : ι → Type u_2
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ (x ∈ ⋃ (i : ι), Sigma.mk i '' (Sigma.mk i ⁻¹' s)) ↔ x ∈ s
simp only [mem_iUnion, mem_image, mem_preimage]
case h.mp
α : Type ?u.161812
β : Type ?u.161815
γ : Type ?u.161818
ι✝ : Sort ?u.161821
ι' : Sort ?u.161824
ι₂ : Sort ?u.161827
κ : ι✝ → Sort ?u.161832
κ₁ : ι✝ → Sort ?u.161837
κ₂ : ι✝ → Sort ?u.161842
κ' : ι' → Sort ?u.161847
ι : Type u_1
σ : ι → Type u_2
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ (∃ i x_1, { fst := i, snd := x_1 } ∈ s ∧ { fst := i, snd := x_1 } = x) → x ∈ s

case h.mpr
α : Type ?u.161812
β : Type ?u.161815
γ : Type ?u.161818
ι✝ : Sort ?u.161821
ι' : Sort ?u.161824
ι₂ : Sort ?u.161827
κ : ι✝ → Sort ?u.161832
κ₁ : ι✝ → Sort ?u.161837
κ₂ : ι✝ → Sort ?u.161842
κ' : ι' → Sort ?u.161847
ι : Type u_1
σ : ι → Type u_2
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ x ∈ s → ∃ i x_1, { fst := i, snd := x_1 } ∈ s ∧ { fst := i, snd := x_1 } = x
case h
α : Type ?u.161812
β : Type ?u.161815
γ : Type ?u.161818
ι✝ : Sort ?u.161821
ι' : Sort ?u.161824
ι₂ : Sort ?u.161827
κ : ι✝ → Sort ?u.161832
κ₁ : ι✝ → Sort ?u.161837
κ₂ : ι✝ → Sort ?u.161842
κ' : ι' → Sort ?u.161847
ι : Type u_1
σ : ι → Type u_2
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ (∃ i x_1, { fst := i, snd := x_1 } ∈ s ∧ { fst := i, snd := x_1 } = x) ↔ x ∈ s
constructor
case h.mp.intro.intro.intro
α : Type ?u.161812
β : Type ?u.161815
γ : Type ?u.161818
ι✝ : Sort ?u.161821
ι' : Sort ?u.161824
ι₂ : Sort ?u.161827
κ : ι✝ → Sort ?u.161832
κ₁ : ι✝ → Sort ?u.161837
κ₂ : ι✝ → Sort ?u.161842
κ' : ι' → Sort ?u.161847
ι : Type u_1
σ : ι → Type u_2
s : Set (Sigma σ)
i : ι
a : σ i
h : { fst := i, snd := a } ∈ s
⊢ { fst := i, snd := a } ∈ s
case h.mp
α : Type ?u.161812
β : Type ?u.161815
γ : Type ?u.161818
ι✝ : Sort ?u.161821
ι' : Sort ?u.161824
ι₂ : Sort ?u.161827
κ : ι✝ → Sort ?u.161832
κ₁ : ι✝ → Sort ?u.161837
κ₂ : ι✝ → Sort ?u.161842
κ' : ι' → Sort ?u.161847
ι : Type u_1
σ : ι → Type u_2
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ (∃ i x_1, { fst := i, snd := x_1 } ∈ s ∧ { fst := i, snd := x_1 } = x) → x ∈ s
rintro ⟨i, a, h, rfl⟩
no goals
case h.mp.intro.intro.intro
α : Type ?u.161812
β : Type ?u.161815
γ : Type ?u.161818
ι✝ : Sort ?u.161821
ι' : Sort ?u.161824
ι₂ : Sort ?u.161827
κ : ι✝ → Sort ?u.161832
κ₁ : ι✝ → Sort ?u.161837
κ₂ : ι✝ → Sort ?u.161842
κ' : ι' → Sort ?u.161847
ι : Type u_1
σ : ι → Type u_2
s : Set (Sigma σ)
i : ι
a : σ i
h : { fst := i, snd := a } ∈ s
⊢ { fst := i, snd := a } ∈ s
exact h
case h.mpr
α : Type ?u.161812
β : Type ?u.161815
γ : Type ?u.161818
ι✝ : Sort ?u.161821
ι' : Sort ?u.161824
ι₂ : Sort ?u.161827
κ : ι✝ → Sort ?u.161832
κ₁ : ι✝ → Sort ?u.161837
κ₂ : ι✝ → Sort ?u.161842
κ' : ι' → Sort ?u.161847
ι : Type u_1
σ : ι → Type u_2
s : Set (Sigma σ)
x : (i : ι) × σ i
h : x ∈ s
⊢ ∃ i x_1, { fst := i, snd := x_1 } ∈ s ∧ { fst := i, snd := x_1 } = x
case h.mpr
α : Type ?u.161812
β : Type ?u.161815
γ : Type ?u.161818
ι✝ : Sort ?u.161821
ι' : Sort ?u.161824
ι₂ : Sort ?u.161827
κ : ι✝ → Sort ?u.161832
κ₁ : ι✝ → Sort ?u.161837
κ₂ : ι✝ → Sort ?u.161842
κ' : ι' → Sort ?u.161847
ι : Type u_1
σ : ι → Type u_2
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ x ∈ s → ∃ i x_1, { fst := i, snd := x_1 } ∈ s ∧ { fst := i, snd := x_1 } = x
intro h
case h.mpr.mk
α : Type ?u.161812
β : Type ?u.161815
γ : Type ?u.161818
ι✝ : Sort ?u.161821
ι' : Sort ?u.161824
ι₂ : Sort ?u.161827
κ : ι✝ → Sort ?u.161832
κ₁ : ι✝ → Sort ?u.161837
κ₂ : ι✝ → Sort ?u.161842
κ' : ι' → Sort ?u.161847
ι : Type u_1
σ : ι → Type u_2
s : Set (Sigma σ)
i : ι
a : σ i
h : { fst := i, snd := a } ∈ s
⊢ ∃ i_1 x, { fst := i_1, snd := x } ∈ s ∧ { fst := i_1, snd := x } = { fst := i, snd := a }
case h.mpr
α : Type ?u.161812
β : Type ?u.161815
γ : Type ?u.161818
ι✝ : Sort ?u.161821
ι' : Sort ?u.161824
ι₂ : Sort ?u.161827
κ : ι✝ → Sort ?u.161832
κ₁ : ι✝ → Sort ?u.161837
κ₂ : ι✝ → Sort ?u.161842
κ' : ι' → Sort ?u.161847
ι : Type u_1
σ : ι → Type u_2
s : Set (Sigma σ)
x : (i : ι) × σ i
h : x ∈ s
⊢ ∃ i x_1, { fst := i, snd := x_1 } ∈ s ∧ { fst := i, snd := x_1 } = x
cases' x with i a
no goals
case h.mpr.mk
α : Type ?u.161812
β : Type ?u.161815
γ : Type ?u.161818
ι✝ : Sort ?u.161821
ι' : Sort ?u.161824
ι₂ : Sort ?u.161827
κ : ι✝ → Sort ?u.161832
κ₁ : ι✝ → Sort ?u.161837
κ₂ : ι✝ → Sort ?u.161842
κ' : ι' → Sort ?u.161847
ι : Type u_1
σ : ι → Type u_2
s : Set (Sigma σ)
i : ι
a : σ i
h : { fst := i, snd := a } ∈ s
⊢ ∃ i_1 x, { fst := i_1, snd := x } ∈ s ∧ { fst := i_1, snd := x } = { fst := i, snd := a }
exact ⟨i, a, h, rfl⟩