ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P : Cᵒᵖ ⥤ D<VAR>hP : Presheaf.IsSheaf J P<VAR>this : IsIso (J.toPlus P)<GOAL>IsIso (J.toPlus P ≫ J.plusMap (J.toPlus P))
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>P : R[X]<VAR>hunit : IsUnit (P.coeff 0)<VAR>hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)<GOAL>IsUnit P
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>hind : ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P<VAR>P : R[X]<VAR>hunit : IsUnit (P.coeff 0)<VAR>hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)<VAR>h : P.natDegree = k<GOAL>IsUnit P
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>hind : ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P<VAR>P : R[X]<VAR>hunit : IsUnit (P.coeff 0)<VAR>hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)<VAR>h : P.natDegree = k<VAR>hdeg : P.natDegree = 0<GOAL>IsUnit P
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>hind : ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P<VAR>P : R[X]<VAR>hunit : IsUnit (P.coeff 0)<VAR>hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)<VAR>h : P.natDegree = k<VAR>hdeg : ¬P.natDegree = 0<GOAL>IsUnit P
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>hind : ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P<VAR>P : R[X]<VAR>hunit : IsUnit (P.coeff 0)<VAR>hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)<VAR>h : P.natDegree = k<VAR>hdeg : ¬P.natDegree = 0<VAR>P₁ : R[X] := P.eraseLead<VAR>hP₁ : P₁ = P.eraseLead<GOAL>IsUnit P
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>hind : ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P<VAR>P : R[X]<VAR>hunit : IsUnit (P.coeff 0)<VAR>hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)<VAR>h : P.natDegree = k<VAR>hdeg : ¬P.natDegree = 0<VAR>P₁ : R[X] := P.eraseLead<VAR>hP₁ : P₁ = P.eraseLead<GOAL>IsUnit P₁
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>hind : ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P<VAR>P : R[X]<VAR>hunit : IsUnit (P.coeff 0)<VAR>hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)<VAR>h : P.natDegree = k<VAR>hdeg : ¬P.natDegree = 0<VAR>P₁ : R[X] := P.eraseLead<VAR>hP₁ : P₁ = P.eraseLead<VAR>hdeg₂ : P.eraseLead.natDegree < P.natDegree<GOAL>IsUnit P₁
<VAR>a b : ℝ<VAR>n : ℕ<VAR>h : 0 ∉ [[a, b]]<GOAL>∫ (x : ℝ) in a..b, x⁻¹ = Real.log (b / a)
<VAR>a b : ℝ<VAR>n : ℕ<VAR>h : 0 ∉ [[a, b]]<VAR>h' : ∀ x ∈ [[a, b]], x ≠ 0<GOAL>∫ (x : ℝ) in a..b, x⁻¹ = Real.log (b / a)
<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>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>f : X' ⟶ Y'<VAR>g₁ g₂ : Y' ⟶ Z'<GOAL>f ≫ add W eY eZ g₁ g₂ = add W eX eZ (f ≫ g₁) (f ≫ g₂)
<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>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>g₁ g₂ : Y' ⟶ Z'<VAR>f : L.obj X ⟶ L.obj Y<GOAL>(homEquiv eX eY).symm f ≫ add W eY eZ g₁ g₂ = add W eX eZ ((homEquiv eX eY).symm f ≫ g₁) ((homEquiv eX eY).symm f ≫ g₂)
<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>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>g₂ : Y' ⟶ Z'<VAR>f : L.obj X ⟶ L.obj Y<VAR>g₁ : L.obj Y ⟶ L.obj Z<GOAL>(homEquiv eX eY).symm f ≫ add W eY eZ ((homEquiv eY eZ).symm g₁) g₂ = add W eX eZ ((homEquiv eX eY).symm f ≫ (homEquiv eY eZ).symm g₁) ((homEquiv eX eY).symm f ≫ g₂)
<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>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>f : L.obj X ⟶ L.obj Y<VAR>g₁ g₂ : L.obj Y ⟶ L.obj Z<GOAL>(homEquiv eX eY).symm f ≫ add W eY eZ ((homEquiv eY eZ).symm g₁) ((homEquiv eY eZ).symm g₂) = add W eX eZ ((homEquiv eX eY).symm f ≫ (homEquiv eY eZ).symm g₁) ((homEquiv eX eY).symm f ≫ (homEquiv eY eZ).symm g₂)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝ : S.HasHomology<GOAL>(S.rightHomologyIso.inv ≫ S.rightHomologyι) ≫ S.fromOpcycles = 0
<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✝ : TopologicalSpace X<VAR>x : X<GOAL>𝓝 x = ⨅ s, ⨅ (_ : IsOpen s), ⨅ (_ : x ∈ s), 𝓟 s
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<GOAL>∀ (x y : A), (↑{ toFun := fun a => a ⊗ₜ[R] 1, map_one' := ⋯, map_mul' := ⋯ }).toFun (x + y) = (↑{ toFun := fun a => a ⊗ₜ[R] 1, map_one' := ⋯, map_mul' := ⋯ }).toFun x + (↑{ toFun := fun a => a ⊗ₜ[R] 1, map_one' := ⋯, map_mul' := ⋯ }).toFun y
<VAR>R : Type u<VAR>inst✝ : LinearOrder R<VAR>x y z : Tropical R<GOAL>x + y = z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x
<VAR>R : Type u<VAR>inst✝ : LinearOrder R<VAR>x y z : Tropical R<GOAL>min (untrop x) (untrop y) = untrop z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x
<VAR>E : Type u_1<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : T2Space E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : E<GOAL>(𝓝 x).HasBasis (fun r => 0 < r) (ball x)
<VAR>E : Type u_1<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : T2Space E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : E<GOAL>(Filter.comap (⇑toEuclidean.toHomeomorph) (𝓝 (toEuclidean.toHomeomorph x))).HasBasis (fun r => 0 < r) (ball x)
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : AffineSpace V P<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : Module k V<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : FiniteDimensional k V<VAR>h : Fintype.card ι = FiniteDimensional.finrank k V + 1<GOAL>Nonempty (AffineBasis ι k P)
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : AffineSpace V P<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : Module k V<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : FiniteDimensional k V<VAR>h : Fintype.card ι = FiniteDimensional.finrank k V + 1<VAR>s : Set P<VAR>b : AffineBasis (↑s) k P<VAR>hb : ⇑b = Subtype.val<GOAL>Nonempty (AffineBasis ι k P)
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : AffineSpace V P<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : Module k V<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : FiniteDimensional k V<VAR>h : Fintype.card ι = FiniteDimensional.finrank k V + 1<VAR>s : Finset P<VAR>b : AffineBasis (↑↑s) k P<VAR>hb : ⇑b = Subtype.val<GOAL>Nonempty (AffineBasis ι k P)
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : AffineSpace V P<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : Module k V<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : FiniteDimensional k V<VAR>h : Fintype.card ι = FiniteDimensional.finrank k V + 1<VAR>s : Finset P<VAR>b : AffineBasis (↑↑s) k P<VAR>hb : ⇑b = Subtype.val<GOAL>Fintype.card ↑↑s = Fintype.card ι
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>s✝ s₁ s₂ : Finset ι<VAR>t✝ t₁ t₂ : (i : ι) → Finset (α i)<VAR>inst✝ : DecidableEq ((i : ι) × α i)<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<VAR>x : ι<VAR>y : α x<GOAL>⟨x, y⟩ ∈ s.sigma t ↔ ⟨x, y⟩ ∈ s.biUnion fun i => map (Embedding.sigmaMk i) (t i)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>σ : Type u_4<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>S s : Subsemigroup M<VAR>x : M × N<GOAL>x ∈ s.prod ⊤ ↔ x ∈ comap (MulHom.fst M N) s
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>h : v ≠ 0<GOAL>∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x) = 1
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>h : v ≠ 0<GOAL>(∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x)).toReal = 1
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>h : v ≠ 0<VAR>hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ<GOAL>(∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x)).toReal = 1
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>h : v ≠ 0<VAR>hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ<VAR>hf : 0 ≤ᶠ[ae ℙ] gaussianPDFReal μ v<GOAL>(∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x)).toReal = 1
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>h : v ≠ 0<VAR>hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ<VAR>hf : 0 ≤ᶠ[ae ℙ] gaussianPDFReal μ v<GOAL>∫ (a : ℝ), gaussianPDFReal μ v a = 1
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>h : v ≠ 0<VAR>hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ<VAR>hf : 0 ≤ᶠ[ae ℙ] gaussianPDFReal μ v<GOAL>(√(2 * π * ↑v))⁻¹ * ∫ (a : ℝ), rexp (-(a - μ) ^ 2 / (2 * ↑v)) = 1
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>h : v ≠ 0<VAR>hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ<VAR>hf : 0 ≤ᶠ[ae ℙ] gaussianPDFReal μ v<GOAL>(√(2 * π * ↑v))⁻¹ * ∫ (x : ℝ), rexp (-x ^ 2 / (2 * ↑v)) = 1
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>h : v ≠ 0<VAR>hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ<VAR>hf : 0 ≤ᶠ[ae ℙ] gaussianPDFReal μ v<GOAL>(√(2 * π * ↑v))⁻¹ * ∫ (x : ℝ), rexp (-((↑v)⁻¹ * 2⁻¹ * x ^ 2)) = 1
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>h : v ≠ 0<VAR>hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ<VAR>hf : 0 ≤ᶠ[ae ℙ] gaussianPDFReal μ v<GOAL>(√(2 * π * ↑v))⁻¹ * ∫ (x : ℝ), rexp (-(↑v)⁻¹ * 2⁻¹ * x ^ 2) = 1
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>h : v ≠ 0<VAR>hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ<VAR>hf : 0 ≤ᶠ[ae ℙ] gaussianPDFReal μ v<GOAL>√((2 * π * ↑v)⁻¹ * (π / ((↑v)⁻¹ * 2⁻¹))) = 1
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>h : v ≠ 0<VAR>hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ<VAR>hf : 0 ≤ᶠ[ae ℙ] gaussianPDFReal μ v<GOAL>0 ≤ (2 * π * ↑v)⁻¹
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<GOAL>↑((associatesEquivIsPrincipal R) 0) = 0
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>eval (v i) ((interpolate s v) r) = r i
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>eval (v i) (C (r i) * Lagrange.basis s v i) + ∑ x ∈ s.erase i, eval (v i) (C (r x) * Lagrange.basis s v x) = r i
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>∑ x ∈ s.erase i, r x * eval (v i) (Lagrange.basis s v x) = 0
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j✝ : ι<VAR>v r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<VAR>j : ι<VAR>H : j ∈ s.erase i<GOAL>r j * eval (v i) (Lagrange.basis s v j) = 0
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M'<VAR>inst✝⁸ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Module A M'<VAR>inst✝⁴ : IsLocalization S A<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>inst✝ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>r : R<VAR>m : LocalizedModule S M<VAR>a : M<VAR>b : ↥S<GOAL>r • lift' S g h (mk a b) = lift' S g h (r • mk a b)
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M'<VAR>inst✝⁸ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Module A M'<VAR>inst✝⁴ : IsLocalization S A<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>inst✝ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>r : R<VAR>m : LocalizedModule S M<VAR>a : M<VAR>b : ↥S<GOAL>r • ↑⋯.unit⁻¹ (g a) = ↑⋯.unit⁻¹ (g (r • a))
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>inst✝⁹ : Ring k<VAR>inst✝⁸ : AddCommGroup V₁<VAR>inst✝⁷ : Module k V₁<VAR>inst✝⁶ : AffineSpace V₁ P₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AffineSpace V₂ P₂<VAR>inst✝² : AddCommGroup V₃<VAR>inst✝¹ : Module k V₃<VAR>inst✝ : AffineSpace V₃ P₃<VAR>f : P₁ ≃ᵃ[k] P₂<VAR>s : Set P₂<GOAL>comap (↑f) (affineSpan k s) = affineSpan k (⇑f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : Filter α<VAR>u : α → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>h : ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Icc (a - ε) (a + ε)<GOAL>Tendsto u f (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : Filter α<VAR>u : α → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>h : ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Icc (a - ε) (a + ε)<GOAL>Tendsto u f (⨅ ε, ⨅ (_ : ε > 0), 𝓟 (Icc (a - ε) (a + ε)))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>hb : 0 < b<GOAL>a / b < 1 ↔ a < b
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a✝ b : R<VAR>n : ℕ<VAR>M : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>q : Submodule R M<VAR>m : M<VAR>hm : m ∈ q<VAR>p : R[X]<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Module A M<VAR>inst✝ : IsScalarTower R A M<VAR>a : A<VAR>hq : q ≤ Submodule.comap ((Algebra.lsmul R R M) a) q<GOAL>(aeval a) p • m ∈ q
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a✝ b : R<VAR>n : ℕ<VAR>M : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>q : Submodule R M<VAR>m : M<VAR>hm : m ∈ q<VAR>p : R[X]<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Module A M<VAR>inst✝ : IsScalarTower R A M<VAR>a : A<VAR>hq : q ≤ Submodule.comap ((Algebra.lsmul R R M) a) q<VAR>f₁ f₂ : R[X]<VAR>h₁ : (fun f => (aeval a) f • m ∈ q) f₁<VAR>h₂ : (fun f => (aeval a) f • m ∈ q) f₂<GOAL>(fun f => (aeval a) f • m ∈ q) (f₁ + f₂)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>M : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>q : Submodule R M<VAR>m : M<VAR>hm : m ∈ q<VAR>p : R[X]<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Module A M<VAR>inst✝ : IsScalarTower R A M<VAR>a : A<VAR>hq : q ≤ Submodule.comap ((Algebra.lsmul R R M) a) q<VAR>n : ℕ<VAR>t : R<VAR>hmq : (fun f => (aeval a) f • m ∈ q) (C t * X ^ n)<GOAL>(fun f => (aeval a) f • m ∈ q) (C t * X ^ (n + 1))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>convexBodySumFun (-x) = convexBodySumFun x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrderedAddCommGroup α<VAR>inst✝¹ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<GOAL>(𝓝 a).HasBasis (fun ε => 0 < ε) fun ε => Ioo (a - ε) (a + ε)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrderedAddCommGroup α<VAR>inst✝¹ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>inst✝ : NoMaxOrder α<VAR>a x✝ : α<GOAL>Ioo (a - x✝) (a + x✝) = {b | |b - a| < x✝}
<VAR>x y : ℕ<GOAL>x.gcd y = if x = 0 then y else (y % x).gcd x
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>Mono (ModuleCat.ofHom (πs C o))
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>Function.Injective ⇑(ModuleCat.ofHom (πs C o))
<VAR>Γ : Type u_1<VAR>inst✝¹ : Inhabited Γ<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>inst✝ : Inhabited Λ<VAR>M : Λ → Stmt₁<VAR>S : Finset Λ<VAR>ss : Supports M S<VAR>l₁ : Λ<VAR>v : σ<VAR>T : Tape Γ<VAR>c' : Cfg₁<VAR>h₁ : c' ∈ step M { l := some l₁, var := v, Tape := T }<VAR>h₂ : { l := some l₁, var := v, Tape := T }.l ∈ Finset.insertNone S<GOAL>c'.l ∈ Finset.insertNone S
<VAR>Γ : Type u_1<VAR>inst✝¹ : Inhabited Γ<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>inst✝ : Inhabited Λ<VAR>M : Λ → Stmt₁<VAR>S : Finset Λ<VAR>ss : Supports M S<VAR>l₁ : Λ<VAR>v : σ<VAR>T : Tape Γ<VAR>c' : Cfg₁<VAR>h₁ : c' ∈ step M { l := some l₁, var := v, Tape := T }<VAR>h₂ : SupportsStmt S (M l₁)<GOAL>c'.l ∈ Finset.insertNone S
<VAR>Γ : Type u_1<VAR>inst✝¹ : Inhabited Γ<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>inst✝ : Inhabited Λ<VAR>M : Λ → Stmt₁<VAR>S : Finset Λ<VAR>ss : Supports M S<VAR>l₁ : Λ<VAR>v : σ<VAR>T : Tape Γ<VAR>c' : Cfg₁<VAR>h₂ : SupportsStmt S (M l₁)<VAR>h₁ : stepAux (M l₁) v T = c'<GOAL>c'.l ∈ Finset.insertNone S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : Zero M<VAR>inst✝ : Zero N<VAR>f : α ↪ β<VAR>v : α →₀ M<VAR>a : β<VAR>h : a ∉ Set.range ⇑f<GOAL>(embDomain f v) a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Preorder α<VAR>inst✝² : AddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<GOAL>a - b ≤ 0 ↔ a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁸ : Preorder α<VAR>inst✝⁷ : Add α<VAR>inst✝⁶ : Sub α<VAR>inst✝⁵ : OrderedSub α<VAR>a✝ b✝ c✝ d : α<VAR>R : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Preorder R<VAR>inst✝² : Sub R<VAR>inst✝¹ : OrderedSub R<VAR>inst✝ : CovariantClass R R (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : R<GOAL>a * c - b * c ≤ (a - b) * c
<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 a b : Set α<VAR>f : α → β<VAR>h : a ⊆ b<GOAL>f '' a ⊆ f '' 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 a b : Set α<VAR>f : α → β<VAR>h : a ⊆ b<GOAL>∀ (x : β), (∃ x_1 ∈ a, f x_1 = x) → ∃ x_1 ∈ b, f x_1 = x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<GOAL>(x ~ᵢ y) ↔ ∀ (s : Set X), IsClosed s → (x ∈ s ↔ y ∈ s)
<VAR>σ : Type u<VAR>F G : Type u → Type u<VAR>inst✝¹ : Applicative F<VAR>inst✝ : Applicative G<VAR>α β γ : Type u<VAR>g : α → β<VAR>f : β → G γ<VAR>x : σ ⊕ α<GOAL>Sum.traverse f (g <$> x) = Sum.traverse (f ∘ g) x
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>(starRingEnd K) z * z = ↑‖z‖ ^ 2
<VAR>α : Type u_1<VAR>b : PosNum<GOAL>1 + b.succ = (1 + b).succ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : QuadraticMap 𝕜 E F<VAR>a b : E<GOAL>lineDeriv 𝕜 (⇑f) a b = polar (⇑f) a b
<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>β : Type u_7<VAR>inst✝ : MeasurableSpace β<VAR>φ : α → β<VAR>hφ : Measurable φ<VAR>f : β → G<VAR>hfm : StronglyMeasurable f<VAR>hG : CompleteSpace G<VAR>hfi : Integrable f (Measure.map φ μ)<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<GOAL>∫ (y : β), f y ∂Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ
<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>β : Type u_7<VAR>inst✝ : MeasurableSpace β<VAR>φ : α → β<VAR>hφ : Measurable φ<VAR>f : β → G<VAR>hfm : StronglyMeasurable f<VAR>hG : CompleteSpace G<VAR>hfi : Integrable f (Measure.map φ μ)<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>this : SeparableSpace ↑(range f ∪ {0})<GOAL>∫ (y : β), f y ∂Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ
<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>β : Type u_7<VAR>inst✝ : MeasurableSpace β<VAR>φ : α → β<VAR>hφ : Measurable φ<VAR>f : β → G<VAR>hfm : StronglyMeasurable f<VAR>hG : CompleteSpace G<VAR>hfi : Integrable f (Measure.map φ μ)<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>this : SeparableSpace ↑(range f ∪ {0})<GOAL>Tendsto (fun n => SimpleFunc.integral (Measure.map φ μ) (approxOn f ⋯ (range f ∪ {0}) 0 ⋯ n)) atTop (𝓝 (∫ (x : α), f (φ x) ∂μ))