ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c✝ : F<VAR>b : E × F → G<VAR>m✝ n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>c : F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>m : Fin (n + 1) → E<GOAL>(0 (init m)) (m (last n)) = 0 m
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s : Set P<VAR>h : affineSpan k s = ⊤<GOAL>vectorSpan k s = ⊤
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : C(X, Y)<VAR>hf : QuotientMap ⇑f<VAR>g✝ : C(X, Z)<VAR>h✝ : FactorsThrough ⇑g✝ ⇑f<VAR>g : C(Y, Z)<VAR>x✝¹ x✝ : X<VAR>h : f x✝¹ = f x✝<GOAL>(g.comp f) x✝¹ = (g.comp f) x✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : C(X, Y)<VAR>hf : QuotientMap ⇑f<VAR>g✝ : C(X, Z)<VAR>h✝ : FactorsThrough ⇑g✝ ⇑f<VAR>g : C(Y, Z)<VAR>x✝¹ x✝ : X<VAR>h : f x✝¹ = f x✝<GOAL>g (f x✝¹) = g (f x✝)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : C(X, Y)<VAR>hf : QuotientMap ⇑f<VAR>g✝ : C(X, Z)<VAR>h : FactorsThrough ⇑g✝ ⇑f<VAR>g : C(Y, Z)<VAR>a : Y<GOAL>((fun g => hf.lift ↑g ⋯) ((fun g => ⟨g.comp f, ⋯⟩) g)) a = g a
<VAR>x✝ y z x : ℝ<GOAL>x ^ 0 = 1
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<GOAL>Tendsto (fun n => (⇑↑(translate (Multiplicative.ofAdd x)))^[n + 1] 0 / (↑n + 1)) atTop (𝓝 x)
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : SeminormedAddCommGroup V<VAR>inst✝⁷ : PseudoMetricSpace P<VAR>inst✝⁶ : NormedAddTorsor V P<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : MetricSpace Q<VAR>inst✝³ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<VAR>p q : P<GOAL>dist ((Equiv.pointReflection p) q) q = ‖2‖ * dist p q
<VAR>x y r r' : ℕ<GOAL>∀ {s t s' t' : ℤ}, Nat.P x y (r, s, t) → Nat.P x y (r', s', t') → Nat.P x y (r.xgcdAux s t r' s' t')
<VAR>α : Type u<VAR>β✝ : Type v<VAR>m : Type u → Type v<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>β : Type u<VAR>f : ℕ → β → α → m β<VAR>b : β<VAR>as : List α<GOAL>foldlIdxM f b as = List.foldlM (fun b p => f p.1 b p.2) b as.enum
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<GOAL>(ae μ)⁻¹ = ae μ
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<GOAL>ae μ ≤ (ae μ)⁻¹
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<GOAL>(ae μ)⁻¹⁻¹ ≤ (ae μ)⁻¹
<VAR>L : Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>inst✝ : L.Structure Q<VAR>f : M ↪ₑ[L] N<VAR>α : Type u_5<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : α → M<VAR>xs : Fin n → M<GOAL>φ.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ.Realize v xs
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>x y : α<VAR>h : x ≠ y<GOAL>{x, y} = [x, y]
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>x y : α<VAR>h : x ≠ y<GOAL>¬x ∈ {y}
<VAR>x y : ℝ≥0<GOAL>sqrt x ≤ 1 ↔ x ≤ 1
<GOAL>γ = -(↑0! * (-γ + ↑(harmonic 0)))
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝⁹ : CommSemiring R<VAR>A✝ : Type v<VAR>inst✝⁸ : Semiring A✝<VAR>inst✝⁷ : Algebra R A✝<VAR>S T : Set A✝<VAR>M N P Q : Submodule R A✝<VAR>m n : A✝<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>inst✝⁶ : CommSemiring A<VAR>inst✝⁵ : CommSemiring B<VAR>inst✝⁴ : Semiring C<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : Algebra B C<VAR>inst✝ : IsScalarTower A B C<VAR>I J : Submodule B C<GOAL>restrictScalars A (I * J) = restrictScalars A I * restrictScalars A J
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝⁹ : CommSemiring R<VAR>A✝ : Type v<VAR>inst✝⁸ : Semiring A✝<VAR>inst✝⁷ : Algebra R A✝<VAR>S T : Set A✝<VAR>M N P Q : Submodule R A✝<VAR>m n : A✝<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>inst✝⁶ : CommSemiring A<VAR>inst✝⁵ : CommSemiring B<VAR>inst✝⁴ : Semiring C<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : Algebra B C<VAR>inst✝ : IsScalarTower A B C<VAR>I J : Submodule B C<GOAL>restrictScalars A (I * J) ≤ restrictScalars A I * restrictScalars A J
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝⁹ : CommSemiring R<VAR>A✝ : Type v<VAR>inst✝⁸ : Semiring A✝<VAR>inst✝⁷ : Algebra R A✝<VAR>S T : Set A✝<VAR>M N P Q : Submodule R A✝<VAR>m n : A✝<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>inst✝⁶ : CommSemiring A<VAR>inst✝⁵ : CommSemiring B<VAR>inst✝⁴ : Semiring C<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : Algebra B C<VAR>inst✝ : IsScalarTower A B C<VAR>I J : Submodule B C<GOAL>restrictScalars A I * restrictScalars A J ≤ restrictScalars A (I * J)
<VAR>a : UnitAddCircle<GOAL>ContinuousOn (evenKernel a) (Ioi 0)
<VAR>a' : ℝ<GOAL>ContinuousOn (evenKernel ↑a') (Ioi 0)
<VAR>a' : ℝ<GOAL>ContinuousOn (fun x => ↑(evenKernel (↑a') x)) (Ioi 0)
<VAR>a' : ℝ<GOAL>ContinuousOn (fun x => cexp (-↑π * ↑a' ^ 2 * ↑x) * jacobiTheta₂ (↑a' * I * ↑x) (I * ↑x)) (Ioi 0)
<VAR>a' x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>Continuous fun x => cexp (-↑π * ↑a' ^ 2 * ↑x)
<VAR>a' x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>ContinuousAt (fun x => jacobiTheta₂ (↑a' * I * ↑x) (I * ↑x)) x
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝⁴ : MulOneClass α<VAR>inst✝³ : Zero α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : PosMulMono α<VAR>inst✝ : PosMulReflectLE α<VAR>a0 : 0 < a<GOAL>a ≤ a * b ↔ a * 1 ≤ a * b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : MonoidHomClass F α β<VAR>t : Multiset ι<VAR>f : ι → Set α<VAR>g : ι → α<VAR>hg : ∀ i ∈ t, g i ∈ f i<GOAL>(Multiset.map g t).prod ∈ (Multiset.map f t).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : MonoidHomClass F α β<VAR>f : ι → Set α<VAR>g : ι → α<VAR>a✝ : List ι<VAR>hg : ∀ i ∈ ⟦a✝⟧, g i ∈ f i<GOAL>(Multiset.map g ⟦a✝⟧).prod ∈ (Multiset.map f ⟦a✝⟧).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : MonoidHomClass F α β<VAR>f : ι → Set α<VAR>g : ι → α<VAR>a✝ : List ι<VAR>hg : ∀ i ∈ ⟦a✝⟧, g i ∈ f i<GOAL>(List.map g a✝).prod ∈ (List.map f a✝).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g✝ : Filter β<VAR>f : Filter α<VAR>g : Filter β<VAR>inst✝ : f.NeBot<GOAL>map Prod.snd (f ×ˢ g) = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g✝ : Filter β<VAR>f : Filter α<VAR>g : Filter β<VAR>inst✝ : f.NeBot<GOAL>map (Prod.snd ∘ fun p => (p.2, p.1)) (g ×ˢ f) = g
<VAR>P : Type u_1<VAR>inst✝ : DistribLattice P<VAR>I J : Ideal P<VAR>x i j : P<VAR>hi : i ∈ I<VAR>hj : j ∈ J<VAR>hx : x ≤ i ⊔ j<GOAL>∃ i' ∈ I, ∃ j' ∈ J, x = i' ⊔ j'
<VAR>P : Type u_1<VAR>inst✝ : DistribLattice P<VAR>I J : Ideal P<VAR>x i j : P<VAR>hi : i ∈ I<VAR>hj : j ∈ J<VAR>hx : x ≤ i ⊔ j<GOAL>x = x ⊓ i ⊔ x ⊓ j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<GOAL>∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<GOAL>∫⁻ (a : α), (⨆ i, f i) a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x<VAR>h_ae_seq_mono : Monotone (aeSeq hf p)<GOAL>∫⁻ (a : α), (⨆ i, f i) a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x<VAR>h_ae_seq_mono : Monotone (aeSeq hf p)<GOAL>∫⁻ (a : α), (⨆ n, aeSeq hf p n) a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x<VAR>h_ae_seq_mono : Monotone (aeSeq hf p)<GOAL>∫⁻ (a : α), ⨆ i, aeSeq hf p i a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x<VAR>h_ae_seq_mono : Monotone (aeSeq hf p)<GOAL>⨆ n, ∫⁻ (a : α), aeSeq hf p n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x<VAR>h_ae_seq_mono : Monotone (aeSeq hf p)<VAR>n : ℕ<GOAL>∫⁻ (a : α), aeSeq hf p n a ∂μ = ∫⁻ (a : α), f n a ∂μ
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype o<VAR>inst✝ : CommRing R<VAR>A : Matrix m n R<GOAL>A.rank = finrank R ↥(Submodule.span R (Set.range Aᵀ))
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalRing R<VAR>J : Ideal R<VAR>h : IsAdic J<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>IsAdic (J ^ n)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalRing R<VAR>J : Ideal R<VAR>h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(∀ (n_1 : ℕ), IsOpen ↑((J ^ n) ^ n_1)) ∧ ∀ s ∈ 𝓝 0, ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ s
<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<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>a : R<GOAL>eval₂ f g (C a) = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f fab : α → β<VAR>fbc : β → γ<VAR>ga ga' : α → α<VAR>gb gb' : β → β<VAR>gc gc' : γ → γ<VAR>h : Semiconj f ga gb<VAR>h' : Semiconj f ga' gb'<VAR>x : α<GOAL>f ((ga ∘ ga') x) = (gb ∘ gb') (f x)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G₀ : Type u_4<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : GroupWithZero G₀<VAR>inst✝⁷ : MulAction G₀ α<VAR>inst✝⁶ : ContinuousConstSMul G₀ α<VAR>inst✝⁵ : TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>c✝ : G₀<VAR>s : Set β<VAR>E : Type u_5<VAR>inst✝⁴ : Zero E<VAR>inst✝³ : MulActionWithZero G₀ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : T1Space E<VAR>inst✝ : ContinuousConstSMul G₀ E<VAR>c : G₀<GOAL>IsClosedMap fun x => c • x
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G₀ : Type u_4<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : GroupWithZero G₀<VAR>inst✝⁷ : MulAction G₀ α<VAR>inst✝⁶ : ContinuousConstSMul G₀ α<VAR>inst✝⁵ : TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>c : G₀<VAR>s : Set β<VAR>E : Type u_5<VAR>inst✝⁴ : Zero E<VAR>inst✝³ : MulActionWithZero G₀ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : T1Space E<VAR>inst✝ : ContinuousConstSMul G₀ E<GOAL>IsClosedMap fun x => 0 • x
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G₀ : Type u_4<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : GroupWithZero G₀<VAR>inst✝⁷ : MulAction G₀ α<VAR>inst✝⁶ : ContinuousConstSMul G₀ α<VAR>inst✝⁵ : TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>c✝ : G₀<VAR>s : Set β<VAR>E : Type u_5<VAR>inst✝⁴ : Zero E<VAR>inst✝³ : MulActionWithZero G₀ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : T1Space E<VAR>inst✝ : ContinuousConstSMul G₀ E<VAR>c : G₀<VAR>hne : c ≠ 0<GOAL>IsClosedMap fun x => c • x
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ ≠ 0<GOAL>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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ ≠ 0<GOAL>p₃ -ᵥ p₂ ≠ 0
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (inr ()) (inr ()) ≠ 0<VAR>L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) := List.ofFn fun i => { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }<VAR>L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) := List.ofFn fun i => { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }<VAR>A : List.map toMatrix L = listTransvecCol M<VAR>B : List.map toMatrix L' = listTransvecRow M<GOAL>((listTransvecCol M).prod * M * (listTransvecRow M).prod).IsTwoBlockDiagonal
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<GOAL>rootOfSplitsXPowSubC hn a L ^ n = (algebraMap K L) a
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>this : ∀ (hfd : (X ^ n - C a).degree ≠ 0), eval₂ (algebraMap K L) (rootOfSplits (algebraMap K L) ⋯ hfd) (X ^ n - C a) = 0<GOAL>rootOfSplitsXPowSubC hn a L ^ n = (algebraMap K L) a
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>this : ∀ (hfd : (X ^ n - C a).degree ≠ 0), rootOfSplits (algebraMap K L) ⋯ hfd ^ n = (algebraMap K L) a<GOAL>rootOfSplitsXPowSubC hn a L ^ n = (algebraMap K L) a
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>l : List α<GOAL>[].diff l = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0∞<GOAL>Tendsto (fun n => r ^ n) atTop (𝓝 0) ↔ r < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0∞<VAR>h : Tendsto (fun n => r ^ n) atTop (𝓝 0)<GOAL>r < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0<VAR>h : Tendsto (fun n => ↑r ^ n) atTop (𝓝 0)<GOAL>↑r < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0<VAR>h : Tendsto (fun n => ↑r ^ n) atTop (𝓝 ↑0)<GOAL>↑r < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0<VAR>h : Tendsto (HPow.hPow r) atTop (𝓝 0)<GOAL>r < 1
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfi : IntegrableOn f s μ<VAR>hg : StronglyMeasurable g<VAR>hgi : IntegrableOn g s μ<VAR>hgf : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>∫ (x : α) in s, ‖g x‖ ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ∂μ
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfi : IntegrableOn f s μ<VAR>hg : StronglyMeasurable g<VAR>hgi : IntegrableOn g s μ<VAR>hgf : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>∫ (x : α) in {x | 0 ≤ g x}, g x ∂μ.restrict s - ∫ (x : α) in {x | g x ≤ 0}, g x ∂μ.restrict s ≤ ∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ.restrict s - ∫ (x : α) in {x | f x ≤ 0}, f x ∂μ.restrict s
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfi : IntegrableOn f s μ<VAR>hg : StronglyMeasurable g<VAR>hgi : IntegrableOn g s μ<VAR>hgf : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}<GOAL>∫ (x : α) in {x | 0 ≤ g x}, g x ∂μ.restrict s - ∫ (x : α) in {x | g x ≤ 0}, g x ∂μ.restrict s ≤ ∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ.restrict s - ∫ (x : α) in {x | f x ≤ 0}, f x ∂μ.restrict s
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfi : IntegrableOn f s μ<VAR>hg : StronglyMeasurable g<VAR>hgi : IntegrableOn g s μ<VAR>hgf : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}<VAR>h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}<GOAL>∫ (x : α) in {x | 0 ≤ g x}, g x ∂μ.restrict s - ∫ (x : α) in {x | g x ≤ 0}, g x ∂μ.restrict s ≤ ∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ.restrict s - ∫ (x : α) in {x | f x ≤ 0}, f x ∂μ.restrict s
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfi : IntegrableOn f s μ<VAR>hg : StronglyMeasurable g<VAR>hgi : IntegrableOn g s μ<VAR>hgf : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}<VAR>h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}<VAR>h_meas_nonpos_g : MeasurableSet {x | g x ≤ 0}<GOAL>∫ (x : α) in {x | 0 ≤ g x}, g x ∂μ.restrict s - ∫ (x : α) in {x | g x ≤ 0}, g x ∂μ.restrict s ≤ ∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ.restrict s - ∫ (x : α) in {x | f x ≤ 0}, f x ∂μ.restrict s
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfi : IntegrableOn f s μ<VAR>hg : StronglyMeasurable g<VAR>hgi : IntegrableOn g s μ<VAR>hgf : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}<VAR>h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}<VAR>h_meas_nonpos_g : MeasurableSet {x | g x ≤ 0}<VAR>h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0}<GOAL>∫ (x : α) in {x | 0 ≤ g x}, g x ∂μ.restrict s - ∫ (x : α) in {x | g x ≤ 0}, g x ∂μ.restrict s ≤ ∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ.restrict s - ∫ (x : α) in {x | f x ≤ 0}, f x ∂μ.restrict s
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfi : IntegrableOn f s μ<VAR>hg : StronglyMeasurable g<VAR>hgi : IntegrableOn g s μ<VAR>hgf : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}<VAR>h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}<VAR>h_meas_nonpos_g : MeasurableSet {x | g x ≤ 0}<VAR>h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0}<GOAL>∫ (x : α) in {x | 0 ≤ g x}, g x ∂μ.restrict s ≤ ∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ.restrict s