awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a_1 : ι
⊢ (inf {a_1} fun (b : ι) ↦ a \ f b) = a \ sup {a_1} f
have singleton : (inf {a_1} fun (b : ι) ↦ a \ f b) = a \ f a_1
Tactic: rw [sup_singleton, inf_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ (inf {a_1} fun (b : ι) ↦ a \ f b) = a \ sup {a_1} f
have singleton₁ : a \ f a_1 = a \ f a_1
Tactic: rw [sup_singleton, inf_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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 a_1 s_1 h).inf fun (b : ι) ↦ a \ f b) = a \ (cons a_1 s_1 h).sup f
have cons : ((cons a_1 s_1 h).inf fun (b : ι) ↦ a \ f b) = a \ (f a_1 ⊔ s_1.sup f)
Tactic: rw [sup_cons, inf_cons, ih, sdiff_sup]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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)
⊢ ((Finset.cons a_1 s_1 h).inf fun (b : ι) ↦ a \ f b) = a \ (Finset.cons a_1 s_1 h).sup f
have cons₁ : (a \ f a_1 ⊓ s_1.inf fun (b : ι) ↦ a \ f b) = a \ (f a_1 ⊔ s_1.sup f)
Tactic: rw [sup_cons, inf_cons, ih, sdiff_sup]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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)
⊢ ((Finset.cons a_1 s_1 h).inf fun (b : ι) ↦ a \ f b) = a \ (Finset.cons a_1 s_1 h).sup f
have cons₂ : a \ f a_1 ⊓ a \ s_1.sup f = a \ (f a_1 ⊔ s_1.sup f)
Tactic: rw [sup_cons, inf_cons, ih, sdiff_sup]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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)
⊢ ((Finset.cons a_1 s_1 h).inf fun (b : ι) ↦ a \ f b) = a \ (Finset.cons a_1 s_1 h).sup f
have cons₃ : a \ f a_1 ⊓ a \ s_1.sup f = a \ f a_1 ⊓ a \ s_1.sup f
Tactic: rw [sup_cons, inf_cons, ih, sdiff_sup]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ (s.inf fun (b : ι) ↦ a \ f b) = a \ s.sup f
have singleton : ∀ (a_1 : ι), (inf {a_1} fun (b : ι) ↦ a \ f b) = a \ sup {a_1} 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]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ (s.inf fun (b : ι) ↦ a \ f b) = a \ s.sup f
have cons : ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s),
  s.Nonempty →
    ∀ (ih : (s.inf fun (b : ι) ↦ a \ f b) = a \ s.sup f),
      ((cons a_1 s h).inf fun (b : ι) ↦ a \ f b) = a \ (cons a_1 s h).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]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a_1 : ι
⊢ (inf {a_1} fun (b : ι) ↦ f b \ a) = inf {a_1} f \ a
have singleton : f a_1 \ a = inf {a_1} f \ a
Tactic: rw [inf_singleton, inf_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ (inf {a_1} fun (b : ι) ↦ f b \ a) = inf {a_1} f \ a
have singleton₁ : f a_1 \ a = f a_1 \ a
Tactic: rw [inf_singleton, inf_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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 a_1 s_1 h).inf fun (b : ι) ↦ f b \ a) = (cons a_1 s_1 h).inf f \ a
have cons : (f a_1 \ a ⊓ s_1.inf fun (b : ι) ↦ f b \ a) = (cons a_1 s_1 h).inf f \ a
Tactic: rw [inf_cons, inf_cons, ih, inf_sdiff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ ((Finset.cons a_1 s_1 h).inf fun (b : ι) ↦ f b \ a) = (Finset.cons a_1 s_1 h).inf f \ a
have cons₁ : (f a_1 \ a ⊓ s_1.inf fun (b : ι) ↦ f b \ a) = (f a_1 ⊓ s_1.inf f) \ a
Tactic: rw [inf_cons, inf_cons, ih, inf_sdiff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ ((Finset.cons a_1 s_1 h).inf fun (b : ι) ↦ f b \ a) = (Finset.cons a_1 s_1 h).inf f \ a
have cons₂ : f a_1 \ a ⊓ s_1.inf f \ a = (f a_1 ⊓ s_1.inf f) \ a
Tactic: rw [inf_cons, inf_cons, ih, inf_sdiff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ ((Finset.cons a_1 s_1 h).inf fun (b : ι) ↦ f b \ a) = (Finset.cons a_1 s_1 h).inf f \ a
have cons₃ : f a_1 \ a ⊓ s_1.inf f \ a = f a_1 \ a ⊓ s_1.inf f \ a
Tactic: rw [inf_cons, inf_cons, ih, inf_sdiff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ (s.inf fun (b : ι) ↦ f b \ a) = s.inf f \ a
have singleton : ∀ (a_1 : ι), (inf {a_1} fun (b : ι) ↦ f b \ a) = inf {a_1} 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]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ (s.inf fun (b : ι) ↦ f b \ a) = s.inf f \ a
have cons : ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s),
  s.Nonempty →
    ∀ (ih : (s.inf fun (b : ι) ↦ f b \ a) = s.inf f \ a),
      ((cons a_1 s h).inf fun (b : ι) ↦ f b \ a) = (cons a_1 s h).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]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ a ≤ s.sup f ↔ ∃ b ∈ s, a ≤ f b
have mp : a ≤ s.sup f → ∃ b ∈ s, a ≤ f b
Tactic: apply Iff.intro
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ a ≤ s.sup f ↔ ∃ b ∈ s, a ≤ f b
have mpr : (∃ b ∈ s, a ≤ f b) → a ≤ s.sup f
Tactic: apply Iff.intro
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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 ≤ (cons c t hc).sup f → ∃ b ∈ cons c t hc, a ≤ f b
have mp : a ≤ f c ∨ a ≤ t.sup f → ∃ b ∈ cons c t hc, a ≤ f b
Tactic: rw [sup_cons, le_sup_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ a ≤ s.sup f → ∃ b ∈ s, a ≤ f b
have mp : a ≤ sup ∅ f → ∃ (b : ι), Membership.mem (γ := Finset ι) ∅ b ∧ 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⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ a ≤ s.sup f → ∃ b ∈ s, a ≤ f b
have 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
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⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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 = ⊤
have simp : ⊤ ≤ s.sup f ↔ ∃ b ∈ s, ⊤ ≤ f b
Tactic: simp only [← top_le_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
ι : Type u_5
α : Type u_7
inst : LinearOrder α
inst_1 : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤
have inl : Subsingleton α → (s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤)
Tactic: cases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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 = ⊤)
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤
have inr : Nontrivial α → (s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤)
Tactic: cases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a < s.sup f ↔ ∃ b ∈ s, a < f b
have mp : a < s.sup f → ∃ b ∈ s, a < f b
Tactic: apply Iff.intro
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ a < s.sup f ↔ ∃ b ∈ s, a < f b
have mpr : (∃ b ∈ s, a < f b) → a < s.sup f
Tactic: apply Iff.intro
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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 < (cons c t hc).sup f → ∃ b ∈ cons c t hc, a < f b
have mp : a < f c ∨ a < t.sup f → ∃ b ∈ cons c t hc, a < f b
Tactic: rw [sup_cons, lt_sup_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a < s.sup f → ∃ b ∈ s, a < f b
have mp : a < sup ∅ f → ∃ (b : ι), Membership.mem (γ := Finset ι) ∅ b ∧ 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⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ a < s.sup f → ∃ b ∈ s, a < f b
have 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
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⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ (insert a s).sup f ∈ f '' (↑(insert a s) : Set ι)
have insert : max (f a) (s.sup f) ∈ f '' (↑(insert a s) : Set ι)
Tactic: rw [Finset.sup_insert (b := a) (s := s) (f := f)]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ max (f a) (s.sup f) ∈ f '' (↑(insert a s) : Set ι)
have insert : max (f a) (s.sup f) ∈ f '' insert a (↑s : Set ι)
Tactic: simp only [Finset.coe_insert]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ max (f a) (s.sup f) ∈ f '' insert a (↑s : Set ι)
have insert : ∀ (ha : f a ≤ s.sup f), max (f a) (s.sup f) ∈ f '' insert a (↑s : Set ι)
Tactic: rcases le_total (f a) (s.sup f) with (ha | ha)
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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 ι)
⊢ max (f a) (s.sup f) ∈ f '' Insert.insert a (↑s : Set ι)
have insert₁ : ∀ (ha : s.sup f ≤ f a), max (f a) (s.sup f) ∈ f '' Insert.insert a (↑s : Set ι)
Tactic: rcases le_total (f a) (s.sup f) with (ha | ha)
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ max (f a) (s.sup f) ∈ f '' insert a (↑s : Set ι)
have insert : s.sup f ∈ f '' insert a (↑s : Set ι)
Tactic: rw [sup_eq_right.mpr ha]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ max (f a) (s.sup f) ∈ f '' insert a (↑s : Set ι)
have insert : f a ∈ f '' insert a (↑s : Set ι)
Tactic: rw [sup_eq_left.mpr ha]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (hypothesis)
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
⊢ max (f a) (s.sup f) ∈ f '' (↑(insert a s) : Set ι)
have x : 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)
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ s.sup f ∈ f '' (↑s : Set ι)
have empty : ∀ (hs : Finset.Nonempty.{u_5} (α := ι) ∅), sup ∅ f ∈ f '' (↑∅ : 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)
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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 ι)
⊢ s.sup f ∈ f '' (↑s : Set ι)
have insert : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    ∀ (h : ∀ (hs : s.Nonempty), s.sup f ∈ f '' (↑s : Set ι)) (hs : (insert a s).Nonempty),
      (insert a s).sup f ∈ f '' (↑(insert a 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)
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ s.sup f ∈ f '' (↑s : Set ι)
have empty : ∀ (hs : Finset.Nonempty.{u_5} (α := ι) ∅), sup ∅ f ∈ f '' (↑∅ : 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)
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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 ι)
⊢ s.sup f ∈ f '' (↑s : Set ι)
have insert : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    ∀ (h : ∀ (hs : s.Nonempty), s.sup f ∈ f '' (↑s : Set ι)) (hs : (insert a s).Nonempty),
      (insert a s).sup f ∈ f '' (↑(insert a 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)
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
⊢ (↑(s.sup' H f) : WithBot α) = s.sup (WithBot.some ∘ f)
have rw : (↑((s.sup (WithBot.some ∘ f)).unbot sorry) : WithBot α) = s.sup (WithBot.some ∘ f)
Tactic: rw [sup', WithBot.coe_unbot]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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)
⊢ (↑(s.sup' H f) : WithBot α) = s.sup (WithBot.some ∘ f)
have rw₁ : s.sup (WithBot.some ∘ f) = s.sup (WithBot.some ∘ f)
Tactic: rw [sup', WithBot.coe_unbot]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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 = f b ⊔ s.sup' H f
have rw : (↑((cons b s hb).sup' sorry f) : WithBot α) = (↑(f b ⊔ s.sup' H f) : WithBot α)
Tactic: rw [← WithBot.coe_eq_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
inst_1 : DecidableEq β
b : β
⊢ (insert b s).sup' ⋯ f = f b ⊔ s.sup' H f
have rw : (↑((insert b s).sup' sorry f) : WithBot α) = (↑(f b ⊔ s.sup' H f) : WithBot α)
Tactic: rw [← WithBot.coe_eq_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
a : α
⊢ s.sup' H f ≤ a ↔ ∀ b ∈ s, f b ≤ a
have simp_rw : (∀ b ∈ s, (WithBot.some ∘ f) b ≤ (↑a : WithBot α)) ↔ ∀ b ∈ s, (↑(f b) : WithBot α) ≤ (↑a : WithBot α)
Tactic: simp_rw [← @WithBot.coe_le_coe α, coe_sup', Finset.sup_le_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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)
⊢ p (s.sup' H f)
have change : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p (↑(s.sup' H f) : WithBot α)
Tactic: change @WithBot.recBotCoe α (fun _ => Prop) True p ↑(s.sup' H f)
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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' H f) : WithBot α)
have rw : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p (s.sup (WithBot.some ∘ f))
Tactic: rw [coe_sup']