awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
s t u : Finset α
⊢ s ⊻ (t ⊻ u) = t ⊻ (s ⊻ u)

Tactic:
image₂_left_comm sup_left_comm

Premises used: sup_left_comm, Finset.image₂_left_comm
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
s t u : Finset α
⊢ s ⊻ t ⊻ u = s ⊻ u ⊻ t

Tactic:
image₂_right_comm sup_right_comm

Premises used: Finset.image₂_right_comm, sup_right_comm
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
s t u v : Finset α
⊢ s ⊻ t ⊻ (u ⊻ v) = s ⊻ u ⊻ (t ⊻ v)

Tactic:
image₂_image₂_image₂_comm sup_sup_sup_comm

Premises used: sup_sup_sup_comm, Finset.image₂_image₂_image₂_comm
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeInf α
s t : Finset α
c : α
⊢ c ∈ s ⊼ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ b = c

Tactic:
simp [(· ⊼ ·)]

Premises used: HasInfs.infs
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeInf α
s t : Finset α
⊢ (↑(s ⊼ t) : Set α) = (↑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 : SemilatticeInf α
s t : Finset α
⊢ #(s ⊼ t) ≤ #s * #t

Tactic:
card_image₂_le _ _ _

Premises used: Finset.card_image₂_le
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeInf α
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.card_image₂_iff
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeInf α
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 : SemilatticeInf α
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 : SemilatticeInf α
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 : SemilatticeInf α
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 : SemilatticeInf α
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 : SemilatticeInf α
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 : SemilatticeInf α
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 : SemilatticeInf α
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 : SemilatticeInf α
s t : Finset α
⊢ (s ⊼ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
image₂_nonempty_iff

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

Tactic:
Nonempty.image₂

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

Tactic:
Nonempty.of_image₂_left

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

Tactic:
Nonempty.of_image₂_right

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

Tactic:
image₂_empty_left

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

Tactic:
image₂_empty_right

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

Tactic:
image₂_eq_empty_iff

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

Tactic:
image₂_singleton_left

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

Tactic:
image₂_singleton_right

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

Tactic:
image₂_singleton

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

Tactic:
image₂_union_left

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

Tactic:
image₂_union_right

Premises used: Finset.image₂_union_right
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeInf α
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 : SemilatticeInf α
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 : SemilatticeInf α
u : Finset α
s t : Set α
⊢ (↑u : Set α) ⊆ 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:
F : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : SemilatticeInf α
inst_3 : SemilatticeInf β
inst_4 : FunLike F α β
inst_5 : InfHomClass F α β
f : F
s t : Finset α
⊢ Eq.{u_3 + 1} (α := Finset β) (image (⇑f : (a : α) → β) (s ⊼ t))
    (image (⇑f : (a : α) → β) s ⊼ image (⇑f : (a : α) → β) t)

Tactic:
image_image₂_distrib <| map_inf f

Premises used: InfHomClass.map_inf, Finset.image_image₂_distrib
-- Module: Mathlib.Data.Finset.Sups
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : SemilatticeInf α
inst_3 : SemilatticeInf β
inst_4 : FunLike F α β
inst_5 : InfHomClass F α β
f : F
hf : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
s t : Finset α
⊢ map { toFun := (⇑f : (a : α) → β), inj' := hf : α ↪ β } (s ⊼ t) =
    map { toFun := (⇑f : (a : α) → β), inj' := hf : α ↪ β } s ⊼
      map { toFun := (⇑f : (a : α) → β), inj' := hf : α ↪ β } t

Tactic:
simpa [map_eq_image] using image_infs f s t

Premises used: Finset.image_infs, Finset.map_eq_image
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeInf α
s : Finset α
⊢ s ⊆ s ⊼ s

Tactic:
fun _a ha ↦ mem_infs.2 ⟨_, ha, _, ha, inf_idem _⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Finset.mem_infs, inf_idem
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeInf α
s : Finset α
⊢ s ⊼ s ⊆ s ↔ InfClosed (↑s : Set α)

Tactic:
infs_subset_iff

Premises used: InfClosed, Finset.infs_subset_iff
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeInf α
s : Finset α
⊢ s ⊼ s = s ↔ InfClosed (↑s : Set α)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeInf α
inst_2 : Fintype α
⊢ Eq.{u_2 + 1} (α := Finset α) (univ ⊼ univ) univ

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeInf α
inst_2 : DecidableLE α
s t : Finset α
a : α
⊢ {b ∈ s ⊼ t | a ≤ b} = {b ∈ s | a ≤ b} ⊼ {b ∈ t | a ≤ b}

Tactic:
simp only [← coe_inj, coe_filter, coe_infs, ← mem_coe, Set.sep_infs_le]

Premises used: Finset.coe_infs, Finset.coe_filter, Finset.coe_inj, Set.sep_infs_le, Finset.mem_coe
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeInf α
s t : Finset α
⊢ (s.biUnion fun (a : α) ↦ image (fun (x : α) ↦ a ⊓ x) t) = s ⊼ t

Tactic:
biUnion_image_left

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

Tactic:
biUnion_image_right

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

Tactic:
image_uncurry_product _ _ _

Premises used: Finset.image_uncurry_product
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeInf α
s t u : Finset α
⊢ s ⊼ t ⊼ u = s ⊼ (t ⊼ u)

Tactic:
image₂_assoc inf_assoc

Premises used: Finset.image₂_assoc, inf_assoc
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeInf α
s t : Finset α
⊢ s ⊼ t = t ⊼ s

Tactic:
image₂_comm inf_comm

Premises used: inf_comm, Finset.image₂_comm
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeInf α
s t u : Finset α
⊢ s ⊼ (t ⊼ u) = t ⊼ (s ⊼ u)

Tactic:
image₂_left_comm inf_left_comm

Premises used: Finset.image₂_left_comm, inf_left_comm
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeInf α
s t u : Finset α
⊢ s ⊼ t ⊼ u = s ⊼ u ⊼ t

Tactic:
image₂_right_comm inf_right_comm

Premises used: inf_right_comm, Finset.image₂_right_comm
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeInf α
s t u v : Finset α
⊢ s ⊼ t ⊼ (u ⊼ v) = s ⊼ u ⊼ (t ⊼ v)

Tactic:
image₂_image₂_image₂_comm inf_inf_inf_comm

Premises used: inf_inf_inf_comm, Finset.image₂_image₂_image₂_comm
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
s t u : Finset α
⊢ s ⊻ t ⊼ u ⊆ (s ⊻ t) ⊼ (s ⊻ u)

Tactic:
image₂_distrib_subset_left sup_inf_left

Premises used: Set.Mem, setOf, sup_inf_left, Finset.image₂_distrib_subset_left
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
s t u : Finset α
⊢ t ⊼ u ⊻ s ⊆ (t ⊻ s) ⊼ (u ⊻ s)

Tactic:
image₂_distrib_subset_right sup_inf_right

Premises used: Set.Mem, setOf, sup_inf_right, Finset.image₂_distrib_subset_right
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
s t u : Finset α
⊢ s ⊼ (t ⊻ u) ⊆ s ⊼ t ⊻ s ⊼ u

Tactic:
image₂_distrib_subset_left inf_sup_left

Premises used: Set.Mem, setOf, Finset.image₂_distrib_subset_left, inf_sup_left
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DistribLattice α
s t u : Finset α
⊢ (t ⊻ u) ⊼ s ⊆ t ⊼ s ⊻ u ⊼ s

Tactic:
image₂_distrib_subset_right inf_sup_right

Premises used: Set.Mem, setOf, inf_sup_right, Finset.image₂_distrib_subset_right
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
s t : Finset α
h : ∀ (u : Finset α), u ∈ (s ∪ t).powerset ↔ u ∈ s.powerset ⊻ t.powerset
⊢ (s ∪ t).powerset = s.powerset ⊻ t.powerset

Tactic:
ext u
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
s t u : Finset α
h : u ⊆ s ∪ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u
⊢ u ∈ (s ∪ t).powerset ↔ u ∈ s.powerset ⊻ t.powerset

Tactic:
simp only [mem_sups, mem_powerset, sup_eq_union]

Premises used: Finset.mem_powerset, Finset.sup_eq_union, Finset.mem_sups
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
s t u : Finset α
⊢ u ⊆ s ∪ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u

Tactic:
⟨fun h ↦ ⟨_, inter_subset_left (s₂ := u), _, inter_subset_left (s₂ := u), ?_⟩, ?_⟩

Premises used: Inter.inter, And.intro, Iff.intro, Exists.intro, Finset.inter_subset_left
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
s t u : Finset α
h : ∀ (h : u ⊆ s ∪ t), s ∩ u ∪ t ∩ u = u
h₁ : (∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u) → u ⊆ s ∪ t
⊢ u ⊆ s ∪ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u

Tactic:
refine ⟨fun h ↦ ⟨_, inter_subset_left (s₂ := u), _, inter_subset_left (s₂ := u), ?_⟩, ?_⟩
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
s t u : Finset α
h : u ⊆ s ∪ t
h₁ : (s ∪ t) ∩ u = u
h₂ h₃ h₄ h₅ : u ⊆ s ∪ t
⊢ s ∩ u ∪ t ∩ u = u

Tactic:
rwa [← union_inter_distrib_right, inter_eq_right]

Premises used: Finset.inter_eq_right, Finset.union_inter_distrib_right
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
s t v : Finset α
hv : v ⊆ s
w : Finset α
hw : w ⊆ t
⊢ v ∪ w ⊆ s ∪ t

Tactic:
union_subset_union hv hw

Premises used: Finset.union_subset_union
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
s t v : Finset α
hv : v ⊆ s
w : Finset α
hw : w ⊆ t
⊢ v ∪ w ⊆ s ∪ t

Tactic:
exact union_subset_union hv hw

Premises used: Finset.union_subset_union
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
s t : Finset α
h : ∀ (u : Finset α), u ∈ (s ∩ t).powerset ↔ u ∈ s.powerset ⊼ t.powerset
⊢ (s ∩ t).powerset = s.powerset ⊼ t.powerset

Tactic:
ext u
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
s t u : Finset α
h : u ⊆ s ∩ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u
⊢ u ∈ (s ∩ t).powerset ↔ u ∈ s.powerset ⊼ t.powerset

Tactic:
simp only [mem_infs, mem_powerset, inf_eq_inter]

Premises used: Finset.inf_eq_inter, Finset.mem_powerset, Finset.mem_infs
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
s t u : Finset α
⊢ u ⊆ s ∩ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u

Tactic:
⟨fun h ↦ ⟨_, inter_subset_left (s₂ := u), _, inter_subset_left (s₂ := u), ?_⟩, ?_⟩

Premises used: Inter.inter, And.intro, Iff.intro, Exists.intro, Finset.inter_subset_left
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
s t u : Finset α
h : ∀ (h : u ⊆ s ∩ t), s ∩ u ∩ (t ∩ u) = u
h₁ : (∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u) → u ⊆ s ∩ t
⊢ u ⊆ s ∩ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u

Tactic:
refine ⟨fun h ↦ ⟨_, inter_subset_left (s₂ := u), _, inter_subset_left (s₂ := u), ?_⟩, ?_⟩
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
s t v : Finset α
hv : v ⊆ s
w : Finset α
hw : w ⊆ t
⊢ v ∩ w ⊆ s ∩ t

Tactic:
inter_subset_inter hv hw

Premises used: Finset.inter_subset_inter
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
s t v : Finset α
hv : v ⊆ s
w : Finset α
hw : w ⊆ t
⊢ v ∩ w ⊆ s ∩ t

Tactic:
exact inter_subset_inter hv hw

Premises used: Finset.inter_subset_inter
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
s : Finset α
⊢ s.powerset ⊻ s.powerset = s.powerset

Tactic:
simp [← powerset_union]

Premises used: Finset.powerset_union
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
s : Finset α
⊢ s.powerset ⊼ s.powerset = s.powerset

Tactic:
simp [← powerset_inter]

Premises used: Finset.powerset_inter
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s t : Finset α
⊢ s ∈ 𝒜 → t ∈ ℬ → s ∪ t ∈ 𝒜 ⊻ ℬ

Tactic:
sup_mem_sups

Premises used: Set.Mem, setOf, Finset.sup_mem_sups
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s t : Finset α
⊢ s ∈ 𝒜 → t ∈ ℬ → s ∩ t ∈ 𝒜 ⊼ ℬ

Tactic:
inf_mem_infs

Premises used: Set.Mem, setOf, Finset.inf_mem_infs
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t : Finset α
c : α
⊢ c ∈ s ○ t ↔ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c

Tactic:
simp [disjSups, and_assoc]

Premises used: Finset.disjSups, and_assoc
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t : Finset α
simp_rw : ∀ ⦃x : α⦄, (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = x
⊢ s ○ t ⊆ s ⊻ t

Tactic:
simp_rw [subset_iff, mem_sups, mem_disjSups]

Premises used: Finset.mem_disjSups, Finset.subset_iff, Finset.mem_sups
-- 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) → ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = x

Tactic:
fun c ⟨a, b, ha, hb, _, hc⟩ => ⟨a, b, ha, hb, hc⟩

Premises used: _private.0.Finset.disjSups_subset_sups.match_1, Membership.mem, Exists, And, Max.max, And.intro, Exists.intro, Eq
-- 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) → ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = x

Tactic:
exact fun c ⟨a, b, ha, hb, _, hc⟩ => ⟨a, b, ha, hb, hc⟩
-- 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) ≤ #s * #t

Tactic:
(card_le_card disjSups_subset_sups).trans <| card_sups_le _ _

Premises used: Finset.card_le_card, Finset.card_sups_le, LE.le.trans, Finset.disjSups_subset_sups
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s₁ s₂ t₁ t₂ : Finset α
hs : s₁ ⊆ s₂
ht : t₁ ⊆ t₂
⊢ s₁ ○ t₁ ⊆ s₂ ○ t₂

Tactic:
image_subset_image <| filter_subset_filter _ <| product_subset_product hs ht

Premises used: Finset.filter_subset_filter, Set.Mem, Finset.product_subset_product, setOf, Finset.image_subset_image
-- 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 α
ht : t₁ ⊆ t₂
⊢ s ○ t₁ ⊆ s ○ t₂

Tactic:
disjSups_subset Subset.rfl ht

Premises used: Finset.Subset.rfl, Finset.disjSups_subset
-- 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 α
hs : s₁ ⊆ s₂
⊢ s₁ ○ t ⊆ s₂ ○ t

Tactic:
disjSups_subset hs Subset.rfl

Premises used: Finset.Subset.rfl, Finset.disjSups_subset
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t : Finset α
p : α → Prop
simp_rw : (∀ (c : α), (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c) → p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)
⊢ (∀ c ∈ s ○ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)

Tactic:
simp_rw [mem_disjSups]

Premises used: Finset.mem_disjSups
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t : Finset α
p : α → Prop
⊢ (∀ (c : α), (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c) → p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)

Tactic:
⟨fun h a ha b hb hab => h _ ⟨_, ha, _, hb, hab, rfl⟩, ?_⟩

Premises used: Max.max, And.intro, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t : Finset α
p : α → Prop
refine : (∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)) → ∀ (c : α), (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c) → p c
⊢ (∀ (c : α), (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c) → p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)

Tactic:
refine ⟨fun h a ha b hb hab => h _ ⟨_, ha, _, hb, hab, rfl⟩, ?_⟩
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t : Finset α
p : α → Prop
h : ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
⊢ p (a ⊔ b)

Tactic:
h _ ha _ hb hab
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t : Finset α
p : α → Prop
h : ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
⊢ p (a ⊔ b)

Tactic:
exact h _ ha _ hb hab
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t u : Finset α
⊢ s ○ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → a ⊔ b ∈ u

Tactic:
forall_disjSups_iff

Premises used: Finset.forall_disjSups_iff
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t : Finset α
simp_rw : (∃ (x : α), ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ (x : α), x ∈ s
⊢ (s ○ t).Nonempty → s.Nonempty

Tactic:
simp_rw [Finset.Nonempty, mem_disjSups]

Premises used: Finset.mem_disjSups, Finset.Nonempty
-- 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 ∈ s

Tactic:
fun ⟨_, a, ha, _⟩ => ⟨a, ha⟩

Premises used: _private.0.Finset.Nonempty.of_disjSups_left.match_1, Membership.mem, Exists, Exists.intro
-- 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 ∈ s

Tactic:
exact fun ⟨_, a, ha, _⟩ => ⟨a, ha⟩
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : DecidableRel (α := α) Disjoint
s t : Finset α
simp_rw : (∃ (x : α), ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ (x : α), x ∈ t
⊢ (s ○ t).Nonempty → t.Nonempty

Tactic:
simp_rw [Finset.Nonempty, mem_disjSups]

Premises used: Finset.mem_disjSups, Finset.Nonempty
-- 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:
fun ⟨_, _, _, b, hb, _⟩ => ⟨b, hb⟩

Premises used: Membership.mem, Exists, _private.0.Finset.Nonempty.of_disjSups_right.match_1, Exists.intro