ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : AddCommMonoid L<VAR>inst✝⁷ : TopologicalSpace L<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : TopologicalSpace N<VAR>v v₁ v₂ : VectorMeasure α M<VAR>w w₁ w₂ : VectorMeasure α N<VAR>R : Type u_6<VAR>inst✝² : Semiring R<VAR>inst✝¹ : DistribMulAction R N<VAR>inst✝ : ContinuousConstSMul R N<VAR>r : R<VAR>h : v ⟂ᵥ w<VAR>s : Set α<VAR>hmeas : MeasurableSet s<VAR>hs₁ : ∀ t ⊆ s, ↑v t = 0<VAR>hs₂ : ∀ t ⊆ sᶜ, ↑w t = 0<VAR>t : Set α<VAR>ht : t ⊆ sᶜ<GOAL>↑(r • w) t = 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F G F₁ F₂ : C ⥤ Type w<VAR>τ₁ : F₁ ⟶ F<VAR>τ₂ : F₂ ⟶ F<VAR>x✝² x✝¹ : C<VAR>x✝ : x✝² ⟶ x✝¹<VAR>x : (coprod F₁ F₂).obj x✝²<GOAL>((coprod F₁ F₂).map x✝ ≫ (fun a x => Sum.casesOn (motive := fun t => x = t → F.obj a) x (fun x_1 h => τ₁.app a x_1) (fun x_1 h => τ₂.app a x_1) ⋯) x✝¹) x = ((fun a x => Sum.casesOn (motive := fun t => x = t → F.obj a) x (fun x_1 h => τ₁.app a x_1) (fun x_1 h => τ₂.app a x_1) ⋯) x✝² ≫ F.map x✝) x
<VAR>α : Type u<VAR>a✝ : α<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : IsCyclic H<VAR>f : G →* H<VAR>hf : f.ker ≤ center G<VAR>a b : G<VAR>x : H<VAR>y : G<VAR>hxy : f y = x<VAR>hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩<VAR>m : ℤ<VAR>hm : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩<VAR>n : ℤ<VAR>hn : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩<GOAL>x ^ m = f a
<VAR>α : Type u<VAR>a✝ : α<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : IsCyclic H<VAR>f : G →* H<VAR>hf : f.ker ≤ center G<VAR>a b : G<VAR>x : H<VAR>y : G<VAR>hxy : f y = x<VAR>hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩<VAR>m : ℤ<VAR>hm✝ : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩<VAR>n : ℤ<VAR>hn : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩<VAR>hm : x ^ m = f a<GOAL>x ^ n = f b
<VAR>α : Type u<VAR>a✝ : α<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : IsCyclic H<VAR>f : G →* H<VAR>hf : f.ker ≤ center G<VAR>a b : G<VAR>x : H<VAR>y : G<VAR>hxy : f y = x<VAR>hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩<VAR>m : ℤ<VAR>hm✝ : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩<VAR>n : ℤ<VAR>hn✝ : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩<VAR>hm : x ^ m = f a<VAR>hn : x ^ n = f b<GOAL>y ^ (-m) * a ∈ f.ker
<VAR>α : Type u<VAR>a✝ : α<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : IsCyclic H<VAR>f : G →* H<VAR>hf : f.ker ≤ center G<VAR>a b : G<VAR>x : H<VAR>y : G<VAR>hxy : f y = x<VAR>hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩<VAR>m : ℤ<VAR>hm✝ : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩<VAR>n : ℤ<VAR>hn✝ : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩<VAR>hm : x ^ m = f a<VAR>hn : x ^ n = f b<VAR>ha : y ^ (-m) * a ∈ center G<GOAL>y ^ (-n) * b ∈ f.ker
<VAR>α : Type u<VAR>a✝ : α<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : IsCyclic H<VAR>f : G →* H<VAR>hf : f.ker ≤ center G<VAR>a b : G<VAR>x : H<VAR>y : G<VAR>hxy : f y = x<VAR>hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩<VAR>m : ℤ<VAR>hm✝ : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩<VAR>n : ℤ<VAR>hn✝ : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩<VAR>hm : x ^ m = f a<VAR>hn : x ^ n = f b<VAR>ha : y ^ (-m) * a ∈ center G<VAR>hb : y ^ (-n) * b ∈ center G<GOAL>a * b = y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b)
<VAR>α : Type u<VAR>a✝ : α<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : IsCyclic H<VAR>f : G →* H<VAR>hf : f.ker ≤ center G<VAR>a b : G<VAR>x : H<VAR>y : G<VAR>hxy : f y = x<VAR>hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩<VAR>m : ℤ<VAR>hm✝ : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩<VAR>n : ℤ<VAR>hn✝ : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩<VAR>hm : x ^ m = f a<VAR>hn : x ^ n = f b<VAR>ha : y ^ (-m) * a ∈ center G<VAR>hb : y ^ (-n) * b ∈ center G<GOAL>y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b) = y ^ m * (y ^ n * (y ^ (-m) * a)) * (y ^ (-n) * b)
<VAR>α : Type u<VAR>a✝ : α<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : IsCyclic H<VAR>f : G →* H<VAR>hf : f.ker ≤ center G<VAR>a b : G<VAR>x : H<VAR>y : G<VAR>hxy : f y = x<VAR>hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩<VAR>m : ℤ<VAR>hm✝ : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩<VAR>n : ℤ<VAR>hn✝ : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩<VAR>hm : x ^ m = f a<VAR>hn : x ^ n = f b<VAR>ha : y ^ (-m) * a ∈ center G<VAR>hb : y ^ (-n) * b ∈ center G<GOAL>y ^ m * (y ^ n * (y ^ (-m) * a)) * (y ^ (-n) * b) = y ^ m * y ^ n * y ^ (-m) * (a * (y ^ (-n) * b))
<VAR>α : Type u<VAR>a✝ : α<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : IsCyclic H<VAR>f : G →* H<VAR>hf : f.ker ≤ center G<VAR>a b : G<VAR>x : H<VAR>y : G<VAR>hxy : f y = x<VAR>hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩<VAR>m : ℤ<VAR>hm✝ : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩<VAR>n : ℤ<VAR>hn✝ : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩<VAR>hm : x ^ m = f a<VAR>hn : x ^ n = f b<VAR>ha : y ^ (-m) * a ∈ center G<VAR>hb : y ^ (-n) * b ∈ center G<GOAL>y ^ m * y ^ n * y ^ (-m) * (a * (y ^ (-n) * b)) = y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a)
<VAR>α : Type u<VAR>a✝ : α<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : IsCyclic H<VAR>f : G →* H<VAR>hf : f.ker ≤ center G<VAR>a b : G<VAR>x : H<VAR>y : G<VAR>hxy : f y = x<VAR>hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩<VAR>m : ℤ<VAR>hm✝ : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩<VAR>n : ℤ<VAR>hn✝ : (fun x_1 => ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩<VAR>hm : x ^ m = f a<VAR>hn : x ^ n = f b<VAR>ha : y ^ (-m) * a ∈ center G<VAR>hb : y ^ (-n) * b ∈ center G<GOAL>y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a) = b * a
<VAR>a n✝ : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>hs : (map (fun i => 2 ^ i) n.bitIndices).sum = n<GOAL>(map (fun i => 2 ^ i) (bit b n).bitIndices).sum = bit b n
<VAR>a n✝ : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>hs : (map (fun i => 2 ^ i) n.bitIndices).sum = n<VAR>hrw : ((fun i => 2 ^ i) ∘ fun x => x + 1) = fun i => 2 * 2 ^ i<GOAL>(map (fun i => 2 ^ i) (bit b n).bitIndices).sum = bit b n
<VAR>a n✝ n : ℕ<VAR>hs : (map (fun i => 2 ^ i) n.bitIndices).sum = n<VAR>hrw : ((fun i => 2 ^ i) ∘ fun x => x + 1) = fun i => 2 * 2 ^ i<GOAL>(map (fun i => 2 ^ i) (bit true n).bitIndices).sum = bit true n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NonUnitalRing α<VAR>a b c : α<VAR>h₁ : a ∣ b<VAR>h₂ : a ∣ c<GOAL>a ∣ b - c
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>i : ℕ<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>x : S<GOAL>quotientToQuotientRangePowQuotSuccAux f p P a_mem (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨(Quotient.mk (P ^ e)) (a * x), ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t✝ : Set α<VAR>t : Set (Set α)<VAR>h : t.PairwiseDisjoint id<VAR>ht₀ : t.Finite<VAR>ht₁ : ∀ x ∈ t, x.Finite<GOAL>∏ᶠ (a : α) (_ : a ∈ ⋃₀ t), f a = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t✝ : Set α<VAR>t : Set (Set α)<VAR>h : t.PairwiseDisjoint id<VAR>ht₀ : t.Finite<VAR>ht₁ : ∀ x ∈ t, x.Finite<GOAL>∏ᶠ (a : α) (_ : a ∈ ⋃ i ∈ t, i), f a = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a
<VAR>m n : ℕ+<GOAL>m ∣ n → m.gcd n = m
<VAR>m n : ℕ+<GOAL>↑m ∣ ↑n → m.gcd n = m
<VAR>m n : ℕ+<VAR>h : ↑m ∣ ↑n<GOAL>m.gcd n = m
<VAR>m n : ℕ+<VAR>h : ↑m ∣ ↑n<GOAL>↑(m.gcd n) = ↑m
<VAR>m n : ℕ+<VAR>h : ↑m ∣ ↑n<GOAL>(↑m).gcd ↑n = ↑m
<VAR>k : ℕ<GOAL>bernoulliFun k 1 = bernoulliFun k 0 + if k = 1 then 1 else 0
<VAR>k : ℕ<GOAL>(algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + if k = 1 then 1 else 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>h : nilpotencyLength R L M ≤ 1<VAR>a✝ : Nontrivial M<GOAL>IsTrivial L M
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>h✝ : nilpotencyLength R L M ≤ 1<VAR>a✝ : Nontrivial M<VAR>h : nilpotencyLength R L M = 0<GOAL>IsTrivial L M
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>h✝ : nilpotencyLength R L M ≤ 1<VAR>a✝ : Nontrivial M<VAR>h : nilpotencyLength R L M = 1<GOAL>IsTrivial L M
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑(Proj.restrict ⋯).toTopCat<VAR>z : HomogeneousLocalization 𝒜 (Submonoid.powers f)<GOAL>¬IsUnit ((mapId 𝒜 ⋯) z) ↔ z ∈ ProjIsoSpecTopComponent.ToSpec.carrier x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑(Proj.restrict ⋯).toTopCat<VAR>z : NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>¬IsUnit ((mapId 𝒜 ⋯) (HomogeneousLocalization.mk z)) ↔ HomogeneousLocalization.mk z ∈ ProjIsoSpecTopComponent.ToSpec.carrier x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑(Proj.restrict ⋯).toTopCat<VAR>z : NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>↑{ deg := z.deg, num := ⟨(RingHom.id A) ↑z.num, ⋯⟩, den := ⟨(RingHom.id A) ↑z.den, ⋯⟩, den_mem := ⋯ }.num ∉ (↑x).asHomogeneousIdeal.toIdeal.primeCompl ↔ ↑z.num ∈ (↑x).asHomogeneousIdeal
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t : Set E<VAR>ι' : Type u_4<VAR>f : ι' ↪ ι<VAR>p : ι → E<VAR>hc : ConvexIndependent 𝕜 p<VAR>s : Set ι'<VAR>x : ι'<VAR>hx : (p ∘ ⇑f) x ∈ (convexHull 𝕜) (p ∘ ⇑f '' s)<GOAL>x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t : Set E<VAR>ι' : Type u_4<VAR>f : ι' ↪ ι<VAR>p : ι → E<VAR>hc : ConvexIndependent 𝕜 p<VAR>s : Set ι'<VAR>x : ι'<VAR>hx : (p ∘ ⇑f) x ∈ (convexHull 𝕜) (p ∘ ⇑f '' s)<GOAL>f x ∈ ⇑f '' s
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Nonempty V<GOAL>∃ v, G.minDegree = G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Nonempty V<VAR>t : ℕ<VAR>ht : (image (fun v => G.degree v) univ).min = ↑t<GOAL>∃ v, G.minDegree = G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Nonempty V<VAR>v : V<VAR>left✝ : v ∈ univ<VAR>ht : (image (fun v => G.degree v) univ).min = ↑(G.degree v)<GOAL>∃ v, G.minDegree = G.degree v
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>g : G<GOAL>IsComplement S {g} ↔ S = univ
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>g : G<VAR>h : IsComplement S {g}<VAR>x : G<VAR>x✝ : x ∈ ⊤<GOAL>x ∈ S
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>g : G<VAR>h : IsComplement S {g}<VAR>x : G<VAR>x✝ : x ∈ ⊤<VAR>y : ↑S × ↑{g}<VAR>hy : (fun x => ↑x.1 * ↑x.2) y = x * g<GOAL>x ∈ S
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>g : G<VAR>h : IsComplement S {g}<VAR>x : G<VAR>x✝ : x ∈ ⊤<VAR>y : ↑S × ↑{g}<VAR>hy : (fun x => ↑x.1 * ↑x.2) y = x * ↑y.2<GOAL>x ∈ S
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>g : G<VAR>h : IsComplement S {g}<VAR>x : G<VAR>x✝ : x ∈ ⊤<VAR>y : ↑S × ↑{g}<VAR>hy : (fun x => ↑x.1 * ↑x.2) y = x * ↑y.2<GOAL>↑y.1 ∈ S
<VAR>R M : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>I : Ideal R<VAR>F F'✝ : I.Filtration M<VAR>h : F.Stable<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R M<VAR>hF : F.Stable<VAR>F' : I.Filtration M<VAR>hf : F' ≤ F<GOAL>F'.Stable
<VAR>R M : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>I : Ideal R<VAR>F F'✝ : I.Filtration M<VAR>h : F.Stable<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R M<VAR>hF : F.submodule.FG<VAR>F' : I.Filtration M<VAR>hf : F' ≤ F<GOAL>F'.submodule.FG
<VAR>R M : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>I : Ideal R<VAR>F F'✝ : I.Filtration M<VAR>h : F.Stable<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R M<VAR>hF : F.submodule.FG<VAR>F' : I.Filtration M<VAR>hf : F' ≤ F<GOAL>∀ (i : ℕ), (F'.N i).FG
<VAR>R M : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>I : Ideal R<VAR>F F'✝ : I.Filtration M<VAR>h : F.Stable<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R M<VAR>hF : F.Stable<VAR>F' : I.Filtration M<VAR>hf : F' ≤ F<GOAL>∀ (i : ℕ), (F.N i).FG
<VAR>R M : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>I : Ideal R<VAR>F F'✝ : I.Filtration M<VAR>h : F.Stable<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R M<VAR>hF : F.submodule.FG<VAR>F' : I.Filtration M<VAR>hf : F' ≤ F<VAR>this : IsNoetherian ↥(reesAlgebra I) ↥F.submodule<GOAL>F'.submodule.FG
<VAR>R M : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>I : Ideal R<VAR>F F'✝ : I.Filtration M<VAR>h : F.Stable<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R M<VAR>hF : F.submodule.FG<VAR>F' : I.Filtration M<VAR>hf : F' ≤ F<VAR>this : ∀ s ≤ F.submodule, s.FG<GOAL>F'.submodule.FG
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<GOAL>0 ≤ᶠ[ae μ] f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<GOAL>∀ᵐ (x : α) ∂μ, 0 ≤ f x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<GOAL>∀ b < 0, μ {x | f x ≤ b} = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<VAR>b : ℝ<VAR>hb_neg : b < 0<VAR>s : Set α := {x | f x ≤ b}<GOAL>μ {x | f x ≤ b} = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<VAR>b : ℝ<VAR>hb_neg : b < 0<VAR>s : Set α := {x | f x ≤ b}<VAR>hs : NullMeasurableSet s μ<GOAL>μ {x | f x ≤ b} = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<VAR>b : ℝ<VAR>hb_neg : b < 0<VAR>s : Set α := {x | f x ≤ b}<VAR>hs : NullMeasurableSet s μ<VAR>mus : μ s < ⊤<GOAL>μ {x | f x ≤ b} = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<VAR>b : ℝ<VAR>hb_neg : b < 0<VAR>s : Set α := {x | f x ≤ b}<VAR>hs : NullMeasurableSet s μ<VAR>mus : μ s < ⊤<VAR>h_int_gt : ∫ (x : α) in s, f x ∂μ ≤ b * (μ s).toReal<GOAL>μ {x | f x ≤ b} = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<VAR>b : ℝ<VAR>hb_neg : b < 0<VAR>s : Set α := {x | f x ≤ b}<VAR>hs : NullMeasurableSet s μ<VAR>mus : μ s < ⊤<VAR>H : μ {x | f x ≤ b} ≠ 0<GOAL>b * (μ s).toReal < ∫ (x : α) in s, f x ∂μ
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁶ : Category.{?u.82244, u_1} C₁<VAR>inst✝⁵ : Category.{?u.82248, u_2} C₂<VAR>inst✝⁴ : Category.{?u.82252, u_3} C₃<VAR>inst✝³ : Category.{?u.82256, u_4} C₄<VAR>inst✝² : Category.{?u.82260, u_5} C₁₂<VAR>inst✝¹ : Category.{?u.82264, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>inst✝ : ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>X₁ Y₁ : GradedObject I₁ C₁<VAR>φ✝ : X₁ ⟶ Y₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ Y₃ : GradedObject I₃ C₃<VAR>φ : X₃ ⟶ Y₃<VAR>j : J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>h : p (i₁, i₂, i₃) = j<GOAL>ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ j ≫ mapTrifunctorMapMap F p φ✝ (𝟙 X₂) (𝟙 Y₃) j = ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ mapTrifunctorMapMap F p φ✝ (𝟙 X₂) (𝟙 X₃) j ≫ mapTrifunctorMapMap F p (𝟙 Y₁) (𝟙 X₂) φ j
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁶ : Category.{?u.82244, u_1} C₁<VAR>inst✝⁵ : Category.{?u.82248, u_2} C₂<VAR>inst✝⁴ : Category.{?u.82252, u_3} C₃<VAR>inst✝³ : Category.{?u.82256, u_4} C₄<VAR>inst✝² : Category.{?u.82260, u_5} C₁₂<VAR>inst✝¹ : Category.{?u.82264, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>inst✝ : ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>X₁ Y₁ : GradedObject I₁ C₁<VAR>φ : X₁ ⟶ Y₁<VAR>X₂ Y₂ : GradedObject I₂ C₂<VAR>ψ : X₂ ⟶ Y₂<VAR>X₃ : GradedObject I₃ C₃<VAR>j : J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>h : p (i₁, i₂, i₃) = j<GOAL>ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ mapTrifunctorMapMap F p (𝟙 X₁) ψ (𝟙 X₃) j ≫ mapTrifunctorMapMap F p φ (𝟙 Y₂) (𝟙 X₃) j = ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ mapTrifunctorMapMap F p φ (𝟙 X₂) (𝟙 X₃) j ≫ mapTrifunctorMapMap F p (𝟙 Y₁) ψ (𝟙 X₃) j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : Countable β<VAR>x : β<VAR>s : β → Set β<VAR>hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y<VAR>this : measurableAtom x = ⋂ y ∈ (measurableAtom x)ᶜ, s y<GOAL>MeasurableSet (⋂ y ∈ (measurableAtom x)ᶜ, s y)
<VAR>G : Type u<VAR>inst✝ : Monoid G<GOAL>exponent G = 0 ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1
<VAR>G : Type u<VAR>inst✝ : Monoid G<GOAL>(¬∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1) ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1
<VAR>G : Type u<VAR>inst✝ : Monoid G<GOAL>(∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1) ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ : C ⥤ D<VAR>R₁ R₂ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>L R : C ⥤ C<VAR>adj : L ⊣ R<VAR>α : R ⟶ 𝟭 C<VAR>c : C<GOAL>𝟙 c ≫ (adj.unit.app c ≫ (𝟙 (R.obj (L.obj c)) ≫ α.app (L.obj c) ≫ 𝟙 (L.obj c)) ≫ 𝟙 (L.obj c)) ≫ 𝟙 (L.obj c) = adj.unit.app c ≫ α.app (L.obj c)
<VAR>α : Type u_1<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ a b : α<GOAL>(a ⊓ b) ^ 2 = a * b / mabs (b / a)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<GOAL>(IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔ IsSheafFor P R
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<GOAL>(∀ (x : FamilyOfElements P R), (∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂) ∧ (x.Compatible → ∃ t, x.IsAmalgamation t)) ↔ IsSheafFor P R
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<GOAL>∀ (a : FamilyOfElements P R), (∀ (t₁ t₂ : P.obj (op X)), a.IsAmalgamation t₁ → a.IsAmalgamation t₂ → t₁ = t₂) ∧ (a.Compatible → ∃ t, a.IsAmalgamation t) ↔ a.Compatible → ∃! t, a.IsAmalgamation t
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>n : ℕ<GOAL>(x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = x ^ n - y ^ n
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s : Set M<VAR>p : Submodule R M<GOAL>↑(lieSpan R L ↑p) = p ↔ ∃ N, ↑N = p
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s : Set M<VAR>p : Submodule R M<GOAL>↑(lieSpan R L ↑p) = p ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>q : Semiquot α<VAR>f : α → β<VAR>a : α<VAR>aq : a ∈ q<GOAL>∀ (h : ∀ a ∈ q, ∀ b ∈ q, f a = f b), q.liftOn f h = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>q : Semiquot α<VAR>f : α → β<VAR>a : α<VAR>aq : a ∈ q<GOAL>∀ (h : ∀ a_1 ∈ mk aq, ∀ b ∈ mk aq, f a_1 = f b), (mk aq).liftOn f h = f a
<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>ζ : M<VAR>f : F<VAR>h✝ h : IsPrimitiveRoot ζ k<VAR>h0 : 0 < k<GOAL>IsUnit ζ
<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>ζ : M<VAR>f : F<VAR>h✝ h : IsPrimitiveRoot ζ k<VAR>h0 : 0 < k<GOAL>ζ * ζ ^ (k - 1) = 1
<VAR>x : ℝ<GOAL>1 ^ x = 1
<VAR>x : ℝ<GOAL>↑(1 ^ x) = ↑1