ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : FiniteMeasure α<VAR>ν : FiniteMeasure β<VAR>s : Set (α × β)<VAR>s_mble : MeasurableSet s<GOAL>(μ.prod ν) s = (∫⁻ (x : α), ↑ν (Prod.mk x ⁻¹' s) ∂↑μ).toNNReal
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<GOAL>H.relindex H = 1
<VAR>𝕜 : Type u_1<VAR>A✝¹ : Type u_2<VAR>A✝ : Type u_3<VAR>inst✝³ : Ring A✝<VAR>A : Type u_4<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ha : (spectrum ℝ a).Nonempty<VAR>ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<GOAL>(spectralRadius ℝ a).toNNReal ∈ spectrum ℝ≥0 a
<VAR>𝕜 : Type u_1<VAR>A✝¹ : Type u_2<VAR>A✝ : Type u_3<VAR>inst✝³ : Ring A✝<VAR>A : Type u_4<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ha : (spectrum ℝ a).Nonempty<VAR>ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<VAR>x : ℝ<VAR>hx₁ : x ∈ spectrum ℝ a<VAR>hx₂ : ↑‖x‖₊ = spectralRadius ℝ a<GOAL>(spectralRadius ℝ a).toNNReal ∈ spectrum ℝ≥0 a
<VAR>𝕜 : Type u_1<VAR>A✝¹ : Type u_2<VAR>A✝ : Type u_3<VAR>inst✝³ : Ring A✝<VAR>A : Type u_4<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ha : (spectrum ℝ a).Nonempty<VAR>ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<VAR>x : ℝ<VAR>hx₁ : x ∈ spectrum ℝ a<VAR>hx₂ : ↑‖x‖₊ = spectralRadius ℝ a<GOAL>↑‖x‖₊ ∈ spectrum ℝ a
<VAR>𝕜 : Type u_1<VAR>A✝¹ : Type u_2<VAR>A✝ : Type u_3<VAR>inst✝³ : Ring A✝<VAR>A : Type u_4<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ha : (spectrum ℝ a).Nonempty<VAR>ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<VAR>x : ℝ<VAR>hx₁ : x ∈ spectrum ℝ a<VAR>hx₂ : ↑‖x‖₊ = spectralRadius ℝ a<VAR>this : 0 ≤ x<GOAL>↑‖x‖₊ ∈ spectrum ℝ a
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), IsNormal (f i)<VAR>a : Ordinal.{max u v}<VAR>s : Set Ordinal.{max u v}<VAR>x✝ : s ∈ Set.range fun i => fixedPoints (f i)<VAR>i : ι<VAR>hi : (fun i => fixedPoints (f i)) i = s<GOAL>nfpFamily f a ∈ s
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), IsNormal (f i)<VAR>a : Ordinal.{max u v}<VAR>s : Set Ordinal.{max u v}<VAR>x✝ : s ∈ Set.range fun i => fixedPoints (f i)<VAR>i : ι<VAR>hi : (fun i => fixedPoints (f i)) i = s<GOAL>f i (nfpFamily f a) = nfpFamily f a
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>a : R<VAR>ha : 0 ≤ a<VAR>c : R<GOAL>0 ≤ star c * a * c
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>a : R<VAR>ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)<VAR>c : R<GOAL>0 ≤ star c * a * c
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>a : R<VAR>ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)<VAR>c x : R<VAR>hx : x ∈ range fun s => star s * s<GOAL>0 ≤ star c * x * c
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>a : R<VAR>ha : a ∈ AddSubmonoid.closure (range fun s => star s * s)<VAR>c x y : R<VAR>hx : 0 ≤ star c * x * c<VAR>hy : 0 ≤ star c * y * c<GOAL>0 ≤ star c * (x + y) * c
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>W✝ X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝¹ : HasPushout f g<VAR>inst✝ : HasPushout (G.map f) (G.map g)<VAR>W : C<VAR>h : Y ⟶ W<VAR>k : Z ⟶ W<VAR>w : f ≫ h = g ≫ k<GOAL>G.map f ≫ G.map h = G.map g ≫ G.map k
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>W✝ X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝¹ : HasPushout f g<VAR>inst✝ : HasPushout (G.map f) (G.map g)<VAR>W : C<VAR>h : Y ⟶ W<VAR>k : Z ⟶ W<VAR>w : f ≫ h = g ≫ k<GOAL>pushoutComparison G f g ≫ G.map (pushout.desc h k w) = pushout.desc (G.map h) (G.map k) ⋯
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : HeytingAlgebra α<VAR>a✝ b✝ c a b : α<GOAL>(a ⇨ b)ᶜᶜ = aᶜᶜ ⇨ bᶜᶜ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : HeytingAlgebra α<VAR>a✝ b✝ c a b : α<GOAL>(a ⇨ b)ᶜᶜ ≤ aᶜᶜ ⇨ bᶜᶜ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : HeytingAlgebra α<VAR>a✝ b✝ c a b : α<GOAL>aᶜᶜ ⇨ bᶜᶜ ≤ (a ⇨ b)ᶜᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝² : DecidablePred p<VAR>inst✝¹ : DecidablePred q<VAR>s✝ t : Finset α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>x : α<GOAL>x ∈ filter p (s.erase a) ↔ x ∈ (filter p s).erase a
<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✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid 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>s : Set M<VAR>li : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>t : Finset ↑s<GOAL>LinearIndependent R Subtype.val
<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✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid 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>s : Set M<VAR>li : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>t : Finset ↑s<VAR>f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩<GOAL>LinearIndependent R Subtype.val
<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✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid 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>s : Set M<VAR>li : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>t : Finset ↑s<VAR>f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩<GOAL>Injective f
<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✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid 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>s : Set M<VAR>li : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>t : Finset ↑s<VAR>f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩<VAR>x : M<VAR>hx : x ∈ Finset.map (Embedding.subtype s) t<VAR>y : M<VAR>hy : y ∈ Finset.map (Embedding.subtype s) t<GOAL>f ⟨x, hx⟩ = f ⟨y, hy⟩ → ⟨x, hx⟩ = ⟨y, hy⟩
<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✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid 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>s : Set M<VAR>li : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>t : Finset ↑s<VAR>f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩<VAR>x : M<VAR>hx✝ : x ∈ Finset.map (Embedding.subtype s) t<VAR>hx : ∃ a ∈ t, (Embedding.subtype s) a = x<VAR>y : M<VAR>hy✝ : y ∈ Finset.map (Embedding.subtype s) t<VAR>hy : ∃ a ∈ t, (Embedding.subtype s) a = y<GOAL>f ⟨x, hx✝⟩ = f ⟨y, hy✝⟩ → ⟨x, hx✝⟩ = ⟨y, hy✝⟩
<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✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid 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>s : Set M<VAR>li : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>t : Finset ↑s<VAR>f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩<VAR>a : Subtype s<VAR>_ha : a ∈ t<VAR>hx : (Embedding.subtype s) a ∈ Finset.map (Embedding.subtype s) t<VAR>b : Subtype s<VAR>_hb : b ∈ t<VAR>hy : (Embedding.subtype s) b ∈ Finset.map (Embedding.subtype s) t<GOAL>f ⟨(Embedding.subtype s) a, hx⟩ = f ⟨(Embedding.subtype s) b, hy⟩ → ⟨(Embedding.subtype s) a, hx⟩ = ⟨(Embedding.subtype s) b, hy⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>ι : Sort u_1<VAR>ι' : Sort u_2<VAR>p : ι → Prop<VAR>p' : ι' → Prop<VAR>s : ι → Set (α × α)<VAR>s' : ι' → Set (β × β)<VAR>h : (𝓤 α).HasBasis p s<VAR>h' : (𝓤 β).HasBasis p' s'<VAR>f : α → β<GOAL>UniformInducing f ↔ (∀ (i : ι'), p' i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧ ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
<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>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>Integrable (↑↑(indicatorConstLp p hs hμs c)) μ
<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>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>c = 0 ∨ (μ.restrict s) univ ≠ ⊤
<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>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>(μ.restrict s) univ ≠ ⊤
<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>s : Set (Set α)<GOAL>generate s = generate (sInter '' {t | t.Finite ∧ t ⊆ s})
<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>s : Set (Set α)<GOAL>⋯.filter = (FilterBasis.ofSets s).filter
<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : ℤ<VAR>hb : b ≠ 0<VAR>A : Fin n → ℤ<GOAL>∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑|A i₁ % b - A i₀ % b| < |b| • ε
<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : ℤ<VAR>hb : b ≠ 0<VAR>A : Fin n → ℤ<VAR>hb' : 0 < ↑|b|<GOAL>∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑|A i₁ % b - A i₀ % b| < |b| • ε
<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : ℤ<VAR>hb : b ≠ 0<VAR>A : Fin n → ℤ<VAR>hb' : 0 < ↑|b|<VAR>hbε : 0 < |b| • ε<GOAL>∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑|A i₁ % b - A i₀ % b| < |b| • ε
<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : ℤ<VAR>hb : b ≠ 0<VAR>A : Fin n → ℤ<VAR>hb' : 0 < ↑|b|<VAR>hbε : 0 < |b| • ε<VAR>hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋<GOAL>∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑|A i₁ % b - A i₀ % b| < |b| • ε
<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : ℤ<VAR>hb : b ≠ 0<VAR>A : Fin n → ℤ<VAR>hb' : 0 < ↑|b|<VAR>hbε : 0 < |b| • ε<VAR>hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋<VAR>i₀ i₁ : Fin n<VAR>hi : (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₀ = (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₁<GOAL>↑|A i₁ % b - A i₀ % b| < |b| • ε
<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : ℤ<VAR>hb : b ≠ 0<VAR>A : Fin n → ℤ<VAR>hb' : 0 < ↑|b|<VAR>hbε : 0 < |b| • ε<VAR>hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋<VAR>i₀ i₁ : Fin n<VAR>hi✝ : (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₀ = (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₁<VAR>hi : ↑⌊↑(A i₀ % b) / |b| • ε⌋.natAbs = ↑⌊↑(A i₁ % b) / |b| • ε⌋.natAbs<GOAL>↑|A i₁ % b - A i₀ % b| < |b| • ε
<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : ℤ<VAR>hb : b ≠ 0<VAR>A : Fin n → ℤ<VAR>hb' : 0 < ↑|b|<VAR>hbε : 0 < |b| • ε<VAR>hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋<VAR>i₀ i₁ : Fin n<VAR>hi✝ : (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₀ = (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₁<VAR>hi : ⌊↑(A i₀ % b) / |b| • ε⌋ = ⌊↑(A i₁ % b) / |b| • ε⌋<GOAL>↑|A i₁ % b - A i₀ % b| < |b| • ε
<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : ℤ<VAR>hb : b ≠ 0<VAR>A : Fin n → ℤ<VAR>hb' : 0 < ↑|b|<VAR>hbε : 0 < |b| • ε<VAR>hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋<VAR>i₀ i₁ : Fin n<VAR>hi✝¹ : (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₀ = (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₁<VAR>hi✝ : ⌊↑(A i₀ % b) / |b| • ε⌋ = ⌊↑(A i₁ % b) / |b| • ε⌋<VAR>hi : |↑(A i₀ % b) / |b| • ε - ↑(A i₁ % b) / |b| • ε| < 1<GOAL>↑|A i₁ % b - A i₀ % b| < |b| • ε
<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : ℤ<VAR>hb : b ≠ 0<VAR>A : Fin n → ℤ<VAR>hb' : 0 < ↑|b|<VAR>hbε : 0 < |b| • ε<VAR>hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋<VAR>i₀ i₁ : Fin n<VAR>hi✝¹ : (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₀ = (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₁<VAR>hi✝ : ⌊↑(A i₀ % b) / |b| • ε⌋ = ⌊↑(A i₁ % b) / |b| • ε⌋<VAR>hi : |↑(A i₁ % b) - ↑(A i₀ % b)| < |b| • ε<GOAL>↑|A i₁ % b - A i₀ % b| < |b| • ε
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : LinearOrderedSemifield β<VAR>s : Set ι<VAR>f f₁ f₂ : ι → α<VAR>g g₁ g₂ : ι → β<VAR>hg : StrongLT 0 g<VAR>i j : ι<GOAL>g⁻¹ j < g⁻¹ i → f i ≤ f j ↔ g i < g j → f i ≤ f j
<VAR>s : String<VAR>n : Nat<GOAL>(s.take n).data = List.take n s.data
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>m m0✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>m₁ m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm₁₂ : m₁ ≤ m₂<VAR>hm₂ : m₂ ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm₂)<VAR>hμm₁ this : SigmaFinite (μ.trim ⋯)<VAR>hf : Integrable f μ<GOAL>μ[μ[f|m₂]|m₁] =ᶠ[ae μ] μ[f|m₁]
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>m m0✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>m₁ m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm₁₂ : m₁ ≤ m₂<VAR>hm₂ : m₂ ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm₂)<VAR>hμm₁ this : SigmaFinite (μ.trim ⋯)<VAR>hf : Integrable f μ<GOAL>∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, (μ[μ[f|m₂]|m₁]) x ∂μ = ∫ (x : α) in s, (μ[f|m₁]) x ∂μ
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>m m0✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>f g : α → F'<VAR>s✝ : Set α<VAR>m₁ m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm₁₂ : m₁ ≤ m₂<VAR>hm₂ : m₂ ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm₂)<VAR>hμm₁ this : SigmaFinite (μ.trim ⋯)<VAR>hf : Integrable f μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>a✝ : μ s < ⊤<GOAL>∫ (x : α) in s, (μ[μ[f|m₂]|m₁]) x ∂μ = ∫ (x : α) in s, (μ[f|m₁]) x ∂μ
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>m m0✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>f g : α → F'<VAR>s✝ : Set α<VAR>m₁ m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm₁₂ : m₁ ≤ m₂<VAR>hm₂ : m₂ ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm₂)<VAR>hμm₁ this : SigmaFinite (μ.trim ⋯)<VAR>hf : Integrable f μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>a✝ : μ s < ⊤<GOAL>∫ (x : α) in s, (μ[f|m₂]) x ∂μ = ∫ (x : α) in s, (μ[f|m₁]) x ∂μ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a b : α<VAR>s : Seq α<GOAL>a = b ∨ a ∈ s → a ∈ cons b s
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K✝ L✝ L' M : Set V<VAR>s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j<VAR>sec : s ∈ G.end<VAR>K L : (Finset V)ᵒᵖ<VAR>h : L ⟶ K<VAR>v : V<VAR>vnL : v ∉ Opposite.unop L<VAR>hs : s L = G.componentComplMk vnL<GOAL>G.componentComplFunctor.map h (G.componentComplMk vnL) = G.componentComplMk ⋯
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>γ : J.sheafify P ⟶ Q<VAR>h : J.toSheafify P ≫ γ = η<GOAL>γ = J.sheafifyLift η hQ
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>γ : J.sheafify P ⟶ Q<VAR>h : J.toSheafify P ≫ γ = η<GOAL>J.toPlus (J.plusObj P) ≫ γ = J.plusLift η hQ
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>γ : J.sheafify P ⟶ Q<VAR>h : J.toSheafify P ≫ γ = η<GOAL>J.toPlus P ≫ J.toPlus (J.plusObj P) ≫ γ = η
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>γ : J.sheafify P ⟶ Q<VAR>h : J.toSheafify P ≫ γ = η<GOAL>(J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ γ = η
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : AddCommGroup S<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>inst✝¹ : Module R Q<VAR>inst✝ : Module R S<VAR>f : N →ₗ[R] P<GOAL>rTensor M (-f) = -rTensor M f
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : AddCommGroup S<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>inst✝¹ : Module R Q<VAR>inst✝ : Module R S<VAR>f : N →ₗ[R] P<GOAL>(rTensorHom M) (-f) = -(rTensorHom M) f
<VAR>σ : Type u<VAR>K : Type v<VAR>inst✝ : Field K<VAR>I : Ideal (MvPolynomial σ K)<VAR>hI : I ≠ ⊤<GOAL>Function.Injective ⇑((Ideal.Quotient.mk I).comp C)
<VAR>σ : Type u<VAR>K : Type v<VAR>inst✝ : Field K<VAR>I : Ideal (MvPolynomial σ K)<VAR>hI : I ≠ ⊤<VAR>x : K<VAR>hx : ((Ideal.Quotient.mk I).comp C) x = 0<GOAL>x = 0
<VAR>σ : Type u<VAR>K : Type v<VAR>inst✝ : Field K<VAR>I : Ideal (MvPolynomial σ K)<VAR>hI : I ≠ ⊤<VAR>x : K<VAR>hx : C x ∈ I<GOAL>x = 0
<VAR>σ : Type u<VAR>K : Type v<VAR>inst✝ : Field K<VAR>I : Ideal (MvPolynomial σ K)<VAR>hI : I ≠ ⊤<VAR>x : K<VAR>hx : C x ∈ I<VAR>hx0 : ¬x = 0<GOAL>1 ∈ I
<VAR>σ : Type u<VAR>K : Type v<VAR>inst✝ : Field K<VAR>I : Ideal (MvPolynomial σ K)<VAR>hI : I ≠ ⊤<VAR>x : K<VAR>hx : C x ∈ I<VAR>hx0 : ¬x = 0<VAR>this : C x⁻¹ * C x ∈ I<GOAL>1 ∈ I
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CancelCommMonoidWithZero R<VAR>inst✝⁴ : UniqueFactorizationMonoid R<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝¹ : CancelCommMonoidWithZero β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>i : α → ℕ<VAR>p : α<VAR>hps : p ∉ s<VAR>is_prime : ∀ q ∈ insert p s, Prime q<VAR>is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'<GOAL>IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CancelCommMonoidWithZero R<VAR>inst✝⁴ : UniqueFactorizationMonoid R<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝¹ : CancelCommMonoidWithZero β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>i : α → ℕ<VAR>p : α<VAR>hps : p ∉ s<VAR>is_prime : ∀ q ∈ insert p s, Prime q<VAR>is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'<VAR>hp : Prime p<GOAL>IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CancelCommMonoidWithZero R<VAR>inst✝⁴ : UniqueFactorizationMonoid R<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝¹ : CancelCommMonoidWithZero β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>i : α → ℕ<VAR>p : α<VAR>hps : p ∉ s<VAR>is_prime : ∀ q ∈ insert p s, Prime q<VAR>is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'<VAR>hp : Prime p<GOAL>∀ ⦃d : α⦄, d ∣ p ^ i p → d ∣ ∏ p' ∈ s, p' ^ i p' → ¬Prime d
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CancelCommMonoidWithZero R<VAR>inst✝⁴ : UniqueFactorizationMonoid R<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝¹ : CancelCommMonoidWithZero β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>i : α → ℕ<VAR>p : α<VAR>hps : p ∉ s<VAR>is_prime : ∀ q ∈ insert p s, Prime q<VAR>is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'<VAR>hp : Prime p<VAR>d : α<VAR>hdp : d ∣ p ^ i p<VAR>hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'<VAR>hd : Prime d<GOAL>p ∈ s
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CancelCommMonoidWithZero R<VAR>inst✝⁴ : UniqueFactorizationMonoid R<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝¹ : CancelCommMonoidWithZero β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>i : α → ℕ<VAR>p : α<VAR>hps : p ∉ s<VAR>is_prime : ∀ q ∈ insert p s, Prime q<VAR>is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'<VAR>hp : Prime p<VAR>d : α<VAR>hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'<VAR>hd : Prime d<VAR>hdp : d ∣ p<GOAL>p ∈ s
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CancelCommMonoidWithZero R<VAR>inst✝⁴ : UniqueFactorizationMonoid R<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝¹ : CancelCommMonoidWithZero β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>i : α → ℕ<VAR>p : α<VAR>hps : p ∉ s<VAR>is_prime : ∀ q ∈ insert p s, Prime q<VAR>is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'<VAR>hp : Prime p<VAR>d : α<VAR>hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'<VAR>hd : Prime d<VAR>hdp : d ∣ p<VAR>q : α<VAR>q_mem' : q ∈ Multiset.map (fun p' => p' ^ i p') s.val<VAR>hdq : d ∣ q<GOAL>p ∈ s