ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>x✝ : α 0<VAR>q : (i : Fin (n + 1)) → α i<VAR>p✝ : (i : Fin n) → α i.succ<VAR>i✝ : Fin n<VAR>y : α i✝.succ<VAR>z : α 0<VAR>inst✝ : (i : Fin (n + 1)) → Preorder (α i)<VAR>i : Fin (n + 1)<VAR>x : α i<VAR>q₁ q₂ : (j : Fin (n + 1)) → α j<VAR>hx : x ∈ Icc (q₁ i) (q₂ i)<VAR>p : (j : Fin n) → α (i.succAbove j)<GOAL>p ∈ i.insertNth x ⁻¹' Icc q₁ q₂ ↔ p ∈ Icc (fun j => q₁ (i.succAbove j)) fun j => q₂ (i.succAbove j)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f : R[X]<VAR>n✝ : ℕ<GOAL>(coeff R n✝) (↑f).derivativeFun = (coeff R n✝) ↑(derivative f)
<VAR>I : Type u<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : I → Type v₁<VAR>g : I → Type v₂<VAR>h : I → Type v₃<VAR>x✝ y : (i : I) → f i<VAR>i✝ : I<VAR>α : Type u_4<VAR>inst✝² : DecidableEq I<VAR>inst✝¹ : Subsingleton I<VAR>inst✝ : One α<VAR>i : I<VAR>x : α<VAR>j : I<GOAL>Pi.mulSingle i x j = x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : CompleteSpace E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>a✝ b✝ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>a b : ℝ<VAR>φ : ℝ → F →L[𝕜] E<VAR>hφ : IntervalIntegrable φ μ a b<VAR>v : F<GOAL>(∫ (x : ℝ) in a..b, φ x ∂μ) v = ∫ (x : ℝ) in a..b, (φ x) v ∂μ
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝ : SMul G X<VAR>B : Set X<GOAL>IsBlock G B ↔ ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c a : G₀<GOAL>a / a * a = a
<VAR>α : Type u_1<VAR>p : α → Option α<VAR>l : List α<GOAL>replaceF p l = replaceFTR p l
<VAR>α : Type u_1<VAR>p : α → Option α<VAR>l : List α<GOAL>replaceF p l = replaceFTR.go p l #[]
<VAR>R : Type u_1<VAR>n✝ x y : ℕ<VAR>hyx : y < x<VAR>hxy : 2 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hneven : Even n<GOAL>padicValNat 2 (x ^ n - y ^ n) + 1 = padicValNat 2 (x + y) + padicValNat 2 (x - y) + padicValNat 2 n
<VAR>R : Type u_1<VAR>n✝ x y : ℕ<VAR>hyx : y < x<VAR>hxy : 2 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hneven : Even n<GOAL>↑(padicValNat 2 (x ^ n - y ^ n)) + ↑1 = ↑(padicValNat 2 (x + y)) + ↑(padicValNat 2 (x - y)) + ↑(padicValNat 2 n)
<VAR>R : Type u_1<VAR>n✝ x y : ℕ<VAR>hyx : y < x<VAR>hxy : 2 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hneven : Even n<GOAL>multiplicity 2 (x ^ n - y ^ n) + ↑1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 2 n
<VAR>R : Type u_1<VAR>n✝ x y : ℕ<VAR>hyx : y < x<VAR>hxy : 2 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hneven : Even n<GOAL>0 < n
<VAR>R : Type u_1<VAR>n✝ x y : ℕ<VAR>hyx : y < x<VAR>hxy : 2 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hneven : Even n<GOAL>0 < x - y
<VAR>R : Type u_1<VAR>n✝ x y : ℕ<VAR>hyx : y < x<VAR>hxy : 2 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hneven : Even n<GOAL>0 < x + y
<VAR>R : Type u_1<VAR>n✝ x y : ℕ<VAR>hyx : y < x<VAR>hxy : 2 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hneven : Even n<GOAL>0 < x ^ n - y ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u}<GOAL>o.bmex f < (succ o.card).ord
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u}<GOAL>o.bmex f < (succ #(Quotient.out o).α).ord
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<GOAL>Tendsto rexp atTop atTop
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>A : Tendsto (fun x => x + 1) atTop atTop<GOAL>Tendsto rexp atTop atTop
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>A : Tendsto (fun x => x + 1) atTop atTop<VAR>B : ∀ᶠ (x : ℝ) in atTop, x + 1 ≤ rexp x<GOAL>Tendsto rexp atTop atTop
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>f : (i : ι) → F' i<GOAL>HasFDerivAt (fun f => f i) (proj i) f
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>f : (i : ι) → F' i<GOAL>HasStrictFDerivAt (fun f => f i) (proj i) f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X : PresheafedSpace C<VAR>x : ↑↑X<GOAL>(stalkFunctor C x).map (𝟙 X).c ≫ stalkPushforward C (𝟙 ↑X) X.presheaf x = 𝟙 (X.presheaf.stalk x)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X : PresheafedSpace C<VAR>x : ↑↑X<GOAL>(stalkFunctor C x).map (𝟙 X).c ≫ (stalkFunctor C x).map (Pushforward.id X.presheaf).hom = 𝟙 (X.presheaf.stalk x)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X : PresheafedSpace C<VAR>x : ↑↑X<GOAL>(stalkFunctor C x).map ((𝟙 X).c ≫ (Pushforward.id X.presheaf).hom) = 𝟙 (X.presheaf.stalk x)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X : PresheafedSpace C<VAR>x : ↑↑X<VAR>e_1✝ : (X.presheaf.stalk x ⟶ X.presheaf.stalk x) = ((stalkFunctor C x).obj X.presheaf ⟶ (stalkFunctor C x).obj X.presheaf)<GOAL>(𝟙 X).c ≫ (Pushforward.id X.presheaf).hom = 𝟙 X.presheaf
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X : PresheafedSpace C<VAR>x : ↑↑X<VAR>e_1✝ : (X.presheaf.stalk x ⟶ X.presheaf.stalk x) = ((stalkFunctor C x).obj X.presheaf ⟶ (stalkFunctor C x).obj X.presheaf)<VAR>U✝ : Opens ↑↑X<GOAL>((𝟙 X).c ≫ (Pushforward.id X.presheaf).hom).app (op U✝) = (𝟙 X.presheaf).app (op U✝)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X : PresheafedSpace C<VAR>x : ↑↑X<VAR>e_1✝ : (X.presheaf.stalk x ⟶ X.presheaf.stalk x) = ((stalkFunctor C x).obj X.presheaf ⟶ (stalkFunctor C x).obj X.presheaf)<VAR>U✝ : Opens ↑↑X<GOAL>𝟙 (((pushforward C (𝟙 ↑X)).obj X.presheaf).obj (op U✝)) = (𝟙 X.presheaf).app (op U✝)
<VAR>a : Ordinal.{u_1}<VAR>ha : 0 < a<GOAL>nfp (fun x => a * x) 1 = a ^ ω
<VAR>a : Ordinal.{u_1}<VAR>ha : 0 < a<GOAL>(fun a_1 => sup fun n => (fun x => a * x)^[n] a_1) 1 = sup fun n => a ^ ↑n
<VAR>a : Ordinal.{u_1}<VAR>ha : 0 < a<GOAL>0 < a
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b z : ℝ<VAR>u v ua ub va vb : ι → ℝ<VAR>inst✝¹ : FTCFilter a la la'<VAR>inst✝ : FTCFilter b lb lb'<VAR>hab : IntervalIntegrable f volume a b<VAR>hmeas : StronglyMeasurableAtFilter f lb' volume<VAR>hf : Tendsto f (lb' ⊓ ae volume) (𝓝 c)<VAR>hu : Tendsto u lt lb<VAR>hv : Tendsto v lt lb<GOAL>(fun t => ((∫ (x : ℝ) in a..v t, f x) - ∫ (x : ℝ) in a..u t, f x) - (v t - u t) • c) =o[lt] (v - u)
<VAR>α : Type u_1<VAR>inst✝ : AddCommMonoid α<VAR>n : ℕ<VAR>x a k a' : α<VAR>h : a + k = a'<GOAL>term n x a + k = term n x a'
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<VAR>h : p.natDegree = 0<GOAL>p = 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<VAR>h : p.natDegree = 0<VAR>this : p = C (p.coeff 0)<GOAL>p = 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<VAR>h : p.natDegree = 0<VAR>this : p = C (p.coeff 0)<GOAL>C (p.coeff 0) = 1
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>s : Set E<VAR>w✝¹ : FormalMultilinearSeries 𝕜 E F<VAR>hf : HasFPowerSeriesWithinAt f w✝¹ s e<VAR>w✝ : FormalMultilinearSeries 𝕜 E G<VAR>hg : HasFPowerSeriesWithinAt g w✝ s e<GOAL>AnalyticWithinAt 𝕜 (fun x => (f x, g x)) s e
<VAR>o₁ e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ : ONote<VAR>h✝¹ : o₁ = e₁.oadd n₁ a₁<VAR>o₂ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>h✝ : o₂ = e₂.oadd n₂ a₂<VAR>h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF<VAR>h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF<GOAL>((e₁.cmp e₂).orElse ((_root_.cmp ↑n₁ ↑n₂).orElse (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹) (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)
<VAR>o₁ e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ : ONote<VAR>h✝¹ : o₁ = e₁.oadd n₁ a₁<VAR>o₂ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>h✝ : o₂ = e₂.oadd n₂ a₂<VAR>h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF<VAR>h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF<VAR>IHe : (e₁.cmp e₂).Compares e₁ e₂<GOAL>((e₁.cmp e₂).orElse ((_root_.cmp ↑n₁ ↑n₂).orElse (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹) (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)
<VAR>o₁ e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ : ONote<VAR>h✝¹ : o₁ = e₁.oadd n₁ a₁<VAR>o₂ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>h✝ : o₂ = e₂.oadd n₂ a₂<VAR>h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF<VAR>h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF<VAR>IHe : match e₁.cmp e₂, e₁, e₂ with | Ordering.lt, a, b => a < b | Ordering.eq, a, b => a = b | Ordering.gt, a, b => b < a<GOAL>((e₁.cmp e₂).orElse ((_root_.cmp ↑n₁ ↑n₂).orElse (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹) (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)
<VAR>o₁ e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ : ONote<VAR>h✝¹ : o₁ = e₁.oadd n₁ a₁<VAR>o₂ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>h✝ : o₂ = e₂.oadd n₂ a₂<VAR>h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF<VAR>h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF<GOAL>(match Ordering.lt, e₁, e₂ with | Ordering.lt, a, b => a < b | Ordering.eq, a, b => a = b | Ordering.gt, a, b => b < a) → (Ordering.lt.orElse ((_root_.cmp ↑n₁ ↑n₂).orElse (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹) (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)
<VAR>o₁ e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ : ONote<VAR>h✝¹ : o₁ = e₁.oadd n₁ a₁<VAR>o₂ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>h✝ : o₂ = e₂.oadd n₂ a₂<VAR>h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF<VAR>h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF<GOAL>(match Ordering.eq, e₁, e₂ with | Ordering.lt, a, b => a < b | Ordering.eq, a, b => a = b | Ordering.gt, a, b => b < a) → (Ordering.eq.orElse ((_root_.cmp ↑n₁ ↑n₂).orElse (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹) (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)
<VAR>o₁ e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ : ONote<VAR>h✝¹ : o₁ = e₁.oadd n₁ a₁<VAR>o₂ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>h✝ : o₂ = e₂.oadd n₂ a₂<VAR>h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF<VAR>h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF<GOAL>(match Ordering.gt, e₁, e₂ with | Ordering.lt, a, b => a < b | Ordering.eq, a, b => a = b | Ordering.gt, a, b => b < a) → (Ordering.gt.orElse ((_root_.cmp ↑n₁ ↑n₂).orElse (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹) (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.Ψ 1 = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>σ : Type u_4<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>S : Subsemigroup M<GOAL>↑(⊥.prod ⊥) = ↑⊥
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<GOAL>G.IsUniform ε {a} {b} ↔ 0 < ε
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>hε : 0 < ε<VAR>s' : Finset α<VAR>hs' : s' ⊆ {a}<VAR>t' : Finset α<VAR>ht' : t' ⊆ {b}<VAR>hs : ↑{a}.card * ε ≤ ↑s'.card<VAR>ht : ↑{b}.card * ε ≤ ↑t'.card<GOAL>|↑(G.edgeDensity s' t') - ↑(G.edgeDensity {a} {b})| < ε
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>hε : 0 < ε<VAR>s' : Finset α<VAR>hs' : s' ⊆ {a}<VAR>t' : Finset α<VAR>ht' : t' ⊆ {b}<VAR>hs : ε ≤ ↑s'.card<VAR>ht : ε ≤ ↑t'.card<GOAL>|↑(G.edgeDensity s' t') - ↑(G.edgeDensity {a} {b})| < ε
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>hε : 0 < ε<VAR>t' : Finset α<VAR>ht' : t' ⊆ {b}<VAR>ht : ε ≤ ↑t'.card<VAR>hs' : ∅ ⊆ {a}<VAR>hs : ε ≤ ↑∅.card<GOAL>|↑(G.edgeDensity ∅ t') - ↑(G.edgeDensity {a} {b})| < ε
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>hε : 0 < ε<VAR>t' : Finset α<VAR>ht' : t' ⊆ {b}<VAR>ht : ε ≤ ↑t'.card<VAR>hs' : {a} ⊆ {a}<VAR>hs : ε ≤ ↑{a}.card<GOAL>|↑(G.edgeDensity {a} t') - ↑(G.edgeDensity {a} {b})| < ε
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>hε : 0 < ε<VAR>hs' : {a} ⊆ {a}<VAR>hs : ε ≤ ↑{a}.card<VAR>ht' : ∅ ⊆ {b}<VAR>ht : ε ≤ ↑∅.card<GOAL>|↑(G.edgeDensity {a} ∅) - ↑(G.edgeDensity {a} {b})| < ε
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>hε : 0 < ε<VAR>hs' : {a} ⊆ {a}<VAR>hs : ε ≤ ↑{a}.card<VAR>ht' : {b} ⊆ {b}<VAR>ht : ε ≤ ↑{b}.card<GOAL>|↑(G.edgeDensity {a} {b}) - ↑(G.edgeDensity {a} {b})| < ε
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : MulZeroClass α<VAR>s✝ t s : Set α<GOAL>0 * s ⊆ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>as : Array α<VAR>bs : Array β<VAR>f : α → β → γ<GOAL>(as.zipWith bs f).size = min as.size bs.size
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>o : Part α<VAR>h : o.Dom<VAR>f : α → Part β<VAR>b : β<GOAL>b ∈ o.bind f ↔ b ∈ f (o.get h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>o : Part α<VAR>h : o.Dom<VAR>f : α → Part β<VAR>b : β<GOAL>(∃ a ∈ o, b ∈ f a) ↔ b ∈ f (o.get h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>o : Part α<VAR>h : o.Dom<VAR>f : α → Part β<VAR>b : β<GOAL>(∃ a ∈ o, b ∈ f a) → b ∈ f (o.get h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>o : Part α<VAR>h : o.Dom<VAR>f : α → Part β<VAR>b : β<VAR>a : α<VAR>ha : a ∈ o<VAR>hb : b ∈ f a<GOAL>b ∈ f (o.get h)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hg : DifferentiableOn 𝕜 f s<GOAL>DifferentiableOn 𝕜 (fun y => f y - g y) s ↔ DifferentiableOn 𝕜 g s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : Nontrivial R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalRing R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module R A<VAR>inst✝² : IsScalarTower R A A<VAR>inst✝¹ : SMulCommClass R A A<VAR>inst✝ : NonUnitalContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfcₙ (fun x => -x) a = -a
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Subgroup G<VAR>f g : (i : ι) → ↥(H i)<VAR>hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y<GOAL>(noncommPiCoprod hcomm).range = ⨆ i, H i
<VAR>m✝ n a✝ b✝ c✝ d a b c m : ℕ<VAR>hc : c ≠ 0<GOAL>a * c ≡ b * c [MOD m * c] → a ≡ b [MOD m]
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>R : F.M → F.M → Prop<VAR>inst✝ : Inhabited F.M<VAR>bisim : IsBisimulation R<VAR>ps : Path F<VAR>a : F.A<VAR>f : F.B a → F.M<VAR>a' : F.A<VAR>f' : F.B a' → F.M<VAR>h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)<VAR>hh : IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a', f'⟩)<GOAL>iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a', f'⟩) ∧ ∃ a_1 f_1 f'_1, isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧ isubtree ps (M.mk ⟨a', f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>R : F.M → F.M → Prop<VAR>inst✝ : Inhabited F.M<VAR>bisim : IsBisimulation R<VAR>ps : Path F<VAR>a : F.A<VAR>f f' : F.B a → F.M<VAR>h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)<VAR>hh : IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩)<GOAL>iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a, f'⟩) ∧ ∃ a_1 f_1 f'_1, isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧ isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>R : F.M → F.M → Prop<VAR>inst✝ : Inhabited F.M<VAR>bisim : IsBisimulation R<VAR>ps : List F.Idx<VAR>ps_ih : ∀ (a : F.A) (f f' : F.B a → F.M), R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) → IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) → iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a, f'⟩) ∧ ∃ a_1 f_1 f'_1, isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧ isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)<VAR>a : F.A<VAR>f f' : F.B a → F.M<VAR>h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)<VAR>a' : F.A<VAR>i : F.B a'<VAR>hh : IsPath (⟨a', i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a', i⟩ :: ps) (M.mk ⟨a, f'⟩)<GOAL>iselect (⟨a', i⟩ :: ps) (M.mk ⟨a, f⟩) = iselect (⟨a', i⟩ :: ps) (M.mk ⟨a, f'⟩) ∧ ∃ a_1 f_1 f'_1, isubtree (⟨a', i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧ isubtree (⟨a', i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>R : F.M → F.M → Prop<VAR>inst✝ : Inhabited F.M<VAR>bisim : IsBisimulation R<VAR>ps : List F.Idx<VAR>ps_ih : ∀ (a : F.A) (f f' : F.B a → F.M), R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) → IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) → iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a, f'⟩) ∧ ∃ a_1 f_1 f'_1, isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧ isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)<VAR>a : F.A<VAR>f f' : F.B a → F.M<VAR>h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)<VAR>i : F.B a<VAR>hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)<GOAL>iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) ∧ ∃ a_1 f_1 f'_1, isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧ isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>R : F.M → F.M → Prop<VAR>inst✝ : Inhabited F.M<VAR>bisim : IsBisimulation R<VAR>ps : List F.Idx<VAR>ps_ih : ∀ (a : F.A) (f f' : F.B a → F.M), R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) → IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) → (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧ ∃ a_1 f_1 f'_1, isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧ isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)<VAR>a : F.A<VAR>f f' : F.B a → F.M<VAR>h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)<VAR>i : F.B a<VAR>hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)<GOAL>(isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩)).head = (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)).head ∧ ∃ a_1 f_1 f'_1, isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧ isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>R : F.M → F.M → Prop<VAR>inst✝ : Inhabited F.M<VAR>bisim : IsBisimulation R<VAR>ps : List F.Idx<VAR>ps_ih : ∀ (a : F.A) (f f' : F.B a → F.M), R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) → IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) → (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧ ∃ a_1 f_1 f'_1, isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧ isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)<VAR>a : F.A<VAR>f f' : F.B a → F.M<VAR>h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)<VAR>i : F.B a<VAR>hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)<VAR>h₁ : R (f i) (f' i)<GOAL>(isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩)).head = (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)).head ∧ ∃ a_1 f_1 f'_1, isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧ isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>R : F.M → F.M → Prop<VAR>inst✝ : Inhabited F.M<VAR>bisim : IsBisimulation R<VAR>ps : List F.Idx<VAR>ps_ih : ∀ (a : F.A) (f f' : F.B a → F.M), R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) → IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) → (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧ ∃ a_1 f_1 f'_1, isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧ isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)<VAR>a : F.A<VAR>f f' : F.B a → F.M<VAR>h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)<VAR>i : F.B a<VAR>hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)<VAR>h₁ : R (f i) (f' i)<VAR>a₀ : F.A<VAR>f₀ : F.B a₀ → F.M<VAR>h : f i = M.mk ⟨a₀, f₀⟩<VAR>a₁ : F.A<VAR>f₁ : F.B a₁ → F.M<VAR>h' : f' i = M.mk ⟨a₁, f₁⟩<GOAL>(isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩)).head = (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)).head ∧ ∃ a_1 f_1 f'_1, isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧ isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)