awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
inst : CompleteLattice α
p : α → Prop
h : ∃ (x : α), p x
S : Set α
hSc : S.Countable
hps : ∀ s ∈ S, p s
hS : sSup S = ⊤
hne : S.Nonempty
s : ℕ → (↑S : Type u)
hs : Surjective s
mpr : Eq.{u + 1} (α := α) (⨆ (y : (↑S : Type u)), (↑y : α)) ⊤
mpr₁ mpr₂ mpr₃ mpr₄ : sSup S = ⊤
⊢ Eq.{u + 1} (α := α) (⨆ (n : ℕ), (fun (n : ℕ) ↦ (↑(s n) : α)) n) ⊤

Tactic:
rwa [hs.iSup_comp, ← sSup_eq_iSup']

Premises used: Function.Surjective.iSup_comp, sSup_eq_iSup'
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
p : Set α → Prop
h : ∃ (s : Set α), p s
⊢ (∃ (s : ℕ → Set α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := Set α) (⋃ (n : ℕ), s n) univ) ↔
    ∃ (S : Set (Set α)), S.Countable ∧ (∀ s ∈ S, p s) ∧ ⋃₀ S = univ

Tactic:
exists_seq_iSup_eq_top_iff_countable h

Premises used: Set.sUnion, Set.exists_seq_iSup_eq_top_iff_countable, Set.iUnion
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
s : Set α
f : α → β
hf : InjOn f s
hs : (f '' s).Countable
⊢ s.Countable

Tactic:
(mapsTo_image _ _).countable_of_injOn hf hs

Premises used: Set.MapsTo.countable_of_injOn, Set.mapsTo_image
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
ι : Sort x
t : ι → Set α
inst : Countable ι
ht : ∀ (i : ι), (t i).Countable
⊢ ∀ (i : ι), Countable.{u + 1} (↑(t i) : Type u)

Tactic:
have := fun i ↦ (ht i).to_subtype
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
ι : Sort x
t : ι → Set α
inst : Countable ι
ht : ∀ (i : ι), (t i).Countable
this : ∀ (i : ι), Countable.{u + 1} (↑(t i) : Type u)
rw :
  Set.Countable.{u} (α := α)
    (range fun (a : (i : ι) ×' (↑(t i) : Type u)) ↦ (↑(a.snd (β := fun (i : ι) ↦ (↑(t i) : Type u))) : α))
⊢ Set.Countable.{u} (α := α) (⋃ (i : ι), t i)

Tactic:
rw [iUnion_eq_range_psigma]

Premises used: Set.iUnion_eq_range_psigma
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
ι : Sort x
t : ι → Set α
inst : Countable ι
ht : ∀ (i : ι), (t i).Countable
this : ∀ (i : ι), Countable.{u + 1} (↑(t i) : Type u)
⊢ Set.Countable.{u} (α := α)
    (range fun (a : (i : ι) ×' (↑(t i) : Type u)) ↦ (↑(a.snd (β := fun (i : ι) ↦ (↑(t i) : Type u))) : α))

Tactic:
apply countable_range

Premises used: Set.countable_range
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
ι : Sort x
inst : Countable ι
t : ι → Set α
⊢ Set.Countable.{u} (α := α) (⋃ (i : ι), t i) ↔ ∀ (i : ι), (t i).Countable

Tactic:
⟨fun h _ => h.mono <| subset_iUnion _ _, countable_iUnion⟩

Premises used: Set.subset_iUnion, Set.countable_iUnion, Iff.intro, Set.Countable.mono
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
s : Set α
t : (a : α) → a ∈ s → Set β
hs : s.Countable
⊢ Countable.{u + 1} (↑s : Type u)

Tactic:
have := hs.to_subtype
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
s : Set α
t : (a : α) → a ∈ s → Set β
hs : s.Countable
this : Countable.{u + 1} (↑s : Type u)
rw : Set.Countable.{v} (α := β) (⋃ (x : (↑s : Type u)), t (↑x : α) ⋯) ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable
rw₁ : (∀ (i : (↑s : Type u)), (t (↑i : α) ⋯).Countable) ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable
rw₂ rw₃ : (∀ (i : (↑s : Type u)), (t (↑i : α) ⋯).Countable) ↔ ∀ (x : (↑s : Type u)), (t (↑x : α) ⋯).Countable
⊢ Set.Countable.{v} (α := β) (⋃ (a : α), ⋃ (h : a ∈ s), t a h) ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable

Tactic:
rw [biUnion_eq_iUnion, countable_iUnion_iff, SetCoe.forall']

Premises used: Set.biUnion_eq_iUnion, Set.countable_iUnion_iff, SetCoe.forall'
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set (Set α)
hs : s.Countable
rw : Set.Countable.{u} (α := α) (⋃ i ∈ s, i) ↔ ∀ a ∈ s, a.Countable
rw₁ rw₂ : (∀ (a : Set α) (ha : a ∈ s), a.Countable) ↔ ∀ a ∈ s, a.Countable
⊢ (⋃₀ s).Countable ↔ ∀ a ∈ s, a.Countable

Tactic:
rw [sUnion_eq_biUnion, hs.biUnion_iff]

Premises used: Set.sUnion_eq_biUnion, Set.Countable.biUnion_iff
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s t : Set α
⊢ (s ∪ t).Countable ↔ s.Countable ∧ t.Countable

Tactic:
simp [union_eq_iUnion, and_comm]

Premises used: and_comm, Set.union_eq_iUnion
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s t : Set α
hs : s.Countable
ht : t.Countable
⊢ (s ∪ t).Countable

Tactic:
countable_union.2 ⟨hs, ht⟩

Premises used: Iff.mpr, Set.countable_union, And.intro
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s t : Set α
h : (s \ t).Countable
ht : t.Countable
⊢ s.Countable

Tactic:
(h.union ht).mono (subset_diff_union _ _)

Premises used: Set.Countable.union, Set.Countable.mono, Set.subset_diff_union
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
a : α
⊢ (insert a s).Countable ↔ s.Countable

Tactic:
simp only [insert_eq, countable_union, countable_singleton, true_and]

Premises used: Set.insert_eq, Set.countable_union, Set.countable_singleton, true_and
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
a : α
h : s.Countable
⊢ (insert a s).Countable

Tactic:
countable_insert.2 h

Premises used: Iff.mpr, Set.countable_insert
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Finite
⊢ s.Countable

Tactic:
have := hs.to_subtype; s.to_countable

Premises used: Set.Finite.to_subtype, Set.to_countable
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
inst : Subsingleton α
s : Set α
⊢ s.Countable

Tactic:
(Finite.of_subsingleton s).countable

Premises used: Set.Finite.of_subsingleton, Set.Finite.countable
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Subsingleton
⊢ s.Countable

Tactic:
hs.finite.countable

Premises used: Set.Subsingleton.finite, Set.Finite.countable
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u_1
inst : PartialOrder α
⊢ Set.Countable.{u_1} (α := α) {x : α | IsTop x}

Tactic:
(finite_isTop α).countable

Premises used: Set.finite_isTop, Set.Finite.countable
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u_1
inst : PartialOrder α
⊢ Set.Countable.{u_1} (α := α) {x : α | IsBot x}

Tactic:
(finite_isBot α).countable

Premises used: Set.finite_isBot, Set.Finite.countable
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Countable
⊢ Countable.{u + 1} (↑s : Type u)

Tactic:
have := hs.to_subtype
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Countable
this : Countable.{u + 1} (↑s : Type u)
⊢ Set.Countable.{u} (α := Set α) {t : Set α | t.Finite ∧ t ⊆ s}

Tactic:
(countable_range fun t : Finset s => Subtype.val '' (t : Set s)).mono ?_

Premises used: Set.countable_range, SetLike.coe, Set.Countable.mono, Set.image, Subtype.val
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Countable
this : Countable.{u + 1} (↑s : Type u)
refine :
  Subset.{u} (α := Set (Set α)) {t : Set α | t.Finite ∧ t ⊆ s}
    (range fun (t : Finset (↑s : Type u)) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t : Set (↑s : Type u)))
⊢ Set.Countable.{u} (α := Set α) {t : Set α | t.Finite ∧ t ⊆ s}

Tactic:
refine (countable_range fun t : Finset s => Subtype.val '' (t : Set s)).mono ?_

Premises used: Set.countable_range, SetLike.coe, Set.Countable.mono, Set.image, Subtype.val
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Countable
this : Countable.{u + 1} (↑s : Type u)
t : Set α
ht : t.Finite
hts : t ⊆ s
⊢ ∀ x ∈ t, x ∈ s

Tactic:
hts

Premises used: Set.Subset
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Countable
this : Countable.{u + 1} (↑s : Type u)
t : Set α
ht : t.Finite
hts : t ⊆ s
lift :
  ∀ (t : Set (↑s : Type u)) (ht : (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t).Finite),
    Membership.mem (γ := Set (Set α))
      (range fun (t : Finset (↑s : Type u)) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t : Set (↑s : Type u)))
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
⊢ Membership.mem (γ := Set (Set α))
    (range fun (t : Finset (↑s : Type u)) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t : Set (↑s : Type u))) t

Tactic:
lift t to Set s using hts

Premises used: Set.Elem, Set
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Countable
this : Countable.{u + 1} (↑s : Type u)
t : Set (↑s : Type u)
ht : (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t).Finite
⊢ t.Finite

Tactic:
ht.of_finite_image Subtype.val_injective.injOn

Premises used: Subtype.val_injective, Function.Injective.injOn, Set.Finite.of_finite_image
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Countable
this : Countable.{u + 1} (↑s : Type u)
t : Set (↑s : Type u)
ht : (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t).Finite
lift :
  ∀ (t : Finset (↑s : Type u)) (ht : (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t : Set (↑s : Type u))).Finite),
    Membership.mem (γ := Set (Set α))
      (range fun (t : Finset (↑s : Type u)) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t : Set (↑s : Type u)))
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t : Set (↑s : Type u)))
⊢ Membership.mem (γ := Set (Set α))
    (range fun (t : Finset (↑s : Type u)) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t : Set (↑s : Type u)))
    (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)

Tactic:
lift t to Finset s using ht.of_finite_image Subtype.val_injective.injOn

Premises used: Subtype.val_injective, Function.Injective.injOn, Finset, Set.Elem, Set.Finite.of_finite_image
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Countable
this : Countable.{u + 1} (↑s : Type u)
t : Finset (↑s : Type u)
ht : (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t : Set (↑s : Type u))).Finite
⊢ Membership.mem (γ := Set (Set α))
    (range fun (t : Finset (↑s : Type u)) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t : Set (↑s : Type u)))
    (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t : Set (↑s : Type u)))

Tactic:
mem_range_self _

Premises used: Set.mem_range_self, Set.Mem
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Countable
this : Countable.{u + 1} (↑s : Type u)
t : Finset (↑s : Type u)
ht : (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t : Set (↑s : Type u))).Finite
⊢ Membership.mem (γ := Set (Set α))
    (range fun (t : Finset (↑s : Type u)) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t : Set (↑s : Type u)))
    (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t : Set (↑s : Type u)))

Tactic:
exact mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
inst : Countable α
⊢ Set.Countable.{u} (α := Set α) {s : Set α | s.Finite}

Tactic:
simpa using countable_setOf_finite_subset countable_univ

Premises used: Set.countable_univ, Set.countable_setOf_finite_subset
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : α → β
inst : Countable β
h : ∀ (b : β), (f ⁻¹' {b}).Countable
simp_rw : Set.Countable.{u} (α := α) univ
simp_rw₁ : (f ⁻¹' univ).Countable
simp_rw₂ : (f ⁻¹' ⋃ (x : β), {x}).Countable
simp_rw₃ : Set.Countable.{u} (α := α) (⋃ (i : β), f ⁻¹' {i})
⊢ Countable α

Tactic:
simp_rw [← Set.countable_univ_iff, ← Set.preimage_univ (f := f), ← Set.iUnion_of_singleton,
    Set.preimage_iUnion, Set.countable_iUnion h]

Premises used: Set.countable_iUnion, Set.countable_univ_iff, Set.preimage_univ, Set.preimage_iUnion, Set.iUnion_of_singleton
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
π : α → Type u_1
inst : Finite α
s : (a : α) → Set (π a)
hs : ∀ (a : α), (s a).Countable
⊢ (pi (α := π) univ s).Countable

Tactic:
have := fun a ↦ (hs a).to_subtype; .of_equiv _ (Equiv.Set.univPi s).symm

Premises used: Equiv.Set.univPi, Countable.of_equiv, Set.Countable.to_subtype, Equiv.symm, Set.Countable
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
π : α → Type u_1
inst : Finite α
s : (a : α) → Set (π a)
hs : ∀ (a : α), (s a).Countable
⊢ Set.Countable (α := (a : α) → π a) {f : (a : α) → π a | ∀ (a : α), f a ∈ s a}

Tactic:
simpa only [← mem_univ_pi] using countable_univ_pi hs

Premises used: Set.countable_univ_pi, Set.mem_univ_pi
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
s : Set α
t : Set β
hs : s.Countable
ht : t.Countable
⊢ (s ×ˢ t).Countable

Tactic:
have := hs.to_subtype; have := ht.to_subtype; .of_equiv _ <| (Equiv.Set.prod _ _).symm

Premises used: Countable.of_equiv, Set.Elem, Equiv.Set.prod, Set.Countable.to_subtype, Equiv.symm, Prod, Set.Countable
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
γ : Type w
s : Set α
t : Set β
hs : s.Countable
ht : t.Countable
f : α → β → γ
rw : Set.Countable.{w} (α := γ) ((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t)
⊢ (Set.image2 f s t).Countable

Tactic:
rw [← image_prod]

Premises used: Set.image_prod
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
γ : Type w
s : Set α
t : Set β
hs : s.Countable
ht : t.Countable
f : α → β → γ
⊢ Set.Countable.{w} (α := γ) ((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t)

Tactic:
(hs.prod ht).image _

Premises used: Set.Countable.prod, Set.Countable.image
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
γ : Type w
s : Set α
t : Set β
hs : s.Countable
ht : t.Countable
f : α → β → γ
⊢ Set.Countable.{w} (α := γ) ((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t)

Tactic:
exact (hs.prod ht).image _

Premises used: Set.Countable.prod, Set.Countable.image
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : s.Countable
⊢ Countable.{u + 1} (↑s : Type u)

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

Premises used: Set.countable_coe_iff
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
t : β
x : α
hx : x ∈ f t
⊢ ∃ (x_1 : (↑s : Type u)), (↑x_1 : α) ∈ f (↑(Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t ⋯) : β)

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

Premises used: Subtype.mk, Exists.intro
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
t : β
x : α
hx : x ∈ f t
⊢ ∃ (x_1 : (↑s : Type u)), (↑x_1 : α) ∈ f (↑(Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t ⋯) : β)

Tactic:
exact ⟨⟨x, (h'f t hx)⟩, hx⟩
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
⊢ ∀ (t : { t : β // (f t).Nonempty }), ∃ (x : (↑s : Type u)), (↑x : α) ∈ f (↑t : β)

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⟩
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
this : ∀ (t : { t : β // (f t).Nonempty }), ∃ (x : (↑s : Type u)), (↑x : α) ∈ f (↑t : β)
choose :
  ∀ (F : (t : { t : β // (f t).Nonempty }) → (↑s : Type u))
    (hF : ∀ (t : { t : β // (f t).Nonempty }), (↑(F t) : α) ∈ f (↑t : β)),
    Countable.{v + 1} (↑{t : β | (f t).Nonempty} : Type v)
⊢ Countable.{v + 1} (↑{t : β | (f t).Nonempty} : Type v)

Tactic:
choose F hF using this
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
F : (t : { t : β // (f t).Nonempty }) → (↑s : Type u)
hF : ∀ (t : { t : β // (f t).Nonempty }), (↑(F t) : α) ∈ f (↑t : β)
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' :
  F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t ht) = F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t' ht')
⊢ (f t ∩ f t').Nonempty

Tactic:
⟨F ⟨t, ht⟩, hF ⟨t, _⟩, ?_⟩

Premises used: Subtype.mk, Set.Nonempty, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
F : (t : { t : β // (f t).Nonempty }) → (↑s : Type u)
hF : ∀ (t : { t : β // (f t).Nonempty }), (↑(F t) : α) ∈ f (↑t : β)
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' :
  F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t ht) = F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t' ht')
refine : (↑(F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t ht)) : α) ∈ f t'
⊢ (f t ∩ f t').Nonempty

Tactic:
refine ⟨F ⟨t, ht⟩, hF ⟨t, _⟩, ?_⟩
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
F : (t : { t : β // (f t).Nonempty }) → (↑s : Type u)
hF : ∀ (t : { t : β // (f t).Nonempty }), (↑(F t) : α) ∈ f (↑t : β)
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' :
  F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t ht) = F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t' ht')
rw : (↑(F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t' ht')) : α) ∈ f t'
⊢ (↑(F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t ht)) : α) ∈ f t'

Tactic:
rw [htt']
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
F : (t : { t : β // (f t).Nonempty }) → (↑s : Type u)
hF : ∀ (t : { t : β // (f t).Nonempty }), (↑(F t) : α) ∈ f (↑t : β)
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' :
  F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t ht) = F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t' ht')
⊢ (↑(F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t' ht')) : α) ∈ f t'

Tactic:
hF ⟨t', _⟩

Premises used: Set.Mem, Subtype.mk
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
F : (t : { t : β // (f t).Nonempty }) → (↑s : Type u)
hF : ∀ (t : { t : β // (f t).Nonempty }), (↑(F t) : α) ∈ f (↑t : β)
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' :
  F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t ht) = F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t' ht')
⊢ (↑(F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t' ht')) : α) ∈ f t'

Tactic:
exact hF ⟨t', _⟩

Premises used: Subtype.mk
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
F : (t : { t : β // (f t).Nonempty }) → (↑s : Type u)
hF : ∀ (t : { t : β // (f t).Nonempty }), (↑(F t) : α) ∈ f (↑t : β)
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' :
  F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t ht) = F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t' ht')
⊢ (f t ∩ f t').Nonempty

Tactic:
have A : (f t ∩ f t').Nonempty := by
      refine ⟨F ⟨t, ht⟩, hF ⟨t, _⟩, ?_⟩
      rw [htt']
      exact hF ⟨t', _⟩
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
F : (t : { t : β // (f t).Nonempty }) → (↑s : Type u)
hF : ∀ (t : { t : β // (f t).Nonempty }), (↑(F t) : α) ∈ f (↑t : β)
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' :
  F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t ht) = F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t' ht')
A : (f t ∩ f t').Nonempty
simp : t = t'
⊢ Eq (α := { t : β // (f t).Nonempty }) (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t ht)
    (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t' ht')

Tactic:
simp only [Subtype.mk.injEq]

Premises used: Subtype.mk.injEq
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
F : (t : { t : β // (f t).Nonempty }) → (↑s : Type u)
hF : ∀ (t : { t : β // (f t).Nonempty }), (↑(F t) : α) ∈ f (↑t : β)
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' :
  F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t ht) = F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t' ht')
A : (f t ∩ f t').Nonempty
by_contra : ∀ (H : ¬t = t'), False
⊢ t = t'

Tactic:
by_contra H
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
F : (t : { t : β // (f t).Nonempty }) → (↑s : Type u)
hF : ∀ (t : { t : β // (f t).Nonempty }), (↑(F t) : α) ∈ f (↑t : β)
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' :
  F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t ht) = F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t' ht')
A : (f t ∩ f t').Nonempty
H : ¬t = t'
⊢ False

Tactic:
not_disjoint_iff_nonempty_inter.2 A (hf H)

Premises used: Iff.mpr, Set.not_disjoint_iff_nonempty_inter
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
F : (t : { t : β // (f t).Nonempty }) → (↑s : Type u)
hF : ∀ (t : { t : β // (f t).Nonempty }), (↑(F t) : α) ∈ f (↑t : β)
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' :
  F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t ht) = F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t' ht')
A : (f t ∩ f t').Nonempty
H : ¬t = t'
⊢ False

Tactic:
exact not_disjoint_iff_nonempty_inter.2 A (hf H)

Premises used: Iff.mpr, Set.not_disjoint_iff_nonempty_inter
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
F : (t : { t : β // (f t).Nonempty }) → (↑s : Type u)
hF : ∀ (t : { t : β // (f t).Nonempty }), (↑(F t) : α) ∈ f (↑t : β)
⊢ Injective F

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)
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
F : (t : { t : β // (f t).Nonempty }) → (↑s : Type u)
hF : ∀ (t : { t : β // (f t).Nonempty }), (↑(F t) : α) ∈ f (↑t : β)
A : Injective F
⊢ Countable.{v + 1} (↑{t : β | (f t).Nonempty} : Type v)

Tactic:
Injective.countable A

Premises used: Function.Injective.countable
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable.{u + 1} (↑s : Type u)
F : (t : { t : β // (f t).Nonempty }) → (↑s : Type u)
hF : ∀ (t : { t : β // (f t).Nonempty }), (↑(F t) : α) ∈ f (↑t : β)
A : Injective F
⊢ Countable.{v + 1} (↑{t : β | (f t).Nonempty} : Type v)

Tactic:
exact Injective.countable A

Premises used: Function.Injective.countable
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Finset α
⊢ (↑s : Set α).Countable

Tactic:
s.finite_toSet.countable

Premises used: Finset.finite_toSet, Set.Finite.countable
-- Module: Mathlib.Data.Set.Defs
Goal:
α : Type u
a b : Set α
h : ∀ (x : α), x ∈ a ↔ x ∈ b
⊢ a = b

Tactic:
funext (fun x ↦ propext (h x))

Premises used: funext, propext, Set
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s t : Set α
⊢ Disjoint s t ↔ s ∩ t ⊆ ∅

Tactic:
disjoint_iff_inf_le

Premises used: disjoint_iff_inf_le
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s t : Set α
⊢ Disjoint s t ↔ s ∩ t = ∅

Tactic:
disjoint_iff

Premises used: disjoint_iff
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s t : Set α
⊢ Disjoint s t → s ∩ t = ∅

Tactic:
Disjoint.eq_bot

Premises used: Disjoint.eq_bot
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s t : Set α
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t

Tactic:
disjoint_iff_inf_le.trans <| forall_congr' fun _ => not_and

Premises used: forall_congr', Iff.trans, disjoint_iff_inf_le, not_and
-- Module: Mathlib.Data.Set.Disjoint
Goal:
α : Type u
s t : Set α
rw : Disjoint t s ↔ ∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s
rw₁ rw₂ : (∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s) ↔ ∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s

Tactic:
rw [disjoint_comm, disjoint_left]

Premises used: Set.disjoint_left, disjoint_comm