ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>hp : p ≠ 0<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (i : ι), StronglyMeasurable (f i)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hfu : UnifIntegrable f p μ<VAR>M : ℝ≥0<VAR>hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M<VAR>δ : ℝ<VAR>hδpos : 0 < δ<VAR>hδ : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>C : ℝ≥0<VAR>hC : ∀ (i : ι), μ {x | C ≤ ‖f i x‖₊} ≤ ENNReal.ofReal δ<GOAL>∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 E₁ G<VAR>k : ℕ<VAR>x : (i : ι) → E₁ i<GOAL>‖f.iteratedFDeriv k x‖ ≤ ↑((Fintype.card ι).descFactorial k) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)
<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>x : F<VAR>n : ℕ<GOAL>((X - C x) ^ n).natSepDegree = if n = 0 then 0 else 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>ha : a ∉ s<VAR>hb : b ∉ s<GOAL>{ ofColex := insert a s } ≤ { ofColex := insert b s } ↔ a ≤ b
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_3<VAR>inst✝ : Group N<VAR>s : Set G<VAR>g✝ g : G<GOAL>zpowers g = ⊥ ↔ g = 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c₁ c₂ : R<GOAL>(((ofQuaternion.toLinearMap ∘ₗ toQuaternion.toLinearMap) ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inl R R R) 1 = (((AlgHom.id R (CliffordAlgebra (Q c₁ c₂))).toLinearMap ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inl R R R) 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c₁ c₂ : R<GOAL>(((ofQuaternion.toLinearMap ∘ₗ toQuaternion.toLinearMap) ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inr R R R) 1 = (((AlgHom.id R (CliffordAlgebra (Q c₁ c₂))).toLinearMap ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inr R R R) 1
<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>inst✝ : Finite ι<VAR>F : ι → X → α<GOAL>Equicontinuous F ↔ ∀ (i : ι), Continuous (F i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing A'<VAR>inst✝⁴ : CommRing A''<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R A'<VAR>inst✝¹ : Algebra R A''<VAR>a b : R<VAR>inst✝ : IsEmpty ι<VAR>this : aeval x = (ofId R A).comp ↑(isEmptyAlgEquiv R ι)<GOAL>AlgebraicIndependent R x ↔ Injective ⇑(algebraMap R A)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing A'<VAR>inst✝⁴ : CommRing A''<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R A'<VAR>inst✝¹ : Algebra R A''<VAR>a b : R<VAR>inst✝ : IsEmpty ι<VAR>this : aeval x = (ofId R A).comp ↑(isEmptyAlgEquiv R ι)<GOAL>Injective ⇑((ofId R A).comp ↑(isEmptyAlgEquiv R ι)) ↔ Injective (⇑(algebraMap R A) ∘ ⇑(isEmptyAlgEquiv R ι))
<VAR>m n : ℕ<GOAL>m + n ≤ pair m n
<VAR>m n : ℕ<GOAL>m + n ≤ if m < n then n * n + m else m * m + (m + n)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ b c d : α<VAR>n p : ℤ<VAR>hp : Even p<VAR>a : α<GOAL>|a| ^ p = a ^ p
<VAR>α : Type u_1<VAR>c₀ : RBColor<VAR>n₀ : Nat<VAR>c : RBColor<VAR>n : Nat<VAR>c' : RBColor<VAR>t : RBNode α<VAR>path : Path α<VAR>hp : Path.Balanced c₀ n₀ path c n<VAR>ht : DelProp c' t n<VAR>hc : c = black → c' ≠ red<GOAL>∃ n, (path.del t c').Balanced black n
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>z : ℂ<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<GOAL>‖f z‖ ≤ ‖(↑ε + ↑(sSupNormIm f 0)) ^ (1 - z) * (↑ε + ↑(sSupNormIm f 1)) ^ z‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>z : ℂ<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<GOAL>‖f z‖ ≤ (ε + sSupNormIm f 0) ^ (1 - z.re) * (ε + sSupNormIm f 1) ^ z.re
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>z : ℂ<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<GOAL>‖f z‖ * ((ε + sSupNormIm f 0) ^ (1 - z.re)) ^ (-1) * ((ε + sSupNormIm f 1) ^ z.re) ^ (-1) ≤ 1
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>z : ℂ<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<GOAL>0 < (ε + sSupNormIm f 1) ^ z.re
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>z : ℂ<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<GOAL>0 < (ε + sSupNormIm f 0) ^ (1 - z.re)
<VAR>σ : Type u_1<VAR>inst✝¹ : Fintype σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>h : 0 < k<GOAL>psum σ R k = (-1) ^ (k + 1) * ↑k * esymm σ R k - ∑ a ∈ filter (fun a => a.1 ∈ Set.Ioo 0 k) (antidiagonal k), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
<VAR>σ : Type u_1<VAR>inst✝¹ : Fintype σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>h : 0 < k<GOAL>psum σ R k = (-1) ^ (k + 1) * ↑k * esymm σ R k - ∑ x ∈ filter (fun a => a.1 < k ∧ 0 < a.1) (antidiagonal k), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2
<VAR>σ : Type u_1<VAR>inst✝¹ : Fintype σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>h : 0 < k<VAR>hesymm : ↑k * esymm σ R k = (-1) ^ (k + 1) * ∑ a ∈ filter (fun a => a.1 < k) (antidiagonal k), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2<GOAL>psum σ R k = (-1) ^ (k + 1) * ↑k * esymm σ R k - ∑ x ∈ filter (fun a => a.1 < k ∧ 0 < a.1) (antidiagonal k), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2
<VAR>σ : Type u_1<VAR>inst✝¹ : Fintype σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>h : 0 < k<VAR>hesymm : ↑k * esymm σ R k = (-1) ^ (k + 1) * (∑ x ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 + ∑ x ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)<GOAL>psum σ R k = (-1) ^ (k + 1) * ↑k * esymm σ R k - ∑ x ∈ filter (fun a => a.1 < k ∧ 0 < a.1) (antidiagonal k), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2
<VAR>σ : Type u_1<VAR>inst✝¹ : Fintype σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>h : 0 < k<VAR>hesymm : ↑k * esymm σ R k = (-1) ^ (k + 1) * (∑ x ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 + ∑ x ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)<VAR>sub_both_sides : (fun x => x - (-1) ^ (k + 1) * ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2) (↑k * esymm σ R k) = (fun x => x - (-1) ^ (k + 1) * ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2) ((-1) ^ (k + 1) * (∑ x ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 + ∑ x ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2))<GOAL>psum σ R k = (-1) ^ (k + 1) * ↑k * esymm σ R k - ∑ x ∈ filter (fun a => a.1 < k ∧ 0 < a.1) (antidiagonal k), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2
<VAR>σ : Type u_1<VAR>inst✝¹ : Fintype σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>h : 0 < k<VAR>hesymm : ↑k * esymm σ R k = (-1) ^ (k + 1) * (∑ x ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 + ∑ x ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)<VAR>sub_both_sides : ↑k * esymm σ R k - (-1) ^ (k + 1) * ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = (-1) ^ (k + 1) * ∑ a ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2<GOAL>psum σ R k = (-1) ^ (k + 1) * ↑k * esymm σ R k - ∑ x ∈ filter (fun a => a.1 < k ∧ 0 < a.1) (antidiagonal k), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2
<VAR>σ : Type u_1<VAR>inst✝¹ : Fintype σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>h : 0 < k<VAR>hesymm : ↑k * esymm σ R k = (-1) ^ (k + 1) * (∑ x ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 + ∑ x ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)<VAR>sub_both_sides✝ : ↑k * esymm σ R k - (-1) ^ (k + 1) * ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = (-1) ^ (k + 1) * ∑ a ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2<VAR>sub_both_sides : (fun x => (-1) ^ (k + 1) * x) (↑k * esymm σ R k - (-1) ^ (k + 1) * ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2) = (fun x => (-1) ^ (k + 1) * x) ((-1) ^ (k + 1) * ∑ a ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2)<GOAL>psum σ R k = (-1) ^ (k + 1) * ↑k * esymm σ R k - ∑ x ∈ filter (fun a => a.1 < k ∧ 0 < a.1) (antidiagonal k), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2
<VAR>σ : Type u_1<VAR>inst✝¹ : Fintype σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>h : 0 < k<VAR>hesymm : ↑k * esymm σ R k = (-1) ^ (k + 1) * (∑ x ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 + ∑ x ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)<VAR>sub_both_sides✝ : ↑k * esymm σ R k - (-1) ^ (k + 1) * ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = (-1) ^ (k + 1) * ∑ a ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2<VAR>sub_both_sides : (-1) ^ (k + 1) * ↑k * esymm σ R k - ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = ∑ a ∈ filter (fun a => a.1 < k ∧ ¬0 < a.1) (antidiagonal k), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2<GOAL>psum σ R k = (-1) ^ (k + 1) * ↑k * esymm σ R k - ∑ x ∈ filter (fun a => a.1 < k ∧ 0 < a.1) (antidiagonal k), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2
<VAR>σ : Type u_1<VAR>inst✝¹ : Fintype σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>h : 0 < k<VAR>hesymm : ↑k * esymm σ R k = (-1) ^ (k + 1) * (∑ x ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 + ∑ x ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)<VAR>sub_both_sides✝ : ↑k * esymm σ R k - (-1) ^ (k + 1) * ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = (-1) ^ (k + 1) * ∑ a ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2<VAR>sub_both_sides : (-1) ^ (k + 1) * ↑k * esymm σ R k - ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = ∑ a ∈ filter (fun a => a.1 < k ∧ ¬0 < a.1) (antidiagonal k), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2<VAR>this : filter (fun a => a.1 < k ∧ ¬0 < a.1) (antidiagonal k) = {(0, k)}<GOAL>psum σ R k = (-1) ^ (k + 1) * ↑k * esymm σ R k - ∑ x ∈ filter (fun a => a.1 < k ∧ 0 < a.1) (antidiagonal k), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2
<VAR>σ : Type u_1<VAR>inst✝¹ : Fintype σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>h : 0 < k<VAR>hesymm : ↑k * esymm σ R k = (-1) ^ (k + 1) * (∑ x ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 + ∑ x ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)<VAR>sub_both_sides✝ : ↑k * esymm σ R k - (-1) ^ (k + 1) * ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = (-1) ^ (k + 1) * ∑ a ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2<VAR>sub_both_sides : (-1) ^ (k + 1) * ↑k * esymm σ R k - ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = (-1) ^ (0, k).1 * esymm σ R (0, k).1 * psum σ R (0, k).2<VAR>this : filter (fun a => a.1 < k ∧ ¬0 < a.1) (antidiagonal k) = {(0, k)}<GOAL>psum σ R k = (-1) ^ (k + 1) * ↑k * esymm σ R k - ∑ x ∈ filter (fun a => a.1 < k ∧ 0 < a.1) (antidiagonal k), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2
<VAR>σ : Type u_1<VAR>inst✝¹ : Fintype σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>h : 0 < k<VAR>hesymm : ↑k * esymm σ R k = (-1) ^ (k + 1) * (∑ x ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 + ∑ x ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)<VAR>sub_both_sides✝ : ↑k * esymm σ R k - (-1) ^ (k + 1) * ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = (-1) ^ (k + 1) * ∑ a ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2<VAR>this : filter (fun a => a.1 < k ∧ ¬0 < a.1) (antidiagonal k) = {(0, k)}<VAR>sub_both_sides : (-1) ^ (k + 1) * ↑k * esymm σ R k - ∑ x ∈ filter (fun a => a.1 < k ∧ 0 < a.1) (antidiagonal k), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 = psum σ R k<GOAL>psum σ R k = (-1) ^ (k + 1) * ↑k * esymm σ R k - ∑ x ∈ filter (fun a => a.1 < k ∧ 0 < a.1) (antidiagonal k), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : AddMonoid ι<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>a : ⨁ (i : ι), ↥(𝒜 i)<VAR>i : ι<GOAL>(proj 𝒜 i) ((decompose 𝒜).symm a) = (decompose 𝒜).symm ((of (fun i => ↥(𝒜 i)) i) (a i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ Icc a₁ a₂ ×ˢ Icc b₁ b₂ ↔ (x, y) ∈ Icc (a₁, b₁) (a₂, b₂)
<VAR>E : Type u_1<VAR>f : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : ℝ → E<VAR>a b : ℝ<VAR>hb : 0 < b<GOAL>∫ (x : ℝ) in Ioi a, g (x * b) = b⁻¹ • ∫ (x : ℝ) in Ioi (a * b), g x
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<GOAL>μ.toFiniteAux = 0 ↔ μ = 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>h : μ.toFiniteAux = 0<GOAL>μ = 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>h : μ.toFiniteAux = 0<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ s = 0 s
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>h : ∀ (s : Set α), MeasurableSet s → μ.toFiniteAux s = 0 s<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ s = 0 s
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h : μ.toFiniteAux s = 0 s<GOAL>μ s = 0 s
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h : ∀ (i : ℕ), 2 ^ (i + 1) * (sFiniteSeq μ i) Set.univ = ⊤ ∨ (sFiniteSeq μ i) s = 0<GOAL>μ s = 0 s
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h : ∀ (i : ℕ), 2 ^ (i + 1) * (sFiniteSeq μ i) Set.univ = ⊤ ∨ (sFiniteSeq μ i) s = 0<GOAL>∑' (i : ℕ), (sFiniteSeq μ i) s = 0 s
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h : ∀ (i : ℕ), 2 ^ (i + 1) * (sFiniteSeq μ i) Set.univ = ⊤ ∨ (sFiniteSeq μ i) s = 0<GOAL>∀ (i : ℕ), (sFiniteSeq μ i) s = 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>n : ℕ<VAR>h : 2 ^ (n + 1) * (sFiniteSeq μ n) Set.univ = ⊤ ∨ (sFiniteSeq μ n) s = 0<GOAL>(sFiniteSeq μ n) s = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝³ : SetLike S R<VAR>inst✝² : Monoid R<VAR>inst✝¹ : AddMonoid ι<VAR>A : ι → S<VAR>inst✝ : GradedMonoid A<VAR>n : ℕ<VAR>r : R<VAR>i : ι<VAR>h : r ∈ A i<GOAL>r ^ n ∈ A (n • i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hsm : NullMeasurableSet s μ<VAR>hs₀ : μ s ≠ 0<GOAL>∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hsm : NullMeasurableSet s μ<VAR>hs₀ : μ s ≠ 0<VAR>t : Set α<VAR>hsub : t ⊆ s<VAR>htm : MeasurableSet t<VAR>hts : t =ᶠ[ae μ] s<GOAL>∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hsm : NullMeasurableSet s μ<VAR>hs₀ : μ s ≠ 0<VAR>t : Set α<VAR>hsub : t ⊆ s<VAR>htm : MeasurableSet t<VAR>hts : t =ᶠ[ae μ] s<VAR>x : α<VAR>hxt : x ∈ t<VAR>m : ℕ<VAR>hm₀ : m ≠ 0<VAR>hmt : f^[m] x ∈ t<GOAL>∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s' : Finset α<VAR>t✝ t' : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝ : DecidableEq (α × β)<VAR>s : Finset α<VAR>t : Finset β<VAR>x✝ : α × β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ s ×ˢ t ↔ (x, y) ∈ t.biUnion fun b => image (fun a => (a, b)) s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s t u v : Finset α<GOAL>s ○ t ○ (u ○ v) = s ○ u ○ (t ○ v)
<VAR>α : Type u_1<VAR>l l₁✝ l₂✝ : List α<VAR>p : α → Prop<VAR>a✝ : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₁ l₂ t : List α<VAR>s : t <+ l₁<VAR>e : t ++ l₂ = l₁ ∪ l₂<VAR>h : a ∈ l₁ ∪ l₂<GOAL>t ++ l₂ = a :: l₁ ∪ l₂
<VAR>α : Type u_1<VAR>l l₁✝ l₂✝ : List α<VAR>p : α → Prop<VAR>a✝ : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₁ l₂ t : List α<VAR>s : t <+ l₁<VAR>e : t ++ l₂ = l₁ ∪ l₂<VAR>h : ¬a ∈ l₁ ∪ l₂<GOAL>a :: t ++ l₂ = a :: l₁ ∪ l₂
<VAR>R : Type u_1<GOAL>μ.IsMultiplicative
<VAR>R : Type u_1<GOAL>μ 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → μ (m * n) = μ m * μ n
<VAR>R : Type u_1<VAR>n m : ℕ<VAR>hn : n ≠ 0<VAR>hm : m ≠ 0<VAR>hnm : n.Coprime m<GOAL>μ (n * m) = μ n * μ m
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<VAR>a✝ : Nontrivial R<GOAL>(p * q).natDegree = p.natDegree + q.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<VAR>a✝ : Nontrivial R<GOAL>p.leadingCoeff * q.leadingCoeff ≠ 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : ArithmeticFunction R<VAR>k x : ℕ<GOAL>(f.ppow (k + 1)) x = (f.pmul (f.ppow k)) x
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : ArithmeticFunction R<VAR>k x : ℕ<GOAL>f x * f x ^ k = (f.pmul (f.ppow k)) x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>|(o.areaForm x) y| ≤ ‖x‖ * ‖y‖
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>x y : T<VAR>m : M<VAR>s : ↥S<GOAL>(x * y) • mk m s = x • y • mk m s
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>x y : T<VAR>m : M<VAR>s : ↥S<GOAL>(IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 * IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2) • mk m s = IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 • IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2 • mk m s
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<GOAL>cylinder s ∅ = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteSemilatticeInf α<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : ι → α<GOAL>iInf s ≤ a ↔ ∀ (b : α), (∀ (i : ι), b ≤ s i) → b ≤ a
<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 : Set α<VAR>f✝ g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → E<GOAL>(μ univ).toReal • ⨍ (x : α), f x ∂μ = ∫ (x : α), f 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 : Set α<VAR>f✝ g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → E<VAR>hμ : μ = 0<GOAL>(μ univ).toReal • ⨍ (x : α), f x ∂μ = ∫ (x : α), f 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 : Set α<VAR>f✝ g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → E<VAR>hμ : μ ≠ 0<GOAL>(μ univ).toReal • ⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ