case h
α✝ : Type ?u.180126
β✝ : Type ?u.180129
γ : Type ?u.180132
ι : Sort ?u.180135
ι' : Sort ?u.180138
ι₂ : Sort ?u.180141
κ : ι → Sort ?u.180146
κ₁ : ι → Sort ?u.180151
κ₂ : ι → Sort ?u.180156
κ' : ι' → Sort ?u.180161
α : Type u_1
β : Type u_2
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ (x ∈ ⋃ (y : β), range fun s => ↑(f s y)) ↔ x ∈ ⋃₀ C
α✝ : Type ?u.180126
β✝ : Type ?u.180129
γ : Type ?u.180132
ι : Sort ?u.180135
ι' : Sort ?u.180138
ι₂ : Sort ?u.180141
κ : ι → Sort ?u.180146
κ₁ : ι → Sort ?u.180151
κ₂ : ι → Sort ?u.180156
κ' : ι' → Sort ?u.180161
α : Type u_1
β : Type u_2
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
⊢ (⋃ (y : β), range fun s => ↑(f s y)) = ⋃₀ C
ext x
case h.mp
α✝ : Type ?u.180126
β✝ : Type ?u.180129
γ : Type ?u.180132
ι : Sort ?u.180135
ι' : Sort ?u.180138
ι₂ : Sort ?u.180141
κ : ι → Sort ?u.180146
κ₁ : ι → Sort ?u.180151
κ₂ : ι → Sort ?u.180156
κ' : ι' → Sort ?u.180161
α : Type u_1
β : Type u_2
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ (x ∈ ⋃ (y : β), range fun s => ↑(f s y)) → x ∈ ⋃₀ C

case h.mpr
α✝ : Type ?u.180126
β✝ : Type ?u.180129
γ : Type ?u.180132
ι : Sort ?u.180135
ι' : Sort ?u.180138
ι₂ : Sort ?u.180141
κ : ι → Sort ?u.180146
κ₁ : ι → Sort ?u.180151
κ₂ : ι → Sort ?u.180156
κ' : ι' → Sort ?u.180161
α : Type u_1
β : Type u_2
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ x ∈ ⋃₀ C → x ∈ ⋃ (y : β), range fun s => ↑(f s y)
case h
α✝ : Type ?u.180126
β✝ : Type ?u.180129
γ : Type ?u.180132
ι : Sort ?u.180135
ι' : Sort ?u.180138
ι₂ : Sort ?u.180141
κ : ι → Sort ?u.180146
κ₁ : ι → Sort ?u.180151
κ₂ : ι → Sort ?u.180156
κ' : ι' → Sort ?u.180161
α : Type u_1
β : Type u_2
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ (x ∈ ⋃ (y : β), range fun s => ↑(f s y)) ↔ x ∈ ⋃₀ C
constructor
case h.mp.intro.intro.intro.intro.mk
α✝ : Type ?u.180126
β✝ : Type ?u.180129
γ : Type ?u.180132
ι : Sort ?u.180135
ι' : Sort ?u.180138
ι₂ : Sort ?u.180141
κ : ι → Sort ?u.180146
κ₁ : ι → Sort ?u.180151
κ₂ : ι → Sort ?u.180156
κ' : ι' → Sort ?u.180161
α : Type u_1
β : Type u_2
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
y : β
s : Set α
hs : s ∈ C
⊢ (fun s => ↑(f s y)) { val := s, property := hs } ∈ ⋃₀ C
case h.mp
α✝ : Type ?u.180126
β✝ : Type ?u.180129
γ : Type ?u.180132
ι : Sort ?u.180135
ι' : Sort ?u.180138
ι₂ : Sort ?u.180141
κ : ι → Sort ?u.180146
κ₁ : ι → Sort ?u.180151
κ₂ : ι → Sort ?u.180156
κ' : ι' → Sort ?u.180161
α : Type u_1
β : Type u_2
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ (x ∈ ⋃ (y : β), range fun s => ↑(f s y)) → x ∈ ⋃₀ C
rintro ⟨s, ⟨y, rfl⟩, ⟨s, hs⟩, rfl⟩
case h.mp.intro.intro.intro.intro.mk
α✝ : Type ?u.180126
β✝ : Type ?u.180129
γ : Type ?u.180132
ι : Sort ?u.180135
ι' : Sort ?u.180138
ι₂ : Sort ?u.180141
κ : ι → Sort ?u.180146
κ₁ : ι → Sort ?u.180151
κ₂ : ι → Sort ?u.180156
κ' : ι' → Sort ?u.180161
α : Type u_1
β : Type u_2
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
y : β
s : Set α
hs : s ∈ C
⊢ (fun s => ↑(f s y)) { val := s, property := hs } ∈ s
case h.mp.intro.intro.intro.intro.mk
α✝ : Type ?u.180126
β✝ : Type ?u.180129
γ : Type ?u.180132
ι : Sort ?u.180135
ι' : Sort ?u.180138
ι₂ : Sort ?u.180141
κ : ι → Sort ?u.180146
κ₁ : ι → Sort ?u.180151
κ₂ : ι → Sort ?u.180156
κ' : ι' → Sort ?u.180161
α : Type u_1
β : Type u_2
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
y : β
s : Set α
hs : s ∈ C
⊢ (fun s => ↑(f s y)) { val := s, property := hs } ∈ ⋃₀ C
refine' ⟨_, hs, _⟩
no goals
case h.mp.intro.intro.intro.intro.mk
α✝ : Type ?u.180126
β✝ : Type ?u.180129
γ : Type ?u.180132
ι : Sort ?u.180135
ι' : Sort ?u.180138
ι₂ : Sort ?u.180141
κ : ι → Sort ?u.180146
κ₁ : ι → Sort ?u.180151
κ₂ : ι → Sort ?u.180156
κ' : ι' → Sort ?u.180161
α : Type u_1
β : Type u_2
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
y : β
s : Set α
hs : s ∈ C
⊢ (fun s => ↑(f s y)) { val := s, property := hs } ∈ s
exact (f ⟨s, hs⟩ y).2
case h.mpr.intro.intro
α✝ : Type ?u.180126
β✝ : Type ?u.180129
γ : Type ?u.180132
ι : Sort ?u.180135
ι' : Sort ?u.180138
ι₂ : Sort ?u.180141
κ : ι → Sort ?u.180146
κ₁ : ι → Sort ?u.180151
κ₂ : ι → Sort ?u.180156
κ' : ι' → Sort ?u.180161
α : Type u_1
β : Type u_2
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
s : Set α
hs : s ∈ C
hx : x ∈ s
⊢ x ∈ ⋃ (y : β), range fun s => ↑(f s y)
case h.mpr
α✝ : Type ?u.180126
β✝ : Type ?u.180129
γ : Type ?u.180132
ι : Sort ?u.180135
ι' : Sort ?u.180138
ι₂ : Sort ?u.180141
κ : ι → Sort ?u.180146
κ₁ : ι → Sort ?u.180151
κ₂ : ι → Sort ?u.180156
κ' : ι' → Sort ?u.180161
α : Type u_1
β : Type u_2
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ x ∈ ⋃₀ C → x ∈ ⋃ (y : β), range fun s => ↑(f s y)
rintro ⟨s, hs, hx⟩
case h.mpr.intro.intro.intro
α✝ : Type ?u.180126
β✝ : Type ?u.180129
γ : Type ?u.180132
ι : Sort ?u.180135
ι' : Sort ?u.180138
ι₂ : Sort ?u.180141
κ : ι → Sort ?u.180146
κ₁ : ι → Sort ?u.180151
κ₂ : ι → Sort ?u.180156
κ' : ι' → Sort ?u.180161
α : Type u_1
β : Type u_2
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
s : Set α
hs : s ∈ C
hx : x ∈ s
y : β
hy : f { val := s, property := hs } y = { val := x, property := hx }
⊢ x ∈ ⋃ (y : β), range fun s => ↑(f s y)
case h.mpr.intro.intro
α✝ : Type ?u.180126
β✝ : Type ?u.180129
γ : Type ?u.180132
ι : Sort ?u.180135
ι' : Sort ?u.180138
ι₂ : Sort ?u.180141
κ : ι → Sort ?u.180146
κ₁ : ι → Sort ?u.180151
κ₂ : ι → Sort ?u.180156
κ' : ι' → Sort ?u.180161
α : Type u_1
β : Type u_2
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
s : Set α
hs : s ∈ C
hx : x ∈ s
⊢ x ∈ ⋃ (y : β), range fun s => ↑(f s y)
cases' hf ⟨s, hs⟩ ⟨x, hx⟩ with y hy
case h.mpr.intro.intro.intro
α✝ : Type ?u.180126
β✝ : Type ?u.180129
γ : Type ?u.180132
ι : Sort ?u.180135
ι' : Sort ?u.180138
ι₂ : Sort ?u.180141
κ : ι → Sort ?u.180146
κ₁ : ι → Sort ?u.180151
κ₂ : ι → Sort ?u.180156
κ' : ι' → Sort ?u.180161
α : Type u_1
β : Type u_2
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
s : Set α
hs : s ∈ C
hx : x ∈ s
y : β
hy : f { val := s, property := hs } y = { val := x, property := hx }
⊢ (fun s => ↑(f s y)) { val := s, property := hs } = x
case h.mpr.intro.intro.intro
α✝ : Type ?u.180126
β✝ : Type ?u.180129
γ : Type ?u.180132
ι : Sort ?u.180135
ι' : Sort ?u.180138
ι₂ : Sort ?u.180141
κ : ι → Sort ?u.180146
κ₁ : ι → Sort ?u.180151
κ₂ : ι → Sort ?u.180156
κ' : ι' → Sort ?u.180161
α : Type u_1
β : Type u_2
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
s : Set α
hs : s ∈ C
hx : x ∈ s
y : β
hy : f { val := s, property := hs } y = { val := x, property := hx }
⊢ x ∈ ⋃ (y : β), range fun s => ↑(f s y)
refine' ⟨_, ⟨y, rfl⟩, ⟨s, hs⟩, _⟩
no goals
case h.mpr.intro.intro.intro
α✝ : Type ?u.180126
β✝ : Type ?u.180129
γ : Type ?u.180132
ι : Sort ?u.180135
ι' : Sort ?u.180138
ι₂ : Sort ?u.180141
κ : ι → Sort ?u.180146
κ₁ : ι → Sort ?u.180151
κ₂ : ι → Sort ?u.180156
κ' : ι' → Sort ?u.180161
α : Type u_1
β : Type u_2
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
s : Set α
hs : s ∈ C
hx : x ∈ s
y : β
hy : f { val := s, property := hs } y = { val := x, property := hx }
⊢ (fun s => ↑(f s y)) { val := s, property := hs } = x
exact congr_arg Subtype.val hy