awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
t : Finset β
u : Finset (α ⊕ β)
⊢ u ⊆ map Embedding.inr t ↔ u.toLeft = ∅ ∧ u.toRight ⊆ t

Tactic:
simp [← empty_disjSum, subset_disjSum]

Premises used: Finset.subset_disjSum, Finset.empty_disjSum
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
u : Finset (α ⊕ β)
⊢ map Embedding.inl s ⊆ u ↔ s ⊆ u.toLeft

Tactic:
simp [← disjSum_empty, disjSum_subset]

Premises used: Finset.disjSum_subset, Finset.disjSum_empty
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
t : Finset β
u : Finset (α ⊕ β)
⊢ map Embedding.inr t ⊆ u ↔ t ⊆ u.toRight

Tactic:
simp [← empty_disjSum, disjSum_subset]

Premises used: Finset.disjSum_subset, Finset.empty_disjSum
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
⊢ GaloisConnection (β := Finset (α ⊕ β)) (fun (x : Finset α) ↦ map Embedding.inl x) toLeft

Tactic:
fun _ _ ↦ map_inl_subset_iff_subset_toLeft

Premises used: Set.Mem, setOf, Finset.map_inl_subset_iff_subset_toLeft, GaloisConnection
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
⊢ GaloisConnection (β := Finset (α ⊕ β)) (fun (x : Finset β) ↦ map Embedding.inr x) toRight

Tactic:
fun _ _ ↦ map_inr_subset_iff_subset_toRight

Premises used: Set.Mem, setOf, Finset.map_inr_subset_iff_subset_toRight, GaloisConnection
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
h : ∀ (x : β), x ∈ (map (Equiv.sumComm α β).toEmbedding u).toLeft ↔ x ∈ u.toRight
⊢ (map (Equiv.sumComm α β).toEmbedding u).toLeft = u.toRight

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : β
⊢ x ∈ (map (Equiv.sumComm α β).toEmbedding u).toLeft ↔ x ∈ u.toRight

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
h : ∀ (x : α), x ∈ (map (Equiv.sumComm α β).toEmbedding u).toRight ↔ x ∈ u.toLeft
⊢ (map (Equiv.sumComm α β).toEmbedding u).toRight = u.toLeft

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : α
⊢ x ∈ (map (Equiv.sumComm α β).toEmbedding u).toRight ↔ x ∈ u.toLeft

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a_1 : α
b_1 : β
x : α ⊕ β
u v : Finset (α ⊕ β)
a : α
b : β
ha : inl a ∉ u
⊢ a ∉ u.toLeft

Tactic:
simpa
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
h : ∀ (y : α), y ∈ (cons (inl a) u ha).toLeft ↔ y ∈ cons a u.toLeft ⋯
⊢ (cons (inl a) u ha).toLeft = cons a u.toLeft ⋯

Tactic:
ext y
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
y : α
⊢ y ∈ (cons (inl a) u ha).toLeft ↔ y ∈ cons a u.toLeft ⋯

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
h : ∀ (y : α), y ∈ (cons (inr b) u hb).toLeft ↔ y ∈ u.toLeft
⊢ (cons (inr b) u hb).toLeft = u.toLeft

Tactic:
ext y
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
y : α
⊢ y ∈ (cons (inr b) u hb).toLeft ↔ y ∈ u.toLeft

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
h : ∀ (y : β), y ∈ (cons (inl a) u ha).toRight ↔ y ∈ u.toRight
⊢ (cons (inl a) u ha).toRight = u.toRight

Tactic:
ext y
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
y : β
⊢ y ∈ (cons (inl a) u ha).toRight ↔ y ∈ u.toRight

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a_1 : α
b_1 : β
x : α ⊕ β
u v : Finset (α ⊕ β)
a : α
b : β
hb : inr b ∉ u
⊢ b ∉ u.toRight

Tactic:
simpa
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
h : ∀ (y : β), y ∈ (cons (inr b) u hb).toRight ↔ y ∈ cons b u.toRight ⋯
⊢ (cons (inr b) u hb).toRight = cons b u.toRight ⋯

Tactic:
ext y
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
y : β
⊢ y ∈ (cons (inr b) u hb).toRight ↔ y ∈ cons b u.toRight ⋯

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
h : ∀ (x : β), x ∈ (image Sum.swap u).toLeft ↔ x ∈ u.toRight
⊢ (image Sum.swap u).toLeft = u.toRight

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
x : β
⊢ x ∈ (image Sum.swap u).toLeft ↔ x ∈ u.toRight

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
h : ∀ (x : α), x ∈ (image Sum.swap u).toRight ↔ x ∈ u.toLeft
⊢ (image Sum.swap u).toRight = u.toLeft

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
x : α
⊢ x ∈ (image Sum.swap u).toRight ↔ x ∈ u.toLeft

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst : DecidableEq α
inst_1 : DecidableEq β
h : ∀ (y : α), y ∈ (insert (inl a) u).toLeft ↔ y ∈ insert a u.toLeft
⊢ (insert (inl a) u).toLeft = insert a u.toLeft

Tactic:
ext y
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst : DecidableEq α
inst_1 : DecidableEq β
y : α
⊢ y ∈ (insert (inl a) u).toLeft ↔ y ∈ insert a u.toLeft

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst : DecidableEq α
inst_1 : DecidableEq β
h : ∀ (y : α), y ∈ (insert (inr b) u).toLeft ↔ y ∈ u.toLeft
⊢ (insert (inr b) u).toLeft = u.toLeft

Tactic:
ext y
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst : DecidableEq α
inst_1 : DecidableEq β
y : α
⊢ y ∈ (insert (inr b) u).toLeft ↔ y ∈ u.toLeft

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst : DecidableEq α
inst_1 : DecidableEq β
h : ∀ (y : β), y ∈ (insert (inl a) u).toRight ↔ y ∈ u.toRight
⊢ (insert (inl a) u).toRight = u.toRight

Tactic:
ext y
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst : DecidableEq α
inst_1 : DecidableEq β
y : β
⊢ y ∈ (insert (inl a) u).toRight ↔ y ∈ u.toRight

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst : DecidableEq α
inst_1 : DecidableEq β
h : ∀ (y : β), y ∈ (insert (inr b) u).toRight ↔ y ∈ insert b u.toRight
⊢ (insert (inr b) u).toRight = insert b u.toRight

Tactic:
ext y
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst : DecidableEq α
inst_1 : DecidableEq β
y : β
⊢ y ∈ (insert (inr b) u).toRight ↔ y ∈ insert b u.toRight

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
h : ∀ (x : α), x ∈ (u ∩ v).toLeft ↔ x ∈ u.toLeft ∩ v.toLeft
⊢ (u ∩ v).toLeft = u.toLeft ∩ v.toLeft

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
x : α
⊢ x ∈ (u ∩ v).toLeft ↔ x ∈ u.toLeft ∩ v.toLeft

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
h : ∀ (x : β), x ∈ (u ∩ v).toRight ↔ x ∈ u.toRight ∩ v.toRight
⊢ (u ∩ v).toRight = u.toRight ∩ v.toRight

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
x : β
⊢ x ∈ (u ∩ v).toRight ↔ x ∈ u.toRight ∩ v.toRight

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
h : ∀ (x : α), x ∈ (u ∪ v).toLeft ↔ x ∈ u.toLeft ∪ v.toLeft
⊢ (u ∪ v).toLeft = u.toLeft ∪ v.toLeft

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
x : α
⊢ x ∈ (u ∪ v).toLeft ↔ x ∈ u.toLeft ∪ v.toLeft

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
h : ∀ (x : β), x ∈ (u ∪ v).toRight ↔ x ∈ u.toRight ∪ v.toRight
⊢ (u ∪ v).toRight = u.toRight ∪ v.toRight

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
x : β
⊢ x ∈ (u ∪ v).toRight ↔ x ∈ u.toRight ∪ v.toRight

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
h : ∀ (x : α), x ∈ (u \ v).toLeft ↔ x ∈ u.toLeft \ v.toLeft
⊢ (u \ v).toLeft = u.toLeft \ v.toLeft

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
x : α
⊢ x ∈ (u \ v).toLeft ↔ x ∈ u.toLeft \ v.toLeft

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
h : ∀ (x : β), x ∈ (u \ v).toRight ↔ x ∈ u.toRight \ v.toRight
⊢ (u \ v).toRight = u.toRight \ v.toRight

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
x : β
⊢ x ∈ (u \ v).toRight ↔ x ∈ u.toRight \ v.toRight

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
s_1 : Finset α_1
t : Finset β_1
s₁ s₂ : Finset α_1
t₁ t₂ : Finset β_1
a_1 : α_1
b_1 : β_1
x : α_1 ⊕ β_1
u v : Finset (α_1 ⊕ β_1)
a : α_1
b : β_1
α : Type u_4
β : Type u_5
s : Prod.{u_4, u_5} (Finset α) (Finset β)
⊢ (fun (s : Finset (α ⊕ β)) ↦ (s.toLeft, s.toRight))
      ((fun (s : Prod.{u_4, u_5} (Finset α) (Finset β)) ↦ s.1.disjSum s.2) s) =
    s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
s : Finset α_1
t : Finset β_1
s₁ s₂ : Finset α_1
t₁ t₂ : Finset β_1
a_1 : α_1
b_1 : β_1
x : α_1 ⊕ β_1
u v : Finset (α_1 ⊕ β_1)
a : α_1
b : β_1
α : Type u_4
β : Type u_5
⊢ ∀ {a b : Finset (α ⊕ β)},
    LE.le (α := Prod.{u_4, u_5} (Finset α) (Finset β))
        (({ toFun := fun (s : Finset (α ⊕ β)) ↦ (s.toLeft, s.toRight),
                invFun := fun (s : Prod.{u_4, u_5} (Finset α) (Finset β)) ↦ s.1.disjSum s.2, left_inv := ⋯,
                right_inv := ⋯ } :
              (a : Finset (α ⊕ β)) → Finset α × Finset β)
            a :
          Prod.{u_4, u_5} (Finset α) (Finset β))
        (({ toFun := fun (s : Finset (α ⊕ β)) ↦ (s.toLeft, s.toRight),
                invFun := fun (s : Prod.{u_4, u_5} (Finset α) (Finset β)) ↦ s.1.disjSum s.2, left_inv := ⋯,
                right_inv := ⋯ } :
              (a : Finset (α ⊕ β)) → Finset α × Finset β)
            b :
          Prod.{u_4, u_5} (Finset α) (Finset β)) ↔
      a ≤ b

Tactic:
simp [← Finset.coe_subset, Set.subset_def]

Premises used: Set.subset_def, Finset.coe_subset
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_4
β : Type u_5
s : Prod.{u_4, u_5} (Finset α) (Finset β)
⊢ (OrderIso.symm sumEquiv : (a : Finset α × Finset β) → Finset (α ⊕ β)) s = s.1.disjSum s.2

Tactic:
rfl

Premises used: Finset.disjSum, rfl
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a_1 : α
b_1 : β
x : α ⊕ β
u v : Finset (α ⊕ β)
a : α
b : β
f : α ⊕ β ↪ γ
⊢ Disjoint (map (Embedding.trans Embedding.inl f) s) (map (Embedding.trans Embedding.inr f) t)

Tactic:
simpa only [← map_map]
            using (Finset.disjoint_map f).2 (disjoint_map_inl_map_inr _ _)

Premises used: Iff.mpr, Finset.disjoint_map, Finset.disjoint_map_inl_map_inr, Finset.map_map
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a_1 : α
b_1 : β
x : α ⊕ β
u v : Finset (α ⊕ β)
a : α
b : β
f : α ⊕ β ↪ γ
⊢ Disjoint (map (Embedding.trans Embedding.inl f) s) (map (Embedding.trans Embedding.inr f) t)

Tactic:
as_aux_lemma =>
          simpa only [← map_map]
            using (Finset.disjoint_map f).2 (disjoint_map_inl_map_inr _ _)

Premises used: Iff.mpr, Finset.disjoint_map, Finset.disjoint_map_inl_map_inr, Finset.map_map
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
f : α ⊕ β ↪ γ
⊢ map f (s.disjSum t) = (map (Embedding.trans Embedding.inl f) s).disjUnion (map (Embedding.trans Embedding.inr f) t) ⋯

Tactic:
val_injective <| Multiset.map_disjSum _

Premises used: Finset.val_injective, Multiset.map_disjSum
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
f : α ⊕ β → γ
b₁ b₂ : γ
op : γ → γ → γ
inst : Std.Commutative op
inst_1 : Std.Associative op
simp_rw :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s.disjSum t).val) =
    op (Multiset.fold op b₁ (Multiset.map (fun (x : α) ↦ f (inl x)) s.val))
      (Multiset.fold op b₂ (Multiset.map (fun (x : β) ↦ f (inr x)) t.val))
simp_rw₁ :
  Multiset.fold op (op b₁ b₂) (Multiset.map f (s.val.disjSum t.val)) =
    op (Multiset.fold op b₁ (Multiset.map (fun (x : α) ↦ f (inl x)) s.val))
      (Multiset.fold op b₂ (Multiset.map (fun (x : β) ↦ f (inr x)) t.val))
simp_rw₂ :
  Multiset.fold op (op b₁ b₂)
      (HAdd.hAdd (α := Multiset γ) (Multiset.map (fun (x : α) ↦ f (inl x)) s.val)
        (Multiset.map (fun (x : β) ↦ f (inr x)) t.val)) =
    op (Multiset.fold op b₁ (Multiset.map (fun (x : α) ↦ f (inl x)) s.val))
      (Multiset.fold op b₂ (Multiset.map (fun (x : β) ↦ f (inr x)) t.val))
⊢ fold op (op b₁ b₂) f (s.disjSum t) =
    op (fold op b₁ (fun (x : α) ↦ f (inl x)) s) (fold op b₂ (fun (x : β) ↦ f (inr x)) t)

Tactic:
simp_rw [fold, disjSum, Multiset.map_disjSum, fold_add]

Premises used: Multiset.fold_add, Finset.fold, Finset.disjSum, Multiset.map_disjSum
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
s t : Finset α
c : α
⊢ c ∈ s ⊻ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = c

Tactic:
simp [(· ⊻ ·)]

Premises used: HasSups.sups
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
inst_3 : SemilatticeSup β
inst_4 : FunLike F α β
inst_5 : SupHomClass 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_sup f

Premises used: SupHomClass.map_sup, 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 : SemilatticeSup α
inst_3 : SemilatticeSup β
inst_4 : FunLike F α β
inst_5 : SupHomClass 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_sups f s t

Premises used: Finset.map_eq_image, Finset.image_sups
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
s : Finset α
⊢ s ⊆ s ⊻ s

Tactic:
fun _a ha ↦ mem_sups.2 ⟨_, ha, _, ha, sup_idem _⟩

Premises used: Iff.mpr, sup_idem, And.intro, Exists.intro, Finset.mem_sups
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
s : Finset α
⊢ s ⊻ s ⊆ s ↔ SupClosed (↑s : Set α)

Tactic:
sups_subset_iff

Premises used: SupClosed, Finset.sups_subset_iff
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
s : Finset α
⊢ s ⊻ s = s ↔ SupClosed (↑s : Set α)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
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 : SemilatticeSup α
inst_2 : DecidableLE α
s t : Finset α
a : α
⊢ {b ∈ s ⊻ t | b ≤ a} = {b ∈ s | b ≤ a} ⊻ {b ∈ t | b ≤ a}

Tactic:
simp only [← coe_inj, coe_filter, coe_sups, ← mem_coe, Set.sep_sups_le]

Premises used: Finset.coe_filter, Finset.coe_inj, Set.sep_sups_le, Finset.coe_sups, Finset.mem_coe
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
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 : SemilatticeSup α
s t u : Finset α
⊢ s ⊻ t ⊻ u = s ⊻ (t ⊻ u)

Tactic:
image₂_assoc sup_assoc

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

Tactic:
image₂_comm sup_comm

Premises used: Finset.image₂_comm, sup_comm