awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : fold (fun (x1 x2 : Finset α) ↦ x1 ∪ x2) ∅ singleton s = s
insert : {a} ∪ fold (fun (x1 x2 : Finset α) ↦ x1 ∪ x2) ∅ singleton s = Insert.insert a s
insert₁ : {a} ∪ s = Insert.insert a s
insert₂ insert₃ : {a} ∪ s = {a} ∪ s
⊢ fold (fun (x1 x2 : Finset α) ↦ x1 ∪ x2) ∅ singleton (Insert.insert a s) = Insert.insert a s

Tactic:
rw [fold_insert has, ih, insert_eq]

Premises used: Finset.insert_eq, Finset.fold_insert
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
empty : Eq (α := Finset α) (fold (fun (x1 x2 : Finset α) ↦ x1 ∪ x2) ∅ singleton ∅) ∅
insert :
  ∀ (a : α) (s : Finset α) (has : a ∉ s) (ih : fold (fun (x1 x2 : Finset α) ↦ x1 ∪ x2) ∅ singleton s = s),
    fold (fun (x1 x2 : Finset α) ↦ x1 ∪ x2) ∅ singleton (Insert.insert a s) = Insert.insert a s
⊢ fold (fun (x1 x2 : Finset α) ↦ x1 ∪ x2) ∅ singleton s = s

Tactic:
induction s using Finset.induction_on with
  | empty => simp only [fold_empty]
  | insert a s has ih => rw [fold_insert has, ih, insert_eq]

Premises used: Finset.insert_eq, Insert.insert, Finset.fold_empty
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ fold (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ singleton s = s

Tactic:
fold_union_empty_singleton s

Premises used: Finset.fold_union_empty_singleton
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
⊢ c ≤ fold min b f s ↔ c ≤ b ∧ ∀ x ∈ s, c ≤ f x

Tactic:
fold_op_rel_iff_and le_min_iff

Premises used: Finset.fold_op_rel_iff_and
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
change : c ≥ fold min b f s ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c
⊢ fold min b f s ≤ c ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c

Tactic:
change _ ≥ _ ↔ _
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
hr : ∀ {x y z : β}, x ≥ min y z ↔ x ≥ y ∨ x ≥ z
⊢ c ≥ fold min b f s ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c

Tactic:
apply fold_op_rel_iff_or

Premises used: Finset.fold_op_rel_iff_or
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c x y z : β
hr : min y z ≤ x ↔ x ≥ y ∨ x ≥ z
⊢ x ≥ min y z ↔ x ≥ y ∨ x ≥ z

Tactic:
change _ ≤ _ ↔ _
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c x y z : β
⊢ min y z ≤ x ↔ x ≥ y ∨ x ≥ z

Tactic:
min_le_iff

Premises used: min_le_iff
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c x y z : β
⊢ min y z ≤ x ↔ x ≥ y ∨ x ≥ z

Tactic:
exact min_le_iff

Premises used: min_le_iff
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
⊢ c < fold min b f s ↔ c < b ∧ ∀ x ∈ s, c < f x

Tactic:
fold_op_rel_iff_and lt_min_iff

Premises used: Finset.fold_op_rel_iff_and
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
change : c > fold min b f s ↔ b < c ∨ ∃ x ∈ s, f x < c
⊢ fold min b f s < c ↔ b < c ∨ ∃ x ∈ s, f x < c

Tactic:
change _ > _ ↔ _
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
hr : ∀ {x y z : β}, x > min y z ↔ x > y ∨ x > z
⊢ c > fold min b f s ↔ b < c ∨ ∃ x ∈ s, f x < c

Tactic:
apply fold_op_rel_iff_or

Premises used: Finset.fold_op_rel_iff_or
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c x y z : β
hr : min y z < x ↔ x > y ∨ x > z
⊢ x > min y z ↔ x > y ∨ x > z

Tactic:
change _ < _ ↔ _
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c x y z : β
⊢ min y z < x ↔ x > y ∨ x > z

Tactic:
min_lt_iff

Premises used: min_lt_iff
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c x y z : β
⊢ min y z < x ↔ x > y ∨ x > z

Tactic:
exact min_lt_iff

Premises used: min_lt_iff
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
change : c ≥ fold max b f s ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c
⊢ fold max b f s ≤ c ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c

Tactic:
change _ ≥ _ ↔ _
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
hr : ∀ {x y z : β}, x ≥ max y z ↔ x ≥ y ∧ x ≥ z
⊢ c ≥ fold max b f s ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c

Tactic:
apply fold_op_rel_iff_and

Premises used: Finset.fold_op_rel_iff_and
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c x y z : β
hr : max y z ≤ x ↔ x ≥ y ∧ x ≥ z
⊢ x ≥ max y z ↔ x ≥ y ∧ x ≥ z

Tactic:
change _ ≤ _ ↔ _
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c x y z : β
⊢ max y z ≤ x ↔ x ≥ y ∧ x ≥ z

Tactic:
max_le_iff

Premises used: max_le_iff
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c x y z : β
⊢ max y z ≤ x ↔ x ≥ y ∧ x ≥ z

Tactic:
exact max_le_iff

Premises used: max_le_iff
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
⊢ c ≤ fold max b f s ↔ c ≤ b ∨ ∃ x ∈ s, c ≤ f x

Tactic:
fold_op_rel_iff_or le_max_iff

Premises used: Finset.fold_op_rel_iff_or
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
change : c > fold max b f s ↔ b < c ∧ ∀ x ∈ s, f x < c
⊢ fold max b f s < c ↔ b < c ∧ ∀ x ∈ s, f x < c

Tactic:
change _ > _ ↔ _
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
hr : ∀ {x y z : β}, x > max y z ↔ x > y ∧ x > z
⊢ c > fold max b f s ↔ b < c ∧ ∀ x ∈ s, f x < c

Tactic:
apply fold_op_rel_iff_and

Premises used: Finset.fold_op_rel_iff_and
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c x y z : β
hr : max y z < x ↔ x > y ∧ x > z
⊢ x > max y z ↔ x > y ∧ x > z

Tactic:
change _ < _ ↔ _
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c x y z : β
⊢ max y z < x ↔ x > y ∧ x > z

Tactic:
max_lt_iff

Premises used: max_lt_iff
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c x y z : β
⊢ max y z < x ↔ x > y ∧ x > z

Tactic:
exact max_lt_iff

Premises used: max_lt_iff
-- Module: Mathlib.Data.Finset.Fold
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
⊢ c < fold max b f s ↔ c < b ∨ ∃ x ∈ s, c < f x

Tactic:
fold_op_rel_iff_or lt_max_iff

Premises used: Finset.fold_op_rel_iff_or
-- Module: Mathlib.Data.Finset.Functor
Goal:
α_1 β_1 : Type u
inst : (P : Prop) → Decidable P
α β : Type u_1
⊢ Eq (α := α → Finset β → Finset α) Functor.mapConst (Functor.map ∘ const β)

Tactic:
simp only [Functor.mapConst, Functor.map]

Premises used: Functor.mapConst, Functor.map
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
s : Finset α
f : α → β
⊢ f <$> s = image f s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Functor
Goal:
α : Type u_1
⊢ Eq (α := α → Finset α) pure singleton

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
s : Finset α
t : Finset (α → β)
⊢ t <*> s = t.sup fun (f : α → β) ↦ image f s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
s : Finset α
t : Finset β
⊢ s <* t = if t = ∅ then ∅ else s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
s : Finset α
t : Finset β
⊢ s *> t = if s = ∅ then ∅ else t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Functor
Goal:
inst : (P : Prop) → Decidable P
α β γ : Type u
f : α → β → γ
s : Finset α
t : Finset β
h : ∀ (a : γ), a ∈ image₂ f s t ↔ a ∈ f <$> s <*> t
⊢ image₂ f s t = f <$> s <*> t

Tactic:
ext
-- Module: Mathlib.Data.Finset.Functor
Goal:
inst : (P : Prop) → Decidable P
α β γ : Type u
f : α → β → γ
s : Finset α
t : Finset β
a : γ
⊢ a ∈ image₂ f s t ↔ a ∈ f <$> s <*> t

Tactic:
simp [mem_sup]

Premises used: Finset.mem_sup
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
rw : (if t = ∅ then ∅ else s) = (image (const β_1) s).sup fun (f : β_1 → α_1) ↦ image f t
⊢ s <* t = const β_1 <$> s <*> t

Tactic:
rw [seq_def, fmap_def, seqLeft_def]

Premises used: Finset.seq_def, Finset.seqLeft_def, Finset.fmap_def
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
inl : (if Eq.{u_1 + 1} (α := Finset β_1) ∅ ∅ then ∅ else s) = (image (const β_1) s).sup fun (f : β_1 → α_1) ↦ image f ∅
inr : ∀ (ht : t.Nonempty), (if t = ∅ then ∅ else s) = (image (const β_1) s).sup fun (f : β_1 → α_1) ↦ image f t
⊢ (if t = ∅ then ∅ else s) = (image (const β_1) s).sup fun (f : β_1 → α_1) ↦ image f t

Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
inl : Eq (α := Finset α_1) ∅ ((image (const β_1) s).sup fun (f : β_1 → α_1) ↦ ∅)
⊢ (if Eq.{u_1 + 1} (α := Finset β_1) ∅ ∅ then ∅ else s) = (image (const β_1) s).sup fun (f : β_1 → α_1) ↦ image f ∅

Tactic:
simp_rw [image_empty, if_true]

Premises used: Finset.image_empty, if_true
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
⊢ Eq (α := Finset α_1) ∅ ((image (const β_1) s).sup fun (f : β_1 → α_1) ↦ ∅)

Tactic:
(sup_bot _).symm

Premises used: Finset.sup_bot, Eq.symm
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
⊢ Eq (α := Finset α_1) ∅ ((image (const β_1) s).sup fun (f : β_1 → α_1) ↦ ∅)

Tactic:
exact (sup_bot _).symm

Premises used: Finset.sup_bot, Eq.symm
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
ht : t.Nonempty
inr :
  ∀ (a : α_1),
    (a ∈ if t = ∅ then ∅ else s) ↔
      Membership.mem (γ := Finset α_1) ((image (const β_1) s).sup fun (f : β_1 → α_1) ↦ image f t) a
⊢ (if t = ∅ then ∅ else s) = (image (const β_1) s).sup fun (f : β_1 → α_1) ↦ image f t

Tactic:
ext a
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
ht : t.Nonempty
a : α_1
inr : a ∈ s ↔ ∃ i ∈ image (const β_1) s, a ∈ image i t
⊢ (a ∈ if t = ∅ then ∅ else s) ↔
    Membership.mem (γ := Finset α_1) ((image (const β_1) s).sup fun (f : β_1 → α_1) ↦ image f t) a

Tactic:
rw [if_neg ht.ne_empty, mem_sup]

Premises used: Finset.mem_sup, Finset.Nonempty.ne_empty, if_neg
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
ht : t.Nonempty
a : α_1
⊢ a ∈ s ↔ ∃ i ∈ image (const β_1) s, a ∈ image i t

Tactic:
⟨fun ha => ⟨const _ a, mem_image_of_mem _ ha, mem_image_const_self.2 ht⟩, ?_⟩

Premises used: Iff.mpr, Finset.mem_image_const_self, And.intro, Iff.intro, Exists.intro, Function.const, Finset.mem_image_of_mem
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
ht : t.Nonempty
a : α_1
inr : (∃ i ∈ image (const β_1) s, a ∈ image i t) → a ∈ s
⊢ a ∈ s ↔ ∃ i ∈ image (const β_1) s, a ∈ image i t

Tactic:
refine ⟨fun ha => ⟨const _ a, mem_image_of_mem _ ha, mem_image_const_self.2 ht⟩, ?_⟩
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
ht : t.Nonempty
a : α_1
f : β_1 → α_1
hf : f ∈ image (const β_1) s
ha : a ∈ image f t
⊢ ∃ a ∈ s, const β_1 a = f

Tactic:
rw [mem_image] at hf ha

Premises used: Finset.mem_image
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
ht : t.Nonempty
a : α_1
f : β_1 → α_1
hf : f ∈ image (const β_1) s
ha : a ∈ image f t
hf₁ : ∃ a ∈ s, const β_1 a = f
⊢ ∃ a_1 ∈ t, f a_1 = a

Tactic:
rw [mem_image] at hf ha

Premises used: Finset.mem_image
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
ht : t.Nonempty
a : α_1
f : β_1 → α_1
hf : ∃ a ∈ s, const β_1 a = f
ha : ∃ a_1 ∈ t, f a_1 = a
inr : ∀ (b : α_1) (hb : b ∈ s) (ha : ∃ a_1 ∈ t, const β_1 b a_1 = a), a ∈ s
⊢ a ∈ s

Tactic:
obtain ⟨b, hb, rfl⟩ := hf

Premises used: rfl
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
ht : t.Nonempty
a b : α_1
hb : b ∈ s
ha : ∃ a_1 ∈ t, const β_1 b a_1 = a
inr : ∀ w ∈ t, const β_1 b w ∈ s
⊢ a ∈ s

Tactic:
obtain ⟨_, _, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
ht : t.Nonempty
b : α_1
hb : b ∈ s
w : β_1
left : w ∈ t
⊢ const β_1 b w ∈ s

Tactic:
hb

Premises used: Set.Mem, setOf
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
ht : t.Nonempty
b : α_1
hb : b ∈ s
w : β_1
left : w ∈ t
⊢ const β_1 b w ∈ s

Tactic:
exact hb
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
rw : (if s = ∅ then ∅ else t) = sup (image (const α_1 id) s) fun (f : β_1 → β_1) ↦ image f t
⊢ Eq (α := Finset β_1) (s *> t) (const α_1 id <$> s <*> t)

Tactic:
rw [seq_def, fmap_def, seqRight_def]

Premises used: Finset.seqRight_def, Finset.seq_def, Finset.fmap_def
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
inl :
  (if Eq.{u_1 + 1} (α := Finset α_1) ∅ ∅ then ∅ else t) = sup (image (const α_1 id) ∅) fun (f : β_1 → β_1) ↦ image f t
inr : ∀ (hs : s.Nonempty), (if s = ∅ then ∅ else t) = sup (image (const α_1 id) s) fun (f : β_1 → β_1) ↦ image f t
⊢ (if s = ∅ then ∅ else t) = sup (image (const α_1 id) s) fun (f : β_1 → β_1) ↦ image f t

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
t : Finset β_1
inl : Eq (α := Finset β_1) ∅ (sup (image (const α_1 id) ∅) fun (f : β_1 → β_1) ↦ image f t)
inl₁ : Eq.{u_1 + 1} (α := Finset β_1) ∅ (sup ∅ fun (f : β_1 → β_1) ↦ image f t)
inl₂ : Eq.{u_1 + 1} (α := Finset β_1) ∅ ⊥
inl₃ inl₄ : Eq.{u_1 + 1} (α := Finset β_1) ∅ ∅
⊢ (if Eq.{u_1 + 1} (α := Finset α_1) ∅ ∅ then ∅ else t) = sup (image (const α_1 id) ∅) fun (f : β_1 → β_1) ↦ image f t

Tactic:
rw [if_pos rfl, image_empty, sup_empty, bot_eq_empty]

Premises used: Finset.bot_eq_empty, Finset.image_empty, Finset.sup_empty, if_pos, rfl
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
hs : s.Nonempty
inr :
  ∀ (a : β_1),
    (a ∈ if s = ∅ then ∅ else t) ↔
      Membership.mem (γ := Finset β_1) (sup (image (const α_1 id) s) fun (f : β_1 → β_1) ↦ image f t) a
⊢ (if s = ∅ then ∅ else t) = sup (image (const α_1 id) s) fun (f : β_1 → β_1) ↦ image f t

Tactic:
ext a
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
hs : s.Nonempty
a : β_1
inr : a ∈ t ↔ ∃ (i : β_1 → β_1), Membership.mem (γ := Finset (β_1 → β_1)) (image (const α_1 id) s) i ∧ a ∈ image i t
⊢ (a ∈ if s = ∅ then ∅ else t) ↔
    Membership.mem (γ := Finset β_1) (sup (image (const α_1 id) s) fun (f : β_1 → β_1) ↦ image f t) a

Tactic:
rw [if_neg hs.ne_empty, mem_sup]

Premises used: Finset.mem_sup, Finset.Nonempty.ne_empty, if_neg
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
hs : s.Nonempty
a : β_1
ha rwa rwa₁ rwa₂ rwa₃ : a ∈ t
⊢ a ∈ image id t

Tactic:
rwa [image_id]

Premises used: Finset.image_id
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
hs : s.Nonempty
a : β_1
inr : (∃ (i : β_1 → β_1), Membership.mem (γ := Finset (β_1 → β_1)) (image (const α_1 id) s) i ∧ a ∈ image i t) → a ∈ t
⊢ a ∈ t ↔ ∃ (i : β_1 → β_1), Membership.mem (γ := Finset (β_1 → β_1)) (image (const α_1 id) s) i ∧ a ∈ image i t

Tactic:
refine ⟨fun ha => ⟨id, mem_image_const_self.2 hs, by rwa [image_id]⟩, ?_⟩
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
hs : s.Nonempty
a : β_1
f : β_1 → β_1
hf : Membership.mem (γ := Finset (β_1 → β_1)) (image (const α_1 id) s) f
ha : a ∈ image f t
⊢ ∃ a ∈ s, const α_1 id a = f

Tactic:
rw [mem_image] at hf ha

Premises used: Finset.mem_image
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
hs : s.Nonempty
a : β_1
f : β_1 → β_1
hf : Membership.mem (γ := Finset (β_1 → β_1)) (image (const α_1 id) s) f
ha : a ∈ image f t
hf₁ : ∃ a ∈ s, const α_1 id a = f
⊢ ∃ a_1 ∈ t, f a_1 = a

Tactic:
rw [mem_image] at hf ha

Premises used: Finset.mem_image
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
hs : s.Nonempty
a : β_1
f : β_1 → β_1
hf : ∃ a ∈ s, const α_1 id a = f
ha : ∃ a_1 ∈ t, f a_1 = a
inr : ∀ (b : β_1) (hb : b ∈ t), f b ∈ t
⊢ a ∈ t

Tactic:
obtain ⟨b, hb, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
hs : s.Nonempty
f : β_1 → β_1
hf : ∃ a ∈ s, const α_1 id a = f
b : β_1
hb : b ∈ t
inr : ∀ w ∈ s, Membership.mem (α := β_1) t (const α_1 id w b : β_1)
⊢ f b ∈ t

Tactic:
obtain ⟨_, _, rfl⟩ := hf

Premises used: rfl
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
hs : s.Nonempty
b : β_1
hb : b ∈ t
w : α_1
left : w ∈ s
⊢ Membership.mem (α := β_1) t (const α_1 id w b : β_1)

Tactic:
hb

Premises used: Set.Mem, setOf
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
hs : s.Nonempty
b : β_1
hb : b ∈ t
w : α_1
left : w ∈ s
⊢ Membership.mem (α := β_1) t (const α_1 id w b : β_1)

Tactic:
exact hb
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
f : α_1 → β_1
s : Finset α_1
⊢ pure f <*> s = f <$> s

Tactic:
simp only [pure_def, seq_def, sup_singleton, fmap_def]

Premises used: Finset.sup_singleton, Finset.seq_def, Finset.pure_def, Finset.fmap_def
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 γ : Type u_1
s : Finset α_1
t : Finset (α_1 → β_1)
u : Finset (β_1 → γ)
h : ∀ (a : γ), a ∈ u <*> (t <*> s) ↔ a ∈ comp <$> u <*> t <*> s
⊢ u <*> (t <*> s) = comp <$> u <*> t <*> s

Tactic:
ext a
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 γ : Type u_1
s : Finset α_1
t : Finset (α_1 → β_1)
u : Finset (β_1 → γ)
a : γ
h :
  Membership.mem (γ := Finset γ) (u.sup fun (f : β_1 → γ) ↦ image f (t.sup fun (f : α_1 → β_1) ↦ image f s)) a ↔
    Membership.mem (γ := Finset γ)
      (sup (sup (image comp u) fun (f : (α_1 → β_1) → α_1 → γ) ↦ image f t) fun (f : α_1 → γ) ↦ image f s) a
⊢ a ∈ u <*> (t <*> s) ↔ a ∈ comp <$> u <*> t <*> s

Tactic:
simp_rw [seq_def, fmap_def]

Premises used: Finset.seq_def, Finset.fmap_def
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 γ : Type u_1
s : Finset α_1
t : Finset (α_1 → β_1)
u : Finset (β_1 → γ)
a : γ
h :
  (∃ i ∈ u, ∃ (a_1 : β_1), (∃ i ∈ t, ∃ a ∈ s, i a = a_1) ∧ i a_1 = a) ↔
    ∃ (i : α_1 → γ),
      (∃ (i_1 : (α_1 → β_1) → α_1 → γ), (∃ a ∈ u, comp a = i_1) ∧ ∃ a ∈ t, i_1 a = i) ∧ ∃ a_1 ∈ s, i a_1 = a
⊢ Membership.mem (γ := Finset γ) (u.sup fun (f : β_1 → γ) ↦ image f (t.sup fun (f : α_1 → β_1) ↦ image f s)) a ↔
    Membership.mem (γ := Finset γ)
      (sup (sup (image comp u) fun (f : (α_1 → β_1) → α_1 → γ) ↦ image f t) fun (f : α_1 → γ) ↦ image f s) a

Tactic:
simp only [mem_sup, mem_image]

Premises used: Finset.mem_sup, Finset.mem_image
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 γ : Type u_1
s : Finset α_1
t : Finset (α_1 → β_1)
u : Finset (β_1 → γ)
a : γ
h :
  (∃ i ∈ u, ∃ (a_1 : β_1), (∃ i ∈ t, ∃ a ∈ s, i a = a_1) ∧ i a_1 = a) →
    ∃ (i : α_1 → γ),
      (∃ (i_1 : (α_1 → β_1) → α_1 → γ), (∃ a ∈ u, comp a = i_1) ∧ ∃ a ∈ t, i_1 a = i) ∧ ∃ a_2 ∈ s, i a_2 = a
h₁ :
  (∃ (i : α_1 → γ),
      (∃ (i_1 : (α_1 → β_1) → α_1 → γ), (∃ a ∈ u, comp a = i_1) ∧ ∃ a ∈ t, i_1 a = i) ∧ ∃ a_1 ∈ s, i a_1 = a) →
    ∃ i ∈ u, ∃ (a_2 : β_1), (∃ i ∈ t, ∃ a ∈ s, i a = a_2) ∧ i a_2 = a
⊢ (∃ i ∈ u, ∃ (a_1 : β_1), (∃ i ∈ t, ∃ a ∈ s, i a = a_1) ∧ i a_1 = a) ↔
    ∃ (i : α_1 → γ),
      (∃ (i_1 : (α_1 → β_1) → α_1 → γ), (∃ a ∈ u, comp a = i_1) ∧ ∃ a ∈ t, i_1 a = i) ∧ ∃ a_1 ∈ s, i a_1 = a

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 γ : Type u_1
s : Finset α_1
t : Finset (α_1 → β_1)
u : Finset (β_1 → γ)
g : β_1 → γ
hg : g ∈ u
f : α_1 → β_1
hf : f ∈ t
a : α_1
ha : a ∈ s
⊢ ∃ (i : α_1 → γ),
    (∃ (i_1 : (α_1 → β_1) → α_1 → γ), (∃ a ∈ u, comp a = i_1) ∧ ∃ a ∈ t, i_1 a = i) ∧ ∃ a_1 ∈ s, i a_1 = g (f a)

Tactic:
⟨g ∘ f, ⟨comp g, ⟨g, hg, rfl⟩, f, hf, rfl⟩, a, ha, rfl⟩

Premises used: Function.comp, And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 γ : Type u_1
s : Finset α_1
t : Finset (α_1 → β_1)
u : Finset (β_1 → γ)
g : β_1 → γ
hg : g ∈ u
f : α_1 → β_1
hf : f ∈ t
a : α_1
ha : a ∈ s
⊢ ∃ (i : α_1 → γ),
    (∃ (i_1 : (α_1 → β_1) → α_1 → γ), (∃ a ∈ u, comp a = i_1) ∧ ∃ a ∈ t, i_1 a = i) ∧ ∃ a_1 ∈ s, i a_1 = g (f a)

Tactic:
exact ⟨g ∘ f, ⟨comp g, ⟨g, hg, rfl⟩, f, hf, rfl⟩, a, ha, rfl⟩
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 γ : Type u_1
s : Finset α_1
t : Finset (α_1 → β_1)
u : Finset (β_1 → γ)
g : β_1 → γ
hg : g ∈ u
f : α_1 → β_1
hf : f ∈ t
a : α_1
ha : a ∈ s
⊢ ∃ i ∈ u, ∃ (a_1 : β_1), (∃ i ∈ t, ∃ a ∈ s, i a = a_1) ∧ i a_1 = (g ∘ f) a

Tactic:
⟨g, hg, f a, ⟨f, hf, a, ha, rfl⟩, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Finset.Functor
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 γ : Type u_1
s : Finset α_1
t : Finset (α_1 → β_1)
u : Finset (β_1 → γ)
g : β_1 → γ
hg : g ∈ u
f : α_1 → β_1
hf : f ∈ t
a : α_1
ha : a ∈ s
⊢ ∃ i ∈ u, ∃ (a_1 : β_1), (∃ i ∈ t, ∃ a ∈ s, i a = a_1) ∧ i a_1 = (g ∘ f) a

Tactic:
exact ⟨g, hg, f a, ⟨f, hf, a, ha, rfl⟩, rfl⟩