awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ hs.toFinset (s := s) = ht.toFinset (s := t) ↔ s = t

Tactic:
@toFinset_inj _ _ _ hs.fintype ht.fintype

Premises used: Set.toFinset_inj, Set.Finite.toFinset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
hs : s.Finite
t : Finset α
rw : (↑(hs.toFinset (s := s)) : Set α) ⊆ (↑t : Set α) ↔ s ⊆ (↑t : Set α)
rw₁ rw₂ : s ⊆ (↑t : Set α) ↔ s ⊆ (↑t : Set α)
⊢ hs.toFinset (s := s) ⊆ t ↔ s ⊆ (↑t : Set α)

Tactic:
rw [← Finset.coe_subset, Finite.coe_toFinset]

Premises used: Set.Finite.coe_toFinset, Finset.coe_subset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
hs : s.Finite
t : Finset α
rw : (↑(hs.toFinset (s := s)) : Set α) ⊂ (↑t : Set α) ↔ s ⊂ (↑t : Set α)
rw₁ rw₂ : s ⊂ (↑t : Set α) ↔ s ⊂ (↑t : Set α)
⊢ hs.toFinset (s := s) ⊂ t ↔ s ⊂ (↑t : Set α)

Tactic:
rw [← Finset.coe_ssubset, Finite.coe_toFinset]

Premises used: Set.Finite.coe_toFinset, Finset.coe_ssubset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
t : Set α
ht : t.Finite
s : Finset α
rw : (↑s : Set α) ⊆ (↑(ht.toFinset (s := t)) : Set α) ↔ (↑s : Set α) ⊆ t
rw₁ rw₂ : (↑s : Set α) ⊆ t ↔ (↑s : Set α) ⊆ t
⊢ s ⊆ ht.toFinset (s := t) ↔ (↑s : Set α) ⊆ t

Tactic:
rw [← Finset.coe_subset, Finite.coe_toFinset]

Premises used: Set.Finite.coe_toFinset, Finset.coe_subset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
t : Set α
ht : t.Finite
s : Finset α
rw : (↑s : Set α) ⊂ (↑(ht.toFinset (s := t)) : Set α) ↔ (↑s : Set α) ⊂ t
rw₁ rw₂ : (↑s : Set α) ⊂ t ↔ (↑s : Set α) ⊂ t
⊢ s ⊂ ht.toFinset (s := t) ↔ (↑s : Set α) ⊂ t

Tactic:
rw [← Finset.coe_ssubset, Finite.coe_toFinset]

Premises used: Set.Finite.coe_toFinset, Finset.coe_ssubset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ hs.toFinset (s := s) ⊆ ht.toFinset (s := t) ↔ s ⊆ t

Tactic:
simp only [← Finset.coe_subset, Finite.coe_toFinset]

Premises used: Set.Finite.coe_toFinset, Finset.coe_subset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ hs.toFinset (s := s) ⊂ ht.toFinset (s := t) ↔ s ⊂ t

Tactic:
simp only [← Finset.coe_ssubset, Finite.coe_toFinset]

Premises used: Set.Finite.coe_toFinset, Finset.coe_ssubset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
h : Set.Finite.{u} (α := α) {x : α | p x}
⊢ h.toFinset (s := {x : α | p x}) = {x : α | p x}

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ Disjoint (hs.toFinset (s := s)) (ht.toFinset (s := t)) ↔ Disjoint s t

Tactic:
@disjoint_toFinset _ _ _ hs.fintype ht.fintype

Premises used: Set.disjoint_toFinset, Set.Finite.toFinset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
inst : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∩ t).Finite
h₁ : ∀ (a : α), a ∈ h.toFinset (s := s ∩ t) ↔ a ∈ hs.toFinset (s := s) ∩ ht.toFinset (s := t)
⊢ h.toFinset (s := s ∩ t) = hs.toFinset (s := s) ∩ ht.toFinset (s := t)

Tactic:
ext
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
inst : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∩ t).Finite
a : α
⊢ a ∈ h.toFinset (s := s ∩ t) ↔ a ∈ hs.toFinset (s := s) ∩ ht.toFinset (s := t)

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
inst : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∪ t).Finite
h₁ : ∀ (a : α), a ∈ h.toFinset (s := s ∪ t) ↔ a ∈ hs.toFinset (s := s) ∪ ht.toFinset (s := t)
⊢ h.toFinset (s := s ∪ t) = hs.toFinset (s := s) ∪ ht.toFinset (s := t)

Tactic:
ext
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
inst : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∪ t).Finite
a : α
⊢ a ∈ h.toFinset (s := s ∪ t) ↔ a ∈ hs.toFinset (s := s) ∪ ht.toFinset (s := t)

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
inst : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s \ t).Finite
h₁ : ∀ (a : α), a ∈ h.toFinset (s := s \ t) ↔ a ∈ hs.toFinset (s := s) \ ht.toFinset (s := t)
⊢ h.toFinset (s := s \ t) = hs.toFinset (s := s) \ ht.toFinset (s := t)

Tactic:
ext
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
inst : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s \ t).Finite
a : α
⊢ a ∈ h.toFinset (s := s \ t) ↔ a ∈ hs.toFinset (s := s) \ ht.toFinset (s := t)

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
inst : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∆ t).Finite
h₁ : ∀ (a : α), a ∈ h.toFinset (s := s ∆ t) ↔ a ∈ hs.toFinset (s := s) ∆ ht.toFinset (s := t)
⊢ h.toFinset (s := s ∆ t) = hs.toFinset (s := s) ∆ ht.toFinset (s := t)

Tactic:
ext
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
inst : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∆ t).Finite
a : α
⊢ a ∈ h.toFinset (s := s ∆ t) ↔ a ∈ hs.toFinset (s := s) ∆ ht.toFinset (s := t)

Tactic:
simp [mem_symmDiff, Finset.mem_symmDiff]

Premises used: Set.mem_symmDiff, Finset.mem_symmDiff
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
inst : DecidableEq α
inst_1 : Fintype α
hs : s.Finite
h : sᶜ.Finite
h₁ : ∀ (a : α), a ∈ h.toFinset (s := sᶜ) ↔ a ∈ (hs.toFinset (s := s))ᶜ
⊢ h.toFinset (s := sᶜ) = (hs.toFinset (s := s))ᶜ

Tactic:
ext
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
inst : DecidableEq α
inst_1 : Fintype α
hs : s.Finite
h : sᶜ.Finite
a : α
⊢ a ∈ h.toFinset (s := sᶜ) ↔ a ∈ (hs.toFinset (s := s))ᶜ

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : Fintype α
h : Set.Finite.{u} (α := α) univ
⊢ h.toFinset (s := univ) = Finset.univ

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
h : s.Finite
⊢ h.toFinset (s := s) = ∅ ↔ s = ∅

Tactic:
@toFinset_eq_empty _ _ h.fintype

Premises used: Set.toFinset_eq_empty, Set.Finite.toFinset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
h : Set.Finite.{u} (α := α) ∅
⊢ h.toFinset (s := ∅) = ∅

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
inst : Fintype α
h : s.Finite
⊢ h.toFinset (s := s) = Finset.univ ↔ s = univ

Tactic:
@toFinset_eq_univ _ _ _ h.fintype

Premises used: Set.toFinset_eq_univ, Set.Finite.toFinset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
s : Set α
inst : DecidableEq β
f : α → β
hs : s.Finite
h : (f '' s).Finite
h₁ : ∀ (a : β), a ∈ h.toFinset (s := f '' s) ↔ a ∈ Finset.image f (hs.toFinset (s := s))
⊢ h.toFinset (s := f '' s) = Finset.image f (hs.toFinset (s := s))

Tactic:
ext
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
s : Set α
inst : DecidableEq β
f : α → β
hs : s.Finite
h : (f '' s).Finite
a : β
⊢ a ∈ h.toFinset (s := f '' s) ↔ a ∈ Finset.image f (hs.toFinset (s := s))

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Fintype β
f : β → α
h : (range f).Finite
h₁ : ∀ (a : α), a ∈ h.toFinset (s := range f) ↔ a ∈ Finset.image f Finset.univ
⊢ h.toFinset (s := range f) = Finset.image f Finset.univ

Tactic:
ext
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Fintype β
f : β → α
h : (range f).Finite
a : α
⊢ a ∈ h.toFinset (s := range f) ↔ a ∈ Finset.image f Finset.univ

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
h : s.Finite
rw : (↑(h.toFinset (s := s)) : Set α).Nontrivial ↔ s.Nontrivial
rw₁ rw₂ : s.Nontrivial ↔ s.Nontrivial
⊢ h.toFinset (s := s).Nontrivial ↔ s.Nontrivial

Tactic:
rw [Finset.Nontrivial, h.coe_toFinset]

Premises used: Set.Finite.coe_toFinset, Finset.Nontrivial
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst : DecidableEq α
s t : Set α
inst_1 : Fintype (↑s : Type u)
inst_2 : Fintype (↑t : Type u)
⊢ ∀ (x : α), x ∈ s.toFinset ∪ t.toFinset ↔ x ∈ s ∪ t

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
inst : Fintype (↑s : Type u)
inst_1 : DecidablePred p
⊢ ∀ (x : α), x ∈ {a ∈ s.toFinset | p a} ↔ Membership.mem (γ := Set α) {a : α | a ∈ s ∧ p a} x

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst : DecidableEq α
inst_1 : Fintype (↑s : Type u)
inst_2 : Fintype (↑t : Type u)
⊢ ∀ (x : α), x ∈ s.toFinset ∩ t.toFinset ↔ x ∈ s ∩ t

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst : Fintype (↑s : Type u)
inst_1 : DecidablePred fun (x : α) ↦ x ∈ t
⊢ ∀ (x : α), x ∈ {a ∈ s.toFinset | a ∈ t} ↔ x ∈ s ∩ t

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst : Fintype (↑t : Type u)
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
⊢ ∀ (x : α), x ∈ {a ∈ t.toFinset | a ∈ s} ↔ x ∈ s ∩ t

Tactic:
simp [and_comm]

Premises used: and_comm
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst : Fintype (↑s : Type u)
inst_1 : DecidablePred fun (x : α) ↦ x ∈ t
h : t ⊆ s
rw : Fintype (↑(s ∩ t) : Type u)
⊢ Fintype (↑t : Type u)

Tactic:
rw [← inter_eq_self_of_subset_right h]

Premises used: Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst : Fintype (↑s : Type u)
inst_1 : DecidablePred fun (x : α) ↦ x ∈ t
h : t ⊆ s
⊢ Fintype (↑(s ∩ t) : Type u)

Tactic:
apply Set.fintypeInterOfLeft

Premises used: Set.fintypeInterOfLeft
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst : DecidableEq α
s t : Set α
inst_1 : Fintype (↑s : Type u)
inst_2 : Fintype (↑t : Type u)
⊢ ∀ (x : α), x ∈ s.toFinset \ t.toFinset ↔ x ∈ s \ t

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
⊢ ∀ (x : α), Membership.mem (γ := Finset α) ∅ x ↔ Membership.mem (γ := Set α) ∅ x

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
⊢ ∀ (x : α), Membership.mem (γ := Finset α) {a} x ↔ Membership.mem (γ := Set α) {a} x

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst : DecidableEq α
inst_1 : Fintype (↑s : Type u)
⊢ ∀ (x : α), x ∈ insert a s.toFinset ↔ x ∈ insert a s

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst : Fintype (↑s : Type u)
h : a ∉ s
⊢ a ∉ s.toFinset.val

Tactic:
simp [h]
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst : Fintype (↑s : Type u)
h : a ∉ s
⊢ ∀ (x : α), x ∈ { val := a ::ₘ s.toFinset.val, nodup := ⋯ : Finset α } ↔ x ∈ insert a s

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst : Fintype (↑s : Type u)
h : a ∈ s
⊢ ∀ (x : α), x ∈ s.toFinset ↔ x ∈ insert a s

Tactic:
simp [h]
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst : DecidableEq β
s : Set α
f : α → β
inst_1 : Fintype (↑s : Type u)
⊢ ∀ (x : β), x ∈ Finset.image f s.toFinset ↔ x ∈ f '' s

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
g : β → Option α
I : IsPartialInv f g
inst : Fintype (↑(f '' s) : Type v)
⊢ ∀ (x : α), x ∈ { val := Multiset.filterMap g (f '' s).toFinset.val, nodup := ⋯ : Finset α } ↔ x ∈ s

Tactic:
simp [I.eq]

Premises used: Function.IsPartialInv.eq
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
n : ℕ
⊢ ∀ (x : ℕ), x ∈ Finset.range n ↔ Membership.mem (γ := Set ℕ) {i : ℕ | i < n} x

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
n : ℕ
⊢ Fintype (↑{i : ℕ | i ≤ n} : Type)

Tactic:
simpa [Nat.lt_succ_iff] using Set.fintypeLTNat (n + 1)

Premises used: Set.fintypeLTNat, Nat.lt_succ_iff, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Finset α
⊢ (↑s : Set α).Finite

Tactic:
Set.toFinite _

Premises used: Set.toFinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Finset α
rw : (↑s : Set α).toFinset = s
rw₁ rw₂ : s = s
⊢ ⋯.toFinset (s := (↑s : Set α)) = s

Tactic:
rw [toFinite_toFinset, toFinset_coe]

Premises used: Finset.toFinset_coe, Set.toFinite_toFinset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
p : Finset α → Prop
h : ∀ (s : Set α) (hs : s.Finite), p (hs.toFinset (s := s))
s : Finset α
⊢ p s

Tactic:
simpa using h s s.finite_toSet

Premises used: SetLike.coe, Finset.finite_toSet
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
p : Finset α → Prop
h : ∃ (s : Finset α), p s
s : Finset α
hs : p s
⊢ p (⋯.toFinset (s := (↑s : Set α)))

Tactic:
simpa
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Multiset α
⊢ Set.Finite.{u} (α := α) {x : α | x ∈ s}

Tactic:
simpa only [← Multiset.mem_toFinset] using s.toFinset.finite_toSet

Premises used: Multiset.toFinset, Finset.finite_toSet, Multiset.mem_toFinset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Multiset α
⊢ Set.Finite.{u} (α := α) {x : α | x ∈ s}

Tactic:
classical simpa only [← Multiset.mem_toFinset] using s.toFinset.finite_toSet

Premises used: Multiset.mem_toFinset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : DecidableEq α
s : Multiset α
h : ∀ (x : α), x ∈ ⋯.toFinset (s := {x : α | x ∈ s}) ↔ x ∈ s.toFinset
⊢ ⋯.toFinset (s := {x : α | x ∈ s}) = s.toFinset

Tactic:
ext x
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : DecidableEq α
s : Multiset α
x : α
⊢ x ∈ ⋯.toFinset (s := {x : α | x ∈ s}) ↔ x ∈ s.toFinset

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
l : List α
⊢ Set.Finite.{u} (α := α) {x : α | x ∈ l}

Tactic:
(show Multiset α from ⟦l⟧).finite_toSet

Premises used: setOf, Multiset.finite_toSet, Quotient.mk, Multiset.Mem, List.isSetoid
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
x : Finset α
⊢ (fun (s : { s : Set α // s.Finite }) ↦ ⋯.toFinset (s := (↑s : Set α)))
      ((fun (s : Finset α) ↦ Subtype.mk (p := fun (s : Set α) ↦ s.Finite) (↑s : Set α) ⋯) x) =
    x

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
x : { s : Set α // s.Finite }
⊢ (fun (s : Finset α) ↦ Subtype.mk (p := fun (s : Set α) ↦ s.Finite) (↑s : Set α) ⋯)
      ((fun (s : { s : Set α // s.Finite }) ↦ ⋯.toFinset (s := (↑s : Set α))) x) =
    x

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
⊢ WellFoundedLT.{u} { s : Set α // s.Finite }

Tactic:
OrderIso.finsetSetFinite.symm.toOrderEmbedding.wellFoundedLT

Premises used: OrderIso.toOrderEmbedding, OrderIso.symm, OrderEmbedding.wellFoundedLT, OrderIso.finsetSetFinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
inst : Finite α
⊢ Finite.{u + 1} (↑s : Type u)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
⊢ Finite.{u + 1} (↑∅ : Type u)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
⊢ Finite.{u + 1} (↑{a} : Type u)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst : Finite.{u + 1} (↑s : Type u)
inst_1 : Finite.{u + 1} (↑t : Type u)
intro : ∀ (val : Fintype (↑s : Type u)), Finite.{u + 1} (↑(s ∪ t) : Type u)
⊢ Finite.{u + 1} (↑(s ∪ t) : Type u)

Tactic:
cases nonempty_fintype s

Premises used: Set.Elem, nonempty_fintype
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst : Finite.{u + 1} (↑s : Type u)
inst_1 : Finite.{u + 1} (↑t : Type u)
val : Fintype (↑s : Type u)
intro : ∀ (val : Fintype (↑t : Type u)), Finite.{u + 1} (↑(s ∪ t) : Type u)
⊢ Finite.{u + 1} (↑(s ∪ t) : Type u)

Tactic:
cases nonempty_fintype t

Premises used: Set.Elem, nonempty_fintype
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst : Finite.{u + 1} (↑s : Type u)
inst_1 : Finite.{u + 1} (↑t : Type u)
val : Fintype (↑s : Type u)
val_1 : Fintype (↑t : Type u)
⊢ Finite.{u + 1} (↑(s ∪ t) : Type u)

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst : Finite.{u + 1} (↑s : Type u)
inst_1 : Finite.{u + 1} (↑t : Type u)
val : Fintype (↑s : Type u)
val_1 : Fintype (↑t : Type u)
⊢ Finite.{u + 1} (↑(s ∪ t) : Type u)

Tactic:
classical
  infer_instance
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
inst : Finite.{u + 1} (↑s : Type u)
intro : ∀ (val : Fintype (↑s : Type u)), Finite.{u + 1} (↑{a : α | a ∈ s ∧ p a} : Type u)
⊢ Finite.{u + 1} (↑{a : α | a ∈ s ∧ p a} : Type u)

Tactic:
cases nonempty_fintype s

Premises used: Set.Elem, nonempty_fintype
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
inst : Finite.{u + 1} (↑s : Type u)
val : Fintype (↑s : Type u)
⊢ Finite.{u + 1} (↑{a : α | a ∈ s ∧ p a} : Type u)

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
inst : Finite.{u + 1} (↑s : Type u)
val : Fintype (↑s : Type u)
⊢ Finite.{u + 1} (↑{a : α | a ∈ s ∧ p a} : Type u)

Tactic:
classical
  infer_instance
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
inst : Finite.{u + 1} (↑s : Type u)
h : t ⊆ s
rw : Finite.{u + 1} (↑{x : α | x ∈ s ∧ x ∈ t} : Type u)
⊢ Finite.{u + 1} (↑t : Type u)

Tactic:
rw [← sep_eq_of_subset h]

Premises used: Set.sep_eq_of_subset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
inst : Finite.{u + 1} (↑s : Type u)
h : t ⊆ s
⊢ Finite.{u + 1} (↑{x : α | x ∈ s ∧ x ∈ t} : Type u)

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst : Finite.{u + 1} (↑t : Type u)
⊢ Finite.{u + 1} (↑(s ∩ t) : Type u)

Tactic:
Finite.Set.subset t inter_subset_right

Premises used: Finite.Set.subset, Set.inter_subset_right
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst : Finite.{u + 1} (↑s : Type u)
⊢ Finite.{u + 1} (↑(s ∩ t) : Type u)

Tactic:
Finite.Set.subset s inter_subset_left

Premises used: Finite.Set.subset, Set.inter_subset_left
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst : Finite.{u + 1} (↑s : Type u)
⊢ Finite.{u + 1} (↑(s \ t) : Type u)

Tactic:
Finite.Set.subset s diff_subset

Premises used: Finite.Set.subset, Set.diff_subset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst : Finite.{u + 1} (↑s : Type u)
⊢ Finite.{u + 1} (↑(insert a s) : Type u)

Tactic:
Finite.Set.finite_union {a} s

Premises used: Set.insert, Set.Mem, setOf, Finite.Set.finite_union, Set.singleton, Singleton.singleton
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
inst : Finite.{u + 1} (↑s : Type u)
intro : ∀ (val : Fintype (↑s : Type u)), Finite.{v + 1} (↑(f '' s) : Type v)
⊢ Finite.{v + 1} (↑(f '' s) : Type v)

Tactic:
cases nonempty_fintype s

Premises used: Set.Elem, nonempty_fintype
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
inst : Finite.{u + 1} (↑s : Type u)
val : Fintype (↑s : Type u)
⊢ Finite.{v + 1} (↑(f '' s) : Type v)

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
inst : Finite.{u + 1} (↑s : Type u)
val : Fintype (↑s : Type u)
⊢ Finite.{v + 1} (↑(f '' s) : Type v)

Tactic:
classical
  infer_instance
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : Subsingleton α
s : Set α
⊢ s.Finite

Tactic:
s.toFinite

Premises used: Set.toFinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : Finite α
⊢ Set.Finite.{u} (α := α) univ

Tactic:
Set.toFinite _

Premises used: Set.toFinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
⊢ Set.Finite.{u} (α := α) univ ↔ Finite α

Tactic:
(Equiv.Set.univ α).finite_iff

Premises used: Equiv.finite_iff, Set.Finite, Equiv.Set.univ
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
hs : s.Finite
t : Set α
ht : t ⊆ s
⊢ Finite.{u + 1} (↑s : Type u)

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

Tactic:
Finite.Set.subset _ ht

Premises used: Finite.Set.subset, Set.Finite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
hs : s.Finite
t : Set α
ht : t ⊆ s
this : Finite.{u + 1} (↑s : Type u)
⊢ t.Finite

Tactic:
exact Finite.Set.subset _ ht

Premises used: Finite.Set.subset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ Finite.{u + 1} (↑s : Type u)

Tactic:
rw [Set.Finite] at hs ht

Premises used: Set.Finite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
hs₁ : Finite.{u + 1} (↑s : Type u)
⊢ Finite.{u + 1} (↑t : Type u)

Tactic:
rw [Set.Finite] at hs ht

Premises used: Set.Finite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
hs : Finite.{u + 1} (↑s : Type u)
ht : Finite.{u + 1} (↑t : Type u)
⊢ (s ∪ t).Finite

Tactic:
apply toFinite

Premises used: Set.toFinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
rw : (s ∪ sᶜ).Finite
⊢ Finite α

Tactic:
rw [← finite_univ_iff, ← union_compl_self s]

Premises used: Set.union_compl_self, Set.finite_univ_iff
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ (s ∪ sᶜ).Finite

Tactic:
hs.union hsc

Premises used: Set.Finite.union
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ (s ∪ sᶜ).Finite

Tactic:
exact hs.union hsc

Premises used: Set.Finite.union
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
⊢ s.Finite → t.Finite → (s ⊔ t).Finite

Tactic:
Finite.union

Premises used: Set.Finite.union
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
hs : s.Finite
p : α → Prop
⊢ Set.Finite.{u} (α := α) {a : α | a ∈ s ∧ p a}

Tactic:
hs.subset <| sep_subset _ _

Premises used: Set.Finite.subset, Set.sep_subset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
hs : s.Finite
t : Set α
⊢ (s ∩ t).Finite

Tactic:
hs.subset inter_subset_left

Premises used: Set.inter_subset_left, Set.Finite.subset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
hs : s.Finite
t : Set α
⊢ (t ∩ s).Finite

Tactic:
hs.subset inter_subset_right

Premises used: Set.Finite.subset, Set.inter_subset_right
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
h : s.Finite
t : Set α
⊢ (s ⊓ t).Finite

Tactic:
h.inter_of_left t

Premises used: Set.Finite.inter_of_left
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
h : s.Finite
t : Set α
⊢ (t ⊓ s).Finite

Tactic:
h.inter_of_right t

Premises used: Set.Finite.inter_of_right
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
h : s ⊆ t
⊢ s.Infinite → t.Infinite

Tactic:
mt fun ht ↦ ht.subset h

Premises used: mt, Set.Finite.subset, Set.Infinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
hs : s.Finite
⊢ (s \ t).Finite

Tactic:
hs.subset diff_subset

Premises used: Set.diff_subset, Set.Finite.subset