ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : PropertyIsLocal P<VAR>R S : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set R<VAR>hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)<VAR>hs : Ideal.map f (Ideal.span s) = Ideal.map f ⊤<GOAL>P f
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : PropertyIsLocal P<VAR>R S : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set R<VAR>hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)<VAR>hs : Ideal.span (⇑f '' s) = ⊤<GOAL>P f
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : PropertyIsLocal P<VAR>R S : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set R<VAR>hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)<VAR>hs : Ideal.span (⇑f '' s) = ⊤<GOAL>∀ (r : ↑(⇑f '' s)), P ((algebraMap S (Localization.Away ↑r)).comp f)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : PropertyIsLocal P<VAR>R S : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set R<VAR>hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)<VAR>hs : Ideal.span (⇑f '' s) = ⊤<VAR>r : R<VAR>hr : r ∈ s<GOAL>P ((algebraMap S (Localization.Away ↑⟨f r, ⋯⟩)).comp f)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : PropertyIsLocal P<VAR>R S : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set R<VAR>hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)<VAR>hs : Ideal.span (⇑f '' s) = ⊤<VAR>r : R<VAR>hr : r ∈ s<GOAL>(algebraMap S (Localization.Away ↑⟨f r, ⋯⟩)).comp f = (Localization.awayMap f ↑⟨r, hr⟩).comp (algebraMap R (Localization.Away r))
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h : F.Stable<VAR>e : F.N 0 ≤ F'.N 0<VAR>n₀ : ℕ<VAR>hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)<GOAL>∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h : F.Stable<VAR>e : F.N 0 ≤ F'.N 0<VAR>n₀ : ℕ<VAR>hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)<GOAL>∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>ρ : Measure (β × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : α<GOAL>(fun b => (Kernel.const α ρ).condKernel (a, b)) =ᶠ[ae ρ.fst] ⇑ρ.condKernel
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>ρ : Measure (β × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : α<VAR>h : (fun b => (Kernel.const α ρ).condKernel (a, b)) =ᶠ[ae ((Kernel.const α ρ).fst a)] ⇑((Kernel.const α ρ) a).condKernel<GOAL>(fun b => (Kernel.const α ρ).condKernel (a, b)) =ᶠ[ae ρ.fst] ⇑ρ.condKernel
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>ρ : Measure (β × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : α<VAR>h : (fun b => (Kernel.const α ρ).condKernel (a, b)) =ᶠ[ae (Measure.map Prod.fst ρ)] ⇑ρ.condKernel<GOAL>(fun b => (Kernel.const α ρ).condKernel (a, b)) =ᶠ[ae ρ.fst] ⇑ρ.condKernel
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>f : ι × ι' → α<VAR>hs : s.SupIndep fun i => t.sup fun i' => f (i, i')<VAR>ht : t.SupIndep fun i' => s.sup fun i => f (i, i')<VAR>u : Finset (ι × ι')<VAR>hu : u ⊆ s ×ˢ t<VAR>i : ι<VAR>i' : ι'<VAR>hi : (i, i') ∈ s ×ˢ t<VAR>hiu : (i, i') ∉ u<GOAL>Disjoint (f (i, i')) (u.sup f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>f : ι × ι' → α<VAR>hs : s.SupIndep fun i => t.sup fun i' => f (i, i')<VAR>ht : t.SupIndep fun i' => s.sup fun i => f (i, i')<VAR>u : Finset (ι × ι')<VAR>hu : u ⊆ s ×ˢ t<VAR>i : ι<VAR>i' : ι'<VAR>hi : (i, i') ∈ s ×ˢ t<VAR>hiu : (i, i') ∉ u<GOAL>∀ ⦃i_1 : ι × ι'⦄, i_1 ∈ u → Disjoint (f (i, i')) (f i_1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>f : ι × ι' → α<VAR>hs : s.SupIndep fun i => t.sup fun i' => f (i, i')<VAR>ht : t.SupIndep fun i' => s.sup fun i => f (i, i')<VAR>u : Finset (ι × ι')<VAR>hu : u ⊆ s ×ˢ t<VAR>i : ι<VAR>i' : ι'<VAR>hi : (i, i') ∈ s ×ˢ t<VAR>hiu : (i, i') ∉ u<VAR>j : ι<VAR>j' : ι'<VAR>hj : (j, j') ∈ u<GOAL>Disjoint (f (i, i')) (f (j, j'))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>f : ι × ι' → α<VAR>hs : s.SupIndep fun i => t.sup fun i' => f (i, i')<VAR>ht : t.SupIndep fun i' => s.sup fun i => f (i, i')<VAR>u : Finset (ι × ι')<VAR>hu : u ⊆ s ×ˢ t<VAR>i : ι<VAR>i' : ι'<VAR>hi : (i, i') ∈ s ×ˢ t<VAR>hiu : (i, i') ∉ u<VAR>j : ι<VAR>j' : ι'<VAR>hj : (j, j') ∈ u<VAR>hij : (i, i') ≠ (j, j')<GOAL>Disjoint (f (i, i')) (f (j, j'))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>f : ι × ι' → α<VAR>hs : s.SupIndep fun i => t.sup fun i' => f (i, i')<VAR>ht : t.SupIndep fun i' => s.sup fun i => f (i, i')<VAR>u : Finset (ι × ι')<VAR>hu : u ⊆ s ×ˢ t<VAR>i : ι<VAR>i' : ι'<VAR>hi : (i, i') ∈ s ×ˢ t<VAR>hiu : (i, i') ∉ u<VAR>j : ι<VAR>j' : ι'<VAR>hij : (i, i') ≠ (j, j')<VAR>hj : (j, j') ∈ s ×ˢ t<GOAL>Disjoint (f (i, i')) (f (j, j'))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>f : ι × ι' → α<VAR>hs : s.SupIndep fun i => t.sup fun i' => f (i, i')<VAR>ht : t.SupIndep fun i' => s.sup fun i => f (i, i')<VAR>u : Finset (ι × ι')<VAR>hu : u ⊆ s ×ˢ t<VAR>i : ι<VAR>i' : ι'<VAR>hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t<VAR>hiu : (i, i') ∉ u<VAR>j : ι<VAR>j' : ι'<VAR>hij : (i, i') ≠ (j, j')<VAR>hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t<GOAL>Disjoint (f (i, i')) (f (j, j'))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>f : ι × ι' → α<VAR>hs : s.SupIndep fun i => t.sup fun i' => f (i, i')<VAR>ht : t.SupIndep fun i' => s.sup fun i => f (i, i')<VAR>u : Finset (ι × ι')<VAR>hu : u ⊆ s ×ˢ t<VAR>i : ι<VAR>i' : ι'<VAR>hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t<VAR>hiu : (i, i') ∉ u<VAR>j' : ι'<VAR>hij : (i, i') ≠ (i, j')<VAR>hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t<GOAL>Disjoint (f (i, i')) (f (i, j'))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>f : ι × ι' → α<VAR>hs : s.SupIndep fun i => t.sup fun i' => f (i, i')<VAR>ht : t.SupIndep fun i' => s.sup fun i => f (i, i')<VAR>u : Finset (ι × ι')<VAR>hu : u ⊆ s ×ˢ t<VAR>i : ι<VAR>i' : ι'<VAR>hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t<VAR>hiu : (i, i') ∉ u<VAR>j : ι<VAR>j' : ι'<VAR>hij✝ : (i, i') ≠ (j, j')<VAR>hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t<VAR>hij : i ≠ j<GOAL>Disjoint (f (i, i')) (f (j, j'))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<GOAL>s ∪ t =ᶠ[ae μ] t ↔ μ (s \ t) = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X : CosimplicialObject C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>X✝ Y✝ : C ⥤ D<VAR>η : X✝ ⟶ Y✝<VAR>A : Augmented C<VAR>n : SimplexCategory<GOAL>η.app A.left ≫ 𝟙 (Y✝.obj A.left) ≫ Y✝.map (A.hom.app n) = (𝟙 (X✝.obj A.left) ≫ X✝.map (A.hom.app n)) ≫ η.app (A.right.obj n)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β✝ : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>inst✝² : Div β<VAR>inst✝¹ : MeasurableDiv₂ β<VAR>f : ι → Ω → β<VAR>inst✝ : IsMarkovKernel κ<VAR>hf_indep : iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<GOAL>IndepFun (f i / f j) (f k) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β✝ : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>inst✝² : Div β<VAR>inst✝¹ : MeasurableDiv₂ β<VAR>f : ι → Ω → β<VAR>inst✝ : IsMarkovKernel κ<VAR>hf_indep : iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<VAR>this : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ<GOAL>IndepFun (f i / f j) (f k) κ μ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>h : UniformContinuous f<VAR>a : α<GOAL>map f (mk a) = mk (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>h : UniformContinuous f<VAR>a : α<GOAL>(mk ∘ f) a = mk (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderClosedTopology α<VAR>inst✝ : TopologicalSpace β<VAR>f g : β → α<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>IsOpen {b | f b < g b}
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g volume t₁ t₂<VAR>h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x<VAR>hT : 0 < T<GOAL>Tendsto (fun t => ∫ (x : ℝ) in 0 ..t, g x) atBot atBot
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g volume t₁ t₂<VAR>h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x<VAR>hT : 0 < T<GOAL>Tendsto (fun n => sSup ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊n / T⌋ • ∫ (x : ℝ) in 0 ..T, g x) atBot atBot
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g volume t₁ t₂<VAR>h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x<VAR>hT : 0 < T<GOAL>Tendsto (fun x => ⌊x / T⌋ • ∫ (x : ℝ) in 0 ..T, g x) atBot atBot
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g volume t₁ t₂<VAR>h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x<VAR>hT : 0 < T<GOAL>Tendsto (fun x => ⌊x / T⌋) atBot atBot
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>x y : G<VAR>n : ℤ<GOAL>x ^ n = 1 ↔ n ≡ 0 [ZMOD ↑(orderOf x)]
<VAR>J : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>E : K ⥤ J<VAR>F : J ⥤ C<VAR>G : C ⥤ D<VAR>inst✝² : HasColimit F<VAR>inst✝¹ : HasColimit (E ⋙ F)<VAR>inst✝ : HasColimit (F ⋙ G)<VAR>h : HasColimit ((E ⋙ F) ⋙ G)<VAR>j : K<GOAL>ι ((E ⋙ F) ⋙ G) j ≫ post (E ⋙ F) G ≫ G.map (pre F E) = ι ((E ⋙ F) ⋙ G) j ≫ pre (F ⋙ G) E ≫ post F G
<VAR>J : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>E : K ⥤ J<VAR>F : J ⥤ C<VAR>G : C ⥤ D<VAR>inst✝² : HasColimit F<VAR>inst✝¹ : HasColimit (E ⋙ F)<VAR>inst✝ : HasColimit (F ⋙ G)<VAR>h : HasColimit ((E ⋙ F) ⋙ G)<VAR>j : K<GOAL>G.map (ι F (E.obj j)) = (ι ((E ⋙ F) ⋙ G) j ≫ pre (F ⋙ G) E) ≫ post F G
<VAR>J : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>E : K ⥤ J<VAR>F : J ⥤ C<VAR>G : C ⥤ D<VAR>inst✝² : HasColimit F<VAR>inst✝¹ : HasColimit (E ⋙ F)<VAR>inst✝ : HasColimit (F ⋙ G)<VAR>h : HasColimit ((E ⋙ F) ⋙ G)<VAR>j : K<VAR>this : HasColimit (E ⋙ F ⋙ G)<GOAL>G.map (ι F (E.obj j)) = (ι ((E ⋙ F) ⋙ G) j ≫ pre (F ⋙ G) E) ≫ post F G
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>e : α ≃ β<VAR>he : UniformEmbedding ⇑e<GOAL>CompleteSpace α ↔ CompleteSpace β
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<GOAL>↑(filter (fun x => x ∈ A) (Ioc 0 1)).card / ↑1 ≤ 1
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<GOAL>(filter (fun x => x ∈ A) (Ioc 0 1)).card ≤ 1
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>v₁ v₂ : V<VAR>x : P<GOAL>dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I : Box ι<VAR>i✝ : ι<VAR>x✝ : ℝ<VAR>y : ι → ℝ<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>x : ℝ<VAR>h : x ∈ Ioo (I.lower i) (I.upper i)<VAR>h' : optParam (∀ (j : ι), update I.lower i x j < I.upper j) ⋯<GOAL>I.splitUpper i x = ↑{ lower := update I.lower i x, upper := I.upper, lower_lt_upper := h' }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : PseudoMetricSpace δ<VAR>f : α → δ<VAR>x : δ<VAR>hμ : μ ≠ 0<GOAL>⋃ i, f ⁻¹' Metric.ball x ↑i = univ
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>n : ℕ<VAR>h : 0 < n<GOAL>addOrderOf ↑(p / ↑n) = n
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>n : ℕ<VAR>h : 0 < n<GOAL>n • ↑(p / ↑n) = 0 ∧ ∀ m < n, 0 < m → m • ↑(p / ↑n) ≠ 0
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>n : ℕ<VAR>h : 0 < ↑n<GOAL>n • ↑(p / ↑n) = 0 ∧ ∀ m < n, 0 < m → m • ↑(p / ↑n) ≠ 0
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>n : ℕ<VAR>h : 0 < ↑n<GOAL>↑(↑n * (p / ↑n)) = 0
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>n : ℕ<VAR>h : 0 < ↑n<VAR>m : ℕ<VAR>hn : m < n<VAR>h0 : 0 < m<GOAL>¬↑(↑m * (p / ↑n)) = 0
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>n : ℕ<VAR>h : 0 < ↑n<VAR>m : ℕ<VAR>hn : m < n<VAR>h0 : 0 < m<GOAL>¬∃ n_1, n_1 • p = ↑m * (p / ↑n)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>n : ℕ<VAR>h : 0 < ↑n<VAR>m : ℕ<VAR>hn : m < n<VAR>h0 : 0 < m<VAR>k : ℕ<VAR>hk : k • p = ↑m * (p / ↑n)<GOAL>False
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>n : ℕ<VAR>h : 0 < ↑n<VAR>m : ℕ<VAR>hn : m < n<VAR>h0 : 0 < m<VAR>k : ℕ<VAR>hk : n * k = m<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>inst✝¹ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>n : ℕ<VAR>inst✝ : LinearOrderedCancelAddCommMonoid M<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>ht : t.Nonempty<VAR>hb : t.card • b ≤ ∑ x ∈ s, w x<GOAL>∑ i ∈ t, b ≤ ∑ i ∈ t, ∑ x ∈ filter (fun x => f x = i) s, w x
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (filter (fun a => a ^ n = 1) univ).card ≤ n<GOAL>0 < (filter (fun a => orderOf a = Fintype.card α) univ).card
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (filter (fun a => a ^ n = 1) univ).card ≤ n<GOAL>0 < Fintype.card α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s✝ : Finset α<VAR>a : α<VAR>inst✝² : LinearOrder β<VAR>c : β<VAR>inst✝¹ : Add β<VAR>inst✝ : CovariantClass β β (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>n : WithBot β<VAR>s : Finset α<GOAL>fold max ⊥ (fun x => ↑(f x) + n) s = fold max ⊥ (WithBot.some ∘ f) s + n
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>t : Set α<VAR>a x y : α<GOAL>exterior ∅ = ∅
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t<VAR>hfs : ∀ t ∈ Ico a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t<VAR>hgs : ∀ t ∈ Ico a b, g t ∈ s t<VAR>ha : f a = g a<VAR>t : ℝ<VAR>ht : t ∈ Icc a b<GOAL>f t = g t
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t<VAR>hfs : ∀ t ∈ Ico a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t<VAR>hgs : ∀ t ∈ Ico a b, g t ∈ s t<VAR>ha : f a = g a<VAR>t : ℝ<VAR>ht : t ∈ Icc a b<VAR>this : dist (f t) (g t) ≤ 0 * rexp (↑K * (t - a))<GOAL>f t = g t
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>g : G<GOAL>QuasiMeasurePreserving (fun h => h * g) μ μ
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s✝ : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>g : G<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>μ s = 0 → (map (fun h => h * g) μ) s = 0
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s✝ : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>g : G<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>μ s = 0 → μ s = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : Top α<VAR>inst✝² : Top β<VAR>inst✝¹ : Top γ<VAR>inst✝ : Top δ<VAR>g : TopHom β γ<VAR>f₁ f₂ : TopHom α β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : TopologicalSpace β<VAR>a : α<GOAL>𝓝[>] a ⊔ 𝓝[{a}] a = 𝓝[≥] a
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n₁ n₂ n₃ : ℕ<VAR>h1 : n₁ ≤ n₂<VAR>h2 : n₂ ≤ n₃<VAR>x : TruncatedWittVector p n₃ R<GOAL>(truncate h1) ((truncate h2) x) = (truncate ⋯) x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n₁ n₂ n₃ : ℕ<VAR>h1 : n₁ ≤ n₂<VAR>h2 : n₂ ≤ n₃<VAR>x : 𝕎 R<GOAL>(truncate h1) ((truncate h2) ((WittVector.truncate n₃) x)) = (truncate ⋯) ((WittVector.truncate n₃) x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s✝ t✝ : Set α<VAR>μ ν : Measure α<VAR>s : Set β<VAR>hs : s.Finite<VAR>t : β → Set α<GOAL>IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, IntegrableOn f (t i) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s✝ t✝ : Set α<VAR>μ ν : Measure α<VAR>s : Set β<VAR>hs : s.Finite<VAR>t : β → Set α<GOAL>IntegrableOn f (⋃ i ∈ ∅, t i) μ ↔ ∀ i ∈ ∅, IntegrableOn f (t i) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s✝ t✝ : Set α<VAR>μ ν : Measure α<VAR>s : Set β<VAR>hs : s.Finite<VAR>t : β → Set α<GOAL>∀ {a : β} {s : Set β}, a ∉ s → s.Finite → (IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, IntegrableOn f (t i) μ) → (IntegrableOn f (⋃ i ∈ insert a s, t i) μ ↔ ∀ i ∈ insert a s, IntegrableOn f (t i) μ)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f g : X → ℝ<VAR>s t : Set X<VAR>hf : IntegrableOn f s μ<VAR>hg : IntegrableOn g s μ<VAR>hs : MeasurableSet s<VAR>h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x<GOAL>∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ