ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>u : 𝕜 → E<VAR>v : 𝕜 → F<VAR>u' : E<VAR>v' : F<VAR>hu : HasDerivAt u u' x<VAR>hv : HasDerivAt v v' x<GOAL>HasDerivAt (fun x => (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>(f + g) ≫ h = f ≫ h + g ≫ h
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<VAR>x : α<VAR>hx : x ∈ rtakeWhile p l<GOAL>p x = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<VAR>x : α<VAR>hx : x ∈ takeWhile p l.reverse<GOAL>p x = true
<VAR>x : ℝ<VAR>hl : -(2 * π) ≤ x<VAR>hr : x ≤ 0<GOAL>sin (x / 2) = -√((1 - cos x) / 2)
<VAR>x : ℝ<VAR>hl : -(2 * π) ≤ x<VAR>hr : x ≤ 0<GOAL>sin (x / 2) ≤ 0
<VAR>x : ℝ≥0∞<VAR>hx_top : ¬x = ⊤<VAR>hx_zero : ¬x = 0<GOAL>x.log.exp = x
<VAR>x : ℝ≥0∞<VAR>hx_top : ¬x = ⊤<VAR>hx_zero : ¬x = 0<VAR>hx_pos : 0 < x.toReal<GOAL>x.log.exp = x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x m : M<GOAL>b.repr m ∈ Finsupp.supported R R ↑(b.repr m).support ∧ (Finsupp.total ι M R ⇑b) (b.repr m) = m
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsClosed s<VAR>hs' : BddBelow s<GOAL>IsClosed ↑(upperClosure s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsClosed s<VAR>hs' : BddBelow s<VAR>val✝ : Fintype ι<GOAL>IsClosed ↑(upperClosure s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x✝ y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsClosed s<VAR>hs' : BddBelow s<VAR>val✝ : Fintype ι<VAR>f : ℕ → ι → ℝ<VAR>x : ι → ℝ<VAR>hf : ∀ (n : ℕ), f n ∈ ↑(upperClosure s)<VAR>hx : Filter.Tendsto f Filter.atTop (nhds x)<GOAL>x ∈ ↑(upperClosure s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x✝ y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsClosed s<VAR>hs' : BddBelow s<VAR>val✝ : Fintype ι<VAR>f : ℕ → ι → ℝ<VAR>x : ι → ℝ<VAR>hx : Filter.Tendsto f Filter.atTop (nhds x)<VAR>g : ℕ → ι → ℝ<VAR>hg : ∀ (n : ℕ), g n ∈ s<VAR>hgf : ∀ (n : ℕ), g n ≤ f n<GOAL>x ∈ ↑(upperClosure s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x✝ y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsClosed s<VAR>hs' : BddBelow s<VAR>val✝ : Fintype ι<VAR>f : ℕ → ι → ℝ<VAR>x : ι → ℝ<VAR>hx : Filter.Tendsto f Filter.atTop (nhds x)<VAR>g : ℕ → ι → ℝ<VAR>hg : ∀ (n : ℕ), g n ∈ s<VAR>hgf : ∀ (n : ℕ), g n ≤ f n<VAR>a : ι → ℝ<VAR>ha : a ∈ upperBounds (range f)<GOAL>x ∈ ↑(upperClosure s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x✝ y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsClosed s<VAR>hs' : BddBelow s<VAR>val✝ : Fintype ι<VAR>f : ℕ → ι → ℝ<VAR>x : ι → ℝ<VAR>hx : Filter.Tendsto f Filter.atTop (nhds x)<VAR>g : ℕ → ι → ℝ<VAR>hg : ∀ (n : ℕ), g n ∈ s<VAR>hgf : ∀ (n : ℕ), g n ≤ f n<VAR>a : ι → ℝ<VAR>ha : a ∈ upperBounds (range f)<VAR>b : ι → ℝ<VAR>hb : b ∈ closure (s ∩ Iic a)<VAR>φ : ℕ → ℕ<VAR>hφ : StrictMono φ<VAR>hbf : Filter.Tendsto (g ∘ φ) Filter.atTop (nhds b)<GOAL>x ∈ ↑(upperClosure s)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b✝ c d a b n : α<VAR>a_nonneg : 0 ≤ a<VAR>a_le_n : a ≤ n<VAR>b_nonneg : 0 ≤ b<VAR>b_le_n : b ≤ n<GOAL>|a - b| ≤ n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b✝ c d a b n : α<VAR>a_nonneg : 0 ≤ a<VAR>a_le_n : a ≤ n<VAR>b_nonneg : 0 ≤ b<VAR>b_le_n : b ≤ n<GOAL>a ≤ n + b ∧ b ≤ n + a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : MetricSpace R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R A A<VAR>inst✝² : SMulCommClass R A A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>f : C(↑(σₙ R a), R)₀<VAR>f' : C(↑(σₙ R a), ↑(σₙ R ((cfcₙHom ha) f)))₀<VAR>hff' : ∀ (x : ↑(σₙ R a)), f x = ↑(f' x)<VAR>g : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀<VAR>ψ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] C(↑(σₙ R a), R)₀ := { toFun := fun x => x.comp f', map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }<VAR>φ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] A := (cfcₙHom ha).comp ψ<GOAL>(cfcₙHom ha) (g.comp f') = (cfcₙHom ⋯) g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : MetricSpace R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R A A<VAR>inst✝² : SMulCommClass R A A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>f : C(↑(σₙ R a), R)₀<VAR>f' : C(↑(σₙ R a), ↑(σₙ R ((cfcₙHom ha) f)))₀<VAR>hff' : ∀ (x : ↑(σₙ R a)), f x = ↑(f' x)<VAR>g : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀<VAR>ψ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] C(↑(σₙ R a), R)₀ := { toFun := fun x => x.comp f', map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }<VAR>φ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] A := (cfcₙHom ha).comp ψ<GOAL>cfcₙHom ⋯ = φ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : MetricSpace R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R A A<VAR>inst✝² : SMulCommClass R A A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>f : C(↑(σₙ R a), R)₀<VAR>f' : C(↑(σₙ R a), ↑(σₙ R ((cfcₙHom ha) f)))₀<VAR>hff' : ∀ (x : ↑(σₙ R a)), f x = ↑(f' x)<VAR>g : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀<VAR>ψ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] C(↑(σₙ R a), R)₀ := { toFun := fun x => x.comp f', map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }<VAR>φ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] A := (cfcₙHom ha).comp ψ<GOAL>Continuous ⇑φ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : MetricSpace R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R A A<VAR>inst✝² : SMulCommClass R A A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>f : C(↑(σₙ R a), R)₀<VAR>f' : C(↑(σₙ R a), ↑(σₙ R ((cfcₙHom ha) f)))₀<VAR>hff' : ∀ (x : ↑(σₙ R a)), f x = ↑(f' x)<VAR>g : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀<VAR>ψ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] C(↑(σₙ R a), R)₀ := { toFun := fun x => x.comp f', map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }<VAR>φ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] A := (cfcₙHom ha).comp ψ<GOAL>φ { toContinuousMap := ContinuousMap.restrict (σₙ R ((cfcₙHom ha) f)) (ContinuousMap.id R), map_zero' := ⋯ } = (cfcₙHom ha) f
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝⁷ : CommSemiring R'<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : (i : ι) → Semiring (A i)<VAR>inst✝⁴ : Algebra R' R<VAR>inst✝³ : (i : ι) → Algebra R (A i)<VAR>inst✝² : (i : ι) → Algebra R' (A i)<VAR>inst✝¹ : ∀ (i : ι), IsScalarTower R' R (A i)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<GOAL>(fun a => (tprod R) ((MonoidHom.mulSingle A i) a)) 1 = 1
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝⁷ : CommSemiring R'<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : (i : ι) → Semiring (A i)<VAR>inst✝⁴ : Algebra R' R<VAR>inst✝³ : (i : ι) → Algebra R (A i)<VAR>inst✝² : (i : ι) → Algebra R' (A i)<VAR>inst✝¹ : ∀ (i : ι), IsScalarTower R' R (A i)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<GOAL>(tprod R) 1 = 1
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝⁷ : CommSemiring R'<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : (i : ι) → Semiring (A i)<VAR>inst✝⁴ : Algebra R' R<VAR>inst✝³ : (i : ι) → Algebra R (A i)<VAR>inst✝² : (i : ι) → Algebra R' (A i)<VAR>inst✝¹ : ∀ (i : ι), IsScalarTower R' R (A i)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>r : R<GOAL>tprodCoeff R 1 ((MonoidHom.mulSingle A i) ((algebraMap R (A i)) r)) = r • tprodCoeff R 1 1
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝⁷ : CommSemiring R'<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : (i : ι) → Semiring (A i)<VAR>inst✝⁴ : Algebra R' R<VAR>inst✝³ : (i : ι) → Algebra R (A i)<VAR>inst✝² : (i : ι) → Algebra R' (A i)<VAR>inst✝¹ : ∀ (i : ι), IsScalarTower R' R (A i)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>r : R<GOAL>tprodCoeff R 1 ((MonoidHom.mulSingle A i) (r • 1)) = r • tprodCoeff R 1 1
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝⁷ : CommSemiring R'<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : (i : ι) → Semiring (A i)<VAR>inst✝⁴ : Algebra R' R<VAR>inst✝³ : (i : ι) → Algebra R (A i)<VAR>inst✝² : (i : ι) → Algebra R' (A i)<VAR>inst✝¹ : ∀ (i : ι), IsScalarTower R' R (A i)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>r : R<GOAL>tprodCoeff R (r • 1) 1 = r • tprodCoeff R 1 1
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C<VAR>hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x<VAR>l : IntegrationParams<GOAL>HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C<VAR>hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x<VAR>l : IntegrationParams<VAR>y : E<VAR>hy : HasIntegral I l f μ.toBoxAdditive.toSMul y<GOAL>HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C<VAR>hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x<VAR>l : IntegrationParams<VAR>y : E<VAR>hy : HasIntegral I l f μ.toBoxAdditive.toSMul y<GOAL>∫ (x : ι → ℝ) in ↑I, f x ∂μ = y
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C<VAR>hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x<VAR>l : IntegrationParams<VAR>y : E<VAR>hy : HasIntegral I l f μ.toBoxAdditive.toSMul y<GOAL>IntegrableOn f (↑I) μ
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<VAR>x : ℕ<VAR>h : p x<GOAL>∃ n < hf.toFinset.card, nth p n = x
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<GOAL>cgf X 0 t = 0
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x y : α<VAR>h : edist x y ≠ ⊤<VAR>this : edist x y ≤ edist x (f x) + edist y (f y) + ↑K * edist x y<GOAL>edist x y ≤ (edist x (f x) + edist y (f y)) / (1 - ↑K)
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x y : α<VAR>h : edist x y ≠ ⊤<GOAL>edist x (f x) + edist (f x) (f y) + edist (f y) y = edist x (f x) + edist y (f y) + edist (f x) (f y)
<VAR>R : Type u_1<VAR>K : Type ?u.12922<VAR>L : Type ?u.12925<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra K L<VAR>x : S<VAR>hx✝ : IsIntegral R x<VAR>hx : ¬IsIntegral R x<GOAL>map (algebraMap R S) (if hx : IsIntegral R x then ⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap R S) x x_1 = 0) hx else 0) /ₘ (X - C x) = 0
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>a • X ^ n = (monomial n) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>hX : Measurable X<VAR>hY : AEMeasurable Y μ<VAR>hf : AEStronglyMeasurable f (Measure.map (fun a => (X a, Y a)) μ)<VAR>hf_int : Integrable (fun a => f (X a, Y a)) μ<GOAL>Integrable f (Measure.map (fun a => (X a, Y a)) μ)
<VAR>m n : ℕ<GOAL>Even (m + n) ↔ (Even m ↔ Even n)
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a✝ : Nontrivial R<GOAL>(∑ i ∈ range n, X ^ i).Monic
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a✝ : Nontrivial R<GOAL>0 < X.natDegree
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<GOAL>num A 0 = 0
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>this : (algebraMap A K) (num A 0) / (algebraMap A K) ↑(den A 0) = 0<GOAL>num A 0 = 0
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>this : (algebraMap A K) (num A 0) = 0 ∨ (algebraMap A K) ↑(den A 0) = 0<GOAL>num A 0 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l l₁ : Filter α<VAR>l₂ : Filter β<VAR>f g : α → β<VAR>p : α → Prop<VAR>inst✝ : (x : α) → Decidable (p x)<VAR>h₀ : Tendsto f (l₁ ⊓ 𝓟 {x | p x}) l₂<VAR>h₁ : Tendsto g (l₁ ⊓ 𝓟 {x | ¬p x}) l₂<GOAL>Tendsto (fun x => if p x then f x else g x) l₁ l₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l l₁ : Filter α<VAR>l₂ : Filter β<VAR>f g : α → β<VAR>p : α → Prop<VAR>inst✝ : (x : α) → Decidable (p x)<VAR>h₀ : ∀ s ∈ l₂, {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁<VAR>h₁ : ∀ s ∈ l₂, {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁<GOAL>∀ s ∈ l₂, (fun x => if p x then f x else g x) ⁻¹' s ∈ l₁
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l l₁ : Filter α<VAR>l₂ : Filter β<VAR>f g : α → β<VAR>p : α → Prop<VAR>inst✝ : (x : α) → Decidable (p x)<VAR>h₀ : ∀ s ∈ l₂, {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁<VAR>h₁ : ∀ s ∈ l₂, {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁<VAR>s : Set β<VAR>hs : s ∈ l₂<GOAL>(fun x => if p x then f x else g x) ⁻¹' s ∈ l₁
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l l₁ : Filter α<VAR>l₂ : Filter β<VAR>f g : α → β<VAR>p : α → Prop<VAR>inst✝ : (x : α) → Decidable (p x)<VAR>h₀ : ∀ s ∈ l₂, {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁<VAR>h₁ : ∀ s ∈ l₂, {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁<VAR>s : Set β<VAR>hs : s ∈ l₂<VAR>x : α<VAR>hp₀ : p x → x ∈ f ⁻¹' s<VAR>hp₁ : ¬p x → x ∈ g ⁻¹' s<GOAL>x ∈ (fun x => if p x then f x else g x) ⁻¹' s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l l₁ : Filter α<VAR>l₂ : Filter β<VAR>f g : α → β<VAR>p : α → Prop<VAR>inst✝ : (x : α) → Decidable (p x)<VAR>h₀ : ∀ s ∈ l₂, {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁<VAR>h₁ : ∀ s ∈ l₂, {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁<VAR>s : Set β<VAR>hs : s ∈ l₂<VAR>x : α<VAR>hp₀ : p x → x ∈ f ⁻¹' s<VAR>hp₁ : ¬p x → x ∈ g ⁻¹' s<GOAL>(if p x then f x else g x) ∈ s
<VAR>a b : ℝ<VAR>nb ne : ℕ<VAR>pb : IsNat b nb<VAR>pe' : IsInt (a ^ nb) (Int.negOfNat ne)<GOAL>IsInt (a ^ b) (Int.negOfNat ne)
<VAR>x y : PGame<VAR>i : x.LeftMoves<VAR>j : y.LeftMoves<GOAL>x * y.moveLeft j = x * (- -y).moveLeft (toLeftMovesNeg (toRightMovesNeg j))
<VAR>x y : PGame<VAR>i : x.LeftMoves<VAR>j : y.LeftMoves<GOAL>y.moveLeft j = (- -y).moveLeft (toLeftMovesNeg (toRightMovesNeg j))
<VAR>n p : ℕ<VAR>pp : Prime p<VAR>m i : ℕ<GOAL>i ∣ p ^ m ↔ ∃ k ≤ m, i = p ^ k
<VAR>α : Type u_1<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ a b : α<GOAL>(a ⊔ b) / (a ⊓ b) = mabs (b / a)
<VAR>α : Type u_1<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ a b : α<GOAL>a / b ⊔ b / a ⊔ 1 = mabs (b / a)
<VAR>α : Type u_1<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ a b : α<GOAL>1 ≤ mabs (b / a)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>IsSquare (-1) ↔ p % 4 ≠ 3
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c✝ : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>c : F<GOAL>ContDiff 𝕜 n fun x => c
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c✝ : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>c : F<GOAL>ContDiff 𝕜 ⊤ fun x => c
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c✝ : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>c : F<GOAL>(Differentiable 𝕜 fun x => c) ∧ ContDiff 𝕜 ⊤ fun y => fderiv 𝕜 (fun x => c) y
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c✝ : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>c : F<GOAL>ContDiff 𝕜 ⊤ fun y => fderiv 𝕜 (fun x => c) y
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c✝ : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>c : F<GOAL>ContDiff 𝕜 ⊤ fun y => 0 y
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<VAR>h : Directed (fun x x_1 => x ≤ x_1) f<GOAL>Disjoint a (⨆ i, f i) ↔ ∀ (i : ι), Disjoint a (f i)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v✝ : V<VAR>f : G ≃g G'<VAR>v : V<VAR>w : ↑(G'.neighborSet (f v))<GOAL>f.symm ↑w ∈ G.neighborSet v
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>m✝ m' m : AddContent C<VAR>hC : IsSetRing C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>m s - m t ≤ m (s \ t)
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>m✝ m' m : AddContent C<VAR>hC : IsSetRing C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>m (s ∩ t ∪ s \ t) - m t ≤ m (s \ t)
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>m✝ m' m : AddContent C<VAR>hC : IsSetRing C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>m (s \ t) + m (s ∩ t) - m t ≤ m (s \ t)
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>m✝ m' m : AddContent C<VAR>hC : IsSetRing C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>m (s \ t) + (m (s ∩ t) - m t) = m (s \ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : Topology.IsLowerSet α<VAR>inst✝ : Topology.IsLowerSet β<VAR>f : α → β<GOAL>Monotone f ↔ Continuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : Topology.IsLowerSet α<VAR>inst✝ : Topology.IsLowerSet β<VAR>f : α → β<GOAL>Monotone (⇑toDual ∘ f ∘ ⇑ofDual) ↔ Continuous f
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<GOAL>cs.leftInvSeq ω.reverse = (cs.rightInvSeq ω).reverse