awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
hs : s.Nonempty
empty : ∀ (hs : Finset.Nonempty.{u_5} (α := ι) ∅), sup ∅ f ∈ f '' (↑∅ : Set ι)
insert :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ∀ (h : ∀ (hs : s.Nonempty), s.sup f ∈ f '' (↑s : Set ι)) (hs : (Insert.insert a s).Nonempty),
        (Insert.insert a s).sup f ∈ f '' (↑(Insert.insert a s) : Set ι)
⊢ s.sup f ∈ f '' (↑s : Set ι)

Tactic:
induction s using Finset.induction with
  | empty => simp only [Finset.not_nonempty_empty] at hs
  | insert a s _ h =>
    rw [Finset.sup_insert (b := a) (s := s) (f := f)]
    cases s.eq_empty_or_nonempty with
    | inl hs => simp [hs]
    | inr hs =>
      simp only [Finset.coe_insert]
      rcases le_total (f a) (s.sup f) with (ha | ha)
      · rw [sup_eq_right.mpr ha]
        exact Set.image_mono (Set.subset_insert a s) (h hs)
      · rw [sup_eq_left.mpr ha]
        apply Set.mem_image_of_mem _ (Set.mem_insert a ↑s)

Premises used: Finset.not_nonempty_empty, Insert.insert, Finset.coe_insert, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
hs : s.Nonempty
empty : ∀ (hs : Finset.Nonempty.{u_5} (α := ι) ∅), sup ∅ f ∈ f '' (↑∅ : Set ι)
insert :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ∀ (h : ∀ (hs : s.Nonempty), s.sup f ∈ f '' (↑s : Set ι)) (hs : (Insert.insert a s).Nonempty),
        (Insert.insert a s).sup f ∈ f '' (↑(Insert.insert a s) : Set ι)
⊢ s.sup f ∈ f '' (↑s : Set ι)

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp only [Finset.not_nonempty_empty] at hs
  | insert a s _ h =>
    rw [Finset.sup_insert (b := a) (s := s) (f := f)]
    cases s.eq_empty_or_nonempty with
    | inl hs => simp [hs]
    | inr hs =>
      simp only [Finset.coe_insert]
      rcases le_total (f a) (s.sup f) with (ha | ha)
      · rw [sup_eq_right.mpr ha]
        exact Set.image_mono (Set.subset_insert a s) (h hs)
      · rw [sup_eq_left.mpr ha]
        apply Set.mem_image_of_mem _ (Set.mem_insert a ↑s)

Premises used: Finset.not_nonempty_empty, Insert.insert, Finset.coe_insert, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
f : β → α
b : β
h : b ∈ s
⊢ ∃ (a : α), s.sup (WithBot.some ∘ f) = (↑a : WithBot α)

Tactic:
(WithBot.le_iff_forall.1 (le_sup (α := WithBot α) h) (f b) rfl).imp fun _ ↦ And.left

Premises used: WithBot.le_iff_forall, Exists.imp, And.left, Iff.mp, Finset.le_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
⊢ s.sup (WithBot.some ∘ f) ≠ ⊥

Tactic:
simpa using H
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
rw : (↑((s.sup (WithBot.some ∘ f)).unbot ⋯) : WithBot α) = s.sup (WithBot.some ∘ f)
rw₁ rw₂ : s.sup (WithBot.some ∘ f) = s.sup (WithBot.some ∘ f)
⊢ (↑(s.sup' H f) : WithBot α) = s.sup (WithBot.some ∘ f)

Tactic:
rw [sup', WithBot.coe_unbot]

Premises used: WithBot.coe_unbot, Finset.sup'
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
b : β
hb : b ∉ s
rw : (↑((cons b s hb).sup' ⋯ f) : WithBot α) = (↑(f b ⊔ s.sup' H f) : WithBot α)
⊢ (cons b s hb).sup' ⋯ f = f b ⊔ s.sup' H f

Tactic:
rw [← WithBot.coe_eq_coe]

Premises used: WithBot.coe_eq_coe
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
b : β
hb : b ∉ s
⊢ (↑((cons b s hb).sup' ⋯ f) : WithBot α) = (↑(f b ⊔ s.sup' H f) : WithBot α)

Tactic:
simp [WithBot.coe_sup]

Premises used: WithBot.coe_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
inst_1 : DecidableEq β
b : β
rw : (↑((insert b s).sup' ⋯ f) : WithBot α) = (↑(f b ⊔ s.sup' H f) : WithBot α)
⊢ (insert b s).sup' ⋯ f = f b ⊔ s.sup' H f

Tactic:
rw [← WithBot.coe_eq_coe]

Premises used: WithBot.coe_eq_coe
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
inst_1 : DecidableEq β
b : β
⊢ (↑((insert b s).sup' ⋯ f) : WithBot α) = (↑(f b ⊔ s.sup' H f) : WithBot α)

Tactic:
simp [WithBot.coe_sup]

Premises used: WithBot.coe_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
f : β → α
b : β
⊢ sup' {b} ⋯ f = f b

Tactic:
rfl

Premises used: WithBot.unbot, Finset.sup', rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
a : α
simp_rw : (∀ b ∈ s, (WithBot.some ∘ f) b ≤ (↑a : WithBot α)) ↔ ∀ b ∈ s, (↑(f b) : WithBot α) ≤ (↑a : WithBot α)
⊢ s.sup' H f ≤ a ↔ ∀ b ∈ s, f b ≤ a

Tactic:
simp_rw [← @WithBot.coe_le_coe α, coe_sup', Finset.sup_le_iff]

Premises used: Finset.coe_sup', WithBot.coe_le_coe, Finset.sup_le_iff
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
a : α
⊢ (∀ b ∈ s, (WithBot.some ∘ f) b ≤ (↑a : WithBot α)) ↔ ∀ b ∈ s, (↑(f b) : WithBot α) ≤ (↑a : WithBot α)

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
f : β → α
b : β
h : b ∈ s
⊢ f b ≤ s.sup' ⋯ f

Tactic:
(sup'_le_iff ⟨b, h⟩ f).1 le_rfl b h

Premises used: le_rfl, Finset.sup'_le_iff, Exists.intro, Iff.mp
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
inst : SemilatticeSup α
s : Finset α
hs : s.Nonempty
⊢ IsLUB (↑s : Set α) (s.sup' hs id)

Tactic:
⟨fun x h => id_eq x ▸ le_sup' id h, fun _ h => Finset.sup'_le hs id h⟩

Premises used: Eq.rec, id, IsLeast, Finset.sup'_le, And.intro, IsLUB, Finset.le_sup', id_eq
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
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 α
s : Finset β
H : s.Nonempty
f : β → α
a : α
h : ∀ b ∈ s, f b = a
⊢ s.sup' H f = a

Tactic:
le_antisymm (sup'_le _ _ (fun _ hb ↦ (h _ hb).le))
    (le_sup'_of_le _ H.choose_spec (h _ H.choose_spec).ge)

Premises used: Exists.choose_spec, Eq.ge, Finset.le_sup'_of_le, Eq.le, le_antisymm, Finset.sup'_le
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
a : α
⊢ (s.sup' H fun (x : β) ↦ a) = a

Tactic:
sup'_eq_of_forall H (fun _ ↦ a) fun _ ↦ congrFun rfl

Premises used: Finset.sup'_eq_of_forall, congrFun, rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : DecidableEq β
s₁ s₂ : Finset β
h₁ : s₁.Nonempty
h₂ : s₂.Nonempty
f : β → α
a : α
⊢ (s₁ ∪ s₂).sup' ⋯ f ≤ a ↔ s₁.sup' h₁ f ⊔ s₂.sup' h₂ f ≤ a

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
γ : Type u_4
inst : SemilatticeSup α
s : Finset β
t : Finset γ
hs : s.Nonempty
ht : t.Nonempty
f : β → γ → α
a : α
⊢ (s.sup' hs fun (b : β) ↦ t.sup' ht (f b)) ≤ a ↔ (t.sup' ht fun (c : γ) ↦ s.sup' hs 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 α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
change : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p (↑(s.sup' H f) : WithBot α)
⊢ p (s.sup' H f)

Tactic:
change @WithBot.recBotCoe α (fun _ => Prop) True p ↑(s.sup' H f)

Premises used: WithBot.some, True, WithBot.recBotCoe, Finset.sup'
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
rw : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p (s.sup (WithBot.some ∘ f))
⊢ WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p (↑(s.sup' H f) : WithBot α)

Tactic:
rw [coe_sup']

Premises used: Finset.coe_sup'
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
⊢ WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p (s.sup (WithBot.some ∘ f))

Tactic:
sup_induction trivial (fun a₁ h₁ a₂ h₂ ↦ ?_) hs

Premises used: trivial, Finset.sup_induction
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
refine :
  ∀ (a₁ : WithBot α) (h₁ : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p a₁) (a₂ : WithBot α)
    (h₂ : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p a₂),
    WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p (a₁ ⊔ a₂)
⊢ WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p (s.sup (WithBot.some ∘ f))

Tactic:
refine sup_induction trivial (fun a₁ h₁ a₂ h₂ ↦ ?_) hs
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁ a₂ x : WithBot α
h₁ : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p ⊥
h₂ : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p x
rwa rwa₁ rwa₂ rwa₃ : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p x
⊢ WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p (⊥ ⊔ x)

Tactic:
rwa [bot_sup_eq]

Premises used: bot_sup_eq
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁_1 a₂ : WithBot α
a₁ : α
h₁ : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p (↑a₁ : WithBot α)
h₂ : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p ⊥
rwa rwa₁ rwa₂ rwa₃ : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p (↑a₁ : WithBot α)
⊢ WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p ((↑a₁ : WithBot α) ⊔ ⊥)

Tactic:
rwa [sup_bot_eq]

Premises used: sup_bot_eq
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁_1 a₂_1 : WithBot α
a₁ a₂ : α
h₁ : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p (↑a₁ : WithBot α)
h₂ : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p (↑a₂ : WithBot α)
⊢ WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p ((↑a₁ : WithBot α) ⊔ (↑a₂ : WithBot α))

Tactic:
hp a₁ h₁ a₂ h₂

Premises used: WithBot.recBotCoe
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁_1 a₂_1 : WithBot α
a₁ a₂ : α
h₁ : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p (↑a₁ : WithBot α)
h₂ : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p (↑a₂ : WithBot α)
⊢ WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p ((↑a₁ : WithBot α) ⊔ (↑a₂ : WithBot α))

Tactic:
exact hp a₁ h₁ a₂ h₂
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁ : WithBot α
h₁ : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p a₁
a₂ : WithBot α
h₂ : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p a₂
⊢ WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p (a₁ ⊔ a₂)

Tactic:
match a₁, a₂ with
  | ⊥, _ => rwa [bot_sup_eq]
  | (a₁ : α), ⊥ => rwa [sup_bot_eq]
  | (a₁ : α), (a₂ : α) => exact hp a₁ h₁ a₂ h₂
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
inst : SemilatticeSup α
s : Set α
w : ∀ x ∈ s, ∀ y ∈ s, x ⊔ y ∈ s
ι : Type u_7
t : Finset ι
H : t.Nonempty
p : ι → α
h : ∀ i ∈ t, p i ∈ s
⊢ t.sup' H p ∈ s

Tactic:
sup'_induction H p w h

Premises used: Finset.sup'_induction
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
t : Finset β
f g : β → α
h₁ : s = t
h₂ : ∀ x ∈ s, f x = g x
subst : ∀ (H : t.Nonempty) (h₂ : ∀ x ∈ t, f x = g x), t.sup' H f = t.sup' ⋯ g
⊢ s.sup' H f = t.sup' ⋯ g

Tactic:
subst s
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
t : Finset β
f g : β → α
H : t.Nonempty
h₂ : ∀ x ∈ t, f x = g x
⊢ t.sup' H f = t.sup' ⋯ g

Tactic:
eq_of_forall_ge_iff fun c => ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
t : Finset β
f g : β → α
H : t.Nonempty
h₂ : ∀ x ∈ t, f x = g x
refine : ∀ (c : α), t.sup' H f ≤ c ↔ t.sup' ⋯ g ≤ c
⊢ t.sup' H f = t.sup' ⋯ g

Tactic:
refine eq_of_forall_ge_iff fun c => ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
t : Finset β
f g : β → α
H : t.Nonempty
h₂ : ∀ x ∈ t, f x = g x
c : α
⊢ t.sup' H f ≤ c ↔ t.sup' ⋯ g ≤ c

Tactic:
simp +contextual only [sup'_le_iff, h₂]

Premises used: Finset.sup'_le_iff
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ g (s.sup' H f) = s.sup' H (g ∘ f)

Tactic:
H.cons_induction ?_ ?_

Premises used: Finset.Nonempty.cons_induction
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
refine_1 : ∀ (a : β), g (sup' {a} ⋯ f) = sup' {a} ⋯ (g ∘ f)
refine_2 :
  ∀ (a : β) (s : Finset β) (h : a ∉ s) (hs : s.Nonempty),
    g (s.sup' hs f) = s.sup' hs (g ∘ f) → g ((cons a s h).sup' ⋯ f) = (cons a s h).sup' ⋯ (g ∘ f)
⊢ g (s.sup' H f) = s.sup' H (g ∘ f)

Tactic:
refine H.cons_induction ?_ ?_
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
a : β
⊢ g (sup' {a} ⋯ f) = sup' {a} ⋯ (g ∘ f)

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
a : β
s_1 : Finset β
h : a ∉ s_1
hs : s_1.Nonempty
h_1 : g (s_1.sup' hs f) = s_1.sup' hs (g ∘ f)
⊢ g ((cons a s_1 h).sup' ⋯ f) = (cons a s_1 h).sup' ⋯ (g ∘ f)

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : FunLike F α β
inst_3 : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (s.sup' hs g) : β) (s.sup' hs ((⇑f : (a : α) → β) ∘ g) : β)

Tactic:
hs.cons_induction ?_ ?_

Premises used: Finset.Nonempty.cons_induction
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : FunLike F α β
inst_3 : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
refine_1 :
  ∀ (a : ι), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (sup' {a} ⋯ g) : β) (sup' {a} ⋯ ((⇑f : (a : α) → β) ∘ g) : β)
refine_2 :
  ∀ (a : ι) (s : Finset ι) (h : a ∉ s) (hs : s.Nonempty),
    Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (s.sup' hs g) : β) (s.sup' hs ((⇑f : (a : α) → β) ∘ g) : β) →
      Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ((cons a s h).sup' ⋯ g) : β)
        ((cons a s h).sup' ⋯ ((⇑f : (a : α) → β) ∘ g) : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (s.sup' hs g) : β) (s.sup' hs ((⇑f : (a : α) → β) ∘ g) : β)

Tactic:
refine hs.cons_induction ?_ ?_
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : FunLike F α β
inst_3 : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
a : ι
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (sup' {a} ⋯ g) : β) (sup' {a} ⋯ ((⇑f : (a : α) → β) ∘ g) : β)

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : FunLike F α β
inst_3 : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
a : ι
s_1 : Finset ι
h : a ∉ s_1
hs_1 : s_1.Nonempty
h_1 : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (s_1.sup' hs_1 g) : β) (s_1.sup' hs_1 ((⇑f : (a : α) → β) ∘ g) : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ((cons a s_1 h).sup' ⋯ g) : β)
    ((cons a s_1 h).sup' ⋯ ((⇑f : (a : α) → β) ∘ g) : β)

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : DecidableEq β
s : Finset γ
f : γ → β
hs : (image f s).Nonempty
g : β → α
rw : (↑((image f s).sup' hs g) : WithBot α) = (↑(s.sup' ⋯ (g ∘ f)) : WithBot α)
⊢ (image f s).sup' hs g = s.sup' ⋯ (g ∘ f)

Tactic:
rw [← WithBot.coe_eq_coe]

Premises used: WithBot.coe_eq_coe
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : DecidableEq β
s : Finset γ
f : γ → β
hs : (image f s).Nonempty
g : β → α
simp : s.sup ((WithBot.some ∘ g) ∘ f) = s.sup (WithBot.some ∘ g ∘ f)
⊢ (↑((image f s).sup' hs g) : WithBot α) = (↑(s.sup' ⋯ (g ∘ f)) : WithBot α)

Tactic:
simp only [coe_sup', sup_image]

Premises used: Finset.coe_sup', Finset.sup_image
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : DecidableEq β
s : Finset γ
f : γ → β
hs : (image f s).Nonempty
g : β → α
⊢ s.sup ((WithBot.some ∘ g) ∘ f) = s.sup (WithBot.some ∘ g ∘ f)

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : DecidableEq β
s : Finset γ
f : γ → β
hs : s.Nonempty
g : β → α
⊢ s.sup' hs (g ∘ f) = (image f s).sup' ⋯ g

Tactic:
.symm <| sup'_image _ _

Premises used: Finset.sup'_image, Eq.symm
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
s : Finset γ
f : γ ↪ β
g : β → α
hs : (map f s).Nonempty
rw : s.sup ((WithBot.some ∘ g) ∘ (⇑f : (a : γ) → β)) = s.sup (WithBot.some ∘ g ∘ (⇑f : (a : γ) → β))
⊢ (map f s).sup' hs g = s.sup' ⋯ (g ∘ (⇑f : (a : γ) → β))

Tactic:
rw [← WithBot.coe_eq_coe, coe_sup', sup_map, coe_sup']

Premises used: Finset.coe_sup', Finset.sup_map, WithBot.coe_eq_coe
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
s : Finset γ
f : γ ↪ β
g : β → α
hs : (map f s).Nonempty
⊢ s.sup ((WithBot.some ∘ g) ∘ (⇑f : (a : γ) → β)) = s.sup (WithBot.some ∘ g ∘ (⇑f : (a : γ) → β))

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
s : Finset γ
f : γ ↪ β
g : β → α
hs : s.Nonempty
⊢ s.sup' hs (g ∘ (⇑f : (a : γ) → β)) = (map f s).sup' ⋯ g

Tactic:
.symm <| sup'_map _ _

Premises used: Finset.sup'_map, Eq.symm
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
f : β → α
s₁ s₂ : Finset β
h : s₁ ⊆ s₂
h₁ : s₁.Nonempty
⊢ s₁.sup' h₁ f ≤ s₂.sup' ⋯ f

Tactic:
Finset.sup'_le h₁ _ (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
inst : SemilatticeSup α
s : Finset β
hs : s.Nonempty
f g : β → α
h : ∀ b ∈ s, f b ≤ g b
⊢ s.sup' hs f ≤ s.sup' hs g

Tactic:
sup'_le _ _ fun b hb ↦ (h b hb).trans (le_sup' _ hb)

Premises used: Finset.sup'_le, 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 : Finset β
H : s.Nonempty
f : β → α
⊢ s.sup' H f = s.sup f

Tactic:
le_antisymm (sup'_le H f fun _ => le_sup) (Finset.sup_le fun _ => le_sup' f)

Premises used: Finset.sup_le, le_antisymm, Finset.sup'_le, Finset.le_sup', Finset.le_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
h : s.Nonempty
f : β → α
⊢ (↑(s.sup f) : WithBot α) = s.sup (WithBot.some ∘ f)

Tactic:
simp only [← sup'_eq_sup h, coe_sup' h]

Premises used: Finset.coe_sup', Finset.sup'_eq_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
C : β → Type u_7
inst : (b : β) → SemilatticeSup (C b)
inst_1 : (b : β) → OrderBot (C b)
s : Finset α
f : α → (b : β) → C b
b : β
⊢ s.sup f b = s.sup fun (a : α) ↦ f a b

Tactic:
comp_sup_eq_sup_comp (fun x : ∀ b : β, C b => x b) (fun _ _ => rfl) rfl

Premises used: Finset.comp_sup_eq_sup_comp, rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
C : β → Type u_7
inst : (b : β) → SemilatticeSup (C b)
s : Finset α
H : s.Nonempty
f : α → (b : β) → C b
b : β
⊢ s.sup' H f b = s.sup' H fun (a : α) ↦ f a b

Tactic:
comp_sup'_eq_sup'_comp H (fun x : ∀ b : β, C b => x b) fun _ _ => rfl

Premises used: Finset.comp_sup'_eq_sup'_comp, rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : SemilatticeSup α
s : Finset ι
hs : s.Nonempty
f : ι → α
⊢ Eq (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) (s.sup' hs f) : αᵒᵈ) (s.inf' hs ((⇑toDual : (a : α) → αᵒᵈ) ∘ f) : αᵒᵈ)

Tactic:
rfl

Premises used: Finset.inf', WithTop.some, WithBot.unbot, WithTop.untop, OrderDual, Finset.inf, Finset.sup', rfl, WithTop
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : SemilatticeInf α
s : Finset ι
hs : s.Nonempty
f : ι → αᵒᵈ
⊢ Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) (s.sup' hs f) : α) (s.inf' hs ((⇑ofDual : (a : αᵒᵈ) → α) ∘ f) : α)

Tactic:
rfl

Premises used: Finset.inf', WithTop.some, WithBot.unbot, WithTop.untop, OrderDual, Finset.inf, Finset.sup', rfl, WithTop
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
a_1 : ι
⊢ a ⊓ sup' {a_1} ⋯ f = sup' {a_1} ⋯ fun (i : ι) ↦ a ⊓ f i

Tactic:
simp
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
s : Finset ι
hs_1 : s.Nonempty
f : ι → α
a : α
a_1 : ι
s_1 : Finset ι
h : a_1 ∉ s_1
hs : s_1.Nonempty
ih : a ⊓ s_1.sup' hs f = s_1.sup' hs fun (i : ι) ↦ a ⊓ f i
cons : a ⊓ (f a_1 ⊔ s_1.sup' hs f) = a ⊓ f a_1 ⊔ s_1.sup' hs fun (i : ι) ↦ a ⊓ f i
cons₁ : a ⊓ f a_1 ⊔ a ⊓ s_1.sup' hs f = a ⊓ f a_1 ⊔ s_1.sup' hs fun (i : ι) ↦ a ⊓ f i
⊢ a ⊓ (Finset.cons a_1 s_1 h).sup' ⋯ f = (Finset.cons a_1 s_1 h).sup' ⋯ fun (i : ι) ↦ a ⊓ f i

Tactic:
simp_rw [sup'_cons hs, inf_sup_left, ih]

Premises used: inf_sup_left, Finset.sup'_cons