ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x₁ x₂ y₁ L : R<VAR>hx' : W.Equation (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L)<VAR>hx : W.a₁ * (L * (W.addX x₁ x₂ L - x₁) + y₁) - (3 * W.addX x₁ x₂ L ^ 2 + 2 * W.a₂ * W.addX x₁ x₂ L + W.a₄) = 0 ∧ 2 * (L * (W.addX x₁ x₂ L - x₁) + y₁) + (W.a₁ * W.addX x₁ x₂ L + W.a₃) = 0<GOAL>eval (W.addX x₁ x₂ L) (derivative ((C L * (X - C x₁) + C y₁) ^ 2 + (C W.a₁ * X + C W.a₃) * (C L * (X - C x₁) + C y₁) - (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆))) = 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x₁ x₂ y₁ L : R<VAR>hx' : W.Equation (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L)<VAR>hx : W.a₁ * (L * (W.addX x₁ x₂ L - x₁) + y₁) - (3 * W.addX x₁ x₂ L ^ 2 + 2 * W.a₂ * W.addX x₁ x₂ L + W.a₄) = 0 ∧ 2 * (L * (W.addX x₁ x₂ L - x₁) + y₁) + (W.a₁ * W.addX x₁ x₂ L + W.a₃) = 0<GOAL>eval (W.addX x₁ x₂ L) (C 2 * (C L * (X - C x₁) + C y₁) * (0 * (X - C x₁) + C L * (1 - 0) + 0) + ((0 * X + C W.a₁ * 1 + 0) * (C L * (X - C x₁) + C y₁) + (C W.a₁ * X + C W.a₃) * (0 * (X - C x₁) + C L * (1 - 0) + 0)) - (C ↑3 * X ^ (3 - 1) + (0 * X ^ 2 + C W.a₂ * (C 2 * X * 1)) + (0 * X + C W.a₄ * 1) + 0)) = 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x₁ x₂ y₁ L : R<VAR>hx' : W.Equation (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L)<VAR>hx : W.a₁ * (L * (W.addX x₁ x₂ L - x₁) + y₁) - (3 * W.addX x₁ x₂ L ^ 2 + 2 * W.a₂ * W.addX x₁ x₂ L + W.a₄) = 0 ∧ 2 * (L * (W.addX x₁ x₂ L - x₁) + y₁) + (W.a₁ * W.addX x₁ x₂ L + W.a₃) = 0<GOAL>eval (W.addX x₁ x₂ L) (C 2 * (C L * (X - C x₁) + C y₁) * C L + (C W.a₁ * (C L * (X - C x₁) + C y₁) + (C W.a₁ * X + C W.a₃) * C L) - (C ↑3 * X ^ (3 - 1) + C W.a₂ * (C 2 * X) + C W.a₄)) = 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x₁ x₂ y₁ L : R<VAR>hx' : W.Equation (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L)<VAR>hx : W.a₁ * (L * (W.addX x₁ x₂ L - x₁) + y₁) - (3 * W.addX x₁ x₂ L ^ 2 + 2 * W.a₂ * W.addX x₁ x₂ L + W.a₄) = 0 ∧ 2 * (L * (W.addX x₁ x₂ L - x₁) + y₁) + (W.a₁ * W.addX x₁ x₂ L + W.a₃) = 0<GOAL>2 * (L * (W.addX x₁ x₂ L - x₁) + y₁) * L + (W.a₁ * (L * (W.addX x₁ x₂ L - x₁) + y₁) + (W.a₁ * W.addX x₁ x₂ L + W.a₃) * L) - (↑3 * W.addX x₁ x₂ L ^ (3 - 1) + W.a₂ * (2 * W.addX x₁ x₂ L) + W.a₄) = 0
<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>inst✝ : InitiallySmall J<VAR>i : J<GOAL>∃ j ∈ Set.range (fromInitialModel J).obj, Nonempty (j ⟶ i)
<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>inst✝ : InitiallySmall J<VAR>i : J<VAR>f : CostructuredArrow (fromInitialModel J) i<GOAL>∃ j ∈ Set.range (fromInitialModel J).obj, Nonempty (j ⟶ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α ⊕ β<GOAL>x.getLeft? = none ↔ x.isRight = true
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : Zero R<VAR>inst✝ : SMulWithZero R V<VAR>x : HahnModule Γ' R V<VAR>x✝ : Γ'<GOAL>((of R).symm (0 • x)).coeff x✝ = ((of R).symm 0).coeff x✝
<VAR>m✝ : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m✝<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>A : Matrix n n R<VAR>hA : A.PosSemidef<VAR>m : Type u_5<VAR>inst✝ : Fintype m<VAR>B : Matrix m n R<GOAL>(B * A * Bᴴ).PosSemidef
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>ι' : Sort u_3<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<GOAL>Iio a ∩ Iio b ∈ Iio '' s
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l✝ l₁ l₂ : List α<VAR>a b✝ : α<VAR>f : β → α<VAR>b : β<VAR>l : List β<GOAL>Chain R (f b) (map f l) ↔ Chain (fun a b => R (f a) (f b)) b l
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a✝ b c d : α<VAR>hc : AddLECancellable c<VAR>h : c ≤ b<VAR>a : α<GOAL>a + b - c = a + (b - c)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝ : Reflective i<VAR>X : C<GOAL>(reflectorAdjunction i).unit.app (i.obj ((reflector i).obj X)) = i.map ((reflector i).map ((reflectorAdjunction i).unit.app X))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝ : Reflective i<VAR>X : C<GOAL>(reflectorAdjunction i).unit.app (i.obj ((reflector i).obj X)) ≫ i.map ((reflectorAdjunction i).counit.app ((reflector i).obj X)) = i.map ((reflector i).map ((reflectorAdjunction i).unit.app X) ≫ (reflectorAdjunction i).counit.app ((reflector i).obj X))
<VAR>m n✝ a✝ b✝ c✝ d a b n c : ℤ<VAR>ha : a ≡ b [ZMOD n]<GOAL>b + 0 ≡ b [ZMOD n]
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ t✝ : Finset α<VAR>a : α<VAR>s t u : Finset α<GOAL>u ∈ (s ∪ t).powerset ↔ u ∈ s.powerset ⊻ t.powerset
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ t✝ : Finset α<VAR>a : α<VAR>s t u : Finset α<GOAL>u ⊆ s ∪ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ t✝ : Finset α<VAR>a : α<VAR>s t u : Finset α<VAR>h : u ⊆ s ∪ t<GOAL>s ∩ u ∪ t ∩ u = u
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ t✝ : Finset α<VAR>a : α<VAR>s t u : Finset α<GOAL>(∃ a ⊆ s, ∃ b ⊆ t, a ∪ b = u) → u ⊆ s ∪ t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x✝ : E<VAR>hs : Convex 𝕜 s<VAR>z x : E<VAR>hx : x ∈ (fun x => z + x) ⁻¹' s<VAR>y : E<VAR>hy : y ∈ (fun x => z + x) ⁻¹' s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>h : a • (fun x => z + x) x + b • (fun x => z + x) y ∈ s<GOAL>a • x + b • y ∈ (fun x => z + x) ⁻¹' s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>this : DecidableEq R := Classical.decEq R<VAR>hp0 : p = 0<GOAL>(p /ₘ q).degree ≤ p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>this : DecidableEq R := Classical.decEq R<VAR>hp0 : ¬p = 0<VAR>hq : q.Monic<VAR>h : q.degree ≤ p.degree<GOAL>(p /ₘ q).degree ≤ p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>this✝ : DecidableEq R := Classical.decEq R<VAR>hp0 : ¬p = 0<VAR>hq : q.Monic<VAR>h : q.degree ≤ p.degree<VAR>this : Nontrivial R<GOAL>(p /ₘ q).degree ≤ p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>this✝ : DecidableEq R := Classical.decEq R<VAR>hp0 : ¬p = 0<VAR>hq : q.Monic<VAR>h : q.degree ≤ p.degree<VAR>this : Nontrivial R<GOAL>↑(p /ₘ q).natDegree ≤ ↑q.natDegree + ↑(p /ₘ q).natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>this : DecidableEq R := Classical.decEq R<VAR>hp0 : ¬p = 0<VAR>hq : q.Monic<VAR>h : ¬q.degree ≤ p.degree<GOAL>(if h : q.Monic then (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then let z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree); let_fun _wf := ⋯; let dm := (p - q * z).divModByMonicAux ⋯; (z + dm.1, dm.2) else (0, p)).1 else 0).degree ≤ p.degree
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A✝ : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R✝<VAR>n : ℕ<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : Semiring A✝<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R✝ A✝<VAR>inst✝³ : Algebra R✝ B<VAR>p✝ q r : R✝[X]<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>p : R[X]<VAR>f : R[X] →ₐ[R] A<GOAL>eval₂ (algebraMap R A) (f X) p = f p
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A✝ : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R✝<VAR>n : ℕ<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : Semiring A✝<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R✝ A✝<VAR>inst✝³ : Algebra R✝ B<VAR>p✝ q r : R✝[X]<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>p : R[X]<VAR>f : R[X] →ₐ[R] A<GOAL>eval₂ (algebraMap R A) (f X) p = f (p.sum fun n a => C a * X ^ n)
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A✝ : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R✝<VAR>n : ℕ<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : Semiring A✝<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R✝ A✝<VAR>inst✝³ : Algebra R✝ B<VAR>p✝ q r : R✝[X]<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>p : R[X]<VAR>f : R[X] →ₐ[R] A<GOAL>∑ n ∈ p.support, (algebraMap R A) (p.coeff n) * f X ^ n = f (∑ n ∈ p.support, C (p.coeff n) * X ^ n)
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A✝ : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R✝<VAR>n : ℕ<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : Semiring A✝<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R✝ A✝<VAR>inst✝³ : Algebra R✝ B<VAR>p✝ q r : R✝[X]<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>p : R[X]<VAR>f : R[X] →ₐ[R] A<GOAL>∑ n ∈ p.support, (algebraMap R A) (p.coeff n) * f X ^ n = ∑ x ∈ p.support, f (C (p.coeff x)) * f X ^ x
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type w<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : Small.{v, u} R<GOAL>Flat R M ↔ ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (L : N →ₗ[R] N'), Function.Injective ⇑L → Function.Injective ⇑(lTensor M L)
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p : ℕ<VAR>_hp✝ : Fact (Nat.Prime p)<VAR>n m : ℕ<VAR>hdvd : p ^ m ∣ Nat.card G<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<VAR>hnm✝ : n ≤ m<VAR>hnm : n < m<VAR>h0m : 0 < m<VAR>_wf : m - 1 < m<VAR>hnm1 : n ≤ m - 1<VAR>K : Subgroup G<VAR>hK : Nat.card ↥K = p ^ (m - 1) ∧ H ≤ K<GOAL>p ^ (m - 1 + 1) ∣ Nat.card G
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p : ℕ<VAR>_hp✝ : Fact (Nat.Prime p)<VAR>n m : ℕ<VAR>hdvd : p ^ m ∣ Nat.card G<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<VAR>hnm✝ : n ≤ m<VAR>hnm : n < m<VAR>h0m : 0 < m<VAR>_wf : m - 1 < m<VAR>hnm1 : n ≤ m - 1<VAR>K : Subgroup G<VAR>hK : Nat.card ↥K = p ^ (m - 1) ∧ H ≤ K<VAR>hdvd' : p ^ (m - 1 + 1) ∣ Nat.card G<VAR>K' : Subgroup G<VAR>hK' : Nat.card ↥K' = p ^ (m - 1 + 1) ∧ K ≤ K'<GOAL>Nat.card ↥K' = p ^ m
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Semiring α<VAR>inst✝¹ : Semiring β<VAR>f : α → β<VAR>hf✝ : IsSemiringHom f<VAR>x y : α<VAR>hf : IsSemiringHom f<VAR>γ : Type u_1<VAR>inst✝ : Semiring γ<VAR>g : β → γ<VAR>hg : IsSemiringHom g<GOAL>(g ∘ f) 0 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Semiring α<VAR>inst✝¹ : Semiring β<VAR>f : α → β<VAR>hf✝ : IsSemiringHom f<VAR>x y : α<VAR>hf : IsSemiringHom f<VAR>γ : Type u_1<VAR>inst✝ : Semiring γ<VAR>g : β → γ<VAR>hg : IsSemiringHom g<GOAL>(g ∘ f) 1 = 1
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Semiring α<VAR>inst✝¹ : Semiring β<VAR>f : α → β<VAR>hf✝ : IsSemiringHom f<VAR>x✝ y✝ : α<VAR>hf : IsSemiringHom f<VAR>γ : Type u_1<VAR>inst✝ : Semiring γ<VAR>g : β → γ<VAR>hg : IsSemiringHom g<VAR>x y : α<GOAL>(g ∘ f) (x + y) = (g ∘ f) x + (g ∘ f) y
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Semiring α<VAR>inst✝¹ : Semiring β<VAR>f : α → β<VAR>hf✝ : IsSemiringHom f<VAR>x✝ y✝ : α<VAR>hf : IsSemiringHom f<VAR>γ : Type u_1<VAR>inst✝ : Semiring γ<VAR>g : β → γ<VAR>hg : IsSemiringHom g<VAR>x y : α<GOAL>(g ∘ f) (x * y) = (g ∘ f) x * (g ∘ f) y
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>p : Submodule R M<VAR>k : ℕ<VAR>μ : R<VAR>hfp : ∀ x ∈ p, f x ∈ p<GOAL>(genEigenspace (LinearMap.restrict f hfp) μ) k = Submodule.comap p.subtype ((f.genEigenspace μ) k)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>p : Submodule R M<VAR>k : ℕ<VAR>μ : R<VAR>hfp : ∀ x ∈ p, f x ∈ p<GOAL>LinearMap.ker ((LinearMap.restrict f hfp - (algebraMap R (End R ↥p)) μ) ^ k) = LinearMap.ker (((f - (algebraMap R (End R M)) μ) ^ k) ∘ₗ p.subtype)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f f₁ f₂ : Filter α<VAR>h h₁ h₂ : Set α → Set β<VAR>hh : Monotone h<GOAL>(∀ s ∈ f, (𝓟 (h s)).NeBot) ↔ ∀ s ∈ f, (h s).Nonempty
<VAR>R : Type u_1<VAR>a b : R<VAR>inst✝ : Monoid R<VAR>n : ℕ<VAR>rra : IsRightRegular a<GOAL>IsRightRegular (a ^ n)
<VAR>R : Type u_1<VAR>a b : R<VAR>inst✝ : Monoid R<VAR>n : ℕ<VAR>rra : IsRightRegular a<GOAL>Function.Injective (fun x => x * a)^[n]
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>p : X → Prop<VAR>s : Set X<VAR>hx : x ∈ e.source<GOAL>(∀ᶠ (y : Y) in 𝓝[↑e.symm ⁻¹' s] ↑e x, p (↑e.symm y)) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p x
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>p : X → Prop<VAR>s : Set X<VAR>hx : x ∈ e.source<GOAL>(∀ᶠ (x : X) in 𝓝[s] x, p (↑e.symm (↑e x))) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p x
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>p : X → Prop<VAR>s : Set X<VAR>hx : x ∈ e.source<VAR>y : X<VAR>hy : ↑e.symm (↑e y) = y<GOAL>p (↑e.symm (↑e y)) ↔ p y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>re ⟪x, y⟫_𝕜 = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>re ⟪x, y⟫_𝕜 = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - (‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖)) / 2
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s✝ t✝ : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x y : (i : δ) → π i<VAR>i : δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>s t : Finset δ<VAR>hst : Disjoint s t<GOAL>∫⋯∫⁻_s ∪ t, f ∂μ = ∫⋯∫⁻_t, ∫⋯∫⁻_s, f ∂μ ∂μ
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>p₁ p₂ p₃ : ι<VAR>h₂₁ : p₂ = p₁<VAR>h₂₃ : p₂ = p₃<GOAL>eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<GOAL>map f ⊤ = 𝓟 (range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f✝ g : α → β<VAR>s✝ : Finset α<VAR>t✝ : Finset β<VAR>a : α<VAR>b c : β<VAR>inst✝ : DecidableEq α<VAR>f : α → β<VAR>s t : Finset α<VAR>hf : Set.InjOn f (↑s ∪ ↑t)<GOAL>f '' (↑s ∩ ↑t) = f '' ↑s ∩ f '' ↑t
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>f : P1 →ᵃ[k] P2<VAR>p : P1<GOAL>Function.Surjective ⇑f.linear ↔ Function.Surjective ⇑f
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>f : P1 →ᵃ[k] P2<VAR>p : P1<VAR>h : ⇑f.linear = ⇑(Equiv.vaddConst (f p)).symm ∘ ⇑f ∘ ⇑(Equiv.vaddConst p)<GOAL>Function.Surjective ⇑f.linear ↔ Function.Surjective ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<GOAL>SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<VAR>h : SuperpolynomialDecay l k f<VAR>z : ℤ<GOAL>Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>P Q : C → Prop<VAR>X : C<GOAL>isoClosure P X ↔ ∃ Y x, Nonempty (X ≅ Y)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → LinearOrder (α i)<VAR>x y : (i : ι) → α i<VAR>i₀ : ι<VAR>m : α i₀<VAR>hm : m ∈ Icc (x i₀) (y i₀)<GOAL>((univ.pi fun i => Ioc (x i) (update y i₀ m i)) ∪ univ.pi fun i => Ioc (update x i₀ m i) (y i)) = univ.pi fun i => Ioc (x i) (y i)
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]<VAR>hbε : 0 < cardPowDegree b • ε<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]<VAR>hbε : 0 < cardPowDegree b • ε<VAR>one_lt_q : 1 < Fintype.card Fq<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]<VAR>hbε : 0 < cardPowDegree b • ε<VAR>one_lt_q : 1 < Fintype.card Fq<VAR>one_lt_q' : 1 < ↑(Fintype.card Fq)<VAR>q_pos : 0 < Fintype.card Fq<VAR>q_pos' : 0 < ↑(Fintype.card Fq)<VAR>le_b : ¬b.natDegree ≤ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]<VAR>hbε : 0 < cardPowDegree b • ε<VAR>one_lt_q : 1 < Fintype.card Fq<VAR>one_lt_q' : 1 < ↑(Fintype.card Fq)<VAR>q_pos : 0 < Fintype.card Fq<VAR>q_pos' : 0 < ↑(Fintype.card Fq)<VAR>le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]<VAR>hbε : 0 < cardPowDegree b • ε<VAR>one_lt_q : 1 < Fintype.card Fq<VAR>one_lt_q' : 1 < ↑(Fintype.card Fq)<VAR>q_pos : 0 < Fintype.card Fq<VAR>q_pos' : 0 < ↑(Fintype.card Fq)<VAR>le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree<VAR>i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ<VAR>i_ne : i₀ ≠ i₁<VAR>deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]<VAR>hbε : 0 < cardPowDegree b • ε<VAR>one_lt_q : 1 < Fintype.card Fq<VAR>one_lt_q' : 1 < ↑(Fintype.card Fq)<VAR>q_pos : 0 < Fintype.card Fq<VAR>q_pos' : 0 < ↑(Fintype.card Fq)<VAR>le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree<VAR>i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ<VAR>i_ne : i₀ ≠ i₁<VAR>deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)<GOAL>↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]<VAR>hbε : 0 < cardPowDegree b • ε<VAR>one_lt_q : 1 < Fintype.card Fq<VAR>one_lt_q' : 1 < ↑(Fintype.card Fq)<VAR>q_pos : 0 < Fintype.card Fq<VAR>q_pos' : 0 < ↑(Fintype.card Fq)<VAR>le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree<VAR>i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ<VAR>i_ne : i₀ ≠ i₁<VAR>deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)<VAR>h : ¬A i₁ % b = A i₀ % b<GOAL>↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]<VAR>hbε : 0 < cardPowDegree b • ε<VAR>one_lt_q : 1 < Fintype.card Fq<VAR>one_lt_q' : 1 < ↑(Fintype.card Fq)<VAR>q_pos : 0 < Fintype.card Fq<VAR>q_pos' : 0 < ↑(Fintype.card Fq)<VAR>le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree<VAR>i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ<VAR>i_ne : i₀ ≠ i₁<VAR>deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)<VAR>h : ¬A i₁ % b = A i₀ % b<VAR>h' : A i₁ % b - A i₀ % b ≠ 0<GOAL>↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε