ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a : ℕ<VAR>ha : a ≠ 0<VAR>h : a.primeFactorsList <+~ primeFactorsList 0<GOAL>a ∣ 0
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>h : a.primeFactorsList <+~ b.primeFactorsList<VAR>hb : b > 0<GOAL>a ∣ b
<VAR>b : ℕ<VAR>hb : b > 0<VAR>a : ℕ<VAR>ha : a + 1 + 1 ≠ 0<VAR>h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList<GOAL>a + 1 + 1 ∣ b
<VAR>b : ℕ<VAR>hb : b > 0<VAR>a : ℕ<VAR>ha : a + 1 + 1 ≠ 0<VAR>h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList<GOAL>b = (a + 1 + 1) * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
<VAR>b : ℕ<VAR>hb : b > 0<VAR>a : ℕ<VAR>ha : a + 1 + 1 ≠ 0<VAR>h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList<GOAL>b = (a + 1 + 1).primeFactorsList.prod * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
<VAR>l : List ℕ<VAR>a m n : ℕ<VAR>x✝ : [].IsZeckendorfRep<GOAL>(map fib []).sum.zeckendorf = []
<VAR>l✝ : List ℕ<VAR>a✝ m n a : ℕ<VAR>l : List ℕ<VAR>hl hl' : (a :: l).IsZeckendorfRep<GOAL>(map fib (a :: l)).sum.zeckendorf = a :: l
<VAR>l✝ : List ℕ<VAR>a✝ m n a : ℕ<VAR>l : List ℕ<VAR>hl' : (a :: l).IsZeckendorfRep<VAR>hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ List.Pairwise (fun a b => b + 2 ≤ a) (l ++ [0])<GOAL>(map fib (a :: l)).sum.zeckendorf = a :: l
<VAR>l✝ : List ℕ<VAR>a✝ m n a : ℕ<VAR>l : List ℕ<VAR>hl' : (a :: l).IsZeckendorfRep<VAR>hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])<GOAL>(map fib (a :: l)).sum.zeckendorf = a :: l
<VAR>l✝ : List ℕ<VAR>a✝ m n a : ℕ<VAR>l : List ℕ<VAR>hl' : (a :: l).IsZeckendorfRep<VAR>hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])<VAR>ha : 0 < a<GOAL>(map fib (a :: l)).sum.zeckendorf = a :: l
<VAR>l✝ : List ℕ<VAR>a✝ m n a : ℕ<VAR>l : List ℕ<VAR>hl' : (a :: l).IsZeckendorfRep<VAR>hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])<VAR>ha : 0 < a<GOAL>(fib a + (map fib l).sum).greatestFib = a
<VAR>l✝ : List ℕ<VAR>a✝ m n a : ℕ<VAR>l : List ℕ<VAR>hl' : (a :: l).IsZeckendorfRep<VAR>hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])<VAR>ha : 0 < a<GOAL>a ≤ (map fib l).sum + (fib a + 1) ∧ ∀ ⦃n : ℕ⦄, a < n → n ≤ (map fib l).sum + (fib a + 1) → (map fib l).sum + fib a < fib n
<VAR>l✝ : List ℕ<VAR>a✝ m n✝ a : ℕ<VAR>l : List ℕ<VAR>hl' : (a :: l).IsZeckendorfRep<VAR>hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])<VAR>ha : 0 < a<VAR>n : ℕ<VAR>hn : a < n<VAR>x✝ : n ≤ (map fib l).sum + (fib a + 1)<GOAL>(map fib l).sum + fib a < fib n
<VAR>l✝ : List ℕ<VAR>a✝ m n✝ a : ℕ<VAR>l : List ℕ<VAR>hl' : (a :: l).IsZeckendorfRep<VAR>hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])<VAR>ha : 0 < a<VAR>n : ℕ<VAR>hn : a < n<VAR>x✝ : n ≤ (map fib l).sum + (fib a + 1)<GOAL>(map fib (a :: l)).sum < fib n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>a b : ℝ<VAR>h : a ≤ b<GOAL>Metric.diam (Icc a b) = b - a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>h : Continuous f<GOAL>Inducing f ↔ ∀ (i : ι), Inducing ((U i).carrier.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>h : Continuous f<GOAL>(∀ (x : α), 𝓝 x = comap f (𝓝 (f x))) ↔ ∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)), 𝓝 x = comap Subtype.val (comap f (𝓝 ((f ∘ Subtype.val) x)))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s✝ s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>hB : ‖B‖ ≤ 1<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s✝ s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>hB : ‖B‖ ≤ 1<GOAL>‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² : OrderedCommRing S<VAR>inst✝¹ : Ring R<VAR>abv : AbsoluteValue R S<VAR>inst✝ : NoZeroDivisors S<VAR>a b : R<GOAL>abv (a - b) = abv (b - a)
<VAR>X Y Z : Scheme<VAR>𝒰✝ : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f✝) g<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<VAR>i : (𝒰.affineRefinement.openCover.pullbackCover f).J<GOAL>(pullbackCoverAffineRefinementObjIso f 𝒰 i).inv ≫ (𝒰.affineRefinement.openCover.pullbackCover f).map i = ((𝒰.obj i.fst).affineCover.pullbackCover (𝒰.pullbackHom f i.fst)).map i.snd ≫ (𝒰.pullbackCover f).map i.fst
<VAR>X Y Z : Scheme<VAR>𝒰✝ : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f✝) g<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<VAR>i : (𝒰.affineRefinement.openCover.pullbackCover f).J<GOAL>(pullbackSymmetry ((𝒰.obj i.fst).affineCover.map i.snd) (pullback.fst (𝒰.map i.fst) f)).inv ≫ (pullbackRightPullbackFstIso (𝒰.map i.fst) f ((𝒰.obj i.fst).affineCover.map i.snd)).hom ≫ pullback.snd (𝒰.affineRefinement.map i) f = pullback.fst (pullback.fst (𝒰.map i.fst) f) ((𝒰.obj i.fst).affineCover.map i.snd) ≫ pullback.snd (𝒰.map i.fst) f
<VAR>X Y Z : Scheme<VAR>𝒰✝ : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f✝) g<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<VAR>i : (𝒰.affineRefinement.openCover.pullbackCover f).J<VAR>e_1✝ : (pullback (pullback.fst (𝒰.map i.fst) f) ((𝒰.obj i.fst).affineCover.map i.snd) ⟶ X) = (pullback (pullback.fst (𝒰.map i.fst) f) ((𝒰.obj i.fst).affineCover.map i.snd) ⟶ X)<GOAL>(pullbackRightPullbackFstIso (𝒰.map i.fst) f ((𝒰.obj i.fst).affineCover.map i.snd)).hom ≫ pullback.snd (𝒰.affineRefinement.map i) f = pullback.snd ((𝒰.obj i.fst).affineCover.map i.snd) (pullback.fst (𝒰.map i.fst) f) ≫ pullback.snd (𝒰.map i.fst) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : SMulCommClass ℝ 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace E<VAR>f g : ↥(Lp E 1 μ)<GOAL>integralCLM (f + g) = integralCLM f + integralCLM g
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>n : ℕ<GOAL>(descPochhammer R (n + 1)).comp (X - 1) = descPochhammer R (n + 1) - (↑n + 1) • (descPochhammer R n).comp (X - 1)
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>n : ℕ<GOAL>(descPochhammer ℤ (n + 1)).comp (X - 1) = descPochhammer ℤ (n + 1) - (↑n + 1) * (descPochhammer ℤ n).comp (X - 1)
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>n : ℕ<GOAL>(descPochhammer ℤ (n + 1)).comp (X - 1) = X * (descPochhammer ℤ n).comp (X - 1) - (↑n + 1) * (descPochhammer ℤ n).comp (X - 1)
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>n : ℕ<GOAL>(X - 1 - ↑n) * (descPochhammer ℤ n).comp (X - 1) = (X - (↑n + 1)) * (descPochhammer ℤ n).comp (X - 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : Prop<VAR>f : p → Part α<VAR>h : p<VAR>Dom✝ : Prop<VAR>get✝ : Dom✝ → α<VAR>h' : f h = { Dom := Dom✝, get := get✝ }<GOAL>{ Dom := ∃ (h : p), (f h).Dom, get := fun ha => (f ⋯).get ⋯ } = { Dom := Dom✝, get := get✝ }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : Prop<VAR>f : p → Part α<VAR>h : p<VAR>Dom✝ : Prop<VAR>get✝ : Dom✝ → α<VAR>h' : f h = { Dom := Dom✝, get := get✝ }<GOAL>HEq (fun ha => get✝ ⋯) get✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : Prop<VAR>f : p → Part α<VAR>h : p<VAR>Dom✝ : Prop<VAR>get✝ : Dom✝ → α<VAR>h' : f h = { Dom := Dom✝, get := get✝ }<GOAL>(∃ (h : p), (f h).Dom) = Dom✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : Prop<VAR>f : p → Part α<VAR>h : p<VAR>Dom✝ : Prop<VAR>get✝ : Dom✝ → α<VAR>h' : f h = { Dom := Dom✝, get := get✝ }<GOAL>∀ (a : ∃ (h : p), (f h).Dom) (a' : Dom✝), HEq a a' → HEq (get✝ ⋯) (get✝ a')
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>a b x y z : α<VAR>h : IsCompl x y<VAR>hle : a ≤ b ⊔ y<GOAL>b ⊓ x ⊔ y ⊓ x = b ⊓ x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring R₁<VAR>inst✝⁶ : AddCommMonoid M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>I₁' : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M<VAR>v : n → M₁<GOAL>B.IsOrthoᵢ v ↔ B.flip.IsOrthoᵢ v
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring R₁<VAR>inst✝⁶ : AddCommMonoid M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>I₁' : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M<VAR>v : n → M₁<GOAL>(∀ (i j : n), i ≠ j → (B (v i)) (v j) = 0) ↔ ∀ (i j : n), i ≠ j → (B.flip (v i)) (v j) = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring R₁<VAR>inst✝⁶ : AddCommMonoid M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>I₁' : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M<VAR>v : n → M₁<VAR>h : ∀ (i j : n), i ≠ j → (B.flip (v i)) (v j) = 0<VAR>i j : n<VAR>hij : i ≠ j<GOAL>(B (v i)) (v j) = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring R₁<VAR>inst✝⁶ : AddCommMonoid M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>I₁' : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M<VAR>v : n → M₁<VAR>h : ∀ (i j : n), i ≠ j → (B (v j)) (v i) = 0<VAR>i j : n<VAR>hij : i ≠ j<GOAL>(B (v i)) (v j) = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring S<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Module S M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R S M<VAR>h : IsArtinian R M<GOAL>IsArtinian S M
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring S<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Module S M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R S M<VAR>h : WellFounded fun x x_1 => x < x_1<GOAL>WellFounded fun x x_1 => x < x_1
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c d : G₀<VAR>m n : ℕ<VAR>h : b = 0 → a = 0<GOAL>a / b * b = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>μ : Measure δ<VAR>s : Set ι<VAR>f : ι → δ → α<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<VAR>g : ι → δ → α := fun i => if hi : i ∈ s then AEMeasurable.mk (f i) ⋯ else fun _b => sSup ∅<GOAL>AEMeasurable (fun b => ⨆ i ∈ s, f i b) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>μ : Measure δ<VAR>s : Set ι<VAR>f : ι → δ → α<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<VAR>g : ι → δ → α := fun i => if hi : i ∈ s then AEMeasurable.mk (f i) ⋯ else fun _b => sSup ∅<VAR>this : ∀ i ∈ s, Measurable (g i)<GOAL>AEMeasurable (fun b => ⨆ i ∈ s, f i b) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>μ : Measure δ<VAR>s : Set ι<VAR>f : ι → δ → α<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<VAR>g : ι → δ → α := fun i => if hi : i ∈ s then AEMeasurable.mk (f i) ⋯ else fun _b => sSup ∅<VAR>this : ∀ i ∈ s, Measurable (g i)<GOAL>(fun b => ⨆ i ∈ s, f i b) =ᶠ[ae μ] fun b => ⨆ i ∈ s, g i b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>μ : Measure δ<VAR>s : Set ι<VAR>f : ι → δ → α<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<VAR>g : ι → δ → α := fun i => if hi : i ∈ s then AEMeasurable.mk (f i) ⋯ else fun _b => sSup ∅<VAR>this✝ : ∀ i ∈ s, Measurable (g i)<VAR>this : ∀ i ∈ s, ∀ᵐ (b : δ) ∂μ, f i b = g i b<GOAL>(fun b => ⨆ i ∈ s, f i b) =ᶠ[ae μ] fun b => ⨆ i ∈ s, g i b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>μ : Measure δ<VAR>s : Set ι<VAR>f : ι → δ → α<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<VAR>g : ι → δ → α := fun i => if hi : i ∈ s then AEMeasurable.mk (f i) ⋯ else fun _b => sSup ∅<VAR>this✝ : ∀ i ∈ s, Measurable (g i)<VAR>this : ∀ i ∈ s, ∀ᵐ (b : δ) ∂μ, f i b = g i b<VAR>b : δ<VAR>hb : ∀ i ∈ s, f i b = g i b<GOAL>⨆ i ∈ s, f i b = ⨆ i ∈ s, g i b
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>pellZd a1 (n + 2) + pellZd a1 n = ↑(2 * a) * pellZd a1 (n + 1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>this : 1 + { re := ↑a, im := 1 } * { re := ↑a, im := 1 } = { re := ↑a, im := 1 } * (2 * ↑a)<GOAL>pellZd a1 (n + 2) + pellZd a1 n = ↑(2 * a) * pellZd a1 (n + 1)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>φ : G →* G<VAR>inst✝ : Finite G<VAR>hφ : FixedPointFree ⇑φ<VAR>h2 : Function.Involutive ⇑φ<VAR>g h : G<GOAL>Commute g h
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>φ : G →* G<VAR>inst✝ : Finite G<VAR>hφ : FixedPointFree ⇑φ<VAR>h2 : Function.Involutive ⇑φ<VAR>g h : G<VAR>key : φ (g * h) = φ g * φ h<GOAL>Commute g h
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p✝ : (i : Fin n) → α✝ i.succ<VAR>i✝ : Fin n<VAR>y : α✝ i✝.succ<VAR>z : α✝ 0<VAR>p : ℕ<VAR>α : Type u_1<VAR>a : Fin m → α<VAR>b : Fin n → α<VAR>c : Fin p → α<VAR>i : Fin (m + n + p)<GOAL>append (append a b) c i = (append a (append b c) ∘ cast ⋯) i
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p✝ : (i : Fin n) → α✝ i.succ<VAR>i✝ : Fin n<VAR>y : α✝ i✝.succ<VAR>z : α✝ 0<VAR>p : ℕ<VAR>α : Type u_1<VAR>a : Fin m → α<VAR>b : Fin n → α<VAR>c : Fin p → α<VAR>i : Fin (m + n + p)<GOAL>append (append a b) c i = append a (append b c) (cast ⋯ i)
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<GOAL>↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 + ε ^ 4 / 3 ≤ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 + ↑(star hP G ε hU V).card * ↑(star hP G ε hV U).card / 16 ^ P.parts.card * (9 / 16) * ε ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<GOAL>ε ^ 4 / 3 ≤ ↑(star hP G ε hU V).card * ↑(star hP G ε hV U).card / 16 ^ P.parts.card * (9 / 16) * ε ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>Ul : 4 / 5 * ε ≤ ↑(star hP G ε hU V).card / 4 ^ P.parts.card<GOAL>ε ^ 4 / 3 ≤ ↑(star hP G ε hU V).card * ↑(star hP G ε hV U).card / 16 ^ P.parts.card * (9 / 16) * ε ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>Ul : 4 / 5 * ε ≤ ↑(star hP G ε hU V).card / 4 ^ P.parts.card<VAR>Vl : 4 / 5 * ε ≤ ↑(star hP G ε hV U).card / 4 ^ P.parts.card<GOAL>ε ^ 4 / 3 ≤ ↑(star hP G ε hU V).card * ↑(star hP G ε hV U).card / 16 ^ P.parts.card * (9 / 16) * ε ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>Ul : 4 / 5 * ε ≤ ↑(star hP G ε hU V).card / 4 ^ P.parts.card<VAR>Vl : 4 / 5 * ε ≤ ↑(star hP G ε hV U).card / 4 ^ P.parts.card<GOAL>ε ^ 4 / 3 ≤ ↑(star hP G ε hU V).card / 4 ^ P.parts.card * (↑(star hP G ε hV U).card / 4 ^ P.parts.card) * (9 / 4 ^ 2 * ε ^ 2)
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>Ul : 4 / 5 * ε ≤ ↑(star hP G ε hU V).card / 4 ^ P.parts.card<VAR>Vl : 4 / 5 * ε ≤ ↑(star hP G ε hV U).card / 4 ^ P.parts.card<VAR>this : 0 < ε<GOAL>ε ^ 4 / 3 ≤ ↑(star hP G ε hU V).card / 4 ^ P.parts.card * (↑(star hP G ε hV U).card / 4 ^ P.parts.card) * (9 / 4 ^ 2 * ε ^ 2)
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>Ul : 4 / 5 * ε ≤ ↑(star hP G ε hU V).card / 4 ^ P.parts.card<VAR>Vl : 4 / 5 * ε ≤ ↑(star hP G ε hV U).card / 4 ^ P.parts.card<VAR>this : 0 < ε<VAR>UVl : 4 / 5 * ε * (4 / 5 * ε) ≤ ↑(star hP G ε hU V).card / 4 ^ P.parts.card * (↑(star hP G ε hV U).card / 4 ^ P.parts.card)<GOAL>ε ^ 4 / 3 ≤ ↑(star hP G ε hU V).card / 4 ^ P.parts.card * (↑(star hP G ε hV U).card / 4 ^ P.parts.card) * (9 / 4 ^ 2 * ε ^ 2)