ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p✝ : ℕ<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>p : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>inst✝ : Finite (Sylow p ↥N)<VAR>P : Sylow p G<VAR>hP : ↑P ≤ N<GOAL>(↑P).normalizer ⊔ N = ⊤
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_2, u_1} C<VAR>inst✝⁵ : HasZeroObject C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : Preadditive C<VAR>inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹ : Pretriangulated C<VAR>S : Subcategory C<VAR>inst✝ : ClosedUnderIsomorphisms S.P<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>h₁ : S.P T.obj₁<VAR>h₃ : S.P T.obj₃<GOAL>S.P T.obj₂
<VAR>l m✝ n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m n : ℕ<VAR>P : Matrix (Fin (m + 1)) (Fin n) α → Prop<GOAL>Exists P ↔ ∃ x, P x
<VAR>l m✝ n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m n : ℕ<VAR>P : Matrix (Fin (m + 1)) (Fin n) α → Prop<GOAL>(∃ r A, P (of (vecCons r A))) ↔ ∃ x, P x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{u_4, u_2} D<VAR>inst✝⁵ : HasZeroMorphisms C<VAR>inst✝⁴ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝³ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : S.HasLeftHomology<VAR>inst✝ : F.PreservesLeftHomologyOf S<GOAL>(S.mapCyclesIso F).hom ≫ F.map S.iCycles = (S.map F).iCycles
<VAR>n : ℕ<GOAL>n.dist n = 0
<VAR>J : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>inst✝² : HasColimit F<VAR>E : K ⥤ J<VAR>inst✝¹ : HasColimit (E ⋙ F)<VAR>L : Type u₃<VAR>inst✝ : Category.{v₃, u₃} L<VAR>D : L ⥤ K<VAR>h : HasColimit (D ⋙ E ⋙ F)<VAR>j : L<GOAL>ι (D ⋙ E ⋙ F) j ≫ pre (E ⋙ F) D ≫ pre F E = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)
<VAR>J : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>inst✝² : HasColimit F<VAR>E : K ⥤ J<VAR>inst✝¹ : HasColimit (E ⋙ F)<VAR>L : Type u₃<VAR>inst✝ : Category.{v₃, u₃} L<VAR>D : L ⥤ K<VAR>h : HasColimit (D ⋙ E ⋙ F)<VAR>j : L<GOAL>ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)
<VAR>J : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>inst✝² : HasColimit F<VAR>E : K ⥤ J<VAR>inst✝¹ : HasColimit (E ⋙ F)<VAR>L : Type u₃<VAR>inst✝ : Category.{v₃, u₃} L<VAR>D : L ⥤ K<VAR>h : HasColimit (D ⋙ E ⋙ F)<VAR>j : L<VAR>this : HasColimit ((D ⋙ E) ⋙ F)<GOAL>ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v v₁ : Valuation R Γ₀<VAR>v₂ : Valuation R Γ'₀<VAR>v₃ : Valuation R Γ''₀<VAR>h : v₁.IsEquiv v₂<VAR>r : R<GOAL>v₁ r ≠ 0 ↔ v₂ r ≠ 0
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v v₁ : Valuation R Γ₀<VAR>v₂ : Valuation R Γ'₀<VAR>v₃ : Valuation R Γ''₀<VAR>h : v₁.IsEquiv v₂<VAR>r : R<VAR>this : v₁ r ≠ v₁ 0 ↔ v₂ r ≠ v₂ 0<GOAL>v₁ r ≠ 0 ↔ v₂ r ≠ 0
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 < x<VAR>hy : 0 < y<VAR>hz : z < 0<GOAL>x ^ z⁻¹ ≤ y ↔ y ^ z ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫ (x : γ), κ.densityProcess ν n a x s ∂ν a = ((κ a) (univ ×ˢ s)).toReal
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Semiring α<GOAL>IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Semiring α<VAR>t : IsCancelMulZero α<GOAL>IsDomain α ∨ Subsingleton α
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Semiring α<VAR>t : IsCancelMulZero α<GOAL>Nontrivial α → IsDomain α
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>x : P.last.M<VAR>a₁ : P.A<VAR>f₁ : P.last.B a₁ → P.last.M<VAR>h₁ : x.dest = ⟨a₁, f₁⟩<VAR>a₂ : P.A<VAR>f₂ : P.last.B a₂ → P.last.M<VAR>h₂ : x.dest = ⟨a₂, f₂⟩<VAR>f' : Path P x ⟹ α<GOAL>dest' P h₁ f' = dest' P h₂ f'
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>x : P.last.M<VAR>a₁ : P.A<VAR>f₁ : P.last.B a₁ → P.last.M<VAR>h₁ : x.dest = ⟨a₁, f₁⟩<VAR>f' : Path P x ⟹ α<VAR>h₂ : x.dest = ⟨a₁, f₁⟩<GOAL>dest' P h₁ f' = dest' P h₂ f'
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → Game<GOAL>BddAbove (Set.range f)
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → Game<VAR>x : PGame<VAR>hx : x ∈ upperBounds (Set.range (Quotient.out ∘ f))<GOAL>BddAbove (Set.range f)
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → Game<VAR>x : PGame<VAR>hx : x ∈ upperBounds (Set.range (Quotient.out ∘ f))<VAR>i : ι<GOAL>f i ≤ ⟦x⟧
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>M : Type u_3<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module A M<VAR>inst✝ : Module R M<VAR>D D1 D2 : Derivation R A M<VAR>r : R<VAR>a✝ b✝ a b : A<VAR>h : a * b = 1<GOAL>D a = -a ^ 2 • D b
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>M : Type u_3<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module A M<VAR>inst✝ : Module R M<VAR>D D1 D2 : Derivation R A M<VAR>r : R<VAR>a✝ b✝ a b : A<VAR>h : a * b = 1<GOAL>D a = -(a ^ 2 • D b)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>M : Type u_3<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module A M<VAR>inst✝ : Module R M<VAR>D D1 D2 : Derivation R A M<VAR>r : R<VAR>a✝ b✝ a b : A<VAR>h : a * b = 1<GOAL>D a + a ^ 2 • D b = 0
<VAR>n : ℕ<GOAL>catalan (n + 1) = ∑ ij ∈ antidiagonal n, catalan ij.1 * catalan ij.2
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<VAR>hI : I ⊆ E<VAR>hX : X ⊆ E<GOAL>(uniqueBaseOn I E).Basis (X ∩ I) X
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : AddCommMonoid R✝<VAR>inst✝⁵ : Pow R✝ ℕ<VAR>inst✝⁴ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝³ : NonAssocSemiring R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : NatPowAssoc R<VAR>inst✝ : BinomialRing R<VAR>r : R<VAR>k : ℕ<GOAL>multichoose (r + 1) (k + 1) = multichoose r (k + 1) + multichoose (r + 1) k
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : AddCommMonoid R✝<VAR>inst✝⁵ : Pow R✝ ℕ<VAR>inst✝⁴ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝³ : NonAssocSemiring R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : NatPowAssoc R<VAR>inst✝ : BinomialRing R<VAR>r : R<VAR>k : ℕ<GOAL>(fun x => (k + 1).factorial • x) (multichoose (r + 1) (k + 1)) = (fun x => (k + 1).factorial • x) (multichoose r (k + 1) + multichoose (r + 1) k)
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : AddCommMonoid R✝<VAR>inst✝⁵ : Pow R✝ ℕ<VAR>inst✝⁴ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝³ : NonAssocSemiring R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : NatPowAssoc R<VAR>inst✝ : BinomialRing R<VAR>r : R<VAR>k : ℕ<GOAL>(ascPochhammer ℕ (k + 1)).smeval (r + 1) = (ascPochhammer ℕ (k + 1)).smeval r + (k + 1).factorial • multichoose (r + 1) k
<VAR>α : Type u<VAR>m n : ℕ<VAR>f : Fin (m * n) → α<VAR>i : Fin m<VAR>j : Fin n<GOAL>↑i * n + n = (↑i + 1) * n
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : X → A<VAR>x✝ : X<GOAL>(⇑((lift R) f) ∘ ι R) x✝ = f x✝
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : X → A<VAR>x✝ : X<GOAL>({ toFun := FreeAlgebra.liftAux R, invFun := fun F => ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ } f) (Quot.mk (Rel R X) (Pre.of x✝)) = f x✝
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>hf : LSeriesSummable f s<VAR>hg : LSeriesSummable g s<GOAL>LSeries (f + g) s = LSeries f s + LSeries g s
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>x y : 𝕎 R<GOAL>WittVector.ghostFun (x * y) = WittVector.ghostFun x * WittVector.ghostFun y
<VAR>G : Type u<VAR>M : Type v<VAR>α : Type w<VAR>s✝ : Set α<VAR>m : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>c : G<VAR>s : Set α<GOAL>EventuallyConst (c • s) (ae μ) ↔ EventuallyConst s (ae μ)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝¹⁹ : Semiring R₁<VAR>inst✝¹⁸ : Semiring R₂<VAR>inst✝¹⁷ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>inst✝¹⁶ : TopologicalSpace M₁<VAR>inst✝¹⁵ : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹⁴ : TopologicalSpace M'₁<VAR>inst✝¹³ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝¹² : TopologicalSpace M₂<VAR>inst✝¹¹ : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝¹⁰ : TopologicalSpace M₃<VAR>inst✝⁹ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝⁸ : TopologicalSpace M₄<VAR>inst✝⁷ : AddCommMonoid M₄<VAR>inst✝⁶ : Module R₁ M₁<VAR>inst✝⁵ : Module R₁ M'₁<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>F : Type u_9<VAR>inst✝¹ : ContinuousAdd M₁<VAR>inst✝ : ContinuousAdd M'₁<GOAL>(inl R₁ M₁ M'₁).coprod (inr R₁ M₁ M'₁) = id R₁ (M₁ × M'₁)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝¹⁹ : Semiring R₁<VAR>inst✝¹⁸ : Semiring R₂<VAR>inst✝¹⁷ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>inst✝¹⁶ : TopologicalSpace M₁<VAR>inst✝¹⁵ : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹⁴ : TopologicalSpace M'₁<VAR>inst✝¹³ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝¹² : TopologicalSpace M₂<VAR>inst✝¹¹ : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝¹⁰ : TopologicalSpace M₃<VAR>inst✝⁹ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝⁸ : TopologicalSpace M₄<VAR>inst✝⁷ : AddCommMonoid M₄<VAR>inst✝⁶ : Module R₁ M₁<VAR>inst✝⁵ : Module R₁ M'₁<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>F : Type u_9<VAR>inst✝¹ : ContinuousAdd M₁<VAR>inst✝ : ContinuousAdd M'₁<GOAL>↑((inl R₁ M₁ M'₁).coprod (inr R₁ M₁ M'₁)) = ↑(id R₁ (M₁ × M'₁))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : StandardBorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>StandardBorelSpace ↑s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : StandardBorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>w✝ : TopologicalSpace α<VAR>left✝¹ : BorelSpace α<VAR>left✝ : PolishSpace α<VAR>s_closed : IsClosed s<VAR>right✝ : IsOpen s<GOAL>StandardBorelSpace ↑s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : StandardBorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>w✝ : TopologicalSpace α<VAR>left✝¹ : BorelSpace α<VAR>left✝ : PolishSpace α<VAR>s_closed : IsClosed s<VAR>right✝ : IsOpen s<VAR>this : PolishSpace ↑s<GOAL>StandardBorelSpace ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m✝ n✝ m n : ℕ<VAR>hm : m < minimalPeriod f x<VAR>hmn : f^[m] x = f^[n] x<GOAL>m ≤ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m✝ n✝ m n : ℕ<VAR>hm : m < minimalPeriod f x<VAR>hmn : f^[m] x = f^[n] x<VAR>hmn' : n < m<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m✝ n✝ m n : ℕ<VAR>hm : m < minimalPeriod f x<VAR>hmn : f^[m - n] (f^[n] x) = f^[n] x<VAR>hmn' : n < m<GOAL>False
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Nontrivial R<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hI : comap (algebraMap R S) I = ⊥<GOAL>I = ⊥
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Nontrivial R<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hI : comap (algebraMap R S) I = ⊥<VAR>x : S<VAR>hx : x ∈ I<GOAL>x ∈ ⊥
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<GOAL>volume {a} = 0
<VAR>b✝ : Game<VAR>b : PGame<VAR>c✝ : Game<VAR>c : PGame<VAR>h : Quot.mk Setoid.r b ⧏ Quot.mk Setoid.r c<VAR>a✝ : Game<VAR>a : PGame<GOAL>Quot.mk Setoid.r a + Quot.mk Setoid.r b ⧏ Quot.mk Setoid.r a + Quot.mk Setoid.r c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>Icc a b \ Ioc a b = {a}
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup Fₗ<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁵ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedSpace 𝕜₂ F<VAR>inst✝² : NormedSpace 𝕜₃ G<VAR>inst✝¹ : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f g : E →SL[σ₁₂] F<VAR>x✝ y z : E<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>hn : ‖f‖ = 0<VAR>x : E<GOAL>‖f‖ * ‖x‖ = 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup Fₗ<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁵ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedSpace 𝕜₂ F<VAR>inst✝² : NormedSpace 𝕜₃ G<VAR>inst✝¹ : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>g : E →SL[σ₁₂] F<VAR>x y z : E<VAR>inst✝ : RingHomIsometric σ₁₂<GOAL>‖0‖ = 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset α<VAR>f : α → β<GOAL>(List.map f s.toList).prod = s.prod f
<VAR>x y : ℝ<GOAL>sinh x ^ 2 = cosh x ^ 2 - 1
<VAR>x y : ℝ<GOAL>↑(sinh x ^ 2) = ↑(cosh x ^ 2 - 1)
<VAR>x y : ℝ*<VAR>hx : x.Infinitesimal<VAR>hy : y.Infinitesimal<GOAL>(x * y).Infinitesimal
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : StrongRankCondition R<VAR>ι : Type u_1<VAR>v : ι → M<VAR>i : LinearIndependent R v<VAR>w : Set M<VAR>inst✝ : Finite ↑w<VAR>s : range v ≤ ↑(span R w)<VAR>this : Fintype ↑w := Fintype.ofFinite ↑w<VAR>t : Finset ι<VAR>v' : ↑↑t → M := fun x => v ↑x<GOAL>t.card ≤ Fintype.card ↑w
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : StrongRankCondition R<VAR>ι : Type u_1<VAR>v : ι → M<VAR>i : LinearIndependent R v<VAR>w : Set M<VAR>inst✝ : Finite ↑w<VAR>s : range v ≤ ↑(span R w)<VAR>this : Fintype ↑w := Fintype.ofFinite ↑w<VAR>t : Finset ι<VAR>v' : ↑↑t → M := fun x => v ↑x<VAR>i' : LinearIndependent (ι := ↑↑t) R v'<GOAL>t.card ≤ Fintype.card ↑w
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : StrongRankCondition R<VAR>ι : Type u_1<VAR>v : ι → M<VAR>i : LinearIndependent R v<VAR>w : Set M<VAR>inst✝ : Finite ↑w<VAR>s : range v ≤ ↑(span R w)<VAR>this : Fintype ↑w := Fintype.ofFinite ↑w<VAR>t : Finset ι<VAR>v' : ↑↑t → M := fun x => v ↑x<VAR>i' : LinearIndependent (ι := ↑↑t) R v'<VAR>s' : range v' ≤ ↑(span R w)<GOAL>t.card ≤ Fintype.card ↑w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Setoid α<GOAL>EqvGen.Setoid Setoid.r ≤ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Setoid α<GOAL>sInf {s | ∀ ⦃x y : α⦄, Setoid.r x y → s.Rel x y} ≤ r
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : CommRing S<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✝ : Nontrivial R<GOAL>lift.{v', v} (Module.rank R M) + lift.{v, v'} (Module.rank R M') ≤ Module.rank R (M × M')
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : CommRing S<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✝ : Nontrivial R<GOAL>lift.{v', v} (Module.rank R M) = Module.rank R ((M × M') ⧸ ker (LinearMap.fst R M M'))
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : CommRing S<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✝ : Nontrivial R<GOAL>lift.{v, v'} (Module.rank R M') = Module.rank R ↥(ker (LinearMap.fst R M M'))
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>T : Subring R<VAR>p : (↥T)[X]<VAR>n : ℕ<GOAL>(ofSubring T p).coeff n = ↑(p.coeff n)
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>T : Subring R<VAR>p : (↥T)[X]<VAR>n : ℕ<GOAL>p.coeff n = 0 → 0 = ↑(p.coeff n)
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>T : Subring R<VAR>p : (↥T)[X]<VAR>n : ℕ<VAR>h : p.coeff n = 0<GOAL>0 = ↑(p.coeff n)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>x : ↑(Proj.restrict ⋯).toTopCat<VAR>z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>HomogeneousLocalization.mk z ∈ carrier x ↔ ↑z.num ∈ (↑x).asHomogeneousIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>x : ↑(Proj.restrict ⋯).toTopCat<VAR>z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>↑z.num ∈ (↑x).asHomogeneousIdeal.toIdeal ↔ ↑z.num ∈ (↑x).asHomogeneousIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>x : ↑(Proj.restrict ⋯).toTopCat<VAR>z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>(↑x).asHomogeneousIdeal.toIdeal.IsPrime
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>x : ↑(Proj.restrict ⋯).toTopCat<VAR>z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>Disjoint ↑(Submonoid.powers f) ↑(↑x).asHomogeneousIdeal.toIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>x : ↑(Proj.restrict ⋯).toTopCat<VAR>z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>IsUnit (IsLocalization.mk' (Localization (Submonoid.powers f)) 1 ⟨↑z.den, ⋯⟩)
<VAR>M : Type u_1<VAR>inst✝³ : Mul M<VAR>inst✝² : Finite M<VAR>G : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>H : Subgroup G<VAR>n : ℕ<VAR>h0 : n ≠ 0<VAR>h2 : Even n<VAR>h1 : n ≠ 1<GOAL>reciprocalFactors n = 3 :: reciprocalFactors (n / 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁵ : Zero α<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : SMulZeroClass α β<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : PosSMulReflectLT α β<VAR>h : a • b < 0<VAR>ha : 0 ≤ a<GOAL>a • b < a • 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel α γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>g : β × γ → ℝ≥0∞<VAR>hg : Measurable g<GOAL>∫⁻ (c : β × γ), g c ∂(κ ×ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂η a ∂κ a
<VAR>F : Type u_1<VAR>R✝ : Type u_2<VAR>A✝ : Type u_3<VAR>B : Type u_4<VAR>C : Type u_5<VAR>D : Type u_6<VAR>inst✝¹⁸ : CommSemiring R✝<VAR>inst✝¹⁷ : Semiring A✝<VAR>inst✝¹⁶ : Algebra R✝ A✝<VAR>inst✝¹⁵ : Star A✝<VAR>inst✝¹⁴ : Semiring B<VAR>inst✝¹³ : Algebra R✝ B<VAR>inst✝¹² : Star B<VAR>inst✝¹¹ : Semiring C<VAR>inst✝¹⁰ : Algebra R✝ C<VAR>inst✝⁹ : Star C<VAR>inst✝⁸ : Semiring D<VAR>inst✝⁷ : Algebra R✝ D<VAR>inst✝⁶ : Star D<VAR>R : Type u_7<VAR>A : Type u_8<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : StarRing R<VAR>inst✝³ : Semiring A<VAR>inst✝² : StarMul A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : StarModule R A<GOAL>∀ (x : R), (↑↑{ toFun := ⇑(algebraMap R A), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }.toRingHom).toFun (star x) = star ((↑↑{ toFun := ⇑(algebraMap R A), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }.toRingHom).toFun x)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : PerfectRing k p<VAR>a : 𝕎 k<VAR>ha : a ≠ 0<GOAL>∃ m b, a = ↑p ^ m * ↑b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : PerfectRing k p<VAR>a : 𝕎 k<VAR>ha : a ≠ 0<VAR>m : ℕ<VAR>b : 𝕎 k<VAR>h₁ : b.coeff 0 ≠ 0<VAR>h₂ : a = ↑p ^ m * b<GOAL>∃ m b, a = ↑p ^ m * ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<GOAL>count ∅ = 0
<VAR>m : ℕ<GOAL>shiftLeft' true m 0 + 1 = (m + 1) * 2 ^ 0
<VAR>m k : ℕ<GOAL>shiftLeft' true m (k + 1) + 1 = (m + 1) * 2 ^ (k + 1)
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>k : K<GOAL>(C k).intDegree = 0
<VAR>s : List Char<VAR>i b e n : Nat<GOAL>go₁ s { byteIdx := i + n } { byteIdx := b + n } { byteIdx := e + n } = go₁ s { byteIdx := i } { byteIdx := b } { byteIdx := e }
<VAR>s : List Char<VAR>i b e n : Nat<GOAL>∀ (c : Char) (cs : List Char), go₂ (c :: cs) { byteIdx := b + n } { byteIdx := e + n } = go₂ (c :: cs) { byteIdx := b } { byteIdx := e }
<VAR>s : List Char<VAR>i b e n : Nat<GOAL>∀ (c : Char) (cs : List Char) (i : Pos), ¬i = { byteIdx := b } → go₁ cs { byteIdx := i.byteIdx + c.utf8Size + n } { byteIdx := b + n } { byteIdx := e + n } = go₁ cs (i + c) { byteIdx := b } { byteIdx := e } → (if { byteIdx := i.byteIdx + n } = { byteIdx := b + n } then go₂ (c :: cs) { byteIdx := i.byteIdx + n } { byteIdx := e + n } else go₁ cs ({ byteIdx := i.byteIdx + n } + c) { byteIdx := b + n } { byteIdx := e + n }) = if i = { byteIdx := b } then go₂ (c :: cs) i { byteIdx := e } else go₁ cs (i + c) { byteIdx := b } { byteIdx := e }
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>x : X<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : Nonempty N<VAR>i : N<VAR>p : ↑(Ω^ N X x)<GOAL>(⟦p⟧)⁻¹ = ⟦symmAt i p⟧
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>x : X<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : Nonempty N<VAR>i : N<VAR>p : ↑(Ω^ N X x)<GOAL>(⟦p⟧)⁻¹ = ⟦fromLoop (Classical.arbitrary N) (Path.symm (toLoop (Classical.arbitrary N) p))⟧