awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Lattice.Fold
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
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 ⊓ (Finset.cons a_1 s h).sup' ⋯ f = (Finset.cons a_1 s h).sup' ⋯ fun (i : ι) ↦ a ⊓ f i
⊢ a ⊓ s.sup' hs f = s.sup' hs 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]

Premises used: Finset.cons, inf_sup_left, Finset.sup'_cons, Singleton.singleton
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : DistribLattice α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
rw : Eq.{u_2 + 1} (α := α) (s.sup' hs fun (i : ι) ↦ a ⊓ f i) (s.sup' hs fun (i : ι) ↦ f i ⊓ a)
⊢ s.sup' hs f ⊓ a = s.sup' hs fun (i : ι) ↦ f i ⊓ a

Tactic:
rw [inf_comm, sup'_inf_distrib_left]

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

Tactic:
simp_rw [inf_comm]

Premises used: inf_comm
-- Module: Mathlib.Data.Finset.Lattice.Fold
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
rw : g (s.sup' H f) = s.sup' H (g ∘ f)
⊢ g (s.sup f) = s.sup (g ∘ f)

Tactic:
rw [← Finset.sup'_eq_sup H, ← Finset.sup'_eq_sup H]

Premises used: Finset.sup'_eq_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
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' H f) = s.sup' H (g ∘ f)

Tactic:
Finset.comp_sup'_eq_sup'_comp H g (fun x y ↦ Monotone.map_sup mono_g x y)

Premises used: Monotone.map_sup, Finset.comp_sup'_eq_sup'_comp
-- Module: Mathlib.Data.Finset.Lattice.Fold
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' H f) = s.sup' H (g ∘ f)

Tactic:
exact Finset.comp_sup'_eq_sup'_comp H g (fun x y ↦ Monotone.map_sup mono_g x y)

Premises used: Monotone.map_sup, Finset.comp_sup'_eq_sup'_comp
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
rw : (∃ b ∈ s, (↑a : WithBot α) ≤ (WithBot.some ∘ f) b) ↔ ∃ b ∈ s, a ≤ f b
⊢ a ≤ s.sup' H f ↔ ∃ b ∈ s, a ≤ f b

Tactic:
rw [← WithBot.coe_le_coe, coe_sup', Finset.le_sup_iff (WithBot.bot_lt_coe a)]

Premises used: Finset.coe_sup', WithBot.coe_le_coe, Finset.le_sup_iff, WithBot.bot_lt_coe
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ (∃ b ∈ s, (↑a : WithBot α) ≤ (WithBot.some ∘ f) b) ↔ ∃ b ∈ s, a ≤ f b

Tactic:
exists_congr (fun _ => and_congr_right' WithBot.coe_le_coe)

Premises used: and_congr_right', WithBot.coe_le_coe, exists_congr
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ (∃ b ∈ s, (↑a : WithBot α) ≤ (WithBot.some ∘ f) b) ↔ ∃ b ∈ s, a ≤ f b

Tactic:
exact exists_congr (fun _ => and_congr_right' WithBot.coe_le_coe)

Premises used: and_congr_right', WithBot.coe_le_coe, exists_congr
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
rw : (∃ b ∈ s, (↑a : WithBot α) < (WithBot.some ∘ f) b) ↔ ∃ b ∈ s, a < f b
⊢ a < s.sup' H f ↔ ∃ b ∈ s, a < f b

Tactic:
rw [← WithBot.coe_lt_coe, coe_sup', Finset.lt_sup_iff]

Premises used: Finset.coe_sup', WithBot.coe_lt_coe, Finset.lt_sup_iff
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ (∃ b ∈ s, (↑a : WithBot α) < (WithBot.some ∘ f) b) ↔ ∃ b ∈ s, a < f b

Tactic:
exists_congr (fun _ => and_congr_right' WithBot.coe_lt_coe)

Premises used: and_congr_right', exists_congr, WithBot.coe_lt_coe
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ (∃ b ∈ s, (↑a : WithBot α) < (WithBot.some ∘ f) b) ↔ ∃ b ∈ s, a < f b

Tactic:
exact exists_congr (fun _ => and_congr_right' WithBot.coe_lt_coe)

Premises used: and_congr_right', exists_congr, WithBot.coe_lt_coe
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
rw : (∀ b ∈ s, (WithBot.some ∘ f) b < (↑a : WithBot α)) ↔ ∀ i ∈ s, f i < a
⊢ s.sup' H f < a ↔ ∀ i ∈ s, f i < a

Tactic:
rw [← WithBot.coe_lt_coe, coe_sup', Finset.sup_lt_iff (WithBot.bot_lt_coe a)]

Premises used: Finset.coe_sup', Finset.sup_lt_iff, WithBot.coe_lt_coe, WithBot.bot_lt_coe
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ (∀ b ∈ s, (WithBot.some ∘ f) b < (↑a : WithBot α)) ↔ ∀ i ∈ s, f i < a

Tactic:
forall₂_congr (fun _ _ => WithBot.coe_lt_coe)

Premises used: forall₂_congr, WithBot.coe_lt_coe
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ (∀ b ∈ s, (WithBot.some ∘ f) b < (↑a : WithBot α)) ↔ ∀ i ∈ s, f i < a

Tactic:
exact forall₂_congr (fun _ _ => WithBot.coe_lt_coe)

Premises used: forall₂_congr, WithBot.coe_lt_coe
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
c : ι
⊢ ∃ (i : ι), Membership.mem (γ := Finset ι) {c} i ∧ sup' {c} ⋯ f = f i

Tactic:
⟨c, mem_singleton_self c, rfl⟩

Premises used: Finset.mem_singleton_self, And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
c : ι
⊢ ∃ (i : ι), Membership.mem (γ := Finset ι) {c} i ∧ sup' {c} ⋯ f = f i

Tactic:
exact ⟨c, mem_singleton_self c, rfl⟩
-- Module: Mathlib.Data.Finset.Lattice.Fold
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
cons : ∀ (b : ι) (hb : b ∈ s) (h' : s.sup' hs f = f b), ∃ i ∈ Finset.cons c s hcs, (Finset.cons c s hcs).sup' ⋯ f = f i
⊢ ∃ i ∈ Finset.cons c s hcs, (Finset.cons c s hcs).sup' ⋯ f = f i

Tactic:
rcases ih with ⟨b, hb, h'⟩
-- Module: Mathlib.Data.Finset.Lattice.Fold
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
cons : ∃ i ∈ Finset.cons c s hcs, max (f c) (f b) = f i
⊢ ∃ i ∈ Finset.cons c s hcs, (Finset.cons c s hcs).sup' ⋯ f = f i

Tactic:
rw [sup'_cons hs, h']

Premises used: Finset.sup'_cons
-- Module: Mathlib.Data.Finset.Lattice.Fold
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
h : f b ≤ f c
⊢ ∃ i ∈ cons c s hcs, max (f c) (f b) = f i

Tactic:
⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩

Premises used: Iff.mpr, sup_eq_left, And.intro, Exists.intro, Or.inl, Finset.mem_cons, rfl
-- Module: Mathlib.Data.Finset.Lattice.Fold
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
h : f b ≤ f c
⊢ ∃ i ∈ cons c s hcs, max (f c) (f b) = f i

Tactic:
exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩
-- Module: Mathlib.Data.Finset.Lattice.Fold
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
h : f c ≤ f b
⊢ ∃ i ∈ cons c s hcs, max (f c) (f b) = f i

Tactic:
⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩

Premises used: Iff.mpr, sup_eq_right, And.intro, Exists.intro, Finset.mem_cons, Or.inr
-- Module: Mathlib.Data.Finset.Lattice.Fold
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
h : f c ≤ f b
⊢ ∃ i ∈ cons c s hcs, max (f c) (f b) = f i

Tactic:
exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩
-- Module: Mathlib.Data.Finset.Lattice.Fold
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
⊢ 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⟩

Premises used: le_total
-- Module: Mathlib.Data.Finset.Lattice.Fold
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
cons :
  ∀ (c : ι) (s : Finset ι) (hcs : c ∉ s) (hs : s.Nonempty) (ih : ∃ i ∈ s, s.sup' hs f = f i),
    ∃ i ∈ Finset.cons c s hcs, (Finset.cons c s hcs).sup' ⋯ f = f i
⊢ ∃ i ∈ s, s.sup' H 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⟩

Premises used: Finset.cons, Singleton.singleton
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : OrderBot α
s : Finset ι
h : s.Nonempty
f : ι → α
⊢ ∃ i ∈ s, s.sup f = f i

Tactic:
sup'_eq_sup h f ▸ exists_mem_eq_sup' h f

Premises used: Eq.rec, Finset.exists_mem_eq_sup', Finset.sup'_eq_sup
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq α
inst_1 : DecidableEq β
s : Finset γ
f : γ → Multiset β
g : β → α
hg : Injective g
⊢ map g (s.sup f) = s.sup (map g ∘ f)

Tactic:
Finset.comp_sup_eq_sup_comp _ (fun _ _ => map_union hg) (map_zero _)

Premises used: Finset.comp_sup_eq_sup_comp, Multiset.map_zero, Multiset.map_union
-- Module: Mathlib.Data.Finset.Lattice.Fold
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)

Tactic:
s.induction ?_ ?_

Premises used: Finset.induction
-- Module: Mathlib.Data.Finset.Lattice.Fold
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)
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)
⊢ count b (s.sup f) = s.sup fun (a : α) ↦ count b (f a)

Tactic:
refine s.induction ?_ ?_
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ count b (Finset.sup ∅ f) = Finset.sup ∅ fun (a : α) ↦ count b (f a)

Tactic:
count_zero _

Premises used: Multiset.foldr, Finset.fold, Multiset.count_zero, Finset.sup, List.foldr, Multiset.fold
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ count b (Finset.sup ∅ f) = Finset.sup ∅ fun (a : α) ↦ count b (f a)

Tactic:
exact count_zero _

Premises used: Multiset.count_zero
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
s_1 : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
refine_2 :
  i ∉ s →
    (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)
⊢ i ∉ s →
    (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)

Tactic:
_
-- Module: Mathlib.Data.Finset.Lattice.Fold
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))
refine_2₄ 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))
⊢ count b ((insert 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]

Premises used: Multiset.sup_eq_union, Finset.sup_insert, Multiset.count_union
-- Module: Mathlib.Data.Finset.Lattice.Fold
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
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)
⊢ x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v

Tactic:
induction s using Finset.cons_induction
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
β : Type u_8
inst : DecidableEq β
f : α → Multiset β
x : β
⊢ x ∈ Finset.sup ∅ f ↔ ∃ (v : α), Membership.mem (γ := Finset α) ∅ v ∧ x ∈ f v

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_7
β : Type u_8
inst : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
h : a ∉ s
h_1 : 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:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Fold
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
cons :
  ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s) (hs : s.Nonempty),
    (a ∈ s.sup' hs f ↔ ∃ i ∈ s, a ∈ f i) → (a ∈ (Finset.cons a_1 s h).sup' ⋯ f ↔ ∃ i ∈ Finset.cons a_1 s h, a ∈ f i)
⊢ a ∈ s.sup' hs f ↔ ∃ i ∈ s, a ∈ f i

Tactic:
induction hs using Nonempty.cons_induction
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a_1 : ι
⊢ a ∈ sup' {a_1} ⋯ f ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) {a_1} i ∧ a ∈ f i

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a_1 : ι
s_1 : Finset ι
h : a_1 ∉ s_1
hs : s_1.Nonempty
h_1 : a ∈ s_1.sup' hs f ↔ ∃ i ∈ s_1, a ∈ f i
⊢ a ∈ (cons a_1 s_1 h).sup' ⋯ f ↔ ∃ i ∈ cons a_1 s_1 h, a ∈ f i

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Fold
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
cons :
  ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s) (hs : s.Nonempty),
    (a ∈ s.inf' hs f ↔ ∀ i ∈ s, a ∈ f i) → (a ∈ (Finset.cons a_1 s h).inf' ⋯ f ↔ ∀ i ∈ Finset.cons a_1 s h, a ∈ f i)
⊢ a ∈ s.inf' hs f ↔ ∀ i ∈ s, a ∈ f i

Tactic:
induction hs using Nonempty.cons_induction
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a_1 : ι
⊢ a ∈ inf' {a_1} ⋯ f ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) {a_1} i → a ∈ f i

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a_1 : ι
s_1 : Finset ι
h : a_1 ∉ s_1
hs : s_1.Nonempty
h_1 : a ∈ s_1.inf' hs f ↔ ∀ i ∈ s_1, a ∈ f i
⊢ a ∈ (cons a_1 s_1 h).inf' ⋯ f ↔ ∀ i ∈ cons a_1 s_1 h, a ∈ f i

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Fold
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
cons :
  ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s),
    (a ∈ s.sup f ↔ ∃ i ∈ s, a ∈ f i) → (a ∈ (Finset.cons a_1 s h).sup f ↔ ∃ i ∈ Finset.cons a_1 s h, a ∈ f i)
⊢ a ∈ s.sup f ↔ ∃ i ∈ s, a ∈ f i

Tactic:
induction s using cons_induction
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
⊢ a ∈ sup ∅ f ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ a ∈ f i

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
ι : Type u_5
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a_1 : ι
s_1 : Finset ι
h : a_1 ∉ s_1
h_1 : a ∈ s_1.sup f ↔ ∃ i ∈ s_1, a ∈ f i
⊢ a ∈ (cons a_1 s_1 h).sup f ↔ ∃ i ∈ cons a_1 s_1 h, a ∈ f i

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
s : Finset β
f : β → α
h : ∀ (a : α), Membership.mem (γ := Finset α) (s.sup fun (b : β) ↦ {f b}) a ↔ a ∈ image f s
⊢ (s.sup fun (b : β) ↦ {f b}) = image f s

Tactic:
ext a
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
s : Finset β
f : β → α
a : α
h : (∃ i ∈ s, Membership.mem (γ := Finset α) {f i} a) ↔ ∃ a_1 ∈ s, f a_1 = a
⊢ Membership.mem (γ := Finset α) (s.sup fun (b : β) ↦ {f b}) a ↔ a ∈ image f s

Tactic:
rw [mem_sup, mem_image]

Premises used: Finset.mem_sup, Finset.mem_image
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
s : Finset β
f : β → α
a : α
⊢ (∃ i ∈ s, Membership.mem (γ := Finset α) {f i} a) ↔ ∃ a_1 ∈ s, f a_1 = a

Tactic:
simp only [mem_singleton, eq_comm]

Premises used: Finset.mem_singleton, eq_comm
-- Module: Mathlib.Data.Finset.Lattice.Fold
Goal:
α : Type u_2
inst : DecidableEq α
s : Finset α
⊢ s.sup singleton = s

Tactic:
(s.sup_singleton_apply _).trans image_id

Premises used: Finset.image_id, Finset.sup_singleton_apply, Eq.trans
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ Disjoint s t ↔ s ∩ t = ∅

Tactic:
disjoint_iff

Premises used: disjoint_iff
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
x : α
⊢ x ∈ s ∨ Membership.mem (γ := Finset α) ∅ x ↔ x ∈ s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
x : α
⊢ Membership.mem (γ := Finset α) ∅ x ∨ x ∈ s ↔ x ∈ s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s.Nonempty
⊢ (s ∪ t).Nonempty

Tactic:
h.mono subset_union_left

Premises used: Finset.subset_union_left, Finset.Nonempty.mono
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : t.Nonempty
⊢ (s ∪ t).Nonempty

Tactic:
h.mono subset_union_right

Premises used: Finset.subset_union_right, Finset.Nonempty.mono
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ insert a s = {a} ∪ s

Tactic:
rfl

Premises used: List.foldr, Multiset.ndinsert, Multiset.ndunion, rfl, ite
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
x : α
s : Finset α
⊢ {x} ∪ s = insert x s

Tactic:
rfl

Premises used: List.foldr, Multiset.ndinsert, Multiset.ndunion, rfl, ite
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
x : α
s : Finset α
rw : {x} ∪ s = insert x s
rw₁ rw₂ : insert x s = insert x s
⊢ s ∪ {x} = insert x s

Tactic:
rw [Finset.union_comm, singleton_union]

Premises used: Finset.union_comm, Finset.singleton_union
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Finset α
⊢ insert a s ∪ t = insert a (s ∪ t)

Tactic:
simp only [insert_eq, union_assoc]

Premises used: Finset.insert_eq, Finset.union_assoc
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Finset α
⊢ s ∪ insert a t = insert a (s ∪ t)

Tactic:
simp only [insert_eq, union_left_comm]

Premises used: Finset.insert_eq, Finset.union_left_comm
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Finset α
⊢ insert a (s ∪ t) = insert a s ∪ insert a t

Tactic:
simp only [insert_union, union_insert, insert_idem]

Premises used: Finset.insert_union, Finset.union_insert, Finset.insert_idem
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
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

Tactic:
Finset.induction_on b empty_right fun x s _xs hi => symm ?_

Premises used: Finset.induction_on
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
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 α
refine : ∀ (x : α) (s : Finset α) (_xs : x ∉ s) (hi : P a s), P (insert x s) a
⊢ P a b

Tactic:
refine Finset.induction_on b empty_right fun x s _xs hi => symm ?_
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
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
rw : P ({x} ∪ s) a
⊢ P (insert x s) a

Tactic:
rw [Finset.insert_eq]

Premises used: Finset.insert_eq
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
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
apply : P {x} a
⊢ P ({x} ∪ s) a

Tactic:
apply union_of _ (symm hi)
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
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

Tactic:
Finset.induction_on a empty_right fun a t _ta hi => symm ?_

Premises used: Finset.induction_on