ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>p : κ → Prop<VAR>s : κ → Set (β × β)<VAR>F : ι → β → α<VAR>hβ : (𝓤 β).HasBasis p s<GOAL>UniformEquicontinuous F ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>p : κ → Prop<VAR>s : κ → Set (β × β)<VAR>F : ι → β → α<VAR>hβ : (𝓤 β).HasBasis p s<GOAL>(∀ ib ∈ 𝓤 α, ∃ ia, p ia ∧ ∀ x ∈ s ia, ((⇑UniformFun.ofFun ∘ swap F) x.1, (⇑UniformFun.ofFun ∘ swap F) x.2) ∈ UniformFun.gen ι α ib) ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>p : κ → Prop<VAR>s : κ → Set (β × β)<VAR>F : ι → β → α<VAR>hβ : (𝓤 β).HasBasis p s<GOAL>(∀ ib ∈ 𝓤 α, ∃ ia, p ia ∧ ∀ (a b : β), (a, b) ∈ s ia → ((⇑UniformFun.ofFun ∘ swap F) a, (⇑UniformFun.ofFun ∘ swap F) b) ∈ UniformFun.gen ι α ib) ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_1} C<VAR>inst✝⁶ : Category.{u_5, u_2} D<VAR>inst✝⁵ : Zero I<VAR>inst✝⁴ : DecidableEq I<VAR>inst✝³ : HasInitial C<VAR>F : C ⥤ D ⥤ D<VAR>X : C<VAR>e : F.obj X ≅ 𝟭 D<VAR>inst✝² : (Y : D) → PreservesColimit (Functor.empty C) (F.flip.obj Y)<VAR>p : I × J → J<VAR>hp : ∀ (j : J), p (0, j) = j<VAR>Y Y' : GradedObject J D<VAR>φ : Y ⟶ Y'<VAR>inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p<VAR>inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p<VAR>j : J<GOAL>ιMapBifunctorMapObj F p ((single₀ I).obj X) Y 0 j j ⋯ ≫ (CofanMapObjFun.iso (mapBifunctorLeftUnitorCofanIsColimit F X e p hp Y j)).inv = (F.map (singleObjApplyIso 0 X).hom).app (Y j) ≫ e.hom.app (Y j)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_1} C<VAR>inst✝⁶ : Category.{u_5, u_2} D<VAR>inst✝⁵ : Zero I<VAR>inst✝⁴ : DecidableEq I<VAR>inst✝³ : HasInitial C<VAR>F : C ⥤ D ⥤ D<VAR>X : C<VAR>e : F.obj X ≅ 𝟭 D<VAR>inst✝² : (Y : D) → PreservesColimit (Functor.empty C) (F.flip.obj Y)<VAR>p : I × J → J<VAR>hp : ∀ (j : J), p (0, j) = j<VAR>Y Y' : GradedObject J D<VAR>φ : Y ⟶ Y'<VAR>inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p<VAR>inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p<VAR>j : J<GOAL>Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(0, j), ⋯⟩ = (F.map (singleObjApplyIso 0 X).hom).app (Y j) ≫ e.hom.app (Y j)
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>a : α<VAR>b b' : β a<VAR>l : List (Sigma β)<VAR>nd : l.NodupKeys<VAR>h : ⟨a, b⟩ ∈ l<VAR>h' : ⟨a, b'⟩ ∈ l<GOAL>b = b'
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<VAR>nd : l.NodupKeys<VAR>h h' : ⟨a, b⟩ ∈ l<GOAL>b = b
<VAR>x n m : ℕ<VAR>hcop : n.Coprime m<VAR>h : x.gcd n * x.gcd m = x<GOAL>x ∣ n * m
<VAR>x n m : ℕ<VAR>hcop : n.Coprime m<VAR>x✝ : x ∣ n * m<GOAL>x.gcd n * x.gcd m ∣ x
<GOAL>Gammaℂ 1 = 1 / ↑π
<GOAL>2 * (2 * ↑π)⁻¹ * 1 = 1 / ↑π
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>s : Set α<GOAL>s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, SymmetricRel V ∧ ball x V ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>s : Set α<GOAL>(∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∃ V ∈ 𝓤 α, SymmetricRel V ∧ ball x V ⊆ s
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Mul α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ s t : Finset α<GOAL>s.card ^ 2 * t.card ^ 2 = (filter (fun x => match x with | (a, b) => a * b ∈ s * t) (s ×ˢ t)).card ^ 2
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Mul α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ s t : Finset α<GOAL>∀ x ∈ s ×ˢ t, match x with | (a, b) => a * b ∈ s * t
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>x : R<VAR>hx : IsQuasiregular x<GOAL>IsUnit (1 + x)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>x : R<VAR>hx : IsQuasiregular x<VAR>y : R<VAR>hy₁ : y + x + x * y = 0<VAR>hy₂ : x + y + y * x = 0<GOAL>IsUnit (1 + x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>hνμ : ν ≪ μ<GOAL>(μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] ν.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>hνμ : ν ≪ μ<GOAL>μ.withDensity (μ.rnDeriv ν)⁻¹ = μ.withDensity (ν.rnDeriv μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>hνμ : ν ≪ μ<GOAL>(ν.withDensity (μ.rnDeriv ν)).withDensity ((ν.withDensity (μ.rnDeriv ν)).rnDeriv ν)⁻¹ = ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>hνμ : ν ≪ μ<GOAL>(ν.withDensity (μ.rnDeriv ν)).withDensity (μ.rnDeriv ν)⁻¹ = ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>hνμ : ν ≪ μ<GOAL>((ν.withDensity (μ.rnDeriv ν)).withDensity fun x => (μ.rnDeriv ν x)⁻¹) = ν
<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 ⊆ s ⊻ t
<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>∀ ⦃x : α⦄, (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝²⁰ : Semiring R₁<VAR>inst✝¹⁹ : Semiring R₂<VAR>inst✝¹⁸ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>inst✝¹⁷ : TopologicalSpace M₁<VAR>inst✝¹⁶ : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹⁵ : TopologicalSpace M'₁<VAR>inst✝¹⁴ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝¹³ : TopologicalSpace M₂<VAR>inst✝¹² : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : TopologicalSpace M₃<VAR>inst✝¹⁰ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝⁹ : TopologicalSpace M₄<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : Module R₁ M₁<VAR>inst✝⁶ : Module R₁ M'₁<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>F : Type u_9<VAR>inst✝² : Module R₁ M₂<VAR>inst✝¹ : TopologicalSpace R₁<VAR>inst✝ : ContinuousSMul R₁ M₂<VAR>f f' : M₂<GOAL>smulRight 1 f = smulRight 1 f' ↔ f = f'
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a : ℝ≥0∞<GOAL>a⁻¹ * a ≤ 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>hf : UniformInducing f<VAR>F : Filter α<GOAL>Cauchy (map f F) ↔ Cauchy F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ<VAR>hf : HasFiniteIntegral f μ<VAR>x : α<GOAL>‖max (f x) 0‖ ≤ ‖f x‖
<VAR>n : ℕ<GOAL>(n + 1).succ * (n + 1).choose 0 = (n + 1).succ.choose (succ 0) * succ 0
<VAR>n k : ℕ<GOAL>(n + 1).succ * (n + 1).choose (k + 1) = (n + 1).succ.choose (k + 1).succ * (k + 1).succ
<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>Even (m - n) ↔ (Even m ↔ Even n)
<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>Even (m - n) ↔ ((Even (m - n) ↔ Even n) ↔ Even n)
<VAR>r : ℝ<VAR>p : ℝ≥0<VAR>ha : 0 ≤ r<GOAL>r.toNNReal < p ↔ r < ↑p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f f₁ f₂ : Filter α<VAR>h h₁ h₂ : Set α → Set β<VAR>m : γ → β<VAR>l : Filter γ<GOAL>Tendsto m l (f.lift' h) ↔ ∀ s ∈ f, ∀ᶠ (a : γ) in l, m a ∈ h s
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>S : Set (Submonoid M)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>S : Set (Submonoid M)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : M<VAR>this : Nonempty ↑S<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>u v : α → ℝ<GOAL>(fun x => ‖f' x‖) =o[l] g ↔ f' =o[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>u v : α → ℝ<GOAL>(∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => ‖f' x‖) g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g
<VAR>a✝ b✝ c✝ d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b c : ℕ<GOAL>a % c * b % c = a * b % c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hf : Integrable f μ<GOAL>edist (toL1 f hf) 0 = ∫⁻ (a : α), edist (f a) 0 ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hf : Integrable f μ<GOAL>(if 1 = ⊤ then eLpNormEssSup f μ else ∫⁻ (a : α), ↑‖f a‖₊ ∂μ) = ∫⁻ (a : α), edist (f a) 0 ∂μ
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z : PresheafedSpace C<VAR>α : X ⟶ Y<VAR>β : Y ⟶ Z<VAR>x : ↑↑X<GOAL>colimMap (whiskerLeft (OpenNhds.inclusion (β.base (α.base x))).op (α ≫ β).c) ≫ colimMap (whiskerRight (𝟙 (OpenNhds.map (α.base ≫ β.base) x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫ colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map (α.base ≫ β.base) x).op = (colimMap (whiskerLeft (OpenNhds.inclusion (β.base (α.base x))).op β.c) ≫ colimMap (whiskerRight (𝟙 (OpenNhds.map β.base (α.base x) ⋙ OpenNhds.inclusion (α.base x)).op) Y.presheaf) ≫ colimit.pre ((OpenNhds.inclusion (α.base x)).op ⋙ Y.presheaf) (OpenNhds.map β.base (α.base x)).op) ≫ colimMap (whiskerLeft (OpenNhds.inclusion (α.base x)).op α.c) ≫ colimMap (whiskerRight (𝟙 (OpenNhds.map α.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫ colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map α.base x).op
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z : PresheafedSpace C<VAR>α : X ⟶ Y<VAR>β : Y ⟶ Z<VAR>x : ↑↑X<GOAL>∀ (j : (OpenNhds (β.base (α.base x)))ᵒᵖ), colimit.ι (((whiskeringLeft (OpenNhds (β.base (α.base x)))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj (OpenNhds.inclusion (β.base (α.base x))).op).obj Z.presheaf) j ≫ colimMap (whiskerLeft (OpenNhds.inclusion (β.base (α.base x))).op (α ≫ β).c) ≫ colimMap (whiskerRight (𝟙 (OpenNhds.map (α.base ≫ β.base) x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫ colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map (α.base ≫ β.base) x).op = colimit.ι (((whiskeringLeft (OpenNhds (β.base (α.base x)))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj (OpenNhds.inclusion (β.base (α.base x))).op).obj Z.presheaf) j ≫ (colimMap (whiskerLeft (OpenNhds.inclusion (β.base (α.base x))).op β.c) ≫ colimMap (whiskerRight (𝟙 (OpenNhds.map β.base (α.base x) ⋙ OpenNhds.inclusion (α.base x)).op) Y.presheaf) ≫ colimit.pre ((OpenNhds.inclusion (α.base x)).op ⋙ Y.presheaf) (OpenNhds.map β.base (α.base x)).op) ≫ colimMap (whiskerLeft (OpenNhds.inclusion (α.base x)).op α.c) ≫ colimMap (whiskerRight (𝟙 (OpenNhds.map α.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫ colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map α.base x).op
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : T2Space Y<VAR>s t : Set X<VAR>f g : X → Y<VAR>h : EqOn f g s<VAR>hf : ContinuousOn f t<VAR>hg : ContinuousOn g t<VAR>hst : s ⊆ t<VAR>hts : t ⊆ closure s<VAR>x : X<VAR>hx : x ∈ t<GOAL>f x = g x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : T2Space Y<VAR>s t : Set X<VAR>f g : X → Y<VAR>h : EqOn f g s<VAR>hf : ContinuousOn f t<VAR>hg : ContinuousOn g t<VAR>hst : s ⊆ t<VAR>hts : t ⊆ closure s<VAR>x : X<VAR>hx : x ∈ t<VAR>this : (𝓝[s] x).NeBot<GOAL>f x = g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>s t : Set α<GOAL>𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ (𝓝 a ⊓ 𝓟 t)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>s t : Multiset α<VAR>a✝ : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>inst✝ : DecidableEq α<VAR>a : α<GOAL>a ^ count a s = (filter (Eq a) s).prod
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l₁ : List α<VAR>h : l₁.length ≤ [].length<GOAL>(l₁.zip []).unzip.1 = l₁
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l₁ : List α<VAR>h : l₁.length ≤ [].length<GOAL>([].zip []).unzip.1 = []
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>a : α<VAR>l₁ : List α<VAR>b : β<VAR>l₂ : List β<VAR>h : (a :: l₁).length ≤ (b :: l₂).length<GOAL>((a :: l₁).zip (b :: l₂)).unzip.1 = a :: l₁
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidableEq α<VAR>x y : α<GOAL>(count x) (of y) = Pi.single x 1 y
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>x y : M<VAR>hsrc : x ∈ (chartAt H y).source<GOAL>mfderiv I I (↑(chartAt H y)) x = tangentCoordChange I x y x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>x y : M<VAR>hsrc : x ∈ (chartAt H y).source<VAR>this : MDifferentiableAt I I (↑(ChartedSpace.chartAt y)) x<GOAL>mfderiv I I (↑(chartAt H y)) x = tangentCoordChange I x y x
<VAR>a b m n p✝ p r i : ℕ<VAR>hr : ¬p ∣ r<GOAL>(p * i + r).factorization p = 0
<VAR>a b m n p✝ p r i : ℕ<VAR>hr : ¬p ∣ r<GOAL>¬p ∣ p * i + r
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X✝ X : T<VAR>U V : Under X<VAR>f g : U ⟶ V<VAR>left✝¹ : U.left ⟶ V.left<VAR>b : U.right ⟶ V.right<VAR>w✝¹ : (Functor.fromPUnit X).map left✝¹ ≫ V.hom = U.hom ≫ (𝟭 T).map b<VAR>left✝ : U.left ⟶ V.left<VAR>e : U.right ⟶ V.right<VAR>w✝ : (Functor.fromPUnit X).map left✝ ≫ V.hom = U.hom ≫ (𝟭 T).map e<VAR>h : { left := left✝¹, right := b, w := w✝¹ }.right = { left := left✝, right := e, w := w✝ }.right<GOAL>left✝¹ = left✝
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : UniformSpace β<VAR>K : Set α<VAR>V : Set (β × β)<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>h : TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p<GOAL>Tendsto F p (𝓝 f)
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : UniformSpace β<VAR>K : Set α<VAR>V : Set (β × β)<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>h : TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p<GOAL>∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : UniformSpace β<VAR>K✝ : Set α<VAR>V : Set (β × β)<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>h : TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p<VAR>K : Set α<VAR>hK : IsCompact K<GOAL>TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : UniformSpace β<VAR>K✝ : Set α<VAR>V : Set (β × β)<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>h : TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p<VAR>K : Set α<VAR>hK : IsCompact K<GOAL>TendstoLocallyUniformlyOn (fun i a => (F i) a) (⇑f) p K
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>h : Module.rank R M = 0<GOAL>toNat (Module.rank R M) = 0
<VAR>α : Type u_1<VAR>s : Set ℝ<VAR>t : Set ℝ≥0<VAR>u : Set ℝ≥0∞<VAR>h : s.OrdConnected<GOAL>(ENNReal.ofReal '' s).OrdConnected
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝² : Zero R<VAR>inst✝¹ : Zero M<VAR>inst✝ : SMulWithZero R M<VAR>s : Set α<VAR>r : α → R<VAR>f : α → M<VAR>a : α<VAR>h✝ : a ∈ s<GOAL>r a • f a = r a • f a
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝² : Zero R<VAR>inst✝¹ : Zero M<VAR>inst✝ : SMulWithZero R M<VAR>s : Set α<VAR>r : α → R<VAR>f : α → M<VAR>a : α<VAR>h✝ : a ∉ s<GOAL>0 = 0 • f a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<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>f g : E → F<VAR>p✝ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r' : ℝ≥0∞<VAR>n✝ m✝ : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>x : E<VAR>m : ℕ<VAR>hm : m ∉ ?m.378525<GOAL>((p m) fun x_1 => x) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<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>f g : E → F<VAR>p✝ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r' : ℝ≥0∞<VAR>n✝ m✝ : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>x : E<VAR>m : ℕ<VAR>hm : ?m.378946 ≤ m<GOAL>((p m) fun x_1 => x) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<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>f g : E → F<VAR>p✝ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r' : ℝ≥0∞<VAR>n✝ m : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>x : E<GOAL>ℕ
<VAR>a b c : ℕ<VAR>P : ℕ → Prop<VAR>h✝ : ∀ (n : ℕ), P (n + 1) → P n<VAR>seed : ℕ<VAR>h : ∀ (n : ℕ), P (n + 1) → P n<VAR>hs : P seed<VAR>hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y<VAR>n : ℕ<GOAL>P n
<VAR>a b c : ℕ<VAR>P : ℕ → Prop<VAR>h✝ : ∀ (n : ℕ), P (n + 1) → P n<VAR>seed : ℕ<VAR>h : ∀ (n : ℕ), P (n + 1) → P n<VAR>hs : P seed<VAR>hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y<VAR>n : ℕ<GOAL>{x | P x}.Finite → False
<VAR>a b c : ℕ<VAR>P : ℕ → Prop<VAR>h✝ : ∀ (n : ℕ), P (n + 1) → P n<VAR>seed : ℕ<VAR>h : ∀ (n : ℕ), P (n + 1) → P n<VAR>hs : P seed<VAR>hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y<VAR>n : ℕ<VAR>hf : {x | P x}.Finite<GOAL>False
<VAR>a b c : ℕ<VAR>P : ℕ → Prop<VAR>h✝ : ∀ (n : ℕ), P (n + 1) → P n<VAR>seed : ℕ<VAR>h : ∀ (n : ℕ), P (n + 1) → P n<VAR>hs : P seed<VAR>hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y<VAR>n : ℕ<VAR>hf : {x | P x}.Finite<VAR>m : ℕ<VAR>hP : m ∈ {x | P x}<VAR>hm : ∀ a' ∈ {x | P x}, id m ≤ id a' → id m = id a'<GOAL>False
<VAR>a b c : ℕ<VAR>P : ℕ → Prop<VAR>h✝ : ∀ (n : ℕ), P (n + 1) → P n<VAR>seed : ℕ<VAR>h : ∀ (n : ℕ), P (n + 1) → P n<VAR>hs : P seed<VAR>hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y<VAR>n : ℕ<VAR>hf : {x | P x}.Finite<VAR>m : ℕ<VAR>hP : m ∈ {x | P x}<VAR>hm : ∀ a' ∈ {x | P x}, id m ≤ id a' → id m = id a'<VAR>y : ℕ<VAR>hl : m < y<VAR>hy : P y<GOAL>False