ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x y✝ : E<VAR>s t : Set E<VAR>h : 𝓝[s] x ≤ 𝓝[t] x<VAR>y : E<VAR>c : ℕ → 𝕜<VAR>d : ℕ → E<VAR>ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s<VAR>ctop : Tendsto (fun n => ‖c n‖) atTop atTop<VAR>clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)<GOAL>Tendsto (fun n => x + d n) atTop (𝓝[t] x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x y✝ : E<VAR>s t : Set E<VAR>h : 𝓝[s] x ≤ 𝓝[t] x<VAR>y : E<VAR>c : ℕ → 𝕜<VAR>d : ℕ → E<VAR>ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s<VAR>ctop : Tendsto (fun n => ‖c n‖) atTop atTop<VAR>clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)<GOAL>Tendsto (fun a => x + d a) atTop (𝓝 x)
<VAR>x✝ y : ℂ<VAR>x : ℝ<GOAL>(starRingEnd ℂ) (tan ↑x) = tan ↑x
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>b : BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>IsPullback b.inl 0 b.snd 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>b : BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>IsPullback (b.inl ≫ b.fst) 0 0 (0 ≫ 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<VAR>h : SuperpolynomialDecay l k (k * f)<VAR>x : α<VAR>hx : k x ≠ 0<GOAL>(k⁻¹ * (k * f)) x = f x
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>s✝ : Multiset α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : Multiset α<VAR>hf : Set.InjOn f {x | x ∈ s}<VAR>x : α<VAR>H : x ∈ s<GOAL>count (f x) (map f s) = count x s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>s✝ : Multiset α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : Multiset α<VAR>hf : Set.InjOn f {x | x ∈ s}<VAR>x : α<VAR>H : x ∈ s<GOAL>count x (filter (fun a => f x = f a) s) = card (filter (fun a => f x = f a) s)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : Preorder β<VAR>l : Filter α<VAR>p : β → Prop<VAR>f : α → β<VAR>hf : Tendsto f l atBot<VAR>h_evtl : ∀ᶠ (x : β) in atBot, p x<GOAL>∀ᶠ (x : α) in l, ∀ y ≤ f x, p y
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : Preorder β<VAR>l : Filter α<VAR>p : β → Prop<VAR>f : α → β<VAR>hf : Tendsto f l atBot<VAR>h_evtl : ∀ᶠ (x : β) in atBot, ∀ y ≤ x, p y<GOAL>∀ᶠ (x : α) in l, ∀ y ≤ f x, p y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs ys xs' : List α<VAR>hx : xs' ~ xs<VAR>h : xs' <+ ys<GOAL>xs.sym2 <+~ ys.sym2
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<GOAL>exterior s ⊆ exterior t ↔ 𝓝ˢ s ≤ 𝓝ˢ t
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<GOAL>exterior s ⊆ exterior t → 𝓝ˢ s ≤ 𝓝ˢ t
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<GOAL>exterior s ⊆ exterior t → ∀ (x : Set α), exterior t ⊆ x → exterior s ⊆ x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : IsScalarTower ℝ 𝕜 E<VAR>hs₀ : Balanced 𝕜 s<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : Absorbent ℝ s<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hs : IsOpen s<GOAL>(gaugeSeminorm hs₀ hs₁ hs₂).ball 0 1 = s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : IsScalarTower ℝ 𝕜 E<VAR>hs₀ : Balanced 𝕜 s<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : Absorbent ℝ s<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hs : IsOpen s<GOAL>{y | (gaugeSeminorm hs₀ hs₁ hs₂) y < 1} = s
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>a : α<VAR>inst✝ : IsStronglyAtomic α<VAR>ha : (Set.Ici a).Infinite<VAR>hfin : {x | a ⋖ x}.Finite<GOAL>∃ b, a ⋖ b ∧ (Set.Ici b).Infinite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>a : α<VAR>inst✝ : IsStronglyAtomic α<VAR>ha : (Set.Ici a).Infinite<VAR>hfin : {x | a ⋖ x}.Finite<VAR>h : ∀ (b : α), a ⋖ b → ¬(Set.Ici b).Infinite<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>a : α<VAR>inst✝ : IsStronglyAtomic α<VAR>ha : (Set.Ici a).Infinite<VAR>hfin : {x | a ⋖ x}.Finite<VAR>h : ∀ (b : α), a ⋖ b → ¬(Set.Ici b).Infinite<VAR>b : α<VAR>hb : b ∈ Set.Ici a \ {a}<GOAL>b ∈ ⋃ i ∈ {x | a ⋖ x}, Set.Ici i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>a : α<VAR>inst✝ : IsStronglyAtomic α<VAR>ha : (Set.Ici a).Infinite<VAR>hfin : {x | a ⋖ x}.Finite<VAR>h : ∀ (b : α), a ⋖ b → ¬(Set.Ici b).Infinite<VAR>b : α<VAR>hb : b ∈ Set.Ici a \ {a}<VAR>x : α<VAR>hax : a ⋖ x<VAR>hxb : x ≤ b<GOAL>b ∈ ⋃ i ∈ {x | a ⋖ x}, Set.Ici i
<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>F : ι → X → α<VAR>x₀ : X<VAR>u : α → β<VAR>hu : UniformInducing u<GOAL>EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x => u ∘ x) ∘ F) x₀
<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>F : ι → X → α<VAR>x₀ : X<VAR>u : α → β<VAR>hu : UniformInducing u<VAR>this : Inducing (⇑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)<GOAL>EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x => u ∘ x) ∘ F) x₀
<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>F : ι → X → α<VAR>x₀ : X<VAR>u : α → β<VAR>hu : UniformInducing u<VAR>this : Inducing (⇑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)<GOAL>ContinuousAt ((⇑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun) ∘ ⇑UniformFun.ofFun ∘ swap F) x₀ ↔ ContinuousAt (⇑UniformFun.ofFun ∘ swap ((fun x => u ∘ x) ∘ F)) x₀
<VAR>A : Type u'<VAR>inst✝¹² : Category.{v', u'} A<VAR>inst✝¹¹ : ConcreteCategory A<VAR>inst✝¹⁰ : HasFunctorialSurjectiveInjectiveFactorization A<VAR>inst✝⁹ : (coherentTopology CompHaus).WEqualsLocallyBijective A<VAR>inst✝⁸ : HasSheafify (coherentTopology CompHaus) A<VAR>inst✝⁷ : (coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)<VAR>inst✝⁶ : Balanced (Sheaf (coherentTopology CompHaus) A)<VAR>inst✝⁵ : PreservesFiniteProducts (CategoryTheory.forget A)<VAR>inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A<VAR>X Y : Condensed A<VAR>f : X ⟶ Y<VAR>inst✝³ : (extensiveTopology Stonean).WEqualsLocallyBijective A<VAR>inst✝² : HasSheafify (extensiveTopology Stonean) A<VAR>inst✝¹ : (extensiveTopology Stonean).HasSheafCompose (CategoryTheory.forget A)<VAR>inst✝ : Balanced (Sheaf (extensiveTopology Stonean) A)<GOAL>Epi f ↔ ∀ (S : Stonean), Function.Surjective ⇑(f.val.app (op S.compHaus))
<VAR>A : Type u'<VAR>inst✝¹² : Category.{v', u'} A<VAR>inst✝¹¹ : ConcreteCategory A<VAR>inst✝¹⁰ : HasFunctorialSurjectiveInjectiveFactorization A<VAR>inst✝⁹ : (coherentTopology CompHaus).WEqualsLocallyBijective A<VAR>inst✝⁸ : HasSheafify (coherentTopology CompHaus) A<VAR>inst✝⁷ : (coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)<VAR>inst✝⁶ : Balanced (Sheaf (coherentTopology CompHaus) A)<VAR>inst✝⁵ : PreservesFiniteProducts (CategoryTheory.forget A)<VAR>inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A<VAR>X Y : Condensed A<VAR>f : X ⟶ Y<VAR>inst✝³ : (extensiveTopology Stonean).WEqualsLocallyBijective A<VAR>inst✝² : HasSheafify (extensiveTopology Stonean) A<VAR>inst✝¹ : (extensiveTopology Stonean).HasSheafCompose (CategoryTheory.forget A)<VAR>inst✝ : Balanced (Sheaf (extensiveTopology Stonean) A)<GOAL>IsLocallySurjective (Presheaf.coherentExtensiveEquivalence.functor.map ((StoneanCompHaus.equivalence A).inverse.map f)) ↔ ∀ (S : Stonean), Function.Surjective ⇑(f.val.app (op S.compHaus))
<VAR>R✝ S✝ : Type u<VAR>inst✝¹⁸ : CommRing R✝<VAR>inst✝¹⁷ : CommRing S✝<VAR>M✝ : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝¹⁶ : CommRing R'<VAR>inst✝¹⁵ : CommRing S'<VAR>f : R✝ →+* S✝<VAR>inst✝¹⁴ : Algebra R✝ R'<VAR>inst✝¹³ : Algebra S✝ S'<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Rₚ : Type u_3<VAR>Sₚ : Type u_4<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : CommRing Rₚ<VAR>inst✝⁹ : CommRing Sₚ<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R Rₚ<VAR>inst✝⁶ : Algebra R Sₚ<VAR>inst✝⁵ : Algebra S Sₚ<VAR>inst✝⁴ : Algebra Rₚ Sₚ<VAR>inst✝³ : IsScalarTower R S Sₚ<VAR>inst✝² : IsScalarTower R Rₚ Sₚ<VAR>M : Submonoid R<VAR>inst✝¹ : IsLocalization M Rₚ<VAR>inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ<VAR>hRS : Finite R S<GOAL>Finite Rₚ Sₚ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s✝ t u s : Set α<GOAL>∀ (s : Set α), (fun s => s = ∅ ∨ s = univ) s → (fun s => s = ∅ ∨ s = univ) sᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (UpperSet α)<VAR>s t : UpperSet α<VAR>a : α<GOAL>Codisjoint ↑s ↑t ↔ Disjoint s t
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<GOAL>∫ (x : ℝ) in a..b, -f x ∂μ = -∫ (x : ℝ) in a..b, f x ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<GOAL>-∫ (a : ℝ) in Ioc a b, f a ∂μ - -∫ (a : ℝ) in Ioc b a, f a ∂μ = -(∫ (x : ℝ) in Ioc a b, f x ∂μ - ∫ (x : ℝ) in Ioc b a, f x ∂μ)
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ⇑(f' i j hij)<VAR>i : ι<GOAL>Function.Injective ⇑(of G (fun i j h => ⇑(f' i j h)) i)
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ⇑(f' i j hij)<VAR>i : ι<GOAL>∀ (x : G i), (of G (fun i j h => ⇑(f' i j h)) i) x = 0 → x = 0
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ⇑(f' i j hij)<VAR>i : ι<VAR>x : G i<VAR>hx : (of G (fun i j h => ⇑(f' i j h)) i) x = 0<GOAL>x = 0
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ⇑(f' i j hij)<VAR>i : ι<VAR>x : G i<VAR>hx : (of G (fun i j h => ⇑(f' i j h)) i) x = 0<VAR>j : ι<VAR>hij : i ≤ j<VAR>hfx : (f' i j hij) x = 0<GOAL>x = 0
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ⇑(f' i j hij)<VAR>i : ι<VAR>x : G i<VAR>hx : (of G (fun i j h => ⇑(f' i j h)) i) x = 0<VAR>j : ι<VAR>hij : i ≤ j<VAR>hfx : (f' i j hij) x = 0<GOAL>(f' i j hij) x = (f' i j hij) 0
<VAR>n : ℕ<GOAL>DifferentiableAt ℂ Gamma (↑n + 1)
<VAR>n m : ℕ<GOAL>↑n + 1 ≠ -↑m
<VAR>n m : ℕ<GOAL>¬↑n + 1 + ↑m = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s✝ : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (z : β × γ) in s ×ˢ Set.univ, f z ∂(κ ⊗ₖ η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>h : IsMaximal (eraseLast s).last (last s)<VAR>hs : s.length = 0<GOAL>last s = (eraseLast s).last
<VAR>n : ℕ<VAR>p : ℕ → Prop<VAR>h : 0 < sInf {m | p m}<GOAL>sInf {m | p m} + n = sInf {m | p (m - n)}
<VAR>n : ℕ<VAR>p : ℕ → Prop<VAR>h : 0 < sInf {m | p m}<GOAL>n ≤ sInf {m | p (m - n)}
<VAR>n : ℕ<VAR>p : ℕ → Prop<VAR>h : 0 < sInf {m | p m}<VAR>m : ℕ<VAR>hm : m ∈ {m | p m}<GOAL>n ≤ sInf {m | p (m - n)}
<VAR>n : ℕ<VAR>p : ℕ → Prop<VAR>h : 0 < sInf {m | p m}<VAR>m : ℕ<VAR>hm : m ∈ {m | p m}<GOAL>m + n ∈ {m | p (m - n)}
<VAR>n : ℕ<VAR>p : ℕ → Prop<VAR>h : 0 < sInf {m | p m}<VAR>m : ℕ<VAR>hm : m ∈ {m | p m}<VAR>b : ℕ<VAR>hb : b ∈ {m | p (m - n)}<VAR>hbn : b < n<GOAL>b - n ∈ {m | p m}
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>hst : ¬s ∩ t = ∅<GOAL>(condCount s) (t ∩ u) = (condCount (s ∩ t)) u * (condCount s) t
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>hst : ¬s ∩ t = ∅<GOAL>Measure.count (s ∩ t) ≠ 0
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>hst : ¬s ∩ t = ∅<GOAL>Measure.count (s ∩ t) ≠ ⊤
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>l : List α<GOAL>powersetCard 0 ⟦l⟧ = {0}
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝³ : DecidableRel G.Adj<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>inst✝ : Semiring α<VAR>n : ℕ<VAR>u v : V<GOAL>(adjMatrix α G ^ n) u v = ↑(Fintype.card ↑{p | p.length = n})
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝³ : DecidableRel G.Adj<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>inst✝ : Semiring α<VAR>n : ℕ<VAR>u v : V<GOAL>(adjMatrix α G ^ n) u v = ↑(G.finsetWalkLength n u v).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>h : Nat.card β = 0<GOAL>Nat.card α = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>h : Nat.card β = 0<VAR>h✝ : Finite β<GOAL>Nat.card α = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>h : Nat.card β = 0<VAR>h✝ : Infinite β<GOAL>Nat.card α = 0
<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<GOAL>HasSum (fun n => 1 / ↑n ^ k * ((fourier ↑n) ↑x + (-1) ^ k * (fourier (-↑n)) ↑x)) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))
<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<GOAL>(fun n => 1 / ↑n ^ k * ((fourier ↑n) ↑x + (-1) ^ k * (fourier (-↑n)) ↑x)) = fun n => 1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / ↑(-↑n) ^ k * (fourier (-↑n)) ↑x
<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<GOAL>-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) = -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) + 1 / ↑0 ^ k * (fourier 0) ↑x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>f : F[X]<VAR>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>hm : f.Monic<VAR>hi : Irreducible f<VAR>x✝ : ∃ n y, f = (expand F (q ^ n)) (X - C y)<VAR>n : ℕ<VAR>y : F<VAR>h : f = (expand F (q ^ n)) (X - C y)<GOAL>f.natSepDegree = 1
<VAR>n : ℕ<GOAL>antidiagonalTuple 1 n = [![n]]
<VAR>n : ℕ<GOAL>((range n).bind fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) ++ map (fun x => Fin.cons n x) (antidiagonalTuple 0 0) = [![n]]
<VAR>n : ℕ<GOAL>((range n).bind fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) ++ map (fun x => Fin.cons n x) (antidiagonalTuple 0 0) = [] ++ [![n]]
<VAR>n : ℕ<GOAL>((range n).bind fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) = []
<VAR>n : ℕ<GOAL>∀ x < n, antidiagonalTuple 0 (n - x) = []
<VAR>n x : ℕ<VAR>hx : x < n<GOAL>antidiagonalTuple 0 (n - x) = []
<VAR>x m : ℕ<VAR>hx : x < x + m + 1<GOAL>antidiagonalTuple 0 (x + m + 1 - x) = []
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<GOAL>(∀ (ib : ℝ), 0 < ib → ∃ ia, (∀ (c : ℝ≥0), l.RCond (ia c)) ∧ ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ closedBall y ib) ↔ ∀ ε > 0, ∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ ε
<VAR>b : ℂ<VAR>hb : b.re ≠ 0<VAR>c T : ℝ<VAR>this : b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2 = b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)<GOAL>‖cexp (-b * (↑T + ↑c * I) ^ 2)‖ = rexp (-(b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)))
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>A : Set X<GOAL>derivedSet (closure A) = derivedSet A
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>A : Set X<VAR>x : X<VAR>hx : x ∈ derivedSet (closure A)<GOAL>x ∈ derivedSet A
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>A : Set X<VAR>x : X<VAR>hx : ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen i → (i ∩ {x}ᶜ ∩ closure A).Nonempty<GOAL>∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen i → (i ∩ {x}ᶜ ∩ A).Nonempty
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>A : Set X<VAR>x : X<VAR>hx : ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen i → (i ∩ {x}ᶜ ∩ closure A).Nonempty<VAR>u : Set X<VAR>this : (u ∩ {x}ᶜ ∩ closure A).Nonempty<VAR>hu_open : IsOpen u<GOAL>(u ∩ {x}ᶜ ∩ A).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a b : α<VAR>inst✝ : LE α<VAR>h : IsMin a<VAR>b✝ : WithTop α<VAR>hb : b✝ ≤ ↑a<GOAL>↑a ≤ b✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a b : α<VAR>inst✝ : LE α<VAR>h : IsMin a<VAR>b✝ : WithTop α<VAR>hb : WithTop.toDual ↑a ≤ WithTop.toDual b✝<GOAL>↑a ≤ b✝
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<VAR>hs : s.OrdConnected<GOAL>(a • s).OrdConnected
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<VAR>hs : s.OrdConnected<GOAL>(a • ↑(upperClosure s) ∩ a • ↑(lowerClosure s)).OrdConnected
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>K₁ K₂ : Compacts G<VAR>hU : (interior U).Nonempty<GOAL>↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) ≤ ↑(index (↑K₁) U) / ↑(index (↑K₀) U) + ↑(index (↑K₂) U) / ↑(index (↑K₀) U)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>K₁ K₂ : Compacts G<VAR>hU : (interior U).Nonempty<GOAL>↑(index (↑(K₁ ⊔ K₂)) U) ≤ ↑(index (↑K₁) U) + ↑(index (↑K₂) U)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>K₁ K₂ : Compacts G<VAR>hU : (interior U).Nonempty<GOAL>0 < ↑(index (↑K₀) U)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.9092, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>e : S₁ ≅ S₂<GOAL>S₁.Exact ∧ Epi S₁.g ↔ S₂.Exact ∧ Epi S₂.g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.9092, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>this : Epi S₁.g ↔ Epi S₂.g<GOAL>S₁.Exact ∧ Epi S₁.g ↔ S₂.Exact ∧ Epi S₂.g
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>hG : ∀ (g : G), g ^ n = 1<GOAL>exponent G ≤ n
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>hG : ∀ (g : G), g ^ n = 1<GOAL>Nat.find ?hc ≤ n
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>hG : ∀ (g : G), g ^ n = 1<GOAL>ExponentExists G
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c < b<VAR>h₂ : a < d<VAR>x : α<GOAL>x ∈ Ioo a b ∪ Ioo c d ↔ x ∈ Ioo (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c < b<VAR>h₂ : a < d<VAR>x : α<GOAL>a < x ∧ x < b ∨ c < x ∧ x < d ↔ (a < x ∨ c < x) ∧ (x < b ∨ x < d)
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' S y<GOAL>slope f x y ≤ f'
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' S y<GOAL>S ∈ 𝓝[<] y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' S y<GOAL>∃ l ∈ Iio y, Ico l y ⊆ S
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ✝ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<GOAL>S₁.leftHomologyIso.hom ≫ homologyMap φ = leftHomologyMap φ ≫ S₂.leftHomologyIso.hom