ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>r : ℝ<GOAL>↑hA.eigenvectorUnitary * ((diagonal fun x => ↑r) * star ↑hA.eigenvectorUnitary) = ↑hA.eigenvectorUnitary * ((algebraMap ℝ (Matrix n n 𝕜)) r * star ↑hA.eigenvectorUnitary)
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>f : C(↑(spectrum ℝ A), ℝ)<GOAL>(↑↑{ toFun := fun g => ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑g ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }.toRingHom).toFun (star f) = star ((↑↑{ toFun := fun g => ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑g ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }.toRingHom).toFun f)
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>f : C(↑(spectrum ℝ A), ℝ)<GOAL>↑hA.eigenvectorUnitary * (diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary) = ↑hA.eigenvectorUnitary * (diagonal (star (RCLike.ofReal ∘ ⇑f ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩)) * star ↑hA.eigenvectorUnitary)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>val✝ : Multiset α<VAR>l : List α<VAR>hs : Multiset.Nodup (Quot.mk Setoid.r l)<GOAL>(permsOfFinset { val := Quot.mk Setoid.r l, nodup := hs }).card = { val := Quot.mk Setoid.r l, nodup := hs }.card !
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<VAR>hf : Injective f<GOAL>f a ∈ image f s ↔ a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<VAR>hf : Injective f<VAR>h : f a ∈ image f s<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<VAR>hf : Injective f<VAR>h : f a ∈ image f s<VAR>y : α<VAR>hy : y ∈ s<VAR>heq : f y = f a<GOAL>a ∈ s
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : X.Opens<VAR>s : Set ↑Γ(X, U)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<GOAL>IsAffineOpen U
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : X.Opens<VAR>s : Set ↑Γ(X, U)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<GOAL>Ideal.span (⇑U.topIso.inv '' s) = ⊤
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : X.Opens<VAR>s : Set ↑Γ(X, U)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<GOAL>∀ i ∈ ⇑U.topIso.inv '' s, IsAffineOpen ((↑U).basicOpen i)
<GOAL>Real.toEReal ⁻¹' Ioo ⊥ ⊤ = univ
<GOAL>Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iio ⊤) = univ
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q✝ r : R[X]<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>x : S<VAR>q : R[X]<VAR>hp : eval₂ f x p = 0<GOAL>eval₂ f x (p * q) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q✝ r : R[X]<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>x : S<VAR>q : R[X]<VAR>hp : eval₂ f x p = 0<GOAL>eval₂ f x p * eval₂ f x q = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group H<VAR>inst✝¹ : MulAction G α<VAR>a : G<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>a ∈ stabilizer G s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group H<VAR>inst✝¹ : MulAction G α<VAR>a : G<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>s ⊆ a⁻¹ • s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s
<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✝⁶ : StrictOrderedCommRing 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>p₁ p₂ x : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>t : R<VAR>ht : t ≤ 0<GOAL>SameRay R (t • (x -ᵥ p₁) +ᵥ p₂ -ᵥ p₂) (p₁ -ᵥ x)
<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✝⁶ : StrictOrderedCommRing 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>p₁ p₂ x : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>t : R<VAR>ht : t ≤ 0<GOAL>SameRay R (-t • (p₁ -ᵥ x)) (p₁ -ᵥ x)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>s : Set (CofiniteTopology X)<GOAL>IsClosed s ↔ s = univ ∨ s.Finite
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝⁸ : (i : ι) → Module R (M i)<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>β : ι → Type u_6<VAR>β₁ : ι → Type u_7<VAR>β₂ : ι → Type u_8<VAR>inst✝⁵ : (i : ι) → AddCommMonoid (β i)<VAR>inst✝⁴ : (i : ι) → AddCommMonoid (β₁ i)<VAR>inst✝³ : (i : ι) → AddCommMonoid (β₂ i)<VAR>inst✝² : (i : ι) → Module R (β i)<VAR>inst✝¹ : (i : ι) → Module R (β₁ i)<VAR>inst✝ : (i : ι) → Module R (β₂ i)<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>r : R<VAR>hf' : ∀ (i : ι) (x : β₁ i), f i (r • x) = r • f i x<VAR>g : Π₀ (i : ι), β₁ i<VAR>i✝ : ι<GOAL>(mapRange f hf (r • g)) i✝ = (r • mapRange f hf g) i✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set β<GOAL>f '' (f ⁻¹' s)ᶜ = range f \ s
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a b c : G₀<VAR>ha : a ≠ 0<VAR>n : ℤ<GOAL>a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a b c : G₀<VAR>ha : a ≠ 0<VAR>n : ℤ<GOAL>a ^ (n - 1) * a * a⁻¹ = a ^ n * a⁻¹
<VAR>α : Type u_1<VAR>inst✝ : StrictOrderedSemiring α<VAR>x : ↑(Ioc 0 1)<GOAL>x = 1 ↔ ↑x = 1
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝¹ : AddGroup G<VAR>inst✝ : AddTorsor G P<VAR>x y : P<VAR>h : Injective fun x => 2 • x<GOAL>(pointReflection x) y = y ↔ y = x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>h : ∀ (a : Pseudoelement P), pseudoApply f a = 0<GOAL>f = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>h : ∀ (a : Pseudoelement P), pseudoApply f a = 0<GOAL>𝟙 P ≫ f = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t✝ u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<GOAL>(s ∩ t).card + (s \ t).card = s.card
<VAR>l r : List Char<GOAL>ValidFor l.reverse r { s := { data := l ++ r }, i := { byteIdx := utf8ByteSize.go l } }
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : NoZeroDivisors R<VAR>P : Fin 3 → R<VAR>hP : W'.Nonsingular P<VAR>hPz : P z = 0<VAR>hPx : P x = 0<GOAL>False
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : NoZeroDivisors R<VAR>P : Fin 3 → R<VAR>hPz : P z = 0<VAR>hPx : P x = 0<VAR>hP : P y ^ 2 = 0 ∧ 2 * P y ≠ 0<GOAL>False
<VAR>𝕜 : Type u<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>inst✝⁴ : StarRing 𝕜<VAR>inst✝³ : TrivialStar 𝕜<VAR>inst✝² : StarAddMonoid F<VAR>inst✝¹ : ContinuousStar F<VAR>inst✝ : StarModule 𝕜 F<VAR>f' : F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>h : HasDerivAtFilter f f' x L<GOAL>HasDerivAtFilter (fun x => star (f x)) (star f') x L
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>((IntFractPair.stream v n).bind fun ap_n => if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹)) = none ↔ IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>s : Submodule K V<VAR>inst✝ : Module.Free K ↥s<GOAL>Module.rank K ↥s = 1 ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ s ≤ span K {v₀}
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>s : Submodule K V<VAR>inst✝ : Module.Free K ↥s<GOAL>(∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v) ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ r, r • v₀ = v
<VAR>α : Type u_1<VAR>r c✝ : ℝ<VAR>l : Filter α<VAR>f g : α → ℝ<VAR>hr : 0 < r<VAR>hg : 0 ≤ᶠ[l] g<VAR>h : f =o[l] g<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>IsBigOWith c l (fun x => f x ^ r) fun x => g x ^ r
<VAR>α : Type u_1<VAR>r c✝ : ℝ<VAR>l : Filter α<VAR>f g : α → ℝ<VAR>hr : 0 < r<VAR>hg : 0 ≤ᶠ[l] g<VAR>h : f =o[l] g<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>IsBigOWith ((c ^ r⁻¹) ^ r) l (fun x => f x ^ r) fun x => g x ^ r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n : ι<GOAL>gramSchmidt 𝕜 f n = f n - ∑ i ∈ Iio n, ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i})) (f n))
<VAR>x : Cardinal.{v}<VAR>m : ℕ∞<GOAL>↑m ≤ lift.{u, v} x ↔ ↑m ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>C : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C<GOAL>∫⁻ (x : α), f x ∂μ ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>C : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C<VAR>this : ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ<GOAL>∫⁻ (x : α), f x ∂μ ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>C : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C<VAR>this : ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ<GOAL>∫⁻ (x : α) in univ, f x ∂μ ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>C : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C<VAR>this : ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ<VAR>S : ℕ → Set α<VAR>x✝ : ∀ (n : ℕ), MeasurableSet (S n)<VAR>hS_mono : Monotone S<GOAL>∫⁻ (x : α) in ⋃ n, S n, f x ∂μ ≤ ⨆ n, ∫⁻ (x : α) in S n, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>C : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C<VAR>this : ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ<VAR>S : ℕ → Set α<VAR>x✝ : ∀ (n : ℕ), MeasurableSet (S n)<VAR>hS_mono : Monotone S<GOAL>Directed (fun x x_1 => x ⊆ x_1) S
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g volume t₁ t₂<VAR>h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x<VAR>hT : 0 < T<GOAL>Tendsto (fun t => ∫ (x : ℝ) in 0 ..t, g x) atTop atTop
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g volume t₁ t₂<VAR>h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x<VAR>hT : 0 < T<GOAL>Tendsto (fun n => sInf ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊n / T⌋ • ∫ (x : ℝ) in 0 ..T, g x) atTop atTop
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g volume t₁ t₂<VAR>h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x<VAR>hT : 0 < T<GOAL>Tendsto (fun x => ⌊x / T⌋ • ∫ (x : ℝ) in 0 ..T, g x) atTop atTop
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g volume t₁ t₂<VAR>h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x<VAR>hT : 0 < T<GOAL>Tendsto (fun x => ⌊x / T⌋) atTop atTop
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<GOAL>IsRegular (X n)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<GOAL>IsLeftRegular (X n)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q P Q : MvPolynomial σ R<VAR>hPQ : X n * P = X n * Q<VAR>i : σ →₀ ℕ<GOAL>coeff i P = coeff i Q
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : α → β<VAR>ι : Sort u_2<VAR>t : TopologicalSpace α<VAR>b : Set (Set β)<GOAL>Continuous f ↔ ∀ s ∈ b, IsOpen (f ⁻¹' s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : α → β<VAR>ι : Sort u_2<VAR>t : TopologicalSpace α<VAR>b : Set (Set β)<GOAL>b ⊆ {s | IsOpen s} ↔ ∀ s ∈ b, IsOpen (f ⁻¹' s)
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>x : M<GOAL>(contractRight ((ι Q) x)) d = (algebraMap R (CliffordAlgebra Q)) (d x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<GOAL>‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<VAR>h : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖<GOAL>‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>F : Presheaf C Y<VAR>V : (Opens ↑Y)ᵒᵖ<VAR>x : ↥((Opens.map f).obj (unop V))<GOAL>((pushforwardPullbackAdjunction C f).unit.app F).app V ≫ germToPullbackStalk C f F ((Opens.map f).obj (unop V)) x = F.germ ⟨f ↑x, ⋯⟩
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>Icc a b = 0 ↔ ¬a ≤ b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>s t : Set X<VAR>inst✝ : NormalSpace X<VAR>st_dis : Disjoint s t<VAR>t_cl : IsClosed t<VAR>T : Set (Set X)<VAR>T_open : ∀ t ∈ T, IsOpen t<VAR>T_count : T.Countable<VAR>T_int : t = ⋂₀ T<GOAL>HasSeparatingCover s t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>s t : Set X<VAR>inst✝ : NormalSpace X<VAR>st_dis : Disjoint s t<VAR>t_cl : IsClosed t<VAR>T_open : ∀ t ∈ ∅, IsOpen t<VAR>T_count : ∅.Countable<VAR>T_int : t = ⋂₀ ∅<GOAL>HasSeparatingCover s t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>s t : Set X<VAR>inst✝ : NormalSpace X<VAR>st_dis : Disjoint s t<VAR>t_cl : IsClosed t<VAR>T : Set (Set X)<VAR>T_open : ∀ t ∈ T, IsOpen t<VAR>T_count : T.Countable<VAR>T_int : t = ⋂₀ T<VAR>T_nonempty : T.Nonempty<GOAL>HasSeparatingCover s t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>s t : Set X<VAR>inst✝ : NormalSpace X<VAR>st_dis : Disjoint s t<VAR>t_cl : IsClosed t<VAR>T : Set (Set X)<VAR>T_open : ∀ t ∈ T, IsOpen t<VAR>T_count : T.Countable<VAR>T_int : t = ⋂₀ T<VAR>T_nonempty : T.Nonempty<VAR>g : ℕ → ↑T<VAR>g_surj : Surjective g<GOAL>HasSeparatingCover s t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>s t : Set X<VAR>inst✝ : NormalSpace X<VAR>st_dis : Disjoint s t<VAR>t_cl : IsClosed t<VAR>T : Set (Set X)<VAR>T_open : ∀ t ∈ T, IsOpen t<VAR>T_count : T.Countable<VAR>T_int : t = ⋂₀ T<VAR>T_nonempty : T.Nonempty<VAR>g : ℕ → ↑T<VAR>g_surj : Surjective g<VAR>g' : ℕ → Set X<VAR>g'_open : ∀ (n : ℕ), IsOpen (g' n)<VAR>clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n<VAR>clg'_sub_g : ∀ (n : ℕ), closure (g' n) ⊆ ↑(g n)<GOAL>HasSeparatingCover s t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>s t : Set X<VAR>inst✝ : NormalSpace X<VAR>st_dis : Disjoint s t<VAR>t_cl : IsClosed t<VAR>T : Set (Set X)<VAR>T_open : ∀ t ∈ T, IsOpen t<VAR>T_count : T.Countable<VAR>T_int : t = ⋂₀ T<VAR>T_nonempty : T.Nonempty<VAR>g : ℕ → ↑T<VAR>g_surj : Surjective g<VAR>g' : ℕ → Set X<VAR>g'_open : ∀ (n : ℕ), IsOpen (g' n)<VAR>clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n<VAR>clg'_sub_g : ∀ (n : ℕ), closure (g' n) ⊆ ↑(g n)<VAR>clg'_int : t = ⋂ i, closure (g' i)<GOAL>HasSeparatingCover s t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>s t : Set X<VAR>inst✝ : NormalSpace X<VAR>st_dis : Disjoint s t<VAR>t_cl : IsClosed t<VAR>T : Set (Set X)<VAR>T_open : ∀ t ∈ T, IsOpen t<VAR>T_count : T.Countable<VAR>T_int : t = ⋂₀ T<VAR>T_nonempty : T.Nonempty<VAR>g : ℕ → ↑T<VAR>g_surj : Surjective g<VAR>g' : ℕ → Set X<VAR>g'_open : ∀ (n : ℕ), IsOpen (g' n)<VAR>clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n<VAR>clg'_sub_g : ∀ (n : ℕ), closure (g' n) ⊆ ↑(g n)<VAR>clg'_int : t = ⋂ i, closure (g' i)<GOAL>s ⊆ ⋃ n, (closure (g' n))ᶜ ∧ ∀ (n : ℕ), IsOpen (closure (g' n))ᶜ ∧ Disjoint (closure (closure (g' n))ᶜ) t
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m✝ m : OuterMeasure α<VAR>m0 m1 : MeasurableSpace α<VAR>h : m0 ≤ m1<GOAL>m.trim ≤ m.trim
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m✝ m : OuterMeasure α<VAR>m0 m1 : MeasurableSpace α<VAR>h : m0 ≤ m1<GOAL>∀ (s : Set α), MeasurableSet s → m.trim s ≤ m s
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m✝ m : OuterMeasure α<VAR>m0 m1 : MeasurableSpace α<VAR>h : m0 ≤ m1<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>m.trim s ≤ m s
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>a b : α<VAR>C : α → Sort u_2<VAR>inst✝ : WellFoundedLT α<VAR>H_succ : (a : α) → ¬IsMax a → C a → C (succ a)<VAR>H_lim : (a : α) → IsSuccLimit a → ((b : α) → b < a → C b) → C a<VAR>ha : IsSuccLimit a<GOAL>SuccOrder.limitRecOn a H_succ H_lim = H_lim a ha fun x x_1 => SuccOrder.limitRecOn x H_succ H_lim
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>a b : α<VAR>C : α → Sort u_2<VAR>inst✝ : WellFoundedLT α<VAR>H_succ : (a : α) → ¬IsMax a → C a → C (succ a)<VAR>H_lim : (a : α) → IsSuccLimit a → ((b : α) → b < a → C b) → C a<VAR>ha : IsSuccLimit a<GOAL>(H_lim a ha fun y x => ⋯.fix (fun a IH => if h : IsSuccLimit a then H_lim a h IH else let x := Classical.indefiniteDescription (fun x => ¬IsMax x ∧ succ x = a) ⋯; ⋯ ▸ H_succ ↑x ⋯ (IH ↑x ⋯)) y) = H_lim a ha fun x x_1 => SuccOrder.limitRecOn x H_succ H_lim
<VAR>h : Decidable (Dom 0)<GOAL>toWithTop 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<VAR>h : G ≤ H<GOAL>G.IsNClique n s → H.IsNClique n s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<VAR>h : G ≤ H<GOAL>G.IsClique ↑s ∧ s.card = n → H.IsClique ↑s ∧ s.card = n
<VAR>m k n : ℕ<GOAL>(n ∈ Set.range fun n => m * n + k) ↔ n ∈ {n | ↑n = ↑k ∧ k ≤ n}
<VAR>m k n : ℕ<GOAL>(∃ y, m * y + k = n) ↔ ↑n = ↑k ∧ k ≤ n
<VAR>m k n : ℕ<GOAL>(∃ y, n = k + m * y) ↔ ↑n = ↑k ∧ k ≤ n
<VAR>m k n : ℕ<VAR>x✝ : ∃ y, n = k + m * y<VAR>a : ℕ<VAR>ha : n = k + m * a<GOAL>↑n = ↑k
<VAR>m k n : ℕ<VAR>x✝ : ↑n = ↑k ∧ k ≤ n<VAR>H₁ : ↑n = ↑k<VAR>H₂ : k ≤ n<GOAL>∃ y, n = k + m * y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Sort u_5<VAR>f : ι → α → ℝ≥0∞<GOAL>∫⁻ (a : α), ⨅ i, f i a ∂μ ≤ ⨅ i, ∫⁻ (a : α), f i a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Sort u_5<VAR>f : ι → α → ℝ≥0∞<GOAL>∫⁻ (a : α), (⨅ i, f i) a ∂μ ≤ ⨅ i, ∫⁻ (a : α), f i a ∂μ
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>χ₁ : L → R<VAR>a✝ : χ₁ ∈ {χ | weightSpace M χ ≠ ⊥}<VAR>χ₂ : L → R<VAR>hχ₂ : χ₂ ∈ {χ | weightSpace M χ ≠ ⊥}<VAR>hχ₁₂ : weightSpace M χ₁ = weightSpace M χ₂<GOAL>χ₁ = χ₂
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>χ₁ : L → R<VAR>a✝ : χ₁ ∈ {χ | weightSpace M χ ≠ ⊥}<VAR>χ₂ : L → R<VAR>hχ₁₂ : weightSpace M χ₁ = weightSpace M χ₂<VAR>hχ₂ : χ₁ ≠ χ₂<GOAL>χ₂ ∉ {χ | weightSpace M χ ≠ ⊥}
<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>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>fract 0 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>normSq (⟪x, y⟫_𝕜 • x - ⟪x, x⟫_𝕜 • y) = normSq x * (normSq x * normSq y - ‖⟪x, y⟫_𝕜‖ ^ 2)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>⟪⟪x, y⟫_𝕜 • x - ⟪x, x⟫_𝕜 • y, ⟪x, y⟫_𝕜 • x - ⟪x, x⟫_𝕜 • y⟫_𝕜 = ↑(normSq x * (normSq x * normSq y - ‖⟪x, y⟫_𝕜‖ ^ 2))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>⟪x, y⟫_𝕜 * ((starRingEnd 𝕜) ⟪x, y⟫_𝕜 * ↑(normSq x)) - ↑(normSq x) * ((starRingEnd 𝕜) ⟪x, y⟫_𝕜 * ⟪x, y⟫_𝕜) - ⟪x, y⟫_𝕜 * (↑(normSq x) * ⟪y, x⟫_𝕜) + ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) = ↑(normSq x * (normSq x * normSq y) - normSq x * ‖⟪x, y⟫_𝕜‖ ^ 2)