awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u v : Finset α
⊢ s ∪ t ∪ (u ∪ v) = s ∪ u ∪ (t ∪ v)

Tactic:
sup_sup_sup_comm _ _ _ _

Premises used: sup_sup_sup_comm
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u v : Finset α
⊢ s ∩ t ∩ (u ∩ v) = s ∩ u ∩ (t ∩ v)

Tactic:
inf_inf_inf_comm _ _ _ _

Premises used: inf_inf_inf_comm
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u

Tactic:
(sup_le_iff : s ⊔ t ≤ u ↔ s ≤ u ∧ t ≤ u)

Premises used: Set.Mem, setOf, sup_le_iff
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ s ⊆ t ∩ u ↔ s ⊆ t ∧ s ⊆ u

Tactic:
(le_inf_iff : s ≤ t ⊓ u ↔ s ≤ t ∧ s ≤ u)

Premises used: Set.Mem, setOf, le_inf_iff
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ∩ t = s ↔ s ⊆ t

Tactic:
inf_eq_left

Premises used: inf_eq_left
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ t ∩ s = s ↔ s ⊆ t

Tactic:
inf_eq_right

Premises used: inf_eq_right
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
ht : s ∩ u ⊆ t
hu : s ∩ t ⊆ u
⊢ s ∩ t = s ∩ u

Tactic:
inf_congr_left ht hu

Premises used: inf_congr_left
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
hs : t ∩ u ⊆ s
ht : s ∩ u ⊆ t
⊢ s ∩ u = t ∩ u

Tactic:
inf_congr_right hs ht

Premises used: inf_congr_right
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ s ∩ t = s ∩ u ↔ s ∩ u ⊆ t ∧ s ∩ t ⊆ u

Tactic:
inf_eq_inf_iff_left

Premises used: Set.Mem, setOf, inf_eq_inf_iff_left
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ s ∩ u = t ∩ u ↔ t ∩ u ⊆ s ∧ s ∩ u ⊆ t

Tactic:
inf_eq_inf_iff_right

Premises used: Set.Mem, setOf, inf_eq_inf_iff_right
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s s' : Finset α
P : Prop
inst_1 : Decidable P
⊢ (if P then s else s') ⊆ s ∪ s'

Tactic:
ite_le_sup s s' P

Premises used: Set.Mem, ite_le_sup, setOf
-- Module: Mathlib.Data.Finset.Lattice.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s s' : Finset α
P : Prop
inst_1 : Decidable P
⊢ s ∩ s' ⊆ if P then s else s'

Tactic:
inf_le_ite s s' P

Premises used: Set.Mem, setOf, inf_le_ite
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f : β → α
⊢ s.sup f = (Multiset.map f s.val).sup

Tactic:
rfl

Premises used: Finset.sup, Multiset.sup, rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
f : β → α
⊢ sup ∅ f = ⊥

Tactic:
fold_empty

Premises used: Finset.fold_empty, Finset.sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f : β → α
b : β
h : b ∉ s
⊢ (cons b s h).sup f = f b ⊔ s.sup f

Tactic:
fold_cons h

Premises used: Finset.fold_cons, Finset.sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f : β → α
inst_2 : DecidableEq β
b : β
⊢ (insert b s).sup f = f b ⊔ s.sup f

Tactic:
fold_insert_idem

Premises used: Finset.fold_insert_idem, Finset.sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq β
s : Finset γ
f : γ → β
g : β → α
⊢ (image f s).sup g = s.sup (g ∘ f)

Tactic:
fold_image_idem

Premises used: Finset.fold_image_idem, Finset.sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset γ
f : γ ↪ β
g : β → α
⊢ (map f s).sup g = s.sup (g ∘ (⇑f : (a : γ) → β))

Tactic:
fold_map

Premises used: Finset.fold_map, Finset.sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
f : β → α
b : β
⊢ sup {b} f = f b

Tactic:
Multiset.sup_singleton

Premises used: Multiset.map, List.map, Multiset.sup_singleton, Finset.fold, Multiset.cons, Multiset.ofList, Finset.sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f g : β → α
empty : ⊥ = sup ∅ f ⊔ sup ∅ g
empty₁ : ⊥ = ⊥ ⊔ sup ∅ g
empty₂ : Eq.{u_2 + 1} (α := α) ⊥ (⊥ ⊔ ⊥)
empty₃ empty₄ : Eq.{u_2 + 1} (α := α) ⊥ ⊥
⊢ sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ g

Tactic:
rw [sup_empty, sup_empty, sup_empty, bot_sup_eq]

Premises used: bot_sup_eq, Finset.sup_empty
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f g : β → α
a : β
s_1 : Finset β
h : a ∉ s_1
ih : s_1.sup (f ⊔ g) = s_1.sup f ⊔ s_1.sup g
cons : (f ⊔ g) a ⊔ (s_1.sup f ⊔ s_1.sup g) = f a ⊔ s_1.sup f ⊔ (g a ⊔ s_1.sup g)
⊢ (Finset.cons a s_1 h).sup (f ⊔ g) = (Finset.cons a s_1 h).sup f ⊔ (Finset.cons a s_1 h).sup g

Tactic:
rw [sup_cons, sup_cons, sup_cons, ih]

Premises used: Finset.sup_cons
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f g : β → α
a : β
s_1 : Finset β
h : a ∉ s_1
ih : s_1.sup (f ⊔ g) = s_1.sup f ⊔ s_1.sup g
⊢ (f ⊔ g) a ⊔ (s_1.sup f ⊔ s_1.sup g) = f a ⊔ s_1.sup f ⊔ (g a ⊔ s_1.sup g)

Tactic:
sup_sup_sup_comm _ _ _ _

Premises used: sup_sup_sup_comm
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f g : β → α
a : β
s_1 : Finset β
h : a ∉ s_1
ih : s_1.sup (f ⊔ g) = s_1.sup f ⊔ s_1.sup g
⊢ (f ⊔ g) a ⊔ (s_1.sup f ⊔ s_1.sup g) = f a ⊔ s_1.sup f ⊔ (g a ⊔ s_1.sup g)

Tactic:
exact sup_sup_sup_comm _ _ _ _

Premises used: sup_sup_sup_comm
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f g : β → α
empty : sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ g
cons :
  ∀ (a : β) (s : Finset β) (h : a ∉ s) (ih : s.sup (f ⊔ g) = s.sup f ⊔ s.sup g),
    (Finset.cons a s h).sup (f ⊔ g) = (Finset.cons a s h).sup f ⊔ (Finset.cons a s h).sup g
⊢ s.sup (f ⊔ g) = s.sup f ⊔ s.sup g

Tactic:
induction s using Finset.cons_induction with
  | empty => rw [sup_empty, sup_empty, sup_empty, bot_sup_eq]
  | cons _ _ _ ih =>
    rw [sup_cons, sup_cons, sup_cons, ih]
    exact sup_sup_sup_comm _ _ _ _

Premises used: sup_sup_sup_comm, Finset.cons, bot_sup_eq, Finset.sup_empty, Finset.sup_cons
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s₁ s₂ : Finset β
f g : β → α
hs : s₁ = s₂
hfg : ∀ a ∈ s₂, f a = g a
subst : ∀ (hfg : ∀ a ∈ s₁, f a = g a), s₁.sup f = s₁.sup g
⊢ s₁.sup f = s₂.sup g

Tactic:
subst hs
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s₁ : Finset β
f g : β → α
hfg : ∀ a ∈ s₁, f a = g a
⊢ s₁.sup f = s₁.sup g

Tactic:
Finset.fold_congr hfg

Premises used: Finset.fold_congr, Finset.sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s₁ : Finset β
f g : β → α
hfg : ∀ a ∈ s₁, f a = g a
⊢ s₁.sup f = s₁.sup g

Tactic:
exact Finset.fold_congr hfg

Premises used: Finset.fold_congr
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
inst_4 : FunLike F α β
inst_5 : SupBotHomClass F α β
f : F
s_1 : Finset ι
g : ι → α
i : ι
s : Finset ι
h_1 : i ∉ s
h : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (s.sup g) : β) (s.sup ((⇑f : (a : α) → β) ∘ g) : β)
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i ⊔ s.sup g) : β) ((cons i s h_1).sup ((⇑f : (a : α) → β) ∘ g) : β)
rw₁ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i ⊔ s.sup g) : β)
    (((⇑f : (a : α) → β) ∘ g) i ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
rw₂ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i) ⊔ (f : (a : α) → β) (s.sup g) : β)
    (((⇑f : (a : α) → β) ∘ g) i ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
rw₃ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i) ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
    (((⇑f : (a : α) → β) ∘ g) i ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
rw₄ rw₅ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i) ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
    ((f : (a : α) → β) (g i) ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ((cons i s h_1).sup g) : β) ((cons i s h_1).sup ((⇑f : (a : α) → β) ∘ g) : β)

Tactic:
rw [sup_cons, sup_cons, map_sup, h, Function.comp_apply]

Premises used: Finset.sup_cons, SupHomClass.map_sup, Function.comp_apply
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f : β → α
a : α
apply : (∀ b ∈ Multiset.map f s.val, b ≤ a) ↔ ∀ b ∈ s, f b ≤ a
⊢ s.sup f ≤ a ↔ ∀ b ∈ s, f b ≤ a

Tactic:
apply Iff.trans Multiset.sup_le

Premises used: Iff.trans, Multiset.sup_le
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f : β → α
a : α
simp : (∀ (b : α), ∀ x ∈ s.val, f x = b → b ≤ a) ↔ ∀ b ∈ s, f b ≤ a
⊢ (∀ b ∈ Multiset.map f s.val, b ≤ a) ↔ ∀ b ∈ s, f b ≤ a

Tactic:
simp only [Multiset.mem_map, and_imp, exists_imp]

Premises used: and_imp, Multiset.mem_map, exists_imp
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f : β → α
a : α
⊢ (∀ (b : α), ∀ x ∈ s.val, f x = b → b ≤ a) ↔ ∀ b ∈ s, f b ≤ a

Tactic:
⟨fun k b hb => k _ _ hb rfl, fun k a' b hb h => h ▸ k _ hb⟩

Premises used: Eq.rec, Iff.intro, rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f : β → α
a : α
⊢ (∀ (b : α), ∀ x ∈ s.val, f x = b → b ≤ a) ↔ ∀ b ∈ s, f b ≤ a

Tactic:
exact ⟨fun k b hb => k _ _ hb rfl, fun k a' b hb h => h ▸ k _ hb⟩
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
a : α
⊢ (s.sup fun (x : β) ↦ a) ≤ a

Tactic:
Finset.sup_le fun _ _ => le_rfl

Premises used: le_rfl, Finset.sup_le
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f : β → α
b : β
hb : b ∈ s
⊢ f b ≤ s.sup f

Tactic:
Finset.sup_le_iff.1 le_rfl _ hb

Premises used: le_rfl, Iff.mp, Finset.sup_le_iff
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f : β → α
⊢ IsLUB (f '' (↑s : Set β)) (s.sup f)

Tactic:
simp +contextual [IsLUB, IsLeast, upperBounds, lowerBounds, le_sup]

Premises used: lowerBounds, upperBounds, IsLeast, IsLUB, Finset.le_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset α
⊢ IsLUB (↑s : Set α) (s.sup id)

Tactic:
simpa using isLUB_sup (f := id)

Premises used: Finset.isLUB_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f : β → α
a : α
b : β
hb : b ∈ s
h : a ≤ f b
⊢ a ≤ s.sup f

Tactic:
h.trans <| le_sup hb

Premises used: LE.le.trans, Finset.le_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
c : α
⊢ (s₁ ∪ s₂).sup f ≤ c ↔ s₁.sup f ⊔ s₂.sup f ≤ c

Tactic:
simp [or_imp, forall_and]

Premises used: or_imp, forall_and
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
h : s.Nonempty
c : α
⊢ (s.sup fun (x : β) ↦ c) = c

Tactic:
eq_of_forall_ge_iff (fun _ => Finset.sup_le_iff.trans h.forall_const)

Premises used: eq_of_forall_ge_iff, Iff.trans, Finset.sup_le_iff, Finset.Nonempty.forall_const
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
inl : Eq.{u_2 + 1} (α := α) (sup ∅ fun (x : β) ↦ ⊥) ⊥
inr : ∀ (hs : s.Nonempty), Eq.{u_2 + 1} (α := α) (s.sup fun (x : β) ↦ ⊥) ⊥
⊢ Eq.{u_2 + 1} (α := α) (s.sup fun (x : β) ↦ ⊥) ⊥

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
⊢ Eq.{u_2 + 1} (α := α) (sup ∅ fun (x : β) ↦ ⊥) ⊥

Tactic:
sup_empty

Premises used: Finset.sup_empty
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
⊢ Eq.{u_2 + 1} (α := α) (sup ∅ fun (x : β) ↦ ⊥) ⊥

Tactic:
exact sup_empty

Premises used: Finset.sup_empty
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
hs : s.Nonempty
⊢ Eq.{u_2 + 1} (α := α) (s.sup fun (x : β) ↦ ⊥) ⊥

Tactic:
sup_const hs _

Premises used: Finset.sup_const
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
hs : s.Nonempty
⊢ Eq.{u_2 + 1} (α := α) (s.sup fun (x : β) ↦ ⊥) ⊥

Tactic:
exact sup_const hs _

Premises used: Finset.sup_const
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f g : β → α
p : β → Prop
inst_2 : DecidablePred p
⊢ (s.sup fun (i : β) ↦ if p i then f i else g i) = (filter p s).sup f ⊔ {i ∈ s | ¬p i}.sup g

Tactic:
fold_ite _

Premises used: Finset.fold_ite, Finset.sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f g : β → α
h : ∀ b ∈ s, f b ≤ g b
⊢ s.sup f ≤ s.sup g

Tactic:
Finset.sup_le fun b hb => le_trans (h b hb) (le_sup hb)

Premises used: Finset.sup_le, Finset.le_sup, le_trans
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s₁ s₂ : Finset β
f : β → α
h : s₁ ⊆ s₂
⊢ s₁.sup f ≤ s₂.sup f

Tactic:
Finset.sup_le (fun _ hb => le_sup (h hb))

Premises used: Finset.sup_le, Finset.le_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
t : Finset γ
f : β → γ → α
a : α
⊢ (s.sup fun (b : β) ↦ t.sup (f b)) ≤ a ↔ (t.sup fun (c : γ) ↦ s.sup fun (b : β) ↦ f b c) ≤ a

Tactic:
simpa using forall₂_comm

Premises used: forall₂_comm
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f : β → α
⊢ (s.attach.sup fun (x : ↥s) ↦ f (↑x : β)) = s.sup f

Tactic:
(s.attach.sup_map (Function.Embedding.subtype _) f).symm.trans <| congr_arg _ attach_map_val

Premises used: congr_arg, Finset.sup_map, Finset.attach, Function.Embedding.subtype, Finset.attach_map_val, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
s : Finset α
⊢ (s.erase ⊥).sup id = s.sup id

Tactic:
(sup_mono (s.erase_subset _)).antisymm (Finset.sup_le_iff.2 fun a ha => ?_)

Premises used: Iff.mpr, LE.le.antisymm, Finset.sup_mono, Finset.sup_le_iff, Finset.erase_subset
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
s : Finset α
refine : ∀ (a : α) (ha : a ∈ s), id a ≤ (s.erase ⊥).sup id
⊢ (s.erase ⊥).sup id = s.sup id

Tactic:
refine (sup_mono (s.erase_subset _)).antisymm (Finset.sup_le_iff.2 fun a ha => ?_)

Premises used: Iff.mpr, LE.le.antisymm, Finset.sup_mono, Finset.sup_le_iff, Finset.erase_subset
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
inl : ∀ (ha : ⊥ ∈ s), id ⊥ ≤ (s.erase ⊥).sup id
inr : ∀ (ha' : a ≠ ⊥), id a ≤ (s.erase ⊥).sup id
⊢ id a ≤ (s.erase ⊥).sup id

Tactic:
obtain rfl | ha' := eq_or_ne a ⊥

Premises used: Bot.bot, eq_or_ne, rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
s : Finset α
ha : ⊥ ∈ s
⊢ id ⊥ ≤ (s.erase ⊥).sup id

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
s : Finset α
ha : ⊥ ∈ s
⊢ id ⊥ ≤ (s.erase ⊥).sup id

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
ha' : a ≠ ⊥
⊢ id a ≤ (s.erase ⊥).sup id

Tactic:
le_sup (mem_erase.2 ⟨ha', ha⟩)

Premises used: Iff.mpr, Finset.mem_erase, And.intro, Finset.le_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
ha' : a ≠ ⊥
⊢ id a ≤ (s.erase ⊥).sup id

Tactic:
exact le_sup (mem_erase.2 ⟨ha', ha⟩)

Premises used: Iff.mpr, Finset.mem_erase, And.intro, Finset.le_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
β : Type u_8
inst : GeneralizedBooleanAlgebra α
f : β → α
a : α
empty : ⊥ = sup ∅ f \ a
empty₁ : ⊥ = ⊥ \ a
empty₂ empty₃ : Eq.{u_7 + 1} (α := α) ⊥ ⊥
⊢ (sup ∅ fun (b : β) ↦ f b \ a) = sup ∅ f \ a

Tactic:
rw [sup_empty, sup_empty, bot_sdiff]

Premises used: bot_sdiff, Finset.sup_empty
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
β : Type u_8
inst : GeneralizedBooleanAlgebra α
f : β → α
a : α
a_1 : β
s : Finset β
h_1 : a_1 ∉ s
h : (s.sup fun (b : β) ↦ f b \ a) = s.sup f \ a
cons : (f a_1 \ a ⊔ s.sup fun (b : β) ↦ f b \ a) = (Finset.cons a_1 s h_1).sup f \ a
cons₁ : (f a_1 \ a ⊔ s.sup fun (b : β) ↦ f b \ a) = (f a_1 ⊔ s.sup f) \ a
cons₂ : f a_1 \ a ⊔ s.sup f \ a = (f a_1 ⊔ s.sup f) \ a
cons₃ cons₄ : f a_1 \ a ⊔ s.sup f \ a = f a_1 \ a ⊔ s.sup f \ a
⊢ ((Finset.cons a_1 s h_1).sup fun (b : β) ↦ f b \ a) = (Finset.cons a_1 s h_1).sup f \ a

Tactic:
rw [sup_cons, sup_cons, h, sup_sdiff]

Premises used: Finset.sup_cons, sup_sdiff
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
β : Type u_8
inst : GeneralizedBooleanAlgebra α
s : Finset β
f : β → α
a : α
empty : (sup ∅ fun (b : β) ↦ f b \ a) = sup ∅ f \ a
cons :
  ∀ (a_1 : β) (s : Finset β) (h : a_1 ∉ s) (h_1 : (s.sup fun (b : β) ↦ f b \ a) = s.sup f \ a),
    ((Finset.cons a_1 s h).sup fun (b : β) ↦ f b \ a) = (Finset.cons a_1 s h).sup f \ a
⊢ (s.sup fun (b : β) ↦ f b \ a) = s.sup f \ a

Tactic:
induction s using Finset.cons_induction with
  | empty => rw [sup_empty, sup_empty, bot_sdiff]
  | cons _ _ _ h => rw [sup_cons, sup_cons, h, sup_sdiff]

Premises used: bot_sdiff, Finset.cons, Finset.sup_empty, Finset.sup_cons, sup_sdiff
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : SemilatticeSup γ
inst_3 : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
rw : g (f c ⊔ t.sup f) = (cons c t hc).sup (g ∘ f)
rw₁ : g (f c ⊔ t.sup f) = (g ∘ f) c ⊔ t.sup (g ∘ f)
rw₂ : g (f c) ⊔ g (t.sup f) = (g ∘ f) c ⊔ t.sup (g ∘ f)
rw₃ : g (f c) ⊔ t.sup (g ∘ f) = (g ∘ f) c ⊔ t.sup (g ∘ f)
rw₄ rw₅ : g (f c) ⊔ t.sup (g ∘ f) = g (f c) ⊔ t.sup (g ∘ f)
⊢ g ((cons c t hc).sup f) = (cons c t hc).sup (g ∘ f)

Tactic:
rw [sup_cons, sup_cons, g_sup, ih, Function.comp_apply]

Premises used: Finset.sup_cons, Function.comp_apply
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x : α // P x }
this_1 : SemilatticeSup { x : α // P x } := Subtype.semilatticeSup (P := P) Psup
this : OrderBot { x : α // P x } := Subtype.orderBot (p := P) Pbot
g_sup : ∀ (x y : { x : α // P x }), (↑(x ⊔ y) : α) = (↑x : α) ⊔ (↑y : α)
bot : Eq.{u_2 + 1} (α := α) (↑⊥ : α) ⊥
⊢ (↑(t.sup f) : α) = t.sup fun (x : β) ↦ (↑(f x) : α)

Tactic:
apply comp_sup_eq_sup_comp Subtype.val

Premises used: Finset.comp_sup_eq_sup_comp, Subtype.val
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x : α // P x }
this_1 : SemilatticeSup { x : α // P x } := Subtype.semilatticeSup (P := P) Psup
this : OrderBot { x : α // P x } := Subtype.orderBot (p := P) Pbot
x y : { x : α // P x }
⊢ (↑(x ⊔ y) : α) = (↑x : α) ⊔ (↑y : α)

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x : α // P x }
this_1 : SemilatticeSup { x : α // P x } := Subtype.semilatticeSup (P := P) Psup
this : OrderBot { x : α // P x } := Subtype.orderBot (p := P) Pbot
⊢ Eq.{u_2 + 1} (α := α) (↑⊥ : α) ⊥

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
β : Type u_8
inst : DecidableEq β
s : Finset α
f : α → Multiset β
⊢ (s.sup f).toFinset = s.sup fun (x : α) ↦ (f x).toFinset

Tactic:
comp_sup_eq_sup_comp Multiset.toFinset toFinset_union rfl

Premises used: Multiset.toFinset, Finset.comp_sup_eq_sup_comp, Multiset.toFinset_union, rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
l : List α
rw : Multiset.fold (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊥ (↑l : Multiset α).dedup = (↑l : Multiset α).dedup.sup
⊢ List.foldr (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊥ l = l.toFinset.sup id

Tactic:
rw [← coe_fold_r, ← Multiset.fold_dedup_idem, sup_def, ← List.toFinset_coe, toFinset_val,
    Multiset.map_id]

Premises used: Multiset.map_id, List.toFinset_coe, Multiset.fold_dedup_idem, Multiset.coe_fold_r, Finset.sup_def, Multiset.toFinset_val
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
l : List α
⊢ Multiset.fold (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊥ (↑l : Multiset α).dedup = (↑l : Multiset α).dedup.sup

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
s : Finset ℕ
⊢ s ⊆ range (s.sup id).succ

Tactic:
fun _ hn =>
  mem_range.2 <| Nat.lt_succ_of_le <| @le_sup _ _ _ _ _ id _ hn

Premises used: Iff.mpr, Nat.lt_succ_of_le, Finset.mem_range, Finset.le_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f : β → α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), Membership.mem (γ := Finset β) ∅ b → p (f b)
⊢ p (sup ∅ f)

Tactic:
hb

Premises used: Multiset.foldr, Finset.fold, Finset.sup, List.foldr, Multiset.fold
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f : β → α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), Membership.mem (γ := Finset β) ∅ b → p (f b)
⊢ p (sup ∅ f)

Tactic:
exact hb
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f : β → α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
a : β
s_1 : Finset β
h : a ∉ s_1
ih : ∀ (hs : ∀ b ∈ s_1, p (f b)), p (s_1.sup f)
hs : ∀ b ∈ Finset.cons a s_1 h, p (f b)
cons : ∀ (hs : p (f a) ∧ ∀ x ∈ s_1, p (f x)), p (f a ⊔ s_1.sup f)
⊢ p ((Finset.cons a s_1 h).sup f)

Tactic:
simp only [sup_cons, forall_mem_cons] at hs ⊢

Premises used: Finset.forall_mem_cons, Finset.sup_cons