awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
empty : r c (fold op b f ∅) ↔ r c b ∧ ∀ (x : α), Membership.mem (γ := Finset α) ∅ x → r c (f x)
⊢ r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
have insert : ∀ (a : α) (s : Finset α) (ha_1 : a ∉ s) (IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)),
  r c (fold op b f (insert a s)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)
Tactic: classical
    induction s using Finset.induction_on with
    | empty => simp
    | insert a s ha IH =>
      rw [Finset.fold_insert ha, hr, IH, ← and_assoc, @and_comm (r c (f a)), and_assoc]
      simp
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha_1 : Std.Associative op
f : α → β
b : β
s_1 : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
⊢ r c (fold op b f (insert a s)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)
have insert : (r c b ∨ r c (f a) ∨ ∃ x ∈ s, r c (f x)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)
Tactic: rw [Finset.fold_insert ha, hr, IH, ← or_assoc, @or_comm (r c (f a)), or_assoc]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
have empty : r c (fold op b f ∅) ↔ r c b ∨ ∃ (x : α), Membership.mem (γ := Finset α) ∅ x ∧ r c (f x)
Tactic: induction s using Finset.induction_on with
    | empty => simp
    | insert a s ha IH =>
      rw [Finset.fold_insert ha, hr, IH, ← or_assoc, @or_comm (r c (f a)), or_assoc]
      simp
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
empty : r c (fold op b f ∅) ↔ r c b ∨ ∃ (x : α), Membership.mem (γ := Finset α) ∅ x ∧ r c (f x)
⊢ r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
have insert : ∀ (a : α) (s : Finset α) (ha_1 : a ∉ s) (IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)),
  r c (fold op b f (insert a s)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)
Tactic: induction s using Finset.induction_on with
    | empty => simp
    | insert a s ha IH =>
      rw [Finset.fold_insert ha, hr, IH, ← or_assoc, @or_comm (r c (f a)), or_assoc]
      simp
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
have empty : r c (fold op b f ∅) ↔ r c b ∨ ∃ (x : α), Membership.mem (γ := Finset α) ∅ x ∧ r c (f x)
Tactic: classical
    induction s using Finset.induction_on with
    | empty => simp
    | insert a s ha IH =>
      rw [Finset.fold_insert ha, hr, IH, ← or_assoc, @or_comm (r c (f a)), or_assoc]
      simp
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
empty : r c (fold op b f ∅) ↔ r c b ∨ ∃ (x : α), Membership.mem (γ := Finset α) ∅ x ∧ r c (f x)
⊢ r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
have insert : ∀ (a : α) (s : Finset α) (ha_1 : a ∉ s) (IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)),
  r c (fold op b f (insert a s)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)
Tactic: classical
    induction s using Finset.induction_on with
    | empty => simp
    | insert a s ha IH =>
      rw [Finset.fold_insert ha, hr, IH, ← or_assoc, @or_comm (r c (f a)), or_assoc]
      simp
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
inst : DecidableEq α
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 a s) = insert a s
have insert : {a} ∪ fold (fun (x1 x2 : Finset α) ↦ x1 ∪ x2) ∅ singleton s = insert a s
Tactic: rw [fold_insert has, ih, insert_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
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
⊢ fold (fun (x1 x2 : Finset α) ↦ x1 ∪ x2) ∅ singleton (Insert.insert a s) = Insert.insert a s
have insert₁ : {a} ∪ s = Insert.insert a s
Tactic: rw [fold_insert has, ih, insert_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
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
⊢ fold (fun (x1 x2 : Finset α) ↦ x1 ∪ x2) ∅ singleton (Insert.insert a s) = Insert.insert a s
have insert₂ : {a} ∪ s = {a} ∪ s
Tactic: rw [fold_insert has, ih, insert_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ fold (fun (x1 x2 : Finset α) ↦ x1 ∪ x2) ∅ singleton s = s
have empty : Eq (α := Finset α) (fold (fun (x1 x2 : Finset α) ↦ x1 ∪ x2) ∅ singleton ∅) ∅
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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
empty : Eq (α := Finset α) (fold (fun (x1 x2 : Finset α) ↦ x1 ∪ x2) ∅ singleton ∅) ∅
⊢ fold (fun (x1 x2 : Finset α) ↦ x1 ∪ x2) ∅ singleton s = s
have 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 a s) = insert a 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
⊢ fold min b f s ≤ c ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c
have change : c ≥ fold min b f s ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c
Tactic: change _ ≥ _ ↔ _
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
⊢ c ≥ fold min b f s ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c
have hr : ∀ {x y z : β}, x ≥ min y z ↔ x ≥ y ∨ x ≥ z
Tactic: apply fold_op_rel_iff_or
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c x y z : β
⊢ x ≥ min y z ↔ x ≥ y ∨ x ≥ z
have hr : min y z ≤ x ↔ x ≥ y ∨ x ≥ z
Tactic: change _ ≤ _ ↔ _
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
⊢ fold min b f s < c ↔ b < c ∨ ∃ x ∈ s, f x < c
have change : c > fold min b f s ↔ b < c ∨ ∃ x ∈ s, f x < c
Tactic: change _ > _ ↔ _
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
⊢ c > fold min b f s ↔ b < c ∨ ∃ x ∈ s, f x < c
have hr : ∀ {x y z : β}, x > min y z ↔ x > y ∨ x > z
Tactic: apply fold_op_rel_iff_or
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c x y z : β
⊢ x > min y z ↔ x > y ∨ x > z
have hr : min y z < x ↔ x > y ∨ x > z
Tactic: change _ < _ ↔ _
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
⊢ fold max b f s ≤ c ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c
have change : c ≥ fold max b f s ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c
Tactic: change _ ≥ _ ↔ _
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
⊢ c ≥ fold max b f s ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c
have hr : ∀ {x y z : β}, x ≥ max y z ↔ x ≥ y ∧ x ≥ z
Tactic: apply fold_op_rel_iff_and
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c x y z : β
⊢ x ≥ max y z ↔ x ≥ y ∧ x ≥ z
have hr : max y z ≤ x ↔ x ≥ y ∧ x ≥ z
Tactic: change _ ≤ _ ↔ _
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
⊢ fold max b f s < c ↔ b < c ∧ ∀ x ∈ s, f x < c
have change : c > fold max b f s ↔ b < c ∧ ∀ x ∈ s, f x < c
Tactic: change _ > _ ↔ _
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c : β
⊢ c > fold max b f s ↔ b < c ∧ ∀ x ∈ s, f x < c
have hr : ∀ {x y z : β}, x > max y z ↔ x > y ∧ x > z
Tactic: apply fold_op_rel_iff_and
-- Lean 4 proof step from Mathlib.Data.Finset.Fold (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst : LinearOrder β
c x y z : β
⊢ x > max y z ↔ x > y ∧ x > z
have hr : max y z < x ↔ x > y ∧ x > z
Tactic: change _ < _ ↔ _
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
inst : (P : Prop) → Decidable P
α β γ : Type u
f : α → β → γ
s : Finset α
t : Finset β
⊢ image₂ f s t = f <$> s <*> t
have h : ∀ (a : γ), a ∈ image₂ f s t ↔ a ∈ f <$> s <*> t
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
⊢ s <* t = const β_1 <$> s <*> t
have rw : (if t = ∅ then ∅ else s) = (image (const β_1) s).sup fun (f : β_1 → α_1) ↦ image f t
Tactic: rw [seq_def, fmap_def, seqLeft_def]
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
⊢ (if t = ∅ then ∅ else s) = (image (const β_1) s).sup fun (f : β_1 → α_1) ↦ image f t
have inl : (if Eq.{u_1 + 1} (α := Finset β_1) ∅ ∅ then ∅ else s) = (image (const β_1) s).sup fun (f : β_1 → α_1) ↦ image f ∅
Tactic: obtain rfl | ht := t.eq_empty_or_nonempty
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
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 ∅
⊢ (if t = ∅ then ∅ else s) = (image (const β_1) s).sup fun (f : β_1 → α_1) ↦ image f t
have inr : ∀ (ht : t.Nonempty), (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
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
⊢ (if Eq.{u_1 + 1} (α := Finset β_1) ∅ ∅ then ∅ else s) = (image (const β_1) s).sup fun (f : β_1 → α_1) ↦ image f ∅
have inl : Eq (α := Finset α_1) ∅ ((image (const β_1) s).sup fun (f : β_1 → α_1) ↦ ∅)
Tactic: simp_rw [image_empty, if_true]
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
ht : t.Nonempty
⊢ (if t = ∅ then ∅ else s) = (image (const β_1) s).sup fun (f : β_1 → α_1) ↦ image f t
have 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
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
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 ∈ if t = ∅ then ∅ else s) ↔
    Membership.mem (γ := Finset α_1) ((image (const β_1) s).sup fun (f : β_1 → α_1) ↦ image f t) a
have inr : a ∈ s ↔ ∃ i ∈ image (const β_1) s, a ∈ image i t
Tactic: rw [if_neg ht.ne_empty, mem_sup]
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
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
have inr : (∃ i ∈ image (const β_1) s, a ∈ image i t) → a ∈ s
Tactic: refine ⟨fun ha => ⟨const _ a, mem_image_of_mem _ ha, mem_image_const_self.2 ht⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (hypothesis)
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
have hf₁ : ∃ a ∈ s, const β_1 a = f
Tactic: rw [mem_image] at hf ha
Cleared hypotheses: hf, ha
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (hypothesis)
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 ∈ s
have ha₁ : ∃ a_1 ∈ t, f a_1 = a
Tactic: rw [mem_image] at hf ha
Cleared hypotheses: hf, ha
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
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
⊢ a ∈ s
have inr : ∀ (b : α_1) (hb : b ∈ s) (ha : ∃ a_1 ∈ t, const β_1 b a_1 = a), a ∈ s
Tactic: obtain ⟨b, hb, rfl⟩ := hf
Cleared hypotheses: f, hf, ha
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
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
⊢ a ∈ s
have inr : ∀ w ∈ t, const β_1 b w ∈ s
Tactic: obtain ⟨_, _, rfl⟩ := ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
⊢ Eq (α := Finset β_1) (s *> t) (const α_1 id <$> s <*> t)
have rw : (if s = ∅ then ∅ else t) = sup (image (const α_1 id) s) fun (f : β_1 → β_1) ↦ image f t
Tactic: rw [seq_def, fmap_def, seqRight_def]
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
⊢ (if s = ∅ then ∅ else t) = sup (image (const α_1 id) s) fun (f : β_1 → β_1) ↦ image f t
have inl : (if Eq.{u_1 + 1} (α := Finset α_1) ∅ ∅ then ∅ else t) = sup (image (const α_1 id) ∅) fun (f : β_1 → β_1) ↦ image f t
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
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
⊢ (if s = ∅ then ∅ else t) = sup (image (const α_1 id) s) fun (f : β_1 → β_1) ↦ image f t
have inr : ∀ (hs : s.Nonempty), (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
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
t : Finset β_1
⊢ (if Eq.{u_1 + 1} (α := Finset α_1) ∅ ∅ then ∅ else t) = sup (image (const α_1 id) ∅) fun (f : β_1 → β_1) ↦ image f t
have inl : Eq (α := Finset β_1) ∅ (sup (image (const α_1 id) ∅) fun (f : β_1 → β_1) ↦ image f t)
Tactic: rw [if_pos rfl, image_empty, sup_empty, bot_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
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)
⊢ (if Eq.{u_1 + 1} (α := Finset α_1) ∅ ∅ then ∅ else t) = sup (image (const α_1 id) ∅) fun (f : β_1 → β_1) ↦ image f t
have inl₁ : Eq.{u_1 + 1} (α := Finset β_1) ∅ (sup ∅ fun (f : β_1 → β_1) ↦ image f t)
Tactic: rw [if_pos rfl, image_empty, sup_empty, bot_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
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)
⊢ (if Eq.{u_1 + 1} (α := Finset α_1) ∅ ∅ then ∅ else t) = sup (image (const α_1 id) ∅) fun (f : β_1 → β_1) ↦ image f t
have inl₂ : Eq.{u_1 + 1} (α := Finset β_1) ∅ ⊥
Tactic: rw [if_pos rfl, image_empty, sup_empty, bot_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
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) ∅ ⊥
⊢ (if Eq.{u_1 + 1} (α := Finset α_1) ∅ ∅ then ∅ else t) = sup (image (const α_1 id) ∅) fun (f : β_1 → β_1) ↦ image f t
have inl₃ : Eq.{u_1 + 1} (α := Finset β_1) ∅ ∅
Tactic: rw [if_pos rfl, image_empty, sup_empty, bot_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
hs : s.Nonempty
⊢ (if s = ∅ then ∅ else t) = sup (image (const α_1 id) s) fun (f : β_1 → β_1) ↦ image f t
have 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
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
hs : s.Nonempty
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
have inr : a ∈ t ↔ ∃ (i : β_1 → β_1), Membership.mem (γ := Finset (β_1 → β_1)) (image (const α_1 id) s) i ∧ a ∈ image i t
Tactic: rw [if_neg hs.ne_empty, mem_sup]
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
hs : s.Nonempty
a : β_1
⊢ a ∈ t ↔ ∃ (i : β_1 → β_1), Membership.mem (γ := Finset (β_1 → β_1)) (image (const α_1 id) s) i ∧ a ∈ image i t
have inr : (∃ (i : β_1 → β_1), Membership.mem (γ := Finset (β_1 → β_1)) (image (const α_1 id) s) i ∧ a ∈ image i t) → a ∈ t
Tactic: refine ⟨fun ha => ⟨id, mem_image_const_self.2 hs, by rwa [image_id]⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (hypothesis)
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 ∈ t
have hf₁ : ∃ a ∈ s, const α_1 id a = f
Tactic: rw [mem_image] at hf ha
Cleared hypotheses: hf, ha
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (hypothesis)
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 ∈ t
have ha₁ : ∃ a_1 ∈ t, f a_1 = a
Tactic: rw [mem_image] at hf ha
Cleared hypotheses: hf, ha
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
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
⊢ a ∈ t
have inr : ∀ (b : β_1) (hb : b ∈ t), f b ∈ t
Tactic: obtain ⟨b, hb, rfl⟩ := ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
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
⊢ f b ∈ t
have inr : ∀ w ∈ s, Membership.mem (α := β_1) t (const α_1 id w b : β_1)
Tactic: obtain ⟨_, _, rfl⟩ := hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 γ : Type u_1
s : Finset α_1
t : Finset (α_1 → β_1)
u : Finset (β_1 → γ)
⊢ u <*> (t <*> s) = comp <$> u <*> t <*> s
have h : ∀ (a : γ), a ∈ u <*> (t <*> s) ↔ a ∈ comp <$> u <*> t <*> s
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 γ : Type u_1
s : Finset α_1
t : Finset (α_1 → β_1)
u : Finset (β_1 → γ)
a : γ
⊢ a ∈ u <*> (t <*> s) ↔ a ∈ comp <$> u <*> t <*> s
have 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
Tactic: simp_rw [seq_def, fmap_def]
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 γ : Type u_1
s : Finset α_1
t : Finset (α_1 → β_1)
u : Finset (β_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
have 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
Tactic: simp only [mem_sup, mem_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 γ : Type u_1
s : Finset α_1
t : Finset (α_1 → β_1)
u : Finset (β_1 → γ)
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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
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
⊢ (∃ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
⊢ Eq (α := Finset (α_1 × β_1)) (Prod.mk <$> s <*> t) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> t <*> s)
have simp_rw : Eq (α := Finset (α_1 × β_1)) (s.biUnion ((fun (f : β_1 → α_1 × β_1) ↦ image f t) ∘ Prod.mk))
  (t.biUnion ((fun (f : α_1 → α_1 × β_1) ↦ image f s) ∘ fun (b : β_1) (a : α_1) ↦ (a, b)))
Tactic: simp_rw [seq_def, fmap_def, sup_image, sup_eq_biUnion]