ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<GOAL>∀ (a : X), ∃ x ∈ Set.range fun x => orbit G x, a ∈ x
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<GOAL>∅ ∉ Set.range fun x => orbit G x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a b : R<VAR>s : S<VAR>inst✝⁶ : MonoidWithZero R<VAR>inst✝⁵ : MonoidWithZero S<VAR>inst✝⁴ : Zero M<VAR>inst✝³ : MulActionWithZero R M<VAR>inst✝² : MulActionWithZero R S<VAR>inst✝¹ : MulActionWithZero S M<VAR>inst✝ : IsScalarTower R S M<GOAL>¬IsSMulRegular M 0 ↔ Nontrivial M
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a b : R<VAR>s : S<VAR>inst✝⁶ : MonoidWithZero R<VAR>inst✝⁵ : MonoidWithZero S<VAR>inst✝⁴ : Zero M<VAR>inst✝³ : MulActionWithZero R M<VAR>inst✝² : MulActionWithZero R S<VAR>inst✝¹ : MulActionWithZero S M<VAR>inst✝ : IsScalarTower R S M<GOAL>(¬∃ x y, x ≠ y) ↔ ∀ (x y : M), x = y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a b : R<VAR>s : S<VAR>inst✝⁶ : MonoidWithZero R<VAR>inst✝⁵ : MonoidWithZero S<VAR>inst✝⁴ : Zero M<VAR>inst✝³ : MulActionWithZero R M<VAR>inst✝² : MulActionWithZero R S<VAR>inst✝¹ : MulActionWithZero S M<VAR>inst✝ : IsScalarTower R S M<GOAL>(∀ (x y : M), x = y) ↔ ∀ (x y : M), x = y
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>C : SubMulAction G X<VAR>B : Set ↥C<GOAL>IsBlock G B ↔ IsBlock G (Subtype.val '' B)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>C : SubMulAction G X<VAR>B : Set ↥C<GOAL>(∀ (g : G), g • B = B ∨ Disjoint (g • B) B) ↔ ∀ (g : G), g • Subtype.val '' B = Subtype.val '' B ∨ Disjoint (g • Subtype.val '' B) (Subtype.val '' B)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>C : SubMulAction G X<VAR>B : Set ↥C<GOAL>∀ (a : G), a • B = B ∨ Disjoint (a • B) B ↔ a • Subtype.val '' B = Subtype.val '' B ∨ Disjoint (a • Subtype.val '' B) (Subtype.val '' B)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>C : SubMulAction G X<VAR>B : Set ↥C<VAR>g : G<GOAL>g • B = B ∨ Disjoint (g • B) B ↔ g • Subtype.val '' B = Subtype.val '' B ∨ Disjoint (g • Subtype.val '' B) (Subtype.val '' B)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>C : SubMulAction G X<VAR>B : Set ↥C<VAR>g : G<GOAL>(fun a => ↑a) '' (g • B) = (fun a => ↑a) '' B ∨ Disjoint (g • B) B ↔ ⇑C.inclusion '' (g • B) = ⇑C.inclusion '' B ∨ Disjoint (⇑C.inclusion '' (g • B)) (⇑C.inclusion '' B)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>C : SubMulAction G X<VAR>B : Set ↥C<VAR>g : G<GOAL>Disjoint (g • B) B ↔ Disjoint (⇑C.inclusion '' (g • B)) (⇑C.inclusion '' B)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>IsOpen ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>IsOpen (⋃₀ ∅)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y p₂ : P<VAR>h : p₂ ∈ s<GOAL>s.WSameSide x y ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y p₂ : P<VAR>h : p₂ ∈ s<GOAL>(y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedRing α<VAR>f g : ι → α<VAR>s : Set ι<VAR>a b c d : α<GOAL>Monovary f g ↔ ∀ (i j : ι), f i * g j + f j * g i ≤ f i * g i + f j * g j
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : Zero N<VAR>f g : α →₀ N<VAR>a✝ : α<GOAL>a✝ ∈ f.neLocus 0 ↔ a✝ ∈ f.support
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>s t : Submodule K V<VAR>inst✝¹ : FiniteDimensional K ↥s<VAR>inst✝ : FiniteDimensional K ↥t<GOAL>finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>s t : Submodule K V<VAR>inst✝¹ : FiniteDimensional K ↥s<VAR>inst✝ : FiniteDimensional K ↥t<VAR>key : Module.rank K ↥(s ⊔ t) + Module.rank K ↥(s ⊓ t) = Module.rank K ↥s + Module.rank K ↥t<GOAL>finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>s t : Submodule K V<VAR>inst✝¹ : FiniteDimensional K ↥s<VAR>inst✝ : FiniteDimensional K ↥t<VAR>key : ↑(finrank K ↥(s ⊔ t)) + ↑(finrank K ↥(s ⊓ t)) = ↑(finrank K ↥s) + ↑(finrank K ↥t)<GOAL>finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x y : R<VAR>h : x ≤ y<VAR>hx : IsSelfAdjoint x<GOAL>IsSelfAdjoint y
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x y : R<VAR>h : ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p<VAR>hx : IsSelfAdjoint x<GOAL>IsSelfAdjoint y
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x : R<VAR>hx : IsSelfAdjoint x<VAR>d : R<VAR>hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)<GOAL>IsSelfAdjoint (x + d)
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x : R<VAR>hx : IsSelfAdjoint x<VAR>d : R<VAR>hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)<GOAL>x + star d = x + d
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x : R<VAR>hx : IsSelfAdjoint x<VAR>d : R<VAR>hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)<GOAL>star d = d
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x : R<VAR>hx : IsSelfAdjoint x<VAR>d : R<VAR>hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)<GOAL>EqOn (⇑↑starAddEquiv) (⇑(AddMonoidHom.id R)) (range fun s => star s * s)
<VAR>α : Type u<VAR>a : α<VAR>inst✝¹ : Group α<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>x✝ : Fintype G<VAR>H : Subgroup G<VAR>hp : Fact (Nat.Prime (Fintype.card G))<GOAL>H = ⊥ ∨ H = ⊤
<VAR>x : ℝ<GOAL>x⁻¹.toNNReal = x.toNNReal⁻¹
<VAR>x : ℝ<VAR>hx : 0 ≤ x<GOAL>x⁻¹.toNNReal = x.toNNReal⁻¹
<VAR>x : ℝ<VAR>hx : x ≤ 0<GOAL>x⁻¹.toNNReal = x.toNNReal⁻¹
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsCofilteredOrEmpty C<VAR>F : C ⥤ Type u_1<VAR>j : C<VAR>x✝¹ x✝ : (i : C) ×' (i ⟶ j)<VAR>i : C<VAR>ij : i ⟶ j<VAR>k : C<VAR>kj : k ⟶ j<GOAL>∃ z, (fun x x_1 => x ⊇ x_1) ((fun f => Set.range (F.map f.snd)) ⟨i, ij⟩) ((fun f => Set.range (F.map f.snd)) z) ∧ (fun x x_1 => x ⊇ x_1) ((fun f => Set.range (F.map f.snd)) ⟨k, kj⟩) ((fun f => Set.range (F.map f.snd)) z)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsCofilteredOrEmpty C<VAR>F : C ⥤ Type u_1<VAR>j : C<VAR>x✝¹ x✝ : (i : C) ×' (i ⟶ j)<VAR>i : C<VAR>ij : i ⟶ j<VAR>k : C<VAR>kj : k ⟶ j<VAR>l : C<VAR>li : l ⟶ i<VAR>lk : l ⟶ k<VAR>e : li ≫ ij = lk ≫ kj<GOAL>∃ z, (fun x x_1 => x ⊇ x_1) ((fun f => Set.range (F.map f.snd)) ⟨i, ij⟩) ((fun f => Set.range (F.map f.snd)) z) ∧ (fun x x_1 => x ⊇ x_1) ((fun f => Set.range (F.map f.snd)) ⟨k, kj⟩) ((fun f => Set.range (F.map f.snd)) z)
<VAR>s : ℂ<GOAL>s.Gammaℝ = 0 ↔ ∃ n, s = -(2 * ↑n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set α<GOAL>r.image (s ∩ r.dom) = r.image s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set α<GOAL>r.image (s ∩ r.dom) ⊆ r.image s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set α<GOAL>r.image s ⊆ r.image (s ∩ r.dom)
<VAR>x : ℝ≥0∞<VAR>y z : ℝ<VAR>hx1 : x ≤ 1<VAR>hyz : z ≤ y<GOAL>x ^ y ≤ x ^ z
<VAR>y z : ℝ<VAR>hyz : z ≤ y<VAR>x : ℝ≥0<VAR>hx1 : ↑x ≤ 1<GOAL>↑x ^ y ≤ ↑x ^ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<VAR>hz : 0 < k<GOAL>(s.orderEmbOfFin h) ⟨0, hz⟩ = s.min' ⋯
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>sm : SplitMono f<VAR>Z✝ : C<VAR>g h : Z✝ ⟶ X<VAR>w : g ≫ f = h ≫ f<GOAL>g = h
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>sm : SplitMono f<VAR>Z✝ : C<VAR>g h : Z✝ ⟶ X<VAR>w : (g ≫ f) ≫ sm.retraction = (h ≫ f) ≫ sm.retraction<GOAL>g = h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PredOrder α<VAR>a b : α<VAR>inst✝ : NoMinOrder α<GOAL>pred a = pred b ↔ a = b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ ν : Measure ((i : ι) → α i)<VAR>inst✝ : ∀ (i : Finset ι), IsProbabilityMeasure (P i)<VAR>hμ : IsProjectiveLimit μ P<GOAL>μ univ = 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ ν : Measure ((i : ι) → α i)<VAR>inst✝ : ∀ (i : Finset ι), IsProbabilityMeasure (P i)<VAR>hμ : IsProjectiveLimit μ P<GOAL>(P ∅) univ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n✝ : ℤ<VAR>x : G<VAR>m n : ℤ<VAR>h : x ^ n = 1<GOAL>x ^ m = x ^ (m % n + n * (m / n))
<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>x : G<VAR>m n : ℤ<VAR>h : x ^ n = 1<GOAL>x ^ (m % n + n * (m / n)) = x ^ (m % n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁷ : AddCommMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N✝ : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝⁴ : Zero M<VAR>inst✝³ : Zero M'<VAR>inst✝² : CommMonoid N✝<VAR>inst✝¹ : DecidableEq α<VAR>N : Type u_16<VAR>inst✝ : AddCommMonoid N<VAR>f : α →₀ N<VAR>a : α<GOAL>(if a ∈ f.support then f a else 0) = f a
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁷ : AddCommMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N✝ : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝⁴ : Zero M<VAR>inst✝³ : Zero M'<VAR>inst✝² : CommMonoid N✝<VAR>inst✝¹ : DecidableEq α<VAR>N : Type u_16<VAR>inst✝ : AddCommMonoid N<VAR>f : α →₀ N<VAR>a : α<GOAL>f a = 0 → 0 = f a
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>N : Type u_4<VAR>inst✝ : CommMonoid N<VAR>s t : Submonoid N<VAR>x : N<GOAL>x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>p n : ℕ<VAR>inst✝¹ : CharP R p<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>(-1) ^ p ^ n = -1
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>p n : ℕ<VAR>inst✝¹ : CharP R p<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>(-1) ^ p ^ n + 1 = 0
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>p n : ℕ<VAR>inst✝¹ : CharP R p<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>(-1) ^ p ^ n + 1 ^ p ^ n = 0
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<GOAL>I + J = 1 ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : ℤ<VAR>n : ℕ<VAR>this : ↑p ^ (-↑n) = ↑↑p ^ (-↑n)<GOAL>‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : ℤ<VAR>n : ℕ<VAR>this : ↑p ^ (-↑n) = ↑↑p ^ (-↑n)<GOAL>↑(padicNorm p ↑k) ≤ ↑↑p ^ (-↑n) ↔ ↑p ^ n ∣ k
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : ℤ<VAR>n : ℕ<VAR>this : ↑p ^ (-↑n) = ↑↑p ^ (-↑n)<GOAL>padicNorm p ↑k ≤ ↑p ^ (-↑n) ↔ ↑(p ^ n) ∣ k
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝³ : PseudoMetricSpace X<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G X<VAR>inst✝ : IsometricSMul G X<VAR>c : G<VAR>x : X<VAR>r : ℝ<GOAL>(fun x => c • x) ⁻¹' sphere x r = sphere (c⁻¹ • x) r
<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>c ^ c = 2 ^ c
<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>2 ^ c ≤ c ^ c
<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>(2 ^ c) ^ c ≤ 2 ^ c
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>s : Set X<VAR>μ : Measure X<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : T2Space X<VAR>h₂s : μ s = 0<VAR>K : ℕ → Set X<VAR>hcompact : ∀ (n : ℕ), IsCompact (K n)<VAR>hcover : ⋃ n, K n = s<GOAL>IsMeagre s
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>s : Set X<VAR>μ : Measure X<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : T2Space X<VAR>h₂s : μ s = 0<VAR>K : ℕ → Set X<VAR>hcompact : ∀ (n : ℕ), IsCompact (K n)<VAR>hcover : ⋃ n, K n = s<VAR>h : ∀ (n : ℕ), IsNowhereDense (K n)<GOAL>IsMeagre s
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>s : Set X<VAR>μ : Measure X<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : T2Space X<VAR>h₂s : μ s = 0<VAR>K : ℕ → Set X<VAR>hcompact : ∀ (n : ℕ), IsCompact (K n)<VAR>hcover : ⋃ n, K n = s<VAR>h : ∀ (n : ℕ), IsNowhereDense (K n)<GOAL>∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>L : List (List α)<VAR>i : ℕ<VAR>h : i < L.length<GOAL>drop (take i (map length L)).sum (take (take (i + 1) (map length L)).sum L.join) = L[i]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>hμν : μ ≤ ν<VAR>f g : α → ℝ≥0∞<VAR>hfg : f ≤ g<GOAL>∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>hμν : μ ≤ ν<VAR>f g : α → ℝ≥0∞<VAR>hfg : f ≤ g<GOAL>⨆ g, ⨆ (_ : ↑g ≤ fun a => f a), g.lintegral μ ≤ ⨆ g_1, ⨆ (_ : ↑g_1 ≤ fun a => g a), g_1.lintegral ν
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>φ φ' : B → F ≃L[𝕜] F<VAR>U U' : Set B<VAR>hU : IsOpen U<VAR>hφ : ContinuousOn (fun x => ↑(φ x)) U<VAR>h2φ : ContinuousOn (fun x => ↑(φ x).symm) U<VAR>hU' : IsOpen U'<VAR>hφ' : ContinuousOn (fun x => ↑(φ' x)) U'<VAR>h2φ' : ContinuousOn (fun x => ↑(φ' x).symm) U'<GOAL>({ toFun := fun x => (x.1, (φ x.1) x.2), invFun := fun x => (x.1, (φ x.1).symm x.2), source := U ×ˢ univ, target := U ×ˢ univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, open_source := ⋯, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ } ≫ₕ { toFun := fun x => (x.1, (φ' x.1) x.2), invFun := fun x => (x.1, (φ' x.1).symm x.2), source := U' ×ˢ univ, target := U' ×ˢ univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, open_source := ⋯, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }).target = (U ∩ U') ×ˢ univ
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : AddMonoid A<VAR>h : ShiftMkCore C A<VAR>n : A<VAR>X : C<GOAL>(h.F n).obj X = (h.F (0 + n)).obj X
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : AddMonoid A<VAR>h : ShiftMkCore C A<VAR>n : A<VAR>X : C<GOAL>(h.add 0 n).inv.app X = (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>h : ∀ (a : α), a ∈ l → ¬p a = true<GOAL>eraseP p l = l
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹³ : Category.{?u.318300, u_1} C<VAR>inst✝¹² : Category.{?u.318304, u_2} D<VAR>inst✝¹¹ : Category.{?u.318308, u_3} E<VAR>inst✝¹⁰ : HasShift C ℤ<VAR>inst✝⁹ : HasShift D ℤ<VAR>inst✝⁸ : HasShift E ℤ<VAR>F : C ⥤ D<VAR>inst✝⁷ : F.CommShift ℤ<VAR>G : D ⥤ E<VAR>inst✝⁶ : G.CommShift ℤ<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : Preadditive D<VAR>inst✝³ : F.Additive<VAR>F₁ F₂ : C ⥤ D<VAR>e : F₁ ≅ F₂<VAR>inst✝² : F₁.CommShift ℤ<VAR>inst✝¹ : F₂.CommShift ℤ<VAR>inst✝ : NatTrans.CommShift e.hom ℤ<VAR>T : Triangle C<GOAL>(F₁.map T.mor₃ ≫ (F₁.commShiftIso 1).hom.app T.obj₁) ≫ (shiftFunctor D 1).map (e.hom.app T.obj₁) = e.hom.app T.obj₃ ≫ F₂.map T.mor₃ ≫ (F₂.commShiftIso 1).hom.app T.obj₁
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : AnalyticAt 𝕜 f x<GOAL>AnalyticAt 𝕜 (fun z => (z - x) ^ 0 • f z) x
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a b : α<VAR>hb : Acc r b<VAR>h : r a b<GOAL>succ ⋯.rank ≤ hb.rank
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a b : α<VAR>hb : Acc r b<VAR>h : r a b<GOAL>succ ⋯.rank ≤ sup fun b_1 => succ ⋯.rank
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a b : α<VAR>hb : Acc r b<VAR>h : r a b<GOAL>succ ⋯.rank ≤ succ ⋯.rank
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s✝ s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>f : α → β<VAR>g : α → γ<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<GOAL>(fun x => (f x, g x)) x ∈ (f '' s) ×ˢ (g '' s)
<VAR>x y : ℝ<VAR>hx : 0 < x<GOAL>rexp (log x) = x
<VAR>x y : ℝ<VAR>hx : 0 < x<GOAL>|x| = x
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>H : ∀ (a : α), a ∈ l → p a<GOAL>pmap f l H = map (fun x => f ↑x ⋯) l.attach
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>H : ∀ (a : α), a ∈ l → p a<GOAL>pmap f l H = pmap (fun a h => f ↑⟨a, h⟩ ⋯) l ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l✝ f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : Surjective f<VAR>l : Filter β<GOAL>range f ∈ l
<VAR>G : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : TopologicalGroup G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝⁴ : μ.IsHaarMeasure<VAR>inst✝³ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝² : μ'.IsMulLeftInvariant<VAR>inst✝¹ : μ.Regular<VAR>inst✝ : μ'.Regular<GOAL>μ' = μ'.haarScalarFactor μ • μ
<VAR>G : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : TopologicalGroup G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝⁴ : μ.IsHaarMeasure<VAR>inst✝³ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝² : μ'.IsMulLeftInvariant<VAR>inst✝¹ : μ.Regular<VAR>inst✝ : μ'.Regular<VAR>A : ∀ (U : Set G), IsOpen U → μ' U = (μ'.haarScalarFactor μ • μ) U<GOAL>μ' = μ'.haarScalarFactor μ • μ
<VAR>G : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : TopologicalGroup G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝⁴ : μ.IsHaarMeasure<VAR>inst✝³ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝² : μ'.IsMulLeftInvariant<VAR>inst✝¹ : μ.Regular<VAR>inst✝ : μ'.Regular<VAR>A : ∀ (U : Set G), IsOpen U → μ' U = (μ'.haarScalarFactor μ • μ) U<VAR>s : Set G<VAR>_hs : MeasurableSet s<GOAL>μ' s = (μ'.haarScalarFactor μ • μ) s
<VAR>G : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : TopologicalGroup G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝⁴ : μ.IsHaarMeasure<VAR>inst✝³ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝² : μ'.IsMulLeftInvariant<VAR>inst✝¹ : μ.Regular<VAR>inst✝ : μ'.Regular<VAR>A : ∀ (U : Set G), IsOpen U → μ' U = (μ'.haarScalarFactor μ • μ) U<VAR>s : Set G<VAR>_hs : MeasurableSet s<GOAL>⨅ U, ⨅ (_ : s ⊆ U), ⨅ (_ : IsOpen U), μ' U = ⨅ U, ⨅ (_ : s ⊆ U), ⨅ (_ : IsOpen U), (μ'.haarScalarFactor μ • μ) U
<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>R : Type u_1<VAR>inst✝ : CommRing R<VAR>h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R hR => IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing<VAR>x : R<VAR>hx : IsNilpotent x<GOAL>x = 0
<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>R : Type u_1<VAR>inst✝ : CommRing R<VAR>h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R hR => IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing<VAR>x : R<VAR>hx : IsNilpotent x<GOAL>∀ (J : Ideal R) (hJ : J.IsMaximal), (algebraMap R (Localization.AtPrime J)) x = 0
<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>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : R<VAR>hx : IsNilpotent x<VAR>J : Ideal R<VAR>hJ : J.IsMaximal<VAR>h : IsReduced (Localization.AtPrime J)<GOAL>(algebraMap R (Localization.AtPrime J)) x = 0
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>n : σ<VAR>f : MvPolynomial σ R<GOAL>degreeOf n f = f.support.sup fun m => m n
<VAR>α✝ : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a✝ : Ordinal.{u_3}<VAR>α : Type u_3<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>a x : α<VAR>x✝ : ∀ (y : α), r y x → Acc r y<VAR>IH : ∀ (y : α), r y x → Acc (fun x x_1 => x < x_1) (typein r y)<VAR>o : Ordinal.{u_3}<VAR>h : o < typein r x<GOAL>Acc (fun x x_1 => x < x_1) o
<VAR>α✝ : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a✝ : Ordinal.{u_3}<VAR>α : Type u_3<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>a x : α<VAR>x✝ : ∀ (y : α), r y x → Acc r y<VAR>IH : ∀ (y : α), r y x → Acc (fun x x_1 => x < x_1) (typein r y)<VAR>b : α<VAR>h : typein r b < typein r x<GOAL>Acc (fun x x_1 => x < x_1) (typein r b)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>n : ℕ<VAR>inst✝ : IsDomain R<VAR>hpos : 0 < n<VAR>μ : R<VAR>h : IsPrimitiveRoot μ n<GOAL>(cyclotomic n R).IsRoot μ
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>n : ℕ<VAR>inst✝ : IsDomain R<VAR>hpos : 0 < n<VAR>μ : R<VAR>h : IsPrimitiveRoot μ n<GOAL>μ ∈ primitiveRoots n R