-- Mathlib/Data/Set/Finite/Lattice.lean
/-- An indexed union of pairwise disjoint sets is finite iff all sets are finite, and all but
finitely many are empty. -/
lemma finite_iUnion_iff {ι : Type*} {s : ι → Set α} (hs : Pairwise fun i j ↦ Disjoint (s i) (s j)) :
    (⋃ i, s i).Finite ↔ (∀ i, (s i).Finite) ∧ {i | (s i).Nonempty}.Finite where
  mp h

Proof state:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (∀ (i : ι), (s i).Finite) ∧ {i | (s i).Nonempty}.Finite
⊢ ∀ i ∉ {i | (s i).Nonempty}, s i = ∅

Tactic:
simp [not_nonempty_iff_eq_empty]

Result:
no goals

Proof state:
case mk.mk.a
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i => ⟨Exists.choose ⋯, ⋯⟩
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ↑(u ⟨j, hj⟩) ∈ s ↑⟨j, hj⟩

Tactic:
exact hj.choose_spec

Result:
no goals

Proof state:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i => ⟨Exists.choose ⋯, ⋯⟩
⊢ Injective u

Tactic:
rintro ⟨i, hi⟩ ⟨j, hj⟩ hij

Result:
case mk.mk
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i => ⟨Exists.choose ⋯, ⋯⟩
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Proof state:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i => ⟨Exists.choose ⋯, ⋯⟩
u_inj : Injective u
this : Finite ↑(⋃ i, s i)
⊢ {i | (s i).Nonempty}.Finite

Tactic:
exact .of_injective u u_inj

Result:
no goals

Proof state:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
⊢ (∀ (i : ι), (s i).Finite) ∧ {i | (s i).Nonempty}.Finite

Tactic:
refine ⟨fun i ↦ h.subset <| subset_iUnion _ _, ?_⟩

Result:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
⊢ {i | (s i).Nonempty}.Finite

Proof state:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
⊢ {i | (s i).Nonempty}.Finite

Tactic:
let u (i : {i | (s i).Nonempty}) : ⋃ i, s i := ⟨i.2.choose, mem_iUnion.2 ⟨i.1, i.2.choose_spec⟩⟩

Result:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i => ⟨Exists.choose ⋯, ⋯⟩
⊢ {i | (s i).Nonempty}.Finite

Proof state:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i => ⟨Exists.choose ⋯, ⋯⟩
⊢ {i | (s i).Nonempty}.Finite

Tactic:
have u_inj : Function.Injective u := by
  rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
  ext
  refine hs.eq <| not_disjoint_iff.2 ⟨u ⟨i, hi⟩, hi.choose_spec, ?_⟩
  rw [hij]
  exact hj.choose_spec

Result:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i => ⟨Exists.choose ⋯, ⋯⟩
u_inj : Injective u
⊢ {i | (s i).Nonempty}.Finite

Proof state:
case mk.mk.a
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i => ⟨Exists.choose ⋯, ⋯⟩
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ↑⟨i, hi⟩ = ↑⟨j, hj⟩

Tactic:
refine hs.eq <| not_disjoint_iff.2 ⟨u ⟨i, hi⟩, hi.choose_spec, ?_⟩

Result:
case mk.mk.a
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i => ⟨Exists.choose ⋯, ⋯⟩
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ↑(u ⟨i, hi⟩) ∈ s ↑⟨j, hj⟩

Proof state:
case mk.mk.a
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i => ⟨Exists.choose ⋯, ⋯⟩
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ↑(u ⟨i, hi⟩) ∈ s ↑⟨j, hj⟩

Tactic:
rw [hij]

Result:
case mk.mk.a
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i => ⟨Exists.choose ⋯, ⋯⟩
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ↑(u ⟨j, hj⟩) ∈ s ↑⟨j, hj⟩

Proof state:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i => ⟨Exists.choose ⋯, ⋯⟩
u_inj : Injective u
⊢ {i | (s i).Nonempty}.Finite

Tactic:
have : Finite (⋃ i, s i) := h

Result:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i => ⟨Exists.choose ⋯, ⋯⟩
u_inj : Injective u
this : Finite ↑(⋃ i, s i)
⊢ {i | (s i).Nonempty}.Finite

Proof state:
case mk.mk
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i => ⟨Exists.choose ⋯, ⋯⟩
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Tactic:
ext

Result:
case mk.mk.a
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j => Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i => ⟨Exists.choose ⋯, ⋯⟩
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ↑⟨i, hi⟩ = ↑⟨j, hj⟩