ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup D<VAR>inst✝⁵ : NormedSpace ℝ D<VAR>inst✝⁴ : MeasurableSpace D<VAR>inst✝³ : BorelSpace D<VAR>inst✝² : SecondCountableTopology D<VAR>inst✝¹ : FiniteDimensional ℝ D<VAR>μ : Measure D<VAR>inst✝ : μ.HasTemperateGrowth<VAR>f : D → E<VAR>C₁ C₂ : ℝ<VAR>k : ℕ<VAR>hf : ∀ (x : D), ‖f x‖ ≤ C₁<VAR>h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂<VAR>h''f : AEStronglyMeasurable f μ<GOAL>AEStronglyMeasurable (fun x => ‖x‖ ^ k * ‖f x‖) μ
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup D<VAR>inst✝⁵ : NormedSpace ℝ D<VAR>inst✝⁴ : MeasurableSpace D<VAR>inst✝³ : BorelSpace D<VAR>inst✝² : SecondCountableTopology D<VAR>inst✝¹ : FiniteDimensional ℝ D<VAR>μ : Measure D<VAR>inst✝ : μ.HasTemperateGrowth<VAR>f : D → E<VAR>C₁ C₂ : ℝ<VAR>k : ℕ<VAR>hf : ∀ (x : D), ‖f x‖ ≤ C₁<VAR>h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂<VAR>h''f : AEStronglyMeasurable f μ<GOAL>∀ᵐ (a : D) ∂μ, ‖‖a‖ ^ k * ‖f a‖‖ ≤ 2 ^ μ.integrablePower * (C₁ + C₂) * (1 + ‖a‖) ^ (-↑μ.integrablePower)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q r : ℚ<VAR>a : α<GOAL>Commute (↑r) a
<VAR>R✝ : Type u₁<VAR>inst✝⁶ : CommSemiring R✝<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝⁵ : CharP R✝ p<VAR>R : Type u₁<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CharP R p<VAR>inst✝² : PerfectRing R p<VAR>S : Type u₂<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CharP S p<VAR>f : R →+* S<VAR>r : R<VAR>n : ℕ<GOAL>(fun n => f ((⇑↑(frobeniusEquiv R p).symm)^[n] r)) (n + 1) ^ p = (fun n => f ((⇑↑(frobeniusEquiv R p).symm)^[n] r)) n
<VAR>R✝ : Type u₁<VAR>inst✝⁶ : CommSemiring R✝<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝⁵ : CharP R✝ p<VAR>R : Type u₁<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CharP R p<VAR>inst✝² : PerfectRing R p<VAR>S : Type u₂<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CharP S p<VAR>f : R →+* Ring.Perfection S p<VAR>r : R<VAR>n : ℕ<GOAL>(coeff S p 0) (f ((⇑(frobeniusEquiv R p).symm)^[n] r)) = (coeff S p n) (f r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set β<GOAL>range f = s ↔ (∀ (a : α), f a ∈ s) ∧ ∀ b ∈ s, ∃ a, f a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set β<GOAL>range f = s ↔ range f ⊆ s ∧ ∀ b ∈ s, ∃ a, f a = b
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : Encodable α<VAR>e : β ≃ α<VAR>n : ℕ<GOAL>(decode n).bind (some ∘ ⇑e.symm) = Option.map (⇑e.symm) (decode n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>C : ℝ<GOAL>Tendsto (fun n => C / ↑n) atTop (𝓝 0)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y x' y' : ℝ<VAR>hx : x ∈ uIcc x' y'<VAR>hy : y ∈ uIcc x' y'<GOAL>y ∈ uIcc y' x'
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y x' y' : ℝ<VAR>hx : x ∈ uIcc x' y'<VAR>hy : y ∈ uIcc x' y'<GOAL>x ∈ uIcc y' x'
<VAR>J : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>J' : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J'<VAR>e : J ≌ J'<VAR>inst✝ : HasColimitsOfShape J C<VAR>F : J' ⥤ C<GOAL>HasColimit F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>f g : α →ₛ β<GOAL>↑(piecewise univ ⋯ f g) = ↑f
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.length (cs.simple i * w) ≠ cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.length (cs.simple i * w) = cs.length (w⁻¹ * cs.simple i)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.length w = cs.length w⁻¹
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>p : F[X]<VAR>K : IntermediateField F E<GOAL>IsSplittingField F (↥K) p ↔ Splits (algebraMap F ↥K) p ∧ K = adjoin F (p.rootSet E)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>p : F[X]<VAR>K : IntermediateField F E<GOAL>Splits (algebraMap F ↥K) p → (Algebra.adjoin F (p.rootSet ↥K) = ⊤ ↔ K = adjoin F (p.rootSet E))
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>p : F[X]<VAR>K : IntermediateField F E<GOAL>Splits (algebraMap F ↥K) p → (Algebra.adjoin F (p.rootSet ↥K) = ⊤ ↔ K.toSubalgebra = Algebra.adjoin F (p.rootSet E))
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>p : F[X]<VAR>K : IntermediateField F E<VAR>hp : Splits (algebraMap F ↥K) p<GOAL>Algebra.adjoin F (p.rootSet E) = K.val.range ↔ K.toSubalgebra = Algebra.adjoin F (p.rootSet E)
<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>ν : Measure α<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → E<VAR>s : Set α<VAR>hs : s.Countable<VAR>hf : Integrable f (μ.restrict s)<GOAL>∫ (a : α) in s, f a ∂μ = ∑' (a : ↑s), (μ {↑a}).toReal • f ↑a
<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>ν : Measure α<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → E<VAR>s : Set α<VAR>hs : s.Countable<VAR>hf : Integrable f (μ.restrict s)<VAR>hi : Countable { x // x ∈ s }<GOAL>∫ (a : α) in s, f a ∂μ = ∑' (a : ↑s), (μ {↑a}).toReal • f ↑a
<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>ν : Measure α<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → E<VAR>s : Set α<VAR>hs : s.Countable<VAR>hf : Integrable f (μ.restrict s)<VAR>hi : Countable { x // x ∈ s }<VAR>hf' : Integrable (fun x => f ↑x) (Measure.comap Subtype.val μ)<GOAL>∫ (a : α) in s, f a ∂μ = ∑' (a : ↑s), (μ {↑a}).toReal • f ↑a
<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>ν : Measure α<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → E<VAR>s : Set α<VAR>hs : s.Countable<VAR>hf : Integrable f (μ.restrict s)<VAR>hi : Countable { x // x ∈ s }<VAR>hf' : Integrable (fun x => f ↑x) (Measure.comap Subtype.val μ)<GOAL>∑' (a : ↑s), ((Measure.comap Subtype.val μ) {a}).toReal • f ↑a = ∑' (a : ↑s), (μ {↑a}).toReal • f ↑a
<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>ν : Measure α<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → E<VAR>s : Set α<VAR>hs : s.Countable<VAR>hf : Integrable f (μ.restrict s)<VAR>hi : Countable { x // x ∈ s }<VAR>hf' : Integrable (fun x => f ↑x) (Measure.comap Subtype.val μ)<VAR>a : ↑s<GOAL>((Measure.comap Subtype.val μ) {a}).toReal • f ↑a = (μ {↑a}).toReal • f ↑a
<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>ν : Measure α<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → E<VAR>s : Set α<VAR>hs : s.Countable<VAR>hf : Integrable f (μ.restrict s)<VAR>hi : Countable { x // x ∈ s }<VAR>hf' : Integrable (fun x => f ↑x) (Measure.comap Subtype.val μ)<VAR>a : ↑s<GOAL>(μ (Subtype.val '' {a})).toReal • f ↑a = (μ {↑a}).toReal • f ↑a
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : CommRing F<VAR>inst✝⁴ : StrongRankCondition F<VAR>inst✝³ : Ring E<VAR>inst✝² : Algebra F E<VAR>S : Subalgebra F E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : Module.Free F ↥S<GOAL>finrank F ↥S = 1 ↔ S = ⊥
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : CommRing F<VAR>inst✝⁴ : StrongRankCondition F<VAR>inst✝³ : Ring E<VAR>inst✝² : Algebra F E<VAR>S : Subalgebra F E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : Module.Free F ↥S<GOAL>finrank F ↥S = 1 ↔ Module.rank F ↥S = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : DecidableRel H.Adj<VAR>inst✝ : DecidableEq α<VAR>tris : Finset (Finset α)<VAR>htris : tris ⊆ G.cliqueFinset 3<VAR>pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton<VAR>tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑tris.card<GOAL>G.FarFromTriangleFree ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : DecidableRel H.Adj<VAR>inst✝ : DecidableEq α<VAR>tris : Finset (Finset α)<VAR>htris : tris ⊆ G.cliqueFinset 3<VAR>pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton<VAR>tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑tris.card<GOAL>∀ ⦃H : SimpleGraph α⦄ [inst : DecidableRel H.Adj], H ≤ G → H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑G.edgeFinset.card - ↑H.edgeFinset.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>G H✝ : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝⁴ : Fintype α<VAR>inst✝³ : DecidableRel G.Adj<VAR>inst✝² : DecidableRel H✝.Adj<VAR>inst✝¹ : DecidableEq α<VAR>tris : Finset (Finset α)<VAR>htris : tris ⊆ G.cliqueFinset 3<VAR>pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton<VAR>tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑tris.card<VAR>H : SimpleGraph α<VAR>inst✝ : DecidableRel H.Adj<VAR>hG : H ≤ G<VAR>hH : H.CliqueFree 3<GOAL>ε * ↑(Fintype.card α ^ 2) ≤ ↑G.edgeFinset.card - ↑H.edgeFinset.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>G H✝ : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝⁴ : Fintype α<VAR>inst✝³ : DecidableRel G.Adj<VAR>inst✝² : DecidableRel H✝.Adj<VAR>inst✝¹ : DecidableEq α<VAR>tris : Finset (Finset α)<VAR>htris : tris ⊆ G.cliqueFinset 3<VAR>pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton<VAR>tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑tris.card<VAR>H : SimpleGraph α<VAR>inst✝ : DecidableRel H.Adj<VAR>hG : H ≤ G<VAR>hH : H.CliqueFree 3<GOAL>ε * ↑(Fintype.card α ^ 2) ≤ ↑(G.edgeFinset.card - H.edgeFinset.card)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (o.oangle x y).sign = -1<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>o.oangle x y = -↑(InnerProductGeometry.angle x y)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (o.oangle x y).sign = -1<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>¬o.oangle x y = ↑(InnerProductGeometry.angle x y)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (o.oangle x y).sign = -1<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>hxy : o.oangle x y = ↑(InnerProductGeometry.angle x y)<GOAL>False
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : ¬0 ≤ (↑(InnerProductGeometry.angle x y)).sign<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>hxy : o.oangle x y = ↑(InnerProductGeometry.angle x y)<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : TopologicalSpace R<VAR>inst✝¹⁰ : TopologicalSemiring R<VAR>A : Type u_2<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : TopologicalSemiring A<VAR>inst✝⁶ : TopologicalSpace R<VAR>inst✝⁵ : TopologicalSemiring R<VAR>B : Type u_3<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : TopologicalSemiring B<VAR>f : A →A[R] B<VAR>hf' : DenseRange ⇑f<VAR>s : Subalgebra R A<VAR>hs : s.topologicalClosure = ⊤<GOAL>(Subalgebra.map (↑f) s).topologicalClosure = ⊤
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : TopologicalSpace R<VAR>inst✝¹⁰ : TopologicalSemiring R<VAR>A : Type u_2<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : TopologicalSemiring A<VAR>inst✝⁶ : TopologicalSpace R<VAR>inst✝⁵ : TopologicalSemiring R<VAR>B : Type u_3<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : TopologicalSemiring B<VAR>f : A →A[R] B<VAR>hf' : DenseRange ⇑f<VAR>s : Subalgebra R A<VAR>hs : ↑s.topologicalClosure = ↑⊤<GOAL>↑(Subalgebra.map (↑f) s).topologicalClosure = ↑⊤
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : TopologicalSpace R<VAR>inst✝¹⁰ : TopologicalSemiring R<VAR>A : Type u_2<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : TopologicalSemiring A<VAR>inst✝⁶ : TopologicalSpace R<VAR>inst✝⁵ : TopologicalSemiring R<VAR>B : Type u_3<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : TopologicalSemiring B<VAR>f : A →A[R] B<VAR>hf' : DenseRange ⇑f<VAR>s : Subalgebra R A<VAR>hs : Dense ↑s<GOAL>Dense ((fun a => f a) '' ↑s)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z✝ : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>B : C<VAR>X Y Z : Subobject B<VAR>h₁ : X ≤ Y<VAR>h₂ : Y ≤ Z<GOAL>X.ofLE Y h₁ ≫ Y.ofLE Z h₂ = X.ofLE Z ⋯
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z✝ : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>B : C<VAR>X Y Z : Subobject B<VAR>h₁ : X ≤ Y<VAR>h₂ : Y ≤ Z<GOAL>underlying.map (h₁.hom ≫ h₂.hom) = underlying.map ⋯.hom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>f g : α → β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>m : MeasurableSpace α<VAR>μ : ι → Measure α<VAR>h : ∀ (i : ι), AEStronglyMeasurable f (μ i)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>AEStronglyMeasurable f (sum μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>f g : α → β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>m : MeasurableSpace α<VAR>μ : ι → Measure α<VAR>h : ∀ (i : ι), AEStronglyMeasurable f (μ i)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>f g : α → β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>m : MeasurableSpace α<VAR>μ : ι → Measure α<VAR>h : ∀ (i : ι), AEStronglyMeasurable f (μ i)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>A : ∀ (i : ι), ∃ t, IsSeparable t ∧ f ⁻¹' t ∈ ae (μ i)<GOAL>∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>f g : α → β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>m : MeasurableSpace α<VAR>μ : ι → Measure α<VAR>h : ∀ (i : ι), AEStronglyMeasurable f (μ i)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>t : ι → Set β<VAR>t_sep : ∀ (i : ι), IsSeparable (t i)<VAR>ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)<GOAL>∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>f g : α → β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>m : MeasurableSpace α<VAR>μ : ι → Measure α<VAR>h : ∀ (i : ι), AEStronglyMeasurable f (μ i)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>t : ι → Set β<VAR>t_sep : ∀ (i : ι), IsSeparable (t i)<VAR>ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)<GOAL>∀ᵐ (x : α) ∂sum μ, f x ∈ ⋃ i, t i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>f g : α → β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>m : MeasurableSpace α<VAR>μ : ι → Measure α<VAR>h : ∀ (i : ι), AEStronglyMeasurable f (μ i)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>t : ι → Set β<VAR>t_sep : ∀ (i : ι), IsSeparable (t i)<VAR>ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)<GOAL>∀ (b : ι), ∀ᵐ (x : α) ∂μ b, ∃ i, f x ∈ t i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>f g : α → β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>m : MeasurableSpace α<VAR>μ : ι → Measure α<VAR>h : ∀ (i : ι), AEStronglyMeasurable f (μ i)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>t : ι → Set β<VAR>t_sep : ∀ (i : ι), IsSeparable (t i)<VAR>ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)<VAR>i : ι<GOAL>∀ᵐ (x : α) ∂μ i, ∃ i, f x ∈ t i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>f g : α → β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>m : MeasurableSpace α<VAR>μ : ι → Measure α<VAR>h : ∀ (i : ι), AEStronglyMeasurable f (μ i)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>t : ι → Set β<VAR>t_sep : ∀ (i : ι), IsSeparable (t i)<VAR>ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)<VAR>i : ι<VAR>x : α<VAR>hx : x ∈ f ⁻¹' t i<GOAL>∃ i, f x ∈ t i
<VAR>a b c d✝ m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hc : 0 < c<VAR>d : ℕ<GOAL>b * c = a * c * d ↔ b = a * d
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : PolishSpace α<VAR>s : Set α<VAR>hs : IsClosed s<GOAL>AnalyticSet s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : PolishSpace α<VAR>s : Set α<VAR>hs : IsClosed s<VAR>this : PolishSpace ↑s<GOAL>AnalyticSet s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : PolishSpace α<VAR>s : Set α<VAR>hs : IsClosed s<VAR>this : PolishSpace ↑s<GOAL>AnalyticSet (range Subtype.val)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝⁴ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝³ : TopologicalSpace 𝕜<VAR>inst✝² : OrderTopology 𝕜<VAR>p a : 𝕜<VAR>hp : Fact (0 < p)<VAR>inst✝¹ : Archimedean 𝕜<VAR>inst✝ : TopologicalSpace B<VAR>f : 𝕜 → B<VAR>hf : f a = f (a + p)<VAR>hc : ContinuousOn f (Icc a (a + p))<GOAL>Continuous (liftIco p a f)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝⁴ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝³ : TopologicalSpace 𝕜<VAR>inst✝² : OrderTopology 𝕜<VAR>p a : 𝕜<VAR>hp : Fact (0 < p)<VAR>inst✝¹ : Archimedean 𝕜<VAR>inst✝ : TopologicalSpace B<VAR>f : 𝕜 → B<VAR>hf : f a = f (a + p)<VAR>hc : ContinuousOn f (Icc a (a + p))<GOAL>Continuous (Quot.lift ((Icc a (a + p)).restrict f) ⋯ ∘ ⇑(equivIccQuot p a))
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝⁴ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝³ : TopologicalSpace 𝕜<VAR>inst✝² : OrderTopology 𝕜<VAR>p a : 𝕜<VAR>hp : Fact (0 < p)<VAR>inst✝¹ : Archimedean 𝕜<VAR>inst✝ : TopologicalSpace B<VAR>f : 𝕜 → B<VAR>hf : f a = f (a + p)<VAR>hc : ContinuousOn f (Icc a (a + p))<GOAL>Continuous (Quot.lift ((Icc a (a + p)).restrict f) ⋯)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : Algebra R A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Algebra R B<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>r : R<VAR>f g : M →ₗ[R] N<VAR>x✝ : M<GOAL>((AlgebraTensorModule.curry (baseChange A 0)) 1) x✝ = ((AlgebraTensorModule.curry 0) 1) x✝
<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<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(finrank ℝ E) < r<GOAL>∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) ∂μ < ⊤