ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>a b : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>inst✝ : CompleteSpace A<VAR>hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x<VAR>huv' : IntegrableOn (fun i => u i * v' i) (Ioi a) volume<VAR>hu'v : IntegrableOn (fun i => u' i * v i) (Ioi a) volume<VAR>h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')<VAR>h_infty : Tendsto (u * v) atTop (𝓝 b')<GOAL>∫ (x : ℝ) in Ioi a, u x * v' x = b' - a' - ∫ (x : ℝ) in Ioi a, u' x * v x
<VAR>A : Type u_1<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>a b : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>inst✝ : CompleteSpace A<VAR>hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x<VAR>huv' : IntegrableOn (fun i => u i * v' i) (Ioi a) volume<VAR>hu'v : IntegrableOn (fun i => u' i * v i) (Ioi a) volume<VAR>h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')<VAR>h_infty : Tendsto (u * v) atTop (𝓝 b')<GOAL>∫ (a : ℝ) in Ioi a, u a * v' a + u' a * v a ∂volume = b' - a'
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>f : F' ⟶ F<VAR>U V : Cᵒᵖ<VAR>i : U ⟶ V<VAR>x : F'.obj U<GOAL>f.app U x ∈ F.map i ⁻¹' (fun U => Set.range (f.app U)) V
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>f : F' ⟶ F<VAR>U V : Cᵒᵖ<VAR>i : U ⟶ V<VAR>x : F'.obj U<VAR>this : ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : F'.obj X), f.app Y (F'.map f_1 x) = F.map f_1 (f.app X x)<GOAL>f.app U x ∈ F.map i ⁻¹' (fun U => Set.range (f.app U)) V
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>m : M<VAR>a : α<GOAL>period m a ∣ orderOf m
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>X : C<VAR>Y : Over X<VAR>S : Sieve Y.left<VAR>hS : S ∈ J.sieves Y.left<GOAL>(Sieve.overEquiv Y).symm S ∈ (J.over X).sieves Y
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ ≠ x₂<GOAL>W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.negY (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) = ((y₂ - W.negY x₂ y₂) * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) - (y₁ - W.negY x₁ y₁) * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) / (x₂ - x₁)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ ≠ x₂<GOAL>(-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃ - (-(-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃)) * (x₂ - x₁) = (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) - (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>c : ℝ<GOAL>cgf (fun x => c) μ t = t * c
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<VAR>J : Type u_4<VAR>i : J ≃ I<GOAL>OrthogonalIdempotents (e ∘ ⇑i) ↔ OrthogonalIdempotents e
<VAR>a✝ b✝ c : ℕ<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>a : α<VAR>b : ℤ<VAR>nb : ℕ<VAR>num : ℤ<VAR>den : ℕ<VAR>pb : IsInt b (Int.negOfNat nb)<VAR>pe' : IsRat (a ^ nb)⁻¹ num den<GOAL>IsRat (a ^ b) num den
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₃₁ : X₃₁ ⟶ X₃₂<VAR>v₃₁ : X₁₁ ⟶ X₃₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₂₁ : X₂₁ ⟶ X₃₁<VAR>v₂₂ : X₂₂ ⟶ X₃₂<VAR>s : IsPullback h₁₁ v₃₁ (v₁₂ ≫ v₂₂) h₃₁<VAR>t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁<GOAL>(h₁₁ ≫ v₁₂) ≫ v₂₂ = v₃₁ ≫ h₃₁
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₃₁ : X₃₁ ⟶ X₃₂<VAR>v₃₁ : X₁₁ ⟶ X₃₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₂₁ : X₂₁ ⟶ X₃₁<VAR>v₂₂ : X₂₂ ⟶ X₃₂<VAR>s : IsPullback h₁₁ v₃₁ (v₁₂ ≫ v₂₂) h₃₁<VAR>t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁<GOAL>h₁₁ ≫ v₁₂ = t.lift (h₁₁ ≫ v₁₂) v₃₁ ⋯ ≫ h₂₁
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>hl : l.reverse ≠ []<GOAL>0 < l.length
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>hl : l.length ≤ 0<GOAL>l.reverse = []
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>hl : l.reverse ≠ []<VAR>hl' : optParam (0 < l.length) ⋯<GOAL>l.reverse.getLast hl = l.get ⟨0, hl'⟩
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>hl : l.reverse ≠ []<VAR>hl' : optParam (0 < l.length) ⋯<GOAL>l.get ⟨l.length - 1 - ↑⟨l.reverse.length - 1, ⋯⟩, ?hn'⟩ = l.get ⟨0, hl'⟩
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>hl : l.reverse ≠ []<VAR>hl' : optParam (0 < l.length) ⋯<GOAL>l.length - 1 - ↑⟨l.reverse.length - 1, ⋯⟩ < l.length
<VAR>z : ℂ<GOAL>sin z = 0 ↔ cos z = 1 ∨ cos z = -1
<VAR>z : ℂ<GOAL>sin z = 0 ↔ 0 = sin z * sin z
<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>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g : α → β<VAR>μ ν : Measure α<VAR>h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y<GOAL>AEMeasurable 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>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g : α → β<VAR>ν : Measure α<VAR>h : ∀ᵐ (x : α) (y : α) ∂0, f x = f y<GOAL>AEMeasurable f 0
<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>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g : α → β<VAR>μ ν : Measure α<VAR>h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y<VAR>hμ : μ ≠ 0<GOAL>AEMeasurable f μ
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<GOAL>hausdorffDist ∅ s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>a : α<VAR>n : ℕ<GOAL>Associates.mk (a ^ n) = Associates.mk a ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>inst✝ : CompleteLattice β<VAR>S : Set (Set α)<VAR>p : α → Prop<GOAL>(∃ x ∈ ⋃₀ S, p x) ↔ ∃ s ∈ S, ∃ x ∈ s, p x
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>x y : HahnSeries Γ R<GOAL>(x * y).support ⊆ x.support + y.support
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>x y : HahnSeries Γ R<GOAL>((HahnModule.of R).symm (x • (HahnModule.of R) y)).support ⊆ x.support +ᵥ y.support
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>p : W → Prop<VAR>w : W<VAR>one : p 1<VAR>mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)<VAR>p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w<GOAL>p w
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>p : W → Prop<VAR>w : W<VAR>one : p 1<VAR>mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)<VAR>p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w<VAR>this : w ∈ Submonoid.closure (Set.range cs.simple)<GOAL>p w
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>p : W → Prop<VAR>w : W<VAR>one : p 1<VAR>mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)<VAR>p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w<VAR>this : w ∈ Submonoid.closure (Set.range cs.simple)<GOAL>p' 1 ⋯
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>p : W → Prop<VAR>w : W<VAR>one : p 1<VAR>mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)<VAR>p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w<VAR>this : w ∈ Submonoid.closure (Set.range cs.simple)<GOAL>∀ (x : W) (hx : x ∈ Set.range cs.simple) (y : W) (hy : y ∈ Submonoid.closure (Set.range cs.simple)), p' y hy → p' (x * y) ⋯
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>p : W → Prop<VAR>w : W<VAR>one : p 1<VAR>mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)<VAR>p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w<VAR>this : w ∈ Submonoid.closure (Set.range cs.simple)<GOAL>w ∈ Submonoid.closure (Set.range cs.simple)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → β → β<VAR>b : β<VAR>hf : ∀ (a : α), f a b = b<VAR>a : α<VAR>l : List α<GOAL>foldr f b (a :: l) = b
<VAR>β✝ : Type w<VAR>α : Type w₂<VAR>γ : Type w₃<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>β : Type w<VAR>f : β → C<VAR>inst✝ : HasProduct f<VAR>P : C<VAR>p : (b : β) → P ⟶ f b<VAR>b : β<GOAL>lift p ≫ π f b = p b
<VAR>x y : EReal<GOAL>(∀ (z : ℝ), ↑z < y → ↑z ≤ x) ↔ y ≤ x
<VAR>x y : EReal<VAR>h : ∀ (z : ℝ), ↑z < y → ↑z ≤ x<GOAL>y ≤ x
<VAR>f : ℕ → ℂ<VAR>h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C<GOAL>abscissaOfAbsConv f ≤ 1
<VAR>f : ℕ → ℂ<VAR>h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C<GOAL>1 = ↑0 + 1
<VAR>f : ℕ → ℂ<VAR>h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C<GOAL>∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hf : HasStrictFDerivAt f f' x<VAR>hg : HasStrictFDerivAt g g' x<VAR>y : E × E<GOAL>f y.1 - f y.2 - f' (y.1 - y.2) + (g y.1 - g y.2 - g' (y.1 - y.2)) = (fun y => f y + g y) y.1 - (fun y => f y + g y) y.2 - (f' + g') (y.1 - y.2)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hf : HasStrictFDerivAt f f' x<VAR>hg : HasStrictFDerivAt g g' x<VAR>y : E × E<GOAL>f y.1 - f y.2 - (f' y.1 - f' y.2) + (g y.1 - g y.2 - (g' y.1 - g' y.2)) = f y.1 + g y.1 - (f y.2 + g y.2) - (f' y.1 + g' y.1 - (f' y.2 + g' y.2))
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>a : α<GOAL>Measurable ((fun p => κ.rnDeriv η p.1 p.2) ∘ fun x => (a, x))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hf : f.IsCycle<VAR>n : ℕ<GOAL>(f ^ n).support = f.support ↔ ¬orderOf f ∣ n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hf : f.IsCycle<VAR>n : ℕ<GOAL>(f ^ n).support = f.support ↔ ¬f ^ n = 1
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<VAR>x : ↑X.toTopCat<GOAL>r ∉ (X.toΓSpecFun x).asIdeal ↔ IsUnit ((X.presheaf.Γgerm x) r)
<VAR>k G✝ : Type u<VAR>inst✝² : CommRing k<VAR>inst✝¹ : Monoid G✝<VAR>G : Type u<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>g : G<VAR>x : CoeSort.coe A<GOAL>(A.ρ g⁻¹ * A.ρ g) x = x
<VAR>ι✝¹ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι✝ : Sort u_3<VAR>I✝ J B : Set α<VAR>f x y : α<VAR>ι : Type u_4<VAR>A : Set ι<VAR>hA : A.Nonempty<VAR>I : ι → Set α<VAR>h : M.Indep (⋃ i ∈ A, I i)<VAR>this : Nonempty ↑A<GOAL>M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)
<VAR>a x : ℝ<GOAL>↑(⋯.lift ↑a) = jacobiTheta₂ (↑a) (I * ↑x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>s✝ t : Set α<VAR>a b : α<VAR>inst✝ : Unique ι<VAR>s : ι → α<GOAL>⨆ i, s i = s default
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>s✝ t : Set α<VAR>a b : α<VAR>inst✝ : Unique ι<VAR>s : ι → α<VAR>this : ∀ (i : ι), s i = s default<GOAL>⨆ i, s i = s default
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : OrderedCancelAddCommMonoid α<VAR>inst✝² : ExistsAddOfLE α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<GOAL>image (fun x => x + c) (Ioo a b) = Ioo (a + c) (b + c)
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X✝ Y✝ Z X Y : C<GOAL>(λ_ X).hom ▷ Y = (α_ (𝟙_ C) X Y).hom ≫ (λ_ (X ⊗ Y)).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z✝ : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>X Y Z : C<VAR>P : Subobject Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : P.Factors g<GOAL>f ≫ P.factorThru g h = P.factorThru (f ≫ g) ⋯
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z✝ : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>X Y Z : C<VAR>P : Subobject Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : P.Factors g<GOAL>(f ≫ P.factorThru g h) ≫ P.arrow = P.factorThru (f ≫ g) ⋯ ≫ P.arrow
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>h : HasDerivAt f f' x<GOAL>HasFDerivAt f (f' • 1) x
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>hf : MonotoneOn f s<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : ℝ) ∂volume.restrict s, DifferentiableWithinAt ℝ f s x
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>hf : MonotoneOn f s<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
<VAR>x : ℝ<VAR>hx : Irrational x<VAR>n : ℕ<GOAL>∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑n)
<VAR>x : ℝ<VAR>hx : Irrational x<VAR>n : ℕ<VAR>A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)<GOAL>∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑n)
<VAR>x : ℝ<VAR>hx : Irrational x<VAR>n : ℕ<VAR>A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)<VAR>B : x ∉ range fun m => (↑n)⁻¹ * ↑m<GOAL>∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑n)
<VAR>x : ℝ<VAR>hx : Irrational x<VAR>n : ℕ<VAR>A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)<VAR>B : x ∉ range fun m => (↑n)⁻¹ * ↑m<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hε : ball x ε ⊆ (range fun m => (↑n)⁻¹ * ↑m)ᶜ<GOAL>∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑n)
<VAR>x : ℝ<VAR>hx : Irrational x<VAR>n : ℕ<VAR>A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)<VAR>B : x ∉ range fun m => (↑n)⁻¹ * ↑m<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hε : ball x ε ⊆ (range fun m => (↑n)⁻¹ * ↑m)ᶜ<VAR>δ : ℝ<VAR>hδ : δ ≤ ε<VAR>m : ℤ<VAR>hlt : dist x (↑m / ↑n) < δ<GOAL>False
<VAR>x : ℝ<VAR>hx : Irrational x<VAR>n : ℕ<VAR>A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)<VAR>B : x ∉ range fun m => (↑n)⁻¹ * ↑m<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hε : ball x ε ⊆ (range fun m => (↑n)⁻¹ * ↑m)ᶜ<VAR>δ : ℝ<VAR>hδ : δ ≤ ε<VAR>m : ℤ<VAR>hlt : dist (↑m / ↑n) x < δ<GOAL>False
<VAR>x : ℝ<VAR>hx : Irrational x<VAR>n : ℕ<VAR>A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)<VAR>B : x ∉ range fun m => (↑n)⁻¹ * ↑m<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hε : ball x ε ⊆ (range fun m => (↑n)⁻¹ * ↑m)ᶜ<VAR>δ : ℝ<VAR>hδ : δ ≤ ε<VAR>m : ℤ<VAR>hlt : dist (↑m / ↑n) x < δ<GOAL>(fun m => (↑n)⁻¹ * ↑m) m = ↑m / ↑n
<VAR>m n✝ : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>h : n = 0 → b = true<VAR>a✝ : n.bodd = n.bits.headI<GOAL>(bit b n).bodd = (bit b n).bits.headI
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : StrongRankCondition R<VAR>inst✝² : Module.Finite R M<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : Nontrivial R<VAR>V : ι → Submodule R M<VAR>hV : Independent V<VAR>I : Type w := { i // V i ≠ ⊥ }<GOAL>lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : StrongRankCondition R<VAR>inst✝² : Module.Finite R M<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : Nontrivial R<VAR>V : ι → Submodule R M<VAR>hV : Independent V<VAR>I : Type w := { i // V i ≠ ⊥ }<VAR>hI : ∀ (i : I), ∃ v ∈ V ↑i, v ≠ 0<GOAL>lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : StrongRankCondition R<VAR>inst✝² : Module.Finite R M<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : Nontrivial R<VAR>V : ι → Submodule R M<VAR>hV : Independent V<VAR>I : Type w := { i // V i ≠ ⊥ }<VAR>v : I → M<VAR>hvV : ∀ (i : I), v i ∈ V ↑i<VAR>hv : ∀ (i : I), v i ≠ 0<GOAL>lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : StrongRankCondition R<VAR>inst✝² : Module.Finite R M<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : Nontrivial R<VAR>V : ι → Submodule R M<VAR>hV : Independent V<VAR>I : Type w := { i // V i ≠ ⊥ }<VAR>v : I → M<VAR>hvV : ∀ (i : I), v i ∈ V ↑i<VAR>hv : ∀ (i : I), v i ≠ 0<VAR>this : LinearIndependent R v<GOAL>lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)
<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>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<GOAL>∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
<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>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<GOAL>∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<GOAL>𝓝[≠] ∞ = map some (coclosedCompact X)
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<GOAL>∀ (i : Set (OnePoint X)), ∞ ∈ i ∧ IsOpen i → ∃ i', (IsClosed i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ i ∩ {∞}ᶜ
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<GOAL>∀ (i' : Set X), IsClosed i' ∧ IsCompact i' → ∃ i, (∞ ∈ i ∧ IsOpen i) ∧ i ∩ {∞}ᶜ ⊆ some '' i'ᶜ
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>h𝒜₁ : 𝒜.Nonempty<VAR>h𝒜₂ : univ ∉ 𝒜<VAR>m : ℕ<VAR>hm : m = 𝒜.card<GOAL>supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>m : ℕ<VAR>ih : ∀ m_1 < m, ∀ {𝒜 : Finset (Finset α)}, 𝒜.Nonempty → univ ∉ 𝒜 → m_1 = 𝒜.card → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹<VAR>𝒜 : Finset (Finset α)<VAR>h𝒜₁ : 𝒜.Nonempty<VAR>h𝒜₂ : univ ∉ 𝒜<VAR>hm : m = 𝒜.card<GOAL>supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>m : ℕ<VAR>𝒜 : Finset (Finset α)<VAR>h𝒜₁ : 𝒜.Nonempty<VAR>h𝒜₂ : univ ∉ 𝒜<VAR>hm : m = 𝒜.card<VAR>ih : ∀ (𝒜 : Finset (Finset α)), 𝒜.card < m → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹<GOAL>supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>m : ℕ<VAR>ih : ∀ (𝒜 : Finset (Finset α)), 𝒜.card < m → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹<VAR>a : Finset α<VAR>h𝒜₁ : {a}.Nonempty<VAR>h𝒜₂ : univ ∉ {a}<VAR>hm : m = {a}.card<GOAL>supSum {a} = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>m : ℕ<VAR>𝒜 : Finset (Finset α)<VAR>h𝒜₁ : 𝒜.Nonempty<VAR>h𝒜₂ : univ ∉ 𝒜<VAR>hm : m = 𝒜.card<VAR>ih : ∀ (𝒜 : Finset (Finset α)), 𝒜.card < m → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹<VAR>h𝒜₃ : 𝒜.Nontrivial<GOAL>supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>𝒜 : Finset (Finset α)<VAR>h𝒜₁ : 𝒜.Nonempty<VAR>h𝒜₂ : univ ∉ 𝒜<VAR>h𝒜₃ : 𝒜.Nontrivial<VAR>n✝ : ℕ<VAR>hm : n✝ + 1 = 𝒜.card<VAR>ih : ∀ (𝒜 : Finset (Finset α)), 𝒜.card < n✝ + 1 → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹<GOAL>supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>inst✝ : Nonempty α<VAR>s : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>hs : s ∉ 𝒜<VAR>h𝒜₁ : (insert s 𝒜).Nonempty<VAR>h𝒜₂ : univ ∉ insert s 𝒜<VAR>h𝒜₃ : (insert s 𝒜).Nontrivial<VAR>ih : ∀ (𝒜_1 : Finset (Finset α)), 𝒜_1.card < 𝒜.card + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹<VAR>hm : 𝒜.card + 1 = (insert s 𝒜).card<GOAL>supSum (insert s 𝒜) = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>inst✝ : Nonempty α<VAR>s : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>hs : s ∉ 𝒜<VAR>h𝒜₁ : (insert s 𝒜).Nonempty<VAR>h𝒜₂ : univ ∉ insert s 𝒜<VAR>h𝒜₃ : (insert s 𝒜).Nontrivial<VAR>ih : ∀ (𝒜_1 : Finset (Finset α)), 𝒜_1.card < 𝒜.card + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹<VAR>hm : 𝒜.card + 1 = (insert s 𝒜).card<VAR>h𝒜 : 𝒜.Nonempty<GOAL>supSum (insert s 𝒜) = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>inst✝ : Nonempty α<VAR>s : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>hs : s ∉ 𝒜<VAR>h𝒜₁ : (insert s 𝒜).Nonempty<VAR>h𝒜₂ : univ ∉ insert s 𝒜<VAR>h𝒜₃ : (insert s 𝒜).Nontrivial<VAR>ih : ∀ (𝒜_1 : Finset (Finset α)), 𝒜_1.card < 𝒜.card + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹<VAR>hm : 𝒜.card + 1 = (insert s 𝒜).card<VAR>h𝒜 : 𝒜.Nonempty<GOAL>(image (fun x => s ⊓ x) 𝒜).card < 𝒜.card + 1