ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p : Submodule R M<VAR>q : Submodule R N<GOAL>map₂ f.flip q p = map₂ f p q
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p : Submodule R M<VAR>q : Submodule R N<GOAL>span R (image2 (fun a b => (f.flip b) a) ↑p ↑q) = span R (image2 (fun m n => (f m) n) ↑p ↑q)
<VAR>ι : Type u_1<VAR>I✝ J : Box ι<VAR>x y : ι → ℝ<VAR>I : Box ι<GOAL>(match ↑I with | some val => true | none => false) = true ↔ (↑↑I).Nonempty
<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>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : MeasurableSpace δ<VAR>f g : α → β<VAR>μ ν : Measure α<VAR>inst✝ : Zero β<VAR>s t : Set α<VAR>ht : MeasurableSet t<VAR>hst : s =ᶠ[ae μ] t<GOAL>AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.42, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<GOAL>𝟙 ((Γ₀.splitting K).N (n + 1)) ≫ K.d (n + 1) n = (((Γ₀.splitting K).cofan (op [n + 1])).inj (Splitting.IndexSet.id (op [n + 1])) ≫ (AlternatingFaceMapComplex.obj (Γ₀.obj K)).d (n + 1) n ≫ (Γ₀.splitting K).πSummand (Splitting.IndexSet.id (op [n]))) ≫ 𝟙 ((Γ₀.splitting K).N n)
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.42, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<GOAL>K.d (n + 1) n = ∑ j : Fin (n + 2), ((Γ₀.splitting K).cofan (op [n + 1])).inj (Splitting.IndexSet.id (op [n + 1])) ≫ ((-1) ^ ↑j • (Γ₀.obj K).δ j) ≫ (Γ₀.splitting K).πSummand (Splitting.IndexSet.id (op [n]))
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.42, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<GOAL>K.d (n + 1) n = ((Γ₀.splitting K).cofan (op [n + 1])).inj (Splitting.IndexSet.id (op [n + 1])) ≫ ((-1) ^ ↑0 • (Γ₀.obj K).δ 0) ≫ (Γ₀.splitting K).πSummand (Splitting.IndexSet.id (op [n]))
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.42, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<GOAL>∀ (x : Fin (n + 2)), x ≠ 0 → ((Γ₀.splitting K).cofan (op [n + 1])).inj (Splitting.IndexSet.id (op [n + 1])) ≫ ((-1) ^ ↑x • (Γ₀.obj K).δ x) ≫ (Γ₀.splitting K).πSummand (Splitting.IndexSet.id (op [n])) = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>p : R[X]<VAR>x : S<GOAL>(normalizeScaleRoots p).degree = p.degree
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>p : R[X]<VAR>x : S<GOAL>(normalizeScaleRoots p).degree ≤ p.degree
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>p : R[X]<VAR>x : S<GOAL>p.degree ≤ (normalizeScaleRoots p).degree
<VAR>α : Type u<VAR>s : Set α<GOAL>IsClosed {u | s ∈ u}
<VAR>α : Type u<VAR>s : Set α<GOAL>IsOpen {u | s ∈ u}ᶜ
<VAR>α : Type u<VAR>s : Set α<GOAL>{u | s ∈ u}ᶜ = {u | sᶜ ∈ u}
<VAR>α : Type u<VAR>s : Set α<VAR>u : Ultrafilter α<GOAL>u ∈ {u | s ∈ u}ᶜ ↔ u ∈ {u | sᶜ ∈ u}
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R M<VAR>f : ι →₀ R<VAR>i : ι<GOAL>(b.toDual (b i)) ((Finsupp.total ι M R ⇑b) f) = f i
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R M<VAR>f : ι →₀ R<VAR>i : ι<GOAL>∑ x ∈ f.support, (b.toDual (b i)) (f x • b x) = f i
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R M<VAR>f : ι →₀ R<VAR>i : ι<GOAL>(if i ∈ f.support then f i else 0) = f i
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>X✝ Y✝ : Augmented C<VAR>η : X✝ ⟶ Y✝<GOAL>η.left.app (op [0]) ≫ Y✝.hom.app (op [0]) = X✝.hom.app (op [0]) ≫ η.right
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>X✝ Y✝ : Augmented C<VAR>η : X✝ ⟶ Y✝<GOAL>(η.left ≫ Y✝.hom).app (op [0]) = X✝.hom.app (op [0]) ≫ η.right
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>X✝ Y✝ : Augmented C<VAR>η : X✝ ⟶ Y✝<GOAL>(X✝.hom ≫ (const C).map η.right).app (op [0]) = X✝.hom.app (op [0]) ≫ η.right
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 1)<VAR>H : i ≤ j.castSucc<GOAL>X.map (SimplexCategory.δ i.castSucc) ≫ X.map (SimplexCategory.σ j.succ) = X.map (SimplexCategory.σ j) ≫ X.map (SimplexCategory.δ i)
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<VAR>l₁ l₂ : List α<GOAL>(l₁ ++ l₂).rdrop l₂.length = l₁
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a : X ⟶ Y<GOAL>-a + a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : NonUnitalSemiring A<VAR>inst✝² : Module R A<VAR>inst✝¹ : SMulCommClass R A A<VAR>inst✝ : IsScalarTower R A A<VAR>a b c : A<GOAL>(mulLeft R a * mulRight R b) c = (mulRight R b * mulLeft R a) c
<VAR>f : StieltjesFunction<VAR>hf_bot : Tendsto (↑f) atBot (𝓝 0)<VAR>hf_top : Tendsto (↑f) atTop (𝓝 1)<GOAL>f.measure univ = 1
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : OrderedSemiring α<VAR>inst✝ : Archimedean α<VAR>x : α<VAR>a✝ : Nontrivial α<GOAL>∃ n, x ≤ ↑n
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>(Lagrange.basis s v i).natDegree = s.card - 1
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<VAR>H : ∀ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0<GOAL>(Lagrange.basis s v i).natDegree = s.card - 1
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<VAR>H : ∀ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0<GOAL>(Lagrange.basis s v i).natDegree = ∑ x ∈ s.erase i, 1
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<VAR>H : ∀ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0<GOAL>∑ x ∈ s.erase i, 1 = ∑ i_1 ∈ s.erase i, (basisDivisor (v i) (v i_1)).natDegree
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j✝ : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<VAR>H : ∀ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0<VAR>j : ι<VAR>hj : j ∈ s.erase i<GOAL>v i ≠ v j
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j✝ : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<VAR>H : ∀ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0<VAR>j : ι<VAR>hj : j ∈ s.erase i<GOAL>¬basisDivisor (v i) (v j) = 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>f : ↥(lp E p)<VAR>hf : ∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal<GOAL>‖f‖ ≤ C
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>f : ↥(lp E p)<VAR>hf : ∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal<GOAL>∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<VAR>hf : IsLocallyInjective f<VAR>g : A → X<VAR>cont : Continuous g<VAR>hg : Function.Injective g<GOAL>IsLocallyInjective (f ∘ g)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<VAR>hf : IsOpen (Function.pullbackDiagonal f)<VAR>g : A → X<VAR>cont : Continuous g<VAR>hg : Function.Injective g<GOAL>IsOpen (Function.pullbackDiagonal (f ∘ g))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<VAR>hf : IsOpen (Function.pullbackDiagonal f)<VAR>g : A → X<VAR>cont : Continuous g<VAR>hg : Function.Injective g<GOAL>IsOpen (Function.mapPullback g id g ⋯ ⋯ ⁻¹' Function.pullbackDiagonal f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : Ordinal.{u} → Ordinal.{max u v}<GOAL>IsNormal f ↔ (∀ (a : Ordinal.{u}), f a < f (succ a)) ∧ ∀ (o : Ordinal.{u}), o.IsLimit → (o.blsub fun x x_1 => f x) = f o
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : Ordinal.{u} → Ordinal.{max u v}<GOAL>(∀ (a : Ordinal.{u}), f a < f (succ a)) → ((∀ (o : Ordinal.{u}), o.IsLimit → (o.bsup fun x x_1 => f x) = f o) ↔ ∀ (o : Ordinal.{u}), o.IsLimit → (o.blsub fun x x_1 => f x) = f o)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : Ordinal.{u} → Ordinal.{max u v}<VAR>h : ∀ (a : Ordinal.{u}), f a < f (succ a)<GOAL>(∀ (o : Ordinal.{u}), o.IsLimit → (o.bsup fun x x_1 => f x) = f o) ↔ ∀ (o : Ordinal.{u}), o.IsLimit → (o.blsub fun x x_1 => f x) = f o
<VAR>K : Type u<VAR>inst✝ : Field K<GOAL>num 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>n : ℕ<VAR>inst✝ : Fintype α<VAR>P : α → ℕ<VAR>hP : ∑ i : α, P i = n<VAR>a : α<GOAL>Multiset.count a (Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P)) = Multiset.count a (Multiset.map (fun a => ↑⟨P, hP⟩ a • {a}) univ.val).sum
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>n : ℕ<VAR>inst✝ : Fintype α<VAR>P : α → ℕ<VAR>hP : ∑ i : α, P i = n<VAR>a : α<GOAL>Multiset.count a (Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P)) = (Multiset.map (fun b => Multiset.count a (↑⟨P, hP⟩ b • {b})) univ.val).sum
<VAR>cd : Fin 2 → ℝ<VAR>z : ℍ<VAR>h : cd ≠ 0<GOAL>↑(cd 0) * ↑z + ↑(cd 1) ≠ 0
<VAR>cd : Fin 2 → ℝ<VAR>z : ℍ<VAR>h : ↑(cd 0) * ↑z + ↑(cd 1) = 0<GOAL>cd = 0
<VAR>cd : Fin 2 → ℝ<VAR>z : ℍ<VAR>h : ↑(cd 0) * ↑z + ↑(cd 1) = 0<VAR>this : cd 0 = 0<GOAL>cd = 0
<VAR>cd : Fin 2 → ℝ<VAR>z : ℍ<VAR>this : cd 0 = 0<VAR>h : cd 1 = 0<GOAL>cd = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<GOAL>∑ i : PointsWithCircumcenterIndex n, circumcenterWeightsWithCircumcenter n i = 1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>j : PointsWithCircumcenterIndex n<VAR>a✝ : j ∈ univ<GOAL>circumcenterWeightsWithCircumcenter n j = if j = circumcenterIndex then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<GOAL>1 = if circumcenterIndex ∈ univ then Function.const (PointsWithCircumcenterIndex n) 1 circumcenterIndex else 0
<VAR>α : Type u_1<VAR>d : DynkinSystem α<VAR>s : Set (Set α)<VAR>hs : IsPiSystem s<VAR>t₁ t₂ : Set α<VAR>ht₁ : (generate s).Has t₁<VAR>ht₂ : (generate s).Has t₂<VAR>s₁ : Set α<VAR>hs₁ : s₁ ∈ s<VAR>this✝¹ : (generate s).Has s₁<VAR>this✝ : generate s ≤ (generate s).restrictOn this✝¹<VAR>this : (generate s).Has (t₂ ∩ s₁)<GOAL>(generate s).Has (s₁ ∩ t₂)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : LindelofSpace X<VAR>U : X → Set X<VAR>hU : ∀ (x : X), U x ∈ 𝓝 x<GOAL>∃ t, t.Countable ∧ ⋃ x ∈ t, U x = univ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t✝ : Set X<VAR>inst✝ : LindelofSpace X<VAR>U : X → Set X<VAR>hU : ∀ (x : X), U x ∈ 𝓝 x<VAR>t : Set X<VAR>tc : t.Countable<VAR>s : univ ⊆ ⋃ x ∈ t, U x<GOAL>∃ t, t.Countable ∧ ⋃ x ∈ t, U x = univ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t✝ : Set X<VAR>inst✝ : LindelofSpace X<VAR>U : X → Set X<VAR>hU : ∀ (x : X), U x ∈ 𝓝 x<VAR>t : Set X<VAR>tc : t.Countable<VAR>s : univ ⊆ ⋃ x ∈ t, U x<GOAL>⋃ x ∈ t, U x = univ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m✝ n✝ : ℤ<VAR>a1 : 1 ≤ a<VAR>m n : ℕ<VAR>mn : m ≤ n<GOAL>1 / a ^ n ≤ 1 / a ^ m
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f' : 𝕜 → F<VAR>hs : IsOpen s<VAR>hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<VAR>x : 𝕜<VAR>hx : x ∈ s<GOAL>deriv f x = f' x
<VAR>α : Type u_1<VAR>inst✝ : NormedAddCommGroup α<VAR>f : ℕ → α<VAR>h : Tendsto f atTop (𝓝 0)<GOAL>(fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ↑n
<VAR>α : Type u_1<VAR>inst✝ : NormedAddCommGroup α<VAR>f : ℕ → α<VAR>h : Tendsto f atTop (𝓝 0)<VAR>this : Tendsto (fun n => ∑ i ∈ range n, 1) atTop atTop → (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ∑ i ∈ range n, 1<GOAL>(fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ↑n
<VAR>α : Type u_1<VAR>inst✝ : NormedAddCommGroup α<VAR>f : ℕ → α<VAR>h : Tendsto f atTop (𝓝 0)<VAR>this : Tendsto (fun n => ↑n) atTop atTop → (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ↑n<GOAL>(fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t✝ : Set α<VAR>inst✝ : Fintype ↑s<VAR>t : Finset α<GOAL>s.toFinset ⊆ t ↔ s ⊆ ↑t
<VAR>F : Type u<VAR>Γ₀ : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation F Γ₀<VAR>O : Type w<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O F<VAR>hv : v.Integers O<VAR>x : F<GOAL>∃ a, x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a
<VAR>F : Type u<VAR>Γ₀ : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation F Γ₀<VAR>O : Type w<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O F<VAR>hv : v.Integers O<VAR>x : F<VAR>h : v x ≤ 1<VAR>a : O<VAR>ha : (algebraMap O F) a = x<GOAL>∃ a, x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a
<VAR>F : Type u<VAR>Γ₀ : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation F Γ₀<VAR>O : Type w<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O F<VAR>hv : v.Integers O<VAR>x : F<VAR>h : v x⁻¹ ≤ 1<VAR>a : O<VAR>ha : (algebraMap O F) a = x⁻¹<GOAL>∃ a, x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a
<VAR>M : Type u_1<VAR>N✝ : Type u_2<VAR>inst✝² : SeminormedAddCommGroup M<VAR>inst✝¹ : SeminormedAddCommGroup N✝<VAR>N : Type u_3<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>f : NormedAddGroupHom M N<VAR>hf : ∀ s ∈ S, f s = 0<VAR>g : NormedAddGroupHom (M ⧸ S) N<VAR>h : g.comp S.normedMk = f<VAR>x : M ⧸ S<GOAL>g x = (lift S f hf) x
<VAR>M : Type u_1<VAR>N✝ : Type u_2<VAR>inst✝² : SeminormedAddCommGroup M<VAR>inst✝¹ : SeminormedAddCommGroup N✝<VAR>N : Type u_3<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>f : NormedAddGroupHom M N<VAR>hf : ∀ s ∈ S, f s = 0<VAR>g : NormedAddGroupHom (M ⧸ S) N<VAR>h : g.comp S.normedMk = f<VAR>x : M<GOAL>g (S.normedMk x) = (lift S f hf) (S.normedMk x)
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Respects f₁ f₂ tr<VAR>a₁ : σ₁<VAR>b₂ a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>ab : b₂ ∈ eval f₂ a₂<GOAL>∃ b₁, tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Respects f₁ f₂ tr<VAR>a₁ : σ₁<VAR>b₂ a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>ab✝ : b₂ ∈ eval f₂ a₂<VAR>ab : Reaches f₂ a₂ b₂<VAR>b0 : f₂ b₂ = none<GOAL>∃ b₁, tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Respects f₁ f₂ tr<VAR>a₁ : σ₁<VAR>b₂ a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>ab✝ : b₂ ∈ eval f₂ a₂<VAR>ab : Reaches f₂ a₂ b₂<VAR>b0 : f₂ b₂ = none<VAR>c₁ : σ₁<VAR>c₂ : σ₂<VAR>bc : Reaches f₂ b₂ c₂<VAR>cc : tr c₁ c₂<VAR>ac : Reaches f₁ a₁ c₁<GOAL>∃ b₁, tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Respects f₁ f₂ tr<VAR>a₁ : σ₁<VAR>b₂ a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>ab✝ : b₂ ∈ eval f₂ a₂<VAR>ab : Reaches f₂ a₂ b₂<VAR>b0 : f₂ b₂ = none<VAR>c₁ : σ₁<VAR>ac : Reaches f₁ a₁ c₁<VAR>bc : Reaches f₂ b₂ b₂<VAR>cc : tr c₁ b₂<GOAL>∃ b₁, tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Respects f₁ f₂ tr<VAR>a₁ : σ₁<VAR>b₂ a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>ab✝ : b₂ ∈ eval f₂ a₂<VAR>ab : Reaches f₂ a₂ b₂<VAR>b0 : f₂ b₂ = none<VAR>c₁ : σ₁<VAR>ac : Reaches f₁ a₁ c₁<VAR>bc : Reaches f₂ b₂ b₂<VAR>cc : tr c₁ b₂<GOAL>f₁ c₁ = none
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Respects f₁ f₂ tr<VAR>a₁ : σ₁<VAR>b₂ a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>ab✝ : b₂ ∈ eval f₂ a₂<VAR>ab : Reaches f₂ a₂ b₂<VAR>b0 : f₂ b₂ = none<VAR>c₁ : σ₁<VAR>ac : Reaches f₁ a₁ c₁<VAR>bc : Reaches f₂ b₂ b₂<VAR>cc : tr c₁ b₂<VAR>d₁ : σ₁<VAR>hfc : f₁ c₁ = some d₁<VAR>d₂ : σ₂<VAR>left✝ : tr d₁ d₂<VAR>bd : Reaches₁ f₂ b₂ d₂<GOAL>some d₁ = none
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Respects f₁ f₂ tr<VAR>a₁ : σ₁<VAR>b₂ a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>ab✝ : b₂ ∈ eval f₂ a₂<VAR>ab : Reaches f₂ a₂ b₂<VAR>b0 : f₂ b₂ = none<VAR>c₁ : σ₁<VAR>ac : Reaches f₁ a₁ c₁<VAR>bc : Reaches f₂ b₂ b₂<VAR>cc : tr c₁ b₂<VAR>d₁ : σ₁<VAR>hfc : f₁ c₁ = some d₁<VAR>d₂ : σ₂<VAR>left✝ : tr d₁ d₂<VAR>bd : Reaches₁ f₂ b₂ d₂<VAR>e : σ₂<VAR>h : e ∈ f₂ b₂<VAR>right✝ : ReflTransGen (fun a b => b ∈ f₂ a) e d₂<GOAL>some d₁ = none
<VAR>p q : Prop<VAR>α : Sort u_1<VAR>s✝ : α → Prop<VAR>β : Type u_2<VAR>inst✝ : LinearOrder β<VAR>s : Set β<GOAL>(s ≠ ∅) = s.Nonempty
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : AffineSubspace ℝ E<VAR>hs : s ≠ ⊤<GOAL>μ ↑s = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : ⊥ ≠ ⊤<GOAL>μ ↑⊥ = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : AffineSubspace ℝ E<VAR>hs : s ≠ ⊤<VAR>hne : (↑s).Nonempty<GOAL>μ ↑s = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : AffineSubspace ℝ E<VAR>hs : ¬s.direction = ⊤<VAR>hne : (↑s).Nonempty<GOAL>μ ↑s = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : AffineSubspace ℝ E<VAR>hs : ¬s.direction = ⊤<VAR>x : E<VAR>hx : x ∈ s<GOAL>μ ↑s = 0
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>ι : Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<GOAL>ofTensorProduct I (ι → R) ∘ₗ ↑((piEquivOfFintype I fun x => R).trans (piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm) = LinearMap.id
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>ι : Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<GOAL>↑(piEquivOfFintype I fun x => R).symm ∘ₗ ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) ∘ₗ ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm ∘ₗ ↑(piEquivOfFintype I fun x => R) = LinearMap.id
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>ι : Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<GOAL>↑(piEquivOfFintype I fun x => R).symm ∘ₗ (↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) ∘ₗ ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm) ∘ₗ ↑(piEquivOfFintype I fun x => R) = LinearMap.id
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁ ∪ s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>𝒢 : Set Cᵒᵖ<GOAL>IsSeparating 𝒢.unop ↔ IsCoseparating 𝒢
<VAR>α : Type u<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : Subsingleton αˣ<VAR>a b : α<VAR>h : a * b = 1<GOAL>b * a = 1
<VAR>x✝ y x : ℂ<VAR>hx : ‖x‖ = 1<VAR>hy : ‖1‖ = 1<GOAL>‖x - 1‖ ∈ Icc (2 / π * angle x 1) (angle x 1)
<VAR>x✝ y x : ℂ<VAR>hx : ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x<VAR>hy : ‖1‖ = 1<GOAL>‖x - 1‖ ∈ Icc (2 / π * angle x 1) (angle x 1)
<VAR>x y : ℂ<VAR>hy : ‖1‖ = 1<VAR>θ : ℝ<VAR>hθ : θ ∈ Ioc (-π) π<GOAL>‖cexp (↑θ * I) - 1‖ ∈ Icc (2 / π * angle (cexp (↑θ * I)) 1) (angle (cexp (↑θ * I)) 1)
<VAR>x y : ℂ<VAR>hy : ‖1‖ = 1<VAR>θ : ℝ<VAR>hθ : θ ∈ Ioc (-π) π<GOAL>‖cos ↑θ - 1 + sin ↑θ * I‖ ∈ Icc (2 / π * |θ|) |θ|
<VAR>x y : ℂ<VAR>hy : ‖1‖ = 1<VAR>θ : ℝ<VAR>hθ : θ ∈ Ioc (-π) π<GOAL>θ ∈ Ioc (-π) (-π + 2 * π)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>f✝ g✝ h : α → β<VAR>f : l.Germ β<VAR>lc : Filter γ<VAR>g : γ → α<VAR>hf : f.IsConstant<VAR>hg : Tendsto g lc l<GOAL>(f.compTendsto g hg).IsConstant
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>f✝ g✝ h : α → β<VAR>lc : Filter γ<VAR>g : γ → α<VAR>hg : Tendsto g lc l<VAR>f : α → β<VAR>hf : IsConstant ⟦f⟧<GOAL>(compTendsto ⟦f⟧ g hg).IsConstant
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type w<VAR>inst✝¹⁴ : Ring R<VAR>inst✝¹³ : Ring S<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module.Free R M<VAR>inst✝⁹ : Module.Finite R M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R N<VAR>inst✝⁶ : Module S N<VAR>inst✝⁵ : SMulCommClass R S N<VAR>inst✝⁴ : StrongRankCondition R<VAR>inst✝³ : StrongRankCondition S<VAR>inst✝² : Module.Free S N<VAR>inst✝¹ : Module R S<VAR>inst✝ : SMulCommClass R S S<GOAL>Module.rank S (M →ₗ[R] S) = lift.{u', v} (Module.rank R M)