awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 : Set α
h_1 : finiteInterClosure (insert A S) T1
h : T1 ∈ S
R : Set α
hR : R ∈ S
h_2 : finiteInterClosure (insert A S) (A ∩ R)
⊢ T1 ∩ (A ∩ R) ∈ S ∨ ∃ Q ∈ S, T1 ∩ (A ∩ R) = A ∩ Q

Tactic:
exact
        Or.inr ⟨T1 ∩ R, cond.inter_mem h hR, by simp only [← Set.inter_assoc, Set.inter_comm _ A]⟩

Premises used: Or.inr
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T2 : Set α
h : finiteInterClosure (insert A S) T2
Q : Set α
hQ : Q ∈ S
h_1 : finiteInterClosure (insert A S) (A ∩ Q)
i : T2 ∈ S
⊢ A ∩ Q ∩ T2 = A ∩ (Q ∩ T2)

Tactic:
simp only [Set.inter_assoc]

Premises used: Set.inter_assoc
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T2 : Set α
h : finiteInterClosure (insert A S) T2
Q : Set α
hQ : Q ∈ S
h_1 : finiteInterClosure (insert A S) (A ∩ Q)
i : T2 ∈ S
⊢ A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ T2 = A ∩ Q_1

Tactic:
exact Or.inr ⟨Q ∩ T2, cond.inter_mem hQ i, by simp only [Set.inter_assoc]⟩

Premises used: Or.inr
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
h_1 : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
h_2 : finiteInterClosure (insert A S) (A ∩ R)
h : ∀ (x : α), x ∈ A ∩ Q ∩ (A ∩ R) ↔ x ∈ A ∩ (Q ∩ R)
⊢ A ∩ Q ∩ (A ∩ R) = A ∩ (Q ∩ R)

Tactic:
ext x
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
h_1 : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
h_2 : finiteInterClosure (insert A S) (A ∩ R)
x : α
h : x ∈ A ∩ Q ∩ (A ∩ R) → x ∈ A ∩ (Q ∩ R)
h₁ : x ∈ A ∩ (Q ∩ R) → x ∈ A ∩ Q ∩ (A ∩ R)
⊢ x ∈ A ∩ Q ∩ (A ∩ R) ↔ x ∈ A ∩ (Q ∩ R)

Tactic:
constructor
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
h : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
h_1 : finiteInterClosure (insert A S) (A ∩ R)
x : α
⊢ x ∈ A ∩ Q ∩ (A ∩ R) → x ∈ A ∩ (Q ∩ R)

Tactic:
simp +contextual
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
h : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
h_1 : finiteInterClosure (insert A S) (A ∩ R)
x : α
⊢ x ∈ A ∩ (Q ∩ R) → x ∈ A ∩ Q ∩ (A ∩ R)

Tactic:
simp +contextual
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
h : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
h_1 : finiteInterClosure (insert A S) (A ∩ R)
⊢ A ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ (A ∩ R) = A ∩ Q_1

Tactic:
exact
        Or.inr
          ⟨Q ∩ R, cond.inter_mem hQ hR, by
            ext x
            constructor <;> simp +contextual⟩

Premises used: Or.inr
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P : Set α
H : P ∈ finiteInterClosure (insert A S)
basic : ∀ {s : Set α} (h : s ∈ insert A S), s ∈ S ∨ ∃ Q ∈ S, s = A ∩ Q
univ : Set.univ ∈ S ∨ ∃ Q ∈ S, Set.univ = A ∩ Q
inter :
  ∀ {T1 T2 : Set α},
    finiteInterClosure (insert A S) T1 →
      finiteInterClosure (insert A S) T2 →
        ∀ (h1 : T1 ∈ S ∨ ∃ Q ∈ S, T1 = A ∩ Q) (h2 : T2 ∈ S ∨ ∃ Q ∈ S, T2 = A ∩ Q),
          T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q
⊢ P ∈ S ∨ ∃ Q ∈ S, P = A ∩ Q

Tactic:
induction H with
  | basic h =>
    cases h
    · exact Or.inr ⟨Set.univ, cond.univ_mem, by simpa⟩
    · exact Or.inl (by assumption)
  | univ => exact Or.inl cond.univ_mem
  | @inter T1 T2 _ _ h1 h2 =>
    rcases h1 with (h | ⟨Q, hQ, rfl⟩) <;> rcases h2 with (i | ⟨R, hR, rfl⟩)
    · exact Or.inl (cond.inter_mem h i)
    · exact
        Or.inr ⟨T1 ∩ R, cond.inter_mem h hR, by simp only [← Set.inter_assoc, Set.inter_comm _ A]⟩
    · exact Or.inr ⟨Q ∩ T2, cond.inter_mem hQ i, by simp only [Set.inter_assoc]⟩
    · exact
        Or.inr
          ⟨Q ∩ R, cond.inter_mem hQ hR, by
            ext x
            constructor <;> simp +contextual⟩

Premises used: Or.inl, Or.inr, rfl, FiniteInter.univ_mem
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
h : ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S
s : Set α
hs : s ∈ insert univ S
t : Set α
ht : t ∈ insert univ S
⊢ s ∩ t ∈ insert univ S

Tactic:
aesop
-- Module: Mathlib.Data.Set.Constructions
Goal:
ι : Type u_2
X : Type u_3
s : ι → Set X
⊢ Eq.{u_3 + 1} (α := Set X) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i) ∅

Tactic:
simp
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
⊢ Countable.{u + 1} (↑s : Type u) ↔ s.Countable

Tactic:
.rfl

Premises used: Iff.rfl, Set.Countable
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
⊢ s.Countable ↔ ∃ (f : (↑s : Type u) → ℕ), Injective f

Tactic:
countable_iff_exists_injective s

Premises used: countable_iff_exists_injective, Set.Elem, Set.Countable
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
⊢ s.Countable ↔ ∃ (f : α → ℕ), InjOn f s

Tactic:
Set.countable_iff_exists_injective.trans exists_injOn_iff_injective.symm

Premises used: Set.countable_iff_exists_injective, Iff.trans, Iff.symm, Set.exists_injOn_iff_injective
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
⊢ s.Countable ↔ Nonempty.{u + 1} (Encodable (↑s : Type u))

Tactic:
Encodable.nonempty_encodable.symm

Premises used: Encodable.nonempty_encodable, Set.Countable, Iff.symm
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
h : s.Countable
default x : α
hx : x ∈ s
⊢ enumerateCountable (s := s) h default (encode (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) = x

Tactic:
simp [enumerateCountable, Encodable.encodek]

Premises used: Set.enumerateCountable, Encodable.encodek
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
h : s.Countable
default : α
⊢ range (enumerateCountable (s := s) h default) ⊆ insert default s

Tactic:
range_subset_iff.mpr (fun n ↦ ?_)

Premises used: Iff.mpr, Set.range_subset_iff
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
h : s.Countable
default : α
refine : ∀ (n : ℕ), enumerateCountable (s := s) h default n ∈ insert default s
⊢ range (enumerateCountable (s := s) h default) ⊆ insert default s

Tactic:
refine range_subset_iff.mpr (fun n ↦ ?_)

Premises used: Iff.mpr, Set.range_subset_iff
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
rw :
  Membership.mem (α := α) (insert default s)
    (match (motive := Option (↑s : Type u) → α) decode n with
      | some y => (↑y : α)
      | none => default :
      α)
⊢ enumerateCountable (s := s) h default n ∈ insert default s

Tactic:
rw [enumerateCountable]

Premises used: Set.enumerateCountable
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ Membership.mem (α := α) (insert default s)
    (match (motive := Option (↑s : Type u) → α) none with
      | some y => (↑y : α)
      | none => default :
      α)

Tactic:
mem_insert _ _

Premises used: Set.Mem, Set.mem_insert
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ Membership.mem (α := α) (insert default s)
    (match (motive := Option (↑s : Type u) → α) none with
      | some y => (↑y : α)
      | none => default :
      α)

Tactic:
exact mem_insert _ _

Premises used: Set.mem_insert
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
val : (↑s : Type u)
⊢ Membership.mem (α := α) (insert default s)
    (match (motive := Option (↑s : Type u) → α) some val with
      | some y => (↑y : α)
      | none => default :
      α)

Tactic:
simp
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ Membership.mem (α := α) (insert default s)
    (match (motive := Option (↑s : Type u) → α) decode n with
      | some y => (↑y : α)
      | none => default :
      α)

Tactic:
match @decode s (Countable.toEncodable h) n with
  | none => exact mem_insert _ _
  | some val => simp
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
h : s.Countable
default : α
h_mem : default ∈ s
⊢ range (enumerateCountable (s := s) h default) = s

Tactic:
subset_antisymm ((range_enumerateCountable_subset h _).trans_eq (insert_eq_of_mem h_mem))
    (subset_range_enumerate h default)

Premises used: LE.le.trans_eq, Set.subset_range_enumerate, Set.insert_eq_of_mem, subset_antisymm, Set.range_enumerateCountable_subset
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
h : s.Countable
default : α
h_mem : default ∈ s
n : ℕ
⊢ enumerateCountable (s := s) h default n ∈ range (enumerateCountable (s := s) h default)

Tactic:
mem_range_self n

Premises used: Set.mem_range_self
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
h : s.Countable
default : α
h_mem : default ∈ s
n : ℕ
h₁ : s = range (enumerateCountable (s := s) h default)
⊢ enumerateCountable (s := s) h default n ∈ s

Tactic:
convert! mem_range_self n

Premises used: Set.mem_range_self
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
h : s.Countable
default : α
h_mem : default ∈ s
n : ℕ
⊢ s = range (enumerateCountable (s := s) h default)

Tactic:
(range_enumerateCountable_of_mem h h_mem).symm

Premises used: Set.range_enumerateCountable_of_mem, Eq.symm
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
h : s.Countable
default : α
h_mem : default ∈ s
n : ℕ
⊢ s = range (enumerateCountable (s := s) h default)

Tactic:
exact (range_enumerateCountable_of_mem h h_mem).symm

Premises used: Set.range_enumerateCountable_of_mem, Eq.symm
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s₁ s₂ : Set α
h : s₁ ⊆ s₂
hs : s₂.Countable
⊢ s₁.Countable

Tactic:
have := hs.to_subtype; (inclusion_injective h).countable

Premises used: Function.Injective.countable, Set.inclusion_injective, Set.Countable.to_subtype, Set.Countable
-- Module: Mathlib.Data.Set.Countable
Goal:
β : Type v
ι : Sort x
inst : Countable ι
f : ι → β
⊢ (range f).Countable

Tactic:
rangeFactorization_surjective.countable.to_set

Premises used: Function.Surjective.countable, Countable.to_set, Set.rangeFactorization_surjective
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
inst : Nonempty α
s : Set α
h : s.Countable
inhabit : ∀ (inhabited_h : Inhabited α), ∃ (f : ℕ → α), s ⊆ range f
⊢ ∃ (f : ℕ → α), s ⊆ range f

Tactic:
inhabit α
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
inst : Nonempty α
s : Set α
h : s.Countable
inhabited_h : Inhabited α
⊢ ∃ (f : ℕ → α), s ⊆ range f

Tactic:
⟨enumerateCountable h default, subset_range_enumerate _ _⟩

Premises used: Inhabited.default, Set.subset_range_enumerate, Set.enumerateCountable, Exists.intro
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
inst : Nonempty α
s : Set α
h : s.Countable
inhabited_h : Inhabited α
⊢ ∃ (f : ℕ → α), s ⊆ range f

Tactic:
exact ⟨enumerateCountable h default, subset_range_enumerate _ _⟩
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Nonempty
⊢ s.Countable ↔ ∃ (f : ℕ → (↑s : Type u)), Surjective f

Tactic:
@countable_iff_exists_surjective s hs.to_subtype

Premises used: countable_iff_exists_surjective, Set.Countable
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
⊢ Set.Countable.{u} (α := α) univ ↔ Countable α

Tactic:
countable_coe_iff.symm.trans (Equiv.Set.univ _).countable_iff

Premises used: Set.countable_coe_iff, Equiv.countable_iff, Iff.trans, Iff.symm, Equiv.Set.univ
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
inst : Countable α
⊢ Set.Countable.{u} (α := α) univ

Tactic:
to_countable univ

Premises used: Set.univ, Set.to_countable
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
rw : ¬Countable α ↔ Uncountable α
rw₁ rw₂ : Uncountable α ↔ Uncountable α
⊢ ¬Set.Countable.{u} (α := α) univ ↔ Uncountable α

Tactic:
rw [countable_univ_iff, not_countable_iff]

Premises used: Set.countable_univ_iff, not_countable_iff
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
inst : Uncountable α
⊢ ¬Set.Countable.{u} (α := α) univ

Tactic:
not_countable_univ_iff.2 ‹_›

Premises used: Iff.mpr, Set.not_countable_univ_iff
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
rcases : ∀ (f : ℕ → (↑s : Type u)) (hf : Surjective f), ∃ (f : ℕ → α), s = range f
⊢ ∃ (f : ℕ → α), s = range f

Tactic:
rcases hc.exists_surjective hs with ⟨f, hf⟩

Premises used: Set.Countable.exists_surjective
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
f : ℕ → (↑s : Type u)
hf : Surjective f
⊢ ∃ (f : ℕ → α), s = range f

Tactic:
⟨(↑) ∘ f, ?_⟩

Premises used: Function.comp, Exists.intro
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
f : ℕ → (↑s : Type u)
hf : Surjective f
refine : s = range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f)
⊢ ∃ (f : ℕ → α), s = range f

Tactic:
refine ⟨(↑) ∘ f, ?_⟩
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
f : ℕ → (↑s : Type u)
hf : Surjective f
rw : s = range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
rw₁ rw₂ : s = s
⊢ s = range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f)

Tactic:
rw [hf.range_comp, Subtype.range_coe]

Premises used: Function.Surjective.range_comp, Subtype.range_coe
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
⊢ Set.Countable.{u} (α := α) ∅

Tactic:
to_countable _

Premises used: Set.to_countable
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
a : α
⊢ Set.Countable (α := α) {a}

Tactic:
to_countable _

Premises used: Set.to_countable
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
s : Set α
hs : s.Countable
f : α → β
rw : Set.Countable.{v} (α := β) (range fun (x : (↑s : Type u)) ↦ f (↑x : α))
⊢ (f '' s).Countable

Tactic:
rw [image_eq_range]

Premises used: Set.image_eq_range
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
s : Set α
hs : s.Countable
f : α → β
⊢ Countable.{u + 1} (↑s : Type u)

Tactic:
have := hs.to_subtype
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
s : Set α
hs : s.Countable
f : α → β
this : Countable.{u + 1} (↑s : Type u)
⊢ Set.Countable.{v} (α := β) (range fun (x : (↑s : Type u)) ↦ f (↑x : α))

Tactic:
apply countable_range

Premises used: Set.countable_range
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Infinite
obtain : ∀ (f : ℕ → (↑s : Type u)) (hf : Injective f), ∃ t ⊆ s, t.Countable ∧ t.Infinite
⊢ ∃ t ⊆ s, t.Countable ∧ t.Infinite

Tactic:
obtain ⟨f, hf⟩ := Infinite.natEmbedding s hs

Premises used: Set.Infinite.natEmbedding
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → (↑s : Type u)
hf : Injective f
⊢ ∃ t ⊆ s, t.Countable ∧ t.Infinite

Tactic:
⟨range (Subtype.val ∘ f), ?_, ?_, ?_⟩

Premises used: Function.comp, And.intro, Exists.intro, Set.range, Subtype.val
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → (↑s : Type u)
hf : Injective f
refine_1 : range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f) ⊆ s
refine_2 : (range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f)).Countable
refine_3 : (range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f)).Infinite
⊢ ∃ t ⊆ s, t.Countable ∧ t.Infinite

Tactic:
refine ⟨range (Subtype.val ∘ f), ?_, ?_, ?_⟩
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → (↑s : Type u)
hf : Injective f
⊢ range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f) ⊆ s

Tactic:
fun _ ⟨y, hy⟩ ↦ hy ▸ Subtype.coe_prop (f y)

Premises used: Subtype.coe_prop, Membership.mem, Eq.rec, _private.0.Set.Infinite.exists_subset_countable_infinite.match_1, Set.Subset
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → (↑s : Type u)
hf : Injective f
⊢ range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f) ⊆ s

Tactic:
exact fun _ ⟨y, hy⟩ ↦ hy ▸ Subtype.coe_prop (f y)
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → (↑s : Type u)
hf : Injective f
⊢ (range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f)).Countable

Tactic:
countable_range (Subtype.val ∘ f)

Premises used: Function.comp, Set.countable_range, Subtype.val
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → (↑s : Type u)
hf : Injective f
⊢ (range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f)).Countable

Tactic:
exact countable_range (Subtype.val ∘ f)

Premises used: Function.comp, Set.countable_range, Subtype.val
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → (↑s : Type u)
hf : Injective f
⊢ (range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f)).Infinite

Tactic:
infinite_range_of_injective <| Injective.comp Subtype.val_injective hf

Premises used: Set.infinite_range_of_injective, Subtype.val_injective, Function.Injective.comp
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → (↑s : Type u)
hf : Injective f
⊢ (range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f)).Infinite

Tactic:
exact infinite_range_of_injective <| Injective.comp Subtype.val_injective hf

Premises used: Set.infinite_range_of_injective, Subtype.val_injective, Function.Injective.comp
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
hf' : InjOn f s
ht : t.Countable
⊢ s.Countable

Tactic:
have := ht.to_subtype
  have : Injective (hf.restrict f s t) := (injOn_iff_injective.1 hf').codRestrict _
  this.countable

Premises used: Function.Injective.countable, Function.Injective.codRestrict, Set.injOn_iff_injective, Subtype.map._proof_1, Iff.mp, Set.Countable.to_subtype, Set.Countable
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
s : Set β
hs : s.Countable
f : α → β
hf : InjOn f (f ⁻¹' s)
⊢ (f ⁻¹' s).Countable

Tactic:
(mapsTo_preimage f s).countable_of_injOn hf hs

Premises used: Set.MapsTo.countable_of_injOn, Set.mapsTo_preimage
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
β : Type v
s : Set β
hs : s.Countable
f : α → β
hf : Injective f
⊢ (f ⁻¹' s).Countable

Tactic:
hs.preimage_of_injOn hf.injOn

Premises used: Function.Injective.injOn, Set.Countable.preimage_of_injOn
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
inst : CompleteLattice α
p : α → Prop
h : ∃ (x : α), p x
mp :
  (∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤) →
    ∃ (S : Set α), S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤
mpr :
  (∃ (S : Set α), S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤) →
    ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
⊢ (∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤) ↔
    ∃ (S : Set α), S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤

Tactic:
constructor
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
inst : CompleteLattice α
p : α → Prop
h : ∃ (x : α), p x
s : ℕ → α
hps : ∀ (n : ℕ), p (s n)
hs : Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
⊢ ∃ (S : Set α), S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤

Tactic:
⟨range s, countable_range s, forall_mem_range.2 hps, ?_⟩

Premises used: Iff.mpr, Set.forall_mem_range, Set.countable_range, And.intro, Exists.intro, Set.range
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
inst : CompleteLattice α
p : α → Prop
h : ∃ (x : α), p x
s : ℕ → α
hps : ∀ (n : ℕ), p (s n)
hs : Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
mp : sSup (range s) = ⊤
⊢ ∃ (S : Set α), S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤

Tactic:
refine ⟨range s, countable_range s, forall_mem_range.2 hps, ?_⟩
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
inst : CompleteLattice α
p : α → Prop
h : ∃ (x : α), p x
s : ℕ → α
hps : ∀ (n : ℕ), p (s n)
hs : Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
mp mp₁ mp₂ mp₃ : iSup s = ⊤
⊢ sSup (range s) = ⊤

Tactic:
rwa [sSup_range]

Premises used: sSup_range
-- 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 = ⊤
mpr :
  ∀ (hSc : Set.Countable.{u} (α := α) ∅) (hps : ∀ (s : α), Membership.mem (γ := Set α) ∅ s → p s)
    (hS : Eq.{u + 1} (α := α) (sSup ∅) ⊤), ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
mpr₁ : ∀ (hne : S.Nonempty), ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
⊢ ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤

Tactic:
rcases eq_empty_or_nonempty S with (rfl | hne)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
inst : CompleteLattice α
p : α → Prop
h : ∃ (x : α), p x
hSc : Set.Countable.{u} (α := α) ∅
hps : ∀ (s : α), Membership.mem (γ := Set α) ∅ s → p s
hS : Eq.{u + 1} (α := α) (sSup ∅) ⊤
⊢ Eq.{u + 1} (α := α) ⊥ ⊤

Tactic:
rw [sSup_empty] at hS

Premises used: sSup_empty
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
inst : CompleteLattice α
p : α → Prop
h : ∃ (x : α), p x
hSc : Set.Countable.{u} (α := α) ∅
hps : ∀ (s : α), Membership.mem (γ := Set α) ∅ s → p s
hS : Eq.{u + 1} (α := α) ⊥ ⊤
⊢ Subsingleton α

Tactic:
haveI := subsingleton_of_bot_eq_top hS
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
inst : CompleteLattice α
p : α → Prop
h : ∃ (x : α), p x
hSc : Set.Countable.{u} (α := α) ∅
hps : ∀ (s : α), Membership.mem (γ := Set α) ∅ s → p s
hS : Eq.{u + 1} (α := α) ⊥ ⊤
this : Subsingleton α
mpr : ∀ (x : α) (hx : p x), ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
⊢ ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤

Tactic:
rcases h with ⟨x, hx⟩
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
inst : CompleteLattice α
p : α → Prop
hSc : Set.Countable.{u} (α := α) ∅
hps : ∀ (s : α), Membership.mem (γ := Set α) ∅ s → p s
hS : Eq.{u + 1} (α := α) ⊥ ⊤
this : Subsingleton α
x : α
hx : p x
⊢ ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤

Tactic:
⟨fun _ => x, fun _ => hx, Subsingleton.elim _ _⟩

Premises used: And.intro, Exists.intro, Subsingleton.elim
-- Module: Mathlib.Data.Set.Countable
Goal:
α : Type u
inst : CompleteLattice α
p : α → Prop
hSc : Set.Countable.{u} (α := α) ∅
hps : ∀ (s : α), Membership.mem (γ := Set α) ∅ s → p s
hS : Eq.{u + 1} (α := α) ⊥ ⊤
this : Subsingleton α
x : α
hx : p x
⊢ ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤

Tactic:
exact ⟨fun _ => x, fun _ => hx, Subsingleton.elim _ _⟩
-- 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
mpr :
  ∀ (s : ℕ → (↑S : Type u)) (hs : Surjective s),
    ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
⊢ ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤

Tactic:
rcases (Set.countable_iff_exists_surjective hne).1 hSc with ⟨s, hs⟩

Premises used: Set.countable_iff_exists_surjective, Iff.mp
-- 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
⊢ ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤

Tactic:
⟨fun n => s n, fun n => hps _ (s n).coe_prop, ?_⟩

Premises used: Subtype.coe_prop, And.intro, Exists.intro, Subtype.val
-- 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} (α := α) (⨆ (n : ℕ), (fun (n : ℕ) ↦ (↑(s n) : α)) n) ⊤
⊢ ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤

Tactic:
refine ⟨fun n => s n, fun n => hps _ (s n).coe_prop, ?_⟩