awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s = s ∪ t ↔ t ⊆ s
have rw : s ∪ t = s ↔ t ⊆ s
Tactic: rw [eq_comm, union_eq_left]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
rw : s ∪ t = s ↔ t ⊆ s
⊢ s = s ∪ t ↔ t ⊆ s
have rw₁ : t ⊆ s ↔ t ⊆ s
Tactic: rw [eq_comm, union_eq_left]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s = t ∪ s ↔ t ⊆ s
have rw : t ∪ s = s ↔ t ⊆ s
Tactic: rw [eq_comm, union_eq_right]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
rw : t ∪ s = s ↔ t ⊆ s
⊢ s = t ∪ s ↔ t ⊆ s
have rw₁ : t ⊆ s ↔ t ⊆ s
Tactic: rw [eq_comm, union_eq_right]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ∩ (t ∪ s) = s
have rw : (t ∪ s) ∩ s = s
Tactic: rw [inter_comm, union_inter_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
rw : (t ∪ s) ∩ s = s
⊢ s ∩ (t ∪ s) = s
have rw₁ : s = s
Tactic: rw [inter_comm, union_inter_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f g : β → α
⊢ sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ g
have empty : ⊥ = sup ∅ f ⊔ sup ∅ g
Tactic: rw [sup_empty, sup_empty, sup_empty, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f g : β → α
empty : ⊥ = sup ∅ f ⊔ sup ∅ g
⊢ sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ g
have empty₁ : ⊥ = ⊥ ⊔ sup ∅ g
Tactic: rw [sup_empty, sup_empty, sup_empty, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f g : β → α
empty : ⊥ = sup ∅ f ⊔ sup ∅ g
empty₁ : ⊥ = ⊥ ⊔ sup ∅ g
⊢ sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ g
have empty₂ : Eq.{u_2 + 1} (α := α) ⊥ (⊥ ⊔ ⊥)
Tactic: rw [sup_empty, sup_empty, sup_empty, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f g : β → α
empty : ⊥ = sup ∅ f ⊔ sup ∅ g
empty₁ : ⊥ = ⊥ ⊔ sup ∅ g
empty₂ : Eq.{u_2 + 1} (α := α) ⊥ (⊥ ⊔ ⊥)
⊢ sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ g
have empty₃ : Eq.{u_2 + 1} (α := α) ⊥ ⊥
Tactic: rw [sup_empty, sup_empty, sup_empty, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f g : β → α
a : β
s_1 : Finset β
h : a ∉ s_1
ih : s_1.sup (f ⊔ g) = s_1.sup f ⊔ s_1.sup g
⊢ (cons a s_1 h).sup (f ⊔ g) = (cons a s_1 h).sup f ⊔ (cons a s_1 h).sup g
have cons : (f ⊔ g) a ⊔ (s_1.sup f ⊔ s_1.sup g) = f a ⊔ s_1.sup f ⊔ (g a ⊔ s_1.sup g)
Tactic: rw [sup_cons, sup_cons, sup_cons, ih]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f g : β → α
⊢ s.sup (f ⊔ g) = s.sup f ⊔ s.sup g
have empty : sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ g
Tactic: induction s using Finset.cons_induction with
  | empty => rw [sup_empty, sup_empty, sup_empty, bot_sup_eq]
  | cons _ _ _ ih =>
    rw [sup_cons, sup_cons, sup_cons, ih]
    exact sup_sup_sup_comm _ _ _ _
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f g : β → α
empty : sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ g
⊢ s.sup (f ⊔ g) = s.sup f ⊔ s.sup g
have cons : ∀ (a : β) (s : Finset β) (h : a ∉ s) (ih : s.sup (f ⊔ g) = s.sup f ⊔ s.sup g),
  (cons a s h).sup (f ⊔ g) = (cons a s h).sup f ⊔ (cons a s h).sup g
Tactic: induction s using Finset.cons_induction with
  | empty => rw [sup_empty, sup_empty, sup_empty, bot_sup_eq]
  | cons _ _ _ ih =>
    rw [sup_cons, sup_cons, sup_cons, ih]
    exact sup_sup_sup_comm _ _ _ _
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s₁ s₂ : Finset β
f g : β → α
hs : s₁ = s₂
hfg : ∀ a ∈ s₂, f a = g a
⊢ s₁.sup f = s₂.sup g
have subst : ∀ (hfg : ∀ a ∈ s₁, f a = g a), s₁.sup f = s₁.sup g
Tactic: subst hs
Cleared hypotheses: s₂, hs, hfg
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
inst_4 : FunLike F α β
inst_5 : SupBotHomClass F α β
f : F
s_1 : Finset ι
g : ι → α
i : ι
s : Finset ι
h_1 : i ∉ s
h : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (s.sup g) : β) (s.sup ((⇑f : (a : α) → β) ∘ g) : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ((cons i s h_1).sup g) : β) ((cons i s h_1).sup ((⇑f : (a : α) → β) ∘ g) : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i ⊔ s.sup g) : β) ((cons i s h_1).sup ((⇑f : (a : α) → β) ∘ g) : β)
Tactic: rw [sup_cons, sup_cons, map_sup, h, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
inst_4 : FunLike F α β
inst_5 : SupBotHomClass F α β
f : F
s_1 : Finset ι
g : ι → α
i : ι
s : Finset ι
h_1 : i ∉ s
h : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (s.sup g) : β) (s.sup ((⇑f : (a : α) → β) ∘ g) : β)
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i ⊔ s.sup g) : β) ((cons i s h_1).sup ((⇑f : (a : α) → β) ∘ g) : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ((cons i s h_1).sup g) : β) ((cons i s h_1).sup ((⇑f : (a : α) → β) ∘ g) : β)
have rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i ⊔ s.sup g) : β)
  (((⇑f : (a : α) → β) ∘ g) i ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
Tactic: rw [sup_cons, sup_cons, map_sup, h, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
inst_4 : FunLike F α β
inst_5 : SupBotHomClass F α β
f : F
s_1 : Finset ι
g : ι → α
i : ι
s : Finset ι
h_1 : i ∉ s
h : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (s.sup g) : β) (s.sup ((⇑f : (a : α) → β) ∘ g) : β)
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i ⊔ s.sup g) : β) ((cons i s h_1).sup ((⇑f : (a : α) → β) ∘ g) : β)
rw₁ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i ⊔ s.sup g) : β)
    (((⇑f : (a : α) → β) ∘ g) i ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ((cons i s h_1).sup g) : β) ((cons i s h_1).sup ((⇑f : (a : α) → β) ∘ g) : β)
have rw₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i) ⊔ (f : (a : α) → β) (s.sup g) : β)
  (((⇑f : (a : α) → β) ∘ g) i ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
Tactic: rw [sup_cons, sup_cons, map_sup, h, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
inst_4 : FunLike F α β
inst_5 : SupBotHomClass F α β
f : F
s_1 : Finset ι
g : ι → α
i : ι
s : Finset ι
h_1 : i ∉ s
h : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (s.sup g) : β) (s.sup ((⇑f : (a : α) → β) ∘ g) : β)
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i ⊔ s.sup g) : β) ((cons i s h_1).sup ((⇑f : (a : α) → β) ∘ g) : β)
rw₁ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i ⊔ s.sup g) : β)
    (((⇑f : (a : α) → β) ∘ g) i ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
rw₂ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i) ⊔ (f : (a : α) → β) (s.sup g) : β)
    (((⇑f : (a : α) → β) ∘ g) i ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ((cons i s h_1).sup g) : β) ((cons i s h_1).sup ((⇑f : (a : α) → β) ∘ g) : β)
have rw₃ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i) ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
  (((⇑f : (a : α) → β) ∘ g) i ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
Tactic: rw [sup_cons, sup_cons, map_sup, h, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
inst_4 : FunLike F α β
inst_5 : SupBotHomClass F α β
f : F
s_1 : Finset ι
g : ι → α
i : ι
s : Finset ι
h_1 : i ∉ s
h : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (s.sup g) : β) (s.sup ((⇑f : (a : α) → β) ∘ g) : β)
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i ⊔ s.sup g) : β) ((cons i s h_1).sup ((⇑f : (a : α) → β) ∘ g) : β)
rw₁ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i ⊔ s.sup g) : β)
    (((⇑f : (a : α) → β) ∘ g) i ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
rw₂ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i) ⊔ (f : (a : α) → β) (s.sup g) : β)
    (((⇑f : (a : α) → β) ∘ g) i ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
rw₃ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i) ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
    (((⇑f : (a : α) → β) ∘ g) i ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ((cons i s h_1).sup g) : β) ((cons i s h_1).sup ((⇑f : (a : α) → β) ∘ g) : β)
have rw₄ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (g i) ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
  ((f : (a : α) → β) (g i) ⊔ s.sup ((⇑f : (a : α) → β) ∘ g) : β)
Tactic: rw [sup_cons, sup_cons, map_sup, h, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f : β → α
a : α
⊢ s.sup f ≤ a ↔ ∀ b ∈ s, f b ≤ a
have apply : (∀ b ∈ Multiset.map f s.val, b ≤ a) ↔ ∀ b ∈ s, f b ≤ a
Tactic: apply Iff.trans Multiset.sup_le
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
f : β → α
a : α
⊢ (∀ b ∈ Multiset.map f s.val, b ≤ a) ↔ ∀ b ∈ s, f b ≤ a
have simp : (∀ (b : α), ∀ x ∈ s.val, f x = b → b ≤ a) ↔ ∀ b ∈ s, f b ≤ a
Tactic: simp only [Multiset.mem_map, and_imp, exists_imp]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
⊢ Eq.{u_2 + 1} (α := α) (s.sup fun (x : β) ↦ ⊥) ⊥
have inl : Eq.{u_2 + 1} (α := α) (sup ∅ fun (x : β) ↦ ⊥) ⊥
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
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 α
s : Finset β
inl : Eq.{u_2 + 1} (α := α) (sup ∅ fun (x : β) ↦ ⊥) ⊥
⊢ Eq.{u_2 + 1} (α := α) (s.sup fun (x : β) ↦ ⊥) ⊥
have inr : ∀ (hs : s.Nonempty), Eq.{u_2 + 1} (α := α) (s.sup fun (x : β) ↦ ⊥) ⊥
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
s : Finset α
⊢ (s.erase ⊥).sup id = s.sup id
have refine : ∀ (a : α) (ha : a ∈ s), id a ≤ (s.erase ⊥).sup id
Tactic: refine (sup_mono (s.erase_subset _)).antisymm (Finset.sup_le_iff.2 fun a ha => ?_)
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ id a ≤ (s.erase ⊥).sup id
have inl : ∀ (ha : ⊥ ∈ s), id ⊥ ≤ (s.erase ⊥).sup id
Tactic: obtain rfl | ha' := eq_or_ne a ⊥
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
inl : ∀ (ha : ⊥ ∈ s), id ⊥ ≤ (s.erase ⊥).sup id
⊢ id a ≤ (s.erase ⊥).sup id
have inr : ∀ (ha' : a ≠ ⊥), id a ≤ (s.erase ⊥).sup id
Tactic: obtain rfl | ha' := eq_or_ne a ⊥
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_7
β : Type u_8
inst : GeneralizedBooleanAlgebra α
f : β → α
a : α
⊢ (sup ∅ fun (b : β) ↦ f b \ a) = sup ∅ f \ a
have empty : ⊥ = sup ∅ f \ a
Tactic: rw [sup_empty, sup_empty, bot_sdiff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_7
β : Type u_8
inst : GeneralizedBooleanAlgebra α
f : β → α
a : α
empty : ⊥ = sup ∅ f \ a
⊢ (sup ∅ fun (b : β) ↦ f b \ a) = sup ∅ f \ a
have empty₁ : ⊥ = ⊥ \ a
Tactic: rw [sup_empty, sup_empty, bot_sdiff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_7
β : Type u_8
inst : GeneralizedBooleanAlgebra α
f : β → α
a : α
empty : ⊥ = sup ∅ f \ a
empty₁ : ⊥ = ⊥ \ a
⊢ (sup ∅ fun (b : β) ↦ f b \ a) = sup ∅ f \ a
have empty₂ : Eq.{u_7 + 1} (α := α) ⊥ ⊥
Tactic: rw [sup_empty, sup_empty, bot_sdiff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_7
β : Type u_8
inst : GeneralizedBooleanAlgebra α
f : β → α
a : α
a_1 : β
s : Finset β
h_1 : a_1 ∉ s
h : (s.sup fun (b : β) ↦ f b \ a) = s.sup f \ a
⊢ ((cons a_1 s h_1).sup fun (b : β) ↦ f b \ a) = (cons a_1 s h_1).sup f \ a
have cons : (f a_1 \ a ⊔ s.sup fun (b : β) ↦ f b \ a) = (cons a_1 s h_1).sup f \ a
Tactic: rw [sup_cons, sup_cons, h, sup_sdiff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_7
β : Type u_8
inst : GeneralizedBooleanAlgebra α
f : β → α
a : α
a_1 : β
s : Finset β
h_1 : a_1 ∉ s
h : (s.sup fun (b : β) ↦ f b \ a) = s.sup f \ a
cons : (f a_1 \ a ⊔ s.sup fun (b : β) ↦ f b \ a) = (Finset.cons a_1 s h_1).sup f \ a
⊢ ((Finset.cons a_1 s h_1).sup fun (b : β) ↦ f b \ a) = (Finset.cons a_1 s h_1).sup f \ a
have cons₁ : (f a_1 \ a ⊔ s.sup fun (b : β) ↦ f b \ a) = (f a_1 ⊔ s.sup f) \ a
Tactic: rw [sup_cons, sup_cons, h, sup_sdiff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_7
β : Type u_8
inst : GeneralizedBooleanAlgebra α
f : β → α
a : α
a_1 : β
s : Finset β
h_1 : a_1 ∉ s
h : (s.sup fun (b : β) ↦ f b \ a) = s.sup f \ a
cons : (f a_1 \ a ⊔ s.sup fun (b : β) ↦ f b \ a) = (Finset.cons a_1 s h_1).sup f \ a
cons₁ : (f a_1 \ a ⊔ s.sup fun (b : β) ↦ f b \ a) = (f a_1 ⊔ s.sup f) \ a
⊢ ((Finset.cons a_1 s h_1).sup fun (b : β) ↦ f b \ a) = (Finset.cons a_1 s h_1).sup f \ a
have cons₂ : f a_1 \ a ⊔ s.sup f \ a = (f a_1 ⊔ s.sup f) \ a
Tactic: rw [sup_cons, sup_cons, h, sup_sdiff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_7
β : Type u_8
inst : GeneralizedBooleanAlgebra α
f : β → α
a : α
a_1 : β
s : Finset β
h_1 : a_1 ∉ s
h : (s.sup fun (b : β) ↦ f b \ a) = s.sup f \ a
cons : (f a_1 \ a ⊔ s.sup fun (b : β) ↦ f b \ a) = (Finset.cons a_1 s h_1).sup f \ a
cons₁ : (f a_1 \ a ⊔ s.sup fun (b : β) ↦ f b \ a) = (f a_1 ⊔ s.sup f) \ a
cons₂ : f a_1 \ a ⊔ s.sup f \ a = (f a_1 ⊔ s.sup f) \ a
⊢ ((Finset.cons a_1 s h_1).sup fun (b : β) ↦ f b \ a) = (Finset.cons a_1 s h_1).sup f \ a
have cons₃ : f a_1 \ a ⊔ s.sup f \ a = f a_1 \ a ⊔ s.sup f \ a
Tactic: rw [sup_cons, sup_cons, h, sup_sdiff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_7
β : Type u_8
inst : GeneralizedBooleanAlgebra α
s : Finset β
f : β → α
a : α
⊢ (s.sup fun (b : β) ↦ f b \ a) = s.sup f \ a
have empty : (sup ∅ fun (b : β) ↦ f b \ a) = sup ∅ f \ a
Tactic: induction s using Finset.cons_induction with
  | empty => rw [sup_empty, sup_empty, bot_sdiff]
  | cons _ _ _ h => rw [sup_cons, sup_cons, h, sup_sdiff]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_7
β : Type u_8
inst : GeneralizedBooleanAlgebra α
s : Finset β
f : β → α
a : α
empty : (sup ∅ fun (b : β) ↦ f b \ a) = sup ∅ f \ a
⊢ (s.sup fun (b : β) ↦ f b \ a) = s.sup f \ a
have cons : ∀ (a_1 : β) (s : Finset β) (h : a_1 ∉ s) (h_1 : (s.sup fun (b : β) ↦ f b \ a) = s.sup f \ a),
  ((cons a_1 s h).sup fun (b : β) ↦ f b \ a) = (cons a_1 s h).sup f \ a
Tactic: induction s using Finset.cons_induction with
  | empty => rw [sup_empty, sup_empty, bot_sdiff]
  | cons _ _ _ h => rw [sup_cons, sup_cons, h, sup_sdiff]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : SemilatticeSup γ
inst_3 : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
⊢ g ((cons c t hc).sup f) = (cons c t hc).sup (g ∘ f)
have rw : g (f c ⊔ t.sup f) = (cons c t hc).sup (g ∘ f)
Tactic: rw [sup_cons, sup_cons, g_sup, ih, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : SemilatticeSup γ
inst_3 : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
rw : g (f c ⊔ t.sup f) = (cons c t hc).sup (g ∘ f)
⊢ g ((cons c t hc).sup f) = (cons c t hc).sup (g ∘ f)
have rw₁ : g (f c ⊔ t.sup f) = (g ∘ f) c ⊔ t.sup (g ∘ f)
Tactic: rw [sup_cons, sup_cons, g_sup, ih, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : SemilatticeSup γ
inst_3 : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
rw : g (f c ⊔ t.sup f) = (cons c t hc).sup (g ∘ f)
rw₁ : g (f c ⊔ t.sup f) = (g ∘ f) c ⊔ t.sup (g ∘ f)
⊢ g ((cons c t hc).sup f) = (cons c t hc).sup (g ∘ f)
have rw₂ : g (f c) ⊔ g (t.sup f) = (g ∘ f) c ⊔ t.sup (g ∘ f)
Tactic: rw [sup_cons, sup_cons, g_sup, ih, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : SemilatticeSup γ
inst_3 : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
rw : g (f c ⊔ t.sup f) = (cons c t hc).sup (g ∘ f)
rw₁ : g (f c ⊔ t.sup f) = (g ∘ f) c ⊔ t.sup (g ∘ f)
rw₂ : g (f c) ⊔ g (t.sup f) = (g ∘ f) c ⊔ t.sup (g ∘ f)
⊢ g ((cons c t hc).sup f) = (cons c t hc).sup (g ∘ f)
have rw₃ : g (f c) ⊔ t.sup (g ∘ f) = (g ∘ f) c ⊔ t.sup (g ∘ f)
Tactic: rw [sup_cons, sup_cons, g_sup, ih, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : SemilatticeSup γ
inst_3 : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
rw : g (f c ⊔ t.sup f) = (cons c t hc).sup (g ∘ f)
rw₁ : g (f c ⊔ t.sup f) = (g ∘ f) c ⊔ t.sup (g ∘ f)
rw₂ : g (f c) ⊔ g (t.sup f) = (g ∘ f) c ⊔ t.sup (g ∘ f)
rw₃ : g (f c) ⊔ t.sup (g ∘ f) = (g ∘ f) c ⊔ t.sup (g ∘ f)
⊢ g ((cons c t hc).sup f) = (cons c t hc).sup (g ∘ f)
have rw₄ : g (f c) ⊔ t.sup (g ∘ f) = g (f c) ⊔ t.sup (g ∘ f)
Tactic: rw [sup_cons, sup_cons, g_sup, ih, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x : α // P x }
this_1 : SemilatticeSup { x : α // P x } := Subtype.semilatticeSup (P := P) Psup
this : OrderBot { x : α // P x } := Subtype.orderBot (p := P) Pbot
⊢ (↑(t.sup f) : α) = t.sup fun (x : β) ↦ (↑(f x) : α)
have g_sup : ∀ (x y : { x : α // P x }), (↑(x ⊔ y) : α) = (↑x : α) ⊔ (↑y : α)
Tactic: apply comp_sup_eq_sup_comp Subtype.val
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x : α // P x }
this_1 : SemilatticeSup { x : α // P x } := Subtype.semilatticeSup (P := P) Psup
this : OrderBot { x : α // P x } := Subtype.orderBot (p := P) Pbot
g_sup : ∀ (x y : { x : α // P x }), (↑(x ⊔ y) : α) = (↑x : α) ⊔ (↑y : α)
⊢ (↑(t.sup f) : α) = t.sup fun (x : β) ↦ (↑(f x) : α)
have bot : Eq.{u_2 + 1} (α := α) (↑⊥ : α) ⊥
Tactic: apply comp_sup_eq_sup_comp Subtype.val
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq α
l : List α
⊢ List.foldr (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊥ l = l.toFinset.sup id
have rw : Multiset.fold (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊥ (↑l : Multiset α).dedup = (↑l : Multiset α).dedup.sup
Tactic: rw [← coe_fold_r, ← Multiset.fold_dedup_idem, sup_def, ← List.toFinset_coe, toFinset_val,
    Multiset.map_id]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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 : ∀ b ∈ cons a s_1 h, p (f b)
⊢ p ((cons a s_1 h).sup f)
have cons : ∀ (hs : p (f a) ∧ ∀ x ∈ s_1, p (f x)), p (f a ⊔ s_1.sup f)
Tactic: simp only [sup_cons, forall_mem_cons] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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)
⊢ p (s.sup f)
have empty : ∀ (hs : ∀ (b : β), Membership.mem (γ := Finset β) ∅ b → p (f b)), p (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)
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
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)
⊢ p (s.sup f)
have cons : ∀ (a : β) (s : Finset β) (h : a ∉ s) (ih : ∀ (hs : ∀ b ∈ s, p (f b)), p (s.sup f)) (hs : ∀ b ∈ cons a s h, p (f b)),
  p ((cons a s h).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)
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (hypothesis)
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
⊢ ∃ x ∈ s, (insert a r).sup id ≤ x
have incs : (↑r : Set α) ⊆ (↑(insert a r) : Set α)
Tactic: have incs : (r : Set α) ⊆ ↑(insert a r) := by
        rw [Finset.coe_subset]
        apply Finset.subset_insert
-- 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 ∈ s, (insert a r).sup id ≤ x
have insert : ∀ (x : α) (hxs : x ∈ s) (hsx_sup : r.sup id ≤ x), ∃ x ∈ s, (insert a r).sup id ≤ x
Tactic: obtain ⟨x, ⟨hxs, hsx_sup⟩⟩ := ih fun x hx => h x <| incs hx