ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>h : ⊤ ∈ {x | x ≠ ⊤}<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>x y : ↑(π C fun x => x ∈ s)<GOAL>(factors C s x).prod y = if y = x then 1 else 0
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α β : Type u<VAR>s : Set α<VAR>t : (a : α) → a ∈ s → Set β<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>hs : #↑s < c<GOAL>#↑(⋃ a, ⋃ (h : a ∈ s), t a h) < c ↔ ∀ (a : α) (ha : a ∈ s), #↑(t a ha) < c
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalSpace G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>K : Compacts G<GOAL>0 ≤ prehaar (↑K₀) U K
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>q : R[X]<VAR>toFinsupp✝ : R[ℕ]<GOAL>X * { toFinsupp := toFinsupp✝ } = { toFinsupp := toFinsupp✝ } * X
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>q : R[X]<VAR>toFinsupp✝ : R[ℕ]<GOAL>Finsupp.single 1 1 * toFinsupp✝ = toFinsupp✝ * Finsupp.single 1 1
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>q : R[X]<VAR>toFinsupp✝ : R[ℕ]<VAR>x✝ : ℕ<GOAL>(Finsupp.single 1 1 * toFinsupp✝) x✝ = (toFinsupp✝ * Finsupp.single 1 1) x✝
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<GOAL>o.cof = sInf {a | ∃ ι f, lsub f = o ∧ #ι = a}
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<GOAL>∀ b ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}, o.cof ≤ b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<GOAL>o.cof ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s s₁✝ s₂✝ t t₁ t₂ u v : Finset α<VAR>a✝ b : α<VAR>s₁ s₂ : Finset α<VAR>a : α<VAR>h : a ∈ s₂<VAR>x : α<GOAL>x ∈ insert a s₁ ∩ s₂ ↔ x ∈ insert a (s₁ ∩ s₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s s₁✝ s₂✝ t t₁ t₂ u v : Finset α<VAR>a✝ b : α<VAR>s₁ s₂ : Finset α<VAR>a : α<VAR>h : a ∈ s₂<VAR>x : α<VAR>this : x = a ∨ x ∈ s₂ ↔ x ∈ s₂<GOAL>x ∈ insert a s₁ ∩ s₂ ↔ x ∈ insert a (s₁ ∩ s₂)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} A<VAR>inst✝ : Category.{u_4, u_2} B<VAR>F : A ⥤ B<VAR>G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A<VAR>adj₁ : G₁ ⊣ sheafToPresheaf J A<VAR>G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B<VAR>adj₂ : G₂ ⊣ sheafToPresheaf J B<GOAL>J.PreservesSheafification F ↔ ∀ (P : Cᵒᵖ ⥤ A), IsIso (G₂.map (whiskerRight (adj₁.unit.app P) F))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} A<VAR>inst✝ : Category.{u_4, u_2} B<VAR>F : A ⥤ B<VAR>G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A<VAR>adj₁ : G₁ ⊣ sheafToPresheaf J A<VAR>G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B<VAR>adj₂ : G₂ ⊣ sheafToPresheaf J B<GOAL>J.PreservesSheafification F ↔ ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α<VAR>h : s = t<VAR>x : α<GOAL>x ∈ s ↔ x ∈ t
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G : MonCat<VAR>inst✝ : MonoidalCategory V<VAR>A B : Action V G<GOAL>((functorCategoryMonoidalEquivalence V G).μIso A B).inv.app PUnit.unit = 𝟙 (((functorCategoryMonoidalEquivalence V G).obj (A ⊗ B)).obj PUnit.unit)
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G : MonCat<VAR>inst✝ : MonoidalCategory V<VAR>A B : Action V G<GOAL>inv (((functorCategoryMonoidalEquivalence V G).μIso A B).app PUnit.unit).hom = 𝟙 (((functorCategoryMonoidalEquivalence V G).obj (A ⊗ B)).obj PUnit.unit)
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G : MonCat<VAR>inst✝ : MonoidalCategory V<VAR>A B : Action V G<GOAL>(((functorCategoryMonoidalEquivalence V G).μIso A B).app PUnit.unit).hom ≫ 𝟙 (((functorCategoryMonoidalEquivalence V G).obj (A ⊗ B)).obj PUnit.unit) = 𝟙 (((functorCategoryMonoidalEquivalence V G).obj A ⊗ (functorCategoryMonoidalEquivalence V G).obj B).obj PUnit.unit)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>hr : Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst<GOAL>↑r ≤ (q.comp p).radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>hr : Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst<VAR>n : ℕ<GOAL>‖q.comp p n‖₊ * r ^ n ≤ ∑' (i : (n : ℕ) × Composition n), ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>s : Set (WithTop α)<GOAL>IsLUB s (sSup s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>s : Set (WithTop α)<VAR>hs : s = ∅<GOAL>IsLUB s (sSup s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>s : Set (WithTop α)<VAR>hs : s.Nonempty<GOAL>IsLUB s (sSup s)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>f g : HahnSeries ℕ R<VAR>n : ℕ<GOAL>(PowerSeries.coeff R n) ({ toFun := fun f => PowerSeries.mk f.coeff, invFun := fun f => { coeff := fun n => (PowerSeries.coeff R n) f, isPWO_support' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun (f * g)) = (PowerSeries.coeff R n) ({ toFun := fun f => PowerSeries.mk f.coeff, invFun := fun f => { coeff := fun n => (PowerSeries.coeff R n) f, isPWO_support' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun f * { toFun := fun f => PowerSeries.mk f.coeff, invFun := fun f => { coeff := fun n => (PowerSeries.coeff R n) f, isPWO_support' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun g)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>f g : HahnSeries ℕ R<VAR>n : ℕ<GOAL>∑ ij ∈ addAntidiagonal ⋯ ⋯ n, f.coeff ij.1 * g.coeff ij.2 = ∑ x ∈ antidiagonal n, f.coeff x.1 * g.coeff x.2
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : CommMonoid P<VAR>f : M →* N<GOAL>((fun g => { toFun := g.comp, map_one' := ⋯, map_mul' := ⋯ }) 1) f = 1 f
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : CommMonoid P<VAR>g₁ g₂ : N →* P<VAR>f : M →* N<GOAL>({ toFun := fun g => { toFun := g.comp, map_one' := ⋯, map_mul' := ⋯ }, map_one' := ⋯ }.toFun (g₁ * g₂)) f = ({ toFun := fun g => { toFun := g.comp, map_one' := ⋯, map_mul' := ⋯ }, map_one' := ⋯ }.toFun g₁ * { toFun := fun g => { toFun := g.comp, map_one' := ⋯, map_mul' := ⋯ }, map_one' := ⋯ }.toFun g₂) f
<VAR>n p : ℕ<VAR>pp : Prime p<VAR>k a : ℕ<GOAL>a ∈ (p ^ k).divisors ↔ a ∈ map { toFun := fun x => p ^ x, inj' := ⋯ } (range (k + 1))
<VAR>n p : ℕ<VAR>pp : Prime p<VAR>k a : ℕ<GOAL>(∃ j ≤ k, a = p ^ j) ↔ a ∈ map { toFun := fun x => p ^ x, inj' := ⋯ } (range (k + 1))
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>F₁ F₂ : W.Localization ⥤ D<VAR>τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂<VAR>X : C<GOAL>app τ (W.Q.obj X) = τ.app X
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>F₁ F₂ : W.Localization ⥤ D<VAR>τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂<VAR>X : C<GOAL>τ.app ((objEquiv W).invFun (W.Q.obj X)) = τ.app X
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>p.mirror.trailingCoeff = p.leadingCoeff
<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>i j : ZMod 2<GOAL>evenOdd Q i * evenOdd Q j ≤ evenOdd Q (i + j)
<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>i j : ZMod 2<GOAL>Submodule.span R ((⋃ i_1, ↑(LinearMap.range (ι Q) ^ ↑i_1)) * ⋃ i, ↑(LinearMap.range (ι Q) ^ ↑i)) ≤ Submodule.span R (⋃ i_1, ↑(LinearMap.range (ι Q) ^ ↑i_1))
<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>i j : ZMod 2<GOAL>(⋃ i_1, ↑(LinearMap.range (ι Q) ^ ↑i_1)) * ⋃ i, ↑(LinearMap.range (ι Q) ^ ↑i) ⊆ ⋃ i_1, ↑(LinearMap.range (ι Q) ^ ↑i_1)
<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>i j : ZMod 2<GOAL>∀ (i_1 : { n // ↑n = i }) (i_2 : { n // ↑n = j }), ∀ x ∈ ↑(LinearMap.range (ι Q) ^ ↑i_1), ∀ y ∈ ↑(LinearMap.range (ι Q) ^ ↑i_2), x * y ∈ ⋃ i_3, ↑(LinearMap.range (ι Q) ^ ↑i_3)
<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>xi yi : ℕ<VAR>x : CliffordAlgebra Q<VAR>hx : x ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨xi, ⋯⟩)<VAR>y : CliffordAlgebra Q<VAR>hy : y ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨yi, ⋯⟩)<GOAL>x * y ∈ ⋃ i, ↑(LinearMap.range (ι Q) ^ ↑i)
<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>xi yi : ℕ<VAR>x : CliffordAlgebra Q<VAR>hx : x ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨xi, ⋯⟩)<VAR>y : CliffordAlgebra Q<VAR>hy : y ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨yi, ⋯⟩)<GOAL>x * y ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨xi + yi, ⋯⟩)
<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>xi yi : ℕ<VAR>x : CliffordAlgebra Q<VAR>hx : x ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨xi, ⋯⟩)<VAR>y : CliffordAlgebra Q<VAR>hy : y ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨yi, ⋯⟩)<GOAL>x * y ∈ ↑(LinearMap.range (ι Q) ^ xi * LinearMap.range (ι Q) ^ yi)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f✝ f : α → β<VAR>hf : LocallyLipschitz f<VAR>g : α → γ<VAR>hg : LocallyLipschitz g<VAR>x : α<VAR>Kf : ℝ≥0<VAR>t₁ : Set α<VAR>h₁t : t₁ ∈ 𝓝 x<VAR>hfL : LipschitzOnWith Kf f t₁<VAR>Kg : ℝ≥0<VAR>t₂ : Set α<VAR>h₂t : t₂ ∈ 𝓝 x<VAR>hgL : LipschitzOnWith Kg g t₂<GOAL>∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (fun x => (f x, g x)) t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f✝ f : α → β<VAR>hf : LocallyLipschitz f<VAR>g : α → γ<VAR>hg : LocallyLipschitz g<VAR>x : α<VAR>Kf : ℝ≥0<VAR>t₁ : Set α<VAR>h₁t : t₁ ∈ 𝓝 x<VAR>hfL : LipschitzOnWith Kf f t₁<VAR>Kg : ℝ≥0<VAR>t₂ : Set α<VAR>h₂t : t₂ ∈ 𝓝 x<VAR>hgL : LipschitzOnWith Kg g t₂<GOAL>LipschitzOnWith (max Kf Kg) (fun x => (f x, g x)) (t₁ ∩ t₂)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>x y : γ<GOAL>dist x y ≤ 0 ↔ x = y
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α → β<VAR>x✝ y✝ z : α<VAR>s : Set α<VAR>h : Isometry f<VAR>x y : α<GOAL>edist x y ≤ ↑1 * edist (f x) (f y)
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>ι : Type u_2<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type u_3<VAR>inst✝⁴ : (i : ι) → AddCommGroup (G i)<VAR>inst✝³ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>M : Type u_4<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>m : M<VAR>g : G i<GOAL>(directLimitRight f M) (m ⊗ₜ[R] (of R ι G f i) g) = (of R ι (fun x => M ⊗[R] G x) (fun i j h => LinearMap.lTensor M (f i j h)) i) (m ⊗ₜ[R] g)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>inst✝ : Infinite α<VAR>s : Set α<VAR>hs : sᶜ.Finite<VAR>h : s.Finite<GOAL>univ.Finite
<VAR>m k : ℕ+<GOAL>↑(m.mod k) + m.div k * ↑k = ↑m
<VAR>m k : ℕ+<GOAL>↑(m.mod k) + ↑k * m.div k = ↑m
<VAR>α : Type u_1<VAR>f g h : Perm α<VAR>x : α<VAR>hffx : f (f x) = x<VAR>n : ℕ<GOAL>(f ^ Int.negSucc n) x = x ∨ (f ^ Int.negSucc n) x = f x
<VAR>α : Type u_1<VAR>f g h : Perm α<VAR>x : α<VAR>hffx : f (f x) = x<VAR>n : ℕ<GOAL>(f ^ (n + 1 + 1)) x = x ∨ (f ^ (n + 1 + 1)) x = f x
<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>hs : IsFundamentalDomain G s μ<VAR>ht : IsFundamentalDomain G t μ<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (g : G) (x : α), f (g • x) = f x<GOAL>∑' (g : G), ∫⁻ (x : α) in s ∩ g • t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ
<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>ι : Type u_6<VAR>ι' : ι → Type u_7<VAR>dom : Set ι<VAR>hdom : dom.Nonempty<VAR>l : ι → Filter α<VAR>s : (i : ι) → ι' i → Set α<VAR>p : (i : ι) → ι' i → Prop<VAR>hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)<VAR>h : DirectedOn (l ⁻¹'o GE.ge) dom<VAR>t : Set α<GOAL>t ∈ ⨅ i ∈ dom, l i ↔ ∃ i, (i.fst ∈ dom ∧ p i.fst i.snd) ∧ s i.fst i.snd ⊆ t
<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>ι : Type u_6<VAR>ι' : ι → Type u_7<VAR>dom : Set ι<VAR>hdom : dom.Nonempty<VAR>l : ι → Filter α<VAR>s : (i : ι) → ι' i → Set α<VAR>p : (i : ι) → ι' i → Prop<VAR>hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)<VAR>h : DirectedOn (l ⁻¹'o GE.ge) dom<VAR>t : Set α<GOAL>(∃ i ∈ dom, t ∈ l i) ↔ ∃ a b, (⟨a, b⟩.fst ∈ dom ∧ p ⟨a, b⟩.fst ⟨a, b⟩.snd) ∧ s ⟨a, b⟩.fst ⟨a, b⟩.snd ⊆ t
<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>ι : Type u_6<VAR>ι' : ι → Type u_7<VAR>dom : Set ι<VAR>hdom : dom.Nonempty<VAR>l : ι → Filter α<VAR>s : (i : ι) → ι' i → Set α<VAR>p : (i : ι) → ι' i → Prop<VAR>hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)<VAR>h : DirectedOn (l ⁻¹'o GE.ge) dom<VAR>t : Set α<VAR>i : ι<GOAL>i ∈ dom ∧ t ∈ l i → ∃ b, (⟨i, b⟩.fst ∈ dom ∧ p ⟨i, b⟩.fst ⟨i, b⟩.snd) ∧ s ⟨i, b⟩.fst ⟨i, b⟩.snd ⊆ t
<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>ι : Type u_6<VAR>ι' : ι → Type u_7<VAR>dom : Set ι<VAR>hdom : dom.Nonempty<VAR>l : ι → Filter α<VAR>s : (i : ι) → ι' i → Set α<VAR>p : (i : ι) → ι' i → Prop<VAR>hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)<VAR>h : DirectedOn (l ⁻¹'o GE.ge) dom<VAR>t : Set α<VAR>i : ι<GOAL>(∃ b, (⟨i, b⟩.fst ∈ dom ∧ p ⟨i, b⟩.fst ⟨i, b⟩.snd) ∧ s ⟨i, b⟩.fst ⟨i, b⟩.snd ⊆ t) → i ∈ dom ∧ t ∈ l i
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>F : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>F' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace 𝕜 F'<VAR>H : Type u_6<VAR>inst✝³ : TopologicalSpace H<VAR>H' : Type u_7<VAR>inst✝² : TopologicalSpace H'<VAR>G : Type u_8<VAR>inst✝¹ : TopologicalSpace G<VAR>G' : Type u_9<VAR>inst✝ : TopologicalSpace G'<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<GOAL>range ↑(I.prod J) = range ↑I ×ˢ range ↑J
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>F : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>F' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace 𝕜 F'<VAR>H : Type u_6<VAR>inst✝³ : TopologicalSpace H<VAR>H' : Type u_7<VAR>inst✝² : TopologicalSpace H'<VAR>G : Type u_8<VAR>inst✝¹ : TopologicalSpace G<VAR>G' : Type u_9<VAR>inst✝ : TopologicalSpace G'<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<GOAL>(I.prod J).target = I.target ×ˢ J.target
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>T : Set α<VAR>hx : x ∈ T<VAR>S : Set α<GOAL>𝓝[S] x = comap (Prod.mk x) (𝓤 α ⊓ 𝓟 (T ×ˢ S))
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t✝ s₁ s₂ t₁ t₂ u : Set E<VAR>x y : E<VAR>s t : Set E<GOAL>⋃ i₂ ∈ t, ⋃ i₁ ∈ s, segment 𝕜 i₁ i₂ = convexJoin 𝕜 t s
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>α : Type u_11<VAR>β : Type u_12<VAR>f : α → β<VAR>x : β<GOAL>x ∈ ⋃ x, {f x} ↔ x ∈ range f
<VAR>C : Type u_1<VAR>inst✝⁷ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝⁵ : Category.{?u.61156, u_3} E<VAR>M : Type u_4<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>inst✝² : HasShift D M<VAR>inst✝¹ : HasShift E M<VAR>X Y Z T : C<VAR>a b c : M<VAR>f : ShiftedHom X Y a<VAR>g : ShiftedHom Y Z b<VAR>h : b + a = c<VAR>F : C ⥤ D<VAR>inst✝ : F.CommShift M<GOAL>F.map (f ≫ (shiftFunctor C a).map g ≫ (shiftFunctorAdd' C b a c h).inv.app Z) ≫ (F.commShiftIso c).hom.app Z = (F.map f ≫ (F.commShiftIso a).hom.app Y) ≫ (shiftFunctor D a).map (F.map g ≫ (F.commShiftIso b).hom.app Z) ≫ (shiftFunctorAdd' D b a c h).inv.app (F.obj Z)
<VAR>C : Type u_1<VAR>inst✝⁷ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝⁵ : Category.{?u.61156, u_3} E<VAR>M : Type u_4<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>inst✝² : HasShift D M<VAR>inst✝¹ : HasShift E M<VAR>X Y Z T : C<VAR>a b c : M<VAR>f : ShiftedHom X Y a<VAR>g : ShiftedHom Y Z b<VAR>h : b + a = c<VAR>F : C ⥤ D<VAR>inst✝ : F.CommShift M<GOAL>F.map f ≫ F.map ((shiftFunctor C a).map g) ≫ F.map ((shiftFunctorAdd' C b a c h).inv.app Z) ≫ (F.commShiftIso c).hom.app Z = F.map f ≫ (F.commShiftIso a).hom.app Y ≫ (shiftFunctor D a).map (F.map g) ≫ (shiftFunctor D a).map ((F.commShiftIso b).hom.app Z) ≫ (shiftFunctorAdd' D b a c h).inv.app (F.obj Z)
<VAR>C : Type u_1<VAR>inst✝⁷ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝⁵ : Category.{?u.61156, u_3} E<VAR>M : Type u_4<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>inst✝² : HasShift D M<VAR>inst✝¹ : HasShift E M<VAR>X Y Z T : C<VAR>a b c : M<VAR>f : ShiftedHom X Y a<VAR>g : ShiftedHom Y Z b<VAR>h : b + a = c<VAR>F : C ⥤ D<VAR>inst✝ : F.CommShift M<GOAL>F.map f ≫ F.map ((shiftFunctor C a).map g) ≫ F.map ((shiftFunctorAdd' C b a c h).inv.app Z) ≫ (F.commShiftIso c).hom.app Z = F.map f ≫ (shiftFunctor C a ⋙ F).map g ≫ (F.commShiftIso a).hom.app ((shiftFunctor C b).obj Z) ≫ (shiftFunctor D a).map ((F.commShiftIso b).hom.app Z) ≫ (shiftFunctorAdd' D b a c h).inv.app (F.obj Z)
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r f g : R[X]<GOAL>(f * g).coeff (f.natDegree + g.natDegree) = f.coeff f.natDegree * g.coeff g.natDegree
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : Preadditive C<VAR>β γ : Type<VAR>inst✝² : Finite β<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>inst✝¹ : HasBiproduct f<VAR>inst✝ : HasBiproduct (f ∘ ⇑ε)<GOAL>((lift fun b => π f (ε b)) ≫ desc fun b => ι f (ε b)) = 𝟙 (⨁ f)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : Preadditive C<VAR>β γ : Type<VAR>inst✝² : Finite β<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>inst✝¹ : HasBiproduct f<VAR>inst✝ : HasBiproduct (f ∘ ⇑ε)<VAR>val✝ : Fintype β<GOAL>((lift fun b => π f (ε b)) ≫ desc fun b => ι f (ε b)) = 𝟙 (⨁ f)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : Preadditive C<VAR>β γ : Type<VAR>inst✝² : Finite β<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>inst✝¹ : HasBiproduct f<VAR>inst✝ : HasBiproduct (f ∘ ⇑ε)<VAR>val✝ : Fintype β<VAR>g g' : γ<GOAL>ι f g' ≫ ((lift fun b => π f (ε b)) ≫ desc fun b => ι f (ε b)) ≫ π f g = ι f g' ≫ 𝟙 (⨁ f) ≫ π f g
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a : α<GOAL>min a a = a
<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : Even n<VAR>hm : m ∉ Ico 0 ↑n<GOAL>0 < ∏ k ∈ Finset.range n, (m - ↑k)
<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : Even n<VAR>hm : m ∉ Ico 0 ↑n<VAR>h : 0 = ∏ k ∈ Finset.range n, (m - ↑k)<GOAL>m ∈ Ico 0 ↑n
<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : Even n<VAR>hm : m ∉ Ico 0 ↑n<VAR>h : ∃ a ∈ Finset.range n, m - ↑a = 0<GOAL>m ∈ Ico 0 ↑n
<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : Even n<VAR>hm : m ∉ Ico 0 ↑n<VAR>a : ℕ<VAR>ha : a ∈ Finset.range n<VAR>h : m - ↑a = 0<GOAL>m ∈ Ico 0 ↑n
<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : Even n<VAR>hm : m ∉ Ico 0 ↑n<VAR>a : ℕ<VAR>ha : a ∈ Finset.range n<VAR>h : m - ↑a = 0<GOAL>↑a ∈ Ico 0 ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a✝ b✝ : α<VAR>f : β → α<VAR>a b : β<GOAL>⨅ x ∈ {a, b}, f x = f a ⊓ f b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝³ : One α<VAR>f : Filter α<VAR>s : Set α<VAR>inst✝² : One β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : OneHomClass F α β<VAR>φ : F<GOAL>map (⇑φ) 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s t : Multiset α<VAR>a✝ : α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l : Multiset α<VAR>d : l.Nodup<GOAL>a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 →ᵃ[𝕜] E<VAR>a b : E<VAR>L : Filter 𝕜<VAR>s : Set 𝕜<VAR>x : 𝕜<GOAL>HasStrictDerivAt (⇑(lineMap a b)) (b - a) x
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>-x < 0 ↔ 0 < x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝³ : Group α<VAR>inst✝² : DivisionMonoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>m : F<VAR>f g f₁ g₁ : Filter α<VAR>f₂ g₂ : Filter β<VAR>h : f.NeBot<VAR>s t₁ : Set α<VAR>h₁ : t₁ ∈ f<VAR>t₂ : Set α<VAR>h₂ : t₂ ∈ f<VAR>hs : t₁ / t₂ ⊆ s<GOAL>s ∈ 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝³ : Group α<VAR>inst✝² : DivisionMonoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>m : F<VAR>f g f₁ g₁ : Filter α<VAR>f₂ g₂ : Filter β<VAR>h : f.NeBot<VAR>s t₁ : Set α<VAR>h₁ : t₁ ∈ f<VAR>t₂ : Set α<VAR>h₂ : t₂ ∈ f<VAR>hs : t₁ / t₂ ⊆ s<VAR>a : α<VAR>ha₁ : a ∈ t₁<VAR>ha₂ : a ∈ t₂<GOAL>s ∈ 1