awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
rw : Eq.{u_2 + 1} (α := α) (s.sup fun (i : ι) ↦ a ⊓ f i) (s.sup fun (i : ι) ↦ f i ⊓ a)
⊢ s.sup f ⊓ a = s.sup fun (i : ι) ↦ f i ⊓ a

Tactic:
rw [_root_.inf_comm, s.sup_inf_distrib_left]

Premises used: Finset.sup_inf_distrib_left, inf_comm
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ Eq.{u_2 + 1} (α := α) (s.sup fun (i : ι) ↦ a ⊓ f i) (s.sup fun (i : ι) ↦ f i ⊓ a)

Tactic:
simp_rw [_root_.inf_comm]

Premises used: inf_comm
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ Disjoint a (s.sup f) ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint a (f i)

Tactic:
simp only [disjoint_iff, sup_inf_distrib_left, Finset.sup_eq_bot_iff]

Premises used: Finset.sup_inf_distrib_left, disjoint_iff, Finset.sup_eq_bot_iff
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ Disjoint (s.sup f) a ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint (f i) a

Tactic:
simp only [disjoint_iff, sup_inf_distrib_right, Finset.sup_eq_bot_iff]

Premises used: disjoint_iff, Finset.sup_inf_distrib_right, Finset.sup_eq_bot_iff
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
f : ι → α
a : α
empty : ⊥ = a \ inf ∅ f
empty₁ : ⊥ = a \ ⊤
empty₂ empty₃ : Eq.{u_2 + 1} (α := α) ⊥ ⊥
⊢ (sup ∅ fun (b : ι) ↦ a \ f b) = a \ inf ∅ f

Tactic:
rw [sup_empty, inf_empty, sdiff_top]

Premises used: Finset.sup_empty, Finset.inf_empty, sdiff_top
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
f : ι → α
a : α
a_1 : ι
s : Finset ι
h_1 : a_1 ∉ s
h : (s.sup fun (b : ι) ↦ a \ f b) = a \ s.inf f
cons : (a \ f a_1 ⊔ s.sup fun (b : ι) ↦ a \ f b) = a \ (Finset.cons a_1 s h_1).inf f
cons₁ : (a \ f a_1 ⊔ s.sup fun (b : ι) ↦ a \ f b) = a \ (f a_1 ⊓ s.inf f)
cons₂ : a \ f a_1 ⊔ a \ s.inf f = a \ (f a_1 ⊓ s.inf f)
cons₃ cons₄ : a \ f a_1 ⊔ a \ s.inf f = a \ f a_1 ⊔ a \ s.inf f
⊢ ((Finset.cons a_1 s h_1).sup fun (b : ι) ↦ a \ f b) = a \ (Finset.cons a_1 s h_1).inf f

Tactic:
rw [sup_cons, inf_cons, h, sdiff_inf]

Premises used: sdiff_inf, Finset.sup_cons, Finset.inf_cons
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
empty : (sup ∅ fun (b : ι) ↦ a \ f b) = a \ inf ∅ f
cons :
  ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s) (h_1 : (s.sup fun (b : ι) ↦ a \ f b) = a \ s.inf f),
    ((Finset.cons a_1 s h).sup fun (b : ι) ↦ a \ f b) = a \ (Finset.cons a_1 s h).inf f
⊢ (s.sup fun (b : ι) ↦ a \ f b) = a \ s.inf f

Tactic:
induction s using Finset.cons_induction with
  | empty => rw [sup_empty, inf_empty, sdiff_top]
  | cons _ _ _ h => rw [sup_cons, inf_cons, h, sdiff_inf]

Premises used: Finset.cons, Finset.sup_empty, sdiff_inf, Finset.inf_empty, Finset.sup_cons, sdiff_top, Finset.inf_cons
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a_1 : ι
singleton : (inf {a_1} fun (b : ι) ↦ a \ f b) = a \ f a_1
singleton₁ singleton₂ : a \ f a_1 = a \ f a_1
⊢ (inf {a_1} fun (b : ι) ↦ a \ f b) = a \ sup {a_1} f

Tactic:
rw [sup_singleton, inf_singleton]

Premises used: Finset.sup_singleton, Finset.inf_singleton
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a_1 : ι
s_1 : Finset ι
h : a_1 ∉ s_1
hs : s_1.Nonempty
ih : (s_1.inf fun (b : ι) ↦ a \ f b) = a \ s_1.sup f
cons : ((Finset.cons a_1 s_1 h).inf fun (b : ι) ↦ a \ f b) = a \ (f a_1 ⊔ s_1.sup f)
cons₁ : (a \ f a_1 ⊓ s_1.inf fun (b : ι) ↦ a \ f b) = a \ (f a_1 ⊔ s_1.sup f)
cons₂ : a \ f a_1 ⊓ a \ s_1.sup f = a \ (f a_1 ⊔ s_1.sup f)
cons₃ cons₄ : a \ f a_1 ⊓ a \ s_1.sup f = a \ f a_1 ⊓ a \ s_1.sup f
⊢ ((Finset.cons a_1 s_1 h).inf fun (b : ι) ↦ a \ f b) = a \ (Finset.cons a_1 s_1 h).sup f

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

Premises used: sdiff_sup, Finset.sup_cons, Finset.inf_cons
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
singleton : ∀ (a_1 : ι), (inf {a_1} fun (b : ι) ↦ a \ f b) = a \ sup {a_1} f
cons :
  ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s),
    s.Nonempty →
      ∀ (ih : (s.inf fun (b : ι) ↦ a \ f b) = a \ s.sup f),
        ((Finset.cons a_1 s h).inf fun (b : ι) ↦ a \ f b) = a \ (Finset.cons a_1 s h).sup f
⊢ (s.inf fun (b : ι) ↦ a \ f b) = a \ s.sup f

Tactic:
induction hs using Finset.Nonempty.cons_induction with
  | singleton => rw [sup_singleton, inf_singleton]
  | cons _ _ _ _ ih => rw [sup_cons, inf_cons, ih, sdiff_sup]

Premises used: Finset.cons, Finset.sup_singleton, sdiff_sup, Finset.sup_cons, Finset.inf_singleton, Singleton.singleton, Finset.inf_cons
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a_1 : ι
singleton : f a_1 \ a = inf {a_1} f \ a
singleton₁ singleton₂ : f a_1 \ a = f a_1 \ a
⊢ (inf {a_1} fun (b : ι) ↦ f b \ a) = inf {a_1} f \ a

Tactic:
rw [inf_singleton, inf_singleton]

Premises used: Finset.inf_singleton
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a_1 : ι
s_1 : Finset ι
h : a_1 ∉ s_1
hs : s_1.Nonempty
ih : (s_1.inf fun (b : ι) ↦ f b \ a) = s_1.inf f \ a
cons : (f a_1 \ a ⊓ s_1.inf fun (b : ι) ↦ f b \ a) = (Finset.cons a_1 s_1 h).inf f \ a
cons₁ : (f a_1 \ a ⊓ s_1.inf fun (b : ι) ↦ f b \ a) = (f a_1 ⊓ s_1.inf f) \ a
cons₂ : f a_1 \ a ⊓ s_1.inf f \ a = (f a_1 ⊓ s_1.inf f) \ a
cons₃ cons₄ : f a_1 \ a ⊓ s_1.inf f \ a = f a_1 \ a ⊓ s_1.inf f \ a
⊢ ((Finset.cons a_1 s_1 h).inf fun (b : ι) ↦ f b \ a) = (Finset.cons a_1 s_1 h).inf f \ a

Tactic:
rw [inf_cons, inf_cons, ih, inf_sdiff]

Premises used: inf_sdiff, Finset.inf_cons
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
singleton : ∀ (a_1 : ι), (inf {a_1} fun (b : ι) ↦ f b \ a) = inf {a_1} f \ a
cons :
  ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s),
    s.Nonempty →
      ∀ (ih : (s.inf fun (b : ι) ↦ f b \ a) = s.inf f \ a),
        ((Finset.cons a_1 s h).inf fun (b : ι) ↦ f b \ a) = (Finset.cons a_1 s h).inf f \ a
⊢ (s.inf fun (b : ι) ↦ f b \ a) = s.inf f \ a

Tactic:
induction hs using Finset.Nonempty.cons_induction with
  | singleton => rw [inf_singleton, inf_singleton]
  | cons _ _ _ _ ih => rw [inf_cons, inf_cons, ih, inf_sdiff]

Premises used: Finset.cons, inf_sdiff, Finset.inf_singleton, Singleton.singleton, Finset.inf_cons
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
⊢ (s.inf fun (b : ι) ↦ f b ⇨ a) = s.sup f ⇨ a

Tactic:
@sup_sdiff_left αᵒᵈ _ _ _ _ _

Premises used: Multiset.foldr, Finset.fold, Finset.sup_sdiff_left, Finset.sup, OrderDual, Finset.inf, Multiset.fold
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ (s.sup fun (b : ι) ↦ f b ⇨ a) = s.inf f ⇨ a

Tactic:
@inf_sdiff_left αᵒᵈ _ _ _ hs _ _

Premises used: Multiset.foldr, Finset.fold, Finset.sup, Finset.inf_sdiff_left, OrderDual, Finset.inf, Multiset.fold
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ (s.sup fun (b : ι) ↦ a ⇨ f b) = a ⇨ s.sup f

Tactic:
@inf_sdiff_right αᵒᵈ _ _ _ hs _ _

Premises used: Multiset.foldr, Finset.fold, Finset.inf_sdiff_right, Finset.sup, OrderDual, Finset.inf, Multiset.fold
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
s : Finset ι
f : ι → α
⊢ (s.sup f)ᶜ = s.inf fun (i : ι) ↦ (f i)ᶜ

Tactic:
map_finset_sup (OrderIso.compl α) _ _

Premises used: OrderIso.compl, OrderDual, Finset.inf, map_finset_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
g : α → β
mono_g : Monotone g
bot : g ⊥ = ⊥
⊢ g (s.sup f) = s.sup (g ∘ f)

Tactic:
comp_sup_eq_sup_comp g mono_g.map_sup bot

Premises used: Finset.comp_sup_eq_sup_comp, Monotone.map_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
mp : a ≤ s.sup f → ∃ b ∈ s, a ≤ f b
mpr : (∃ b ∈ s, a ≤ f b) → a ≤ s.sup f
⊢ a ≤ s.sup f ↔ ∃ b ∈ s, a ≤ f b

Tactic:
apply Iff.intro

Premises used: Iff.intro
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ a ≤ sup ∅ f → ∃ (b : ι), Membership.mem (γ := Finset ι) ∅ b ∧ a ≤ f b

Tactic:
(absurd · (not_le_of_gt ha))

Premises used: absurd, not_le_of_gt
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ a ≤ sup ∅ f → ∃ (b : ι), Membership.mem (γ := Finset ι) ∅ b ∧ a ≤ f b

Tactic:
exact (absurd · (not_le_of_gt ha))

Premises used: absurd, not_le_of_gt
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : c ∉ t
ih : a ≤ t.sup f → ∃ b ∈ t, a ≤ f b
mp : a ≤ f c ∨ a ≤ t.sup f → ∃ b ∈ cons c t hc, a ≤ f b
⊢ a ≤ (cons c t hc).sup f → ∃ b ∈ cons c t hc, a ≤ f b

Tactic:
rw [sup_cons, le_sup_iff]

Premises used: Finset.sup_cons, le_sup_iff
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : c ∉ t
ih : a ≤ t.sup f → ∃ b ∈ t, a ≤ f b
⊢ a ≤ f c ∨ a ≤ t.sup f → ∃ b ∈ cons c t hc, a ≤ f b

Tactic:
fun
      | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
      | Or.inr h => let ⟨b, hb, hle⟩ := ih h; ⟨b, mem_cons.2 (Or.inr hb), hle⟩

Premises used: Iff.mpr, Finset.cons, Membership.mem, Exists, _private.0.Finset.le_sup_iff.match_2, LE.le, And, And.intro, Exists.intro, Or.inl, Finset.mem_cons, Or.inr, rfl, _private.0.Finset.le_sup_iff.match_1
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : c ∉ t
ih : a ≤ t.sup f → ∃ b ∈ t, a ≤ f b
⊢ a ≤ f c ∨ a ≤ t.sup f → ∃ b ∈ cons c t hc, a ≤ f b

Tactic:
exact fun
      | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
      | Or.inr h => let ⟨b, hb, hle⟩ := ih h; ⟨b, mem_cons.2 (Or.inr hb), hle⟩
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
mp : a ≤ sup ∅ f → ∃ (b : ι), Membership.mem (γ := Finset ι) ∅ b ∧ a ≤ f b
mp₁ :
  ∀ (c : ι) (t : Finset ι) (hc : c ∉ t) (ih : a ≤ t.sup f → ∃ b ∈ t, a ≤ f b),
    a ≤ (cons c t hc).sup f → ∃ b ∈ cons c t hc, a ≤ f b
⊢ a ≤ s.sup f → ∃ b ∈ s, a ≤ f b

Tactic:
induction s using cons_induction with
    | empty => exact (absurd · (not_le_of_gt ha))
    | cons c t hc ih =>
      rw [sup_cons, le_sup_iff]
      exact fun
      | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
      | Or.inr h => let ⟨b, hb, hle⟩ := ih h; ⟨b, mem_cons.2 (Or.inr hb), hle⟩

Premises used: Finset.cons, absurd, Finset.sup_cons, le_sup_iff, not_le_of_gt
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ (∃ b ∈ s, a ≤ f b) → a ≤ s.sup f

Tactic:
fun ⟨b, hb, hle⟩ => le_trans hle (le_sup hb)

Premises used: LE.le, Finset.sup, _private.0.Finset.le_sup_iff.match_3, Finset.le_sup, le_trans
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ (∃ b ∈ s, a ≤ f b) → a ≤ s.sup f

Tactic:
exact fun ⟨b, hb, hle⟩ => le_trans hle (le_sup hb)
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
ι : Type u_5
α : Type u_7
inst : LinearOrder α
inst_1 : BoundedOrder α
inst_2 : Nontrivial α
s : Finset ι
f : ι → α
simp : ⊤ ≤ s.sup f ↔ ∃ b ∈ s, ⊤ ≤ f b
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Tactic:
simp only [← top_le_iff]

Premises used: top_le_iff
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
ι : Type u_5
α : Type u_7
inst : LinearOrder α
inst_1 : BoundedOrder α
inst_2 : Nontrivial α
s : Finset ι
f : ι → α
⊢ ⊤ ≤ s.sup f ↔ ∃ b ∈ s, ⊤ ≤ f b

Tactic:
Finset.le_sup_iff bot_lt_top

Premises used: Finset.le_sup_iff, bot_lt_top
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
ι : Type u_5
α : Type u_7
inst : LinearOrder α
inst_1 : BoundedOrder α
inst_2 : Nontrivial α
s : Finset ι
f : ι → α
⊢ ⊤ ≤ s.sup f ↔ ∃ b ∈ s, ⊤ ≤ f b

Tactic:
exact Finset.le_sup_iff bot_lt_top

Premises used: Finset.le_sup_iff, bot_lt_top
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
ι : Type u_5
α : Type u_7
inst : LinearOrder α
inst_1 : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
inl : Subsingleton α → (s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤)
inr : Nontrivial α → (s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤)
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Tactic:
cases subsingleton_or_nontrivial α

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
ι : Type u_5
α : Type u_7
inst : LinearOrder α
inst_1 : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
h : Subsingleton α
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Tactic:
simpa [Subsingleton.elim _ (⊤ : α)]

Premises used: Subsingleton.elim, Top.top
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
ι : Type u_5
α : Type u_7
inst : LinearOrder α
inst_1 : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
h : Nontrivial α
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Tactic:
Finset.sup_eq_top_iff

Premises used: Finset.sup_eq_top_iff
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
ι : Type u_5
α : Type u_7
inst : LinearOrder α
inst_1 : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
h : Nontrivial α
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Tactic:
exact Finset.sup_eq_top_iff

Premises used: Finset.sup_eq_top_iff
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
mp : a < s.sup f → ∃ b ∈ s, a < f b
mpr : (∃ b ∈ s, a < f b) → a < s.sup f
⊢ a < s.sup f ↔ ∃ b ∈ s, a < f b

Tactic:
apply Iff.intro

Premises used: Iff.intro
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a < sup ∅ f → ∃ (b : ι), Membership.mem (γ := Finset ι) ∅ b ∧ a < f b

Tactic:
(absurd · not_lt_bot)

Premises used: not_lt_bot, absurd
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a < sup ∅ f → ∃ (b : ι), Membership.mem (γ := Finset ι) ∅ b ∧ a < f b

Tactic:
exact (absurd · not_lt_bot)

Premises used: not_lt_bot, absurd
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
c : ι
t : Finset ι
hc : c ∉ t
ih : a < t.sup f → ∃ b ∈ t, a < f b
mp : a < f c ∨ a < t.sup f → ∃ b ∈ cons c t hc, a < f b
⊢ a < (cons c t hc).sup f → ∃ b ∈ cons c t hc, a < f b

Tactic:
rw [sup_cons, lt_sup_iff]

Premises used: lt_sup_iff, Finset.sup_cons
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
c : ι
t : Finset ι
hc : c ∉ t
ih : a < t.sup f → ∃ b ∈ t, a < f b
⊢ a < f c ∨ a < t.sup f → ∃ b ∈ cons c t hc, a < f b

Tactic:
fun
      | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
      | Or.inr h => let ⟨b, hb, hlt⟩ := ih h; ⟨b, mem_cons.2 (Or.inr hb), hlt⟩

Premises used: Iff.mpr, _private.0.Finset.lt_sup_iff.match_2, Finset.cons, Membership.mem, Exists, _private.0.Finset.lt_sup_iff.match_1, And, And.intro, LT.lt, Exists.intro, Or.inl, Finset.mem_cons, Or.inr, rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
c : ι
t : Finset ι
hc : c ∉ t
ih : a < t.sup f → ∃ b ∈ t, a < f b
⊢ a < f c ∨ a < t.sup f → ∃ b ∈ cons c t hc, a < f b

Tactic:
exact fun
      | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
      | Or.inr h => let ⟨b, hb, hlt⟩ := ih h; ⟨b, mem_cons.2 (Or.inr hb), hlt⟩
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
mp : a < sup ∅ f → ∃ (b : ι), Membership.mem (γ := Finset ι) ∅ b ∧ a < f b
mp₁ :
  ∀ (c : ι) (t : Finset ι) (hc : c ∉ t) (ih : a < t.sup f → ∃ b ∈ t, a < f b),
    a < (cons c t hc).sup f → ∃ b ∈ cons c t hc, a < f b
⊢ a < s.sup f → ∃ b ∈ s, a < f b

Tactic:
induction s using cons_induction with
    | empty => exact (absurd · not_lt_bot)
    | cons c t hc ih =>
      rw [sup_cons, lt_sup_iff]
      exact fun
      | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
      | Or.inr h => let ⟨b, hb, hlt⟩ := ih h; ⟨b, mem_cons.2 (Or.inr hb), hlt⟩

Premises used: Finset.cons, not_lt_bot, lt_sup_iff, absurd, Finset.sup_cons
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ (∃ b ∈ s, a < f b) → a < s.sup f

Tactic:
fun ⟨b, hb, hlt⟩ => lt_of_lt_of_le hlt (le_sup hb)

Premises used: LT.lt, Finset.sup, _private.0.Finset.lt_sup_iff.match_3, lt_of_lt_of_le, Finset.le_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ (∃ b ∈ s, a < f b) → a < s.sup f

Tactic:
exact fun ⟨b, hb, hlt⟩ => lt_of_lt_of_le hlt (le_sup hb)
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : c ∉ t
⊢ ((∀ b ∈ t, f b < a) → t.sup f < a) → (∀ b ∈ cons c t hc, f b < a) → (cons c t hc).sup f < a

Tactic:
simpa only [sup_cons, sup_lt_iff, mem_cons, forall_eq_or_imp] using And.imp_right

Premises used: forall_eq_or_imp, sup_lt_iff, Finset.sup_cons, And.imp_right, Finset.mem_cons
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
hs : Finset.Nonempty.{u_5} (α := ι) ∅
⊢ sup ∅ f ∈ f '' (↑∅ : Set ι)

Tactic:
simp only [Finset.not_nonempty_empty] at hs

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

Tactic:
rw [Finset.sup_insert (b := a) (s := s) (f := f)]

Premises used: Finset.sup_insert
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s_1 : Finset ι
f : ι → α
a : ι
s : Finset ι
h_1 : a ∉ s
h : ∀ (hs : s.Nonempty), s.sup f ∈ f '' (↑s : Set ι)
hs_1 : (insert a s).Nonempty
hs : s = ∅
⊢ max (f a) (s.sup f) ∈ f '' (↑(insert a s) : Set ι)

Tactic:
simp [hs]
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s_1 : Finset ι
f : ι → α
a : ι
s : Finset ι
h_1 : a ∉ s
h : ∀ (hs : s.Nonempty), s.sup f ∈ f '' (↑s : Set ι)
hs_1 : (Insert.insert a s).Nonempty
hs : s.Nonempty
insert : max (f a) (s.sup f) ∈ f '' Insert.insert a (↑s : Set ι)
⊢ max (f a) (s.sup f) ∈ f '' (↑(Insert.insert a s) : Set ι)

Tactic:
simp only [Finset.coe_insert]

Premises used: Finset.coe_insert
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s_1 : Finset ι
f : ι → α
a : ι
s : Finset ι
h_1 : a ∉ s
h : ∀ (hs : s.Nonempty), s.sup f ∈ f '' (↑s : Set ι)
hs_1 : (Insert.insert a s).Nonempty
hs : s.Nonempty
insert : ∀ (ha : f a ≤ s.sup f), max (f a) (s.sup f) ∈ f '' Insert.insert a (↑s : Set ι)
insert₁ : ∀ (ha : s.sup f ≤ f a), max (f a) (s.sup f) ∈ f '' Insert.insert a (↑s : Set ι)
⊢ max (f a) (s.sup f) ∈ f '' Insert.insert a (↑s : Set ι)

Tactic:
rcases le_total (f a) (s.sup f) with (ha | ha)

Premises used: le_total, Finset.sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s_1 : Finset ι
f : ι → α
a : ι
s : Finset ι
h_1 : a ∉ s
h : ∀ (hs : s.Nonempty), s.sup f ∈ f '' (↑s : Set ι)
hs_1 : (Insert.insert a s).Nonempty
hs : s.Nonempty
ha : f a ≤ s.sup f
insert : s.sup f ∈ f '' Insert.insert a (↑s : Set ι)
⊢ max (f a) (s.sup f) ∈ f '' Insert.insert a (↑s : Set ι)

Tactic:
rw [sup_eq_right.mpr ha]

Premises used: Iff.mpr, sup_eq_right
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s_1 : Finset ι
f : ι → α
a : ι
s : Finset ι
h_1 : a ∉ s
h : ∀ (hs : s.Nonempty), s.sup f ∈ f '' (↑s : Set ι)
hs_1 : (insert a s).Nonempty
hs : s.Nonempty
ha : f a ≤ s.sup f
⊢ s.sup f ∈ f '' insert a (↑s : Set ι)

Tactic:
Set.image_mono (Set.subset_insert a s) (h hs)

Premises used: Set.image_mono, SetLike.coe, Set.subset_insert
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s_1 : Finset ι
f : ι → α
a : ι
s : Finset ι
h_1 : a ∉ s
h : ∀ (hs : s.Nonempty), s.sup f ∈ f '' (↑s : Set ι)
hs_1 : (insert a s).Nonempty
hs : s.Nonempty
ha : f a ≤ s.sup f
⊢ s.sup f ∈ f '' insert a (↑s : Set ι)

Tactic:
exact Set.image_mono (Set.subset_insert a s) (h hs)

Premises used: Set.image_mono, SetLike.coe, Set.subset_insert
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s_1 : Finset ι
f : ι → α
a : ι
s : Finset ι
h_1 : a ∉ s
h : ∀ (hs : s.Nonempty), s.sup f ∈ f '' (↑s : Set ι)
hs_1 : (Insert.insert a s).Nonempty
hs : s.Nonempty
ha : s.sup f ≤ f a
insert : f a ∈ f '' Insert.insert a (↑s : Set ι)
⊢ max (f a) (s.sup f) ∈ f '' Insert.insert a (↑s : Set ι)

Tactic:
rw [sup_eq_left.mpr ha]

Premises used: Iff.mpr, sup_eq_left
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s_1 : Finset ι
f : ι → α
a : ι
s : Finset ι
h_1 : a ∉ s
h : ∀ (hs : s.Nonempty), s.sup f ∈ f '' (↑s : Set ι)
hs_1 : (insert a s).Nonempty
hs : s.Nonempty
ha : s.sup f ≤ f a
⊢ f a ∈ f '' insert a (↑s : Set ι)

Tactic:
apply Set.mem_image_of_mem _ (Set.mem_insert a ↑s)

Premises used: SetLike.coe, Set.mem_image_of_mem, Set.mem_insert
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s_1 : Finset ι
f : ι → α
a : ι
s : Finset ι
h_1 : a ∉ s
h : ∀ (hs : s.Nonempty), s.sup f ∈ f '' (↑s : Set ι)
hs : (insert a s).Nonempty
⊢ s = ∅ ∨ s.Nonempty

Tactic:
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: le_total, SetLike.coe, Set.mem_image_of_mem, Set.mem_insert, Finset.sup, Finset.coe_insert, Finset.eq_empty_or_nonempty