ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>E : Type u_3<VAR>inst✝¹³ : Field F<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field E<VAR>inst✝¹⁰ : Algebra F K<VAR>inst✝⁹ : Algebra F E<VAR>inst✝⁸ : Algebra K E<VAR>inst✝⁷ : IsScalarTower F K E<VAR>A₁ : Type u_4<VAR>B₁ : Type u_5<VAR>A₂ : Type u_6<VAR>B₂ : Type u_7<VAR>inst✝⁶ : Field A₁<VAR>inst✝⁵ : Field B₁<VAR>inst✝⁴ : Field A₂<VAR>inst✝³ : Field B₂<VAR>inst✝² : Algebra A₁ B₁<VAR>inst✝¹ : Algebra A₂ B₂<VAR>e₁ : A₁ ≃+* A₂<VAR>e₂ : B₁ ≃+* B₂<VAR>he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)<VAR>inst✝ : Algebra.IsSeparable A₁ B₁<VAR>this✝² : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra<VAR>this✝¹ : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra<VAR>this✝ : IsScalarTower A₁ A₂ B₁<VAR>e : B₁ ≃ₐ[A₂] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }<VAR>this : Algebra.IsSeparable A₂ B₁<GOAL>Algebra.IsSeparable A₂ B₂
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>0 ≤ -x ↔ x ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁✝ a₂✝ : α<VAR>b✝ b₁ b₂ : β<VAR>γ : Type u_3<VAR>inst✝⁸ : Zero α<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Zero β<VAR>inst✝⁵ : Preorder β<VAR>inst✝⁴ : Zero γ<VAR>inst✝³ : Preorder γ<VAR>inst✝² : SMul α β<VAR>inst✝¹ : SMul α γ<VAR>f : β → γ<VAR>inst✝ : SMulPosMono α γ<VAR>b : β<VAR>a₁ a₂ : α<VAR>ha : a₁ ≤ a₂<VAR>hf : ∀ {b₁ b₂ : β}, True<VAR>smul : α → β → True<VAR>zero : True<VAR>hb : 0 ≤ f b<GOAL>a₁ • f b ≤ a₂ • f b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<GOAL>toIcoMod hp a b = b ↔ b ∈ Set.Ico a (a + p)
<VAR>𝕜 : Type u_1<VAR>ι✝ : Type u_2<VAR>E : ι✝ → Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : (i : ι✝) → TopologicalSpace (E i)<VAR>inst✝⁵ : (i : ι✝) → AddCommGroup (E i)<VAR>inst✝⁴ : (i : ι✝) → Module 𝕜 (E i)<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : TopologicalAddGroup F<VAR>ι : Type u_5<VAR>p : ι → Prop<VAR>b : ι → Set F<VAR>h : (𝓝 0).HasBasis p b<VAR>this : UniformSpace F := TopologicalAddGroup.toUniformSpace F<GOAL>(𝓝 0).HasBasis (fun Si => IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun Si => {f | MapsTo (⇑f) Si.1 (b Si.2)}
<VAR>𝕜 : Type u_1<VAR>ι✝ : Type u_2<VAR>E : ι✝ → Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : (i : ι✝) → TopologicalSpace (E i)<VAR>inst✝⁵ : (i : ι✝) → AddCommGroup (E i)<VAR>inst✝⁴ : (i : ι✝) → Module 𝕜 (E i)<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : TopologicalAddGroup F<VAR>ι : Type u_5<VAR>p : ι → Prop<VAR>b : ι → Set F<VAR>h : (𝓝 0).HasBasis p b<VAR>this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<VAR>this : UniformAddGroup F<GOAL>(𝓝 0).HasBasis (fun Si => IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun Si => {f | MapsTo (⇑f) Si.1 (b Si.2)}
<VAR>𝕜 : Type u_1<VAR>ι✝ : Type u_2<VAR>E : ι✝ → Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : (i : ι✝) → TopologicalSpace (E i)<VAR>inst✝⁵ : (i : ι✝) → AddCommGroup (E i)<VAR>inst✝⁴ : (i : ι✝) → Module 𝕜 (E i)<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : TopologicalAddGroup F<VAR>ι : Type u_5<VAR>p : ι → Prop<VAR>b : ι → Set F<VAR>h : (𝓝 0).HasBasis p b<VAR>this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<VAR>this : UniformAddGroup F<GOAL>(Filter.comap toUniformOnFun (𝓝 (toUniformOnFun 0))).HasBasis (fun Si => IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun Si => {f | MapsTo (⇑f) Si.1 (b Si.2)}
<VAR>𝕜 : Type u_1<VAR>ι✝ : Type u_2<VAR>E : ι✝ → Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : (i : ι✝) → TopologicalSpace (E i)<VAR>inst✝⁵ : (i : ι✝) → AddCommGroup (E i)<VAR>inst✝⁴ : (i : ι✝) → Module 𝕜 (E i)<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : TopologicalAddGroup F<VAR>ι : Type u_5<VAR>p : ι → Prop<VAR>b : ι → Set F<VAR>h : (𝓝 0).HasBasis p b<VAR>this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<VAR>this : UniformAddGroup F<GOAL>{s | IsVonNBounded 𝕜 s}.Nonempty
<VAR>𝕜 : Type u_1<VAR>ι✝ : Type u_2<VAR>E : ι✝ → Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : (i : ι✝) → TopologicalSpace (E i)<VAR>inst✝⁵ : (i : ι✝) → AddCommGroup (E i)<VAR>inst✝⁴ : (i : ι✝) → Module 𝕜 (E i)<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : TopologicalAddGroup F<VAR>ι : Type u_5<VAR>p : ι → Prop<VAR>b : ι → Set F<VAR>h : (𝓝 0).HasBasis p b<VAR>this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<VAR>this : UniformAddGroup F<GOAL>DirectedOn (fun x x_1 => x ⊆ x_1) {s | IsVonNBounded 𝕜 s}
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ (convexHull 𝕜) s<GOAL>∃ ι x_1 z w, Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ ⋃ t, ⋃ (_ : ↑t ⊆ s), ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑t<GOAL>∃ ι x_1 z w, Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hx : ∃ i, ↑i ⊆ s ∧ AffineIndependent 𝕜 Subtype.val ∧ x ∈ (convexHull 𝕜) ↑i<GOAL>∃ ι x_1 z w, Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>t : Finset E<VAR>ht₁ : ↑t ⊆ s<VAR>ht₂ : AffineIndependent 𝕜 Subtype.val<VAR>ht₃ : x ∈ (convexHull 𝕜) ↑t<GOAL>∃ ι x_1 z w, Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>t : Finset E<VAR>ht₁ : ↑t ⊆ s<VAR>ht₂ : AffineIndependent 𝕜 Subtype.val<VAR>ht₃ : ∃ w, (∀ y ∈ t, 0 ≤ w y) ∧ ∑ y ∈ t, w y = 1 ∧ t.centerMass w id = x<GOAL>∃ ι x_1 z w, Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hs : NullMeasurableSet s μ<VAR>ht : NullMeasurableSet t μ<VAR>hd : AEDisjoint μ s t<GOAL>μ (s ∪ t) = μ s + μ t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hs : NullMeasurableSet s μ<VAR>ht : NullMeasurableSet t μ<VAR>hd : AEDisjoint μ s t<GOAL>Pairwise (AEDisjoint μ on fun b => bif b then s else t)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hs : NullMeasurableSet s μ<VAR>ht : NullMeasurableSet t μ<VAR>hd : AEDisjoint μ s t<GOAL>∀ (i : Bool), NullMeasurableSet (bif i then s else t) μ
<VAR>X : Type u<VAR>inst✝ : TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<VAR>t : ↑I<GOAL>(delayReflRight 1 γ) t = γ t
<VAR>x y : ℂ<GOAL>sinh x ^ 2 = cosh x ^ 2 - 1
<VAR>x y : ℂ<GOAL>sinh x ^ 2 = cosh x ^ 2 - (cosh x ^ 2 - sinh x ^ 2)
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<GOAL>0 < z ↔ 0 < re z ∧ im z = 0
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a : α<VAR>l✝ l : List α<VAR>h : Sorted r l<VAR>k : ℕ<VAR>x y : α<VAR>hx : x ∈ take k l<VAR>hy : y ∈ drop k l<GOAL>r x y
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a : α<VAR>l✝ l : List α<VAR>h : Sorted r l<VAR>k : ℕ<VAR>x : α<VAR>hx : x ∈ take k l<VAR>iy : ℕ<VAR>hiy : iy < (drop k l).length<VAR>hy : (drop k l)[iy] ∈ drop k l<GOAL>r x (drop k l)[iy]
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a : α<VAR>l✝ l : List α<VAR>h : Sorted r l<VAR>k iy : ℕ<VAR>hiy : iy < (drop k l).length<VAR>hy : (drop k l)[iy] ∈ drop k l<VAR>ix : ℕ<VAR>hix : ix < (take k l).length<VAR>hx : (take k l)[ix] ∈ take k l<GOAL>r (take k l)[ix] (drop k l)[iy]
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a : α<VAR>l✝ l : List α<VAR>h : Sorted r l<VAR>k iy : ℕ<VAR>hiy : iy < (drop k l).length<VAR>hy : (drop k l)[iy] ∈ drop k l<VAR>ix : ℕ<VAR>hix : ix < (take k l).length<VAR>hx : (take k l)[ix] ∈ take k l<GOAL>r l[ix] l[k + iy]
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a : α<VAR>l✝ l : List α<VAR>h : Sorted r l<VAR>k iy : ℕ<VAR>hiy : iy < (drop k l).length<VAR>hy : (drop k l)[iy] ∈ drop k l<VAR>ix : ℕ<VAR>hix✝ : ix < (take k l).length<VAR>hix : ix < min k l.length<VAR>hx : (take k l)[ix] ∈ take k l<GOAL>r l[ix] l[k + iy]
<VAR>s : Set ℤ<VAR>h1 : s.Nonempty<VAR>h2 : BddAbove s<GOAL>sSup s ∈ s
<VAR>s : Set ℤ<VAR>h1 : s.Nonempty<VAR>h2 : BddAbove s<GOAL>sSup s = ↑((Classical.choose h2).greatestOfBdd ⋯ h1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>s : Set α<GOAL>kernImage f sᶜ = (f '' s)ᶜ
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>n : Fin 2<GOAL>(CoordinateRing.basis W) n = (AdjoinRoot.powerBasis' ⋯).gen ^ ↑n
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>i : K →+* L<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : Algebra R L<VAR>p : R[X]<VAR>h : Splits (algebraMap R K) p<VAR>f : K →ₐ[R] L<GOAL>⇑f '' p.rootSet K = p.rootSet L
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : OpensMeasurableSpace E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace F<VAR>f : E → F<VAR>v : E<VAR>inst✝ : SecondCountableTopology E<VAR>hf : Continuous f<VAR>this✝¹ : MeasurableSpace 𝕜 := borel 𝕜<VAR>this✝ : BorelSpace 𝕜<VAR>g : E × E → 𝕜 → F := fun p t => f (p.1 + t • p.2)<GOAL>StronglyMeasurable fun p => lineDeriv 𝕜 f p.1 p.2
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : OpensMeasurableSpace E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace F<VAR>f : E → F<VAR>v : E<VAR>inst✝ : SecondCountableTopology E<VAR>hf : Continuous f<VAR>this✝¹ : MeasurableSpace 𝕜 := borel 𝕜<VAR>this✝ : BorelSpace 𝕜<VAR>g : E × E → 𝕜 → F := fun p t => f (p.1 + t • p.2)<VAR>this : Continuous (Function.uncurry g)<GOAL>StronglyMeasurable fun p => lineDeriv 𝕜 f p.1 p.2
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>sinZeta (-a) s = -sinZeta a s
<VAR>x✝ y x : ℝ<GOAL>arcsin x = 0 ↔ x = 0
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>r : ℝ<VAR>ha : r ≤ 0<VAR>f : ι → ℝ<GOAL>(⨅ i, f i) * r = ⨆ i, f i * r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a✝ b✝ c✝ d a b c : G<VAR>h : a = b * c<GOAL>a / b = c
<VAR>a b c p q : ℚ<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<GOAL>0 ≤ n₁ /. ↑d₁ → 0 ≤ n₂ /. ↑d₂ → 0 ≤ n₁ /. ↑d₁ * (n₂ /. ↑d₂)
<VAR>a b c p q : ℚ<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>d₁0 : 0 < ↑d₁<GOAL>0 ≤ n₁ /. ↑d₁ → 0 ≤ n₂ /. ↑d₂ → 0 ≤ n₁ /. ↑d₁ * (n₂ /. ↑d₂)
<VAR>a b c p q : ℚ<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>d₁0 : 0 < ↑d₁<VAR>d₂0 : 0 < ↑d₂<GOAL>0 ≤ n₁ /. ↑d₁ → 0 ≤ n₂ /. ↑d₂ → 0 ≤ n₁ /. ↑d₁ * (n₂ /. ↑d₂)
<VAR>a b c p q : ℚ<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>d₁0 : 0 < ↑d₁<VAR>d₂0 : 0 < ↑d₂<GOAL>0 ≤ n₁ → 0 ≤ n₂ → 0 ≤ n₁ * n₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a a' : α<VAR>b : M<GOAL>single a b = 0 ↔ b = 0
<VAR>b x y : ℝ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>logb b (x * y) = logb b x + logb b y
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha_pos : a ≠ 0<VAR>hb_pos : b ≠ 0<VAR>dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization<VAR>d : ℕ := dfac.prod fun x x_1 => x ^ x_1<GOAL>(a.gcd b).factorization = a.factorization ⊓ b.factorization
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha_pos : a ≠ 0<VAR>hb_pos : b ≠ 0<VAR>dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization<VAR>d : ℕ := dfac.prod fun x x_1 => x ^ x_1<VAR>dfac_prime : ∀ p ∈ dfac.support, Prime p<GOAL>(a.gcd b).factorization = a.factorization ⊓ b.factorization
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha_pos : a ≠ 0<VAR>hb_pos : b ≠ 0<VAR>dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization<VAR>d : ℕ := dfac.prod fun x x_1 => x ^ x_1<VAR>dfac_prime : ∀ p ∈ dfac.support, Prime p<VAR>h1 : d.factorization = dfac<GOAL>(a.gcd b).factorization = a.factorization ⊓ b.factorization
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha_pos : a ≠ 0<VAR>hb_pos : b ≠ 0<VAR>dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization<VAR>d : ℕ := dfac.prod fun x x_1 => x ^ x_1<VAR>dfac_prime : ∀ p ∈ dfac.support, Prime p<VAR>h1 : d.factorization = dfac<VAR>hd_pos : d ≠ 0<GOAL>(a.gcd b).factorization = a.factorization ⊓ b.factorization
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha_pos : a ≠ 0<VAR>hb_pos : b ≠ 0<VAR>dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization<VAR>d : ℕ := dfac.prod fun x x_1 => x ^ x_1<VAR>dfac_prime : ∀ p ∈ dfac.support, Prime p<VAR>h1 : d.factorization = dfac<VAR>hd_pos : d ≠ 0<GOAL>d = a.gcd b
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha_pos : a ≠ 0<VAR>hb_pos : b ≠ 0<VAR>dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization<VAR>d : ℕ := dfac.prod fun x x_1 => x ^ x_1<VAR>dfac_prime : ∀ p ∈ dfac.support, Prime p<VAR>h1 : d.factorization = dfac<VAR>hd_pos : d ≠ 0<GOAL>d ∣ a
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha_pos : a ≠ 0<VAR>hb_pos : b ≠ 0<VAR>dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization<VAR>d : ℕ := dfac.prod fun x x_1 => x ^ x_1<VAR>dfac_prime : ∀ p ∈ dfac.support, Prime p<VAR>h1 : d.factorization = dfac<VAR>hd_pos : d ≠ 0<GOAL>d ∣ b
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha_pos : a ≠ 0<VAR>hb_pos : b ≠ 0<VAR>dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization<VAR>d : ℕ := dfac.prod fun x x_1 => x ^ x_1<VAR>dfac_prime : ∀ p ∈ dfac.support, Prime p<VAR>h1 : d.factorization = dfac<VAR>hd_pos : d ≠ 0<GOAL>∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ d
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hr : ¬r = 0<GOAL>padicNorm p (q / r) * padicNorm p r = padicNorm p q
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>p q : ℚ<VAR>K : Type u_5<VAR>inst✝ : LinearOrderedField K<GOAL>0 ≤ ↑q ↔ 0 ≤ q
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>W✝ : Subspace K V<VAR>inst✝ : FiniteDimensional K V<VAR>W : Subspace K (Module.Dual K V)<GOAL>finrank K ↥W + finrank K ↥(dualCoannihilator W) = finrank K V
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>W✝ : Subspace K V<VAR>inst✝ : FiniteDimensional K V<VAR>W : Subspace K (Module.Dual K V)<GOAL>finrank K ↥W + finrank K ↥(dualAnnihilator W) = finrank K V
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>W✝ : Subspace K V<VAR>inst✝ : FiniteDimensional K V<VAR>W : Subspace K (Module.Dual K V)<VAR>equiv : (Module.Dual K V ⧸ W) ≃ₗ[K] ↥(dualAnnihilator W) := W.quotEquivAnnihilator<GOAL>finrank K ↥W + finrank K ↥(dualAnnihilator W) = finrank K V
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>W✝ : Subspace K V<VAR>inst✝ : FiniteDimensional K V<VAR>W : Subspace K (Module.Dual K V)<VAR>equiv : (Module.Dual K V ⧸ W) ≃ₗ[K] ↥(dualAnnihilator W) := W.quotEquivAnnihilator<VAR>eq : finrank K (Module.Dual K V ⧸ W) = finrank K ↥(dualAnnihilator W)<GOAL>finrank K ↥W + finrank K ↥(dualAnnihilator W) = finrank K V
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>I J : HasZeroMorphisms C<GOAL>I = J
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>I J : HasZeroMorphisms C<GOAL>∀ (X Y : C), Zero.zero = Zero.zero
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>I J : HasZeroMorphisms C<VAR>X Y : C<GOAL>Zero.zero = Zero.zero
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>I J : HasZeroMorphisms C<VAR>X Y : C<VAR>this : Zero.zero ≫ Zero.zero = Zero.zero<GOAL>Zero.zero = Zero.zero
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>I J : HasZeroMorphisms C<VAR>X Y : C<VAR>this : Zero.zero ≫ Zero.zero = Zero.zero<VAR>that : Zero.zero ≫ Zero.zero = Zero.zero<GOAL>Zero.zero = Zero.zero
<VAR>α : Type u_1<VAR>m n : PosNum<VAR>h : m = n<GOAL>↑m < ↑n ↔ Ordering.eq = Ordering.lt
<VAR>α : Type u_1<VAR>m n : PosNum<VAR>h : Ordering.casesOn Ordering.gt (↑m < ↑n) (m = n) (↑n < ↑m)<GOAL>↑m < ↑n ↔ Ordering.gt = Ordering.lt
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (filter (fun a => a ^ n = 1) univ).card ≤ n<VAR>d : ℕ<VAR>IH : ∀ m < d, m ∣ Fintype.card α → 0 < (filter (fun a => orderOf a = m) univ).card → (filter (fun a => orderOf a = m) univ).card = φ m<VAR>hd : d ∣ Fintype.card α<VAR>hpos : 0 < (filter (fun a => orderOf a = d) univ).card<GOAL>(filter (fun a => orderOf a = d) univ).card = φ d
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (filter (fun a => a ^ n = 1) univ).card ≤ n<VAR>IH : ∀ m < 0, m ∣ Fintype.card α → 0 < (filter (fun a => orderOf a = m) univ).card → (filter (fun a => orderOf a = m) univ).card = φ m<VAR>hd : 0 ∣ Fintype.card α<VAR>hpos : 0 < (filter (fun a => orderOf a = 0) univ).card<GOAL>(filter (fun a => orderOf a = 0) univ).card = φ 0
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (filter (fun a => a ^ n = 1) univ).card ≤ n<VAR>d : ℕ<VAR>IH : ∀ m < d, m ∣ Fintype.card α → 0 < (filter (fun a => orderOf a = m) univ).card → (filter (fun a => orderOf a = m) univ).card = φ m<VAR>hd : d ∣ Fintype.card α<VAR>hpos : 0 < (filter (fun a => orderOf a = d) univ).card<VAR>hd0 : d ≠ 0<GOAL>(filter (fun a => orderOf a = d) univ).card = φ d
<VAR>α : Type u<VAR>a✝ : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (filter (fun a => a ^ n = 1) univ).card ≤ n<VAR>d : ℕ<VAR>IH : ∀ m < d, m ∣ Fintype.card α → 0 < (filter (fun a => orderOf a = m) univ).card → (filter (fun a => orderOf a = m) univ).card = φ m<VAR>hd : d ∣ Fintype.card α<VAR>hpos : 0 < (filter (fun a => orderOf a = d) univ).card<VAR>hd0 : d ≠ 0<VAR>a : α<VAR>ha' : a ∈ filter (fun a => orderOf a = d) univ<GOAL>(filter (fun a => orderOf a = d) univ).card = φ d
<VAR>α : Type u<VAR>a✝ : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (filter (fun a => a ^ n = 1) univ).card ≤ n<VAR>d : ℕ<VAR>IH : ∀ m < d, m ∣ Fintype.card α → 0 < (filter (fun a => orderOf a = m) univ).card → (filter (fun a => orderOf a = m) univ).card = φ m<VAR>hd : d ∣ Fintype.card α<VAR>hpos : 0 < (filter (fun a => orderOf a = d) univ).card<VAR>hd0 : d ≠ 0<VAR>a : α<VAR>ha' : a ∈ filter (fun a => orderOf a = d) univ<VAR>ha : orderOf a = d<GOAL>(filter (fun a => orderOf a = d) univ).card = φ d
<VAR>α : Type u<VAR>a✝ : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (filter (fun a => a ^ n = 1) univ).card ≤ n<VAR>d : ℕ<VAR>IH : ∀ m < d, m ∣ Fintype.card α → 0 < (filter (fun a => orderOf a = m) univ).card → (filter (fun a => orderOf a = m) univ).card = φ m<VAR>hd : d ∣ Fintype.card α<VAR>hpos : 0 < (filter (fun a => orderOf a = d) univ).card<VAR>hd0 : d ≠ 0<VAR>a : α<VAR>ha' : a ∈ filter (fun a => orderOf a = d) univ<VAR>ha : orderOf a = d<VAR>h1 : ∑ m ∈ d.properDivisors, (filter (fun a => orderOf a = m) univ).card = ∑ m ∈ d.properDivisors, φ m<GOAL>(filter (fun a => orderOf a = d) univ).card = φ d
<VAR>α : Type u<VAR>a✝ : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (filter (fun a => a ^ n = 1) univ).card ≤ n<VAR>d : ℕ<VAR>IH : ∀ m < d, m ∣ Fintype.card α → 0 < (filter (fun a => orderOf a = m) univ).card → (filter (fun a => orderOf a = m) univ).card = φ m<VAR>hd : d ∣ Fintype.card α<VAR>hpos : 0 < (filter (fun a => orderOf a = d) univ).card<VAR>hd0 : d ≠ 0<VAR>a : α<VAR>ha' : a ∈ filter (fun a => orderOf a = d) univ<VAR>ha : orderOf a = d<VAR>h1 : ∑ m ∈ d.properDivisors, (filter (fun a => orderOf a = m) univ).card = ∑ m ∈ d.properDivisors, φ m<VAR>h2 : ∑ m ∈ d.divisors, (filter (fun a => orderOf a = m) univ).card = ∑ m ∈ d.divisors, φ m<GOAL>(filter (fun a => orderOf a = d) univ).card = φ d
<VAR>m n k : ℕ<GOAL>(m * n).lcm (m * k) = m * n.lcm k
<VAR>m n k : ℕ<GOAL>(m * n).lcm (m * k) ∣ m * n.lcm k
<VAR>m n k : ℕ<GOAL>m * n.lcm k ∣ (m * n).lcm (m * k)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>m : Matrix n n R[X]<VAR>i j : n<VAR>k : ℕ<GOAL>k ∈ (m i j).support → k ∈ (matPolyEquiv m).support
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>m : Matrix n n R[X]<VAR>i j : n<VAR>k : ℕ<GOAL>k ∉ (matPolyEquiv m).support → k ∉ (m i j).support
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>m : Matrix n n R[X]<VAR>i j : n<VAR>k : ℕ<GOAL>(matPolyEquiv m).coeff k = 0 → (m i j).coeff k = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>m : Matrix n n R[X]<VAR>i j : n<VAR>k : ℕ<VAR>hk : (matPolyEquiv m).coeff k = 0<GOAL>(m i j).coeff k = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>m : Matrix n n R[X]<VAR>i j : n<VAR>k : ℕ<VAR>hk : (matPolyEquiv m).coeff k = 0<GOAL>0 i j = 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>inst✝² : DivisionSemiring α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSemiring α<VAR>f g : ι → α<VAR>a a₁ a₂ : α<VAR>h : HasSum f a<VAR>b : α<GOAL>HasSum (fun i => f i / b) (a / b)
<VAR>f✝ f : ℝ → ℝ<VAR>hf : GrowsPolynomially (-f)<GOAL>GrowsPolynomially f
<VAR>f✝ f : ℝ → ℝ<VAR>hf : GrowsPolynomially (-f)<GOAL>GrowsPolynomially (- -f)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs_m : MeasurableSet s<VAR>hf_int : Integrable f μ<GOAL>μ.restrict s[f|m] =ᶠ[ae (μ.restrict s)] μ[f|m]
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs_m : MeasurableSet s<VAR>hf_int : Integrable f μ<VAR>this : SigmaFinite ((μ.restrict s).trim hm)<GOAL>μ.restrict s[f|m] =ᶠ[ae (μ.restrict s)] μ[f|m]