ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>inst✝⁷ : Monoid M<VAR>inst✝⁶ : MulAction M α<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MulAction G α<VAR>g✝ : G<VAR>a✝ b : α<VAR>inst✝³ : Group H<VAR>inst✝² : MulAction G H<VAR>inst✝¹ : SMulCommClass G H H<VAR>inst✝ : IsScalarTower G H H<VAR>g : G<VAR>a : H<VAR>n : ℤ<GOAL>(g • a) ^ n = g ^ n • a ^ n
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<GOAL>(p.concat h).darts = p.darts.concat { toProd := (v, w), adj := h }
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>inst✝ : Subsingleton ↥H<GOAL>H = ⊥
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>inst✝ : Subsingleton ↥H<GOAL>∀ x ∈ H, x = 1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>inst✝ : Subsingleton ↥H<VAR>y : G<VAR>hy : y ∈ H<GOAL>y = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>b : β<VAR>p : β → Prop<VAR>s : (x : β) → x = b ∨ p x → Set α<GOAL>⋂ x, ⋂ (h : x = b ∨ p x), s x h = s b ⋯ ∩ ⋂ x, ⋂ (h : p x), s x ⋯
<VAR>p : ℝ<GOAL>(Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p
<VAR>p : ℝ<VAR>hp : 0 ≤ p<GOAL>(Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p
<VAR>p : ℝ<VAR>hp : p < 0<GOAL>(Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hg : ConcaveOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>hgi : Integrable (g ∘ f) μ<GOAL>∫ (x : α), g (f x) ∂μ ≤ g (∫ (x : α), f x ∂μ)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>K : SimplicialComplex 𝕜 E<VAR>s t : Finset E<VAR>x : E<VAR>hs : s ∈ K.faces<GOAL>(convexHull 𝕜) ↑s ⊆ K.space
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>K : SimplicialComplex 𝕜 E<VAR>s t : Finset E<VAR>x : E<VAR>hs : s ∈ K.faces<GOAL>(convexHull 𝕜) ↑s = (convexHull 𝕜) ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ≃o β<VAR>a b : β<GOAL>⇑e ⁻¹' Ioo a b = Ioo (e.symm a) (e.symm b)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>f₁ : ι → κ<VAR>f₂ : (i : ι) → σ i → τ (f₁ i)<GOAL>(∀ (i : ι), Continuous fun a => Sigma.map f₁ f₂ ⟨i, a⟩) ↔ ∀ (i : ι), Continuous (f₂ i)
<VAR>M : Type u<VAR>inst✝² : Monoid M<VAR>α : Type v<VAR>inst✝¹ : MulAction M α<VAR>β : Type u_1<VAR>inst✝ : MulAction M β<VAR>y : α × β<VAR>g : M<GOAL>((fun m => m • y) g).1 ∈ orbit M y.1
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle x (x + y)).sin = ‖y‖ / ‖x + y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle x (x + y)).sign = 1<GOAL>(o.oangle x (x + y)).sin = ‖y‖ / ‖x + y‖
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>e : α ≃ β<VAR>f : Filter β<GOAL>map (⇑e) (map (⇑e.symm) f) = map (⇑e) (comap (⇑e) f)
<VAR>α β : Type u<VAR>n : ℕ<GOAL>succ ↑n = ↑n + 1
<VAR>α β : Type u<VAR>n : ℕ<GOAL>↑n.succ = ↑n + 1
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<GOAL>∀ (l : List α), foldr cons [] l = l
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>s : Submonoid M<VAR>x : M × N<GOAL>x ∈ s.prod ⊤ ↔ x ∈ comap (MonoidHom.fst M N) s
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>this : Nat.choose 4 2 = 6<GOAL>bernoulli' 4 = -1 / 30
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>this : Nat.choose 4 2 = 6<GOAL>1 - ∑ k ∈ range 4, ↑(Nat.choose 4 k) / (↑4 - ↑k + 1) * bernoulli' k = -1 / 30
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s✝ : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>s : β → Set α<VAR>S : Set β<VAR>h : DirectedOn (s ⁻¹'o fun x x_1 => x ≥ x_1) S<VAR>ne : S.Nonempty<VAR>t : Set α<GOAL>t ∈ ⨅ i ∈ S, 𝓟 (s i) ↔ ∃ i ∈ S, s i ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s✝ : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>s : β → Set α<VAR>S : Set β<VAR>h : DirectedOn (s ⁻¹'o fun x x_1 => x ≥ x_1) S<VAR>ne : S.Nonempty<VAR>t : Set α<GOAL>DirectedOn ((fun i => 𝓟 (s i)) ⁻¹'o fun x x_1 => x ≥ x_1) S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s✝ : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>s : β → Set α<VAR>S : Set β<VAR>h : Directed (fun x x_1 => x ≥ x_1) (s ∘ Subtype.val)<VAR>ne : S.Nonempty<VAR>t : Set α<GOAL>Directed (fun x x_1 => x ≥ x_1) ((fun i => 𝓟 (s i)) ∘ Subtype.val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s✝ : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>s : β → Set α<VAR>S : Set β<VAR>h : Directed (fun x x_1 => x ≥ x_1) (s ∘ Subtype.val)<VAR>ne : S.Nonempty<VAR>t : Set α<GOAL>∀ ⦃x y : Set α⦄, x ≥ y → 𝓟 x ≥ 𝓟 y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>f : α → β<VAR>h : Injective f<VAR>b : β<VAR>w : b ∉ Set.range f<GOAL>b ∉ map { toFun := f, inj' := h } univ
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>hst : G.IsUniform ε s t<GOAL>↑(SimpleGraph.badVertices G ε s t).card ≤ ↑s.card * ε
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>hst : G.IsUniform ε s t<VAR>hε : ε ≤ 1<GOAL>↑(SimpleGraph.badVertices G ε s t).card ≤ ↑s.card * ε
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>hst : G.IsUniform ε s t<VAR>hε : ε ≤ 1<VAR>h : ↑s.card * ε < ↑(SimpleGraph.badVertices G ε s t).card<GOAL>False
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>hst : G.IsUniform ε s t<VAR>hε : ε ≤ 1<VAR>h : ↑s.card * ε < ↑(SimpleGraph.badVertices G ε s t).card<VAR>this : |↑(G.edgeDensity (SimpleGraph.badVertices G ε s t) t) - ↑(G.edgeDensity s t)| < ε<GOAL>False
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>hst : G.IsUniform ε s t<VAR>hε : ε ≤ 1<VAR>h : ↑s.card * ε < ↑(SimpleGraph.badVertices G ε s t).card<VAR>this : ↑(G.edgeDensity (SimpleGraph.badVertices G ε s t) t) - ↑(G.edgeDensity s t) < ε ∧ ↑(G.edgeDensity s t) - ↑(G.edgeDensity (SimpleGraph.badVertices G ε s t) t) < ε<GOAL>False
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : AddMonoid G<VAR>A : Type u₃<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra k A<VAR>B : Type u_3<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra k B<VAR>F : k[G] →ₐ[k] A<VAR>f : MonoidAlgebra k G<GOAL>F f = sum f fun a b => b • F (single a 1)
<VAR>n : ℕ<GOAL>0 < n.size ↔ 0 < n
<VAR>n : ℕ<GOAL>2 ^ 0 ≤ n ↔ 0 < n
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : NormedLinearOrderedField K<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝² : FloorRing K<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : Unique ι<VAR>k : K<VAR>x✝ : ?m.166713<GOAL>(?m.166719.repr ↑(floor (Basis.singleton ι K) k)) x✝ = (?m.166719.repr ↑⌊k⌋) x✝
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>I J : HasZeroMorphisms C<VAR>w : ∀ (X Y : C), Zero.zero = Zero.zero<GOAL>I = J
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>I J : HasZeroMorphisms C<VAR>w : ∀ (X Y : C), Zero.zero = Zero.zero<VAR>this : zero = zero<GOAL>I = J
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>t : RBNode α<GOAL>All (fun a => p a ∧ q a) t ↔ All p t ∧ All q t
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>(Icc a b).card = ↑b + 1 - ↑a
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁴ : Fintype l<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Unique ι<VAR>inst✝ : NonUnitalSeminormedRing α<VAR>A : Matrix l m α<VAR>v : m → α<GOAL>‖A *ᵥ v‖₊ ≤ ‖A‖₊ * ‖v‖₊
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁴ : Fintype l<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Unique ι<VAR>inst✝ : NonUnitalSeminormedRing α<VAR>A : Matrix l m α<VAR>v : m → α<GOAL>‖col (Fin 1) (A *ᵥ v)‖₊ ≤ ‖A‖₊ * ‖col (Fin 1) v‖₊
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>f : 𝕜 → B<VAR>x : 𝕜<VAR>hx : x ∈ Ioc a (a + p)<GOAL>liftIoc p a f ↑x = f x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>f : 𝕜 → B<VAR>x : 𝕜<VAR>hx : x ∈ Ioc a (a + p)<VAR>this : (equivIoc p a) ↑x = ⟨x, hx⟩<GOAL>liftIoc p a f ↑x = f x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>f : 𝕜 → B<VAR>x : 𝕜<VAR>hx : x ∈ Ioc a (a + p)<VAR>this : (equivIoc p a) ↑x = ⟨x, hx⟩<GOAL>(Ioc a (a + p)).restrict f ⟨x, hx⟩ = f x
<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>A : C<VAR>inst✝ : S.HasHomology<VAR>k : A ⟶ S.X₂<VAR>x : A ⟶ S.X₁<VAR>hx : k = x ≫ S.f<GOAL>k ≫ S.g = 0
<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>A : C<VAR>inst✝ : S.HasHomology<VAR>k : A ⟶ S.X₂<VAR>x : A ⟶ S.X₁<VAR>hx : k = x ≫ S.f<GOAL>S.liftCycles k ⋯ ≫ S.leftHomologyπ ≫ S.leftHomologyIso.hom = 0
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 →ᵃ[𝕜] E<VAR>a b : E<VAR>L : Filter 𝕜<VAR>s : Set 𝕜<VAR>x : 𝕜<GOAL>HasDerivAtFilter (⇑f) (f.linear 1) x L
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 →ᵃ[𝕜] E<VAR>a b : E<VAR>L : Filter 𝕜<VAR>s : Set 𝕜<VAR>x : 𝕜<GOAL>HasDerivAtFilter (⇑f.linear + fun x => f 0) (f.linear 1) x L
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>G H : C ⥤ D<VAR>α : G ⟶ H<VAR>F : D ⥤ E<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(G ⋙ F).map f ≫ (fun X => F.map (α.app X)) Y = (fun X => F.map (α.app X)) X ≫ (H ⋙ F).map f
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>A : ι → Submodule R M<VAR>h : IsInternal A<VAR>α : ι → Type u_2<VAR>v : (i : ι) → Basis (α i) R ↥(A i)<VAR>x : M<VAR>i : ι<VAR>a : α i<VAR>hx : x ∈ A i<GOAL>((h.collectedBasis v).repr x) ⟨i, a⟩ = ((v i).repr ⟨x, hx⟩) a
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>A : ι → Submodule R M<VAR>h : IsInternal A<VAR>α : ι → Type u_2<VAR>v : (i : ι) → Basis (α i) R ↥(A i)<VAR>x : M<VAR>i : ι<VAR>a : α i<VAR>hx : x ∈ A i<GOAL>((sigmaFinsuppLequivDFinsupp R).symm (DFinsupp.mapRange (fun i => ⇑(v i).repr) ⋯ (↑(LinearEquiv.ofBijective (coeLinearMap A) h).symm x))) ⟨i, a⟩ = ((v i).repr ⟨x, hx⟩) a
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num ∣ p
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>p / gcd p q ∣ p
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>(q / gcd p q).leadingCoeff⁻¹ ≠ 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>L₂ : Type u_1<VAR>M₂ : Type u_2<VAR>inst✝⁶ : LieRing L₂<VAR>inst✝⁵ : LieAlgebra R L₂<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L₂ M₂<VAR>inst✝¹ : LieModule R L₂ M₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>g : M →ₗ[R] M₂<VAR>hf : Surjective ⇑f<VAR>hg : Surjective ⇑g<VAR>hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆<VAR>inst✝ : LieModule.IsNilpotent R L M<VAR>k : ℕ<VAR>hk : lowerCentralSeries R L M k = ⊥<GOAL>LieModule.IsNilpotent R L₂ M₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>L₂ : Type u_1<VAR>M₂ : Type u_2<VAR>inst✝⁶ : LieRing L₂<VAR>inst✝⁵ : LieAlgebra R L₂<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L₂ M₂<VAR>inst✝¹ : LieModule R L₂ M₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>g : M →ₗ[R] M₂<VAR>hf : Surjective ⇑f<VAR>hg : Surjective ⇑g<VAR>hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆<VAR>inst✝ : LieModule.IsNilpotent R L M<VAR>k : ℕ<VAR>hk : lowerCentralSeries R L M k = ⊥<GOAL>lowerCentralSeries R L₂ M₂ k = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>L₂ : Type u_1<VAR>M₂ : Type u_2<VAR>inst✝⁶ : LieRing L₂<VAR>inst✝⁵ : LieAlgebra R L₂<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L₂ M₂<VAR>inst✝¹ : LieModule R L₂ M₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>g : M →ₗ[R] M₂<VAR>hf : Surjective ⇑f<VAR>hg : Surjective ⇑g<VAR>hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆<VAR>inst✝ : LieModule.IsNilpotent R L M<VAR>k : ℕ<VAR>hk : ↑(lowerCentralSeries R L M k) = ↑⊥<GOAL>↑(lowerCentralSeries R L₂ M₂ k) = ↑⊥
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>1 ∈ Set.range fun p => ∑ i : α, a i * b i ^ p
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∃ a_1, ∑ i : α, a i * b i ^ a_1 ≤ 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∃ b_1, 1 ≤ ∑ i : α, a i * b i ^ b_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x✝ : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x<VAR>hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n<VAR>hf0 : Summable fun n => f n x₀<VAR>x : E<VAR>A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<GOAL>HasFDerivAt (fun y => ∑' (n : α), f n y) (∑' (n : α), f' n x) x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>inst✝ : AddGroup β<VAR>f g : α → β<VAR>l : Filter α<VAR>h : f - g =ᶠ[l] 0<GOAL>f =ᶠ[l] g
<VAR>n : ℕ<VAR>x : ↑I<GOAL>∑ k : Fin (n + 1), (bernstein n ↑k) x = 1
<VAR>n : ℕ<VAR>x : ↑I<VAR>this : ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial ℝ n ν = 1<GOAL>∑ k : Fin (n + 1), (bernstein n ↑k) x = 1
<VAR>n : ℕ<VAR>x : ↑I<VAR>this : (Polynomial.aeval ↑x) (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial ℝ n ν) = (Polynomial.aeval ↑x) 1<GOAL>∑ k : Fin (n + 1), (bernstein n ↑k) x = 1
<VAR>n : ℕ<VAR>x : ↑I<VAR>this : ∑ x_1 : Fin (n + 1), Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = 1<GOAL>∑ k : Fin (n + 1), (bernstein n ↑k) x = 1
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f.eraseLead ≠ 0<GOAL>0 < f.natDegree
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f.eraseLead ≠ 0<VAR>h₂ : ¬0 < f.natDegree<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : (C (f.coeff 0)).eraseLead ≠ 0<VAR>h₂ : ¬0 < f.natDegree<GOAL>False
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>L : Filter F<VAR>h : ¬DifferentiableAt 𝕜 f x<GOAL>∇ f x = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>I : R →+* R<VAR>B F : M →ₗ[R] M →ₛₗ[I] M₃<VAR>B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃<VAR>B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] M₃<VAR>f f' : M →ₗ[R] M₁<VAR>g g' : M₁ →ₗ[R] M<VAR>h : B.IsAdjointPair B' f g<VAR>h' : B.IsAdjointPair B' f' g'<VAR>x : M<VAR>x✝ : M₁<GOAL>(B' ((f + f') x)) x✝ = (B x) ((g + g') x✝)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤<GOAL>0 < μ {x | ∫⁻ (a : α), f a ∂μ ≤ f x}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f g : ↥(lp (fun i => ℝ) ⊤)<VAR>n : ℕ<VAR>C : ℝ<VAR>inst✝ : MetricSpace α<VAR>x : ℕ → α<VAR>a✝ b✝ : α<VAR>H : DenseRange x<VAR>a b : α<GOAL>dist (embeddingOfSubset x a) (embeddingOfSubset x b) = dist a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f g : ↥(lp (fun i => ℝ) ⊤)<VAR>n : ℕ<VAR>C : ℝ<VAR>inst✝ : MetricSpace α<VAR>x : ℕ → α<VAR>a✝ b✝ : α<VAR>H : DenseRange x<VAR>a b : α<VAR>e : ℝ<VAR>epos : 0 < e<GOAL>dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f g : ↥(lp (fun i => ℝ) ⊤)<VAR>n✝ : ℕ<VAR>C : ℝ<VAR>inst✝ : MetricSpace α<VAR>x : ℕ → α<VAR>a✝ b✝ : α<VAR>H : DenseRange x<VAR>a b : α<VAR>e : ℝ<VAR>epos : 0 < e<VAR>n : ℕ<VAR>hn : dist a (x n) < e / 2<GOAL>dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f g : ↥(lp (fun i => ℝ) ⊤)<VAR>n✝ : ℕ<VAR>C✝ : ℝ<VAR>inst✝ : MetricSpace α<VAR>x : ℕ → α<VAR>a✝ b✝ : α<VAR>H : DenseRange x<VAR>a b : α<VAR>e : ℝ<VAR>epos : 0 < e<VAR>n : ℕ<VAR>hn : dist a (x n) < e / 2<VAR>C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n<GOAL>dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f g : ↥(lp (fun i => ℝ) ⊤)<VAR>n✝ : ℕ<VAR>C✝ : ℝ<VAR>inst✝ : MetricSpace α<VAR>x : ℕ → α<VAR>a✝ b✝ : α<VAR>H : DenseRange x<VAR>a b : α<VAR>e : ℝ<VAR>epos : 0 < e<VAR>n : ℕ<VAR>hn : dist a (x n) < e / 2<VAR>C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n<VAR>this : dist a b ≤ dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e<GOAL>dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>x₁ x₂ : M<VAR>x✝ : ∃ c, c • x₁ = c • x₂<VAR>c : ↥S<VAR>h : f (c • x₁) = f (c • x₂)<GOAL>f x₁ = f x₂
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>x₁ x₂ : M<VAR>x✝ : ∃ c, c • x₁ = c • x₂<VAR>c : ↥S<VAR>h : ((algebraMap R (Module.End R M')) ↑c) (f x₁) = ((algebraMap R (Module.End R M')) ↑c) (f x₂)<GOAL>f x₁ = f x₂
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v w : V<VAR>e : Sym2 V<VAR>H : SimpleGraph V<VAR>s✝ s₁ s₂ s : Set (Sym2 V)<VAR>x✝¹ x✝ : V<GOAL>(G.deleteEdges s).Adj x✝¹ x✝ ↔ (G.deleteEdges (s ∩ G.edgeSet)).Adj x✝¹ x✝
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.121039, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : CategoryWithHomology C<VAR>K : CochainComplex C ℤ<VAR>A : C<VAR>n i : ℤ<VAR>f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i<VAR>j : ℤ<VAR>hj : (up ℤ).next i = j<VAR>hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0<VAR>i' : ℤ<VAR>hi' : n + i = i'<VAR>j' : ℤ<VAR>hj' : (up ℤ).next i' = j'<GOAL>(f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) ≫ K.d i' j' = 0