ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι✝ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>ι : Type u_5<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ<VAR>As_disj : Pairwise (AEDisjoint μ on As)<VAR>Union_As_finite : μ (⋃ i, As i) ≠ ⊤<VAR>posmeas : Set ι := {i | 0 < μ (As i)}<VAR>posmeas_def : posmeas = {i | 0 < μ (As i)}<VAR>as : ℕ → ℝ≥0∞<VAR>left✝ : StrictAnti as<VAR>as_mem : ∀ (n : ℕ), as n ∈ Ioo 0 1<VAR>as_lim : Tendsto as atTop (𝓝 0)<VAR>fairmeas : ℕ → Set ι := fun n => {i | as n ≤ μ (As i)}<VAR>countable_union : posmeas = ⋃ n, fairmeas n<GOAL>posmeas.Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι✝ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>ι : Type u_5<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ<VAR>As_disj : Pairwise (AEDisjoint μ on As)<VAR>Union_As_finite : μ (⋃ i, As i) ≠ ⊤<VAR>posmeas : Set ι := {i | 0 < μ (As i)}<VAR>posmeas_def : posmeas = {i | 0 < μ (As i)}<VAR>as : ℕ → ℝ≥0∞<VAR>left✝ : StrictAnti as<VAR>as_mem : ∀ (n : ℕ), as n ∈ Ioo 0 1<VAR>as_lim : Tendsto as atTop (𝓝 0)<VAR>fairmeas : ℕ → Set ι := fun n => {i | as n ≤ μ (As i)}<VAR>countable_union : posmeas = ⋃ n, fairmeas n<GOAL>(⋃ n, fairmeas n).Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι✝ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>ι : Type u_5<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ<VAR>As_disj : Pairwise (AEDisjoint μ on As)<VAR>Union_As_finite : μ (⋃ i, As i) ≠ ⊤<VAR>posmeas : Set ι := {i | 0 < μ (As i)}<VAR>posmeas_def : posmeas = {i | 0 < μ (As i)}<VAR>as : ℕ → ℝ≥0∞<VAR>left✝ : StrictAnti as<VAR>as_mem : ∀ (n : ℕ), as n ∈ Ioo 0 1<VAR>as_lim : Tendsto as atTop (𝓝 0)<VAR>fairmeas : ℕ → Set ι := fun n => {i | as n ≤ μ (As i)}<VAR>countable_union : posmeas = ⋃ n, fairmeas n<VAR>n : ℕ<GOAL>(fairmeas n).Finite
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle y (y - x)).tan * ‖y‖ = ‖x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle y (y - x)).sign = 1<GOAL>(o.oangle y (y - x)).tan * ‖y‖ = ‖x‖
<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>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>φ₁ φ₂ : F ⟶ G<VAR>ho : Homotopy φ₁ φ₂<GOAL>ofHom φ₁ = δ (-1) 0 (ofHomotopy ho) + ofHom φ₂
<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>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>φ₁ φ₂ : F ⟶ G<VAR>z : { z // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }<VAR>p : ℤ<GOAL>φ₁.f p = (((dNext p) fun i j => if hij : i + -1 = j then (↑z).v i j hij else 0) + (prevD p) fun i j => if hij : i + -1 = j then (↑z).v i j hij else 0) + φ₂.f p
<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>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>φ₁ φ₂ : F ⟶ G<VAR>z : { z // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }<VAR>p : ℤ<VAR>eq : (ofHom φ₁).v p p ⋯ = (δ (-1) 0 ↑z + ofHom φ₂).v p p ⋯<GOAL>φ₁.f p = (((dNext p) fun i j => if hij : i + -1 = j then (↑z).v i j hij else 0) + (prevD p) fun i j => if hij : i + -1 = j then (↑z).v i j hij else 0) + φ₂.f p
<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>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>φ₁ φ₂ : F ⟶ G<VAR>z : { z // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }<VAR>p : ℤ<VAR>eq : (ofHom φ₁).v p p ⋯ = (δ (-1) 0 ↑z + ofHom φ₂).v p p ⋯<VAR>h₁ : (ComplexShape.up ℤ).Rel (p - 1) p<VAR>h₂ : (ComplexShape.up ℤ).Rel p (p + 1)<GOAL>φ₁.f p = (((dNext p) fun i j => if hij : i + -1 = j then (↑z).v i j hij else 0) + (prevD p) fun i j => if hij : i + -1 = j then (↑z).v i j hij else 0) + φ₂.f p
<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>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>φ₁ φ₂ : F ⟶ G<VAR>z : { z // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }<VAR>p : ℤ<VAR>h₁ : (ComplexShape.up ℤ).Rel (p - 1) p<VAR>h₂ : (ComplexShape.up ℤ).Rel p (p + 1)<VAR>eq : φ₁.f p = F.d p (p + 1) ≫ (↑z).v (p + 1) p ⋯ + (↑z).v p (p - 1) ⋯ ≫ G.d (p - 1) p + φ₂.f p<GOAL>φ₁.f p = (((dNext p) fun i j => if hij : i + -1 = j then (↑z).v i j hij else 0) + (prevD p) fun i j => if hij : i + -1 = j then (↑z).v i j hij else 0) + φ₂.f p
<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>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>φ₁ φ₂ : F ⟶ G<VAR>z : { z // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }<VAR>p q : ℤ<VAR>hpq : p + -1 = q<GOAL>(if hij : p + -1 = q then (↑z).v p q hij else 0) = (↑z).v p q hpq
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>X : Type u_2<VAR>inst✝² : MulAction G X<VAR>H : Type u_3<VAR>Y : Type u_4<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction H Y<VAR>φ : H → G<VAR>j : Y →ₑ[φ] X<VAR>B : Set X<VAR>hB : IsBlock G B<GOAL>IsBlock H (⇑j ⁻¹' B)
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>X : Type u_2<VAR>inst✝² : MulAction G X<VAR>H : Type u_3<VAR>Y : Type u_4<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction H Y<VAR>φ : H → G<VAR>j : Y →ₑ[φ] X<VAR>B : Set X<VAR>hB : IsBlock G B<GOAL>∀ (g : H), g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>X : Type u_2<VAR>inst✝² : MulAction G X<VAR>H : Type u_3<VAR>Y : Type u_4<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction H Y<VAR>φ : H → G<VAR>j : Y →ₑ[φ] X<VAR>B : Set X<VAR>hB : IsBlock G B<VAR>g : H<GOAL>g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>X : Type u_2<VAR>inst✝² : MulAction G X<VAR>H : Type u_3<VAR>Y : Type u_4<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction H Y<VAR>φ : H → G<VAR>j : Y →ₑ[φ] X<VAR>B : Set X<VAR>hB : IsBlock G B<VAR>g : H<GOAL>⇑j ⁻¹' (φ g • B) = ⇑j ⁻¹' B ∨ Disjoint (⇑j ⁻¹' (φ g • B)) (⇑j ⁻¹' B)
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>X : Type u_2<VAR>inst✝² : MulAction G X<VAR>H : Type u_3<VAR>Y : Type u_4<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction H Y<VAR>φ : H → G<VAR>j : Y →ₑ[φ] X<VAR>B : Set X<VAR>hB : IsBlock G B<VAR>g : H<GOAL>φ g • B = B → ⇑j ⁻¹' (φ g • B) = ⇑j ⁻¹' B
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>X : Type u_2<VAR>inst✝² : MulAction G X<VAR>H : Type u_3<VAR>Y : Type u_4<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction H Y<VAR>φ : H → G<VAR>j : Y →ₑ[φ] X<VAR>B : Set X<VAR>hB : IsBlock G B<VAR>g : H<GOAL>Disjoint (φ g • B) B → Disjoint (⇑j ⁻¹' (φ g • B)) (⇑j ⁻¹' B)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>x y✝ z : E<VAR>h : ConvexOn 𝕜 s f<VAR>hw₀ : ∀ i ∈ t, 0 ≤ w i<VAR>hw₁ : 0 < ∑ i ∈ t, w i<VAR>hp : ∀ i ∈ t, p i ∈ s<VAR>y : E := t.centerMass w p<GOAL>∃ i ∈ t, f y ≤ f (p i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>x y✝ z : E<VAR>h : ConvexOn 𝕜 s f<VAR>hw₀ : ∀ i ∈ t, 0 ≤ w i<VAR>hw₁ : 0 < ∑ i ∈ t, w i<VAR>hp : ∀ i ∈ t, p i ∈ s<VAR>y : E := t.centerMass w p<VAR>i : ι<VAR>hi : i ∈ filter (fun i => w i ≠ 0) t<VAR>hfi : w i • f y ≤ w i • (f ∘ p) i<GOAL>∃ i ∈ t, f y ≤ f (p i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>x y✝ z : E<VAR>h : ConvexOn 𝕜 s f<VAR>hw₀ : ∀ i ∈ t, 0 ≤ w i<VAR>hw₁ : 0 < ∑ i ∈ t, w i<VAR>hp : ∀ i ∈ t, p i ∈ s<VAR>y : E := t.centerMass w p<VAR>i : ι<VAR>hi : i ∈ t ∧ w i ≠ 0<VAR>hfi : w i • f y ≤ w i • (f ∘ p) i<GOAL>∃ i ∈ t, f y ≤ f (p i)
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : Set (Subsemigroup M)<VAR>s : Subsemigroup M<VAR>hs : s ∈ S<GOAL>∀ {x : M}, x ∈ s → x ∈ sSup S
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : Set (Subsemigroup M)<VAR>s : Subsemigroup M<VAR>hs : s ∈ S<VAR>this : s ≤ sSup S<GOAL>∀ {x : M}, x ∈ s → x ∈ sSup S
<VAR>p : ℝ<VAR>hp : Fact (0 < p)<VAR>m n : ℕ<GOAL>‖↑(↑m / ↑n * p)‖ = p * (↑(min (m % n) (n - m % n)) / ↑n)
<VAR>p : ℝ<VAR>hp : Fact (0 < p)<VAR>m n : ℕ<VAR>this : p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n<GOAL>‖↑(↑m / ↑n * p)‖ = p * (↑(min (m % n) (n - m % n)) / ↑n)
<VAR>X : Type u_1<VAR>Y✝ : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝ g✝ : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>Y : Type u_5<VAR>inst✝ : MeasurableSpace Y<VAR>g : X → Y<VAR>f : Y → E<VAR>s : Set Y<VAR>hs : MeasurableSet s<VAR>hf : AEStronglyMeasurable f (Measure.map g μ)<VAR>hg : AEMeasurable g μ<GOAL>∫ (y : Y) in s, f y ∂Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ
<VAR>X : Type u_1<VAR>Y✝ : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝ g✝ : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>Y : Type u_5<VAR>inst✝ : MeasurableSpace Y<VAR>g : X → Y<VAR>f : Y → E<VAR>s : Set Y<VAR>hs : MeasurableSet s<VAR>hf : AEStronglyMeasurable f (Measure.map g μ)<VAR>hg : AEMeasurable g μ<GOAL>Measure.map g (μ.restrict (g ⁻¹' s)) ≤ Measure.map g μ
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>ψ : L ⟶ M<VAR>i j k : ι<VAR>inst✝² : K.HasHomology i<VAR>inst✝¹ : L.HasHomology i<VAR>inst✝ : M.HasHomology i<GOAL>ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ ≫ ψ)) = ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ) ≫ ShortComplex.homologyMap ((shortComplexFunctor C c i).map ψ)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_2<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : Finite α<VAR>this✝ : Fintype α<VAR>this : Fintype ↑(fixedPoints G α)<GOAL>Nat.card α ≡ Nat.card ↑(fixedPoints G α) [MOD p]
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_2<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : Finite α<VAR>this✝ : Fintype α<VAR>this : Fintype ↑(fixedPoints G α)<GOAL>card α ≡ card ↑(fixedPoints G α) [MOD p]
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>x y : α<GOAL>(fixedBy α (swap x y))ᶜ.Finite
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s✝ t : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>s : Finset α<GOAL>s ∈ ∂⁺ 𝒜ᶜˢ ↔ s ∈ (∂ 𝒜)ᶜˢ
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s✝ t : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>s : Finset α<GOAL>(∃ s_1, s_1ᶜ ∈ 𝒜 ∧ ∃ a ∉ s_1, insert a s_1 = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∈ s_1, s_1.erase a = sᶜ
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s✝ t : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>s : Finset α<GOAL>(∃ b, ((Equiv.symm (Function.Involutive.toPerm compl ⋯)) b)ᶜ ∈ 𝒜 ∧ ∃ a ∉ (Equiv.symm (Function.Involutive.toPerm compl ⋯)) b, insert a ((Equiv.symm (Function.Involutive.toPerm compl ⋯)) b) = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∈ s_1, s_1.erase a = sᶜ
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : Cᵒᵖ<GOAL>IsCodetector (unop G) ↔ IsDetector G
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : Monoid P<VAR>f : M →* P<VAR>g : N →* P<GOAL>MonoidHom.mrange (lift f g) = MonoidHom.mrange f ⊔ MonoidHom.mrange g
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : α<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>edist x y ≤ ENNReal.ofReal r ↔ dist x y ≤ r
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a * a⁻¹ < a * b ↔ 1 < a * b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ a b c : α<VAR>h₁ : a ≤ b<VAR>h₂ : b ≤ c<GOAL>Ioc a b ∪ Ioc b c = Ioc a c
<VAR>E : Type u_1<VAR>f : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : ℝ → E<VAR>p : ℝ<VAR>hp : 0 < p<GOAL>∫ (x : ℝ) in Ioi 0, (p * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi 0, g y
<VAR>E : Type u_1<VAR>f : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : ℝ → E<VAR>p : ℝ<VAR>hp : 0 < p<VAR>x✝ : ℝ<GOAL>p = |p|
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>inst✝ : NonAssocSemiring R<VAR>s : Set R<GOAL>(closure s).op = closure (MulOpposite.unop ⁻¹' s)
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>inst✝ : NonAssocSemiring R<VAR>s : Set R<GOAL>sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>inst✝ : NonAssocSemiring R<VAR>s : Set R<VAR>a : Subsemiring Rᵐᵒᵖ<GOAL>a ∈ {a | s ⊆ MulOpposite.op ⁻¹' ↑a} ↔ a ∈ {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
<VAR>α : Type u<VAR>c d : Cardinal.{u}<GOAL>toNat c = 1 ↔ c = 1
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>pullback.lift S.L₁.f 0 ⋯ ≫ S.φ₁ = S.v₁₂.τ₁
<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>a✝ b c✝ d x✝ y z : P<VAR>r R✝ : ℝ<VAR>c : P<VAR>a R : ℝ<VAR>x : P<GOAL>inversion c (a * R) x = (homothety c (a ^ 2)) (inversion c R x)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>inst✝¹ : IsDomain R<VAR>G : Subgroup Rˣ<VAR>inst✝ : Fintype ↥G<GOAL>nodal (↑G).toFinset Units.val = X ^ Fintype.card ↥G - 1
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>inst✝¹ : IsDomain R<VAR>G : Subgroup Rˣ<VAR>inst✝ : Fintype ↥G<VAR>h : degree 1 < (X ^ Fintype.card ↥G).degree<GOAL>nodal (↑G).toFinset Units.val = X ^ Fintype.card ↥G - 1
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>inst✝¹ : IsDomain R<VAR>G : Subgroup Rˣ<VAR>inst✝ : Fintype ↥G<VAR>h : degree 1 < (X ^ Fintype.card ↥G).degree<GOAL>Set.InjOn Units.val ↑(↑G).toFinset
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>inst✝¹ : IsDomain R<VAR>G : Subgroup Rˣ<VAR>inst✝ : Fintype ↥G<VAR>h : degree 1 < (X ^ Fintype.card ↥G).degree<GOAL>(nodal (↑G).toFinset Units.val).degree ≤ ↑(↑G).toFinset.card
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>inst✝¹ : IsDomain R<VAR>G : Subgroup Rˣ<VAR>inst✝ : Fintype ↥G<VAR>h : degree 1 < (X ^ Fintype.card ↥G).degree<GOAL>(nodal (↑G).toFinset Units.val).degree = (X ^ Fintype.card ↥G - 1).degree
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>inst✝¹ : IsDomain R<VAR>G : Subgroup Rˣ<VAR>inst✝ : Fintype ↥G<VAR>h : degree 1 < (X ^ Fintype.card ↥G).degree<GOAL>(nodal (↑G).toFinset Units.val).leadingCoeff = (X ^ Fintype.card ↥G - 1).leadingCoeff
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>inst✝¹ : IsDomain R<VAR>G : Subgroup Rˣ<VAR>inst✝ : Fintype ↥G<VAR>h : degree 1 < (X ^ Fintype.card ↥G).degree<GOAL>∀ i ∈ (↑G).toFinset, eval (↑i) (nodal (↑G).toFinset Units.val) = eval (↑i) (X ^ Fintype.card ↥G - 1)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>i j : σ →₀ ℕ<GOAL>(monomial i) 1 ∣ (monomial j) 1 ↔ i ≤ j
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>i j : σ →₀ ℕ<GOAL>(1 = 0 ∨ i ≤ j) ∧ 1 ∣ 1 ↔ i ≤ j
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f✝ g : α → E<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → α → E<VAR>this : DecidableEq ι<GOAL>(∀ i ∈ s, Memℒp (f i) p μ) → Memℒp (fun a => ∑ i ∈ s, f i a) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f✝ g : α → E<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → α → E<VAR>this : DecidableEq ι<GOAL>(∀ i ∈ ∅, Memℒp (f i) p μ) → Memℒp (fun a => ∑ i ∈ ∅, f i a) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f✝ g : α → E<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → α → E<VAR>this : DecidableEq ι<GOAL>∀ ⦃a : ι⦄ {s : Finset ι}, a ∉ s → ((∀ i ∈ s, Memℒp (f i) p μ) → Memℒp (fun a => ∑ i ∈ s, f i a) p μ) → (∀ i ∈ insert a s, Memℒp (f i) p μ) → Memℒp (fun a_3 => ∑ i ∈ insert a s, f i a_3) p μ
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>α : Type u_4<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<GOAL>diam (closure s) = diam s
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : (a : α) → DecidableEq (N a)<VAR>inst✝ : (a : α) → Zero (N a)<VAR>f g : Π₀ (a : α), N a<VAR>a✝ : α<GOAL>a✝ ∈ f.neLocus 0 ↔ a✝ ∈ f.support
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝² : Monoid N<VAR>inst✝¹ : (i : ι) → DecidableEq (M i)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>p : Pair M i<GOAL>rcons p = of p.head • p.tail
<VAR>α : Type u<VAR>inst✝ : CanonicallyOrderedCommMonoid α<VAR>a c✝ d c : α<GOAL>a ≤ a * c
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddGroup R<VAR>x : HahnSeries Γ R<GOAL>(-x).orderTop = x.orderTop
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ : Cat<VAR>f✝ : a✝ ⟶ b✝<GOAL>({ obj := fun C => Cat.of (WithTerminal ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map₂ (𝟙 f✝)).app = (𝟙 ({ obj := fun C => Cat.of (WithTerminal ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map f✝)).app
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ : Cat<VAR>f✝ : a✝ ⟶ b✝<VAR>X : ↑({ obj := fun C => Cat.of (WithTerminal ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.obj a✝)<GOAL>({ obj := fun C => Cat.of (WithTerminal ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map₂ (𝟙 f✝)).app X = (𝟙 ({ obj := fun C => Cat.of (WithTerminal ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map f✝)).app X
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ : Cat<VAR>f✝ g✝ h✝ : a✝ ⟶ b✝<VAR>η✝ : f✝ ⟶ g✝<VAR>θ✝ : g✝ ⟶ h✝<GOAL>({ obj := fun C => Cat.of (WithTerminal ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map₂ (η✝ ≫ θ✝)).app = ({ obj := fun C => Cat.of (WithTerminal ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map₂ η✝ ≫ { obj := fun C => Cat.of (WithTerminal ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map₂ θ✝).app
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ : Cat<VAR>f✝ g✝ h✝ : a✝ ⟶ b✝<VAR>η✝ : f✝ ⟶ g✝<VAR>θ✝ : g✝ ⟶ h✝<VAR>X : ↑({ obj := fun C => Cat.of (WithTerminal ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.obj a✝)<GOAL>({ obj := fun C => Cat.of (WithTerminal ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map₂ (η✝ ≫ θ✝)).app X = ({ obj := fun C => Cat.of (WithTerminal ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map₂ η✝ ≫ { obj := fun C => Cat.of (WithTerminal ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map₂ θ✝).app X
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>inst✝ : Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<GOAL>Orthonormal 𝕜 ⇑b
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s✝ s : Set α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε<GOAL>TotallyBounded s
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s✝ s : Set α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε<VAR>hs : s = ∅<GOAL>TotallyBounded s
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s✝ s : Set α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε<VAR>hs : s.Nonempty<GOAL>TotallyBounded s
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s✝ s : Set α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε<VAR>x0 : α<VAR>hx0 : x0 ∈ s<VAR>this : Inhabited ↑s<GOAL>TotallyBounded s
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε✝ ε₁ ε₂ : ℝ<VAR>s✝ s : Set α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε<VAR>x0 : α<VAR>hx0 : x0 ∈ s<VAR>this : Inhabited ↑s<VAR>ε : ℝ<VAR>ε0 : ε > 0<GOAL>∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
<VAR>α : Type u<VAR>β✝ : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε✝ ε₁ ε₂ : ℝ<VAR>s✝ s : Set α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε<VAR>x0 : α<VAR>hx0 : x0 ∈ s<VAR>this : Inhabited ↑s<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>β : Type u<VAR>fβ : Fintype β<VAR>F : ↑s → β<VAR>hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε<VAR>Finv : β → ↑s := Function.invFun F<GOAL>∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
<VAR>α : Type u<VAR>β✝ : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x✝ y z : α<VAR>δ ε✝ ε₁ ε₂ : ℝ<VAR>s✝ s : Set α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε<VAR>x0 : α<VAR>hx0 : x0 ∈ s<VAR>this : Inhabited ↑s<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>β : Type u<VAR>fβ : Fintype β<VAR>F : ↑s → β<VAR>hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε<VAR>Finv : β → ↑s := Function.invFun F<VAR>x : α<VAR>xs : x ∈ s<GOAL>x ∈ ⋃ y ∈ range (Subtype.val ∘ Finv), ball y ε
<VAR>α : Type u<VAR>β✝ : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x✝ y z : α<VAR>δ ε✝ ε₁ ε₂ : ℝ<VAR>s✝ s : Set α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε<VAR>x0 : α<VAR>hx0 : x0 ∈ s<VAR>this : Inhabited ↑s<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>β : Type u<VAR>fβ : Fintype β<VAR>F : ↑s → β<VAR>hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε<VAR>Finv : β → ↑s := Function.invFun F<VAR>x : α<VAR>xs : x ∈ s<VAR>x' : ↑s := Finv (F ⟨x, xs⟩)<GOAL>x ∈ ⋃ y ∈ range (Subtype.val ∘ Finv), ball y ε