awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
s : Set α
h : s.Finite
⊢ range (ι := Fin (Fintype.card.{u} (↑(↑(h.toFinset (s := s)) : Set α) : Type u)))
      (⇑(Equiv.asEmbedding (p := fun (x : α) ↦ x ∈ (↑(h.toFinset (s := s)) : Set α))
            (Equiv.symm (Fintype.equivFin (↑(↑(h.toFinset (s := s)) : Set α) : Type u)))) :
        (a : Fin (Fintype.card (↑(↑h.toFinset : Set α) : Type u))) → α) =
    s

Tactic:
simp only [Finset.coe_sort_coe, Equiv.asEmbedding_range, Finite.coe_toFinset, setOf_mem_eq]

Premises used: Finset.coe_sort_coe, Set.Finite.coe_toFinset, Set.setOf_mem_eq, Equiv.asEmbedding_range
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
s : Set α
h : s.Finite
⊢ ∃ (n : ℕ) (f : Fin n → α), Injective f ∧ range f = s

Tactic:
let ⟨n, f, hf⟩ := h.fin_embedding
  ⟨n, f, f.injective, hf⟩

Premises used: _private.0.Set.Finite.fin_param.match_1, Exists, Set.Finite.fin_embedding, And, And.intro, Exists.intro, Function.Embedding.injective, Set.range, Function.Injective, Eq, DFunLike.coe
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
have : ∀ (this : Finite.{u + 1} (↑S : Type u)), C S
⊢ C S

Tactic:
have : Finite S := Finite.to_subtype h
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this : Finite.{u + 1} (↑S : Type u)
⊢ Finite.{max 1 (u + 1)} { T : Set α // T ⊆ S }

Tactic:
have : Finite {T : Set α // T ⊆ S} := Finite.of_equiv (Set S) (Equiv.Set.powerset S).symm
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this_1 : Finite.{u + 1} (↑S : Type u)
this : Finite.{max 1 (u + 1)} { T : Set α // T ⊆ S }
rw : C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S ⋯ : { x : Set α // x ⊆ S }) : Set α)
⊢ C S

Tactic:
rw [← Subtype.coe_mk (p := (· ⊆ S)) _ le_rfl]

Premises used: Subtype.coe_mk, le_rfl
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this_1 : Finite.{u + 1} (↑S : Type u)
this : Finite.{max 1 (u + 1)} { T : Set α // T ⊆ S }
⊢ C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S0 hS0) : Set α)

Tactic:
rw [← Subtype.coe_mk (p := (· ⊆ S)) _ hS0] at H0

Premises used: Subtype.coe_mk
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this_1 : Finite.{u + 1} (↑S : Type u)
this : Finite.{max 1 (u + 1)} { T : Set α // T ⊆ S }
H0₁ : C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S0 hS0) : Set α)
⊢ ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)

Tactic:
rw [← Subtype.coe_mk (p := (· ⊆ S)) _ hS0] at H0

Premises used: Subtype.coe_mk
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this_1 : Finite.{u + 1} (↑S : Type u)
this : Finite.{max 1 (u + 1)} { T : Set α // T ⊆ S }
H0₁ : C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S0 hS0) : Set α)
H1₁ : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
⊢ Finite.{u + 1} (↑S : Type u)

Tactic:
rw [← Subtype.coe_mk (p := (· ⊆ S)) _ hS0] at H0

Premises used: Subtype.coe_mk
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this_1 : Finite.{u + 1} (↑S : Type u)
this : Finite.{max 1 (u + 1)} { T : Set α // T ⊆ S }
H0₁ : C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S0 hS0) : Set α)
H1₁ : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this₁ : Finite.{u + 1} (↑S : Type u)
⊢ Finite.{max 1 (u + 1)} { T : Set α // T ⊆ S }

Tactic:
rw [← Subtype.coe_mk (p := (· ⊆ S)) _ hS0] at H0

Premises used: Subtype.coe_mk
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S0 hS0) : Set α)
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this_1 : Finite.{u + 1} (↑S : Type u)
this : Finite.{max 1 (u + 1)} { T : Set α // T ⊆ S }
⊢ C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S ⋯ : { x : Set α // x ⊆ S }) : Set α)

Tactic:
Finite.to_wellFoundedGT.wf.induction_bot' (fun s hs hs' ↦ ?_) H0

Premises used: WellFounded.induction_bot', IsWellFounded.wf
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S0 hS0) : Set α)
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this_1 : Finite.{u + 1} (↑S : Type u)
this : Finite.{max 1 (u + 1)} { T : Set α // T ⊆ S }
refine :
  ∀ (s : { x : Set α // x ⊆ S })
    (hs : (↑s : Set α) ≠ (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S ⋯ : { x : Set α // x ⊆ S }) : Set α))
    (hs' : C (↑s : Set α)), ∃ (c : { x : Set α // x ⊆ S }), s < c ∧ C (↑c : Set α)
⊢ C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S ⋯ : { x : Set α // x ⊆ S }) : Set α)

Tactic:
refine Finite.to_wellFoundedGT.wf.induction_bot' (fun s hs hs' ↦ ?_) H0

Premises used: WellFounded.induction_bot', IsWellFounded.wf
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S0 hS0) : Set α)
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this_1 : Finite.{u + 1} (↑S : Type u)
this : Finite.{max 1 (u + 1)} { T : Set α // T ⊆ S }
s : { x : Set α // x ⊆ S }
hs : (↑s : Set α) ≠ (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S ⋯ : { x : Set α // x ⊆ S }) : Set α)
hs' : C (↑s : Set α)
obtain :
  ∀ (a : α) (ha' : C (insert a (↑s : Set α))) (ha1 : a ∈ S) (ha2 : a ∉ (↑s : Set α)),
    ∃ (c : { x : Set α // x ⊆ S }), s < c ∧ C (↑c : Set α)
⊢ ∃ (c : { x : Set α // x ⊆ S }), s < c ∧ C (↑c : Set α)

Tactic:
obtain ⟨a, ⟨ha1, ha2⟩, ha'⟩ := H1 s (ssubset_of_ne_of_subset hs s.2) hs'

Premises used: ssubset_of_ne_of_subset, Subtype.val, Subtype.property
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S0 hS0) : Set α)
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this_1 : Finite.{u + 1} (↑S : Type u)
this : Finite.{max 1 (u + 1)} { T : Set α // T ⊆ S }
s : { x : Set α // x ⊆ S }
hs : (↑s : Set α) ≠ (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S ⋯ : { x : Set α // x ⊆ S }) : Set α)
hs' : C (↑s : Set α)
a : α
ha' : C (insert a (↑s : Set α))
ha1 : a ∈ S
ha2 : a ∉ (↑s : Set α)
⊢ ∃ (c : { x : Set α // x ⊆ S }), s < c ∧ C (↑c : Set α)

Tactic:
⟨⟨insert a s.1, insert_subset ha1 s.2⟩, Set.ssubset_insert ha2, ha'⟩

Premises used: Set.ssubset_insert, Insert.insert, Subtype.mk, And.intro, Exists.intro, Subtype.val, Set.insert_subset, Subtype.property
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S0 hS0) : Set α)
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this_1 : Finite.{u + 1} (↑S : Type u)
this : Finite.{max 1 (u + 1)} { T : Set α // T ⊆ S }
s : { x : Set α // x ⊆ S }
hs : (↑s : Set α) ≠ (↑(Subtype.mk (p := fun (x : Set α) ↦ x ⊆ S) S ⋯ : { x : Set α // x ⊆ S }) : Set α)
hs' : C (↑s : Set α)
a : α
ha' : C (insert a (↑s : Set α))
ha1 : a ∈ S
ha2 : a ∉ (↑s : Set α)
⊢ ∃ (c : { x : Set α // x ⊆ S }), s < c ∧ C (↑c : Set α)

Tactic:
exact ⟨⟨insert a s.1, insert_subset ha1 s.2⟩, Set.ssubset_insert ha2, ha'⟩
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
inst : Finite α
C : Set α → Prop
S0 : Set α
H0 : C S0
H1 : ∀ (S : Set α), S ≠ univ → C S → ∃ a ∉ S, C (insert a S)
⊢ ∀ s ⊂ univ, C s → ∃ a ∈ univ \ s, C (insert a s)

Tactic:
simpa [ssubset_univ_iff]

Premises used: Set.ssubset_univ_iff
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
X : Type u_1
⊢ Eq.{u_1 + 1} (α := Set X)
    (⋃₀
      {x : Set X |
        match (motive := Set X → Prop) x with
        | s => s.Finite})
    univ

Tactic:
sUnion_eq_univ_iff.mpr fun x ↦ ⟨{x}, finite_singleton x, rfl⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Singleton.singleton, Set.sUnion_eq_univ_iff, Set.finite_singleton, rfl
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
β : Type v
inst : LinearOrder β
s : Set α
f : α → β
h1 : s.Finite
x : α
hx : x ∈ s
⊢ ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b

Tactic:
simpa only [exists_prop, Finite.mem_toFinset] using
      h1.toFinset.exists_min_image f ⟨x, h1.mem_toFinset.2 hx⟩

Premises used: Iff.mpr, Set.Finite.mem_toFinset, exists_prop, Set.Finite.toFinset, Exists.intro, Finset.exists_min_image
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
β : Type v
inst : LinearOrder β
s : Set α
f : α → β
h1 : s.Finite
x : α
hx : x ∈ s
⊢ ∃ a ∈ s, ∀ b ∈ s, f b ≤ f a

Tactic:
simpa only [exists_prop, Finite.mem_toFinset] using
      h1.toFinset.exists_max_image f ⟨x, h1.mem_toFinset.2 hx⟩

Premises used: Iff.mpr, Set.Finite.mem_toFinset, Finset.exists_max_image, exists_prop, Set.Finite.toFinset, Exists.intro
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : LinearOrder β
s : Set α
f : α → β
h : s.Finite
inl : ∀ (h : Set.Finite.{u} (α := α) ∅), ∃ (a : α), ∀ (b : α), Membership.mem (γ := Set α) ∅ b → f a ≤ f b
inr : ∀ (hs : s.Nonempty), ∃ (a : α), ∀ b ∈ s, f a ≤ f b
⊢ ∃ (a : α), ∀ b ∈ s, f a ≤ f b

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : LinearOrder β
f : α → β
h : Set.Finite.{u} (α := α) ∅
⊢ ∃ (a : α), ∀ (b : α), Membership.mem (γ := Set α) ∅ b → f a ≤ f b

Tactic:
‹Nonempty α›.elim fun a => ⟨a, fun _ => False.elim⟩

Premises used: Nonempty.elim, False.elim, Exists.intro
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : LinearOrder β
f : α → β
h : Set.Finite.{u} (α := α) ∅
⊢ ∃ (a : α), ∀ (b : α), Membership.mem (γ := Set α) ∅ b → f a ≤ f b

Tactic:
exact ‹Nonempty α›.elim fun a => ⟨a, fun _ => False.elim⟩

Premises used: Nonempty.elim
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : LinearOrder β
s : Set α
f : α → β
h : s.Finite
hs : s.Nonempty
inr : ∀ x₀ ∈ s, ∀ (hx₀ : ∀ b ∈ s, f x₀ ≤ f b), ∃ (a : α), ∀ b ∈ s, f a ≤ f b
⊢ ∃ (a : α), ∀ b ∈ s, f a ≤ f b

Tactic:
rcases Set.exists_min_image s f h hs with ⟨x₀, _, hx₀⟩

Premises used: Set.exists_min_image
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : LinearOrder β
s : Set α
f : α → β
h : s.Finite
hs : s.Nonempty
x₀ : α
left : x₀ ∈ s
hx₀ : ∀ b ∈ s, f x₀ ≤ f b
⊢ ∃ (a : α), ∀ b ∈ s, f a ≤ f b

Tactic:
⟨x₀, fun x hx => hx₀ x hx⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : LinearOrder β
s : Set α
f : α → β
h : s.Finite
hs : s.Nonempty
x₀ : α
left : x₀ ∈ s
hx₀ : ∀ b ∈ s, f x₀ ≤ f b
⊢ ∃ (a : α), ∀ b ∈ s, f a ≤ f b

Tactic:
exact ⟨x₀, fun x hx => hx₀ x hx⟩
-- Module: Mathlib.Data.Set.Finite.Lemmas
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : LinearOrder β
s : Set α
f : α → β
h : s.Finite
⊢ ∃ (a : α), ∀ b ∈ s, f b ≤ f a

Tactic:
exists_lower_bound_image (β := βᵒᵈ) s f h

Premises used: Set.exists_lower_bound_image
-- Module: Mathlib.Data.Set.Finite.List
Goal:
α : Type u_1
inst : Finite α
n : ℕ
⊢ Set.Finite.{u_1} (α := List α) {l : List α | l.length = n}

Tactic:
List.Vector.finite

Premises used: List.Vector.finite, Set.Mem, setOf, List.Vector, Set.Finite
-- Module: Mathlib.Data.Set.Finite.List
Goal:
α : Type u_1
inst : Finite α
n : ℕ
⊢ Set.Finite.{u_1} (α := List α) (⋃ i ∈ (↑(Finset.range n) : Set ℕ), {l : List α | l.length = i})

Tactic:
(Finset.range n).finite_toSet.biUnion fun i _ ↦ finite_length_eq α i

Premises used: Finset.range, List.finite_length_eq, Finset.finite_toSet, Set.Finite.biUnion
-- Module: Mathlib.Data.Set.Finite.List
Goal:
α : Type u_1
inst : Finite α
n : ℕ
h :
  Eq.{u_1 + 1} (α := Set (List α)) {l : List α | l.length < n}
    (⋃ i ∈ (↑(Finset.range n) : Set ℕ), {l : List α | l.length = i})
⊢ Set.Finite.{u_1} (α := List α) {l : List α | l.length < n}

Tactic:
convert! (Finset.range n).finite_toSet.biUnion fun i _ ↦ finite_length_eq α i

Premises used: Finset.range, List.finite_length_eq, Finset.finite_toSet, Set.Finite.biUnion
-- Module: Mathlib.Data.Set.Finite.List
Goal:
α : Type u_1
inst : Finite α
n : ℕ
h :
  ∀ (x : List α),
    Membership.mem (γ := Set (List α)) {l : List α | l.length < n} x ↔
      Membership.mem (γ := Set (List α)) (⋃ i ∈ (↑(Finset.range n) : Set ℕ), {l : List α | l.length = i}) x
⊢ Eq.{u_1 + 1} (α := Set (List α)) {l : List α | l.length < n}
    (⋃ i ∈ (↑(Finset.range n) : Set ℕ), {l : List α | l.length = i})

Tactic:
ext
-- Module: Mathlib.Data.Set.Finite.List
Goal:
α : Type u_1
inst : Finite α
n : ℕ
x : List α
⊢ Membership.mem (γ := Set (List α)) {l : List α | l.length < n} x ↔
    Membership.mem (γ := Set (List α)) (⋃ i ∈ (↑(Finset.range n) : Set ℕ), {l : List α | l.length = i}) x

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.List
Goal:
α : Type u_1
inst : Finite α
n : ℕ
⊢ Set.Finite.{u_1} (α := List α) {l : List α | l.length ≤ n}

Tactic:
simpa [Nat.lt_succ_iff] using finite_length_lt α (n + 1)

Premises used: Nat.lt_succ_iff, HAdd.hAdd, List.finite_length_lt, OfNat.ofNat
-- Module: Mathlib.Data.Set.Finite.Monad
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst : DecidableEq β
f : Set (α → β)
s : Set α
inst_1 : Fintype (↑f : Type (max u v))
inst_2 : Fintype (↑s : Type u)
rw : Fintype (↑(⋃ f_1 ∈ f, f_1 '' s) : Type v)
⊢ Fintype (↑(f.seq s) : Type v)

Tactic:
rw [seq_def]

Premises used: Set.seq_def
-- Module: Mathlib.Data.Set.Finite.Monad
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst : DecidableEq β
f : Set (α → β)
s : Set α
inst_1 : Fintype (↑f : Type (max u v))
inst_2 : Fintype (↑s : Type u)
⊢ Fintype (↑(⋃ f_1 ∈ f, f_1 '' s) : Type v)

Tactic:
apply Set.fintypeBiUnion'

Premises used: Set.fintypeBiUnion'
-- Module: Mathlib.Data.Set.Finite.Monad
Goal:
α : Type u
a : α
⊢ Set.Finite (pure a)

Tactic:
toFinite _

Premises used: Set.toFinite
-- Module: Mathlib.Data.Set.Finite.Monad
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : Set (α → β)
s : Set α
inst : Finite (↑f : Type (max u v))
inst_1 : Finite.{u + 1} (↑s : Type u)
rw : Finite.{v + 1} (↑(⋃ f_1 ∈ f, f_1 '' s) : Type v)
⊢ Finite.{v + 1} (↑(f.seq s) : Type v)

Tactic:
rw [seq_def]

Premises used: Set.seq_def
-- Module: Mathlib.Data.Set.Finite.Monad
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : Set (α → β)
s : Set α
inst : Finite (↑f : Type (max u v))
inst_1 : Finite.{u + 1} (↑s : Type u)
⊢ Finite.{v + 1} (↑(⋃ f_1 ∈ f, f_1 '' s) : Type v)

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.Finite.Monad
Goal:
α β : Type u_1
s : Set α
f : α → Set β
h : s.Finite
hf : ∀ a ∈ s, (f a).Finite
⊢ (s >>= f).Finite

Tactic:
h.biUnion hf

Premises used: Set.Finite.biUnion
-- Module: Mathlib.Data.Set.Finite.Monad
Goal:
α : Type u
β : Type v
f : Set (α → β)
s : Set α
hf : f.Finite
hs : s.Finite
⊢ (f.seq s).Finite

Tactic:
hf.image2 _ hs

Premises used: Set.Finite.image2, Set.seq
-- Module: Mathlib.Data.Set.Finite.Monad
Goal:
α β : Type u
f : Set (α → β)
s : Set α
hf : f.Finite
hs : s.Finite
⊢ (f <*> s).Finite

Tactic:
hf.seq hs

Premises used: Set.Finite.seq
-- Module: Mathlib.Data.Set.Finite.Powerset
Goal:
α : Type u
a : Set α
h : a.Finite
⊢ (↑(Finset.map
          (RelEmbedding.toEmbedding (r := fun (x1 x2 : Finset α) ↦ x1 ≤ x2) (s := fun (x1 x2 : Set α) ↦ x1 ≤ x2)
            Finset.coeEmb)
          h.toFinset (s := a).powerset) :
      Set (Set α)).Finite

Tactic:
((Finset.powerset h.toFinset).map Finset.coeEmb.1).finite_toSet

Premises used: Finset.map, RelEmbedding.toEmbedding, Finset.coeEmb, Set.Finite.toFinset, Finset.powerset, Finset.finite_toSet
-- Module: Mathlib.Data.Set.Finite.Powerset
Goal:
α : Type u
a : Set α
h : a.Finite
h₁ :
  {b : Set α | b ⊆ a} =
    (↑(Finset.map
          (RelEmbedding.toEmbedding (r := fun (x1 x2 : Finset α) ↦ x1 ≤ x2) (s := fun (x1 x2 : Set α) ↦ x1 ≤ x2)
            Finset.coeEmb)
          h.toFinset (s := a).powerset) :
      Set (Set α))
⊢ Set.Finite.{u} (α := Set α) {b : Set α | b ⊆ a}

Tactic:
convert! ((Finset.powerset h.toFinset).map Finset.coeEmb.1).finite_toSet

Premises used: Finset.map, RelEmbedding.toEmbedding, Finset.coeEmb, Set.Finite.toFinset, Finset.powerset, Finset.finite_toSet
-- Module: Mathlib.Data.Set.Finite.Powerset
Goal:
α : Type u
a : Set α
h : a.Finite
h₁ :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {b : Set α | b ⊆ a} s ↔
      s ∈
        (↑(Finset.map
              (RelEmbedding.toEmbedding (r := fun (x1 x2 : Finset α) ↦ x1 ≤ x2) (s := fun (x1 x2 : Set α) ↦ x1 ≤ x2)
                Finset.coeEmb)
              h.toFinset (s := a).powerset) :
          Set (Set α))
⊢ {b : Set α | b ⊆ a} =
    (↑(Finset.map
          (RelEmbedding.toEmbedding (r := fun (x1 x2 : Finset α) ↦ x1 ≤ x2) (s := fun (x1 x2 : Set α) ↦ x1 ≤ x2)
            Finset.coeEmb)
          h.toFinset (s := a).powerset) :
      Set (Set α))

Tactic:
ext s
-- Module: Mathlib.Data.Set.Finite.Powerset
Goal:
α : Type u
a : Set α
h : a.Finite
s : Set α
⊢ Membership.mem (γ := Set (Set α)) {b : Set α | b ⊆ a} s ↔
    s ∈
      (↑(Finset.map
            (RelEmbedding.toEmbedding (r := fun (x1 x2 : Finset α) ↦ x1 ≤ x2) (s := fun (x1 x2 : Set α) ↦ x1 ≤ x2)
              Finset.coeEmb)
            h.toFinset (s := a).powerset) :
        Set (Set α))

Tactic:
simpa [← @exists_finite_iff_finset α fun t => t ⊆ a ∧ t = s, Finite.subset_toFinset,
    ← and_assoc, Finset.coeEmb] using h.subset

Premises used: Set.Finite.subset, Set.Finite.subset_toFinset, Finset.coeEmb, and_assoc, Set.exists_finite_iff_finset
-- Module: Mathlib.Data.Set.Finite.Powerset
Goal:
α : Type u
s : Set α
h : s.Finite
⊢ (𝒫 s).Finite

Tactic:
h.finite_subsets

Premises used: Set.powerset, Set.Finite.finite_subsets
-- Module: Mathlib.Data.Set.Finite.Range
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst : DecidableEq α
f : ι → α
inst_1 : Fintype (PLift ι)
⊢ ∀ (x : α), x ∈ Finset.image (f ∘ PLift.down) Finset.univ ↔ x ∈ range f

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Range
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : ι → α
inst : Finite ι
haveI : ∀ (this : Fintype (PLift ι)), Finite.{u + 1} (↑(range f) : Type u)
⊢ Finite.{u + 1} (↑(range f) : Type u)

Tactic:
haveI := Fintype.ofFinite (PLift ι)
-- Module: Mathlib.Data.Set.Finite.Range
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : ι → α
inst : Finite ι
this : Fintype (PLift ι)
⊢ Finite.{u + 1} (↑(range f) : Type u)

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.Finite.Range
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : ι → α
inst : Finite ι
haveI haveI₁ haveI₂ : ∀ (this : Fintype (PLift ι)), Finite.{u + 1} (↑(range f) : Type u)
⊢ Finite.{u + 1} (↑(range f) : Type u)

Tactic:
classical
  haveI := Fintype.ofFinite (PLift ι)
  infer_instance
-- Module: Mathlib.Data.Set.Finite.Range
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst : Finite α
f : α → β
⊢ Finite.{v + 1} (↑{x : β | ∃ (x_1 : α), f x_1 = x} : Type v)

Tactic:
Finite.Set.finite_range f

Premises used: Finite.Set.finite_range, Set.range
-- Module: Mathlib.Data.Set.Finite.Range
Goal:
α : Type u
ι : Sort w
f : ι → α
inst : Finite ι
⊢ (range f).Finite

Tactic:
toFinite _

Premises used: Set.toFinite
-- Module: Mathlib.Data.Set.Finite.Range
Goal:
α : Type u
β : Type v
s : Set α
hs : s.Finite
F : (i : α) → i ∈ s → β
⊢ Finite.{u + 1} (↑s : Type u)

Tactic:
have := hs.to_subtype
-- Module: Mathlib.Data.Set.Finite.Range
Goal:
α : Type u
β : Type v
s : Set α
hs : s.Finite
F : (i : α) → i ∈ s → β
this : Finite.{u + 1} (↑s : Type u)
⊢ Set.Finite.{v} (α := β) {y : β | ∃ (x : α) (hx : x ∈ s), F x hx = y}

Tactic:
simpa [range] using finite_range fun x : s => F x x.2

Premises used: Set.finite_range, Set.range, Subtype.val, Subtype.property
-- Module: Mathlib.Data.Set.Finite.Range
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
u : Set β
hu : u.Finite
hsu : u ⊆ f '' s
⊢ Finite.{v + 1} (↑u : Type v)

Tactic:
have : Finite u := Finite.to_subtype hu
-- Module: Mathlib.Data.Set.Finite.Range
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
u : Set β
hu : u.Finite
hsu : u ⊆ f '' s
this : Finite.{v + 1} (↑u : Type v)
choose :
  ∀ (g : ⦃a : β⦄ → a ∈ u → α) (hg : ∀ ⦃a : β⦄ (a_1 : a ∈ u), g a_1 ∈ s) (hg' : ∀ ⦃a : β⦄ (a_1 : a ∈ u), f (g a_1) = a),
    ∃ t ⊆ s, ∃ (_ : t.Finite), f '' t = u
⊢ ∃ t ⊆ s, ∃ (_ : t.Finite), f '' t = u

Tactic:
choose g hg hg' using hsu
-- Module: Mathlib.Data.Set.Finite.Range
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
u : Set β
hu : u.Finite
this : Finite.{v + 1} (↑u : Type v)
g : ⦃a : β⦄ → a ∈ u → α
hg : ∀ ⦃a : β⦄ (a_1 : a ∈ u), g a_1 ∈ s
hg' : ∀ ⦃a : β⦄ (a_1 : a ∈ u), f (g a_1) = a
g' : (x : (↑u : Type v)) → α := fun (x : (↑u : Type v)) ↦ g ⋯
a : α
ha : a ∈ range g'
⊢ a ∈ s

Tactic:
aesop
-- Module: Mathlib.Data.Set.Finite.Range
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
u : Set β
hu : u.Finite
this : Finite.{v + 1} (↑u : Type v)
g : ⦃a : β⦄ → a ∈ u → α
hg : ∀ ⦃a : β⦄ (a_1 : a ∈ u), g a_1 ∈ s
hg' : ∀ ⦃a : β⦄ (a_1 : a ∈ u), f (g a_1) = a
g' : (x : (↑u : Type v)) → α := fun (x : (↑u : Type v)) ↦ g ⋯
⊢ f '' range g' = u

Tactic:
aesop
-- Module: Mathlib.Data.Set.Finite.Range
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
u : Set β
hu : u.Finite
this : Finite.{v + 1} (↑u : Type v)
g : ⦃a : β⦄ → a ∈ u → α
hg : ∀ ⦃a : β⦄ (a_1 : a ∈ u), g a_1 ∈ s
hg' : ∀ ⦃a : β⦄ (a_1 : a ∈ u), f (g a_1) = a
g' : (x : (↑u : Type v)) → α := fun (x : (↑u : Type v)) ↦ g ⋯
⊢ ∃ t ⊆ s, ∃ (_ : t.Finite), f '' t = u

Tactic:
exact ⟨range g', fun a ha ↦ by aesop, finite_range _, by aesop⟩
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s : Set α
K : s.FiniteExhaustion
n : ℕ
⊢ Finite.{u_1 + 1} (↑((K : (a : ℕ) → Set α) n) : Type u_1)

Tactic:
K.finite' n

Premises used: Set.FiniteExhaustion.finite'
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s : Set α
K : s.FiniteExhaustion
⊢ K.toFun (s := s) = (⇑K : (a : ℕ) → Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s : Set α
K : s.FiniteExhaustion
n : ℕ
⊢ Set.Finite.{u_1} (α := α) ((K : (a : ℕ) → Set α) n)

Tactic:
K.finite' n

Premises used: Set.Finite, Set.FiniteExhaustion.finite'
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s : Set α
K : s.FiniteExhaustion
n : ℕ
⊢ Subset (α := Set α) ((K : (a : ℕ) → Set α) n : Set α) ((K : (a : ℕ) → Set α) (n + 1) : Set α)

Tactic:
K.subset_succ' n

Premises used: Set.FiniteExhaustion.subset_succ'
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s : Set α
K : s.FiniteExhaustion
m n : ℕ
h : m ≤ n
⊢ Subset (α := Set α) ((K : (a : ℕ) → Set α) m : Set α) ((K : (a : ℕ) → Set α) n : Set α)

Tactic:
OrderHomClass.mono K h

Premises used: OrderHomClass.mono
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s : Set α
K : s.FiniteExhaustion
⊢ ⋃ (n : ℕ), (K : (a : ℕ) → Set α) n = s

Tactic:
K.iUnion_eq'

Premises used: Set.FiniteExhaustion.iUnion_eq'
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
a : Nonempty.{u_1 + 1} s.FiniteExhaustion
⊢ s.FiniteExhaustion

Tactic:
apply Classical.choice

Premises used: Classical.choice
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
pos : ∀ (h : Nonempty.{u_1 + 1} (↑s : Type u_1)), Nonempty.{u_1 + 1} s.FiniteExhaustion
neg : ∀ (h : ¬Nonempty.{u_1 + 1} (↑s : Type u_1)), Nonempty.{u_1 + 1} s.FiniteExhaustion
⊢ Nonempty.{u_1 + 1} s.FiniteExhaustion

Tactic:
by_cases h : Nonempty s

Premises used: Set.Elem, Nonempty