awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup (β := β) a s = some b
x : α
pos : ∀ (h' : x = a), lookup (β := β) x (erase (β := β) a s ∪ singleton (β := β) a b) = lookup (β := β) x s
neg : ∀ (h' : ¬x = a), lookup (β := β) x (erase (β := β) a s ∪ singleton (β := β) a b) = lookup (β := β) x s
⊢ lookup (β := β) x (erase (β := β) a s ∪ singleton (β := β) a b) = lookup (β := β) x s

Tactic:
by_cases h' : x = a
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup (β := β) a s = some b
x : α
h' : x = a
pos :
  ∀ (b : β x) (h : lookup (β := β) x s = some b),
    lookup (β := β) x (erase (β := β) x s ∪ singleton (β := β) x b) = lookup (β := β) x s
⊢ lookup (β := β) x (erase (β := β) a s ∪ singleton (β := β) a b) = lookup (β := β) x s

Tactic:
subst a
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : Finmap β
x : α
b : β x
h : lookup (β := β) x s = some b
pos : lookup (β := β) x (singleton (β := β) x b) = lookup (β := β) x s
pos₁ : some b = lookup (β := β) x s
pos₂ pos₃ : some b = some b
⊢ lookup (β := β) x (erase (β := β) x s ∪ singleton (β := β) x b) = lookup (β := β) x s

Tactic:
rw [lookup_union_right notMem_erase_self, lookup_singleton_eq, h]

Premises used: Finmap.lookup_singleton_eq, Finmap.notMem_erase_self, Finmap.lookup_union_right
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup (β := β) a s = some b
x : α
h' rwa rwa₁ rwa₂ rwa₃ : ¬x = a
⊢ x ∉ singleton (β := β) a b

Tactic:
rwa [mem_singleton]

Premises used: Finmap.mem_singleton
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup (β := β) a s = some b
x : α
h' : ¬x = a
⊢ x ∉ singleton (β := β) a b

Tactic:
have : x ∉ singleton a b := by rwa [mem_singleton]
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup (β := β) a s = some b
x : α
h' : ¬x = a
this : x ∉ singleton (β := β) a b
neg : lookup (β := β) x (erase (β := β) a s) = lookup (β := β) x s
neg₁ neg₂ : lookup (β := β) x s = lookup (β := β) x s
⊢ lookup (β := β) x (erase (β := β) a s ∪ singleton (β := β) a b) = lookup (β := β) x s

Tactic:
rw [lookup_union_left_of_not_in this, lookup_erase_ne h']

Premises used: Finmap.lookup_union_left_of_not_in, Finmap.lookup_erase_ne
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
x : Finmap β
⊢ Disjoint (β := β) ∅ x

Tactic:
nofun

Premises used: False, Finmap.Disjoint, _private.0.Finmap.disjoint_empty.match_1, Not
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
x y : Finmap β
h : x.Disjoint (β := β) y
⊢ y.Disjoint (β := β) x

Tactic:
fun p hy hx => h p hx hy

Premises used: Finmap.Disjoint, Not
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
x y : Finmap β
⊢ x.Disjoint (β := β) y ↔ y.Disjoint (β := β) x

Tactic:
⟨Disjoint.symm x y, Disjoint.symm y x⟩

Premises used: Finmap.Disjoint.symm, Iff.intro
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
x y z : Finmap β
⊢ (x ∪ y).Disjoint (β := β) z ↔ x.Disjoint (β := β) z ∧ y.Disjoint (β := β) z

Tactic:
simp [Disjoint, Finmap.mem_union, or_imp, forall_and]

Premises used: or_imp, Finmap.Disjoint, Finmap.mem_union, forall_and
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
x y z : Finmap β
rw : (y ∪ z).Disjoint (β := β) x ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
rw₁ : y.Disjoint (β := β) x ∧ z.Disjoint (β := β) x ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
rw₂ : x.Disjoint (β := β) y ∧ z.Disjoint (β := β) x ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
rw₃ rw₄ : x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z
⊢ x.Disjoint (β := β) (y ∪ z) ↔ x.Disjoint (β := β) y ∧ x.Disjoint (β := β) z

Tactic:
rw [Disjoint.symm_iff, disjoint_union_left, Disjoint.symm_iff _ x, Disjoint.symm_iff _ x]

Premises used: Finmap.Disjoint.symm_iff, Finmap.disjoint_union_left
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁_1 s₂_1 : Finmap β
s₁ s₂ : AList β
h : s₁.toFinmap (β := β).Disjoint (β := β) (s₂.toFinmap (β := β))
⊢ s₁.toFinmap (β := β) ∪ s₂.toFinmap (β := β) = s₂.toFinmap (β := β) ∪ s₁.toFinmap (β := β)

Tactic:
simp only [AList.toFinmap_eq, union_toFinmap, AList.union_comm_of_disjoint h]

Premises used: AList.toFinmap_eq, AList.union_comm_of_disjoint, Finmap.union_toFinmap
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
a : ∀ (x : α), lookup (β := β) x s₁ = lookup (β := β) x s₂
⊢ s₁ = s₂

Tactic:
apply ext_lookup

Premises used: Finmap.ext_lookup
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
⊢ lookup (β := β) x (s₁ ∪ s₃) = lookup (β := β) x (s₂ ∪ s₃)

Tactic:
have : (s₁ ∪ s₃).lookup x = (s₂ ∪ s₃).lookup x := h'' ▸ rfl
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup (β := β) x (s₁ ∪ s₃) = lookup (β := β) x (s₂ ∪ s₃)
pos : ∀ (hs₁ : x ∈ s₁), lookup (β := β) x s₁ = lookup (β := β) x s₂
neg : ∀ (hs₁ : x ∉ s₁), lookup (β := β) x s₁ = lookup (β := β) x s₂
⊢ lookup (β := β) x s₁ = lookup (β := β) x s₂

Tactic:
by_cases hs₁ : x ∈ s₁
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup (β := β) x (s₁ ∪ s₃) = lookup (β := β) x (s₂ ∪ s₃)
hs₁ : x ∈ s₁
pos :
  ∀ (this : lookup (β := β) x s₁ = lookup (β := β) x (s₂ ∪ s₃)) (hs₁ : x ∈ s₁),
    lookup (β := β) x s₁ = lookup (β := β) x s₂
pos₁ pos₂ pos₃ pos₄ :
  ∀ (this : lookup (β := β) x s₁ = lookup (β := β) x s₂) (hs₁ : x ∈ s₁), lookup (β := β) x s₁ = lookup (β := β) x s₂
⊢ lookup (β := β) x s₁ = lookup (β := β) x s₂

Tactic:
rwa [lookup_union_left hs₁, lookup_union_left_of_not_in (h _ hs₁)] at this

Premises used: Finmap.lookup_union_left_of_not_in, Finmap.lookup_union_left
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup (β := β) x (s₁ ∪ s₃) = lookup (β := β) x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
pos : ∀ (hs₂ : x ∈ s₂), lookup (β := β) x s₁ = lookup (β := β) x s₂
neg : ∀ (hs₂ : x ∉ s₂), lookup (β := β) x s₁ = lookup (β := β) x s₂
⊢ lookup (β := β) x s₁ = lookup (β := β) x s₂

Tactic:
by_cases hs₂ : x ∈ s₂
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup (β := β) x (s₁ ∪ s₃) = lookup (β := β) x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
hs₂ : x ∈ s₂
pos :
  ∀ (this : lookup (β := β) x s₁ = lookup (β := β) x (s₂ ∪ s₃)) (hs₁ : x ∉ s₁) (hs₂ : x ∈ s₂),
    lookup (β := β) x s₁ = lookup (β := β) x s₂
pos₁ pos₂ pos₃ pos₄ :
  ∀ (this : lookup (β := β) x s₁ = lookup (β := β) x s₂) (hs₁ : x ∉ s₁) (hs₂ : x ∈ s₂),
    lookup (β := β) x s₁ = lookup (β := β) x s₂
⊢ lookup (β := β) x s₁ = lookup (β := β) x s₂

Tactic:
rwa [lookup_union_left_of_not_in (h' _ hs₂), lookup_union_left hs₂] at this

Premises used: Finmap.lookup_union_left_of_not_in, Finmap.lookup_union_left
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint (β := β) s₃
h' : s₂.Disjoint (β := β) s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup (β := β) x (s₁ ∪ s₃) = lookup (β := β) x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
hs₂ : x ∉ s₂
neg : none = lookup (β := β) x s₂
neg₁ neg₂ : Eq.{v + 1} (α := Option (β x)) none none
⊢ lookup (β := β) x s₁ = lookup (β := β) x s₂

Tactic:
rw [lookup_eq_none.mpr hs₁, lookup_eq_none.mpr hs₂]

Premises used: Iff.mpr, Finmap.lookup_eq_none
-- Module: Mathlib.Data.Finset.Attach
Goal:
α : Type u_1
s : Finset α
⊢ s.attach.val = s.val.attach

Tactic:
rfl

Premises used: Multiset.pmap, Multiset.attach, rfl
-- Module: Mathlib.Data.Finset.Attach
Goal:
α : Type u_1
s : Finset α
⊢ ∀ (x : ↥s), x ∈ s.attach

Tactic:
Multiset.mem_attach _

Premises used: Set.Mem, setOf, Multiset.Mem, Multiset.mem_attach, Multiset.pmap, Multiset.attach
-- Module: Mathlib.Data.Finset.Attach
Goal:
α : Type u_1
s : Finset α
h : ∀ (x : ↥s), x ∈ (↑s.attach : Set ↥s) ↔ Membership.mem (γ := Set ↥s) Set.univ x
⊢ (↑s.attach : Set ↥s) = Set.univ

Tactic:
ext
-- Module: Mathlib.Data.Finset.Attach
Goal:
α : Type u_1
s : Finset α
x : ↥s
⊢ x ∈ (↑s.attach : Set ↥s) ↔ Membership.mem (γ := Set ↥s) Set.univ x

Tactic:
simp
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
⊢ s.disjUnion t h = s ∪ t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u

Tactic:
simp only [disjoint_left, mem_union, or_imp, forall_and]

Premises used: or_imp, Finset.mem_union, Finset.disjoint_left, forall_and
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u

Tactic:
simp only [disjoint_right, mem_union, or_imp, forall_and]

Premises used: or_imp, Finset.disjoint_right, Finset.mem_union, forall_and
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ (∃ a ∈ s, a ∈ t) ↔ (s ∩ t).Nonempty

Tactic:
simp [Finset.Nonempty]

Premises used: Finset.Nonempty
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
rw : Disjoint s t ∨ ¬Disjoint s t
⊢ Disjoint s t ∨ (s ∩ t).Nonempty

Tactic:
rw [← not_disjoint_iff_nonempty_inter]

Premises used: Finset.not_disjoint_iff_nonempty_inter
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ Disjoint s t ∨ ¬Disjoint s t

Tactic:
em _

Premises used: em
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ Disjoint s t ∨ ¬Disjoint s t

Tactic:
exact em _

Premises used: em
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s t : Finset α
h : s ⊆ t
⊢ Disjoint s t ↔ s = ∅

Tactic:
disjoint_of_le_iff_left_eq_bot h

Premises used: disjoint_of_le_iff_left_eq_bot
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
ι : Type u_4
s : Set ι
f : ι → Finset α
⊢ s.PairwiseDisjoint f ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j

Tactic:
simp [Set.PairwiseDisjoint, Set.Pairwise, not_imp_comm (a := _ = _),
    not_disjoint_iff_nonempty_inter]

Premises used: not_imp_comm, Set.PairwiseDisjoint, Finset.not_disjoint_iff_nonempty_inter, Set.Pairwise
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ IsDirectedOrder.{u_1} (Finset α)

Tactic:
infer_instance
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ IsDirectedOrder.{u_1} (Finset α)

Tactic:
classical infer_instance
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ IsDirected.{u_1 + 1} (Finset α) fun (x1 x2 : Finset α) ↦ x1 ⊆ x2

Tactic:
isDirected_le

Premises used: Finset.isDirected_le
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ erase ∅ a = ∅

Tactic:
rfl

Premises used: Multiset.zero, Finset.empty, Multiset.ofList, List.erase, Multiset.erase, Finset.erase, rfl
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
hs : s.Nontrivial
⊢ ∀ (a_1 : α), a_1 ∈ s ∧ a_1 ≠ a → a_1 ∈ s.erase a

Tactic:
simp_all
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
simp : (∃ x ∈ s, x ≠ a) ↔ s.Nontrivial
⊢ (s.erase a).Nonempty ↔ s.Nontrivial

Tactic:
simp only [Finset.Nonempty, mem_erase, and_comm (b := _ ∈ _)]

Premises used: and_comm, Finset.mem_erase, Finset.Nonempty
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ (∃ x ∈ s, x ≠ a) ↔ s.Nontrivial

Tactic:
⟨?_, fun hs ↦ hs.exists_ne a⟩

Premises used: Iff.intro, Finset.Nontrivial.exists_ne
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
refine : (∃ x ∈ s, x ≠ a) → s.Nontrivial
⊢ (∃ x ∈ s, x ≠ a) ↔ s.Nontrivial

Tactic:
refine ⟨?_, fun hs ↦ hs.exists_ne a⟩
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hba : b ≠ a
⊢ s.Nontrivial

Tactic:
⟨_, hb, _, ha, hba⟩

Premises used: And.intro, Exists.intro, Set.Nontrivial
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hba : b ≠ a
⊢ s.Nontrivial

Tactic:
exact ⟨_, hb, _, ha, hba⟩
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ erase {a} a = ∅

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
⊢ (insert a s).erase a = s.erase a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ (insert a s).erase a = s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
s : Finset α
h : a ≠ b
⊢ (insert a s).erase b = insert a (s.erase b)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
s : Finset α
ha : a ∉ s
hb : a ≠ b
⊢ (cons a s ha).erase b = cons a (s.erase b) ⋯

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
h : a ∈ s
⊢ insert a (s.erase a) = s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
hs : a ∈ s
ht : a ∉ t
⊢ s.erase a = t ↔ s = insert a t

Tactic:
aesop
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ Set.InvOn (insert a) (fun (s : Finset α) ↦ s.erase a) {s : Finset α | a ∈ s} {s : Finset α | a ∉ s}

Tactic:
⟨fun _s ↦ insert_erase, fun _s ↦ erase_insert⟩

Premises used: Set.InvOn, Finset.erase_insert, And.intro, Finset.insert_erase
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ s.erase a ⊂ s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ s.erase a ∪ {a} = s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ⊂ t ↔ ∃ a ∈ t, s ⊆ t.erase a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
grw grw₁ : s.erase a ⊆ s.erase a
⊢ s.erase a ⊆ (insert a s).erase a

Tactic:
grw [← subset_insert]

Premises used: Finset.subset_insert
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
h : a ∉ s
⊢ (cons a s h).erase a = s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Finset α
⊢ s ⊆ insert a t ↔ s.erase a ⊆ t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).erase a ⊆ s

Tactic:
subset_insert_iff.1 Subset.rfl

Premises used: Finset.Subset.rfl, Iff.mp, Finset.subset_insert_iff
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ s ⊆ insert a (s.erase a)

Tactic:
subset_insert_iff.2 Subset.rfl

Premises used: Iff.mpr, Finset.Subset.rfl, Finset.subset_insert_iff
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
rw : s.erase a ⊆ t ↔ s ⊆ t
rw₁ rw₂ : s ⊆ t ↔ s ⊆ t
⊢ s ⊆ insert a t ↔ s ⊆ t

Tactic:
rw [subset_insert_iff, erase_eq_of_notMem h]

Premises used: Finset.erase_eq_of_notMem, Finset.subset_insert_iff
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
h : a ∈ t
rw : s ⊆ insert a t ↔ s ⊆ t
rw₁ rw₂ : s ⊆ t ↔ s ⊆ t
⊢ s.erase a ⊆ t ↔ s ⊆ t

Tactic:
rw [← subset_insert_iff, insert_eq_of_mem h]

Premises used: Finset.insert_eq_of_mem, Finset.subset_insert_iff
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
hs : Membership.mem (γ := Set (Finset α)) {s : Finset α | a ∈ s} s
t : Finset α
ht : Membership.mem (γ := Set (Finset α)) {s : Finset α | a ∈ s} t
h : s.erase a = (fun (s : Finset α) ↦ s.erase a) t
rw : insert a (s.erase a) = t
rw₁ : insert a (s.erase a) = insert a (t.erase a)
rw₂ rw₃ : insert a ((fun (s : Finset α) ↦ s.erase a) t) = insert a (t.erase a)
⊢ s = t

Tactic:
rw [← insert_erase hs, ← insert_erase ht, h]

Premises used: Finset.insert_erase
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
hs : s.Nontrivial
obtain :
  ∀ (a : α) (ha : a ∈ (↑s : Set α)) (b : α) (hb : b ∈ (↑s : Set α)) (hab : a ≠ b),
    ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s
⊢ ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s

Tactic:
obtain ⟨a, ha, b, hb, hab⟩ := hs
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
⊢ b ∈ s.erase a

Tactic:
have : b ∈ s.erase a := mem_erase.2 ⟨hab.symm, hb⟩
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
this : b ∈ s.erase a
⊢ ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s

Tactic:
⟨(s.erase a).erase b, a, ?_, b, ?_, ?_, ?_⟩

Premises used: Exists.intro, Finset.erase
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
this : b ∈ s.erase a
refine_1 : a ∉ (s.erase a).erase b
refine_2 : b ∉ (s.erase a).erase b
refine_3 : ¬a = b
refine_4 : cons a (cons b ((s.erase a).erase b) ⋯) ⋯ = s
⊢ ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s

Tactic:
refine ⟨(s.erase a).erase b, a, ?_, b, ?_, ?_, ?_⟩
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
this : b ∈ s.erase a
⊢ a ∉ (s.erase a).erase b

Tactic:
simp [insert_erase ha, *]

Premises used: Finset.insert_erase
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
this : b ∈ s.erase a
⊢ b ∉ (s.erase a).erase b

Tactic:
simp [insert_erase ha, *]

Premises used: Finset.insert_erase
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
this : b ∈ s.erase a
⊢ ¬a = b

Tactic:
simp [insert_erase ha, *]

Premises used: Finset.insert_erase
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
this : b ∈ s.erase a
⊢ cons a (cons b ((s.erase a).erase b) ⋯) ⋯ = s

Tactic:
simp [insert_erase ha, *]

Premises used: Finset.insert_erase
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
hs : s.Nontrivial
obtain :
  ∀ (a : α) (ha : a ∈ (↑s : Set α)) (b : α) (hb : b ∈ (↑s : Set α)) (hab : a ≠ b),
    ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s
obtain₁ :
  ∀ (a : α) (ha : a ∈ (↑s : Set α)) (b : α) (hb : b ∈ (↑s : Set α)) (hab : a ≠ b) (this : b ∈ s.erase a),
    ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s
⊢ ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s

Tactic:
classical
  obtain ⟨a, ha, b, hb, hab⟩ := hs
  have : b ∈ s.erase a := mem_erase.2 ⟨hab.symm, hb⟩
  refine ⟨(s.erase a).erase b, a, ?_, b, ?_, ?_, ?_⟩ <;> simp [insert_erase ha, *]
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
hb : b ∈ s
h : ∀ (a_1 : α), a_1 ∈ s.erase a \ s.erase b ↔ Membership.mem (γ := Finset α) {b} a_1
⊢ s.erase a \ s.erase b = {b}

Tactic:
ext
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
hb : b ∈ s
a_1 : α
⊢ a_1 ∈ s.erase a \ s.erase b ↔ Membership.mem (γ := Finset α) {b} a_1

Tactic:
aesop
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ s \ {a} = s.erase a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
⊢ s.erase a = s \ {a}

Tactic:
(sdiff_singleton_eq_erase _ _).symm

Premises used: Finset.sdiff_singleton_eq_erase, Eq.symm
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
simp_rw : Disjoint (s \ {a}) t ↔ Disjoint s (t \ {a})
⊢ Disjoint (s.erase a) t ↔ Disjoint s (t.erase a)

Tactic:
simp_rw [erase_eq, disjoint_sdiff_comm]

Premises used: Finset.erase_eq, disjoint_sdiff_comm
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
rw : Disjoint s ((insert a t).erase a) ↔ Disjoint s t
rw₁ rw₂ : Disjoint s t ↔ Disjoint s t
⊢ Disjoint (s.erase a) (insert a t) ↔ Disjoint s t

Tactic:
rw [disjoint_erase_comm, erase_insert ha]

Premises used: Finset.erase_insert, Finset.disjoint_erase_comm
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
rw : Disjoint ((insert a s).erase a) t ↔ Disjoint s t
rw₁ rw₂ : Disjoint s t ↔ Disjoint s t
⊢ Disjoint (insert a s) (t.erase a) ↔ Disjoint s t

Tactic:
rw [← disjoint_erase_comm, erase_insert ha]

Premises used: Finset.erase_insert, Finset.disjoint_erase_comm
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
hst : Disjoint (s.erase a) t
rw : a ∉ s.erase a ∧ Disjoint (s.erase a) t
⊢ Disjoint s t

Tactic:
rw [← erase_insert ha, ← disjoint_erase_comm, disjoint_insert_right]

Premises used: Finset.disjoint_insert_right, Finset.erase_insert, Finset.disjoint_erase_comm
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
hst : Disjoint (s.erase a) t
⊢ a ∉ s.erase a ∧ Disjoint (s.erase a) t

Tactic:
⟨notMem_erase _ _, hst⟩

Premises used: And.intro, Finset.notMem_erase
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
hst : Disjoint (s.erase a) t
⊢ a ∉ s.erase a ∧ Disjoint (s.erase a) t

Tactic:
exact ⟨notMem_erase _ _, hst⟩
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
hst : Disjoint s (t.erase a)
rw : a ∉ t.erase a ∧ Disjoint s (t.erase a)
⊢ Disjoint s t

Tactic:
rw [← erase_insert ha, disjoint_erase_comm, disjoint_insert_left]

Premises used: Finset.erase_insert, Finset.disjoint_insert_left, Finset.disjoint_erase_comm
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
hst : Disjoint s (t.erase a)
⊢ a ∉ t.erase a ∧ Disjoint s (t.erase a)

Tactic:
⟨notMem_erase _ _, hst⟩

Premises used: And.intro, Finset.notMem_erase
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
hst : Disjoint s (t.erase a)
⊢ a ∉ t.erase a ∧ Disjoint s (t.erase a)

Tactic:
exact ⟨notMem_erase _ _, hst⟩
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Finset α
⊢ s ∩ t.erase a = (s ∩ t).erase a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Finset α
⊢ s.erase a ∩ t = (s ∩ t).erase a

Tactic:
grind