ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>LocallyFiniteOrder α<VAR>a b c d : α<GOAL>Finset.Ico a b * Finset.Icc c d ⊆ Finset.Ico (a * c) (b * d)
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>LocallyFiniteOrder α<VAR>a b c d : α<GOAL>Finset.Ioc a b * Finset.Ico c d ⊆ Finset.Ioo (a * c) (b * d)
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LT.lt<VAR>LocallyFiniteOrder α<VAR>a b c d : α<GOAL>Finset.Ioc a b + Finset.Ico c d ⊆ Finset.Ioo (a + c) (b + d)
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>LocallyFiniteOrder α<VAR>a b c d : α<GOAL>Finset.Ico a b * Finset.Ioc c d ⊆ Finset.Ioo (a * c) (b * d)
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LT.lt<VAR>LocallyFiniteOrder α<VAR>a b c d : α<GOAL>Finset.Ico a b + Finset.Ioc c d ⊆ Finset.Ioo (a + c) (b + d)
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LT.lt<VAR>LocallyFiniteOrderBot α<VAR>a b : α<GOAL>Finset.Iic a + Finset.Iio b ⊆ Finset.Iio (a + b)
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>LocallyFiniteOrderBot α<VAR>a b : α<GOAL>Finset.Iic a * Finset.Iio b ⊆ Finset.Iio (a * b)
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LT.lt<VAR>LocallyFiniteOrderBot α<VAR>a b : α<GOAL>Finset.Iio a + Finset.Iic b ⊆ Finset.Iio (a + b)
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>LocallyFiniteOrderBot α<VAR>a b : α<GOAL>Finset.Iio a * Finset.Iic b ⊆ Finset.Iio (a * b)
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LT.lt<VAR>LocallyFiniteOrderTop α<VAR>a b : α<GOAL>Finset.Ioi a + Finset.Ici b ⊆ Finset.Ioi (a + b)
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>LocallyFiniteOrderTop α<VAR>a b : α<GOAL>Finset.Ioi a * Finset.Ici b ⊆ Finset.Ioi (a * b)
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>LocallyFiniteOrderTop α<VAR>a b : α<GOAL>Finset.Ici a * Finset.Ioi b ⊆ Finset.Ioi (a * b)
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>DecidableEq α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LT.lt<VAR>LocallyFiniteOrderTop α<VAR>a b : α<GOAL>Finset.Ici a + Finset.Ioi b ⊆ Finset.Ioi (a + b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<GOAL>(s.disjSum t).val = s.val.disjSum t.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Finset β<GOAL>∅.disjSum t = Finset.map Function.Embedding.inr t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<GOAL>s.disjSum ∅ = Finset.map Function.Embedding.inl s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<GOAL>(s.disjSum t).card = s.card + t.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<GOAL>Disjoint (Finset.map Function.Embedding.inl s) (Finset.map Function.Embedding.inr t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<GOAL>(Finset.map Function.Embedding.inl s).disjUnion (Finset.map Function.Embedding.inr t) ⋯ = s.disjSum t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>x : α ⊕ β<GOAL>x ∈ s.disjSum t ↔ (∃ a ∈ s, Sum.inl a = x) ∨ ∃ b ∈ t, Sum.inr b = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<GOAL>Sum.inl a ∈ s.disjSum t ↔ a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>b : β<GOAL>Sum.inr b ∈ s.disjSum t ↔ b ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<GOAL>s.disjSum t = ∅ ↔ s = ∅ ∧ t = ∅
<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₁.disjSum t₁ ⊆ s₂.disjSum t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Finset β<GOAL>Monotone fun s => s.disjSum t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<GOAL>Monotone s.disjSum
<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₁.disjSum t₁ ⊂ s₂.disjSum t₂
<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₁.disjSum t₁ ⊂ s₂.disjSum t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Finset β<GOAL>StrictMono fun s => s.disjSum t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<GOAL>StrictMono s.disjSum
<VAR>n : ℕ<VAR>s : Finset ℕ<VAR>h : ∀ m ∈ s, m < n<VAR>a : Fin n<GOAL>a ∈ s.attachFin h ↔ ↑a ∈ s
<VAR>n : ℕ<VAR>s : Finset ℕ<VAR>h : ∀ m ∈ s, m < n<GOAL>(s.attachFin h).card = s.card
<VAR>n m : ℕ<VAR>hm : n ∣ m<GOAL>ZMod.unitsMap hm = Units.map ↑(ZMod.castHom hm (ZMod n))
<VAR>n m d : ℕ<VAR>hm : n ∣ m<VAR>hd : m ∣ d<GOAL>(ZMod.unitsMap hm).comp (ZMod.unitsMap hd) = ZMod.unitsMap ⋯
<VAR>n : ℕ<GOAL>ZMod.unitsMap ⋯ = MonoidHom.id (ZMod n)ˣ
<VAR>n m : ℕ<VAR>hm : n ∣ m<VAR>a : (ZMod m)ˣ<GOAL>IsUnit (↑a).cast
<VAR>n m : ℕ<VAR>hm : NeZero m<VAR>h : n ∣ m<GOAL>Function.Surjective ⇑(ZMod.unitsMap h)
<VAR>n p : ℕ<VAR>h : p ∈ n.primeFactors<GOAL>¬IsUnit ↑p
<VAR>N : ℕ<VAR>a : ZMod N<GOAL>∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d
<VAR>n : ℕ<VAR>a b c : Fin n<GOAL>a * (b + c) = a * b + a * c
<VAR>n : ℕ<VAR>Fintype (ZMod n)<GOAL>Fintype.card (ZMod n) = n
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Finset β<VAR>hf : Set.InjOn f (f ⁻¹' ↑s)<VAR>x : α<GOAL>x ∈ s.preimage f hf ↔ f x ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Finset β<VAR>hf : Set.InjOn f (f ⁻¹' ↑s)<GOAL>↑(s.preimage f hf) = f ⁻¹' ↑s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>∅.preimage f ⋯ = ∅
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>Fintype α<VAR>Fintype β<VAR>hf : Set.InjOn f (f ⁻¹' ↑Finset.univ)<GOAL>Finset.univ.preimage f hf = Finset.univ
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → β<VAR>s t : Finset β<VAR>hs : Set.InjOn f (f ⁻¹' ↑s)<VAR>ht : Set.InjOn f (f ⁻¹' ↑t)<GOAL>(s ∩ t).preimage f ⋯ = s.preimage f hs ∩ t.preimage f ht
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → β<VAR>s t : Finset β<VAR>hst : Set.InjOn f (f ⁻¹' ↑(s ∪ t))<GOAL>(s ∪ t).preimage f hst = s.preimage f ⋯ ∪ t.preimage f ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq α<VAR>DecidableEq β<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>s : Finset β<VAR>hf : Function.Injective f<GOAL>sᶜ.preimage f ⋯ = (s.preimage f ⋯)ᶜ
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ↪ β<VAR>s : Finset α<GOAL>(Finset.map f s).preimage ⇑f ⋯ = s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>h : Function.Injective f<GOAL>Monotone fun s => s.preimage f ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>hf : Set.InjOn f (f ⁻¹' ↑t)<GOAL>Finset.image f s ⊆ t ↔ s ⊆ t.preimage f hf
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ↪ β<VAR>s : Finset α<VAR>t : Finset β<GOAL>Finset.map f s ⊆ t ↔ s ⊆ t.preimage ⇑f ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset β<VAR>(x : β) → Decidable (x ∈ Set.range f)<VAR>hf : Set.InjOn f (f ⁻¹' ↑s)<GOAL>Finset.image f (s.preimage f hf) = Finset.filter (fun x => x ∈ Set.range f) s
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset β<VAR>hf : Set.BijOn f (f ⁻¹' ↑s) ↑s<GOAL>Finset.image f (s.preimage f ⋯) = s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ↪ β<VAR>s : Finset β<VAR>t : Finset α<VAR>hs : s ⊆ Finset.map f t<GOAL>s.preimage ⇑f ⋯ ⊆ t
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ↪ β<VAR>s : Finset β<VAR>t : Finset α<GOAL>s ⊆ Finset.map f t ↔ ∃ u ⊆ t, s = Finset.map f u
<VAR>α : Type u<VAR>β : α → Type u_1<VAR>DecidableEq α<VAR>s : Finset ((a : α) × β a)<VAR>t : Finset α<GOAL>(t.sigma fun a => s.preimage (Sigma.mk a) ⋯) = Finset.filter (fun a => a.fst ∈ t) s
<VAR>α : Type u<VAR>β : α → Type u_1<VAR>DecidableEq α<VAR>s : Finset ((a : α) × β a)<VAR>t : Finset α<VAR>ht : Finset.image Sigma.fst s ⊆ t<GOAL>(t.sigma fun a => s.preimage (Sigma.mk a) ⋯) = s
<VAR>α : Type u<VAR>β : α → Type u_1<VAR>DecidableEq α<VAR>s : Finset ((a : α) × β a)<GOAL>((Finset.image Sigma.fst s).sigma fun a => s.preimage (Sigma.mk a) ⋯) = s
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddGroup α<VAR>a : α<VAR>AddAction α β<VAR>b : β<VAR>n : ZMod (Function.minimalPeriod (fun x => a +ᵥ x) b)<GOAL>(AddAction.zmultiplesQuotientStabilizerEquiv a b).symm n = n.cast • ↑⟨a, ⋯⟩
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Group α<VAR>a : α<VAR>MulAction α β<VAR>b : β<VAR>n : ZMod (Function.minimalPeriod (fun x => a • x) b)<GOAL>(MulAction.zpowersQuotientStabilizerEquiv a b).symm n = ↑⟨a, ⋯⟩ ^ n.cast
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Group α<VAR>a : α<VAR>MulAction α β<VAR>b : β<VAR>k : ZMod (Function.minimalPeriod (fun x => a • x) b)<GOAL>(MulAction.orbitZPowersEquiv a b).symm k = ⟨a, ⋯⟩ ^ k.cast • ⟨b, ⋯⟩
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddGroup α<VAR>a : α<VAR>AddAction α β<VAR>b : β<VAR>k : ZMod (Function.minimalPeriod (fun x => a +ᵥ x) b)<GOAL>(AddAction.orbitZMultiplesEquiv a b).symm k = k.cast • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Group α<VAR>a : α<VAR>MulAction α β<VAR>b : β<VAR>k : ℤ<GOAL>(MulAction.orbitZPowersEquiv a b).symm ↑k = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>AddGroup α<VAR>a : α<VAR>AddAction α β<VAR>b : β<VAR>k : ℤ<GOAL>(AddAction.orbitZMultiplesEquiv a b).symm ↑k = k • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddGroup α<VAR>a : α<VAR>AddAction α β<VAR>b : β<VAR>Fintype ↑(AddAction.orbit (↥(AddSubgroup.zmultiples a)) b)<GOAL>Function.minimalPeriod (fun x => a +ᵥ x) b = Fintype.card ↑(AddAction.orbit (↥(AddSubgroup.zmultiples a)) b)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Group α<VAR>a : α<VAR>MulAction α β<VAR>b : β<VAR>Fintype ↑(MulAction.orbit (↥(Subgroup.zpowers a)) b)<GOAL>Function.minimalPeriod (fun x => a • x) b = Fintype.card ↑(MulAction.orbit (↥(Subgroup.zpowers a)) b)
<VAR>α : Type u_3<VAR>Group α<VAR>a : α<GOAL>Nat.card ↥(Subgroup.zpowers a) = orderOf a
<VAR>α : Type u_3<VAR>AddGroup α<VAR>a : α<GOAL>Nat.card ↥(AddSubgroup.zmultiples a) = addOrderOf a
<VAR>α : Type u_3<VAR>AddGroup α<VAR>a : α<GOAL>(↑(AddSubgroup.zmultiples a)).Finite ↔ IsOfFinAddOrder a
<VAR>α : Type u_3<VAR>Group α<VAR>a : α<GOAL>(↑(Subgroup.zpowers a)).Finite ↔ IsOfFinOrder a
<VAR>α : Type u_3<VAR>Group α<VAR>a : α<GOAL>(↑(Subgroup.zpowers a)).Infinite ↔ ¬IsOfFinOrder a
<VAR>α : Type u_3<VAR>AddGroup α<VAR>a : α<GOAL>(↑(AddSubgroup.zmultiples a)).Infinite ↔ ¬IsOfFinAddOrder a
<VAR>α : Type u_1<VAR>s t : Set α<VAR>OrderedCancelCommMonoid α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>(s * t).IsPWO
<VAR>α : Type u_1<VAR>s t : Set α<VAR>OrderedCancelAddCommMonoid α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>(s + t).IsPWO
<VAR>α : Type u_1<VAR>s t : Set α<VAR>LinearOrderedCancelCommMonoid α<VAR>hs : s.IsWF<VAR>ht : t.IsWF<GOAL>(s * t).IsWF
<VAR>α : Type u_1<VAR>s t : Set α<VAR>LinearOrderedCancelAddCommMonoid α<VAR>hs : s.IsWF<VAR>ht : t.IsWF<GOAL>(s + t).IsWF
<VAR>α : Type u_1<VAR>s t : Set α<VAR>LinearOrderedCancelAddCommMonoid α<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hsn : s.Nonempty<VAR>htn : t.Nonempty<GOAL>⋯.min ⋯ = hs.min hsn + ht.min htn
<VAR>α : Type u_1<VAR>s t : Set α<VAR>LinearOrderedCancelCommMonoid α<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hsn : s.Nonempty<VAR>htn : t.Nonempty<GOAL>⋯.min ⋯ = hs.min hsn * ht.min htn
<VAR>α : Type u_1<VAR>OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<VAR>x : α × α<GOAL>x ∈ Finset.mulAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<VAR>x : α × α<GOAL>x ∈ Finset.addAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 + x.2 = a
<VAR>α : Type u_1<VAR>OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<VAR>u : Set α<VAR>hu : u.IsPWO<VAR>h : u ⊆ s<GOAL>Finset.mulAntidiagonal hu ht a ⊆ Finset.mulAntidiagonal hs ht a
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<VAR>u : Set α<VAR>hu : u.IsPWO<VAR>h : u ⊆ s<GOAL>Finset.addAntidiagonal hu ht a ⊆ Finset.addAntidiagonal hs ht a
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<VAR>u : Set α<VAR>hu : u.IsPWO<VAR>h : u ⊆ t<GOAL>Finset.addAntidiagonal hs hu a ⊆ Finset.addAntidiagonal hs ht a
<VAR>α : Type u_1<VAR>OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<VAR>u : Set α<VAR>hu : u.IsPWO<VAR>h : u ⊆ t<GOAL>Finset.mulAntidiagonal hs hu a ⊆ Finset.mulAntidiagonal hs ht a
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<VAR>x : α × α<GOAL>x.swap ∈ Finset.addAntidiagonal hs ht a ↔ x ∈ Finset.addAntidiagonal ht hs a
<VAR>α : Type u_1<VAR>OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<VAR>x : α × α<GOAL>x.swap ∈ Finset.mulAntidiagonal hs ht a ↔ x ∈ Finset.mulAntidiagonal ht hs a
<VAR>α : Type u_1<VAR>OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>{a | (Finset.mulAntidiagonal hs ht a).Nonempty} ⊆ s * t
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>{a | (Finset.addAntidiagonal hs ht a).Nonempty} ⊆ s + t
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>{a | (Finset.addAntidiagonal hs ht a).Nonempty}.IsPWO
<VAR>α : Type u_1<VAR>OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>{a | (Finset.mulAntidiagonal hs ht a).Nonempty}.IsPWO
<VAR>α : Type u_2<VAR>LinearOrderedCancelCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hns : s.Nonempty<VAR>hnt : t.Nonempty<GOAL>Finset.mulAntidiagonal ⋯ ⋯ (hs.min hns * ht.min hnt) = {(hs.min hns, ht.min hnt)}
<VAR>α : Type u_2<VAR>LinearOrderedCancelAddCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hns : s.Nonempty<VAR>hnt : t.Nonempty<GOAL>Finset.addAntidiagonal ⋯ ⋯ (hs.min hns + ht.min hnt) = {(hs.min hns, ht.min hnt)}
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f g : (i : ι) → π i<VAR>DecidableEq ι<VAR>j : ι<VAR>(i : ι) → Decidable (i ∈ insert j s)<GOAL>(insert j s).piecewise f g j = f j
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>f g : (i : ι) → π i<VAR>(i : ι) → Decidable (i ∈ ∅)<GOAL>∅.piecewise f g = g
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f g : (i : ι) → π i<VAR>(j : ι) → Decidable (j ∈ s)<VAR>(j : ι) → Decidable (j ∈ ↑s)<GOAL>(↑s).piecewise f g = s.piecewise f g
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f g : (i : ι) → π i<VAR>(j : ι) → Decidable (j ∈ s)<VAR>i : ι<VAR>hi : i ∈ s<GOAL>s.piecewise f g i = f i
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f g : (i : ι) → π i<VAR>(j : ι) → Decidable (j ∈ s)<VAR>i : ι<VAR>hi : i ∉ s<GOAL>s.piecewise f g i = g i
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>(j : ι) → Decidable (j ∈ s)<VAR>f f' g g' : (i : ι) → π i<VAR>hf : ∀ i ∈ s, f i = f' i<VAR>hg : ∀ i ∉ s, g i = g' i<GOAL>s.piecewise f g = s.piecewise f' g'
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f g : (i : ι) → π i<VAR>(j : ι) → Decidable (j ∈ s)<VAR>DecidableEq ι<VAR>i j : ι<VAR>(i : ι) → Decidable (i ∈ insert j s)<VAR>h : i ≠ j<GOAL>(insert j s).piecewise f g i = s.piecewise f g i
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f g : (i : ι) → π i<VAR>(j : ι) → Decidable (j ∈ s)<VAR>DecidableEq ι<VAR>j : ι<VAR>(i : ι) → Decidable (i ∈ insert j s)<GOAL>(insert j s).piecewise f g = Function.update (s.piecewise f g) j (f j)
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f g : (i : ι) → π i<VAR>(j : ι) → Decidable (j ∈ s)<VAR>i : ι<VAR>p : π i → Prop<VAR>hf : p (f i)<VAR>hg : p (g i)<GOAL>p (s.piecewise f g i)
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>f g : (i : ι) → π i<VAR>DecidableEq ι<VAR>i : ι<GOAL>{i}.piecewise f g = Function.update g i (f i)
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s t : Finset ι<VAR>(i : ι) → Decidable (i ∈ s)<VAR>(i : ι) → Decidable (i ∈ t)<VAR>h : s ⊆ t<VAR>f₁ f₂ g : (a : ι) → π a<GOAL>s.piecewise (t.piecewise f₁ f₂) g = s.piecewise f₁ g
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>(j : ι) → Decidable (j ∈ s)<VAR>f₁ f₂ g : (a : ι) → π a<GOAL>s.piecewise (s.piecewise f₁ f₂) g = s.piecewise f₁ g
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s t : Finset ι<VAR>(i : ι) → Decidable (i ∈ s)<VAR>(i : ι) → Decidable (i ∈ t)<VAR>h : t ⊆ s<VAR>f g₁ g₂ : (a : ι) → π a<GOAL>s.piecewise f (t.piecewise g₁ g₂) = s.piecewise f g₂
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>(j : ι) → Decidable (j ∈ s)<VAR>f g₁ g₂ : (a : ι) → π a<GOAL>s.piecewise f (s.piecewise g₁ g₂) = s.piecewise f g₂
<VAR>ι : Type u_1<VAR>β : Type u_3<VAR>DecidableEq ι<VAR>f : ι → β<VAR>i : ι<VAR>v : β<GOAL>Function.update f i v = {i}.piecewise (fun x => v) f
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f g : (i : ι) → π i<VAR>(j : ι) → Decidable (j ∈ s)<VAR>DecidableEq ι<VAR>i : ι<VAR>v : π i<GOAL>Function.update (s.piecewise f g) i v = s.piecewise (Function.update f i v) (Function.update g i v)
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f g : (i : ι) → π i<VAR>(j : ι) → Decidable (j ∈ s)<VAR>DecidableEq ι<VAR>i : ι<VAR>hi : i ∈ s<VAR>v : π i<GOAL>Function.update (s.piecewise f g) i v = s.piecewise (Function.update f i v) g
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f g : (i : ι) → π i<VAR>(j : ι) → Decidable (j ∈ s)<VAR>DecidableEq ι<VAR>i : ι<VAR>hi : i ∉ s<VAR>v : π i<GOAL>Function.update (s.piecewise f g) i v = s.piecewise f (Function.update g i v)
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f : (i : ι) → π i<VAR>(j : ι) → Decidable (j ∈ s)<GOAL>s.piecewise f f = f
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>Fintype ι<VAR>(i : ι) → Decidable (i ∈ Finset.univ)<VAR>f g : (i : ι) → π i<GOAL>Finset.univ.piecewise f g = f
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>(i : ι) → Decidable (i ∈ s)<VAR>(i : ι) → Decidable (i ∈ sᶜ)<VAR>f g : (i : ι) → π i<GOAL>sᶜ.piecewise f g = s.piecewise g f
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>i : ι<VAR>f g : (i : ι) → π i<GOAL>(Finset.univ.erase i).piecewise f g = Function.update f i (g i)
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>(j : ι) → Decidable (j ∈ s)<VAR>π : ι → Type u_3<VAR>t : Set ι<VAR>t' : (i : ι) → Set (π i)<VAR>f g : (i : ι) → π i<VAR>hf : f ∈ t.pi t'<VAR>hg : g ∈ t.pi t'<GOAL>s.piecewise f g ∈ t.pi t'
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>(j : ι) → Decidable (j ∈ s)<VAR>π : ι → Type u_3<VAR>f g h : (i : ι) → π i<VAR>(i : ι) → Preorder (π i)<VAR>hf : f ≤ h<VAR>hg : g ≤ h<GOAL>s.piecewise f g ≤ h
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>(j : ι) → Decidable (j ∈ s)<VAR>π : ι → Type u_3<VAR>f g h : (i : ι) → π i<VAR>(i : ι) → Preorder (π i)<VAR>hf : h ≤ f<VAR>hg : h ≤ g<GOAL>h ≤ s.piecewise f g
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>(j : ι) → Decidable (j ∈ s)<VAR>π : ι → Type u_3<VAR>f g f' g' : (i : ι) → π i<VAR>(i : ι) → Preorder (π i)<VAR>hf : ∀ x ∈ s, f x ≤ f' x<VAR>hg : ∀ x ∉ s, g x ≤ g' x<GOAL>s.piecewise f g ≤ s.piecewise f' g'
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>(j : ι) → Decidable (j ∈ s)<VAR>π : ι → Type u_3<VAR>f g f' g' : (i : ι) → π i<VAR>(i : ι) → Preorder (π i)<VAR>hf : f ≤ f'<VAR>hg : g ≤ g'<GOAL>s.piecewise f g ≤ s.piecewise f' g'
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>(j : ι) → Decidable (j ∈ s)<VAR>π : ι → Type u_3<VAR>f g f' g' : (i : ι) → π i<VAR>(i : ι) → Preorder (π i)<VAR>hf : f ∈ Set.Icc f' g'<VAR>hg : g ∈ Set.Icc f' g'<GOAL>s.piecewise f g ∈ Set.Icc f' g'
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>(j : ι) → Decidable (j ∈ s)<VAR>π : ι → Type u_3<VAR>f g : (i : ι) → π i<VAR>(i : ι) → Preorder (π i)<VAR>h : f ≤ g<GOAL>s.piecewise f g ∈ Set.Icc f g
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>(j : ι) → Decidable (j ∈ s)<VAR>π : ι → Type u_3<VAR>f g : (i : ι) → π i<VAR>(i : ι) → Preorder (π i)<VAR>h : g ≤ f<GOAL>s.piecewise f g ∈ Set.Icc g f
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Set.univ.encard = s.encard
<VAR>α : Type u_3<GOAL>Set.univ.encard = PartENat.withTopEquiv (PartENat.card α)
<VAR>α : Type u_1<VAR>s : Set α<VAR>h : s.Finite<GOAL>s.encard = ↑h.toFinset.card
<VAR>α : Type u_1<VAR>s : Set α<VAR>Fintype ↑s<GOAL>s.encard = ↑s.toFinset.card
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>(↑s).encard = ↑s.card
<VAR>α : Type u_1<VAR>s : Set α<VAR>h : s.Infinite<GOAL>s.encard = ⊤
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.encard = 0 ↔ s = ∅
<VAR>α : Type u_1<GOAL>∅.encard = 0
<VAR>α : Type u_1<VAR>s : Set α<VAR>h : s.encard ≠ 0<GOAL>s.Nonempty
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.encard ≠ 0 ↔ s.Nonempty
<VAR>α : Type u_1<VAR>s : Set α<GOAL>0 < s.encard ↔ s.Nonempty
<VAR>α : Type u_1<VAR>e : α<GOAL>{e}.encard = 1
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : Disjoint s t<GOAL>(s ∪ t).encard = s.encard + t.encard
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>has : a ∉ s<GOAL>(insert a s).encard = s.encard + 1
<VAR>α : Type u_1<VAR>s : Set α<VAR>h : s.Finite<GOAL>s.encard < ⊤
<VAR>α : Type u_1<VAR>s : Set α<VAR>h : s.Finite<GOAL>s.encard = ↑s.encard.toNat
<VAR>α : Type u_1<VAR>s : Set α<VAR>h : s.Finite<GOAL>∃ n, s.encard = ↑n
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.encard < ⊤ ↔ s.Finite
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.encard = ⊤ ↔ s.Infinite
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.encard ≠ ⊤ ↔ s.Finite
<VAR>α : Type u_1<VAR>s : Set α<VAR>k : ℕ<VAR>h : s.encard ≤ ↑k<GOAL>s.Finite
<VAR>α : Type u_1<VAR>s : Set α<VAR>k : ℕ<VAR>h : s.encard = ↑k<GOAL>s.Finite
<VAR>α : Type u_1<VAR>s : Set α<VAR>k : ℕ<GOAL>s.encard ≤ ↑k ↔ s.Finite ∧ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>s.encard ≤ t.encard
<VAR>α : Type u_3<GOAL>Monotone Set.encard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>(t \ s).encard + s.encard = t.encard
<VAR>α : Type u_1<VAR>s : Set α<GOAL>1 ≤ s.encard ↔ s.Nonempty
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>(s \ t).encard + (s ∩ t).encard = s.encard
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>(s ∪ t).encard + (s ∩ t).encard = s.encard + t.encard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : (s ∩ t).Finite<GOAL>s.encard = t.encard ↔ (s \ t).encard = (t \ s).encard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : (s ∩ t).Finite<GOAL>s.encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : (s ∩ t).Finite<GOAL>s.encard < t.encard ↔ (s \ t).encard < (t \ s).encard
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>(s ∪ t).encard ≤ s.encard + t.encard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s.encard = t.encard<GOAL>s.Finite ↔ t.Finite
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s.encard = t.encard<GOAL>s.Infinite ↔ t.Infinite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Finite<VAR>h : t.encard ≤ s.encard<GOAL>t.Finite
<VAR>α : Type u_1<VAR>s t : Set α<VAR>ht : t.Finite<VAR>hst : s ⊆ t<VAR>hts : t.encard ≤ s.encard<GOAL>s = t
<VAR>α : Type u_1<VAR>s t : Set α<VAR>hs : s.Finite<VAR>hst : s ⊆ t<VAR>hts : t.encard ≤ s.encard<GOAL>s = t