ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>X Y : R<VAR>h : Y ^ 2 + W.toAffine.a₁ * X * Y + W.toAffine.a₃ * Y = X ^ 3 + W.toAffine.a₂ * X ^ 2 + W.toAffine.a₄ * X + W.toAffine.a₆<VAR>hX : W.toAffine.a₁ * Y = 3 * X ^ 2 + 2 * W.toAffine.a₂ * X + W.toAffine.a₄<VAR>hY : Y = -Y - W.toAffine.a₁ * X - W.toAffine.a₃<GOAL>Y ^ 2 + W.a₁ * X * Y + 2 * W.a₃ * Y = W.a₂ * X ^ 2 + 2 * W.a₄ * X + 3 * W.a₆
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>B : FilterBasis α<VAR>this : Directed (fun x x_1 => x ≥ x_1) fun s => 𝓟 ↑s<VAR>U : Set α<GOAL>U ∈ B.filter ↔ U ∈ ⨅ s, 𝓟 ↑s
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype m'<VAR>inst✝⁵ : NonUnitalNonAssocSemiring α<VAR>inst✝⁴ : NonUnitalNonAssocSemiring β<VAR>inst✝³ : NonUnitalNonAssocSemiring γ<VAR>inst✝² : Module R α<VAR>inst✝¹ : Module R β<VAR>inst✝ : Module R γ<VAR>f : α →ₗ[R] β →ₗ[R] γ<VAR>h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'<VAR>A : Matrix l m α<VAR>B : Matrix m n α<VAR>A' : Matrix l' m' β<VAR>B' : Matrix m' n' β<VAR>i : l<VAR>i' : l'<VAR>j : n<VAR>j' : n'<GOAL>((kroneckerMapBilinear f) (A * B)) (A' * B') (i, i') (j, j') = (((kroneckerMapBilinear f) A) A' * ((kroneckerMapBilinear f) B) B') (i, i') (j, j')
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype m'<VAR>inst✝⁵ : NonUnitalNonAssocSemiring α<VAR>inst✝⁴ : NonUnitalNonAssocSemiring β<VAR>inst✝³ : NonUnitalNonAssocSemiring γ<VAR>inst✝² : Module R α<VAR>inst✝¹ : Module R β<VAR>inst✝ : Module R γ<VAR>f : α →ₗ[R] β →ₗ[R] γ<VAR>h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'<VAR>A : Matrix l m α<VAR>B : Matrix m n α<VAR>A' : Matrix l' m' β<VAR>B' : Matrix m' n' β<VAR>i : l<VAR>i' : l'<VAR>j : n<VAR>j' : n'<GOAL>(f (∑ j_1 : m, A i j_1 * B j_1 j)) (∑ j : m', A' i' j * B' j j') = ∑ x : m, ∑ x_1 : m', (f (A i x)) (A' i' x_1) * (f (B x j)) (B' x_1 j')
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : OrderedAddCommMonoid α<VAR>inst✝³ : OrderedAddCommMonoid β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : SMul 𝕜 β<VAR>f : F → β<VAR>s : Set F<VAR>hf : ConvexOn 𝕜 s f<VAR>g : E →ₗ[𝕜] F<VAR>x : E<VAR>hx : x ∈ ⇑g ⁻¹' s<VAR>y : E<VAR>hy : y ∈ ⇑g ⁻¹' s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>f (g (a • x + b • y)) = f (a • g x + b • g y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>inst✝² : Preorder ι<VAR>inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hm : Monotone s<GOAL>Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋃ n, s n)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>inst✝² : Preorder ι<VAR>inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hm : Monotone s<GOAL>Tendsto (⇑μ ∘ s) atTop (𝓝 (⨆ i, μ (s i)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<GOAL>∫⁻ (x : α) in s, 1 ∂μ = μ s
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>i : ℕ<VAR>h : i < l.length<GOAL>l[i]?.isSome = true
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>i : ℕ<VAR>h : i < l.length<GOAL>l[i] = l[i]?.get ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>ι' : Type v<VAR>f : ι → Ordinal.{max (max u v) w}<VAR>g : ι' → Ordinal.{max (max u v) w}<VAR>h : range f ⊆ range g<GOAL>range (succ ∘ f) ⊆ range (succ ∘ g)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>T : Set ℝ<VAR>hT : T ⊆ Ioi 0<VAR>hT' : MeasurableSet T<VAR>hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))<VAR>s : ℂ<GOAL>IntegrableOn (fun t => ↑t ^ (s - 1) • f t) T volume ↔ IntegrableOn (fun t => t ^ (s.re - 1) * ‖f t‖) T volume
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>T : Set ℝ<VAR>hT : T ⊆ Ioi 0<VAR>hT' : MeasurableSet T<VAR>hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))<VAR>s : ℂ<VAR>this : AEStronglyMeasurable (fun t => ↑t ^ (s - 1) • f t) (volume.restrict T)<GOAL>IntegrableOn (fun t => ↑t ^ (s - 1) • f t) T volume ↔ IntegrableOn (fun t => t ^ (s.re - 1) * ‖f t‖) T volume
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>T : Set ℝ<VAR>hT : T ⊆ Ioi 0<VAR>hT' : MeasurableSet T<VAR>hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))<VAR>s : ℂ<VAR>this : AEStronglyMeasurable (fun t => ↑t ^ (s - 1) • f t) (volume.restrict T)<GOAL>IntegrableOn (fun a => ‖↑a ^ (s - 1) • f a‖) T volume ↔ IntegrableOn (fun t => t ^ (s.re - 1) * ‖f t‖) T volume
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>T : Set ℝ<VAR>hT : T ⊆ Ioi 0<VAR>hT' : MeasurableSet T<VAR>hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))<VAR>s : ℂ<VAR>this : AEStronglyMeasurable (fun t => ↑t ^ (s - 1) • f t) (volume.restrict T)<VAR>t : ℝ<VAR>ht : t ∈ T<GOAL>‖↑t ^ (s - 1) • f t‖ = t ^ (s.re - 1) * ‖f t‖
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ : C ⥤ D<VAR>R₁ R₂ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>L R : C ⥤ C<VAR>adj : L ⊣ R<VAR>α : 𝟭 C ⟶ L<VAR>c : C<GOAL>𝟙 (R.obj c) ≫ (𝟙 (R.obj c) ≫ (𝟙 (R.obj c) ≫ α.app (R.obj c) ≫ 𝟙 (L.obj (R.obj c))) ≫ adj.counit.app c) ≫ 𝟙 c = α.app (R.obj c) ≫ adj.counit.app c
<VAR>x y : ℝ<VAR>h : x ≤ y<GOAL>√x ≤ √y
<VAR>x y : ℝ<VAR>h : x ≤ y<GOAL>x.toNNReal ≤ y.toNNReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>f : Fin 7 → β<GOAL>∏ i : Fin 7, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>f : Fin 7 → β<GOAL>f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (castSucc 5) * f (last 6) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : SeminormedAddCommGroup F<VAR>f : ι → E<VAR>g : ι → ℝ<VAR>hg : Summable g<VAR>h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i<GOAL>CauchySeq fun s => ∑ i ∈ s, f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : SeminormedAddCommGroup F<VAR>f : ι → E<VAR>g : ι → ℝ<VAR>hg : Summable g<VAR>h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : SeminormedAddCommGroup F<VAR>f : ι → E<VAR>g : ι → ℝ<VAR>hg : Summable g<VAR>h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>s : Finset ι<VAR>hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε<GOAL>∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε
<VAR>n : ℤ<VAR>d : ℕ<GOAL>n % ↑d = n - ↑d * ⌊↑n / ↑d⌋
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁✝ l₂✝ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>l₁ l₂ : List (Sigma β)<VAR>p : l₁ ~ l₂<VAR>l : List (Sigma β)<GOAL>l₁.kunion l ~ l₂.kunion l
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁸ : CommSemiring K<VAR>inst✝⁷ : CommSemiring L<VAR>inst✝⁶ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝⁵ : ExpChar K p<VAR>inst✝⁴ : ExpChar L p<VAR>inst✝³ : ExpChar M p<VAR>inst✝² : PerfectRing M p<VAR>inst✝¹ : IsPRadical i p<VAR>inst✝ : PerfectRing L p<VAR>x : L<GOAL>liftAux i i p x = x
<VAR>K : Type u_1<VAR>inst✝ : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>S : Finset Λ<VAR>q₁ q₂ : Stmt₂<VAR>h : q₁ ∈ stmts₁ q₂<VAR>hs : SupportsStmt S q₂<GOAL>SupportsStmt S q₁
<VAR>R : Type uR<VAR>inst✝³ : Semiring R<VAR>S : Type uS<VAR>inst✝² : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra S A<VAR>r : R → R → Prop<VAR>a : R<VAR>n : ℕ<GOAL>RingQuot.npow r n { toQuot := Quot.mk (Rel r) a } = { toQuot := Quot.mk (Rel r) (a ^ n) }
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ = x₂<VAR>hy : y₁ = W.negY x₂ y₂<GOAL>W.slope x₁ x₂ y₁ y₂ = 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>w w₁✝ w₂✝ : ι → k<VAR>p : ι → V<VAR>s : Finset V<VAR>hp : AffineIndependent k Subtype.val<VAR>w₁ w₂ : V → k<VAR>hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i<VAR>hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i<GOAL>∀ i ∈ s, w₁ i = w₂ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>f : β → σ<VAR>g : α → β<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>n : ℕ<GOAL>(Nat.casesOn (encode (decode n)) 0 fun n => encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) = encode (Option.map (fun a => f (g a)) (decode n))
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>ι : Type u_1<VAR>I : ι → Ideal R<GOAL>ker (Pi.ringHom fun i => Quotient.mk (I i)) = ⨅ i, I i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝⁶ : LinearOrder ι<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : OrderTopology ι<VAR>inst✝³ : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝² : SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>inst✝¹ : Filter.atTop.IsCountablyGenerated<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>hin : i ≤ n<GOAL>μ[f n|hτ.measurableSpace] =ᶠ[ae (μ.restrict {x | τ x = i})] f i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝⁶ : LinearOrder ι<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : OrderTopology ι<VAR>inst✝³ : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝² : SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>inst✝¹ : Filter.atTop.IsCountablyGenerated<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>hin : i ≤ n<GOAL>μ[f n|hτ.measurableSpace] =ᶠ[ae (μ.restrict {x | τ x = i})] μ[f n|↑ℱ i]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝⁶ : LinearOrder ι<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : OrderTopology ι<VAR>inst✝³ : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝² : SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>inst✝¹ : Filter.atTop.IsCountablyGenerated<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>hin : i ≤ n<VAR>t : Set Ω<GOAL>MeasurableSet ({x | τ x = i} ∩ t) ↔ MeasurableSet ({x | τ x = i} ∩ t)
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>∃ q, (of v).dens n = ↑q
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>a✝ b : ℚ<VAR>nth_cont_eq : (of v).conts n = Pair.map Rat.cast { a := a✝, b := b }<GOAL>∃ q, (of v).dens n = ↑q
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>a✝ b : ℚ<VAR>nth_cont_eq : (of v).conts n = Pair.map Rat.cast { a := a✝, b := b }<GOAL>(of v).dens n = ↑b
<VAR>a b : Ordinal.{u}<VAR>hb₁ : b ≠ 1<VAR>hb : Principal (fun x x_1 => x + x_1) b<GOAL>Principal (fun x x_1 => x + x_1) (a * b)
<VAR>b : Ordinal.{u}<VAR>hb₁ : b ≠ 1<VAR>hb : Principal (fun x x_1 => x + x_1) b<GOAL>Principal (fun x x_1 => x + x_1) (0 * b)
<VAR>a b : Ordinal.{u}<VAR>hb₁ : b ≠ 1<VAR>hb : Principal (fun x x_1 => x + x_1) b<VAR>h✝ : 0 < a<GOAL>Principal (fun x x_1 => x + x_1) (a * b)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₃<VAR>f g : E →SL[σ₁₂] F<VAR>h✝ : F →SL[σ₂₃] G<VAR>x✝ : E<VAR>h : ∃ x, ‖x‖ ≠ 0<VAR>x : E<VAR>hx : ‖x‖ ≠ 0<GOAL>1 ≤ ‖id 𝕜 E‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₃<VAR>f g : E →SL[σ₁₂] F<VAR>h✝ : F →SL[σ₂₃] G<VAR>x✝ : E<VAR>h : ∃ x, ‖x‖ ≠ 0<VAR>x : E<VAR>hx : ‖x‖ ≠ 0<VAR>this : ‖(id 𝕜 E) x‖ / ‖x‖ ≤ ‖id 𝕜 E‖<GOAL>1 ≤ ‖id 𝕜 E‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>k : ℕ∞<GOAL>k ≤ s.encard → ∃ t ⊆ s, t.encard = k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>k : ℕ∞<VAR>n : ℕ<VAR>IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n<VAR>hle : ↑n.succ ≤ s.encard<GOAL>∃ t ⊆ s, t.encard = ↑n.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>k : ℕ∞<GOAL>(∀ (n : ℕ), ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n) → ⊤ ≤ s.encard → ∃ t ⊆ s, t.encard = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>k : ℕ∞<GOAL>(∀ (n : ℕ), ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n) → s.Infinite → ∃ t ⊆ s, t.Infinite
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>Y Z : C<VAR>f : Z ⟶ Y<VAR>I : InjectiveResolution Y<VAR>J : InjectiveResolution Z<GOAL>J.cocomplex.d 0 1 ≫ descFOne f I J = descFZero f I J ≫ I.cocomplex.d 0 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>inst✝ : OmegaCompletePartialOrder α<VAR>c : Chain α<VAR>x : α<VAR>h : ∀ (i : ℕ), c i ≤ x ∨ x ≤ c i<VAR>this : ¬∀ (i : ℕ), c i ≤ x<GOAL>∃ i, ¬c i ≤ x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>inst✝ : OmegaCompletePartialOrder α<VAR>c : Chain α<VAR>x : α<VAR>h : ∀ (i : ℕ), c i ≤ x ∨ x ≤ c i<VAR>this : ∃ x_1, ¬c x_1 ≤ x<GOAL>∃ i, ¬c i ≤ x
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>f : E → H'<VAR>s : Set E<VAR>x : E<GOAL>ContDiffWithinAtProp 𝓘(𝕜, E) I' n f s x ↔ ContDiffWithinAt 𝕜 n (↑I' ∘ f) s x
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>r x y z : R<VAR>a b c : ℍ[R]<GOAL>normSq ↑x = x ^ 2
<VAR>ι : Type u_1<VAR>inst✝¹ : Finite ι<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>J : Box ι<VAR>x✝ : ↑J ≤ ⊤<VAR>π : Prepartition J<VAR>hπ : π.IsPartition<GOAL>∑ Ji ∈ π.boxes, (fun J => (μ ↑J).toReal) Ji = (fun J => (μ ↑J).toReal) J
<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>f : ↥(Lp β 1 μ)<GOAL>‖f‖ = (∫⁻ (a : α), ↑‖↑↑f a‖₊ ∂μ).toReal
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<GOAL>Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f✝ g✝ : ι → α<VAR>inst✝¹ : CommRing α<VAR>inst✝ : LinearOrder ι<VAR>s : Finset ι<VAR>f g : ι → α<GOAL>∏ i ∈ s, (f i - g i) = ∏ i ∈ s, f i - ∑ i ∈ s, (g i * ∏ j ∈ filter (fun x => x < i) s, (f j - g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f✝ g✝ : ι → α<VAR>inst✝¹ : CommRing α<VAR>inst✝ : LinearOrder ι<VAR>s : Finset ι<VAR>f g : ι → α<GOAL>∏ x ∈ s, (f x + -g x) = ∏ i ∈ s, f i + -∑ x ∈ s, (g x * ∏ x ∈ filter (fun x_1 => x_1 < x) s, (f x + -g x)) * ∏ i ∈ filter (fun j => x < j) s, f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f✝ g✝ : ι → α<VAR>inst✝¹ : CommRing α<VAR>inst✝ : LinearOrder ι<VAR>s : Finset ι<VAR>f g : ι → α<GOAL>-∑ x ∈ s, (g x * ∏ x ∈ filter (fun x_1 => x_1 < x) s, (f x + -g x)) * ∏ i ∈ filter (fun j => x < j) s, f i = ∑ i ∈ s, (-g i * ∏ j ∈ filter (fun x => x < i) s, (f j + -g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<GOAL>T_gen p F a > 0
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<GOAL>‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 > 0
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>f : M → E'<VAR>g : M → F'<VAR>hf : ContMDiffWithinAt I 𝓘(𝕜, E') n f s x<VAR>hg : ContMDiffWithinAt I 𝓘(𝕜, F') n g s x<GOAL>ContMDiffWithinAt I 𝓘(𝕜, E' × F') n (fun x => (f x, g x)) s x