ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : TopCat<VAR>F : TopCat.Presheaf CommRingCat X<VAR>U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X<VAR>n₁ n₂ : ℕ<VAR>y₁ : ↑(F.obj (op U₁))<VAR>y₂ : ↑(F.obj (op U₂))<VAR>f : ↑(F.obj (op (U₁ ⊔ U₂)))<VAR>x : ↑(F.obj (op U₃))<VAR>h₄₁ : U₄ ≤ U₁<VAR>h₄₂ : U₄ ≤ U₂<VAR>h₅₁ : U₅ ≤ U₁<VAR>h₅₃ : U₅ ≤ U₃<VAR>h₆₂ : U₆ ≤ U₂<VAR>h₆₃ : U₆ ≤ U₃<VAR>h₇₄ : U₇ ≤ U₄<VAR>h₇₅ : U₇ ≤ U₅<VAR>h₇₆ : U₇ ≤ U₆<VAR>e₁ : (F.map (homOfLE ⋯).op) y₁ = (F.map (homOfLE ⋯).op) f ^ n₁ * (F.map (homOfLE ⋯).op) x<VAR>e₂ : (F.map (homOfLE ⋯).op) y₂ = (F.map (homOfLE ⋯).op) f ^ n₂ * (F.map (homOfLE ⋯).op) x<GOAL>(F.map (homOfLE ⋯).op) f ^ n₂ * (F.map (homOfLE ⋯).op) y₁ = (F.map (homOfLE ⋯).op) f ^ n₁ * (F.map (homOfLE ⋯).op) y₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>t : Set (α × β)<VAR>ht : MeasurableSet t<VAR>hκs : ∀ (a : α), IsFiniteMeasure (κ a)<GOAL>Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>t : Set (α × β)<VAR>ht : MeasurableSet t<VAR>hκs : ∀ (a : α), IsFiniteMeasure (κ a)<GOAL>(fun t => Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)) ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>t : Set (α × β)<VAR>ht : MeasurableSet t<VAR>hκs : ∀ (a : α), IsFiniteMeasure (κ a)<GOAL>∀ t ∈ image2 (fun x x_1 => x ×ˢ x_1) {s | MeasurableSet s} {t | MeasurableSet t}, (fun t => Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>t : Set (α × β)<VAR>ht : MeasurableSet t<VAR>hκs : ∀ (a : α), IsFiniteMeasure (κ a)<GOAL>∀ (t : Set (α × β)), MeasurableSet t → (fun t => Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)) t → (fun t => Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)) tᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>t : Set (α × β)<VAR>ht : MeasurableSet t<VAR>hκs : ∀ (a : α), IsFiniteMeasure (κ a)<GOAL>∀ (f : ℕ → Set (α × β)), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), (fun t => Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)) (f i)) → (fun t => Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)) (⋃ i, f i)
<VAR>α : Type u_1<VAR>f : ℕ → α<VAR>a : ℕ<VAR>hf : Periodic f a<VAR>n : ℕ<GOAL>f (n % a) = f n
<VAR>b : Ordinal.{u_1}<VAR>b1 : 1 < b<GOAL>log b 0 = 0
<VAR>b : Ordinal.{u_1}<VAR>b1 : 1 < b<GOAL>sInf {o | 0 < b ^ o} ≤ succ 0
<VAR>b : Ordinal.{u_1}<VAR>b1 : 1 < b<GOAL>succ 0 ∈ {o | 0 < b ^ o}
<VAR>b : Ordinal.{u_1}<VAR>b1 : 1 < b<GOAL>0 < b ^ succ 0
<VAR>b : Ordinal.{u_1}<VAR>b1 : 1 < b<GOAL>0 < b
<VAR>b : Ordinal.{u_1}<VAR>b1 : ¬1 < b<GOAL>log b 0 = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>j : ι<VAR>hj : e.BoundaryGE j<VAR>inst✝ : e.IsTruncLE<GOAL>False
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>j : ι<VAR>hj : e.BoundaryGE j<VAR>inst✝ : e.IsTruncLE<VAR>i : ι<VAR>hi : e.f i = c'.prev (e.f j)<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>inst✝ : LinearOrderedAddCommGroup β<VAR>x : β<GOAL>↑|x| = |↑x|
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>x y : M<VAR>h : f.toMap x = f.toMap y<GOAL>g x = g y
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>x y : M<VAR>h : f.toMap x = f.toMap y<VAR>c : ↥S<VAR>hc : ↑c * x = ↑c * y<GOAL>g x = g y
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>x y : M<VAR>h : f.toMap x = f.toMap y<VAR>c : ↥S<VAR>hc : ↑c * x = ↑c * y<GOAL>↑((IsUnit.liftRight (g.restrict S) hg) c)⁻¹ * (g.restrict S) c * g x = g y
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>x y : M<VAR>h : f.toMap x = f.toMap y<VAR>c : ↥S<VAR>hc : ↑c * x = ↑c * y<GOAL>↑((IsUnit.liftRight (g.restrict S) hg) c)⁻¹ * g ↑c * g x = g y
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>h : f₁ =ᶠ[𝓝 x] f<GOAL>lineDeriv 𝕜 f₁ x v = lineDeriv 𝕜 f x v
<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<GOAL>setToFun μ T hT 0 = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : MonoidWithZero R<VAR>r u : R<VAR>hu : IsUnit u<VAR>h_comm : Commute r u<VAR>n : ℕ<GOAL>(r * u) ^ n = 0 ↔ r ^ n = 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>hp : p ≠ 0<VAR>h : p.IsRoot a<VAR>hlt : 0 ≥ p.degree<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>hp : p ≠ 0<VAR>h : p.IsRoot a<VAR>hlt : 0 ≥ p.degree<VAR>this : p = C (p.coeff 0)<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>hp : p ≠ 0<VAR>h : p.coeff 0 = 0<VAR>hlt : 0 ≥ p.degree<VAR>this : p = C (p.coeff 0)<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>hp : p ≠ 0<VAR>h : p.coeff 0 = 0<VAR>hlt : 0 ≥ p.degree<VAR>this : p = 0<GOAL>False
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>𝕜 : Type u_5<VAR>inst✝⁵ : CommRing 𝕜<VAR>inst✝⁴ : PartialOrder 𝕜<VAR>inst✝³ : StarRing 𝕜<VAR>inst✝² : StarOrderedRing 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>hD : D.IsHermitian<GOAL>(Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>𝕜 : Type u_5<VAR>inst✝⁵ : CommRing 𝕜<VAR>inst✝⁴ : PartialOrder 𝕜<VAR>inst✝³ : StarRing 𝕜<VAR>inst✝² : StarOrderedRing 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>hD : D.IsHermitian<GOAL>(Matrix.fromBlocks D Bᴴ B A).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian
<VAR>i j : ℤ<GOAL>i.natAbs.lcm j.natAbs = j.natAbs.lcm i.natAbs
<VAR>m n : ℕ<VAR>a : ℤ<VAR>b : ℕ<GOAL>↑a = 0 ↔ ↑b ∣ a
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<GOAL>∃ J, M.Basis' J X ∧ I ⊆ J
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<GOAL>∃ J, M.Basis J (X ∩ M.E) ∧ I ⊆ J
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<GOAL>j ∈ Set.range ⇑(c.embedding (c.index j))
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<VAR>this : (c.embedding (c.index j)) (c.invEmbedding j) ∈ Set.range ⇑(c.embedding (c.index j))<GOAL>j ∈ Set.range ⇑(c.embedding (c.index j))
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherianRing R<GOAL>Subsingleton (CotangentSpace R) ↔ IsField R
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherianRing R<GOAL>IsIdempotentElem (maximalIdeal R) ↔ IsField R
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherianRing R<GOAL>maximalIdeal R = ⊥ ∨ maximalIdeal R = ⊤ ↔ maximalIdeal R = ⊥
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>h : 0 < c<GOAL>(fun x => x * c) ⁻¹' Ioo a b = Ioo (a / c) (b / c)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ≥0<GOAL>w₁ + w₂ + w₃ + w₄ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ * p₃ ^ ↑w₃ * p₄ ^ ↑w₄ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>M.Indep M.E ↔ M = freeOn M.E
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>u : UniformSpace β<VAR>f : α → β<VAR>l : Filter α<GOAL>Cauchy l ↔ Cauchy (map f l)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>u : UniformSpace β<VAR>f : α → β<VAR>l : Filter α<GOAL>l.NeBot ∧ l ×ˢ l ≤ 𝓤 α ↔ l.NeBot ∧ l ×ˢ l ≤ Filter.comap (fun p => (f p.1, f p.2)) (𝓤 β)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_7, u_1} C<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.7542, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝¹ : Category.{?u.7594, u_4} A<VAR>G : C ⥤ D<VAR>inst✝ : G.IsCoverDense K<VAR>ℱ : SheafOfTypes K<VAR>X : D<VAR>s t : ℱ.val.obj (op X)<VAR>h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t<GOAL>s = t
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_7, u_1} C<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.7542, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝¹ : Category.{?u.7594, u_4} A<VAR>G : C ⥤ D<VAR>inst✝ : G.IsCoverDense K<VAR>ℱ : SheafOfTypes K<VAR>X : D<VAR>s t : ℱ.val.obj (op X)<VAR>h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t<GOAL>∀ ⦃Y : D⦄ ⦃f : Y ⟶ X⦄, (Sieve.coverByImage G X).arrows f → ℱ.val.map f.op s = ℱ.val.map f.op t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<GOAL>a ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<GOAL>b = a ∨ b = succ a → a ≤ b ∧ b ≤ succ a
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>V : Type u_5<VAR>W : Type u_6<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NormedAddCommGroup V<VAR>inst✝¹² : NormedSpace 𝕜 V<VAR>inst✝¹¹ : MeasurableSpace V<VAR>inst✝¹⁰ : BorelSpace V<VAR>inst✝⁹ : NormedAddCommGroup W<VAR>inst✝⁸ : NormedSpace 𝕜 W<VAR>inst✝⁷ : MeasurableSpace W<VAR>inst✝⁶ : BorelSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →L[𝕜] W →L[𝕜] 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>M : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝ : (i : ι) → NormedSpace ℝ (M i)<VAR>f : V → F →L[ℝ] E<VAR>a : F<VAR>w : W<VAR>he : Continuous ⇑e<VAR>hf : Integrable f μ<GOAL>(fourierIntegral e μ L.toLinearMap₂ f w) a = fourierIntegral e μ L.toLinearMap₂ (fun x => (f x) a) w
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>V : Type u_5<VAR>W : Type u_6<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NormedAddCommGroup V<VAR>inst✝¹² : NormedSpace 𝕜 V<VAR>inst✝¹¹ : MeasurableSpace V<VAR>inst✝¹⁰ : BorelSpace V<VAR>inst✝⁹ : NormedAddCommGroup W<VAR>inst✝⁸ : NormedSpace 𝕜 W<VAR>inst✝⁷ : MeasurableSpace W<VAR>inst✝⁶ : BorelSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →L[𝕜] W →L[𝕜] 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>M : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝ : (i : ι) → NormedSpace ℝ (M i)<VAR>f : V → F →L[ℝ] E<VAR>a : F<VAR>w : W<VAR>he : Continuous ⇑e<VAR>hf : Integrable f μ<GOAL>∫ (x : V), (e (-(L.toLinearMap₂ x) w) • f x) a ∂μ = fourierIntegral e μ L.toLinearMap₂ (fun x => (f x) a) w
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>V : Type u_5<VAR>W : Type u_6<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NormedAddCommGroup V<VAR>inst✝¹² : NormedSpace 𝕜 V<VAR>inst✝¹¹ : MeasurableSpace V<VAR>inst✝¹⁰ : BorelSpace V<VAR>inst✝⁹ : NormedAddCommGroup W<VAR>inst✝⁸ : NormedSpace 𝕜 W<VAR>inst✝⁷ : MeasurableSpace W<VAR>inst✝⁶ : BorelSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →L[𝕜] W →L[𝕜] 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>M : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝ : (i : ι) → NormedSpace ℝ (M i)<VAR>f : V → F →L[ℝ] E<VAR>a : F<VAR>w : W<VAR>he : Continuous ⇑e<VAR>hf : Integrable f μ<GOAL>Integrable (fun v => e (-(L.toLinearMap₂ v) w) • f v) μ
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>S : Type u_3<VAR>R : Type u_4<VAR>inst✝⁹ : DecidableEq ι<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : SetLike σ R<VAR>inst✝⁶ : AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>inst✝⁵ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝⁴ : SetLike.GradedMonoid A<VAR>inst✝³ : Sub ι<VAR>inst✝² : OrderedSub ι<VAR>inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>r : ↥(A i)<VAR>r' : ⨁ (i : ι), ↥(A i)<VAR>n : ι<VAR>inst✝ : Decidable (i ≤ n)<VAR>h : i ≤ n<GOAL>↑(((of (fun i => ↥(A i)) i) r * r') n) = ↑r * ↑(r' (n - i))
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>S : Type u_3<VAR>R : Type u_4<VAR>inst✝⁹ : DecidableEq ι<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : SetLike σ R<VAR>inst✝⁶ : AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>inst✝⁵ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝⁴ : SetLike.GradedMonoid A<VAR>inst✝³ : Sub ι<VAR>inst✝² : OrderedSub ι<VAR>inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>r : ↥(A i)<VAR>r' : ⨁ (i : ι), ↥(A i)<VAR>n : ι<VAR>inst✝ : Decidable (i ≤ n)<VAR>h : ¬i ≤ n<GOAL>↑(((of (fun i => ↥(A i)) i) r * r') n) = 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>s : Set α<VAR>φ : ι → Set α<VAR>hs : MeasurableSet s<VAR>ae_eventually_mem : ∀ᵐ (x : α) ∂μ, x ∈ s → ∀ᶠ (n : ι) in l, x ∈ φ n<VAR>measurable : ∀ (n : ι), MeasurableSet (φ n)<GOAL>∀ᵐ (x : α) ∂μ.restrict s, ∀ᶠ (i : ι) in l, x ∈ φ i
<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✝¹ : OrderedCancelCommMonoid M<VAR>f g : ι → M<VAR>s t : Finset ι<VAR>inst✝ : DecidableEq ι<GOAL>∏ i ∈ s \ t, f i ≤ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>↑((last n).cycleRange i) = ↑((finRotate (n + 1)) i)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>P : G.Partition<VAR>v : V<GOAL>v ∈ P.partOfVertex v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>P : G.Partition<VAR>v : V<VAR>right✝ : ∀ (y : Set V), (fun b => b ∈ P.parts ∧ v ∈ b) y → y = Exists.choose ⋯<VAR>left✝ : Exists.choose ⋯ ∈ P.parts<VAR>h : v ∈ Exists.choose ⋯<GOAL>v ∈ P.partOfVertex v
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>rightHomologyMap' (φ - φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ - rightHomologyMap' φ' h₁ h₂
<VAR>α : Type u_1<VAR>inst✝¹ : Inv α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x : α<GOAL>(equivShrink α) x⁻¹ = ((equivShrink α) x)⁻¹
<VAR>α : Type u_1<VAR>inst✝¹ : Inv α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x : α<GOAL>(equivShrink α) x⁻¹ = (equivShrink α).symm.symm ((equivShrink α).symm ((equivShrink α) x))⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : α ≃ₜ β<VAR>s : Compacts α<GOAL>↑(Compacts.map ⇑f.symm ⋯ (Compacts.map ⇑f ⋯ s)) = ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : α ≃ₜ β<VAR>s : Compacts β<GOAL>↑(Compacts.map ⇑f ⋯ (Compacts.map ⇑f.symm ⋯ s)) = ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a✝ b c d e : α<VAR>m n : ℤ<VAR>a : α<GOAL>a / 3 + a / 3 + a / 3 = a
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>B✝ B : GroupFilterBasis G<GOAL>B.N 1 = toFilterBasis.filter
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_2, u_1} C<VAR>inst✝⁵ : HasZeroObject C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : Preadditive C<VAR>inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹ : Pretriangulated C<VAR>S : Subcategory C<VAR>inst✝ : ClosedUnderIsomorphisms S.P<GOAL>S.P 0
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_2, u_1} C<VAR>inst✝⁵ : HasZeroObject C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : Preadditive C<VAR>inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹ : Pretriangulated C<VAR>S : Subcategory C<VAR>inst✝ : ClosedUnderIsomorphisms S.P<VAR>X : C<VAR>hX : IsZero X<VAR>mem : S.P X<GOAL>S.P 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<GOAL>AEMeasurable (v.limRatio ρ) μ
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>p q : ℝ≥0<VAR>hpq : p < q<GOAL>∃ u v_1, MeasurableSet u ∧ MeasurableSet v_1 ∧ {x | v.limRatio ρ x < ↑p} ⊆ u ∧ {x | ↑q < v.limRatio ρ x} ⊆ v_1 ∧ μ (u ∩ v_1) = 0
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>inst✝ : IsDomain R<GOAL>∃ q, ExpChar R q
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>inst✝ : IsDomain R<VAR>h✝ : CharZero R<GOAL>∃ q, ExpChar R q
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>inst✝ : IsDomain R<VAR>p : ℕ<VAR>right✝ : CharP R p<VAR>hp : Nat.Prime p<GOAL>∃ q, ExpChar R q
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ γ : Path x y<GOAL>{ toFun := ⇑γ ∘ σ, continuous_toFun := ⋯ }.toFun 0 = y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ γ : Path x y<GOAL>{ toFun := ⇑γ ∘ σ, continuous_toFun := ⋯ }.toFun 1 = x
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>f : ι' ↪ ι<VAR>hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))<VAR>i : ι<GOAL>∃ a, f a = i
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>f : ι' ↪ ι<VAR>hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))<VAR>i : ι<VAR>repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr<GOAL>∃ a, f a = i
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>f : ι' ↪ ι<VAR>hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))<VAR>i : ι<VAR>repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr<VAR>l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)<GOAL>∃ a, f a = i
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>f : ι' ↪ ι<VAR>hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))<VAR>i : ι<VAR>repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr<VAR>l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)<VAR>h_total_l : (Finsupp.total ι M R v) l = v i<GOAL>∃ a, f a = i
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>f : ι' ↪ ι<VAR>hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))<VAR>i : ι<VAR>repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr<VAR>l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)<VAR>h_total_l : (Finsupp.total ι M R v) l = v i<VAR>h_total_eq : (Finsupp.total ι M R v) l = (Finsupp.total ι M R v) (Finsupp.single i 1)<GOAL>∃ a, f a = i
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>f : ι' ↪ ι<VAR>hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))<VAR>i : ι<VAR>repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr<VAR>l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)<VAR>h_total_l : (Finsupp.total ι M R v) l = v i<VAR>h_total_eq : (Finsupp.total ι M R v) l = (Finsupp.total ι M R v) (Finsupp.single i 1)<VAR>l_eq : l = Finsupp.single i 1<GOAL>∃ a, f a = i
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>f : ι' ↪ ι<VAR>hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))<VAR>i : ι<VAR>repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr<VAR>l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)<VAR>h_total_l : (Finsupp.total ι M R v) l = v i<VAR>h_total_eq : (Finsupp.total ι M R v) l = (Finsupp.total ι M R v) (Finsupp.single i 1)<VAR>l_eq : Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩) = Finsupp.single i 1<GOAL>∃ a, f a = i