ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : LinearOrder α<VAR>m : Type u_3<VAR>M : Matrix m m R<VAR>b : m → α<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Fintype m<VAR>hM : M.BlockTriangular b<VAR>ih : ∀ t ⊂ image b univ, ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m], M.BlockTriangular b → image b univ = t → M.det = ∏ a ∈ t, (M.toSquareBlock b a).det<VAR>h✝ : Nonempty m<GOAL>M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : LinearOrder α<VAR>m : Type u_3<VAR>M : Matrix m m R<VAR>b : m → α<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Fintype m<VAR>hM : M.BlockTriangular b<VAR>ih : ∀ t ⊂ image b univ, ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m], M.BlockTriangular b → image b univ = t → M.det = ∏ a ∈ t, (M.toSquareBlock b a).det<VAR>h✝ : Nonempty m<VAR>k : α := (image b univ).max' ⋯<GOAL>M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : LinearOrder α<VAR>m : Type u_3<VAR>M : Matrix m m R<VAR>b : m → α<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Fintype m<VAR>hM : M.BlockTriangular b<VAR>ih : ∀ t ⊂ image b univ, ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m], M.BlockTriangular b → image b univ = t → M.det = ∏ a ∈ t, (M.toSquareBlock b a).det<VAR>h✝ : Nonempty m<VAR>k : α := (image b univ).max' ⋯<GOAL>(M.toSquareBlockProp fun i => b i = k).det * (M.toSquareBlockProp fun i => ¬b i = k).det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : LinearOrder α<VAR>m : Type u_3<VAR>M : Matrix m m R<VAR>b : m → α<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Fintype m<VAR>hM : M.BlockTriangular b<VAR>ih : ∀ t ⊂ image b univ, ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m], M.BlockTriangular b → image b univ = t → M.det = ∏ a ∈ t, (M.toSquareBlock b a).det<VAR>h✝ : Nonempty m<VAR>k : α := (image b univ).max' ⋯<GOAL>∀ (i : m), b i = k → ∀ (j : m), ¬b j = k → M i j = 0
<VAR>k k₂ : ℕ<VAR>c : Code<VAR>n x : ℕ<VAR>hl : k + 1 ≤ k₂ + 1<VAR>h : x ∈ evaln (k + 1) c n<GOAL>x ∈ evaln (k₂ + 1) c n
<VAR>k k₂ : ℕ<VAR>c : Code<VAR>n x : ℕ<VAR>hl : k + 1 ≤ k₂ + 1<VAR>h : x ∈ evaln (k + 1) c n<VAR>hl' : k ≤ k₂<GOAL>x ∈ evaln (k₂ + 1) c n
<VAR>k k₂ : ℕ<VAR>c : Code<VAR>n x : ℕ<VAR>hl : k + 1 ≤ k₂ + 1<VAR>h : x ∈ evaln (k + 1) c n<VAR>hl' : k ≤ k₂<VAR>this : ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ}, k ≤ k₂ → (x ∈ o₁ → x ∈ o₂) → (x ∈ do guard (n ≤ k) o₁) → x ∈ do guard (n ≤ k₂) o₂<GOAL>x ∈ evaln (k₂ + 1) c n
<VAR>k k₂ : ℕ<VAR>c : Code<VAR>n x : ℕ<VAR>hl : k + 1 ≤ k₂ + 1<VAR>hl' : k ≤ k₂<VAR>this : ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ}, k ≤ k₂ → (x ∈ o₁ → x ∈ o₂) → (x ∈ do guard (n ≤ k) o₁) → x ∈ do guard (n ≤ k₂) o₂<VAR>h : evaln (k + 1) c n = some x<GOAL>evaln (k₂ + 1) c n = some x
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIicTopology α<VAR>f : β → α<VAR>hf : Continuous f<VAR>x₀ : β<VAR>h : ∀ᶠ (x : β) in cocompact β, f x₀ ≤ f x<GOAL>∀ᶠ (x : β) in cocompact β ⊓ 𝓟 univ, f x₀ ≤ f x
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>x : E<GOAL>(if x ∈ s then ((μ s)⁻¹ • 1) x else 0) = if x ∈ s then (μ s)⁻¹ else 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<GOAL>Convex ℝ (convexBodySum K B)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B c : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>h : 0 ≤ c<GOAL>convexBodySumFun (c • x) ≤ c * convexBodySumFun x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B c : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>h : 0 ≤ c<GOAL>c = |c|
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v w : Fin n → R<VAR>i j : Fin n<GOAL>(vandermonde v * (vandermonde w)ᵀ) i j = ∑ k : Fin n, (v i * w j) ^ ↑k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>hinj : Injective f<VAR>z z' : Sym2 α<GOAL>map f z = map f z' → z = z'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>hinj : Injective f<VAR>z z' : Sym2 α<VAR>x y x' y' : α<GOAL>map f s(x, y) = map f s(x', y') → s(x, y) = s(x', y')
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁴ : Category.{v, u} V<VAR>inst✝³ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>W : Type u_2<VAR>inst✝² : Category.{u_3, u_2} W<VAR>inst✝¹ : Preadditive W<VAR>G : V ⥤ W<VAR>inst✝ : G.Additive<VAR>hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<VAR>n : ι<GOAL>((G.mapHomologicalComplex c).map (nullHomotopicMap' hom)).f n = (nullHomotopicMap' fun i j hij => G.map (hom i j hij)).f n
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁴ : Category.{v, u} V<VAR>inst✝³ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>W : Type u_2<VAR>inst✝² : Category.{u_3, u_2} W<VAR>inst✝¹ : Preadditive W<VAR>G : V ⥤ W<VAR>inst✝ : G.Additive<VAR>hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<VAR>n : ι<GOAL>(nullHomotopicMap fun i j => G.map (dite (c.Rel j i) (hom i j) fun x => 0)).f n = (nullHomotopicMap' fun i j hij => G.map (hom i j hij)).f n
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>p' : G.Walk v w<GOAL>↑(p.append p').support = ↑p.support + ↑p'.support - {v}
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>p' : G.Walk v w<GOAL>↑p.support + ↑p'.support.tail = ↑p.support + ↑p'.support - {v}
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>p' : G.Walk v w<GOAL>{u} + ↑p.support.tail + ↑p'.support.tail = {u} + ↑p.support.tail + ({v} + ↑p'.support.tail) - {v}
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>p' : G.Walk v w<GOAL>{u} + ↑p.support.tail + ↑p'.support.tail = {u} + ↑p.support.tail + (↑p'.support.tail + {v}) - {v}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>f✝ : 𝕜 → E<VAR>a✝ b✝ : 𝕜<VAR>s : Set 𝕜<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E →L[𝕜] F<VAR>g : 𝕜 → E<VAR>a b : 𝕜<VAR>H : a = b → DifferentiableAt 𝕜 g a<GOAL>dslope (⇑f ∘ g) a b = f (dslope g a b)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>f✝ : 𝕜 → E<VAR>a b✝ : 𝕜<VAR>s : Set 𝕜<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E →L[𝕜] F<VAR>g : 𝕜 → E<VAR>b : 𝕜<VAR>H : b = b → DifferentiableAt 𝕜 g b<GOAL>dslope (⇑f ∘ g) b b = f (dslope g b b)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>f✝ : 𝕜 → E<VAR>a✝ b✝ : 𝕜<VAR>s : Set 𝕜<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E →L[𝕜] F<VAR>g : 𝕜 → E<VAR>a b : 𝕜<VAR>H : a = b → DifferentiableAt 𝕜 g a<VAR>hne : b ≠ a<GOAL>dslope (⇑f ∘ g) a b = f (dslope g a b)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_4, u_1} C<VAR>inst✝⁶ : Category.{u_3, u_2} D<VAR>inst✝⁵ : HasZeroMorphisms C<VAR>inst✝⁴ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝³ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : hl₁.IsPreservedBy F<VAR>inst✝ : hl₂.IsPreservedBy F<VAR>γ : LeftHomologyMapData φ hl₁ hl₂<GOAL>F.map (leftHomologyMap' φ hl₁ hl₂) = leftHomologyMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)
<VAR>α✝ : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>x✝ : UniformSpace α<GOAL>𝓤 α = 𝓤 α
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>hab : a ≤ b<VAR>hc : 0 ≤ c<GOAL>(fun x => x * c) '' Icc a b = Icc (a * c) (b * c)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>hab : a ≤ b<VAR>hc : 0 ≤ c<VAR>h✝ : 0 = c<GOAL>(fun x => x * c) '' Icc a b = Icc (a * c) (b * c)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>hab : a ≤ b<VAR>hc : 0 ≤ c<VAR>h✝ : 0 < c<GOAL>(fun x => x * c) '' Icc a b = Icc (a * c) (b * c)
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝ g✝ : α✝ → β<VAR>inst✝¹ : CommMonoid β<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝ : CommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>e : ι → κ<VAR>he : Set.InjOn e ↑s<VAR>hest : Set.MapsTo e ↑s ↑t<VAR>h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1<VAR>h : ∀ i ∈ s, f i = g (e i)<GOAL>∏ i ∈ s, f i = ∏ j ∈ t, g j
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℂ<VAR>b : ℂ<VAR>hl : b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0<GOAL>(∀ᶠ (x : α) in l, f x = 0 → b.re = 0 → b = 0) ↔ b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℂ<VAR>b : ℂ<VAR>hl : b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0<GOAL>(∃ᶠ (x : α) in l, f x = 0) → b.re = 0 → b = 0 ↔ b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
<VAR>x✝ y✝ x y : ℝ<VAR>hy : 0 ≤ y<GOAL>√(x / y) = √x / √y
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type ?u.105022<VAR>inst✝ : MulAction R X<VAR>r : R<VAR>s t : ↥S<GOAL>↑s /ₒ t * (r /ₒ s) = r /ₒ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f✝ g : Filter α<VAR>s✝ t : Set α<VAR>ι : Type w<VAR>s : Finset ι<VAR>f : ι → Set α<GOAL>⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>ι : Type w<VAR>f : ι → Set α<GOAL>⨅ i ∈ ∅, 𝓟 (f i) = 𝓟 (⋂ i ∈ ∅, f i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f✝ g : Filter α<VAR>s✝ t : Set α<VAR>ι : Type w<VAR>f : ι → Set α<VAR>i : ι<VAR>s : Finset ι<VAR>a✝ : i ∉ s<VAR>hs : ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)<GOAL>⨅ i_1 ∈ insert i s, 𝓟 (f i_1) = 𝓟 (⋂ i_1 ∈ insert i s, f i_1)
<VAR>α : Type u<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : FinCategory J<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : OrderTop α<VAR>x y : α<GOAL>limit (pair x y) = Finset.univ.inf (pair x y).obj
<VAR>α : Type u<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : FinCategory J<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : OrderTop α<VAR>x y : α<GOAL>x ⊓ (y ⊓ ⊤) = x ⊓ y
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Basis I X<VAR>hJI : J ⊆ I<VAR>hJ : X ⊆ M.closure J<GOAL>J = I
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Basis I X<VAR>hJI : J ⊆ I<VAR>hJ : X ⊆ M.closure J<GOAL>I ⊆ M.closure J
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<GOAL>SuperpolynomialDecay l k (f * k) ↔ SuperpolynomialDecay l k f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>l : Filter β<VAR>f : α → β<GOAL>Tendsto (fun x => f ↑x) atTop l ↔ Tendsto f (𝓝[<] a) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>l : Filter β<VAR>f : α → β<GOAL>Tendsto (fun x => f ↑x) atTop l ↔ Tendsto (f ∘ Subtype.val) atTop l
<VAR>α : Type u_1<VAR>inst✝ : Lattice α<VAR>h : ∀ (x y z : α), x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z<VAR>x✝ y z : α<VAR>xz : x✝ ≤ z<GOAL>(x✝ ⊔ y) ⊓ z ≤ x✝ ⊔ y ⊓ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b c d : G<VAR>n✝ : ℤ<VAR>a : G<VAR>n : ℕ<GOAL>a ^ (↑n + 1) = a ^ ↑n * a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b c d : G<VAR>n : ℤ<VAR>a : G<GOAL>a ^ (Int.negSucc 0 + 1) = a ^ Int.negSucc 0 * a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b c d : G<VAR>n✝ : ℤ<VAR>a : G<VAR>n : ℕ<GOAL>a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b c d : G<VAR>n✝ : ℤ<VAR>a : G<VAR>n : ℕ<GOAL>a ^ (Int.negSucc (n + 1) + 1) = (a ^ (n + 1))⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b c d : G<VAR>n✝ : ℤ<VAR>a : G<VAR>n : ℕ<GOAL>a ^ (-↑(n + 1)) = (a ^ (n + 1))⁻¹
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t✝ : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>h : IsFundamentalDomain G s μ<VAR>f : α → E<VAR>t : Set α<VAR>hf : IntegrableOn f t μ<GOAL>∑' (g : G), ∫ (x : α) in g • s, f x ∂μ.restrict t = ∑' (g : G), ∫ (x : α) in t ∩ g • s, f x ∂μ
<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✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<GOAL>∃ t, Meq.mk S t = s
<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✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<GOAL>∃ t, Meq.mk S t = s
<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✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<GOAL>∃ t, Meq.mk S t = s
<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✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<GOAL>∃ t, Meq.mk S t = s
<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✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<GOAL>∃ t, Meq.mk S t = s
<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✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<VAR>w : Meq P B := meqOfSep P hsep X S s T t ht<GOAL>∃ t, Meq.mk S t = s
<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✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<VAR>w : Meq P B := meqOfSep P hsep X S s T t ht<GOAL>Meq.mk S (mk w) = s
<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✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<VAR>w : Meq P B := meqOfSep P hsep X S s T t ht<VAR>I : S.Arrow<GOAL>((J.plusObj P).map I.f.op) (mk w) = ↑s I