ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>b o : Ordinal.{u_1}<VAR>ho : o ≠ 0<VAR>hb : 0 < b<GOAL>0 < o / b ^ log b o
<VAR>n : ℕ<GOAL>↑(bif (↑n).bodd then 1 else 0) + 2 * (↑n).div2 = ↑n
<VAR>n : ℕ<GOAL>(bif -[n+1].bodd then 1 else 0) + 2 * -[n+1].div2 = -[n+1]
<VAR>n : ℕ<GOAL>(bif -[n+1].bodd then 1 else 0) + 2 * -[n+1].div2 = -[(bif n.bodd then 1 else 0) + 2 * n.div2+1]
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>y : E<VAR>f g : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hf : HasIntegral I l f μ.toBoxAdditive.toSMul y<VAR>hfg : f =ᶠ[ae (μ.restrict ↑I)] g<VAR>hl : l.bRiemann = false<GOAL>HasIntegral I l g μ.toBoxAdditive.toSMul y
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>y : E<VAR>f g : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hf : HasIntegral I l f μ.toBoxAdditive.toSMul y<VAR>hfg : f =ᶠ[ae (μ.restrict ↑I)] g<VAR>hl : l.bRiemann = false<VAR>this : g - f =ᶠ[ae (μ.restrict ↑I)] 0<GOAL>HasIntegral I l g μ.toBoxAdditive.toSMul y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁵ : OrderedRing 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<GOAL>openSegment 𝕜 x y = (fun θ => x + θ • (y - x)) '' Ioo 0 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁵ : OrderedRing 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>a✝¹ : 𝕜<VAR>a✝ : a✝¹ ∈ Ioo 0 1<GOAL>x + a✝¹ • (y - x) = (1 - a✝¹) • x + a✝¹ • y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁵ : OrderedRing 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>a✝¹ : 𝕜<VAR>a✝ : a✝¹ ∈ Ioo 0 1<GOAL>x + (a✝¹ • y - a✝¹ • x) = x - a✝¹ • x + a✝¹ • y
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f' : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀<VAR>hf' : HasStrictFDerivAt f f' x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<VAR>htop : LinearMap.range (f'.prod φ') = ⊤<VAR>fφ : E → F × ℝ := fun x => (f x, φ x)<GOAL>False
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f' : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀<VAR>hf' : HasStrictFDerivAt f f' x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<VAR>htop : LinearMap.range (f'.prod φ') = ⊤<VAR>fφ : E → F × ℝ := fun x => (f x, φ x)<VAR>A : map φ (𝓝[f ⁻¹' {f x₀}] x₀) = 𝓝 (φ x₀)<GOAL>False
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x a : α<VAR>h_a : a ∈ fixedPoints ⇑f<VAR>h_le_init : x ≤ a<VAR>i : Ordinal.{u}<GOAL>lfpApprox f x i ≤ a
<VAR>A : Type u_1<VAR>inst✝³ : NormedCommRing A<VAR>inst✝² : NormedAlgebra ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>I : Ideal A<VAR>inst✝ : I.IsMaximal<VAR>a : A<VAR>ha : a ∈ I<GOAL>(CharacterSpace.equivAlgHom.symm ((↑(NormedRing.algEquivComplexOfComplete ⋯).symm).comp (Quotient.mkₐ ℂ I))) a = 0
<VAR>A : Type u_1<VAR>inst✝³ : NormedCommRing A<VAR>inst✝² : NormedAlgebra ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>I : Ideal A<VAR>inst✝ : I.IsMaximal<VAR>a : A<VAR>ha : a ∈ I<GOAL>⋯.some = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel α γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>s : Set (β × γ)<VAR>hs : MeasurableSet s<GOAL>((κ ×ₖ η) a) s = ((κ a).prod (η a)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel α γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>s : Set (β × γ)<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β), (η a) {c | (b, c) ∈ s} ∂κ a = ∫⁻ (x : β), (η a) (Prod.mk x ⁻¹' s) ∂κ a
<VAR>w x✝ y✝ z✝ x : ℝ<VAR>hx : x ≠ 0<VAR>y z : ℝ≥0<VAR>hyz : (fun y => y ^ x) y = (fun y => y ^ x) z<GOAL>y = z
<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>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hf : IsBoundedLinearMap 𝕜 f<GOAL>ContDiff 𝕜 n f
<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>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hf : IsBoundedLinearMap 𝕜 f<GOAL>ContDiff 𝕜 ⊤ f
<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>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hf : IsBoundedLinearMap 𝕜 f<GOAL>Differentiable 𝕜 f ∧ ContDiff 𝕜 ⊤ fun y => _root_.fderiv 𝕜 f y
<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>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hf : IsBoundedLinearMap 𝕜 f<GOAL>ContDiff 𝕜 ⊤ fun y => _root_.fderiv 𝕜 f y
<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>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hf : IsBoundedLinearMap 𝕜 f<GOAL>ContDiff 𝕜 ⊤ fun y => hf.toContinuousLinearMap
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<GOAL>Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(lTensor M (Submodule.subtype I))
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hf' : IsClosed (range f)<VAR>K : Set Y<VAR>hK : IsLindelof K<GOAL>IsLindelof (f ⁻¹' K)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hf' : IsClosed (range f)<VAR>K : Set Y<VAR>hK : IsLindelof (K ∩ range f)<GOAL>IsLindelof (f ⁻¹' K)
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>h : IsTopologicalBasis s<GOAL>IsTopologicalBasis (insert ∅ s)
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>h : IsTopologicalBasis s<GOAL>∀ t₁ ∈ insert ∅ s, ∀ t₂ ∈ insert ∅ s, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ insert ∅ s, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>h : IsTopologicalBasis s<GOAL>t = generateFrom (insert ∅ s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<GOAL>IsClosed ↑Kᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<GOAL>IsClosed ↑(⨅ v, LinearMap.ker ((innerSL 𝕜) ↑v))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>this : ∀ (v : ↥K), IsClosed ↑(LinearMap.ker ((innerSL 𝕜) ↑v))<GOAL>IsClosed ↑(⨅ v, LinearMap.ker ((innerSL 𝕜) ↑v))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>this : ∀ (v : ↥K), IsClosed ↑(LinearMap.ker ((innerSL 𝕜) ↑v))<GOAL>↑(⨅ v, LinearMap.ker ((innerSL 𝕜) ↑v)) = ⋂ i, ↑(LinearMap.ker ((innerSL 𝕜) ↑i))
<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>α : Type u_5<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>p : Prop<VAR>f : δ → α<VAR>hf : Measurable f<GOAL>Measurable fun b => ⨆ (_ : p), f 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>α : Type u_5<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>p : Prop<VAR>f : δ → α<VAR>hf : Measurable f<GOAL>Measurable fun b => if h : p then f b else sSup ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α → ℝ≥0∞<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∑' (x : ℕ), f x ≠ ⊤<GOAL>Tendsto f atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α → ℝ≥0∞<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∑' (x : ℕ), f x ≠ ⊤<GOAL>Tendsto f cofinite (𝓝 0)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₁, u₂} D<VAR>i : D ⥤ C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : CartesianClosed C<VAR>h : ∀ (B : D) (A : C), (A ⟹ i.obj B) ∈ i.essImage<VAR>B✝ A : C<VAR>B' : D<VAR>iB' : i.obj B' ≅ B✝<GOAL>(A ⟹ B✝) ∈ i.essImage
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>m n : ℤ<VAR>H : (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)<GOAL>h.IsClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>m n : ℤ<VAR>H : (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)<GOAL>(x = 1 * (m ^ 2 - n ^ 2) ∧ y = 1 * (2 * m * n) ∨ x = 1 * (2 * m * n) ∧ y = 1 * (m ^ 2 - n ^ 2)) ∧ m.gcd n = 1
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>m n : ℤ<VAR>t : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2<VAR>co : m.gcd n = 1<VAR>right✝ : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<GOAL>(x = 1 * (m ^ 2 - n ^ 2) ∧ y = 1 * (2 * m * n) ∨ x = 1 * (2 * m * n) ∧ y = 1 * (m ^ 2 - n ^ 2)) ∧ m.gcd n = 1
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>m n : ℤ<VAR>t : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2<VAR>co : m.gcd n = 1<VAR>right✝ : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<GOAL>(x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧ m.gcd n = 1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → S<VAR>this : (a : Prop) → Decidable a<VAR>i : ι<VAR>hi : i ∈ s<GOAL>(algebraMap R S) (↑(∏ j ∈ s.erase i, (sec M (f j)).2) * (sec M (f i)).1) = ↑(∏ i ∈ s, (sec M (f i)).2) • f i
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → S<VAR>this : (a : Prop) → Decidable a<VAR>i : ι<VAR>hi : i ∈ s<GOAL>(↑(∏ j ∈ s.erase i, (sec M (f j)).2) * ↑(sec M (f i)).2) • f i = ↑(∏ i ∈ s, (sec M (f i)).2) • f i
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → S<VAR>this : (a : Prop) → Decidable a<VAR>i : ι<VAR>hi : i ∈ s<GOAL>↑(∏ j ∈ s.erase i, (sec M (f j)).2) * ↑(sec M (f i)).2 = ↑(∏ i ∈ s, (sec M (f i)).2)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → S<VAR>this : (a : Prop) → Decidable a<VAR>i : ι<VAR>hi : i ∈ s<GOAL>↑(∏ j ∈ s.erase i, (sec M (f j)).2) * ↑(sec M (f i)).2 = ∏ x ∈ s, M.subtype (sec M (f x)).2
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → S<VAR>this : (a : Prop) → Decidable a<VAR>i : ι<VAR>hi : i ∈ s<GOAL>∏ x ∈ s, ↑(sec M (f x)).2 = ∏ x ∈ s, M.subtype (sec M (f x)).2
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>closure sᶜ = (interior s)ᶜ
<VAR>n : ℕ<GOAL>n + 1 ∣ n.centralBinom
<VAR>n : ℕ<VAR>h_s : (n + 1).Coprime (2 * n + 1)<GOAL>n + 1 ∣ n.centralBinom
<VAR>n : ℕ<VAR>h_s : (n + 1).Coprime (2 * n + 1)<GOAL>n + 1 ∣ (2 * n + 1) * n.centralBinom
<VAR>n : ℕ<VAR>h_s : (n + 1).Coprime (2 * n + 1)<GOAL>2 * (n + 1) ∣ 2 * ((2 * n + 1) * n.centralBinom)
<VAR>n : ℕ<VAR>h_s : (n + 1).Coprime (2 * n + 1)<GOAL>(n + 1) * 2 ∣ (n + 1) * (n + 1).centralBinom
<VAR>n k : ℕ<VAR>hnk : n < k<GOAL>(hermite n).coeff k = 0
<VAR>n k : ℕ<VAR>hnk : n < n + k + 1<GOAL>(hermite n).coeff (n + k + 1) = 0
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<GOAL>alternatization ((↑a).domCoprod ↑b) = ((Fintype.card ιa).factorial * (Fintype.card ιb).factorial) • a.domCoprod b
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₁ : Type u_3<VAR>V₁' : Type u_4<VAR>V₂ : Type u_5<VAR>V₃ : Type u_6<VAR>V₄ : Type u_7<VAR>P₁ : Type u_8<VAR>P₁' : Type u_9<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>P₃ : Type u_12<VAR>P₄ : Type u_13<VAR>inst✝²⁴ : NormedField 𝕜<VAR>inst✝²³ : SeminormedAddCommGroup V<VAR>inst✝²² : NormedSpace 𝕜 V<VAR>inst✝²¹ : PseudoMetricSpace P<VAR>inst✝²⁰ : NormedAddTorsor V P<VAR>inst✝¹⁹ : SeminormedAddCommGroup V₁<VAR>inst✝¹⁸ : NormedSpace 𝕜 V₁<VAR>inst✝¹⁷ : PseudoMetricSpace P₁<VAR>inst✝¹⁶ : NormedAddTorsor V₁ P₁<VAR>inst✝¹⁵ : SeminormedAddCommGroup V₁'<VAR>inst✝¹⁴ : NormedSpace 𝕜 V₁'<VAR>inst✝¹³ : MetricSpace P₁'<VAR>inst✝¹² : NormedAddTorsor V₁' P₁'<VAR>inst✝¹¹ : SeminormedAddCommGroup V₂<VAR>inst✝¹⁰ : NormedSpace 𝕜 V₂<VAR>inst✝⁹ : PseudoMetricSpace P₂<VAR>inst✝⁸ : NormedAddTorsor V₂ P₂<VAR>inst✝⁷ : SeminormedAddCommGroup V₃<VAR>inst✝⁶ : NormedSpace 𝕜 V₃<VAR>inst✝⁵ : PseudoMetricSpace P₃<VAR>inst✝⁴ : NormedAddTorsor V₃ P₃<VAR>inst✝³ : SeminormedAddCommGroup V₄<VAR>inst✝² : NormedSpace 𝕜 V₄<VAR>inst✝¹ : PseudoMetricSpace P₄<VAR>inst✝ : NormedAddTorsor V₄ P₄<VAR>f : P →ᵃⁱ[𝕜] P₂<VAR>f₁ : P₁' →ᵃⁱ[𝕜] P₂<VAR>x y : P<GOAL>dist (f x) (f y) = dist x y
<VAR>R : Type u_1<VAR>inst✝ : Ring R<GOAL>cyclotomic 1 R = X - 1
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ<GOAL>cyclotomic 1 R = X - 1
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ<GOAL>X - 1 = cyclotomic 1 R
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ<GOAL>X - 1 = map (Int.castRingHom R) (X - 1)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>inst✝³ : HasPushout g₁ g₂<VAR>inst✝² : HasPushout g₃ g₄<VAR>inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄<VAR>inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)<GOAL>pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄) ≫ (pushoutAssoc g₁ g₂ g₃ g₄).inv = pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄
<VAR>R : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>p : ι →₀ M<VAR>n : N<GOAL>(finsuppLeft R M N ι) (p ⊗ₜ[R] n) = p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>p : ι →₀ M<VAR>n : N<GOAL>(finsuppLeft R M N ι) (0 ⊗ₜ[R] n) = Finsupp.sum 0 fun i m => Finsupp.single i (m ⊗ₜ[R] n)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>p : ι →₀ M<VAR>n : N<GOAL>∀ (f g : ι →₀ M), ((finsuppLeft R M N ι) (f ⊗ₜ[R] n) = f.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)) → ((finsuppLeft R M N ι) (g ⊗ₜ[R] n) = g.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)) → (finsuppLeft R M N ι) ((f + g) ⊗ₜ[R] n) = (f + g).sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>p : ι →₀ M<VAR>n : N<GOAL>∀ (a : ι) (b : M), (finsuppLeft R M N ι) (Finsupp.single a b ⊗ₜ[R] n) = (Finsupp.single a b).sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>P : Type u_7<VAR>inst✝ : NormedAddCommGroup P<VAR>f : α → P<VAR>hf : Integrable f μ<GOAL>ENNReal.ofReal (∫ (x : α), ‖f x‖ ∂μ) = ∫⁻ (x : α), ↑‖f x‖₊ ∂μ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>hs : IsClosed s<GOAL>frontier s = s \ interior s
<VAR>n : ℕ<GOAL>HasDerivAt Gamma (↑n ! * (-↑γ + ↑(harmonic n))) (↑n + 1)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x y : α<VAR>hy : x ≠ y<VAR>hx : x ∉ l<VAR>h : optParam (x ∈ y :: l ++ [x]) ⋯<GOAL>(y :: l ++ [x]).next x h = y
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x y : α<VAR>hy : x ≠ y<VAR>hx : x ∉ l<VAR>h : optParam (x ∈ y :: l ++ [x]) ⋯<GOAL>(y :: l ++ [x]).get ⟨0, ⋯⟩ = y
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x y : α<VAR>hy : x ≠ y<VAR>hx : x ∉ l<VAR>h : optParam (x ∈ y :: l ++ [x]) ⋯<GOAL>x ∉ y :: l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_4}<GOAL>a % 1 = 0
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π✝ : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π✝ i)<VAR>f : X → (i : ι) → π✝ i<VAR>π : ι → Type u_8<VAR>g : (a : ι) → Set (Set (π a))<GOAL>Pi.topologicalSpace = generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π✝ : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π✝ i)<VAR>f : X → (i : ι) → π✝ i<VAR>π : ι → Type u_8<VAR>g : (a : ι) → Set (Set (π a))<GOAL>Pi.topologicalSpace ≤ generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π✝ : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π✝ i)<VAR>f : X → (i : ι) → π✝ i<VAR>π : ι → Type u_8<VAR>g : (a : ι) → Set (Set (π a))<GOAL>generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s} ≤ Pi.topologicalSpace
<VAR>n : ℕ<VAR>e : Perm (Fin (n + 1))<VAR>p : Fin (n + 2)<GOAL>(decomposeFin.symm (p, e)) 1 = (swap 0 p) (e 0).succ
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>v1 v2 : ℕ<GOAL>padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f (max v1 (max v2 (stationaryPoint hf))))
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>v1 v2 : ℕ<GOAL>stationaryPoint hf ≤ max v1 (max v2 (stationaryPoint hf))
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>v1 v2 : ℕ<GOAL>stationaryPoint hf ≤ stationaryPoint hf