ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>N : Submodule R M<VAR>inst✝ : IsArtinianRing R<VAR>hN : N.FG<VAR>s : Finset M<VAR>hs : span R ↑s = N<VAR>this✝ : DecidableEq M<VAR>this : DecidableEq R<GOAL>IsArtinian R ↥N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>N : Submodule R M<VAR>inst✝ : IsArtinianRing R<VAR>hN : N.FG<VAR>s : Finset M<VAR>hs : span R ↑s = N<VAR>this✝¹ : DecidableEq M<VAR>this✝ : DecidableEq R<VAR>this : ∀ x ∈ s, x ∈ N<GOAL>IsArtinian R ↥N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>N : Submodule R M<VAR>inst✝ : IsArtinianRing R<VAR>hN : N.FG<VAR>s : Finset M<VAR>hs : span R ↑s = N<VAR>this✝¹ : DecidableEq M<VAR>this✝ : DecidableEq R<VAR>this : ∀ x ∈ s, x ∈ N<GOAL>(↑↑s →₀ R) →ₗ[R] ↥N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>N : Submodule R M<VAR>inst✝ : IsArtinianRing R<VAR>hN : N.FG<VAR>s : Finset M<VAR>hs : span R ↑s = N<VAR>this✝¹ : DecidableEq M<VAR>this✝ : DecidableEq R<VAR>this : ∀ x ∈ s, x ∈ N<GOAL>Surjective ⇑?refine_1
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c a : G₀<GOAL>a / (a / a) = a
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a : α<VAR>l₁ : List α<VAR>b : α<VAR>l₂ : List α<VAR>h₁ : a ∈ l₁<VAR>h₂ : ¬a ∈ b :: l₂<GOAL>a ∈ l₁.diff (b :: l₂)
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a : α<VAR>l₁ : List α<VAR>b : α<VAR>l₂ : List α<VAR>h₁ : a ∈ l₁<VAR>h₂ : ¬a ∈ b :: l₂<GOAL>a ∈ (l₁.erase b).diff l₂
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasShift C ℤ<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>S : Subcategory C<VAR>Y Z : C<VAR>g : Y ⟶ Z<GOAL>S.W g ↔ ∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), S.P X
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasShift C ℤ<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>S : Subcategory C<VAR>Y Z : C<VAR>g : Y ⟶ Z<GOAL>(∃ Z_1 g_1 h, ∃ (_ : Triangle.mk g g_1 h ∈ distinguishedTriangles), S.P Z_1) ↔ ∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), S.P X
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>completedSinZeta a (1 - s) = completedHurwitzZetaOdd a s
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup V<VAR>inst✝⁶ : InnerProductSpace ℝ V<VAR>inst✝⁵ : MetricSpace P<VAR>inst✝⁴ : NormedAddTorsor V P<VAR>p p₀ p₁✝ p₂✝ : P<VAR>V₂ : Type u_3<VAR>P₂ : Type u_4<VAR>inst✝³ : NormedAddCommGroup V₂<VAR>inst✝² : InnerProductSpace ℝ V₂<VAR>inst✝¹ : MetricSpace P₂<VAR>inst✝ : NormedAddTorsor V₂ P₂<VAR>f : P →ᵃⁱ[ℝ] P₂<VAR>p₁ p₂ p₃ : P<GOAL>∠ (f p₁) (f p₂) (f p₃) = ∠ p₁ p₂ p₃
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<GOAL>(map f H).index ∣ H.index
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<GOAL>(H ⊔ f.ker).index ∣ H.index
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J K L I : Ideal R<VAR>hI : I.IsPrime<VAR>s : Finset R<GOAL>∏ x ∈ s, x ∈ I ↔ ∃ p ∈ s, p ∈ I
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J K L I : Ideal R<VAR>hI : I.IsPrime<VAR>s : Finset R<GOAL>s.val.prod ∈ I ↔ ∃ p ∈ s, p ∈ I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>m : ℕ<VAR>h : Finite a b<VAR>hm : (multiplicity a b).get h < m<GOAL>multiplicity a b < ↑m
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<VAR>s : Set Ω<GOAL>μ s ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>s : Set α<VAR>a : α<VAR>inst✝ : MeasurableSpace.SeparatesPoints α<VAR>x y : α<VAR>x_ne_y : (fun x => dirac x) x = (fun x => dirac x) y<GOAL>x = y
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝³ : CommSemiring k<VAR>inst✝² : Group G<VAR>inst✝¹ : AddCommMonoid V<VAR>inst✝ : Module k V<VAR>ρ : Representation k G V<VAR>v : V<GOAL>v ∈ ρ.invariants ↔ ∀ (g : G), (ρ g) v = v
<VAR>a b : Ordinal.{u_1}<VAR>b1 : 0 < b<GOAL>a ≤ a ^ b
<VAR>a b : Ordinal.{u_1}<VAR>b1 : 0 < b<GOAL>a ^ 1 ≤ a ^ b
<VAR>a b : Ordinal.{u_1}<VAR>b1 : 0 < b<VAR>a1 : a ≤ 1<GOAL>a ^ 1 ≤ a ^ b
<VAR>a b : Ordinal.{u_1}<VAR>b1 : 0 < b<VAR>a1 : a > 1<GOAL>a ^ 1 ≤ a ^ b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>a✝ b c d e : α<VAR>m n✝ : ℤ<VAR>a : ℕ<VAR>h : 0 < a<VAR>n : ℤ<GOAL>0 < ↑a ^ n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>a✝ b c d e : α<VAR>m n✝ : ℤ<VAR>a : ℕ<VAR>h : 0 < a<VAR>n : ℤ<GOAL>0 < ↑a
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I✝ : Ideal α<VAR>a b : α<VAR>I : Ideal α<VAR>hI : I.IsMaximal<VAR>x : α<VAR>hx : x ∉ I<GOAL>∃ y, ∃ i ∈ I, y * x + i = 1
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I✝ : Ideal α<VAR>a b : α<VAR>I : Ideal α<VAR>hI : I.IsMaximal<VAR>x : α<VAR>hx : x ∉ I<VAR>H₁ : 1 ∉ I<VAR>H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J<GOAL>∃ y, ∃ i ∈ I, y * x + i = 1
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I✝ : Ideal α<VAR>a b : α<VAR>I : Ideal α<VAR>hI : I.IsMaximal<VAR>x : α<VAR>hx : x ∉ I<VAR>H₁ : 1 ∉ I<VAR>H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J<VAR>y z : α<VAR>hz : z ∈ span ↑I<VAR>hy : 1 = y * x + z<GOAL>∃ y, ∃ i ∈ I, y * x + i = 1
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I✝ : Ideal α<VAR>a b : α<VAR>I : Ideal α<VAR>hI : I.IsMaximal<VAR>x : α<VAR>hx : x ∉ I<VAR>H₁ : 1 ∉ I<VAR>H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J<VAR>y z : α<VAR>hz : z ∈ span ↑I<VAR>hy : 1 = y * x + z<GOAL>z ∈ I
<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>r : ℝ<VAR>hr : r ≠ 0<GOAL>2 • o.oangle (r • x) y = 2 • o.oangle x y
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>Q : QuadraticMap R M N<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower S R M<VAR>inst✝¹ : Module S N<VAR>inst✝ : IsScalarTower S R N<VAR>x y : M<GOAL>(⋯.choose x) y = (Q.polarBilin x) y
<VAR>Ω : Type u_1<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁴ : SMul R ℝ≥0<VAR>inst✝³ : SMul R ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ≥0<VAR>c : R<VAR>μ : FiniteMeasure Ω<GOAL>⇑(c • μ) = c • ⇑μ
<VAR>Ω : Type u_1<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁴ : SMul R ℝ≥0<VAR>inst✝³ : SMul R ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ≥0<VAR>c : R<VAR>μ : FiniteMeasure Ω<VAR>x✝ : Set Ω<GOAL>(c • μ) x✝ = (c • ⇑μ) x✝
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(imageIsoImage f).hom ≫ Limits.image.ι f = kernel.ι (cokernel.π f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>c : ℝ<VAR>c_nn : 0 ≤ c<GOAL>closedBall 0 c = Icc 0 c.toNNReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>c : ℝ<VAR>c_nn : 0 ≤ c<GOAL>c.toNNReal = ⟨c, c_nn⟩
<VAR>α : Type u_1<VAR>p : PosNum<GOAL>↑(pos p).pred = (↑(pos p)).pred
<VAR>α : Type u_1<VAR>p : PosNum<GOAL>(↑p).pred = (↑(pos p)).pred
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → 𝕜<VAR>g : E → F<VAR>hf : ContDiffAt 𝕜 n f x<VAR>hg : ContDiffAt 𝕜 n g x<GOAL>ContDiffAt 𝕜 n (fun x => f x • g x) x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → 𝕜<VAR>g : E → F<VAR>hf : ContDiffWithinAt 𝕜 n f univ x<VAR>hg : ContDiffWithinAt 𝕜 n g univ x<GOAL>ContDiffWithinAt 𝕜 n (fun x => f x • g x) univ x
<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>0 < r.sign * r
<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>h : 0 = r.sign * r<GOAL>r = 0
<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>h : 0 = r.sign * r<VAR>hs0 : r.sign = 0<GOAL>r = 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>val✝ : ↑(PrimeSpectrum.Top R)<VAR>property✝ : val✝ ∈ U<GOAL>(stalkToFiberRingHom R ↑⟨val✝, property✝⟩) (((structureSheaf R).presheaf.germ ⟨val✝, property✝⟩) s) = ↑s ⟨val✝, property✝⟩
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.degree = 1<GOAL>C (p.coeff 1) * X + C (p.coeff 0) = C p.leadingCoeff * X + C (p.coeff 0)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.degree = ↑1<GOAL>C (p.coeff 1) * X + C (p.coeff 0) = C p.leadingCoeff * X + C (p.coeff 0)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>e : (Module.Dual R M ⊗[R] M × Module.Dual R N ⊗[R] N) ≃ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N) := (dualTensorHomEquiv R M M).prod (dualTensorHomEquiv R N N)<GOAL>trace R (M × N) ∘ₗ prodMapLinear R M N M N R = id.coprod id ∘ₗ (trace R M).prodMap (trace R N)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>e : (Module.Dual R M ⊗[R] M × Module.Dual R N ⊗[R] N) ≃ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N) := (dualTensorHomEquiv R M M).prod (dualTensorHomEquiv R N N)<VAR>h : Function.Surjective ⇑↑e<GOAL>trace R (M × N) ∘ₗ prodMapLinear R M N M N R = id.coprod id ∘ₗ (trace R M).prodMap (trace R N)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>e : (Module.Dual R M ⊗[R] M × Module.Dual R N ⊗[R] N) ≃ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N) := (dualTensorHomEquiv R M M).prod (dualTensorHomEquiv R N N)<VAR>h : Function.Surjective ⇑↑e<GOAL>(trace R (M × N) ∘ₗ prodMapLinear R M N M N R) ∘ₗ ↑e = (id.coprod id ∘ₗ (trace R M).prodMap (trace R N)) ∘ₗ ↑e
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>l : Filter α<VAR>inst✝ : CountableInterFilter l<VAR>s t : Set α<VAR>hst : s =ᶠ[l] t<VAR>t' : Set α<VAR>ht' : MeasurableSet t'<VAR>htt' : t =ᶠ[l] t'<GOAL>EventuallyMeasurableSet m l s
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.inits = l.initsTR
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.inits = (foldr (fun a arrs => (Array.map (fun t => a :: t) arrs).push []) #[[]] l).data.reverse
<VAR>u : Lean.Level<VAR>n✝¹ num✝ : ℤ<VAR>n✝ denom✝ : ℕ<VAR>inv✝ : Invertible ↑denom✝<VAR>h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝<GOAL>IsRat (mkRat ↑n✝¹ ↑n✝) num✝ denom✝
<VAR>u : Lean.Level<VAR>n✝¹ num✝ : ℤ<VAR>n✝ denom✝ : ℕ<VAR>inv✝ : Invertible ↑denom✝<VAR>h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝<GOAL>IsRat (↑↑n✝¹ / ↑↑n✝) num✝ denom✝
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ z⁻¹ < y ↔ x < y ^ z
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>I : MulticospanIndex C<VAR>inst✝² : HasMultiequalizer I<VAR>inst✝¹ : HasProduct I.left<VAR>inst✝ : HasProduct I.right<VAR>a : I.L<GOAL>ιPi I ≫ Pi.π I.left a = ι I a
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>I : MulticospanIndex C<VAR>inst✝² : HasMultiequalizer I<VAR>inst✝¹ : HasProduct I.left<VAR>inst✝ : HasProduct I.right<VAR>a : I.L<GOAL>equalizer.ι I.fstPiMap I.sndPiMap ≫ Pi.π I.left a = (limit.isoLimitCone { cone := I.multiforkEquivPiFork.inverse.obj (limit.cone (parallelPair I.fstPiMap I.sndPiMap)), isLimit := IsLimit.ofPreservesConeTerminal I.multiforkEquivPiFork.inverse (limit.isLimit (parallelPair I.fstPiMap I.sndPiMap)) }).inv ≫ ι I a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ m : MeasurableSpace α<VAR>v : VectorMeasure α ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>v.ennrealToMeasure s = ↑v s
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>inst✝¹ : K.HasHomology j<VAR>inst✝ : (K.sc' i j k).HasHomology<GOAL>(K.opcyclesIsoSc' i j k hi hk).inv ≫ K.fromOpcycles j k = (K.sc' i j k).fromOpcycles
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : α ↪ β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α ≃ β<GOAL>map f.symm.toEmbedding t ⊆ s ↔ t ⊆ map f.toEmbedding s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x✝ y✝ z : P<VAR>x y : V<GOAL>midpoint R x y +ᵥ midpoint R x y = midpoint R x y +ᵥ midpoint R y x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x✝ y✝ z : P<VAR>x y : V<GOAL>midpoint R x y +ᵥ midpoint R y x = x + y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<GOAL>μ (s ∪ t) < ⊤ ↔ μ s < ⊤ ∧ μ t < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>h : μ (s ∪ t) < ⊤<GOAL>μ s < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>h : μ (s ∪ t) < ⊤<GOAL>μ t < ⊤
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>0 ≤ -x + x
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>-(-x + x) ≤ 0
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>X Y : C<VAR>inst✝¹ : HasBinaryBiproduct X Y<VAR>inst✝ : PreservesBinaryBiproduct X Y F<VAR>W : C<VAR>f : X ⟶ W<VAR>g : Y ⟶ W<GOAL>(F.mapBiprod X Y).inv ≫ F.map (desc f g) = desc (F.map f) (F.map g)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<GOAL>IsProperMap f ↔ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<GOAL>(Continuous f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ) ↔ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>x✝ : Continuous f<GOAL>(∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ) ↔ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
<VAR>x y : PartENat<GOAL>x < y ↔ ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy
<VAR>x y : PartENat<GOAL>((∃ (h : y.Dom → x.Dom), ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy) ∧ ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), y.get ⋯ ≤ x.get hy) ↔ ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z✝ X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>homeo : ↑(pullback f g) ≃ₜ ↑(of { p // f p.1 = g p.2 }) := homeoOfIso (pullbackIsoProdSubtype f g)<GOAL>(pullback f g).str = induced (⇑(pullback.fst f g)) X.str ⊓ induced (⇑(pullback.snd f g)) Y.str
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z✝ X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>homeo : ↑(pullback f g) ≃ₜ ↑(of { p // f p.1 = g p.2 }) := homeoOfIso (pullbackIsoProdSubtype f g)<GOAL>induced (⇑homeo) (of { p // f p.1 = g p.2 }).topologicalSpace_coe = induced (⇑(pullback.fst f g)) X.str ⊓ induced (⇑(pullback.snd f g)) Y.str
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z✝ X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>homeo : ↑(pullback f g) ≃ₜ ↑(of { p // f p.1 = g p.2 }) := homeoOfIso (pullbackIsoProdSubtype f g)<GOAL>induced (⇑homeo) (induced Subtype.val (induced Prod.fst X.str ⊓ induced Prod.snd Y.str)) = induced (⇑(pullback.fst f g)) X.str ⊓ induced (⇑(pullback.snd f g)) Y.str
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z✝ X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>homeo : ↑(pullback f g) ≃ₜ ↑(of { p // f p.1 = g p.2 }) := homeoOfIso (pullbackIsoProdSubtype f g)<GOAL>induced ((Prod.fst ∘ Subtype.val) ∘ ⇑homeo) X.str ⊓ induced ((Prod.snd ∘ Subtype.val) ∘ ⇑homeo) Y.str = induced (⇑(pullback.fst f g)) X.str ⊓ induced (⇑(pullback.snd f g)) Y.str
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>ι : Type v<VAR>α : ι → TopCat<VAR>i : ι<VAR>x : ↑(α i)<GOAL>(sigmaIsoSigma α).inv ⟨i, x⟩ = (Sigma.ι α i) x
<VAR>n m : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a ≠ 0<GOAL>(a.pred ha).castSucc < b ↔ a ≤ b
<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>h : contained C o<VAR>this : (∀ (i : I), ∀ x ∈ C, x i ≠ false → ord I i < o) → (π C fun x => ord I x < o) = C<GOAL>C = π C fun x => ord I x < 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>h : contained C o<VAR>this : (∀ (i : I), ∀ x ∈ C, x i = true → ord I i < o) → (Proj fun x => ord I x < o) '' C = C<GOAL>C = π C fun x => ord I x < o
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g'✝ g✝ φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>f f' g g' : ℝ → ℝ<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hf' : ContinuousOn f' [[a, b]]<VAR>hg : ContinuousOn g [[f a, f b]]<VAR>hgg' : ∀ x ∈ Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Ioi x) x<VAR>hg' : ContinuousOn g' (f '' [[a, b]])<GOAL>∫ (x : ℝ) in a..b, (g' ∘ f) x * f' x = (g ∘ f) b - (g ∘ f) a
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<GOAL>LocallyIntegrableOn P.f_modif (Ioi 0) volume
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume<GOAL>LocallyIntegrableOn P.f_modif (Ioi 0) volume
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>IntegrableAtFilter ((Ioi 1).indicator fun x => P.f x - P.f₀) (𝓝[Ioi 0] x) volume
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>IntegrableAtFilter ((Ioo 0 1).indicator fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) (𝓝[Ioi 0] x) volume
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<GOAL>map (mk' N) N' = ⊥ ↔ N' ≤ N
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<GOAL>asympBound g a b n = ↑n ^ p a b * (1 + ∑ u ∈ range n, g ↑u / ↑u ^ (p a b + 1))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : OrderedAddCommMonoid α<VAR>inst✝³ : OrderedAddCommMonoid β<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : SMul 𝕜 α<VAR>inst✝ : SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>g✝ : β → α<VAR>g : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>hfg : EqOn f g s<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>g (a • x + b • y) ≤ a • g x + b • g y
<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>inst✝² : LinearOrder γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderTopology γ<VAR>f : α → γ<GOAL>Continuous f ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hq : q.Monic<VAR>hp0 : p ≠ 0<VAR>h0q : 0 < q.degree<VAR>hpq : p.degree < q.degree<GOAL>(p /ₘ q).degree < p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hq : q.Monic<VAR>hp0 : p ≠ 0<VAR>h0q : 0 < q.degree<VAR>hpq : p.degree < q.degree<VAR>this : Nontrivial R<GOAL>(p /ₘ q).degree < p.degree