ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>ιM : Type u_7<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : AddCommGroup L<VAR>inst✝¹¹ : Module R L<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁸ : Fintype ι<VAR>inst✝⁷ : Fintype ι'<VAR>inst✝⁶ : Fintype ιM<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : DecidableEq ι'<VAR>inst✝³ : Module.Free R M<VAR>inst✝² : Module.Finite R M<VAR>b : Basis ι R L<VAR>A : Type u_8<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<GOAL>(tensorProduct R A M M ∘ₗ baseChange A φ).polyCharpolyAux (basis A b) (Module.Free.chooseBasis A (TensorProduct R A M)) = Polynomial.map (MvPolynomial.map (algebraMap R A)) (φ.polyCharpolyAux b (Module.Free.chooseBasis R M))
<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>ιM : Type u_7<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : AddCommGroup L<VAR>inst✝¹¹ : Module R L<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁸ : Fintype ι<VAR>inst✝⁷ : Fintype ι'<VAR>inst✝⁶ : Fintype ιM<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : DecidableEq ι'<VAR>inst✝³ : Module.Free R M<VAR>inst✝² : Module.Finite R M<VAR>b : Basis ι R L<VAR>A : Type u_8<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<GOAL>(tensorProduct R A M M ∘ₗ baseChange A φ).polyCharpolyAux (basis A b) (Module.Free.chooseBasis A (TensorProduct R A M)) = (tensorProduct R A M M ∘ₗ baseChange A φ).polyCharpolyAux (basis A b) (basis A (Module.Free.chooseBasis R M))
<VAR>m✝ n✝ m : ℕ∞<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>m.toNat = n ↔ m = ↑n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : CommSemiring R<VAR>S : Set M<VAR>hS : closure S = ⊤<VAR>f : MonoidAlgebra R M<GOAL>∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : CommSemiring R<VAR>S : Set M<VAR>hS : closure S = ⊤<VAR>m : M<GOAL>∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = (of R M) m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : CommSemiring R<VAR>S : Set M<VAR>hS : closure S = ⊤<VAR>f g : MonoidAlgebra R M<VAR>ihf : ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = f<VAR>ihg : ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = g<GOAL>∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = f + g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : CommSemiring R<VAR>S : Set M<VAR>hS : closure S = ⊤<VAR>r : R<VAR>f : MonoidAlgebra R M<VAR>ih : ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = f<GOAL>∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = r • f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁵ : Zero α<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : SMulZeroClass α β<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : PosSMulMono α β<VAR>ha : 0 ≤ a<VAR>hb : b ≤ 0<GOAL>a • b ≤ 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : CancelMonoidWithZero M₀<VAR>a b c : M₀<GOAL>a * c = b * c ↔ a = b ∨ c = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : β → Bool<VAR>l : List α<VAR>f : α → List β<GOAL>countP p (l.bind f) = Nat.sum (map (countP p ∘ f) l)
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<GOAL>μ.mass ≠ 0 ↔ μ ≠ 0
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<GOAL>μ.mass = 0 ↔ μ = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>t t' : Set (ProjectiveSpectrum 𝒜)<VAR>r : A<GOAL>r ∈ vanishingIdeal t ⊔ vanishingIdeal t' → r ∈ vanishingIdeal (t ∩ t')
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>t t' : Set (ProjectiveSpectrum 𝒜)<VAR>r : A<GOAL>(∃ y ∈ (vanishingIdeal t).toIdeal, ∃ z ∈ (vanishingIdeal t').toIdeal, y + z = r) → ∀ x ∈ t ∩ t', r ∈ x.asHomogeneousIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>t t' : Set (ProjectiveSpectrum 𝒜)<VAR>f : A<VAR>hf : f ∈ (vanishingIdeal t).toIdeal<VAR>g : A<VAR>hg : g ∈ (vanishingIdeal t').toIdeal<VAR>x : ProjectiveSpectrum 𝒜<VAR>hxt : x ∈ t<VAR>hxt' : x ∈ t'<GOAL>f + g ∈ x.asHomogeneousIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>t t' : Set (ProjectiveSpectrum 𝒜)<VAR>f : A<VAR>hf : ∀ x ∈ t, f ∈ x.asHomogeneousIdeal<VAR>g : A<VAR>hg : ∀ x ∈ t', g ∈ x.asHomogeneousIdeal<VAR>x : ProjectiveSpectrum 𝒜<VAR>hxt : x ∈ t<VAR>hxt' : x ∈ t'<GOAL>f + g ∈ x.asHomogeneousIdeal
<VAR>f g : Code<VAR>k : Cont'<GOAL>codeSupp (f.case g) k = trStmts₁ (trNormal (f.case g) k) ∪ (codeSupp f k ∪ codeSupp g k)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → E<VAR>I : ℝ≥0<VAR>hfm : AEStronglyMeasurable f μ<VAR>htendsto : Tendsto (fun i => ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) l (𝓝 ↑I)<GOAL>Tendsto (fun i => ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) l (𝓝 (ENNReal.ofReal ↑I))
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<VAR>s : Set R<VAR>x : R<GOAL>s ∈ 𝓝 x ↔ ∃ γ, {y | v (y - x) < ↑γ} ⊆ s
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : AddGroup H<VAR>inst✝ : AddConstMapClass F G H a b<VAR>f : F<VAR>x : G<GOAL>f (x - a) = f x - b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Set α<VAR>x : α<GOAL>s.encard - 1 ≤ (s \ {x}).encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Set α<VAR>x : α<GOAL>s.encard - {x}.encard ≤ (s \ {x}).encard
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : Zero β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : ZeroAtInftyContinuousMapClass F α β<VAR>C : ℝ<VAR>f g : α →C₀ β<GOAL>Isometry toBCF
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q p : R[X]<VAR>a : R<VAR>n : ℕ<VAR>h : p.natDegree ≤ n<GOAL>(p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q p : R[X]<VAR>a : R<VAR>n : ℕ<VAR>h : p.natDegree ≤ n<GOAL>(p /ₘ (X - C a)).coeff n = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>c • ball 0 1 = ball 0 ‖c‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁴ : OrderedRing α<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module α β<VAR>inst✝¹ : PosSMulStrictMono α β<VAR>inst✝ : PosSMulReflectLT α β<VAR>ha : a < 0<GOAL>a • b < 0 ↔ 0 < b
<VAR>a b : ℝ<VAR>n : ℕ<VAR>t : ℝ<VAR>ht : t ≠ -1<GOAL>∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t = (1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))
<VAR>a b : ℝ<VAR>n : ℕ<VAR>t : ℝ<VAR>ht : t ≠ -1<VAR>this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s<GOAL>∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t = (1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))
<VAR>a b : ℝ<VAR>n : ℕ<VAR>t : ℝ<VAR>ht : t ≠ -1<VAR>this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s<GOAL>↑(∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t) = ↑((1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1)))
<VAR>a b : ℝ<VAR>n : ℕ<VAR>t : ℝ<VAR>ht : t ≠ -1<VAR>this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s<GOAL>↑(∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t) = ∫ (x : ℝ) in ?convert_1..?convert_2, ↑x * (1 + ↑x ^ 2) ^ ↑t
<VAR>a b : ℝ<VAR>n : ℕ<VAR>t : ℝ<VAR>ht : t ≠ -1<VAR>this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s<GOAL>↑((1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))) = (1 + ↑?convert_2 ^ 2) ^ (↑t + 1) / (2 * (↑t + 1)) - (1 + ↑?convert_1 ^ 2) ^ (↑t + 1) / (2 * (↑t + 1))
<VAR>a b : ℝ<VAR>n : ℕ<VAR>t : ℝ<VAR>ht : t ≠ -1<VAR>this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s<GOAL>ℝ
<VAR>a b : ℝ<VAR>n : ℕ<VAR>t : ℝ<VAR>ht : t ≠ -1<VAR>this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s<GOAL>↑t ≠ -1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>inst✝ : Preorder α<VAR>a : α<VAR>ha : ∀ b ∈ s, b < a<GOAL>(insert a s).chainHeight = s.chainHeight + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>inst✝ : Preorder α<VAR>a : α<VAR>ha : ∀ b ∈ s, b < a<GOAL>(⇑ofDual ⁻¹' insert a s).chainHeight = (⇑ofDual ⁻¹' s).chainHeight + 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f g : Filter α<VAR>s t : Set α<VAR>inst✝¹ : Subsingleton α<VAR>l : Filter α<VAR>inst✝ : l.NeBot<GOAL>l = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f g : Filter α<VAR>s✝ t : Set α<VAR>inst✝¹ : Subsingleton α<VAR>l : Filter α<VAR>inst✝ : l.NeBot<VAR>s : Set α<VAR>hs : s ∈ l<GOAL>s ∈ ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f g : Filter α<VAR>s t : Set α<VAR>inst✝¹ : Subsingleton α<VAR>l : Filter α<VAR>inst✝ : l.NeBot<VAR>hs : univ ∈ l<GOAL>univ ∈ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>hi : ¬MeasurableSet i<GOAL>v.restrict i ≤ restrict 0 i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>hf : Inducing f<GOAL>f x ⤳ f y ↔ x ⤳ y
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<GOAL>NumberField.discr K = (-1) ^ (↑p ^ k * (↑p - 1) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝² : Group H<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>d : TransversalPair G A B<VAR>inst✝ : DecidableEq G<VAR>u : ℤˣ<VAR>w : NormalWord d<VAR>h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'<GOAL>¬Cancels u w
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝² : Group H<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>d : TransversalPair G A B<VAR>inst✝ : DecidableEq G<VAR>u : ℤˣ<VAR>w : NormalWord d<VAR>h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'<GOAL>w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>a : R<VAR>ha : a ≠ 0<GOAL>(C a * X).natDegree = 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w₁ w₂ : ι → k<VAR>hw : ∀ i ∈ s, w₁ i = w₂ i<VAR>p₁ p₂ : ι → P<VAR>hp : ∀ i ∈ s, p₁ i = p₂ i<VAR>b : P<GOAL>(s.weightedVSubOfPoint p₁ b) w₁ = (s.weightedVSubOfPoint p₂ b) w₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w₁ w₂ : ι → k<VAR>hw : ∀ i ∈ s, w₁ i = w₂ i<VAR>p₁ p₂ : ι → P<VAR>hp : ∀ i ∈ s, p₁ i = p₂ i<VAR>b : P<GOAL>∑ i ∈ s, w₁ i • (p₁ i -ᵥ b) = ∑ i ∈ s, w₂ i • (p₂ i -ᵥ b)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w₁ w₂ : ι → k<VAR>hw : ∀ i ∈ s, w₁ i = w₂ i<VAR>p₁ p₂ : ι → P<VAR>hp : ∀ i ∈ s, p₁ i = p₂ i<VAR>b : P<VAR>i : ι<VAR>hi : i ∈ s<GOAL>w₁ i • (p₁ i -ᵥ b) = w₂ i • (p₂ i -ᵥ b)
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁷ : DecidableEq n<VAR>inst✝⁶ : DecidableEq p<VAR>inst✝⁵ : DecidableEq q<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : CommRing R<VAR>inst✝² : Fintype p<VAR>inst✝¹ : Fintype q<VAR>inst✝ : Fintype l<GOAL>(PB l R)ᵀ * JB l R * PB l R = 2 • fromBlocks 1 0 0 (S l R)
<VAR>a b m n✝ p✝ n p : ℕ<GOAL>0 < p ^ n.factorization p
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g : G<VAR>x : X.V<VAR>r : k<GOAL>(((linearization k G).obj X).ρ g) (Finsupp.single x r) = Finsupp.single (X.ρ g x) r
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℕ<VAR>inst✝ : StrictOrderedSemiring A<VAR>h : NormNum.IsNat e n<VAR>w : Nat.ble 1 n = true<GOAL>0 < e
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℕ<VAR>inst✝ : StrictOrderedSemiring A<VAR>h : NormNum.IsNat e n<VAR>w : Nat.ble 1 n = true<GOAL>0 < ↑n
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℕ<VAR>inst✝ : StrictOrderedSemiring A<VAR>h : NormNum.IsNat e n<VAR>w : Nat.ble 1 n = true<GOAL>0 < n
<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>R : Type u_12<VAR>R' : Type u_13<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<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✝² : SeminormedRing R'<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedField 𝕜'<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>l l' : Filter α<VAR>h : f' =Θ[l] g'<GOAL>Tendsto (norm ∘ f') l atTop ↔ Tendsto (norm ∘ g') l atTop
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝¹ : OrderedAddCommGroup α<VAR>inst✝ : OrderedAddCommMonoid β<VAR>i : FunLike F α β<VAR>f : F<VAR>iamhc : AddMonoidHomClass F α β<VAR>h : Monotone ⇑f<VAR>a : α<GOAL>0 ≤ a → 0 ≤ f a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝¹ : OrderedAddCommGroup α<VAR>inst✝ : OrderedAddCommMonoid β<VAR>i : FunLike F α β<VAR>f : F<VAR>iamhc : AddMonoidHomClass F α β<VAR>h : Monotone ⇑f<VAR>a : α<GOAL>0 ≤ a → f 0 ≤ f a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝¹ : OrderedAddCommGroup α<VAR>inst✝ : OrderedAddCommMonoid β<VAR>i : FunLike F α β<VAR>f : F<VAR>iamhc : AddMonoidHomClass F α β<VAR>h : ∀ (a : α), 0 ≤ a → 0 ≤ f a<VAR>a b : α<VAR>hl : a ≤ b<GOAL>f a ≤ f b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝¹ : OrderedAddCommGroup α<VAR>inst✝ : OrderedAddCommMonoid β<VAR>i : FunLike F α β<VAR>f : F<VAR>iamhc : AddMonoidHomClass F α β<VAR>h : ∀ (a : α), 0 ≤ a → 0 ≤ f a<VAR>a b : α<VAR>hl : a ≤ b<GOAL>f a ≤ f (b - a) + f a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a : α<GOAL>⌈a⌉₊ ≤ ⌊a⌋₊ + 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a : α<GOAL>a ≤ ↑⌊a⌋₊ + 1
<VAR>R : Type u_1<VAR>inst✝⁴ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>N : Type u_3<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>ι : Type u_4<VAR>ι' : Type u_5<GOAL>reindex R M (Equiv.refl ι) = Equiv.refl (Orientation R M ι)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>E : Type u_4<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : β → E<VAR>g : α → β<VAR>a : α<VAR>hg : Measurable g<VAR>inst✝ : MeasurableSingletonClass β<GOAL>∫ (x : β), f x ∂(deterministic g hg) a = f (g a)
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>h : DifferentiableAt 𝕜 f x<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>(fderivWithin 𝕜 f s x) 1 = (fderiv 𝕜 f x) 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<VAR>S : Subalgebra R B<VAR>h : S ≤ f.range<GOAL>map f (comap f S) = S
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : Semiring k<VAR>inst✝¹ : MulOneClass G<VAR>inst✝ : Semiring R<VAR>f g : MonoidAlgebra k G →+* R<VAR>h₁ : ∀ (b : k), f (single 1 b) = g (single 1 b)<VAR>h_of : ∀ (a : G), f (single a 1) = g (single a 1)<VAR>a : G<VAR>b : k<GOAL>((fun f => ↑f) f) (Finsupp.single a b) = ((fun f => ↑f) g) (Finsupp.single a b)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : Semiring k<VAR>inst✝¹ : MulOneClass G<VAR>inst✝ : Semiring R<VAR>f g : MonoidAlgebra k G →+* R<VAR>h₁ : ∀ (b : k), f (single 1 b) = g (single 1 b)<VAR>h_of : ∀ (a : G), f (single a 1) = g (single a 1)<VAR>a : G<VAR>b : k<GOAL>((fun f => ↑f) f) (single 1 b * single a 1) = ((fun f => ↑f) g) (single 1 b * single a 1)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : Semiring k<VAR>inst✝¹ : MulOneClass G<VAR>inst✝ : Semiring R<VAR>f g : MonoidAlgebra k G →+* R<VAR>h₁ : ∀ (b : k), f (single 1 b) = g (single 1 b)<VAR>h_of : ∀ (a : G), f (single a 1) = g (single a 1)<VAR>a : G<VAR>b : k<GOAL>f (single 1 b * single a 1) = g (single 1 b * single a 1)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddMonoid M<VAR>α : Type u_13<VAR>β : Type u_14<VAR>x✝ y✝ : α ⊕ β →₀ M<GOAL>__src✝.toFun (x✝ + y✝) = __src✝.toFun x✝ + __src✝.toFun y✝
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonUnitalSemiring R<VAR>x y z : HahnSeries Γ R<VAR>b : Γ<GOAL>(x * y * z).coeff b = (x * (y * z)).coeff b
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonUnitalSemiring R<VAR>x y z : HahnSeries Γ R<VAR>b : Γ<GOAL>∑ ij ∈ addAntidiagonal ⋯ ⋯ b, (x * y).coeff ij.1 * z.coeff ij.2 = ∑ ij ∈ addAntidiagonal ⋯ ⋯ b, x.coeff ij.1 * (y * z).coeff ij.2
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonUnitalSemiring R<VAR>x y z : HahnSeries Γ R<VAR>b : Γ<GOAL>∑ x_1 ∈ (addAntidiagonal ⋯ ⋯ b).sigma fun a => addAntidiagonal ⋯ ⋯ a.1, x.coeff x_1.snd.1 * y.coeff x_1.snd.2 * z.coeff x_1.fst.2 = ∑ x_1 ∈ (addAntidiagonal ⋯ ⋯ b).sigma fun a => addAntidiagonal ⋯ ⋯ a.2, x.coeff x_1.fst.1 * (y.coeff x_1.snd.1 * z.coeff x_1.snd.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>H : Nat.Primrec fun n => encode (decode n)<VAR>f : α → List β<VAR>g : α → σ<VAR>h : α → β × List β → σ<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>hh : Primrec₂ h<VAR>this✝ : Primcodable (List β) := prim H<VAR>this : Primrec fun a => Option.map (fun o => Option.casesOn o (g a) (h a)) (decode (encode (f a)))<VAR>a : α<GOAL>Option.map (fun o => Option.casesOn o (g a) (h a)) (decode (encode (f a))) = some (List.casesOn (f a) (g a) fun b l => h a (b, l))
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>a : α<VAR>f : Multiset α<VAR>ha : Irreducible a<VAR>pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a<VAR>this : DecidableEq α<GOAL>∃ p, a ~ᵤ p ∧ f = {p}
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>a : α<VAR>f : Multiset α<VAR>ha : Irreducible a<VAR>pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a<VAR>this : DecidableEq α<GOAL>(fun g => g.prod ~ᵤ a → (∀ b ∈ g, Prime b) → ∃ p, a ~ᵤ p ∧ g = {p}) 0
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>a : α<VAR>f : Multiset α<VAR>ha : Irreducible a<VAR>pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a<VAR>this : DecidableEq α<GOAL>∀ (a_1 : α) (s : Multiset α), (fun g => g.prod ~ᵤ a → (∀ b ∈ g, Prime b) → ∃ p, a ~ᵤ p ∧ g = {p}) s → (fun g => g.prod ~ᵤ a → (∀ b ∈ g, Prime b) → ∃ p, a ~ᵤ p ∧ g = {p}) (a_1 ::ₘ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>p : α → ℕ →. Bool<VAR>hp : Partrec₂ p<VAR>n : ℕ<GOAL>(Nat.rfind fun n_1 => (fun m => decide (m = 0)) <$> (↑(decode (Nat.pair n n_1))).bind fun a => Part.map encode ((fun a => Part.map (fun b => bif (a, b).2 then 0 else 1) (p a.1 a.2)) a)) = (↑(decode n)).bind fun a => Part.map encode ((fun a => Nat.rfind (p a)) a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>p : α → ℕ →. Bool<VAR>hp : Partrec₂ p<VAR>n : ℕ<VAR>a : α<VAR>e : decode n = Option.some a<GOAL>(Nat.rfind fun n => Part.map (fun m => decide (m = 0)) (Part.map (fun b => bif b then 0 else 1) (p a n))) = Nat.rfind (p a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>p : α → ℕ →. Bool<VAR>hp : Partrec₂ p<VAR>n : ℕ<VAR>a : α<VAR>e : decode n = Option.some a<GOAL>(fun n => Part.map (fun m => decide (m = 0)) (Part.map (fun b => bif b then 0 else 1) (p a n))) = p a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>p : α → ℕ →. Bool<VAR>hp : Partrec₂ p<VAR>n✝ : ℕ<VAR>a : α<VAR>e : decode n✝ = Option.some a<VAR>n : ℕ<GOAL>Part.map (fun m => decide (m = 0)) (Part.map (fun b => bif b then 0 else 1) (p a n)) = p a n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>p : α → ℕ →. Bool<VAR>hp : Partrec₂ p<VAR>n✝ : ℕ<VAR>a : α<VAR>e : decode n✝ = Option.some a<VAR>n : ℕ<GOAL>Part.map (fun x => decide ((bif x then 0 else 1) = 0)) (p a n) = p a n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>p : α → ℕ →. Bool<VAR>hp : Partrec₂ p<VAR>n✝ : ℕ<VAR>a : α<VAR>e : decode n✝ = Option.some a<VAR>n : ℕ<VAR>b : Bool<GOAL>decide ((bif b then 0 else 1) = 0) = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε✝ ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f g : α → ℝ≥0∞<VAR>ι : Type u_4<VAR>a : ι → ℝ≥0∞<VAR>tsum_ne_top : ∑' (i : ι), a i ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε_ne_zero : ε ≠ 0<GOAL>{i | ε ≤ a i}.Finite