ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>RatFunc.mk p q = { toFractionRing := Localization.mk p ⟨q, ⋯⟩ }
<VAR>xl xr : Type u<VAR>x y z : PGame<VAR>h₁ : x ⧏ y<VAR>h₂ : y ≤ z<GOAL>x ⧏ z
<VAR>xl xr : Type u<VAR>x y z : PGame<VAR>h₁ : ¬y ≤ x<VAR>h₂ : y ≤ z<GOAL>¬z ≤ x
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>𝕜' : Type u_6<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>c' : E →L[𝕜] 𝕜'<VAR>hc : HasFDerivAt c c' x<VAR>f : F<GOAL>HasFDerivAt (fun y => c y • f) (c'.smulRight f) x
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder ι<VAR>inst✝⁵ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝⁴ : Countable ι<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>f : Filtration ι m<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n n' : ι<VAR>hu : Adapted f u<VAR>hs : MeasurableSet s<VAR>i : ι<GOAL>MeasurableSet {ω | hitting u s n n' ω ≤ i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder ι<VAR>inst✝⁵ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝⁴ : Countable ι<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>f : Filtration ι m<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n n' : ι<VAR>hu : Adapted f u<VAR>hs : MeasurableSet s<VAR>i : ι<VAR>hi : n' ≤ i<GOAL>MeasurableSet {ω | hitting u s n n' ω ≤ i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder ι<VAR>inst✝⁵ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝⁴ : Countable ι<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>f : Filtration ι m<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n n' : ι<VAR>hu : Adapted f u<VAR>hs : MeasurableSet s<VAR>i : ι<VAR>hi : i < n'<GOAL>MeasurableSet {ω | hitting u s n n' ω ≤ i}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e₁ : S<VAR>he : e₁ ∈ f.range<VAR>he₁ : IsIdempotentElem e₁<VAR>e₂ : R<VAR>he₂ : IsIdempotentElem e₂<VAR>he₁e₂ : e₁ * f e₂ = 0<VAR>he₂e₁ : f e₂ * e₁ = 0<GOAL>∃ e', IsIdempotentElem e' ∧ f e' = e₁ ∧ e' * e₂ = 0 ∧ e₂ * e' = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e₂ : R<VAR>he₂ : IsIdempotentElem e₂<VAR>e' : R<VAR>h₁ : IsIdempotentElem e'<VAR>h₂ : e' * e₂ = 0<VAR>he : f e' ∈ f.range<VAR>he₁ : IsIdempotentElem (f e')<VAR>he₁e₂ : f e' * f e₂ = 0<VAR>he₂e₁ : f e₂ * f e' = 0<GOAL>∃ e'_1, IsIdempotentElem e'_1 ∧ f e'_1 = f e' ∧ e'_1 * e₂ = 0 ∧ e₂ * e'_1 = 0
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>β : Type u_2<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hd : Pairwise (Disjoint on f)<VAR>hm : ∀ (i : β), P (f i)<GOAL>extend m (⋃ i, f i) = ∑' (i : β), extend m (f i)
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>β : Type u_2<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hd : Pairwise (Disjoint on f)<VAR>hm : ∀ (i : β), P (f i)<VAR>val✝ : Encodable β<GOAL>extend m (⋃ i, f i) = ∑' (i : β), extend m (f i)
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>β : Type u_2<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hd : Pairwise (Disjoint on f)<VAR>hm : ∀ (i : β), P (f i)<VAR>val✝ : Encodable β<GOAL>extend m (⋃ i, ⋃ b ∈ Encodable.decode₂ β i, f b) = ∑' (i : ℕ), extend m (⋃ b ∈ Encodable.decode₂ β i, f b)
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>β : Type u_2<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hd : Pairwise (Disjoint on f)<VAR>hm : ∀ (i : β), P (f i)<VAR>val✝ : Encodable β<GOAL>extend m ∅ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝ : NormedDivisionRing 𝕜<VAR>m : ℤ<VAR>hm : m < 0<GOAL>Tendsto (fun x => ‖x ^ m‖) (𝓝[≠] 0) atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝ : NormedDivisionRing 𝕜<VAR>m : ℤ<VAR>hm : -m < 0<GOAL>Tendsto (fun x => ‖x ^ (-m)‖) (𝓝[≠] 0) atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝ : NormedDivisionRing 𝕜<VAR>m : ℕ<VAR>hm : 0 < ↑m<GOAL>Tendsto (fun x => ‖x ^ (-↑m)‖) (𝓝[≠] 0) atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝ : NormedDivisionRing 𝕜<VAR>m : ℕ<VAR>hm : 0 < m<GOAL>Tendsto (fun x => ‖x ^ (-↑m)‖) (𝓝[≠] 0) atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝ : NormedDivisionRing 𝕜<VAR>m : ℕ<VAR>hm : 0 < m<GOAL>Tendsto (fun x => ‖x⁻¹‖ ^ m) (𝓝[≠] 0) atTop
<VAR>K : Type u<VAR>V : Type v<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Field F<VAR>inst✝¹ : Ring E<VAR>inst✝ : Algebra F E<VAR>hr : finrank F E = 2<VAR>i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))<VAR>h : ⊥ = ⊤<GOAL>False
<VAR>K : Type u<VAR>V : Type v<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Field F<VAR>inst✝¹ : Ring E<VAR>inst✝ : Algebra F E<VAR>hr : finrank F E = 2<VAR>i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))<VAR>S : Subalgebra F E<GOAL>S = ⊥ ∨ S = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Field F<VAR>inst✝¹ : Ring E<VAR>inst✝ : Algebra F E<VAR>hr : finrank F E = 2<VAR>i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))<VAR>S : Subalgebra F E<VAR>this : FiniteDimensional F E<GOAL>S = ⊥ ∨ S = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Field F<VAR>inst✝¹ : Ring E<VAR>inst✝ : Algebra F E<VAR>hr : finrank F E = 2<VAR>i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))<VAR>S : Subalgebra F E<VAR>this✝ : FiniteDimensional F E<VAR>this : FiniteDimensional F ↥S<GOAL>S = ⊥ ∨ S = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Field F<VAR>inst✝¹ : Ring E<VAR>inst✝ : Algebra F E<VAR>hr : finrank F E = 2<VAR>i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))<VAR>S : Subalgebra F E<VAR>this✝¹ : FiniteDimensional F E<VAR>this✝ : FiniteDimensional F ↥S<VAR>this : finrank F ↥S ≤ 2<GOAL>S = ⊥ ∨ S = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Field F<VAR>inst✝¹ : Ring E<VAR>inst✝ : Algebra F E<VAR>hr : finrank F E = 2<VAR>i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))<VAR>S : Subalgebra F E<VAR>this✝² : FiniteDimensional F E<VAR>this✝¹ : FiniteDimensional F ↥S<VAR>this✝ : finrank F ↥S ≤ 2<VAR>this : 0 < finrank F ↥S<GOAL>S = ⊥ ∨ S = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelMonoidWithZero α<VAR>a c d : α<VAR>a_eq : a = a * c * d<VAR>ha0 : ¬a = 0<GOAL>a ~ᵤ a * c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelMonoidWithZero α<VAR>a c d : α<VAR>a_eq : a = a * c * d<VAR>ha0 : ¬a = 0<VAR>hac0 : a * c ≠ 0<GOAL>a ~ᵤ a * c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelMonoidWithZero α<VAR>a c d : α<VAR>a_eq : a = a * c * d<VAR>ha0 : ¬a = 0<VAR>hac0 : a * c ≠ 0<VAR>this : a * (c * d) = a * 1<GOAL>a ~ᵤ a * c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelMonoidWithZero α<VAR>a c d : α<VAR>a_eq : a = a * c * d<VAR>ha0 : ¬a = 0<VAR>hac0 : a * c ≠ 0<VAR>this : a * (c * d) = a * 1<VAR>hcd : c * d = 1<GOAL>a ~ᵤ a * c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelMonoidWithZero α<VAR>a c d : α<VAR>a_eq : a = a * c * d<VAR>ha0 : ¬a = 0<VAR>hac0 : a * c ≠ 0<VAR>this✝ : a * (c * d) = a * 1<VAR>hcd : c * d = 1<VAR>this : a * c * (d * c) = a * c * 1<GOAL>a ~ᵤ a * c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelMonoidWithZero α<VAR>a c d : α<VAR>a_eq : a = a * c * d<VAR>ha0 : ¬a = 0<VAR>hac0 : a * c ≠ 0<VAR>this✝ : a * (c * d) = a * 1<VAR>hcd : c * d = 1<VAR>this : a * c * (d * c) = a * c * 1<VAR>hdc : d * c = 1<GOAL>a ~ᵤ a * c
<VAR>a b m n✝ p n : ℕ<GOAL>n.factorization = 0 ↔ n = 0 ∨ n = 1
<VAR>a b m n✝ p n : ℕ<GOAL>Multiset.toFinsupp ↑n.primeFactorsList = 0 ↔ n = 0 ∨ n = 1
<VAR>k G : Type u<VAR>inst✝² : CommRing k<VAR>inst✝¹ : Group G<VAR>A : Rep k G<VAR>inst✝ : A.IsTrivial<VAR>f : Additive G →+ CoeSort.coe A<VAR>g h : G<GOAL>(⇑f ∘ ⇑Additive.ofMul) (g * h) = (A.ρ g) ((⇑f ∘ ⇑Additive.ofMul) h) + (⇑f ∘ ⇑Additive.ofMul) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>I : Type u<VAR>f : I → Type v<VAR>x✝ y : (i : I) → f i<VAR>i j✝ : I<VAR>inst✝¹ : DecidableEq I<VAR>inst✝ : (i : I) → Group (f i)<VAR>g : (i : I) → f i<VAR>x : f i<VAR>j : I<GOAL>Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>I : Type u<VAR>f : I → Type v<VAR>x✝ y : (i : I) → f i<VAR>i j : I<VAR>inst✝¹ : DecidableEq I<VAR>inst✝ : (i : I) → Group (f i)<VAR>g : (i : I) → f i<VAR>x : f i<GOAL>Function.update g i x i = (g / mulSingle i (g i) * mulSingle i x) i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>I : Type u<VAR>f : I → Type v<VAR>x✝ y : (i : I) → f i<VAR>i j✝ : I<VAR>inst✝¹ : DecidableEq I<VAR>inst✝ : (i : I) → Group (f i)<VAR>g : (i : I) → f i<VAR>x : f i<VAR>j : I<VAR>h : i ≠ j<GOAL>Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s t : Set α<VAR>f : α → β<VAR>a : α<VAR>x✝ : β<GOAL>x✝ ∈ f '' {a} ↔ x✝ ∈ {f a}
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q✝ r : R[X]<VAR>n : ℕ<VAR>p q : R[ℕ]<GOAL>({ toFinsupp := p } * { toFinsupp := q }).coeff n = ∑ x ∈ antidiagonal n, { toFinsupp := p }.coeff x.1 * { toFinsupp := q }.coeff x.2
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q✝ r : R[X]<VAR>n : ℕ<VAR>p q : R[ℕ]<GOAL>(p * q) n = ∑ x ∈ antidiagonal n, p x.1 * q x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Inhabited α<VAR>l✝ : List α<VAR>a : α<VAR>l : List α<GOAL>(a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : Field A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : Nontrivial B<VAR>p : A[X]<VAR>hp1 : Irreducible p<VAR>hp2 : (Polynomial.aeval x) p = 0<GOAL>p * C p.leadingCoeff⁻¹ = minpoly A x
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : Field A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : Nontrivial B<VAR>p : A[X]<VAR>hp1 : Irreducible p<VAR>hp2 : (Polynomial.aeval x) p = 0<VAR>this : p.leadingCoeff ≠ 0<GOAL>p * C p.leadingCoeff⁻¹ = minpoly A x
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : Field A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : Nontrivial B<VAR>p : A[X]<VAR>hp1 : Irreducible p<VAR>hp2 : (Polynomial.aeval x) p = 0<VAR>this : p.leadingCoeff ≠ 0<GOAL>Irreducible (p * C p.leadingCoeff⁻¹)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : Field A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : Nontrivial B<VAR>p : A[X]<VAR>hp1 : Irreducible p<VAR>hp2 : (Polynomial.aeval x) p = 0<VAR>this : p.leadingCoeff ≠ 0<GOAL>(Polynomial.aeval x) (p * C p.leadingCoeff⁻¹) = 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : Field A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : Nontrivial B<VAR>p : A[X]<VAR>hp1 : Irreducible p<VAR>hp2 : (Polynomial.aeval x) p = 0<VAR>this : p.leadingCoeff ≠ 0<GOAL>(p * C p.leadingCoeff⁻¹).Monic
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>x y : R<GOAL>(map W f).toAffine.Nonsingular (f x) (f y) ↔ W.Nonsingular x y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n : ℕ<GOAL>Even n ↔ ¬Odd n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y✝ : E<VAR>s✝ t : Set E<VAR>f : E →ᵃ[𝕜] F<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>y : F<VAR>y' : E<VAR>hy' : y' ∈ s<VAR>hy'f : f y' = y<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>f (a • x + b • y') = a • f x + b • y
<VAR>x✝ y✝ x y : ℝ≥0<GOAL>sqrt (x * y) = sqrt x * sqrt y
<VAR>s : ℝ<VAR>this : ∀ (r : ℝ), ↑r = ↑r<GOAL>∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (↑s - 1) = ↑(∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1))
<VAR>s : ℝ<VAR>this : ∀ (r : ℝ), ↑r = ↑r<GOAL>∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (↑s - 1) = ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x) * x ^ (s - 1))
<VAR>s : ℝ<VAR>this : ∀ (r : ℝ), ↑r = ↑r<GOAL>EqOn (fun x => ↑(rexp (-x)) * ↑x ^ (↑s - 1)) (fun x => ↑(rexp (-x) * x ^ (s - 1))) (Ioi 0)
<VAR>s : ℝ<VAR>this : ∀ (r : ℝ), ↑r = ↑r<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>↑(rexp (-x)) * ↑x ^ (↑s - 1) = ↑(rexp (-x) * x ^ (s - 1))
<VAR>s : ℝ<VAR>this : ∀ (r : ℝ), ↑r = ↑r<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>↑(rexp (-x)) * ↑x ^ (↑s - 1) = ↑(rexp (-x)) * ↑x ^ ↑(s - 1)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(map Prod.fst (μ.prod ν)) s = (ν univ • μ) s
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : (forget C).Corepresentable<VAR>J : Type w<VAR>inst✝¹ : Category.{t, w} J<VAR>G : J ⥤ C<VAR>inst✝ : HasLimit G<GOAL>Small.{v, max v w} ↑(G ⋙ forget C).sections
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : (forget C).Corepresentable<VAR>J : Type w<VAR>inst✝¹ : Category.{t, w} J<VAR>G : J ⥤ C<VAR>inst✝ : HasLimit G<GOAL>HasLimit (G ⋙ forget C)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁ : InfinitePlace K<VAR>B : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<VAR>n m : ℕ<VAR>h : n < m<VAR>w : InfinitePlace K<VAR>hw : w ≠ w₁<GOAL>w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB m)) < w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB n))
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : Group α<VAR>a✝ b✝ a b : α<GOAL>mabs (a / b) = mabs (b / a)
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<GOAL>(filter (fun t => t.1.card < k) (MvPolynomial.NewtonIdentities.pairs σ k)).disjUnion (filter (fun t => t.1.card = k) (MvPolynomial.NewtonIdentities.pairs σ k)) ⋯ = MvPolynomial.NewtonIdentities.pairs σ k
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<GOAL>∀ (a : Finset σ × σ), a ∈ filter (fun a => (a.1.card ≤ k ∧ (a.1.card = k → a.2 ∈ a.1)) ∧ a.1.card < k) univ ∪ filter (fun a => (a.1.card ≤ k ∧ (a.1.card = k → a.2 ∈ a.1)) ∧ a.1.card = k) univ ↔ a ∈ univ ∧ a.1.card ≤ k ∧ (a.1.card = k → a.2 ∈ a.1)
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>a : Finset σ × σ<GOAL>a ∈ filter (fun a => (a.1.card ≤ k ∧ (a.1.card = k → a.2 ∈ a.1)) ∧ a.1.card < k) univ ∪ filter (fun a => (a.1.card ≤ k ∧ (a.1.card = k → a.2 ∈ a.1)) ∧ a.1.card = k) univ ↔ a ∈ univ ∧ a.1.card ≤ k ∧ (a.1.card = k → a.2 ∈ a.1)
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>a : Finset σ × σ<GOAL>a ∈ univ ∧ ((a.1.card ≤ k ∧ (a.1.card = k → a.2 ∈ a.1)) ∧ a.1.card < k ∨ (a.1.card ≤ k ∧ (a.1.card = k → a.2 ∈ a.1)) ∧ a.1.card = k) ↔ a ∈ univ ∧ a.1.card ≤ k ∧ (a.1.card = k → a.2 ∈ a.1)
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>a : Finset σ × σ<VAR>ha : a ∈ univ ∧ a.1.card ≤ k ∧ (a.1.card = k → a.2 ∈ a.1)<GOAL>a ∈ univ ∧ ((a.1.card ≤ k ∧ (a.1.card = k → a.2 ∈ a.1)) ∧ a.1.card < k ∨ (a.1.card ≤ k ∧ (a.1.card = k → a.2 ∈ a.1)) ∧ a.1.card = k)
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>a : Finset σ × σ<VAR>ha : a ∈ univ ∧ a.1.card ≤ k ∧ (a.1.card = k → a.2 ∈ a.1)<VAR>hacard : a.1.card < k ∨ a.1.card = k<GOAL>a ∈ univ ∧ ((a.1.card ≤ k ∧ (a.1.card = k → a.2 ∈ a.1)) ∧ a.1.card < k ∨ (a.1.card ≤ k ∧ (a.1.card = k → a.2 ∈ a.1)) ∧ a.1.card = k)
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>s t : Set α<VAR>h : 𝒜.Countable<VAR>ℬ : Set (Set α) := {s | s ∈ 𝒜} ∪ {s | sᶜ ∈ 𝒜}<GOAL>(generateSetAlgebra 𝒜).Countable
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>s t : Set α<VAR>h : 𝒜.Countable<VAR>ℬ : Set (Set α) := {s | s ∈ 𝒜} ∪ {s | sᶜ ∈ 𝒜}<VAR>count_ℬ : ℬ.Countable<GOAL>(generateSetAlgebra 𝒜).Countable
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>s t : Set α<VAR>h : 𝒜.Countable<VAR>ℬ : Set (Set α) := {s | s ∈ 𝒜} ∪ {s | sᶜ ∈ 𝒜}<VAR>count_ℬ : ℬ.Countable<VAR>f : Set (Set (Set α)) → Set α := fun A => ⋃ a ∈ A, ⋂ t ∈ a, t<VAR>𝒞 : Set (Set (Set α)) := {a | a.Finite ∧ a ⊆ ℬ}<GOAL>(generateSetAlgebra 𝒜).Countable
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>s t : Set α<VAR>h : 𝒜.Countable<VAR>ℬ : Set (Set α) := {s | s ∈ 𝒜} ∪ {s | sᶜ ∈ 𝒜}<VAR>count_ℬ : ℬ.Countable<VAR>f : Set (Set (Set α)) → Set α := fun A => ⋃ a ∈ A, ⋂ t ∈ a, t<VAR>𝒞 : Set (Set (Set α)) := {a | a.Finite ∧ a ⊆ ℬ}<VAR>count_𝒞 : 𝒞.Countable<GOAL>(generateSetAlgebra 𝒜).Countable
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>s t : Set α<VAR>h : 𝒜.Countable<VAR>ℬ : Set (Set α) := {s | s ∈ 𝒜} ∪ {s | sᶜ ∈ 𝒜}<VAR>count_ℬ : ℬ.Countable<VAR>f : Set (Set (Set α)) → Set α := fun A => ⋃ a ∈ A, ⋂ t ∈ a, t<VAR>𝒞 : Set (Set (Set α)) := {a | a.Finite ∧ a ⊆ ℬ}<VAR>count_𝒞 : 𝒞.Countable<VAR>𝒟 : Set (Set (Set (Set α))) := {A | A.Finite ∧ A ⊆ 𝒞}<GOAL>(generateSetAlgebra 𝒜).Countable
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>s t : Set α<VAR>h : 𝒜.Countable<VAR>ℬ : Set (Set α) := {s | s ∈ 𝒜} ∪ {s | sᶜ ∈ 𝒜}<VAR>count_ℬ : ℬ.Countable<VAR>f : Set (Set (Set α)) → Set α := fun A => ⋃ a ∈ A, ⋂ t ∈ a, t<VAR>𝒞 : Set (Set (Set α)) := {a | a.Finite ∧ a ⊆ ℬ}<VAR>count_𝒞 : 𝒞.Countable<VAR>𝒟 : Set (Set (Set (Set α))) := {A | A.Finite ∧ A ⊆ 𝒞}<VAR>count_𝒟 : 𝒟.Countable<GOAL>(generateSetAlgebra 𝒜).Countable
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>s t : Set α<VAR>h : 𝒜.Countable<VAR>ℬ : Set (Set α) := {s | s ∈ 𝒜} ∪ {s | sᶜ ∈ 𝒜}<VAR>count_ℬ : ℬ.Countable<VAR>f : Set (Set (Set α)) → Set α := fun A => ⋃ a ∈ A, ⋂ t ∈ a, t<VAR>𝒞 : Set (Set (Set α)) := {a | a.Finite ∧ a ⊆ ℬ}<VAR>count_𝒞 : 𝒞.Countable<VAR>𝒟 : Set (Set (Set (Set α))) := {A | A.Finite ∧ A ⊆ 𝒞}<VAR>count_𝒟 : 𝒟.Countable<VAR>this : generateSetAlgebra 𝒜 ⊆ f '' 𝒟<GOAL>(generateSetAlgebra 𝒜).Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝¹ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝ : Finite ι<VAR>s : (i : ι) → Set (π i)<VAR>x : (i : ι) → π i<GOAL>𝓝[univ.pi s] x = ⨅ i, comap (fun x => x i) (𝓝[s i] x i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : Preorder β<VAR>f : α → β<GOAL>Monotone f ↔ ∀ (a b : α), a ⋖ b → f a ≤ f b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>h : ∀ (a b : α), a ⋖ b → f a ≤ f b<VAR>a b : α<VAR>hab : a ≤ b<GOAL>f a ≤ f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(μ + ν).toSignedMeasure i = ↑(μ.toSignedMeasure + ν.toSignedMeasure) i
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasBinaryProducts C<VAR>f : X ⟶ Y<GOAL>(leftUnitor X).inv ≫ map (𝟙 (⊤_ C)) f = f ≫ (leftUnitor Y).inv
<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝² : Monoid α✝<VAR>inst✝¹ : Monoid β<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>a b : α<VAR>x✝ : IsConj a b<VAR>c : αˣ<VAR>hc : SemiconjBy (↑c) a b<GOAL>a = b
<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝² : Monoid α✝<VAR>inst✝¹ : Monoid β<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>a b : α<VAR>x✝ : IsConj a b<VAR>c : αˣ<VAR>hc : a = b<GOAL>a = b
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>𝕜✝ : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : TopologicalSpace β✝<VAR>f✝ g : α → β✝<VAR>𝕜 : Type u_4<VAR>β : Type u_5<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : InnerProductSpace 𝕜 β<VAR>f : α → β<VAR>c : β<VAR>f' : α → β<VAR>hf'_meas : StronglyMeasurable f'<VAR>hf_ae : f =ᶠ[ae μ] f'<GOAL>AEStronglyMeasurable' m (fun x => ⟪c, f x⟫_𝕜) μ
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>𝕜✝ : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : TopologicalSpace β✝<VAR>f✝ g : α → β✝<VAR>𝕜 : Type u_4<VAR>β : Type u_5<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : InnerProductSpace 𝕜 β<VAR>f : α → β<VAR>c : β<VAR>f' : α → β<VAR>hf'_meas : StronglyMeasurable f'<VAR>hf_ae : f =ᶠ[ae μ] f'<VAR>x : α<VAR>hx : f x = f' x<GOAL>(fun x => ⟪c, f x⟫_𝕜) x = (fun x => ⟪c, f' x⟫_𝕜) x
<VAR>n : ℕ<GOAL>IsSquare ↑n ↔ IsSquare n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁵ : OrderedRing 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>f : E →ᵃ[𝕜] F<VAR>a b : E<VAR>x : F<GOAL>x ∈ ⇑f '' [a-[𝕜]b] ↔ x ∈ [f a-[𝕜]f b]
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ X Y : C<VAR>h : IsInitial X<VAR>c : BinaryCofan X Y<GOAL>Nonempty (IsColimit c) ↔ IsIso c.inr
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ X Y : C<VAR>h : IsInitial X<VAR>c : BinaryCofan X Y<GOAL>Nonempty (IsColimit c) ↔ Nonempty (IsColimit (mk c.inr c.inl))