ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : 2 < ↑n<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>this✝¹ : NeZero ↑↑n<VAR>E : Type v := AlgebraicClosure L<VAR>z : E<VAR>hz : (cyclotomic (↑n) E).IsRoot z<VAR>this✝ : FiniteDimensional K L := finiteDimensional {n} K L<VAR>this : IsGalois K L := isGalois n K L<VAR>Hprod : ∏ σ : L →ₐ[K] E, (1 - σ ζ) = eval 1 (cyclotomic' (↑n) E)<GOAL>∏ x : L →ₐ[K] E, (1 - x ζ) = (algebraMap K E) ↑(eval 1 (cyclotomic ↑n ℤ))
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : 2 < ↑n<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>this✝² : NeZero ↑↑n<VAR>E : Type v := AlgebraicClosure L<VAR>z : E<VAR>hz : (cyclotomic (↑n) E).IsRoot z<VAR>this✝¹ : FiniteDimensional K L := finiteDimensional {n} K L<VAR>this✝ : IsGalois K L := isGalois n K L<VAR>Hprod : ∏ σ : L →ₐ[K] E, (1 - σ ζ) = eval 1 (cyclotomic' (↑n) E)<VAR>this : NeZero ↑↑n<GOAL>∏ x : L →ₐ[K] E, (1 - x ζ) = (algebraMap K E) ↑(eval 1 (cyclotomic ↑n ℤ))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>x y : S<VAR>d : ℕ<VAR>hd : d ≠ 0<GOAL>y ∈ Submodule.span R (Set.range fun i => x ^ ↑i) ↔ ∃ f, f.natDegree < d ∧ y = (aeval x) f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>x y : S<VAR>d : ℕ<VAR>hd : d ≠ 0<GOAL>(∃ f, f.degree < ↑d ∧ y = (aeval x) f) ↔ ∃ f, f.natDegree < d ∧ y = (aeval x) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>μ : ι → Measure α<VAR>i : ι<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ i) s ≤ (sum μ) s
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a b c : α<VAR>u₁ u₂ : αˣ<GOAL>↑(u₁ / u₂) = ↑u₁ /ₚ u₂
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid G<VAR>a b x y✝ : G<VAR>n m : ℕ<VAR>inst✝ : Monoid β<VAR>y : β<VAR>hx : IsOfFinOrder x<VAR>h : orderOf y ∣ orderOf x<GOAL>IsOfFinOrder y
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid G<VAR>a b x y✝ : G<VAR>n m : ℕ<VAR>inst✝ : Monoid β<VAR>y : β<VAR>hx : 0 < orderOf x<VAR>h : orderOf y ∣ orderOf x<GOAL>0 < orderOf y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>f : X → Set X<VAR>hf : ∀ (x : X), f x ∈ 𝓝 x<GOAL>∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>f : X → Set X<VAR>hf : ∀ (x : X), f x ∈ 𝓝[univ] x<GOAL>∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>f : X → Set X<VAR>hf : ∀ (x : X), f x ∈ 𝓝[univ] x<VAR>s : Set X<VAR>hsc : s.Countable<VAR>hsU : univ ⊆ ⋃ x ∈ s, f x<GOAL>∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ
<VAR>n✝ : ℕ<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : DecidableEq τ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(indiscrete n).parts = {n}
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : (a : Prop) → Decidable a<GOAL>HasSum (fun n => if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - if ↑a = 0 then 1 else 0)
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : (a : Prop) → Decidable a<GOAL>HasSum (fun n => if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - if ∃ n, ↑n = a then 1 else 0)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>y : Q ⊗[R] N<GOAL>(inverse Q hfg hg) ((lTensor Q g) y) = Submodule.Quotient.mk y
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>g : G<VAR>h1 : 1 ∈ T<VAR>hg : g ∈ S<GOAL>↑(hST.equiv g).2 = ↑⟨1, h1⟩
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>o : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>x✝ : m<VAR>m✝ : n →₀ ℕ<GOAL>coeff m✝ (toMvPolynomial 0 x✝) = coeff m✝ (0 x✝)
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<GOAL>n ≤ n.sqrt * n.sqrt + n.sqrt + n.sqrt
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<GOAL>n ≤ n.sqrt.succ * n.sqrt + n.sqrt
<VAR>α : Type u<VAR>c d : Cardinal.{u}<GOAL>toNat c = 0 ↔ c = 0 ∨ ℵ₀ ≤ c
<VAR>α : Type u<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Inhabited α<VAR>β : Type v<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Inhabited β<VAR>γ : Type w<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Inhabited γ<VAR>p : α → Prop<VAR>q : β → Prop<GOAL>of p = of q ↔ ManyOneEquiv p q
<VAR>α : Type u<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Inhabited α<VAR>β : Type v<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Inhabited β<VAR>γ : Type w<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Inhabited γ<VAR>p : α → Prop<VAR>q : β → Prop<GOAL>Setoid.r (toNat p) (toNat q) ↔ ManyOneEquiv p q
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>g : G<GOAL>s ∈ fixedBy (Set α) g ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
<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✝ : LocallyFiniteOrder α<VAR>a b c d : α<GOAL>↑(Ico a b * Icc c d) ⊆ ↑(Ico (a * c) (b * d))
<VAR>X✝ X : LocallyRingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>n : ℕ<VAR>hn : f ^ n = 0<GOAL>X.toRingedSpace.basicOpen f = ⊥
<VAR>α : Type u_1<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a b : ℝ≥0∞<VAR>h : a = ⊤ → b = ⊤<VAR>h_nnreal : a ≠ ⊤ → b ≠ ⊤ → a.toNNReal ≤ b.toNNReal<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a b : ℝ≥0∞<VAR>h : a = ⊤ → b = ⊤<VAR>h_nnreal : a ≠ ⊤ → b ≠ ⊤ → a.toNNReal ≤ b.toNNReal<VAR>hlt : b < a<GOAL>False
<VAR>α : Type u_1<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a : ℝ≥0∞<VAR>b : ℝ≥0<VAR>h : a = ⊤ → ↑b = ⊤<VAR>h_nnreal : a ≠ ⊤ → ↑b ≠ ⊤ → a.toNNReal ≤ (↑b).toNNReal<VAR>hlt : ↑b < a<GOAL>False
<VAR>α : Type u_1<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q b a : ℝ≥0<VAR>h : ↑a = ⊤ → ↑b = ⊤<VAR>h_nnreal : ↑a ≠ ⊤ → ↑b ≠ ⊤ → (↑a).toNNReal ≤ (↑b).toNNReal<VAR>hlt : ↑b < ↑a<GOAL>False
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁹ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>E : Type u_9<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : Module R E<VAR>F : Type u_10<VAR>inst✝⁴ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>inst✝³ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝² : (i : ι) → Module R (t i)<VAR>inst✝¹ : (i : ι) → AddCommMonoid (t' i)<VAR>inst✝ : (i : ι) → Module R (t' i)<VAR>g : (i : ι) → t i →ₗ[R] t' i<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>x✝ : (i : ι) → s i<GOAL>((map fun i => g i ∘ₗ f i).compMultilinearMap (tprod R)) x✝ = ((map g ∘ₗ map f).compMultilinearMap (tprod R)) x✝
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] => P<VAR>hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>R S : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set S<VAR>hs : Ideal.span s = ⊤<VAR>hT✝ : ∀ (r : ↑s), ∃ T x x_1, ∃ (_ : IsLocalization.Away (↑r) T), P ((algebraMap S T).comp f)<VAR>r : ↑s<VAR>T : Type u<VAR>w✝² : CommRing T<VAR>w✝¹ : Algebra S T<VAR>w✝ : IsLocalization.Away (↑r) T<VAR>hT : P ((algebraMap S T).comp f)<GOAL>P ((algebraMap S (Localization.Away ↑r)).comp f)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] => P<VAR>hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>R S : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set S<VAR>hs : Ideal.span s = ⊤<VAR>hT✝ : ∀ (r : ↑s), ∃ T x x_1, ∃ (_ : IsLocalization.Away (↑r) T), P ((algebraMap S T).comp f)<VAR>r : ↑s<VAR>T : Type u<VAR>w✝² : CommRing T<VAR>w✝¹ : Algebra S T<VAR>w✝ : IsLocalization.Away (↑r) T<VAR>hT : P ((algebraMap S T).comp f)<GOAL>(algebraMap S (Localization.Away ↑r)).comp f = (Localization.algEquiv (Submonoid.powers ↑r) T).symm.toRingEquiv.toRingHom.comp ((algebraMap S T).comp f)
<VAR>M : Type u<VAR>inst✝² : Monoid M<VAR>α : Type v<VAR>inst✝¹ : MulAction M α<VAR>β : Type u_1<VAR>inst✝ : MulAction M β<VAR>a : α<GOAL>(fun m => m • a) 1 = a
<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>h : l.HasBasis p s<GOAL>l = generate {U | ∃ i, p i ∧ s i = U}
<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]<VAR>hp : p ≠ 0<VAR>s : Multiset R<GOAL>(Multiset.map (fun a => X - C a) s).prod ∣ p ↔ s ≤ p.roots
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>h : p₁ ≠ p₂<GOAL>∡ p₁ s.center p₂ = ↑π - 2 • ∡ p₂ p₁ s.center
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : ι → Matroid α<VAR>h : ∀ (i : ι), (M i).Finitary<GOAL>(Matroid.sum' M).Finitary
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : ι → Matroid α<VAR>h : ∀ (i : ι), (M i).Finitary<VAR>this : (Matroid.sigma M).Finitary<GOAL>(Matroid.sum' M).Finitary
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>γ : α → Type u_2<VAR>δ : α → Type u_3<VAR>s : (a : α) → Finset (γ a)<VAR>t : (a : α) → Finset (δ a)<VAR>x : (a : α) → δ a<GOAL>x ∈ ↑(piFinset t) ↔ x ∈ Set.univ.pi fun a => ↑(t a)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>γ : α → Type u_2<VAR>δ : α → Type u_3<VAR>s : (a : α) → Finset (γ a)<VAR>t : (a : α) → Finset (δ a)<VAR>x : (a : α) → δ a<GOAL>x ∈ ↑(piFinset t) ↔ ∀ (i : α), x i ∈ ↑(t i)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : AddCommMonoid G<VAR>inst✝ : AddCommMonoid H<VAR>A B : Set (G × G)<VAR>s : Set G<VAR>t : Set H<VAR>f : G → H<VAR>a b c x₁ y₁ x₂ y₂ : G<VAR>hf : IsAddFreimanIso 2 s t f<VAR>hAs : A ⊆ s ×ˢ s<VAR>hx₁ : x₁ ∈ s<VAR>hy₁ : y₁ ∈ s<VAR>hx₂ : x₂ ∈ s<VAR>hy₂ : y₂ ∈ s<GOAL>IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂) ↔ IsCorner A x₁ y₁ x₂ y₂
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : AddCommMonoid G<VAR>inst✝ : AddCommMonoid H<VAR>A B : Set (G × G)<VAR>s : Set G<VAR>t : Set H<VAR>f : G → H<VAR>a b c x₁ y₁ x₂ y₂ : G<VAR>hf : IsAddFreimanIso 2 s t f<VAR>hAs : A ⊆ s ×ˢ s<VAR>hx₁ : x₁ ∈ s<VAR>hy₁ : y₁ ∈ s<VAR>hx₂ : x₂ ∈ s<VAR>hy₂ : y₂ ∈ s<VAR>hf' : InjOn (fun x => (f x.1, f x.2)) (s ×ˢ s)<GOAL>IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂) ↔ IsCorner A x₁ y₁ x₂ y₂
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : AddCommMonoid G<VAR>inst✝ : AddCommMonoid H<VAR>A B : Set (G × G)<VAR>s : Set G<VAR>t : Set H<VAR>f : G → H<VAR>a b c x₁ y₁ x₂ y₂ : G<VAR>hf : IsAddFreimanIso 2 s t f<VAR>hAs : A ⊆ s ×ˢ s<VAR>hx₁ : x₁ ∈ s<VAR>hy₁ : y₁ ∈ s<VAR>hx₂ : x₂ ∈ s<VAR>hy₂ : y₂ ∈ s<VAR>hf' : InjOn (fun x => (f x.1, f x.2)) (s ×ˢ s)<GOAL>(f x₁, f y₁) ∈ Prod.map f f '' A ∧ (f x₁, f y₂) ∈ Prod.map f f '' A ∧ (f x₂, f y₁) ∈ Prod.map f f '' A ∧ f x₁ + f y₂ = f x₂ + f y₁ ↔ (x₁, y₁) ∈ A ∧ (x₁, y₂) ∈ A ∧ (x₂, y₁) ∈ A ∧ x₁ + y₂ = x₂ + y₁
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>a✝ : α<VAR>ha : IsWellOrderLimitElement a✝<VAR>inst✝¹ : IsWellOrder α fun x x_1 => x < x_1<VAR>inst✝ : OrderBot α<VAR>a : α<GOAL>a = ⊥ ∨ (∃ b, a = wellOrderSucc b ∧ b < a) ∨ IsWellOrderLimitElement a
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>a✝ : α<VAR>ha : IsWellOrderLimitElement a✝<VAR>inst✝¹ : IsWellOrder α fun x x_1 => x < x_1<VAR>inst✝ : OrderBot α<VAR>a : α<VAR>h₁ : ¬a = ⊥<VAR>h₂ : ¬∃ b, a = wellOrderSucc b ∧ b < a<GOAL>IsWellOrderLimitElement a
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>a✝ : α<VAR>ha : IsWellOrderLimitElement a✝<VAR>inst✝¹ : IsWellOrder α fun x x_1 => x < x_1<VAR>inst✝ : OrderBot α<VAR>a : α<VAR>h₁ : ¬a = ⊥<VAR>h₂ : ¬∃ b, a = wellOrderSucc b ∧ b < a<VAR>b : α<VAR>hb : b < a<GOAL>∃ c, b < c ∧ c < a
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>a : α<VAR>ha : IsWellOrderLimitElement a<VAR>inst✝¹ : IsWellOrder α fun x x_1 => x < x_1<VAR>inst✝ : OrderBot α<VAR>b : α<VAR>h₁ : ¬wellOrderSucc b = ⊥<VAR>h₂ : ¬∃ b_1, wellOrderSucc b = wellOrderSucc b_1 ∧ b_1 < wellOrderSucc b<VAR>hb : b < wellOrderSucc b<GOAL>∃ c, b < c ∧ c < wellOrderSucc b
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>a✝ : α<VAR>ha : IsWellOrderLimitElement a✝<VAR>inst✝¹ : IsWellOrder α fun x x_1 => x < x_1<VAR>inst✝ : OrderBot α<VAR>a : α<VAR>h₁ : ¬a = ⊥<VAR>h₂ : ¬∃ b, a = wellOrderSucc b ∧ b < a<VAR>b : α<VAR>hb : b < a<VAR>h₃ : wellOrderSucc b < a<GOAL>∃ c, b < c ∧ c < a
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝¹⁰ : Category.{?u.100947, u_1} C<VAR>inst✝⁹ : Category.{?u.100951, u_2} D<VAR>inst✝⁸ : Category.{?u.100955, u_3} E<VAR>inst✝⁷ : Category.{?u.100959, u_4} E'<VAR>A : Type u_5<VAR>inst✝⁶ : AddMonoid A<VAR>inst✝⁵ : HasShift D A<VAR>inst✝⁴ : HasShift E A<VAR>inst✝³ : HasShift E' A<VAR>F G✝ H : SingleFunctors C D A<VAR>G G' : D ⥤ E<VAR>e : G ≅ G'<VAR>inst✝² : G.CommShift A<VAR>inst✝¹ : G'.CommShift A<VAR>inst✝ : NatTrans.CommShift e.hom A<VAR>n a a' : A<VAR>ha' : n + a = a'<VAR>X : C<GOAL>((F.postcomp G).shiftIso n a a' ha').hom.app X ≫ e.hom.app ((F.functor a).obj X) = (shiftFunctor E n).map (e.hom.app ((F.functor a').obj X)) ≫ ((F.postcomp G').shiftIso n a a' ha').hom.app X
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f✝ g✝ : Ultrafilter α<VAR>s t : Set α<VAR>p q : α → Prop<VAR>f : Ultrafilter α<VAR>g : Filter α<GOAL>Disjoint (↑f) g ↔ ¬↑f ≤ g
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ g, ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Integrable (⇑g) μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>f : α → E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hf : Memℒp f (ENNReal.ofReal 1) μ<GOAL>∃ g, ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Memℒp (⇑g) (ENNReal.ofReal 1) μ
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>l : List (Perm α)<VAR>x : α<VAR>hx : x ∈ l.prod.support<GOAL>∃ f ∈ l, x ∈ f.support
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>l : List (Perm α)<VAR>x : α<VAR>hx : ∀ f ∈ l, x ∉ f.support<GOAL>x ∉ l.prod.support
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>l : List (Perm α)<VAR>x : α<VAR>hx : ∀ f ∈ l, f x = x<GOAL>l.prod x = x
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>x : ↑S.X₁<GOAL>S.moduleCatHomologyπ (((ModuleCat.kernelIsLimit S.g).lift (KernelFork.ofι S.f ⋯)) x) = 0 x
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>x : ↑S.X₁<GOAL>((ModuleCat.kernelIsLimit S.g).lift (KernelFork.ofι S.f ⋯)) x ∈ LinearMap.range S.moduleCatToCycles
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>x : ↑S.X₁<GOAL>∃ y, S.moduleCatToCycles y = ((ModuleCat.kernelIsLimit S.g).lift (KernelFork.ofι S.f ⋯)) x
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>x✝ : IsUnit 0<VAR>a : M₀<VAR>a0 : 0 * a = 1<VAR>inv_val✝ : a * 0 = 1<GOAL>0 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>h : IntegrableAtFilter f l μ<VAR>h' : ∀ s ∈ l, μ s = ⊤<VAR>a : E<VAR>hf : Tendsto f l (𝓝 a)<GOAL>a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>h : IntegrableAtFilter f l μ<VAR>h' : ∀ s ∈ l, μ s = ⊤<VAR>a : E<VAR>hf : Tendsto f l (𝓝 a)<VAR>H : ¬a = 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>h : IntegrableAtFilter f l μ<VAR>h' : ∀ s ∈ l, μ s = ⊤<VAR>a : E<VAR>hf : Tendsto f l (𝓝 a)<VAR>H : ¬a = 0<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : ε < ‖a‖<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>h' : ∀ s ∈ l, μ s = ⊤<VAR>a : E<VAR>hf : Tendsto f l (𝓝 a)<VAR>H : ¬a = 0<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : ε < ‖a‖<VAR>u : Set α<VAR>ul : u ∈ l<VAR>hu : IntegrableOn f u μ<VAR>v : Set α := u ∩ {b | ε < ‖f b‖}<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>h' : ∀ s ∈ l, μ s = ⊤<VAR>a : E<VAR>hf : Tendsto f l (𝓝 a)<VAR>H : ¬a = 0<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : ε < ‖a‖<VAR>u : Set α<VAR>ul : u ∈ l<VAR>hu : IntegrableOn f u μ<VAR>v : Set α := u ∩ {b | ε < ‖f b‖}<VAR>hv : IntegrableOn f v μ<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>h' : ∀ s ∈ l, μ s = ⊤<VAR>a : E<VAR>hf : Tendsto f l (𝓝 a)<VAR>H : ¬a = 0<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : ε < ‖a‖<VAR>u : Set α<VAR>ul : u ∈ l<VAR>hu : IntegrableOn f u μ<VAR>v : Set α := u ∩ {b | ε < ‖f b‖}<VAR>hv : IntegrableOn f v μ<VAR>vl : v ∈ l<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>h' : ∀ s ∈ l, μ s = ⊤<VAR>a : E<VAR>hf : Tendsto f l (𝓝 a)<VAR>H : ¬a = 0<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : ε < ‖a‖<VAR>u : Set α<VAR>ul : u ∈ l<VAR>hu : IntegrableOn f u μ<VAR>v : Set α := u ∩ {b | ε < ‖f b‖}<VAR>hv : IntegrableOn f v μ<VAR>vl : v ∈ l<VAR>this : (μ.restrict v) v < ⊤<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>h' : ∀ s ∈ l, μ s = ⊤<VAR>a : E<VAR>hf : Tendsto f l (𝓝 a)<VAR>H : ¬a = 0<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : ε < ‖a‖<VAR>u : Set α<VAR>ul : u ∈ l<VAR>hu : IntegrableOn f u μ<VAR>v : Set α := u ∩ {b | ε < ‖f b‖}<VAR>hv : IntegrableOn f v μ<VAR>vl : v ∈ l<VAR>this✝ : (μ.restrict v) v < ⊤<VAR>this : μ v ≠ ⊤<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I J : Ideal R<GOAL>↑(I * J) = ↑I * ↑J
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I J : Ideal R<GOAL>↑(I * J) = ⟨↑↑I * ↑↑J, ⋯⟩
<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 : α → E<VAR>hf : ∀ (g : G) (x : α), f (g • x) = f x<GOAL>∫⁻ (a : α) in s, ↑‖f a‖₊ ∂μ < ⊤ ↔ ∫⁻ (a : α) in t, ↑‖f a‖₊ ∂μ < ⊤
<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 : α → E<VAR>hf : ∀ (g : G) (x : α), f (g • x) = f x<GOAL>∀ (g : G) (x : α), ↑‖f (g • x)‖₊ = ↑‖f x‖₊
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s✝ t s : Set E<GOAL>Bornology.IsBounded ((convexHull ℝ) s) ↔ Bornology.IsBounded s
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}<GOAL>∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)