awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
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
⊢ P ∈ S ∨ ∃ Q ∈ S, P = A ∩ Q
have 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
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⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
s : Set α
h : s.Countable
default : α
⊢ range (enumerateCountable (s := s) h default) ⊆ insert default s
have refine : ∀ (n : ℕ), enumerateCountable (s := s) h default n ∈ insert default s
Tactic: refine range_subset_iff.mpr (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ enumerateCountable (s := s) h default n ∈ insert default s
have rw : Membership.mem (α := α) (insert default s)
  (match (motive := Option (↑s : Type u) → α) decode n with
    | some y => (↑y : α)
    | none => default :
    α)
Tactic: rw [enumerateCountable]
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
s : Set α
h : s.Countable
default : α
h_mem : default ∈ s
n : ℕ
⊢ enumerateCountable (s := s) h default n ∈ s
have h₁ : s = range (enumerateCountable (s := s) h default)
Tactic: convert! mem_range_self n
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
inst : Nonempty α
s : Set α
h : s.Countable
⊢ ∃ (f : ℕ → α), s ⊆ range f
have inhabit : ∀ (inhabited_h : Inhabited α), ∃ (f : ℕ → α), s ⊆ range f
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
⊢ ¬Set.Countable.{u} (α := α) univ ↔ Uncountable α
have rw : ¬Countable α ↔ Uncountable α
Tactic: rw [countable_univ_iff, not_countable_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
rw : ¬Countable α ↔ Uncountable α
⊢ ¬Set.Countable.{u} (α := α) univ ↔ Uncountable α
have rw₁ : Uncountable α ↔ Uncountable α
Tactic: rw [countable_univ_iff, not_countable_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
⊢ ∃ (f : ℕ → α), s = range f
have rcases : ∀ (f : ℕ → (↑s : Type u)) (hf : Surjective f), ∃ (f : ℕ → α), s = range f
Tactic: rcases hc.exists_surjective hs with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
f : ℕ → (↑s : Type u)
hf : Surjective f
⊢ ∃ (f : ℕ → α), s = range f
have refine : s = range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f)
Tactic: refine ⟨(↑) ∘ f, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
f : ℕ → (↑s : Type u)
hf : Surjective f
⊢ s = range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f)
have rw : s = range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
Tactic: rw [hf.range_comp, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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))
⊢ s = range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f)
have rw₁ : s = s
Tactic: rw [hf.range_comp, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
β : Type v
s : Set α
hs : s.Countable
f : α → β
⊢ (f '' s).Countable
have rw : Set.Countable.{v} (α := β) (range fun (x : (↑s : Type u)) ↦ f (↑x : α))
Tactic: rw [image_eq_range]
-- Lean 4 proof step from Mathlib.Data.Set.Countable (hypothesis)
Goal:
α : Type u
β : Type v
s : Set α
hs : s.Countable
f : α → β
⊢ Set.Countable.{v} (α := β) (range fun (x : (↑s : Type u)) ↦ f (↑x : α))
have this : Countable.{u + 1} (↑s : Type u)
Tactic: have := hs.to_subtype
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
s : Set α
hs : s.Infinite
⊢ ∃ t ⊆ s, t.Countable ∧ t.Infinite
have obtain : ∀ (f : ℕ → (↑s : Type u)) (hf : Injective f), ∃ t ⊆ s, t.Countable ∧ t.Infinite
Tactic: obtain ⟨f, hf⟩ := Infinite.natEmbedding s hs
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → (↑s : Type u)
hf : Injective f
⊢ ∃ t ⊆ s, t.Countable ∧ t.Infinite
have refine_1 : range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f) ⊆ s
Tactic: refine ⟨range (Subtype.val ∘ f), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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
⊢ ∃ t ⊆ s, t.Countable ∧ t.Infinite
have refine_2 : (range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f)).Countable
Tactic: refine ⟨range (Subtype.val ∘ f), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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
⊢ ∃ t ⊆ s, t.Countable ∧ t.Infinite
have refine_3 : (range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f)).Infinite
Tactic: refine ⟨range (Subtype.val ∘ f), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
inst : CompleteLattice α
p : α → Prop
h : ∃ (x : α), p x
⊢ (∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤) ↔
    ∃ (S : Set α), S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤
have mp : (∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤) →
  ∃ (S : Set α), S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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 = ⊤
⊢ (∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤) ↔
    ∃ (S : Set α), S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤
have mpr : (∃ (S : Set α), S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤) →
  ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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 = ⊤
have mp : sSup (range s) = ⊤
Tactic: refine ⟨range s, countable_range s, forall_mem_range.2 hps, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
inst : CompleteLattice α
p : α → Prop
h : ∃ (x : α), p x
S : Set α
hSc : S.Countable
hps : ∀ s ∈ S, p s
hS : sSup S = ⊤
⊢ ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
have 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) ⊤
Tactic: rcases eq_empty_or_nonempty S with (rfl | hne)
Cleared hypotheses: S, hSc, hps, hS
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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) ⊤
⊢ ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
have mpr₁ : ∀ (hne : S.Nonempty), ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
Tactic: rcases eq_empty_or_nonempty S with (rfl | hne)
-- Lean 4 proof step from Mathlib.Data.Set.Countable (hypothesis)
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 ∅) ⊤
⊢ ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
have hS₁ : Eq.{u + 1} (α := α) ⊥ ⊤
Tactic: rw [sSup_empty] at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Data.Set.Countable (hypothesis)
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} (α := α) ⊥ ⊤
⊢ ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
have this : Subsingleton α
Tactic: haveI := subsingleton_of_bot_eq_top hS
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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 α
⊢ ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
have mpr : ∀ (x : α) (hx : p x), ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
Tactic: rcases h with ⟨x, hx⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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 : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
have mpr : ∀ (s : ℕ → (↑S : Type u)) (hs : Surjective s),
  ∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ Eq.{u + 1} (α := α) (⨆ (n : ℕ), s n) ⊤
Tactic: rcases (Set.countable_iff_exists_surjective hne).1 hSc with ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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) ⊤
have mpr : Eq.{u + 1} (α := α) (⨆ (n : ℕ), (fun (n : ℕ) ↦ (↑(s n) : α)) n) ⊤
Tactic: refine ⟨fun n => s n, fun n => hps _ (s n).coe_prop, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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
⊢ Eq.{u + 1} (α := α) (⨆ (n : ℕ), (fun (n : ℕ) ↦ (↑(s n) : α)) n) ⊤
have mpr : Eq.{u + 1} (α := α) (⨆ (y : (↑S : Type u)), (↑y : α)) ⊤
Tactic: rwa [hs.iSup_comp, ← sSup_eq_iSup']
-- Lean 4 proof step from Mathlib.Data.Set.Countable (hypothesis)
Goal:
α : Type u
ι : Sort x
t : ι → Set α
inst : Countable ι
ht : ∀ (i : ι), (t i).Countable
⊢ Set.Countable.{u} (α := α) (⋃ (i : ι), t i)
have this : ∀ (i : ι), Countable.{u + 1} (↑(t i) : Type u)
Tactic: have := fun i ↦ (ht i).to_subtype
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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} (α := α) (⋃ (i : ι), t i)
have rw : Set.Countable.{u} (α := α)
  (range fun (a : (i : ι) ×' (↑(t i) : Type u)) ↦ (↑(a.snd (β := fun (i : ι) ↦ (↑(t i) : Type u))) : α))
Tactic: rw [iUnion_eq_range_psigma]
-- Lean 4 proof step from Mathlib.Data.Set.Countable (hypothesis)
Goal:
α : Type u
β : Type v
s : Set α
t : (a : α) → a ∈ s → Set β
hs : s.Countable
⊢ Set.Countable.{v} (α := β) (⋃ (a : α), ⋃ (h : a ∈ s), t a h) ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable
have this : Countable.{u + 1} (↑s : Type u)
Tactic: have := hs.to_subtype
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
β : Type v
s : Set α
t : (a : α) → a ∈ s → Set β
hs : s.Countable
this : Countable.{u + 1} (↑s : Type u)
⊢ Set.Countable.{v} (α := β) (⋃ (a : α), ⋃ (h : a ∈ s), t a h) ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable
have rw : Set.Countable.{v} (α := β) (⋃ (x : (↑s : Type u)), t (↑x : α) sorry) ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable
Tactic: rw [biUnion_eq_iUnion, countable_iUnion_iff, SetCoe.forall']
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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
⊢ Set.Countable.{v} (α := β) (⋃ (a : α), ⋃ (h : a ∈ s), t a h) ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable
have rw₁ : (∀ (i : (↑s : Type u)), (t (↑i : α) sorry).Countable) ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable
Tactic: rw [biUnion_eq_iUnion, countable_iUnion_iff, SetCoe.forall']
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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
⊢ Set.Countable.{v} (α := β) (⋃ (a : α), ⋃ (h : a ∈ s), t a h) ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable
have rw₂ : (∀ (i : (↑s : Type u)), (t (↑i : α) sorry).Countable) ↔ ∀ (x : (↑s : Type u)), (t (↑x : α) sorry).Countable
Tactic: rw [biUnion_eq_iUnion, countable_iUnion_iff, SetCoe.forall']
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
s : Set (Set α)
hs : s.Countable
⊢ (⋃₀ s).Countable ↔ ∀ a ∈ s, a.Countable
have rw : Set.Countable.{u} (α := α) (⋃ i ∈ s, i) ↔ ∀ a ∈ s, a.Countable
Tactic: rw [sUnion_eq_biUnion, hs.biUnion_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
s : Set (Set α)
hs : s.Countable
rw : Set.Countable.{u} (α := α) (⋃ i ∈ s, i) ↔ ∀ a ∈ s, a.Countable
⊢ (⋃₀ s).Countable ↔ ∀ a ∈ s, a.Countable
have rw₁ : (∀ (a : Set α) (ha : a ∈ s), a.Countable) ↔ ∀ a ∈ s, a.Countable
Tactic: rw [sUnion_eq_biUnion, hs.biUnion_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Countable (hypothesis)
Goal:
α : Type u
s : Set α
hs : s.Countable
⊢ Set.Countable.{u} (α := Set α) {t : Set α | t.Finite ∧ t ⊆ s}
have this : Countable.{u + 1} (↑s : Type u)
Tactic: have := hs.to_subtype
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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}
have 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)))
Tactic: refine (countable_range fun t : Finset s => Subtype.val '' (t : Set s)).mono ?_
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
s : Set α
hs : s.Countable
this : Countable.{u + 1} (↑s : Type u)
t : Set α
ht : t.Finite
hts : t ⊆ s
⊢ Membership.mem (γ := Set (Set α))
    (range fun (t : Finset (↑s : Type u)) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t : Set (↑s : Type u))) t
have 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)
Tactic: lift t to Set s using hts
Cleared hypotheses: t, ht, hts
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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
⊢ 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)
have 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)))
Tactic: lift t to Finset s using ht.of_finite_image Subtype.val_injective.injOn
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
β : Type v
f : α → β
inst : Countable β
h : ∀ (b : β), (f ⁻¹' {b}).Countable
⊢ Countable α
have simp_rw : Set.Countable.{u} (α := α) univ
Tactic: simp_rw [← Set.countable_univ_iff, ← Set.preimage_univ (f := f), ← Set.iUnion_of_singleton,
    Set.preimage_iUnion, Set.countable_iUnion h]
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
β : Type v
f : α → β
inst : Countable β
h : ∀ (b : β), (f ⁻¹' {b}).Countable
simp_rw : Set.Countable.{u} (α := α) univ
⊢ Countable α
have simp_rw₁ : (f ⁻¹' univ).Countable
Tactic: simp_rw [← Set.countable_univ_iff, ← Set.preimage_univ (f := f), ← Set.iUnion_of_singleton,
    Set.preimage_iUnion, Set.countable_iUnion h]
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
β : Type v
f : α → β
inst : Countable β
h : ∀ (b : β), (f ⁻¹' {b}).Countable
simp_rw : Set.Countable.{u} (α := α) univ
simp_rw₁ : (f ⁻¹' univ).Countable
⊢ Countable α
have simp_rw₂ : (f ⁻¹' ⋃ (x : β), {x}).Countable
Tactic: simp_rw [← Set.countable_univ_iff, ← Set.preimage_univ (f := f), ← Set.iUnion_of_singleton,
    Set.preimage_iUnion, Set.countable_iUnion h]
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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
⊢ Countable α
have simp_rw₃ : Set.Countable.{u} (α := α) (⋃ (i : β), f ⁻¹' {i})
Tactic: simp_rw [← Set.countable_univ_iff, ← Set.preimage_univ (f := f), ← Set.iUnion_of_singleton,
    Set.preimage_iUnion, Set.countable_iUnion h]
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s : Set α
t : Set β
hs : s.Countable
ht : t.Countable
f : α → β → γ
⊢ (Set.image2 f s t).Countable
have rw : Set.Countable.{w} (α := γ) ((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t)
Tactic: rw [← image_prod]
-- Lean 4 proof step from Mathlib.Data.Set.Countable (hypothesis)
Goal:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : s.Countable
⊢ Set.Countable.{v} (α := β) {t : β | (f t).Nonempty}
have hs₁ : Countable.{u + 1} (↑s : Type u)
Tactic: rw [← Set.countable_coe_iff] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Set.Countable (hypothesis)
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)
⊢ Countable.{v + 1} (↑{t : β | (f t).Nonempty} : Type v)
have this : ∀ (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⟩
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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 : β)
⊢ Countable.{v + 1} (↑{t : β | (f t).Nonempty} : Type v)
have 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)
Tactic: choose F hF using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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
have refine : (↑(F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t ht)) : α) ∈ f t'
Tactic: refine ⟨F ⟨t, ht⟩, hF ⟨t, _⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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'
have rw : (↑(F (Subtype.mk (p := fun (t : β) ↦ (f t).Nonempty) t' ht')) : α) ∈ f t'
Tactic: rw [htt']
-- Lean 4 proof step from Mathlib.Data.Set.Countable (hypothesis)
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')
⊢ 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')
have A : (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', _⟩
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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
⊢ 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')
have simp : t = t'
Tactic: simp only [Subtype.mk.injEq]
-- Lean 4 proof step from Mathlib.Data.Set.Countable (goal)
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
⊢ t = t'
have by_contra : ∀ (H : ¬t = t'), False
Tactic: by_contra H