ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>inst✝³ : HasPushout g₁ g₂<VAR>inst✝² : HasPushout g₃ g₄<VAR>inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄<VAR>inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)<GOAL>pushout.inr g₃ g₄ ≫ pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯ = pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄
<VAR>a b : UnitAddCircle<GOAL>Differentiable ℂ fun s => hurwitzZeta a s - hurwitzZeta b s
<VAR>a b : UnitAddCircle<GOAL>Differentiable ℂ fun s => hurwitzZetaEven a s - hurwitzZetaEven b s + (hurwitzZetaOdd a s - hurwitzZetaOdd b s)
<VAR>a b : UnitAddCircle<GOAL>Differentiable ℂ (hurwitzZetaOdd a)
<VAR>a b : UnitAddCircle<GOAL>Differentiable ℂ (hurwitzZetaOdd b)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : OrderedRing 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMulWithZero 𝕜 E<VAR>s : Set E<GOAL>StarConvex 𝕜 0 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : OrderedRing 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMulWithZero 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>x✝ : x ∈ s<VAR>h : ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • 0 + b • x ∈ s<VAR>a : 𝕜<VAR>ha₀ : 0 ≤ a<VAR>ha₁ : a ≤ 1<GOAL>a • x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : OrderedRing 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMulWithZero 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>x✝ : x ∈ s<VAR>h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • 0 + b • x ∈ s
<VAR>x : ℝ≥0<VAR>h : x ≠ 0<VAR>y : ℝ<GOAL>↑x ^ y = ↑(x ^ y)
<VAR>x : ℝ≥0<VAR>h : x ≠ 0<VAR>y : ℝ<GOAL>some x ^ y = ↑(x ^ y)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hda : d ∣ a<VAR>hdb : d ∣ b<GOAL>a / d = b / d ↔ a = b
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hda : d ∣ a<VAR>hdb : d ∣ b<VAR>h : a / d = b / d<GOAL>a = b
<VAR>z : ℂ<GOAL>(cexp (z * I) + cexp (-(z * I))) / ((cexp (-(z * I)) - cexp (z * I)) * I) = (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))
<VAR>z : ℂ<VAR>h1 : cexp (z * I) + cexp (-(z * I)) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)<GOAL>(cexp (z * I) + cexp (-(z * I))) / ((cexp (-(z * I)) - cexp (z * I)) * I) = (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))
<VAR>z : ℂ<VAR>h1 : cexp (z * I) + cexp (-(z * I)) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)<VAR>h2 : (cexp (-(z * I)) - cexp (z * I)) * I = cexp (-(z * I)) * (I * (1 - cexp (2 * I * z)))<GOAL>(cexp (z * I) + cexp (-(z * I))) / ((cexp (-(z * I)) - cexp (z * I)) * I) = (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>o : HomOrthogonal s<VAR>α : Type<VAR>inst✝ : Finite α<VAR>f : α → ι<VAR>b a : α<VAR>j_property : a ∈ f ⁻¹' {f b}<GOAL>o.matrixDecomposition (𝟙 (⨁ fun a => s (f a))) (f b) ⟨b, ⋯⟩ ⟨a, j_property⟩ = 1 ⟨b, ⋯⟩ ⟨a, j_property⟩
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>o : HomOrthogonal s<VAR>α : Type<VAR>inst✝ : Finite α<VAR>f : α → ι<VAR>b a : α<VAR>j_property✝ : a ∈ f ⁻¹' {f b}<VAR>j_property : f a = f b<GOAL>o.matrixDecomposition (𝟙 (⨁ fun a => s (f a))) (f b) ⟨b, ⋯⟩ ⟨a, j_property✝⟩ = 1 ⟨b, ⋯⟩ ⟨a, j_property✝⟩
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>o : HomOrthogonal s<VAR>α : Type<VAR>inst✝ : Finite α<VAR>f : α → ι<VAR>b a : α<VAR>j_property✝ : a ∈ f ⁻¹' {f b}<VAR>j_property : f a = f b<GOAL>eqToHom ⋯ ≫ biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b = if ⟨b, ⋯⟩ = ⟨a, j_property✝⟩ then 𝟙 (s (f b)) else 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>inst✝⁶ : SMul M α✝<VAR>inst✝⁵ : SMul M β<VAR>inst✝⁴ : SMul N α✝<VAR>inst✝³ : SMul N β<VAR>a✝ : M<VAR>x : α✝ × β<VAR>α : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid α<VAR>inst✝ : DistribMulAction M α<VAR>a : M<VAR>c : β<GOAL>a • (0, c) = (0, a • c)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ : R⟦X⟧<GOAL>(coeff R 0) φ = (constantCoeff R) φ
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q p : R[X]<VAR>hp : p.degree ≠ 0<VAR>a : R<VAR>inst✝ : Nontrivial R<GOAL>(p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q p : R[X]<VAR>hp : p.degree ≠ 0<VAR>a : R<VAR>inst✝ : Nontrivial R<VAR>hd : p.degree < 0<GOAL>(p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q p : R[X]<VAR>hp : p.degree ≠ 0<VAR>a : R<VAR>inst✝ : Nontrivial R<VAR>hd : 0 < p.degree<GOAL>(p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q p : R[X]<VAR>hp : p.degree ≠ 0<VAR>a : R<VAR>inst✝ : Nontrivial R<VAR>hd : 0 < p.degree<GOAL>(X - C a).degree ≤ p.degree
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace Y<VAR>f : OnePoint ℕ → Y<GOAL>Continuous f ↔ Tendsto (fun x => f ↑x) atTop (𝓝 (f ∞))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f✝ g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>f : E → F<VAR>fa : CPolynomialOn 𝕜 f univ<GOAL>Continuous f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f✝ g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>f : E → F<VAR>fa : CPolynomialOn 𝕜 f univ<GOAL>ContinuousOn f univ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝ : SFinite μ<VAR>ht_subset : t ⊆ μ.sigmaFiniteSetᶜ<GOAL>μ t = 0 ∨ μ t = ⊤
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝ : SFinite μ<VAR>ht_subset : t ⊆ μ.sigmaFiniteSetᶜ<VAR>this : μ t = (μ.restrict μ.sigmaFiniteSetᶜ) t<GOAL>μ t = 0 ∨ μ t = ⊤
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝ : SFinite μ<VAR>ht_subset : t ⊆ μ.sigmaFiniteSetᶜ<VAR>this : μ t = (μ.restrict μ.sigmaFiniteSetᶜ) t<GOAL>(μ.restrict μ.sigmaFiniteSetᶜ) t = 0 ∨ (μ.restrict μ.sigmaFiniteSetᶜ) t = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Ring α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>h : multiplicity p b < multiplicity p a<GOAL>multiplicity p (a - b) = multiplicity p b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Ring α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>h : multiplicity p b < multiplicity p a<GOAL>multiplicity p b < multiplicity p a
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>f : G →* G'<VAR>x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }<VAR>y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }<VAR>z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }<VAR>key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹<GOAL>¬IsSolvable (Perm (Fin 5))
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>f : G →* G'<VAR>x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }<VAR>y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }<VAR>z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }<VAR>key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹<VAR>n : ℕ<GOAL>x ∈ derivedSeries (Perm (Fin 5)) n
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension S K L<VAR>hS : n ∈ S<GOAL>Splits (algebraMap K L) (cyclotomic (↑n) K)
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension S K L<VAR>hS : n ∈ S<GOAL>cyclotomic (↑n) K ∣ X ^ ↑n - C 1
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension S K L<VAR>hS : n ∈ S<GOAL>X ^ ↑n - C 1 = cyclotomic (↑n) K * ∏ i ∈ (↑n).properDivisors, cyclotomic i K
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<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✝¹ : Module R M₄<VAR>inst✝ : IsArtinian R M<VAR>r : R<VAR>rs : List R<VAR>h : IsRegular M (r :: rs)<GOAL>r :: rs = []
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<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✝¹ : Module R M₄<VAR>inst✝ : IsArtinian R M<VAR>r : R<VAR>rs : List R<VAR>h : (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs) ∧ r • ⊤ ⊔ Ideal.ofList rs • ⊤ < ⊤<GOAL>r :: rs = []
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<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✝¹ : Module R M₄<VAR>inst✝ : IsArtinian R M<VAR>r : R<VAR>rs : List R<VAR>h : (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs) ∧ r • ⊤ ⊔ Ideal.ofList rs • ⊤ < ⊤<GOAL>r • ⊤ = ⊤
<VAR>a b r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<VAR>hr' : 0 < ↑r<GOAL>↑(count (fun x => x ≡ v [MOD r]) b) = ⌈(↑b - ↑(v % r)) / ↑r⌉
<VAR>a b r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<VAR>hr' : 0 < ↑r<GOAL>⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑0 - ↑v) / ↑r⌉ = ⌈(↑b - ↑(v % r)) / ↑r⌉
<VAR>a b r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<VAR>hr' : 0 < ↑r<GOAL>⌈(↑b - ↑(v % r)) / ↑r⌉ - ⌈-↑(v % r) / ↑r⌉ = ⌈(↑b - ↑(v % r)) / ↑r⌉
<VAR>a b r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<VAR>hr' : 0 < ↑r<GOAL>v % r < r ∧ -↑(v % r) ≤ 0
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X : C<VAR>f : J → C<VAR>j✝ : J<GOAL>(biproduct.ι (fun j => X ⊗ f j) j✝ ≫ biproduct.desc fun j => X ◁ biproduct.ι f j) = biproduct.ι (fun j => X ⊗ f j) j✝ ≫ ∑ j : J, biproduct.π (fun j => X ⊗ f j) j ≫ X ◁ biproduct.ι f j
<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>g : E → F<VAR>c : ℝ≥0<VAR>𝕜 : Type u_5<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace 𝕜 F<VAR>L L' : E →L[𝕜] F<VAR>f : ↥(Lp E p μ)<GOAL>↑↑((L + L').compLp f) =ᶠ[ae μ] ↑↑(L.compLp f + L'.compLp f)
<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>g : E → F<VAR>c : ℝ≥0<VAR>𝕜 : Type u_5<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace 𝕜 F<VAR>L L' : E →L[𝕜] F<VAR>f : ↥(Lp E p μ)<GOAL>(fun a => (L + L') (↑↑f a)) =ᶠ[ae μ] ↑↑(L.compLp f + L'.compLp f)
<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>g : E → F<VAR>c : ℝ≥0<VAR>𝕜 : Type u_5<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace 𝕜 F<VAR>L L' : E →L[𝕜] F<VAR>f : ↥(Lp E p μ)<GOAL>(fun a => (L + L') (↑↑f a)) =ᶠ[ae μ] ↑↑(L.compLp f) + ↑↑(L'.compLp f)
<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>g : E → F<VAR>c : ℝ≥0<VAR>𝕜 : Type u_5<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace 𝕜 F<VAR>L L' : E →L[𝕜] F<VAR>f : ↥(Lp E p μ)<GOAL>(fun a => (L + L') (↑↑f a)) =ᶠ[ae μ] fun x => L (↑↑f x) + L' (↑↑f x)
<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>g : E → F<VAR>c : ℝ≥0<VAR>𝕜 : Type u_5<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace 𝕜 F<VAR>L L' : E →L[𝕜] F<VAR>f : ↥(Lp E p μ)<VAR>x : α<GOAL>(L + L') (↑↑f x) = L (↑↑f x) + L' (↑↑f x)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>P Q R : C<VAR>f✝ f' : P ⟶ Q<VAR>g✝ g' : Q ⟶ R<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : HasColimit (parallelPair f 0)<VAR>w : cokernel.π f = 0<VAR>R✝ : C<VAR>g : Y ⟶ R✝<VAR>h : f ≫ g = 0<GOAL>g = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>M : Matrix n n R<VAR>hM : M.PosSemidef<VAR>k✝ k : ℕ<GOAL>(M ^ (k + 2)).PosSemidef
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>M : Matrix n n R<VAR>hM : M.PosSemidef<VAR>k✝ k : ℕ<GOAL>(M * M ^ k * M).PosSemidef
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l : List α<GOAL>countP p l = l.length ↔ ∀ (a : α), a ∈ l → p a = true
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝¹ : DecidableRel fun a b => a ∣ b<VAR>inst✝ : DecidableEq (𝓞 K)<GOAL>FermatLastTheoremForThreeGen.Solution.u₄ S ^ 2 = 1
<VAR>x y : ℝ<VAR>f g : CauSeq ℚ abs<GOAL>mk f ≤ mk g ↔ f ≤ g
<VAR>x y : ℝ<VAR>f g : CauSeq ℚ abs<GOAL>f < g ∨ f ≈ g ↔ f ≤ g
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<GOAL>∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>IinS : ↑I ∈ S<GOAL>∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>IinS : ↑I ∈ S<VAR>chainub : ∀ c ⊆ S, IsChain (fun x x_1 => x ⊆ x_1) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub<GOAL>∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>IinS : ↑I ∈ S<VAR>chainub : ∀ c ⊆ S, IsChain (fun x x_1 => x ⊆ x_1) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<GOAL>∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>IinS : ↑I ∈ S<VAR>chainub : ∀ c ⊆ S, IsChain (fun x x_1 => x ⊆ x_1) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<GOAL>∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>IinS : ↑I ∈ S<VAR>chainub : ∀ c ⊆ S, IsChain (fun x x_1 => x ⊆ x_1) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<GOAL>J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<GOAL>J.IsPrime
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<GOAL>J.IsPrime
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<GOAL>∀ {x y : α}, x ⊓ y ∈ J → x ∈ J ∨ y ∈ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<GOAL>a₁ ⊓ a₂ ∈ J → a₁ ∈ J ∨ a₂ ∈ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<GOAL>a₁ ∉ J ∧ a₂ ∉ J → a₁ ⊓ a₂ ∉ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<GOAL>a₁ ⊓ a₂ ∉ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<GOAL>a₁ ⊓ a₂ ∉ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<GOAL>a₁ ⊓ a₂ ∉ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<VAR>J₁J : ↑J₁ ≠ Jset<GOAL>a₁ ⊓ a₂ ∉ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<VAR>J₁J : ↑J₁ ≠ Jset<VAR>J₂J : ↑J₂ ≠ Jset<GOAL>a₁ ⊓ a₂ ∉ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<VAR>J₁J : ↑J₁ ≠ Jset<VAR>J₂J : ↑J₂ ≠ Jset<VAR>J₁S : ↑J₁ ∉ S<GOAL>a₁ ⊓ a₂ ∉ J