ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : IsDedekindDomain A<VAR>M : Submonoid A<VAR>hM : M ≤ A⁰<VAR>Aₘ : Type u_4<VAR>inst✝³ : CommRing Aₘ<VAR>inst✝² : IsDomain Aₘ<VAR>inst✝¹ : Algebra A Aₘ<VAR>inst✝ : IsLocalization M Aₘ<VAR>h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)<VAR>this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra<VAR>this✝ : IsScalarTower A Aₘ (FractionRing A)<VAR>this : IsFractionRing Aₘ (FractionRing A)<GOAL>∀ {x : FractionRing A}, IsIntegral Aₘ x → ∃ y, (algebraMap Aₘ (FractionRing A)) y = x
<VAR>M : Type u_1<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : Pow M ℕ<VAR>inst✝ : NatPowAssoc M<VAR>m n : ℕ<VAR>x : M<GOAL>x ^ m * x ^ n = x ^ n * x ^ m
<VAR>α : Type u_1<VAR>f : α → ℝ≥0<VAR>hf : Summable f<GOAL>Tendsto f cofinite (𝓝 0)
<VAR>α : Type u_1<VAR>f : α → ℝ≥0<VAR>hf : Summable fun a => ↑(f a)<GOAL>Tendsto (fun a => ↑(f a)) cofinite (𝓝 ↑0)
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<GOAL>(x + y).denom ∣ x.denom * y.denom
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<GOAL>∃ p, x + y = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)
<VAR>f : StieltjesFunction<VAR>l u : ℝ<VAR>hfl : Tendsto (↑f) atBot (𝓝 l)<VAR>hfu : Tendsto (↑f) atTop (𝓝 u)<GOAL>f.measure univ = ofReal (u - l)
<VAR>f : StieltjesFunction<VAR>l u : ℝ<VAR>hfl : Tendsto (↑f) atBot (𝓝 l)<VAR>hfu : Tendsto (↑f) atTop (𝓝 u)<GOAL>Tendsto (fun x => f.measure (Iic x)) atTop (𝓝 (ofReal (u - l)))
<VAR>f : StieltjesFunction<VAR>l u : ℝ<VAR>hfl : Tendsto (↑f) atBot (𝓝 l)<VAR>hfu : Tendsto (↑f) atTop (𝓝 u)<GOAL>Tendsto (fun x => ofReal (↑f x - l)) atTop (𝓝 (ofReal (u - l)))
<VAR>k✝ G✝ : Type u<VAR>inst✝⁷ : CommRing k✝<VAR>inst✝⁶ : Group G✝<VAR>A✝ : Rep k✝ G✝<VAR>k G A : Type u<VAR>inst✝⁵ : CommRing k<VAR>inst✝⁴ : Group G<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module k A<VAR>inst✝¹ : DistribMulAction G A<VAR>inst✝ : SMulCommClass G k A<VAR>f : ↥(oneCoboundaries (Rep.ofDistribMulAction k G A))<GOAL>IsOneCoboundary ↑↑f
<VAR>k✝ G✝ : Type u<VAR>inst✝⁷ : CommRing k✝<VAR>inst✝⁶ : Group G✝<VAR>A✝ : Rep k✝ G✝<VAR>k G A : Type u<VAR>inst✝⁵ : CommRing k<VAR>inst✝⁴ : Group G<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module k A<VAR>inst✝¹ : DistribMulAction G A<VAR>inst✝ : SMulCommClass G k A<VAR>f : ↥(oneCoboundaries (Rep.ofDistribMulAction k G A))<VAR>x : CoeSort.coe (Rep.ofDistribMulAction k G A)<VAR>hx : (dZero (Rep.ofDistribMulAction k G A)) x = ↑↑f<GOAL>IsOneCoboundary ↑↑f
<VAR>G✝ : Type u_1<VAR>P✝ : Type u_2<VAR>inst✝³ : AddGroup G✝<VAR>inst✝² : AddTorsor G✝ P✝<VAR>G : Type u_3<VAR>P : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : AddTorsor G P<VAR>h : Injective fun x => 2 • x<VAR>y x₁ x₂ : P<VAR>hy : (pointReflection x₁) y = (pointReflection x₂) y<GOAL>x₁ = x₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝ : AddGroup α<VAR>h : Periodic f c<VAR>n : ℕ<GOAL>f (x - n • c) = f x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<GOAL>nthRootsFinset 0 R = ∅
<VAR>α : Type u<VAR>n : ℕ<GOAL>finRange n = [] ↔ n = 0
<VAR>p : Char → Bool<VAR>s : String<GOAL>(s.takeWhile p).data = List.takeWhile p s.data
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x✝ : M<VAR>s✝ t✝ : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x✝ →L[𝕜] TangentSpace I' (f x✝)<VAR>g' : TangentSpace I' (f x✝) →L[𝕜] TangentSpace I'' (g (f x✝))<VAR>x : M<VAR>y : M'<VAR>s : Set M<VAR>t : Set M'<VAR>hs : UniqueMDiffWithinAt I s x<VAR>ht : UniqueMDiffWithinAt I' t y<GOAL>UniqueMDiffWithinAt (I.prod I') (s ×ˢ t) (x, y)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x✝ : M<VAR>s✝ t✝ : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x✝ →L[𝕜] TangentSpace I' (f x✝)<VAR>g' : TangentSpace I' (f x✝) →L[𝕜] TangentSpace I'' (g (f x✝))<VAR>x : M<VAR>y : M'<VAR>s : Set M<VAR>t : Set M'<VAR>hs : UniqueMDiffWithinAt I s x<VAR>ht : UniqueMDiffWithinAt I' t y<GOAL>(↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) ×ˢ (↑(extChartAt I' y).symm ⁻¹' t ∩ range ↑I') ⊆ ↑(extChartAt (I.prod I') (x, y)).symm ⁻¹' s ×ˢ t ∩ range ↑(I.prod I')
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x✝ : M<VAR>s✝ t✝ : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x✝ →L[𝕜] TangentSpace I' (f x✝)<VAR>g' : TangentSpace I' (f x✝) →L[𝕜] TangentSpace I'' (g (f x✝))<VAR>x : M<VAR>y : M'<VAR>s : Set M<VAR>t : Set M'<VAR>hs : UniqueMDiffWithinAt I s x<VAR>ht : UniqueMDiffWithinAt I' t y<GOAL>(↑(extChartAt I x).symm ⁻¹' s) ×ˢ (↑(extChartAt I' y).symm ⁻¹' t) ∩ range ↑I ×ˢ range ↑I' ⊆ ↑(extChartAt (I.prod I') (x, y)).symm ⁻¹' s ×ˢ t ∩ range ↑I ×ˢ range ↑I'
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : Associates α<VAR>a✝ : Nontrivial α<GOAL>(a * b).factors = a.factors + b.factors
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : Associates α<VAR>a✝ : Nontrivial α<GOAL>(a * b).factors.prod.factors = (a.factors + b.factors).prod.factors
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>X : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>hs : IsNowhereDense s<GOAL>IsNowhereDense (closure s)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M : Mon_ C<VAR>Z : C<VAR>f : Z ⟶ M.X<GOAL>(f ⊗ M.one) ≫ M.mul = (ρ_ Z).hom ≫ f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : R[X]<VAR>x : S<VAR>h : IsUnit ((aeval x) (derivative P))<GOAL>P.newtonMap x = x - ↑h.unit⁻¹ * (aeval x) P
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝³ : Preorder β<VAR>f✝ g✝ : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : LinearOrderedAddCommMonoid γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderTopology γ<VAR>f g : α → γ<VAR>hf : UpperSemicontinuousAt f x<VAR>hg : UpperSemicontinuousAt g x<VAR>hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)<GOAL>UpperSemicontinuousAt (fun z => f z + g z) x
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝³ : Preorder β<VAR>f✝ g✝ : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : LinearOrderedAddCommMonoid γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderTopology γ<VAR>f g : α → γ<VAR>hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)<VAR>hf : UpperSemicontinuousWithinAt f univ x<VAR>hg : UpperSemicontinuousWithinAt g univ x<GOAL>UpperSemicontinuousWithinAt (fun z => f z + g z) univ x
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : MeasurableSpace H<VAR>inst✝¹ : Mul G<VAR>μ✝ : Measure G<VAR>inst✝ : MeasurableMul G<VAR>μ : Measure G<GOAL>(∀ (g : G), Measure.map (fun x => x * g) μ = μ) ↔ μ.IsMulRightInvariant
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} J<VAR>inst✝ : Category.{u_4, u_2} C<VAR>P Q : Karoubi (J ⥤ C)<VAR>f : P ⟶ Q<VAR>X : J<GOAL>toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C = (whiskeringRight J C (Karoubi C)).obj (toKaroubi C)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} J<VAR>inst✝ : Category.{u_4, u_2} C<VAR>P Q : Karoubi (J ⥤ C)<VAR>f : P ⟶ Q<VAR>X : J<GOAL>autoParam (∀ (X Y : J ⥤ C) (f : X ⟶ Y), (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).map f = eqToHom ⋯ ≫ ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).map f ≫ eqToHom ⋯) _auto✝
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} J<VAR>inst✝ : Category.{u_4, u_2} C<VAR>P Q : Karoubi (J ⥤ C)<VAR>f : P ⟶ Q<VAR>X : J<GOAL>∀ (X : J ⥤ C), (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X = ((whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : SeminormedAddGroup α<VAR>inst✝² : SeminormedAddGroup β<VAR>inst✝¹ : SMulZeroClass α β<VAR>inst✝ : BoundedSMul α β<VAR>s : α<VAR>x y : β<GOAL>dist (s • x) (s • y) ≤ ‖s‖ * dist x y
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<GOAL>(∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0) ↔ T1Space E
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<GOAL>T1Space E → ∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>a✝ : T1Space E<GOAL>∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0
<VAR>p : ℚ → Prop<VAR>x✝ : ∃ r, p r<VAR>r : ℚ<VAR>hr : p r<GOAL>↑r.num / ↑↑r.den = r
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>⌊0⌋ = 0
<VAR>α : Sort u_1<GOAL>⨆ x, 0 = 0
<VAR>α : Sort u_1<VAR>h✝ : IsEmpty α<GOAL>⨆ x, 0 = 0
<VAR>α : Sort u_1<VAR>h✝ : Nonempty α<GOAL>⨆ x, 0 = 0
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f✝ f' : α → β → γ<VAR>g✝ g'✝ : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a✝ a' : α<VAR>b✝ b' : β<VAR>c✝ c' : γ<VAR>d d' : δ<VAR>f : δ → γ → ε<VAR>g : α → β → δ<VAR>f₁ : α → γ → α'<VAR>f₂ : β → γ → β'<VAR>g' : α' → β' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)<VAR>a : α<VAR>ha : a ∈ s<VAR>b : β<VAR>hb : b ∈ t<VAR>c : γ<VAR>hc : c ∈ u<GOAL>g' (f₁ a c) (f₂ b c) ∈ image2 g' (image2 f₁ s u) (image2 f₂ t u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>s : Set β<VAR>hs : s.Countable<VAR>f : α → β<VAR>hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})<GOAL>∑' (b : ↑s), μ (f ⁻¹' {↑b}) = μ (f ⁻¹' s)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hb : 0 < b<GOAL>a < a / b * b + b
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hb : 0 < b<GOAL>a / b < (a / b).succ
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>y : Y<VAR>f : X → Z<GOAL>(Inducing fun x => (f x, y)) ↔ Inducing f
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>inst✝ : CardinalInterFilter l c<VAR>S : Set ι<VAR>hS : #↑S < c<VAR>s : (i : ι) → i ∈ S → Set α<GOAL>⋂ i, ⋂ (hi : i ∈ S), s i hi ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>inst✝ : CardinalInterFilter l c<VAR>S : Set ι<VAR>hS : #↑S < c<VAR>s : (i : ι) → i ∈ S → Set α<GOAL>⋂ x, s ↑x ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>ι : Sort u_1<VAR>S : ι → NonUnitalStarSubalgebra R A<VAR>x : A<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>𝕜 : Type u_1<VAR>inst✝²⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁹ : NormedAddCommGroup E<VAR>inst✝¹⁸ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁷ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁶ : TopologicalSpace M<VAR>inst✝¹⁵ : ChartedSpace H M<VAR>inst✝¹⁴ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹³ : NormedAddCommGroup E'<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹¹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹⁰ : TopologicalSpace M'<VAR>inst✝⁹ : ChartedSpace H' M'<VAR>inst✝⁸ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>inst✝² : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x z : M<VAR>F' : Type u_11<VAR>inst✝¹ : NormedRing F'<VAR>inst✝ : NormedAlgebra 𝕜 F'<VAR>p q : M → F'<VAR>p' q' : TangentSpace I z →L[𝕜] F'<VAR>hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'<VAR>hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q'<GOAL>HasFDerivWithinAt (writtenInExtChartAt I 𝓘(𝕜, F') z (p * q)) (p z • q' + p'.smulRight (q z)) (↑(extChartAt I z).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I z) z)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>inst✝ : R.hasPullbacks<GOAL>Presieve.IsSheafFor P R ↔ Nonempty (IsLimit (Fork.ofι (forkMap P R) ⋯))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>inst✝ : R.hasPullbacks<GOAL>Presieve.IsSheafFor P R ↔ ∀ (y : FirstObj P R), firstMap P R y = secondMap P R y → ∃! x, forkMap P R x = y
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>inst✝ : R.hasPullbacks<GOAL>Presieve.IsSheafFor P R ↔ ∀ (a : Presieve.FamilyOfElements P R), firstMap P R ((firstObjEqFamily P R).toEquiv.symm a) = secondMap P R ((firstObjEqFamily P R).toEquiv.symm a) → ∃! x, forkMap P R x = (firstObjEqFamily P R).toEquiv.symm a
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>inst✝ : R.hasPullbacks<GOAL>Presieve.IsSheafFor P R ↔ ∀ (a : Presieve.FamilyOfElements P R), a.Compatible → ∃! x, forkMap P R x = (firstObjEqFamily P R).toEquiv.symm a
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>inst✝ : R.hasPullbacks<GOAL>∀ (a : Presieve.FamilyOfElements P R), a.Compatible → ((∃! t, a.IsAmalgamation t) ↔ ∃! x, forkMap P R x = (firstObjEqFamily P R).toEquiv.symm a)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>inst✝ : R.hasPullbacks<VAR>x : Presieve.FamilyOfElements P R<VAR>b✝ : x.Compatible<GOAL>(∃! t, x.IsAmalgamation t) ↔ ∃! x_1, forkMap P R x_1 = (firstObjEqFamily P R).toEquiv.symm x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>inst✝ : R.hasPullbacks<VAR>x : Presieve.FamilyOfElements P R<VAR>b✝ : x.Compatible<GOAL>∀ (a : P.obj (op X)), x.IsAmalgamation a ↔ forkMap P R a = (firstObjEqFamily P R).toEquiv.symm x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>inst✝ : R.hasPullbacks<VAR>x : Presieve.FamilyOfElements P R<VAR>b✝ : x.Compatible<VAR>t : P.obj (op X)<GOAL>x.IsAmalgamation t ↔ forkMap P R t = (firstObjEqFamily P R).toEquiv.symm x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>inst✝ : R.hasPullbacks<VAR>x : Presieve.FamilyOfElements P R<VAR>b✝ : x.Compatible<VAR>t : P.obj (op X)<GOAL>x.IsAmalgamation t ↔ (firstObjEqFamily P R).toEquiv (forkMap P R t) = x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_4, u_1} C<VAR>inst✝⁷ : Category.{u_3, u_2} D<VAR>inst✝⁶ : Preadditive C<VAR>inst✝⁵ : HasZeroObject C<VAR>inst✝⁴ : HasBinaryBiproducts C<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>G : C ⥤ D<VAR>inst✝ : G.Additive<VAR>n : ℤ<GOAL>G.map ((triangle φ).mor₃.f n) ≫ 𝟙 (G.obj (K.X (n + 1))) = (mapHomologicalComplexXIso φ G n).hom ≫ (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃.f n
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_4, u_1} C<VAR>inst✝⁷ : Category.{u_3, u_2} D<VAR>inst✝⁶ : Preadditive C<VAR>inst✝⁵ : HasZeroObject C<VAR>inst✝⁴ : HasBinaryBiproducts C<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>G : C ⥤ D<VAR>inst✝ : G.Additive<VAR>n : ℤ<GOAL>G.map ((triangle φ).mor₃.f n) ≫ 𝟙 (G.obj (K.X (n + 1))) = (G.map ((↑(fst φ)).v n (n + 1) ⋯) ≫ (inl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) n ⋯ + G.map ((snd φ).v n n ⋯) ≫ (inr ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n) ≫ (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃.f n
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_4, u_1} C<VAR>inst✝⁷ : Category.{u_3, u_2} D<VAR>inst✝⁶ : Preadditive C<VAR>inst✝⁵ : HasZeroObject C<VAR>inst✝⁴ : HasBinaryBiproducts C<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>G : C ⥤ D<VAR>inst✝ : G.Additive<VAR>n : ℤ<GOAL>G.map ((triangle φ).mor₃.f n) = -G.map ((↑(fst φ)).v n (n + 1) ⋯)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_4, u_1} C<VAR>inst✝⁷ : Category.{u_3, u_2} D<VAR>inst✝⁶ : Preadditive C<VAR>inst✝⁵ : HasZeroObject C<VAR>inst✝⁴ : HasBinaryBiproducts C<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>G : C ⥤ D<VAR>inst✝ : G.Additive<VAR>n : ℤ<GOAL>G.map (((-↑(fst φ)).rightShift 1 0 triangle.proof_2).v n n ⋯) = -G.map ((↑(fst φ)).v n (n + 1) ⋯)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_4, u_1} C<VAR>inst✝⁷ : Category.{u_3, u_2} D<VAR>inst✝⁶ : Preadditive C<VAR>inst✝⁵ : HasZeroObject C<VAR>inst✝⁴ : HasBinaryBiproducts C<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>G : C ⥤ D<VAR>inst✝ : G.Additive<VAR>n : ℤ<GOAL>G.map ((-↑(fst φ)).v n (n + 1) ⋯ ≫ (K.shiftFunctorObjXIso 1 n (n + 1) ⋯).inv) = -G.map ((↑(fst φ)).v n (n + 1) ⋯)
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>f : PartialHomeomorph H H<VAR>hf : f ∈ G<GOAL>f.symm ≫ₕ PartialHomeomorph.refl H ∈ G ∧ (PartialHomeomorph.refl H).symm ≫ₕ f ∈ G
<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>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>h : a ∈ s<GOAL>(∏ x ∈ s.erase a, f x) * f a = ∏ x ∈ s, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>a : α<VAR>b : β<GOAL>a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>a : α<VAR>b : β<GOAL>(0 < -a → 0 ≤ b) ∧ (0 < b → 0 ≤ -a) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
<VAR>α : Type u_1<VAR>m n : PosNum<VAR>h : ↑m < ↑n<GOAL>↑m + ↑m + 1 + 1 ≤ ↑n + ↑n
<VAR>α : Type u_1<VAR>m n : PosNum<VAR>h : ↑m < ↑n<GOAL>↑m + 1 + (↑m + 1) ≤ ↑n + ↑n
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>a b : α<VAR>u : αˣ<GOAL>a ∣ b * ↑u ↔ a ∣ b
<VAR>G : Type u_1<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : SFinite μ<VAR>s : Set G<VAR>inst✝ : μ.IsMulRightInvariant<GOAL>MeasurePreserving ?m.119417 ?m.119413 (?m.119343.prod ?m.119344)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f✝ g : R → R<VAR>a✝ : A<VAR>ha : autoParam (p a✝) _auto✝<VAR>hf✝ : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a✝)) _auto✝<VAR>f : R → R<VAR>a : A<VAR>hf : ¬ContinuousOn f (spectrum R a)<GOAL>cfc f a = 0