awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Basic
Goal:
ι : Type u_5
inst : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α (↑i : ι)
g : (i : ↥t) → α (↑i : ι)
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
simp_rw :
  Eq.{u_4 + 1} (α := α i)
    (Eq.rec (motive :=
        fun (x : ↥(s ∪ t))
          (x_1 :
            (Equiv.symm (Equiv.symm (Finset.union s t h)) : (a : ↥s ⊕ ↥t) → ↥(s ∪ t))
                ((Equiv.symm (Finset.union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t)
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi')) =
              x) ↦
        α (↑x : ι))
        (Sum.rec (motive := fun (x : ↥s ⊕ ↥t) ↦ α (↑((Finset.union s t h : (a : ↥s ⊕ ↥t) → ↥(s ∪ t)) x) : ι)) f g
          ((Equiv.symm (Finset.union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t)
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi')))
        ⋯ :
      α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    (f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))
⊢ Eq.{u_4 + 1} (α := α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    ((piFinsetUnion α h : (a : ((i : ↥s) → α (↑i : ι)) × ((i : ↥t) → α (↑i : ι))) → (i : ↥(s ∪ t)) → α (↑i : ι)) (f, g)
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') :
      α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    (f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))

Tactic:
simp_rw [piFinsetUnion, sumPiEquivProdPi, piCongrLeft, piCongrLeft', trans_apply, coe_fn_symm_mk]

Premises used: Equiv.coe_fn_symm_mk, Equiv.trans_apply, Equiv.piFinsetUnion, Equiv.piCongrLeft, Equiv.sumPiEquivProdPi, Equiv.piCongrLeft'
-- Module: Mathlib.Data.Finset.Basic
Goal:
ι : Type u_5
inst : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α (↑i : ι)
g : (i : ↥t) → α (↑i : ι)
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
rw! :
  Eq.{u_4 + 1} (α := α i)
    (@Eq.rec _ _
        (fun (x : ↥(s ∪ t))
            (x_1 :
              (Equiv.symm (Equiv.symm (Finset.union s t h)) : (a : ↥s ⊕ ↥t) → ↥(s ∪ t))
                  (Sum.inl (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) =
                x) ↦
          α (↑x : ι))
        (Sum.rec (motive := fun (x : ↥s ⊕ ↥t) ↦ α (↑((Finset.union s t h : (a : ↥s ⊕ ↥t) → ↥(s ∪ t)) x) : ι)) f g
          (Sum.inl (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)))
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') ⋯ :
      α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    (f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))
⊢ Eq.{u_4 + 1} (α := α i)
    (Eq.rec (motive :=
        fun (x : ↥(s ∪ t))
          (x_1 :
            (Equiv.symm (Equiv.symm (Finset.union s t h)) : (a : ↥s ⊕ ↥t) → ↥(s ∪ t))
                ((Equiv.symm (Finset.union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t)
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi')) =
              x) ↦
        α (↑x : ι))
        (Sum.rec (motive := fun (x : ↥s ⊕ ↥t) ↦ α (↑((Finset.union s t h : (a : ↥s ⊕ ↥t) → ↥(s ∪ t)) x) : ι)) f g
          ((Equiv.symm (Finset.union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t)
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi')))
        ⋯ :
      α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    (f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))

Tactic:
rw! [Finset.union_symm_left h hi hi']

Premises used: Equiv.Finset.union_symm_left
-- Module: Mathlib.Data.Finset.Basic
Goal:
ι : Type u_5
inst : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α (↑i : ι)
g : (i : ↥t) → α (↑i : ι)
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ Eq.{u_4 + 1} (α := α i)
    (@Eq.rec _ _
        (fun (x : ↥(s ∪ t))
            (x_1 :
              (Equiv.symm (Equiv.symm (Finset.union s t h)) : (a : ↥s ⊕ ↥t) → ↥(s ∪ t))
                  (Sum.inl (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) =
                x) ↦
          α (↑x : ι))
        (Sum.rec (motive := fun (x : ↥s ⊕ ↥t) ↦ α (↑((Finset.union s t h : (a : ↥s ⊕ ↥t) → ↥(s ∪ t)) x) : ι)) f g
          (Sum.inl (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)))
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') ⋯ :
      α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    (f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Basic
Goal:
ι : Type u_5
inst : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α (↑i : ι)
g : (i : ↥t) → α (↑i : ι)
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
simp_rw :
  Eq.{u_4 + 1} (α := α i)
    (Eq.rec (motive :=
        fun (x : ↥(s ∪ t))
          (x_1 :
            (Equiv.symm (Equiv.symm (Finset.union s t h)) : (a : ↥s ⊕ ↥t) → ↥(s ∪ t))
                ((Equiv.symm (Finset.union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t)
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi')) =
              x) ↦
        α (↑x : ι))
        (Sum.rec (motive := fun (x : ↥s ⊕ ↥t) ↦ α (↑((Finset.union s t h : (a : ↥s ⊕ ↥t) → ↥(s ∪ t)) x) : ι)) f g
          ((Equiv.symm (Finset.union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t)
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi')))
        ⋯ :
      α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    (g (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : ι))
⊢ Eq.{u_4 + 1} (α := α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    ((piFinsetUnion α h : (a : ((i : ↥s) → α (↑i : ι)) × ((i : ↥t) → α (↑i : ι))) → (i : ↥(s ∪ t)) → α (↑i : ι)) (f, g)
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') :
      α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    (g (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : ι))

Tactic:
simp_rw [piFinsetUnion, sumPiEquivProdPi, piCongrLeft, piCongrLeft', trans_apply, coe_fn_symm_mk]

Premises used: Equiv.coe_fn_symm_mk, Equiv.trans_apply, Equiv.piFinsetUnion, Equiv.piCongrLeft, Equiv.sumPiEquivProdPi, Equiv.piCongrLeft'
-- Module: Mathlib.Data.Finset.Basic
Goal:
ι : Type u_5
inst : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α (↑i : ι)
g : (i : ↥t) → α (↑i : ι)
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
rw! :
  Eq.{u_4 + 1} (α := α i)
    (@Eq.rec _ _
        (fun (x : ↥(s ∪ t))
            (x_1 :
              (Equiv.symm (Equiv.symm (Finset.union s t h)) : (a : ↥s ⊕ ↥t) → ↥(s ∪ t))
                  (Sum.inr (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi)) =
                x) ↦
          α (↑x : ι))
        (Sum.rec (motive := fun (x : ↥s ⊕ ↥t) ↦ α (↑((Finset.union s t h : (a : ↥s ⊕ ↥t) → ↥(s ∪ t)) x) : ι)) f g
          (Sum.inr (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi)))
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') ⋯ :
      α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    (g (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : ι))
⊢ Eq.{u_4 + 1} (α := α i)
    (Eq.rec (motive :=
        fun (x : ↥(s ∪ t))
          (x_1 :
            (Equiv.symm (Equiv.symm (Finset.union s t h)) : (a : ↥s ⊕ ↥t) → ↥(s ∪ t))
                ((Equiv.symm (Finset.union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t)
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi')) =
              x) ↦
        α (↑x : ι))
        (Sum.rec (motive := fun (x : ↥s ⊕ ↥t) ↦ α (↑((Finset.union s t h : (a : ↥s ⊕ ↥t) → ↥(s ∪ t)) x) : ι)) f g
          ((Equiv.symm (Finset.union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t)
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi')))
        ⋯ :
      α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    (g (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : ι))

Tactic:
rw! [Finset.union_symm_right h hi hi']

Premises used: Equiv.Finset.union_symm_right
-- Module: Mathlib.Data.Finset.Basic
Goal:
ι : Type u_5
inst : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α (↑i : ι)
g : (i : ↥t) → α (↑i : ι)
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ Eq.{u_4 + 1} (α := α i)
    (@Eq.rec _ _
        (fun (x : ↥(s ∪ t))
            (x_1 :
              (Equiv.symm (Equiv.symm (Finset.union s t h)) : (a : ↥s ⊕ ↥t) → ↥(s ∪ t))
                  (Sum.inr (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi)) =
                x) ↦
          α (↑x : ι))
        (Sum.rec (motive := fun (x : ↥s ⊕ ↥t) ↦ α (↑((Finset.union s t h : (a : ↥s ⊕ ↥t) → ↥(s ∪ t)) x) : ι)) f g
          (Sum.inr (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi)))
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') ⋯ :
      α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i hi') : ι))
    (g (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) : ι))

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
a : α
h : ∀ (x : α), x ∈ (replicate n a).toFinset ↔ Membership.mem (γ := Finset α) (if n = 0 then ∅ else {a}) x
⊢ (replicate n a).toFinset = if n = 0 then ∅ else {a}

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
a x : α
h : n ≠ 0 ∧ x = a ↔ Membership.mem (γ := Finset α) (if n = 0 then ∅ else {a}) x
⊢ x ∈ (replicate n a).toFinset ↔ Membership.mem (γ := Finset α) (if n = 0 then ∅ else {a}) x

Tactic:
simp only [mem_toFinset, mem_replicate]

Premises used: Multiset.mem_replicate, Multiset.mem_toFinset
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
a x : α
pos : ∀ (hn : n = 0), n ≠ 0 ∧ x = a ↔ Membership.mem (γ := Finset α) ∅ x
neg : ∀ (hn : ¬n = 0), n ≠ 0 ∧ x = a ↔ Membership.mem (γ := Finset α) {a} x
⊢ n ≠ 0 ∧ x = a ↔ Membership.mem (γ := Finset α) (if n = 0 then ∅ else {a}) x

Tactic:
split_ifs with hn
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
a x : α
hn : n = 0
⊢ n ≠ 0 ∧ x = a ↔ Membership.mem (γ := Finset α) ∅ x

Tactic:
simp [hn]
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
a x : α
hn : ¬n = 0
⊢ n ≠ 0 ∧ x = a ↔ Membership.mem (γ := Finset α) {a} x

Tactic:
simp [hn]
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
rw : x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
⊢ x ∈ s ∪ t ↔ Xor (x ∈ s) (x ∈ t)

Tactic:
rw [Finset.mem_union, Xor]

Premises used: Xor, Finset.mem_union
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
⊢ ∀ ⦃a : α⦄, a ∈ s → a ∉ t

Tactic:
have := disjoint_left.1 h
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_4
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
this : ∀ ⦃a : α⦄, a ∈ s → a ∉ t
mp : x ∈ s ∨ x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mpr : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → x ∈ s ∨ x ∈ t
mp₁ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₂ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₃ : x ∈ s → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₄ : x ∈ t → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
mp₅ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
mp₆ : x ∈ s → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
mp₇ : x ∈ t → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
mp₈ : x ∈ t → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
mpr₁ : x ∈ s → x ∉ t → x ∈ s ∨ x ∈ t
mpr₂ : x ∈ t → x ∉ s → x ∈ s ∨ x ∈ t
mpr₃ : x ∈ s → x ∉ t → x ∈ s ∨ x ∈ t
mpr₄ : x ∈ t → x ∉ s → x ∈ s ∨ x ∈ t
mpr₅ : x ∈ s → x ∉ t → x ∉ s → x ∈ t
mpr₆ : x ∈ t → x ∉ s → x ∉ s → x ∈ t
mp₉ : x ∈ s → x ∉ s → x ∈ t
mp₁₀ mp₁₁ mp₁₂ : x ∈ s → ¬x ∉ t → x ∈ t
mp₁₃ : x ∈ s → x ∈ s → x ∉ s → False
mp₁₄ mp₁₅ mp₁₆ : x ∈ s → x ∈ s → ¬x ∉ t → False
mp₁₇ : x ∈ t → x ∈ s → x ∉ s → False
mp₁₈ mp₁₉ mp₂₀ : x ∈ t → x ∈ s → ¬x ∉ t → False
mpr₇ : x ∈ s → x ∉ t → x ∉ s → x ∈ t
mp₂₁ mp₂₂ mp₂₃ : x ∈ s → x ∈ t → x ∈ t
mp₂₄ mp₂₅ mp₂₆ : x ∈ s → x ∈ s → x ∈ t → False
mp₂₇ mp₂₈ mp₂₉ : x ∈ t → x ∈ s → x ∈ t → False
mp₃₀ mp₃₁ mp₃₂ : x ∈ s → x ∈ s → x ∈ t → False
mp₃₃ mp₃₄ mp₃₅ : x ∈ t → x ∈ s → x ∈ t → False
mp₃₆ mp₃₇ : x ∈ s → x ∈ s → x ∈ t → False
mp₃₈ mp₃₉ : x ∈ t → x ∈ s → x ∈ t → False
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s

Tactic:
tauto
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_4
h : IsEmpty α
S : Finset α
hS : Membership.mem (γ := Set (Finset α)) Set.univ S
⊢ Membership.mem (γ := Set (Finset α)) {∅} S

Tactic:
simp [Finset.eq_empty_of_isEmpty S]

Premises used: Finset.eq_empty_of_isEmpty
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_4
h : IsEmpty α
⊢ Subset (α := Set (Finset α)) {∅} Set.univ

Tactic:
simp
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_4
H : ∀ (s : Finset α), s = ∅
a : α
⊢ Eq (α := Finset α) {a} ∅

Tactic:
specialize H {a}

Premises used: Singleton.singleton
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_4
a : α
H : Eq (α := Finset α) {a} ∅
⊢ False

Tactic:
aesop
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_4
h : IsEmpty α
⊢ Eq (α := Set (Finset α)) Set.univ {∅}

Tactic:
simp
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : Subsingleton α
x : α
hx : x ∈ s
y : α
rwa rwa₁ rwa₂ rwa₃ : x ∈ s
⊢ y ∈ s

Tactic:
rwa [Subsingleton.elim y x]

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : Subsingleton α
x : α
hx : x ∈ s
⊢ s = univ

Tactic:
exact eq_univ_of_forall fun y => by rwa [Subsingleton.elim y x]

Premises used: Finset.eq_univ_of_forall
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
rw : (↑univ : Set α).Nonempty ↔ Nonempty α
rw₁ : Set.Nonempty.{u_1} (α := α) Set.univ ↔ Nonempty α
rw₂ rw₃ : Set.Nonempty.{u_1} (α := α) Set.univ ↔ Set.Nonempty.{u_1} (α := α) Set.univ
⊢ Finset.Nonempty.{u_1} (α := α) univ ↔ Nonempty α

Tactic:
rw [← coe_nonempty, coe_univ, Set.nonempty_iff_univ_nonempty]

Premises used: Finset.coe_univ, Finset.coe_nonempty, Set.nonempty_iff_univ_nonempty
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
⊢ Finset.Nonempty.{u_1} (α := α) univ

Tactic:
univ_nonempty_iff.2 ‹_›

Premises used: Iff.mpr, Finset.univ_nonempty_iff
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
contrapose! : Finset.Nonempty.{u_1} (α := α) univ ↔ Nonempty α
⊢ Eq.{u_1 + 1} (α := Finset α) univ ∅ ↔ IsEmpty α

Tactic:
contrapose!
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
⊢ Finset.Nonempty.{u_1} (α := α) univ ↔ Nonempty α

Tactic:
univ_nonempty_iff

Premises used: Finset.univ_nonempty_iff
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
⊢ Finset.Nonempty.{u_1} (α := α) univ ↔ Nonempty α

Tactic:
exact univ_nonempty_iff

Premises used: Finset.univ_nonempty_iff
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
rw : (↑univ : Set α).Nontrivial ↔ Nontrivial α
rw₁ : Set.Nontrivial.{u_1} (α := α) Set.univ ↔ Nontrivial α
rw₂ rw₃ : Nontrivial α ↔ Nontrivial α
⊢ Finset.Nontrivial.{u_1} (α := α) univ ↔ Nontrivial α

Tactic:
rw [Finset.Nontrivial, Finset.coe_univ, Set.nontrivial_univ_iff]

Premises used: Finset.coe_univ, Finset.Nontrivial, Set.nontrivial_univ_iff
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_4
inst : Fintype α
inst_1 : Nonempty α
⊢ Ne.{u_4 + 1} (α := Finset α) univ ∅

Tactic:
fun h ↦ (Finset.univ_eq_empty_iff.1 h).elim (Classical.arbitrary _)

Premises used: IsEmpty.elim, Classical.arbitrary, Iff.mp, Not, Finset.univ_eq_empty_iff
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
h : Nontrivial α
⊢ Finset.Nontrivial.{u_1} (α := α) univ

Tactic:
univ_nontrivial_iff.mpr h

Premises used: Iff.mpr, Finset.univ_nontrivial_iff
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nontrivial α
a : α
apply : (↑{a} : Set α) ≠ (↑univ : Set α)
⊢ Ne (α := Finset α) {a} univ

Tactic:
apply SetLike.coe_ne_coe.1

Premises used: SetLike.coe_ne_coe, Iff.mp
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nontrivial α
a : α
⊢ (↑{a} : Set α) ≠ (↑univ : Set α)

Tactic:
simp
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : IsEmpty α
⊢ Eq.{u_1 + 1} (α := Finset α) univ ∅

Tactic:
univ_eq_empty_iff.2 ‹_›

Premises used: Iff.mpr, Finset.univ_eq_empty_iff
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Unique α
⊢ Eq (α := Finset α) univ {default}

Tactic:
Finset.ext fun x => iff_of_true (mem_univ _) <| mem_singleton.2 <| Subsingleton.elim x default

Premises used: Iff.mpr, Finset.mem_univ, Inhabited.default, Finset.mem_singleton, Finset.ext, iff_of_true, Subsingleton.elim
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
⊢ Eq.{u_1 + 1} (α := Finset α) ⊤ univ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
⊢ s ⊂ univ ↔ s ≠ univ

Tactic:
@lt_top_iff_ne_top _ _ _ s

Premises used: Set.Mem, setOf, lt_top_iff_ne_top, Set.Subset
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
⊢ univ ⊆ s ↔ s = univ

Tactic:
@top_le_iff _ _ _ s

Premises used: Set.Mem, setOf, top_le_iff
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s t : Finset α
inst : Fintype α
⊢ Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ s → a ∈ t

Tactic:
simp [codisjoint_iff, eq_univ_iff_forall, or_iff_not_imp_left]

Premises used: Finset.eq_univ_iff_forall, codisjoint_iff, Classical.or_iff_not_imp_left
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s t : Finset α
inst : Fintype α
⊢ Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ s → a ∈ t

Tactic:
classical simp [codisjoint_iff, eq_univ_iff_forall, or_iff_not_imp_left]

Premises used: Finset.eq_univ_iff_forall, codisjoint_iff, Classical.or_iff_not_imp_left
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s t : Finset α
inst : Fintype α
⊢ Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ t → a ∈ s

Tactic:
codisjoint_comm.trans codisjoint_left

Premises used: Finset.codisjoint_left, codisjoint_comm, Iff.trans
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
⊢ s \ t = s ∩ tᶜ

Tactic:
sdiff_eq

Premises used: sdiff_eq
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ sᶜ = univ \ s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
a : α
⊢ a ∈ sᶜ ↔ a ∉ s

Tactic:
simp [compl_eq_univ_sdiff]

Premises used: Finset.compl_eq_univ_sdiff
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
a : α
rw : ¬a ∉ s ↔ a ∈ s
rw₁ rw₂ : a ∈ s ↔ a ∈ s
⊢ a ∉ sᶜ ↔ a ∈ s

Tactic:
rw [mem_compl, not_not]

Premises used: Classical.not_not, Finset.mem_compl
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ (↑sᶜ : Set α) = (↑s : Set α)ᶜ

Tactic:
Set.ext fun _ => mem_compl

Premises used: Set.ext, Finset.mem_compl
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s t : Finset α
inst : Fintype α
inst_1 : DecidableEq α
⊢ sᶜ ⊆ tᶜ ↔ t ⊆ s

Tactic:
@compl_le_compl_iff_le (Finset α) _ _ _

Premises used: compl_le_compl_iff_le
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s t : Finset α
inst : Fintype α
inst_1 : DecidableEq α
⊢ sᶜ ⊂ tᶜ ↔ t ⊂ s

Tactic:
@compl_lt_compl_iff_lt (Finset α) _ _ _

Premises used: compl_lt_compl_iff_lt, Set.Subset
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s t : Finset α
inst : Fintype α
inst_1 : DecidableEq α
⊢ s ⊆ tᶜ ↔ t ⊆ sᶜ

Tactic:
le_compl_iff_le_compl (α := Finset α)

Premises used: Set.Mem, setOf, le_compl_iff_le_compl
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s t : Finset α
inst : Fintype α
inst_1 : DecidableEq α
⊢ s ⊆ tᶜ ↔ Disjoint s t

Tactic:
le_compl_iff_disjoint_right (α := Finset α)

Premises used: Set.Mem, setOf, le_compl_iff_disjoint_right
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s t : Finset α
inst : Fintype α
inst_1 : DecidableEq α
⊢ s ⊆ tᶜ ↔ Disjoint t s

Tactic:
le_compl_iff_disjoint_left (α := Finset α)

Premises used: Set.Mem, setOf, le_compl_iff_disjoint_left
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
a : α
rw : {a} ⊆ sᶜ ↔ a ∉ s
rw₁ : a ∈ sᶜ ↔ a ∉ s
rw₂ rw₃ : a ∉ s ↔ a ∉ s
⊢ s ⊆ {a}ᶜ ↔ a ∉ s

Tactic:
rw [subset_compl_comm, singleton_subset_iff, mem_compl]

Premises used: Finset.singleton_subset_iff, Finset.mem_compl, Finset.subset_compl_comm
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ Eq.{u_1 + 1} (α := Finset α) ∅ᶜ univ

Tactic:
compl_bot

Premises used: compl_bot
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ Eq.{u_1 + 1} (α := Finset α) univᶜ ∅

Tactic:
compl_top

Premises used: compl_top
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ sᶜ = ∅ ↔ s = univ

Tactic:
compl_eq_bot

Premises used: compl_eq_bot
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ sᶜ = univ ↔ s = ∅

Tactic:
compl_eq_top

Premises used: compl_eq_top
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ s ∪ sᶜ = univ

Tactic:
sup_compl_eq_top

Premises used: sup_compl_eq_top
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ s ∩ sᶜ = ∅

Tactic:
inf_compl_eq_bot

Premises used: inf_compl_eq_bot
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
⊢ (s ∪ t)ᶜ = sᶜ ∩ tᶜ

Tactic:
compl_sup

Premises used: compl_sup
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s t : Finset α
⊢ (s ∩ t)ᶜ = sᶜ ∪ tᶜ

Tactic:
compl_inf

Premises used: compl_inf
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
a : α
h : ∀ (a_1 : α), a_1 ∈ (s.erase a)ᶜ ↔ a_1 ∈ insert a sᶜ
⊢ (s.erase a)ᶜ = insert a sᶜ

Tactic:
ext
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
a a_1 : α
⊢ a_1 ∈ (s.erase a)ᶜ ↔ a_1 ∈ insert a sᶜ

Tactic:
simp only [or_iff_not_imp_left, mem_insert, not_and, mem_compl, mem_erase]

Premises used: Finset.mem_insert, Finset.mem_compl, Finset.mem_erase, Classical.or_iff_not_imp_left, not_and
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
a : α
h : ∀ (a_1 : α), a_1 ∈ (insert a s)ᶜ ↔ a_1 ∈ sᶜ.erase a
⊢ (insert a s)ᶜ = sᶜ.erase a

Tactic:
ext
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
a a_1 : α
⊢ a_1 ∈ (insert a s)ᶜ ↔ a_1 ∈ sᶜ.erase a

Tactic:
simp only [not_or, mem_insert, mem_compl, mem_erase]

Premises used: Finset.mem_insert, Finset.mem_compl, not_or, Finset.mem_erase
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
a : α
ha : a ∉ s
simp_rw : insert a (sᶜ.erase a) = sᶜ
⊢ insert a (insert a s)ᶜ = sᶜ

Tactic:
simp_rw [compl_insert, insert_erase (mem_compl.2 ha)]

Premises used: Iff.mpr, Finset.compl_insert, Finset.mem_compl, Finset.insert_erase
-- Module: Mathlib.Data.Finset.BooleanAlgebra
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
rw : (erase {x} x)ᶜ = univ
rw₁ : Eq.{u_1 + 1} (α := Finset α) ∅ᶜ univ
rw₂ rw₃ : Eq.{u_1 + 1} (α := Finset α) univ univ
⊢ Eq (α := Finset α) (insert x {x}ᶜ) univ

Tactic:
rw [← compl_erase, erase_singleton, compl_empty]

Premises used: Finset.compl_erase, Finset.compl_empty, Finset.erase_singleton