ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁷ : Ring R<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✝ : NoZeroSMulDivisors R M<VAR>h : Module.rank R M = 0<VAR>a✝ : Nontrivial R<GOAL>Finite R M
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁷ : Ring R<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✝ : NoZeroSMulDivisors R M<VAR>h : Subsingleton M<VAR>a✝ : Nontrivial R<GOAL>Finite R M
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} D<VAR>inst✝ : HasWeakSheafify J D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>γ : sheafify J P ⟶ Q<VAR>h : (sheafificationAdjunction J D).unit.app P ≫ γ = η<VAR>γ' : (presheafToSheaf J D).obj P ⟶ { val := Q, cond := hQ } := { val := γ }<GOAL>γ'.val = (((sheafificationAdjunction J D).homEquiv P { val := Q, cond := hQ }).symm η).val
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} D<VAR>inst✝ : HasWeakSheafify J D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>γ : sheafify J P ⟶ Q<VAR>h : (sheafificationAdjunction J D).unit.app P ≫ γ = η<VAR>γ' : (presheafToSheaf J D).obj P ⟶ { val := Q, cond := hQ } := { val := γ }<GOAL>(sheafificationAdjunction J D).unit.app P ≫ (sheafToPresheaf J D).map γ' = η
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<VAR>ha : a ∈ s<GOAL>s = {a} ∨ s.Nontrivial
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<VAR>ha : a ∈ s<GOAL>s.Subsingleton ∨ s.Nontrivial
<VAR>n k : ℕ<VAR>h : 0 < n<GOAL>(n - 1)! * n.ascFactorial k = (n + k - 1)!
<VAR>n k : ℕ<VAR>h : 0 < n<GOAL>n.pred ! * n.ascFactorial k = (n.pred + k)!
<VAR>n k : ℕ<VAR>h : 0 < n<GOAL>n.pred ! * (n - succ 0 + succ 0).ascFactorial k = (n.pred + k)!
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>a / b < 1 ↔ a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>n : ℕ<GOAL>∃ j, μ (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>n : ℕ<VAR>N : ι<VAR>hN : ∀ n_1 ≥ N, μ (s ∩ notConvergentSeq f g n n_1) ∈ Icc (0 - ENNReal.ofReal (ε * 2⁻¹ ^ n)) (0 + ENNReal.ofReal (ε * 2⁻¹ ^ n))<GOAL>∃ j, μ (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>n : ℕ<VAR>N : ι<VAR>hN : ∀ n_1 ≥ N, μ (s ∩ notConvergentSeq f g n n_1) ∈ Icc (0 - ENNReal.ofReal (ε * 2⁻¹ ^ n)) (ENNReal.ofReal (ε * 2⁻¹ ^ n))<GOAL>∃ j, μ (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n)
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>S✝ : Type u_2<VAR>inst✝⁵ : AddCommGroup S✝<VAR>inst✝⁴ : Pow S✝ ℕ<VAR>inst✝³ : Module R S✝<VAR>p q✝ : R[X]<VAR>x : S✝<VAR>S : Type u_3<VAR>inst✝² : NonAssocRing S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>q : ℕ[X]<VAR>n : ℕ<GOAL>q.smeval (-↑n) = ↑(q.smeval (-↑n))
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>S✝ : Type u_2<VAR>inst✝⁵ : AddCommGroup S✝<VAR>inst✝⁴ : Pow S✝ ℕ<VAR>inst✝³ : Module R S✝<VAR>p q✝ : R[X]<VAR>x : S✝<VAR>S : Type u_3<VAR>inst✝² : NonAssocRing S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>q : ℕ[X]<VAR>n : ℕ<GOAL>q.sum (smul_pow (-↑n)) = ↑(q.sum (smul_pow (-↑n)))
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>S✝ : Type u_2<VAR>inst✝⁵ : AddCommGroup S✝<VAR>inst✝⁴ : Pow S✝ ℕ<VAR>inst✝³ : Module R S✝<VAR>p q✝ : R[X]<VAR>x : S✝<VAR>S : Type u_3<VAR>inst✝² : NonAssocRing S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>q : ℕ[X]<VAR>n : ℕ<GOAL>∑ x ∈ q.support, q.coeff x • (-↑n) ^ x = ∑ x ∈ q.support, ↑(q.coeff x • (-↑n) ^ x)
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>S✝ : Type u_2<VAR>inst✝⁵ : AddCommGroup S✝<VAR>inst✝⁴ : Pow S✝ ℕ<VAR>inst✝³ : Module R S✝<VAR>p q✝ : R[X]<VAR>x : S✝<VAR>S : Type u_3<VAR>inst✝² : NonAssocRing S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>q : ℕ[X]<VAR>n : ℕ<GOAL>∀ x ∈ q.support, q.coeff x • (-↑n) ^ x = ↑(q.coeff x • (-↑n) ^ x)
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>S✝ : Type u_2<VAR>inst✝⁵ : AddCommGroup S✝<VAR>inst✝⁴ : Pow S✝ ℕ<VAR>inst✝³ : Module R S✝<VAR>p q✝ : R[X]<VAR>x : S✝<VAR>S : Type u_3<VAR>inst✝² : NonAssocRing S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>q : ℕ[X]<VAR>n k : ℕ<VAR>a✝ : k ∈ q.support<GOAL>q.coeff k • (-↑n) ^ k = ↑(q.coeff k • (-↑n) ^ k)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f✝ f : R →+* S₁<VAR>g : S₁ →+* R<VAR>hf : LeftInverse ⇑f ⇑g<VAR>X : MvPolynomial σ S₁<GOAL>(map f) ((map g) X) = X
<VAR>α✝ : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α✝ × Bool)<VAR>β✝ : Type v<VAR>f : α✝ → β✝<VAR>x✝ y : FreeGroup α✝<VAR>α : Type ?u.60273<VAR>β : Type ?u.60274<VAR>e : α ≃ β<VAR>x : FreeGroup α<GOAL>(map ⇑e.symm) ((map ⇑e) x) = x
<VAR>α✝ : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α✝ × Bool)<VAR>β✝ : Type v<VAR>f : α✝ → β✝<VAR>x✝ y : FreeGroup α✝<VAR>α : Type ?u.60273<VAR>β : Type ?u.60274<VAR>e : α ≃ β<VAR>x : FreeGroup β<GOAL>(map ⇑e) ((map ⇑e.symm) x) = x
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R M<VAR>m : M<VAR>i : ι<GOAL>(b.toDual m) (b i) = (b.repr m) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : α ≃ β<VAR>e' : β ≃ γ<VAR>x✝ : Finset α<VAR>a✝ : γ<GOAL>a✝ ∈ (e.finsetCongr.trans e'.finsetCongr) x✝ ↔ a✝ ∈ (e.trans e').finsetCongr x✝
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : F[X]<VAR>h : ¬f * g = 0<GOAL>(f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : F[X]<VAR>h : ¬f * g = 0<GOAL>(∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b) ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : F[X]<VAR>h : ¬f = 0 ∧ ¬g = 0<GOAL>(∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b) ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : F[X]<VAR>h : ¬f = 0 ∧ ¬g = 0<VAR>H : ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b<VAR>u : F[X]<VAR>hu : Irreducible u<VAR>x✝¹ : u ∣ f<VAR>x✝ : u ∣ g<VAR>v : F[X]<VAR>hf : f = u * v<VAR>w : F[X]<VAR>hg : g = u * w<GOAL>False
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : F[X]<VAR>h : ¬f = 0 ∧ ¬g = 0<GOAL>f = 0 ∧ g = 0 ∨ IsCoprime f g → ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : F[X]<VAR>h : ¬f = 0 ∧ ¬g = 0<VAR>x : AlgebraicClosure F<VAR>hf : f ≠ 0 ∧ (aeval x) f = 0<VAR>hg : g ≠ 0 ∧ (aeval x) g = 0<VAR>u v : F[X]<VAR>hfg : u * f + v * g = 1<GOAL>False
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>num✝ : ℤ<VAR>denom✝ : ℕ<VAR>inv✝¹ inv✝ : Invertible ↑denom✝<GOAL>inv✝¹ = inv✝
<VAR>m✝ n✝ m n : ℕ<VAR>inst✝ : NeZero m<VAR>h : m ≤ n<VAR>a : ZMod m<GOAL>a.cast = 0 ↔ a = 0
<VAR>m✝ n✝ m n : ℕ<VAR>inst✝ : NeZero m<VAR>h : m ≤ n<VAR>a : ZMod m<GOAL>a.cast = cast 0 ↔ a = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype p<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : NonUnitalRing R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : NoZeroDivisors R<VAR>A : Matrix m n R<VAR>v : n → R<GOAL>v ᵥ* (Aᴴ * A) = 0 ↔ v ᵥ* Aᴴ = 0
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a ≤ b * c<VAR>h0 : ¬c = 0<VAR>hinf : ¬c = ⊤<GOAL>a / c ≤ b
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>S : Multiset α<GOAL>((range (card S + 1)).bind fun k => powersetCard k S) = S.powerset
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>a✝ : List α<GOAL>((range (card ⟦a✝⟧ + 1)).bind fun k => powersetCard k ⟦a✝⟧) = powerset ⟦a✝⟧
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>a✝ : List α<GOAL>↑(List.map ofList ((List.range (a✝.length + 1)).bind fun a => sublistsLen a a✝)) = ↑(List.map ofList a✝.sublists')
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : CoheytingAlgebra α<VAR>a : α<GOAL>(￢a) ∆ a = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : CoheytingAlgebra α<VAR>a : α<GOAL>⊤ ≤ ￢a ⊔ a
<VAR>S : ShortComplex Ab<VAR>x : ↑S.X₁<GOAL>S.g (S.f x) = 0
<VAR>S : ShortComplex Ab<VAR>x : ↑S.X₁<GOAL>0 x = 0
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : Zero β✝<VAR>inst✝¹ : Zero γ<VAR>μ : Measure α<VAR>f✝ : α →ₛ β✝<VAR>β : Type u_5<VAR>inst✝ : MonoidWithZero β<VAR>f g : α →ₛ β<VAR>hf : f.FinMeasSupp μ<VAR>hg : g.FinMeasSupp μ<GOAL>(f * g).FinMeasSupp μ
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : Zero β✝<VAR>inst✝¹ : Zero γ<VAR>μ : Measure α<VAR>f✝ : α →ₛ β✝<VAR>β : Type u_5<VAR>inst✝ : MonoidWithZero β<VAR>f g : α →ₛ β<VAR>hf : f.FinMeasSupp μ<VAR>hg : g.FinMeasSupp μ<GOAL>(map (fun p => p.1 * p.2) (f.pair g)).FinMeasSupp μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrable f μ<GOAL>AEStronglyMeasurable f μ
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x₁ x₂ y₁ L : R<GOAL>evalEval (W.addX x₁ x₂ L) (L * (W.addX x₁ x₂ L - x₁) + y₁) (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) = 0 ↔ eval (W.addX x₁ x₂ L) (eval (C L * (X - C x₁) + C y₁) (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆))) = 0
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>x : M<GOAL>(ι R) x = 0 ↔ x = 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>b : β i<VAR>h : b ≠ 0<VAR>j : ι<GOAL>j ∈ (update i f b).support ↔ j ∈ insert i f.support
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>b : β i<VAR>h : b ≠ 0<GOAL>i ∈ (update i f b).support ↔ i ∈ insert i f.support
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>b : β i<VAR>h : b ≠ 0<VAR>j : ι<VAR>hi : i ≠ j<GOAL>j ∈ (update i f b).support ↔ j ∈ insert i f.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : AddGroup β<VAR>h : Antiperiodic f c<VAR>n : ℤ<GOAL>f (x + n • c) = ↑n.negOnePow • f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : AddGroup β<VAR>h : Antiperiodic f c<VAR>k : ℤ<GOAL>f (x + (2 * k) • c) = ↑(2 * k).negOnePow • f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : AddGroup β<VAR>h : Antiperiodic f c<VAR>k : ℤ<GOAL>f (x + (2 * k + 1) • c) = ↑(2 * k + 1).negOnePow • f x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>m n m' : M<VAR>f : m ⟶ m'<VAR>X : C<GOAL>(F.obj n).map ((F.map f).app X) ≫ (F.μ m' n).app X = (F.μ m n).app X ≫ (F.map (f ▷ n)).app X
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>m n m' : M<VAR>f : m ⟶ m'<VAR>X : C<GOAL>(F.obj n).map ((F.map f).app X) ≫ (F.μ m' n).app X = (F.map (𝟙 n)).app ((F.obj m).obj X) ≫ (F.obj n).map ((F.map f).app X) ≫ (F.μ m' n).app X
<VAR>R✝ : Type u_1<VAR>inst✝⁵ : Semiring R✝<VAR>r : R✝<VAR>p✝ : R✝[X]<VAR>S✝ : Type u_2<VAR>inst✝⁴ : AddCommMonoid S✝<VAR>inst✝³ : Pow S✝ ℕ<VAR>inst✝² : MulActionWithZero R✝ S✝<VAR>x✝ : S✝<VAR>R : Type u_3<VAR>inst✝¹ : Semiring R<VAR>S : Type u_4<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>x : S<VAR>this : Module R S := f.toModule<GOAL>eval₂ f x p = p.smeval x
<VAR>R✝ : Type u_1<VAR>inst✝⁵ : Semiring R✝<VAR>r : R✝<VAR>p✝ : R✝[X]<VAR>S✝ : Type u_2<VAR>inst✝⁴ : AddCommMonoid S✝<VAR>inst✝³ : Pow S✝ ℕ<VAR>inst✝² : MulActionWithZero R✝ S✝<VAR>x✝ : S✝<VAR>R : Type u_3<VAR>inst✝¹ : Semiring R<VAR>S : Type u_4<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>x : S<VAR>this : Module R S := f.toModule<GOAL>(p.sum fun e a => f a * x ^ e) = p.sum (smul_pow x)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>f : F[X]<VAR>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>hm : f.Monic<VAR>hi : Irreducible f<VAR>h : f.natSepDegree = 1<GOAL>∃ n y, (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = X ^ q ^ n - C y
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>f : F[X]<VAR>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>hm : f.Monic<VAR>hi : Irreducible f<VAR>h : f.natSepDegree = 1<VAR>n : ℕ<VAR>y : F<VAR>hf : f = X ^ q ^ n - C y<GOAL>∃ n y, (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = X ^ q ^ n - C y
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.ψ₂ ^ 2 = C W.Ψ₂Sq + 4 * W.toAffine.polynomial
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → β → α<VAR>S : Set β<VAR>h : UniformEquicontinuousOn F S<GOAL>UniformEquicontinuousOn Subtype.val S
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → β → α<VAR>S : Set β<VAR>h : UniformEquicontinuousOn F S<GOAL>UniformEquicontinuousOn (F ∘ rangeSplitting F) S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<GOAL>rexp 4 < 64
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<GOAL>4 / ↑6 < log 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<GOAL>0 < ↑6
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>h : Fintype.card α ≤ Fintype.card β<GOAL>Nonempty (α ↪ β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hr : r ≠ ⊤<GOAL>∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>F✝ : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α✝<VAR>inst✝⁵ : PseudoEMetricSpace β✝<VAR>inst✝⁴ : FunLike F✝ α✝ β✝<VAR>α : Type u_6<VAR>β : Type u_7<VAR>F : Type u_8<VAR>inst✝³ : PseudoMetricSpace α<VAR>inst✝² : PseudoMetricSpace β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : DilationClass F α β<VAR>f : F<VAR>x y : α<VAR>r : ℝ≥0<VAR>hxy : nndist x y ≠ 0<VAR>hr : nndist (f x) (f y) = r * nndist x y<GOAL>edist x y ≠ 0
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>F✝ : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α✝<VAR>inst✝⁵ : PseudoEMetricSpace β✝<VAR>inst✝⁴ : FunLike F✝ α✝ β✝<VAR>α : Type u_6<VAR>β : Type u_7<VAR>F : Type u_8<VAR>inst✝³ : PseudoMetricSpace α<VAR>inst✝² : PseudoMetricSpace β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : DilationClass F α β<VAR>f : F<VAR>x y : α<VAR>r : ℝ≥0<VAR>hxy : nndist x y ≠ 0<VAR>hr : nndist (f x) (f y) = r * nndist x y<GOAL>edist (f x) (f y) = ↑r * edist x y
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : NoncompactSpace G<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<GOAL>∃ g, Disjoint K (g • L)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : NoncompactSpace G<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>A : ¬K * L⁻¹ = univ<GOAL>∃ g, Disjoint K (g • L)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : NoncompactSpace G<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>A : ¬K * L⁻¹ = univ<VAR>g : G<VAR>hg : g ∉ K * L⁻¹<GOAL>∃ g, Disjoint K (g • L)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : NoncompactSpace G<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>A : ¬K * L⁻¹ = univ<VAR>g : G<VAR>hg : g ∉ K * L⁻¹<GOAL>Disjoint K (g • L)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : NoncompactSpace G<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>A : ¬K * L⁻¹ = univ<VAR>g : G<VAR>hg : g ∉ K * L⁻¹<VAR>a : G<VAR>ha : a ∈ K<VAR>h'a : a ∈ g • L<GOAL>g ∈ K * L⁻¹
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : NoncompactSpace G<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>A : ¬K * L⁻¹ = univ<VAR>g : G<VAR>hg : g ∉ K * L⁻¹<VAR>b : G<VAR>bL : b ∈ L<VAR>ha : (fun x => g • x) b ∈ K<GOAL>g ∈ K * L⁻¹
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : NoncompactSpace G<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>A : ¬K * L⁻¹ = univ<VAR>g : G<VAR>hg : g ∉ K * L⁻¹<VAR>b : G<VAR>bL : b ∈ L<VAR>ha : (fun x => g • x) b ∈ K<GOAL>(fun x x_1 => x * x_1) (g * b) b⁻¹ = g
<GOAL>∀ᶠ (x : ℝ) in residual ℝ, Liouville x
<GOAL>{x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) ∈ residual ℝ
<GOAL>∀ᶠ (x : ℝ) in residual ℝ, x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)
<GOAL>IsGδ {x | (fun x => x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)) x}
<GOAL>range Rat.cast ⊆ {x | (fun x => x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)) x}
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>g₁ : Y₁ ⟶ Z₁<VAR>g₂ : Y₂ ⟶ Z₂<GOAL>tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>g₁ : Y₁ ⟶ Z₁<VAR>g₂ : Y₂ ⟶ Z₂<GOAL>∀ (j : Discrete WalkingPair), tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app j = (tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r : α → α → Prop<VAR>f✝ g : Filter α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : IsDirected β fun x x_1 => x ≤ x_1<VAR>f : α → β<VAR>b : β<VAR>hb : ∀ᶠ (x : β) in map f cofinite, (fun x x_1 => x ≤ x_1) x b<VAR>this : Nonempty β<GOAL>BddAbove (range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r : α → α → Prop<VAR>f✝ g : Filter α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : IsDirected β fun x x_1 => x ≤ x_1<VAR>f : α → β<VAR>b : β<VAR>hb : ∀ᶠ (x : β) in map f cofinite, (fun x x_1 => x ≤ x_1) x b<VAR>this : Nonempty β<GOAL>BddAbove (f '' {x | f x ≤ b}) ∧ BddAbove (f '' {x | f x ≤ b}ᶜ)
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>not_terminatedAt_n : ¬(of v).TerminatedAt n<VAR>g : GenContFract K := of v<VAR>nextConts : Pair K := g.contsAux (n + 2)<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>conts_eq : conts = g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<VAR>pred_conts_eq : pred_conts = g.contsAux n<GOAL>|v - g.convs n| ≤ 1 / (conts.b * nextConts.b)
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>not_terminatedAt_n : ¬(of v).TerminatedAt n<VAR>g : GenContFract K := of v<VAR>nextConts : Pair K := g.contsAux (n + 2)<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>conts_eq : conts = g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<VAR>pred_conts_eq : pred_conts = g.contsAux n<VAR>gp : Pair K<VAR>s_nth_eq : g.s.get? n = some gp<GOAL>|v - g.convs n| ≤ 1 / (conts.b * nextConts.b)