-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_range_eq_sUnion {α β : Type*} (C : Set (Set α)) {f : ∀ s : C, β → (s : Type _)}
    (hf : ∀ s : C, Surjective (f s)) : ⋃ y : β, range (fun s : C => (f s y).val) = ⋃₀ C

Proof state:
case h.mpr.intro.intro
α : Type u_12
β : Type u_13
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)

Tactic:
obtain ⟨y, hy⟩ := hf ⟨s, hs⟩ ⟨x, hx⟩

Result:
case h.mpr.intro.intro.intro
α : Type u_12
β : Type u_13
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 ⟨s, hs⟩ y = ⟨x, hx⟩
⊢ x ∈ ⋃ y, range fun s => ↑(f s y)

Proof state:
case h
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ (x ∈ ⋃ y, range fun s => ↑(f s y)) ↔ x ∈ ⋃₀ C

Tactic:
constructor

Result:
case h.mp
α : Type u_12
β : Type u_13
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_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ x ∈ ⋃₀ C → x ∈ ⋃ y, range fun s => ↑(f s y)

Proof state:
case h.mp.intro.intro.intro.intro.mk
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
y : β
s : Set α
hs : s ∈ C
⊢ (fun s => ↑(f s y)) ⟨s, hs⟩ ∈ ⋃₀ C

Tactic:
refine ⟨_, hs, ?_⟩

Result:
case h.mp.intro.intro.intro.intro.mk
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
y : β
s : Set α
hs : s ∈ C
⊢ (fun s => ↑(f s y)) ⟨s, hs⟩ ∈ s

Proof state:
case h.mpr
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ x ∈ ⋃₀ C → x ∈ ⋃ y, range fun s => ↑(f s y)

Tactic:
rintro ⟨s, hs, hx⟩

Result:
case h.mpr.intro.intro
α : Type u_12
β : Type u_13
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)

Proof state:
case h.mpr.intro.intro.intro
α : Type u_12
β : Type u_13
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 ⟨s, hs⟩ y = ⟨x, hx⟩
⊢ x ∈ ⋃ y, range fun s => ↑(f s y)

Tactic:
refine ⟨_, ⟨y, rfl⟩, ⟨s, hs⟩, ?_⟩

Result:
case h.mpr.intro.intro.intro
α : Type u_12
β : Type u_13
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 ⟨s, hs⟩ y = ⟨x, hx⟩
⊢ (fun s => ↑(f s y)) ⟨s, hs⟩ = x

Proof state:
case h.mpr.intro.intro.intro
α : Type u_12
β : Type u_13
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 ⟨s, hs⟩ y = ⟨x, hx⟩
⊢ (fun s => ↑(f s y)) ⟨s, hs⟩ = x

Tactic:
exact congr_arg Subtype.val hy

Result:
no goals

Proof state:
case h.mp.intro.intro.intro.intro.mk
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
y : β
s : Set α
hs : s ∈ C
⊢ (fun s => ↑(f s y)) ⟨s, hs⟩ ∈ s

Tactic:
exact (f ⟨s, hs⟩ y).2

Result:
no goals

Proof state:
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
⊢ (⋃ y, range fun s => ↑(f s y)) = ⋃₀ C

Tactic:
ext x

Result:
case h
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ (x ∈ ⋃ y, range fun s => ↑(f s y)) ↔ x ∈ ⋃₀ C

Proof state:
case h.mp
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ (x ∈ ⋃ y, range fun s => ↑(f s y)) → x ∈ ⋃₀ C

Tactic:
rintro ⟨s, ⟨y, rfl⟩, ⟨s, hs⟩, rfl⟩

Result:
case h.mp.intro.intro.intro.intro.mk
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
y : β
s : Set α
hs : s ∈ C
⊢ (fun s => ↑(f s y)) ⟨s, hs⟩ ∈ ⋃₀ C