awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ ∃ x ∈ s, (insert a r).sup id ≤ x
have insert : ∀ (y : α) (hys : y ∈ s) (hay : a ≤ y), ∃ x ∈ s, (insert a r).sup id ≤ x
Tactic: obtain ⟨y, hys, hay⟩ := h a (Finset.mem_insert_self a r)
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ ∃ x ∈ s, (insert a r).sup id ≤ x
have insert : ∀ (z : α) (hzs : z ∈ s) (hxz : x ≤ z) (hyz : y ≤ z), ∃ x ∈ s, (insert a r).sup id ≤ x
Tactic: obtain ⟨z, hzs, ⟨hxz, hyz⟩⟩ := hdir x hxs y hys
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ ∃ x ∈ s, (insert a r).sup id ≤ x
have right : (insert a r).sup id ≤ z
Tactic: use z, hzs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ (insert a r).sup id ≤ z
have right : a ≤ z ∧ r.sup id ≤ z
Tactic: rw [sup_insert, id, sup_le_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_7
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
t : Finset α
⊢ (∀ x ∈ t, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, t.sup id ≤ x
have empty : (∀ (x : α), Membership.mem (γ := Finset α) ∅ x → ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, 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⟩
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ (∀ x ∈ t, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, t.sup id ≤ x
have insert : ∀ (a : α) (r : Finset α),
  a ∉ r →
    ∀ (ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x),
      (∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, (insert a r).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⟩
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_7
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
t : Finset α
⊢ (∀ x ∈ t, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, t.sup id ≤ x
have empty : (∀ (x : α), Membership.mem (γ := Finset α) ∅ x → ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, 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⟩
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ (∀ x ∈ t, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, t.sup id ≤ x
have insert : ∀ (a : α) (r : Finset α),
  a ∉ r →
    ∀ (ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x),
      (∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, (insert a r).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⟩
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
f : β → α
S : Finset β
⊢ S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥
have empty : sup ∅ f = ⊥ ↔ ∀ (s : β), Membership.mem (γ := Finset β) ∅ s → f s = ⊥
Tactic: induction S using Finset.induction
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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 = ⊥
⊢ S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥
have insert : ∀ (a : β) (s : Finset β),
  a ∉ s → (s.sup f = ⊥ ↔ ∀ s_1 ∈ s, f s_1 = ⊥) → ((insert a s).sup f = ⊥ ↔ ∀ s_1 ∈ insert a s, f s_1 = ⊥)
Tactic: induction S using Finset.induction
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
f : β → α
S : Finset β
⊢ S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥
have empty : sup ∅ f = ⊥ ↔ ∀ (s : β), Membership.mem (γ := Finset β) ∅ s → f s = ⊥
Tactic: classical induction S using Finset.induction <;> simp [*]
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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 = ⊥
⊢ S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥
have insert : ∀ (a : β) (s : Finset β),
  a ∉ s → (s.sup f = ⊥ ↔ ∀ s_1 ∈ s, f s_1 = ⊥) → ((insert a s).sup f = ⊥ ↔ ∀ s_1 ∈ insert a s, f s_1 = ⊥)
Tactic: classical induction S using Finset.induction <;> simp [*]
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : IsEmpty β
f : β → α
S : Finset β
⊢ S.sup f = ⊥
have rw : ∀ s ∈ S, f s = ⊥
Tactic: rw [Finset.sup_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice β
s : Finset α
f : α → β
⊢ s.sup f = sSup (f '' (↑s : Set α))
have rw : s.sup f = sSup (↑(image f s) : Set β)
Tactic: rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.id_comp]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice β
s : Finset α
f : α → β
rw : s.sup f = sSup (↑(image f s) : Set β)
⊢ s.sup f = sSup (f '' (↑s : Set α))
have rw₁ : s.sup f = (image f s).sup id
Tactic: rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.id_comp]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ s.sup f = sSup (f '' (↑s : Set α))
have rw₂ : s.sup f = s.sup (id ∘ f)
Tactic: rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.id_comp]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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)
⊢ s.sup f = sSup (f '' (↑s : Set α))
have rw₃ : s.sup f = s.sup f
Tactic: rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.id_comp]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice β
s : Finset α
f : α → β
⊢ s.sup f = sSup (f '' (↑s : Set α))
have classical : s.sup f = sSup (↑(image f s) : Set β)
Tactic: classical rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.id_comp]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice β
s : Finset α
f : α → β
classical : s.sup f = sSup (↑(image f s) : Set β)
⊢ s.sup f = sSup (f '' (↑s : Set α))
have classical₁ : s.sup f = (image f s).sup id
Tactic: classical rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.id_comp]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ s.sup f = sSup (f '' (↑s : Set α))
have classical₂ : s.sup f = s.sup (id ∘ f)
Tactic: classical rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.id_comp]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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)
⊢ s.sup f = sSup (f '' (↑s : Set α))
have classical₃ : s.sup f = s.sup f
Tactic: classical rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.id_comp]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup β
inst_1 : OrderBot β
inst_2 : WellFoundedGT β
f : α → β
⊢ ∃ (t : Finset α), ∀ (a : α), f a ≤ t.sup f
have inl : IsEmpty α → ∃ (t : Finset α), ∀ (a : α), f a ≤ t.sup f
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ ∃ (t : Finset α), ∀ (a : α), f a ≤ t.sup f
have inr : Nonempty α → ∃ (t : Finset α), ∀ (a : α), f a ≤ t.sup f
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup β
inst_1 : OrderBot β
inst_2 : WellFoundedGT β
f : α → β
h : Nonempty α
⊢ ∃ (t : Finset α), ∀ (a : α), f a ≤ t.sup f
have 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
Tactic: obtain ⟨_, ⟨t, rfl⟩, ht⟩ := wellFounded_gt.has_min _ (Set.range_nonempty (sup · f))
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
have inr : ∀ (a : α), f a ≤ t.sup f
Tactic: refine ⟨t, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (hypothesis)
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 : α
⊢ f a ≤ t.sup f
have this : ¬(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⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ f a ≤ t.sup f
have inr : ∀ (this : ¬¬f a ≤ (fun (x : Finset α) ↦ x.sup f) t), f a ≤ t.sup f
Tactic: rwa [right_lt_sup, not_not] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ f a ≤ t.sup f
have inr₁ : ∀ (this : f a ≤ (fun (x : Finset α) ↦ x.sup f) t), f a ≤ t.sup f
Tactic: rwa [right_lt_sup, not_not] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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 : α
⊢ f a ≤ t.sup f
have inr : ∀ (this : ¬(fun (x : Finset α) ↦ x.sup f) t < 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
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
inst_1 : OrderBot α
f : ι → α
a : α
⊢ a ⊓ sup ∅ f = sup ∅ fun (i : ι) ↦ a ⊓ f i
have empty : a ⊓ ⊥ = ⊥
Tactic: simp_rw [Finset.sup_empty, inf_bot_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ a ⊓ (cons a_1 s h_1).sup f = (cons a_1 s h_1).sup fun (i : ι) ↦ a ⊓ f i
have cons : a ⊓ (f a_1 ⊔ s.sup f) = (cons a_1 s h_1).sup fun (i : ι) ↦ a ⊓ f i
Tactic: rw [sup_cons, sup_cons, inf_sup_left, h]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ a ⊓ (Finset.cons a_1 s h_1).sup f = (Finset.cons a_1 s h_1).sup fun (i : ι) ↦ a ⊓ f i
have cons₁ : a ⊓ (f a_1 ⊔ s.sup f) = a ⊓ f a_1 ⊔ s.sup fun (i : ι) ↦ a ⊓ f i
Tactic: rw [sup_cons, sup_cons, inf_sup_left, h]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ a ⊓ (Finset.cons a_1 s h_1).sup f = (Finset.cons a_1 s h_1).sup fun (i : ι) ↦ a ⊓ f i
have cons₂ : a ⊓ f a_1 ⊔ a ⊓ s.sup f = a ⊓ f a_1 ⊔ s.sup fun (i : ι) ↦ a ⊓ f i
Tactic: rw [sup_cons, sup_cons, inf_sup_left, h]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ a ⊓ (Finset.cons a_1 s h_1).sup f = (Finset.cons a_1 s h_1).sup fun (i : ι) ↦ a ⊓ f i
have cons₃ : (a ⊓ f a_1 ⊔ s.sup fun (i : ι) ↦ a ⊓ f i) = a ⊓ f a_1 ⊔ s.sup fun (i : ι) ↦ a ⊓ f i
Tactic: rw [sup_cons, sup_cons, inf_sup_left, h]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a ⊓ s.sup f = s.sup fun (i : ι) ↦ a ⊓ f i
have empty : a ⊓ sup ∅ f = 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ a ⊓ s.sup f = s.sup fun (i : ι) ↦ a ⊓ f i
have cons : ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s) (h_1 : a ⊓ s.sup f = s.sup fun (i : ι) ↦ a ⊓ f i),
  a ⊓ (cons a_1 s h).sup f = (cons a_1 s h).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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ s.sup f ⊓ a = s.sup fun (i : ι) ↦ f i ⊓ a
have rw : Eq.{u_2 + 1} (α := α) (s.sup fun (i : ι) ↦ a ⊓ f i) (s.sup fun (i : ι) ↦ f i ⊓ a)
Tactic: rw [_root_.inf_comm, s.sup_inf_distrib_left]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
f : ι → α
a : α
⊢ (sup ∅ fun (b : ι) ↦ a \ f b) = a \ inf ∅ f
have empty : ⊥ = a \ inf ∅ f
Tactic: rw [sup_empty, inf_empty, sdiff_top]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
f : ι → α
a : α
empty : ⊥ = a \ inf ∅ f
⊢ (sup ∅ fun (b : ι) ↦ a \ f b) = a \ inf ∅ f
have empty₁ : ⊥ = a \ ⊤
Tactic: rw [sup_empty, inf_empty, sdiff_top]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
f : ι → α
a : α
empty : ⊥ = a \ inf ∅ f
empty₁ : ⊥ = a \ ⊤
⊢ (sup ∅ fun (b : ι) ↦ a \ f b) = a \ inf ∅ f
have empty₂ : Eq.{u_2 + 1} (α := α) ⊥ ⊥
Tactic: rw [sup_empty, inf_empty, sdiff_top]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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_1 s h_1).sup fun (b : ι) ↦ a \ f b) = a \ (cons a_1 s h_1).inf f
have cons : (a \ f a_1 ⊔ s.sup fun (b : ι) ↦ a \ f b) = a \ (cons a_1 s h_1).inf f
Tactic: rw [sup_cons, inf_cons, h, sdiff_inf]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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
⊢ ((Finset.cons a_1 s h_1).sup fun (b : ι) ↦ a \ f b) = a \ (Finset.cons a_1 s h_1).inf f
have cons₁ : (a \ f a_1 ⊔ s.sup fun (b : ι) ↦ a \ f b) = a \ (f a_1 ⊓ s.inf f)
Tactic: rw [sup_cons, inf_cons, h, sdiff_inf]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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)
⊢ ((Finset.cons a_1 s h_1).sup fun (b : ι) ↦ a \ f b) = a \ (Finset.cons a_1 s h_1).inf f
have cons₂ : a \ f a_1 ⊔ a \ s.inf f = a \ (f a_1 ⊓ s.inf f)
Tactic: rw [sup_cons, inf_cons, h, sdiff_inf]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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)
⊢ ((Finset.cons a_1 s h_1).sup fun (b : ι) ↦ a \ f b) = a \ (Finset.cons a_1 s h_1).inf f
have cons₃ : a \ f a_1 ⊔ a \ s.inf f = a \ f a_1 ⊔ a \ s.inf f
Tactic: rw [sup_cons, inf_cons, h, sdiff_inf]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
⊢ (s.sup fun (b : ι) ↦ a \ f b) = a \ s.inf f
have empty : (sup ∅ fun (b : ι) ↦ a \ f b) = a \ 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
empty : (sup ∅ fun (b : ι) ↦ a \ f b) = a \ inf ∅ f
⊢ (s.sup fun (b : ι) ↦ a \ f b) = a \ s.inf f
have cons : ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s) (h_1 : (s.sup fun (b : ι) ↦ a \ f b) = a \ s.inf f),
  ((cons a_1 s h).sup fun (b : ι) ↦ a \ f b) = a \ (cons a_1 s h).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]
Cleared hypotheses: s