ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹¹ : MeasurableSpace X<VAR>inst✝¹⁰ : TopologicalSpace X<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : TopologicalSpace Y<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f✝ g✝ : X → E<VAR>μ : Measure X<VAR>s✝ : Set X<VAR>inst✝⁵ : OpensMeasurableSpace X<VAR>A K : Set X<VAR>inst✝⁴ : LocallyCompactSpace X<VAR>inst✝³ : T2Space X<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SecondCountableTopologyEither X E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : X → 𝕜<VAR>g : X → E<VAR>s : Set X<VAR>hs : IsOpen s<VAR>hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ<VAR>hg : ContinuousOn g s<GOAL>∀ k ⊆ s, IsCompact k → IntegrableOn (fun x => f x • g x) k μ
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 2 ≠ 0<GOAL>W.preΨ₄.leadingCoeff = 2
<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>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w✝ : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>w : InfinitePlace k<VAR>hw : ¬IsUnramifiedIn K w<GOAL>Even (finrank k K)
<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>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>v : InfinitePlace K<VAR>hw : ¬IsUnramifiedIn K ((fun x => x.comap (algebraMap k K)) v)<GOAL>Even (finrank k K)
<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>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>v : InfinitePlace K<VAR>hw : ¬IsUnramified k v<GOAL>Even (finrank k K)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<GOAL>(κ.singularPart η) a = 0 ↔ κ a ≪ η a
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<GOAL>(κ.singularPart η) a = 0 ↔ (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ≪ η a
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>h : (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ≪ η a<GOAL>(κ.singularPart η) a = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>h : (η.withDensity (κ.rnDeriv η)) a ≪ η a ∧ (κ.singularPart η) a ≪ η a<GOAL>(κ.singularPart η) a = 0
<VAR>G : PGame<VAR>inst✝ : G.Impartial<GOAL>G.grundyValue = 0 ↔ G ≈ 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>inst✝ : l.NeBot<VAR>h : Tendsto f l atBot<GOAL>Tendsto (fun x => f x * r) l atTop ↔ r < 0
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f : β → E<GOAL>∫ (z : α × β), f z.2 ∂μ.prod ν = (μ univ).toReal • ∫ (y : β), f y ∂ν
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>U : Set (ProjectiveSpectrum 𝒜)<GOAL>IsOpen U ↔ ∃ s, Uᶜ = zeroLocus 𝒜 s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>U : Set (ProjectiveSpectrum 𝒜)<GOAL>IsOpen U ↔ ∃ s, zeroLocus 𝒜 s = Uᶜ
<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✝ t t' : TopologicalSpace X<VAR>H : ∀ (x : X), 𝓝 x = 𝓝 x<VAR>x✝ : Set X<GOAL>IsOpen x✝ ↔ IsOpen x✝
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝² : TopologicalSpace X✝<VAR>X : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>U : Set X<VAR>inst✝ : (x : X) → Decidable (x ∈ U)<VAR>hU : IsClopen U<VAR>x✝ : X<GOAL>x✝ ∈ ⇑(ofIsClopen hU) ⁻¹' {0} ↔ x✝ ∈ U
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝² : TopologicalSpace X✝<VAR>X : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>U : Set X<VAR>inst✝ : (x : X) → Decidable (x ∈ U)<VAR>hU : IsClopen U<VAR>x✝ : X<GOAL>x✝ ∉ U → False ↔ x✝ ∈ U
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<GOAL>(p - q).degree ≤ max p.degree q.degree
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type ?u.24237<VAR>inst✝ : MulAction R X<VAR>r r' r₁ r₂ : R<VAR>s t : ↥S<VAR>h : ↑t * r = ↑t * r'<VAR>r₁' : R<VAR>t' : ↥S<VAR>hr₁ : ↑t' * r₁ = r₁' * ↑t<GOAL>r₁ * r * r₂ /ₒ s = r₁ * r' * r₂ /ₒ s
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type ?u.24237<VAR>inst✝ : MulAction R X<VAR>r r' r₁ r₂ : R<VAR>s t : ↥S<VAR>h : ↑t * r = ↑t * r'<VAR>r₁' : R<VAR>t' : ↥S<VAR>hr₁ : ↑t' * r₁ = r₁' * ↑t<GOAL>t' • (r₁ * r * r₂) /ₒ (t' * s) = t' • (r₁ * r' * r₂) /ₒ (t' * s)
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type ?u.24237<VAR>inst✝ : MulAction R X<VAR>r r' r₁ r₂ : R<VAR>s t : ↥S<VAR>h : ↑t * r = ↑t * r'<VAR>r₁' : R<VAR>t' : ↥S<VAR>hr₁ : ↑t' * r₁ = r₁' * ↑t<GOAL>t' • (r₁ * r * r₂) = t' • (r₁ * r' * r₂)
<VAR>b : ℝ<VAR>hb₀ : -1 < b<VAR>hb₁ : b < 1<GOAL>Tendsto (fun x => b ^ x) atTop (𝓝 0)
<VAR>b : ℝ<VAR>hb₀ : -1 < b<VAR>hb₁ : b < 1<VAR>hb : b < 0<GOAL>Tendsto (fun x => b ^ x) atTop (𝓝 0)
<VAR>hb₀ : -1 < 0<VAR>hb₁ : 0 < 1<GOAL>Tendsto (fun x => 0 ^ x) atTop (𝓝 0)
<VAR>b : ℝ<VAR>hb₀ : -1 < b<VAR>hb₁ : b < 1<VAR>hb : 0 < b<GOAL>Tendsto (fun x => b ^ x) atTop (𝓝 0)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>x : HahnSeries Γ R<GOAL>x.support.Nonempty ↔ x ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>f : σ → τ<VAR>φ : MvPolynomial σ R<GOAL>((rename f) φ).degrees ⊆ Multiset.map f φ.degrees
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>x : β<VAR>n : ℕ<GOAL>‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>x : β<VAR>n : ℕ<VAR>this : edist (↑(approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist y₀ (f x)<GOAL>‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>x : β<VAR>n : ℕ<VAR>this : edist (↑(approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist (f x) y₀<GOAL>‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>x : β<VAR>n : ℕ<VAR>this : ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ↑‖f x - y₀‖₊<GOAL>‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → β → β<VAR>b : β<VAR>a : α<VAR>l : List α<GOAL>scanr f b (a :: l) = foldr f b (a :: l) :: scanr f b l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → β → β<VAR>b : β<VAR>a : α<VAR>l : List α<GOAL>f a (foldr (fun a x => (f a x.1, x.1 :: x.2)) (b, []) l).1 = f a (foldr f b l)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>r : AdicCauchySequence I R<VAR>h : I ^ m = I ^ m • ⊤<GOAL>(Ideal.Quotient.mk (I ^ m)) (↑r n) = (Ideal.Quotient.mk (I ^ m)) (↑r m)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>r : AdicCauchySequence I R<VAR>h : I ^ m = I ^ m • ⊤<GOAL>Submodule.Quotient.mk (↑r n) = Submodule.Quotient.mk (↑r m)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : HeytingAlgebra α<VAR>a b c : α<VAR>inst✝ : Nontrivial α<VAR>h : a = aᶜ<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : HeytingAlgebra α<VAR>b c : α<VAR>inst✝ : Nontrivial α<VAR>h : ⊥ = ⊥ᶜ<GOAL>False
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : WithLp p (α × β)<GOAL>edist x y ≤ ↑(2 ^ (1 / p).toReal) * edist ((WithLp.equiv p (α × β)) x) ((WithLp.equiv p (α × β)) y)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>hp : Fact (1 ≤ ⊤)<VAR>x y : WithLp ⊤ (α × β)<GOAL>edist x y ≤ ↑(2 ^ (1 / ⊤).toReal) * edist ((WithLp.equiv ⊤ (α × β)) x) ((WithLp.equiv ⊤ (α × β)) y)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : WithLp p (α × β)<VAR>h : 1 ≤ p.toReal<GOAL>edist x y ≤ ↑(2 ^ (1 / p).toReal) * edist ((WithLp.equiv p (α × β)) x) ((WithLp.equiv p (α × β)) y)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b✝ : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p q b : R[X]<VAR>P : R[X][X]<GOAL>P ∈ Ideal.span {C (X - C a), X - C b} ↔ eval a (eval b P) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b✝ : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p q b : R[X]<VAR>P : R[X][X]<GOAL>(∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P) ↔ eval a (eval b P) = 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s✝ s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i✝ : ι<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>s : Set (α i)<GOAL>univ.pi (update (fun j => univ) i s) = eval i ⁻¹' s
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>φ ψ : MvPolynomial σ R<GOAL>↑φ = 1 ↔ φ = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : CommSemiring B<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R B<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module B M<VAR>inst✝ : Module R M<VAR>D D1 D2 : Derivation R A M<VAR>r : R<VAR>a b : A<VAR>n : ℕ<GOAL>D ↑n = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts ys : List α<VAR>f : List α → β<GOAL>map f (permutationsAux2 t ts [] ys id).2 = (permutationsAux2 t ts [] ys f).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts ys : List α<VAR>f : List α → β<GOAL>(permutationsAux2 (id t) ts (map f []) ys ?f').2 = (permutationsAux2 t ts [] ys f).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts ys : List α<VAR>f : List α → β<GOAL>List α → β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts ys : List α<VAR>f : List α → β<GOAL>∀ (a : List α), f (id a) = ?f' (map id a)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c c₁ c₂ p₁ p₂ : P<GOAL>p₁ ∈ perpBisector p₁ p₂ ↔ p₁ = p₂
<VAR>a b : Rat<GOAL>a - b = mkRat (a.num * ↑b.den - b.num * ↑a.den) (a.den * b.den)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>t : Finset (α × β × γ)<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>x✝ : α × β × γ<VAR>ε : 𝕜<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableEq γ<VAR>x y z : α ⊕ β ⊕ γ<GOAL>(graph t).Adj x y → (graph t).Adj x z → (graph t).Adj y z → ∃ a b c, {in₀ a, in₁ b, in₂ c} = {x, y, z} ∧ (graph t).Adj (in₀ a) (in₁ b) ∧ (graph t).Adj (in₀ a) (in₂ c) ∧ (graph t).Adj (in₁ b) (in₂ c)
<VAR>α : Type u_1<VAR>p q✝ q : ℚ≥0<VAR>n : ℕ<GOAL>(q ^ n).num = q.num ^ n
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f x : σ → R<VAR>p : MvPolynomial σ R<VAR>s : R<GOAL>(eval x) (s • p) = s * (eval x) p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{u_6, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E E' : L.RightExtension F<VAR>h✝ h : E.IsPointwiseRightKanExtension<VAR>G : L.RightExtension F<VAR>f₁ f₂ : G ⟶ E<VAR>Y : D<GOAL>f₁.left.app Y = f₂.left.app Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{u_6, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E E' : L.RightExtension F<VAR>h✝ h : E.IsPointwiseRightKanExtension<VAR>G : L.RightExtension F<VAR>f₁ f₂ : G ⟶ E<VAR>Y : D<GOAL>∀ (j : StructuredArrow Y L), f₁.left.app Y ≫ (E.coneAt Y).π.app j = f₂.left.app Y ≫ (E.coneAt Y).π.app j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{u_6, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E E' : L.RightExtension F<VAR>h✝ h : E.IsPointwiseRightKanExtension<VAR>G : L.RightExtension F<VAR>f₁ f₂ : G ⟶ E<VAR>Y : D<VAR>X : StructuredArrow Y L<GOAL>f₁.left.app Y ≫ (E.coneAt Y).π.app X = f₂.left.app Y ≫ (E.coneAt Y).π.app X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{u_6, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E E' : L.RightExtension F<VAR>h✝ h : E.IsPointwiseRightKanExtension<VAR>G : L.RightExtension F<VAR>f₁ f₂ : G ⟶ E<VAR>Y : D<VAR>X : StructuredArrow Y L<VAR>eq₁ : (((whiskeringLeft C D H).obj L).map f₁.left ≫ E.hom).app X.right = G.hom.app X.right<GOAL>f₁.left.app Y ≫ (E.coneAt Y).π.app X = f₂.left.app Y ≫ (E.coneAt Y).π.app X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{u_6, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E E' : L.RightExtension F<VAR>h✝ h : E.IsPointwiseRightKanExtension<VAR>G : L.RightExtension F<VAR>f₁ f₂ : G ⟶ E<VAR>Y : D<VAR>X : StructuredArrow Y L<VAR>eq₁ : (((whiskeringLeft C D H).obj L).map f₁.left ≫ E.hom).app X.right = G.hom.app X.right<VAR>eq₂ : (((whiskeringLeft C D H).obj L).map f₂.left ≫ E.hom).app X.right = G.hom.app X.right<GOAL>f₁.left.app Y ≫ (E.coneAt Y).π.app X = f₂.left.app Y ≫ (E.coneAt Y).π.app X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{u_6, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E E' : L.RightExtension F<VAR>h✝ h : E.IsPointwiseRightKanExtension<VAR>G : L.RightExtension F<VAR>f₁ f₂ : G ⟶ E<VAR>Y : D<VAR>X : StructuredArrow Y L<VAR>eq₁ : f₁.left.app (L.obj X.right) ≫ E.hom.app X.right = G.hom.app X.right<VAR>eq₂ : f₂.left.app (L.obj X.right) ≫ E.hom.app X.right = G.hom.app X.right<GOAL>f₁.left.app Y ≫ E.left.map X.hom ≫ E.hom.app X.right = f₂.left.app Y ≫ E.left.map X.hom ≫ E.hom.app X.right
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Zero α<VAR>s : Finset ι<VAR>f : ι →₀ α<VAR>t : ι →₀ Finset α<VAR>ht : t.support ⊆ s<GOAL>f ∈ s.finsupp ⇑t ↔ ∀ (i : ι), f i ∈ t i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Zero α<VAR>s : Finset ι<VAR>f : ι →₀ α<VAR>t : ι →₀ Finset α<VAR>ht : t.support ⊆ s<VAR>i : ι<VAR>h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)<GOAL>f i ∈ t i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Zero α<VAR>s : Finset ι<VAR>f : ι →₀ α<VAR>t : ι →₀ Finset α<VAR>ht : t.support ⊆ s<VAR>i : ι<VAR>h : f i ∈ t i<VAR>hi : i ∈ f.support<VAR>H : t i = 0<GOAL>f i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν μ : Measure α<VAR>inst✝ : SigmaFinite μ<GOAL>μ.rnDeriv μ =ᶠ[ae μ] fun x => 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>h : μ.withDensity (μ.rnDeriv μ) + μ.singularPart μ = μ<GOAL>μ.rnDeriv μ =ᶠ[ae μ] fun x => 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>h : μ.withDensity (μ.rnDeriv μ) = μ<GOAL>μ.rnDeriv μ =ᶠ[ae μ] fun x => 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>h : μ.withDensity (μ.rnDeriv μ) = μ.withDensity 1<VAR>h_one : μ = μ.withDensity 1<GOAL>μ.rnDeriv μ =ᶠ[ae μ] fun x => 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>h : μ.withDensity (μ.rnDeriv μ) = μ.withDensity 1<VAR>h_one : μ = μ.withDensity 1<GOAL>AEMeasurable 1 μ
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>inst✝² : G.Full<VAR>inst✝¹ : G.Faithful<VAR>I : D<VAR>hI : Injective (G.obj I)<VAR>X Y : D<VAR>f : X ⟶ I<VAR>g : X ⟶ Y<VAR>inst✝ : Mono g<VAR>this : PreservesLimitsOfSize.{0, 0, u_2, v₁, u_1, u₁} G<GOAL>∃ h, g ≫ h = f
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>inst✝² : G.Full<VAR>inst✝¹ : G.Faithful<VAR>I : D<VAR>hI : Injective (G.obj I)<VAR>X Y : D<VAR>f : X ⟶ I<VAR>g : X ⟶ Y<VAR>inst✝ : Mono g<VAR>this : PreservesLimitsOfSize.{0, 0, u_2, v₁, u_1, u₁} G<VAR>w : G.obj Y ⟶ G.obj I<VAR>h : G.map g ≫ w = G.map f<GOAL>∃ h, g ≫ h = f
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>inst✝² : G.Full<VAR>inst✝¹ : G.Faithful<VAR>I : D<VAR>hI : Injective (G.obj I)<VAR>X Y : D<VAR>f : X ⟶ I<VAR>g : X ⟶ Y<VAR>inst✝ : Mono g<VAR>this : PreservesLimitsOfSize.{0, 0, u_2, v₁, u_1, u₁} G<VAR>w : G.obj Y ⟶ G.obj I<VAR>h : G.map g ≫ w = G.map f<GOAL>g ≫ inv (adj.counit.app Y) ≫ F.map w ≫ adj.counit.app I = f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>v w : E<VAR>h : ⟪v, w⟫_𝕜 = 0<GOAL>‖w - v‖ = ‖w + v‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>v w : E<VAR>h : ⟪v, w⟫_𝕜 = 0<GOAL>‖w - v‖ * ‖w - v‖ = ‖w + v‖ * ‖w + v‖
<VAR>m n✝ : ℕ<VAR>α✝ : Fin (n✝ + 1) → Type u<VAR>x : α✝ (last n✝)<VAR>q : (i : Fin (n✝ + 1)) → α✝ i<VAR>p : (i : Fin n✝) → α✝ i.castSucc<VAR>i✝ : Fin n✝<VAR>y : α✝ i✝.castSucc<VAR>z : α✝ (last n✝)<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>f : Fin n → α<VAR>i : Fin n<GOAL>(snoc f a ∘ castSucc) i = f i
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : BorelSpace β<VAR>f : ι → Ω → β<VAR>i j : ι<VAR>s : ι → Set Ω<VAR>hf : ∀ (i : ι), StronglyMeasurable (f i)<VAR>hfi : iIndepFun (fun x => mβ) f μ<VAR>hij : i < j<GOAL>Indep (MeasurableSpace.comap (f j) mβ) (↑(Filtration.natural f hf) i) μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : BorelSpace β<VAR>f : ι → Ω → β<VAR>i j : ι<VAR>s : ι → Set Ω<VAR>hf : ∀ (i : ι), StronglyMeasurable (f i)<VAR>hfi : iIndepFun (fun x => mβ) f μ<VAR>hij : i < j<GOAL>Indep (⨆ k ∈ {j}, MeasurableSpace.comap (f k) mβ) (⨆ k ∈ {k | k ≤ i}, MeasurableSpace.comap (f k) mβ) μ
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>c✝ d✝ : C<VAR>f : c✝ ⟶ d✝<GOAL>Groupoid.inv f ≫ 𝟙 c✝ ≫ f ∈ discrete.arrows d✝ d✝
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>c✝ d✝ : C<VAR>f : c✝ ⟶ d✝<GOAL>𝟙 d✝ ∈ discrete.arrows d✝ d✝
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝² : NonUnitalNonAssocRing R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalAddGroup R<VAR>hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)<VAR>hmul_left : ∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)<VAR>hmul_right : ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)<GOAL>Continuous fun p => p.1 * p.2
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>μ : Measure E<GOAL>μ.toSphere univ = ↑(dim E) * μ (ball 0 1 \ {0})
<VAR>Γ✝ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁹ : PartialOrder Γ✝<VAR>inst✝⁸ : PartialOrder Γ'<VAR>inst✝⁷ : VAdd Γ✝ Γ'<VAR>inst✝⁶ : IsOrderedCancelVAdd Γ✝ Γ'<VAR>inst✝⁵ : AddCommMonoid V<VAR>Γ : Type u_5<VAR>inst✝⁴ : OrderedAddCommMonoid Γ<VAR>inst✝³ : AddAction Γ Γ'<VAR>inst✝² : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝¹ : MonoidWithZero R<VAR>inst✝ : MulActionWithZero R V<VAR>x : HahnModule Γ' R V<VAR>g : Γ'<GOAL>((of R).symm (1 • x)).coeff g = ((of R).symm x).coeff g
<GOAL>⋂ r, Iic ↑r = ∅
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>A : C<VAR>i₁₂ : I₁₂<VAR>f g : (K.total c₁₂).X i₁₂ ⟶ A<VAR>h : ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂), K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ f = K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ g<GOAL>f = g