ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>H : Type u_5<VAR>inst✝ : NormedAddCommGroup H<VAR>m0 : MeasurableSpace α<VAR>μ' : Measure α<VAR>f : α → H<VAR>hm : m ≤ m0<VAR>hf_meas_ae : AEStronglyMeasurable f (μ'.trim hm)<VAR>hf : HasFiniteIntegral f (μ'.trim hm)<GOAL>HasFiniteIntegral f μ'
<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>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>H : Type u_5<VAR>inst✝ : NormedAddCommGroup H<VAR>m0 : MeasurableSpace α<VAR>μ' : Measure α<VAR>f : α → H<VAR>hm : m ≤ m0<VAR>hf_meas_ae : AEStronglyMeasurable f (μ'.trim hm)<VAR>hf : ∫⁻ (a : α), ↑‖f a‖₊ ∂μ'.trim hm < ⊤<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ∂μ' < ⊤
<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>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>H : Type u_5<VAR>inst✝ : NormedAddCommGroup H<VAR>m0 : MeasurableSpace α<VAR>μ' : Measure α<VAR>f : α → H<VAR>hm : m ≤ m0<VAR>hf_meas_ae : AEStronglyMeasurable f (μ'.trim hm)<VAR>hf : ∫⁻ (a : α), ↑‖f a‖₊ ∂μ'.trim hm < ⊤<GOAL>AEMeasurable (fun a => ↑‖f a‖₊) (μ'.trim hm)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : RightHomologyMapData φ h₁ h₂<VAR>γ' : RightHomologyMapData φ' h₁ h₂<GOAL>rightHomologyMap' (φ + φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ + rightHomologyMap' φ' h₁ h₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>A : Set α<VAR>hA : MeasurableSet A<GOAL>∫⁻ (x : α) in A, f x ∂μ + ∫⁻ (x : α) in Aᶜ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>inst✝⁴ : AddMonoidWithOne α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : ZeroLEOneClass α<VAR>inst✝¹ : NeZero 1<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 < 3
<VAR>α : Type u_1<VAR>inst✝⁴ : AddMonoidWithOne α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : ZeroLEOneClass α<VAR>inst✝¹ : NeZero 1<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 < 2 + 1
<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.homologyπ j ≫ (K.homologyIsoSc' i j k hi hk).hom = (K.cyclesIsoSc' i j k hi hk).hom ≫ (K.sc' i j k).homologyπ
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p✝ q : α → Prop<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>p : α → Prop<GOAL>(p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b
<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>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>dist p₁ ((homothety p₁ c) p₂) = ‖c‖ * dist p₁ p₂
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>h : IsUnit A.det<GOAL>A * A⁻¹ = 1
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>h : IsUnit A.det<VAR>val✝ : Invertible A<GOAL>A * A⁻¹ = 1
<VAR>T : ℝ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hT : 0 < T<VAR>x : AddCircle T<GOAL>(fourier n) (x + ↑(T / 2 / ↑n)) = -(fourier n) x
<VAR>T : ℝ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hT : 0 < T<VAR>x : AddCircle T<GOAL>↑(n • x).toCircle * ↑(toCircle ↑(n • (T / 2 / ↑n))) = -(fourier n) x
<VAR>T : ℝ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hT : 0 < T<VAR>x : AddCircle T<VAR>this : ↑n ≠ 0<GOAL>↑(n • x).toCircle * ↑(toCircle ↑(n • (T / 2 / ↑n))) = -(fourier n) x
<VAR>T : ℝ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hT : 0 < T<VAR>x : AddCircle T<VAR>this✝ : ↑n ≠ 0<VAR>this : ↑(toCircle ↑(n • (T / 2 / ↑n))) = -1<GOAL>↑(n • x).toCircle * ↑(toCircle ↑(n • (T / 2 / ↑n))) = -(fourier n) x
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>i j : ι<VAR>h : c.Rel i j<GOAL>c.prev j = i
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>i j : ι<VAR>h : c.Rel i j<GOAL>c.Rel (c.prev j) j
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>i j : ι<VAR>h : c.Rel i j<GOAL>c.Rel ?hc.choose j
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>i j : ι<VAR>h : c.Rel i j<GOAL>∃ i, c.Rel i j
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>a : A<GOAL>IsNilpotent (mulLeft R a) ↔ IsNilpotent a
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_3<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : IsLocalization M S<VAR>a : R<VAR>m : ↥M<GOAL>C (IsLocalization.mk' S a m) = IsLocalization.mk' (MvPolynomial σ S) (C a) ⟨C ↑m, ⋯⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : BooleanAlgebra α<VAR>a b c d : α<GOAL>a ⇔ (a ⇔ b) = b
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁵ : Finite ι<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>v : ι → M<GOAL>Surjective ⇑((piEquiv ι R M) v) ↔ span R (range v) = ⊤
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a b : α<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>h : a ≠ b<VAR>h₁ : f a = 1<GOAL>multinomial {a, b} f = (f b).succ
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝ : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f g : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>hind : CompleteLattice.Independent fun i => (ϕ i).range<VAR>hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)<GOAL>Function.Injective ⇑(noncommPiCoprod ϕ hcomm)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α → β<VAR>x y z : α<VAR>s✝ : Set α<VAR>hf : Isometry f<VAR>s : Set α<VAR>d : ℝ≥0∞<GOAL>EMetric.diam (f '' s) ≤ d ↔ EMetric.diam s ≤ d
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β✝<VAR>inst✝² : TopologicalSpace β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : NormedSpace ℝ β<VAR>m : MeasurableSpace α<VAR>c : ℝ<VAR>hf : StronglyMeasurable f<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>x : α<GOAL>‖↑(hf.approxBounded c n) x‖ ≤ c
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β✝<VAR>inst✝² : TopologicalSpace β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : NormedSpace ℝ β<VAR>m : MeasurableSpace α<VAR>c : ℝ<VAR>hf : StronglyMeasurable f<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>x : α<GOAL>‖min 1 (c / ‖↑(hf.approx n) x‖) • ↑(hf.approx n) x‖ ≤ c
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β✝<VAR>inst✝² : TopologicalSpace β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : NormedSpace ℝ β<VAR>m : MeasurableSpace α<VAR>c : ℝ<VAR>hf : StronglyMeasurable f<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>x : α<GOAL>‖min 1 (c / ‖↑(hf.approx n) x‖)‖ * ‖↑(hf.approx n) x‖ ≤ c
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β✝<VAR>inst✝² : TopologicalSpace β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : NormedSpace ℝ β<VAR>m : MeasurableSpace α<VAR>c : ℝ<VAR>hf : StronglyMeasurable f<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>x : α<VAR>h0 : ¬‖↑(hf.approx n) x‖ = 0<GOAL>‖min 1 (c / ‖↑(hf.approx n) x‖)‖ * ‖↑(hf.approx n) x‖ ≤ c
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β✝<VAR>inst✝² : TopologicalSpace β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : NormedSpace ℝ β<VAR>m : MeasurableSpace α<VAR>c : ℝ<VAR>hf : StronglyMeasurable f<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>x : α<VAR>h0 : ¬‖↑(hf.approx n) x‖ = 0<VAR>h : ‖↑(hf.approx n) x‖ ≤ c<GOAL>‖min 1 (c / ‖↑(hf.approx n) x‖)‖ * ‖↑(hf.approx n) x‖ ≤ c
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β✝<VAR>inst✝² : TopologicalSpace β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : NormedSpace ℝ β<VAR>m : MeasurableSpace α<VAR>c : ℝ<VAR>hf : StronglyMeasurable f<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>x : α<VAR>h0 : ¬‖↑(hf.approx n) x‖ = 0<VAR>h : c ≤ ‖↑(hf.approx n) x‖<GOAL>‖min 1 (c / ‖↑(hf.approx n) x‖)‖ * ‖↑(hf.approx n) x‖ ≤ c
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s✝ t✝ : Set α<VAR>x : α<VAR>δ : ℝ<VAR>s t : Set α<GOAL>cthickening δ (s ∪ t) = cthickening δ s ∪ cthickening δ t
<VAR>x : ℝ<VAR>hx : x ≤ 0<VAR>y : ℂ<VAR>hlt : x < 0<GOAL>↑x ^ y = (-↑x) ^ y * cexp (↑π * I * y)
<VAR>x : ℝ<VAR>hx : x ≤ 0<VAR>y : ℂ<VAR>hlt : x < 0<VAR>hne : ↑x ≠ 0<GOAL>↑x ^ y = (-↑x) ^ y * cexp (↑π * I * y)
<VAR>α : Sort u_1<VAR>r p✝ q✝ : α → Prop<VAR>P Q : (x : α) → p✝ x → Prop<VAR>b : Prop<VAR>inst✝ : Nonempty α<VAR>p : α → Prop<VAR>q : Prop<GOAL>(∀ (x : α), p x ∧ q) ↔ (∀ (x : α), p x) ∧ q
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<GOAL>Submodule.LinearDisjoint 1 N
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<GOAL>Function.Injective ⇑(N.subtype ∘ₗ ↑N.lTensorOne)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>inst✝ : LinearOrder β<VAR>s : Set α<VAR>f : α → β<VAR>h1 : s.Finite<VAR>x : α<VAR>hx : x ∈ s<GOAL>∃ a ∈ s, ∀ b ∈ s, f a ≤ f b
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<VAR>s : Set α<GOAL>μ.toFiniteAux s = ∑' (n : ℕ), (2 ^ (n + 1) * (sFiniteSeq μ n) Set.univ)⁻¹ * (sFiniteSeq μ n) s
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<VAR>s : Set α<GOAL>∑' (i : ℕ), ((2 ^ (i + 1) * (sFiniteSeq μ i) Set.univ)⁻¹ • sFiniteSeq μ i) s = ∑' (n : ℕ), (2 ^ (n + 1) * (sFiniteSeq μ n) Set.univ)⁻¹ * (sFiniteSeq μ n) s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra.FinitePresentation R A<VAR>f : A →ₐ[R] S<VAR>hf : Function.Surjective ⇑f<VAR>t : Finset A<VAR>ht : Ideal.span ↑t = ⊤<VAR>H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))<GOAL>Algebra.FinitePresentation R S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra.FinitePresentation R A<VAR>f : A →ₐ[R] S<VAR>hf : Function.Surjective ⇑f<VAR>t : Finset A<VAR>ht : Ideal.span ↑t = ⊤<VAR>H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))<GOAL>(ker f.toRingHom).FG
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra.FinitePresentation R A<VAR>f : A →ₐ[R] S<VAR>hf : Function.Surjective ⇑f<VAR>t : Finset A<VAR>ht : Ideal.span ↑t = ⊤<VAR>H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))<GOAL>∀ (g : ↑↑t), (ker (Localization.awayMap f.toRingHom ↑g)).FG
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra.FinitePresentation R A<VAR>f : A →ₐ[R] S<VAR>hf : Function.Surjective ⇑f<VAR>t : Finset A<VAR>ht : Ideal.span ↑t = ⊤<VAR>H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))<VAR>g : ↑↑t<VAR>f' : Localization.Away ↑g →ₐ[R] Localization.Away (f ↑g) := Localization.awayMapₐ f ↑g<GOAL>(ker (Localization.awayMap f.toRingHom ↑g)).FG
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra.FinitePresentation R A<VAR>f : A →ₐ[R] S<VAR>hf : Function.Surjective ⇑f<VAR>t : Finset A<VAR>ht : Ideal.span ↑t = ⊤<VAR>H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))<VAR>g : ↑↑t<VAR>f' : Localization.Away ↑g →ₐ[R] Localization.Away (f ↑g) := Localization.awayMapₐ f ↑g<VAR>this : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away ↑g)<GOAL>(ker (Localization.awayMap f.toRingHom ↑g)).FG
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra.FinitePresentation R A<VAR>f : A →ₐ[R] S<VAR>hf : Function.Surjective ⇑f<VAR>t : Finset A<VAR>ht : Ideal.span ↑t = ⊤<VAR>H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))<VAR>g : ↑↑t<VAR>f' : Localization.Away ↑g →ₐ[R] Localization.Away (f ↑g) := Localization.awayMapₐ f ↑g<VAR>this : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away ↑g)<GOAL>Function.Surjective ⇑f'
<VAR>K : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : Field A<VAR>inst✝¹ : Algebra ℚ A<VAR>inst✝ : IsAlgClosed A<VAR>x : K<GOAL>(range fun φ => φ x) = (minpoly ℚ x).rootSet A
<VAR>K : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : Field A<VAR>inst✝¹ : Algebra ℚ A<VAR>inst✝ : IsAlgClosed A<VAR>x : K<GOAL>(range fun φ => φ x) = range fun ψ => ψ x
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f = ⊥<VAR>h' : limsup v f ≠ ⊤<GOAL>limsup (u + v) f = ⊥
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f = ⊥<VAR>h' : limsup v f ≠ ⊤<GOAL>limsup (u + v) f ≤ ⊥
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f = ⊥<VAR>h' : limsup v f ≠ ⊤<GOAL>∀ (z : ℝ), ⊥ < ↑z → limsup (u + v) f ≤ ↑z
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f = ⊥<VAR>h' : limsup v f ≠ ⊤<VAR>x : ℝ<GOAL>⊥ < ↑x → limsup (u + v) f ≤ ↑x
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f = ⊥<VAR>h' : limsup v f ≠ ⊤<VAR>x y : ℝ<VAR>hy : limsup v f < ↑y<VAR>right✝ : ↑y < ⊤<GOAL>⊥ < ↑x → limsup (u + v) f ≤ ↑x
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f = ⊥<VAR>h' : limsup v f ≠ ⊤<VAR>x y : ℝ<VAR>hy : limsup v f < ↑y<VAR>right✝ : ↑y < ⊤<GOAL>⊥ < ↑x - ↑y + ↑y → limsup (u + v) f ≤ ↑x - ↑y + ↑y
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f = ⊥<VAR>h' : limsup v f ≠ ⊤<VAR>x y : ℝ<VAR>hy : limsup v f < ↑y<VAR>right✝ : ↑y < ⊤<VAR>a✝ : ⊥ < ↑x - ↑y + ↑y<GOAL>limsup (u + v) f ≤ ↑x - ↑y + ↑y
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f = ⊥<VAR>h' : limsup v f ≠ ⊤<VAR>x y : ℝ<VAR>hy : limsup v f < ↑y<VAR>right✝ : ↑y < ⊤<VAR>a✝ : ⊥ < ↑x - ↑y + ↑y<GOAL>limsup u f < ↑x - ↑y
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : limsup u f = ⊥<VAR>h' : limsup v f ≠ ⊤<VAR>x y : ℝ<VAR>hy : limsup v f < ↑y<VAR>right✝ : ↑y < ⊤<VAR>a✝ : ⊥ < ↑x - ↑y + ↑y<GOAL>⊥ < ↑(x - y)
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal (MvPolynomial σ R)<VAR>p : MvPolynomial σ R<VAR>hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I<GOAL>p ∈ I
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal (MvPolynomial σ R)<VAR>p : MvPolynomial σ R<VAR>hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I<GOAL>∑ v ∈ p.support, (monomial v) (coeff v p) ∈ I
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal (MvPolynomial σ R)<VAR>p : MvPolynomial σ R<VAR>hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I<GOAL>∀ m ∈ p.support, (monomial m) (coeff m p) ∈ I
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal (MvPolynomial σ R)<VAR>p : MvPolynomial σ R<VAR>hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I<VAR>m : σ →₀ ℕ<VAR>a✝ : m ∈ p.support<GOAL>(monomial m) (coeff m p) ∈ I
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal (MvPolynomial σ R)<VAR>p : MvPolynomial σ R<VAR>hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I<VAR>m : σ →₀ ℕ<VAR>a✝ : m ∈ p.support<GOAL>C (coeff m p) * (monomial m) 1 ∈ I
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal (MvPolynomial σ R)<VAR>p : MvPolynomial σ R<VAR>hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I<VAR>m : σ →₀ ℕ<VAR>a✝ : m ∈ p.support<GOAL>C (coeff m p) ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g✝ : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>g : α → β<VAR>hf : TendstoLocallyUniformlyOn F f p s<VAR>hg : EqOn f g s<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>x : α<VAR>hx : x ∈ s<VAR>t : Set α<VAR>ht : t ∈ 𝓝[s] x<VAR>h : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u<GOAL>∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (g y, F n y) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g✝ : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>g : α → β<VAR>hf : TendstoLocallyUniformlyOn F f p s<VAR>hg : EqOn f g s<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>x : α<VAR>hx : x ∈ s<VAR>t : Set α<VAR>ht : t ∈ 𝓝[s] x<VAR>h : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u<GOAL>∀ᶠ (n : ι) in p, ∀ y ∈ s ∩ t, (g y, F n y) ∈ u
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.314058, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 4<VAR>app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯<VAR>w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄ = app₃ ≫ g.map' 3 4 ⋯ ⋯<GOAL>2 < 4 + 1
<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>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>h : Memℒp (fun x => ‖f x‖) p μ<GOAL>eLpNorm f 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>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>h : Memℒp (fun x => ‖f x‖) p μ<GOAL>eLpNorm (fun x => ‖f x‖) p μ < ⊤
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasStrictFDerivAt c c' x<VAR>hd : HasStrictFDerivAt d d' x<GOAL>HasStrictFDerivAt (fun y => c y * d y) (c x • d' + d x • c') x
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasStrictFDerivAt c c' x<VAR>hd : HasStrictFDerivAt d d' x<GOAL>d x • c' = c'.smulRight (d x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasStrictFDerivAt c c' x<VAR>hd : HasStrictFDerivAt d d' x<VAR>z : E<GOAL>(d x • c') z = (c'.smulRight (d x)) z
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>n : ℕ<VAR>fι : Fin n → ι<VAR>fA : (a : Fin n) → A (fι a)<GOAL>(List.ofFn fun a => (of A (fι a)) (fA a)).prod = (of A ((List.finRange n).dProdIndex fι)) ((List.finRange n).dProd fι fA)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : IsIrrefl α r<VAR>s' s : Multiset α<GOAL>CutExpand r s' s ↔ ∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : IsIrrefl α r<VAR>s' s : Multiset α<GOAL>(∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s' = (s + t).erase a) ↔ ∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t