ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : AffineSpace V P<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : Module k V<VAR>b : AffineBasis ι k P<VAR>ι' : Type u_1<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : Finite ι'<VAR>inst✝ : DecidableEq ι'<VAR>p : ι' → P<VAR>A : Matrix ι ι' k<VAR>hA : b.toMatrix p * A = 1<VAR>val✝ : Fintype ι'<GOAL>∀ (w1 w2 : ι' → k), ∑ i : ι', w1 i = 1 → ∑ i : ι', w2 i = 1 → (Finset.affineCombination k Finset.univ p) w1 = (Finset.affineCombination k Finset.univ p) w2 → w1 = w2
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : AffineSpace V P<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : Module k V<VAR>b : AffineBasis ι k P<VAR>ι' : Type u_1<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : Finite ι'<VAR>inst✝ : DecidableEq ι'<VAR>p : ι' → P<VAR>A : Matrix ι ι' k<VAR>hA : b.toMatrix p * A = 1<VAR>val✝ : Fintype ι'<VAR>w₁ w₂ : ι' → k<VAR>hw₁ : ∑ i : ι', w₁ i = 1<VAR>hw₂ : ∑ i : ι', w₂ i = 1<VAR>hweq : (Finset.affineCombination k Finset.univ p) w₁ = (Finset.affineCombination k Finset.univ p) w₂<VAR>hweq' : (fun w => w ᵥ* A) (w₁ ᵥ* b.toMatrix p) = (fun w => w ᵥ* A) (w₂ ᵥ* b.toMatrix p)<GOAL>w₁ = w₂
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝³ : SeminormedRing 𝕜<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Zero E<VAR>inst✝ : TopologicalSpace E<VAR>q : ι → Prop<VAR>s : ι → Set E<VAR>A : Set E<VAR>h : (𝓝 0).HasBasis q s<GOAL>IsVonNBounded 𝕜 A ↔ ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝³ : SeminormedRing 𝕜<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Zero E<VAR>inst✝ : TopologicalSpace E<VAR>q : ι → Prop<VAR>s : ι → Set E<VAR>A : Set E<VAR>h : (𝓝 0).HasBasis q s<VAR>hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A<VAR>V : Set E<VAR>hV : V ∈ 𝓝 0<GOAL>Absorbs 𝕜 V A
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝³ : SeminormedRing 𝕜<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Zero E<VAR>inst✝ : TopologicalSpace E<VAR>q : ι → Prop<VAR>s : ι → Set E<VAR>A : Set E<VAR>h : (𝓝 0).HasBasis q s<VAR>hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A<VAR>V : Set E<VAR>hV✝ : V ∈ 𝓝 0<VAR>i : ι<VAR>hi : q i<VAR>hV : s i ⊆ V<GOAL>Absorbs 𝕜 V A
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>v : Set E<VAR>A : ι → Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>hv : Orthonormal 𝕜 Subtype.val<GOAL>∃ u b, v ⊆ ↑u ∧ ⇑b = Subtype.val
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>v : Set E<VAR>A : ι → Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>hv : Orthonormal 𝕜 Subtype.val<VAR>u₀ : Set E<VAR>hu₀s : u₀ ⊇ v<VAR>hu₀ : Orthonormal 𝕜 Subtype.val<VAR>hu₀_max : ∀ u ⊇ u₀, Orthonormal 𝕜 Subtype.val → u = u₀<GOAL>∃ u b, v ⊆ ↑u ∧ ⇑b = Subtype.val
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>v : Set E<VAR>A : ι → Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>hv : Orthonormal 𝕜 Subtype.val<VAR>u₀ : Set E<VAR>hu₀s : u₀ ⊇ v<VAR>hu₀ : Orthonormal 𝕜 Subtype.val<VAR>hu₀_max : (span 𝕜 u₀)ᗮ = ⊥<GOAL>∃ u b, v ⊆ ↑u ∧ ⇑b = Subtype.val
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>v : Set E<VAR>A : ι → Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>hv : Orthonormal 𝕜 Subtype.val<VAR>u₀ : Set E<VAR>hu₀s : u₀ ⊇ v<VAR>hu₀ : Orthonormal 𝕜 Subtype.val<VAR>hu₀_max : (span 𝕜 u₀)ᗮ = ⊥<VAR>hu₀_finite : u₀.Finite<GOAL>∃ u b, v ⊆ ↑u ∧ ⇑b = Subtype.val
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>v : Set E<VAR>A : ι → Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>hv : Orthonormal 𝕜 Subtype.val<VAR>u₀ : Set E<VAR>hu₀s : u₀ ⊇ v<VAR>hu₀ : Orthonormal 𝕜 Subtype.val<VAR>hu₀_max : (span 𝕜 u₀)ᗮ = ⊥<VAR>hu₀_finite : u₀.Finite<VAR>u : Finset E := hu₀_finite.toFinset<VAR>fu : { x // x ∈ u } ≃ ↑u₀ := hu₀_finite.subtypeEquivToFinset.symm<GOAL>∃ u b, v ⊆ ↑u ∧ ⇑b = Subtype.val
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>v : Set E<VAR>A : ι → Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>hv : Orthonormal 𝕜 Subtype.val<VAR>u₀ : Set E<VAR>hu₀s : u₀ ⊇ v<VAR>hu₀ : Orthonormal 𝕜 Subtype.val<VAR>hu₀_max : (span 𝕜 u₀)ᗮ = ⊥<VAR>hu₀_finite : u₀.Finite<VAR>u : Finset E := hu₀_finite.toFinset<VAR>fu : { x // x ∈ u } ≃ ↑u₀ := hu₀_finite.subtypeEquivToFinset.symm<VAR>hu : Orthonormal 𝕜 Subtype.val<GOAL>∃ u b, v ⊆ ↑u ∧ ⇑b = Subtype.val
<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>G : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<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_2<VAR>inst✝² : DecidableEq ι<VAR>𝔸' : Type u_3<VAR>inst✝¹ : NormedCommRing 𝔸'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → 𝕜 → 𝔸'<VAR>f' : ι → 𝔸'<VAR>hf : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x<GOAL>HasDerivWithinAt (fun x => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) s x
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<GOAL>toLaurent X = T 1
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>this : X = (monomial 1) 1<GOAL>toLaurent X = T 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<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>μ ν : Measure α<VAR>s t : Set α<VAR>f g : α → E<GOAL>⨍ (x : α), 0 ∂μ = 0
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>E : B → Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e : Pretrivialization F TotalSpace.proj<VAR>b : B<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<GOAL>Continuous (TotalSpace.mk b)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>E : B → Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e✝ : Pretrivialization F TotalSpace.proj<VAR>b : B<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯<GOAL>Continuous (TotalSpace.mk b)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>E : B → Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e✝ : Pretrivialization F TotalSpace.proj<VAR>b : B<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯<GOAL>Continuous (↑e.toPartialHomeomorph ∘ TotalSpace.mk b)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : AddCommGroup P<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R P<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<GOAL>⟨⅟2, ⋯⟩ • (Q₁.prod Q₂).polarBilin = LinearMap.compl₁₂ (⟨⅟2, ⋯⟩ • Q₁.polarBilin) (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) + LinearMap.compl₁₂ (⟨⅟2, ⋯⟩ • Q₂.polarBilin) (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : AddCommGroup P<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R P<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<GOAL>⟨⅟2, ⋯⟩ • LinearMap.compl₁₂ Q₁.polarBilin (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) + ⟨⅟2, ⋯⟩ • LinearMap.compl₁₂ Q₂.polarBilin (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂) = LinearMap.compl₁₂ (⟨⅟2, ⋯⟩ • Q₁.polarBilin) (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) + LinearMap.compl₁₂ (⟨⅟2, ⋯⟩ • Q₂.polarBilin) (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M✝ : εNFA α σ<VAR>S : Set σ<VAR>x : List α<VAR>s : σ<VAR>a : α<VAR>M : NFA α σ<GOAL>M.toεNFA.accepts = M.accepts
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M✝ : εNFA α σ<VAR>S : Set σ<VAR>x : List α<VAR>s : σ<VAR>a : α<VAR>M : NFA α σ<GOAL>{x | ∃ S ∈ M.toεNFA.accept, S ∈ M.evalFrom M.toεNFA.start x} = M.accepts
<VAR>m✝ n✝ m n : ℕ<GOAL>m ! * (m + 1) ^ (n + 1) ≤ (m + (n + 1))!
<VAR>m✝ n✝ m n : ℕ<GOAL>m ! * (m + 1) ^ n * (m + 1) ≤ (m + n)! * (m + n + 1)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X✝ Y✝ : Set α<VAR>e : α<VAR>M : Matroid α<VAR>X Y : Set α<GOAL>M.closure (M.closure X ∪ Y) = M.closure (X ∪ Y)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>H : p ∈ (comap f I).minimalPrimes<GOAL>∃ p' ∈ I.minimalPrimes, comap f p' = p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>H : p ∈ (comap f I).minimalPrimes<VAR>p' : Ideal S<VAR>h₁ : p'.IsPrime<VAR>h₂ : I ≤ p'<VAR>h₃ : comap f p' = p<GOAL>∃ p' ∈ I.minimalPrimes, comap f p' = p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>H : p ∈ (comap f I).minimalPrimes<VAR>p' : Ideal S<VAR>h₁ : p'.IsPrime<VAR>h₂ : I ≤ p'<VAR>h₃ : comap f p' = p<VAR>q : Ideal S<VAR>hq : q ∈ I.minimalPrimes<VAR>hq' : q ≤ p'<GOAL>∃ p' ∈ I.minimalPrimes, comap f p' = p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>H : p ∈ (comap f I).minimalPrimes<VAR>p' : Ideal S<VAR>h₁ : p'.IsPrime<VAR>h₂ : I ≤ p'<VAR>h₃ : comap f p' = p<VAR>q : Ideal S<VAR>hq : q ∈ I.minimalPrimes<VAR>hq' : q ≤ p'<GOAL>p = comap f q
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>H : p ∈ (comap f I).minimalPrimes<VAR>p' : Ideal S<VAR>h₁ : p'.IsPrime<VAR>h₂ : I ≤ p'<VAR>h₃ : comap f p' = p<VAR>q : Ideal S<VAR>hq : q ∈ I.minimalPrimes<VAR>hq' : q ≤ p'<VAR>this : q.IsPrime<GOAL>p = comap f q
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>H : p ∈ (comap f I).minimalPrimes<VAR>p' : Ideal S<VAR>h₁ : p'.IsPrime<VAR>h₂ : I ≤ p'<VAR>h₃ : comap f p' = p<VAR>q : Ideal S<VAR>hq : q ∈ I.minimalPrimes<VAR>hq' : q ≤ p'<VAR>this✝ : q.IsPrime<VAR>this : comap f q ≤ p<GOAL>p = comap f q
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν = (X + (1 - X)) ^ n
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν = ∑ m ∈ Finset.range (n + 1), X ^ m * (1 - X) ^ (n - m) * ↑(n.choose m)
<VAR>F : Type u_1<VAR>inst✝⁵ : Field F<VAR>E : Type u_2<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>H : Subgroup (E ≃ₐ[F] E)<VAR>K : IntermediateField F E<VAR>inst✝² : DecidablePred fun x => x ∈ K.fixingSubgroup<VAR>inst✝¹ : FiniteDimensional F E<VAR>inst✝ : IsGalois F E<GOAL>Fintype.card ↥K.fixingSubgroup = finrank (↥K) E
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<GOAL>0 < T n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<GOAL>(a + b) ^ 2 ≤ 2 * (a ^ 2 + b ^ 2)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<GOAL>a * b + b * a ≤ a * a + b * b
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>h✝ : a ≤ b<GOAL>a * b + b * a ≤ a * a + b * b
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>h✝ : b ≤ a<GOAL>a * b + b * a ≤ a * a + b * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Union α<VAR>a b : α<GOAL>some a ∪ some b = some (a ∪ b)
<VAR>d✝ : ℤ<VAR>c d b : ℕ<GOAL>Nonnegg c d (-↑0) ↑b → SqLe 0 d b c
<VAR>d✝ : ℤ<VAR>c d a b : ℕ<GOAL>Nonnegg c d (-↑(a + 1)) ↑b ↔ SqLe (a + 1) d b c
<VAR>d✝ : ℤ<VAR>c d a b : ℕ<GOAL>Nonnegg c d (Int.negSucc a) ↑b ↔ SqLe (a + 1) d b c
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<GOAL>∀ (a : List R[X]), (prod ⟦a⟧).natDegree ≤ (Multiset.map natDegree ⟦a⟧).sum
<VAR>n✝ m n : ℕ<VAR>hn : n ≠ 0<GOAL>m ∈ n.properDivisors ↔ ∃ k > 1, n = m * k
<VAR>n✝ m n : ℕ<VAR>hn : n ≠ 0<VAR>h : m ∈ n.properDivisors<GOAL>n = m * (n / m)
<VAR>n✝ m n : ℕ<VAR>hn : n ≠ 0<GOAL>(∃ k > 1, n = m * k) → m ∈ n.properDivisors
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c✝ c : Con M<VAR>f : M → N<VAR>H : ∀ (x y : M), f (x * y) = f x * f y<VAR>h : mulKer f H ≤ c<VAR>hf : Surjective f<GOAL>c.mapGen f = c.mapOfSurjective f H h hf
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c✝ c : Con M<VAR>f : M → N<VAR>H : ∀ (x y : M), f (x * y) = f x * f y<VAR>h : mulKer f H ≤ c<VAR>hf : Surjective f<GOAL>c.mapGen f = conGen ⇑(c.mapOfSurjective f H h hf)
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>F : Type u_3<VAR>inst✝ : Field F<VAR>w : InfinitePlace K<GOAL>¬w.IsComplex ↔ w.IsReal
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<GOAL>⌈a + b⌉ ≤ ⌈a⌉ + ⌈b⌉
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<GOAL>a + b ≤ ↑⌈a⌉ + ↑⌈b⌉
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → ℕ<GOAL>Odd (∑ i ∈ s, f i) ↔ Odd (filter (fun x => Odd (f x)) s).card
<VAR>x✝ y✝ z x : ℝ<VAR>hx : 0 < x<VAR>y : ℝ<GOAL>x ^ y = rexp (log x * y)
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>k : ℤ<VAR>hk : k ≠ 0<GOAL>PythagoreanTriple (k * x) (k * y) (k * z) ↔ PythagoreanTriple x y z
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>k : ℤ<VAR>hk : k ≠ 0<GOAL>PythagoreanTriple (k * x) (k * y) (k * z) → PythagoreanTriple x y z
<VAR>x y z : ℤ<VAR>h✝ : PythagoreanTriple x y z<VAR>k : ℤ<VAR>hk : k ≠ 0<VAR>h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)<GOAL>x * x + y * y = z * z
<VAR>x y z : ℤ<VAR>h✝ : PythagoreanTriple x y z<VAR>k : ℤ<VAR>hk : k ≠ 0<VAR>h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)<GOAL>(x * x + y * y) * (k * k) = z * z * (k * k)
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>x : α<GOAL>(countP p) (of x) = if p x then Multiplicative.ofAdd 1 else 1
<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>b : ℝ≥0<GOAL>ENNReal.ofReal a < ↑b ↔ a < (↑b).toReal
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ℝ × ℝ → E<VAR>f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E<VAR>a b : ℝ × ℝ<VAR>hle : a ≤ b<VAR>s : Set (ℝ × ℝ)<VAR>hs : s.Countable<VAR>Hcf : ContinuousOn f (Set.Icc a b)<VAR>Hcg : ContinuousOn g (Set.Icc a b)<VAR>Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x<VAR>Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x<VAR>Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm<GOAL>∫ (x : ℝ × ℝ) in Set.Icc a b, (f' x) (1, 0) + (g' x) (0, 1) = ∑ i : Fin 2, ((∫ (x : Fin 1 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove), ![f, g] i (e.symm (i.insertNth (e b i) x))) - ∫ (x : Fin 1 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove), ![f, g] i (e.symm (i.insertNth (e a i) x)))
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ℝ × ℝ → E<VAR>f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E<VAR>a b : ℝ × ℝ<VAR>hle : a ≤ b<VAR>s : Set (ℝ × ℝ)<VAR>hs : s.Countable<VAR>Hcf : ContinuousOn f (Set.Icc a b)<VAR>Hcg : ContinuousOn g (Set.Icc a b)<VAR>Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x<VAR>Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x<VAR>Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm<GOAL>∀ (x y : ℝ × ℝ), e x ≤ e y ↔ x ≤ y
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ℝ × ℝ → E<VAR>f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E<VAR>a b : ℝ × ℝ<VAR>hle : a ≤ b<VAR>s : Set (ℝ × ℝ)<VAR>hs : s.Countable<VAR>Hcf : ContinuousOn f (Set.Icc a b)<VAR>Hcg : ContinuousOn g (Set.Icc a b)<VAR>Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x<VAR>Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x<VAR>Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm<GOAL>MeasurePreserving (⇑e) volume volume
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ℝ × ℝ → E<VAR>f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E<VAR>a b : ℝ × ℝ<VAR>hle : a ≤ b<VAR>s : Set (ℝ × ℝ)<VAR>hs : s.Countable<VAR>Hcf : ContinuousOn f (Set.Icc a b)<VAR>Hcg : ContinuousOn g (Set.Icc a b)<VAR>Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x<VAR>Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x<VAR>Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm<GOAL>∀ (i : Fin (1 + 1)), ContinuousOn (![f, g] i) (Set.Icc a b)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ℝ × ℝ → E<VAR>f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E<VAR>a b : ℝ × ℝ<VAR>hle : a ≤ b<VAR>s : Set (ℝ × ℝ)<VAR>hs : s.Countable<VAR>Hcf : ContinuousOn f (Set.Icc a b)<VAR>Hcg : ContinuousOn g (Set.Icc a b)<VAR>Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x<VAR>Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x<VAR>Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm<VAR>x : ℝ × ℝ<VAR>hx : x ∈ interior (Set.Icc a b) \ s<GOAL>∀ (i : Fin (1 + 1)), HasFDerivAt (![f, g] i) (![f', g'] i x) x
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ℝ × ℝ → E<VAR>f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E<VAR>a b : ℝ × ℝ<VAR>hle : a ≤ b<VAR>s : Set (ℝ × ℝ)<VAR>hs : s.Countable<VAR>Hcf : ContinuousOn f (Set.Icc a b)<VAR>Hcg : ContinuousOn g (Set.Icc a b)<VAR>Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x<VAR>Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x<VAR>Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm<GOAL>∀ (x : ℝ × ℝ), (f' x) (1, 0) + (g' x) (0, 1) = ∑ i : Fin (1 + 1), (![f', g'] i x) (e.symm (Pi.single i 1))
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ℝ × ℝ → E<VAR>f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E<VAR>a b : ℝ × ℝ<VAR>hle : a ≤ b<VAR>s : Set (ℝ × ℝ)<VAR>hs : s.Countable<VAR>Hcf : ContinuousOn f (Set.Icc a b)<VAR>Hcg : ContinuousOn g (Set.Icc a b)<VAR>Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x<VAR>Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x<VAR>Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm<GOAL>∑ i : Fin 2, ((∫ (x : Fin 1 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove), ![f, g] i (e.symm (i.insertNth (e b i) x))) - ∫ (x : Fin 1 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove), ![f, g] i (e.symm (i.insertNth (e a i) x))) = ((∫ (y : ℝ) in Set.Icc a.2 b.2, f (b.1, y)) - ∫ (y : ℝ) in Set.Icc a.2 b.2, f (a.1, y)) + ((∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, b.2)) - ∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, a.2))