awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : p (f a) ∧ ∀ x ∈ s_1, p (f x)
⊢ p (f a ⊔ s_1.sup f)

Tactic:
hp _ hs.1 _ (ih hs.2)

Premises used: And.right, And.left
-- 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 : p (f a) ∧ ∀ x ∈ s_1, p (f x)
⊢ p (f a ⊔ s_1.sup f)

Tactic:
exact hp _ hs.1 _ (ih hs.2)

Premises used: And.right, And.left
-- 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 ∈ s, p (f b)
empty : ∀ (hs : ∀ (b : β), Membership.mem (γ := Finset β) ∅ b → p (f b)), p (sup ∅ f)
cons :
  ∀ (a : β) (s : Finset β) (h : a ∉ s) (ih : ∀ (hs : ∀ b ∈ s, p (f b)), p (s.sup f))
    (hs : ∀ b ∈ Finset.cons a s h, p (f b)), p ((Finset.cons a s h).sup f)
⊢ p (s.sup f)

Tactic:
induction s using Finset.cons_induction with
  | empty => exact hb
  | cons _ _ _ ih =>
    simp only [sup_cons, forall_mem_cons] at hs ⊢
    exact hp _ hs.1 _ (ih hs.2)

Premises used: Finset.cons, Finset.forall_mem_cons, Finset.sup_cons
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ (∀ (x : α), Membership.mem (γ := Finset α) ∅ x → ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, sup ∅ id ≤ x

Tactic:
simpa only [forall_prop_of_true, and_true, forall_prop_of_false, bot_le, not_false_iff,
        sup_empty, forall_true_iff, notMem_empty]

Premises used: and_true, forall_prop_of_false, Finset.sup_empty, Finset.notMem_empty, forall_prop_of_true, forall_true_iff, not_false_iff, bot_le
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
r : Finset α
h_1 : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
⊢ r ⊆ insert a r

Tactic:
apply Finset.subset_insert

Premises used: Finset.subset_insert
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
r : Finset α
h_1 : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
⊢ (↑r : Set α) ⊆ (↑(insert a r) : Set α)

Tactic:
have incs : (r : Set α) ⊆ ↑(insert a r) := by
        rw [Finset.coe_subset]
        apply Finset.subset_insert
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
r : Finset α
h_1 : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ Insert.insert a r, ∃ y ∈ s, x ≤ y
incs : (↑r : Set α) ⊆ (↑(Insert.insert a r) : Set α)
insert : ∀ (x : α) (hxs : x ∈ s) (hsx_sup : r.sup id ≤ x), ∃ x ∈ s, (Insert.insert a r).sup id ≤ x
⊢ ∃ x ∈ s, (Insert.insert a r).sup id ≤ x

Tactic:
obtain ⟨x, ⟨hxs, hsx_sup⟩⟩ := ih fun x hx => h x <| incs hx
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
r : Finset α
h_1 : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ Insert.insert a r, ∃ y ∈ s, x ≤ y
incs : (↑r : Set α) ⊆ (↑(Insert.insert a r) : Set α)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
insert : ∀ (y : α) (hys : y ∈ s) (hay : a ≤ y), ∃ x ∈ s, (Insert.insert a r).sup id ≤ x
⊢ ∃ x ∈ s, (Insert.insert a r).sup id ≤ x

Tactic:
obtain ⟨y, hys, hay⟩ := h a (Finset.mem_insert_self a r)

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
r : Finset α
h_1 : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ Insert.insert a r, ∃ y ∈ s, x ≤ y
incs : (↑r : Set α) ⊆ (↑(Insert.insert a r) : Set α)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
insert : ∀ (z : α) (hzs : z ∈ s) (hxz : x ≤ z) (hyz : y ≤ z), ∃ x ∈ s, (Insert.insert a r).sup id ≤ x
⊢ ∃ x ∈ s, (Insert.insert a r).sup id ≤ x

Tactic:
obtain ⟨z, hzs, ⟨hxz, hyz⟩⟩ := hdir x hxs y hys
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
r : Finset α
h_1 : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
incs : (↑r : Set α) ⊆ (↑(insert a r) : Set α)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
right : (insert a r).sup id ≤ z
⊢ ∃ x ∈ s, (insert a r).sup id ≤ x

Tactic:
use z, hzs
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
r : Finset α
h_1 : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
incs : (↑r : Set α) ⊆ (↑(insert a r) : Set α)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
right : a ≤ z ∧ r.sup id ≤ z
⊢ (insert a r).sup id ≤ z

Tactic:
rw [sup_insert, id, sup_le_iff]

Premises used: Finset.sup_insert, id, sup_le_iff
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
r : Finset α
h_1 : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
incs : (↑r : Set α) ⊆ (↑(insert a r) : Set α)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ a ≤ z ∧ r.sup id ≤ z

Tactic:
⟨le_trans hay hyz, le_trans hsx_sup hxz⟩

Premises used: And.intro, le_trans
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
r : Finset α
h_1 : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
incs : (↑r : Set α) ⊆ (↑(insert a r) : Set α)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ a ≤ z ∧ r.sup id ≤ z

Tactic:
exact ⟨le_trans hay hyz, le_trans hsx_sup hxz⟩
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
t : Finset α
empty : (∀ (x : α), Membership.mem (γ := Finset α) ∅ x → ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, sup ∅ id ≤ x
insert :
  ∀ (a : α) (r : Finset α),
    a ∉ r →
      ∀ (ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x),
        (∀ x ∈ Insert.insert a r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, (Insert.insert a r).sup id ≤ x
⊢ (∀ x ∈ t, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, t.sup id ≤ x

Tactic:
induction t using Finset.induction_on with
    | empty =>
      simpa only [forall_prop_of_true, and_true, forall_prop_of_false, bot_le, not_false_iff,
        sup_empty, forall_true_iff, notMem_empty]
    | insert a r _ ih =>
      intro h
      have incs : (r : Set α) ⊆ ↑(insert a r) := by
        rw [Finset.coe_subset]
        apply Finset.subset_insert
      -- x ∈ s is above the sup of r
      obtain ⟨x, ⟨hxs, hsx_sup⟩⟩ := ih fun x hx => h x <| incs hx
      -- y ∈ s is above a
      obtain ⟨y, hys, hay⟩ := h a (Finset.mem_insert_self a r)
      -- z ∈ s is above x and y
      obtain ⟨z, hzs, ⟨hxz, hyz⟩⟩ := hdir x hxs y hys
      use z, hzs
      rw [sup_insert, id, sup_le_iff]
      exact ⟨le_trans hay hyz, le_trans hsx_sup hxz⟩

Premises used: Finset.sup_insert, and_true, forall_prop_of_false, Finset.sup_empty, id, Insert.insert, Finset.notMem_empty, sup_le_iff, forall_prop_of_true, forall_true_iff, not_false_iff, bot_le
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
t : Finset α
empty : (∀ (x : α), Membership.mem (γ := Finset α) ∅ x → ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, sup ∅ id ≤ x
insert :
  ∀ (a : α) (r : Finset α),
    a ∉ r →
      ∀ (ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x),
        (∀ x ∈ Insert.insert a r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, (Insert.insert a r).sup id ≤ x
⊢ (∀ x ∈ t, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, t.sup id ≤ x

Tactic:
classical
    induction t using Finset.induction_on with
    | empty =>
      simpa only [forall_prop_of_true, and_true, forall_prop_of_false, bot_le, not_false_iff,
        sup_empty, forall_true_iff, notMem_empty]
    | insert a r _ ih =>
      intro h
      have incs : (r : Set α) ⊆ ↑(insert a r) := by
        rw [Finset.coe_subset]
        apply Finset.subset_insert
      -- x ∈ s is above the sup of r
      obtain ⟨x, ⟨hxs, hsx_sup⟩⟩ := ih fun x hx => h x <| incs hx
      -- y ∈ s is above a
      obtain ⟨y, hys, hay⟩ := h a (Finset.mem_insert_self a r)
      -- z ∈ s is above x and y
      obtain ⟨z, hzs, ⟨hxz, hyz⟩⟩ := hdir x hxs y hys
      use z, hzs
      rw [sup_insert, id, sup_le_iff]
      exact ⟨le_trans hay hyz, le_trans hsx_sup hxz⟩

Premises used: Finset.sup_insert, and_true, forall_prop_of_false, Finset.sup_empty, id, Insert.insert, Finset.notMem_empty, sup_le_iff, forall_prop_of_true, forall_true_iff, not_false_iff, bot_le
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Set α
w₁ : ⊥ ∈ s
w₂ : ∀ x ∈ s, ∀ y ∈ s, x ⊔ y ∈ s
ι : Type u_7
t : Finset ι
p : ι → α
h : ∀ i ∈ t, p i ∈ s
⊢ t.sup p ∈ s

Tactic:
@sup_induction _ _ _ _ _ _ (· ∈ s) w₁ w₂ h

Premises used: Finset.sup_induction
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
f : β → α
S : Finset β
empty : sup ∅ f = ⊥ ↔ ∀ (s : β), Membership.mem (γ := Finset β) ∅ s → f s = ⊥
insert :
  ∀ (a : β) (s : Finset β),
    a ∉ s →
      (s.sup f = ⊥ ↔ ∀ s_1 ∈ s, f s_1 = ⊥) → ((Insert.insert a s).sup f = ⊥ ↔ ∀ s_1 ∈ Insert.insert a s, f s_1 = ⊥)
⊢ S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥

Tactic:
induction S using Finset.induction
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
f : β → α
⊢ sup ∅ f = ⊥ ↔ ∀ (s : β), Membership.mem (γ := Finset β) ∅ s → f s = ⊥

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
f : β → α
a : β
s : Finset β
h : a ∉ s
h_1 : s.sup f = ⊥ ↔ ∀ s_1 ∈ s, f s_1 = ⊥
⊢ (insert a s).sup f = ⊥ ↔ ∀ s_1 ∈ insert a s, f s_1 = ⊥

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
f : β → α
S : Finset β
empty : sup ∅ f = ⊥ ↔ ∀ (s : β), Membership.mem (γ := Finset β) ∅ s → f s = ⊥
insert :
  ∀ (a : β) (s : Finset β),
    a ∉ s →
      (s.sup f = ⊥ ↔ ∀ s_1 ∈ s, f s_1 = ⊥) → ((Insert.insert a s).sup f = ⊥ ↔ ∀ s_1 ∈ Insert.insert a s, f s_1 = ⊥)
empty₁ : sup ∅ f = ⊥ ↔ ∀ (s : β), Membership.mem (γ := Finset β) ∅ s → f s = ⊥
insert₁ :
  ∀ (a : β) (s : Finset β),
    a ∉ s →
      (s.sup f = ⊥ ↔ ∀ s_1 ∈ s, f s_1 = ⊥) → ((Insert.insert a s).sup f = ⊥ ↔ ∀ s_1 ∈ Insert.insert a s, f s_1 = ⊥)
empty₂ : sup ∅ f = ⊥ ↔ ∀ (s : β), Membership.mem (γ := Finset β) ∅ s → f s = ⊥
insert₂ :
  ∀ (a : β) (s : Finset β),
    a ∉ s →
      (s.sup f = ⊥ ↔ ∀ s_1 ∈ s, f s_1 = ⊥) → ((Insert.insert a s).sup f = ⊥ ↔ ∀ s_1 ∈ Insert.insert a s, f s_1 = ⊥)
empty₃ : sup ∅ f = ⊥ ↔ ∀ (s : β), Membership.mem (γ := Finset β) ∅ s → f s = ⊥
insert₃ :
  ∀ (a : β) (s : Finset β),
    a ∉ s →
      (s.sup f = ⊥ ↔ ∀ s_1 ∈ s, f s_1 = ⊥) → ((Insert.insert a s).sup f = ⊥ ↔ ∀ s_1 ∈ Insert.insert a s, f s_1 = ⊥)
⊢ S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥

Tactic:
classical induction S using Finset.induction <;> simp [*]
-- 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 : β ⊕ γ → α
⊢ (s.disjSum t).sup f = (s.sup fun (x : β) ↦ f (Sum.inl x)) ⊔ t.sup fun (x : γ) ↦ f (Sum.inr x)

Tactic:
congr(fold _ $(bot_sup_eq _ |>.symm) _ _).trans (fold_disjSum _ _ _ _ _ _)

Premises used: Finset.fold_disjSum, congrArg, Finset.fold, bot_sup_eq, id, Finset.sup, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : IsEmpty β
f : β → α
S : Finset β
rw : ∀ s ∈ S, f s = ⊥
⊢ S.sup f = ⊥

Tactic:
rw [Finset.sup_eq_bot_iff]

Premises used: Finset.sup_eq_bot_iff
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : IsEmpty β
f : β → α
S : Finset β
⊢ ∀ s ∈ S, f s = ⊥

Tactic:
fun x _ => False.elim <| IsEmpty.false x

Premises used: False.elim, IsEmpty.false
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : IsEmpty β
f : β → α
S : Finset β
⊢ ∀ s ∈ S, f s = ⊥

Tactic:
exact fun x _ => False.elim <| IsEmpty.false x

Premises used: False.elim, IsEmpty.false
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
p : β → Prop
inst_2 : DecidablePred p
f : (b : β) → p b → α
g : (b : β) → ¬p b → α
b : β
h₀ : b ∈ s
h₁ : p b
⊢ f b h₁ ≤ s.sup fun (i : β) ↦ if h : p i then f i h else g i h

Tactic:
grind [le_sup_of_le]

Premises used: Finset.le_sup_of_le
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
p : β → Prop
inst_2 : DecidablePred p
f : (b : β) → p b → α
g : (b : β) → ¬p b → α
b : β
h₀ : b ∈ s
h₁ : ¬p b
⊢ g b h₁ ≤ s.sup fun (i : β) ↦ if h : p i then f i h else g i h

Tactic:
grind [le_sup_of_le]

Premises used: Finset.le_sup_of_le
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice β
s : Finset α
f : α → β
⊢ s.sup f = ⨆ a ∈ s, f a

Tactic:
le_antisymm
    (Finset.sup_le (fun a ha => le_iSup_of_le a <| le_iSup (fun _ => f a) ha))
    (iSup_le fun _ => iSup_le fun ha => le_sup ha)

Premises used: le_iSup, Finset.sup_le, le_antisymm, le_iSup_of_le, iSup_le, Finset.le_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
inst : CompleteLattice α
s : Finset α
⊢ s.sup id = sSup (↑s : Set α)

Tactic:
simp [sSup_eq_iSup, sup_eq_iSup]

Premises used: sSup_eq_iSup, Finset.sup_eq_iSup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
s : Finset (Set α)
⊢ s.sup id = ⋃₀ (↑s : Set (Set α))

Tactic:
sup_id_eq_sSup _

Premises used: Set.sUnion, Finset.sup_id_eq_sSup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
s : Finset (Set α)
⊢ s.inf id = ⋂₀ (↑s : Set (Set α))

Tactic:
inf_id_eq_sInf _

Premises used: Finset.inf_id_eq_sInf, Set.sInter
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
s : Finset α
f : α → Set β
⊢ s.sup f = ⋃ x ∈ s, f x

Tactic:
sup_eq_iSup _ _

Premises used: Finset.sup_eq_iSup, Set.iUnion
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
s : Finset α
f : α → Set β
⊢ s.inf f = ⋂ x ∈ s, f x

Tactic:
inf_eq_iInf _ _

Premises used: Set.iInter, Finset.inf_eq_iInf
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice β
s : Finset α
f : α → β
rw : s.sup f = sSup (↑(image f s) : Set β)
rw₁ : s.sup f = (image f s).sup id
rw₂ : s.sup f = s.sup (id ∘ f)
rw₃ rw₄ : s.sup f = s.sup f
⊢ s.sup f = sSup (f '' (↑s : Set α))

Tactic:
rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.id_comp]

Premises used: Finset.coe_image, Finset.sup_image, Finset.sup_id_eq_sSup, Function.id_comp
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice β
s : Finset α
f : α → β
classical : s.sup f = sSup (↑(image f s) : Set β)
classical₁ : s.sup f = (image f s).sup id
classical₂ : s.sup f = s.sup (id ∘ f)
classical₃ classical₄ : s.sup f = s.sup f
⊢ s.sup f = sSup (f '' (↑s : Set α))

Tactic:
classical rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.id_comp]

Premises used: Finset.coe_image, Finset.sup_image, Finset.sup_id_eq_sSup, Function.id_comp
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup β
inst_1 : OrderBot β
inst_2 : WellFoundedGT β
f : α → β
inl : IsEmpty α → ∃ (t : Finset α), ∀ (a : α), f a ≤ t.sup f
inr : Nonempty α → ∃ (t : Finset α), ∀ (a : α), f a ≤ t.sup f
⊢ ∃ (t : Finset α), ∀ (a : α), f a ≤ t.sup f

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup β
inst_1 : OrderBot β
inst_2 : WellFoundedGT β
f : α → β
h : IsEmpty α
⊢ ∃ (t : Finset α), ∀ (a : α), f a ≤ t.sup f

Tactic:
⟨⊥, isEmptyElim⟩

Premises used: isEmptyElim, Bot.bot, Exists.intro
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup β
inst_1 : OrderBot β
inst_2 : WellFoundedGT β
f : α → β
h : IsEmpty α
⊢ ∃ (t : Finset α), ∀ (a : α), f a ≤ t.sup f

Tactic:
exact ⟨⊥, isEmptyElim⟩
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup β
inst_1 : OrderBot β
inst_2 : WellFoundedGT β
f : α → β
h : Nonempty α
inr :
  ∀ (t : Finset α)
    (ht :
      ∀ (x : β),
        Membership.mem (γ := Set β) (Set.range fun (x : Finset α) ↦ x.sup f) x → ¬(fun (x : Finset α) ↦ x.sup f) t < x),
    ∃ (t : Finset α), ∀ (a : α), f a ≤ t.sup f
⊢ ∃ (t : Finset α), ∀ (a : α), f a ≤ t.sup f

Tactic:
obtain ⟨_, ⟨t, rfl⟩, ht⟩ := wellFounded_gt.has_min _ (Set.range_nonempty (sup · f))

Premises used: Set.range_nonempty, Finset.sup, wellFounded_gt, WellFounded.has_min, rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup β
inst_1 : OrderBot β
inst_2 : WellFoundedGT β
f : α → β
h : Nonempty α
t : Finset α
ht :
  ∀ (x : β),
    Membership.mem (γ := Set β) (Set.range fun (x : Finset α) ↦ x.sup f) x → ¬(fun (x : Finset α) ↦ x.sup f) t < x
⊢ ∃ (t : Finset α), ∀ (a : α), f a ≤ t.sup f

Tactic:
⟨t, fun a ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup β
inst_1 : OrderBot β
inst_2 : WellFoundedGT β
f : α → β
h : Nonempty α
t : Finset α
ht :
  ∀ (x : β),
    Membership.mem (γ := Set β) (Set.range fun (x : Finset α) ↦ x.sup f) x → ¬(fun (x : Finset α) ↦ x.sup f) t < x
inr : ∀ (a : α), f a ≤ t.sup f
⊢ ∃ (t : Finset α), ∀ (a : α), f a ≤ t.sup f

Tactic:
refine ⟨t, fun a ↦ ?_⟩
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup β
inst_1 : OrderBot β
inst_2 : WellFoundedGT β
f : α → β
h : Nonempty α
t : Finset α
ht :
  ∀ (x : β),
    Membership.mem (γ := Set β) (Set.range fun (x : Finset α) ↦ x.sup f) x → ¬(fun (x : Finset α) ↦ x.sup f) t < x
a : α
⊢ (fun (x : Finset α) ↦ x.sup f) (insert a t) = f a ⊔ t.sup f

Tactic:
simp
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup β
inst_1 : OrderBot β
inst_2 : WellFoundedGT β
f : α → β
h : Nonempty α
t : Finset α
ht :
  ∀ (x : β),
    Membership.mem (γ := Set β) (Set.range fun (x : Finset α) ↦ x.sup f) x → ¬(fun (x : Finset α) ↦ x.sup f) t < x
a : α
⊢ ¬(fun (x : Finset α) ↦ x.sup f) t < f a ⊔ t.sup f

Tactic:
have := ht (f a ⊔ t.sup f) ⟨insert a t, by simp⟩
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup β
inst_1 : OrderBot β
inst_2 : WellFoundedGT β
f : α → β
h : Nonempty α
t : Finset α
ht :
  ∀ (x : β),
    Membership.mem (γ := Set β) (Set.range fun (x : Finset α) ↦ x.sup f) x → ¬(fun (x : Finset α) ↦ x.sup f) t < x
a : α
this : ¬(fun (x : Finset α) ↦ x.sup f) t < f a ⊔ t.sup f
inr : ∀ (this : ¬¬f a ≤ (fun (x : Finset α) ↦ x.sup f) t), f a ≤ t.sup f
inr₁ inr₂ inr₃ inr₄ : ∀ (this : f a ≤ (fun (x : Finset α) ↦ x.sup f) t), f a ≤ t.sup f
⊢ f a ≤ t.sup f

Tactic:
rwa [right_lt_sup, not_not] at this

Premises used: Classical.not_not, right_lt_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup β
inst_1 : OrderBot β
inst_2 : WellFoundedGT β
f : α → β
h : Nonempty α
t : Finset α
ht :
  ∀ (x : β),
    Membership.mem (γ := Set β) (Set.range fun (x : Finset α) ↦ x.sup f) x → ¬(fun (x : Finset α) ↦ x.sup f) t < x
a : α
inr inr₁ inr₂ : ∀ (this : ¬(fun (x : Finset α) ↦ x.sup f) t < f a ⊔ t.sup f), f a ≤ t.sup f
⊢ f a ≤ t.sup f

Tactic:
classical
  have := ht (f a ⊔ t.sup f) ⟨insert a t, by simp⟩
  rwa [right_lt_sup, not_not] at this

Premises used: Classical.not_not, right_lt_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice β
inst_1 : WellFoundedGT β
f : α → β
⊢ ∃ (t : Finset α), t.sup f = ⨆ (a : α), f a

Tactic:
have ⟨t, ht⟩ := exists_sup_ge f
  ⟨t, (Finset.sup_le fun _ _ ↦ le_iSup ..).antisymm <| iSup_le ht⟩

Premises used: iSup, Exists, LE.le.antisymm, le_iSup, Finset.exists_sup_ge, Finset.sup_le, Exists.intro, _private.0.Finset.exists_sup_eq_iSup.match_1, iSup_le, Finset.sup, Eq
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f : β → α
⊢ Eq (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) (s.sup f) : αᵒᵈ) (s.inf ((⇑toDual : (a : α) → αᵒᵈ) ∘ f) : αᵒᵈ)

Tactic:
rfl

Premises used: Multiset.foldr, Finset.fold, Finset.sup, OrderDual, Finset.inf, rfl, Multiset.fold
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeInf α
inst_1 : OrderTop α
s : Finset β
f : β → αᵒᵈ
⊢ Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) (s.sup f) : α) (s.inf ((⇑ofDual : (a : αᵒᵈ) → α) ∘ f) : α)

Tactic:
rfl

Premises used: Multiset.foldr, Finset.fold, Finset.sup, OrderDual, Finset.inf, rfl, Multiset.fold
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
inst_1 : OrderBot α
f : ι → α
a : α
empty : a ⊓ ⊥ = ⊥
⊢ a ⊓ sup ∅ f = sup ∅ fun (i : ι) ↦ a ⊓ f i

Tactic:
simp_rw [Finset.sup_empty, inf_bot_eq]

Premises used: Finset.sup_empty, inf_bot_eq
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
inst_1 : OrderBot α
f : ι → α
a : α
a_1 : ι
s : Finset ι
h_1 : a_1 ∉ s
h : a ⊓ s.sup f = s.sup fun (i : ι) ↦ a ⊓ f i
cons : a ⊓ (f a_1 ⊔ s.sup f) = (Finset.cons a_1 s h_1).sup fun (i : ι) ↦ a ⊓ f i
cons₁ : a ⊓ (f a_1 ⊔ s.sup f) = a ⊓ f a_1 ⊔ s.sup fun (i : ι) ↦ a ⊓ f i
cons₂ : a ⊓ f a_1 ⊔ a ⊓ s.sup f = a ⊓ f a_1 ⊔ s.sup fun (i : ι) ↦ a ⊓ f i
cons₃ cons₄ : (a ⊓ f a_1 ⊔ s.sup fun (i : ι) ↦ a ⊓ f i) = a ⊓ f a_1 ⊔ s.sup fun (i : ι) ↦ a ⊓ f i
⊢ a ⊓ (Finset.cons a_1 s h_1).sup f = (Finset.cons a_1 s h_1).sup fun (i : ι) ↦ a ⊓ f i

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

Premises used: inf_sup_left, Finset.sup_cons
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
empty : a ⊓ sup ∅ f = sup ∅ fun (i : ι) ↦ a ⊓ f i
cons :
  ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s) (h_1 : a ⊓ s.sup f = s.sup fun (i : ι) ↦ a ⊓ f i),
    a ⊓ (Finset.cons a_1 s h).sup f = (Finset.cons a_1 s h).sup fun (i : ι) ↦ a ⊓ f i
⊢ a ⊓ s.sup f = s.sup fun (i : ι) ↦ a ⊓ f i

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

Premises used: Finset.cons, Finset.sup_empty, inf_sup_left, inf_bot_eq, Finset.sup_cons