ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommMonoid M<VAR>a : M<VAR>l l₁ l₂ : List M<VAR>x : M<VAR>xs : List M<VAR>y : M<VAR>ys : List M<GOAL>x * (y * ((zipWith (fun x x_1 => x * x_1) xs ys).prod * (drop ys.length xs).prod * (drop xs.length ys).prod)) = x * y * (zipWith (fun x x_1 => x * x_1) xs ys).prod * (drop ys.length xs).prod * (drop xs.length ys).prod
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderTop α<VAR>a b c : α<GOAL>Codisjoint a (b ⊓ c) ↔ Codisjoint a b ∧ Codisjoint a c
<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>a✝ : α<VAR>f✝ g : α → β<VAR>M : Type u_6<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommMonoid M<VAR>f : α → M<VAR>a : α<VAR>l : List α<VAR>hl : (a :: l).Nodup<GOAL>(a :: l).toFinset.prod f = (map f (a :: l)).prod
<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>a✝ : α<VAR>f✝ g : α → β<VAR>M : Type u_6<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommMonoid M<VAR>f : α → M<VAR>a : α<VAR>l : List α<VAR>hl✝ : (a :: l).Nodup<VAR>not_mem : a ∉ l<VAR>hl : l.Nodup<GOAL>(a :: l).toFinset.prod f = (map f (a :: l)).prod
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>T T' T'' : D<VAR>Y Y' Y'' : C<VAR>S S' : C ⥤ D<VAR>f : CostructuredArrow S T<VAR>g : Y' ⟶ f.left<VAR>g' : Y'' ⟶ Y'<GOAL>(f.homMk' (g' ≫ g)).left = (eqToHom ⋯ ≫ (mk (S.map g ≫ f.hom)).homMk' g' ≫ f.homMk' g).left
<VAR>x : ZFSet<VAR>h : x.Nonempty<VAR>x✝ : ZFSet<GOAL>x✝ ∈ (⋂₀ x).toSet ↔ x✝ ∈ ⋂₀ (toSet '' x.toSet)
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>xeq : abs ⟨a, f⟩ = x<VAR>h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ<VAR>p : (i : Fin2 n) → α i → Prop<GOAL>LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>xeq : abs ⟨a, f⟩ = x<VAR>h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ<VAR>p : (i : Fin2 n) → α i → Prop<GOAL>(∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)) ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>xeq : abs ⟨a, f⟩ = x<VAR>h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ<VAR>p : (i : Fin2 n) → α i → Prop<VAR>h' : ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u<GOAL>∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>xeq : abs ⟨a, f⟩ = x<VAR>h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ<VAR>p : (i : Fin2 n) → α i → Prop<VAR>h' : ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u<GOAL>∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>xeq : abs ⟨a, f⟩ = x<VAR>h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ<VAR>p : (i : Fin2 n) → α i → Prop<VAR>h' : ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u<VAR>j : Fin2 n<VAR>y : (P F).B a j<GOAL>f j y ∈ supp x j
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>xeq : abs ⟨a, f⟩ = x<VAR>h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ<VAR>p : (i : Fin2 n) → α i → Prop<VAR>h' : ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u<VAR>j : Fin2 n<VAR>y : (P F).B a j<GOAL>∀ (a : (P F).A) (f_1 : (P F).B a ⟹ α), abs ⟨a, f_1⟩ = x → f j y ∈ f_1 j '' univ
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>xeq : abs ⟨a, f⟩ = x<VAR>h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ<VAR>p : (i : Fin2 n) → α i → Prop<VAR>h' : ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u<VAR>j : Fin2 n<VAR>y : (P F).B a j<VAR>a' : (P F).A<VAR>f' : (P F).B a' ⟹ α<VAR>xeq' : abs ⟨a', f'⟩ = x<GOAL>f j y ∈ f j '' univ
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>f : Π₀ (i : ι), β i<VAR>i j : ι<GOAL>(filter (fun x => x ≠ i) f) j = (erase i f) j
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>v₃ : Basis l R M₃<VAR>x : R<VAR>i✝ j✝ : n<GOAL>(toMatrix v₁ v₁) (DistribMulAction.toLinearMap R M₁ x) i✝ j✝ = Matrix.diagonal (fun x_1 => x) i✝ j✝
<VAR>z : ℂ<GOAL>HasSum (fun n => z ^ (2 * n + 1) / ↑(2 * n + 1)!) (sinh z)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>x : M<VAR>hI : (Submodule.span R {x}).annihilator.IsPrime<GOAL>⊤.annihilator ≤ (Submodule.span R {x}).annihilator
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : HasAntidiagonal A<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>f g : A → α<VAR>inst✝¹ : T3Space α<VAR>inst✝ : TopologicalSemiring α<VAR>h : Summable fun x => f x.1 * g x.2<GOAL>Summable fun n => ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : HasAntidiagonal A<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>f g : A → α<VAR>inst✝¹ : T3Space α<VAR>inst✝ : TopologicalSemiring α<VAR>h : Summable fun x => f (↑x.snd).1 * g (↑x.snd).2<GOAL>Summable fun n => ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : HasAntidiagonal A<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>f g : A → α<VAR>inst✝¹ : T3Space α<VAR>inst✝ : TopologicalSemiring α<VAR>h : Summable fun x => f (↑x.snd).1 * g (↑x.snd).2<GOAL>Summable fun x => ∑' (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t✝ : Set α<VAR>a : α<VAR>hs : s.Finite<VAR>ht : t✝.Finite<VAR>t : Finset α<GOAL>hs.toFinset ⊂ t ↔ s ⊂ ↑t
<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>n : ℕ<VAR>s : Simplex k P n<VAR>i : Fin (n + 1)<VAR>i✝ : Fin (0 + 1)<GOAL>(s.face ⋯).points i✝ = (mkOfPoint k (s.points i)).points i✝
<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>n : ℕ<VAR>s : Simplex k P n<VAR>i : Fin (n + 1)<VAR>i✝ : Fin (0 + 1)<GOAL>s.points (({i}.orderEmbOfFin ⋯) i✝) = s.points i
<VAR>u v m n : ℤ<GOAL>Even (n + 1) ↔ ¬Even n
<VAR>x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x < 1<VAR>H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)<GOAL>rexp x < 1 / (1 - x)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>hι : Cardinal.lift.{v, u} #ι < (lsub f).cof<VAR>hf : ∀ (i : ι), f i < lsub f<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f g : α →ₛ E<VAR>hf : Memℒp (↑f) p μ<VAR>hg : Memℒp (↑g) p μ<GOAL>toLp (f - g) ⋯ = toLp f hf - toLp g hg
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : X ≅ 0<VAR>Z : C<VAR>g h : Z ⟶ X<VAR>x✝ : g ≫ f = h ≫ f<GOAL>g = h
<VAR>A₁ : Type u_1<VAR>A₂ : Type u_2<VAR>inst✝² : AddCommGroup A₁<VAR>inst✝¹ : AddCommGroup A₂<VAR>inst✝ : NoZeroSMulDivisors ℕ A₂<VAR>f : A₁ →+ A₂<VAR>n : ℕ<VAR>g : A₁<VAR>hg : n • g ∈ f.ker<GOAL>n = 0 ∨ g ∈ f.ker
<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 ≈ g<GOAL>-f ≈ -g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f✝ g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>inst✝ : MeasurableSpace β<VAR>e : α → β<VAR>he : MeasurableEmbedding e<VAR>f : β → E<GOAL>IntegrableAtFilter f (map e l) (Measure.map e μ) ↔ IntegrableAtFilter (f ∘ e) l μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f✝ g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>inst✝ : MeasurableSpace β<VAR>e : α → β<VAR>he : MeasurableEmbedding e<VAR>f : β → E<GOAL>(∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ) ↔ ∃ s ∈ l, IntegrableOn (f ∘ e) s μ
<VAR>m n : ℕ<GOAL>m.Coprime n ↔ IsRelPrime m n
<VAR>m n : ℕ<GOAL>m.gcd n = 1 ↔ ∀ ⦃d : ℕ⦄, d ∣ m.gcd n → d ∣ 1
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<GOAL>(∏ i ∈ s, f i).natDegree ≤ ∑ i ∈ s, (f i).natDegree
<VAR>A : Type u_1<VAR>inst✝⁹ : NonUnitalNormedRing A<VAR>inst✝⁸ : CompleteSpace A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : CstarRing A<VAR>inst✝³ : NormedSpace ℂ A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : SMulCommClass ℂ A A<VAR>inst✝ : IsScalarTower ℂ A A<VAR>a b : A<VAR>hb : autoParam (IsSelfAdjoint b) _auto✝<GOAL>star a * b * a ≤ ‖b‖ • (star a * a)
<VAR>A : Type u_1<VAR>inst✝⁹ : NonUnitalNormedRing A<VAR>inst✝⁸ : CompleteSpace A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : CstarRing A<VAR>inst✝³ : NormedSpace ℂ A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : SMulCommClass ℂ A A<VAR>inst✝ : IsScalarTower ℂ A A<VAR>a b : A<VAR>hb : autoParam (IsSelfAdjoint b) _auto✝<GOAL>∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)
<VAR>A : Type u_1<VAR>inst✝⁹ : NonUnitalNormedRing A<VAR>inst✝⁸ : CompleteSpace A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : CstarRing A<VAR>inst✝³ : NormedSpace ℂ A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : SMulCommClass ℂ A A<VAR>inst✝ : IsScalarTower ℂ A A<VAR>a✝ b✝ : A<VAR>hb✝ : autoParam (IsSelfAdjoint b✝) _auto✝<VAR>a b : Unitization ℂ A<VAR>hb : IsSelfAdjoint b<GOAL>star a * b * a ≤ ‖b‖ • (star a * a)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>v.intValuationDef x ≠ 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors))) ≠ 0
<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>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f✝ : α → β<VAR>f : Bool → Measure α<GOAL>sum f = f true + f false
<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>f₂ : 𝕜 → F<VAR>s₂ : Set 𝕜<VAR>hs : IsOpen s₂<GOAL>ContDiffOn 𝕜 ⊤ f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 ⊤ (deriv f₂) s₂
<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>f₂ : 𝕜 → F<VAR>s₂ : Set 𝕜<VAR>hs : IsOpen s₂<GOAL>DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 ⊤ (derivWithin f₂ s₂) s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 ⊤ (deriv f₂) s₂
<VAR>ι✝ : Type u_1<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι✝ → Type u_3<VAR>r : α✝ → α✝ → Prop<VAR>ι : Type u_4<VAR>α : Type u_5<VAR>β : ι → Type u_6<VAR>inst✝¹ : (i : ι) → Preorder (β i)<VAR>inst✝ : Preorder α<VAR>f : α → (i : ι) → β i<GOAL>Antitone f ↔ ∀ (i : ι), Antitone fun x => f x i
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : Fintype m<VAR>inst✝⁸ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>inst✝³ : AddCommMonoid M₃<VAR>inst✝² : Module R M₃<VAR>v₃ : Basis l R M₃<VAR>inst✝¹ : Finite l<VAR>inst✝ : DecidableEq m<VAR>f : M₂ →ₗ[R] M₃<VAR>g : M₁ →ₗ[R] M₂<GOAL>(toMatrix v₁ v₃) (f ∘ₗ g) = (toMatrix v₂ v₃) f * (toMatrix v₁ v₂) g
<VAR>a x z✝ z : ℂ<GOAL>z.arg = 0 ↔ 0 ≤ z
<VAR>a : UnitAddCircle<VAR>n : ℕ<GOAL>hurwitzZetaEven a (-2 * (↑n + 1)) = 0
<VAR>a : UnitAddCircle<VAR>n : ℕ<VAR>this : -2 * (↑n + 1) ≠ 0<GOAL>hurwitzZetaEven a (-2 * (↑n + 1)) = 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>u : ℕ → E<VAR>l : E<VAR>h : Tendsto u atTop (𝓝 l)<GOAL>Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ range n, u i) atTop (𝓝 l)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>u : ℕ → E<VAR>l : E<VAR>h : Tendsto u atTop (𝓝 l)<GOAL>(fun x => (↑x)⁻¹ • ∑ i ∈ range x, u i - l) =o[atTop] fun _x => 1
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>u : ℕ → E<VAR>l : E<VAR>h : Tendsto u atTop (𝓝 l)<VAR>this : (fun n => ∑ i ∈ range n, (u i - l)) =o[atTop] fun n => ↑n<GOAL>(fun x => (↑x)⁻¹ • ∑ i ∈ range x, u i - l) =o[atTop] fun _x => 1
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>u : ℕ → E<VAR>l : E<VAR>h : Tendsto u atTop (𝓝 l)<VAR>this : (fun n => ∑ i ∈ range n, (u i - l)) =o[atTop] fun n => ↑n<GOAL>(fun x => (↑x)⁻¹ • ∑ i ∈ range x, (u i - l)) =ᶠ[atTop] fun x => (↑x)⁻¹ • ∑ i ∈ range x, u i - l
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>u : ℕ → E<VAR>l : E<VAR>h : Tendsto u atTop (𝓝 l)<VAR>this : (fun n => ∑ i ∈ range n, (u i - l)) =o[atTop] fun n => ↑n<GOAL>(fun x => (↑x)⁻¹ • ↑x) =ᶠ[atTop] fun _x => 1
<VAR>u : ℤˣ<GOAL>u * u = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>b : β<GOAL>b ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁✝ l₂✝ : List α<VAR>a b : α<VAR>l₁ l₂ l₃ : List α<VAR>h₁ : Chain' R (l₁ ++ l₂)<VAR>h₂ : Chain' R (l₂ ++ l₃)<VAR>hn : l₂ ≠ []<GOAL>∀ (x : α), x ∈ (l₁ ++ l₂).getLast? → ∀ (y : α), y ∈ l₃.head? → R x y
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>X : C<VAR>n : ℕ<VAR>X✝ Y✝ Z✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>f' : Y✝ ⟶ Z✝<VAR>α : ↑({ obj := fun Y => AddCommGrp.of (Ext X Y n), map := fun {X_1 Y} f => AddCommGrp.ofHom ((Ext.mk₀ f).postcomp X ⋯) }.obj X✝)<GOAL>Ext.comp α (Ext.mk₀ (f ≫ f')) ⋯ = (Ext.comp α (Ext.mk₀ f) ⋯).comp (Ext.mk₀ f') ⋯
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>X : C<VAR>n : ℕ<VAR>X✝ Y✝ Z✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>f' : Y✝ ⟶ Z✝<VAR>α : ↑({ obj := fun Y => AddCommGrp.of (Ext X Y n), map := fun {X_1 Y} f => AddCommGrp.ofHom ((Ext.mk₀ f).postcomp X ⋯) }.obj X✝)<GOAL>Ext.comp α ((Ext.mk₀ f).comp (Ext.mk₀ f') ⋯) ⋯ = (Ext.comp α (Ext.mk₀ f) ⋯).comp (Ext.mk₀ f') ⋯
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>X : C<VAR>n : ℕ<VAR>X✝ Y✝ Z✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>f' : Y✝ ⟶ Z✝<VAR>α : ↑({ obj := fun Y => AddCommGrp.of (Ext X Y n), map := fun {X_1 Y} f => AddCommGrp.ofHom ((Ext.mk₀ f).postcomp X ⋯) }.obj X✝)<GOAL>(Ext.comp α (Ext.mk₀ f) ⋯).comp (Ext.mk₀ f') ⋯ = Ext.comp α ((Ext.mk₀ f).comp (Ext.mk₀ f') ⋯) ⋯
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>X : C<VAR>n : ℕ<VAR>X✝ Y✝ Z✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>f' : Y✝ ⟶ Z✝<VAR>α : ↑({ obj := fun Y => AddCommGrp.of (Ext X Y n), map := fun {X_1 Y} f => AddCommGrp.ofHom ((Ext.mk₀ f).postcomp X ⋯) }.obj X✝)<GOAL>n + 0 + 0 = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>a : Associates α<VAR>x : Associates α<VAR>ndvd : ¬a * x ∣ a<GOAL>¬IsUnit x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>a : Associates α<VAR>x : Associates α<VAR>ndvd : IsUnit x<GOAL>a * x ∣ a
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>h : W ⟶ X<VAR>k : W ⟶ Y<VAR>comm : h ≫ f = k ≫ g<VAR>inst✝² : PreservesLimit (cospan f g) G<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPullback (G.map f) (G.map g)<GOAL>(iso G f g).inv ≫ G.map (pullback.snd f g) = pullback.snd (G.map f) (G.map g)
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionCommMonoid α<VAR>a✝ b c✝ d : α<VAR>hb : IsUnit b<VAR>hd : IsUnit d<VAR>a c : α<VAR>h : a / b = c / d<GOAL>a * d = c * b
<VAR>K : Type u_1<VAR>inst✝² : DivisionRing K<VAR>Γ₀ : Type u_2<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>inst✝ : Valued K Γ₀<GOAL>Continuous ⇑v
<VAR>K : Type u_1<VAR>inst✝² : DivisionRing K<VAR>Γ₀ : Type u_2<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>inst✝ : Valued K Γ₀<GOAL>∀ (x : K), ContinuousAt (⇑v) x
<VAR>K : Type u_1<VAR>inst✝² : DivisionRing K<VAR>Γ₀ : Type u_2<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>inst✝ : Valued K Γ₀<VAR>x : K<GOAL>ContinuousAt (⇑v) x
<VAR>K : Type u_1<VAR>inst✝² : DivisionRing K<VAR>Γ₀ : Type u_2<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>inst✝ : Valued K Γ₀<GOAL>ContinuousAt (⇑v) 0
<VAR>K : Type u_1<VAR>inst✝² : DivisionRing K<VAR>Γ₀ : Type u_2<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>inst✝ : Valued K Γ₀<VAR>x : K<VAR>h : x ≠ 0<GOAL>ContinuousAt (⇑v) x
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝² : CommRing R<VAR>a b x✝ y✝ : R<VAR>p✝ : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p : R<VAR>hp : Prime p<VAR>x y : R<VAR>hxy : p ∣ x - y<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : ¬p ∣ ↑n<GOAL>multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>inst✝ : PseudoMetricSpace β<VAR>f : α → β<GOAL>UniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
<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>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>σₙ R (cfcₙ f a) = f '' σₙ R a
<VAR>m n : PosNum<GOAL>n.cmp m = Ordering.lt ↔ m.cmp n = Ordering.gt
<VAR>m n : PosNum<GOAL>(m.cmp n).swap = Ordering.lt ↔ m.cmp n = Ordering.gt
<VAR>m : ℕ<VAR>inst✝ : NeZero m<VAR>f : ℕ → ℝ<VAR>hf : Antitone f<VAR>k : ZMod m<GOAL>Summable ({n | ↑n = k}.indicator f) ↔ Summable f
<VAR>m : ℕ<VAR>inst✝ : NeZero m<VAR>f : ℕ → ℝ<VAR>hf : Antitone f<VAR>k : ZMod m<VAR>H : Summable ({n | ↑n = k}.indicator f)<GOAL>Summable f
<VAR>m : ℕ<VAR>inst✝ : NeZero m<VAR>f : ℕ → ℝ<VAR>hf : Antitone f<VAR>k : ZMod m<VAR>H : Summable ({n | ↑n = k}.indicator f)<GOAL>Summable (∑ a : ZMod m, {n | ↑n = a}.indicator f)
<VAR>m : ℕ<VAR>inst✝ : NeZero m<VAR>f : ℕ → ℝ<VAR>hf : Antitone f<VAR>k : ZMod m<VAR>H : Summable ({n | ↑n = k}.indicator f)<VAR>x✝ : ℕ<GOAL>(∑ a : ZMod m, {n | ↑n = a}.indicator f) x✝ = ∑ i : ZMod m, {n | ↑n = i}.indicator f x✝
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>M : (Matrix n n R)[X]<VAR>r : R<GOAL>(matPolyEquiv.symm M).map (eval r) = eval ((scalar n) r) M
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>M : (Matrix n n R)[X]<VAR>r : R<GOAL>(aeval r).mapMatrix.comp ↑matPolyEquiv.symm = eval₂AlgHom' (AlgHom.id R (Matrix n n R)) ((scalar n) r) ⋯
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s s₁ s₂ t t₁ t₂ u : Finset α<VAR>a b c : α<GOAL>s ○ (t₁ ∩ t₂) ⊆ s ○ t₁ ∩ s ○ t₂
<VAR>α : Type u_1<VAR>inst✝² : GeneralizedBooleanAlgebra α<VAR>inst✝¹ : DecidableRel Disjoint<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a✝ b✝ a b : α<GOAL>compress (a \ b) (b \ a) b = a
<VAR>α : Type u_1<VAR>inst✝² : GeneralizedBooleanAlgebra α<VAR>inst✝¹ : DecidableRel Disjoint<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a✝ b✝ a b : α<GOAL>(b ⊔ a \ b) \ (b \ a) = a
<VAR>α : Type u_1<VAR>inst✝² : GeneralizedBooleanAlgebra α<VAR>inst✝¹ : DecidableRel Disjoint<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a✝ b✝ a b : α<GOAL>b \ (b \ a) ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>g : β → γ<VAR>hg : Continuous g<VAR>f : α →ₘ[μ] β<GOAL>↑(comp g hg f) =ᶠ[ae μ] g ∘ ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>g : β → γ<VAR>hg : Continuous g<VAR>f : α →ₘ[μ] β<GOAL>↑(mk (g ∘ ↑f) ⋯) =ᶠ[ae μ] g ∘ ↑f