ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f : Finset α → β<VAR>DecidableEq α<GOAL>Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f s ≤ f (insert a s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f : Finset α → β<VAR>DecidableEq α<GOAL>Antitone f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f (insert a s) ≤ f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f : Finset α → β<VAR>DecidableEq α<GOAL>StrictMono f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f s < f (insert a s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f : Finset α → β<VAR>DecidableEq α<GOAL>StrictAnti f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f (insert a s) < f s
<VAR>α : Type u_1<VAR>o : Part α<VAR>Decidable o.Dom<VAR>x : α<GOAL>x ∈ o.toFinset ↔ x ∈ o
<VAR>α : Type u_1<VAR>Decidable Part.none.Dom<GOAL>Part.none.toFinset = ∅
<VAR>α : Type u_1<VAR>a : α<VAR>Decidable (Part.some a).Dom<GOAL>(Part.some a).toFinset = {a}
<VAR>α : Type u_1<VAR>o : Part α<VAR>Decidable o.Dom<GOAL>↑o.toFinset = {x | x ∈ o}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α →. β<VAR>(x : α) → Decidable (f x).Dom<VAR>s : Finset α<VAR>b : β<GOAL>b ∈ Finset.pimage f s ↔ ∃ a ∈ s, b ∈ f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α →. β<VAR>(x : α) → Decidable (f x).Dom<VAR>s : Finset α<GOAL>↑(Finset.pimage f s) = f.image ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset α<VAR>f : α → β<VAR>(x : α) → Decidable (Part.some (f x)).Dom<GOAL>Finset.pimage (fun x => Part.some (f x)) s = Finset.image f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f g : α →. β<VAR>(x : α) → Decidable (f x).Dom<VAR>(x : α) → Decidable (g x).Dom<VAR>s t : Finset α<VAR>h₁ : s = t<VAR>h₂ : ∀ x ∈ t, f x = g x<GOAL>Finset.pimage f s = Finset.pimage g t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α →. β<VAR>(x : α) → Decidable (f x).Dom<VAR>s : Finset α<GOAL>Finset.pimage f s = Finset.image (fun x => (f ↑x).get ⋯) (Finset.filter (fun x => (f x).Dom) s).attach
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α →. β<VAR>(x : α) → Decidable (f x).Dom<VAR>s t : Finset α<VAR>DecidableEq α<GOAL>Finset.pimage f (s ∪ t) = Finset.pimage f s ∪ Finset.pimage f t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α →. β<VAR>(x : α) → Decidable (f x).Dom<GOAL>Finset.pimage f ∅ = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α →. β<VAR>(x : α) → Decidable (f x).Dom<VAR>s : Finset α<VAR>t : Finset β<GOAL>Finset.pimage f s ⊆ t ↔ ∀ x ∈ s, ∀ y ∈ f x, y ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α →. β<VAR>(x : α) → Decidable (f x).Dom<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>Finset.pimage f s ⊆ Finset.pimage f t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α →. β<VAR>(x : α) → Decidable (f x).Dom<VAR>s t : Finset α<VAR>DecidableEq α<GOAL>Finset.pimage f (s ∩ t) ⊆ Finset.pimage f s ∩ Finset.pimage f t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<GOAL>(s ×ˢ t).val = s.val ×ˢ t.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>p : α × β<GOAL>p ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b : β<VAR>ha : a ∈ s<VAR>hb : b ∈ t<GOAL>(a, b) ∈ s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<GOAL>↑(s ×ˢ t) = ↑s ×ˢ ↑t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>DecidableEq α<GOAL>Finset.image Prod.fst (s ×ˢ t) ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>DecidableEq β<GOAL>Finset.image Prod.snd (s ×ˢ t) ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>DecidableEq α<VAR>ht : t.Nonempty<GOAL>Finset.image Prod.fst (s ×ˢ t) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>DecidableEq β<VAR>ht : s.Nonempty<GOAL>Finset.image Prod.snd (s ×ˢ t) = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>s : Finset (α × β)<GOAL>s ⊆ Finset.image Prod.fst s ×ˢ Finset.image Prod.snd s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>hs : s ⊆ s'<VAR>ht : t ⊆ t'<GOAL>s ×ˢ t ⊆ s' ×ˢ t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s' : Finset α<VAR>t : Finset β<VAR>hs : s ⊆ s'<GOAL>s ×ˢ t ⊆ s' ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t t' : Finset β<VAR>ht : t ⊆ t'<GOAL>s ×ˢ t ⊆ s ×ˢ t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<GOAL>Finset.map { toFun := Prod.swap, inj' := ⋯ } (t ×ˢ s) = s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq (α × β)<VAR>s : Finset α<VAR>t : Finset β<GOAL>Finset.image Prod.swap (t ×ˢ s) = s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq (α × β)<VAR>s : Finset α<VAR>t : Finset β<GOAL>s ×ˢ t = s.biUnion fun a => Finset.image (fun b => (a, b)) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq (α × β)<VAR>s : Finset α<VAR>t : Finset β<GOAL>s ×ˢ t = t.biUnion fun b => Finset.image (fun a => (a, b)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>DecidableEq γ<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α × β → Finset γ<GOAL>(s ×ˢ t).biUnion f = s.biUnion fun a => t.biUnion fun b => f (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<GOAL>(s ×ˢ t).card = s.card * t.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<GOAL>(s ×ˢ t).Nontrivial ↔ s.Nonempty ∧ t.Nonempty ∧ (s.Nontrivial ∨ t.Nontrivial)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>p : α → Prop<VAR>q : β → Prop<VAR>DecidablePred p<VAR>DecidablePred q<GOAL>Finset.filter (fun x => p x.1 ∧ q x.2) (s ×ˢ t) = Finset.filter p s ×ˢ Finset.filter q t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Finset.filter (fun x => p x.1) (s ×ˢ t) = Finset.filter p s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>q : β → Prop<VAR>DecidablePred q<GOAL>Finset.filter (fun x => q x.2) (s ×ˢ t) = s ×ˢ Finset.filter q t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>p : α → Prop<VAR>q : β → Prop<VAR>DecidablePred p<VAR>DecidablePred q<GOAL>(Finset.filter (fun x => p x.1 = q x.2) (s ×ˢ t)).card = (Finset.filter p s).card * (Finset.filter q t).card + (Finset.filter (fun x => ¬p x) s).card * (Finset.filter (fun x => ¬q x) t).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Finset β<GOAL>∅ ×ˢ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<GOAL>s ×ˢ ∅ = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>(s ×ˢ t).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>h : (s ×ˢ t).Nonempty<GOAL>s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>h : (s ×ˢ t).Nonempty<GOAL>t.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<GOAL>(s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<GOAL>s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Finset β<VAR>a : α<GOAL>{a} ×ˢ t = Finset.map { toFun := Prod.mk a, inj' := ⋯ } t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>b : β<GOAL>s ×ˢ {b} = Finset.map { toFun := fun i => (i, b), inj' := ⋯ } s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s' : Finset α<VAR>t : Finset β<VAR>DecidableEq α<VAR>DecidableEq β<GOAL>(s ∪ s') ×ˢ t = s ×ˢ t ∪ s' ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t t' : Finset β<VAR>DecidableEq α<VAR>DecidableEq β<GOAL>s ×ˢ (t ∪ t') = s ×ˢ t ∪ s ×ˢ t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s' : Finset α<VAR>t : Finset β<VAR>DecidableEq α<VAR>DecidableEq β<GOAL>(s ∩ s') ×ˢ t = s ×ˢ t ∩ s' ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t t' : Finset β<VAR>DecidableEq α<VAR>DecidableEq β<GOAL>s ×ˢ (t ∩ t') = s ×ˢ t ∩ s ×ˢ t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>DecidableEq α<VAR>DecidableEq β<GOAL>s ×ˢ t ∩ s' ×ˢ t' = (s ∩ s') ×ˢ (t ∩ t')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s' : Finset α<VAR>t t' : Finset β<GOAL>Disjoint (s ×ˢ t) (s' ×ˢ t') ↔ Disjoint s s' ∨ Disjoint t t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s s' : Finset α<VAR>t : Finset β<VAR>hs : Disjoint s s'<GOAL>s.disjUnion s' hs ×ˢ t = (s ×ˢ t).disjUnion (s' ×ˢ t) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t t' : Finset β<VAR>ht : Disjoint t t'<GOAL>s ×ˢ t.disjUnion t' ht = (s ×ˢ t).disjUnion (s ×ˢ t') ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>x : α × α<GOAL>x ∈ s.diag ↔ x.1 ∈ s ∧ x.1 = x.2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>x : α × α<GOAL>x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>↑s.offDiag = (↑s).offDiag
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s.diag.card = s.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s.offDiag.card = s.card * s.card - s.card
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>Monotone Finset.diag
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>Monotone Finset.offDiag
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>∅.diag = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>∅.offDiag = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s.diag ∪ s.offDiag = s ×ˢ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Disjoint s.diag s.offDiag
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s ×ˢ s \ s.diag = s.offDiag
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s ×ˢ s \ s.offDiag = s.diag
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∩ t).diag = s.diag ∩ t.diag
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∩ t).offDiag = s.offDiag ∩ t.offDiag
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∪ t).diag = s.diag ∪ t.diag
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : Disjoint s t<GOAL>(s ∪ t).offDiag = s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>{a}.offDiag = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>{a}.diag = {(a, a)}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>(insert a s).diag = insert (a, a) s.diag
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>has : a ∉ s<GOAL>(insert a s).offDiag = s.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a}
<VAR>ι : Type u_4<VAR>PartialOrder ι<VAR>DecidableEq ι<VAR>DecidableRel LE.le<VAR>DecidableRel LT.lt<VAR>s : Finset ι<GOAL>Finset.filter (fun i => i.1 < i.2) s.offDiag = Finset.filter (fun i => i.1 ≤ i.2) s.offDiag
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>a : α<GOAL>s ⋖ a ::ₘ s
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>h : s ⋖ t<GOAL>∃ a, a ::ₘ s = t
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>s ⋖ t ↔ ∃ a, a ::ₘ s = t
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>h : s ⋖ t<GOAL>Multiset.card s ⋖ Multiset.card t
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>IsAtom s ↔ ∃ a, s = {a}
<VAR>α : Type u_1<VAR>a : α<GOAL>IsAtom {a}
<VAR>α : Type u_1<VAR>m : Multiset α<GOAL>grade ℕ m = Multiset.card m
<VAR>α : Type u_1<GOAL>(Set.range Finset.val).OrdConnected
<VAR>α : Type u_1<GOAL>(Set.range Finset.toSet).OrdConnected
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>s.val ⩿ t.val ↔ s ⩿ t
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>s.val ⋖ t.val ↔ s ⋖ t
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>↑s ⩿ ↑t ↔ s ⩿ t
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>↑s ⋖ ↑t ↔ s ⋖ t
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∉ s<GOAL>s ⋖ Finset.cons a s ha
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>h : s ⋖ t<GOAL>∃ a, ∃ (ha : a ∉ s), Finset.cons a s ha = t
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>s ⋖ t ↔ ∃ a, ∃ (ha : a ∉ s), Finset.cons a s ha = t
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>h : s ⋖ t<GOAL>s.card ⋖ t.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>s ⩿ insert a s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>s.erase a ⩿ s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>DecidableEq α<VAR>ha : a ∉ s<GOAL>s ⋖ insert a s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>DecidableEq α<VAR>ha : a ∈ s<GOAL>s.erase a ⋖ s
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>DecidableEq α<VAR>h : s ⋖ t<GOAL>∃ a ∉ s, insert a s = t
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>DecidableEq α<VAR>h : s ⋖ t<GOAL>∃ a ∈ t, t.erase a = s
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>DecidableEq α<GOAL>s ⋖ t ↔ ∃ a ∉ s, insert a s = t
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>DecidableEq α<GOAL>t ⋖ s ↔ t ⊆ s ∧ (s \ t).card = 1
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>DecidableEq α<GOAL>s ⋖ t ↔ ∃ a ∈ t, t.erase a = s
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>IsAtom s ↔ ∃ a, s = {a}
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>a : α<GOAL>IsCoatom {a}ᶜ
<VAR>α : Type u_1<VAR>s : Finset α<VAR>Fintype α<VAR>DecidableEq α<GOAL>IsCoatom s ↔ ∃ a, s = {a}ᶜ
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>grade (Multiset α) s = s.val
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>grade ℕ s = s.card
<VAR>α : Type u_1<GOAL>(Set.range singleton).PairwiseDisjoint id
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s : Set ι<VAR>f : ι → Finset α<VAR>hs : s.PairwiseDisjoint f<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>a : α<VAR>hai : a ∈ f i<VAR>haj : a ∈ f j<GOAL>i = j
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>f : ι → α<VAR>hs : (↑s).PairwiseDisjoint f<VAR>g : ι → ι<VAR>hf : ∀ (a : ι), f (g a) ≤ f a<GOAL>(↑(Finset.image g s)).PairwiseDisjoint f
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<VAR>hs : (↑s).PairwiseDisjoint f<GOAL>(↑s.attach).PairwiseDisjoint (f ∘ Subtype.val)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>Lattice α<VAR>OrderBot α<VAR>s : Set ι'<VAR>g : ι' → Finset ι<VAR>f : ι → α<VAR>hs : s.PairwiseDisjoint fun i' => (g i').sup f<VAR>hg : ∀ i ∈ s, (↑(g i)).PairwiseDisjoint f<GOAL>(⋃ i ∈ s, ↑(g i)).PairwiseDisjoint f
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>r : α → α → Prop<VAR>l : List α<VAR>hl : (↑l.toFinset).Pairwise r<VAR>hn : l.Nodup<GOAL>List.Pairwise r l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>r : α → α → Prop<VAR>l : List α<VAR>hn : l.Nodup<VAR>hs : Symmetric r<GOAL>(↑l.toFinset).Pairwise r ↔ List.Pairwise r l
<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>DecidableEq ι<VAR>l : List ι<VAR>f : ι → α<VAR>hl : (↑l.toFinset).PairwiseDisjoint f<VAR>hn : l.Nodup<GOAL>List.Pairwise (Disjoint on f) l
<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>DecidableEq ι<VAR>l : List ι<VAR>f : ι → α<VAR>hn : l.Nodup<GOAL>(↑l.toFinset).PairwiseDisjoint f ↔ List.Pairwise (Disjoint on f) l
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>c : γ<GOAL>c ∈ Finset.image₂ f s t ↔ ∃ a ∈ s, ∃ b ∈ t, f a b = c
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<GOAL>↑(Finset.image₂ f s t) = Set.image2 f ↑s ↑t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<GOAL>(Finset.image₂ f s t).card ≤ s.card * t.card
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<GOAL>(Finset.image₂ f s t).card = s.card * t.card ↔ Set.InjOn (fun x => f x.1 x.2) (↑s ×ˢ ↑t)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>hf : Function.Injective2 f<VAR>s : Finset α<VAR>t : Finset β<GOAL>(Finset.image₂ f s t).card = s.card * t.card
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b : β<VAR>ha : a ∈ s<VAR>hb : b ∈ t<GOAL>f a b ∈ Finset.image₂ f s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b : β<VAR>hf : Function.Injective2 f<GOAL>f a b ∈ Finset.image₂ f s t ↔ a ∈ s ∧ b ∈ t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>hs : s ⊆ s'<VAR>ht : t ⊆ t'<GOAL>Finset.image₂ f s t ⊆ Finset.image₂ f s' t'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t t' : Finset β<VAR>ht : t ⊆ t'<GOAL>Finset.image₂ f s t ⊆ Finset.image₂ f s t'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s s' : Finset α<VAR>t : Finset β<VAR>hs : s ⊆ s'<GOAL>Finset.image₂ f s t ⊆ Finset.image₂ f s' t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>b : β<VAR>hb : b ∈ t<GOAL>Finset.image (fun a => f a b) s ⊆ Finset.image₂ f s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>ha : a ∈ s<GOAL>Finset.image (fun b => f a b) t ⊆ Finset.image₂ f s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>p : γ → Prop<GOAL>(∀ z ∈ Finset.image₂ f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>u : Finset γ<GOAL>Finset.image₂ f s t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>u : Finset γ<GOAL>Finset.image₂ f s t ⊆ u ↔ ∀ a ∈ s, Finset.image (fun b => f a b) t ⊆ u
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>u : Finset γ<GOAL>Finset.image₂ f s t ⊆ u ↔ ∀ b ∈ t, Finset.image (fun a => f a b) s ⊆ u
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<GOAL>(Finset.image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>(Finset.image₂ f s t).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>h : (Finset.image₂ f s t).Nonempty<GOAL>s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>h : (Finset.image₂ f s t).Nonempty<GOAL>t.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>t : Finset β<GOAL>Finset.image₂ f ∅ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<GOAL>Finset.image₂ f s ∅ = ∅
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<GOAL>Finset.image₂ f s t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>t : Finset β<VAR>a : α<GOAL>Finset.image₂ f {a} t = Finset.image (fun b => f a b) t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>b : β<GOAL>Finset.image₂ f s {b} = Finset.image (fun a => f a b) s
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>t : Finset β<VAR>a : α<GOAL>Finset.image₂ f {a} t = Finset.image (f a) t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>a : α<VAR>b : β<GOAL>Finset.image₂ f {a} {b} = {f a b}
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s s' : Finset α<VAR>t : Finset β<VAR>DecidableEq α<GOAL>Finset.image₂ f (s ∪ s') t = Finset.image₂ f s t ∪ Finset.image₂ f s' t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t t' : Finset β<VAR>DecidableEq β<GOAL>Finset.image₂ f s (t ∪ t') = Finset.image₂ f s t ∪ Finset.image₂ f s t'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>DecidableEq α<GOAL>Finset.image₂ f (insert a s) t = Finset.image (fun b => f a b) t ∪ Finset.image₂ f s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>b : β<VAR>DecidableEq β<GOAL>Finset.image₂ f s (insert b t) = Finset.image (fun a => f a b) s ∪ Finset.image₂ f s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s s' : Finset α<VAR>t : Finset β<VAR>DecidableEq α<VAR>hf : Function.Injective2 f<GOAL>Finset.image₂ f (s ∩ s') t = Finset.image₂ f s t ∩ Finset.image₂ f s' t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t t' : Finset β<VAR>DecidableEq β<VAR>hf : Function.Injective2 f<GOAL>Finset.image₂ f s (t ∩ t') = Finset.image₂ f s t ∩ Finset.image₂ f s t'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s s' : Finset α<VAR>t : Finset β<VAR>DecidableEq α<GOAL>Finset.image₂ f (s ∩ s') t ⊆ Finset.image₂ f s t ∩ Finset.image₂ f s' t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t t' : Finset β<VAR>DecidableEq β<GOAL>Finset.image₂ f s (t ∩ t') ⊆ Finset.image₂ f s t ∩ Finset.image₂ f s t'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f f' : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b<GOAL>Finset.image₂ f s t = Finset.image₂ f' s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f f' : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>h : ∀ (a : α) (b : β), f a b = f' a b<GOAL>Finset.image₂ f s t = Finset.image₂ f' s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>t : Finset β<VAR>a : α<VAR>hf : Function.Injective (f a)<GOAL>(Finset.image₂ f {a} t).card = t.card
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>b : β<VAR>hf : Function.Injective fun a => f a b<GOAL>(Finset.image₂ f s {b}).card = s.card
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>a : α<VAR>DecidableEq β<VAR>t₁ t₂ : Finset β<VAR>hf : Function.Injective (f a)<GOAL>Finset.image₂ f {a} (t₁ ∩ t₂) = Finset.image₂ f {a} t₁ ∩ Finset.image₂ f {a} t₂
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>b : β<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<VAR>hf : Function.Injective fun a => f a b<GOAL>Finset.image₂ f (s₁ ∩ s₂) {b} = Finset.image₂ f s₁ {b} ∩ Finset.image₂ f s₂ {b}
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>t : Finset β<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>hf : ∀ (a : α), Function.Injective (f a)<GOAL>t.card ≤ (Finset.image₂ f s t).card
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>ht : t.Nonempty<VAR>hf : ∀ (b : β), Function.Injective fun a => f a b<GOAL>s.card ≤ (Finset.image₂ f s t).card
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<GOAL>(s.biUnion fun a => Finset.image (f a) t) = Finset.image₂ f s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<GOAL>(t.biUnion fun b => Finset.image (fun a => f a b) s) = Finset.image₂ f s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq γ<VAR>DecidableEq δ<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β → γ<VAR>g : γ → δ<GOAL>Finset.image g (Finset.image₂ f s t) = Finset.image₂ (fun a b => g (f a b)) s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq γ<VAR>DecidableEq δ<VAR>s : Finset α<VAR>t : Finset β<VAR>f : γ → β → δ<VAR>g : α → γ<GOAL>Finset.image₂ f (Finset.image g s) t = Finset.image₂ (fun a b => f (g a) b) s t