ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β✝ : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x✝ y z : α<VAR>δ ε✝ ε₁ ε₂ : ℝ<VAR>s✝ s : Set α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε<VAR>x0 : α<VAR>hx0 : x0 ∈ s<VAR>this✝ : Inhabited ↑s<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>β : Type u<VAR>fβ : Fintype β<VAR>F : ↑s → β<VAR>hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε<VAR>Finv : β → ↑s := Function.invFun F<VAR>x : α<VAR>xs : x ∈ s<VAR>x' : ↑s := Finv (F ⟨x, xs⟩)<VAR>this : F x' = F ⟨x, xs⟩<GOAL>x ∈ ⋃ y ∈ range (Subtype.val ∘ Finv), ball y ε
<VAR>α : Type u<VAR>β✝ : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x✝ y z : α<VAR>δ ε✝ ε₁ ε₂ : ℝ<VAR>s✝ s : Set α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε<VAR>x0 : α<VAR>hx0 : x0 ∈ s<VAR>this✝ : Inhabited ↑s<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>β : Type u<VAR>fβ : Fintype β<VAR>F : ↑s → β<VAR>hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε<VAR>Finv : β → ↑s := Function.invFun F<VAR>x : α<VAR>xs : x ∈ s<VAR>x' : ↑s := Finv (F ⟨x, xs⟩)<VAR>this : F x' = F ⟨x, xs⟩<GOAL>∃ i, ∃ (_ : ∃ y, (Subtype.val ∘ Finv) y = i), x ∈ ball i ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : SMulCommClass ℝ 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace E<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>L1.integralCLM ↑f = MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : OrderTop α<VAR>inst✝² : OrderBot β<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : LocallyFiniteOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Ico (inrₗ b₁) (inrₗ b₂) = map (Embedding.inr.trans toLex.toEmbedding) (Ico b₁ b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : OrderTop α<VAR>inst✝² : OrderBot β<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : LocallyFiniteOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Ico (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ico b₁ b₂))
<VAR>α : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero α<VAR>inst✝⁴ : UniqueFactorizationMonoid α<VAR>inst✝³ : DecidableEq (Associates α)<VAR>inst✝² : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>a p : Associates α<VAR>hp : Irreducible p<VAR>inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)<VAR>n : ℕ<VAR>h : a ∣ p ^ n<GOAL>Nat.find ⋯ = p.count a.factors
<VAR>α : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero α<VAR>inst✝⁴ : UniqueFactorizationMonoid α<VAR>inst✝³ : DecidableEq (Associates α)<VAR>inst✝² : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>a p : Associates α<VAR>hp : Irreducible p<VAR>inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)<VAR>n : ℕ<VAR>h : a ∣ p ^ n<GOAL>Nat.find ⋯ ≤ p.count a.factors
<VAR>α : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero α<VAR>inst✝⁴ : UniqueFactorizationMonoid α<VAR>inst✝³ : DecidableEq (Associates α)<VAR>inst✝² : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>a p : Associates α<VAR>hp : Irreducible p<VAR>inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)<VAR>n : ℕ<VAR>h : a ∣ p ^ n<GOAL>p.count a.factors ≤ Nat.find ⋯
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁴ : RCLike 𝕂<VAR>E' : Type u_2<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕂 E'<VAR>F' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace 𝕂 F'<VAR>f : E' → F'<VAR>f' : E' →L[𝕂] F'<VAR>x : E'<VAR>hf : ContDiffAt 𝕂 n f x<VAR>hf' : HasFDerivAt f f' x<VAR>hn : 1 ≤ n<VAR>u : Set E'<VAR>H : u ∈ 𝓝[insert x univ] x<VAR>p : E' → FormalMultilinearSeries 𝕂 E' F'<VAR>hp : HasFTaylorSeriesUpToOn (↑1) f p u<GOAL>HasStrictFDerivAt f f' x
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁴ : RCLike 𝕂<VAR>E' : Type u_2<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕂 E'<VAR>F' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace 𝕂 F'<VAR>f : E' → F'<VAR>f' : E' →L[𝕂] F'<VAR>x : E'<VAR>hf : ContDiffAt 𝕂 n f x<VAR>hf' : HasFDerivAt f f' x<VAR>hn : 1 ≤ n<VAR>u : Set E'<VAR>p : E' → FormalMultilinearSeries 𝕂 E' F'<VAR>hp : HasFTaylorSeriesUpToOn (↑1) f p u<VAR>H : u ∈ 𝓝 x<GOAL>HasStrictFDerivAt f f' x
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁴ : RCLike 𝕂<VAR>E' : Type u_2<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕂 E'<VAR>F' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace 𝕂 F'<VAR>f : E' → F'<VAR>f' : E' →L[𝕂] F'<VAR>x : E'<VAR>hf : ContDiffAt 𝕂 n f x<VAR>hf' : HasFDerivAt f f' x<VAR>hn : 1 ≤ n<VAR>u : Set E'<VAR>p : E' → FormalMultilinearSeries 𝕂 E' F'<VAR>hp : HasFTaylorSeriesUpToOn (↑1) f p u<VAR>H : u ∈ 𝓝 x<VAR>this : HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕂 E' F') (p x 1)) x<GOAL>HasStrictFDerivAt f f' x
<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' : Type u_3<VAR>inst✝¹ : Field E'<VAR>inst✝ : Algebra F E'<VAR>f : E →ₐ[F] E'<VAR>x : E'<GOAL>x ∈ Subfield.map (↑f) (Subfield.closure (Set.range ⇑(algebraMap F E) ∪ S)) ↔ x ∈ Subfield.closure (Set.range ⇑(algebraMap F E') ∪ ⇑f '' S)
<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' : Type u_3<VAR>inst✝¹ : Field E'<VAR>inst✝ : Algebra F E'<VAR>f : E →ₐ[F] E'<VAR>x : E'<GOAL>x ∈ Subfield.closure (Set.range ⇑(algebraMap F E') ∪ ⇑↑f '' S) ↔ x ∈ Subfield.closure (Set.range ⇑(algebraMap F E') ∪ ⇑f '' S)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f✝ f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG✝ hG : G.LocalInvariantProp G' P<VAR>U V : Opens M<VAR>hUV : U ≤ V<VAR>f : ↥V → M'<VAR>x : ↥U<GOAL>LiftPropAt P f (inclusion hUV x) ↔ LiftPropAt P (f ∘ inclusion hUV) x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f✝ f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG✝ hG : G.LocalInvariantProp G' P<VAR>U V : Opens M<VAR>hUV : U ≤ V<VAR>f : ↥V → M'<VAR>x : ↥U<GOAL>ContinuousWithinAt f univ (inclusion hUV x) ∧ P (↑(chartAt H' (f (inclusion hUV x))) ∘ f ∘ ↑(chartAt H (inclusion hUV x)).symm) (↑(chartAt H (inclusion hUV x)).symm ⁻¹' univ) (↑(chartAt H (inclusion hUV x)) (inclusion hUV x)) ↔ ContinuousWithinAt (f ∘ inclusion hUV) univ x ∧ P (↑(chartAt H' ((f ∘ inclusion hUV) x)) ∘ (f ∘ inclusion hUV) ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' univ) (↑(chartAt H x) x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : ↥(Lp E 2 μ)<GOAL>eLpNorm (fun x => ⟪↑↑f x, ↑↑g x⟫_𝕜) 1 μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : ↥(Lp E 2 μ)<VAR>h : ∀ (x : α), ‖⟪↑↑f x, ↑↑g x⟫_𝕜‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖<GOAL>eLpNorm (fun x => ⟪↑↑f x, ↑↑g x⟫_𝕜) 1 μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : ↥(Lp E 2 μ)<VAR>h : ∀ (x : α), ‖⟪↑↑f x, ↑↑g x⟫_𝕜‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖<GOAL>AEStronglyMeasurable (fun a => ‖↑↑f a‖ ^ 2) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : ↥(Lp E 2 μ)<VAR>h : ∀ (x : α), ‖⟪↑↑f x, ↑↑g x⟫_𝕜‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖<GOAL>AEStronglyMeasurable (fun a => ‖↑↑g a‖ ^ 2) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : ↥(Lp E 2 μ)<VAR>h : ∀ (x : α), ‖⟪↑↑f x, ↑↑g x⟫_𝕜‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖<GOAL>eLpNorm (fun a => ‖↑↑f a‖ ^ 2) 1 μ + eLpNorm (fun a => ‖↑↑g a‖ ^ 2) 1 μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : ↥(Lp E 2 μ)<VAR>h : ∀ (x : α), ‖⟪↑↑f x, ↑↑g x⟫_𝕜‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖<GOAL>eLpNorm (fun a => ‖↑↑f a‖ ^ 2) 1 μ < ⊤ ∧ eLpNorm (fun a => ‖↑↑g a‖ ^ 2) 1 μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hx : x ∈ box n d<GOAL>∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hx : ∀ (i : Fin n), x i < d<GOAL>∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hx : ∀ (i : Fin n), x i < d<VAR>this : ∀ (i : Fin n), x i ^ 2 ≤ (d - 1) ^ 2<GOAL>∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>ι' : Sort u_3<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<GOAL>Iic a ∩ Iic b ∈ Iic '' s
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>st : s ⊆ t<VAR>f' : E →L[𝕜] F<VAR>hf' : HasFDerivWithinAt f f' t x<GOAL>DifferentiableWithinAt 𝕜 f s x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R T<VAR>inst✝² : Algebra S T<VAR>inst✝¹ : IsScalarTower R S T<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M S<GOAL>EssFiniteType R S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R T<VAR>inst✝² : Algebra S T<VAR>inst✝¹ : IsScalarTower R S T<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M S<GOAL>∃ σ, ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R T<VAR>inst✝² : Algebra S T<VAR>inst✝¹ : IsScalarTower R S T<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M S<GOAL>∀ (s : S), ∃ t ∈ adjoin R ↑∅, IsUnit t ∧ s * t ∈ adjoin R ↑∅
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R T<VAR>inst✝² : Algebra S T<VAR>inst✝¹ : IsScalarTower R S T<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M S<GOAL>∀ (s : S), ∃ a, IsUnit ((algebraMap R S) a) ∧ ∃ y, (algebraMap R S) y = s * (algebraMap R S) a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R T<VAR>inst✝² : Algebra S T<VAR>inst✝¹ : IsScalarTower R S T<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M S<VAR>s : S<GOAL>∃ a, IsUnit ((algebraMap R S) a) ∧ ∃ y, (algebraMap R S) y = s * (algebraMap R S) a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R T<VAR>inst✝² : Algebra S T<VAR>inst✝¹ : IsScalarTower R S T<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M S<VAR>s : S<VAR>x : R<VAR>t : ↥M<VAR>e : s * (algebraMap R S) ↑(x, t).2 = (algebraMap R S) (x, t).1<GOAL>∃ a, IsUnit ((algebraMap R S) a) ∧ ∃ y, (algebraMap R S) y = s * (algebraMap R S) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>g : α → α<VAR>hco : Function.Commute f g<VAR>hfg : IsPeriodicPt (f ∘ g) n x<VAR>hg : IsPeriodicPt g n x<GOAL>IsPeriodicPt f n x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>g : α → α<VAR>hco : Function.Commute f g<VAR>hfg : IsFixedPt (f^[n] ∘ g^[n]) x<VAR>hg : IsPeriodicPt g n x<GOAL>IsPeriodicPt f n x
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝¹ : Type u_3<VAR>β✝ : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α✝¹<VAR>a : α✝¹<VAR>f✝ g : α✝¹ → β✝<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α✝ : Type u_8<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype κ<VAR>inst✝³ : CommMonoid α✝<VAR>α : Type u_9<VAR>β : Type u_10<VAR>inst✝² : CommMonoid β<VAR>inst✝¹ : Unique α<VAR>inst✝ : Fintype α<VAR>f : α → β<GOAL>∏ x : α, f x = f default
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<GOAL>Filter.map rexp atTop = atTop
<VAR>R : Type u_1<VAR>S : Type ?u.268667<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : LocalRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>P : Type u_4<VAR>inst✝⁴ : AddCommGroup P<VAR>inst✝³ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f ⇑g<VAR>inst✝² : Finite R M<VAR>inst✝¹ : Finite R N<VAR>inst✝ : Free R N<VAR>hf : Function.Injective ⇑(LinearMap.lTensor k f)<GOAL>Free R P
<VAR>R : Type u_1<VAR>S : Type ?u.268667<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : LocalRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>P : Type u_4<VAR>inst✝⁴ : AddCommGroup P<VAR>inst✝³ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f ⇑g<VAR>inst✝² : Finite R M<VAR>inst✝¹ : Finite R N<VAR>inst✝ : Free R N<VAR>hf : Function.Injective ⇑(LinearMap.lTensor k f)<VAR>this : FinitePresentation R P<GOAL>Free R P
<VAR>R : Type u_1<VAR>S : Type ?u.268667<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : LocalRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>P : Type u_4<VAR>inst✝⁴ : AddCommGroup P<VAR>inst✝³ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f ⇑g<VAR>inst✝² : Finite R M<VAR>inst✝¹ : Finite R N<VAR>inst✝ : Free R N<VAR>hf : Function.Injective ⇑(LinearMap.lTensor k f)<VAR>this : FinitePresentation R P<GOAL>Function.Injective ⇑(LinearMap.rTensor P (Submodule.subtype 𝔪))
<VAR>R : Type u_1<VAR>S : Type ?u.268667<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : LocalRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>P : Type u_4<VAR>inst✝⁴ : AddCommGroup P<VAR>inst✝³ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f ⇑g<VAR>inst✝² : Finite R M<VAR>inst✝¹ : Finite R N<VAR>inst✝ : Free R N<VAR>hf : Function.Injective ⇑(LinearMap.lTensor k f)<VAR>this : FinitePresentation R P<GOAL>Function.Injective ⇑(LinearMap.lTensor P (Submodule.subtype 𝔪))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁰ : Category.{u_3, u_1} C<VAR>inst✝⁹ : Category.{u_4, u_2} D<VAR>inst✝⁸ : HasZeroMorphisms C<VAR>inst✝⁷ : HasZeroMorphisms D<VAR>F G : C ⥤ D<VAR>τ : F ⟶ G<VAR>S : ShortComplex C<VAR>inst✝⁶ : S.HasHomology<VAR>inst✝⁵ : F.PreservesZeroMorphisms<VAR>inst✝⁴ : G.PreservesZeroMorphisms<VAR>inst✝³ : F.PreservesLeftHomologyOf S<VAR>inst✝² : G.PreservesLeftHomologyOf S<VAR>inst✝¹ : F.PreservesRightHomologyOf S<VAR>inst✝ : G.PreservesRightHomologyOf S<GOAL>τ.app S.homology = (S.mapHomologyIso F).inv ≫ ShortComplex.homologyMap (S.mapNatTrans τ) ≫ (S.mapHomologyIso G).hom
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<GOAL>G.degree s = (filter (G.Adj s) univ).card
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>a✝ : V<GOAL>a✝ ∈ filter (fun x => ¬G.Adj s x) univ ↔ a✝ ∈ h.finpartition.part s
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>a✝ : V<GOAL>a✝ ∈ univ ∧ ¬G.Adj s a✝ ↔ a✝ ∈ h.finpartition.part s
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>a✝ : V<GOAL>a✝ ∈ univ ∧ ¬G.Adj s a✝ ↔ Setoid.r s a✝
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>k : ℕ<VAR>μ : K<VAR>hx : f.HasEigenvalue μ<VAR>hk : 0 < k<GOAL>0 = finrank K ↥⊥
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : LinearOrderedRing α<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module α β<VAR>inst✝¹ : OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>inst✝ : Fintype ι<VAR>hfg : Antivary f g<GOAL>∑ i : ι, f i • g i < ∑ i : ι, f (σ i) • g i ↔ ¬Antivary (f ∘ ⇑σ) g
<VAR>α : Type u_1<VAR>inst✝³ : Semifield α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : PosMulReflectLT α<VAR>inst✝ : ZeroLEOneClass α<VAR>a b : α<GOAL>a⁻¹ < 0 ↔ a < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : Countable ι<VAR>U : ι → Set α<VAR>hU : ⋃ i, U i = univ<VAR>hμ : μ ≠ 0<GOAL>∃ i, 0 < μ (U i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : Countable ι<VAR>U : ι → Set α<VAR>hU : ⋃ i, U i = univ<VAR>H : ∀ (i : ι), μ (U i) ≤ 0<GOAL>μ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : Countable ι<VAR>U : ι → Set α<VAR>hU : ⋃ i, U i = univ<VAR>H : ∀ (i : ι), μ (U i) ≤ 0<GOAL>μ (⋃ i, U i) = 0
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>P₃ : Type u_4<VAR>P₄ : Type u_5<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>V₃ : Type u_8<VAR>V₄ : Type u_9<VAR>inst✝²⁰ : Ring k<VAR>inst✝¹⁹ : AddCommGroup V₁<VAR>inst✝¹⁸ : Module k V₁<VAR>inst✝¹⁷ : AddTorsor V₁ P₁<VAR>inst✝¹⁶ : AddCommGroup V₂<VAR>inst✝¹⁵ : Module k V₂<VAR>inst✝¹⁴ : AddTorsor V₂ P₂<VAR>inst✝¹³ : AddCommGroup V₃<VAR>inst✝¹² : Module k V₃<VAR>inst✝¹¹ : AddTorsor V₃ P₃<VAR>inst✝¹⁰ : AddCommGroup V₄<VAR>inst✝⁹ : Module k V₄<VAR>inst✝⁸ : AddTorsor V₄ P₄<VAR>inst✝⁷ : TopologicalSpace P₁<VAR>inst✝⁶ : AddCommMonoid P₁<VAR>inst✝⁵ : Module k P₁<VAR>inst✝⁴ : TopologicalSpace P₂<VAR>inst✝³ : AddCommMonoid P₂<VAR>inst✝² : Module k P₂<VAR>inst✝¹ : TopologicalSpace P₃<VAR>inst✝ : TopologicalSpace P₄<VAR>e : P₁ ≃ᵃL[k] P₂<VAR>s : Set P₂<GOAL>⇑e.symm '' s = ⇑e ⁻¹' s
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt g (g' x) x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝[≠] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[≠] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[≠] a) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[≠] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : (∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt f (f' x) x) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt f (f' x) x<VAR>hgg' : (∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt g (g' x) x) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt g (g' x) x<VAR>hg' : (∀ᶠ (x : ℝ) in 𝓝[<] a, g' x ≠ 0) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝[<] a) (𝓝 0) ∧ Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[<] a) (𝓝 0) ∧ Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] a) l ∧ Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] a) l ∧ Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>ha : 0 ≤ a<GOAL>⌈a + 1⌉₊ = ⌈a⌉₊ + 1
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → ProbabilityMeasure Ω<VAR>μ : ProbabilityMeasure Ω<GOAL>Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ))
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → ProbabilityMeasure Ω<VAR>μ : ProbabilityMeasure Ω<GOAL>Tendsto (toFiniteMeasure ∘ μs) F (𝓝 μ.toFiniteMeasure) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ))
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>y \ x ⊔ x = y \ x ⊔ (x ⊔ x ⊓ y)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>y ⊓ x ⊔ y \ x ⊔ x = y ⊔ x
<VAR>x✝ y✝ x y : ℝ<VAR>hx : x ∈ Ioc (-(π / 2)) (π / 2)<GOAL>x ≤ arcsin y ↔ sin x ≤ y
<VAR>a✝ x✝ y✝ a x y : ℂ<GOAL>angle x (y / a) = angle (x * a) y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>s s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a✝ a : α<GOAL>s.sup f ≤ a ↔ ∀ b ∈ s, f b ≤ a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>s s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a✝ a : α<GOAL>(∀ b ∈ Multiset.map f s.val, b ≤ a) ↔ ∀ b ∈ s, f b ≤ a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>s s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a✝ a : α<GOAL>(∀ (b : α), ∀ x ∈ s.val, f x = b → b ≤ a) ↔ ∀ b ∈ s, f b ≤ a
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>h₂ : IsZero T.obj₂<VAR>h₃ : IsZero T.obj₃<GOAL>IsZero T.obj₁