ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>J : Type w<VAR>f : J → C<VAR>inst✝⁶ : HasProduct f<VAR>D : Type t<VAR>inst✝⁵ : Category.{r, t} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>F : C ⥤ D<VAR>inst✝³ : PreservesLimit (Discrete.functor f) F<VAR>inst✝² : HasProduct fun j => F.obj (f j)<VAR>inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)<VAR>inst✝ : PreservesLimit (Discrete.functor fun b => F.obj (f b)) (forget D)<VAR>x y : (forget D).obj (F.obj (∏ᶜ f))<VAR>h : ∀ (i : J), (F.map (Pi.π f i)) x = (F.map (Pi.π f i)) y<VAR>j : J<GOAL>((forget D).map (piComparison F f) ≫ (forget D).map (limit.π (Discrete.functor fun b => F.obj (f b)) { as := j })) x = ((forget D).map (piComparison F f) ≫ (forget D).map (limit.π (Discrete.functor fun b => F.obj (f b)) { as := j })) y
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>J : Type w<VAR>f : J → C<VAR>inst✝⁶ : HasProduct f<VAR>D : Type t<VAR>inst✝⁵ : Category.{r, t} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>F : C ⥤ D<VAR>inst✝³ : PreservesLimit (Discrete.functor f) F<VAR>inst✝² : HasProduct fun j => F.obj (f j)<VAR>inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)<VAR>inst✝ : PreservesLimit (Discrete.functor fun b => F.obj (f b)) (forget D)<VAR>x y : (forget D).obj (F.obj (∏ᶜ f))<VAR>h : ∀ (i : J), (F.map (Pi.π f i)) x = (F.map (Pi.π f i)) y<VAR>j : J<GOAL>(forget D).map (F.map (Pi.π f j)) x = (forget D).map (F.map (Pi.π f j)) y
<VAR>n m : ℕ<VAR>j : Fin n<VAR>i : Fin (n + 1)<VAR>hi : i ≠ 0<GOAL>j ≤ i.pred hi ↔ j.succ ≤ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f g : α → β<VAR>s✝ : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>x✝ : β<GOAL>x✝ ∈ image f s.toFinset ↔ x✝ ∈ (Multiset.map f s).toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α →ₘ[μ] β<VAR>g : α →ₘ[μ] γ<GOAL>f.pair g = mk (fun x => (↑f x, ↑g x)) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>μ : Measure α<VAR>r : ℝ≥0∞<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((r • μ).bind ⇑κ) s = (r • μ.bind ⇑κ) s
<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type (max u v)<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<GOAL>∃ ι x x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, DirectSum.IsInternal fun i => torsionBy R M (p i ^ e i)
<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type (max u v)<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<GOAL>Fintype { x // x ∈ (factors ⊤.annihilator).toFinset }
<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type (max u v)<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<GOAL>∀ (i : { x // x ∈ (factors ⊤.annihilator).toFinset }), Irreducible (IsPrincipal.generator ↑i)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>i : E →ₐ[F] K<VAR>x : E<GOAL>i x ∈ perfectClosure F K ↔ x ∈ perfectClosure F E
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>i : E →ₐ[F] K<VAR>x : E<GOAL>(∃ n, i x ^ ringExpChar F ^ n ∈ (algebraMap F K).range) ↔ ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>i : E →ₐ[F] K<VAR>x : E<VAR>x✝ : ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F E).range<VAR>n : ℕ<VAR>y : F<VAR>h : (algebraMap F E) y = x ^ ringExpChar F ^ n<GOAL>(algebraMap F K) y = i x ^ ringExpChar F ^ n
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>f✝ g✝ : Arrow C<VAR>inst✝³ : HasImage f✝.hom<VAR>inst✝² : HasImage g✝.hom<VAR>sq✝ : f✝ ⟶ g✝<VAR>f g : Arrow C<VAR>inst✝¹ : HasImage f.hom<VAR>inst✝ : HasImage g.hom<VAR>sq : f ⟶ g<VAR>F G : ImageMap sq<GOAL>F.map = G.map
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Mul G<VAR>a₁ a₂ : G<VAR>b₁ b₂ : k<GOAL>single a₁ b₁ * single a₂ b₂ = single (a₁ * a₂) (b₁ * b₂)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Mul G<VAR>a₁ a₂ : G<VAR>b₁ b₂ : k<GOAL>(sum (single a₁ b₁) fun a₁ b₁ => sum (single a₂ b₂) fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂)) = single (a₁ * a₂) (b₁ * b₂)
<VAR>z : ℂ<GOAL>HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) (sin z)
<VAR>z : ℂ<GOAL>HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) ((NormedSpace.exp ℂ (-z * I) - NormedSpace.exp ℂ (z * I)) * I / 2)
<VAR>z : ℂ<VAR>this : HasSum (fun i => ((-z * I) ^ i / ↑i ! - (z * I) ^ i / ↑i !) * I / 2) ((NormedSpace.exp ℂ (-z * I) - NormedSpace.exp ℂ (z * I)) * I / 2)<GOAL>HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) ((NormedSpace.exp ℂ (-z * I) - NormedSpace.exp ℂ (z * I)) * I / 2)
<VAR>z : ℂ<VAR>this : HasSum ((fun i => ((-z * I) ^ i / ↑i ! - (z * I) ^ i / ↑i !) * I / 2) ∘ ⇑(Nat.divModEquiv 2).symm) ((NormedSpace.exp ℂ (-z * I) - NormedSpace.exp ℂ (z * I)) * I / 2)<GOAL>HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) ((NormedSpace.exp ℂ (-z * I) - NormedSpace.exp ℂ (z * I)) * I / 2)
<VAR>z : ℂ<VAR>this : HasSum (fun x => ((-z * I) ^ (x.1 * 2 + ↑x.2) / ↑(x.1 * 2 + ↑x.2)! - (z * I) ^ (x.1 * 2 + ↑x.2) / ↑(x.1 * 2 + ↑x.2)!) * I / 2) ((NormedSpace.exp ℂ (-z * I) - NormedSpace.exp ℂ (z * I)) * I / 2)<GOAL>HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) ((NormedSpace.exp ℂ (-z * I) - NormedSpace.exp ℂ (z * I)) * I / 2)
<VAR>z : ℂ<VAR>this : HasSum (fun x => ((-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! - (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) * I / 2) ((NormedSpace.exp ℂ (-z * I) - NormedSpace.exp ℂ (z * I)) * I / 2)<GOAL>HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) ((NormedSpace.exp ℂ (-z * I) - NormedSpace.exp ℂ (z * I)) * I / 2)
<VAR>z : ℂ<VAR>this : HasSum (fun x => ((-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! - (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) * I / 2) ((NormedSpace.exp ℂ (-z * I) - NormedSpace.exp ℂ (z * I)) * I / 2)<VAR>k : ℕ<GOAL>HasSum (fun c => ((-z * I) ^ (2 * (k, c).1 + ↑(k, c).2) / ↑(2 * (k, c).1 + ↑(k, c).2)! - (z * I) ^ (2 * (k, c).1 + ↑(k, c).2) / ↑(2 * (k, c).1 + ↑(k, c).2)!) * I / 2) ((z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! / I)
<VAR>z : ℂ<VAR>this : HasSum (fun x => ((-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! - (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) * I / 2) ((NormedSpace.exp ℂ (-z * I) - NormedSpace.exp ℂ (z * I)) * I / 2)<VAR>k : ℕ<GOAL>HasSum (fun c => ((-z * I) ^ (2 * k + ↑c) / ↑(2 * k + ↑c)! - (z * I) ^ (2 * k + ↑c) / ↑(2 * k + ↑c)!) * I / 2) ((z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! / I)
<VAR>z : ℂ<VAR>this : HasSum (fun x => ((-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! - (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) * I / 2) ((NormedSpace.exp ℂ (-z * I) - NormedSpace.exp ℂ (z * I)) * I / 2)<VAR>k : ℕ<GOAL>(z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! / I = ∑ b : Fin 2, ((-z * I) ^ (2 * k + ↑b) / ↑(2 * k + ↑b)! - (z * I) ^ (2 * k + ↑b) / ↑(2 * k + ↑b)!) * I / 2
<VAR>z : ℂ<VAR>this : HasSum (fun x => ((-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! - (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) * I / 2) ((NormedSpace.exp ℂ (-z * I) - NormedSpace.exp ℂ (z * I)) * I / 2)<VAR>k : ℕ<GOAL>(z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! / I = ((-z * I) ^ (2 * k + ↑0) / ↑(2 * k + ↑0)! - (z * I) ^ (2 * k + ↑0) / ↑(2 * k + ↑0)!) * I / 2 + ((-z * I) ^ (2 * k + ↑1) / ↑(2 * k + ↑1)! - (z * I) ^ (2 * k + ↑1) / ↑(2 * k + ↑1)!) * I / 2
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : Module.Finite R L<VAR>x : L<VAR>D : LieDerivation R L L<VAR>hD : D ∈ __spread✝⁻⁰.carrier<GOAL>⁅x, D⁆ ∈ __spread✝⁻⁰.carrier
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : Module.Finite R L<VAR>x : L<VAR>D : LieDerivation R L L<VAR>hD : D ∈ __spread✝⁻⁰.carrier<VAR>this : (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule = (lieIdealSubalgebra R (LieDerivation R L L) (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule<GOAL>⁅x, D⁆ ∈ __spread✝⁻⁰.carrier
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : Module.Finite R L<VAR>x : L<VAR>D : LieDerivation R L L<VAR>this : (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule = (lieIdealSubalgebra R (LieDerivation R L L) (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule<VAR>hD : D ∈ (lieIdealSubalgebra R (LieDerivation R L L) (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule<GOAL>⁅x, D⁆ ∈ (lieIdealSubalgebra R (LieDerivation R L L) (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : Module.Finite R L<VAR>x : L<VAR>D : LieDerivation R L L<VAR>this : (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule = (lieIdealSubalgebra R (LieDerivation R L L) (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule<VAR>hD : D ∈ (lieIdealSubalgebra R (LieDerivation R L L) (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule<GOAL>⁅(ad R L) x, D⁆ ∈ (lieIdealSubalgebra R (LieDerivation R L L) (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ Z : Scheme<VAR>f✝ : X✝ ⟶ Z<VAR>g✝ : Y✝ ⟶ Z<VAR>H : IsOpenImmersion f✝<VAR>X Y U : Scheme<VAR>f : Y ⟶ U<VAR>g : U ⟶ X<VAR>h : IsOpenImmersion g<VAR>V : U.Opens<GOAL>Scheme.Hom.app f V = (Scheme.Hom.appIso g V).inv ≫ Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (eqToHom ⋯).op
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>j : Fin (n + 1)<VAR>op : α → α → α<VAR>g : Fin (n + 1) → α<VAR>k : Fin n<VAR>h : ↑k = ↑j<GOAL>j.contractNth op g k = op (g k.castSucc) (g k.succ)
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>j : Fin (n + 1)<VAR>op : α → α → α<VAR>g : Fin (n + 1) → α<VAR>k : Fin n<VAR>h : ↑k = ↑j<VAR>this : ¬↑k < ↑j<GOAL>j.contractNth op g k = op (g k.castSucc) (g k.succ)
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>f : α → ℝ<GOAL>((fun x => 1) =O[l] fun x => rexp (f x)) ↔ IsBoundedUnder (fun x x_1 => x ≥ x_1) l f
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>x : E<GOAL>-x ∈ p.ball 0 r ↔ x ∈ p.ball 0 r
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<VAR>x y : ℍ[R,c₁,c₂]<GOAL>q.lift (x + y) = q.lift x + q.lift y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<VAR>x y : ℍ[R,c₁,c₂]<GOAL>(algebraMap R A) x.re + (algebraMap R A) y.re + (x.imI • q.i + y.imI • q.i) + (x.imJ • q.j + y.imJ • q.j) + (x.imK • q.k + y.imK • q.k) = (algebraMap R A) x.re + x.imI • q.i + x.imJ • q.j + x.imK • q.k + ((algebraMap R A) y.re + y.imI • q.i + y.imJ • q.j + y.imK • q.k)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E p)<GOAL>0 ≤ ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E 0)<GOAL>0 ≤ ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E ⊤)<GOAL>0 ≤ ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E p)<VAR>hp : 0 < p.toReal<GOAL>0 ≤ ‖f‖
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>P : (α → ℝ≥0∞) → Prop<VAR>h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (s.indicator fun x => c)<VAR>h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)<VAR>h_iSup : ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ n, f n x<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>P f
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>P : (α → ℝ≥0∞) → Prop<VAR>h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (s.indicator fun x => c)<VAR>h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)<VAR>h_iSup : ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ n, f n x<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>f = fun x => ⨆ n, ↑(eapprox f n) x
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>P : (α → ℝ≥0∞) → Prop<VAR>h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (s.indicator fun x => c)<VAR>h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)<VAR>h_iSup : ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ n, f n x<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∀ (n : ℕ), P ↑(eapprox f n)
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>inst✝ : DivisionRing K<VAR>gp : Pair K<VAR>ppredA predA : K<VAR>succ_nth_s_eq : g.s.get? (n + 1) = some gp<VAR>nth_num_eq : g.nums n = ppredA<VAR>succ_nth_num_eq : g.nums (n + 1) = predA<GOAL>g.nums (n + 2) = gp.b * predA + gp.a * ppredA
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>inst✝ : DivisionRing K<VAR>gp : Pair K<VAR>predA : K<VAR>succ_nth_s_eq : g.s.get? (n + 1) = some gp<VAR>succ_nth_num_eq : g.nums (n + 1) = predA<VAR>ppredConts : Pair K<VAR>nth_conts_eq : g.conts n = ppredConts<VAR>nth_num_eq : g.nums n = ppredConts.a<GOAL>g.nums (n + 2) = gp.b * predA + gp.a * ppredConts.a
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>inst✝ : DivisionRing K<VAR>gp : Pair K<VAR>succ_nth_s_eq : g.s.get? (n + 1) = some gp<VAR>ppredConts : Pair K<VAR>nth_conts_eq : g.conts n = ppredConts<VAR>nth_num_eq : g.nums n = ppredConts.a<VAR>predConts : Pair K<VAR>succ_nth_conts_eq : g.conts (n + 1) = predConts<VAR>succ_nth_num_eq : g.nums (n + 1) = predConts.a<GOAL>g.nums (n + 2) = gp.b * predConts.a + gp.a * ppredConts.a
<VAR>c : Code<VAR>n x : ℕ<GOAL>x ∈ c.eval n ↔ x ∈ rfindOpt fun k => evaln k c n
<VAR>c : Code<VAR>n x : ℕ<GOAL>∀ {a m n_1 : ℕ}, m ≤ n_1 → a ∈ evaln m c n → a ∈ evaln n_1 c n
<VAR>c : Code<VAR>n✝ x a m n : ℕ<VAR>hl : m ≤ n<GOAL>a ∈ evaln m c n✝ → a ∈ evaln n c n✝
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>X Y Z : Dial C<VAR>F : X.Hom Y<VAR>G : Y.Hom Z<GOAL>(Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)).obj X.rel ≤ (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))).obj Z.rel
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : InitialMonoClass C<VAR>I X : C<VAR>hI : IsInitial I<VAR>f : I ⟶ X<GOAL>Mono f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : InitialMonoClass C<VAR>I X : C<VAR>hI : IsInitial I<VAR>f : I ⟶ X<GOAL>Mono (hI.to X)
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : TopologicalSpace L<VAR>inst✝² : TopologicalSpace X<VAR>ι : Type u_3<VAR>inst✝¹ : SemilatticeInf L<VAR>inst✝ : ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>t : Set X<VAR>x : X<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x<GOAL>ContinuousWithinAt (s.inf' hne f) t x
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y Y' : C<VAR>p : Y = Y'<VAR>f : X ⟶ Y<VAR>g : X ⟶ Y'<VAR>h : f = g ≫ eqToHom ⋯<GOAL>f ≫ eqToHom p = g
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>x : O<VAR>hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0<GOAL>preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) x) = v ((algebraMap O K) x)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>x : O<VAR>hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0<VAR>r : O<VAR>hr : r * ↑p = (Quotient.mk'' x).out' - x<GOAL>preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) x) = v ((algebraMap O K) x)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>x : O<VAR>hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0<VAR>r : O<VAR>hr : r * ↑p = (Quotient.mk'' x).out' - x<GOAL>¬v ((algebraMap O K) x) ≤ v ((algebraMap O K) (Quotient.out' ((Ideal.Quotient.mk (Ideal.span {↑p})) x)) - (algebraMap O K) x)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>x : O<VAR>hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0<VAR>r : O<VAR>hr : r * ↑p = (Quotient.mk'' x).out' - x<GOAL>¬r * ↑p ∣ x
<VAR>x y z : ℝ<GOAL>|0| < |x| ↔ x ≠ 0
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>hX : ¬Integrable (fun ω => rexp (t * X ω)) μ<GOAL>mgf X μ t = 0
<VAR>F : Type u_1<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : Module ℝ F<VAR>inst✝³ : TopologicalSpace F<VAR>E : Type u_2<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : TopologicalSpace E<VAR>s : Set E<VAR>h : AmpleSet s<VAR>L : E ≃ᵃL[ℝ] F<VAR>x : E<VAR>hx : x ∈ s<GOAL>⇑L '' (convexHull ℝ) (connectedComponentIn s x) = univ
<VAR>x✝ y x : ℝ≥0<GOAL>sqrt (x * x) = x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<GOAL>Set.range ⇑(pullback.fst f g ≫ f).val.base = Set.range ⇑f.val.base ∩ Set.range ⇑g.val.base
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Finset α<VAR>a b : α<GOAL>s ⊂ t ↔ ∃ a, ∃ (h : a ∉ s), cons a s h ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Finset α<VAR>a b : α<VAR>h : s ⊂ t<GOAL>∃ a, ∃ (h : a ∉ s), cons a s h ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Finset α<VAR>a✝ b : α<VAR>h : s ⊂ t<VAR>a : α<VAR>hs : a ∈ t<VAR>ht : a ∉ s<GOAL>∃ a, ∃ (h : a ∉ s), cons a s h ⊆ t
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<VAR>hs : s.Nontrivial<VAR>z : α<GOAL>∃ x ∈ s, x ≠ z
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<VAR>hs : s.Nontrivial<VAR>z : α<VAR>H : ∀ x ∈ s, x = z<GOAL>False
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L (fun n => χ ↑n) s * L ((fun n => χ ↑n) * fun n => ↑(μ n)) s = 1
<VAR>b x y : Ordinal.{u_1}<VAR>xy : x ≤ y<VAR>hx : x = 0<GOAL>log b x ≤ log b y
<VAR>b x y : Ordinal.{u_1}<VAR>xy : x ≤ y<VAR>hx : ¬x = 0<VAR>hb : ¬1 < b<GOAL>log b x ≤ log b y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>U R (n + 1) = X * U R n + T R (n + 1)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>inst✝ : ∀ (i : ι), Nonempty (α i)<GOAL>Filter.coprodᵢ f = ⊥ ↔ f = ⊥
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>h : IsOpen s<GOAL>(closure (s ∩ t))ᶜ ⊆ (s ∩ closure t)ᶜ
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h : IsPrimitiveRoot ζ✝ k<VAR>inst✝ : IsDomain R<VAR>n : ℕ<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ n<VAR>α a : R<VAR>e : α ^ n = a<GOAL>nthRoots n a = Multiset.map (fun x => ζ ^ x * α) (Multiset.range n)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h : IsPrimitiveRoot ζ✝ k<VAR>inst✝ : IsDomain R<VAR>ζ α a : R<VAR>hζ : IsPrimitiveRoot ζ 0<VAR>e : α ^ 0 = a<GOAL>nthRoots 0 a = Multiset.map (fun x => ζ ^ x * α) (Multiset.range 0)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h : IsPrimitiveRoot ζ✝ k<VAR>inst✝ : IsDomain R<VAR>n : ℕ<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ n<VAR>α a : R<VAR>e : α ^ n = a<VAR>hn : n > 0<GOAL>nthRoots n a = Multiset.map (fun x => ζ ^ x * α) (Multiset.range n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s t : Finset α<VAR>inst✝ : DecidableEq α<VAR>a : α<GOAL>s ⊆ {a}ᶜ ↔ a ∉ s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>p q r : R[X]<VAR>C : Type z<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>f : A ≃ₐ[R] B<VAR>g : B ≃ₐ[R] C<GOAL>(mapAlgEquiv f).trans (mapAlgEquiv g) = mapAlgEquiv (f.trans g)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>p q r : R[X]<VAR>C : Type z<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>f : A ≃ₐ[R] B<VAR>g : B ≃ₐ[R] C<GOAL>∀ (a : A[X]), ((mapAlgEquiv f).trans (mapAlgEquiv g)) a = (mapAlgEquiv (f.trans g)) a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>p q r : R[X]<VAR>C : Type z<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>f : A ≃ₐ[R] B<VAR>g : B ≃ₐ[R] C<VAR>x : A[X]<GOAL>((mapAlgEquiv f).trans (mapAlgEquiv g)) x = (mapAlgEquiv (f.trans g)) x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>p q r : R[X]<VAR>C : Type z<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>f : A ≃ₐ[R] B<VAR>g : B ≃ₐ[R] C<VAR>x : A[X]<GOAL>map ((↑g).comp ↑f) x = map (↑(f.trans g)) x
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>m : ι → OuterMeasure α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>(⨅ i, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)