awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t : Finset α
⊢ (∃ (x : α), ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ (x : α), x ∈ t

Tactic:
exact fun ⟨_, _, _, b, hb, _⟩ => ⟨b, hb⟩
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
t : Finset α
⊢ ∅ ○ t = ∅

Tactic:
simp [disjSups]

Premises used: Finset.disjSups
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s : Finset α
⊢ s ○ ∅ = ∅

Tactic:
simp [disjSups]

Premises used: Finset.disjSups
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
a b : α
pos : ∀ (h : Disjoint a b), Eq (α := Finset α) ({a} ○ {b}) {a ⊔ b}
neg : ∀ (h : ¬Disjoint a b), Eq (α := Finset α) ({a} ○ {b}) ∅
⊢ Eq (α := Finset α) ({a} ○ {b}) (if Disjoint a b then {a ⊔ b} else ∅)

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
a b : α
h : Disjoint a b
⊢ Eq (α := Finset α) ({a} ○ {b}) {a ⊔ b}

Tactic:
simp [disjSups, filter_singleton, h]

Premises used: Finset.disjSups, Finset.filter_singleton
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
a b : α
h : ¬Disjoint a b
⊢ Eq (α := Finset α) ({a} ○ {b}) ∅

Tactic:
simp [disjSups, filter_singleton, h]

Premises used: Finset.disjSups, Finset.filter_singleton
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s₁ s₂ t : Finset α
⊢ (s₁ ∪ s₂) ○ t = s₁ ○ t ∪ s₂ ○ t

Tactic:
simp [disjSups, filter_union, image_union]

Premises used: Finset.image_union, Finset.disjSups, Finset.filter_union
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t₁ t₂ : Finset α
⊢ s ○ (t₁ ∪ t₂) = s ○ t₁ ∪ s ○ t₂

Tactic:
simp [disjSups, filter_union, image_union]

Premises used: Finset.image_union, Finset.disjSups, Finset.filter_union
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s₁ s₂ t : Finset α
⊢ (s₁ ∩ s₂) ○ t ⊆ s₁ ○ t ∩ s₂ ○ t

Tactic:
simpa only [disjSups, inter_product, filter_inter_distrib] using image_inter_subset _ _ _

Premises used: Finset.image_inter_subset, Finset.disjSups, Finset.inter_product, Finset.filter_inter_distrib
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t₁ t₂ : Finset α
⊢ s ○ (t₁ ∩ t₂) ⊆ s ○ t₁ ∩ s ○ t₂

Tactic:
simpa only [disjSups, product_inter, filter_inter_distrib] using image_inter_subset _ _ _

Premises used: Finset.product_inter, Finset.image_inter_subset, Finset.disjSups, Finset.filter_inter_distrib
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t : Finset α
⊢ s ○ t = t ○ s

Tactic:
aesop (add simp disjoint_comm, simp sup_comm)

Premises used: disjoint_comm, sup_comm
-- Module: Mathlib.Data.Finset.Sups
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ Std.Commutative fun (x1 x2 : Finset α) ↦ x1 ○ x2

Tactic:
⟨disjSups_comm⟩

Premises used: Finset.disjSups_comm, Std.Commutative.mk
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
⊢ ∀ (s t u : Finset α), s ○ t ○ u = s ○ (t ○ u)

Tactic:
(associative_of_commutative_of_le inferInstance ?_).assoc

Premises used: Std.Associative.assoc
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
refine : ∀ (a b c : Finset α), a ○ b ○ c ≤ a ○ (b ○ c)
⊢ ∀ (s t u : Finset α), s ○ t ○ u = s ○ (t ○ u)

Tactic:
refine (associative_of_commutative_of_le inferInstance ?_).assoc

Premises used: Std.Associative.assoc
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
simp :
  ∀ (a b c : Finset α) (a_1 : α),
    (∃ a_2 ∈ a, ∃ b_1 ∈ b, Disjoint a_2 b_1 ∧ a_2 ⊔ b_1 = a_1) →
      ∀ b_1 ∈ c,
        Disjoint a_1 b_1 →
          ∃ a_5 ∈ a,
            ∃ (b_2 : α), (∃ a ∈ b, ∃ b ∈ c, Disjoint a b ∧ a ⊔ b = b_2) ∧ Disjoint a_5 b_2 ∧ a_5 ⊔ b_2 = a_1 ⊔ b_1
⊢ ∀ (a b c : Finset α), a ○ b ○ c ≤ a ○ (b ○ c)

Tactic:
simp only [le_eq_subset, disjSups_subset_iff, mem_disjSups]

Premises used: Finset.disjSups_subset_iff, Finset.mem_disjSups, Finset.le_eq_subset
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t u : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
c : α
hc : c ∈ u
habc : Disjoint (a ⊔ b) c
⊢ Disjoint a c ∧ Disjoint b c

Tactic:
rw [disjoint_sup_left] at habc

Premises used: disjoint_sup_left
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t u : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
c : α
hc : c ∈ u
habc : Disjoint a c ∧ Disjoint b c
⊢ ∃ a_1 ∈ s, ∃ (b_1 : α), (∃ a ∈ t, ∃ b ∈ u, Disjoint a b ∧ a ⊔ b = b_1) ∧ Disjoint a_1 b_1 ∧ a_1 ⊔ b_1 = a ⊔ b ⊔ c

Tactic:
⟨a, ha, _, ⟨b, hb, c, hc, habc.2, rfl⟩, hab.sup_right habc.1, (sup_assoc ..).symm⟩

Premises used: sup_assoc, And.right, And.left, And.intro, Disjoint.sup_right, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t u : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
c : α
hc : c ∈ u
habc : Disjoint a c ∧ Disjoint b c
⊢ ∃ a_1 ∈ s, ∃ (b_1 : α), (∃ a ∈ t, ∃ b ∈ u, Disjoint a b ∧ a ⊔ b = b_1) ∧ Disjoint a_1 b_1 ∧ a_1 ⊔ b_1 = a ⊔ b ⊔ c

Tactic:
exact ⟨a, ha, _, ⟨b, hb, c, hc, habc.2, rfl⟩, hab.sup_right habc.1, (sup_assoc ..).symm⟩
-- Module: Mathlib.Data.Finset.Sups
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DistribLattice α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t u v : Finset α
⊢ Std.Associative fun (x1 x2 : Finset α) ↦ x1 ○ x2

Tactic:
⟨disjSups_assoc⟩

Premises used: Finset.disjSups_assoc, Std.Associative.mk
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t u : Finset α
simp_rw : s ○ t ○ u = t ○ s ○ u
⊢ s ○ (t ○ u) = t ○ (s ○ u)

Tactic:
simp_rw [← disjSups_assoc, disjSups_comm s]

Premises used: Finset.disjSups_comm, Finset.disjSups_assoc
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t u : Finset α
simp_rw : s ○ (t ○ u) = s ○ (u ○ t)
⊢ s ○ t ○ u = s ○ u ○ t

Tactic:
simp_rw [disjSups_assoc, disjSups_comm]

Premises used: Finset.disjSups_comm, Finset.disjSups_assoc
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t u v : Finset α
simp_rw : s ○ t ○ u ○ v = s ○ u ○ t ○ v
⊢ s ○ t ○ (u ○ v) = s ○ u ○ (t ○ v)

Tactic:
simp_rw [← disjSups_assoc, disjSups_right_comm]

Premises used: Finset.disjSups_right_comm, Finset.disjSups_assoc
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
c : α
⊢ c ∈ s \\ t ↔ ∃ a ∈ s, ∃ b ∈ t, a \ b = c

Tactic:
simp [(· \\ ·)]

Premises used: Finset.diffs
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
⊢ (↑(s \\ t) : Set α) = Set.image2 (fun (x1 x2 : α) ↦ x1 \ x2) (↑s : Set α) (↑t : Set α)

Tactic:
coe_image₂ _ _ _

Premises used: setOf, Finset.coe_image₂
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
⊢ #(s \\ t) ≤ #s * #t

Tactic:
card_image₂_le _ _ _

Premises used: Finset.diffs, Finset.card_image₂_le
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
⊢ #(s \\ t) = #s * #t ↔ Set.InjOn (β := α) (fun (x : α × α) ↦ x.1 \ x.2) ((↑s : Set α) ×ˢ (↑t : Set α))

Tactic:
card_image₂_iff

Premises used: Finset.diffs, Finset.card_image₂_iff
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
a b : α
⊢ a ∈ s → b ∈ t → a \ b ∈ s \\ t

Tactic:
mem_image₂_of_mem

Premises used: Set.Mem, setOf, Finset.mem_image₂_of_mem
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s₁ s₂ t₁ t₂ : Finset α
⊢ s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ \\ t₁ ⊆ s₂ \\ t₂

Tactic:
image₂_subset

Premises used: Set.Mem, setOf, Finset.image₂_subset
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t₁ t₂ : Finset α
⊢ t₁ ⊆ t₂ → s \\ t₁ ⊆ s \\ t₂

Tactic:
image₂_subset_left

Premises used: Set.Mem, setOf, Finset.image₂_subset_left
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s₁ s₂ t : Finset α
⊢ s₁ ⊆ s₂ → s₁ \\ t ⊆ s₂ \\ t

Tactic:
image₂_subset_right

Premises used: Set.Mem, setOf, Finset.image₂_subset_right
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
b : α
⊢ b ∈ t → image (fun (x : α) ↦ x \ b) s ⊆ s \\ t

Tactic:
image_subset_image₂_left

Premises used: Set.Mem, setOf, Finset.image_subset_image₂_left
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
a : α
⊢ a ∈ s → image (fun (x : α) ↦ a \ x) t ⊆ s \\ t

Tactic:
image_subset_image₂_right

Premises used: Set.Mem, setOf, Finset.image_subset_image₂_right
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
p : α → Prop
⊢ (∀ c ∈ s \\ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a \ b)

Tactic:
forall_mem_image₂

Premises used: Set.Mem, setOf, Finset.forall_mem_image₂
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t u : Finset α
⊢ s \\ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a \ b ∈ u

Tactic:
image₂_subset_iff

Premises used: Set.Mem, setOf, Finset.image₂_subset_iff
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
⊢ (s \\ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
image₂_nonempty_iff

Premises used: Finset.diffs, Finset.image₂_nonempty_iff
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
⊢ s.Nonempty → t.Nonempty → (s \\ t).Nonempty

Tactic:
Nonempty.image₂

Premises used: Finset.diffs, Finset.Nonempty.image₂
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
⊢ (s \\ t).Nonempty → s.Nonempty

Tactic:
Nonempty.of_image₂_left

Premises used: Finset.diffs, Finset.Nonempty.of_image₂_left
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
⊢ (s \\ t).Nonempty → t.Nonempty

Tactic:
Nonempty.of_image₂_right

Premises used: Finset.Nonempty.of_image₂_right, Finset.diffs
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
t : Finset α
⊢ ∅ \\ t = ∅

Tactic:
image₂_empty_left

Premises used: Finset.diffs, Finset.image₂_empty_left
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s : Finset α
⊢ s \\ ∅ = ∅

Tactic:
image₂_empty_right

Premises used: Finset.diffs, Finset.image₂_empty_right
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
⊢ s \\ t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
image₂_eq_empty_iff

Premises used: Finset.diffs, Finset.image₂_eq_empty_iff
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
t : Finset α
a : α
⊢ {a} \\ t = image (fun (x : α) ↦ a \ x) t

Tactic:
image₂_singleton_left

Premises used: Finset.diffs, Finset.image₂_singleton_left
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s : Finset α
b : α
⊢ s \\ {b} = image (fun (x : α) ↦ x \ b) s

Tactic:
image₂_singleton_right

Premises used: Finset.diffs, Finset.image₂_singleton_right
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
a b : α
⊢ Eq (α := Finset α) ({a} \\ {b}) {a \ b}

Tactic:
image₂_singleton

Premises used: Finset.diffs, Finset.image₂_singleton
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s₁ s₂ t : Finset α
⊢ (s₁ ∪ s₂) \\ t = s₁ \\ t ∪ s₂ \\ t

Tactic:
image₂_union_left

Premises used: Finset.diffs, Finset.image₂_union_left
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t₁ t₂ : Finset α
⊢ s \\ (t₁ ∪ t₂) = s \\ t₁ ∪ s \\ t₂

Tactic:
image₂_union_right

Premises used: Finset.diffs, Finset.image₂_union_right
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s₁ s₂ t : Finset α
⊢ (s₁ ∩ s₂) \\ t ⊆ s₁ \\ t ∩ s₂ \\ t

Tactic:
image₂_inter_subset_left

Premises used: Set.Mem, setOf, Finset.image₂_inter_subset_left
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t₁ t₂ : Finset α
⊢ s \\ (t₁ ∩ t₂) ⊆ s \\ t₁ ∩ s \\ t₂

Tactic:
image₂_inter_subset_right

Premises used: Set.Mem, setOf, Finset.image₂_inter_subset_right
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
u : Finset α
s t : Set α
⊢ (↑u : Set α) ⊆ Set.image2 (fun (x1 x2 : α) ↦ x1 \ x2) s t →
    ∃ (s' : Finset α) (t' : Finset α), (↑s' : Set α) ⊆ s ∧ (↑t' : Set α) ⊆ t ∧ u ⊆ s' \\ t'

Tactic:
subset_set_image₂

Premises used: Set.Mem, setOf, Finset.subset_set_image₂
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
⊢ (s.biUnion fun (a : α) ↦ image (fun (x : α) ↦ a \ x) t) = s \\ t

Tactic:
biUnion_image_left

Premises used: Finset.diffs, Finset.biUnion_image_left
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
⊢ (t.biUnion fun (b : α) ↦ image (fun (x : α) ↦ x \ b) s) = s \\ t

Tactic:
biUnion_image_right

Premises used: Finset.diffs, Finset.biUnion_image_right
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
⊢ image (uncurry fun (x1 x2 : α) ↦ x1 \ x2) (s ×ˢ t) = s \\ t

Tactic:
image_uncurry_product _ _ _

Premises used: Finset.diffs, Finset.image_uncurry_product
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t u : Finset α
⊢ s \\ t \\ u = s \\ u \\ t

Tactic:
image₂_right_comm sdiff_right_comm

Premises used: Finset.diffs, Finset.image₂_right_comm, sdiff_right_comm
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Finset α
a : α
rw : aᶜ ∈ s ↔ a ∈ sᶜˢ
rw₁ :
  Membership.mem (α := α) (map { toFun := compl, inj' := ⋯ : α ↪ α } s)
      (({ toFun := compl, inj' := ⋯ } : (a : α) → α) aᶜ : α) ↔
    a ∈ sᶜˢ
rw₂ : aᶜᶜ ∈ map { toFun := compl, inj' := ⋯ : α ↪ α } s ↔ a ∈ sᶜˢ
rw₃ : a ∈ map { toFun := compl, inj' := ⋯ : α ↪ α } s ↔ a ∈ sᶜˢ
rw₄ rw₅ : a ∈ map { toFun := compl, inj' := ⋯ : α ↪ α } s ↔ a ∈ map { toFun := compl, inj' := ⋯ : α ↪ α } s
⊢ a ∈ sᶜˢ ↔ aᶜ ∈ s

Tactic:
rw [Iff.comm, ← mem_map' ⟨compl, compl_injective⟩, Embedding.coeFn_mk, compl_compl, compls]

Premises used: compl_compl, Compl.compl, Finset.compls, Function.Embedding.mk, compl_injective, Function.Embedding.coeFn_mk, Iff.comm, Finset.mem_map'
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Finset α
inst_1 : DecidableEq α
⊢ image compl s = sᶜˢ

Tactic:
simp [compls, map_eq_image]

Premises used: Finset.compls, Finset.map_eq_image
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Finset α
⊢ (↑sᶜˢ : Set α) = compl '' (↑s : Set α)

Tactic:
coe_map _ _

Premises used: setOf, Finset.coe_map
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Finset α
⊢ #sᶜˢ = #s

Tactic:
card_map _

Premises used: Finset.card_map, Finset.compls
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Finset α
a : α
⊢ a ∈ s → aᶜ ∈ sᶜˢ

Tactic:
mem_map_of_mem _

Premises used: Set.Mem, setOf, Finset.mem_map_of_mem
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
s₁ s₂ : Finset α
⊢ s₁ᶜˢ ⊆ s₂ᶜˢ ↔ s₁ ⊆ s₂

Tactic:
map_subset_map

Premises used: Set.Mem, setOf, Finset.map_subset_map
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Finset α
p : α → Prop
⊢ (∀ a ∈ sᶜˢ, p a) ↔ ∀ a ∈ s, p aᶜ

Tactic:
forall_mem_map

Premises used: Finset.forall_mem_map, Set.Mem, setOf
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Finset α
p : α → Prop
⊢ (∃ a ∈ sᶜˢ, p a) ↔ ∃ a ∈ s, p aᶜ

Tactic:
aesop
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Finset α
h : ∀ (a : α), a ∈ sᶜˢᶜˢ ↔ a ∈ s
⊢ sᶜˢᶜˢ = s

Tactic:
ext
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Finset α
a : α
⊢ a ∈ sᶜˢᶜˢ ↔ a ∈ s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
s t : Finset α
rw : sᶜˢᶜˢ ⊆ tᶜˢ ↔ s ⊆ tᶜˢ
rw₁ rw₂ : s ⊆ tᶜˢ ↔ s ⊆ tᶜˢ
⊢ sᶜˢ ⊆ t ↔ s ⊆ tᶜˢ

Tactic:
rw [← compls_subset_compls, compls_compls]

Premises used: Finset.compls_compls, Finset.compls_subset_compls
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Finset α
⊢ sᶜˢ.Nonempty ↔ s.Nonempty

Tactic:
map_nonempty

Premises used: Finset.compls, Finset.map_nonempty
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
⊢ Eq.{u_2 + 1} (α := Finset α) ∅ᶜˢ ∅

Tactic:
map_empty _

Premises used: Finset.compls, Finset.map_empty
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Finset α
⊢ sᶜˢ = ∅ ↔ s = ∅

Tactic:
map_eq_empty

Premises used: Finset.compls, Finset.map_eq_empty
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
a : α
⊢ Eq (α := Finset α) {a}ᶜˢ {aᶜ}

Tactic:
map_singleton _ _

Premises used: Finset.compls, Finset.map_singleton
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : Fintype α
h : ∀ (a : α), Membership.mem (γ := Finset α) univᶜˢ a ↔ Membership.mem (γ := Finset α) univ a
⊢ Eq.{u_2 + 1} (α := Finset α) univᶜˢ univ

Tactic:
ext
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : Fintype α
a : α
⊢ Membership.mem (γ := Finset α) univᶜˢ a ↔ Membership.mem (γ := Finset α) univ a

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
⊢ (s ∪ t)ᶜˢ = sᶜˢ ∪ tᶜˢ

Tactic:
map_union _ _

Premises used: Finset.compls, Finset.map_union
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
⊢ (s ∩ t)ᶜˢ = sᶜˢ ∩ tᶜˢ

Tactic:
map_inter _ _

Premises used: Finset.compls, Finset.map_inter
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
simp_rw : image compl (s ⊼ t) = image compl s ⊻ image compl t
⊢ (s ⊼ t)ᶜˢ = sᶜˢ ⊻ tᶜˢ

Tactic:
simp_rw [← image_compl]

Premises used: Finset.image_compl
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
⊢ image compl (s ⊼ t) = image compl s ⊻ image compl t

Tactic:
image_image₂_distrib fun _ _ ↦ compl_inf

Premises used: compl_inf, Finset.image_image₂_distrib
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
⊢ image compl (s ⊼ t) = image compl s ⊻ image compl t

Tactic:
exact image_image₂_distrib fun _ _ ↦ compl_inf

Premises used: compl_inf, Finset.image_image₂_distrib
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
simp_rw : image compl (s ⊻ t) = image compl s ⊼ image compl t
⊢ (s ⊻ t)ᶜˢ = sᶜˢ ⊼ tᶜˢ

Tactic:
simp_rw [← image_compl]

Premises used: Finset.image_compl
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
⊢ image compl (s ⊻ t) = image compl s ⊼ image compl t

Tactic:
image_image₂_distrib fun _ _ ↦ compl_sup

Premises used: compl_sup, Finset.image_image₂_distrib
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
⊢ image compl (s ⊻ t) = image compl s ⊼ image compl t

Tactic:
exact image_image₂_distrib fun _ _ ↦ compl_sup

Premises used: compl_sup, Finset.image_image₂_distrib
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
h : ∀ (a : α), a ∈ s ⊼ tᶜˢ ↔ a ∈ s \\ t
⊢ s ⊼ tᶜˢ = s \\ t

Tactic:
ext
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
a : α
h : (∃ a_1 ∈ s, ∃ (b : α), bᶜ ∈ t ∧ a_1 ⊓ b = a) ↔ ∃ a_1 ∈ s, ∃ b ∈ t, a_1 ⊓ bᶜ = a
⊢ a ∈ s ⊼ tᶜˢ ↔ a ∈ s \\ t

Tactic:
simp [sdiff_eq]

Premises used: sdiff_eq
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
a : α
⊢ (∃ a_1 ∈ s, ∃ (b : α), bᶜ ∈ t ∧ a_1 ⊓ b = a) ↔ ∃ a_1 ∈ s, ∃ b ∈ t, a_1 ⊓ bᶜ = a

Tactic:
aesop
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
rw : t ⊼ sᶜˢ = t \\ s
rw₁ rw₂ : t \\ s = t \\ s
⊢ sᶜˢ ⊼ t = t \\ s

Tactic:
rw [infs_comm, infs_compls_eq_diffs]

Premises used: Finset.infs_comm, Finset.infs_compls_eq_diffs
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : BooleanAlgebra α
inst_1 : DecidableEq α
s t : Finset α
rw : s ⊼ tᶜˢᶜˢ = s ⊼ t
rw₁ rw₂ : s ⊼ t = s ⊼ t
⊢ s \\ tᶜˢ = s ⊼ t

Tactic:
rw [← infs_compls_eq_diffs, compls_compls]

Premises used: Finset.compls_compls, Finset.infs_compls_eq_diffs
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_4
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
n : ℕ
h𝒜 : Set.Sized n (↑𝒜 : Set (Finset α))
s : Finset α
hs : s ∈ 𝒜
rw : Fintype.card α - #s = Fintype.card α - n
rw₁ rw₂ : Fintype.card α - n = Fintype.card α - n
⊢ #sᶜ = Fintype.card α - n

Tactic:
rw [Finset.card_compl, h𝒜 hs]

Premises used: Finset.card_compl
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_4
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
n : ℕ
hn : n ≤ Fintype.card α
h𝒜 : Set.Sized n (↑𝒜ᶜˢ : Set (Finset α))
⊢ Set.Sized (Fintype.card α - n) (↑𝒜 : Set (Finset α))

Tactic:
simpa using h𝒜.compls

Premises used: Set.Sized.compls