-- Mathlib/Data/Set/Countable.lean
theorem countable_setOf_nonempty_of_disjoint {f : β → Set α}
    (hf : Pairwise (Disjoint on f)) {s : Set α} (h'f : ∀ t, f t ⊆ s) (hs : s.Countable) :
    Set.Countable {t | (f t).Nonempty}

Proof state:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
⊢ Countable ↑{t | (f t).Nonempty}

Tactic:
have A : Injective F := by
  rintro ⟨t, ht⟩ ⟨t', ht'⟩ htt'
  have A : (f t ∩ f t').Nonempty := by
    refine ⟨F ⟨t, ht⟩, hF ⟨t, _⟩, ?_⟩
    rw [htt']
    exact hF ⟨t', _⟩
  simp only [Subtype.mk.injEq]
  by_contra H
  exact not_disjoint_iff_nonempty_inter.2 A (hf H)

Result:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
A : Injective F
⊢ Countable ↑{t | (f t).Nonempty}

Proof state:
case mk.mk
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
A : (f t ∩ f t').Nonempty
H : ¬t = t'
⊢ False

Tactic:
exact not_disjoint_iff_nonempty_inter.2 A (hf H)

Result:
no goals

Proof state:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
⊢ ∀ (t : { t // (f t).Nonempty }), ∃ x, ↑x ∈ f ↑t

Tactic:
rintro ⟨t, ⟨x, hx⟩⟩

Result:
case mk.intro
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
t : β
x : α
hx : x ∈ f t
⊢ ∃ x_1, ↑x_1 ∈ f ↑⟨t, ⋯⟩

Proof state:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
A : Injective F
⊢ Countable ↑{t | (f t).Nonempty}

Tactic:
exact Injective.countable A

Result:
no goals

Proof state:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : s.Countable
⊢ {t | (f t).Nonempty}.Countable

Tactic:
rw [← Set.countable_coe_iff] at hs ⊢

Result:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
⊢ Countable ↑{t | (f t).Nonempty}

Proof state:
case mk.mk
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
A : (f t ∩ f t').Nonempty
⊢ ⟨t, ht⟩ = ⟨t', ht'⟩

Tactic:
simp only [Subtype.mk.injEq]

Result:
case mk.mk
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
A : (f t ∩ f t').Nonempty
⊢ t = t'

Proof state:
case mk.mk
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
A : (f t ∩ f t').Nonempty
⊢ t = t'

Tactic:
by_contra H

Result:
case mk.mk
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
A : (f t ∩ f t').Nonempty
H : ¬t = t'
⊢ False

Proof state:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
⊢ ↑(F ⟨t', ht'⟩) ∈ f t'

Tactic:
exact hF ⟨t', _⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
⊢ Injective F

Tactic:
rintro ⟨t, ht⟩ ⟨t', ht'⟩ htt'

Result:
case mk.mk
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
⊢ ⟨t, ht⟩ = ⟨t', ht'⟩

Proof state:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
⊢ ↑(F ⟨t, ht⟩) ∈ f t'

Tactic:
rw [htt']

Result:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
⊢ ↑(F ⟨t', ht'⟩) ∈ f t'

Proof state:
case mk.intro
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
t : β
x : α
hx : x ∈ f t
⊢ ∃ x_1, ↑x_1 ∈ f ↑⟨t, ⋯⟩

Tactic:
exact ⟨⟨x, (h'f t hx)⟩, hx⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
⊢ Countable ↑{t | (f t).Nonempty}

Tactic:
have : ∀ t : {t // (f t).Nonempty}, ∃ x : s, x.1 ∈ f t := by
  rintro ⟨t, ⟨x, hx⟩⟩
  exact ⟨⟨x, (h'f t hx)⟩, hx⟩

Result:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
this : ∀ (t : { t // (f t).Nonempty }), ∃ x, ↑x ∈ f ↑t
⊢ Countable ↑{t | (f t).Nonempty}

Proof state:
case mk.mk
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
⊢ ⟨t, ht⟩ = ⟨t', ht'⟩

Tactic:
have A : (f t ∩ f t').Nonempty := by
  refine ⟨F ⟨t, ht⟩, hF ⟨t, _⟩, ?_⟩
  rw [htt']
  exact hF ⟨t', _⟩

Result:
case mk.mk
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
A : (f t ∩ f t').Nonempty
⊢ ⟨t, ht⟩ = ⟨t', ht'⟩

Proof state:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
this : ∀ (t : { t // (f t).Nonempty }), ∃ x, ↑x ∈ f ↑t
⊢ Countable ↑{t | (f t).Nonempty}

Tactic:
choose F hF using this

Result:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
⊢ Countable ↑{t | (f t).Nonempty}