awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : (t : Set γ) → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → (g : (m : ℕ) → m < n → γ) → γ :=
  fun (n : ℕ) (g : (m : ℕ) → m < n → γ) ↦ c (range fun (k : (↑(Iio n) : Type)) ↦ g (↑k : ℕ) ⋯)
u : ℕ → γ := fun (n : ℕ) ↦ n.strongRecOn' (P := fun (x : ℕ) ↦ γ) f
n : ℕ
⊢ u n = c (range fun (x : (↑(Iio n) : Type)) ↦ u (↑x : ℕ))

Tactic:
exact Nat.strongRecOn'_beta

Premises used: Nat.strongRecOn'_beta
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
⊢ Fintype.card.{u} (↑∅ : Type u) = 0

Tactic:
rfl

Premises used: Fintype.card, Multiset.zero, Multiset.ofList, Finset.card, Multiset.card, rfl
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
a : α
s : Set α
inst : Fintype (↑s : Type u)
h : a ∉ s
⊢ Fintype.card.{u} (↑(insert a s) : Type u) = Fintype.card.{u} (↑s : Type u) + 1

Tactic:
simp [Fintype.card_ofFinset]

Premises used: Fintype.card_ofFinset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
a : α
s : Set α
inst : Fintype (↑s : Type u)
h : a ∉ s
d : Fintype (↑(insert a s) : Type u)
rw : Fintype.card.{u} (↑(insert a s) : Type u) = Fintype.card.{u} (↑(insert a s) : Type u)
⊢ Fintype.card.{u} (↑(insert a s) : Type u) = Fintype.card.{u} (↑s : Type u) + 1

Tactic:
rw [← card_fintypeInsertOfNotMem s h]

Premises used: Set.card_fintypeInsertOfNotMem
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
a : α
s : Set α
inst : Fintype (↑s : Type u)
h : a ∉ s
d : Fintype (↑(insert a s) : Type u)
⊢ Fintype.card.{u} (↑(insert a s) : Type u) = Fintype.card.{u} (↑(insert a s) : Type u)

Tactic:
congr!
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
s : Set α
inst : Fintype (↑s : Type u)
f : α → β
inst_1 : Fintype (↑(f '' s) : Type v)
H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
this : (a : Prop) → Decidable a
⊢ ∀ (x : β), x ∈ Finset.image f s.toFinset ↔ x ∈ f '' s

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
s : Set α
inst : Fintype (↑s : Type u)
f : α → β
inst_1 : Fintype (↑(f '' s) : Type v)
H : Injective f
⊢ Fintype.card.{v} (↑(f '' s) : Type v) = Fintype.card.{u} (↑s : Type u)

Tactic:
card_image_of_inj_on fun _ _ _ _ h => H h

Premises used: Set.card_image_of_inj_on
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
a : α
⊢ Fintype.card.{u} (↑{a} : Type u) = 1

Tactic:
rfl

Premises used: Fintype.card, Multiset.cons, Multiset.ofList, Finset.card, Multiset.card, rfl
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
inst : Fintype (↑s : Type u)
inst_1 : Fintype (↑t : Type u)
h : s ⊂ t
⊢ Fintype.card.{u} (↑s : Type u) < Fintype.card.{u} (↑t : Type u)

Tactic:
Fintype.card_lt_of_injective_not_surjective (Set.inclusion h.1) (Set.inclusion_injective h.1)
    fun hst => (ssubset_iff_subset_ne.1 h).2 (eq_of_inclusion_surjective hst)

Premises used: Set.eq_of_inclusion_surjective, And.right, And.left, Set.inclusion_injective, Iff.mp, Set.inclusion, Fintype.card_lt_of_injective_not_surjective, ssubset_iff_subset_ne
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
inst : Fintype (↑s : Type u)
inst_1 : Fintype (↑t : Type u)
hsub : s ⊆ t
⊢ Fintype.card.{u} (↑s : Type u) ≤ Fintype.card.{u} (↑t : Type u)

Tactic:
Fintype.card_le_of_injective (Set.inclusion hsub) (Set.inclusion_injective hsub)

Premises used: Fintype.card_le_of_injective, Set.inclusion_injective, Set.inclusion
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
inst : Fintype (↑s : Type u)
inst_1 : Fintype (↑t : Type u)
hsub : s ⊆ t
hcard : Fintype.card.{u} (↑t : Type u) ≤ Fintype.card.{u} (↑s : Type u)
⊢ s = t

Tactic:
(eq_or_ssubset_of_subset hsub).elim id fun h => absurd hcard <| not_le_of_gt <| card_lt_card h

Premises used: id, Set.card_lt_card, absurd, eq_or_ssubset_of_subset, not_le_of_gt, Or.elim
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
inst : Fintype α
f : α → β
hf : Injective f
inst_1 : Fintype (↑(range f) : Type v)
⊢ Fintype.card.{v} (↑(range f) : Type v) = Fintype.card α

Tactic:
Eq.symm <| Fintype.card_congr <| Equiv.ofInjective f hf

Premises used: Fintype.card_congr, Equiv.ofInjective, Eq.symm
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
inst : Fintype (↑s : Type u)
h : s.Finite
⊢ h.toFinset (s := s).card = Fintype.card.{u} (↑s : Type u)

Tactic:
Eq.symm <| Fintype.card_of_finset' _ fun _ ↦ h.mem_toFinset

Premises used: Set.Finite.mem_toFinset, Fintype.card_of_finset', Eq.symm
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : Fintype α
a : α
inst_1 : Fintype (↑{x : α | x ≠ a} : Type u)
haveI : ∀ (this : DecidableEq α), Fintype.card.{u} (↑{x : α | x ≠ a} : Type u) = Fintype.card α - 1
⊢ Fintype.card.{u} (↑{x : α | x ≠ a} : Type u) = Fintype.card α - 1

Tactic:
haveI := Classical.decEq α
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : Fintype α
a : α
inst_1 : Fintype (↑{x : α | x ≠ a} : Type u)
this : DecidableEq α
rw : Finset.card.{u} (α := α) (toFinset {x : α | x ≠ a}) = Fintype.card α - 1
rw₁ : Finset.card.{u} (α := α) {x : α | x ≠ a} = Fintype.card α - 1
rw₂ : (Finset.erase Finset.univ a).card = Fintype.card α - 1
rw₃ : Finset.card.{u} (α := α) Finset.univ - 1 = Fintype.card α - 1
rw₄ rw₅ : Fintype.card α - 1 = Fintype.card α - 1
⊢ Fintype.card.{u} (↑{x : α | x ≠ a} : Type u) = Fintype.card α - 1

Tactic:
rw [← toFinset_card, toFinset_setOf, Finset.filter_ne',
    Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ]

Premises used: Finset.mem_univ, Finset.card_univ, Finset.card_erase_of_mem, Set.toFinset_card, Finset.filter_ne', Set.toFinset_setOf
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
rw : ¬Set.Finite.{u} (α := α) univ ↔ Infinite α
rw₁ : ¬Finite α ↔ Infinite α
rw₂ rw₃ : Infinite α ↔ Infinite α
⊢ Set.Infinite.{u} (α := α) univ ↔ Infinite α

Tactic:
rw [Set.Infinite, finite_univ_iff, not_finite_iff_infinite]

Premises used: not_finite_iff_infinite, Set.finite_univ_iff, Set.Infinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
h : Infinite α
⊢ Set.Infinite.{u} (α := α) univ

Tactic:
infinite_univ_iff.2 h

Premises used: Iff.mpr, Set.infinite_univ_iff
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
hs : s.Infinite
ht : t.Finite
by_contra! : ∀ (h : ∀ (a : α) (_ : a ∈ s), a ∈ t), False
⊢ ∃ a ∈ s, a ∉ t

Tactic:
by_contra! h
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
hs : s.Infinite
ht : t.Finite
h : ∀ (a : α) (_ : a ∈ s), a ∈ t
⊢ False

Tactic:
hs <| ht.subset h

Premises used: Set.Finite.subset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
hs : s.Infinite
ht : t.Finite
h : ∀ (a : α) (_ : a ∈ s), a ∈ t
⊢ False

Tactic:
exact hs <| ht.subset h

Premises used: Set.Finite.subset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
hs : s.Infinite
t : Finset α
⊢ ∃ a ∈ s, a ∉ t

Tactic:
hs.exists_notMem_finite t.finite_toSet

Premises used: Set.Infinite.exists_notMem_finite, Finset.finite_toSet
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
inst : Infinite α
hs : s.Finite
by_contra! : ∀ (h : ∀ (a : α), a ∈ s), False
⊢ ∃ (a : α), a ∉ s

Tactic:
by_contra! h
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
inst : Infinite α
hs : s.Finite
h : ∀ (a : α), a ∈ s
⊢ False

Tactic:
infinite_univ (hs.subset fun a _ ↦ h _)

Premises used: Set.Finite.subset, Set.infinite_univ
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
inst : Infinite α
hs : s.Finite
h : ∀ (a : α), a ∈ s
⊢ False

Tactic:
exact infinite_univ (hs.subset fun a _ ↦ h _)

Premises used: Set.Finite.subset, Set.infinite_univ
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : Infinite α
s : Finset α
⊢ ∃ (a : α), a ∉ s

Tactic:
s.finite_toSet.exists_notMem

Premises used: Set.Finite.exists_notMem, Finset.finite_toSet
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
hs : s.Infinite
n : ℕ
⊢ (↑(Finset.map (Embedding.subtype fun (x : α) ↦ x ∈ s) (Finset.map (natEmbedding s hs) (Finset.range n))) : Set α) ⊆
      s ∧
    (Finset.map (Embedding.subtype fun (x : α) ↦ x ∈ s) (Finset.map (natEmbedding s hs) (Finset.range n))).card = n

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

Tactic:
simpa using hs.union h

Premises used: Set.Finite.union
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : Infinite α
s : Set α
hs : s.Finite
h : sᶜ.Finite
⊢ Set.Finite.{u} (α := α) univ

Tactic:
simpa using hs.union h

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

Tactic:
fun h =>
  hs <| h.of_diff ht

Premises used: Not, Set.Finite.of_diff, Set.Infinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u_1
s t : Set α
hs : s.Infinite
ht : (s \ t).Finite
⊢ (s ∩ t).Infinite

Tactic:
simpa using hs.diff ht

Premises used: Set.Infinite.diff
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
⊢ (s ∪ t).Infinite ↔ s.Infinite ∨ t.Infinite

Tactic:
simp only [Set.Infinite, finite_union, not_and_or]

Premises used: Set.finite_union, not_and_or, Set.Infinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
hs : (f '' s).Infinite
⊢ s.Infinite

Tactic:
mt (Finite.image f) hs

Premises used: mt, Set.Finite.image, Set.Infinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
s : Set α
f : α → β
hi : InjOn f s
⊢ (f '' s).Infinite ↔ s.Infinite

Tactic:
not_congr <| finite_image_iff hi

Premises used: Set.finite_image_iff, not_congr, Set.Infinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ (range f).Infinite ↔ Infinite α

Tactic:
simpa using (finite_range_iff hf).not

Premises used: Set.finite_range_iff, Iff.not
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
s : Set α
t : Set β
f : α → β
hi : InjOn f s
hm : MapsTo f s t
hs : s.Infinite
⊢ t.Infinite

Tactic:
((infinite_image_iff hi).2 hs).mono (mapsTo_iff_image_subset.mp hm)

Premises used: Iff.mpr, Set.Infinite.mono, Set.mapsTo_iff_image_subset, Iff.mp, Set.infinite_image_iff
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
s : Set α
t : Set β
f : α → β
hs : s.Infinite
hf : MapsTo f s t
ht : t.Finite
contrapose! : ∀ (ht : ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), f x ≠ f y), t.Infinite
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

Tactic:
contrapose! ht
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
s : Set α
t : Set β
f : α → β
hs : s.Infinite
hf : MapsTo f s t
ht : ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), f x ≠ f y
⊢ t.Infinite

Tactic:
infinite_of_injOn_mapsTo (fun x hx y hy => not_imp_not.1 (ht x hx y hy)) hf hs

Premises used: Iff.mp, Set.infinite_of_injOn_mapsTo, not_imp_not
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
s : Set α
t : Set β
f : α → β
hs : s.Infinite
hf : MapsTo f s t
ht : ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), f x ≠ f y
⊢ t.Infinite

Tactic:
exact infinite_of_injOn_mapsTo (fun x hx y hy => not_imp_not.1 (ht x hx y hy)) hf hs

Premises used: Iff.mp, Set.infinite_of_injOn_mapsTo, not_imp_not
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
inst : Infinite α
f : α → β
hi : Injective f
rw : Set.Infinite.{u} (α := α) univ
⊢ (range f).Infinite

Tactic:
rw [← image_univ, infinite_image_iff hi.injOn]

Premises used: Set.image_univ, Function.Injective.injOn, Set.infinite_image_iff
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
inst : Infinite α
f : α → β
hi : Injective f
⊢ Set.Infinite.{u} (α := α) univ

Tactic:
infinite_univ

Premises used: Set.infinite_univ
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
inst : Infinite α
f : α → β
hi : Injective f
⊢ Set.Infinite.{u} (α := α) univ

Tactic:
exact infinite_univ

Premises used: Set.infinite_univ
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
inst : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : ∀ (x : α), f x ∈ s
⊢ range f ⊆ s

Tactic:
rw [← range_subset_iff] at hf

Premises used: Set.range_subset_iff
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
inst : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : range f ⊆ s
⊢ s.Infinite

Tactic:
(infinite_range_of_injective hi).mono hf

Premises used: Set.Infinite.mono, Set.infinite_range_of_injective
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
inst : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : range f ⊆ s
⊢ s.Infinite

Tactic:
exact (infinite_range_of_injective hi).mono hf

Premises used: Set.Infinite.mono, Set.infinite_range_of_injective
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
⊢ Finite.{v + 1} (↑(f '' s) : Type v)

Tactic:
have : Finite (f '' s) := finite_coe_iff.mpr h_fin
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this : Finite.{v + 1} (↑(f '' s) : Type v)
⊢ Infinite.{u + 1} (↑s : Type u)

Tactic:
have : Infinite s := infinite_coe_iff.mpr h_inf
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this_1 : Finite.{v + 1} (↑(f '' s) : Type v)
this : Infinite.{u + 1} (↑s : Type u)
⊢ ¬Injective (β := (↑(f '' s) : Type v)) (codRestrict (s.restrict (π := fun (a : α) ↦ β) f) (f '' s) ⋯)

Tactic:
have h := not_injective_infinite_finite
            ((f '' s).codRestrict (s.restrict f) fun x => ⟨x, x.property, rfl⟩)
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this_1 : Finite.{v + 1} (↑(f '' s) : Type v)
this : Infinite.{u + 1} (↑s : Type u)
h : ¬Injective (β := (↑(f '' s) : Type v)) (codRestrict (s.restrict (π := fun (a : α) ↦ β) f) (f '' s) ⋯)
contrapose :
  ∀ (h : InjOn f s),
    Injective (β := (↑(f '' s) : Type v)) (codRestrict (s.restrict (π := fun (a : α) ↦ β) f) (f '' s) ⋯)
⊢ ¬InjOn f s

Tactic:
contrapose h
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this_1 : Finite.{v + 1} (↑(f '' s) : Type v)
this : Infinite.{u + 1} (↑s : Type u)
h : InjOn f s
rwa : Injective (s.restrict (π := fun (a : α) ↦ β) f)
rwa₁ rwa₂ rwa₃ rwa₄ : InjOn f s
⊢ Injective (β := (↑(f '' s) : Type v)) (codRestrict (s.restrict (π := fun (a : α) ↦ β) f) (f '' s) ⋯)

Tactic:
rwa [injective_codRestrict, ← injOn_iff_injective]

Premises used: Set.injective_codRestrict, Set.injOn_iff_injective
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
P : α → ℕ → Prop
inst : (x : α) → DecidablePred (P x)
b : ℕ
⊢ Set.Finite (α := ℕ) (range fun (x : α) ↦ Nat.findGreatest (P x) b)

Tactic:
(finite_le_nat b).subset <| range_subset_iff.2 fun _ => Nat.findGreatest_le _

Premises used: Iff.mpr, Set.Finite.subset, Set.range_subset_iff, Nat.findGreatest_le, Set.finite_le_nat
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : Infinite α
n : ℕ
obtain : ∀ (s : Finset α), ∃ (s_1 : Finset α), #s_1 = #s + 1
⊢ ∃ (s : Finset α), #s = n + 1

Tactic:
obtain ⟨s, rfl⟩ := exists_card_eq n

Premises used: rfl
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : Infinite α
s : Finset α
obtain : ∀ (a : α) (ha : a ∉ s), ∃ (s_1 : Finset α), #s_1 = #s + 1
⊢ ∃ (s_1 : Finset α), #s_1 = #s + 1

Tactic:
obtain ⟨a, ha⟩ := s.exists_notMem

Premises used: Finset.exists_notMem
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : Infinite α
s : Finset α
a : α
ha : a ∉ s
⊢ ∃ (s_1 : Finset α), #s_1 = #s + 1

Tactic:
⟨insert a s, card_insert_of_notMem ha⟩

Premises used: Insert.insert, Finset.card_insert_of_notMem, Exists.intro
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : Infinite α
s : Finset α
a : α
ha : a ∉ s
⊢ ∃ (s_1 : Finset α), #s_1 = #s + 1

Tactic:
exact ⟨insert a s, card_insert_of_notMem ha⟩
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : Infinite α
n : ℕ
obtain : ∀ (s : Finset α), ∃ (s_1 : Finset α), #s_1 = #s + 1
obtain₁ : ∀ (s : Finset α) (a : α) (ha : a ∉ s), ∃ (s_1 : Finset α), #s_1 = #s + 1
⊢ ∃ (s : Finset α), #s = n + 1

Tactic:
classical
    obtain ⟨s, rfl⟩ := exists_card_eq n
    obtain ⟨a, ha⟩ := s.exists_notMem
    exact ⟨insert a s, card_insert_of_notMem ha⟩

Premises used: rfl
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s (↑t : Set β)
obtain :
  ∀ (u : Set α) (hus : u ⊆ s) (hf : InjOn f u) (himg : f '' u = (↑t : Set β)),
    ∃ (u : Finset α), (↑u : Set α) ⊆ s ∧ InjOn f (↑u : Set α) ∧ image f u = t
⊢ ∃ (u : Finset α), (↑u : Set α) ⊆ s ∧ InjOn f (↑u : Set α) ∧ image f u = t

Tactic:
obtain ⟨u, hus, hf, himg⟩ := hfs.exists_subset_injOn_image_eq

Premises used: Set.SurjOn.exists_subset_injOn_image_eq
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s (↑t : Set β)
u : Set α
hus : u ⊆ s
hf : InjOn f u
himg : f '' u = (↑t : Set β)
⊢ (f '' u).Finite

Tactic:
simp [himg]
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s (↑t : Set β)
u : Set α
hus : u ⊆ s
hf : InjOn f u
himg : f '' u = (↑t : Set β)
⊢ (↑(⋯.toFinset (s := u)) : Set α) ⊆ s

Tactic:
simpa
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s (↑t : Set β)
u : Set α
hus : u ⊆ s
hf : InjOn f u
himg : f '' u = (↑t : Set β)
⊢ InjOn f (↑(⋯.toFinset (s := u)) : Set α)

Tactic:
simpa
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s (↑t : Set β)
u : Set α
hus : u ⊆ s
hf : InjOn f u
himg : f '' u = (↑t : Set β)
refine : image f (⋯.toFinset (s := u)) = t
⊢ ∃ (u : Finset α), (↑u : Set α) ⊆ s ∧ InjOn f (↑u : Set α) ∧ image f u = t

Tactic:
refine ⟨(Finite.of_finite_image (by simp [himg]) hf).toFinset, by simpa, by simpa, ?_⟩
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s (↑t : Set β)
u : Set α
hus : u ⊆ s
hf : InjOn f u
himg : f '' u = (↑t : Set β)
⊢ image f (⋯.toFinset (s := u)) = t

Tactic:
simpa [← Finset.coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
h_1 : Nontrivial α
rcases : ∀ (x y : α) (hne : x ≠ y), Finite α
⊢ Finite α

Tactic:
rcases exists_pair_ne α with ⟨x, y, hne⟩

Premises used: exists_pair_ne
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
h_1 : Nontrivial α
x y : α
hne : x ≠ y
⊢ Finite α

Tactic:
@Finite.of_fintype α ⟨{x, y}, fun z => ?_⟩

Premises used: Finite.of_fintype
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
h_1 : Nontrivial α
x y : α
hne : x ≠ y
refine : ∀ (z : α), Membership.mem (γ := Finset α) {x, y} z
⊢ Finite α

Tactic:
refine @Finite.of_fintype α ⟨{x, y}, fun z => ?_⟩

Premises used: Finite.of_fintype
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
h_1 : Nontrivial α
x y : α
hne : x ≠ y
z : α
⊢ Membership.mem (γ := Finset α) {x, y} z

Tactic:
simpa [hne] using eq_or_eq_or_eq_of_forall_not_lt_lt h z x y

Premises used: eq_or_eq_or_eq_of_forall_not_lt_lt
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : LinearOrder α
s : Set α
h : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ s, x < y → y < z → False
⊢ ∀ ⦃x y z : (↑s : Type u)⦄, x < y → y < z → False

Tactic:
simpa only [SetCoe.forall'] using h

Premises used: SetCoe.forall'
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst : DecidableEq α
inst_1 : Fintype (PLift ι)
f : ι → Set α
inst_2 : (i : ι) → Fintype (↑(f i) : Type u)
⊢ ∀ (x : α),
    Membership.mem (γ := Finset α) (Finset.biUnion Finset.univ fun (i : PLift ι) ↦ (f i.down).toFinset) x ↔
      Membership.mem (γ := Set α) (⋃ (i : ι), f i) x

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst : DecidableEq α
s : Set (Set α)
inst_1 : Fintype (↑s : Type u)
H : (t : (↑s : Type u)) → Fintype (↑(↑t : Set α) : Type u)
rw : Fintype (↑(⋃ (i : (↑s : Type u)), (↑i : Set α)) : Type u)
⊢ Fintype (↑(⋃₀ s) : Type u)

Tactic:
rw [sUnion_eq_iUnion]

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst : DecidableEq α
s : Set (Set α)
inst_1 : Fintype (↑s : Type u)
H : (t : (↑s : Type u)) → Fintype (↑(↑t : Set α) : Type u)
⊢ Fintype (↑(⋃ (i : (↑s : Type u)), (↑i : Set α)) : Type u)

Tactic:
exact @Set.fintypeiUnion _ _ _ _ _ H

Premises used: Set.fintypeiUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
inst : Fintype β
inst_1 : DecidableEq α
f : β → Set α
inst_2 : (w : β) → Fintype (↑(f w) : Type u)
h :
  ∀ (v : α),
    Membership.mem (γ := Finset α) (toFinset (⋃ (x : β), f x)) v ↔
      Membership.mem (γ := Finset α) (Finset.biUnion Finset.univ fun (x : β) ↦ (f x).toFinset) v
⊢ Eq.{u + 1} (α := Finset α) (toFinset (⋃ (x : β), f x)) (Finset.biUnion Finset.univ fun (x : β) ↦ (f x).toFinset)

Tactic:
ext v
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
inst : Fintype β
inst_1 : DecidableEq α
f : β → Set α
inst_2 : (w : β) → Fintype (↑(f w) : Type u)
v : α
⊢ Membership.mem (γ := Finset α) (toFinset (⋃ (x : β), f x)) v ↔
    Membership.mem (γ := Finset α) (Finset.biUnion Finset.univ fun (x : β) ↦ (f x).toFinset) v

Tactic:
simp only [mem_toFinset, mem_iUnion, Finset.mem_biUnion, Finset.mem_univ, true_and]

Premises used: Finset.mem_univ, Set.mem_iUnion, Set.mem_toFinset, Finset.mem_biUnion, true_and
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
ι_1 : Sort w
γ : Type x
inst : DecidableEq α
ι : Type u_1
s : Set ι
inst_1 : Fintype (↑s : Type u_1)
t : ι → Set α
H : (i : ι) → i ∈ s → Fintype (↑(t i) : Type u)
this : (i : ↥s.toFinset) → Fintype (↑(t (↑i : ι)) : Type u)
x : α
⊢ Membership.mem (γ := Finset α) (s.toFinset.attach.biUnion fun (x : ↥s.toFinset) ↦ (t (↑x : ι)).toFinset) x ↔
    Membership.mem (γ := Set α) (⋃ x ∈ s, t x) x

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
ι_1 : Sort w
γ : Type x
inst : DecidableEq α
ι : Type u_1
s : Set ι
inst_1 : Fintype (↑s : Type u_1)
t : ι → Set α
inst_2 : (i : ι) → Fintype (↑(t i) : Type u)
⊢ ∀ (x : α),
    Membership.mem (γ := Finset α) (s.toFinset.biUnion fun (x : ι) ↦ (t x).toFinset) x ↔
      Membership.mem (γ := Set α) (⋃ x ∈ s, t x) x

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

Tactic:
have : Fintype (PLift ι) := Fintype.ofFinite _
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst : Finite ι
f : ι → Set α
inst_1 : ∀ (i : ι), Finite.{u + 1} (↑(f i) : Type u)
this : Fintype (PLift ι)
have : ∀ (this : (i : ι) → Fintype (↑(f i) : Type u)), Finite.{u + 1} (↑(⋃ (i : ι), f i) : Type u)
⊢ Finite.{u + 1} (↑(⋃ (i : ι), f i) : Type u)

Tactic:
have : ∀ i, Fintype (f i) := fun i => Fintype.ofFinite _