ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ<VAR>hf : ∀ i ∈ s, 0 ≤ f i<GOAL>ENNReal.ofReal (∏ i ∈ s, f i) = ∏ i ∈ s, ENNReal.ofReal (f i)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ<VAR>hf : ∀ i ∈ s, 0 ≤ f i<GOAL>(∏ i ∈ s, f i).toNNReal = ∏ a ∈ s, (f a).toNNReal
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : IsIso g<GOAL>inv (pullback.fst f g) ≫ pullback.snd f g = f ≫ inv g
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hg : DifferentiableAt 𝕜' g₁ (h x)<VAR>hh : DifferentiableAt 𝕜 h x<VAR>hy : y = h x<GOAL>deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)
<VAR>n : ℤ<GOAL>χ₈ ↑n = χ₈ ↑(n % 8)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ p✝ q✝ : R[X]<VAR>ι : Type u_1<VAR>p q : R[X]<VAR>H : (p + q).natDegree < p.natDegree<GOAL>p.natDegree = q.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ p✝ q✝ : R[X]<VAR>ι : Type u_1<VAR>p q : R[X]<VAR>H : (p + q).natDegree < p.natDegree<VAR>h : ¬p.natDegree = q.natDegree<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>h : P.toPoly = Q.toPoly<GOAL>P.a = Q.a
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁴ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝³ : NormedRing 𝕜<VAR>inst✝² : (i : α) → Module 𝕜 (E i)<VAR>inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝ : DecidableEq α<VAR>hp : 0 < p.toReal<VAR>f : (i : α) → E i<VAR>i : α<GOAL>‖lp.single p i (f i)‖ = ‖f i‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁴ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝³ : NormedRing 𝕜<VAR>inst✝² : (i : α) → Module 𝕜 (E i)<VAR>inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝ : DecidableEq α<VAR>hp : 0 < p.toReal<VAR>f : (i : α) → E i<VAR>i : α<GOAL>(fun y => y ^ p.toReal) ‖lp.single p i (f i)‖ = (fun y => y ^ p.toReal) ‖f i‖
<VAR>R : Type u₁<VAR>inst✝¹ : CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CharP R p<VAR>f : Ring.Perfection R p<VAR>n : ℕ<VAR>hfn : (coeff R p n) f ≠ 0<VAR>k✝ k : ℕ<VAR>ih : (coeff R p (n + k)) f ≠ 0<VAR>h : (coeff R p (n + k.succ)) f = 0<GOAL>(coeff R p (n + k)) f = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : SummableFamily Γ R α<VAR>f : α ↪ β<VAR>a : α<VAR>b : β<VAR>h : b ∉ Set.range ⇑f<GOAL>(s.embDomain f) b = 0
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>hs : IsOpen s<VAR>x : α<VAR>xs : x ∈ s<VAR>n : Set α<VAR>hn : n ∈ 𝓝[s] x<GOAL>0 < μ n
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>hs : IsOpen s<VAR>x : α<VAR>xs : x ∈ s<VAR>n : Set α<VAR>hn : n ∈ 𝓝[s] x<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>xu : x ∈ u<VAR>hu : u ∩ s ⊆ n<GOAL>0 < μ n
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>hs : IsOpen s<VAR>x : α<VAR>xs : x ∈ s<VAR>n : Set α<VAR>hn : n ∈ 𝓝[s] x<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>xu : x ∈ u<VAR>hu : u ∩ s ⊆ n<GOAL>0 < μ (u ∩ s)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a o : Ordinal.{u}<VAR>f✝ : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>f : (b : Ordinal.{u_2}) → b < 0 → Ordinal.{u_2}<GOAL>0 ≤ (cof 0).ord
<VAR>n : ℕ<VAR>h : 2 ≤ n<GOAL>(finRotate n).cycleType = {n}
<VAR>m : ℕ<VAR>h : 2 ≤ 2 + m<GOAL>(finRotate (2 + m)).cycleType = {2 + m}
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>c : KernelFork (f - g)<GOAL>Fork.ι c ≫ f = Fork.ι c ≫ g
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i✝ : ι<VAR>f : (i j : ι) → C.X i ⟶ D.X j<VAR>i i' : ι<VAR>w : c.Rel i i'<GOAL>(dNext i) f = C.d i i' ≫ f i' i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i✝ : ι<VAR>f : (i j : ι) → C.X i ⟶ D.X j<VAR>i : ι<VAR>w : c.Rel i (c.next i)<GOAL>(dNext i) f = C.d i (c.next i) ≫ f (c.next i) i
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>h : c • x ∈ s<VAR>hc : c ≠ 0<GOAL>egauge 𝕜 s x ≤ ↑‖c‖₊⁻¹
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>h : c • x ∈ s<VAR>hc : c ≠ 0<GOAL>egauge 𝕜 s x ≤ ↑‖c⁻¹‖₊
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Ring R<VAR>n : ℤ<GOAL>(↑n).natDegree = 0
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<GOAL>Tendsto (logb b) atTop atBot
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<GOAL>∀ (b_1 : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → logb b a ≤ b_1
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>e : ℝ<GOAL>∃ i, ∀ (a : ℝ), i ≤ a → logb b a ≤ e
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>e : ℝ<GOAL>∀ (a : ℝ), 1 ⊔ b ^ e ≤ a → logb b a ≤ e
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>e a : ℝ<GOAL>1 ⊔ b ^ e ≤ a → logb b a ≤ e
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>e a : ℝ<GOAL>1 ≤ a → b ^ e ≤ a → logb b a ≤ e
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>e a : ℝ<VAR>ha : 1 ≤ a<GOAL>b ^ e ≤ a → logb b a ≤ e
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>e a : ℝ<VAR>ha : 1 ≤ a<GOAL>b ^ e ≤ a → b ^ e ≤ a
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>e a : ℝ<VAR>ha : 1 ≤ a<GOAL>0 < a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>ha✝ : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>h_spec : spectrum R a ⊆ {0}<VAR>ha : autoParam (p a) _auto✝<GOAL>a = 0
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g✝ : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f g : 𝕜 → 𝕜<VAR>a : 𝕜<VAR>hf : HasDerivAt f 0 (g a)<VAR>hfg : f ∘ g =ᶠ[𝓝 a] id<VAR>hg : DifferentiableAt 𝕜 g a<GOAL>False
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g✝ : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f g : 𝕜 → 𝕜<VAR>a : 𝕜<VAR>hf : HasDerivAt f 0 (g a)<VAR>hfg : f ∘ g =ᶠ[𝓝 a] id<VAR>hg : DifferentiableAt 𝕜 g a<VAR>this : HasDerivAt id (0 * deriv g a) a<GOAL>False
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>S : Set F<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>f : F →+* K<GOAL>IsSubfield (Set.range ⇑f)
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>S : Set F<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>f : F →+* K<GOAL>IsSubfield (⇑f '' Set.univ)
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedGroup E<VAR>inst✝ : SeminormedGroup F<VAR>s : Set E<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a b : E<GOAL>dist b (a * b) = ‖a‖
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g✝ : Filter α<VAR>s t : Set α<VAR>f g : Filter α<GOAL>f ⊓ g = ⊥ ↔ ∃ U ∈ f, ∃ V ∈ g, U ∩ V = ∅
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>s : Finset ι<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i ∈ s, (↑(f i)).Intersecting<VAR>this : DecidableEq ι<GOAL>(s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>s : Finset ι<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i ∈ s, (↑(f i)).Intersecting<VAR>this : DecidableEq ι<VAR>hs : Fintype.card α ≤ s.card<GOAL>(s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>s : Finset ι<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i ∈ s, (↑(f i)).Intersecting<VAR>this : DecidableEq ι<VAR>hs : s.card ≤ Fintype.card α<GOAL>(s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i ∈ ∅, (↑(f i)).Intersecting<VAR>hs : ∅.card ≤ Fintype.card α<GOAL>(∅.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - ∅.card)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : ∀ (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → s.card ≤ Fintype.card α → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting<VAR>hs : (cons i s hi).card ≤ Fintype.card α<GOAL>((cons i s hi).biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - (cons i s hi).card)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : ∀ (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → s.card ≤ Fintype.card α → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting<VAR>hs : (cons i s hi).card ≤ Fintype.card α<VAR>f' : ι → Finset (Finset α) := fun j => if hj : j ∈ cons i s hi then ⋯.choose else ∅<GOAL>((cons i s hi).biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - (cons i s hi).card)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : ∀ (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → s.card ≤ Fintype.card α → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting<VAR>hs : (cons i s hi).card ≤ Fintype.card α<VAR>f' : ι → Finset (Finset α) := fun j => if hj : j ∈ cons i s hi then ⋯.choose else ∅<VAR>hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * (f' j).card = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting<GOAL>((cons i s hi).biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - (cons i s hi).card)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : ∀ (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → s.card ≤ Fintype.card α → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting<VAR>hs : (cons i s hi).card ≤ Fintype.card α<VAR>f' : ι → Finset (Finset α) := fun j => if hj : j ∈ cons i s hi then ⋯.choose else ∅<VAR>hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * (f' j).card = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting<VAR>hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)<GOAL>((cons i s hi).biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - (cons i s hi).card)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : ∀ (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → s.card ≤ Fintype.card α → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting<VAR>hs : (cons i s hi).card ≤ Fintype.card α<VAR>f' : ι → Finset (Finset α) := fun j => if hj : j ∈ cons i s hi then ⋯.choose else ∅<VAR>hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * (f' j).card = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting<VAR>hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)<GOAL>((cons i s hi).biUnion f').card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - (cons i s hi).card)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : ∀ (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → s.card ≤ Fintype.card α → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting<VAR>hs : (cons i s hi).card ≤ Fintype.card α<VAR>f' : ι → Finset (Finset α) := fun j => if hj : j ∈ cons i s hi then ⋯.choose else ∅<VAR>hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * (f' j).card = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting<VAR>hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)<GOAL>((insert i s).biUnion f').card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - (cons i s hi).card)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : ∀ (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → s.card ≤ Fintype.card α → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting<VAR>hs : (cons i s hi).card ≤ Fintype.card α<VAR>f' : ι → Finset (Finset α) := fun j => if hj : j ∈ cons i s hi then ⋯.choose else ∅<VAR>hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * (f' j).card = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting<VAR>hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)<GOAL>(f' i ∪ s.biUnion f').card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - (cons i s hi).card)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : ∀ (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → s.card ≤ Fintype.card α → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting<VAR>hs : (cons i s hi).card ≤ Fintype.card α<VAR>f' : ι → Finset (Finset α) := fun j => if hj : j ∈ cons i s hi then ⋯.choose else ∅<VAR>hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * (f' j).card = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting<VAR>hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)<GOAL>(f' i).card + ((f' i ∪ s.biUnion f') \ f' i).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - (cons i s hi).card)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : ∀ (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → s.card ≤ Fintype.card α → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting<VAR>hs : (cons i s hi).card ≤ Fintype.card α<VAR>f' : ι → Finset (Finset α) := fun j => if hj : j ∈ cons i s hi then ⋯.choose else ∅<VAR>hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * (f' j).card = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting<VAR>hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)<GOAL>(f' i).card + (s.biUnion f' ∩ (f' i)ᶜ).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - (cons i s hi).card)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : ∀ (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → s.card ≤ Fintype.card α → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting<VAR>hs : (cons i s hi).card ≤ Fintype.card α<VAR>f' : ι → Finset (Finset α) := fun j => if hj : j ∈ cons i s hi then ⋯.choose else ∅<VAR>hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * (f' j).card = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting<VAR>hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)<GOAL>2 ^ (Fintype.card α + 1) * ((f' i).card + (s.biUnion f' ∩ (f' i)ᶜ).card) ≤ 2 ^ (Fintype.card α + 1) * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - (cons i s hi).card))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : ∀ (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → s.card ≤ Fintype.card α → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting<VAR>hs : (cons i s hi).card ≤ Fintype.card α<VAR>f' : ι → Finset (Finset α) := fun j => if hj : j ∈ cons i s hi then ⋯.choose else ∅<VAR>hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * (f' j).card = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting<VAR>hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)<GOAL>2 ^ Fintype.card α * (2 * (f' i).card) + 2 * (2 ^ Fintype.card α * (s.biUnion f' ∩ (f' i)ᶜ).card) ≤ 2 * 2 ^ Fintype.card α * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - (cons i s hi).card))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : ∀ (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → s.card ≤ Fintype.card α → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting<VAR>hs : (cons i s hi).card ≤ Fintype.card α<VAR>f' : ι → Finset (Finset α) := fun j => if hj : j ∈ cons i s hi then ⋯.choose else ∅<VAR>hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * (f' j).card = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting<VAR>hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)<GOAL>IsUpperSet ↑(s.biUnion f')
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : ∀ (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → s.card ≤ Fintype.card α → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting<VAR>hs : (cons i s hi).card ≤ Fintype.card α<VAR>f' : ι → Finset (Finset α) := fun j => if hj : j ∈ cons i s hi then ⋯.choose else ∅<VAR>hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * (f' j).card = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting<VAR>hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)<GOAL>IsLowerSet ↑(f' i)ᶜ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : ∀ (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → s.card ≤ Fintype.card α → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting<VAR>hs : (cons i s hi).card ≤ Fintype.card α<VAR>f' : ι → Finset (Finset α) := fun j => if hj : j ∈ cons i s hi then ⋯.choose else ∅<VAR>hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * (f' j).card = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting<VAR>hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)<GOAL>2 ^ Fintype.card α * Fintype.card (Finset α) + 2 * ((s.biUnion f').card * (f' i)ᶜ.card) ≤ 2 * 2 ^ Fintype.card α * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - (cons i s hi).card))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : ∀ (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → s.card ≤ Fintype.card α → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting<VAR>hs : (cons i s hi).card ≤ Fintype.card α<VAR>f' : ι → Finset (Finset α) := fun j => if hj : j ∈ cons i s hi then ⋯.choose else ∅<VAR>hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * (f' j).card = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting<VAR>hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)<GOAL>2 ^ Fintype.card α * (2 ^ Fintype.card α + (s.biUnion f').card) ≤ 2 ^ Fintype.card α * (2 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - (cons i s hi).card)))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : ∀ (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → s.card ≤ Fintype.card α → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting<VAR>hs : (cons i s hi).card ≤ Fintype.card α<VAR>f' : ι → Finset (Finset α) := fun j => if hj : j ∈ cons i s hi then ⋯.choose else ∅<VAR>hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * (f' j).card = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting<VAR>hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)<GOAL>2 ^ Fintype.card α + (s.biUnion f').card ≤ 2 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - (cons i s hi).card))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nonempty α<VAR>this : DecidableEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : ∀ (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → s.card ≤ Fintype.card α → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)<VAR>f : ι → Finset (Finset α)<VAR>hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting<VAR>hs : (cons i s hi).card ≤ Fintype.card α<VAR>f' : ι → Finset (Finset α) := fun j => if hj : j ∈ cons i s hi then ⋯.choose else ∅<VAR>hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * (f' j).card = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting<VAR>hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)<GOAL>2 ^ Fintype.card α + (2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)) ≤ 2 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - (cons i s hi).card))
<VAR>m n✝ : ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>(bit b n).div2 = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>(1 - x) * ∑' (i : ℕ), x ^ i = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<VAR>this : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)<GOAL>(1 - x) * ∑' (i : ℕ), x ^ i = 1