awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : Finset α → Prop
empty : motive ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : s.Nodup), motive { val := s, nodup := nd }
nd : (a ::ₘ s).Nodup
⊢ motive (Finset.cons a { val := s, nodup := ⋯ } ⋯)

Tactic:
cons a _ _ (IH _)
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : Finset α → Prop
empty : motive ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : s.Nodup), motive { val := s, nodup := nd }
nd : (a ::ₘ s).Nodup
⊢ motive (Finset.cons a { val := s, nodup := ⋯ } ⋯)

Tactic:
exact cons a _ _ (IH _)
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : Finset α → Prop
empty : motive ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)
s : Multiset α
nd : s.Nodup
empty₁ : ∀ (nd : Nodup.{u_3} (α := α) 0), motive { val := 0, nodup := nd }
cons₁ :
  ∀ (a : α) (s : Multiset α) (IH : ∀ (nd : s.Nodup), motive { val := s, nodup := nd }) (nd : (a ::ₘ s).Nodup),
    motive { val := a ::ₘ s, nodup := nd }
⊢ motive { val := s, nodup := nd }

Tactic:
induction s using Multiset.induction with
    | empty => exact empty
    | cons a s IH =>
      rw [mk_cons nd]
      exact cons a _ _ (IH _)
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : Finset α → Prop
s : Finset α
empty : motive ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)
⊢ motive s

Tactic:
cons_induction empty cons s

Premises used: Finset.cons_induction
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : Finset α → Prop
inst : DecidableEq α
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (Insert.insert a s)
⊢ ∀ (s : Finset α), motive s

Tactic:
cons_induction empty fun a s ha => (s.cons_eq_insert a ha).symm ▸ insert a s ha

Premises used: Finset.cons_induction
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : Finset α → Prop
inst : DecidableEq α
s : Finset α
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (Insert.insert a s)
⊢ motive s

Tactic:
Finset.induction empty insert s

Premises used: Finset.induction
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : Finset α → Prop
inst : DecidableEq α
S : Finset α
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), a ∈ S → s ⊆ S → a ∉ s → motive s → motive (Insert.insert a s)
⊢ motive S

Tactic:
@Finset.induction_on α (fun T => T ⊆ S → motive T) _ S (fun _ => empty)
    (fun a s has hqs hs =>
      let ⟨hS, sS⟩ := Finset.insert_subset_iff.1 hs
      insert a s hS sS has (hqs sS))
    (Finset.Subset.refl S)

Premises used: Finset.Subset.refl, Finset.insert_subset_iff, Insert.insert, Finset.induction_on, Iff.mp, _private.0.Finset.induction_on'.match_1
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
hs : Finset.Nonempty.{u_3} (α := α) ∅
⊢ motive ∅ hs

Tactic:
(not_nonempty_empty hs).elim

Premises used: Finset.not_nonempty_empty, False.elim
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
hs : Finset.Nonempty.{u_3} (α := α) ∅
⊢ motive ∅ hs

Tactic:
exact (not_nonempty_empty hs).elim

Premises used: Finset.not_nonempty_empty, False.elim
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
t : Finset α
ha : a ∉ t
h : ∀ (hs : t.Nonempty), motive t hs
hs : (Finset.cons a t ha).Nonempty
cons₁ :
  ∀ (ha : a ∉ ∅) (h : ∀ (hs : Finset.Nonempty.{u_3} (α := α) ∅), motive ∅ hs) (hs : (Finset.cons a ∅ ha).Nonempty),
    motive (Finset.cons a ∅ ha) hs
cons₂ : ∀ (ht : t.Nonempty), motive (Finset.cons a t ha) hs
⊢ motive (Finset.cons a t ha) hs

Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
ha : a ∉ ∅
h : ∀ (hs : Finset.Nonempty.{u_3} (α := α) ∅), motive ∅ hs
hs : (Finset.cons a ∅ ha).Nonempty
⊢ motive (Finset.cons a ∅ ha) hs

Tactic:
singleton a

Premises used: Finset.cons
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
ha : a ∉ ∅
h : ∀ (hs : Finset.Nonempty.{u_3} (α := α) ∅), motive ∅ hs
hs : (Finset.cons a ∅ ha).Nonempty
⊢ motive (Finset.cons a ∅ ha) hs

Tactic:
exact singleton a
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
t : Finset α
ha : a ∉ t
h : ∀ (hs : t.Nonempty), motive t hs
hs : (Finset.cons a t ha).Nonempty
ht : t.Nonempty
⊢ motive (Finset.cons a t ha) hs

Tactic:
cons a t ha ht (h ht)
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
t : Finset α
ha : a ∉ t
h : ∀ (hs : t.Nonempty), motive t hs
hs : (Finset.cons a t ha).Nonempty
ht : t.Nonempty
⊢ motive (Finset.cons a t ha) hs

Tactic:
exact cons a t ha ht (h ht)
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
s : Finset α
hs : s.Nonempty
empty : ∀ (hs : Finset.Nonempty.{u_3} (α := α) ∅), motive ∅ hs
cons₁ :
  ∀ (a : α) (t : Finset α) (ha : a ∉ t) (h : ∀ (hs : t.Nonempty), motive t hs) (hs : (Finset.cons a t ha).Nonempty),
    motive (Finset.cons a t ha) hs
⊢ motive s hs

Tactic:
induction s using Finset.cons_induction with
  | empty => exact (not_nonempty_empty hs).elim
  | cons a t ha h =>
    obtain rfl | ht := t.eq_empty_or_nonempty
    · exact singleton a
    · exact cons a t ha ht (h ht)

Premises used: rfl
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
s : Finset α
hs : s.Nonempty
⊢ ∃ (t : Finset α) (a : α) (ha : a ∉ t), cons a t ha = s

Tactic:
hs.cons_induction (fun a ↦ ⟨∅, a, _, cons_empty _⟩) fun _ _ _ _ _ ↦ ⟨_, _, _, rfl⟩

Premises used: Finset.Nonempty.cons_induction
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t_1 : Finset α
a b : α
f : α → β
t : Finset α
x : α
h : x ∉ t
y : ↥(insert x t)
⊢ (fun (y : Option ↥t) ↦
        (y.elim (Subtype.mk (p := fun (i : α) ↦ i ∈ insert x t) x ⋯) fun (z : ↥t) ↦
            Subtype.mk (p := fun (i : α) ↦ i ∈ insert x t) (↑z : α) ⋯ :
          ↥(insert x t)))
      ((fun (y : ↥(insert x t)) ↦
          (if h : (↑y : α) = x then none else some (Subtype.mk (p := fun (i : α) ↦ i ∈ t) (↑y : α) ⋯) : Option ↥t))
        y) =
    y

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t_1 : Finset α
a b : α
f : α → β
t : Finset α
x : α
h : x ∉ t
⊢ Eq.{u_1 + 1} (α := Option ↥t)
    ((fun (y : ↥(insert x t)) ↦
        (if h : (↑y : α) = x then none else some (Subtype.mk (p := fun (i : α) ↦ i ∈ t) (↑y : α) ⋯) : Option ↥t))
      ((fun (y : Option ↥t) ↦
          (y.elim (Subtype.mk (p := fun (i : α) ↦ i ∈ insert x t) x ⋯) fun (z : ↥t) ↦
              Subtype.mk (p := fun (i : α) ↦ i ∈ insert x t) (↑z : α) ⋯ :
            ↥(insert x t)))
        none))
    none

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t_1 : Finset α
a b : α
f : α → β
t : Finset α
x : α
h : x ∉ t
y : ↥t
⊢ (fun (y : ↥(insert x t)) ↦
        (if h : (↑y : α) = x then none else some (Subtype.mk (p := fun (i : α) ↦ i ∈ t) (↑y : α) ⋯) : Option ↥t))
      ((fun (y : Option ↥t) ↦
          (y.elim (Subtype.mk (p := fun (i : α) ↦ i ∈ insert x t) x ⋯) fun (z : ↥t) ↦
              Subtype.mk (p := fun (i : α) ↦ i ∈ insert x t) (↑z : α) ⋯ :
            ↥(insert x t)))
        (some y)) =
    some y

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s_1 t : Finset α
a_1 b : α
f_1 : α → β
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x : (i : α) → i ∈ insert a s → f i
⊢ prodPiInsert f (insertPiProd f x) = x

Tactic:
grind [prodPiInsert, insertPiProd]

Premises used: Finset.insertPiProd, Finset.prodPiInsert
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s_1 t : Finset α
a_1 b : α
f_1 : α → β
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x : f a × ((i : α) → i ∈ s → f i)
fst : (insertPiProd f (prodPiInsert f x)).1 = x.1
snd : ∀ (x_1 : α) (hi : x_1 ∈ s), (insertPiProd f (prodPiInsert f x)).2 x_1 hi = x.2 x_1 hi
⊢ insertPiProd f (prodPiInsert f x) = x

Tactic:
ext _ hi
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s_1 t : Finset α
a_1 b : α
f_1 : α → β
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x : f a × ((i : α) → i ∈ s → f i)
⊢ (insertPiProd f (prodPiInsert f x)).1 = x.1

Tactic:
grind [prodPiInsert, insertPiProd]

Premises used: Finset.insertPiProd, Finset.prodPiInsert
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s_1 t : Finset α
a_1 b : α
f_1 : α → β
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x : f a × ((i : α) → i ∈ s → f i)
x_1 : α
hi : x_1 ∈ s
⊢ (insertPiProd f (prodPiInsert f x)).2 x_1 hi = x.2 x_1 hi

Tactic:
grind [prodPiInsert, insertPiProd]

Premises used: Finset.insertPiProd, Finset.prodPiInsert
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
p : α → Prop
⊢ (∃ x ∈ insert a s, p x) ↔ p a ∨ ∃ x ∈ s, p x

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
p : α → Prop
⊢ (∀ x ∈ insert a s, p x) ↔ p a ∧ ∀ x ∈ s, p x

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
a : α
s : Finset α
H : ∀ x ∈ insert a s, p x
x : α
h : x ∈ s
⊢ p x

Tactic:
H _ <| mem_insert_of_mem h

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := Finset α) (toFinset 0) ∅

Tactic:
rfl

Premises used: Multiset.toFinset, Multiset.dedup, List.dedup, Multiset.zero, Finset.empty, Multiset.ofList, List.pwFilter, List.foldr, rfl
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ (a ::ₘ s).toFinset = insert a s.toFinset

Tactic:
Finset.eq_of_veq dedup_cons

Premises used: Multiset.dedup_cons, Finset.eq_of_veq
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
rw : (a ::ₘ 0).toFinset = {a}
rw₁ : Eq (α := Finset α) (insert a (toFinset 0)) {a}
rw₂ : Eq (α := Finset α) (insert a ∅) {a}
rw₃ rw₄ : Eq (α := Finset α) {a} {a}
⊢ Eq (α := Finset α) (toFinset {a}) {a}

Tactic:
rw [← cons_zero, toFinset_cons, toFinset_zero, LawfulSingleton.insert_empty_eq]

Premises used: Multiset.toFinset_cons, Multiset.toFinset_zero, LawfulSingleton.insert_empty_eq, Multiset.cons_zero
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := Finset α) (toFinset []) ∅

Tactic:
rfl

Premises used: Multiset.toFinset, Multiset.dedup, List.dedup, Multiset.zero, Finset.empty, List.toFinset, Multiset.ofList, List.pwFilter, List.foldr, rfl
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
pos : ∀ (h : a ∈ l), (a :: l).toFinset.val = (insert a l.toFinset).val
neg : ∀ (h : a ∉ l), (a :: l).toFinset.val = (insert a l.toFinset).val
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val

Tactic:
by_cases h : a ∈ l
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
h : a ∈ l
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val

Tactic:
simp [h]
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
h : a ∉ l
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val

Tactic:
simp [h]
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
hn : n ≠ 0
h : ∀ (x : α), x ∈ (replicate n a).toFinset ↔ Membership.mem (γ := Finset α) {a} x
⊢ (replicate n a).toFinset = {a}

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
hn : n ≠ 0
x : α
⊢ x ∈ (replicate n a).toFinset ↔ Membership.mem (γ := Finset α) {a} x

Tactic:
simp [hn, List.mem_replicate]

Premises used: List.mem_replicate
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
nil : Eq.{u_1 + 1} (α := Finset α) (toFinset []) ∅ ↔ Eq.{u_1 + 1} (α := List α) [] []
cons : ∀ (head : α) (tail : List α), (head :: tail).toFinset = ∅ ↔ head :: tail = []
⊢ l.toFinset = ∅ ↔ l = []

Tactic:
cases l
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := Finset α) (toFinset []) ∅ ↔ Eq.{u_1 + 1} (α := List α) [] []

Tactic:
simp
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
⊢ (head :: tail).toFinset = ∅ ↔ head :: tail = []

Tactic:
simp
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ l.toFinset.Nonempty ↔ l ≠ []

Tactic:
simp [Finset.nonempty_iff_ne_empty]

Premises used: Finset.nonempty_iff_ne_empty
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a : α
s : Finset α
rw : s.val.toList = [a] ↔ s = {a}
rw₁ : s.val = {a} ↔ s = {a}
rw₂ rw₃ : s = {a} ↔ s = {a}
⊢ s.toList = [a] ↔ s = {a}

Tactic:
rw [toList, Multiset.toList_eq_singleton_iff, val_eq_singleton_iff]

Premises used: Finset.toList, Multiset.toList_eq_singleton_iff, Finset.val_eq_singleton_iff
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
⊢ ∀ (a : α), toList {a} = [a]

Tactic:
Multiset.toList_singleton

Premises used: Finset.toList, Multiset.toList_singleton
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a : α
s : Finset α
h : a ∉ s
⊢ (a :: s.toList).Nodup

Tactic:
simp [h, nodup_toList s]

Premises used: Finset.nodup_toList
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a : α
s : Finset α
h : a ∉ s
x : α
⊢ x ∈ (cons a s h).toList ↔ x ∈ a :: s.toList

Tactic:
simp only [List.mem_cons, Finset.mem_toList, Finset.mem_cons]

Premises used: List.mem_cons, Finset.mem_toList, Finset.mem_cons
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ (insert a s).toList ~ a :: s.toList

Tactic:
cons_eq_insert _ _ h ▸ toList_cons _

Premises used: Finset.toList_cons, Eq.rec, Finset.cons_eq_insert
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
s : Finset α
a : α
ha : a ∉ s
r : β → β → Prop
f : α → β
simp :
  ((↑s : Set α).Pairwise (r on f) ∧ ∀ b ∈ (↑s : Set α), a ≠ b → (r on f) a b ∧ (r on f) b a) ↔
    (↑s : Set α).Pairwise (r on f) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)
⊢ _root_.Pairwise.{u_1} (α := ↥(cons a s ha)) (r on fun (a_1 : ↥(cons a s ha)) ↦ f (↑a_1 : α)) ↔
    _root_.Pairwise.{u_1} (α := ↥s) (r on fun (a : ↥s) ↦ f (↑a : α)) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)

Tactic:
simp only [pairwise_subtype_iff_pairwise_finset', Finset.coe_cons, Set.pairwise_insert]

Premises used: Finset.coe_cons, Set.pairwise_insert, Finset.pairwise_subtype_iff_pairwise_finset'
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
s : Finset α
a : α
ha : a ∉ s
r : β → β → Prop
f : α → β
⊢ ((↑s : Set α).Pairwise (r on f) ∧ ∀ b ∈ (↑s : Set α), a ≠ b → (r on f) a b ∧ (r on f) b a) ↔
    (↑s : Set α).Pairwise (r on f) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
r : α → α → Prop
⊢ _root_.Pairwise (α := ↥(cons a s ha)) (r on fun (a_1 : ↥(cons a s ha)) ↦ (↑a_1 : α)) ↔
    _root_.Pairwise (α := ↥s) (r on fun (a : ↥s) ↦ (↑a : α)) ∧ ∀ b ∈ s, r a b ∧ r b a

Tactic:
pairwise_cons' ha r id

Premises used: Finset.pairwise_cons', id
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t : Finset α
u₁ u₂ : ↥(t \ s).powerset
h :
  Eq.{u_1 + 1} (α := Finset α) ((fun (u : ↥(t \ s).powerset) ↦ (↑u : Finset α).disjUnion s ⋯) u₁)
    ((fun (u : ↥(t \ s).powerset) ↦ (↑u : Finset α).disjUnion s ⋯) u₂)
⊢ u₁ = u₂

Tactic:
simpa only [disjUnion_inj_left, Subtype.ext_iff] using h

Premises used: Finset.disjUnion_inj_left, Subtype.ext_iff
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t u : Finset α
pos :
  ∀ (hst : s ⊆ t),
    Membership.mem (γ := Finset (Finset α))
        ((fun (s t : Finset α) ↦
            (if s ⊆ t then
                map { toFun := fun (u : ↥(t \ s).powerset) ↦ (↑u : Finset α).disjUnion s ⋯, inj' := ⋯ }
                  (t \ s).powerset.attach
              else ∅ :
              Finset (Finset α)))
          s t)
        u ↔
      s ≤ u ∧ u ≤ t
neg :
  ∀ (hst : ¬s ⊆ t),
    Membership.mem (γ := Finset (Finset α))
        ((fun (s t : Finset α) ↦
            (if s ⊆ t then
                map { toFun := fun (u : ↥(t \ s).powerset) ↦ (↑u : Finset α).disjUnion s ⋯, inj' := ⋯ }
                  (t \ s).powerset.attach
              else ∅ :
              Finset (Finset α)))
          s t)
        u ↔
      s ≤ u ∧ u ≤ t
⊢ Membership.mem (γ := Finset (Finset α))
      ((fun (s t : Finset α) ↦
          (if s ⊆ t then
              map { toFun := fun (u : ↥(t \ s).powerset) ↦ (↑u : Finset α).disjUnion s ⋯, inj' := ⋯ }
                (t \ s).powerset.attach
            else ∅ :
            Finset (Finset α)))
        s t)
      u ↔
    s ≤ u ∧ u ≤ t

Tactic:
by_cases hst : s ⊆ t
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t u : Finset α
hst : s ⊆ t
this : (∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u) ↔ s ⊆ u ∧ u ⊆ t
⊢ Membership.mem (γ := Finset (Finset α))
      ((fun (s t : Finset α) ↦
          (if s ⊆ t then
              map { toFun := fun (u : ↥(t \ s).powerset) ↦ (↑u : Finset α).disjUnion s ⋯, inj' := ⋯ }
                (t \ s).powerset.attach
            else ∅ :
            Finset (Finset α)))
        s t)
      u ↔
    s ≤ u ∧ u ≤ t

Tactic:
simpa [hst, subset_sdiff, and_assoc]

Premises used: Finset.subset_sdiff, and_assoc
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t u : Finset α
hst : s ⊆ t
pos : (∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u) ↔ s ⊆ u ∧ u ⊆ t
⊢ Membership.mem (γ := Finset (Finset α))
      ((fun (s t : Finset α) ↦
          (if s ⊆ t then
              map { toFun := fun (u : ↥(t \ s).powerset) ↦ (↑u : Finset α).disjUnion s ⋯, inj' := ⋯ }
                (t \ s).powerset.attach
            else ∅ :
            Finset (Finset α)))
        s t)
      u ↔
    s ≤ u ∧ u ≤ t

Tactic:
suffices (∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u) ↔ s ⊆ u ∧ u ⊆ t by
          simpa [hst, subset_sdiff, and_assoc]
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t u : Finset α
hst : s ⊆ t
pos : (∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u) → s ⊆ u ∧ u ⊆ t
pos₁ : s ⊆ u ∧ u ⊆ t → ∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u
⊢ (∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u) ↔ s ⊆ u ∧ u ⊆ t

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t : Finset α
hst : s ⊆ t
u : Finset α
hut : u ⊆ t
⊢ s ⊆ u ∪ s ∧ u ∪ s ⊆ t

Tactic:
⟨subset_union_right, union_subset hut hst⟩

Premises used: Finset.union_subset, And.intro, Finset.subset_union_right
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t : Finset α
hst : s ⊆ t
u : Finset α
hut : u ⊆ t
⊢ s ⊆ u ∪ s ∧ u ∪ s ⊆ t

Tactic:
exact ⟨subset_union_right, union_subset hut hst⟩
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t u : Finset α
hst : s ⊆ t
hsu : s ⊆ u
hut : u ⊆ t
⊢ ∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u

Tactic:
⟨u \ s, sdiff_subset.trans hut, disjoint_sdiff_self_left, sdiff_union_of_subset hsu⟩

Premises used: HasSubset.Subset.trans, Finset.sdiff_union_of_subset, SDiff.sdiff, And.intro, Exists.intro, disjoint_sdiff_self_left, Finset.sdiff_subset
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t u : Finset α
hst : s ⊆ t
hsu : s ⊆ u
hut : u ⊆ t
⊢ ∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u

Tactic:
exact ⟨u \ s, sdiff_subset.trans hut, disjoint_sdiff_self_left, sdiff_union_of_subset hsu⟩
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t u : Finset α
hst : ¬s ⊆ t
this : s ⊆ u → ¬u ⊆ t
⊢ Membership.mem (γ := Finset (Finset α))
      ((fun (s t : Finset α) ↦
          (if s ⊆ t then
              map { toFun := fun (u : ↥(t \ s).powerset) ↦ (↑u : Finset α).disjUnion s ⋯, inj' := ⋯ }
                (t \ s).powerset.attach
            else ∅ :
            Finset (Finset α)))
        s t)
      u ↔
    s ≤ u ∧ u ≤ t

Tactic:
simpa [hst]
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t u : Finset α
hst : ¬s ⊆ t
neg : s ⊆ u → ¬u ⊆ t
⊢ Membership.mem (γ := Finset (Finset α))
      ((fun (s t : Finset α) ↦
          (if s ⊆ t then
              map { toFun := fun (u : ↥(t \ s).powerset) ↦ (↑u : Finset α).disjUnion s ⋯, inj' := ⋯ }
                (t \ s).powerset.attach
            else ∅ :
            Finset (Finset α)))
        s t)
      u ↔
    s ≤ u ∧ u ≤ t

Tactic:
suffices s ⊆ u → ¬u ⊆ t by simpa [hst]
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t u : Finset α
hst : ¬s ⊆ t
⊢ s ⊆ u → ¬u ⊆ t

Tactic:
fun hsu hut ↦ hst (hsu.trans hut)

Premises used: HasSubset.Subset.trans, Not
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t u : Finset α
hst : ¬s ⊆ t
⊢ s ⊆ u → ¬u ⊆ t

Tactic:
exact fun hsu hut ↦ hst (hsu.trans hut)
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : ∀ (a : Finset α), a ∈ Icc s t ↔ a ∈ {u ∈ t.powerset | s ⊆ u}
⊢ Icc s t = {u ∈ t.powerset | s ⊆ u}

Tactic:
ext
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t a : Finset α
⊢ a ∈ Icc s t ↔ a ∈ {u ∈ t.powerset | s ⊆ u}

Tactic:
simp [and_comm]

Premises used: and_comm
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : ∀ (a : Finset α), a ∈ Ico s t ↔ a ∈ {u ∈ t.ssubsets | s ⊆ u}
⊢ Ico s t = {u ∈ t.ssubsets | s ⊆ u}

Tactic:
ext
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t a : Finset α
⊢ a ∈ Ico s t ↔ a ∈ {u ∈ t.ssubsets | s ⊆ u}

Tactic:
simp [and_comm]

Premises used: and_comm
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : ∀ (a : Finset α), a ∈ Ioc s t ↔ a ∈ {u ∈ t.powerset | s ⊂ u}
⊢ Ioc s t = {u ∈ t.powerset | s ⊂ u}

Tactic:
ext
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t a : Finset α
⊢ a ∈ Ioc s t ↔ a ∈ {u ∈ t.powerset | s ⊂ u}

Tactic:
simp [and_comm]

Premises used: and_comm
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : ∀ (a : Finset α), a ∈ Ioo s t ↔ a ∈ {u ∈ t.ssubsets | s ⊂ u}
⊢ Ioo s t = {u ∈ t.ssubsets | s ⊂ u}

Tactic:
ext
-- Module: Mathlib.Data.Finset.Interval
Goal:
α : Type u_1
inst : DecidableEq α
s t a : Finset α
⊢ a ∈ Ioo s t ↔ a ∈ {u ∈ t.ssubsets | s ⊂ u}

Tactic:
simp [and_comm]

Premises used: and_comm