ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<VAR>A : C<VAR>x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)<VAR>A' : C<VAR>π : A' ⟶ A<VAR>w✝¹ : Epi π<VAR>x' : A' ⟶ (mappingCone S.f).X n₀<VAR>w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0<VAR>hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫ (mappingCone S.f).homologyπ n₀<VAR>a : A' ⟶ S.X₁.X n₁<VAR>b : A' ⟶ S.X₂.X n₀<VAR>w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0<VAR>hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀<GOAL>(mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫ (mappingCone S.f).homologyπ n₀ ≫ HomologicalComplex.homologyMap (triangle S.f).mor₃ n₀ ≫ ((HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftIso 1 n₀ n₁ ⋯).hom.app S.X₁ = S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<VAR>A : C<VAR>x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)<VAR>A' : C<VAR>π : A' ⟶ A<VAR>w✝¹ : Epi π<VAR>x' : A' ⟶ (mappingCone S.f).X n₀<VAR>w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0<VAR>hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫ (mappingCone S.f).homologyπ n₀<VAR>a : A' ⟶ S.X₁.X n₁<VAR>b : A' ⟶ S.X₂.X n₀<VAR>w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0<VAR>hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀<GOAL>HomologicalComplex.liftCycles S.X₁ ((x' ≫ (triangle S.f).mor₃.f n₀) ≫ (S.X₁.shiftFunctorObjXIso 1 n₀ n₁ ⋯).hom) (n₁ + 1) ⋯ ⋯ ≫ HomologicalComplex.homologyπ S.X₁ n₁ ≫ 𝟙 (((HomologicalComplex.homologyFunctor C (up ℤ) 0).shift n₁).obj S.X₁) = S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<VAR>A : C<VAR>x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)<VAR>A' : C<VAR>π : A' ⟶ A<VAR>w✝¹ : Epi π<VAR>x' : A' ⟶ (mappingCone S.f).X n₀<VAR>w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0<VAR>hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫ (mappingCone S.f).homologyπ n₀<VAR>a : A' ⟶ S.X₁.X n₁<VAR>b : A' ⟶ S.X₂.X n₀<VAR>w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0<VAR>hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀<GOAL>HomologicalComplex.liftCycles S.X₁ ((x' ≫ (triangle S.f).mor₃.f n₀) ≫ (HomologicalComplex.XIsoOfEq S.X₁ ⋯).hom) (n₁ + 1) ⋯ ⋯ ≫ HomologicalComplex.homologyπ S.X₁ n₁ ≫ 𝟙 (HomologicalComplex.homology S.X₁ n₁) = S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<VAR>i j : Ordinal.{u}<VAR>hi : i < o<VAR>hj : j < o<VAR>hij : i ≤ j<GOAL>f i hi ≤ f j hj
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<VAR>i j : Ordinal.{u}<VAR>hi : i < o<VAR>hj : j < o<VAR>hij✝ : i ≤ j<VAR>hij : i < j<GOAL>f i hi ≤ f j hj
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<VAR>i : Ordinal.{u}<VAR>hi hj : i < o<VAR>hij : i ≤ i<GOAL>f i hi ≤ f i hj
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>H : Symmetric R<VAR>s1 s2 : WSeq α<VAR>h : Function.swap (LiftRel R) s2 s1<GOAL>LiftRel R s2 s1
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>I : MultispanIndex C<VAR>inst✝¹ : HasCoproduct I.left<VAR>inst✝ : HasCoproduct I.right<VAR>K₁ K₂ : Multicofork I<VAR>f : K₁ ⟶ K₂<GOAL>K₁.toSigmaCofork.ι.app WalkingParallelPair.zero ≫ f.hom = K₂.toSigmaCofork.ι.app WalkingParallelPair.zero
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>I : MultispanIndex C<VAR>inst✝¹ : HasCoproduct I.left<VAR>inst✝ : HasCoproduct I.right<VAR>K₁ K₂ : Multicofork I<VAR>f : K₁ ⟶ K₂<GOAL>K₁.toSigmaCofork.ι.app WalkingParallelPair.one ≫ f.hom = K₂.toSigmaCofork.ι.app WalkingParallelPair.one
<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>f : α → E<VAR>hf : Integrable f μ<VAR>h'f : StronglyMeasurable f<VAR>A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 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>f : α → E<VAR>hf : Integrable f μ<VAR>h'f : StronglyMeasurable f<VAR>A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'<VAR>t : Set E<VAR>t_count : t.Countable<VAR>ht : range f ⊆ closure t<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 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>f : α → E<VAR>hf : Integrable f μ<VAR>h'f : StronglyMeasurable f<VAR>A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'<VAR>t : Set E<VAR>t_count : t.Countable<VAR>ht : range f ⊆ closure t<VAR>main : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - (A.set n).indicator (fun x => c) y‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - (A.set n).indicator (fun x => c) x‖₊)<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 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>f : α → E<VAR>hf : Integrable f μ<VAR>h'f : StronglyMeasurable f<VAR>A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'<VAR>t : Set E<VAR>t_count : t.Countable<VAR>ht : range f ⊆ closure t<VAR>main : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - (A.set n).indicator (fun x => c) y‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - (A.set n).indicator (fun x => c) x‖₊)<VAR>x : α<VAR>hx : ∀ (n : ℕ), ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - (A.set n).indicator (fun x => c) y‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - (A.set n).indicator (fun x => c) x‖₊)<VAR>h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a<GOAL>Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 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>f : α → E<VAR>hf : Integrable f μ<VAR>h'f : StronglyMeasurable f<VAR>A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'<VAR>t : Set E<VAR>t_count : t.Countable<VAR>ht : range f ⊆ closure t<VAR>main : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - (A.set n).indicator (fun x => c) y‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - (A.set n).indicator (fun x => c) x‖₊)<VAR>x : α<VAR>hx : ∀ (n : ℕ), ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - (A.set n).indicator (fun x => c) y‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - (A.set n).indicator (fun x => c) x‖₊)<VAR>h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a<VAR>M : ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - c‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - c‖₊)<GOAL>Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 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>f : α → E<VAR>hf : Integrable f μ<VAR>h'f : StronglyMeasurable f<VAR>A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'<VAR>t : Set E<VAR>t_count : t.Countable<VAR>ht : range f ⊆ closure t<VAR>main : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - (A.set n).indicator (fun x => c) y‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - (A.set n).indicator (fun x => c) x‖₊)<VAR>x : α<VAR>hx : ∀ (n : ℕ), ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - (A.set n).indicator (fun x => c) y‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - (A.set n).indicator (fun x => c) x‖₊)<VAR>h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a<VAR>M : ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - c‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - c‖₊)<VAR>ε : ℝ≥0∞<VAR>εpos : ε > 0<GOAL>∀ᶠ (x_1 : Set α) in v.filterAt x, (∫⁻ (y : α) in x_1, ↑‖f y - f x‖₊ ∂μ) / μ x_1 ≤ ε
<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>f : α → E<VAR>hf : Integrable f μ<VAR>h'f : StronglyMeasurable f<VAR>A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'<VAR>t : Set E<VAR>t_count : t.Countable<VAR>ht : range f ⊆ closure t<VAR>main : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - (A.set n).indicator (fun x => c) y‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - (A.set n).indicator (fun x => c) x‖₊)<VAR>x : α<VAR>hx : ∀ (n : ℕ), ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - (A.set n).indicator (fun x => c) y‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - (A.set n).indicator (fun x => c) x‖₊)<VAR>h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a<VAR>M : ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - c‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - c‖₊)<VAR>ε : ℝ≥0∞<VAR>εpos : ε > 0<VAR>c : E<VAR>ct : c ∈ t<VAR>xc : ↑‖f x - c‖₊ < ε / 2<GOAL>∀ᶠ (x_1 : Set α) in v.filterAt x, (∫⁻ (y : α) in x_1, ↑‖f y - f x‖₊ ∂μ) / μ x_1 ≤ ε
<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>f : α → E<VAR>hf : Integrable f μ<VAR>h'f : StronglyMeasurable f<VAR>A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'<VAR>t : Set E<VAR>t_count : t.Countable<VAR>ht : range f ⊆ closure t<VAR>main : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - (A.set n).indicator (fun x => c) y‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - (A.set n).indicator (fun x => c) x‖₊)<VAR>x : α<VAR>hx : ∀ (n : ℕ), ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - (A.set n).indicator (fun x => c) y‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - (A.set n).indicator (fun x => c) x‖₊)<VAR>h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a<VAR>M : ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - c‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - c‖₊)<VAR>ε : ℝ≥0∞<VAR>εpos : ε > 0<VAR>c : E<VAR>ct : c ∈ t<VAR>xc : ↑‖f x - c‖₊ < ε / 2<VAR>a : Set α<VAR>ha : (∫⁻ (y : α) in a, ↑‖f y - c‖₊ ∂μ) / μ a < ε / 2<VAR>h'a : 0 < μ a<VAR>h''a : μ a < ⊤<GOAL>(∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a ≤ ε
<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>f : α → E<VAR>hf : Integrable f μ<VAR>h'f : StronglyMeasurable f<VAR>A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'<VAR>t : Set E<VAR>t_count : t.Countable<VAR>ht : range f ⊆ closure t<VAR>main : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - (A.set n).indicator (fun x => c) y‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - (A.set n).indicator (fun x => c) x‖₊)<VAR>x : α<VAR>hx : ∀ (n : ℕ), ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - (A.set n).indicator (fun x => c) y‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - (A.set n).indicator (fun x => c) x‖₊)<VAR>h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a<VAR>M : ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - c‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 ↑‖f x - c‖₊)<VAR>ε : ℝ≥0∞<VAR>εpos : ε > 0<VAR>c : E<VAR>ct : c ∈ t<VAR>xc : ↑‖f x - c‖₊ < ε / 2<VAR>a : Set α<VAR>ha : (∫⁻ (y : α) in a, ↑‖f y - c‖₊ ∂μ) / μ a < ε / 2<VAR>h'a : 0 < μ a<VAR>h''a : μ a < ⊤<GOAL>∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ ≤ ε * μ a
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>h : Disjoint s₁ s₂<GOAL>∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>h : Disjoint s₁ s₂<GOAL>∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁ ∪ s₂, f x) * ∏ x ∈ ∅, f x
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝² : Zero Γ<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : MulZeroOneClass R<GOAL>leadingCoeff 1 = 1
<VAR>a b c : ℝ≥0<VAR>h : a ≠ 0<GOAL>a * b = a * c ↔ b = c
<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 : R[X]<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>hq : q.Monic<VAR>a✝ : Nontrivial S<GOAL>map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
<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 : R[X]<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>hq : q.Monic<VAR>a✝ : Nontrivial S<VAR>this : Nontrivial R<GOAL>map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
<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 : R[X]<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>hq : q.Monic<VAR>a✝ : Nontrivial S<VAR>this✝ : Nontrivial R<VAR>this : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q)<GOAL>map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
<VAR>ι : Type u_1<VAR>I✝ J I : Box ι<VAR>s : Set ι<VAR>i : ι<GOAL>(I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : Center C<VAR>U U' : C<GOAL>((fun U => α_ X.fst Y.fst U ≪≫ whiskerLeftIso X.fst (Y.snd.β U) ≪≫ (α_ X.fst U Y.fst).symm ≪≫ whiskerRightIso (X.snd.β U) Y.fst ≪≫ α_ U X.fst Y.fst) (U ⊗ U')).hom = (α_ (X.fst ⊗ Y.fst) U U').inv ≫ ((fun U => α_ X.fst Y.fst U ≪≫ whiskerLeftIso X.fst (Y.snd.β U) ≪≫ (α_ X.fst U Y.fst).symm ≪≫ whiskerRightIso (X.snd.β U) Y.fst ≪≫ α_ U X.fst Y.fst) U).hom ▷ U' ≫ (α_ U (X.fst ⊗ Y.fst) U').hom ≫ U ◁ ((fun U => α_ X.fst Y.fst U ≪≫ whiskerLeftIso X.fst (Y.snd.β U) ≪≫ (α_ X.fst U Y.fst).symm ≪≫ whiskerRightIso (X.snd.β U) Y.fst ≪≫ α_ U X.fst Y.fst) U').hom ≫ (α_ U U' (X.fst ⊗ Y.fst)).inv
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : Center C<VAR>U U' : C<GOAL>(α_ X.fst Y.fst (U ⊗ U')).hom ≫ X.fst ◁ (Y.snd.β (U ⊗ U')).hom ≫ (α_ X.fst (U ⊗ U') Y.fst).inv ≫ (X.snd.β (U ⊗ U')).hom ▷ Y.fst ≫ (α_ (U ⊗ U') X.fst Y.fst).hom = (α_ (X.fst ⊗ Y.fst) U U').inv ≫ ((α_ X.fst Y.fst U).hom ≫ X.fst ◁ (Y.snd.β U).hom ≫ (α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom) ▷ U' ≫ (α_ U (X.fst ⊗ Y.fst) U').hom ≫ U ◁ ((α_ X.fst Y.fst U').hom ≫ X.fst ◁ (Y.snd.β U').hom ≫ (α_ X.fst U' Y.fst).inv ≫ (X.snd.β U').hom ▷ Y.fst ≫ (α_ U' X.fst Y.fst).hom) ≫ (α_ U U' (X.fst ⊗ Y.fst)).inv
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : Center C<VAR>U U' : C<GOAL>(α_ X.fst Y.fst (U ⊗ U')).hom ≫ X.fst ◁ ((α_ Y.fst U U').inv ≫ (Y.snd.β U).hom ▷ U' ≫ (α_ U Y.fst U').hom ≫ U ◁ (Y.snd.β U').hom ≫ (α_ U U' Y.fst).inv) ≫ (α_ X.fst (U ⊗ U') Y.fst).inv ≫ ((α_ X.fst U U').inv ≫ (X.snd.β U).hom ▷ U' ≫ (α_ U X.fst U').hom ≫ U ◁ (X.snd.β U').hom ≫ (α_ U U' X.fst).inv) ▷ Y.fst ≫ (α_ (U ⊗ U') X.fst Y.fst).hom = (α_ (X.fst ⊗ Y.fst) U U').inv ≫ ((α_ X.fst Y.fst U).hom ≫ X.fst ◁ (Y.snd.β U).hom ≫ (α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom) ▷ U' ≫ (α_ U (X.fst ⊗ Y.fst) U').hom ≫ U ◁ ((α_ X.fst Y.fst U').hom ≫ X.fst ◁ (Y.snd.β U').hom ≫ (α_ X.fst U' Y.fst).inv ≫ (X.snd.β U').hom ▷ Y.fst ≫ (α_ U' X.fst Y.fst).hom) ≫ (α_ U U' (X.fst ⊗ Y.fst)).inv
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : Center C<VAR>U U' : C<VAR>f : U ⟶ U'<GOAL>(X.fst ⊗ Y.fst) ◁ f ≫ ((fun U => α_ X.fst Y.fst U ≪≫ whiskerLeftIso X.fst (Y.snd.β U) ≪≫ (α_ X.fst U Y.fst).symm ≪≫ whiskerRightIso (X.snd.β U) Y.fst ≪≫ α_ U X.fst Y.fst) U').hom = ((fun U => α_ X.fst Y.fst U ≪≫ whiskerLeftIso X.fst (Y.snd.β U) ≪≫ (α_ X.fst U Y.fst).symm ≪≫ whiskerRightIso (X.snd.β U) Y.fst ≪≫ α_ U X.fst Y.fst) U).hom ≫ f ▷ (X.fst ⊗ Y.fst)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : Center C<VAR>U U' : C<VAR>f : U ⟶ U'<GOAL>(X.fst ⊗ Y.fst) ◁ f ≫ (α_ X.fst Y.fst U').hom ≫ X.fst ◁ (Y.snd.β U').hom ≫ (α_ X.fst U' Y.fst).inv ≫ (X.snd.β U').hom ▷ Y.fst ≫ (α_ U' X.fst Y.fst).hom = ((α_ X.fst Y.fst U).hom ≫ X.fst ◁ (Y.snd.β U).hom ≫ (α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom) ≫ f ▷ (X.fst ⊗ Y.fst)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>n : ℤ<VAR>K : CochainComplex C ℤ<VAR>i✝ j✝ k✝ : ℤ<VAR>a✝¹ : (ComplexShape.up ℤ).Rel i✝ j✝<VAR>a✝ : (ComplexShape.up ℤ).Rel j✝ k✝<GOAL>(fun i j => n.negOnePow • K.d (i + n) (j + n)) i✝ j✝ ≫ (fun i j => n.negOnePow • K.d (i + n) (j + n)) j✝ k✝ = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>n : ℤ<VAR>K : CochainComplex C ℤ<VAR>i j : ℤ<VAR>hij : ¬(ComplexShape.up ℤ).Rel i j<GOAL>n.negOnePow • K.d (i + n) (j + n) = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>n : ℤ<VAR>K : CochainComplex C ℤ<VAR>i j : ℤ<VAR>hij : ¬(ComplexShape.up ℤ).Rel i j<GOAL>¬(ComplexShape.up ℤ).Rel (i + n) (j + n)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>n : ℤ<VAR>X✝ Y✝ : CochainComplex C ℤ<VAR>φ : X✝ ⟶ Y✝<VAR>i✝ j✝ : ℤ<VAR>a✝ : (ComplexShape.up ℤ).Rel i✝ j✝<GOAL>φ.f (i✝ + n) ≫ (n.negOnePow • Y✝.d (i✝ + n) (j✝ + n)) = (n.negOnePow • X✝.d (i✝ + n) (j✝ + n)) ≫ φ.f (j✝ + n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s✝ : Finset α<VAR>h : m ≤ n<VAR>hG : G.CliqueFree m<VAR>s : Finset α<VAR>hs : G.IsNClique n s<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s✝ : Finset α<VAR>h : m ≤ n<VAR>hG : G.CliqueFree m<VAR>s : Finset α<VAR>hs : G.IsNClique n s<VAR>t : Finset α<VAR>hts : t ⊆ s<VAR>ht : t.card = m<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<GOAL>l ≤ l' ↔ ∀ t ∈ l', ∃ i, p i ∧ s i ⊆ t
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>inst✝² : Fintype R<VAR>R' : Type v<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>ψ : AddChar R R'<VAR>p n : ℕ<VAR>fp : Fact (Nat.Prime p)<VAR>hch : CharP R' p<VAR>hp : IsUnit ↑p<VAR>hp' : p ≠ 2<VAR>hg : gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)<GOAL>(χ (-1) * ↑(Fintype.card R)) ^ (p ^ n / 2) = χ (↑p ^ n)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>inst✝² : Fintype R<VAR>R' : Type v<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>ψ : AddChar R R'<VAR>p n : ℕ<VAR>fp : Fact (Nat.Prime p)<VAR>hch : CharP R' p<VAR>hp : IsUnit ↑p<VAR>hp' : p ≠ 2<VAR>hg : gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)<VAR>this : gaussSum χ ψ ≠ 0<GOAL>(χ (-1) * ↑(Fintype.card R)) ^ (p ^ n / 2) = χ (↑p ^ n)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>inst✝² : Fintype R<VAR>R' : Type v<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>ψ : AddChar R R'<VAR>p n : ℕ<VAR>fp : Fact (Nat.Prime p)<VAR>hch : CharP R' p<VAR>hp : IsUnit ↑p<VAR>hp' : p ≠ 2<VAR>hg : gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)<VAR>this : gaussSum χ ψ ≠ 0<GOAL>(gaussSum χ ψ ^ 2) ^ (p ^ n / 2) = χ (↑p ^ n)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>inst✝² : Fintype R<VAR>R' : Type v<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>ψ : AddChar R R'<VAR>p n : ℕ<VAR>fp : Fact (Nat.Prime p)<VAR>hch : CharP R' p<VAR>hp : IsUnit ↑p<VAR>hp' : p ≠ 2<VAR>hg : gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)<VAR>this : gaussSum χ ψ ≠ 0<GOAL>(gaussSum χ ψ ^ 2) ^ (p ^ n / 2) * gaussSum χ ψ = χ (↑p ^ n) * gaussSum χ ψ
<VAR>α✝ : Type u<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>n : ℕ<GOAL>↑(Int.negOfNat n) = -↑n
<VAR>J : Type u<VAR>inst✝³ : Preorder J<VAR>inst✝² : IsDirected J fun x x_1 => x ≤ x_1<VAR>F : Jᵒᵖ ⥤ Type v<VAR>inst✝¹ : ∀ (j : Jᵒᵖ), Finite (F.obj j)<VAR>inst✝ : ∀ (j : Jᵒᵖ), Nonempty (F.obj j)<GOAL>F.sections.Nonempty
<VAR>J : Type u<VAR>inst✝³ : Preorder J<VAR>inst✝² : IsDirected J fun x x_1 => x ≤ x_1<VAR>F : Jᵒᵖ ⥤ Type v<VAR>inst✝¹ : ∀ (j : Jᵒᵖ), Finite (F.obj j)<VAR>inst✝ : ∀ (j : Jᵒᵖ), Nonempty (F.obj j)<VAR>h✝ : IsEmpty J<GOAL>F.sections.Nonempty
<VAR>J : Type u<VAR>inst✝³ : Preorder J<VAR>inst✝² : IsDirected J fun x x_1 => x ≤ x_1<VAR>F : Jᵒᵖ ⥤ Type v<VAR>inst✝¹ : ∀ (j : Jᵒᵖ), Finite (F.obj j)<VAR>inst✝ : ∀ (j : Jᵒᵖ), Nonempty (F.obj j)<VAR>h✝ : Nonempty J<GOAL>F.sections.Nonempty
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>n : ℤ<VAR>x : α<GOAL>(f ^ n) x ∈ f.support ↔ x ∈ f.support
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>H : J ⥤ K ⥤ C<VAR>inst✝ : HasLimitsOfShape J C<VAR>k : K<VAR>W : C<VAR>f g : W ⟶ (limit H).obj k<VAR>w : ∀ (j : J), f ≫ (limit.π H j).app k = g ≫ (limit.π H j).app k<GOAL>f = g
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>H : J ⥤ K ⥤ C<VAR>inst✝ : HasLimitsOfShape J C<VAR>k : K<VAR>W : C<VAR>f g : W ⟶ (limit H).obj k<VAR>w : ∀ (j : J), f ≫ (limit.π H j).app k = g ≫ (limit.π H j).app k<GOAL>f ≫ (limitObjIsoLimitCompEvaluation H k).hom = g ≫ (limitObjIsoLimitCompEvaluation H k).hom