ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>n : ℕ<VAR>x y : ℤ<VAR>hx : ¬2 ∣ x<VAR>hxy : 4 ∣ x - y<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<VAR>i : ℕ<GOAL>∀ (x : ℤ), Odd x → x ^ 2 ^ (i + 1) % 4 = 1
<VAR>R : Type u_1<VAR>n : ℕ<VAR>x✝ y : ℤ<VAR>hx✝ : ¬2 ∣ x✝<VAR>hxy : 4 ∣ x✝ - y<VAR>hx_odd : Odd x✝<VAR>hxy_even : Even (x✝ - y)<VAR>hy_odd : Odd y<VAR>i : ℕ<VAR>x : ℤ<VAR>hx : Odd x<GOAL>x ^ 2 ^ (i + 1) % 4 = 1
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>((μ + ν).withDensity f) s = (μ.withDensity f + ν.withDensity f) s
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hr : 0 < r<VAR>hf : ContinuousOn f (sphere z r)<VAR>hg : ContinuousOn g (sphere z r)<GOAL>cderiv r (f - g) z = cderiv r f z - cderiv r g z
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hr : 0 < r<VAR>hf : ContinuousOn f (sphere z r)<VAR>hg : ContinuousOn g (sphere z r)<VAR>h1 : ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)<GOAL>cderiv r (f - g) z = cderiv r f z - cderiv r g z
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hr : 0 < r<VAR>hf : ContinuousOn f (sphere z r)<VAR>hg : ContinuousOn g (sphere z r)<VAR>h1 : ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)<GOAL>((2 * ↑π * I)⁻¹ • ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • (f - g) w) = (2 * ↑π * I)⁻¹ • ((∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • f w) - ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • g w)
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hr : 0 < r<VAR>hf : ContinuousOn f (sphere z r)<VAR>hg : ContinuousOn g (sphere z r)<VAR>h1 : ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)<GOAL>(∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • (f - g) w) = (∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • f w) - ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • g w
<VAR>a x✝ z x : ℂ<GOAL>abs x * Real.cos x.arg = x.re
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s s₁ s₂ : LowerSet α<VAR>t t₁ t₂ : LowerSet β<VAR>x : α × β<GOAL>s ×ˢ t = ⊥ ↔ s = ⊥ ∨ t = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s s₁ s₂ : LowerSet α<VAR>t t₁ t₂ : LowerSet β<VAR>x : α × β<GOAL>↑(s ×ˢ t) = ↑⊥ ↔ ↑s = ↑⊥ ∨ ↑t = ↑⊥
<VAR>f g : MulRingNorm ℚ<VAR>x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n<VAR>c : ℝ<VAR>hc : 0 < c<VAR>h : ∀ (n : ℕ), f ↑n ^ c = g ↑n<VAR>x : ℚ<GOAL>f x ^ c = g x
<VAR>a : ℕ<GOAL>Periodic (fun n => n % a) a
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))<VAR>h_le : minkowskiBound K I ≤ volume (convexBodySum K B)<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ ↑(FractionalIdeal.absNorm ↑I) * (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))<VAR>h_le : minkowskiBound K I ≤ volume (convexBodySum K B)<VAR>x✝ : K<GOAL>↑(FractionalIdeal.absNorm ↑I) * (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)| = (B / ↑(finrank ℚ K)) ^ finrank ℚ K
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))<VAR>h_le : minkowskiBound K I ≤ volume (convexBodySum K B)<VAR>x✝ : K<GOAL>↑(FractionalIdeal.absNorm ↑I) * (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial * √|↑(discr K)| / ↑(finrank ℚ K) ^ finrank ℚ K = (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal / ↑(finrank ℚ K) ^ finrank ℚ K
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))<VAR>h_le : minkowskiBound K I ≤ volume (convexBodySum K B)<VAR>x✝ : K<GOAL>↑(FractionalIdeal.absNorm ↑I) * (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial * √|↑(discr K)| = (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))<VAR>h_le : minkowskiBound K I ≤ volume (convexBodySum K B)<VAR>x✝ : K<GOAL>(minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal = ↑(FractionalIdeal.absNorm ↑I) * (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial * √|↑(discr K)|
<VAR>z : ℍ<VAR>n : ℤ<GOAL>ModularGroup.T ^ n • z = ↑n +ᵥ z
<VAR>z : ℍ<VAR>n : ℤ<GOAL>(↑((algebraMap ℤ ℝ) (↑↑(ModularGroup.T ^ n) 0 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑↑(ModularGroup.T ^ n) 0 1))) / (↑((algebraMap ℤ ℝ) (↑↑(ModularGroup.T ^ n) 1 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑↑(ModularGroup.T ^ n) 1 1))) = ↑z + ↑↑n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>n : ℕ<VAR>a : α<VAR>l : List α<GOAL>(sublistsLen (n + 1) (a :: l)).length = (a :: l).length.choose (n + 1)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : IsIdempotentComplete C<VAR>inst✝ : HasFiniteCoproducts C<GOAL>(Compatibility.υ toKaroubiCompN₂IsoN₁).hom = Γ₂N₁.hom
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : IsIdempotentComplete C<VAR>inst✝ : HasFiniteCoproducts C<GOAL>Γ₂N₁.inv ≫ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom = 𝟙 (N₁ ⋙ Γ₂)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : IsIdempotentComplete C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<GOAL>(Γ₂N₁.inv ≫ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom).app X = (𝟙 (N₁ ⋙ Γ₂)).app X
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : IsIdempotentComplete C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<GOAL>Γ₂N₁.inv.app X ≫ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom.app X = (𝟙 (N₁ ⋙ Γ₂)).app X
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : IsIdempotentComplete C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<GOAL>((Γ₂N₂ToKaroubiIso.app X).inv ≫ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X)) ≫ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom.app X = (𝟙 (N₁ ⋙ Γ₂)).app X
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : IsIdempotentComplete C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<GOAL>Γ₂N₂ToKaroubiIso.inv.app X ≫ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X) ≫ Γ₂N₂.hom.app ((toKaroubiEquivalence (SimplicialObject C)).functor.obj X) ≫ Preadditive.DoldKan.equivalence.inverse.map (toKaroubiCompN₂IsoN₁.hom.app X) = (𝟙 (N₁ ⋙ Γ₂)).app X
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : IsIdempotentComplete C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<GOAL>Γ₂N₂ToKaroubiIso.inv.app X ≫ (𝟙 (N₂ ⋙ Γ₂)).app ((toKaroubi (SimplicialObject C)).obj X) ≫ Preadditive.DoldKan.equivalence.inverse.map (toKaroubiCompN₂IsoN₁.hom.app X) = (𝟙 (N₁ ⋙ Γ₂)).app X
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : IsIdempotentComplete C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<GOAL>Γ₂.map (toKaroubiCompN₂IsoN₁.inv.app X) ≫ Preadditive.DoldKan.equivalence.inverse.map (toKaroubiCompN₂IsoN₁.hom.app X) = 𝟙 ((N₁ ⋙ Γ₂).obj X)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : IsIdempotentComplete C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<GOAL>Γ₂.map (toKaroubiCompN₂IsoN₁.inv.app X) ≫ Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app X) = 𝟙 ((N₁ ⋙ Γ₂).obj X)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : IsIdempotentComplete C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<GOAL>𝟙 (Γ₂.obj (N₁.obj X)) = 𝟙 ((N₁ ⋙ Γ₂).obj X)
<VAR>a b : ℕ<VAR>ha : 2 ≤ a<VAR>hb : 2 < b<GOAL>2 ≤ (a ^ b + 1) / (a + 1)
<VAR>a b : ℕ<VAR>ha : 2 ≤ a<VAR>hb : 2 < b<GOAL>2 * a.succ ≤ a ^ b + 1
<VAR>a b : ℕ<VAR>ha : 2 ≤ a<VAR>hb : 2 < b<GOAL>Nat.mul 2 a + 1 ≤ a ^ b
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} E<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>inst✝¹ : HasZeroMorphisms E<VAR>F : C ⥤ D<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>X : C<VAR>hX : IsZero X<GOAL>IsZero (F.obj X)
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} E<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>inst✝¹ : HasZeroMorphisms E<VAR>F : C ⥤ D<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>X : C<VAR>hX : 𝟙 X = 0<GOAL>𝟙 (F.obj X) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>ι : Type u_5<VAR>F : Filter ι<VAR>inst✝ : F.NeBot<VAR>b : ℝ≥0∞<VAR>b_ne_top : b ≠ ⊤<VAR>xs : ι → ℝ≥0∞<VAR>le_b : ∀ᶠ (i : ι) in F, xs i ≤ b<GOAL>liminf (fun i => (xs i).toReal) F = (liminf xs F).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>ι : Type u_5<VAR>F : Filter ι<VAR>inst✝ : F.NeBot<VAR>b : ℝ≥0∞<VAR>b_ne_top : b ≠ ⊤<VAR>xs : ι → ℝ≥0∞<VAR>le_b : ∀ᶠ (i : ι) in F, xs i ≤ b<VAR>liminf_le : liminf xs F ≤ b<GOAL>liminf (fun i => (xs i).toReal) F = (liminf xs F).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>ι : Type u_5<VAR>F : Filter ι<VAR>inst✝ : F.NeBot<VAR>b : ℝ≥0∞<VAR>b_ne_top : b ≠ ⊤<VAR>xs : ι → ℝ≥0∞<VAR>le_b : ∀ᶠ (i : ι) in F, xs i ≤ b<VAR>liminf_le : liminf xs F ≤ b<VAR>aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)<GOAL>liminf (fun i => (xs i).toReal) F = (liminf xs F).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>ι : Type u_5<VAR>F : Filter ι<VAR>inst✝ : F.NeBot<VAR>b : ℝ≥0∞<VAR>b_ne_top : b ≠ ⊤<VAR>xs : ι → ℝ≥0∞<VAR>le_b : ∀ᶠ (i : ι) in F, xs i ≤ b<VAR>liminf_le : liminf xs F ≤ b<VAR>aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)<VAR>aux' : (liminf xs F).toReal = b.truncateToReal (liminf xs F)<GOAL>liminf (fun i => (xs i).toReal) F = (liminf xs F).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>ι : Type u_5<VAR>F : Filter ι<VAR>inst✝ : F.NeBot<VAR>b : ℝ≥0∞<VAR>b_ne_top : b ≠ ⊤<VAR>xs : ι → ℝ≥0∞<VAR>le_b : ∀ᶠ (i : ι) in F, xs i ≤ b<VAR>liminf_le : liminf xs F ≤ b<VAR>aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)<VAR>aux' : (liminf xs F).toReal = b.truncateToReal (liminf xs F)<GOAL>liminf (fun a => b.truncateToReal (xs a)) F = b.truncateToReal (liminf xs F)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>ι : Type u_5<VAR>F : Filter ι<VAR>inst✝ : F.NeBot<VAR>b : ℝ≥0∞<VAR>b_ne_top : b ≠ ⊤<VAR>xs : ι → ℝ≥0∞<VAR>le_b : ∀ᶠ (i : ι) in F, xs i ≤ b<VAR>liminf_le : liminf xs F ≤ b<VAR>aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)<VAR>aux' : (liminf xs F).toReal = b.truncateToReal (liminf xs F)<VAR>key : b.truncateToReal (liminf xs F) = liminf (b.truncateToReal ∘ xs) F<GOAL>liminf (fun a => b.truncateToReal (xs a)) F = b.truncateToReal (liminf xs F)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>a : I<VAR>z : I → Bool<VAR>hz : z ∈ C<VAR>hx : ↑⟨Proj (fun x => x ∈ s) z, ⋯⟩ a = true<GOAL>e (π C fun x => x ∈ s) a ∈ factors C s ⟨Proj (fun x => x ∈ s) z, ⋯⟩
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>a : I<VAR>z : I → Bool<VAR>hz : z ∈ C<VAR>hx : ↑⟨Proj (fun x => x ∈ s) z, ⋯⟩ a = true<GOAL>∃ a_1 ∈ s, (if Proj (fun x => x ∈ s) z a_1 = true then e (π C fun x => x ∈ s) a_1 else 1 - e (π C fun x => x ∈ s) a_1) = e (π C fun x => x ∈ s) a
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>a : I<VAR>z : I → Bool<VAR>hz : z ∈ C<VAR>hx : ↑⟨Proj (fun x => x ∈ s) z, ⋯⟩ a = true<GOAL>a ∈ s
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>m n : σ →₀ ℕ<VAR>h : m ≠ n<VAR>a : R<GOAL>(coeff R m) ((monomial R n) a) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>h : a < b<GOAL>insert a (Ioo a b) = Ico a b
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a✝ b✝ : α<VAR>n a b c : ℕ<GOAL>multinomial univ ![a, b, c] = (a + b + c)! / (a ! * b ! * c !)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a✝ b✝ : α<VAR>n a b c : ℕ<GOAL>(![a, b, c] 0 + ![a, b, c] 1 + ![a, b, c] 2)! / ((![a, b, c] 0)! * (![a, b, c] 1)! * (![a, b, c] 2)!) = (a + b + c)! / (a ! * b ! * c !)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>A : Type v<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a b : A<GOAL>((ad R A) a) b = ((LinearMap.mulLeft R - LinearMap.mulRight R) a) b
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L (fun n => ↑(ζ n)) s * L (fun n => ↑(μ n)) s = 1
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L ((fun x => ↑(ζ x)) ⍟ fun n => ↑(μ n)) s = 1
<VAR>α : Type u_1<VAR>m n : PosNum<VAR>h : ↑m = ↑n<GOAL>pos m = pos n
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>π : ι → Set (Set α)<VAR>S : Set ι<VAR>i : ι<VAR>his : i ∈ S<GOAL>π i ⊆ piiUnionInter π S
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>π : ι → Set (Set α)<VAR>S : Set ι<VAR>i : ι<VAR>his : i ∈ S<VAR>h_ss : {i} ⊆ S<GOAL>π i ⊆ piiUnionInter π S
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>π : ι → Set (Set α)<VAR>S : Set ι<VAR>i : ι<VAR>his : i ∈ S<VAR>h_ss : {i} ⊆ S<GOAL>π i ⊆ piiUnionInter π {i}
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>π : ι → Set (Set α)<VAR>S : Set ι<VAR>i : ι<VAR>his : i ∈ S<VAR>h_ss : {i} ⊆ S<GOAL>π i ⊆ π i ∪ {univ}
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : ContinuousMul G<VAR>h : IsClosed {1}<VAR>x : G<GOAL>IsClosed {x}
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CompleteLattice α<VAR>h : IsCoatomistic αᵒᵈ<VAR>b : α<GOAL>∃ s, b = sSup s ∧ ∀ a ∈ s, IsAtom a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CompleteLattice α<VAR>h : IsAtomistic α<VAR>b : αᵒᵈ<GOAL>∃ s, b = sInf s ∧ ∀ a ∈ s, IsCoatom a
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasPullbacks C<VAR>A : C<VAR>f₁ f₂ : Subobject A<VAR>inst✝ : HasBinaryProduct f₁ f₂<GOAL>(f₁ ⨯ f₂) = f₁ ⊓ f₂
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasPullbacks C<VAR>A : C<VAR>f₁ f₂ : Subobject A<VAR>inst✝ : HasBinaryProduct f₁ f₂<GOAL>(f₁ ⨯ f₂) ≤ f₁ ⊓ f₂
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasPullbacks C<VAR>A : C<VAR>f₁ f₂ : Subobject A<VAR>inst✝ : HasBinaryProduct f₁ f₂<GOAL>f₁ ⊓ f₂ ≤ (f₁ ⨯ f₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : T2Space M<VAR>v : VectorMeasure α M<VAR>f : ℕ → Set α<VAR>A B : Set α<VAR>hA : MeasurableSet A<VAR>hB : MeasurableSet B<VAR>h : A ⊆ B<GOAL>↑v A + ↑v (B \ A) = ↑v B
<VAR>U : Type u_1<VAR>inst✝² : Quiver U<VAR>V : Type u_2<VAR>inst✝¹ : Quiver V<VAR>φ : U ⥤q V<VAR>W : Type ?u.7311<VAR>inst✝ : Quiver W<VAR>ψ : V ⥤q W<VAR>u : U<GOAL>φ.symmetrify.costar u = ⇑(symmetrifyCostar (φ.obj u)).symm ∘ Sum.map (φ.costar u) (φ.star u) ∘ ⇑(symmetrifyCostar u)
<VAR>U : Type u_1<VAR>inst✝² : Quiver U<VAR>V : Type u_2<VAR>inst✝¹ : Quiver V<VAR>φ : U ⥤q V<VAR>W : Type ?u.7311<VAR>inst✝ : Quiver W<VAR>ψ : V ⥤q W<VAR>u : U<GOAL>⇑(symmetrifyCostar (φ.obj u)) ∘ φ.symmetrify.costar u = Sum.map (φ.costar u) (φ.star u) ∘ ⇑(symmetrifyCostar u)
<VAR>a b p q : ℝ<VAR>h : p.IsConjExponent q<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a⁻¹⁻¹ + b⁻¹⁻¹ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Option α ≃ Option β<VAR>x : α<VAR>h : e (some x) = none<GOAL>some (e.removeNone_aux x) = e none
<VAR>α✝ β✝ : Type u<VAR>a b : Cardinal.{v}<VAR>α β : Type v<GOAL>lift.{u, v} #α ≤ lift.{u, v} #β ↔ #α ≤ #β
<VAR>α✝ β✝ : Type u<VAR>a b : Cardinal.{v}<VAR>α β : Type v<GOAL>lift.{max v u, v} #α ≤ lift.{max v u, v} #β ↔ #α ≤ #β
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<GOAL>(mkMetric fun x => ⊤) = ⊤
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<GOAL>⊤ ≤ ⨆ r, ⨆ (_ : r > 0), ⊤
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<GOAL>∀ (b : OuterMeasure X), (∀ (i : ℝ≥0∞), ⨆ (_ : i > 0), ⊤ ≤ b) → ⊤ ≤ b
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f✝ : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>f : E ≃ᵐ E<VAR>g : E → ℝ<VAR>hg : ∀ᵐ (x : E) ∂μ, x ∈ ⇑f '' s → 0 ≤ g x<VAR>hg_int : IntegrableOn g (⇑f '' s) μ<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt (⇑f) (f' x) s x<GOAL>(Measure.map (⇑f.symm) (μ.withDensity fun x => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>h : (f '' s).ncard = s.ncard<VAR>hs : autoParam s.Finite _auto✝<GOAL>InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>h : (f '' s).encard = s.encard<VAR>hs : autoParam s.Finite _auto✝<GOAL>InjOn f s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Preorder (π i)<VAR>x y : (i : ι) → π i<VAR>i : ι<VAR>a b : π i<GOAL>update x i a ≤ update x i b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>f : ι → Set Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<GOAL>iIndep (fun i => MeasurableSpace.comap (fun x => x ∈ f i) ⊤) κ μ ↔ iIndepSet f κ μ
<VAR>a b✝ c : ℕ<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>an : ℤ<VAR>ad b : ℕ<VAR>inv✝ : Invertible ↑ad<VAR>this : Invertible (↑ad ^ b)<GOAL>IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)
<VAR>a b✝ c : ℕ<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>an : ℤ<VAR>ad b : ℕ<VAR>inv✝ : Invertible ↑ad<VAR>this : Invertible ↑(ad ^ b)<GOAL>IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)
<VAR>a b✝ c : ℕ<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>an : ℤ<VAR>ad b : ℕ<VAR>inv✝ : Invertible ↑ad<VAR>this : Invertible ↑(ad ^ b)<GOAL>(↑an * ⅟↑ad) ^ b = ↑(an ^ b) * ⅟↑(ad ^ b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<GOAL>univ.pi t₁ ⊆ univ.pi t₂ ↔ (∀ (i : ι), t₁ i ⊆ t₂ i) ∨ ∃ i, t₁ i = ∅
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<GOAL>¬IsUnramified k w ↔ w.IsComplex ∧ (w.comap (algebraMap k K)).IsReal
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<GOAL>(¬(if (w.comap (algebraMap k K)).IsReal then 1 else 2) = if w.IsReal then 1 else 2) ↔ ¬w.IsReal ∧ (w.comap (algebraMap k K)).IsReal
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>h₁ : ¬(w.comap (algebraMap k K)).IsReal<VAR>h₂ : w.IsReal<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<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>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>f : Q₂ →qᵢ Q₃<VAR>g : Q₁ →qᵢ Q₂<VAR>m : M₁<GOAL>(((map f).comp (map g)).toLinearMap ∘ₗ ι Q₁) m = ((map (f.comp g)).toLinearMap ∘ₗ ι Q₁) m
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<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>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>f : Q₂ →qᵢ Q₃<VAR>g : Q₁ →qᵢ Q₂<VAR>m : M₁<GOAL>(map f) ((map g) ((ι Q₁) m)) = (map (f.comp g)) ((ι Q₁) m)
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra 𝕜 A<VAR>inst✝¹ : IsAlgClosed 𝕜<VAR>inst✝ : Nontrivial A<VAR>I : FiniteDimensional 𝕜 A<VAR>a : A<GOAL>(σ a).Nonempty
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra 𝕜 A<VAR>inst✝¹ : IsAlgClosed 𝕜<VAR>inst✝ : Nontrivial A<VAR>I : FiniteDimensional 𝕜 A<VAR>a : A<VAR>p : 𝕜[X]<VAR>h_mon : p.Monic<VAR>h_eval_p : eval₂ ↑ₐ a p = 0<GOAL>(σ a).Nonempty
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra 𝕜 A<VAR>inst✝¹ : IsAlgClosed 𝕜<VAR>inst✝ : Nontrivial A<VAR>I : FiniteDimensional 𝕜 A<VAR>a : A<VAR>p : 𝕜[X]<VAR>h_mon : p.Monic<VAR>h_eval_p : eval₂ ↑ₐ a p = 0<VAR>nu : ¬IsUnit ((aeval a) p)<GOAL>(σ a).Nonempty
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra 𝕜 A<VAR>inst✝¹ : IsAlgClosed 𝕜<VAR>inst✝ : Nontrivial A<VAR>I : FiniteDimensional 𝕜 A<VAR>a : A<VAR>p : 𝕜[X]<VAR>h_mon : p.Monic<VAR>h_eval_p : eval₂ ↑ₐ a p = 0<VAR>nu : ¬IsUnit ((aeval a) (Multiset.map (fun a => X - C a) p.roots).prod)<GOAL>(σ a).Nonempty
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra 𝕜 A<VAR>inst✝¹ : IsAlgClosed 𝕜<VAR>inst✝ : Nontrivial A<VAR>I : FiniteDimensional 𝕜 A<VAR>a : A<VAR>p : 𝕜[X]<VAR>h_mon : p.Monic<VAR>h_eval_p : eval₂ ↑ₐ a p = 0<VAR>nu : ¬IsUnit ((aeval a) (Multiset.map (fun a => X - C a) p.roots).prod)<VAR>k : 𝕜<VAR>hk : k ∈ σ a<VAR>right✝ : eval k p = 0<GOAL>(σ a).Nonempty