awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
inl : IsEmpty α → (↑(Fintype.card α) : ℚ≥0) * s.dens = (↑(#s) : ℚ≥0)
inr : Nonempty α → (↑(Fintype.card α) : ℚ≥0) * s.dens = (↑(#s) : ℚ≥0)
⊢ (↑(Fintype.card α) : ℚ≥0) * s.dens = (↑(#s) : ℚ≥0)

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
h : IsEmpty α
⊢ (↑(Fintype.card α) : ℚ≥0) * s.dens = (↑(#s) : ℚ≥0)

Tactic:
simp [Subsingleton.elim s ∅]

Premises used: EmptyCollection.emptyCollection, Subsingleton.elim
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
h : Nonempty α
inr : Ne (α := ℚ≥0) (↑(Fintype.card α) : ℚ≥0) 0
⊢ (↑(Fintype.card α) : ℚ≥0) * s.dens = (↑(#s) : ℚ≥0)

Tactic:
rw [dens, mul_div_cancel₀]

Premises used: Finset.dens, mul_div_cancel₀
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
h : Nonempty α
⊢ Ne (α := ℚ≥0) (↑(Fintype.card α) : ℚ≥0) 0

Tactic:
mod_cast Fintype.card_ne_zero

Premises used: congrArg, cast, Fintype.card, Ne, Nat.cast, Fintype.card_ne_zero, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
h : Nonempty α
⊢ Ne (α := ℚ≥0) (↑(Fintype.card α) : ℚ≥0) 0

Tactic:
exact mod_cast Fintype.card_ne_zero

Premises used: Fintype.card_ne_zero
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
rw : (↑(Fintype.card α) : ℚ≥0) * s.dens = (↑(#s) : ℚ≥0)
rw₁ rw₂ : Eq (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(#s) : ℚ≥0)
⊢ s.dens * (↑(Fintype.card α) : ℚ≥0) = (↑(#s) : ℚ≥0)

Tactic:
rw [mul_comm, card_mul_dens]

Premises used: Finset.card_mul_dens, mul_comm
-- Module: Mathlib.Data.Finset.Density
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : Semifield 𝕜
inst_2 : CharZero 𝕜
s : Finset α
⊢ HMul.hMul (α := 𝕜) (↑(Fintype.card α) : 𝕜) (↑s.dens : 𝕜) = (↑(#s) : 𝕜)

Tactic:
mod_cast s.card_mul_dens

Premises used: Finset.card_mul_dens, HMul.hMul, congrArg, cast, NNRat.cast_mul._simp_1, Fintype.card, Finset.dens, Nat.cast, NNRat.cast_inj._simp_1, Finset.card, congrFun', Eq.symm, NNRat.cast_natCast, NNRat.cast, Eq, Eq.trans
-- Module: Mathlib.Data.Finset.Density
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : Semifield 𝕜
inst_2 : CharZero 𝕜
s : Finset α
⊢ HMul.hMul (α := 𝕜) (↑s.dens : 𝕜) (↑(Fintype.card α) : 𝕜) = (↑(#s) : 𝕜)

Tactic:
mod_cast s.dens_mul_card

Premises used: HMul.hMul, congrArg, cast, NNRat.cast_mul._simp_1, Fintype.card, Finset.dens_mul_card, Finset.dens, Nat.cast, NNRat.cast_inj._simp_1, Finset.card, congrFun', Eq.symm, NNRat.cast_natCast, NNRat.cast, Eq, Eq.trans
-- Module: Mathlib.Data.Finset.Density
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : Semifield 𝕜
inst_2 : CharZero 𝕜
s : Finset α
⊢ (↑s.dens : 𝕜) = HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(Fintype.card α) : 𝕜)

Tactic:
simp [dens]

Premises used: Finset.dens
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
inst_1 : Nonempty α
⊢ dens.{u_2} (α := α) univ = 1

Tactic:
simp [dens, card_univ]

Premises used: Finset.card_univ, Finset.dens
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
inst_1 : Nonempty α
⊢ s.dens = 1 ↔ s = univ

Tactic:
simp [dens, div_eq_one_iff_eq, card_eq_iff_eq_univ]

Premises used: Finset.card_eq_iff_eq_univ, div_eq_one_iff_eq, Finset.dens
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
inst_1 : Nonempty α
⊢ s.dens ≠ 1 ↔ s ≠ univ

Tactic:
dens_eq_one.not

Premises used: Iff.not, Finset.dens_eq_one
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
inl : IsEmpty α → s.dens ≤ 1
inr : Nonempty α → s.dens ≤ 1
⊢ s.dens ≤ 1

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
h : IsEmpty α
⊢ s.dens ≤ 1

Tactic:
simp [Subsingleton.elim s ∅]

Premises used: EmptyCollection.emptyCollection, Subsingleton.elim
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
h : Nonempty α
⊢ s.dens ≤ 1

Tactic:
simpa using dens_le_dens s.subset_univ

Premises used: Finset.dens_le_dens, Finset.subset_univ
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
simp_rw :
  HDiv.hDiv (α := ℚ≥0) (↑(#(s ∪ t)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
      HDiv.hDiv (α := ℚ≥0) (↑(#(s ∩ t)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) =
    HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
      HDiv.hDiv (α := ℚ≥0) (↑(#t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
simp_rw₁ :
  HAdd.hAdd (α := ℚ≥0) (↑(#(s ∪ t)) : ℚ≥0) (↑(#(s ∩ t)) : ℚ≥0) / (↑(Fintype.card α) : ℚ≥0) =
    HAdd.hAdd (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(#t) : ℚ≥0) / (↑(Fintype.card α) : ℚ≥0)
simp_rw₂ :
  HDiv.hDiv (α := ℚ≥0) (↑(#(s ∪ t) + #(s ∩ t)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) =
    HDiv.hDiv (α := ℚ≥0) (↑(#s + #t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
⊢ (s ∪ t).dens + (s ∩ t).dens = s.dens + t.dens

Tactic:
simp_rw [dens, ← add_div, ← Nat.cast_add, card_union_add_card_inter]

Premises used: Finset.card_union_add_card_inter, Finset.dens, Nat.cast_add, add_div
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
rw : (s ∪ t).dens + (s ∩ t).dens = s.dens + t.dens
rw₁ rw₂ : s.dens + t.dens = s.dens + t.dens
⊢ (s ∩ t).dens + (s ∪ t).dens = s.dens + t.dens

Tactic:
rw [add_comm, dens_union_add_dens_inter]

Premises used: Finset.dens_union_add_dens_inter, add_comm
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
inst_1 : DecidableEq α
h : Disjoint s t
rw : (s.disjUnion t h).dens = s.dens + t.dens
rw₁ rw₂ : s.dens + t.dens = s.dens + t.dens
⊢ (s ∪ t).dens = s.dens + t.dens

Tactic:
rw [← disjUnion_eq_union s t h, dens_disjUnion _ _ _]

Premises used: Finset.dens_disjUnion, Finset.disjUnion_eq_union
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
inst_1 : DecidableEq α
h : s ⊆ t
⊢ (t \ s).dens + s.dens = t.dens

Tactic:
simp [dens, ← card_sdiff_add_card_eq_card h, add_div]

Premises used: Finset.dens, Finset.card_sdiff_add_card_eq_card, add_div
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
rw : (s \ t ∪ t).dens = (s ∪ t).dens
rw₁ rw₂ : (s ∪ t).dens = (s ∪ t).dens
⊢ (s \ t).dens + t.dens = (s ∪ t).dens

Tactic:
rw [← dens_union_of_disjoint sdiff_disjoint, sdiff_union_self_eq_union]

Premises used: Finset.dens_union_of_disjoint, Finset.sdiff_union_self_eq_union, Finset.sdiff_disjoint
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
inst_1 : DecidableEq α
h : #s = #t
simp_rw simp_rw₁ : (s \ t).dens + t.dens = (t \ s).dens + t.dens
simp_rw₂ : (s ∪ t).dens = (t \ s).dens + t.dens
simp_rw₃ : (t ∪ s).dens = (t \ s).dens + t.dens
simp_rw₄ : (t \ s).dens + s.dens = (t \ s).dens + t.dens
simp_rw₅ :
  HDiv.hDiv (α := ℚ≥0) (↑(#(t \ s)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
      HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) =
    HDiv.hDiv (α := ℚ≥0) (↑(#(t \ s)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
      HDiv.hDiv (α := ℚ≥0) (↑(#t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
⊢ Eq (α := ℚ≥0) ((fun (x : ℚ≥0) ↦ x + t.dens) (s \ t).dens) ((fun (x : ℚ≥0) ↦ x + t.dens) (t \ s).dens)

Tactic:
simp_rw [dens_sdiff_add_dens, union_comm s, ← dens_sdiff_add_dens, dens, h]

Premises used: Finset.union_comm, Finset.dens_sdiff_add_dens, Finset.dens
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
rw : (s \ t ∪ s ∩ t).dens = s.dens
rw₁ rw₂ : s.dens = s.dens
⊢ (s \ t).dens + (s ∩ t).dens = s.dens

Tactic:
rw [← dens_union_of_disjoint (disjoint_sdiff_inter _ _), sdiff_union_inter]

Premises used: Finset.dens_union_of_disjoint, Finset.disjoint_sdiff_inter, Finset.sdiff_union_inter
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
rw : (s \ t).dens + (s ∩ t).dens = s.dens
rw₁ rw₂ : s.dens = s.dens
⊢ (s ∩ t).dens + (s \ t).dens = s.dens

Tactic:
rw [add_comm, dens_sdiff_add_dens_inter]

Premises used: Finset.dens_sdiff_add_dens_inter, add_comm
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_4
inst : Fintype α
s : Finset α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : (x : α) → Decidable ¬p x
rw : ({a ∈ s | p a} ∪ {a ∈ s | ¬p a}).dens = s.dens
rw₁ rw₂ : s.dens = s.dens
⊢ {a ∈ s | p a}.dens + {a ∈ s | ¬p a}.dens = s.dens

Tactic:
rw [← dens_union_of_disjoint (disjoint_filter_filter_not ..), filter_union_filter_not_eq]

Premises used: Finset.dens_union_of_disjoint, Finset.disjoint_filter_filter_not, Finset.filter_union_filter_not_eq
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_4
inst : Fintype α
s : Finset α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : (x : α) → Decidable ¬p x
rw : ({a ∈ s | p a} ∪ {a ∈ s | ¬p a}).dens = s.dens
rw₁ rw₂ : s.dens = s.dens
⊢ {a ∈ s | p a}.dens + {a ∈ s | ¬p a}.dens = s.dens

Tactic:
classical
  rw [← dens_union_of_disjoint (disjoint_filter_filter_not ..), filter_union_filter_not_eq]

Premises used: Finset.dens_union_of_disjoint, Finset.disjoint_filter_filter_not, Finset.filter_union_filter_not_eq
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
⊢ (s ∪ t).dens ≤ s.dens + t.dens

Tactic:
dens_union_add_dens_inter s t ▸ le_add_of_nonneg_right zero_le'

Premises used: Finset.dens_union_add_dens_inter, Eq.rec, le_add_of_nonneg_right, zero_le'
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
inst_1 : DecidableEq α
⊢ s.dens ≤ (s \ t).dens + t.dens

Tactic:
dens_sdiff_add_dens s _ ▸ dens_le_dens subset_union_left

Premises used: Eq.rec, Finset.dens_sdiff_add_dens, Finset.subset_union_left, Eq.symm, Finset.dens_le_dens
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
inst_1 : DecidableEq α
h : s ⊆ t
⊢ (t \ s).dens = t.dens - s.dens

Tactic:
eq_tsub_of_add_eq (dens_sdiff_add_dens_eq_dens h)

Premises used: eq_tsub_of_add_eq, Finset.dens_sdiff_add_dens_eq_dens
-- Module: Mathlib.Data.Finset.Density
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
⊢ t.dens - s.dens ≤ (t \ s).dens

Tactic:
tsub_le_iff_right.2 dens_le_dens_sdiff_add_dens

Premises used: Iff.mpr, Finset.dens_le_dens_sdiff_add_dens, tsub_le_iff_right
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s t : Finset α
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t

Tactic:
⟨fun h a hs ht => notMem_empty a <|
    singleton_subset_iff.mp (h (singleton_subset_iff.mpr hs) (singleton_subset_iff.mpr ht)),
    fun h _ hs ht _ ha => (h (hs ha) (ht ha)).elim⟩

Premises used: Iff.mpr, False.elim, Finset.singleton_subset_iff, Finset.notMem_empty, Iff.intro, Iff.mp
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s t : Finset α
rw : Disjoint t s ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s
rw₁ rw₂ : (∀ ⦃a : α⦄, a ∈ t → a ∉ s) ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s

Tactic:
rw [_root_.disjoint_comm, disjoint_left]

Premises used: disjoint_comm, Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s t : Finset α
⊢ Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b

Tactic:
simp only [disjoint_left, imp_not_comm, forall_eq']

Premises used: forall_eq', imp_not_comm, Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s t : Finset α
⊢ Disjoint s.val t.val ↔ Disjoint s t

Tactic:
Multiset.disjoint_left.trans disjoint_left.symm

Premises used: Multiset.disjoint_left, Iff.trans, Finset.disjoint_left, Iff.symm
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s t : Finset α
a b : α
h : Disjoint s t
ha : a ∈ s
hb : b ∈ t
⊢ a ≠ b

Tactic:
disjoint_iff_ne.1 h _ ha _ hb

Premises used: Finset.disjoint_iff_ne, Iff.mp
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s t : Finset α
x : α
rw : x ∈ s ∧ ¬x ∉ t ↔ x ∈ s ∧ x ∈ t
rw₁ rw₂ : x ∈ s ∧ x ∈ t ↔ x ∈ s ∧ x ∈ t
⊢ ¬(x ∈ s → x ∉ t) ↔ x ∈ s ∧ x ∈ t

Tactic:
rw [Classical.not_imp, not_not]

Premises used: Classical.not_not, Classical.not_imp
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s t u : Finset α
h : s ⊆ u
d : Disjoint u t
⊢ Disjoint s t

Tactic:
disjoint_left.2 fun _x m₁ => (disjoint_left.1 d) (h m₁)

Premises used: Iff.mpr, Iff.mp, Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s t u : Finset α
h : t ⊆ u
d : Disjoint s u
⊢ Disjoint s t

Tactic:
disjoint_right.2 fun _x m₁ => (disjoint_right.1 d) (h m₁)

Premises used: Iff.mpr, Iff.mp, Finset.disjoint_right
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s : Finset α
⊢ Disjoint ∅ s

Tactic:
disjoint_bot_left

Premises used: disjoint_bot_left
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s : Finset α
⊢ Disjoint s ∅

Tactic:
disjoint_bot_right

Premises used: disjoint_bot_right
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s : Finset α
a : α
⊢ Disjoint {a} s ↔ a ∉ s

Tactic:
simp only [disjoint_left, mem_singleton, forall_eq]

Premises used: Finset.mem_singleton, forall_eq, Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s : Finset α
a : α
⊢ Disjoint s {a} ↔ a ∉ s

Tactic:
disjoint_comm.trans disjoint_singleton_left

Premises used: disjoint_comm, Iff.trans, Finset.disjoint_singleton_left
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
a b : α
rw : a ∉ {b} ↔ a ≠ b
rw₁ rw₂ : ¬a = b ↔ a ≠ b
⊢ Disjoint (α := Finset α) {a} {b} ↔ a ≠ b

Tactic:
rw [disjoint_singleton_left, mem_singleton]

Premises used: Finset.mem_singleton, Finset.disjoint_singleton_left
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s : Finset α
⊢ Disjoint s s ↔ s = ∅

Tactic:
disjoint_self

Premises used: disjoint_self
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s t : Finset α
⊢ Disjoint (↑s : Set α) (↑t : Set α) ↔ Disjoint s t

Tactic:
simp only [Finset.disjoint_left, Set.disjoint_left, mem_coe]

Premises used: Set.disjoint_left, Finset.disjoint_left, Finset.mem_coe
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
ι : Type u_5
s : Set ι
f : ι → Finset α
⊢ (Set.PairwiseDisjoint.{u_2, u_5} (α := Set α) s fun (i : ι) ↦ (↑(f i) : Set α)) ↔ s.PairwiseDisjoint f

Tactic:
forall₅_congr fun _ _ _ _ _ => disjoint_coe

Premises used: forall₅_congr, Finset.disjoint_coe, Set.PairwiseDisjoint, Set.Pairwise
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
ι : Type u_1
α : Type u_2
s : Set ι
f : ι → α
⊢ (Set.PairwiseDisjoint.{u_2, u_1} (α := Finset α) s fun (i : ι) ↦ {f i}) ↔ Set.InjOn f s

Tactic:
simp [Set.PairwiseDisjoint, Set.Pairwise, not_imp_not, Set.InjOn]

Premises used: Set.PairwiseDisjoint, Set.Pairwise, Set.InjOn, not_imp_not
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_5
s t : Finset α
h : Disjoint s t
a : α
mk :
  ∀ (val : Multiset α) (s : List α) (nodup : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s))
    {h : Disjoint { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α } t},
    a ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α }.disjUnion t h ↔
      a ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α } ∨ a ∈ t
⊢ a ∈ s.disjUnion t h ↔ a ∈ s ∨ a ∈ t

Tactic:
rcases s with ⟨⟨s⟩⟩
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_5
t : Finset α
a : α
val : Multiset α
s : List α
nodup : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s)
h : Disjoint { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α } t
mk :
  ∀ (val : Multiset α) (t : List α) (nodup_1 : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) t))
    {h :
      Disjoint { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α }
        { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) t, nodup := nodup_1 }},
    a ∈
        { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α }.disjUnion
          { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) t, nodup := nodup_1 : Finset α } h ↔
      a ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α } ∨
        a ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) t, nodup := nodup_1 : Finset α }
⊢ a ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α }.disjUnion t h ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α } ∨ a ∈ t

Tactic:
rcases t with ⟨⟨t⟩⟩
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_5
a : α
val : Multiset α
s : List α
nodup : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s)
val_1 : Multiset α
t : List α
nodup_1 : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) t)
h :
  Disjoint { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α }
    { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) t, nodup := nodup_1 }
⊢ a ∈
      { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α }.disjUnion
        { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) t, nodup := nodup_1 : Finset α } h ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := nodup : Finset α } ∨
      a ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) t, nodup := nodup_1 : Finset α }

Tactic:
apply List.mem_append

Premises used: List.mem_append
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s t : Finset α
h : Disjoint s t
⊢ ∀ (x : α), x ∈ (↑(s.disjUnion t h) : Set α) ↔ x ∈ (↑s : Set α) ∪ (↑t : Set α)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s t : Finset α
h : Disjoint s t
⊢ s.disjUnion t h = t.disjUnion s ⋯

Tactic:
eq_of_veq <| Multiset.add_comm _ _

Premises used: Finset.eq_of_veq, Multiset.add_comm
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s₁ s₂ t : Finset α
h₁ : Disjoint s₁ t
h₂ : Disjoint s₂ t
⊢ s₁.disjUnion t h₁ = s₂.disjUnion t h₂ ↔ s₁ = s₂

Tactic:
simp [← val_inj, Multiset.add_left_inj]

Premises used: Multiset.add_left_inj, Finset.val_inj
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s t₁ t₂ : Finset α
h₁ : Disjoint s t₁
h₂ : Disjoint s t₂
⊢ s.disjUnion t₁ h₁ = s.disjUnion t₂ h₂ ↔ t₁ = t₂

Tactic:
simp [← val_inj, Multiset.add_right_inj]

Premises used: Multiset.add_right_inj, Finset.val_inj
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
t : Finset α
h : Disjoint ∅ t
⊢ disjUnion ∅ t h = t

Tactic:
eq_of_veq <| Multiset.zero_add _

Premises used: Finset.eq_of_veq, Multiset.zero_add
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s : Finset α
h : Disjoint s ∅
⊢ s.disjUnion ∅ h = s

Tactic:
eq_of_veq <| Multiset.add_zero _

Premises used: Multiset.add_zero, Finset.eq_of_veq
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
a : α
t : Finset α
h : Disjoint {a} t
⊢ disjUnion {a} t h = cons a t ⋯

Tactic:
eq_of_veq <| Multiset.singleton_add _ _

Premises used: Multiset.singleton_add, Finset.eq_of_veq
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
s : Finset α
a : α
h : Disjoint s {a}
rw : disjUnion {a} s ⋯ = cons a s ⋯
rw₁ rw₂ : cons a s ⋯ = cons a s ⋯
⊢ s.disjUnion {a} h = cons a s ⋯

Tactic:
rw [disjUnion_comm, singleton_disjUnion]

Premises used: Finset.singleton_disjUnion, Finset.disjUnion_comm
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
inst : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t

Tactic:
simp only [disjoint_left, mem_insert, or_imp, forall_and, forall_eq]

Premises used: forall_eq, or_imp, Finset.mem_insert, Finset.disjoint_left, forall_and
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
inst : DecidableEq α
s t : Finset α
a : α
rw : a ∉ s ∧ Disjoint t s ↔ a ∉ s ∧ Disjoint s t
rw₁ rw₂ : a ∉ s ∧ Disjoint s t ↔ a ∉ s ∧ Disjoint s t
⊢ Disjoint (insert a t) s ↔ a ∉ s ∧ Disjoint s t

Tactic:
rw [disjoint_insert_left, _root_.disjoint_comm]

Premises used: disjoint_comm, Finset.disjoint_insert_left
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
inst : DecidableEq α
m1 m2 : Multiset α
⊢ Disjoint m1.toFinset m2.toFinset ↔ Disjoint m1 m2

Tactic:
simp [disjoint_left, Finset.disjoint_left]

Premises used: Multiset.disjoint_left, Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Disjoint
Goal:
α : Type u_2
inst : DecidableEq α
l l' : List α
⊢ _root_.Disjoint l.toFinset l'.toFinset ↔ l.Disjoint l'

Tactic:
Multiset.disjoint_toFinset.trans (Multiset.coe_disjoint _ _)

Premises used: List.toFinset, Multiset.disjoint_toFinset, Iff.trans, Multiset.coe_disjoint
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
⊢ s.Nonempty ↔ ∃ (x : α), x ∈ s

Tactic:
Iff.rfl

Premises used: Iff.rfl, Finset.Nonempty
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
⊢ (∃ (a : α), a ∈ s ∧ true = true) ↔ s.Nonempty

Tactic:
simp [Finset.Nonempty]

Premises used: Finset.Nonempty
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
⊢ (↑s : Set α).Nonempty ↔ s.Nonempty

Tactic:
Iff.rfl

Premises used: Iff.rfl, Set.Nonempty, Finset.Nonempty
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
⊢ Nonempty.{u_1 + 1} ↥s ↔ s.Nonempty

Tactic:
nonempty_subtype

Premises used: nonempty_subtype, Finset.Nonempty
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
h : s.Nonempty
⊢ ∃ (x : α), x ∈ s

Tactic:
h

Premises used: Finset.Nonempty
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s t : Finset α
hst : s ⊆ t
hs : s.Nonempty
⊢ t.Nonempty

Tactic:
Set.Nonempty.mono hst hs

Premises used: Set.Nonempty.mono, Set.Nonempty, Finset.Nonempty
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
h : s.Nonempty
p : Prop
⊢ (∀ (x : α), x ∈ s → p) ↔ p

Tactic:
let ⟨x, hx⟩ := h
  ⟨fun h => h x hx, fun h _ _ => h⟩

Premises used: Iff, Iff.intro, _private.0.Finset.Nonempty.forall_const.match_1
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
⊢ s.Nonempty → Nonempty.{u_1 + 1} ↥s

Tactic:
nonempty_coe_sort.2

Premises used: Iff.mpr, Finset.nonempty_coe_sort
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
⊢ s.Nonempty → Nonempty α

Tactic:
fun ⟨x, _hx⟩ => ⟨x⟩

Premises used: Nonempty.intro, Nonempty, _private.0.Finset.Nonempty.forall_const.match_1
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Multiset α) (val ∅) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
a : α
⊢ ¬Membership.mem (γ := Finset α) ∅ a

Tactic:
simp only [mem_def, empty_val, notMem_zero, not_false_iff]

Premises used: Multiset.notMem_zero, Finset.empty_val, not_false_iff, Finset.mem_def
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
⊢ ¬Finset.Nonempty.{u_1} (α := α) ∅

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

Premises used: False, Finset.notMem_empty, _private.0.Finset.not_nonempty_empty.match_1, Not
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Finset α) { val := 0, nodup := ⋯ } ∅

Tactic:
rfl

Premises used: Finset.empty, rfl
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
a : α
s : Finset α
h : a ∈ s
⊢ s ≠ ∅

Tactic:
fun e =>
  notMem_empty a <| e ▸ h

Premises used: Eq.rec, Finset.notMem_empty, Not
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
h : s.Nonempty
⊢ s ≠ ∅

Tactic:
(Exists.elim h) fun _a => ne_empty_of_mem

Premises used: Finset.ne_empty_of_mem, Exists.elim
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
⊢ ∅ ⊆ s

Tactic:
zero_subset _

Premises used: Set.Mem, setOf, Multiset.Mem, Multiset.zero_subset, Multiset.Subset
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
H : ∀ (x : α), ¬x ∈ s
⊢ s = ∅

Tactic:
eq_of_veq (eq_zero_of_forall_notMem H)

Premises used: Finset.eq_of_veq, Multiset.eq_zero_of_forall_notMem
-- Module: Mathlib.Data.Finset.Empty
Goal:
α : Type u_1
s : Finset α
⊢ s = ∅ ↔ ∀ (x : α), ¬x ∈ s

Tactic:
grind