ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>S : Type u_2<VAR>inst✝ : Field S<VAR>f : R[X] →+* S<VAR>hf : Function.Surjective ⇑f<VAR>this : (RingHom.ker f).IsMaximal<VAR>g : R[X] ⧸ RingHom.ker f →+* S := Quotient.lift (RingHom.ker f) f ⋯<VAR>hfg : g.comp (Quotient.mk (RingHom.ker f)) = f<GOAL>(f.comp C).IsIntegral
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>S : Type u_2<VAR>inst✝ : Field S<VAR>f : R[X] →+* S<VAR>hf : Function.Surjective ⇑f<VAR>this : (RingHom.ker f).IsMaximal<VAR>g : R[X] ⧸ RingHom.ker f →+* S := Quotient.lift (RingHom.ker f) f ⋯<VAR>hfg : g.comp (Quotient.mk (RingHom.ker f)) = f<GOAL>(g.comp ((Quotient.mk (RingHom.ker f)).comp C)).IsIntegral
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>S : Type u_2<VAR>inst✝ : Field S<VAR>f : R[X] →+* S<VAR>hf : Function.Surjective ⇑f<VAR>this : (RingHom.ker f).IsMaximal<VAR>g : R[X] ⧸ RingHom.ker f →+* S := Quotient.lift (RingHom.ker f) f ⋯<VAR>hfg : g.comp (Quotient.mk (RingHom.ker f)) = f<GOAL>Function.Surjective ⇑g
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>S : Type u_2<VAR>inst✝ : Field S<VAR>f : R[X] →+* S<VAR>this : (RingHom.ker f).IsMaximal<VAR>g : R[X] ⧸ RingHom.ker f →+* S := Quotient.lift (RingHom.ker f) f ⋯<VAR>hf : Function.Surjective (⇑g ∘ ⇑(Quotient.mk (RingHom.ker f)))<VAR>hfg : g.comp (Quotient.mk (RingHom.ker f)) = f<GOAL>Function.Surjective ⇑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<VAR>r : ℝ≥0<VAR>hr : 0 < r<GOAL>nndist f g < r ↔ ∀ (b : β), nndist (f b) (g b) < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<VAR>r : ℝ≥0<VAR>hr : ⊥ < r<GOAL>nndist f g < r ↔ ∀ (b : β), nndist (f b) (g b) < r
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>m✝ : OuterMeasure α<VAR>β : Type u_3<VAR>f : α → β<VAR>hf : Injective f<VAR>m : OuterMeasure α<VAR>s : Set α<GOAL>((comap f) ((map f) m)) s = m s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>p : ι → P<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<GOAL>(s.weightedVSub p) (weightedVSubVSubWeights k i j) = p i -ᵥ p j
<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>φ : S₁ ⟶ S₂<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>h₁ : IsIso (opcyclesMap φ)<VAR>h₂ : Mono φ.τ₃<GOAL>IsIso (homologyMap φ)
<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>φ : S₁ ⟶ S₂<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>h₁ : IsIso (opcyclesMap φ)<VAR>h₂ : Mono φ.τ₃<VAR>h : (S₂.homologyι ≫ inv (opcyclesMap φ)) ≫ S₁.fromOpcycles = 0<GOAL>IsIso (homologyMap φ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : MeasurableSpace α<VAR>a : α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : Decidable (a ∈ s)<GOAL>∫⁻ (x : α) in s, f x ∂dirac a = if a ∈ s then f a else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : MeasurableSpace α<VAR>a : α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : Decidable (a ∈ s)<GOAL>(∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i j : N<VAR>f : ↑(Ω^ N X x)<GOAL>⟦symmAt i f⟧ = ⟦symmAt j f⟧
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i j : N<VAR>f : ↑(Ω^ N X x)<GOAL>⟦fromLoop i (Path.symm (toLoop i f))⟧ = ⟦fromLoop j (Path.symm (toLoop j f))⟧
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i j : N<VAR>f : ↑(Ω^ N X x)<VAR>inv : (G : Type ?u.632657) → Group G → G → G := fun G x x_1 => x_1⁻¹<GOAL>⟦fromLoop i (Path.symm (toLoop i f))⟧ = ⟦fromLoop j (Path.symm (toLoop j f))⟧
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝² : Semiring R<VAR>p q r : R[X]<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Semiring T<VAR>f : R →+* S<VAR>g : S →+* T<VAR>x : S<GOAL>g (eval₂ f x p) = eval₂ (g.comp f) (g x) p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>E : Type u_4<VAR>inst✝ : One β<VAR>l : Filter α<VAR>f : α → β<VAR>s : Set α<VAR>hf : f =ᶠ[l] 1<GOAL>s.mulIndicator 1 =ᶠ[l] 1
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hp : ¬Prime p<GOAL>p ^ n.factorization p = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α<VAR>s : Finset α<VAR>h : a ∉ s<GOAL>(a :: s.toList).Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α<VAR>s : Finset α<VAR>h : a ∉ s<VAR>x : α<GOAL>x ∈ (cons a s h).toList ↔ x ∈ a :: s.toList
<VAR>α : Type u<VAR>β : Type v<VAR>σ τ : Perm α<VAR>hστ : σ.Disjoint τ<VAR>n : ℕ<GOAL>(σ * τ) ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeInf α<VAR>a : α<VAR>f : β → ↑(Iio a)<VAR>l : Filter β<GOAL>Tendsto f l atBot ↔ Tendsto (fun x => ↑(f x)) l atBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_3<VAR>m : Type u_4<VAR>R : Type u_5<VAR>inst✝² : CommSemiring α<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n α<VAR>h : A.IsSymm<VAR>k : ℕ<GOAL>(A ^ k).IsSymm
<VAR>S T : ℝ<VAR>hT : 0 < T<VAR>z τ : ℂ<VAR>hz : |z.im| ≤ S<VAR>hτ : T ≤ τ.im<VAR>n : ℤ<GOAL>‖jacobiTheta₂'_term n z τ‖ ≤ 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
<VAR>S T : ℝ<VAR>hT : 0 < T<VAR>z τ : ℂ<VAR>hz : |z.im| ≤ S<VAR>hτ : T ≤ τ.im<VAR>n : ℤ<GOAL>‖2 * ↑π * I * ↑n‖ * ‖jacobiTheta₂_term n z τ‖ ≤ 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
<VAR>S T : ℝ<VAR>hT : 0 < T<VAR>z τ : ℂ<VAR>hz : |z.im| ≤ S<VAR>hτ : T ≤ τ.im<VAR>n : ℤ<GOAL>‖2 * ↑π * I * ↑n‖ = 2 * π * ↑|n|
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>r : α → β → Prop<GOAL>(∀ (a : α), ∃! b, r a b) ↔ ∃ f, r = fun x x_1 => f x = x_1
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ Z✝ : C<VAR>f : Y✝ ⟶ X✝<VAR>S R : Sieve X✝<VAR>I : Type u_1<VAR>Y : I → C<VAR>X : C<VAR>i : I<VAR>g : X ⟶ Y i<VAR>Z : C<VAR>h : Z ⟶ X<GOAL>(ofObjects Y X).arrows h ↔ ⊤.arrows h
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ Z✝ : C<VAR>f : Y✝ ⟶ X✝<VAR>S R : Sieve X✝<VAR>I : Type u_1<VAR>Y : I → C<VAR>X : C<VAR>i : I<VAR>g : X ⟶ Y i<VAR>Z : C<VAR>h : Z ⟶ X<GOAL>(ofObjects Y X).arrows h
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ Z✝ : C<VAR>f : Y✝ ⟶ X✝<VAR>S R : Sieve X✝<VAR>I : Type u_1<VAR>Y : I → C<VAR>X : C<VAR>i : I<VAR>g : X ⟶ Y i<VAR>Z : C<VAR>h : Z ⟶ X<GOAL>∃ i, Nonempty (Z ⟶ Y i)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>hc : c ≠ 0<GOAL>a ≤ b / c ↔ a * c ≤ b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : HeytingAlgebra α<VAR>inst✝¹ : HeytingAlgebra β<VAR>inst✝ : HeytingHomClass F α β<VAR>f : F<VAR>a : α<GOAL>f aᶜ = (f a)ᶜ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>pb : PowerBasis A B<VAR>b : B<GOAL>∃ a, pb.gen ∣ b - (algebraMap A B) a
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsIntegrallyClosed R<VAR>p : R[X]<VAR>h : p.Monic<GOAL>Irreducible p ↔ Irreducible (Polynomial.map (algebraMap R K) p)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsIntegrallyClosed R<VAR>p : R[X]<VAR>h : p.Monic<VAR>hp : Irreducible p<VAR>a b : K[X]<VAR>H : Polynomial.map (algebraMap R K) p = a * b<VAR>hₐ : ¬IsUnit a<GOAL>IsUnit b
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsIntegrallyClosed R<VAR>p : R[X]<VAR>h : p.Monic<VAR>hp : Irreducible p<VAR>a b : K[X]<VAR>H : Polynomial.map (algebraMap R K) p = a * b<VAR>hₐ : ¬IsUnit a<VAR>a' : R[X]<VAR>ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a<GOAL>IsUnit b
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsIntegrallyClosed R<VAR>p : R[X]<VAR>h : p.Monic<VAR>hp : Irreducible p<VAR>a b : K[X]<VAR>H : Polynomial.map (algebraMap R K) p = a * b<VAR>hₐ : ¬IsUnit a<VAR>a' : R[X]<VAR>ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a<VAR>b' : R[X]<VAR>hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b<GOAL>IsUnit b
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsIntegrallyClosed R<VAR>p : R[X]<VAR>h : p.Monic<VAR>hp : Irreducible p<VAR>a b : K[X]<VAR>H : Polynomial.map (algebraMap R K) p = a * b<VAR>hₐ : ¬IsUnit a<VAR>a' : R[X]<VAR>ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a<VAR>b' : R[X]<VAR>hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b<VAR>this : a.leadingCoeff * b.leadingCoeff = 1<GOAL>IsUnit b
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsIntegrallyClosed R<VAR>p : R[X]<VAR>h : p.Monic<VAR>hp : Irreducible p<VAR>a b : K[X]<VAR>hₐ : ¬IsUnit a<VAR>a' : R[X]<VAR>ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a<VAR>b' : R[X]<VAR>H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')<VAR>hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b<VAR>this : a.leadingCoeff * b.leadingCoeff = 1<GOAL>IsUnit b
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsIntegrallyClosed R<VAR>p : R[X]<VAR>h : p.Monic<VAR>hp : Irreducible p<VAR>a b : K[X]<VAR>hₐ : ¬IsUnit a<VAR>a' : R[X]<VAR>ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a<VAR>b' : R[X]<VAR>H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')<VAR>hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b<VAR>this : a.leadingCoeff * b.leadingCoeff = 1<GOAL>IsUnit ((mapRingHom (algebraMap R K)) b' * C b.leadingCoeff)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsIntegrallyClosed R<VAR>p : R[X]<VAR>h : p.Monic<VAR>hp : Irreducible p<VAR>a b : K[X]<VAR>hₐ : ¬IsUnit a<VAR>a' : R[X]<VAR>ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a<VAR>b' : R[X]<VAR>H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')<VAR>hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b<VAR>this : a.leadingCoeff * b.leadingCoeff = 1<GOAL>p = a' * b'
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsIntegrallyClosed R<VAR>p : R[X]<VAR>h : p.Monic<VAR>hp : Irreducible p<VAR>a b : K[X]<VAR>hₐ : ¬IsUnit a<VAR>a' : R[X]<VAR>ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a<VAR>b' : R[X]<VAR>H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')<VAR>hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b<VAR>this : a.leadingCoeff * b.leadingCoeff = 1<GOAL>¬IsUnit a'
<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 x y : P<GOAL>(pointReflection R (midpoint R x y)) x = y
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : MonoidalPreadditive C<VAR>P Q R S : C<VAR>J : Type u_2<VAR>s : Finset J<VAR>f : P ⟶ Q<VAR>g : J → (R ⟶ S)<GOAL>(∑ j ∈ s, g j) ⊗ f = ∑ j ∈ s, g j ⊗ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → β ⊕ γ<VAR>g : α → β →. σ<VAR>h : α → γ →. σ<VAR>hf : Computable f<VAR>hg : Partrec₂ g<VAR>hh : Partrec₂ h<VAR>a : α<GOAL>(bif Sum.casesOn (f a) (fun b => true) fun b => false then Sum.casesOn (f a) (fun b => Part.map Option.some (g (a, b).1 (a, b).2)) fun c => Part.some Option.none else Sum.casesOn (f a) (fun b => Part.some Option.none) fun b => Part.map Option.some (h (a, b).1 (a, b).2)) = Part.map Option.some (Sum.casesOn (f a) (g a) (h a))
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝² : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsAffine Y<VAR>𝒰 : X.OpenCover<VAR>inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)<VAR>H : ∀ (i : 𝒰.J), Q (Scheme.Hom.app (𝒰.map i ≫ f) ⊤)<GOAL>P f
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝² : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsAffine Y<VAR>𝒰 : X.OpenCover<VAR>inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)<VAR>H : ∀ (i : 𝒰.J), Q (Scheme.Hom.app (𝒰.map i ≫ f) ⊤)<GOAL>sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => Q) f
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝² : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsAffine Y<VAR>𝒰 : X.OpenCover<VAR>inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)<VAR>H : ∀ (i : 𝒰.J), Q (Scheme.Hom.app (𝒰.map i ≫ f) ⊤)<VAR>U : ↑X.affineOpens<GOAL>Q (Scheme.Hom.appLE f ⊤ ↑U ⋯)
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝² : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsAffine Y<VAR>𝒰 : X.OpenCover<VAR>inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)<VAR>H : ∀ (i : 𝒰.J), Q (Scheme.Hom.app (𝒰.map i ≫ f) ⊤)<VAR>U : ↑X.affineOpens<VAR>S : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩<GOAL>Q (Scheme.Hom.appLE f ⊤ ↑U ⋯)
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>(l.rotate n).length = l.length
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝ : SFinite μ<VAR>h : μ μ.sigmaFiniteSetᶜ = 0<GOAL>SigmaFinite μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝ : SFinite μ<VAR>h : μ μ.sigmaFiniteSetᶜ = 0<GOAL>SigmaFinite (μ.restrict μ.sigmaFiniteSet)
<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✝² : CompleteSpace E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f✝ g : ℝ → E<VAR>μ : Measure ℝ<VAR>𝕜 : Type u_6<VAR>inst✝ : RCLike 𝕜<VAR>r : 𝕜<VAR>f : ℝ → 𝕜<GOAL>∫ (x : ℝ) in a..b, f x / r ∂μ = (∫ (x : ℝ) in a..b, f x ∂μ) / r
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℝ<VAR>x p : ℝ<VAR>hf : Tendsto f l (𝓝 x)<VAR>h : x ≠ 0 ∨ 0 ≤ p<VAR>h0 : 0 = p<GOAL>Tendsto (fun a => f a ^ 0) l (𝓝 (x ^ 0))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B X X' Y Y' Z : C<VAR>inst✝ : Closed A<GOAL>curry (𝟙 (A ⊗ (𝟭 C).obj X)) = (ihom.coev A).app X
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B X X' Y Y' Z : C<VAR>inst✝ : Closed A<GOAL>(ihom.coev A).app ((𝟭 C).obj X) ≫ 𝟙 ((ihom A).obj (A ⊗ (𝟭 C).obj X)) = (ihom.coev A).app X
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>p₁ p₂ p₃ p₄ : P<GOAL>dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ dist p₁ p₃ + dist p₂ p₄
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>p₁ p₂ p₃ p₄ : P<GOAL>‖p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)‖ ≤ ‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>inst✝ : IsBezout R<GOAL>IsBezout S
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>inst✝ : IsBezout R<GOAL>∀ (x y : S), Submodule.IsPrincipal (Ideal.span {x, y})
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>inst✝ : IsBezout R<VAR>x y : R<GOAL>Submodule.IsPrincipal (Ideal.span {f x, f y})
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>inst✝ : IsBezout R<VAR>x y : R<GOAL>Ideal.span {f x, f y} = Submodule.span S {f (gcd x y)}
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R✝<VAR>inst✝⁷ : AddCommMonoid M✝<VAR>inst✝⁶ : Module R✝ M✝<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R✝ N<VAR>R : Type u_6<VAR>M : Type u_7<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Finite R M<VAR>f : End R M<VAR>h : ∀ (m : M), ∃ n, (f ^ n) m = 0<GOAL>IsNilpotent f
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R✝<VAR>inst✝⁷ : AddCommMonoid M✝<VAR>inst✝⁶ : Module R✝ M✝<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R✝ N<VAR>R : Type u_6<VAR>M : Type u_7<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Finite R M<VAR>f : End R M<VAR>h : ∀ (m : M), ∃ n, (f ^ n) m = 0<VAR>S : Finset M<VAR>hS : span R ↑S = ⊤<GOAL>IsNilpotent f
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R✝<VAR>inst✝⁷ : AddCommMonoid M✝<VAR>inst✝⁶ : Module R✝ M✝<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R✝ N<VAR>R : Type u_6<VAR>M : Type u_7<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Finite R M<VAR>f : End R M<VAR>S : Finset M<VAR>hS : span R ↑S = ⊤<VAR>g : M → ℕ<VAR>hg : ∀ (m : M), (f ^ g m) m = 0<GOAL>IsNilpotent f
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R✝<VAR>inst✝⁷ : AddCommMonoid M✝<VAR>inst✝⁶ : Module R✝ M✝<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R✝ N<VAR>R : Type u_6<VAR>M : Type u_7<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Finite R M<VAR>f : End R M<VAR>S : Finset M<VAR>hS : span R ↑S = ⊤<VAR>g : M → ℕ<VAR>hg : ∀ (m : M), (f ^ g m) m = 0<GOAL>f ^ S.sup g = 0
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R✝<VAR>inst✝⁷ : AddCommMonoid M✝<VAR>inst✝⁶ : Module R✝ M✝<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R✝ N<VAR>R : Type u_6<VAR>M : Type u_7<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Finite R M<VAR>f : End R M<VAR>S : Finset M<VAR>hS : span R ↑S = ⊤<VAR>g : M → ℕ<VAR>hg : ∀ (m : M), (f ^ g m) m = 0<VAR>m : M<VAR>hm : m ∈ span R ↑S<GOAL>(f ^ S.sup g) m = 0 m
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R✝<VAR>inst✝⁷ : AddCommMonoid M✝<VAR>inst✝⁶ : Module R✝ M✝<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R✝ N<VAR>R : Type u_6<VAR>M : Type u_7<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Finite R M<VAR>f : End R M<VAR>S : Finset M<VAR>hS : span R ↑S = ⊤<VAR>g : M → ℕ<VAR>hg : ∀ (m : M), (f ^ g m) m = 0<VAR>m x✝ : M<VAR>h✝ : x✝ ∈ ↑S<GOAL>(f ^ S.sup g) x✝ = 0 x✝
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R✝<VAR>inst✝⁷ : AddCommMonoid M✝<VAR>inst✝⁶ : Module R✝ M✝<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R✝ N<VAR>R : Type u_6<VAR>M : Type u_7<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Finite R M<VAR>f : End R M<VAR>S : Finset M<VAR>hS : span R ↑S = ⊤<VAR>g : M → ℕ<VAR>hg : ∀ (m : M), (f ^ g m) m = 0<VAR>m : M<GOAL>(f ^ S.sup g) 0 = 0 0
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R✝<VAR>inst✝⁷ : AddCommMonoid M✝<VAR>inst✝⁶ : Module R✝ M✝<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R✝ N<VAR>R : Type u_6<VAR>M : Type u_7<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Finite R M<VAR>f : End R M<VAR>S : Finset M<VAR>hS : span R ↑S = ⊤<VAR>g : M → ℕ<VAR>hg : ∀ (m : M), (f ^ g m) m = 0<VAR>m x✝ : M<VAR>hx✝ : x✝ ∈ span R ↑S<VAR>y✝ : M<VAR>hy✝ : y✝ ∈ span R ↑S<VAR>a✝¹ : (f ^ S.sup g) x✝ = 0 x✝<VAR>a✝ : (f ^ S.sup g) y✝ = 0 y✝<GOAL>(f ^ S.sup g) (x✝ + y✝) = 0 (x✝ + y✝)
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R✝<VAR>inst✝⁷ : AddCommMonoid M✝<VAR>inst✝⁶ : Module R✝ M✝<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R✝ N<VAR>R : Type u_6<VAR>M : Type u_7<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Finite R M<VAR>f : End R M<VAR>S : Finset M<VAR>hS : span R ↑S = ⊤<VAR>g : M → ℕ<VAR>hg : ∀ (m : M), (f ^ g m) m = 0<VAR>m : M<VAR>a✝¹ : R<VAR>x✝ : M<VAR>hx✝ : x✝ ∈ span R ↑S<VAR>a✝ : (f ^ S.sup g) x✝ = 0 x✝<GOAL>(f ^ S.sup g) (a✝¹ • x✝) = 0 (a✝¹ • x✝)
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>n : ℕ<GOAL>(fun z => |z.im| ^ n) ≤ᶠ[l] fun z => Real.exp z.re
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν✝ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>β : Type u_5<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>g✝ : β → E<VAR>ν : Measure β<VAR>g : β →ₘ[ν] E<VAR>hf : MeasurePreserving f μ ν<GOAL>eLpNorm (↑(g.compMeasurePreserving f hf)) p μ = eLpNorm (↑g) p ν
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν✝ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>β : Type u_5<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>g✝ : β → E<VAR>ν : Measure β<VAR>g : β →ₘ[ν] E<VAR>hf : MeasurePreserving f μ ν<GOAL>eLpNorm (↑g ∘ f) p μ = eLpNorm (↑g) p ν