ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasPullbacks C<VAR>X Y : C<VAR>g : Y ⟶ X<VAR>inst✝ : Mono g<VAR>f₂ : Subobject Y<GOAL>∀ (f₁ : Subobject Y), (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map g).obj f₂
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasPullbacks C<VAR>X Y : C<VAR>g : Y ⟶ X<VAR>inst✝ : Mono g<VAR>f₂ : Subobject Y<GOAL>∀ (a : MonoOver Y), (map g).obj (Quotient.mk'' a ⊓ f₂) = (map g).obj (Quotient.mk'' a) ⊓ (map g).obj f₂
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasPullbacks C<VAR>X Y : C<VAR>g : Y ⟶ X<VAR>inst✝ : Mono g<VAR>f₂ : Subobject Y<VAR>f₁ : MonoOver Y<GOAL>(map g).obj (Quotient.mk'' f₁ ⊓ f₂) = (map g).obj (Quotient.mk'' f₁) ⊓ (map g).obj f₂
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasPullbacks C<VAR>X Y : C<VAR>g : Y ⟶ X<VAR>inst✝ : Mono g<VAR>f₂ : Subobject Y<VAR>f₁ : MonoOver Y<GOAL>(map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) = (map ((MonoOver.map g).obj f₁).arrow).obj ((pullback ((MonoOver.map g).obj f₁).arrow).obj ((map g).obj f₂))
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasPullbacks C<VAR>X Y : C<VAR>g : Y ⟶ X<VAR>inst✝ : Mono g<VAR>f₂ : Subobject Y<VAR>f₁ : MonoOver Y<GOAL>(map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) = (map (f₁.arrow ≫ g)).obj ((pullback (f₁.arrow ≫ g)).obj ((map g).obj f₂))
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>n : ℕ<VAR>F : L.Functions n<VAR>x : Fin n → Σˣ f<VAR>i j : ι<VAR>hi : i ∈ upperBounds (range (Sigma.fst ∘ x))<VAR>hj : j ∈ upperBounds (range (Sigma.fst ∘ x))<VAR>k : ι<VAR>ik : i ≤ k<VAR>jk : j ≤ k<GOAL>(f i k ik) (funMap F (unify f x i hi)) = (f j k jk) (funMap F (unify f x j hj))
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup L<VAR>inst✝¹² : Module R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : Fintype ι'<VAR>inst✝⁷ : Fintype ιM<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : DecidableEq ι'<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>b : Basis ι R L<VAR>inst✝² : Module.Finite R L<VAR>inst✝¹ : Module.Free R L<VAR>inst✝ : Nontrivial R<VAR>x : L<GOAL>φ.nilRank ≤ (charpoly (φ x)).natTrailingDegree
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup L<VAR>inst✝¹² : Module R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : Fintype ι'<VAR>inst✝⁷ : Fintype ιM<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : DecidableEq ι'<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>b : Basis ι R L<VAR>inst✝² : Module.Finite R L<VAR>inst✝¹ : Module.Free R L<VAR>inst✝ : Nontrivial R<VAR>x : L<GOAL>(φ.polyCharpoly (chooseBasis R L)).coeff (charpoly (φ x)).natTrailingDegree ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup L<VAR>inst✝¹² : Module R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : Fintype ι'<VAR>inst✝⁷ : Fintype ιM<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : DecidableEq ι'<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>b : Basis ι R L<VAR>inst✝² : Module.Finite R L<VAR>inst✝¹ : Module.Free R L<VAR>inst✝ : Nontrivial R<VAR>x : L<VAR>h : (MvPolynomial.eval ⇑((chooseBasis R L).repr x)) ((φ.polyCharpoly (chooseBasis R L)).coeff (charpoly (φ x)).natTrailingDegree) = (MvPolynomial.eval ⇑((chooseBasis R L).repr x)) 0<GOAL>False
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup L<VAR>inst✝¹² : Module R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : Fintype ι'<VAR>inst✝⁷ : Fintype ιM<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : DecidableEq ι'<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>b : Basis ι R L<VAR>inst✝² : Module.Finite R L<VAR>inst✝¹ : Module.Free R L<VAR>inst✝ : Nontrivial R<VAR>x : L<VAR>h : (charpoly (φ x)).coeff (charpoly (φ x)).natTrailingDegree = 0<GOAL>False
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup L<VAR>inst✝¹² : Module R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : Fintype ι'<VAR>inst✝⁷ : Fintype ιM<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : DecidableEq ι'<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>b : Basis ι R L<VAR>inst✝² : Module.Finite R L<VAR>inst✝¹ : Module.Free R L<VAR>inst✝ : Nontrivial R<VAR>x : L<VAR>h : (charpoly (φ x)).coeff (charpoly (φ x)).natTrailingDegree = 0<GOAL>charpoly (φ x) ≠ 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>y : M<VAR>hy : y ∈ f.source<GOAL>(f.extend I).target ∈ 𝓝[range ↑I] ↑(f.extend I) y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>y : M<VAR>hy : y ∈ f.source<GOAL>↑(f.extend I) '' (f.extend I).source ∈ map (↑(f.extend I)) (𝓝 y)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>f : R[X]<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>h : IsAdjoinRootMonic S f<VAR>hirr : Irreducible f<VAR>q : R[X]<VAR>hq : f = minpoly R h.root * q<GOAL>Associated f (minpoly R h.root)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>f : R[X]<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>h : IsAdjoinRootMonic S f<VAR>hirr : Irreducible f<VAR>q : R[X]<VAR>hq : f = minpoly R h.root * q<GOAL>minpoly R h.root = minpoly R h.root * 1
<VAR>x : Prop<VAR>p : x = x → Prop<VAR>h : ∀ (he : x ↔ x), p ⋯<GOAL>p ⋯
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t<VAR>hfs : ∀ t ∈ Ico a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t<VAR>hgs : ∀ t ∈ Ico a b, g t ∈ s t<VAR>ha : dist (f a) (g a) ≤ δ<GOAL>∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * rexp (↑K * (t - a))
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t<VAR>hfs : ∀ t ∈ Ico a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t<VAR>hgs : ∀ t ∈ Ico a b, g t ∈ s t<VAR>ha : dist (f a) (g a) ≤ δ<VAR>f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0<GOAL>∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * rexp (↑K * (t - a))
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t<VAR>hfs : ∀ t ∈ Ico a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t<VAR>hgs : ∀ t ∈ Ico a b, g t ∈ s t<VAR>ha : dist (f a) (g a) ≤ δ<VAR>f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0<VAR>g_bound : ∀ t ∈ Ico a b, dist (v t (g t)) (v t (g t)) ≤ 0<GOAL>∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * rexp (↑K * (t - a))
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t<VAR>hfs : ∀ t ∈ Ico a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t<VAR>hgs : ∀ t ∈ Ico a b, g t ∈ s t<VAR>ha : dist (f a) (g a) ≤ δ<VAR>f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0<VAR>g_bound : ∀ t ∈ Ico a b, dist (v t (g t)) (v t (g t)) ≤ 0<VAR>t : ℝ<VAR>ht : t ∈ Icc a b<GOAL>dist (f t) (g t) ≤ δ * rexp (↑K * (t - a))
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t<VAR>hfs : ∀ t ∈ Ico a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t<VAR>hgs : ∀ t ∈ Ico a b, g t ∈ s t<VAR>ha : dist (f a) (g a) ≤ δ<VAR>f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0<VAR>g_bound : ∀ t ∈ Ico a b, dist (v t (g t)) (v t (g t)) ≤ 0<VAR>t : ℝ<VAR>ht : t ∈ Icc a b<VAR>this : dist (f t) (g t) ≤ gronwallBound δ (↑K) (0 + 0) (t - a)<GOAL>dist (f t) (g t) ≤ δ * rexp (↑K * (t - a))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m✝ : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter β<VAR>m : α → β<VAR>hf : range m ∈ f<GOAL>map m (comap m f) = f
<VAR>z✝ : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z : ℂ<GOAL>normSq z = ‖z‖ ^ 2
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>σ : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>S : Subalgebra R A<VAR>x : σ → ↥S<VAR>p : MvPolynomial σ R<GOAL>(aeval fun i => ↑(x i)) p = ↑((aeval x) p)
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<GOAL>All P (l.node4R x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r
<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>g : α → ℝ≥0∞<VAR>hf_meas : ∀ (n : ℕ), Measurable (f n)<VAR>h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g<VAR>h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤<GOAL>⨅ n, ∫⁻ (a : α), ⨆ i, ⨆ (_ : i ≥ n), f i a ∂μ = ∫⁻ (a : α), ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), f i a ∂μ
<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>g : α → ℝ≥0∞<VAR>hf_meas : ∀ (n : ℕ), Measurable (f n)<VAR>h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g<VAR>h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤<GOAL>∀ (n : ℕ), Measurable fun a => ⨆ i, ⨆ (_ : i ≥ n), f i a
<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>g : α → ℝ≥0∞<VAR>hf_meas : ∀ (n : ℕ), Measurable (f n)<VAR>h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g<VAR>h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤<GOAL>Antitone fun n a => ⨆ i, ⨆ (_ : i ≥ n), f i a
<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>g : α → ℝ≥0∞<VAR>hf_meas : ∀ (n : ℕ), Measurable (f n)<VAR>h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g<VAR>h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤<GOAL>∫⁻ (a : α), ⨆ i, ⨆ (_ : i ≥ 0), f i a ∂μ ≠ ⊤
<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>g : α → ℝ≥0∞<VAR>hf_meas : ∀ (n : ℕ), Measurable (f n)<VAR>h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g<VAR>h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤<GOAL>∫⁻ (a : α), ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), f i a ∂μ = ∫⁻ (a : α), limsup (fun n => f n a) atTop ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>inst✝ : ∀ (i : ι), CompleteSpace (G i)<GOAL>LinearMap.range hV.linearIsometry.toLinearMap = (⨆ i, LinearMap.range (V i).toLinearMap).topologicalClosure
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>inst✝ : ∀ (i : ι), CompleteSpace (G i)<GOAL>LinearMap.range hV.linearIsometry.toLinearMap ≤ (⨆ i, LinearMap.range (V i).toLinearMap).topologicalClosure
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>inst✝ : ∀ (i : ι), CompleteSpace (G i)<GOAL>(⨆ i, LinearMap.range (V i).toLinearMap).topologicalClosure ≤ LinearMap.range hV.linearIsometry.toLinearMap
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : HasImage f<VAR>E : Epi f<GOAL>Epi (image.ι f)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : HasImage f<VAR>E : Epi (factorThruImage f ≫ image.ι f)<GOAL>Epi (image.ι f)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>v : V<VAR>n : ℕ<GOAL>‖fourierPowSMulRight L f v n‖ ≤ (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>v : V<VAR>n : ℕ<VAR>m : Fin n → W<GOAL>‖(fourierPowSMulRight L f v n) m‖ ≤ (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖ * ∏ i : Fin n, ‖m i‖
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>I : C<VAR>hI : IsInitial I<VAR>h : ∀ (X : C), Mono (hI.to X)<VAR>I' X : C<VAR>hI' : IsInitial I'<GOAL>Mono (hI'.to X)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>I : C<VAR>hI : IsInitial I<VAR>h : ∀ (X : C), Mono (hI.to X)<VAR>I' X : C<VAR>hI' : IsInitial I'<GOAL>Mono ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>a : α<GOAL>(condCDF ρ a).measure univ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>a : α<GOAL>(condCDF ρ a).measure univ = ENNReal.ofReal (1 - 0)
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹² : NormedRing A<VAR>inst✝¹¹ : NormedAlgebra ℂ A<VAR>inst✝¹⁰ : CompleteSpace A<VAR>inst✝⁹ : StarRing A<VAR>inst✝⁸ : CstarRing A<VAR>inst✝⁷ : NormedRing B<VAR>inst✝⁶ : NormedAlgebra ℂ B<VAR>inst✝⁵ : CompleteSpace B<VAR>inst✝⁴ : StarRing B<VAR>inst✝³ : CstarRing B<VAR>inst✝² : EquivLike F A B<VAR>inst✝¹ : NonUnitalAlgEquivClass F ℂ A B<VAR>inst✝ : StarAlgEquivClass F ℂ A B<VAR>φ : F<VAR>a : A<GOAL>‖a‖₊ ≤ ‖φ a‖₊
<VAR>a : ℝ<VAR>ha : a < -1<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>∫ (t : ℝ) in Ioi c, t ^ a = -c ^ (a + 1) / (a + 1)
<VAR>a : ℝ<VAR>ha : a < -1<VAR>c : ℝ<VAR>hc : 0 < c<VAR>hd : ∀ x ∈ Ici c, HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x<GOAL>∫ (t : ℝ) in Ioi c, t ^ a = -c ^ (a + 1) / (a + 1)
<VAR>a : ℝ<VAR>ha : a < -1<VAR>c : ℝ<VAR>hc : 0 < c<VAR>hd : ∀ x ∈ Ici c, HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x<VAR>ht : Tendsto (fun t => t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))<GOAL>∫ (t : ℝ) in Ioi c, t ^ a = -c ^ (a + 1) / (a + 1)
<VAR>a : ℝ<VAR>ha : a < -1<VAR>c : ℝ<VAR>hc : 0 < c<VAR>hd : ∀ x ∈ Ici c, HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x<VAR>ht : Tendsto (fun t => t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))<GOAL>-c ^ (a + 1) / (a + 1) = 0 / (a + 1) - c ^ (a + 1) / (a + 1)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>J : Type<VAR>inst✝¹ : Finite J<VAR>f : J → C<VAR>inst✝ : HasCoproduct f<GOAL>HasBiproduct f
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>J : Type<VAR>inst✝¹ : Finite J<VAR>f : J → C<VAR>inst✝ : HasCoproduct f<VAR>val✝ : Fintype J<GOAL>HasBiproduct f
<VAR>s : ℂ<VAR>hs : ∀ (m : ℕ), s ≠ -↑m<VAR>n : ℕ := ⌊1 - s.re⌋₊ + 1<GOAL>DifferentiableAt ℂ Gamma s
<VAR>s : ℂ<VAR>hs : ∀ (m : ℕ), s ≠ -↑m<VAR>n : ℕ := ⌊1 - s.re⌋₊ + 1<VAR>hn : 1 - s.re < ↑n<GOAL>DifferentiableAt ℂ Gamma s
<VAR>s : ℂ<VAR>hs : ∀ (m : ℕ), s ≠ -↑m<VAR>n : ℕ := ⌊1 - s.re⌋₊ + 1<VAR>hn : 1 - s.re < ↑n<GOAL>Gamma =ᶠ[𝓝 s] GammaAux n
<VAR>s : ℂ<VAR>hs : ∀ (m : ℕ), s ≠ -↑m<VAR>n : ℕ := ⌊1 - s.re⌋₊ + 1<VAR>hn : 1 - s.re < ↑n<VAR>S : Set ℂ := {t | 1 - t.re < ↑n}<GOAL>Gamma =ᶠ[𝓝 s] GammaAux n
<VAR>s : ℂ<VAR>hs : ∀ (m : ℕ), s ≠ -↑m<VAR>n : ℕ := ⌊1 - s.re⌋₊ + 1<VAR>hn : 1 - s.re < ↑n<VAR>S : Set ℂ := {t | 1 - t.re < ↑n}<VAR>this : S ∈ 𝓝 s<GOAL>Gamma =ᶠ[𝓝 s] GammaAux n
<VAR>s : ℂ<VAR>hs : ∀ (m : ℕ), s ≠ -↑m<VAR>n : ℕ := ⌊1 - s.re⌋₊ + 1<VAR>hn : 1 - s.re < ↑n<VAR>S : Set ℂ := {t | 1 - t.re < ↑n}<VAR>this : S ∈ 𝓝 s<GOAL>EqOn Gamma (GammaAux n) S
<VAR>s : ℂ<VAR>hs : ∀ (m : ℕ), s ≠ -↑m<VAR>n : ℕ := ⌊1 - s.re⌋₊ + 1<VAR>hn : 1 - s.re < ↑n<VAR>S : Set ℂ := {t | 1 - t.re < ↑n}<VAR>this : S ∈ 𝓝 s<VAR>t : ℂ<VAR>ht : t ∈ S<GOAL>Gamma t = GammaAux n t
<VAR>s : ℂ<VAR>hs : ∀ (m : ℕ), s ≠ -↑m<VAR>n : ℕ := ⌊1 - s.re⌋₊ + 1<VAR>hn : 1 - s.re < ↑n<VAR>S : Set ℂ := {t | 1 - t.re < ↑n}<VAR>this : S ∈ 𝓝 s<VAR>t : ℂ<VAR>ht : 1 - t.re < ↑n<GOAL>Gamma t = GammaAux n t
<VAR>s : ℂ<VAR>hs : ∀ (m : ℕ), s ≠ -↑m<VAR>n : ℕ := ⌊1 - s.re⌋₊ + 1<VAR>hn : 1 - s.re < ↑n<VAR>S : Set ℂ := {t | 1 - t.re < ↑n}<VAR>this : S ∈ 𝓝 s<VAR>t : ℂ<VAR>ht : 1 - t.re < ↑n<GOAL>-t.re < ↑n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : SMul 𝕜 E<VAR>s : Set E<VAR>f g : E → β<VAR>hf : QuasiconvexOn 𝕜 s f<VAR>r : β<VAR>x : E<VAR>hx : x ∈ {x | x ∈ s ∧ f x < r}<VAR>y : E<VAR>hy : y ∈ {x | x ∈ s ∧ f x < r}<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ {x | x ∈ s ∧ f x < r}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : SMul 𝕜 E<VAR>s : Set E<VAR>f g : E → β<VAR>hf : QuasiconvexOn 𝕜 s f<VAR>r : β<VAR>x : E<VAR>hx : x ∈ {x | x ∈ s ∧ f x < r}<VAR>y : E<VAR>hy : y ∈ {x | x ∈ s ∧ f x < r}<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>h : a • x + b • y ∈ {x_1 | x_1 ∈ s ∧ f x_1 ≤ max (f x) (f y)}<GOAL>a • x + b • y ∈ {x | x ∈ s ∧ f x < r}
<VAR>x y : PGame<VAR>ox : x.Numeric<VAR>oy : y.Numeric<GOAL>x < y ↔ (∃ i, (∀ (i' : x.LeftMoves), x.moveLeft i' < y.moveLeft i) ∧ ∀ (j : (y.moveLeft i).RightMoves), x < (y.moveLeft i).moveRight j) ∨ ∃ j, (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i < y) ∧ ∀ (j' : y.RightMoves), x.moveRight j < y.moveRight j'
<VAR>x y : PGame<VAR>ox : x.Numeric<VAR>oy : y.Numeric<GOAL>((∃ i, (∀ (i' : x.LeftMoves), x.moveLeft i' ⧏ y.moveLeft i) ∧ ∀ (j : (y.moveLeft i).RightMoves), x ⧏ (y.moveLeft i).moveRight j) ∨ ∃ j, (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i ⧏ y) ∧ ∀ (j' : y.RightMoves), x.moveRight j ⧏ y.moveRight j') ↔ (∃ i, (∀ (i' : x.LeftMoves), x.moveLeft i' < y.moveLeft i) ∧ ∀ (j : (y.moveLeft i).RightMoves), x < (y.moveLeft i).moveRight j) ∨ ∃ j, (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i < y) ∧ ∀ (j' : y.RightMoves), x.moveRight j < y.moveRight j'
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>hp0 : 0 ≤ p<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>hp0 : 0 ≤ p<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_zero : (fun x => f x ^ p) =ᶠ[ae μ] 0<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>hp0 : 0 ≤ p<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_zero : (fun x => f x ^ p) =ᶠ[ae μ] 0<VAR>x : α<GOAL>f x ^ p = 0 x → f x = 0 x
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>hp0 : 0 ≤ p<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_zero : (fun x => f x ^ p) =ᶠ[ae μ] 0<VAR>x : α<GOAL>¬f x = 0 → ¬f x ^ p = 0
<VAR>α : Type u_1<VAR>inst✝³ : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a✝ b✝ c d : α<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a - (a - b) = min a b
<VAR>q : ℚ<GOAL>sqrt (q * q) = |q|
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>r : R<VAR>i j : ℕ<VAR>h : i ≤ j<VAR>f_compat : (ZMod.castHom ⋯ (ZMod (p ^ i))).comp (f j) = f i<GOAL>↑p ^ i ∣ nthHom f r j - nthHom f r i
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>r : R<VAR>i j : ℕ<VAR>h : i ≤ j<VAR>f_compat : (ZMod.castHom ⋯ (ZMod (p ^ i))).comp (f j) = f i<GOAL>↑(nthHom f r j) - ↑(nthHom f r i) = 0