awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
simp_rw :
  Eq (α := Finset (α_1 × β_1)) (s.biUnion ((fun (f : β_1 → α_1 × β_1) ↦ image f t) ∘ Prod.mk))
    (t.biUnion ((fun (f : α_1 → α_1 × β_1) ↦ image f s) ∘ fun (b : β_1) (a : α_1) ↦ (a, b)))
⊢ Eq (α := Finset (α_1 × β_1)) (Prod.mk <$> s <*> t) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> t <*> s)

Tactic:
simp_rw [seq_def, fmap_def, sup_image, sup_eq_biUnion]

Premises used: Finset.seq_def, Finset.sup_eq_biUnion, Finset.sup_image, Finset.fmap_def
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
trans : (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t) = s ×ˢ t
trans₁ : s ×ˢ t = t.biUnion fun (b : β_1) ↦ image (fun (a : α_1) ↦ (a, b)) s
⊢ Eq (α := Finset (α_1 × β_1)) (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t)
    (t.biUnion fun (b : β_1) ↦ image (fun (a : α_1) ↦ (a, b)) s)

Tactic:
trans s ×ˢ t
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
rw rw₁ :
  Eq (α := Finset (α_1 × β_1)) (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t)
    (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t)
⊢ (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t) = s ×ˢ t

Tactic:
rw [product_eq_biUnion]

Premises used: Finset.product_eq_biUnion
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
rw rw₁ :
  Eq (α := Finset (α_1 × β_1)) (t.biUnion fun (b : β_1) ↦ image (fun (a : α_1) ↦ (a, b)) s)
    (t.biUnion fun (b : β_1) ↦ image (fun (a : α_1) ↦ (a, b)) s)
⊢ s ×ˢ t = t.biUnion fun (b : β_1) ↦ image (fun (a : α_1) ↦ (a, b)) s

Tactic:
rw [product_eq_biUnion_right]

Premises used: Finset.product_eq_biUnion_right
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
trans : (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t) = s ×ˢ t
trans₁ : s ×ˢ t = t.biUnion fun (b : β_1) ↦ image (fun (a : α_1) ↦ (a, b)) s
trans₂ : (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t) = s ×ˢ t
trans₃ : s ×ˢ t = t.biUnion fun (b : β_1) ↦ image (fun (a : α_1) ↦ (a, b)) s
⊢ Eq (α := Finset (α_1 × β_1)) (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t)
    (t.biUnion fun (b : β_1) ↦ image (fun (a : α_1) ↦ (a, b)) s)

Tactic:
trans s ×ˢ t <;> [rw [product_eq_biUnion]; rw [product_eq_biUnion_right]]

Premises used: Finset.product_eq_biUnion, Finset.product_eq_biUnion_right
-- Module: Mathlib.Data.Finset.Functor
Goal:
inst : (P : Prop) → Decidable P
α β : Type u_1
⊢ Eq.{u_1 + 1} (α := Finset β → (β → Finset α) → Finset α) (fun (x1 : Finset β) (x2 : β → Finset α) ↦ x1 >>= x2) sup

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Functor
Goal:
inst : (P : Prop) → Decidable P
α β γ : Type u_1
s : Finset α
f : α → Finset β
g : β → Finset γ
⊢ s >>= f >>= g = s >>= fun (x : α) ↦ f x >>= g

Tactic:
simp only [bind, sup_eq_biUnion, biUnion_biUnion]

Premises used: Finset.sup_eq_biUnion, Bind.bind, Finset.biUnion_biUnion
-- Module: Mathlib.Data.Finset.Functor
Goal:
α : Type u
inst : DecidableEq α
s : Finset α
rw : Eq (α := Id (Finset α)) (Multiset.toFinset <$> pure s.val) (pure s)
⊢ Eq (α := Id (Finset α)) (traverse pure s) (pure s)

Tactic:
rw [traverse, Multiset.id_traverse]

Premises used: Multiset.id_traverse, Finset.traverse
-- Module: Mathlib.Data.Finset.Functor
Goal:
α : Type u
inst : DecidableEq α
s : Finset α
⊢ Eq (α := Id (Finset α)) (Multiset.toFinset <$> pure s.val) (pure s)

Tactic:
s.val_toFinset

Premises used: Finset.val_toFinset, Id
-- Module: Mathlib.Data.Finset.Functor
Goal:
α : Type u
inst : DecidableEq α
s : Finset α
⊢ Eq (α := Id (Finset α)) (Multiset.toFinset <$> pure s.val) (pure s)

Tactic:
exact s.val_toFinset

Premises used: Finset.val_toFinset
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
h : α → β
⊢ Functor.map h ∘ Multiset.toFinset = Multiset.toFinset ∘ Functor.map h

Tactic:
funext fun _ => image_toFinset

Premises used: Finset.image_toFinset, funext
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
h : α → β
s : Multiset α
⊢ image h s.toFinset = (h <$> s).toFinset

Tactic:
congrFun (map_comp_coe h) s

Premises used: Multiset.toFinset, Finset.map_comp_coe, congrFun, Finset.image
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β γ : Type u
G : Type u → Type u
inst : Applicative G
inst_1 : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
unfold :
  Functor.map h <$> Multiset.toFinset <$> Multiset.traverse g s.val =
    Multiset.toFinset <$> Multiset.traverse (Functor.map h ∘ g) s.val
⊢ Functor.map h <$> traverse g s = traverse (Functor.map h ∘ g) s

Tactic:
unfold traverse

Premises used: Finset.traverse
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β γ : Type u
G : Type u → Type u
inst : Applicative G
inst_1 : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
⊢ Functor.map h <$> Multiset.toFinset <$> Multiset.traverse g s.val =
    Multiset.toFinset <$> Multiset.traverse (Functor.map h ∘ g) s.val

Tactic:
simp only [Functor.map_map, fmap_def, map_comp_coe_apply, Multiset.fmap_def, ←
    Multiset.map_traverse]

Premises used: Multiset.fmap_def, Finset.map_comp_coe_apply, Multiset.map_traverse, Functor.map_map, Finset.fmap_def
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s : Multiset α
a : α
t : Multiset α
hst : s < t
hts : t < a ::ₘ s
⊢ t.card < succ s.card

Tactic:
simpa using card_lt_card hts

Premises used: Multiset.card_lt_card
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Multiset α
h : s ⋖ t
⊢ ∃ (a : α), a ::ₘ s = t

Tactic:
(lt_iff_cons_le.1 h.lt).imp fun _a ha ↦ ha.eq_of_not_lt <| h.2 <| lt_cons_self _ _

Premises used: Multiset.lt_iff_cons_le, Exists.imp, Iff.mp, CovBy.lt
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s : Multiset α
a : α
⊢ s ⋖ a ::ₘ s

Tactic:
covBy_cons _ _

Premises used: Multiset.covBy_cons
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s : Multiset α
a : α
⊢ s ⋖ a ::ₘ s

Tactic:
exact covBy_cons _ _

Premises used: Multiset.covBy_cons
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Multiset α
h : s ⋖ t
obtain : ∀ (a : α) (h : s ⋖ a ::ₘ s), s.card ⋖ (a ::ₘ s).card
⊢ s.card ⋖ t.card

Tactic:
obtain ⟨a, rfl⟩ := h.exists_multiset_cons

Premises used: CovBy.exists_multiset_cons, rfl
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s : Multiset α
a : α
h : s ⋖ a ::ₘ s
rw : s.card ⋖ s.card + 1
⊢ s.card ⋖ (a ::ₘ s).card

Tactic:
rw [card_cons]

Premises used: Multiset.card_cons
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s : Multiset α
a : α
h : s ⋖ a ::ₘ s
⊢ s.card ⋖ s.card + 1

Tactic:
covBy_succ _

Premises used: Order.succ, Order.covBy_succ
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s : Multiset α
a : α
h : s ⋖ a ::ₘ s
⊢ s.card ⋖ s.card + 1

Tactic:
exact covBy_succ _

Premises used: Order.covBy_succ
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s : Multiset α
⊢ IsAtom s ↔ ∃ (a : α), s = {a}

Tactic:
simp [← bot_covBy_iff, covBy_iff, eq_comm]

Premises used: Multiset.covBy_iff, eq_comm, bot_covBy_iff
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
a : α
⊢ IsAtom (α := Multiset α) {a}

Tactic:
isAtom_iff.2 ⟨_, rfl⟩

Premises used: Iff.mpr, Exists.intro, Multiset.isAtom_iff, rfl
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s_1 t : Multiset α
a : α
s : Multiset α
hs : IsMin s
rw : IsMin (card.{u_1} (α := α) ⊥)
⊢ IsMin s.card

Tactic:
rw [isMin_iff_eq_bot.1 hs]

Premises used: isMin_iff_eq_bot, Iff.mp
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s_1 t : Multiset α
a : α
s : Multiset α
hs : IsMin s
⊢ IsMin (card.{u_1} (α := α) ⊥)

Tactic:
isMin_bot

Premises used: Multiset.card, isMin_bot
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s_1 t : Multiset α
a : α
s : Multiset α
hs : IsMin s
⊢ IsMin (card.{u_1} (α := α) ⊥)

Tactic:
exact isMin_bot

Premises used: isMin_bot
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
m : Multiset α
⊢ grade ℕ m = m.card

Tactic:
rfl

Premises used: Multiset.card, grade, rfl
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
x : Multiset α
hx : Membership.mem (γ := Set (Multiset α)) (Set.range val) x
s : Finset α
t : Multiset α
ht : t ∈ Set.Icc x s.val
⊢ Membership.mem (γ := Set (Multiset α)) (Set.range val) t

Tactic:
⟨⟨t, Multiset.nodup_of_le ht.2 s.2⟩, rfl⟩

Premises used: Multiset.nodup_of_le, Set.Mem, setOf, Finset.nodup, And.right, Exists.intro, Set.range, Finset.mk, rfl
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
x : Multiset α
hx : Membership.mem (γ := Set (Multiset α)) (Set.range val) x
s : Finset α
t : Multiset α
ht : t ∈ Set.Icc x s.val
⊢ Membership.mem (γ := Set (Multiset α)) (Set.range val) t

Tactic:
exact ⟨⟨t, Multiset.nodup_of_le ht.2 s.2⟩, rfl⟩
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
x : Set α
hx : x ∈ Set.range (ι := Finset α) SetLike.coe
s : Finset α
t : Set α
ht : t ∈ Set.Icc x (↑s : Set α)
⊢ t ∈ Set.range (ι := Finset α) SetLike.coe

Tactic:
⟨_, (s.finite_toSet.subset ht.2).coe_toFinset⟩

Premises used: Set.Mem, setOf, Set.Finite.coe_toFinset, Set.Finite.subset, And.right, Exists.intro, Finset.finite_toSet, Set.range
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
x : Set α
hx : x ∈ Set.range (ι := Finset α) SetLike.coe
s : Finset α
t : Set α
ht : t ∈ Set.Icc x (↑s : Set α)
⊢ t ∈ Set.range (ι := Finset α) SetLike.coe

Tactic:
exact ⟨_, (s.finite_toSet.subset ht.2).coe_toFinset⟩
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Finset α
⊢ s.val ⩿ t.val ↔ s ⩿ t

Tactic:
ordConnected_range_val.apply_wcovBy_apply_iff ⟨⟨_, val_injective⟩, val_le_iff⟩

Premises used: RelEmbedding.mk, Finset.ordConnected_range_val, Function.Embedding.mk, Finset.val_injective, Set.OrdConnected.apply_wcovBy_apply_iff, Finset.val_le_iff
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Finset α
⊢ s.val ⋖ t.val ↔ s ⋖ t

Tactic:
ordConnected_range_val.apply_covBy_apply_iff ⟨⟨_, val_injective⟩, val_le_iff⟩

Premises used: RelEmbedding.mk, Finset.ordConnected_range_val, Function.Embedding.mk, Finset.val_injective, Set.OrdConnected.apply_covBy_apply_iff, Finset.val_le_iff
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Finset α
⊢ (↑s : Set α) ⩿ (↑t : Set α) ↔ s ⩿ t

Tactic:
ordConnected_range_coe.apply_wcovBy_apply_iff ⟨⟨_, coe_injective⟩, coe_subset⟩

Premises used: RelEmbedding.mk, Finset.ordConnected_range_coe, setOf, Function.Embedding.mk, Multiset.Mem, Finset.coe_injective, Set.OrdConnected.apply_wcovBy_apply_iff, Finset.coe_subset
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Finset α
⊢ (↑s : Set α) ⋖ (↑t : Set α) ↔ s ⋖ t

Tactic:
ordConnected_range_coe.apply_covBy_apply_iff ⟨⟨_, coe_injective⟩, coe_subset⟩

Premises used: RelEmbedding.mk, Finset.ordConnected_range_coe, setOf, Function.Embedding.mk, Multiset.Mem, Finset.coe_injective, Set.OrdConnected.apply_covBy_apply_iff, Finset.coe_subset
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
⊢ s ⋖ cons a s ha

Tactic:
simp [← val_covBy_val]

Premises used: Finset.val_covBy_val
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Finset α
h : s ⋖ t
⊢ ∃ (a : α) (ha : a ∉ s), cons a s ha = t

Tactic:
let ⟨a, ha, hst⟩ := ssubset_iff_exists_cons_subset.1 h.lt
  ⟨a, ha, (hst.eq_of_not_ssuperset <| h.2 <| ssubset_cons _).symm⟩

Premises used: Finset.cons, Exists, Finset.ssubset_iff_exists_cons_subset, And.right, Exists.intro, Iff.mp, HasSubset.Subset.eq_of_not_ssuperset, CovBy.lt, Eq.symm, Eq, Finset.ssubset_cons, _private.0.CovBy.exists_finset_cons.match_1
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
⊢ s ⋖ cons a s ha

Tactic:
covBy_cons _

Premises used: Finset.covBy_cons
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
⊢ s ⋖ cons a s ha

Tactic:
exact covBy_cons _

Premises used: Finset.covBy_cons
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Finset α
h : s ⋖ t
⊢ #s ⋖ #t

Tactic:
(val_covBy_val.2 h).card_multiset

Premises used: Iff.mpr, CovBy.card_multiset, Finset.card, Finset.val_covBy_val
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
⊢ s ⩿ insert a s

Tactic:
simp [← coe_wcovBy_coe]

Premises used: Finset.coe_wcovBy_coe
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
⊢ s.erase a ⩿ s

Tactic:
simp [← coe_wcovBy_coe]

Premises used: Finset.coe_wcovBy_coe
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s : Finset α
a : α
inst : DecidableEq α
ha : a ∉ s
⊢ s ⋖ insert a s

Tactic:
(wcovBy_insert _ _).covBy_of_lt <| ssubset_insert ha

Premises used: WCovBy.covBy_of_lt, Finset.ssubset_insert, Finset.wcovBy_insert
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
a : α
⊢ CovBy (α := Finset α) ∅ {a}

Tactic:
exact insert_empty_eq (β := Finset α) a ▸ covBy_insert <| notMem_empty a

Premises used: Finset.notMem_empty
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
a : α
⊢ CovBy (α := Finset α) ∅ {a}

Tactic:
classical exact insert_empty_eq (β := Finset α) a ▸ covBy_insert <| notMem_empty a

Premises used: Finset.notMem_empty
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s : Finset α
a : α
inst : DecidableEq α
ha : a ∈ s
⊢ s.erase a ⋖ s

Tactic:
⟨erase_ssubset ha, (erase_wcovBy _ _).2⟩

Premises used: CovBy, Finset.erase_wcovBy, And.right, And.intro, Finset.erase_ssubset
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
h : s ⋖ t
⊢ ∃ a ∉ s, insert a s = t

Tactic:
simpa using h.exists_finset_cons

Premises used: CovBy.exists_finset_cons
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
h : s ⋖ t
⊢ ∃ a ∈ t, t.erase a = s

Tactic:
simpa only [← coe_inj, coe_erase] using h.finset_coe.exists_set_sdiff_singleton

Premises used: CovBy.exists_set_sdiff_singleton, Finset.coe_erase, Finset.coe_inj, CovBy.finset_coe
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ s ⋖ t ↔ ∃ a ∉ s, insert a s = t

Tactic:
simp only [← coe_covBy_coe, Set.covBy_iff_exists_insert, ← coe_inj, coe_insert, mem_coe]

Premises used: Finset.coe_inj, Finset.coe_covBy_coe, Finset.coe_insert, Set.covBy_iff_exists_insert, Finset.mem_coe
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
rw : (∃ a ∉ t, insert a t = s) ↔ t ⊆ s ∧ #(s \ t) = 1
⊢ t ⋖ s ↔ t ⊆ s ∧ #(s \ t) = 1

Tactic:
rw [covBy_iff_exists_insert]

Premises used: Finset.covBy_iff_exists_insert
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
mp : (∃ a ∉ t, insert a t = s) → t ⊆ s ∧ #(s \ t) = 1
mpr : t ⊆ s ∧ #(s \ t) = 1 → ∃ a ∉ t, insert a t = s
⊢ (∃ a ∉ t, insert a t = s) ↔ t ⊆ s ∧ #(s \ t) = 1

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
t : Finset α
inst : DecidableEq α
a : α
ha : a ∉ t
⊢ t ⊆ insert a t ∧ #(insert a t \ t) = 1

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
mpr : (t ⊆ s ∧ ∃ (a : α), s \ t = {a}) → ∃ a ∉ t, insert a t = s
⊢ t ⊆ s ∧ #(s \ t) = 1 → ∃ a ∉ t, insert a t = s

Tactic:
simp_rw [card_eq_one]

Premises used: Finset.card_eq_one
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
hts : t ⊆ s
a : α
ha : s \ t = {a}
⊢ ∃ a ∉ t, insert a t = s

Tactic:
⟨a, (mem_sdiff.1 <| superset_of_eq ha <| mem_singleton_self _).2, ?_⟩

Premises used: Finset.mem_singleton_self, Finset.mem_sdiff, And.right, And.intro, Exists.intro, Iff.mp, superset_of_eq
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
hts : t ⊆ s
a : α
ha : s \ t = {a}
mpr : insert a t = s
⊢ ∃ a ∉ t, insert a t = s

Tactic:
refine ⟨a, (mem_sdiff.1 <| superset_of_eq ha <| mem_singleton_self _).2, ?_⟩
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
hts : t ⊆ s
a : α
ha : s \ t = {a}
mpr : {a} ∪ t = s
mpr₁ : s \ t ∪ t = s
mpr₂ mpr₃ : s = s
⊢ insert a t = s

Tactic:
rw [insert_eq, ← ha, sdiff_union_of_subset hts]

Premises used: Finset.insert_eq, Finset.sdiff_union_of_subset
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ s ⋖ t ↔ ∃ a ∈ t, t.erase a = s

Tactic:
simp only [← coe_covBy_coe, Set.covBy_iff_exists_sdiff_singleton, ← coe_inj, coe_erase, mem_coe]

Premises used: Set.covBy_iff_exists_sdiff_singleton, Finset.coe_erase, Finset.coe_inj, Finset.coe_covBy_coe, Finset.mem_coe
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
a : α
⊢ IsAtom (α := Finset α) {a}

Tactic:
⟨singleton_ne_empty a, fun _ ↦ eq_empty_of_ssubset_singleton⟩

Premises used: Finset.eq_empty_of_ssubset_singleton, And.intro, IsAtom, Finset.singleton_ne_empty
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s : Finset α
⊢ IsAtom s ↔ ∃ (a : α), s = {a}

Tactic:
simp [← bot_covBy_iff, covBy_iff_exists_cons, eq_comm]

Premises used: Finset.covBy_iff_exists_cons, eq_comm, bot_covBy_iff
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a : α
⊢ IsCoatom (α := Finset α) {a}ᶜ

Tactic:
(isAtom_singleton a).compl

Premises used: Finset.isAtom_singleton, IsAtom.compl
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
simp_rw : IsAtom sᶜ ↔ ∃ (a : α), s = {a}ᶜ
simp_rw₁ : (∃ (a : α), sᶜ = {a}) ↔ ∃ (a : α), s = {a}ᶜ
simp_rw₂ : (∃ (a : α), IsCompl s {a}) ↔ ∃ (a : α), s = {a}ᶜ
⊢ IsCoatom s ↔ ∃ (a : α), s = {a}ᶜ

Tactic:
simp_rw [← isAtom_compl, Finset.isAtom_iff, compl_eq_iff_isCompl, eq_compl_iff_isCompl]

Premises used: Finset.isAtom_iff, eq_compl_iff_isCompl, compl_eq_iff_isCompl, isAtom_compl
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s_1 t : Finset α
a : α
s : Finset α
hs : IsMin s
rw : IsMin.{u_1} (α := Multiset α) (val ⊥)
⊢ IsMin s.val

Tactic:
rw [isMin_iff_eq_bot.1 hs]

Premises used: isMin_iff_eq_bot, Iff.mp
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s_1 t : Finset α
a : α
s : Finset α
hs : IsMin s
⊢ IsMin.{u_1} (α := Multiset α) (val ⊥)

Tactic:
isMin_bot

Premises used: isMin_bot
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s_1 t : Finset α
a : α
s : Finset α
hs : IsMin s
⊢ IsMin.{u_1} (α := Multiset α) (val ⊥)

Tactic:
exact isMin_bot

Premises used: isMin_bot
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s : Finset α
⊢ grade (Multiset α) s = s.val

Tactic:
rfl

Premises used: grade, rfl
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s_1 t : Finset α
a : α
s : Finset α
hs : IsMin s
rw : IsMin (card.{u_1} (α := α) ⊥)
⊢ IsMin #s

Tactic:
rw [isMin_iff_eq_bot.1 hs]

Premises used: isMin_iff_eq_bot, Iff.mp
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s_1 t : Finset α
a : α
s : Finset α
hs : IsMin s
⊢ IsMin (card.{u_1} (α := α) ⊥)

Tactic:
isMin_bot

Premises used: Finset.card, Multiset.card, isMin_bot
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s_1 t : Finset α
a : α
s : Finset α
hs : IsMin s
⊢ IsMin (card.{u_1} (α := α) ⊥)

Tactic:
exact isMin_bot

Premises used: isMin_bot
-- Module: Mathlib.Data.Finset.Grade
Goal:
α : Type u_1
s : Finset α
⊢ grade ℕ s = #s

Tactic:
rfl

Premises used: Finset.card, Multiset.card, grade, rfl
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ (map f s).val = Multiset.map (⇑f : (a : α) → β) s.val

Tactic:
rfl

Premises used: Multiset.map, rfl
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
⊢ map f ∅ = ∅

Tactic:
rfl

Premises used: Multiset.map, List.map, Finset.map, Multiset.zero, Finset.empty, Multiset.ofList, rfl
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
b : β
⊢ b ∈ map f s ↔ ∃ a ∈ s, (f : (a : α) → β) a = b

Tactic:
Multiset.mem_map

Premises used: Multiset.map, Set.Mem, Multiset.mem_map, setOf, Multiset.Mem
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α ≃ β
b : β
simp : (∃ a ∈ s, (f : (a : α) → β) a = b) ↔ Membership.mem (α := α) s ((f.symm : (a : β) → α) b : α)
⊢ b ∈ map f.toEmbedding s ↔ Membership.mem (α := α) s ((f.symm : (a : β) → α) b : α)

Tactic:
simp only [mem_map, Equiv.coe_toEmbedding]

Premises used: Equiv.coe_toEmbedding, Finset.mem_map
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α ≃ β
b : β
⊢ (∃ a ∈ s, (f : (a : α) → β) a = b) ↔ Membership.mem (α := α) s ((f.symm : (a : β) → α) b : α)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
a : α
s : Finset α
⊢ Membership.mem (α := β) (map f s) ((f : (a : α) → β) a : β) ↔ a ∈ s

Tactic:
mem_map_of_injective f.2

Premises used: Multiset.map, Set.Mem, setOf, Function.Embedding.inj', Multiset.mem_map_of_injective, Multiset.Mem
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
s : Finset α
hf : Injective f
⊢ f a ∈ map { toFun := f, inj' := hf : α ↪ β } s ↔ a ∈ s

Tactic:
Finset.mem_map' _

Premises used: Set.Mem, setOf, Finset.mem_map'
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
a : α
s : Finset α
⊢ a ∈ s → Membership.mem (α := β) (map f s) ((f : (a : α) → β) a : β)

Tactic:
(mem_map' _).2

Premises used: Iff.mpr, Finset.mem_map'
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
p : (a : β) → a ∈ map f s → Prop
⊢ (∀ (y : β) (H : y ∈ map f s), p y H) ↔ ∀ (x : α) (H : x ∈ s), p ((f : (a : α) → β) x) ⋯

Tactic:
grind
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
x : ↥s
⊢ Membership.mem (α := β) (map f s) ((f : (a : α) → β) (↑x : α) : β)

Tactic:
mem_map_of_mem f x.prop

Premises used: Subtype.prop, Finset.mem_map_of_mem
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ (↑(map f s) : Set β) = (⇑f : (a : α) → β) '' (↑s : Set α)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ (↑(map f s) : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
s : Finset α
σ : Equiv.Perm α
hs : {a : α | (σ : (a : α) → α) a ≠ a} ⊆ (↑s : Set α)
⊢ map (Equiv.toEmbedding σ) s = s

Tactic:
coe_injective <| (coe_map _ _).trans <| Set.image_perm hs

Premises used: Finset.coe_injective, Set.image_perm, Finset.coe_map, Eq.trans
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
inst : DecidableEq α
inst_1 : DecidableEq β
s : Multiset α
x : β
⊢ x ∈ map f s.toFinset ↔ Membership.mem (γ := Finset β) (toFinset (Multiset.map (⇑f : (a : α) → β) s)) x

Tactic:
simp only [mem_map, Multiset.mem_map, Multiset.mem_toFinset]

Premises used: Multiset.mem_map, Finset.mem_map, Multiset.mem_toFinset
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
s : Finset α
x : α
⊢ x ∈ map (Embedding.refl α) s ↔ x ∈ s

Tactic:
simpa only [mem_map, exists_prop] using exists_eq_right

Premises used: exists_eq_right, exists_prop, Finset.mem_map
-- Module: Mathlib.Data.Finset.Image
Goal:
α β : Type u_4
h : α = β
s : Finset α
subst : map (Equiv.cast ⋯).toEmbedding s ≍ s
⊢ map (Equiv.cast h).toEmbedding s ≍ s

Tactic:
subst h
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_4
s : Finset α
⊢ map (Equiv.cast ⋯).toEmbedding s ≍ s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
g : β ↪ γ
s : Finset α
simp :
  Eq.{u_3 + 1} (α := Multiset γ)
    (Multiset.map (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)) s.val)
    (Multiset.map (⇑(f.trans g) : (a : α) → γ) s.val)
⊢ (map g (map f s)).val = (map (f.trans g) s).val

Tactic:
simp only [map_val, Multiset.map_map]

Premises used: Finset.map_val, Multiset.map_map