ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝ : μ.IsMulRightInvariant<VAR>g : G<VAR>this✝ : QuasiMeasurePreserving (fun h => h * g⁻¹) μ μ<VAR>this : QuasiMeasurePreserving (Inv.inv ∘ (fun h => h * g⁻¹) ∘ Inv.inv) μ μ<GOAL>QuasiMeasurePreserving (fun h => g * h) μ μ
<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✝ : μ.IsMulRightInvariant<VAR>g : G<VAR>this✝ : QuasiMeasurePreserving (fun h => h * g⁻¹) μ μ<VAR>this : QuasiMeasurePreserving (fun x => g * x) μ μ<GOAL>QuasiMeasurePreserving (fun h => g * h) μ μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular<VAR>h' : ∀ (n : ℕ), IsOpen (s n)<VAR>h'' : univ ⊆ ⋃ n, s n<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>r : ℝ≥0∞<VAR>hr : r > μ A<GOAL>∃ U ⊇ A, IsOpen U ∧ μ U < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular<VAR>h' : ∀ (n : ℕ), IsOpen (s n)<VAR>h'' : univ ⊆ ⋃ n, s n<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>r : ℝ≥0∞<VAR>hr : r > μ A<VAR>HA : μ A < ⊤<GOAL>∃ U ⊇ A, IsOpen U ∧ μ U < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular<VAR>h' : ∀ (n : ℕ), IsOpen (s n)<VAR>h'' : univ ⊆ ⋃ n, s n<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>r : ℝ≥0∞<VAR>hr : r > μ A<VAR>HA : μ A < ⊤<VAR>hm : ∀ (n : ℕ), MeasurableSet (s n)<GOAL>∃ U ⊇ A, IsOpen U ∧ μ U < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular<VAR>h' : ∀ (n : ℕ), IsOpen (s n)<VAR>h'' : univ ⊆ ⋃ n, s n<VAR>r : ℝ≥0∞<VAR>hm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>A : ℕ → Set α<VAR>hAm : ∀ (n : ℕ), MeasurableSet (A n)<VAR>hAs : ∀ (n : ℕ), A n ⊆ s n<VAR>hAd : Pairwise (Disjoint on A)<VAR>hA : MeasurableSet (⋃ n, A n)<VAR>hr : r > μ (⋃ n, A n)<VAR>HA : μ (⋃ n, A n) < ⊤<GOAL>∃ U ⊇ ⋃ n, A n, IsOpen U ∧ μ U < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular<VAR>h' : ∀ (n : ℕ), IsOpen (s n)<VAR>h'' : univ ⊆ ⋃ n, s n<VAR>r : ℝ≥0∞<VAR>hm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>A : ℕ → Set α<VAR>hAm : ∀ (n : ℕ), MeasurableSet (A n)<VAR>hAs : ∀ (n : ℕ), A n ⊆ s n<VAR>hAd : Pairwise (Disjoint on A)<VAR>hA : MeasurableSet (⋃ n, A n)<VAR>hr : r > μ (⋃ n, A n)<VAR>HA : μ (⋃ n, A n) < ⊤<VAR>δ : ℕ → ℝ≥0∞<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>hδε : ∑' (i : ℕ), δ i < r - μ (⋃ n, A n)<GOAL>∃ U ⊇ ⋃ n, A n, IsOpen U ∧ μ U < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular<VAR>h' : ∀ (n : ℕ), IsOpen (s n)<VAR>h'' : univ ⊆ ⋃ n, s n<VAR>r : ℝ≥0∞<VAR>hm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>A : ℕ → Set α<VAR>hAm : ∀ (n : ℕ), MeasurableSet (A n)<VAR>hAs : ∀ (n : ℕ), A n ⊆ s n<VAR>hAd : Pairwise (Disjoint on A)<VAR>hA : MeasurableSet (⋃ n, A n)<VAR>hr : r > μ (⋃ n, A n)<VAR>HA : μ (⋃ n, A n) < ⊤<VAR>δ : ℕ → ℝ≥0∞<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r<GOAL>∃ U ⊇ ⋃ n, A n, IsOpen U ∧ μ U < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular<VAR>h' : ∀ (n : ℕ), IsOpen (s n)<VAR>h'' : univ ⊆ ⋃ n, s n<VAR>r : ℝ≥0∞<VAR>hm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>A : ℕ → Set α<VAR>hAm : ∀ (n : ℕ), MeasurableSet (A n)<VAR>hAs : ∀ (n : ℕ), A n ⊆ s n<VAR>hAd : Pairwise (Disjoint on A)<VAR>hA : MeasurableSet (⋃ n, A n)<VAR>hr : r > μ (⋃ n, A n)<VAR>HA : μ (⋃ n, A n) < ⊤<VAR>δ : ℕ → ℝ≥0∞<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r<VAR>this : ∀ (n : ℕ), ∃ U ⊇ A n, IsOpen U ∧ μ U < μ (A n) + δ n<GOAL>∃ U ⊇ ⋃ n, A n, IsOpen U ∧ μ U < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular<VAR>h' : ∀ (n : ℕ), IsOpen (s n)<VAR>h'' : univ ⊆ ⋃ n, s n<VAR>r : ℝ≥0∞<VAR>hm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>A : ℕ → Set α<VAR>hAm : ∀ (n : ℕ), MeasurableSet (A n)<VAR>hAs : ∀ (n : ℕ), A n ⊆ s n<VAR>hAd : Pairwise (Disjoint on A)<VAR>hA : MeasurableSet (⋃ n, A n)<VAR>hr : r > μ (⋃ n, A n)<VAR>HA : μ (⋃ n, A n) < ⊤<VAR>δ : ℕ → ℝ≥0∞<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r<VAR>U : ℕ → Set α<VAR>hAU : ∀ (n : ℕ), U n ⊇ A n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hU : ∀ (n : ℕ), μ (U n) < μ (A n) + δ n<GOAL>∃ U ⊇ ⋃ n, A n, IsOpen U ∧ μ U < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular<VAR>h' : ∀ (n : ℕ), IsOpen (s n)<VAR>h'' : univ ⊆ ⋃ n, s n<VAR>r : ℝ≥0∞<VAR>hm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>A : ℕ → Set α<VAR>hAm : ∀ (n : ℕ), MeasurableSet (A n)<VAR>hAs : ∀ (n : ℕ), A n ⊆ s n<VAR>hAd : Pairwise (Disjoint on A)<VAR>hA : MeasurableSet (⋃ n, A n)<VAR>hr : r > μ (⋃ n, A n)<VAR>HA : μ (⋃ n, A n) < ⊤<VAR>δ : ℕ → ℝ≥0∞<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r<VAR>U : ℕ → Set α<VAR>hAU : ∀ (n : ℕ), U n ⊇ A n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hU : ∀ (n : ℕ), μ (U n) < μ (A n) + δ n<GOAL>μ (⋃ n, U n) < r
<VAR>a₀ a₁ a₂ : Type u<VAR>i : ℕ<GOAL>lift.{v, u} #(Sequence₂ a₀ a₁ a₂ i) = #(Sequence₂ (ULift.{v, u} a₀) (ULift.{v, u} a₁) (ULift.{v, u} a₂) i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r₁ r₂ : ℝ<VAR>h : |r₁| < |r₂|<GOAL>(fun x => ‖r₁ ^ x‖) =o[atTop] fun x => ‖r₂ ^ x‖
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Semiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>i : ι × κ<VAR>r : R<GOAL>(finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) = Finsupp.single i.1 1 ⊗ₜ[R] Finsupp.single i.2 r
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Semiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>i : ι × κ<VAR>r : R<GOAL>(finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i (1 * r)) = Finsupp.single i.1 1 ⊗ₜ[R] Finsupp.single i.2 r
<VAR>b n : ℕ<VAR>hb : 1 < b<VAR>hn : 2 ≤ n<GOAL>(n + b - 1) / b < n
<VAR>b n : ℕ<VAR>hb : 1 < b<VAR>hn : 2 ≤ n<GOAL>n + b ≤ n * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : OrderTop α<VAR>inst✝² : OrderBot β<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : LocallyFiniteOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Ico (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Ico a₁ a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : OrderTop α<VAR>inst✝² : OrderBot β<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : LocallyFiniteOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Ico (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ico a₁ a₂))
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>f : α → ℝ≥0 × ℝ≥0∞ := fun x => (1, infEdist x E / ENNReal.ofReal δ)<VAR>sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p => ↑p.1 - p.2<GOAL>Continuous (sub ∘ f)
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>f : α → ℝ≥0 × ℝ≥0∞ := fun x => (1, infEdist x E / ENNReal.ofReal δ)<VAR>sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p => ↑p.1 - p.2<GOAL>Continuous fun x => (f x).2
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>f : α → ℝ≥0 × ℝ≥0∞ := fun x => (1, infEdist x E / ENNReal.ofReal δ)<VAR>sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p => ↑p.1 - p.2<GOAL>ENNReal.ofReal δ ≠ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b : k<VAR>m n : ℕ<GOAL>fract (↑m / ↑n) = ↑(m % n) / ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b : k<VAR>m : ℕ<GOAL>fract (↑m / ↑0) = ↑(m % 0) / ↑0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b : k<VAR>m n : ℕ<VAR>hn : n > 0<GOAL>fract (↑m / ↑n) = ↑(m % n) / ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b : k<VAR>m n : ℕ<VAR>hn : n > 0<VAR>hn' : 0 < ↑n<GOAL>fract (↑m / ↑n) = ↑(m % n) / ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b : k<VAR>m n : ℕ<VAR>hn : n > 0<VAR>hn' : 0 < ↑n<GOAL>0 ≤ ↑(m % n) / ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b : k<VAR>m n : ℕ<VAR>hn : n > 0<VAR>hn' : 0 < ↑n<GOAL>↑(m % n) / ↑n < 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b : k<VAR>m n : ℕ<VAR>hn : n > 0<VAR>hn' : 0 < ↑n<GOAL>↑m / ↑n - ↑(m % n) / ↑n = ↑(↑m / ↑n)
<VAR>m : ℕ∞<GOAL>↑m = 1 ↔ m = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l : List α<VAR>a m : α<GOAL>l.maximum = ↑m ↔ m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l : List α<VAR>a m : α<GOAL>(m ∈ l ∧ (∀ (a : α), a ∈ l → id a ≤ id m) ∧ ∀ (a : α), a ∈ l → id m ≤ id a → indexOf m l ≤ indexOf a l) ↔ m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l : List α<VAR>a m : α<GOAL>m ∈ l → (∀ (a : α), a ∈ l → a ≤ m) → ∀ (a : α), a ∈ l → m ≤ a → indexOf m l ≤ indexOf a l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l : List α<VAR>a✝¹ m : α<VAR>a✝ : m ∈ l<VAR>h : ∀ (a : α), a ∈ l → a ≤ m<VAR>a : α<VAR>hal : a ∈ l<VAR>hma : m ≤ a<GOAL>indexOf m l ≤ indexOf a l
<VAR>α : Type u_1<VAR>l : List α<VAR>x : Multiset α × Multiset α<VAR>h : x ∈ (powersetAux l).revzip<GOAL>x.1 + x.2 = ↑l
<VAR>α : Type u_1<VAR>l : List α<VAR>x : Multiset α × Multiset α<VAR>h : ∃ a ∈ l.sublists.revzip, Prod.map ofList ofList a = x<GOAL>x.1 + x.2 = ↑l
<VAR>α : Type u_1<VAR>l : List α<VAR>x : Multiset α × Multiset α<VAR>h : ∃ a b, (a, b) ∈ l.sublists.revzip ∧ (↑a, ↑b) = x<GOAL>x.1 + x.2 = ↑l
<VAR>α : Type u_1<VAR>l l₁ l₂ : List α<VAR>h : (l₁, l₂) ∈ l.sublists.revzip<GOAL>(↑l₁, ↑l₂).1 + (↑l₁, ↑l₂).2 = ↑l
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>a✝ : α<VAR>n✝ : Nat<VAR>s✝ : HeapNode α<VAR>h✝ : WF le a✝ s✝ n✝<VAR>res : Heap α<VAR>a : α<VAR>c s : HeapNode α<VAR>n : Nat<VAR>left✝ : ∀ [inst : TotalBLE le], le a✝ a = true<VAR>h : WF le a c n<VAR>h' : WF le a✝ s n<VAR>hr : Heap.WF le (node a c s).rank res<GOAL>WF le a c ((node a c s).rank - 1)
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>a✝ : α<VAR>n✝ : Nat<VAR>s✝ : HeapNode α<VAR>h✝ : WF le a✝ s✝ n✝<VAR>res : Heap α<VAR>a : α<VAR>c s : HeapNode α<VAR>n : Nat<VAR>left✝ : ∀ [inst : TotalBLE le], le a✝ a = true<VAR>h : WF le a c s.rank<VAR>h' : WF le a✝ s n<VAR>hr : Heap.WF le (node a c s).rank res<GOAL>WF le a c ((node a c s).rank - 1)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>A : C ⥤ Type w<VAR>I : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} I<VAR>inst✝² : Small.{w, u₁} I<VAR>F : I ⥤ A.Elements<VAR>inst✝¹ : HasLimitsOfShape I C<VAR>inst✝ : PreservesLimitsOfShape I A<VAR>i i' : I<VAR>f : i ⟶ i'<GOAL>↑(((Functor.const I).obj ⟨limit (F ⋙ π A), liftedConeElement F⟩).map f ≫ (fun i => ⟨limit.π (F ⋙ π A) i, ⋯⟩) i') = ↑((fun i => ⟨limit.π (F ⋙ π A) i, ⋯⟩) i ≫ F.map f)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<GOAL>arccos (⟪x, -y⟫_ℝ / (‖x‖ * ‖-y‖)) = π - arccos (⟪x, y⟫_ℝ / (‖x‖ * ‖y‖))
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : Module R M✝<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>T : Type u_5<VAR>inst✝⁵ : AddCommGroup T<VAR>inst✝⁴ : Module (AdicCompletion I R) T<VAR>ι : Type u_6<VAR>inst✝³ : DecidableEq ι<VAR>M : ι → Type u_7<VAR>inst✝² : (i : ι) → AddCommGroup (M i)<VAR>inst✝¹ : (i : ι) → Module R (M i)<VAR>inst✝ : Fintype ι<VAR>j : ι<VAR>x : AdicCauchySequence I (M j)<GOAL>((sumInv I M ∘ₗ sum I M) ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x) = (LinearMap.id ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : Module R M✝<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>T : Type u_5<VAR>inst✝⁵ : AddCommGroup T<VAR>inst✝⁴ : Module (AdicCompletion I R) T<VAR>ι : Type u_6<VAR>inst✝³ : DecidableEq ι<VAR>M : ι → Type u_7<VAR>inst✝² : (i : ι) → AddCommGroup (M i)<VAR>inst✝¹ : (i : ι) → Module R (M i)<VAR>inst✝ : Fintype ι<VAR>j : ι<VAR>x : AdicCauchySequence I (M j)<VAR>i : ι<GOAL>(component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) i) (((sumInv I M ∘ₗ sum I M) ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x)) = (component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) i) ((LinearMap.id ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x))
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : Module R M✝<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>T : Type u_5<VAR>inst✝⁵ : AddCommGroup T<VAR>inst✝⁴ : Module (AdicCompletion I R) T<VAR>ι : Type u_6<VAR>inst✝³ : DecidableEq ι<VAR>M : ι → Type u_7<VAR>inst✝² : (i : ι) → AddCommGroup (M i)<VAR>inst✝¹ : (i : ι) → Module R (M i)<VAR>inst✝ : Fintype ι<VAR>j : ι<VAR>x : AdicCauchySequence I (M j)<VAR>i : ι<VAR>n : ℕ<GOAL>↑((component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) i) (((sumInv I M ∘ₗ sum I M) ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x))) n = ↑((component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) i) ((LinearMap.id ∘ₗ lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x))) n
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : Module R M✝<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>T : Type u_5<VAR>inst✝⁵ : AddCommGroup T<VAR>inst✝⁴ : Module (AdicCompletion I R) T<VAR>ι : Type u_6<VAR>inst✝³ : DecidableEq ι<VAR>M : ι → Type u_7<VAR>inst✝² : (i : ι) → AddCommGroup (M i)<VAR>inst✝¹ : (i : ι) → Module R (M i)<VAR>inst✝ : Fintype ι<VAR>j : ι<VAR>x : AdicCauchySequence I (M j)<VAR>i : ι<VAR>n : ℕ<GOAL>Submodule.Quotient.mk ((component R ι M i) ((lof R ι M j) (↑x n))) = ↑((component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) i) ((lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((mk I (M j)) x))) n
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : Module R M✝<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>T : Type u_5<VAR>inst✝⁵ : AddCommGroup T<VAR>inst✝⁴ : Module (AdicCompletion I R) T<VAR>ι : Type u_6<VAR>inst✝³ : DecidableEq ι<VAR>M : ι → Type u_7<VAR>inst✝² : (i : ι) → AddCommGroup (M i)<VAR>inst✝¹ : (i : ι) → Module R (M i)<VAR>inst✝ : Fintype ι<VAR>j : ι<VAR>x : AdicCauchySequence I (M j)<VAR>i : ι<VAR>n : ℕ<GOAL>Submodule.Quotient.mk (if h : j = i then Eq.recOn h (↑x n) else 0) = ↑(if h : j = i then Eq.recOn h ((mk I (M j)) x) else 0) n
<VAR>xl✝ xr✝ : Type u<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u_1<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>zl zr : Type u_1<VAR>zL : zl → PGame<VAR>zR : zr → PGame<VAR>h : mk xl xr xL xR ≤ mk yl yr yL yR<GOAL>mk xl xr xL xR + mk zl zr zL zR ≤ mk yl yr yL yR + mk zl zr zL zR
<VAR>xl✝ xr✝ : Type u<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u_1<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>zl zr : Type u_1<VAR>zL : zl → PGame<VAR>zR : zr → PGame<VAR>h : mk xl xr xL xR ≤ mk yl yr yL yR<VAR>i : xl<GOAL>(∃ i', (mk xl xr xL xR + mk zl zr zL zR).moveLeft (Sum.inl i) ≤ (mk yl yr yL yR + mk zl zr zL zR).moveLeft i') ∨ ∃ j, ((mk xl xr xL xR + mk zl zr zL zR).moveLeft (Sum.inl i)).moveRight j ≤ mk yl yr yL yR + mk zl zr zL zR
<VAR>xl✝ xr✝ : Type u<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u_1<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>zl zr : Type u_1<VAR>zL : zl → PGame<VAR>zR : zr → PGame<VAR>h : mk xl xr xL xR ≤ mk yl yr yL yR<VAR>i : zl<GOAL>(∃ i', (mk xl xr xL xR + mk zl zr zL zR).moveLeft (Sum.inr i) ≤ (mk yl yr yL yR + mk zl zr zL zR).moveLeft i') ∨ ∃ j, ((mk xl xr xL xR + mk zl zr zL zR).moveLeft (Sum.inr i)).moveRight j ≤ mk yl yr yL yR + mk zl zr zL zR
<VAR>xl✝ xr✝ : Type u<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u_1<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>zl zr : Type u_1<VAR>zL : zl → PGame<VAR>zR : zr → PGame<VAR>h : mk xl xr xL xR ≤ mk yl yr yL yR<VAR>i : yr<GOAL>(∃ i_1, mk xl xr xL xR + mk zl zr zL zR ≤ ((mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inl i)).moveLeft i_1) ∨ ∃ j', (mk xl xr xL xR + mk zl zr zL zR).moveRight j' ≤ (mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inl i)
<VAR>xl✝ xr✝ : Type u<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u_1<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>zl zr : Type u_1<VAR>zL : zl → PGame<VAR>zR : zr → PGame<VAR>h : mk xl xr xL xR ≤ mk yl yr yL yR<VAR>i : zr<GOAL>(∃ i_1, mk xl xr xL xR + mk zl zr zL zR ≤ ((mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inr i)).moveLeft i_1) ∨ ∃ j', (mk xl xr xL xR + mk zl zr zL zR).moveRight j' ≤ (mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inr i)
<VAR>α : Type u_1<VAR>inst✝⁵ : Mul α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝¹ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>a b : α<GOAL>↑(Iic a * Iio b) ⊆ ↑(Iio (a * b))
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n i j : ℕ<GOAL>(l.rdrop i).rdrop j = l.rdrop (i + j)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>n : ℕ<VAR>S : ComposableArrows C n<VAR>hS : S.IsComplex<VAR>i : ℕ<VAR>hk : autoParam (i + 1 + 1 ≤ n) _auto✝<GOAL>S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 1 + 1) ⋯ hk = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>h : HasProd f a<GOAL>HasProd (fun b => (f b)⁻¹) a⁻¹
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p : R[X]<GOAL>(-p).roots = p.roots
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a✝ b✝ a b : α<VAR>s : Finset α<VAR>x : α<GOAL>x ∈ insert a (insert b s) ↔ x ∈ insert b (insert a s)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : DecidableEq M<VAR>s : Finset M'<GOAL>⇑f '' ↑(Finset.image (fun t => integerMultiple S f s id t) s.attach) = commonDenomOfFinset S f s • ↑s
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : DecidableEq M<VAR>s : Finset M'<GOAL>⇑f '' ((fun t => integerMultiple S f s id t) '' ↑s.attach) = commonDenomOfFinset S f s • ↑s
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t<VAR>G : ℝ → ℝ<VAR>G_mble : Measurable G<VAR>G_nn : 0 ≤ G<VAR>g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t<VAR>G : ℝ → ℝ<VAR>G_mble : Measurable G<VAR>G_nn : 0 ≤ G<VAR>g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G<VAR>g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)