ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>μ✝ : K<VAR>h : minpoly K f ≠ 0<VAR>μ : K<GOAL>f.HasEigenvalue μ ↔ μ ∈ (minpoly K f).rootSet K
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>H : SimpleGraph V<VAR>hG : G.IsTuranMaximal r<VAR>hH : H.CliqueFree (r + 1)<GOAL>G ≤ H ↔ G = H
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Fintype ι<VAR>inst✝² : (i : ι) → Zero (β i)<VAR>inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝ : CommMonoid γ<VAR>v : Π₀ (i : ι), β i<VAR>f : (i : ι) → β i → γ<VAR>hf : ∀ (i : ι), f i 0 = 1<GOAL>∏ i ∈ v.support, f i (v i) = ∏ i : ι, f i (v i)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Fintype ι<VAR>inst✝² : (i : ι) → Zero (β i)<VAR>inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝ : CommMonoid γ<VAR>v : Π₀ (i : ι), β i<VAR>f : (i : ι) → β i → γ<VAR>hf : ∀ (i : ι), f i 0 = 1<GOAL>∀ x ∈ Finset.univ, x ∉ v.support → f x (v x) = 1
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Fintype ι<VAR>inst✝² : (i : ι) → Zero (β i)<VAR>inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝ : CommMonoid γ<VAR>v : Π₀ (i : ι), β i<VAR>f : (i : ι) → β i → γ<VAR>hf : ∀ (i : ι), f i 0 = 1<VAR>i : ι<VAR>a✝ : i ∈ Finset.univ<VAR>hi : i ∉ v.support<GOAL>f i (v i) = 1
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Fintype ι<VAR>inst✝² : (i : ι) → Zero (β i)<VAR>inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝ : CommMonoid γ<VAR>v : Π₀ (i : ι), β i<VAR>f : (i : ι) → β i → γ<VAR>hf : ∀ (i : ι), f i 0 = 1<VAR>i : ι<VAR>a✝ : i ∈ Finset.univ<VAR>hi : v i = 0<GOAL>f i (v i) = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra K F<VAR>ι : Type w<VAR>inst✝ : Algebra R F<VAR>pb : PowerBasis R S<VAR>hf : Splits (algebraMap R F) (minpoly R pb.gen)<GOAL>(algebraMap R F) ((norm R) pb.gen) = ((minpoly R pb.gen).aroots F).prod
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra K F<VAR>ι : Type w<VAR>inst✝ : Algebra R F<VAR>pb : PowerBasis R S<VAR>hf : Splits (algebraMap R F) (minpoly R pb.gen)<VAR>this : Nontrivial R<GOAL>(algebraMap R F) ((norm R) pb.gen) = ((minpoly R pb.gen).aroots F).prod
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra K F<VAR>ι : Type w<VAR>inst✝ : Algebra R F<VAR>pb : PowerBasis R S<VAR>hf : Splits (algebraMap R F) (minpoly R pb.gen)<VAR>this✝ : Nontrivial R<VAR>this : (minpoly R pb.gen).Monic<GOAL>(algebraMap R F) ((norm R) pb.gen) = ((minpoly R pb.gen).aroots F).prod
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra K F<VAR>ι : Type w<VAR>inst✝ : Algebra R F<VAR>pb : PowerBasis R S<VAR>hf : Splits (algebraMap R F) (minpoly R pb.gen)<VAR>this✝ : Nontrivial R<VAR>this : (minpoly R pb.gen).Monic<GOAL>((algebraMap R F) (-1) * -1) ^ (minpoly R pb.gen).natDegree * (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).roots.prod = ((minpoly R pb.gen).aroots F).prod
<VAR>a✝ b c a : ℕ<VAR>h : 0 < a<GOAL>Ico (a - 1) a = {a - 1}
<VAR>X : Scheme<VAR>U V : X.Opens<VAR>i : U = V<GOAL>X.presheaf.map (eqToHom i).op = eqToHom ⋯
<VAR>m : ℕ∞<VAR>n : ℕ<GOAL>↑m = ↑n ↔ m = ↑n
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>x y : ↑(π C fun x => x ∈ s)<VAR>h : y ≠ x<GOAL>(List.map (⇑(LocallyConstant.evalMonoidHom y)) (factors C s x)).prod = 0
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>x y : ↑(π C fun x => x ∈ s)<VAR>h : y ≠ x<GOAL>0 ∈ List.map (⇑(LocallyConstant.evalMonoidHom y)) (factors C s x)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>x y : ↑(π C fun x => x ∈ s)<VAR>h : y ≠ x<GOAL>∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>x y : ↑(π C fun x => x ∈ s)<VAR>h : y ≠ x<VAR>a : I<VAR>ha : ↑y a ≠ ↑x a<GOAL>∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_6<VAR>f : α → G<VAR>hf : HasFiniteIntegral f μ<VAR>l : Filter ι<VAR>s : ι → Set α<VAR>hs : Tendsto (⇑μ ∘ s) l (𝓝 0)<GOAL>Tendsto (fun i => ∫ (x : α) in s i, f x ∂μ) l (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_6<VAR>f : α → G<VAR>hf : HasFiniteIntegral f μ<VAR>l : Filter ι<VAR>s : ι → Set α<VAR>hs : Tendsto (⇑μ ∘ s) l (𝓝 0)<GOAL>Tendsto (fun x => ‖∫ (x : α) in s x, f x ∂μ‖) l (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_6<VAR>f : α → G<VAR>hf : HasFiniteIntegral f μ<VAR>l : Filter ι<VAR>s : ι → Set α<VAR>hs : Tendsto (⇑μ ∘ s) l (𝓝 0)<GOAL>Tendsto (fun a => ↑‖∫ (x : α) in s a, f x ∂μ‖₊) l (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeInf α<VAR>inst✝⁵ : BoundedOrder α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeInf β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>hs : a ∉ upperClosure ↑s<VAR>ht : a ∈ upperClosure ↑t<GOAL>(s ∪ t).truncatedInf a = t.truncatedInf a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>a b : α<GOAL>upperBounds ∅ = univ
<VAR>m : ℤ<VAR>n : ℕ<VAR>ihn : 0 ≤ ∏ k ∈ Finset.range (n + n), (m - ↑k)<GOAL>0 ≤ ∏ k ∈ Finset.range (n + 1 + (n + 1)), (m - ↑k)
<VAR>m : ℤ<VAR>n : ℕ<VAR>ihn : 0 ≤ ∏ k ∈ Finset.range (2 * n), (m - ↑k)<GOAL>0 ≤ ∏ k ∈ Finset.range (n + 1 + (n + 1)), (m - ↑k)
<VAR>m : ℤ<VAR>n : ℕ<VAR>ihn : 0 ≤ ∏ k ∈ Finset.range (2 * n), (m - ↑k)<GOAL>0 ≤ (∏ x ∈ Finset.range ((1 + 1) * n), (m - ↑x)) * ((m - ↑((1 + 1) * n)) * (m - ↑((1 + 1) * n + 1)))
<VAR>m : ℤ<VAR>n : ℕ<VAR>ihn : 0 ≤ ∏ k ∈ Finset.range (2 * n), (m - ↑k)<VAR>k : ℕ<GOAL>0 ≤ (m - ↑k) * (m - ↑(k + 1))
<VAR>m : ℤ<VAR>n : ℕ<VAR>ihn : 0 ≤ ∏ k ∈ Finset.range (2 * n), (m - ↑k)<VAR>k : ℕ<VAR>hmk : m ≤ ↑k<GOAL>0 ≤ (m - ↑k) * (m - ↑(k + 1))
<VAR>m : ℤ<VAR>n : ℕ<VAR>ihn : 0 ≤ ∏ k ∈ Finset.range (2 * n), (m - ↑k)<VAR>k : ℕ<VAR>hmk : ↑k < m<GOAL>0 ≤ (m - ↑k) * (m - ↑(k + 1))
<VAR>F : 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>β : Type u_8<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>t : α → Finset β<VAR>a✝ : β<GOAL>a✝ ∈ s.sup t ↔ a✝ ∈ s.biUnion t
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f : α → α<VAR>h : id ≤ f<VAR>n : ℕ<VAR>x : α<GOAL>f^[n] x ≤ f^[n + 1] x
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f : α → α<VAR>h : id ≤ f<VAR>n : ℕ<VAR>x : α<GOAL>f^[n] x ≤ f (f^[n] x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>s : Set α<VAR>hs : s.Finite<GOAL>s ∩ mulSupport f = ↑hs.toFinset ∩ mulSupport f
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>ι : Type v<VAR>inst✝⁶ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : (i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>P : Type u₁<VAR>inst✝³ : AddCommGroup P<VAR>g✝ : (i : ι) → G i →+ P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) ((f i j hij) x) = (g✝ i) x<VAR>G' : ι → Type v'<VAR>inst✝² : (i : ι) → AddCommGroup (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →+ G' j<VAR>G'' : ι → Type v''<VAR>inst✝¹ : (i : ι) → AddCommGroup (G'' i)<VAR>f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>e : (i : ι) → G i ≃+ G' i<VAR>he : ∀ (i j : ι) (h : i ≤ j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp ↑(e i)<VAR>i : ι<VAR>g : G' i<GOAL>(congr e he).symm ((of G' f' i) g) = (of G f i) ((e i).symm g)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>hF : F.Final<VAR>hFG : (F ⋙ G).Final<VAR>s₁ : C ≌ AsSmall C := AsSmall.equiv<VAR>s₂ : D ≌ AsSmall D := AsSmall.equiv<VAR>s₃ : E ≌ AsSmall E := AsSmall.equiv<VAR>_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor := isoWhiskerLeft (s₁.inverse ⋙ F) (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))<GOAL>G.Final
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>hF : F.Final<VAR>hFG : (F ⋙ G).Final<VAR>s₁ : C ≌ AsSmall C := AsSmall.equiv<VAR>s₂ : D ≌ AsSmall D := AsSmall.equiv<VAR>s₃ : E ≌ AsSmall E := AsSmall.equiv<VAR>_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor := isoWhiskerLeft (s₁.inverse ⋙ F) (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))<GOAL>∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)), IsIso (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>hFG : (F ⋙ G).Final<VAR>s₁ : C ≌ AsSmall C := AsSmall.equiv<VAR>s₂ : D ≌ AsSmall D := AsSmall.equiv<VAR>hF : ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)), IsIso (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))<VAR>s₃ : E ≌ AsSmall E := AsSmall.equiv<VAR>_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor := isoWhiskerLeft (s₁.inverse ⋙ F) (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))<GOAL>∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)), IsIso (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>s₁ : C ≌ AsSmall C := AsSmall.equiv<VAR>s₂ : D ≌ AsSmall D := AsSmall.equiv<VAR>hF : ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)), IsIso (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))<VAR>s₃ : E ≌ AsSmall E := AsSmall.equiv<VAR>hFG : ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)), IsIso (colimit.pre G_1 ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor))<VAR>_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor := isoWhiskerLeft (s₁.inverse ⋙ F) (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))<GOAL>∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)), IsIso (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>s₁ : C ≌ AsSmall C := AsSmall.equiv<VAR>s₂ : D ≌ AsSmall D := AsSmall.equiv<VAR>hF : ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)), IsIso (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))<VAR>s₃ : E ≌ AsSmall E := AsSmall.equiv<VAR>_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor := isoWhiskerLeft (s₁.inverse ⋙ F) (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))<VAR>H : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)<VAR>hFG : IsIso (colimit.pre H ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor))<GOAL>IsIso (colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>s₁ : C ≌ AsSmall C := AsSmall.equiv<VAR>s₂ : D ≌ AsSmall D := AsSmall.equiv<VAR>hF : ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)), IsIso (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))<VAR>s₃ : E ≌ AsSmall E := AsSmall.equiv<VAR>_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor := isoWhiskerLeft (s₁.inverse ⋙ F) (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))<VAR>H : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)<VAR>hFG : IsIso (colimit.pre ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H) (s₁.inverse ⋙ F ⋙ s₂.functor) ≫ colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor))<GOAL>IsIso (colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor))
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>A : AlgebraCat R<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (Algebra.linearMap R ↑A) (of R ↑A) ≫ mul' R ↑A = (CategoryTheory.MonoidalCategory.leftUnitor (of R ↑A)).hom
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>A : AlgebraCat R<VAR>x : ↑(of R ↑A)<GOAL>(((TensorProduct.mk R ↑(𝟙_ (ModuleCat R)) ↑(of R ↑A)).compr₂ (CategoryTheory.MonoidalCategory.whiskerRight (Algebra.linearMap R ↑A) (of R ↑A) ≫ mul' R ↑A)) 1) x = (((TensorProduct.mk R ↑(𝟙_ (ModuleCat R)) ↑(of R ↑A)).compr₂ (CategoryTheory.MonoidalCategory.leftUnitor (of R ↑A)).hom) 1) x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>A : AlgebraCat R<VAR>x : ↑(of R ↑A)<GOAL>(mul' R ↑A) ((CategoryTheory.MonoidalCategory.whiskerRight (Algebra.linearMap R ↑A) (of R ↑A)) (((TensorProduct.mk R ↑(𝟙_ (ModuleCat R)) ↑(of R ↑A)) 1) x)) = (CategoryTheory.MonoidalCategory.leftUnitor (of R ↑A)).hom (((TensorProduct.mk R ↑(𝟙_ (ModuleCat R)) ↑(of R ↑A)) 1) x)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>A : AlgebraCat R<VAR>x : ↑(of R ↑A)<GOAL>(1, x).1 • LinearMap.id (1, x).2 = 1 • x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>A : AlgebraCat R<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft (of R ↑A) (Algebra.linearMap R ↑A) ≫ mul' R ↑A = (CategoryTheory.MonoidalCategory.rightUnitor (of R ↑A)).hom
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>A : AlgebraCat R<VAR>x : ↑(of R ↑A)<GOAL>(((TensorProduct.mk R ↑(of R ↑A) ↑(𝟙_ (ModuleCat R))).compr₂ (CategoryTheory.MonoidalCategory.whiskerLeft (of R ↑A) (Algebra.linearMap R ↑A) ≫ mul' R ↑A)) x) 1 = (((TensorProduct.mk R ↑(of R ↑A) ↑(𝟙_ (ModuleCat R))).compr₂ (CategoryTheory.MonoidalCategory.rightUnitor (of R ↑A)).hom) x) 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>A : AlgebraCat R<VAR>x : ↑(of R ↑A)<GOAL>(CategoryTheory.MonoidalCategory.whiskerLeft (of R ↑A) (Algebra.linearMap R ↑A) ≫ mul' R ↑A) (((TensorProduct.mk R ↑(of R ↑A) ↑(𝟙_ (ModuleCat R))) x) 1) = (CategoryTheory.MonoidalCategory.rightUnitor (of R ↑A)).hom (((TensorProduct.mk R ↑(of R ↑A) ↑(𝟙_ (ModuleCat R))) x) 1)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>A : AlgebraCat R<VAR>x : ↑(of R ↑A)<GOAL>(mul' R ↑A) ((CategoryTheory.MonoidalCategory.whiskerLeft (of R ↑A) (Algebra.linearMap R ↑A)) (((TensorProduct.mk R ↑(of R ↑A) ↑(𝟙_ (ModuleCat R))) x) 1)) = (CategoryTheory.MonoidalCategory.rightUnitor (of R ↑A)).hom (((TensorProduct.mk R ↑(of R ↑A) ↑(𝟙_ (ModuleCat R))) x) 1)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>A : AlgebraCat R<VAR>x : ↑(of R ↑A)<GOAL>(x, 1).2 • LinearMap.id (x, 1).1 = 1 • x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>A : AlgebraCat R<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (mul' R ↑A) (of R ↑A) ≫ mul' R ↑A = (CategoryTheory.MonoidalCategory.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom ≫ CategoryTheory.MonoidalCategory.whiskerLeft (of R ↑A) (mul' R ↑A) ≫ mul' R ↑A
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : Module R X<GOAL>(↑__spread✝⁻⁰).toFun 0 = 0
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : MeasurableSpace H<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝³ : Group G<VAR>inst✝² : TopologicalGroup G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : μ.Regular<VAR>hμ : μ ≠ 0<VAR>s : Set G<VAR>hs : IsOpen s<GOAL>μ s ≠ 0 ↔ s.Nonempty
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : Semifield R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : HasContinuousInv₀ R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f✝ : R → R<VAR>a✝ : A<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>f : R → R<VAR>n : ℤ<VAR>a : Aˣ<VAR>hf : autoParam (ContinuousOn f ((fun x => x ^ n) '' spectrum R ↑a)) _auto✝<VAR>ha : autoParam (p ↑a) _auto✝<GOAL>cfc (fun x => f (x ^ n)) ↑a = cfc f ↑(a ^ n)
<VAR>e : ℝ<VAR>d n : ℕ<VAR>h : NormNum.IsNat e n<GOAL>0 ≤ Real.log e
<VAR>e : ℝ<VAR>d n : ℕ<VAR>h : NormNum.IsNat e n<GOAL>0 ≤ Real.log ↑n
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>y : I → Bool<VAR>left✝¹ : y ∈ C1 C ho<VAR>left✝ : Proj (fun x => ord I x < o) y ∈ C0 C ho<GOAL>Proj (fun x => ord I x < o) y (term I ho) = false
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<VAR>hn : 0 < n<VAR>b' : ℝ := b (min_bi b)<GOAL>(Ico ⌊b (min_bi b) / 2 * ↑n⌋₊ n).Nonempty
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<VAR>hn : 0 < n<VAR>b' : ℝ := b (min_bi b)<VAR>hb_pos : 0 < b'<GOAL>(Ico ⌊b (min_bi b) / 2 * ↑n⌋₊ n).Nonempty
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<VAR>hn : 0 < n<VAR>b' : ℝ := b (min_bi b)<VAR>hb_pos : 0 < b'<GOAL>⌊b (min_bi b) / 2 * ↑n⌋₊ < n
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : SemilatticeSup α<VAR>f : α → β<VAR>l : Filter β<GOAL>Tendsto f atTop l ↔ ∀ s ∈ l, ∃ a, ∀ b ≥ a, f b ∈ s
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.71152, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K'✝ : ChainComplex C ℕ<VAR>f✝ : K✝ ⟶ K'✝<VAR>Δ✝ Δ'✝ Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ' Δ : SimplexCategoryᵒᵖ<VAR>θ : Δ' ⟶ Δ<GOAL>(obj K).map θ ≫ (fun Δ => (splitting K).desc Δ fun A => f.f (unop A.fst).len ≫ ((splitting K').cofan Δ).inj A) Δ = (fun Δ => (splitting K).desc Δ fun A => f.f (unop A.fst).len ≫ ((splitting K').cofan Δ).inj A) Δ' ≫ (obj K').map θ
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.71152, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K'✝ : ChainComplex C ℕ<VAR>f✝ : K✝ ⟶ K'✝<VAR>Δ✝ Δ'✝ Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ' Δ : SimplexCategoryᵒᵖ<VAR>θ : Δ' ⟶ Δ<GOAL>∀ (A : Splitting.IndexSet Δ'), ((splitting K).cofan Δ').inj A ≫ (obj K).map θ ≫ (fun Δ => (splitting K).desc Δ fun A => f.f (unop A.fst).len ≫ ((splitting K').cofan Δ).inj A) Δ = ((splitting K).cofan Δ').inj A ≫ (fun Δ => (splitting K).desc Δ fun A => f.f (unop A.fst).len ≫ ((splitting K').cofan Δ).inj A) Δ' ≫ (obj K').map θ
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.71152, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K'✝ : ChainComplex C ℕ<VAR>f✝ : K✝ ⟶ K'✝<VAR>Δ✝ Δ'✝ Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ' Δ : SimplexCategoryᵒᵖ<VAR>θ : Δ' ⟶ Δ<VAR>A : Splitting.IndexSet Δ'<GOAL>((splitting K).cofan Δ').inj A ≫ (obj K).map θ ≫ (fun Δ => (splitting K).desc Δ fun A => f.f (unop A.fst).len ≫ ((splitting K').cofan Δ).inj A) Δ = ((splitting K).cofan Δ').inj A ≫ (fun Δ => (splitting K).desc Δ fun A => f.f (unop A.fst).len ≫ ((splitting K').cofan Δ).inj A) Δ' ≫ (obj K').map θ
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.71152, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K'✝ : ChainComplex C ℕ<VAR>f✝ : K✝ ⟶ K'✝<VAR>Δ✝ Δ'✝ Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ' Δ : SimplexCategoryᵒᵖ<VAR>θ : Δ' ⟶ Δ<VAR>A : Splitting.IndexSet Δ'<GOAL>Obj.Termwise.mapMono K (image.ι (θ.unop ≫ A.e)) ≫ f.f (unop (A.pull θ).fst).len ≫ ((splitting K').cofan Δ).inj (A.pull θ) = f.f (unop A.fst).len ≫ Obj.Termwise.mapMono K' (image.ι (θ.unop ≫ A.e)) ≫ ((splitting K').cofan Δ).inj (A.pull θ)
<VAR>k : Type u<VAR>inst✝ : CommRing k<VAR>G : Grp<VAR>X Y : Rep k ↑G<VAR>x✝ : ↥(X.ρ.linHom Y.ρ).invariants<GOAL>(fun f => ⟨f.hom, ⋯⟩) ({ toFun := fun f => { hom := ↑f, comm := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }.toFun x✝) = x✝
<VAR>k : Type u<VAR>inst✝ : CommRing k<VAR>G : Grp<VAR>X Y : Rep k ↑G<VAR>x✝ : ↥(X.ρ.linHom Y.ρ).invariants<GOAL>↑((fun f => ⟨f.hom, ⋯⟩) ({ toFun := fun f => { hom := ↑f, comm := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }.toFun x✝)) = ↑x✝
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E✝ : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E✝<VAR>X : C<VAR>E : PreOneHypercover X<VAR>F : C ⥤ D<VAR>x✝¹ x✝ : E.I₀<VAR>j : E.I₁ x✝¹ x✝<GOAL>(fun x x_1 j => F.map (E.p₁ j)) x✝¹ x✝ j ≫ (fun i => F.map (E.f i)) x✝¹ = (fun x x_1 j => F.map (E.p₂ j)) x✝¹ x✝ j ≫ (fun i => F.map (E.f i)) x✝
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p q r : Submodule R M<VAR>h₁ : IsCompl q r<VAR>h₂ : q ≤ p<GOAL>IsCompl (comap p.subtype q) (comap p.subtype r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hf : f.LimZero<VAR>hg : g.LimZero<GOAL>(f - g).LimZero