ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : Fintype α<VAR>s t : Finset α<VAR>f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)<VAR>this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)<GOAL>(filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) (univ ×ˢ t ×ˢ t)).card = (univ ×ˢ t ×ˢ t).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : Fintype α<VAR>s t : Finset α<VAR>f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)<VAR>this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)<GOAL>(filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) (univ ×ˢ t ×ˢ t)).card = (image f (univ ×ˢ t ×ˢ t)).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : Fintype α<VAR>s t : Finset α<VAR>f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)<VAR>this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)<VAR>a : (α × α) × α × α<GOAL>a ∈ filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) (univ ×ˢ t ×ˢ t) ↔ a ∈ image f (univ ×ˢ t ×ˢ t)
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : Fintype α<VAR>s t : Finset α<VAR>f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)<VAR>this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)<VAR>a : (α × α) × α × α<GOAL>(a.2.1 ∈ t ∧ a.2.2 ∈ t) ∧ a.1.1 * a.2.1 = a.1.2 * a.2.2 ↔ ∃ a_1 a_2 b, (a_2 ∈ t ∧ b ∈ t) ∧ f (a_1, a_2, b) = a
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : Fintype α<VAR>s t : Finset α<VAR>f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)<VAR>this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)<VAR>a : (α × α) × α × α<GOAL>(∃ a_1 a_2 b, (a_2 ∈ t ∧ b ∈ t) ∧ f (a_1, a_2, b) = a) → (a.2.1 ∈ t ∧ a.2.2 ∈ t) ∧ a.1.1 * a.2.1 = a.1.2 * a.2.2
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : Fintype α<VAR>s t : Finset α<VAR>f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)<VAR>this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)<VAR>b c d : α<VAR>hcd : c ∈ t ∧ d ∈ t<GOAL>((f (b, c, d)).2.1 ∈ t ∧ (f (b, c, d)).2.2 ∈ t) ∧ (f (b, c, d)).1.1 * (f (b, c, d)).2.1 = (f (b, c, d)).1.2 * (f (b, c, d)).2.2
<VAR>X Y : Scheme<VAR>U✝ : X.Opens<VAR>hU : IsAffineOpen U✝<VAR>f✝ : ↑Γ(X, U✝)<VAR>f : X.Hom Y<VAR>H : IsOpenImmersion f<VAR>U : X.Opens<GOAL>IsAffineOpen (f ''ᵁ U) ↔ IsAffineOpen U
<VAR>X Y : Scheme<VAR>U✝ : X.Opens<VAR>hU✝ : IsAffineOpen U✝<VAR>f✝ : ↑Γ(X, U✝)<VAR>f : X.Hom Y<VAR>H : IsOpenImmersion f<VAR>U : X.Opens<VAR>hU : IsAffineOpen (f ''ᵁ U)<GOAL>Set.range ⇑(X.ofRestrict ⋯ ≫ f).val.base = Set.range ⇑(Y.ofRestrict ⋯).val.base
<VAR>X Y : Scheme<VAR>U✝ : X.Opens<VAR>hU✝ : IsAffineOpen U✝<VAR>f✝ : ↑Γ(X, U✝)<VAR>f : X.Hom Y<VAR>H : IsOpenImmersion f<VAR>U : X.Opens<VAR>hU : IsAffineOpen (f ''ᵁ U)<GOAL>IsIso (IsOpenImmersion.isoOfRangeEq (X.ofRestrict ⋯ ≫ f) (Y.ofRestrict ⋯) ?refine_1).hom
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>I : R →+* R<VAR>B F : M →ₗ[R] M →ₛₗ[I] M₃<VAR>B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃<VAR>B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] M₃<VAR>f f'✝ : M →ₗ[R] M₁<VAR>g g'✝ : M₁ →ₗ[R] M<VAR>f' : M₁ →ₗ[R] M₂<VAR>g' : M₂ →ₗ[R] M₁<VAR>h : B.IsAdjointPair B' f g<VAR>h' : B'.IsAdjointPair B'' f' g'<VAR>x✝¹ : M<VAR>x✝ : M₂<GOAL>(B'' ((f' ∘ₗ f) x✝¹)) x✝ = (B x✝¹) ((g ∘ₗ g') x✝)
<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>x y : G<GOAL>Inseparable x y ↔ x / y ∈ closure 1
<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>x y : G<GOAL>Inseparable ((Homeomorph.mulRight y⁻¹) x) ((Homeomorph.mulRight y⁻¹) y) ↔ Inseparable (x / y) 1
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>ι' : Sort u_3<VAR>inst✝ : LinearOrder α<VAR>Ixx : α → α → Set α<VAR>p : α → α → Prop<VAR>Hne : ∀ {a b : α}, (Ixx a b).Nonempty → p a b<VAR>Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)<VAR>s t : Set α<VAR>l₁ : α<VAR>hls₁ : l₁ ∈ s<VAR>u₁ : α<VAR>hut₁ : u₁ ∈ t<VAR>left✝¹ : p l₁ u₁<VAR>l₂ : α<VAR>hls₂ : l₂ ∈ s<VAR>u₂ : α<VAR>hut₂ : u₂ ∈ t<VAR>left✝ : p l₂ u₂<GOAL>(Ixx (max l₁ l₂) (min u₁ u₂)).Nonempty → Ixx (max l₁ l₂) (min u₁ u₂) ∈ {S | ∃ l ∈ s, ∃ u ∈ t, p l u ∧ Ixx l u = S}
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)<VAR>i : ι<GOAL>biprod.inl.f i ≫ biprod.snd.f i = 0
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a b : α<GOAL>(a == b) = decide (a = b)
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a b : α<GOAL>(a == b) = decide ((a == b) = true)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>x y : α<GOAL>x ≤ y ↔ TransGen (fun x x_1 => x ⩿ x_1) x y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>x y : α<VAR>h : TransGen (fun x x_1 => x ⩿ x_1) x y<GOAL>x ≤ y
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<VAR>v' : Fin 0 → M<GOAL>Realize (Formula.iExs f φ) v v' ↔ ∃ i, φ.Realize fun a => Sum.elim v i (f a)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<VAR>v' : Fin 0 → M<GOAL>Realize (Formula.iExs f φ) v v' = (Formula.iExs f φ).Realize v
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<VAR>v' : Fin 0 → M<GOAL>v' = default
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>X Y : C<VAR>inst✝¹ : Simple Y<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<VAR>w : IsIso f → False<GOAL>f = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>m M N : ℕ<VAR>i : (n : ℕ) × (Fin n → ℕ)<GOAL>i ∈ compPartialSumSource m M N ↔ (m ≤ i.fst ∧ i.fst < M) ∧ ∀ (a : Fin i.fst), 1 ≤ i.snd a ∧ i.snd a < N
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a b : α<VAR>inst✝ : DecidableEq α<VAR>ha : a ∈ 𝓒 u v s<GOAL>compress u v a ∈ 𝓒 u v s
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a b : α<VAR>inst✝ : DecidableEq α<VAR>ha : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a<GOAL>compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a b : α<VAR>inst✝ : DecidableEq α<VAR>ha : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a<GOAL>compress u v a ∈ s ∧ compress u v a ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p q : Submodule R M<GOAL>Subsingleton ↥p ↔ p = ⊥
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p q : Submodule R M<GOAL>(∀ (x y : ↥p), x = y) ↔ ∀ x ∈ p, x = 0
<VAR>K✝ : Type uK<VAR>inst✝⁸ : Field K✝<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁷ : AddCommGroup V₁<VAR>inst✝⁶ : Module K✝ V₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module K✝ V₂<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>W : Subspace K (Dual K V)<VAR>inst✝ : FiniteDimensional K V<GOAL>Submodule.map (Dual.eval K V) (Submodule.dualCoannihilator W) = Submodule.dualAnnihilator W
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>hf : 1 < f<GOAL>∃ i ∈ Finset.univ, 1 < f i
<VAR>R : Type u_1<VAR>inst✝¹² : Semiring R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommMonoid N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>N' : Type u_6<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>m : MultilinearMap R (fun x => M) N'<VAR>v : ι → M<VAR>i j : ι<VAR>i_ne_j : i ≠ j<VAR>hv : v i = v j<GOAL>(∑ σ : Perm ι, Perm.sign σ • domDomCongr σ m) v = 0
<VAR>R : Type u_1<VAR>inst✝¹² : Semiring R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommMonoid N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>N' : Type u_6<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>m : MultilinearMap R (fun x => M) N'<VAR>v : ι → M<VAR>i j : ι<VAR>i_ne_j : i ≠ j<VAR>hv : v i = v j<GOAL>∑ a : Perm ι, (Perm.sign a • domDomCongr a m) v = 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>ha : ¬a = 0<GOAL>(fun x => x * a⁻¹) ⁻¹' [[b, c]] = (fun x => x / a) ⁻¹' [[b, c]]
<VAR>α : Type u<VAR>ι : Type v<VAR>a : Cardinal.{u}<VAR>inst✝¹ : Countable ι<VAR>f : ι → Set α<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i<VAR>h'f : ∀ (i : ι), #↑(f i) = a<GOAL>#α = a
<VAR>α : Type u<VAR>ι : Type v<VAR>a : Cardinal.{u}<VAR>inst✝¹ : Countable ι<VAR>f : ι → Set α<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i<VAR>h'f : ∀ (i : ι), #↑(f i) = a<GOAL>#α ≤ a
<VAR>α : Type u<VAR>ι : Type v<VAR>a : Cardinal.{u}<VAR>inst✝¹ : Countable ι<VAR>f : ι → Set α<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i<VAR>h'f : ∀ (i : ι), #↑(f i) = a<GOAL>a ≤ #α
<VAR>x : ℝ<VAR>lx : Liouville x<VAR>f : ℤ[X]<VAR>f0 : f ≠ 0<VAR>ef0 : (aeval x) f = 0<GOAL>False
<VAR>x : ℝ<VAR>lx : Liouville x<VAR>f : ℤ[X]<VAR>f0 : f ≠ 0<VAR>ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0<GOAL>False
<VAR>x : ℝ<VAR>lx : Liouville x<VAR>f : ℤ[X]<VAR>f0 : f ≠ 0<VAR>ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0<VAR>A : ℝ<VAR>hA : 0 < A<VAR>h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)<GOAL>False
<VAR>x : ℝ<VAR>lx : Liouville x<VAR>f : ℤ[X]<VAR>f0 : f ≠ 0<VAR>ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0<VAR>A : ℝ<VAR>hA : 0 < A<VAR>h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)<VAR>r : ℕ<VAR>hn : A < (1 + 1) ^ r<GOAL>False
<VAR>x : ℝ<VAR>lx : Liouville x<VAR>f : ℤ[X]<VAR>f0 : f ≠ 0<VAR>ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0<VAR>A : ℝ<VAR>hA : 0 < A<VAR>h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)<VAR>r : ℕ<VAR>hn : A < (1 + 1) ^ r<VAR>a b : ℤ<VAR>b1 : 1 < b<VAR>a1 : |x - ↑a / ↑b| < 1 / ↑b ^ (r + f.natDegree)<GOAL>False
<VAR>x : ℝ<VAR>lx : Liouville x<VAR>f : ℤ[X]<VAR>f0 : f ≠ 0<VAR>ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0<VAR>A : ℝ<VAR>hA : 0 < A<VAR>h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)<VAR>r : ℕ<VAR>hn : A < (1 + 1) ^ r<VAR>a b : ℤ<VAR>b1 : 1 < b<VAR>a1 : |x - ↑a / ↑b| < 1 / ↑b ^ (r + f.natDegree)<VAR>b0 : 0 < ↑b<GOAL>False
<VAR>x : ℝ<VAR>lx : Liouville x<VAR>f : ℤ[X]<VAR>f0 : f ≠ 0<VAR>ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0<VAR>A : ℝ<VAR>hA : 0 < A<VAR>h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)<VAR>r : ℕ<VAR>hn : A < (1 + 1) ^ r<VAR>a b : ℤ<VAR>b1 : 1 < b<VAR>a1 : |x - ↑a / ↑b| < 1 / ↑b ^ (r + f.natDegree)<VAR>b0 : 0 < ↑b<GOAL>↑b ^ f.natDegree * |x - ↑a / ↑b| < ↑b ^ f.natDegree * |x - ↑a / ↑b|
<VAR>x : ℝ<VAR>lx : Liouville x<VAR>f : ℤ[X]<VAR>f0 : f ≠ 0<VAR>ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0<VAR>A : ℝ<VAR>hA : 0 < A<VAR>h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)<VAR>r : ℕ<VAR>hn : A < (1 + 1) ^ r<VAR>a b : ℤ<VAR>b1 : 1 < b<VAR>a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1<VAR>b0 : 0 < ↑b<GOAL>↑b ^ f.natDegree * |x - ↑a / ↑b| < ↑b ^ f.natDegree * |x - ↑a / ↑b|
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>p : ι → Submodule R N<GOAL>Independent p ↔ ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>p : ι → Submodule R N<GOAL>(∀ (i : ι), ∀ x ∈ p i, ∀ (x_1 : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i x_1) = x → x = 0) ↔ ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>p : ι → Submodule R N<VAR>i : ι<GOAL>(∀ (x : ↥(p i)) (x_1 : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i x_1) = ↑x → ↑x = 0) ↔ ∀ (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
<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<GOAL>(monomial s) a = C a * s.prod fun n e => X n ^ e
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → 𝕜<VAR>g : 𝕜 → E<VAR>x : 𝕜<VAR>m : ℕ<VAR>hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x<VAR>n : ℕ<VAR>hg : AnalyticAt 𝕜 (fun z => (z - x) ^ n • g z) x<GOAL>AnalyticAt 𝕜 (fun z => (z - x) ^ (m + n) • (f • g) z) x
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → 𝕜<VAR>g : 𝕜 → E<VAR>x : 𝕜<VAR>m : ℕ<VAR>hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x<VAR>n : ℕ<VAR>hg : AnalyticAt 𝕜 (fun z => (z - x) ^ n • g z) x<VAR>z : 𝕜<GOAL>(z - x) ^ (m + n) • (f • g) z = ((z - x) ^ m • f z) • (z - x) ^ n • g z
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CommMonoid M<VAR>f : α → M<VAR>a✝ b : α<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>a : α<GOAL>(∏ x ∈ Iio a, f x) * f a = ∏ x ∈ Iic a, f x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>inst✝ : l.NeBot<GOAL>Tendsto (fun x => f x * r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q✝ r : R[X]<VAR>n : ℕ<VAR>p q : R[X]<VAR>qn : q.natDegree ≤ n<GOAL>(p + q).natDegree ≤ n ↔ p.natDegree ≤ n
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q✝ r : R[X]<VAR>n : ℕ<VAR>p q : R[X]<VAR>qn : q.natDegree ≤ n<VAR>h : (p + q).natDegree ≤ n<GOAL>p.natDegree ≤ n
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m✝ n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q✝ r : R[X]<VAR>n : ℕ<VAR>p q : R[X]<VAR>qn : q.natDegree ≤ n<VAR>h : (p + q).natDegree ≤ n<VAR>m : ℕ<VAR>hm : n < m<GOAL>p.coeff m = 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m✝ n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q✝ r : R[X]<VAR>n : ℕ<VAR>p q : R[X]<VAR>qn : q.natDegree ≤ n<VAR>h : (p + q).natDegree ≤ n<VAR>m : ℕ<VAR>hm : n < m<GOAL>p.coeff m = (p + q).coeff m
<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>S : Type v<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : Nontrivial R<VAR>x y : R[X]<VAR>h : x * 0 + y * derivative 0 = 1<GOAL>False
<VAR>z : ℂ<GOAL>|z.im| < abs z ↔ z.re ≠ 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<GOAL>W'.Nonsingular P ↔ W'.Equation P ∧ (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4) ≠ 0 ∨ 2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3 ≠ 0 ∨ W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 - (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5) ≠ 0)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∀ᵐ (ω : Ω), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| < ε * ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>c_pos : 0 < c<GOAL>∀ᵐ (ω : Ω), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| < ε * ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>c_pos : 0 < c<VAR>hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ<GOAL>∀ᵐ (ω : Ω), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| < ε * ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>c_pos : 0 < c<VAR>hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ<VAR>A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)<GOAL>∀ᵐ (ω : Ω), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| < ε * ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>c_pos : 0 < c<VAR>hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ<VAR>A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)<VAR>Y : ℕ → Ω → ℝ := fun n => truncation (X n) ↑n<VAR>S : ℕ → Ω → ℝ := fun n => ∑ i ∈ range n, Y i<VAR>hS : S = fun n => ∑ i ∈ range n, Y i<VAR>u : ℕ → ℕ := fun n => ⌊c ^ n⌋₊<GOAL>∀ᵐ (ω : Ω), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (range ⌊c ^ n⌋₊).sum Y a| < ε * ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>c_pos : 0 < c<VAR>hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ<VAR>A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)<VAR>Y : ℕ → Ω → ℝ := fun n => truncation (X n) ↑n<VAR>S : ℕ → Ω → ℝ := fun n => ∑ i ∈ range n, Y i<VAR>hS : S = fun n => ∑ i ∈ range n, Y i<VAR>u : ℕ → ℕ := fun n => ⌊c ^ n⌋₊<VAR>u_mono : Monotone u<GOAL>∀ᵐ (ω : Ω), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (range ⌊c ^ n⌋₊).sum Y a| < ε * ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>c_pos : 0 < c<VAR>hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ<VAR>A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)<VAR>Y : ℕ → Ω → ℝ := fun n => truncation (X n) ↑n<VAR>S : ℕ → Ω → ℝ := fun n => ∑ i ∈ range n, Y i<VAR>hS : S = fun n => ∑ i ∈ range n, Y i<VAR>u : ℕ → ℕ := fun n => ⌊c ^ n⌋₊<VAR>u_mono : Monotone u<VAR>I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * variance (Y j) ℙ ≤ 2 * ∫ (a : Ω), X 0 a<GOAL>∀ᵐ (ω : Ω), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (range ⌊c ^ n⌋₊).sum Y a| < ε * ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>c_pos : 0 < c<VAR>hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ<VAR>A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)<VAR>Y : ℕ → Ω → ℝ := fun n => truncation (X n) ↑n<VAR>S : ℕ → Ω → ℝ := fun n => ∑ i ∈ range n, Y i<VAR>hS : S = fun n => ∑ i ∈ range n, Y i<VAR>u : ℕ → ℕ := fun n => ⌊c ^ n⌋₊<VAR>u_mono : Monotone u<VAR>I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * variance (Y j) ℙ ≤ 2 * ∫ (a : Ω), X 0 a<VAR>C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)<VAR>I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * variance (S (u i)) ℙ ≤ C<VAR>I3 : ∀ (N : ℕ), ∑ i ∈ range N, ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} ≤ ENNReal.ofReal (ε⁻¹ ^ 2 * C)<GOAL>∀ᵐ (ω : Ω), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (range ⌊c ^ n⌋₊).sum Y a| < ε * ↑⌊c ^ n⌋₊