awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (WithBot.some ∘ f))
have refine : ∀ (a₁ : WithBot α) (h₁ : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p a₁) (a₂ : WithBot α)
  (h₂ : WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p a₂),
  WithBot.recBotCoe (C := fun (x : WithBot α) ↦ Prop) True p (a₁ ⊔ a₂)
Tactic: refine sup_induction trivial (fun a₁ h₁ a₂ h₂ ↦ ?_) 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
t : Finset β
f g : β → α
h₁ : s = t
h₂ : ∀ x ∈ s, f x = g x
⊢ s.sup' H f = t.sup' ⋯ g
have subst : ∀ (H : t.Nonempty) (h₂ : ∀ x ∈ t, f x = g x), t.sup' H f = t.sup' sorry g
Tactic: subst s
Cleared hypotheses: s, H, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
t : Finset β
f g : β → α
H : t.Nonempty
h₂ : ∀ x ∈ t, f x = g x
⊢ t.sup' H f = t.sup' ⋯ g
have refine : ∀ (c : α), t.sup' H f ≤ c ↔ t.sup' sorry g ≤ c
Tactic: refine eq_of_forall_ge_iff fun c => ?_
-- 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 : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ g (s.sup' H f) = s.sup' H (g ∘ f)
have refine_1 : ∀ (a : β), g (sup' {a} sorry f) = sup' {a} sorry (g ∘ f)
Tactic: refine H.cons_induction ?_ ?_
-- 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 : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
refine_1 : ∀ (a : β), g (sup' {a} ⋯ f) = sup' {a} ⋯ (g ∘ f)
⊢ g (s.sup' H f) = s.sup' H (g ∘ f)
have refine_2 : ∀ (a : β) (s : Finset β) (h : a ∉ s) (hs : s.Nonempty),
  g (s.sup' hs f) = s.sup' hs (g ∘ f) → g ((cons a s h).sup' sorry f) = (cons a s h).sup' sorry (g ∘ f)
Tactic: refine H.cons_induction ?_ ?_
-- 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 : SemilatticeSup β
inst_2 : FunLike F α β
inst_3 : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (s.sup' hs g) : β) (s.sup' hs ((⇑f : (a : α) → β) ∘ g) : β)
have refine_1 : ∀ (a : ι), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (sup' {a} sorry g) : β) (sup' {a} sorry ((⇑f : (a : α) → β) ∘ g) : β)
Tactic: refine hs.cons_induction ?_ ?_
-- 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 : SemilatticeSup β
inst_2 : FunLike F α β
inst_3 : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
refine_1 :
  ∀ (a : ι), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (sup' {a} ⋯ g) : β) (sup' {a} ⋯ ((⇑f : (a : α) → β) ∘ g) : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (s.sup' hs g) : β) (s.sup' hs ((⇑f : (a : α) → β) ∘ g) : β)
have refine_2 : ∀ (a : ι) (s : Finset ι) (h : a ∉ s) (hs : s.Nonempty),
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (s.sup' hs g) : β) (s.sup' hs ((⇑f : (a : α) → β) ∘ g) : β) →
    Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ((cons a s h).sup' sorry g) : β)
      ((cons a s h).sup' sorry ((⇑f : (a : α) → β) ∘ g) : β)
Tactic: refine hs.cons_induction ?_ ?_
-- 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 : DecidableEq β
s : Finset γ
f : γ → β
hs : (image f s).Nonempty
g : β → α
⊢ (image f s).sup' hs g = s.sup' ⋯ (g ∘ f)
have rw : (↑((image f s).sup' hs g) : WithBot α) = (↑(s.sup' sorry (g ∘ 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
γ : Type u_4
inst : SemilatticeSup α
inst_1 : DecidableEq β
s : Finset γ
f : γ → β
hs : (image f s).Nonempty
g : β → α
⊢ (↑((image f s).sup' hs g) : WithBot α) = (↑(s.sup' ⋯ (g ∘ f)) : WithBot α)
have simp : s.sup ((WithBot.some ∘ g) ∘ f) = s.sup (WithBot.some ∘ g ∘ f)
Tactic: simp only [coe_sup', sup_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
s : Finset γ
f : γ ↪ β
g : β → α
hs : (map f s).Nonempty
⊢ (map f s).sup' hs g = s.sup' ⋯ (g ∘ (⇑f : (a : γ) → β))
have rw : s.sup ((WithBot.some ∘ g) ∘ (⇑f : (a : γ) → β)) = s.sup (WithBot.some ∘ g ∘ (⇑f : (a : γ) → β))
Tactic: rw [← WithBot.coe_eq_coe, coe_sup', sup_map, coe_sup']
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
s : Finset ι
hs_1 : s.Nonempty
f : ι → α
a : α
a_1 : ι
s_1 : Finset ι
h : a_1 ∉ s_1
hs : s_1.Nonempty
ih : a ⊓ s_1.sup' hs f = s_1.sup' hs fun (i : ι) ↦ a ⊓ f i
⊢ a ⊓ (cons a_1 s_1 h).sup' ⋯ f = (cons a_1 s_1 h).sup' ⋯ fun (i : ι) ↦ a ⊓ f i
have cons : a ⊓ (f a_1 ⊔ s_1.sup' hs f) = a ⊓ f a_1 ⊔ s_1.sup' hs fun (i : ι) ↦ a ⊓ f i
Tactic: simp_rw [sup'_cons hs, inf_sup_left, ih]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
s : Finset ι
hs_1 : s.Nonempty
f : ι → α
a : α
a_1 : ι
s_1 : Finset ι
h : a_1 ∉ s_1
hs : s_1.Nonempty
ih : a ⊓ s_1.sup' hs f = s_1.sup' hs fun (i : ι) ↦ a ⊓ f i
cons : a ⊓ (f a_1 ⊔ s_1.sup' hs f) = a ⊓ f a_1 ⊔ s_1.sup' hs fun (i : ι) ↦ a ⊓ f i
⊢ a ⊓ (Finset.cons a_1 s_1 h).sup' ⋯ f = (Finset.cons a_1 s_1 h).sup' ⋯ fun (i : ι) ↦ a ⊓ f i
have cons₁ : a ⊓ f a_1 ⊔ a ⊓ s_1.sup' hs f = a ⊓ f a_1 ⊔ s_1.sup' hs fun (i : ι) ↦ a ⊓ f i
Tactic: simp_rw [sup'_cons hs, inf_sup_left, ih]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ a ⊓ s.sup' hs f = s.sup' hs fun (i : ι) ↦ a ⊓ f i
have singleton : ∀ (a_1 : ι), a ⊓ sup' {a_1} sorry f = sup' {a_1} sorry fun (i : ι) ↦ a ⊓ f i
Tactic: induction hs using Finset.Nonempty.cons_induction with
  | singleton => simp
  | cons _ _ _ hs ih => simp_rw [sup'_cons hs, inf_sup_left, ih]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
singleton : ∀ (a_1 : ι), a ⊓ sup' {a_1} ⋯ f = sup' {a_1} ⋯ fun (i : ι) ↦ a ⊓ f i
⊢ a ⊓ s.sup' hs f = s.sup' hs fun (i : ι) ↦ a ⊓ f i
have cons : ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s) (hs : s.Nonempty) (ih : a ⊓ s.sup' hs f = s.sup' hs fun (i : ι) ↦ a ⊓ f i),
  a ⊓ (cons a_1 s h).sup' sorry f = (cons a_1 s h).sup' sorry fun (i : ι) ↦ a ⊓ f i
Tactic: induction hs using Finset.Nonempty.cons_induction with
  | singleton => simp
  | cons _ _ _ hs ih => simp_rw [sup'_cons hs, inf_sup_left, ih]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ s.sup' hs f ⊓ a = s.sup' hs fun (i : ι) ↦ f i ⊓ a
have rw : Eq.{u_2 + 1} (α := α) (s.sup' hs fun (i : ι) ↦ a ⊓ f i) (s.sup' hs fun (i : ι) ↦ f i ⊓ a)
Tactic: rw [inf_comm, sup'_inf_distrib_left]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
ι : Type u_5
inst : LinearOrder α
s : Finset ι
f : ι → α
inst_1 : OrderBot α
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
g : α → β
mono_g : Monotone g
H : s.Nonempty
⊢ g (s.sup f) = s.sup (g ∘ f)
have rw : g (s.sup' H f) = s.sup' H (g ∘ f)
Tactic: rw [← Finset.sup'_eq_sup H, ← Finset.sup'_eq_sup H]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ a ≤ s.sup' H f ↔ ∃ b ∈ s, a ≤ f b
have rw : (∃ b ∈ s, (↑a : WithBot α) ≤ (WithBot.some ∘ f) b) ↔ ∃ b ∈ s, a ≤ f b
Tactic: rw [← WithBot.coe_le_coe, coe_sup', Finset.le_sup_iff (WithBot.bot_lt_coe a)]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ a < s.sup' H f ↔ ∃ b ∈ s, a < f b
have rw : (∃ b ∈ s, (↑a : WithBot α) < (WithBot.some ∘ f) b) ↔ ∃ b ∈ s, a < f b
Tactic: rw [← WithBot.coe_lt_coe, coe_sup', Finset.lt_sup_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ s.sup' H f < a ↔ ∀ i ∈ s, f i < a
have rw : (∀ b ∈ s, (WithBot.some ∘ f) b < (↑a : WithBot α)) ↔ ∀ i ∈ s, f i < a
Tactic: rw [← WithBot.coe_lt_coe, coe_sup', Finset.sup_lt_iff (WithBot.bot_lt_coe a)]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s_1 : Finset ι
H : s_1.Nonempty
f : ι → α
c : ι
s : Finset ι
hcs : c ∉ s
hs : s.Nonempty
ih : ∃ i ∈ s, s.sup' hs f = f i
⊢ ∃ i ∈ cons c s hcs, (cons c s hcs).sup' ⋯ f = f i
have cons : ∀ (b : ι) (hb : b ∈ s) (h' : s.sup' hs f = f b), ∃ i ∈ cons c s hcs, (cons c s hcs).sup' sorry f = f i
Tactic: rcases ih with ⟨b, hb, h'⟩
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s_1 : Finset ι
H : s_1.Nonempty
f : ι → α
c : ι
s : Finset ι
hcs : c ∉ s
hs : s.Nonempty
b : ι
hb : b ∈ s
h' : s.sup' hs f = f b
⊢ ∃ i ∈ cons c s hcs, (cons c s hcs).sup' ⋯ f = f i
have cons : ∃ i ∈ cons c s hcs, max (f c) (f b) = f i
Tactic: rw [sup'_cons hs, h']
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (hypothesis)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s_1 : Finset ι
H : s_1.Nonempty
f : ι → α
c : ι
s : Finset ι
hcs : c ∉ s
hs : s.Nonempty
b : ι
hb : b ∈ s
h' : s.sup' hs f = f b
⊢ ∃ i ∈ cons c s hcs, max (f c) (f b) = f i
have x : f b ≤ f c ∨ f c ≤ f b
Tactic: cases le_total (f b) (f c) with
    | inl h => exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩
    | inr h => exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
⊢ ∃ i ∈ s, s.sup' H f = f i
have singleton : ∀ (c : ι), ∃ (i : ι), Membership.mem (γ := Finset ι) {c} i ∧ sup' {c} sorry f = f i
Tactic: induction H using Finset.Nonempty.cons_induction with
  | singleton c => exact ⟨c, mem_singleton_self c, rfl⟩
  | cons c s hcs hs ih =>
    rcases ih with ⟨b, hb, h'⟩
    rw [sup'_cons hs, h']
    cases le_total (f b) (f c) with
    | inl h => exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩
    | inr h => exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
singleton : ∀ (c : ι), ∃ (i : ι), Membership.mem (γ := Finset ι) {c} i ∧ sup' {c} ⋯ f = f i
⊢ ∃ i ∈ s, s.sup' H f = f i
have cons : ∀ (c : ι) (s : Finset ι) (hcs : c ∉ s) (hs : s.Nonempty) (ih : ∃ i ∈ s, s.sup' hs f = f i),
  ∃ i ∈ cons c s hcs, (cons c s hcs).sup' sorry f = f i
Tactic: induction H using Finset.Nonempty.cons_induction with
  | singleton c => exact ⟨c, mem_singleton_self c, rfl⟩
  | cons c s hcs hs ih =>
    rcases ih with ⟨b, hb, h'⟩
    rw [sup'_cons hs, h']
    cases le_total (f b) (f c) with
    | inl h => exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩
    | inr h => exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ count b (s.sup f) = s.sup fun (a : α) ↦ count b (f a)
have refine_1 : count b (Finset.sup ∅ f) = Finset.sup ∅ fun (a : α) ↦ count b (f a)
Tactic: refine s.induction ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
refine_1 : count b (Finset.sup ∅ f) = Finset.sup ∅ fun (a : α) ↦ count b (f a)
⊢ count b (s.sup f) = s.sup fun (a : α) ↦ count b (f a)
have refine_2 : ∀ (a : α) (s : Finset α),
  a ∉ s →
    (count b (s.sup f) = s.sup fun (a : α) ↦ count b (f a)) →
      count b ((insert a s).sup f) = (insert a s).sup fun (a : α) ↦ count b (f a)
Tactic: refine s.induction ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
s_1 : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
h : i ∉ s
ih : count b (s.sup f) = s.sup fun (a : α) ↦ count b (f a)
⊢ count b ((insert i s).sup f) = (insert i s).sup fun (a : α) ↦ count b (f a)
have refine_2 : count b (f i ⊔ s.sup f) = (insert i s).sup fun (a : α) ↦ count b (f a)
Tactic: rw [Finset.sup_insert, sup_eq_union, count_union, Finset.sup_insert, ih]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
s_1 : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
h : i ∉ s
ih : count b (s.sup f) = s.sup fun (a : α) ↦ count b (f a)
refine_2 : count b (f i ⊔ s.sup f) = (insert i s).sup fun (a : α) ↦ count b (f a)
⊢ count b ((insert i s).sup f) = (insert i s).sup fun (a : α) ↦ count b (f a)
have refine_2₁ : count b (f i ∪ s.sup f) = (insert i s).sup fun (a : α) ↦ count b (f a)
Tactic: rw [Finset.sup_insert, sup_eq_union, count_union, Finset.sup_insert, ih]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
s_1 : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
h : i ∉ s
ih : count b (s.sup f) = s.sup fun (a : α) ↦ count b (f a)
refine_2 : count b (f i ⊔ s.sup f) = (insert i s).sup fun (a : α) ↦ count b (f a)
refine_2₁ : count b (f i ∪ s.sup f) = (insert i s).sup fun (a : α) ↦ count b (f a)
⊢ count b ((insert i s).sup f) = (insert i s).sup fun (a : α) ↦ count b (f a)
have refine_2₂ : max (count b (f i)) (count b (s.sup f)) = (insert i s).sup fun (a : α) ↦ count b (f a)
Tactic: rw [Finset.sup_insert, sup_eq_union, count_union, Finset.sup_insert, ih]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
s_1 : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
h : i ∉ s
ih : count b (s.sup f) = s.sup fun (a : α) ↦ count b (f a)
refine_2 : count b (f i ⊔ s.sup f) = (insert i s).sup fun (a : α) ↦ count b (f a)
refine_2₁ : count b (f i ∪ s.sup f) = (insert i s).sup fun (a : α) ↦ count b (f a)
refine_2₂ : max (count b (f i)) (count b (s.sup f)) = (insert i s).sup fun (a : α) ↦ count b (f a)
⊢ count b ((insert i s).sup f) = (insert i s).sup fun (a : α) ↦ count b (f a)
have refine_2₃ : max (count b (f i)) (count b (s.sup f)) = max (count b (f i)) (s.sup fun (a : α) ↦ count b (f a))
Tactic: rw [Finset.sup_insert, sup_eq_union, count_union, Finset.sup_insert, ih]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
s_1 : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
h : i ∉ s
ih : count b (s.sup f) = s.sup fun (a : α) ↦ count b (f a)
refine_2 : count b (f i ⊔ s.sup f) = (insert i s).sup fun (a : α) ↦ count b (f a)
refine_2₁ : count b (f i ∪ s.sup f) = (insert i s).sup fun (a : α) ↦ count b (f a)
refine_2₂ : max (count b (f i)) (count b (s.sup f)) = (insert i s).sup fun (a : α) ↦ count b (f a)
refine_2₃ : max (count b (f i)) (count b (s.sup f)) = max (count b (f i)) (s.sup fun (a : α) ↦ count b (f a))
⊢ count b ((insert i s).sup f) = (insert i s).sup fun (a : α) ↦ count b (f a)
have refine_2₄ : max (count b (f i)) (s.sup fun (a : α) ↦ count b (f a)) = max (count b (f i)) (s.sup fun (a : α) ↦ count b (f a))
Tactic: rw [Finset.sup_insert, sup_eq_union, count_union, Finset.sup_insert, ih]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_7
β : Type u_8
inst : DecidableEq β
s : Finset α
f : α → Multiset β
x : β
⊢ x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v
have empty : x ∈ Finset.sup ∅ f ↔ ∃ (v : α), Membership.mem (γ := Finset α) ∅ v ∧ x ∈ f v
Tactic: induction s using Finset.cons_induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_7
β : Type u_8
inst : DecidableEq β
s : Finset α
f : α → Multiset β
x : β
empty : x ∈ Finset.sup ∅ f ↔ ∃ (v : α), Membership.mem (γ := Finset α) ∅ v ∧ x ∈ f v
⊢ x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v
have cons : ∀ (a : α) (s : Finset α) (h : a ∉ s),
  (x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v) → (x ∈ (Finset.cons a s h).sup f ↔ ∃ v ∈ Finset.cons a s h, x ∈ f v)
Tactic: induction s using Finset.cons_induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
hs : s.Nonempty
⊢ a ∈ s.sup' hs f ↔ ∃ i ∈ s, a ∈ f i
have singleton : ∀ (a_1 : ι), a ∈ sup' {a_1} sorry f ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) {a_1} i ∧ a ∈ f i
Tactic: induction hs using Nonempty.cons_induction
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
hs : s.Nonempty
singleton : ∀ (a_1 : ι), a ∈ sup' {a_1} ⋯ f ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) {a_1} i ∧ a ∈ f i
⊢ a ∈ s.sup' hs f ↔ ∃ i ∈ s, a ∈ f i
have cons : ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s) (hs : s.Nonempty),
  (a ∈ s.sup' hs f ↔ ∃ i ∈ s, a ∈ f i) → (a ∈ (cons a_1 s h).sup' sorry f ↔ ∃ i ∈ cons a_1 s h, a ∈ f i)
Tactic: induction hs using Nonempty.cons_induction
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
hs : s.Nonempty
⊢ a ∈ s.inf' hs f ↔ ∀ i ∈ s, a ∈ f i
have singleton : ∀ (a_1 : ι), a ∈ inf' {a_1} sorry f ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) {a_1} i → a ∈ f i
Tactic: induction hs using Nonempty.cons_induction
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
hs : s.Nonempty
singleton : ∀ (a_1 : ι), a ∈ inf' {a_1} ⋯ f ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) {a_1} i → a ∈ f i
⊢ a ∈ s.inf' hs f ↔ ∀ i ∈ s, a ∈ f i
have cons : ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s) (hs : s.Nonempty),
  (a ∈ s.inf' hs f ↔ ∀ i ∈ s, a ∈ f i) → (a ∈ (cons a_1 s h).inf' sorry f ↔ ∀ i ∈ cons a_1 s h, a ∈ f i)
Tactic: induction hs using Nonempty.cons_induction
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
⊢ a ∈ s.sup f ↔ ∃ i ∈ s, a ∈ f i
have empty : a ∈ sup ∅ f ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ a ∈ f i
Tactic: induction s using cons_induction
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
empty : a ∈ sup ∅ f ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ a ∈ f i
⊢ a ∈ s.sup f ↔ ∃ i ∈ s, a ∈ f i
have cons : ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s),
  (a ∈ s.sup f ↔ ∃ i ∈ s, a ∈ f i) → (a ∈ (cons a_1 s h).sup f ↔ ∃ i ∈ cons a_1 s h, a ∈ f i)
Tactic: induction s using cons_induction
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
s : Finset β
f : β → α
⊢ (s.sup fun (b : β) ↦ {f b}) = image f s
have h : ∀ (a : α), Membership.mem (γ := Finset α) (s.sup fun (b : β) ↦ {f b}) a ↔ a ∈ image f s
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Fold (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
s : Finset β
f : β → α
a : α
⊢ Membership.mem (γ := Finset α) (s.sup fun (b : β) ↦ {f b}) a ↔ a ∈ image f s
have h : (∃ i ∈ s, Membership.mem (γ := Finset α) {f i} a) ↔ ∃ a_1 ∈ s, f a_1 = a
Tactic: rw [mem_sup, mem_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
s : Finset α
⊢ s ∪ {x} = insert x s
have rw : {x} ∪ s = insert x s
Tactic: rw [Finset.union_comm, singleton_union]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
s : Finset α
rw : {x} ∪ s = insert x s
⊢ s ∪ {x} = insert x s
have rw₁ : insert x s = insert x s
Tactic: rw [Finset.union_comm, singleton_union]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a b : Finset α
⊢ P a b
have refine : ∀ (x : α) (s : Finset α) (_xs : x ∉ s) (hi : P a s), P (insert x s) a
Tactic: refine Finset.induction_on b empty_right fun x s _xs hi => symm ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi : P a s
⊢ P (insert x s) a
have rw : P ({x} ∪ s) a
Tactic: rw [Finset.insert_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi : P a s
⊢ P ({x} ∪ s) a
have apply : P {x} a
Tactic: apply union_of _ (symm hi)
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi : P a s
⊢ P {x} a
have refine : ∀ (a : α) (t : Finset α) (_ta : a ∉ t) (hi : P {x} t), P (insert a t) {x}
Tactic: refine Finset.induction_on a empty_right fun a t _ta hi => symm ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a_1 b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi_1 : P a_1 s
a : α
t : Finset α
_ta : a ∉ t
hi : P {x} t
⊢ P (insert a t) {x}
have rw : P ({a} ∪ t) {x}
Tactic: rw [Finset.insert_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₂
x : α
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ insert a (s₁ ∩ s₂)
have this : x = a ∨ x ∈ s₂ ↔ x ∈ s₂
Tactic: have : x = a ∨ x ∈ s₂ ↔ x ∈ s₂ := or_iff_right_of_imp <| by rintro rfl; exact h
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₁
⊢ s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)
have rw : insert a s₂ ∩ s₁ = insert a (s₁ ∩ s₂)
Tactic: rw [inter_comm, insert_inter_of_mem h, inter_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₁
rw : insert a s₂ ∩ s₁ = insert a (s₁ ∩ s₂)
⊢ s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)
have rw₁ : insert a (s₂ ∩ s₁) = insert a (s₁ ∩ s₂)
Tactic: rw [inter_comm, insert_inter_of_mem h, inter_comm]