ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>b : ℝ<GOAL>{b} = ⋂ r, ⋂ (_ : r > 0), Icc (b - r) (b + r)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Summable fun i => f i ^ p<VAR>hg : Summable fun i => g i ^ q<VAR>H₁ : ∀ (s : Finset ι), ∑ i ∈ s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)<VAR>bdd : BddAbove (Set.range fun s => ∑ i ∈ s, f i * g i)<GOAL>(Summable fun i => f i * g i) ∧ ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Summable fun i => f i ^ p<VAR>hg : Summable fun i => g i ^ q<VAR>H₁ : ∀ (s : Finset ι), ∑ i ∈ s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)<VAR>bdd : BddAbove (Set.range fun s => ∑ i ∈ s, f i * g i)<VAR>H₂ : Summable fun i => f i * g i<GOAL>(Summable fun i => f i * g i) ∧ ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
<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 / a = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>p : ℕ<VAR>inst✝ : Nontrivial R<VAR>h : CharP R p<VAR>hp : p ≠ 2<GOAL>IsPrimitiveRoot (-1) 2
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>p : ℕ<VAR>inst✝ : Nontrivial R<VAR>h : CharP R p<VAR>hp : p ≠ 2<GOAL>2 = orderOf (-1)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>p : ℕ<VAR>inst✝ : Nontrivial R<VAR>h : CharP R p<VAR>hp : p ≠ 2<GOAL>¬ringChar R = 2
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>inst✝ : Fact (1 ≤ p)<GOAL>Continuous fun f => posPart (-f)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>inst✝ : Fintype α<VAR>hG : G.Colorable (card α)<GOAL>G.chromaticNumber = ↑(card α) ↔ ∀ (C : G.Coloring α), Surjective ⇑C
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : mabs a = b<GOAL>a = b ∨ a = b⁻¹
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>Hd : a ∣ b<GOAL>a * (b / a) = b
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e : Trivialization F proj<VAR>x : Z<GOAL>x ∈ e.source ↔ proj x ∈ e.baseSet
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>M M₁ M₂ M₃ : ModuleCat R<VAR>l₁₂ : M₁ ⟶ M₂<VAR>l₂₃ : M₂ ⟶ M₃<VAR>x : ↑(obj' f M₁)<GOAL>(LinearMap.baseChange S (l₁₂ ≫ l₂₃)) x = (LinearMap.baseChange S l₁₂ ≫ LinearMap.baseChange S l₂₃) x
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>M M₁ M₂ M₃ : ModuleCat R<VAR>l₁₂ : M₁ ⟶ M₂<VAR>l₂₃ : M₂ ⟶ M₃<GOAL>(LinearMap.baseChange S (l₁₂ ≫ l₂₃)) 0 = (LinearMap.baseChange S l₁₂ ≫ LinearMap.baseChange S l₂₃) 0
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>M M₁ M₂ M₃ : ModuleCat R<VAR>l₁₂ : M₁ ⟶ M₂<VAR>l₂₃ : M₂ ⟶ M₃<VAR>x✝ : ↑((restrictScalars f).obj (mk S))<VAR>y✝ : ↑M₁<GOAL>(LinearMap.baseChange S (l₁₂ ≫ l₂₃)) (x✝ ⊗ₜ[R] y✝) = (LinearMap.baseChange S l₁₂ ≫ LinearMap.baseChange S l₂₃) (x✝ ⊗ₜ[R] y✝)
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>M M₁ M₂ M₃ : ModuleCat R<VAR>l₁₂ : M₁ ⟶ M₂<VAR>l₂₃ : M₂ ⟶ M₃<VAR>x y : ↑((restrictScalars f).obj (mk S)) ⊗[R] ↑M₁<VAR>ihx : (LinearMap.baseChange S (l₁₂ ≫ l₂₃)) x = (LinearMap.baseChange S l₁₂ ≫ LinearMap.baseChange S l₂₃) x<VAR>ihy : (LinearMap.baseChange S (l₁₂ ≫ l₂₃)) y = (LinearMap.baseChange S l₁₂ ≫ LinearMap.baseChange S l₂₃) y<GOAL>(LinearMap.baseChange S (l₁₂ ≫ l₂₃)) (x + y) = (LinearMap.baseChange S l₁₂ ≫ LinearMap.baseChange S l₂₃) (x + y)
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝² : AddCommMonoid G<VAR>inst✝¹ : AddMonoid H<VAR>inst✝ : AddConstMapClass F G H a b<VAR>f : F<VAR>n : ℕ<VAR>x : G<GOAL>f (n • a + x) = f x + n • b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : CompleteLattice β<VAR>f : α → β<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<GOAL>essSup f (c • μ) = essSup f μ
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)<VAR>x : β<VAR>h : ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (TypeVec.id ::: k) <$$> g f f' x<GOAL>(corec₁ g x).dest = g _root_.id (corec₁ g) x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)<VAR>x : β<VAR>h : ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (TypeVec.id ::: k) <$$> g f f' x<GOAL>g (Sum.elim _root_.id (corec' fun x => g Sum.inl Sum.inr x) ∘ Sum.inl) (Sum.elim _root_.id (corec' fun x => g Sum.inl Sum.inr x) ∘ Sum.inr) x = g _root_.id (corec₁ g) x
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x : ℝ≥0∞<GOAL>x.toReal = 1 ↔ x = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he✝ : OrthogonalIdempotents e<VAR>inst✝ : Fintype I<VAR>he : CompleteOrthogonalIdempotents e<VAR>hf : Function.Injective ⇑f<GOAL>CompleteOrthogonalIdempotents (⇑f ∘ e) ↔ CompleteOrthogonalIdempotents e
<VAR>α : Type u_1<VAR>f g h : Perm α<GOAL>f.Disjoint g⁻¹ ↔ f.Disjoint g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>xs : List α<VAR>h : xs.Nodup<VAR>n : ℕ<VAR>hn : n + 1 < xs.length<GOAL>xs.formPerm (xs.nthLe n ⋯) = xs.nthLe (n + 1) hn
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X✝ Y✝ Z X Y : C<GOAL>X ◁ eqToHom ⋯ = eqToHom ⋯
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>h : T.IsComplete<VAR>φ : L.Sentence<VAR>M : Type u_1<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : M ⊨ T<VAR>inst✝ : Nonempty M<GOAL>M ⊨ φ ↔ T ⊨ᵇ φ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>h : T.IsComplete<VAR>φ : L.Sentence<VAR>M : Type u_1<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : M ⊨ T<VAR>inst✝ : Nonempty M<VAR>hφ : T ⊨ᵇ φ<GOAL>M ⊨ φ ↔ T ⊨ᵇ φ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>h : T.IsComplete<VAR>φ : L.Sentence<VAR>M : Type u_1<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : M ⊨ T<VAR>inst✝ : Nonempty M<VAR>hφn : T ⊨ᵇ Formula.not φ<GOAL>M ⊨ φ ↔ T ⊨ᵇ φ
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n✝ n' a : ℤ<VAR>γ : Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'<VAR>n : ℤ<VAR>hn : n + a = n'<GOAL>δ n (n + 1) ((↑γ).leftUnshift n hn) = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : PseudoEMetricSpace X<VAR>inst✝¹ : PseudoEMetricSpace Y<VAR>inst✝ : PseudoEMetricSpace Z<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>b : X<GOAL>edist (f b) (f b) ≤ ↑C * edist b b ^ ↑r
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : PseudoEMetricSpace X<VAR>inst✝¹ : PseudoEMetricSpace Y<VAR>inst✝ : PseudoEMetricSpace Z<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>b : X<GOAL>0 ≤ ↑C * edist b b ^ ↑r
<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>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Fintype κ<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>f : ι → α<GOAL>(∏ j : ι, if i = j then f j else 1) = f i
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₁ : Type u_3<VAR>V₁' : Type u_4<VAR>V₂ : Type u_5<VAR>V₃ : Type u_6<VAR>V₄ : Type u_7<VAR>P₁ : Type u_8<VAR>P₁' : Type u_9<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>P₃ : Type u_12<VAR>P₄ : Type u_13<VAR>inst✝²⁴ : NormedField 𝕜<VAR>inst✝²³ : SeminormedAddCommGroup V<VAR>inst✝²² : NormedSpace 𝕜 V<VAR>inst✝²¹ : PseudoMetricSpace P<VAR>inst✝²⁰ : NormedAddTorsor V P<VAR>inst✝¹⁹ : SeminormedAddCommGroup V₁<VAR>inst✝¹⁸ : NormedSpace 𝕜 V₁<VAR>inst✝¹⁷ : PseudoMetricSpace P₁<VAR>inst✝¹⁶ : NormedAddTorsor V₁ P₁<VAR>inst✝¹⁵ : SeminormedAddCommGroup V₁'<VAR>inst✝¹⁴ : NormedSpace 𝕜 V₁'<VAR>inst✝¹³ : MetricSpace P₁'<VAR>inst✝¹² : NormedAddTorsor V₁' P₁'<VAR>inst✝¹¹ : SeminormedAddCommGroup V₂<VAR>inst✝¹⁰ : NormedSpace 𝕜 V₂<VAR>inst✝⁹ : PseudoMetricSpace P₂<VAR>inst✝⁸ : NormedAddTorsor V₂ P₂<VAR>inst✝⁷ : SeminormedAddCommGroup V₃<VAR>inst✝⁶ : NormedSpace 𝕜 V₃<VAR>inst✝⁵ : PseudoMetricSpace P₃<VAR>inst✝⁴ : NormedAddTorsor V₃ P₃<VAR>inst✝³ : SeminormedAddCommGroup V₄<VAR>inst✝² : NormedSpace 𝕜 V₄<VAR>inst✝¹ : PseudoMetricSpace P₄<VAR>inst✝ : NormedAddTorsor V₄ P₄<VAR>f : P →ᵃ[𝕜] P₂<VAR>inhabited_h : Inhabited P<VAR>this : ⇑f.linear = ⇑(AffineIsometryEquiv.vaddConst 𝕜 (f default)).toHomeomorph.symm ∘ ⇑f ∘ ⇑(AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph<GOAL>Continuous (⇑(AffineIsometryEquiv.vaddConst 𝕜 (f default)).toHomeomorph.symm ∘ ⇑f ∘ ⇑(AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph) ↔ Continuous ⇑f
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I : LieIdeal R L<VAR>h₁ : I ≤ center R L<VAR>h₂ : IsNilpotent R (L ⧸ I)<GOAL>IsNilpotent R L
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I : LieIdeal R L<VAR>h₁ : I ≤ center R L<VAR>h₂ : IsNilpotent R (L ⧸ I)<GOAL>LieModule.IsNilpotent R L (L ⧸ I)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I : LieIdeal R L<VAR>h₁ : I ≤ center R L<VAR>k : ℕ<VAR>hk : lowerCentralSeries R (L ⧸ I) (L ⧸ I) k = ⊥<GOAL>LieModule.IsNilpotent R L (L ⧸ I)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I : LieIdeal R L<VAR>h₁ : I ≤ center R L<VAR>k : ℕ<VAR>hk : lowerCentralSeries R (L ⧸ I) (L ⧸ I) k = ⊥<GOAL>lowerCentralSeries R L (L ⧸ I) k = ⊥
<VAR>R : CommRingCat<GOAL>map (eqToHom ⋯) = eqToHom ⋯
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>(of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>h : fract v = 0<GOAL>(of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>h : fract v ≠ 0<GOAL>(of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝ : MulOneClass M<VAR>s t : Set α<VAR>f✝ g : α → M<VAR>a : α<VAR>h : a ∉ s ∩ t<VAR>f : α → M<GOAL>(s ∪ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n✝ : ℤ<VAR>γ✝ γ₁ γ₂ : Cochain K L n✝<VAR>a n' : ℤ<VAR>γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'<VAR>n : ℤ<VAR>hn : n' + a = n<VAR>m m' : ℤ<VAR>hm' : m' + a = m<GOAL>δ n m (γ.rightUnshift n hn) = a.negOnePow • (δ n' m' γ).rightUnshift m hm'
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n✝ : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n✝<VAR>a n' n : ℤ<VAR>hn : n' + a = n<VAR>m m' : ℤ<VAR>hm' : m' + a = m<VAR>γ' : Cochain K L n<GOAL>δ n m (((rightShiftAddEquiv K L n a n' hn) γ').rightUnshift n hn) = a.negOnePow • (δ n' m' ((rightShiftAddEquiv K L n a n' hn) γ')).rightUnshift m hm'
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n✝ : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n✝<VAR>a n' n : ℤ<VAR>hn : n' + a = n<VAR>m m' : ℤ<VAR>hm' : m' + a = m<VAR>γ' : Cochain K L n<GOAL>δ n m ((γ'.rightShift a n' hn).rightUnshift n hn) = a.negOnePow • (δ n' m' (γ'.rightShift a n' hn)).rightUnshift m hm'
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y : R<GOAL>W.Equation x y ↔ y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0
<VAR>X : Type u_1<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : CompleteSpace X<VAR>x : X<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ϕ : X → ℝ<VAR>cont : Continuous ϕ<VAR>nonneg : ∀ (y : X), 0 ≤ ϕ y<GOAL>∃ ε' > 0, ∃ x', ε' ≤ ε ∧ d x' x ≤ 2 * ε ∧ ε * ϕ x ≤ ε' * ϕ x' ∧ ∀ (y : X), d x' y ≤ ε' → ϕ y ≤ 2 * ϕ x'
<VAR>X : Type u_1<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : CompleteSpace X<VAR>x : X<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ϕ : X → ℝ<VAR>cont : Continuous ϕ<VAR>nonneg : ∀ (y : X), 0 ≤ ϕ y<VAR>H : ¬∃ ε' > 0, ∃ x', ε' ≤ ε ∧ d x' x ≤ 2 * ε ∧ ε * ϕ x ≤ ε' * ϕ x' ∧ ∀ (y : X), d x' y ≤ ε' → ϕ y ≤ 2 * ϕ x'<GOAL>False
<VAR>X : Type u_1<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : CompleteSpace X<VAR>x : X<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ϕ : X → ℝ<VAR>cont : Continuous ϕ<VAR>nonneg : ∀ (y : X), 0 ≤ ϕ y<VAR>H : ¬∃ ε' > 0, ∃ x', ε' ≤ ε ∧ d x' x ≤ 2 * ε ∧ ε * ϕ x ≤ ε' * ϕ x' ∧ ∀ (y : X), d x' y ≤ ε' → ϕ y ≤ 2 * ϕ x'<VAR>reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'<GOAL>False
<VAR>X : Type u_1<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : CompleteSpace X<VAR>x : X<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ϕ : X → ℝ<VAR>cont : Continuous ϕ<VAR>nonneg : ∀ (y : X), 0 ≤ ϕ y<VAR>reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'<VAR>H : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → ∃ y, d x' y ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ y<GOAL>False
<VAR>X : Type u_1<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : CompleteSpace X<VAR>x : X<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ϕ : X → ℝ<VAR>cont : Continuous ϕ<VAR>nonneg : ∀ (y : X), 0 ≤ ϕ y<VAR>this : Nonempty X<VAR>F : ℕ → X → X<VAR>u : ℕ → X := fun n => Nat.recOn n x F<VAR>hu : ∀ (n : ℕ), d (u n) x ≤ 2 * ε ∧ 2 ^ n * ϕ x ≤ ϕ (u n) → d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))<VAR>key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))<GOAL>False
<VAR>X : Type u_1<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : CompleteSpace X<VAR>x : X<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ϕ : X → ℝ<VAR>cont : Continuous ϕ<VAR>nonneg : ∀ (y : X), 0 ≤ ϕ y<VAR>this : Nonempty X<VAR>F : ℕ → X → X<VAR>u : ℕ → X := fun n => Nat.recOn n x F<VAR>hu : ∀ (n : ℕ), d (u n) x ≤ 2 * ε ∧ 2 ^ n * ϕ x ≤ ϕ (u n) → d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))<VAR>key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))<VAR>key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / 2 ^ x<VAR>key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))<GOAL>False
<VAR>X : Type u_1<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : CompleteSpace X<VAR>x : X<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ϕ : X → ℝ<VAR>cont : Continuous ϕ<VAR>nonneg : ∀ (y : X), 0 ≤ ϕ y<VAR>this : Nonempty X<VAR>F : ℕ → X → X<VAR>u : ℕ → X := fun n => Nat.recOn n x F<VAR>key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / 2 ^ x<VAR>key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))<GOAL>False
<VAR>X : Type u_1<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : CompleteSpace X<VAR>x : X<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ϕ : X → ℝ<VAR>cont : Continuous ϕ<VAR>nonneg : ∀ (y : X), 0 ≤ ϕ y<VAR>this : Nonempty X<VAR>F : ℕ → X → X<VAR>u : ℕ → X := fun n => Nat.recOn n x F<VAR>key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / 2 ^ x<VAR>key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))<VAR>cauchy_u : CauchySeq u<GOAL>False
<VAR>X : Type u_1<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : CompleteSpace X<VAR>x : X<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ϕ : X → ℝ<VAR>cont : Continuous ϕ<VAR>nonneg : ∀ (y : X), 0 ≤ ϕ y<VAR>this : Nonempty X<VAR>F : ℕ → X → X<VAR>u : ℕ → X := fun n => Nat.recOn n x F<VAR>key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / 2 ^ x<VAR>key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))<VAR>cauchy_u : CauchySeq u<VAR>y : X<VAR>limy : Tendsto u atTop (𝓝 y)<GOAL>False
<VAR>X : Type u_1<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : CompleteSpace X<VAR>x : X<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ϕ : X → ℝ<VAR>cont : Continuous ϕ<VAR>nonneg : ∀ (y : X), 0 ≤ ϕ y<VAR>this : Nonempty X<VAR>F : ℕ → X → X<VAR>u : ℕ → X := fun n => Nat.recOn n x F<VAR>key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / 2 ^ x<VAR>key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))<VAR>cauchy_u : CauchySeq u<VAR>y : X<VAR>limy : Tendsto u atTop (𝓝 y)<VAR>lim_top : Tendsto (ϕ ∘ u) atTop atTop<GOAL>False
<VAR>X : Type u_1<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : CompleteSpace X<VAR>x : X<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ϕ : X → ℝ<VAR>cont : Continuous ϕ<VAR>nonneg : ∀ (y : X), 0 ≤ ϕ y<VAR>this : Nonempty X<VAR>F : ℕ → X → X<VAR>u : ℕ → X := fun n => Nat.recOn n x F<VAR>key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / 2 ^ x<VAR>key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))<VAR>cauchy_u : CauchySeq u<VAR>y : X<VAR>limy : Tendsto u atTop (𝓝 y)<VAR>lim_top : Tendsto (ϕ ∘ u) atTop atTop<VAR>lim : Tendsto (ϕ ∘ u) atTop (𝓝 (ϕ y))<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>m : ℕ<VAR>a : α<GOAL>(replicate (m + 1) a).getLast ⋯ = a
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>m : ℕ<VAR>a : α<GOAL>(replicate m a ++ [a]).getLast ⋯ = a
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>f : M →ₗ[R] N<VAR>p : Submodule R N<VAR>hf : Injective ⇑f<VAR>h : p ≤ LinearMap.range f<VAR>x y : ↥(comap f p)<VAR>hxy : (LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯) x = (LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯) y<GOAL>x = y
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>f : M →ₗ[R] N<VAR>p : Submodule R N<VAR>hf : Injective ⇑f<VAR>h : p ≤ LinearMap.range f<VAR>x✝ : ↥p<VAR>y : M<VAR>hx : f y ∈ p<GOAL>∃ a, (LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯) a = ⟨f y, hx⟩
<VAR>ι : Sort u_1<VAR>f g : ι → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>s : Set ℝ≥0∞<VAR>hf : ∀ r ∈ s, r ≠ ⊤<GOAL>(sInf s).toReal = sInf (ENNReal.toReal '' s)
<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>β : Type u_6<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>hs : IsFundamentalDomain G s μ<VAR>ht : IsFundamentalDomain G t μ<VAR>f : α → β<VAR>hf : ∀ (g : G) (x : α), f (g • x) = f x<GOAL>AEStronglyMeasurable f (μ.restrict s) ↔ AEStronglyMeasurable f (sum fun g => μ.restrict (g • t ∩ s))
<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>β : Type u_6<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>hs : IsFundamentalDomain G s μ<VAR>ht : IsFundamentalDomain G t μ<VAR>f : α → β<VAR>hf : ∀ (g : G) (x : α), f (g • x) = f x<GOAL>AEStronglyMeasurable f (sum fun g => μ.restrict (g • t ∩ s)) ↔ ∀ (g : G), AEStronglyMeasurable f (μ.restrict (g • (g⁻¹ • s ∩ t)))
<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>β : Type u_6<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>hs : IsFundamentalDomain G s μ<VAR>ht : IsFundamentalDomain G t μ<VAR>f : α → β<VAR>hf : ∀ (g : G) (x : α), f (g • x) = f x<GOAL>(∀ (g : G), AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g⁻¹⁻¹ • s ∩ t)))) ↔ ∀ (g : G), AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g • s ∩ t)))
<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>β : Type u_6<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>hs : IsFundamentalDomain G s μ<VAR>ht : IsFundamentalDomain G t μ<VAR>f : α → β<VAR>hf : ∀ (g : G) (x : α), f (g • x) = f x<GOAL>(∀ (g : G), AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g • s ∩ t)))) ↔ ∀ (g : G), AEStronglyMeasurable f (μ.restrict (g • s ∩ t))
<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>β : Type u_6<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>hs : IsFundamentalDomain G s μ<VAR>ht : IsFundamentalDomain G t μ<VAR>f : α → β<VAR>hf : ∀ (g : G) (x : α), f (g • x) = f x<VAR>g : G<GOAL>AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g • s ∩ t))) ↔ AEStronglyMeasurable f (μ.restrict (g • s ∩ t))