-- Mathlib/Data/Set/Finite/Lattice.lean
theorem eq_finite_iUnion_of_finite_subset_iUnion {ι} {s : ι → Set α} {t : Set α} (tfin : t.Finite)
    (h : t ⊆ ⋃ i, s i) :
    ∃ I : Set ι,
      I.Finite ∧
        ∃ σ : { i | i ∈ I } → Set α, (∀ i, (σ i).Finite) ∧ (∀ i, σ i ⊆ s i) ∧ t = ⋃ i, σ i :=
  let ⟨I, Ifin, hI⟩ := finite_subset_iUnion tfin h
  ⟨I, Ifin, fun x => s x ∩ t, fun _ => tfin.subset inter_subset_right, fun _ =>
    inter_subset_left, by
    ext x
    rw [mem_iUnion]
    constructor
    · intro x_in
      rcases mem_iUnion.mp (hI x_in) with ⟨i, _, ⟨hi, rfl⟩, H⟩
      exact ⟨⟨i, hi⟩, ⟨H, x_in⟩⟩
    · rintro ⟨i, -, H⟩
      exact H⟩

Proof state:
case h.mpr
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ (∃ i, x ∈ s ↑i ∩ t) → x ∈ t

Tactic:
rintro ⟨i, -, H⟩

Result:
case h.mpr.intro.intro
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
i : ↑{i | i ∈ I}
H : x ∈ t
⊢ x ∈ t

Proof state:
case h
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ x ∈ t ↔ x ∈ ⋃ i, (fun x => s ↑x ∩ t) i

Tactic:
rw [mem_iUnion]

Result:
case h
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ x ∈ t ↔ ∃ i, x ∈ s ↑i ∩ t

Proof state:
case h.mp
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ x ∈ t → ∃ i, x ∈ s ↑i ∩ t

Tactic:
intro x_in

Result:
case h.mp
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
x_in : x ∈ t
⊢ ∃ i, x ∈ s ↑i ∩ t

Proof state:
case h.mp
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
x_in : x ∈ t
⊢ ∃ i, x ∈ s ↑i ∩ t

Tactic:
rcases mem_iUnion.mp (hI x_in) with ⟨i, _, ⟨hi, rfl⟩, H⟩

Result:
case h.mp.intro.intro.intro.intro
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
x_in : x ∈ t
i : ι
hi : i ∈ I
H : x ∈ (fun h => s i) hi
⊢ ∃ i, x ∈ s ↑i ∩ t

Proof state:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
⊢ t = ⋃ i, (fun x => s ↑x ∩ t) i

Tactic:
ext x

Result:
case h
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ x ∈ t ↔ x ∈ ⋃ i, (fun x => s ↑x ∩ t) i

Proof state:
case h.mp.intro.intro.intro.intro
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
x_in : x ∈ t
i : ι
hi : i ∈ I
H : x ∈ (fun h => s i) hi
⊢ ∃ i, x ∈ s ↑i ∩ t

Tactic:
exact ⟨⟨i, hi⟩, ⟨H, x_in⟩⟩

Result:
no goals

Proof state:
case h
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ x ∈ t ↔ ∃ i, x ∈ s ↑i ∩ t

Tactic:
constructor

Result:
case h.mp
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ x ∈ t → ∃ i, x ∈ s ↑i ∩ t

case h.mpr
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ (∃ i, x ∈ s ↑i ∩ t) → x ∈ t

Proof state:
case h.mpr.intro.intro
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
i : ↑{i | i ∈ I}
H : x ∈ t
⊢ x ∈ t

Tactic:
exact H

Result:
no goals