ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<VAR>hfi : ∀ (n : ℕ), IntegrableOn (↑(f n)) (↑I) μ<VAR>hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (↑(f n)) μ.toBoxAdditive.toSMul<VAR>hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖↑(f n) x - g x‖ ≤ ‖↑(f m) x - g x‖<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>ε0' : 0 < ↑ε<VAR>N₀ : ℕ<VAR>hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖↑(f N₀) x - g x‖ ∂μ ≤ ↑ε<VAR>Nx : (ι → ℝ) → ℕ<VAR>hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x<VAR>hNxε : ∀ (x : ι → ℝ), dist (↑(f (Nx x)) x) (g x) ≤ ↑ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x => ⋯.convergenceR (↑(δ (Nx x))) c x<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c (r c) π<VAR>hπp : π.IsPartition<GOAL>dist (integralSum g μ.toBoxAdditive.toSMul π) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤ ((μ ↑I).toReal + 1 + 1) * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<VAR>hfi : ∀ (n : ℕ), IntegrableOn (↑(f n)) (↑I) μ<VAR>hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (↑(f n)) μ.toBoxAdditive.toSMul<VAR>hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖↑(f n) x - g x‖ ≤ ‖↑(f m) x - g x‖<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>ε0' : 0 < ↑ε<VAR>N₀ : ℕ<VAR>hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖↑(f N₀) x - g x‖ ∂μ ≤ ↑ε<VAR>Nx : (ι → ℝ) → ℕ<VAR>hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x<VAR>hNxε : ∀ (x : ι → ℝ), dist (↑(f (Nx x)) x) (g x) ≤ ↑ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x => ⋯.convergenceR (↑(δ (Nx x))) c x<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c (r c) π<VAR>hπp : π.IsPartition<GOAL>dist (integralSum g μ.toBoxAdditive.toSMul π) (∑ J ∈ π.boxes, (μ ↑J).toReal • ↑(f (Nx (π.tag J))) (π.tag J)) + dist (∑ J ∈ π.boxes, (μ ↑J).toReal • ↑(f (Nx (π.tag J))) (π.tag J)) (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in ↑J, ↑(f (Nx (π.tag J))) x ∂μ) + dist (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in ↑J, ↑(f (Nx (π.tag J))) x ∂μ) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤ ((μ ↑I).toReal + 1 + 1) * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<VAR>hfi : ∀ (n : ℕ), IntegrableOn (↑(f n)) (↑I) μ<VAR>hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (↑(f n)) μ.toBoxAdditive.toSMul<VAR>hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖↑(f n) x - g x‖ ≤ ‖↑(f m) x - g x‖<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>ε0' : 0 < ↑ε<VAR>N₀ : ℕ<VAR>hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖↑(f N₀) x - g x‖ ∂μ ≤ ↑ε<VAR>Nx : (ι → ℝ) → ℕ<VAR>hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x<VAR>hNxε : ∀ (x : ι → ℝ), dist (↑(f (Nx x)) x) (g x) ≤ ↑ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x => ⋯.convergenceR (↑(δ (Nx x))) c x<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c (r c) π<VAR>hπp : π.IsPartition<GOAL>dist (integralSum g μ.toBoxAdditive.toSMul π) (∑ J ∈ π.boxes, (μ ↑J).toReal • ↑(f (Nx (π.tag J))) (π.tag J)) + dist (∑ J ∈ π.boxes, (μ ↑J).toReal • ↑(f (Nx (π.tag J))) (π.tag J)) (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in ↑J, ↑(f (Nx (π.tag J))) x ∂μ) + dist (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in ↑J, ↑(f (Nx (π.tag J))) x ∂μ) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤ (μ ↑I).toReal * ↑ε + ↑ε + ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<VAR>hfi : ∀ (n : ℕ), IntegrableOn (↑(f n)) (↑I) μ<VAR>hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (↑(f n)) μ.toBoxAdditive.toSMul<VAR>hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖↑(f n) x - g x‖ ≤ ‖↑(f m) x - g x‖<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>ε0' : 0 < ↑ε<VAR>N₀ : ℕ<VAR>hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖↑(f N₀) x - g x‖ ∂μ ≤ ↑ε<VAR>Nx : (ι → ℝ) → ℕ<VAR>hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x<VAR>hNxε : ∀ (x : ι → ℝ), dist (↑(f (Nx x)) x) (g x) ≤ ↑ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x => ⋯.convergenceR (↑(δ (Nx x))) c x<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c (r c) π<VAR>hπp : π.IsPartition<GOAL>dist (integralSum g μ.toBoxAdditive.toSMul π) (∑ J ∈ π.boxes, (μ ↑J).toReal • ↑(f (Nx (π.tag J))) (π.tag J)) ≤ (μ ↑I).toReal * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<VAR>hfi : ∀ (n : ℕ), IntegrableOn (↑(f n)) (↑I) μ<VAR>hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (↑(f n)) μ.toBoxAdditive.toSMul<VAR>hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖↑(f n) x - g x‖ ≤ ‖↑(f m) x - g x‖<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>ε0' : 0 < ↑ε<VAR>N₀ : ℕ<VAR>hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖↑(f N₀) x - g x‖ ∂μ ≤ ↑ε<VAR>Nx : (ι → ℝ) → ℕ<VAR>hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x<VAR>hNxε : ∀ (x : ι → ℝ), dist (↑(f (Nx x)) x) (g x) ≤ ↑ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x => ⋯.convergenceR (↑(δ (Nx x))) c x<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c (r c) π<VAR>hπp : π.IsPartition<GOAL>dist (∑ J ∈ π.boxes, (μ ↑J).toReal • ↑(f (Nx (π.tag J))) (π.tag J)) (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in ↑J, ↑(f (Nx (π.tag J))) x ∂μ) ≤ ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : (ι → ℝ) → E<VAR>hg : StronglyMeasurable g<VAR>this : SeparableSpace ↑(Set.range g ∪ {0})<VAR>hgi : IntegrableOn g (↑I) μ<VAR>f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯<VAR>hfi : ∀ (n : ℕ), IntegrableOn (↑(f n)) (↑I) μ<VAR>hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (↑(f n)) μ.toBoxAdditive.toSMul<VAR>hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖↑(f n) x - g x‖ ≤ ‖↑(f m) x - g x‖<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>ε0' : 0 < ↑ε<VAR>N₀ : ℕ<VAR>hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖↑(f N₀) x - g x‖ ∂μ ≤ ↑ε<VAR>Nx : (ι → ℝ) → ℕ<VAR>hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x<VAR>hNxε : ∀ (x : ι → ℝ), dist (↑(f (Nx x)) x) (g x) ≤ ↑ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x => ⋯.convergenceR (↑(δ (Nx x))) c x<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c (r c) π<VAR>hπp : π.IsPartition<GOAL>dist (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in ↑J, ↑(f (Nx (π.tag J))) x ∂μ) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤ ↑ε
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<VAR>hY : IsZero X<GOAL>biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y)
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<VAR>hY : IsZero X<GOAL>0 = biprod.fst
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : Group G'<VAR>inst✝⁵ : Group G''<VAR>A : Type u_4<VAR>inst✝⁴ : AddGroup A<VAR>M : Type u_5<VAR>S : Type u_6<VAR>inst✝³ : DivInvMonoid M<VAR>inst✝² : SetLike S M<VAR>hSM : SubgroupClass S M<VAR>H K : S<VAR>inst✝¹ : SetLike S G<VAR>inst✝ : SubgroupClass S G<VAR>x y : G<VAR>h : x ∈ H<VAR>hba : y * x ∈ H<GOAL>y ∈ H
<VAR>step a s n : Nat<VAR>h : a ≤ s<GOAL>map (fun x => x - a) (range' s n step) = range' (s - a) n step
<VAR>step a s n : Nat<VAR>h : a ≤ s<GOAL>map (fun x => x - a) (range' (a + (s - a)) n step) = range' (s - a) n step
<VAR>step a s n : Nat<VAR>h : a ≤ s<GOAL>((fun x => x - a) ∘ fun x => a + x) = id
<VAR>step a s n : Nat<VAR>h : a ≤ s<VAR>x : Nat<GOAL>((fun x => x - a) ∘ fun x => a + x) x = id x
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I J : FractionalIdeal S P<GOAL>↑(I * J) = ↑I * ↑J
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<GOAL>μ.everywherePosSubset s =ᶠ[ae μ] s
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<VAR>A : μ (s \ μ.everywherePosSubset s) ≠ ⊤<GOAL>μ.everywherePosSubset s =ᶠ[ae μ] s
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<VAR>A : μ (s \ μ.everywherePosSubset s) ≠ ⊤<GOAL>∀ i ⊆ s \ μ.everywherePosSubset s, IsCompact i → μ i = 0
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k✝ : Set α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<VAR>A : μ (s \ μ.everywherePosSubset s) ≠ ⊤<VAR>k : Set α<VAR>hk : k ⊆ s \ μ.everywherePosSubset s<VAR>h'k : IsCompact k<GOAL>μ k = 0
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p : RelSeries r<VAR>i : Fin p.length<VAR>a : α<VAR>prev_connect : r (p.toFun i.castSucc) a<VAR>connect_next : r a (p.toFun i.succ)<VAR>m : Fin (p.length + 1)<VAR>x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc<VAR>y : α := i.succ.castSucc.insertNth a p.toFun m.succ<GOAL>r x y
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p : RelSeries r<VAR>i : Fin p.length<VAR>a : α<VAR>prev_connect : r (p.toFun i.castSucc) a<VAR>connect_next : r a (p.toFun i.succ)<VAR>m : Fin (p.length + 1)<VAR>x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc<VAR>y : α := i.succ.castSucc.insertNth a p.toFun m.succ<VAR>hm : ↑m < ↑i<GOAL>r x y
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p : RelSeries r<VAR>i : Fin p.length<VAR>a : α<VAR>prev_connect : r (p.toFun i.castSucc) a<VAR>connect_next : r a (p.toFun i.succ)<VAR>m : Fin (p.length + 1)<VAR>x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc<VAR>y : α := i.succ.castSucc.insertNth a p.toFun m.succ<VAR>hm : ↑m = ↑i<GOAL>r x y
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p : RelSeries r<VAR>i : Fin p.length<VAR>a : α<VAR>prev_connect : r (p.toFun i.castSucc) a<VAR>connect_next : r a (p.toFun i.succ)<VAR>m : Fin (p.length + 1)<VAR>x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc<VAR>y : α := i.succ.castSucc.insertNth a p.toFun m.succ<VAR>hm : ↑i < ↑m<GOAL>r x y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>h : B ⊆ M.E<GOAL>M✶.Base B ↔ M.Base (M.E \ B) ∧ B ⊆ M.E
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 < x<VAR>hy : 0 < y<VAR>hz : z < 0<GOAL>x < y ^ z⁻¹ ↔ y < x ^ z
<VAR>ξ : ℝ<VAR>hξ : Irrational ξ<VAR>q : ℚ<GOAL>∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
<VAR>ξ : ℝ<VAR>hξ : Irrational ξ<VAR>q : ℚ<VAR>h : 0 < |ξ - ↑q|<GOAL>∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
<VAR>ξ : ℝ<VAR>hξ : Irrational ξ<VAR>q : ℚ<VAR>h : 0 < |ξ - ↑q|<VAR>m : ℕ<VAR>hm : 1 / |ξ - ↑q| < ↑m<GOAL>∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
<VAR>ξ : ℝ<VAR>hξ : Irrational ξ<VAR>q : ℚ<VAR>h : 0 < |ξ - ↑q|<VAR>m : ℕ<VAR>hm : 1 / |ξ - ↑q| < ↑m<VAR>m_pos : 0 < ↑m<GOAL>∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
<VAR>ξ : ℝ<VAR>hξ : Irrational ξ<VAR>q : ℚ<VAR>h : 0 < |ξ - ↑q|<VAR>m : ℕ<VAR>hm : 1 / |ξ - ↑q| < ↑m<VAR>m_pos : 0 < ↑m<VAR>q' : ℚ<VAR>hbd : |ξ - ↑q'| ≤ 1 / ((↑m + 1) * ↑q'.den)<VAR>hden : q'.den ≤ m<GOAL>∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
<VAR>ξ : ℝ<VAR>hξ : Irrational ξ<VAR>q : ℚ<VAR>h : 0 < |ξ - ↑q|<VAR>m : ℕ<VAR>hm : 1 / |ξ - ↑q| < ↑m<VAR>m_pos : 0 < ↑m<VAR>q' : ℚ<VAR>hbd : |ξ - ↑q'| ≤ 1 / ((↑m + 1) * ↑q'.den)<VAR>hden : q'.den ≤ m<VAR>den_pos : 0 < ↑q'.den<GOAL>∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
<VAR>ξ : ℝ<VAR>hξ : Irrational ξ<VAR>q : ℚ<VAR>h : 0 < |ξ - ↑q|<VAR>m : ℕ<VAR>hm : 1 / |ξ - ↑q| < ↑m<VAR>m_pos : 0 < ↑m<VAR>q' : ℚ<VAR>hbd : |ξ - ↑q'| ≤ 1 / ((↑m + 1) * ↑q'.den)<VAR>hden : q'.den ≤ m<VAR>den_pos : 0 < ↑q'.den<VAR>md_pos : 0 < (↑m + 1) * ↑q'.den<GOAL>∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
<VAR>ξ : ℝ<VAR>hξ : Irrational ξ<VAR>q : ℚ<VAR>h : 0 < |ξ - ↑q|<VAR>m : ℕ<VAR>hm : 1 / |ξ - ↑q| < ↑m<VAR>m_pos : 0 < ↑m<VAR>q' : ℚ<VAR>hbd : |ξ - ↑q'| ≤ 1 / ((↑m + 1) * ↑q'.den)<VAR>hden : q'.den ≤ m<VAR>den_pos : 0 < ↑q'.den<VAR>md_pos : 0 < (↑m + 1) * ↑q'.den<GOAL>1 / ((↑m + 1) * ↑q'.den) < 1 / ↑q'.den ^ 2
<VAR>ξ : ℝ<VAR>hξ : Irrational ξ<VAR>q : ℚ<VAR>h : 0 < |ξ - ↑q|<VAR>m : ℕ<VAR>hm : 1 / |ξ - ↑q| < ↑m<VAR>m_pos : 0 < ↑m<VAR>q' : ℚ<VAR>hbd : |ξ - ↑q'| ≤ 1 / ((↑m + 1) * ↑q'.den)<VAR>hden : q'.den ≤ m<VAR>den_pos : 0 < ↑q'.den<VAR>md_pos : 0 < (↑m + 1) * ↑q'.den<GOAL>↑q'.den < ↑m + 1
<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>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : IsDomain R<VAR>h : I ≠ ⊤<GOAL>⨅ i, I ^ i = ⊥
<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>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : IsDomain R<VAR>h : I ≠ ⊤<GOAL>⨅ i, I ^ i ≤ ⊥
<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>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : IsDomain R<VAR>h : I ≠ ⊤<VAR>x : R<VAR>hx : x ∈ ⨅ i, I ^ i<GOAL>x ∈ ⊥
<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>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : IsDomain R<VAR>h : I ≠ ⊤<VAR>x : R<VAR>hx : x ∈ ⨅ i, I ^ i<VAR>hx' : x ∉ ⊥<GOAL>False
<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>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : IsDomain R<VAR>h : I ≠ ⊤<VAR>x : R<VAR>hx : x ∈ ⨅ i, I ^ i<VAR>hx' : x ∉ ⊥<VAR>this : x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x<GOAL>False
<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>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : IsDomain R<VAR>h : I ≠ ⊤<VAR>x : R<VAR>hx : x ∈ ⨅ i, I ^ i<VAR>hx' : x ∉ ⊥<VAR>this : x ∈ ⨅ i, I ^ i ↔ ∃ r, ↑r * x = x<GOAL>False
<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>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : IsDomain R<VAR>h : I ≠ ⊤<VAR>x : R<VAR>hx : x ∈ ⨅ i, I ^ i<VAR>hx' : x ∉ ⊥<VAR>this : x ∈ ⨅ i, I ^ i ↔ ∃ r, ↑r * x = x<VAR>r : ↥I<VAR>hr : ↑r * x = x<GOAL>False
<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>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : IsDomain R<VAR>h : I ≠ ⊤<VAR>x : R<VAR>hx : x ∈ ⨅ i, I ^ i<VAR>hx' : x ∉ ⊥<VAR>this✝ : x ∈ ⨅ i, I ^ i ↔ ∃ r, ↑r * x = x<VAR>r : ↥I<VAR>hr : ↑r * x = x<VAR>this : ↑r = 1<GOAL>False
<VAR>p i : ℕ<GOAL>sZMod p i = ↑(sMod p i)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝ : LinearOrderedRing R<VAR>a b : R<VAR>n : ℕ<GOAL>a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>f : R[X]<VAR>h : derivative f = 0<GOAL>f.natDegree = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>h : derivative 0 = 0<GOAL>natDegree 0 = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>f : R[X]<VAR>h : derivative f = 0<VAR>hf : f ≠ 0<GOAL>f.natDegree = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>f : R[X]<VAR>h : derivative f = 0<VAR>hf : f ≠ 0<GOAL>f.degree ≤ 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>f : R[X]<VAR>h : derivative f = 0<VAR>hf : f ≠ 0<VAR>f_nat_degree_pos : 0 < f.degree<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>f : R[X]<VAR>h : derivative f = 0<VAR>hf : f ≠ 0<VAR>f_nat_degree_pos : 0 < f.natDegree<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>f : R[X]<VAR>h : derivative f = 0<VAR>hf : f ≠ 0<VAR>f_nat_degree_pos : 0 < f.natDegree<VAR>m : ℕ := f.natDegree - 1<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>f : R[X]<VAR>h : derivative f = 0<VAR>hf : f ≠ 0<VAR>f_nat_degree_pos : 0 < f.natDegree<VAR>m : ℕ := f.natDegree - 1<VAR>hm : m + 1 = f.natDegree<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>f : R[X]<VAR>h : derivative f = 0<VAR>hf : f ≠ 0<VAR>f_nat_degree_pos : 0 < f.natDegree<VAR>m : ℕ := f.natDegree - 1<VAR>hm : m + 1 = f.natDegree<VAR>h2 : (derivative f).coeff m = f.coeff (m + 1) * (↑m + 1)<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>f : R[X]<VAR>h : ∀ (n : ℕ), (derivative f).coeff n = coeff 0 n<VAR>hf : f ≠ 0<VAR>f_nat_degree_pos : 0 < f.natDegree<VAR>m : ℕ := f.natDegree - 1<VAR>hm : m + 1 = f.natDegree<VAR>h2 : (derivative f).coeff m = f.coeff (m + 1) * (↑m + 1)<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>f : R[X]<VAR>h : ∀ (n : ℕ), (derivative f).coeff n = coeff 0 n<VAR>hf : f ≠ 0<VAR>f_nat_degree_pos : 0 < f.natDegree<VAR>m : ℕ := f.natDegree - 1<VAR>hm : m + 1 = f.natDegree<VAR>h2 : m + 1 = 0 ∨ f.coeff (m + 1) = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>f : R[X]<VAR>h : ∀ (n : ℕ), (derivative f).coeff n = coeff 0 n<VAR>hf : f ≠ 0<VAR>f_nat_degree_pos : 0 < f.natDegree<VAR>m : ℕ := f.natDegree - 1<VAR>hm : m + 1 = f.natDegree<VAR>h2 : f.coeff (m + 1) = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>f : R[X]<VAR>h : ∀ (n : ℕ), (derivative f).coeff n = coeff 0 n<VAR>hf : f ≠ 0<VAR>f_nat_degree_pos : 0 < f.natDegree<VAR>m : ℕ := f.natDegree - 1<VAR>hm : m + 1 = f.natDegree<VAR>h2 : f = 0<GOAL>False
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>a b : M<VAR>inst✝¹ : Invertible ((ι Q) a)<VAR>inst✝ : Invertible (Q a)<GOAL>⅟((ι Q) a) * (ι Q) b * (ι Q) a = (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : SeminormedRing 𝕜<VAR>inst✝ : SMul 𝕜 E<VAR>s t u v A B : Set E<VAR>x✝¹ : 𝕜<VAR>x✝ : ‖x✝¹‖ ≤ 1<GOAL>x✝¹ • ∅ ⊆ ∅
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Field K<VAR>R₁ : Type u_4<VAR>inst✝³ : CommRing R₁<VAR>inst✝² : IsDomain R₁<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I J : FractionalIdeal R₁⁰ K<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<VAR>hIJ : I ≤ J<VAR>x : K<GOAL>x ∈ (fun a => ↑a) J⁻¹ → x ∈ (fun a => ↑a) I⁻¹
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Field K<VAR>R₁ : Type u_4<VAR>inst✝³ : CommRing R₁<VAR>inst✝² : IsDomain R₁<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I J : FractionalIdeal R₁⁰ K<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<VAR>hIJ : I ≤ J<VAR>x : K<GOAL>(∀ y ∈ J, x * y ∈ 1) → ∀ y ∈ I, x * y ∈ 1
<VAR>x y : ℂ<GOAL>SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
<VAR>y : ℂ<GOAL>SameRay ℝ 0 y ↔ 0 = 0 ∨ y = 0 ∨ arg 0 = y.arg
<VAR>x y : ℂ<VAR>hx : x ≠ 0<GOAL>SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
<VAR>x : ℂ<VAR>hx : x ≠ 0<GOAL>SameRay ℝ x 0 ↔ x = 0 ∨ 0 = 0 ∨ x.arg = arg 0
<VAR>x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
<VAR>x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>‖x‖ • y = ‖y‖ • x ↔ ↑(abs y) / ↑(abs x) * x = y
<VAR>x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>↑(abs x) * y = ↑(abs y) * x ↔ ↑(abs y) * x = y * ↑(abs x)