ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>hα : IsIntegral F α<VAR>hβ : IsIntegral F β<VAR>f : F[X] := minpoly F α<VAR>g : F[X] := minpoly F β<VAR>ιFE : F →+* E := algebraMap F E<VAR>ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField<VAR>c : F<VAR>hc : ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots, ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c<VAR>γ : E := α + c • β<VAR>p : (↥F⟮γ⟯)[X] := EuclideanDomain.gcd ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X)) (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)<VAR>h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)<VAR>map_g_ne_zero : Polynomial.map ιFE g ≠ 0<VAR>h_ne_zero : h ≠ 0<VAR>h_sep : h.Separable<VAR>h_root : eval β h = 0<VAR>h_splits : Splits ιEE' h<VAR>h_roots : ∀ x ∈ (Polynomial.map ιEE' h).roots, x = ιEE' β<GOAL>Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>hα : IsIntegral F α<VAR>hβ : IsIntegral F β<VAR>f : F[X] := minpoly F α<VAR>g : F[X] := minpoly F β<VAR>ιFE : F →+* E := algebraMap F E<VAR>ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField<VAR>c : F<VAR>hc : ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots, ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c<VAR>γ : E := α + c • β<VAR>p : (↥F⟮γ⟯)[X] := EuclideanDomain.gcd ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X)) (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)<VAR>h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)<VAR>map_g_ne_zero : Polynomial.map ιFE g ≠ 0<VAR>h_ne_zero : h ≠ 0<VAR>h_sep : h.Separable<VAR>h_root : eval β h = 0<VAR>h_splits : Splits ιEE' h<VAR>h_roots : ∀ x ∈ (Polynomial.map ιEE' h).roots, x = ιEE' β<GOAL>Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = h
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>e : ℕ<VAR>he : 2 ≤ e<GOAL>I ^ e < I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>e : ℕ<VAR>he : 2 ≤ e<GOAL>I = (fun x => I ^ x) 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>e : ℕ<VAR>he : 2 ≤ e<GOAL>I = I ^ 1
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>n : ℕ<VAR>a c : K<GOAL>∃ p > n, Nat.Prime p ∧ a * c ^ p / ↑(p - 1)! < 1
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>n : ℕ<VAR>a c : K<GOAL>∃ p > n, Nat.Prime p ∧ a * c ^ p < ↑(p - 1)!
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f g : R<GOAL>basicOpen (f * g) ≤ basicOpen g
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f g : R<GOAL>basicOpen f ⊓ basicOpen g ≤ basicOpen g
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g✝ g : Ω → ℝ<GOAL>Tendsto (fun n => eLpNorm (μ[g|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g✝ g : Ω → ℝ<VAR>ht : Tendsto (fun n => eLpNorm (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)<GOAL>Tendsto (fun n => eLpNorm (μ[g|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g✝ g : Ω → ℝ<VAR>ht : Tendsto (fun n => eLpNorm (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)<VAR>heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x<GOAL>Tendsto (fun n => eLpNorm (μ[g|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g✝ g : Ω → ℝ<VAR>ht : Tendsto (fun n => eLpNorm (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)<VAR>heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x<VAR>n : ℕ<GOAL>μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n] =ᶠ[ae μ] μ[g|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g✝ g : Ω → ℝ<VAR>ht : Tendsto (fun n => eLpNorm (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)<VAR>heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x<VAR>n : ℕ<VAR>x : Ω<VAR>hxeq : (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x<GOAL>(μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) x = (μ[g|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) x
<VAR>J K : Type v<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : SmallCategory K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝ : HasColimits C<VAR>j : J<VAR>k : K<GOAL>colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k ≫ ((colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).inv ≫ (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl ((Prod.braiding K J).functor ⋙ G))).hom) ≫ (colimitIsoColimitCurryCompColim G).hom = colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j
<VAR>J K : Type v<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : SmallCategory K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝ : HasColimits C<VAR>j : J<VAR>k : K<GOAL>((colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k ≫ (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).inv) ≫ (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl ((Prod.braiding K J).functor ⋙ G))).hom) ≫ (colimitIsoColimitCurryCompColim G).hom = colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j
<VAR>ι : Sort u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝² : PartialOrder α✝<VAR>α : Type u_4<VAR>inst✝¹ : BooleanAlgebra α<VAR>inst✝ : IsAtomic α<VAR>x y : α<VAR>h : ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)<GOAL>x = y
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M N P : Mon_ C<GOAL>((λ_ (𝟙_ C)).inv ≫ ((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one) ⊗ P.one)) ≫ (α_ M.X N.X P.X).hom = (λ_ (𝟙_ C)).inv ≫ (M.one ⊗ (λ_ (𝟙_ C)).inv ≫ (N.one ⊗ P.one))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M N P : Mon_ C<GOAL>((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one) ⊗ P.one) ≫ (α_ M.X N.X P.X).hom = M.one ⊗ (λ_ (𝟙_ C)).inv ≫ (N.one ⊗ P.one)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M N P : Mon_ C<GOAL>(((λ_ (𝟙_ C)).inv ⊗ 𝟙 (𝟙_ C)) ≫ ((M.one ⊗ N.one) ⊗ P.one)) ≫ (α_ M.X N.X P.X).hom = M.one ⊗ (λ_ (𝟙_ C)).inv ≫ (N.one ⊗ P.one)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M N P : Mon_ C<GOAL>((λ_ (𝟙_ C)).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom ≫ (M.one ⊗ N.one ⊗ P.one) = M.one ⊗ (λ_ (𝟙_ C)).inv ≫ (N.one ⊗ P.one)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M N P : Mon_ C<GOAL>((λ_ (𝟙_ C)).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom ≫ (M.one ⊗ N.one ⊗ P.one) = (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M N P : Mon_ C<GOAL>(λ_ (𝟙_ C ⊗ 𝟙_ C)).inv ≫ (M.one ⊗ N.one ⊗ P.one) = (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M N P : Mon_ C<GOAL>(λ_ (𝟙_ C)).inv ≫ (λ_ (𝟙_ C ⊗ 𝟙_ C)).inv ≫ (M.one ⊗ N.one ⊗ P.one) = (λ_ (𝟙_ C)).inv ≫ (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M N P : Mon_ C<GOAL>((λ_ (𝟙_ C)).inv ≫ 𝟙_ C ◁ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one) = (λ_ (𝟙_ C)).inv ≫ (𝟙 (𝟙_ C) ⊗ (λ_ (𝟙_ C)).inv) ≫ (M.one ⊗ N.one ⊗ P.one)
<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>cyclotomic n ℤ = ⋯.choose
<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>map (Int.castRingHom ℤ) ⋯.choose = ⋯.choose
<VAR>n : ℕ<VAR>h : n ≠ 0<VAR>i : ℕ<GOAL>(map (Int.castRingHom ℤ) ⋯.choose).coeff i = ⋯.choose.coeff i
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : CommRing R✝<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R✝ M✝<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>N N' : Submodule R M<VAR>hN' : N'.FG<VAR>hIJ : I ≤ ⊥.jacobson<VAR>hNN : N' ≤ N ⊔ I • N'<GOAL>N' ≤ N
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m₁ m₂ : M<VAR>s : ↥S<GOAL>mk' f (m₁ + m₂) s = mk' f m₁ s + mk' f m₂ s
<VAR>α : Type u_1<VAR>s✝ t✝ : Set α<VAR>a : α<VAR>inst✝¹ : AddMonoid α<VAR>inst✝ : StarAddMonoid α<VAR>s t : Set α<GOAL>(s + t)⋆ = s⋆ + t⋆
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>inst✝ : Finite ι<VAR>s : ι → Set α<GOAL>TotallyBounded (⋃ i, s i) ↔ ∀ (i : ι), TotallyBounded (s i)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>inst✝ : Finite ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), TotallyBounded (s i)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<GOAL>∃ t, t.Finite ∧ ⋃ i, s i ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>inst✝ : Finite ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), TotallyBounded (s i)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>t : ι → Set α<VAR>htf : ∀ (x : ι), (t x).Finite<VAR>ht : ∀ (x : ι), s x ⊆ ⋃ y ∈ t x, {x | (x, y) ∈ U}<GOAL>∃ t, t.Finite ∧ ⋃ i, s i ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>inst✝ : Finite ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), TotallyBounded (s i)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>t : ι → Set α<VAR>htf : ∀ (x : ι), (t x).Finite<VAR>ht : ∀ (x : ι), s x ⊆ ⋃ y ∈ t x, {x | (x, y) ∈ U}<GOAL>⋃ i, s i ⊆ ⋃ y ∈ ⋃ i, t i, {x | (x, y) ∈ U}
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>inst✝ : Finite ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), TotallyBounded (s i)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>t : ι → Set α<VAR>htf : ∀ (x : ι), (t x).Finite<VAR>ht : ∀ (x : ι), s x ⊆ ⋃ y ∈ t x, {x | (x, y) ∈ U}<GOAL>⋃ i, s i ⊆ ⋃ i, ⋃ x ∈ t i, {x_1 | (x_1, x) ∈ U}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α →ₘ[μ] E<GOAL>f ∈ Lp E p μ ↔ Memℒp (↑f) p μ
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α<VAR>v : Vector α (n + 1)<VAR>i : ℕ<VAR>hi : i < n + 1<VAR>j : ℕ<VAR>hj : j < n + 2<GOAL>⟨(List.insertNth j a ↑v).eraseIdx ↑(if ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨i, ⋯⟩ else ⟨i + 1, ⋯⟩), ⋯⟩ = ⟨List.insertNth (↑(if h : ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯)) a ↑(match v with | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩), ⋯⟩
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α<VAR>v : Vector α (n + 1)<VAR>i : ℕ<VAR>hi : i < n + 1<VAR>j : ℕ<VAR>hj : j < n + 2<GOAL>(List.insertNth j a ↑v).eraseIdx ↑(if ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨i, ⋯⟩ else ⟨i + 1, ⋯⟩) = List.insertNth (↑(if h : ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯)) a ↑(match v with | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α<VAR>v : Vector α (n + 1)<VAR>i : ℕ<VAR>hi : i < n + 1<VAR>j : ℕ<VAR>hj : j < n + 2<GOAL>(List.insertNth j a ↑v).eraseIdx ↑(if i < j then ⟨i, ⋯⟩ else ⟨i + 1, ⋯⟩) = List.insertNth (↑(if h : i < j then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯)) a ↑(match v with | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>ν : Measure α<VAR>hle : μ ≤ ν<VAR>hf : 0 ≤ᶠ[ae ν] f<VAR>hfi : Integrable f ν<GOAL>∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>ν : Measure α<VAR>hle : μ ≤ ν<VAR>hf : 0 ≤ᶠ[ae ν] f<VAR>hfi : Integrable f ν<VAR>hfi' : Integrable f μ<GOAL>∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>ν : Measure α<VAR>hle : μ ≤ ν<VAR>hf : 0 ≤ᶠ[ae ν] f<VAR>hfi : Integrable f ν<VAR>hfi' : Integrable f μ<VAR>hf' : 0 ≤ᶠ[ae μ] f<GOAL>∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>ν : Measure α<VAR>hle : μ ≤ ν<VAR>hf : 0 ≤ᶠ[ae ν] f<VAR>hfi : Integrable f ν<VAR>hfi' : Integrable f μ<VAR>hf' : 0 ≤ᶠ[ae μ] f<GOAL>∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂ν
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>ν : Measure α<VAR>hle : μ ≤ ν<VAR>hf : 0 ≤ᶠ[ae ν] f<VAR>hfi : Integrable f ν<VAR>hfi' : Integrable f μ<VAR>hf' : 0 ≤ᶠ[ae μ] f<GOAL>∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>ν : Measure α<VAR>hle : μ ≤ ν<VAR>hf : 0 ≤ᶠ[ae ν] f<VAR>hfi : Integrable f ν<VAR>hfi' : Integrable f μ<VAR>hf' : 0 ≤ᶠ[ae μ] f<GOAL>∫⁻ (a : α), ENNReal.ofReal (f a) ∂ν ≠ ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : OrderTop α<VAR>inst✝ : OrderTopology α<GOAL>𝓝 ⊤ = ⨅ l, ⨅ (_ : l < ⊤), 𝓟 (Ioi l)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : NormalizedGCDMonoid R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>f : R →+* S<VAR>hinj : Function.Injective ⇑f<VAR>p : R[X]<VAR>s : S<VAR>hpzero : p ≠ 0<VAR>hp : eval₂ f s p = 0<GOAL>eval₂ f s p.primPart = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : NormalizedGCDMonoid R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>f : R →+* S<VAR>hinj : Function.Injective ⇑f<VAR>p : R[X]<VAR>s : S<VAR>hpzero : p ≠ 0<VAR>hp : f p.content * eval₂ f s p.primPart = 0<GOAL>eval₂ f s p.primPart = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : NormalizedGCDMonoid R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>f : R →+* S<VAR>hinj : Function.Injective ⇑f<VAR>p : R[X]<VAR>s : S<VAR>hpzero : p ≠ 0<VAR>hp : f p.content * eval₂ f s p.primPart = 0<VAR>hcont : p.content ≠ 0<GOAL>eval₂ f s p.primPart = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : NormalizedGCDMonoid R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>f : R →+* S<VAR>hinj : Function.Injective ⇑f<VAR>p : R[X]<VAR>s : S<VAR>hpzero : p ≠ 0<VAR>hp : f p.content * eval₂ f s p.primPart = 0<VAR>hcont : f p.content ≠ f 0<GOAL>eval₂ f s p.primPart = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : NormalizedGCDMonoid R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>f : R →+* S<VAR>hinj : Function.Injective ⇑f<VAR>p : R[X]<VAR>s : S<VAR>hpzero : p ≠ 0<VAR>hp : f p.content * eval₂ f s p.primPart = 0<VAR>hcont : f p.content ≠ 0<GOAL>eval₂ f s p.primPart = 0
<VAR>z : ℂ<VAR>n✝ n : ℕ<GOAL>∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = 1 / 2 * ∫ (x : ℝ) in 0 ..π, sin x ^ n
<VAR>z : ℂ<VAR>n✝ n : ℕ<GOAL>(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) + ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = ∫ (x : ℝ) in 0 ..π, sin x ^ n
<VAR>z : ℂ<VAR>n✝ n : ℕ<VAR>L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)<GOAL>(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) + ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = ∫ (x : ℝ) in 0 ..π, sin x ^ n
<VAR>z : ℂ<VAR>n✝ n : ℕ<VAR>L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)<VAR>R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π<GOAL>(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) + ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = ∫ (x : ℝ) in 0 ..π, sin x ^ n
<VAR>z : ℂ<VAR>n✝ n : ℕ<VAR>L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)<VAR>R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π<GOAL>(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) + ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = (∫ (x : ℝ) in 0 ..π / 2, sin x ^ n) + ∫ (x : ℝ) in π / 2 ..π, sin x ^ n
<VAR>A : Type u_1<VAR>inst✝¹ : AddCancelMonoid A<VAR>inst✝ : HasAntidiagonal A<VAR>p q : A × A<VAR>n : A<VAR>hp : p ∈ antidiagonal n<VAR>hq : q ∈ antidiagonal n<GOAL>p = q ↔ p.1 = q.1
<VAR>A : Type u_1<VAR>inst✝¹ : AddCancelMonoid A<VAR>inst✝ : HasAntidiagonal A<VAR>p q : A × A<VAR>n : A<VAR>hp : p ∈ antidiagonal n<VAR>hq : q ∈ antidiagonal n<VAR>h : p.1 = q.1<GOAL>q.1 + p.2 = q.1 + q.2
<VAR>A : Type u_1<VAR>inst✝¹ : AddCancelMonoid A<VAR>inst✝ : HasAntidiagonal A<VAR>p q : A × A<VAR>n : A<VAR>hp : p.1 + p.2 = n<VAR>hq : q.1 + q.2 = n<VAR>h : p.1 = q.1<GOAL>q.1 + p.2 = q.1 + q.2
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : LieAlgebra.IsNilpotent R L<VAR>inst✝ : LinearWeights R L M<VAR>χ : L → R<VAR>x : L<VAR>x✝ : ↥↑(shiftedWeightSpace R L M χ)<GOAL>↑(((toEnd R L ↥↑(shiftedWeightSpace R L M χ)) x) x✝) = ↑(((shift R L M χ).conj ((toEnd R L ↥↑(weightSpace M χ)) x - χ x • LinearMap.id)) x✝)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : LinearOrder α<VAR>u : ι → α<VAR>h : Monotone u<VAR>H : ¬BddAbove (range u)<VAR>b : α<GOAL>∃ a, b ≤ u a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : LinearOrder α<VAR>u : ι → α<VAR>h : Monotone u<VAR>H : ¬BddAbove (range u)<VAR>b : α<VAR>N : ι<VAR>hN : b < u N<GOAL>∃ a, b ≤ u a
<VAR>a b P Q : Prop<GOAL>¬Xor' P Q ↔ (P ↔ Q)
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf✝ : ContractingWith K f<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : CompleteSpace α<VAR>n : ℕ<VAR>hf : ContractingWith K f^[n]<VAR>x : α := fixedPoint f^[n] hf<GOAL>IsFixedPt f x
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf✝ : ContractingWith K f<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : CompleteSpace α<VAR>n : ℕ<VAR>hf : ContractingWith K f^[n]<VAR>x : α := fixedPoint f^[n] hf<VAR>hx : f^[n] x = x<GOAL>IsFixedPt f x
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf✝ : ContractingWith K f<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : CompleteSpace α<VAR>n : ℕ<VAR>hf : ContractingWith K f^[n]<VAR>x : α := fixedPoint f^[n] hf<VAR>hx : f^[n] x = x<VAR>this : dist (f^[n] x) (f^[n] (f x)) ≤ ↑K * dist x (f x)<GOAL>IsFixedPt f x
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf✝ : ContractingWith K f<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : CompleteSpace α<VAR>n : ℕ<VAR>hf : ContractingWith K f^[n]<VAR>x : α := fixedPoint f^[n] hf<VAR>hx : f^[n] x = x<VAR>this : dist x (f x) ≤ ↑K * dist x (f x)<GOAL>IsFixedPt f x
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf✝ : ContractingWith K f<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : CompleteSpace α<VAR>n : ℕ<VAR>hf : ContractingWith K f^[n]<VAR>x : α := fixedPoint f^[n] hf<VAR>hx : f^[n] x = x<GOAL>dist x (f x) ≤ ↑K * dist x (f x) → IsFixedPt f x
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf✝ : ContractingWith K f<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : CompleteSpace α<VAR>n : ℕ<VAR>hf : ContractingWith K f^[n]<VAR>x : α := fixedPoint f^[n] hf<VAR>hx : f^[n] x = x<GOAL>¬IsFixedPt f x → ↑K * dist x (f x) < dist x (f x)