ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ Z✝ : C<VAR>f✝ g✝ : X✝ ⟶ Y✝<VAR>h✝ : Y✝ ⟶ Z✝<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : X ⟶ Z<VAR>inst✝ : IsIso g<VAR>hh : IsIso (f ≫ g)<VAR>w : f ≫ g = h<VAR>this : IsIso (f ≫ g)<GOAL>IsIso f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝ : AddSemigroup α<VAR>h : Periodic f c<VAR>a x : α<GOAL>(fun x => f (a + x)) (x + c) = (fun x => f (a + x)) 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>p : A[X]<GOAL>p ∈ RingHom.ker (Polynomial.aeval x) ↔ p ∈ Submodule.span A[X] {minpoly A x}
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>a : R<GOAL>(C a * X ^ n).degree ≤ ↑n
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>a : R<GOAL>((monomial n) a).degree ≤ ↑n
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.210393, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>k : A ⟶ S.X₂<VAR>hk : k ≫ S.g = 0<VAR>inst✝¹ : S.HasLeftHomology<VAR>φ : S ⟶ S₁<VAR>inst✝ : S₁.HasLeftHomology<GOAL>(k ≫ φ.τ₂) ≫ S₁.g = 0
<GOAL>∃ᶠ (m : ℕ) in atTop, Odd m
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ<GOAL>(gradedComm R 𝒜 ℬ) (((gradedMul R 𝒜 ℬ) x) y) = ((gradedMul R ℬ 𝒜) ((gradedComm R 𝒜 ℬ) x)) ((gradedComm R 𝒜 ℬ) y)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ<GOAL>(gradedMul R 𝒜 ℬ).compr₂ ↑(gradedComm R 𝒜 ℬ) = (gradedMul R ℬ 𝒜 ∘ₗ ↑(gradedComm R 𝒜 ℬ)).compl₂ ↑(gradedComm R 𝒜 ℬ)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ<VAR>i₁ : ι<VAR>a₁ : 𝒜 i₁<VAR>j₁ : ι<VAR>b₁ : ℬ j₁<VAR>i₂ : ι<VAR>a₂ : 𝒜 i₂<VAR>j₂ : ι<VAR>b₂ : ℬ j₂<GOAL>(gradedComm R 𝒜 ℬ) (((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 i₁) a₁ ⊗ₜ[R] (lof R ι ℬ j₁) b₁)) ((lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] (lof R ι ℬ j₂) b₂)) = ((gradedMul R ℬ 𝒜) ((gradedComm R 𝒜 ℬ) ((lof R ι 𝒜 i₁) a₁ ⊗ₜ[R] (lof R ι ℬ j₁) b₁))) ((gradedComm R 𝒜 ℬ) ((lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] (lof R ι ℬ j₂) b₂))
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ<VAR>i₁ : ι<VAR>a₁ : 𝒜 i₁<VAR>j₁ : ι<VAR>b₁ : ℬ j₁<VAR>i₂ : ι<VAR>a₂ : 𝒜 i₂<VAR>j₂ : ι<VAR>b₂ : ℬ j₂<GOAL>(gradedComm R 𝒜 ℬ) ((-1) ^ (j₁ * i₂) • ((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂)) = ((gradedMul R ℬ 𝒜) ((-1) ^ (j₁ * i₁) • (lof R ι ℬ j₁) b₁ ⊗ₜ[R] (lof R ι 𝒜 i₁) a₁)) ((-1) ^ (j₂ * i₂) • (lof R ι ℬ j₂) b₂ ⊗ₜ[R] (lof R ι 𝒜 i₂) a₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ<VAR>i₁ : ι<VAR>a₁ : 𝒜 i₁<VAR>j₁ : ι<VAR>b₁ : ℬ j₁<VAR>i₂ : ι<VAR>a₂ : 𝒜 i₂<VAR>j₂ : ι<VAR>b₂ : ℬ j₂<GOAL>↑↑((-1) ^ (j₁ * i₂)) • (gradedComm R 𝒜 ℬ) (((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂)) = ↑↑((-1) ^ (j₂ * i₂)) • ↑↑((-1) ^ (j₁ * i₁)) • ((gradedMul R ℬ 𝒜) ((lof R ι ℬ j₁) b₁ ⊗ₜ[R] (lof R ι 𝒜 i₁) a₁)) ((lof R ι ℬ j₂) b₂ ⊗ₜ[R] (lof R ι 𝒜 i₂) a₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ<VAR>i₁ : ι<VAR>a₁ : 𝒜 i₁<VAR>j₁ : ι<VAR>b₁ : ℬ j₁<VAR>i₂ : ι<VAR>a₂ : 𝒜 i₂<VAR>j₂ : ι<VAR>b₂ : ℬ j₂<GOAL>((-1) ^ (j₁ * i₂) * (-1) ^ ((j₁ + j₂) * (i₁ + i₂))) • ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂) ⊗ₜ[R] ((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂) = ((-1) ^ (j₂ * i₂) * ((-1) ^ (j₁ * i₁) * (-1) ^ (i₁ * j₂))) • ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂) ⊗ₜ[R] ((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ<VAR>i₁ : ι<VAR>a₁ : 𝒜 i₁<VAR>j₁ : ι<VAR>b₁ : ℬ j₁<VAR>i₂ : ι<VAR>a₂ : 𝒜 i₂<VAR>j₂ : ι<VAR>b₂ : ℬ j₂<GOAL>(-1) ^ (j₁ * i₂ + (j₁ * i₁ + j₂ * i₁ + (j₁ * i₂ + j₂ * i₂))) • ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂) ⊗ₜ[R] ((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂) = (-1) ^ (j₂ * i₂ + (j₁ * i₁ + j₂ * i₁)) • ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂) ⊗ₜ[R] ((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ<VAR>i₁ : ι<VAR>a₁ : 𝒜 i₁<VAR>j₁ : ι<VAR>b₁ : ℬ j₁<VAR>i₂ : ι<VAR>a₂ : 𝒜 i₂<VAR>j₂ : ι<VAR>b₂ : ℬ j₂<GOAL>(-1) ^ (2 • (j₁ * i₂) + (j₁ * i₁ + (j₂ * i₁ + j₂ * i₂))) = (-1) ^ (j₁ * i₁ + (j₂ * i₁ + j₂ * i₂))
<VAR>α : Type u<VAR>β : Type v<VAR>x : α<VAR>l : List α<VAR>k : Nat<GOAL>x ∈ l.eraseIdx k ↔ ∃ i, ↑i ≠ k ∧ l.get i = x
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v w u : V<VAR>p : G.Walk u u<GOAL>p.IsPath ↔ p = nil
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>a b : α<GOAL>(∃ n, succ^[n] a = b) ↔ a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>a b : α<GOAL>(∃ n, succ^[n] a = b) → a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>a : α<VAR>n : ℕ<GOAL>a ≤ succ^[n] a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>f : ↥(Lp ℝ p μ)<VAR>a : α<VAR>h : ↑↑(negPart f) a = max (-↑↑f a) 0<GOAL>↑↑(negPart f) a = -min (↑↑f a) 0
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>h : NumberField K<VAR>inst✝¹ : Finite ↑S<VAR>inst✝ : IsCyclotomicExtension S K L<GOAL>FiniteDimensional ℚ L
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>h : NumberField K<VAR>inst✝¹ : Finite ↑S<VAR>inst✝ : IsCyclotomicExtension S K L<VAR>this : CharZero L<GOAL>FiniteDimensional ℚ L
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>h : NumberField K<VAR>inst✝¹ : Finite ↑S<VAR>inst✝ : IsCyclotomicExtension S K L<VAR>this✝ : CharZero L<VAR>this : Module.Finite K L<GOAL>FiniteDimensional ℚ L
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : AddGroup N<VAR>f f₁ f₂ g g₁ g₂ : α →₀ N<GOAL>f.neLocus (f - g) = g.support
<VAR>a t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) ↑(cosKernel (↑a) t)
<VAR>a t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) (jacobiTheta₂ (↑a) (I * ↑t))
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : ∀ (n : ℤ), cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t)) = jacobiTheta₂_term n (↑a) (I * ↑t)<GOAL>HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) (jacobiTheta₂ (↑a) (I * ↑t))
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : ∀ (n : ℤ), cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t)) = jacobiTheta₂_term n (↑a) (I * ↑t)<GOAL>HasSum (fun n => jacobiTheta₂_term n (↑a) (I * ↑t)) (jacobiTheta₂ (↑a) (I * ↑t))
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<VAR>h : c₂.Rel i₂ i₂'<VAR>i₁₂ : I₁₂<VAR>h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂<GOAL>K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂ h'
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x y : M<VAR>c : ↥S<VAR>h : f.toMap (x * ↑c) = f.toMap (y * ↑c)<GOAL>f.toMap (↑c * x) = f.toMap (↑c * y)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p₁ : ι → P<VAR>p₂ b : P<GOAL>∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (s.weightedVSubOfPoint p₁ b) w - (∑ i ∈ s, w i) • (p₂ -ᵥ b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<GOAL>T0Space α ↔ Pairwise fun x y => ∃ r ∈ 𝓤 α, (x, y) ∉ r
<VAR>ι : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>α : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype p<VAR>inst✝ : NonUnitalCommSemiring R<VAR>A : Matrix m n R<VAR>B : Matrix n p R<VAR>C : Matrix p m R<GOAL>(A * B * C).trace = (C * A * B).trace
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>s : Multiset R<GOAL>(Multiset.map (fun a => X - C a) s).prod.roots = s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>s : Multiset R<GOAL>(s.bind fun a => (X - C a).roots) = s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>s : Multiset R<GOAL>0 ∉ Multiset.map (fun a => X - C a) s
<VAR>P : PFunctor.{u}<VAR>α : Type v₁<VAR>β : Type v₂<VAR>γ : Type v₃<VAR>inst✝² : DecidableEq P.A<VAR>inst✝¹ : Inhabited α<VAR>inst✝ : Inhabited β<VAR>x : ↑P α<VAR>f : α → β<VAR>i : P.Idx<VAR>h : i.fst = x.fst<GOAL>(P.map f x).iget i = f (x.iget i)
<VAR>P : PFunctor.{u}<VAR>α : Type v₁<VAR>β : Type v₂<VAR>γ : Type v₃<VAR>inst✝² : DecidableEq P.A<VAR>inst✝¹ : Inhabited α<VAR>inst✝ : Inhabited β<VAR>x : ↑P α<VAR>f : α → β<VAR>i : P.Idx<VAR>h : i.fst = x.fst<GOAL>(P.map f x).snd (cast ⋯ i.snd) = f (x.snd (cast ⋯ i.snd))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommSemiring R<VAR>n k : ℕ<GOAL>(⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) • X ^ (n - k)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>f : ι → α<VAR>h : IsSupClosedCompact α<GOAL>WellFounded fun x x_1 => x > x_1
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>f : ι → α<VAR>h : IsSupClosedCompact α<VAR>a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1<GOAL>False
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>f : ι → α<VAR>h : IsSupClosedCompact α<VAR>a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1<GOAL>sSup (range ⇑a) ∈ range ⇑a
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>ι' : Sort u_3<VAR>inst✝ : LinearOrder α<VAR>f : ι → α<VAR>g : ι' → α<GOAL>∀ {a₁ b₁ a₂ b₂ : α}, Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (max a₁ a₂) (min b₁ b₂)
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : ∀ (ε : ℝ≥0), 0 < ε → b < ⊤ → a ≤ b + ↑ε<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : b < a<GOAL>∃ ε, 0 < ε ∧ b < ⊤ ∧ b + ↑ε < a
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r✝ p q : ℝ≥0<VAR>h : b < a<VAR>r : ℝ≥0<VAR>hr0 : 0 < r<VAR>hr : b + ↑r < a<GOAL>∃ ε, 0 < ε ∧ b < ⊤ ∧ b + ↑ε < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>self : Buckets α β<VAR>i : USize<VAR>d d' : AssocList α β<VAR>h : i.toNat < self.val.size<VAR>h' : i.toNat < (self.update i d h).val.size<GOAL>(self.update i d h).update i d' h' = self.update i d' h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>self : Buckets α β<VAR>i : USize<VAR>d d' : AssocList α β<VAR>h : i.toNat < self.val.size<VAR>h' : i.toNat < (self.update i d h).val.size<GOAL>⟨(self.val.set ⟨i.toNat, h⟩ d).set ⟨i.toNat, h'⟩ d', ⋯⟩ = ⟨self.val.set ⟨i.toNat, h⟩ d', ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>self : Buckets α β<VAR>i : USize<VAR>d d' : AssocList α β<VAR>h : i.toNat < self.val.size<VAR>h' : i.toNat < (self.update i d h).val.size<GOAL>(self.val.set ⟨i.toNat, h⟩ d).set ⟨i.toNat, h'⟩ d' = self.val.set ⟨i.toNat, h⟩ d'
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X✝ Y : C<VAR>D : Type u_1<VAR>inst✝ : Category.{u_2, u_1} D<VAR>F G : C ⥤ Dᵒᵖ<VAR>e : F ≅ G<VAR>X : C<GOAL>(e.inv.app X).unop ≫ (e.hom.app X).unop = 𝟙 (Opposite.unop (F.obj X))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s✝ s₁ s₂ : Set α<VAR>t✝ t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>s : Set α<VAR>t : Set β<GOAL>Prod.swap '' s ×ˢ t = t ×ˢ s
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<GOAL>sin (∠ p₁ p₂ p₃) = 0 → Collinear ℝ {p₁, p₂, p₃}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<GOAL>¬Collinear ℝ {p₁, p₂, p₃} → ¬sin (∠ p₁ p₂ p₃) = 0
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>hB : M.Indep B<VAR>hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)<VAR>hnb : ¬M.Base B<GOAL>False
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B'✝ I J D X : Set α<VAR>e f : α<VAR>hB : M.Indep B<VAR>hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)<VAR>hnb : ¬M.Base B<VAR>B' : Set α<VAR>hB' : M.Base B'<GOAL>False
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B'✝ I J D X : Set α<VAR>e✝ f : α<VAR>hB : M.Indep B<VAR>hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)<VAR>hnb : ¬M.Base B<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>e : α<VAR>he : e ∈ B' \ B<VAR>h : M.Indep (insert e B)<GOAL>False
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : (i : ι) → Set (π i)<VAR>a : (i : ι) → π i<GOAL>a ∈ interior (I.pi s) ↔ a ∈ I.pi fun i => interior (s i)
<VAR>α : Type u_1<VAR>inst✝¹² : TopologicalSpace α<VAR>R : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>A : Type u_3<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : Algebra R A<VAR>inst✝⁷ : TopologicalSemiring A<VAR>A₂ : Type u_4<VAR>inst✝⁶ : TopologicalSpace A₂<VAR>inst✝⁵ : Semiring A₂<VAR>inst✝⁴ : Algebra R A₂<VAR>inst✝³ : TopologicalSemiring A₂<VAR>𝕜 : Type u_5<VAR>inst✝² : TopologicalSpace 𝕜<VAR>s✝ : Set C(α, 𝕜)<VAR>f✝ : ↑s✝<VAR>x✝ : α<VAR>inst✝¹ : Field 𝕜<VAR>inst✝ : TopologicalRing 𝕜<VAR>s : Subalgebra 𝕜 C(α, 𝕜)<VAR>h : s.SeparatesPoints<VAR>v : α → 𝕜<VAR>x y : α<VAR>n : ¬x = y<VAR>f : C(α, 𝕜)<VAR>hf : f ∈ ↑s<VAR>hxy : (fun f => ⇑f) f x ≠ (fun f => ⇑f) f y<GOAL>∃ f ∈ ↑s, f x = v x ∧ f y = v y
<VAR>α : Type u_1<VAR>inst✝¹² : TopologicalSpace α<VAR>R : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>A : Type u_3<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : Algebra R A<VAR>inst✝⁷ : TopologicalSemiring A<VAR>A₂ : Type u_4<VAR>inst✝⁶ : TopologicalSpace A₂<VAR>inst✝⁵ : Semiring A₂<VAR>inst✝⁴ : Algebra R A₂<VAR>inst✝³ : TopologicalSemiring A₂<VAR>𝕜 : Type u_5<VAR>inst✝² : TopologicalSpace 𝕜<VAR>s✝ : Set C(α, 𝕜)<VAR>f✝ : ↑s✝<VAR>x✝ : α<VAR>inst✝¹ : Field 𝕜<VAR>inst✝ : TopologicalRing 𝕜<VAR>s : Subalgebra 𝕜 C(α, 𝕜)<VAR>h : s.SeparatesPoints<VAR>v : α → 𝕜<VAR>x y : α<VAR>n : ¬x = y<VAR>f : C(α, 𝕜)<VAR>hf : f ∈ ↑s<VAR>hxy : f x - f y ≠ 0<GOAL>∃ f ∈ ↑s, f x = v x ∧ f y = v y
<VAR>α : Type u_1<VAR>inst✝¹² : TopologicalSpace α<VAR>R : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>A : Type u_3<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : Algebra R A<VAR>inst✝⁷ : TopologicalSemiring A<VAR>A₂ : Type u_4<VAR>inst✝⁶ : TopologicalSpace A₂<VAR>inst✝⁵ : Semiring A₂<VAR>inst✝⁴ : Algebra R A₂<VAR>inst✝³ : TopologicalSemiring A₂<VAR>𝕜 : Type u_5<VAR>inst✝² : TopologicalSpace 𝕜<VAR>s✝ : Set C(α, 𝕜)<VAR>f✝ : ↑s✝<VAR>x✝ : α<VAR>inst✝¹ : Field 𝕜<VAR>inst✝ : TopologicalRing 𝕜<VAR>s : Subalgebra 𝕜 C(α, 𝕜)<VAR>h : s.SeparatesPoints<VAR>v : α → 𝕜<VAR>x y : α<VAR>n : ¬x = y<VAR>f : C(α, 𝕜)<VAR>hf : f ∈ ↑s<VAR>hxy : f x - f y ≠ 0<VAR>a : 𝕜 := v x<VAR>b : 𝕜 := v y<VAR>f' : ↥s := ((b - a) * (f x - f y)⁻¹) • ((algebraMap 𝕜 ↥s) (f x) - ⟨f, hf⟩) + (algebraMap 𝕜 ↥s) a<GOAL>∃ f ∈ ↑s, f x = v x ∧ f y = v y
<VAR>α : Type u_1<VAR>inst✝¹² : TopologicalSpace α<VAR>R : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>A : Type u_3<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : Algebra R A<VAR>inst✝⁷ : TopologicalSemiring A<VAR>A₂ : Type u_4<VAR>inst✝⁶ : TopologicalSpace A₂<VAR>inst✝⁵ : Semiring A₂<VAR>inst✝⁴ : Algebra R A₂<VAR>inst✝³ : TopologicalSemiring A₂<VAR>𝕜 : Type u_5<VAR>inst✝² : TopologicalSpace 𝕜<VAR>s✝ : Set C(α, 𝕜)<VAR>f✝ : ↑s✝<VAR>x✝ : α<VAR>inst✝¹ : Field 𝕜<VAR>inst✝ : TopologicalRing 𝕜<VAR>s : Subalgebra 𝕜 C(α, 𝕜)<VAR>h : s.SeparatesPoints<VAR>v : α → 𝕜<VAR>x y : α<VAR>n : ¬x = y<VAR>f : C(α, 𝕜)<VAR>hf : f ∈ ↑s<VAR>hxy : f x - f y ≠ 0<VAR>a : 𝕜 := v x<VAR>b : 𝕜 := v y<VAR>f' : ↥s := ((b - a) * (f x - f y)⁻¹) • ((algebraMap 𝕜 ↥s) (f x) - ⟨f, hf⟩) + (algebraMap 𝕜 ↥s) a<GOAL>↑f' x = v x
<VAR>α : Type u_1<VAR>inst✝¹² : TopologicalSpace α<VAR>R : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>A : Type u_3<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : Algebra R A<VAR>inst✝⁷ : TopologicalSemiring A<VAR>A₂ : Type u_4<VAR>inst✝⁶ : TopologicalSpace A₂<VAR>inst✝⁵ : Semiring A₂<VAR>inst✝⁴ : Algebra R A₂<VAR>inst✝³ : TopologicalSemiring A₂<VAR>𝕜 : Type u_5<VAR>inst✝² : TopologicalSpace 𝕜<VAR>s✝ : Set C(α, 𝕜)<VAR>f✝ : ↑s✝<VAR>x✝ : α<VAR>inst✝¹ : Field 𝕜<VAR>inst✝ : TopologicalRing 𝕜<VAR>s : Subalgebra 𝕜 C(α, 𝕜)<VAR>h : s.SeparatesPoints<VAR>v : α → 𝕜<VAR>x y : α<VAR>n : ¬x = y<VAR>f : C(α, 𝕜)<VAR>hf : f ∈ ↑s<VAR>hxy : f x - f y ≠ 0<VAR>a : 𝕜 := v x<VAR>b : 𝕜 := v y<VAR>f' : ↥s := ((b - a) * (f x - f y)⁻¹) • ((algebraMap 𝕜 ↥s) (f x) - ⟨f, hf⟩) + (algebraMap 𝕜 ↥s) a<GOAL>↑f' y = v y
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f g : NormedAddGroupHom V₁ V₂<GOAL>Function.Injective toFun
<VAR>p : ℕ<VAR>w : 1 < p<VAR>p' : ℕ := p - 2<GOAL>LucasLehmerTest p → Nat.Prime (mersenne p)
<VAR>p : ℕ<VAR>w : 1 < p<VAR>p' : ℕ := p - 2<VAR>z : p = p' + 2<GOAL>LucasLehmerTest p → Nat.Prime (mersenne p)
<VAR>p : ℕ<VAR>w✝ : 1 < p<VAR>p' : ℕ := p - 2<VAR>z : p = p' + 2<VAR>w : 1 < p' + 2<GOAL>LucasLehmerTest p → Nat.Prime (mersenne p)
<VAR>p : ℕ<VAR>w✝ : 1 < p<VAR>p' : ℕ := p - 2<VAR>z : p = p' + 2<VAR>w : 1 < p' + 2<GOAL>¬Nat.Prime (mersenne p) → ¬LucasLehmerTest p
<VAR>p : ℕ<VAR>w✝ : 1 < p<VAR>p' : ℕ := p - 2<VAR>z : p = p' + 2<VAR>w : 1 < p' + 2<VAR>a : ¬Nat.Prime (mersenne (p' + 2))<VAR>t : LucasLehmerTest (p' + 2)<GOAL>False
<VAR>p : ℕ<VAR>w✝ : 1 < p<VAR>p' : ℕ := p - 2<VAR>z : p = p' + 2<VAR>w : 1 < p' + 2<VAR>a : ¬Nat.Prime (mersenne (p' + 2))<VAR>t : LucasLehmerTest (p' + 2)<VAR>h₁ : 2 ^ (p' + 2) < ↑(q (p' + 2)) ^ 2<GOAL>False
<VAR>p : ℕ<VAR>w✝ : 1 < p<VAR>p' : ℕ := p - 2<VAR>z : p = p' + 2<VAR>w : 1 < p' + 2<VAR>a : ¬Nat.Prime (mersenne (p' + 2))<VAR>t : LucasLehmerTest (p' + 2)<VAR>h₁ : 2 ^ (p' + 2) < ↑(q (p' + 2)) ^ 2<VAR>h₂ : (mersenne (p' + 2)).minFac ^ 2 ≤ mersenne (p' + 2)<GOAL>False
<VAR>p : ℕ<VAR>w✝ : 1 < p<VAR>p' : ℕ := p - 2<VAR>z : p = p' + 2<VAR>w : 1 < p' + 2<VAR>a : ¬Nat.Prime (mersenne (p' + 2))<VAR>t : LucasLehmerTest (p' + 2)<VAR>h₁ : 2 ^ (p' + 2) < ↑(q (p' + 2)) ^ 2<VAR>h₂ : (mersenne (p' + 2)).minFac ^ 2 ≤ mersenne (p' + 2)<VAR>h : 2 ^ (p' + 2) < mersenne (p' + 2)<GOAL>False