case h
α : Type u_1
β : Type u_2
γ : Type ?u.180962
ι : Sort u_3
ι' : Sort ?u.180968
ι₂ : Sort ?u.180971
κ : ι → Sort ?u.180976
κ₁ : ι → Sort ?u.180981
κ₂ : ι → Sort ?u.180986
κ' : ι' → Sort ?u.180991
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (x ∈ ⋃ (y : β), range fun x => ↑(f x y)) ↔ x ∈ ⋃ (x : ι), C x
α : Type u_1
β : Type u_2
γ : Type ?u.180962
ι : Sort u_3
ι' : Sort ?u.180968
ι₂ : Sort ?u.180971
κ : ι → Sort ?u.180976
κ₁ : ι → Sort ?u.180981
κ₂ : ι → Sort ?u.180986
κ' : ι' → Sort ?u.180991
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
⊢ (⋃ (y : β), range fun x => ↑(f x y)) = ⋃ (x : ι), C x
ext x
case h
α : Type u_1
β : Type u_2
γ : Type ?u.180962
ι : Sort u_3
ι' : Sort ?u.180968
ι₂ : Sort ?u.180971
κ : ι → Sort ?u.180976
κ₁ : ι → Sort ?u.180981
κ₂ : ι → Sort ?u.180986
κ' : ι' → Sort ?u.180991
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ range fun x => ↑(f x i)) ↔ ∃ i, x ∈ C i
case h
α : Type u_1
β : Type u_2
γ : Type ?u.180962
ι : Sort u_3
ι' : Sort ?u.180968
ι₂ : Sort ?u.180971
κ : ι → Sort ?u.180976
κ₁ : ι → Sort ?u.180981
κ₂ : ι → Sort ?u.180986
κ' : ι' → Sort ?u.180991
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (x ∈ ⋃ (y : β), range fun x => ↑(f x y)) ↔ x ∈ ⋃ (x : ι), C x
rw [mem_iUnion, mem_iUnion]
case h.mp
α : Type u_1
β : Type u_2
γ : Type ?u.180962
ι : Sort u_3
ι' : Sort ?u.180968
ι₂ : Sort ?u.180971
κ : ι → Sort ?u.180976
κ₁ : ι → Sort ?u.180981
κ₂ : ι → Sort ?u.180986
κ' : ι' → Sort ?u.180991
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ range fun x => ↑(f x i)) → ∃ i, x ∈ C i

case h.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.180962
ι : Sort u_3
ι' : Sort ?u.180968
ι₂ : Sort ?u.180971
κ : ι → Sort ?u.180976
κ₁ : ι → Sort ?u.180981
κ₂ : ι → Sort ?u.180986
κ' : ι' → Sort ?u.180991
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ C i) → ∃ i, x ∈ range fun x => ↑(f x i)
case h
α : Type u_1
β : Type u_2
γ : Type ?u.180962
ι : Sort u_3
ι' : Sort ?u.180968
ι₂ : Sort ?u.180971
κ : ι → Sort ?u.180976
κ₁ : ι → Sort ?u.180981
κ₂ : ι → Sort ?u.180986
κ' : ι' → Sort ?u.180991
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ range fun x => ↑(f x i)) ↔ ∃ i, x ∈ C i
constructor
case h.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.180962
ι : Sort u_3
ι' : Sort ?u.180968
ι₂ : Sort ?u.180971
κ : ι → Sort ?u.180976
κ₁ : ι → Sort ?u.180981
κ₂ : ι → Sort ?u.180986
κ' : ι' → Sort ?u.180991
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
y : β
i : ι
⊢ ∃ i_1, (fun x => ↑(f x y)) i ∈ C i_1
case h.mp
α : Type u_1
β : Type u_2
γ : Type ?u.180962
ι : Sort u_3
ι' : Sort ?u.180968
ι₂ : Sort ?u.180971
κ : ι → Sort ?u.180976
κ₁ : ι → Sort ?u.180981
κ₂ : ι → Sort ?u.180986
κ' : ι' → Sort ?u.180991
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ range fun x => ↑(f x i)) → ∃ i, x ∈ C i
rintro ⟨y, i, rfl⟩
no goals
case h.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.180962
ι : Sort u_3
ι' : Sort ?u.180968
ι₂ : Sort ?u.180971
κ : ι → Sort ?u.180976
κ₁ : ι → Sort ?u.180981
κ₂ : ι → Sort ?u.180986
κ' : ι' → Sort ?u.180991
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
y : β
i : ι
⊢ ∃ i_1, (fun x => ↑(f x y)) i ∈ C i_1
exact ⟨i, (f i y).2⟩
case h.mpr.intro
α : Type u_1
β : Type u_2
γ : Type ?u.180962
ι : Sort u_3
ι' : Sort ?u.180968
ι₂ : Sort ?u.180971
κ : ι → Sort ?u.180976
κ₁ : ι → Sort ?u.180981
κ₂ : ι → Sort ?u.180986
κ' : ι' → Sort ?u.180991
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
i : ι
hx : x ∈ C i
⊢ ∃ i, x ∈ range fun x => ↑(f x i)
case h.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.180962
ι : Sort u_3
ι' : Sort ?u.180968
ι₂ : Sort ?u.180971
κ : ι → Sort ?u.180976
κ₁ : ι → Sort ?u.180981
κ₂ : ι → Sort ?u.180986
κ' : ι' → Sort ?u.180991
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ C i) → ∃ i, x ∈ range fun x => ↑(f x i)
rintro ⟨i, hx⟩
case h.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.180962
ι : Sort u_3
ι' : Sort ?u.180968
ι₂ : Sort ?u.180971
κ : ι → Sort ?u.180976
κ₁ : ι → Sort ?u.180981
κ₂ : ι → Sort ?u.180986
κ' : ι' → Sort ?u.180991
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
i : ι
hx : x ∈ C i
y : β
hy : f i y = { val := x, property := hx }
⊢ ∃ i, x ∈ range fun x => ↑(f x i)
case h.mpr.intro
α : Type u_1
β : Type u_2
γ : Type ?u.180962
ι : Sort u_3
ι' : Sort ?u.180968
ι₂ : Sort ?u.180971
κ : ι → Sort ?u.180976
κ₁ : ι → Sort ?u.180981
κ₂ : ι → Sort ?u.180986
κ' : ι' → Sort ?u.180991
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
i : ι
hx : x ∈ C i
⊢ ∃ i, x ∈ range fun x => ↑(f x i)
cases' hf i ⟨x, hx⟩ with y hy
no goals
case h.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.180962
ι : Sort u_3
ι' : Sort ?u.180968
ι₂ : Sort ?u.180971
κ : ι → Sort ?u.180976
κ₁ : ι → Sort ?u.180981
κ₂ : ι → Sort ?u.180986
κ' : ι' → Sort ?u.180991
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
i : ι
hx : x ∈ C i
y : β
hy : f i y = { val := x, property := hx }
⊢ ∃ i, x ∈ range fun x => ↑(f x i)
exact ⟨y, i, congr_arg Subtype.val hy⟩