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

Tactic:
(hd.union ht).subset <| subset_diff_union _ _

Premises used: Set.Finite.union, Set.Finite.subset, Set.subset_diff_union
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∆ t).Finite

Tactic:
hs.diff.union ht.diff

Premises used: Set.Finite.union, Set.Finite.diff, symmDiff
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
⊢ Set.Finite.{u} (α := α) ∅

Tactic:
toFinite _

Premises used: Set.toFinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
h : Set.Infinite.{u} (α := α) ∅
⊢ False

Tactic:
h finite_empty

Premises used: Set.finite_empty
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
h : Set.Infinite.{u} (α := α) ∅
⊢ False

Tactic:
exact h finite_empty

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

Tactic:
toFinite _

Premises used: Set.toFinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
a : α
s : Set α
hs : s.Finite
⊢ (insert a s).Finite

Tactic:
(finite_singleton a).union hs

Premises used: Set.Finite.union, Set.insert, Set.Mem, setOf, Set.singleton, Set.finite_singleton
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
s : Set α
f : α → β
hs : s.Finite
⊢ Finite.{u + 1} (↑s : Type u)

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

Tactic:
apply toFinite

Premises used: Set.toFinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
s : Set α
t : Set β
f : α → β
hf : SurjOn f s t
hs : s.Finite
⊢ t.Finite

Tactic:
(hs.image _).subset hf

Premises used: Set.Finite.subset, Set.Finite.image
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α β : Type u_1
s : Set α
⊢ ∀ (f : α → β), s.Finite → (f <$> s).Finite

Tactic:
Finite.image

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

Tactic:
have := h.to_subtype
  .of_injective _ hi.bijOn_image.bijective.injective

Premises used: Set.Finite, Set.InjOn.bijOn_image, Function.Bijective.injective, Set.Finite.to_subtype, Set.BijOn.mapsTo, Set.image, Set.BijOn.bijective, Set.MapsTo.restrict, Finite.of_injective
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
hm : MapsTo f s t
hi : InjOn f s
ht : t.Finite
⊢ s.Finite

Tactic:
.of_finite_image (ht.subset (image_subset_iff.mpr hm)) hi

Premises used: Iff.mpr, Set.Finite.subset, Set.Finite.of_finite_image, Set.image_subset_iff
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : BijOn f s t
⊢ s.Finite ↔ t.Finite

Tactic:
⟨fun h1 ↦ h1.of_surjOn _ h.2.2, fun h1 ↦ h1.of_injOn h.1 h.2.1⟩

Premises used: And.right, And.left, Set.Finite.of_injOn, Iff.intro, Set.Finite.of_surjOn
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : (f ⁻¹' s).Finite
hs : s ⊆ range f
rw : (f '' f ⁻¹' s).Finite
⊢ s.Finite

Tactic:
rw [← image_preimage_eq_of_subset hs]

Premises used: Set.image_preimage_eq_of_subset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : (f ⁻¹' s).Finite
hs : s ⊆ range f
⊢ (f '' f ⁻¹' s).Finite

Tactic:
Finite.image f h

Premises used: Set.Finite.image
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : (f ⁻¹' s).Finite
hs : s ⊆ range f
⊢ (f '' f ⁻¹' s).Finite

Tactic:
exact Finite.image f h

Premises used: Set.Finite.image
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : (f ⁻¹' s).Finite
hf : Surjective f
⊢ s.Finite

Tactic:
hf.image_preimage s ▸ h.image _

Premises used: Eq.rec, Set.Finite.image, Function.Surjective.image_preimage
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
I : InjOn f (f ⁻¹' s)
h : s.Finite
⊢ (f ⁻¹' s).Finite

Tactic:
(h.subset (image_preimage_subset f s)).of_finite_image I

Premises used: Set.Finite.subset, Set.Finite.of_finite_image, Set.image_preimage_subset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
hs : s.Infinite
hf : s ⊆ range f
⊢ (f ⁻¹' s).Infinite

Tactic:
fun h ↦ hs <| finite_of_finite_preimage h hf

Premises used: Set.finite_of_finite_preimage, Not, Set.Infinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
hs : (s ∩ range f).Infinite
⊢ (f ⁻¹' s).Infinite

Tactic:
(hs.preimage inter_subset_right).mono <| preimage_mono inter_subset_left

Premises used: Set.Infinite.mono, Set.inter_subset_left, Set.Infinite.preimage, Set.preimage_mono, Set.inter_subset_right
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
s : Set β
f : α ↪ β
h : s.Finite
⊢ Set.Finite.{u} (α := α) ((⇑f : (a : α) → β) ⁻¹' s)

Tactic:
h.preimage fun _ _ _ _ h' => f.injective h'

Premises used: Function.Embedding.injective, Set.Finite.preimage
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
n : ℕ
⊢ Set.Finite (α := ℕ) {i : ℕ | i < n}

Tactic:
toFinite _

Premises used: Set.toFinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
n : ℕ
⊢ Set.Finite (α := ℕ) {i : ℕ | i ≤ n}

Tactic:
toFinite _

Premises used: Set.toFinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
⊢ SurjOn f s s ↔ BijOn f s s

Tactic:
⟨fun h ↦ ⟨hm, ?_, h⟩, BijOn.surjOn⟩

Premises used: Set.BijOn.surjOn, And.intro, Iff.intro
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
refine : ∀ (h : SurjOn f s s), InjOn f s
⊢ SurjOn f s s ↔ BijOn f s s

Tactic:
refine ⟨fun h ↦ ⟨hm, ?_, h⟩, BijOn.surjOn⟩
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : SurjOn f s s
⊢ Finite.{u + 1} (↑s : Type u)

Tactic:
have : Finite s := finite_coe_iff.mpr hs
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : SurjOn f s s
this : Finite.{u + 1} (↑s : Type u)
⊢ InjOn f s

Tactic:
hm.restrict_inj.mp (Finite.injective_iff_surjective.mpr <| hm.restrict_surjective_iff.mpr h)

Premises used: Iff.mpr, Iff.mp, Finite.injective_iff_surjective, Set.MapsTo.restrict_surjective_iff, Set.MapsTo.restrict_inj
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : SurjOn f s s
this : Finite.{u + 1} (↑s : Type u)
⊢ InjOn f s

Tactic:
exact hm.restrict_inj.mp (Finite.injective_iff_surjective.mpr <| hm.restrict_surjective_iff.mpr h)

Premises used: Iff.mpr, Iff.mp, Finite.injective_iff_surjective, Set.MapsTo.restrict_surjective_iff, Set.MapsTo.restrict_inj
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
⊢ InjOn f s ↔ BijOn f s s

Tactic:
⟨fun h ↦ ⟨hm, h, ?_⟩, BijOn.injOn⟩

Premises used: Set.BijOn.injOn, And.intro, Iff.intro
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
refine : ∀ (h : InjOn f s), SurjOn f s s
⊢ InjOn f s ↔ BijOn f s s

Tactic:
refine ⟨fun h ↦ ⟨hm, h, ?_⟩, BijOn.injOn⟩
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : InjOn f s
⊢ Finite.{u + 1} (↑s : Type u)

Tactic:
have : Finite s := finite_coe_iff.mpr hs
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : InjOn f s
this : Finite.{u + 1} (↑s : Type u)
⊢ SurjOn f s s

Tactic:
hm.restrict_surjective_iff.mp (Finite.injective_iff_surjective.mp <| hm.restrict_inj.mpr h)

Premises used: Iff.mpr, Iff.mp, Finite.injective_iff_surjective, Set.MapsTo.restrict_surjective_iff, Set.MapsTo.restrict_inj
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : InjOn f s
this : Finite.{u + 1} (↑s : Type u)
⊢ SurjOn f s s

Tactic:
exact hm.restrict_surjective_iff.mp (Finite.injective_iff_surjective.mp <| hm.restrict_inj.mpr h)

Premises used: Iff.mpr, Iff.mp, Finite.injective_iff_surjective, Set.MapsTo.restrict_surjective_iff, Set.MapsTo.restrict_inj
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Finset α
⊢ Set.Finite.{u} (α := α) {a : α | a ∈ s}

Tactic:
toFinite _

Premises used: Set.toFinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
h : s.Subsingleton
⊢ s.Finite

Tactic:
h.induction_on finite_empty finite_singleton

Premises used: Set.finite_empty, Set.Subsingleton.induction_on, Set.finite_singleton
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set α
hs : s.Infinite
⊢ s.Nontrivial

Tactic:
not_subsingleton_iff.1 <| mt Subsingleton.finite hs

Premises used: Set.not_subsingleton_iff, mt, Iff.mp, Set.Subsingleton.finite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
s : Set (α ⊕ β)
⊢ (Sum.inl ⁻¹' s).Finite ∧ (Sum.inr ⁻¹' s).Finite ↔ s.Finite

Tactic:
⟨fun h => image_preimage_inl_union_image_preimage_inr s ▸ (h.1.image _).union (h.2.image _),
    fun h => ⟨h.preimage Sum.inl_injective.injOn, h.preimage Sum.inr_injective.injOn⟩⟩

Premises used: Set.Finite.union, Sum.inr_injective, Set.image_preimage_inl_union_image_preimage_inr, Function.Injective.injOn, Sum.inl_injective, Eq.rec, Sum.inl, Set.Finite.image, And.right, And.left, Sum.inr, And.intro, Iff.intro, Set.Finite.preimage
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
p : Set α → Prop
⊢ (∃ (s : Set α), s.Finite ∧ p s) ↔ ∃ (s : Finset α), p (↑s : Set α)

Tactic:
⟨fun ⟨_, hs, hps⟩ => ⟨hs.toFinset, hs.coe_toFinset.symm ▸ hps⟩, fun ⟨s, hs⟩ =>
    ⟨s, s.finite_toSet, hs⟩⟩

Premises used: Set.Finite, Exists, Eq.rec, Set.Finite.coe_toFinset, And, SetLike.coe, _private.0.Set.exists_finite_iff_finset.match_1, Set.Finite.toFinset, And.intro, Iff.intro, Exists.intro, Finset.finite_toSet, Eq.symm, _private.0.Set.exists_finite_iff_finset.match_2
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
simp_rw :
  (∃ (s_1 : Finset β), (∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ Finset.image f s' = s_1) ∧ p (↑s_1 : Set β)) ↔
    ∃ (s_1 : Finset α), (↑s_1 : Set α) ⊆ s ∧ p (f '' (↑s_1 : Set α))
⊢ (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)

Tactic:
simp_rw [@and_comm (_ ⊆ _), and_assoc, exists_finite_iff_finset, @and_comm (p _),
    Finset.subset_set_image_iff]

Premises used: and_comm, Finset.subset_set_image_iff, and_assoc, Set.exists_finite_iff_finset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ (s_1 : Finset β), (∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ Finset.image f s' = s_1) ∧ p (↑s_1 : Set β)) ↔
    ∃ (s_1 : Finset α), (↑s_1 : Set α) ⊆ s ∧ p (f '' (↑s_1 : Set α))

Tactic:
aesop
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
simp_rw : (∃ (t : Set β), (t.Finite ∧ p t) ∧ t ⊆ f '' s) ↔ ∃ (t : Set α), (t.Finite ∧ p (f '' t)) ∧ t ⊆ s
simp_rw₁ : (∃ (t : Set β), t.Finite ∧ p t ∧ t ⊆ f '' s) ↔ ∃ (t : Set α), t.Finite ∧ p (f '' t) ∧ t ⊆ s
simp_rw₂ :
  (∃ (s_1 : Finset β), p (↑s_1 : Set β) ∧ (↑s_1 : Set β) ⊆ f '' s) ↔
    ∃ (s_1 : Finset α), p (f '' (↑s_1 : Set α)) ∧ (↑s_1 : Set α) ⊆ s
simp_rw₃ :
  (∃ (s_1 : Finset β), (↑s_1 : Set β) ⊆ f '' s ∧ p (↑s_1 : Set β)) ↔
    ∃ (s_1 : Finset α), (↑s_1 : Set α) ⊆ s ∧ p (f '' (↑s_1 : Set α))
simp_rw₄ :
  (∃ (s_1 : Finset β), (∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ Finset.image f s' = s_1) ∧ p (↑s_1 : Set β)) ↔
    ∃ (s_1 : Finset α), (↑s_1 : Set α) ⊆ s ∧ p (f '' (↑s_1 : Set α))
⊢ (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)

Tactic:
classical
  simp_rw [@and_comm (_ ⊆ _), and_assoc, exists_finite_iff_finset, @and_comm (p _),
    Finset.subset_set_image_iff]
  aesop

Premises used: and_comm, Finset.subset_set_image_iff, and_assoc, Set.exists_finite_iff_finset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
p : α → Prop
inst : DecidablePred p
f g : α → β
hf : (range f).Finite
hg : (range g).Finite
⊢ Set.Finite.{v} (α := β) (range fun (x : α) ↦ if p x then f x else g x)

Tactic:
(hf.union hg).subset range_ite_subset

Premises used: Set.Finite.union, Set.Finite.subset, Set.range_ite_subset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
c : β
⊢ Set.Finite.{v} (α := β) (range fun (x : α) ↦ c)

Tactic:
(finite_singleton c).subset range_const_subset

Premises used: Set.range_const_subset, Set.Finite.subset, Set.finite_singleton
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s t : Set α
⊢ (s ∪ t).Finite ↔ s.Finite ∧ t.Finite

Tactic:
⟨fun h => ⟨h.subset subset_union_left, h.subset subset_union_right⟩, fun ⟨hs, ht⟩ =>
    hs.union ht⟩

Premises used: Set.Finite.union, _private.0.Set.finite_union.match_1, Set.subset_union_right, Set.Finite, Set.Finite.subset, Set.subset_union_left, And.intro, Iff.intro, Union.union
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
s : Set α
f : α → β
hi : InjOn f s
⊢ (f '' s).Finite ↔ s.Finite

Tactic:
⟨fun h => h.of_finite_image hi, Finite.image _⟩

Premises used: Set.Finite.image, Set.Finite.of_finite_image, Iff.intro
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ (range f).Finite ↔ Finite α

Tactic:
simpa [finite_univ_iff] using finite_image_iff (s := univ) hf.injOn

Premises used: Function.Injective.injOn, Set.finite_image_iff, Set.finite_univ_iff
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
⊢ Set.Finite.{u} (α := α) univ ↔ Nonempty.{u + 1} (Fintype α)

Tactic:
⟨fun h => ⟨fintypeOfFiniteUniv h⟩, fun ⟨_i⟩ => finite_univ⟩

Premises used: Set.fintypeOfFiniteUniv, Set.univ, Set.Finite, Nonempty.intro, Set.finite_univ, Iff.intro, _private.0.Set.univ_finite_iff_nonempty_fintype.match_1
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
a : α
ha : Set.Finite (α := α) {a}
⊢ ha.toFinset (s := {a}) = {a}

Tactic:
Set.toFinite_toFinset _

Premises used: Multiset.map, List.map, Finset.map, Set.toFinite_toFinset, Multiset.cons, Set.toFinset, Multiset.ofList
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : DecidableEq α
s : Set α
a : α
hs : (insert a s).Finite
⊢ ∀ (a_1 : α), a_1 ∈ hs.toFinset (s := insert a s) ↔ a_1 ∈ insert a (⋯.toFinset (s := s))

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
inst : DecidableEq α
a : α
s : Set α
hs : s.Finite
⊢ ⋯.toFinset (s := insert a s) = insert a (hs.toFinset (s := s))

Tactic:
Finite.toFinset_insert _

Premises used: Set.Finite.toFinset_insert
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
s : Set (Option α)
⊢ s.Finite ↔ Set.Finite.{u} (α := α) {x : α | some x ∈ s}

Tactic:
⟨fun h => h.preimage_embedding Embedding.some, fun h =>
    ((h.image some).insert none).subset fun x =>
      x.casesOn (fun _ => Or.inl rfl) fun _ hx => Or.inr <| mem_image_of_mem _ hx⟩

Premises used: Function.Embedding.some, Set.Finite.preimage_embedding, Option.casesOn, Option.some, Set.Finite.subset, Set.Finite.image, Option.none, Iff.intro, Set.Finite.insert
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
⊢ s.Finite

Tactic:
hs
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
lift : ∀ (s : Finset α) (hs : (↑s : Set α).Finite), motive (↑s : Set α) hs
⊢ motive s hs

Tactic:
lift s to Finset α using hs

Premises used: Finset
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
hs : (↑∅ : Set α).Finite
⊢ motive (↑∅ : Set α) hs

Tactic:
simpa
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
a : α
s : Finset α
ha : a ∉ s
ih : ∀ (hs : (↑s : Set α).Finite), motive (↑s : Set α) hs
hs : (↑(Finset.cons a s ha) : Set α).Finite
⊢ motive (↑(Finset.cons a s ha) : Set α) hs

Tactic:
simpa using @insert a s ha (Set.toFinite _) (ih _)

Premises used: Set.toFinite
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
s : Finset α
hs : (↑s : Set α).Finite
empty₁ : ∀ (hs : (↑∅ : Set α).Finite), motive (↑∅ : Set α) hs
cons :
  ∀ (a : α) (s : Finset α) (ha : a ∉ s) (ih : ∀ (hs : (↑s : Set α).Finite), motive (↑s : Set α) hs)
    (hs : (↑(Finset.cons a s ha) : Set α).Finite), motive (↑(Finset.cons a s ha) : Set α) hs
⊢ motive (↑s : Set α) hs

Tactic:
induction s using Finset.cons_induction_on with
  | empty => simpa
  | cons a s ha ih => simpa using @insert a s ha (Set.toFinite _) (ih _)
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
⊢ motive s hs

Tactic:
Set.Finite.induction_on (motive := fun t _ => ∀ hts : t ⊆ s, motive t (hs.subset hts)) s hs
    (fun _ => empty) ?_ .rfl

Premises used: Set.Finite.induction_on, Set.Subset.rfl
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
refine :
  ∀ {a : α} {s_1 : Set α},
    a ∉ s_1 →
      ∀ (hs_1 : s_1.Finite),
        (fun (t : Set α) (x : t.Finite) ↦ ∀ (hts : t ⊆ s), motive t ⋯) s_1 hs_1 →
          (fun (t : Set α) (x : t.Finite) ↦ ∀ (hts : t ⊆ s), motive t ⋯) (Insert.insert a s_1) ⋯
⊢ motive s hs

Tactic:
refine Set.Finite.induction_on (motive := fun t _ => ∀ hts : t ⊆ s, motive t (hs.subset hts)) s hs
    (fun _ => empty) ?_ .rfl

Premises used: Set.Finite.induction_on, Set.Subset.rfl
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s_1 : Set α
hs : s_1.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s_1 → ∀ (hts : t ⊆ s_1), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
has : a ∉ s
_ :
  ∀ (hs_1 : s.Finite),
    (fun (t : Set α) (x : t.Finite) ↦ ∀ (hts : t ⊆ s_1), motive t ⋯) s hs_1 →
      (fun (t : Set α) (x : t.Finite) ↦ ∀ (hts : t ⊆ s_1), motive t ⋯) (Insert.insert a s) ⋯
⊢ ∀ (hs_1 : s.Finite),
    (fun (t : Set α) (x : t.Finite) ↦ ∀ (hts : t ⊆ s_1), motive t ⋯) s hs_1 →
      (fun (t : Set α) (x : t.Finite) ↦ ∀ (hts : t ⊆ s_1), motive t ⋯) (Insert.insert a s) ⋯

Tactic:
_
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s_1 : Set α
hs : s_1.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s_1 → ∀ (hts : t ⊆ s_1), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
has : a ∉ s
hs_1 : s.Finite
hCs : ∀ (hts : s ⊆ s_1), motive s ⋯
haS : Insert.insert a s ⊆ s_1
⊢ a ∈ s_1 ∧ s ⊆ s_1

Tactic:
rw [insert_subset_iff] at haS

Premises used: Set.insert_subset_iff
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s_1 : Set α
hs : s_1.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s_1 → ∀ (hts : t ⊆ s_1), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
has : a ∉ s
hs_1 : s.Finite
hCs : ∀ (hts : s ⊆ s_1), motive s ⋯
haS_1 : Insert.insert a s ⊆ s_1
haS : a ∈ s_1 ∧ s ⊆ s_1
⊢ motive (Insert.insert a s) ⋯

Tactic:
insert haS.1 haS.2 has (hCs haS.2)

Premises used: And.right, And.left
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s_1 : Set α
hs : s_1.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s_1 → ∀ (hts : t ⊆ s_1), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
has : a ∉ s
hs_1 : s.Finite
hCs : ∀ (hts : s ⊆ s_1), motive s ⋯
haS_1 : Insert.insert a s ⊆ s_1
haS : a ∈ s_1 ∧ s ⊆ s_1
⊢ motive (Insert.insert a s) ⋯

Tactic:
exact insert haS.1 haS.2 has (hCs haS.2)

Premises used: And.right, And.left
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
γ : Type u_1
P : γ → Set γ → Prop
h : ∀ (t : Set γ), t.Finite → ∃ (c : γ), P c t
⊢ Nonempty γ

Tactic:
haveI : Nonempty γ := (h ∅ finite_empty).nonempty
-- Module: Mathlib.Data.Set.Finite.Basic
Goal:
γ : Type u_1
P : γ → Set γ → Prop
h : ∀ (t : Set γ), t.Finite → ∃ (c : γ), P c t
this : Nonempty γ
choose! :
  ∀ (c : (t : Set γ) → γ) (hc : ∀ (t : Set γ), t.Finite → P (c t) t), ∃ (u : ℕ → γ), ∀ (n : ℕ), P (u n) (u '' Iio n)
⊢ ∃ (u : ℕ → γ), ∀ (n : ℕ), P (u n) (u '' Iio n)

Tactic:
choose! c hc using h
-- 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
⊢ ∃ (u : ℕ → γ), ∀ (n : ℕ), P (u n) (u '' Iio n)

Tactic:
⟨u, fun n => ?_⟩

Premises used: Exists.intro
-- 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
refine : ∀ (n : ℕ), P (u n) (u '' Iio n)
⊢ ∃ (u : ℕ → γ), ∀ (n : ℕ), P (u n) (u '' Iio n)

Tactic:
refine ⟨u, fun n => ?_⟩
-- 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 : ℕ
⊢ P (c (u '' Iio n)) (u '' Iio n)

Tactic:
hc (u '' Iio n) ((finite_lt_nat _).image _)

Premises used: Set.Finite.image, Set.image, Set.Iio, Set.finite_lt_nat
-- 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 : ℕ
h : u n = c (u '' Iio n)
⊢ P (u n) (u '' Iio n)

Tactic:
convert! hc (u '' Iio n) ((finite_lt_nat _).image _)

Premises used: Set.Finite.image, Set.image, Set.Iio, Set.finite_lt_nat
-- 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 : ℕ
h : u n = c (range fun (x : (↑(Iio n) : Type)) ↦ u (↑x : ℕ))
⊢ u n = c (u '' Iio n)

Tactic:
rw [image_eq_range]

Premises used: Set.image_eq_range
-- 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:
Nat.strongRecOn'_beta

Premises used: Nat.strongRecOn'_beta