ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : ConditionallyCompleteLattice α<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : Nonempty ι<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>g : ι → α<VAR>hg : BddAbove (range g)<GOAL>sSup (range (f ∘ g)) = sSup (range fun i => f (g i))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type ?u.705515<VAR>S' : Type ?u.705518<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type ?u.707949<VAR>S'' : Type ?u.707952<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>r : P.Ring<VAR>x : P.Cotangent<GOAL>(r • x).val = r • x.val
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type ?u.705515<VAR>S' : Type ?u.705518<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type ?u.707949<VAR>S'' : Type ?u.707952<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>r : P.Ring<VAR>x : P.Cotangent<GOAL>(P.σ ((algebraMap P.Ring S) r) - r) • x.val = 0
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>x : α<GOAL>[x] = l.rotate n ↔ [x] = l
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : (i : ι) → Zero (α i)<VAR>inst✝¹ : (i : ι) → Preorder (α i)<VAR>r : ι → ι → Prop<VAR>inst✝ : IsStrictOrder ι r<VAR>x y : Π₀ (i : ι), α i<VAR>hlt : x < y<GOAL>∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : (i : ι) → Zero (α i)<VAR>inst✝¹ : (i : ι) → Preorder (α i)<VAR>r : ι → ι → Prop<VAR>inst✝ : IsStrictOrder ι r<VAR>x y : Π₀ (i : ι), α i<VAR>hlt✝ : x < y<VAR>hle : ⇑x ≤ ⇑y<VAR>j : ι<VAR>hlt : x j < y j<GOAL>∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝² : Add α<VAR>inst✝¹ : MulOneClass α<VAR>inst✝ : RightDistribClass α<VAR>a b : α<GOAL>(a + 1) * b = a * b + b
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>s : Finset (Perm α)<VAR>h1 : ∀ f ∈ s, f.IsCycle<VAR>h2 : (↑s).Pairwise Disjoint<VAR>h0 : s.noncommProd id ⋯ = σ<GOAL>σ.cycleType = Multiset.map (Finset.card ∘ support) s.val
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>s : Finset (Perm α)<VAR>h1 : ∀ f ∈ s, f.IsCycle<VAR>h2 : (↑s).Pairwise Disjoint<VAR>h0 : s.noncommProd id ⋯ = σ<GOAL>Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val = Multiset.map (Finset.card ∘ support) s.val
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>s : Finset (Perm α)<VAR>h1 : ∀ f ∈ s, f.IsCycle<VAR>h2 : (↑s).Pairwise Disjoint<VAR>h0 : s.noncommProd id ⋯ = σ<GOAL>σ.cycleFactorsFinset = s
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>s : Finset (Perm α)<VAR>h1 : ∀ f ∈ s, f.IsCycle<VAR>h2 : (↑s).Pairwise Disjoint<VAR>h0 : s.noncommProd id ⋯ = σ<GOAL>(∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s).Pairwise Disjoint), s.noncommProd id ⋯ = σ
<VAR>Λ : ℂ → ℂ<VAR>hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s<VAR>L : ℂ<VAR>h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)<VAR>s : ℂ<VAR>hs' : s ≠ 1<GOAL>DifferentiableAt ℂ (Function.update (fun s => Λ s / s.Gammaℝ) 0 (L / 2)) s
<VAR>Λ : ℂ → ℂ<VAR>hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s<VAR>L : ℂ<VAR>h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)<VAR>s : ℂ<VAR>hs' : s ≠ 1<VAR>claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t<GOAL>DifferentiableAt ℂ (Function.update (fun s => Λ s / s.Gammaℝ) 0 (L / 2)) s
<VAR>Λ : ℂ → ℂ<VAR>hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s<VAR>L : ℂ<VAR>h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)<VAR>s : ℂ<VAR>hs' : s ≠ 1<VAR>claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t<VAR>claim2 : Tendsto (fun s => Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))<GOAL>DifferentiableAt ℂ (Function.update (fun s => Λ s / s.Gammaℝ) 0 (L / 2)) s
<VAR>Λ : ℂ → ℂ<VAR>hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s<VAR>L : ℂ<VAR>h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)<VAR>s : ℂ<VAR>hs' : s ≠ 1<VAR>claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t<VAR>claim2 : Tendsto (fun s => Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))<VAR>hs : s ≠ 0<GOAL>DifferentiableAt ℂ (Function.update (fun s => Λ s / s.Gammaℝ) 0 (L / 2)) s
<VAR>Λ : ℂ → ℂ<VAR>hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s<VAR>L : ℂ<VAR>h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)<VAR>claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t<VAR>claim2 : Tendsto (fun s => Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))<VAR>hs' : 0 ≠ 1<GOAL>DifferentiableAt ℂ (Function.update (fun s => Λ s / s.Gammaℝ) 0 (L / 2)) 0
<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).Nonempty → s.Nonempty
<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) → ∃ x, x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : a₁ < b₁<GOAL>Ioc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ b₁ ≤ b₂ ∧ a₂ ≤ a₁
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<GOAL>setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g
<VAR>σ : Type u<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : Applicative G<VAR>inst✝¹ : LawfulApplicative G<VAR>inst✝ : LawfulApplicative F<VAR>η : ApplicativeTransformation F G<VAR>α : Type u_1<VAR>β : Type u<VAR>f : α → F β<VAR>x : σ ⊕ α<GOAL>(fun {α} => η.app α) (Sum.traverse f x) = Sum.traverse ((fun {α} => η.app α) ∘ f) x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>hG : G.IsUniform ε s t<VAR>hε : ε ≤ 0<GOAL>↑s.card * ε ≤ ↑∅.card
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>hG : G.IsUniform ε s t<VAR>hε : ε ≤ 0<GOAL>↑t.card * ε ≤ ↑∅.card
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroObject C<VAR>X : C<VAR>h : IsSimpleOrder (Subobject X)<GOAL>Simple X
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set α<GOAL>IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen 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>s : Set α<GOAL>(∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen V ∧ ball x V ⊆ s
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a✝ b✝ c✝ a b c : α<GOAL>min (a / b) (a / c) = a / max b c
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>f✝ : R →+* S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>H : ∀ a ∈ I, f a = 0<VAR>hI : ker f ≤ I<GOAL>Function.Injective ⇑(Ideal.Quotient.lift I f H)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>f✝ : R →+* S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>H : ∀ a ∈ I, f a = 0<VAR>hI : ker f ≤ I<GOAL>∀ (x : R ⧸ I), (Ideal.Quotient.lift I f H) x = 0 → x = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>f✝ : R →+* S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>H : ∀ a ∈ I, f a = 0<VAR>hI : ker f ≤ I<VAR>u : R ⧸ I<VAR>hu : (Ideal.Quotient.lift I f H) u = 0<GOAL>u = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>f✝ : R →+* S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>H : ∀ a ∈ I, f a = 0<VAR>hI : ker f ≤ I<VAR>v : R<VAR>hu : (Ideal.Quotient.lift I f H) ((Ideal.Quotient.mk I) v) = 0<GOAL>(Ideal.Quotient.mk I) v = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>f✝ : R →+* S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>H : ∀ a ∈ I, f a = 0<VAR>hI : ker f ≤ I<VAR>v : R<VAR>hu : f v = 0<GOAL>(Ideal.Quotient.mk I) v = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>f✝ : R →+* S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>H : ∀ a ∈ I, f a = 0<VAR>hI : ker f ≤ I<VAR>v : R<VAR>hu : f v = 0<GOAL>v ∈ I
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : NoZeroSMulDivisors R P<VAR>x y : P<GOAL>spanSingleton S x = spanSingleton S y ↔ ∃ z, z • x = y
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : NoZeroSMulDivisors R P<VAR>x y : P<GOAL>⟨span R {x}, ⋯⟩ = ⟨span R {y}, ⋯⟩ ↔ span R {x} = span R {y}
<VAR>n k : ℕ<GOAL>(n - k) * (n - k + 1).ascFactorial k = (n - k).ascFactorial (k + 1)
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>((monomial n) a).coeff m = if n = m then a else 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>s : Finset ι<VAR>f : ι → α → E<GOAL>(∀ i ∈ s, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>s : Finset ι<VAR>f : ι → α → E<GOAL>(∀ i ∈ ∅, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ ∅, f i) = ∑ i ∈ ∅, setToFun μ T hT (f i)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>s : Finset ι<VAR>f : ι → α → E<GOAL>∀ ⦃a : ι⦄ {s : Finset ι}, a ∉ s → ((∀ i ∈ s, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)) → (∀ i ∈ insert a s, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ insert a s, f i) = ∑ i ∈ insert a s, setToFun μ T hT (f i)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : DecidableEq α<VAR>inst✝⁴ : DecidableEq β<VAR>inst✝³ : SemilatticeSup α<VAR>inst✝² : SemilatticeSup β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : SupHomClass F α β<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a b c : α<VAR>f : F<VAR>hf : Injective ⇑f<VAR>s t : Finset α<GOAL>map { toFun := ⇑f, inj' := hf } (s ⊻ t) = map { toFun := ⇑f, inj' := hf } s ⊻ map { toFun := ⇑f, inj' := hf } t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : DecidableEq α<VAR>s : Finset α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>inst✝ : Fintype α<VAR>h : ∀ (a : α), (filter (fun x => a ∈ x) B).card = n<GOAL>∑ s ∈ B, s.card = Fintype.card α * n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝¹ : NormedLinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<GOAL>SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), f =O[l] fun a => k a ^ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝¹ : NormedLinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<GOAL>(∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)) ↔ ∀ (z : ℤ), f =O[l] fun a => k a ^ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝¹ : NormedLinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<VAR>hk0 : ∀ᶠ (x : α) in l, k x ≠ 0<GOAL>(∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)) ↔ ∀ (z : ℤ), f =O[l] fun a => k a ^ z
<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>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : MDifferentiableWithinAt I I' f s x<VAR>hs : s ∈ 𝓝 x<GOAL>MDifferentiableAt I I' f 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>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : MDifferentiableWithinAt I I' f s x<VAR>hs : s ∈ 𝓝 x<VAR>this : s = univ ∩ s<GOAL>MDifferentiableAt I I' f x
<VAR>x✝ : PGame<VAR>inst✝ : x✝.Impartial<VAR>G : PGame := x✝<GOAL>x✝ ≈ nim x✝.grundyValue
<VAR>x✝ : PGame<VAR>inst✝ : x✝.Impartial<VAR>G : PGame := x✝<GOAL>∀ (i : (x✝ + nim x✝.grundyValue).LeftMoves), (x✝ + nim x✝.grundyValue).moveLeft i ‖ 0
<VAR>x✝ : PGame<VAR>inst✝ : x✝.Impartial<VAR>G : PGame := x✝<VAR>i : (x✝ + nim x✝.grundyValue).LeftMoves<GOAL>(x✝ + nim x✝.grundyValue).moveLeft i ‖ 0
<VAR>x✝ : PGame<VAR>inst✝ : x✝.Impartial<VAR>G : PGame := x✝<VAR>i : (x✝ + nim x✝.grundyValue).LeftMoves<GOAL>∀ (i : x✝.LeftMoves), (x✝ + nim x✝.grundyValue).moveLeft (toLeftMovesAdd (Sum.inl i)) ‖ 0
<VAR>x✝ : PGame<VAR>inst✝ : x✝.Impartial<VAR>G : PGame := x✝<VAR>i : (x✝ + nim x✝.grundyValue).LeftMoves<GOAL>∀ (i : (nim x✝.grundyValue).LeftMoves), (x✝ + nim x✝.grundyValue).moveLeft (toLeftMovesAdd (Sum.inr i)) ‖ 0
<VAR>G✝ : PGame<VAR>inst✝ : G✝.Impartial<VAR>a✝ : ∀ (y : (G : PGame) ×' G.Impartial), (invImage (fun x => PSigma.casesOn x fun G inst => G) instWellFoundedRelation).1 y ⟨G✝, inst✝⟩ → y.1 ≈ nim y.1.grundyValue<VAR>G : PGame := G✝<VAR>i₁ : G✝.LeftMoves<GOAL>(invImage (fun x => PSigma.casesOn x fun G inst => G) instWellFoundedRelation).1 ⟨G.moveLeft i₁, ⋯⟩ ⟨G✝, inst✝⟩
<VAR>G✝ : PGame<VAR>inst✝ : G✝.Impartial<VAR>a✝ : ∀ (y : (G : PGame) ×' G.Impartial), (invImage (fun x => PSigma.casesOn x fun G inst => G) instWellFoundedRelation).1 y ⟨G✝, inst✝⟩ → y.1 ≈ nim y.1.grundyValue<VAR>G : PGame := G✝<VAR>i₂ : (mk (Quotient.out G✝.grundyValue).α (Quotient.out G✝.grundyValue).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)).LeftMoves<VAR>h' : ∃ i, (G.moveLeft i).grundyValue = typein (Quotient.out G.grundyValue).r i₂<VAR>i : G.LeftMoves<VAR>hi : (G.moveLeft i).grundyValue = typein (Quotient.out G.grundyValue).r i₂<VAR>h✝ : h' = ⋯<GOAL>(invImage (fun x => PSigma.casesOn x fun G inst => G) instWellFoundedRelation).1 ⟨G.moveLeft i, ⋯⟩ ⟨G✝, inst✝⟩
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>i j : D.J<VAR>eq : (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i))<GOAL>D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>i j : D.J<VAR>eq : (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i))<VAR>this : D.t' i j i ≫ D.t' j i i ≫ D.t' i i j = 𝟙 (pullback (D.f i j) (D.f i i))<GOAL>D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>i j : D.J<VAR>eq : (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i))<VAR>this : (pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ inv (pullback.snd (D.f j i) (D.f j i))) ≫ (pullback.snd (D.f j i) (D.f j i) ≫ D.t j i ≫ inv (pullback.snd (D.f i i) (D.f i j))) ≫ pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i)) = 𝟙 (pullback (D.f i j) (D.f i i))<GOAL>D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>i j : D.J<VAR>eq : (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i))<VAR>this : pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ D.t j i ≫ inv (pullback.fst (D.f i j) (D.f i i)) = 𝟙 (pullback (D.f i j) (D.f i i))<GOAL>D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>i j : D.J<VAR>eq : (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i))<VAR>this : D.t i j ≫ D.t j i = (inv (pullback.fst (D.f i j) (D.f i i)) ≫ 𝟙 (pullback (D.f i j) (D.f i i))) ≫ pullback.fst (D.f i j) (D.f i i)<GOAL>D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))
<VAR>xl xr : Type u<GOAL>star ⧏ 0
<VAR>xl xr : Type u<GOAL>∃ j, ∀ (i : (star.moveRight j).LeftMoves), (star.moveRight j).moveLeft i ⧏ 0
<VAR>xl xr : Type u<GOAL>∀ (i : (star.moveRight default).LeftMoves), (star.moveRight default).moveLeft i ⧏ 0
<VAR>xl xr : Type u<GOAL>0 ⧏ star
<VAR>xl xr : Type u<GOAL>∃ i, ∀ (j : (star.moveLeft i).RightMoves), 0 ⧏ (star.moveLeft i).moveRight j
<VAR>xl xr : Type u<GOAL>∀ (j : (star.moveLeft default).RightMoves), 0 ⧏ (star.moveLeft default).moveRight j
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<GOAL>divided_by_X_pow_order ⋯ = 1
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<GOAL>X * divided_by_X_pow_order ⋯ = X
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I✝ I : Ideal A<VAR>hI : IsHomogeneous 𝒜 I<VAR>x : A<GOAL>x ∈ I ↔ ∀ (i : ι), ↑(((decompose 𝒜) x) i) ∈ I
<VAR>u : XgcdType<GOAL>u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.x * u.y
<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>hf : HasFPowerSeriesAt f pf x<VAR>hg : HasFPowerSeriesAt g pg x<GOAL>HasFPowerSeriesAt (f + g) (pf + pg) x
<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>hf : HasFPowerSeriesAt f pf x<VAR>hg : HasFPowerSeriesAt g pg x<VAR>r : ℝ≥0∞<VAR>hr : HasFPowerSeriesOnBall f pf x r ∧ HasFPowerSeriesOnBall g pg x r<GOAL>HasFPowerSeriesAt (f + g) (pf + pg) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>inst✝ : MeasurableSpace α<VAR>s : ℕ → Set α<VAR>hs : ∀ (n : ℕ), MeasurableSet (s n)<GOAL>MeasurableSet (liminf s atTop)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>inst✝ : IsProbabilityMeasure μ<GOAL>μ[|univ] = μ