ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y✝ z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>y : α<GOAL>(∀ ⦃c : ℝ⦄, ε < c → dist y x < c) ↔ ∀ i > ε, y ∈ ball x i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : OrderedRing α<VAR>inst✝⁵ : OrderedRing β<VAR>inst✝⁴ : LocallyFiniteOrder α<VAR>inst✝³ : LocallyFiniteOrder β<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>n : ℕ<GOAL>(box (n + 1)).card = (Icc (-↑n.succ) ↑n.succ).card * (Icc (-↑n.succ) ↑n.succ).card - (Icc (-↑n) ↑n).card * (Icc (-↑n) ↑n).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : OrderedRing α<VAR>inst✝⁵ : OrderedRing β<VAR>inst✝⁴ : LocallyFiniteOrder α<VAR>inst✝³ : LocallyFiniteOrder β<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>n : ℕ<GOAL>(Icc (-↑n.succ).1 (↑n.succ).1).card * (Icc (-↑n.succ).2 (↑n.succ).2).card - (Icc (-↑n).1 (↑n).1).card * (Icc (-↑n).2 (↑n).2).card = (Icc (-↑n.succ) ↑n.succ).card * (Icc (-↑n.succ) ↑n.succ).card - (Icc (-↑n) ↑n).card * (Icc (-↑n) ↑n).card
<VAR>z x✝ y✝ : ℝ<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>hn : n ≠ 0<VAR>x y : α<VAR>h : x < y<VAR>hy : 0 < y<GOAL>∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
<VAR>z x✝ y✝ : ℝ<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>hn : n ≠ 0<VAR>x y : α<VAR>h : x < y<VAR>hy : 0 < y<VAR>q₂ : ℚ<VAR>hx₂ : max x 0 < ↑q₂<VAR>hy₂ : ↑q₂ < y<GOAL>∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
<VAR>z x✝ y✝ : ℝ<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>hn : n ≠ 0<VAR>x y : α<VAR>h : x < y<VAR>hy : 0 < y<VAR>q₂ : ℚ<VAR>hx₂ : max x 0 < ↑q₂<VAR>hy₂ : ↑q₂ < y<VAR>q₁ : ℚ<VAR>hx₁ : max x 0 < ↑q₁<VAR>hq₁₂ : ↑q₁ < ↑q₂<GOAL>∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
<VAR>z x✝ y✝ : ℝ<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>hn : n ≠ 0<VAR>x y : α<VAR>h : x < y<VAR>hy : 0 < y<VAR>q₂ : ℚ<VAR>hx₂ : max x 0 < ↑q₂<VAR>hy₂ : ↑q₂ < y<VAR>q₁ : ℚ<VAR>hx₁ : max x 0 < ↑q₁<VAR>hq₁₂ : ↑q₁ < ↑q₂<VAR>this : 0 < ↑q₂<GOAL>∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
<VAR>z x✝ y✝ : ℝ<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>hn : n ≠ 0<VAR>x y : α<VAR>h : x < y<VAR>hy : 0 < y<VAR>q₂ : ℚ<VAR>hx₂ : max x 0 < ↑q₂<VAR>hy₂ : ↑q₂ < y<VAR>q₁ : ℚ<VAR>hx₁ : max x 0 < ↑q₁<VAR>hq₁₂ : q₁ < q₂<VAR>this : 0 < q₂<GOAL>∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
<VAR>z x✝ y✝ : ℝ<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>hn : n ≠ 0<VAR>x y : α<VAR>h : x < y<VAR>hy : 0 < y<VAR>q₂ : ℚ<VAR>hx₂ : max x 0 < ↑q₂<VAR>hy₂ : ↑q₂ < y<VAR>q₁ : ℚ<VAR>hx₁ : max x 0 < ↑q₁<VAR>hq₁₂ : q₁ < q₂<VAR>this : 0 < q₂<VAR>q : ℚ<VAR>hq : 0 < q<VAR>hq₁ : q₁ < q ^ n<VAR>hq₂ : q ^ n < q₂<GOAL>∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
<VAR>w : List ℕ<VAR>hw : List.Sorted (fun x x_1 => x ≥ x_1) w<VAR>i : Fin w.length<GOAL>(ofRowLens w hw).rowLen ↑i = w.get i
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n : ℕ<VAR>inst✝ : DivisionRing R<VAR>a : ℚ<VAR>f : R[X]<GOAL>a • f = C ↑a * f
<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>f : X ≅ Y<GOAL>inv f.hom = f.inv
<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>f : X ≅ Y<GOAL>f.hom ≫ f.inv = 𝟙 X
<VAR>m : Type u → Type u<VAR>inst✝¹ : _root_.Monad m<VAR>inst✝ : LawfulMonad m<VAR>α β : Type u<VAR>f : α → β<VAR>a : (ofTypeFunctor m ⋙ ofTypeFunctor m).obj α<GOAL>((ofTypeFunctor m ⋙ ofTypeFunctor m).map f ≫ joinM) a = (joinM ≫ (ofTypeFunctor m).map f) a
<VAR>m : Type u → Type u<VAR>inst✝¹ : _root_.Monad m<VAR>inst✝ : LawfulMonad m<VAR>α : Type u<VAR>a : (ofTypeFunctor m).obj ((ofTypeFunctor m ⋙ ofTypeFunctor m).obj α)<GOAL>((ofTypeFunctor m).map ({ app := @joinM m inst✝¹, naturality := ⋯ }.app α) ≫ { app := @joinM m inst✝¹, naturality := ⋯ }.app α) a = ({ app := @joinM m inst✝¹, naturality := ⋯ }.app ((ofTypeFunctor m).obj α) ≫ { app := @joinM m inst✝¹, naturality := ⋯ }.app α) a
<VAR>m : Type u → Type u<VAR>inst✝¹ : _root_.Monad m<VAR>inst✝ : LawfulMonad m<VAR>α : Type u<VAR>a : (𝟭 (Type u)).obj ((ofTypeFunctor m).obj α)<GOAL>({ app := @pure m Applicative.toPure, naturality := ⋯ }.app ((ofTypeFunctor m).obj α) ≫ { app := @joinM m inst✝¹, naturality := ⋯ }.app α) a = 𝟙 ((𝟭 (Type u)).obj ((ofTypeFunctor m).obj α)) a
<VAR>m : Type u → Type u<VAR>inst✝¹ : _root_.Monad m<VAR>inst✝ : LawfulMonad m<VAR>α : Type u<VAR>a : (ofTypeFunctor m).obj ((𝟭 (Type u)).obj α)<GOAL>((ofTypeFunctor m).map ({ app := @pure m Applicative.toPure, naturality := ⋯ }.app α) ≫ { app := @joinM m inst✝¹, naturality := ⋯ }.app α) a = 𝟙 ((ofTypeFunctor m).obj ((𝟭 (Type u)).obj α)) a
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>P : Subobject X<VAR>Q : MonoOver X<GOAL>mk (arrow (Quotient.mk'' Q)) = Quotient.mk'' Q
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>P : Subobject X<VAR>Q : MonoOver X<VAR>e : (Quotient.mk'' Q).out' ≅ Q<GOAL>mk (arrow (Quotient.mk'' Q)) = Quotient.mk'' Q
<VAR>x : ℤ[i]<GOAL>norm x = 0 ↔ x = 0
<VAR>x : ℤ[i]<GOAL>↑(norm x) = ↑0 ↔ x = 0
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n✝ : A<VAR>C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop<VAR>algebraMap : ∀ (r : R), C 0 ((_root_.algebraMap R A) r) ⋯<VAR>add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯<VAR>mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯<VAR>n : ℕ<VAR>n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx<VAR>x : A<GOAL>∀ (hx : x ∈ M ^ (n + 1)), C (n + 1) x hx
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n✝ : A<VAR>C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop<VAR>algebraMap : ∀ (r : R), C 0 ((_root_.algebraMap R A) r) ⋯<VAR>add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯<VAR>mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯<VAR>n : ℕ<VAR>n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx<VAR>x : A<GOAL>∀ (hx : x ∈ M * M ^ n), C (n + 1) x ⋯
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n✝ : A<VAR>C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop<VAR>algebraMap : ∀ (r : R), C 0 ((_root_.algebraMap R A) r) ⋯<VAR>add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯<VAR>mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯<VAR>n : ℕ<VAR>n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx<VAR>x : A<VAR>hx : x ∈ M * M ^ n<GOAL>C (n + 1) x ⋯
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic R<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>φ : R →+* S<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableEq R<GOAL>P.roots.toFinset.card ≤ 3
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic R<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>φ : R →+* S<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableEq R<GOAL>card P.toPoly.roots ≤ 3
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>hα : ¬α.IsZero<GOAL>chainTopCoeff (⇑α) β ≤ chainLength α β
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>hα : ¬α.IsZero<GOAL>¬(chainLength α β).succ ≤ chainTopCoeff (⇑α) β
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>hα : ¬α.IsZero<VAR>e : (chainLength α β).succ ≤ chainTopCoeff (⇑α) β<GOAL>False
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>hα : ¬α.IsZero<VAR>e : (chainLength α β).succ ≤ chainTopCoeff (⇑α) β<GOAL>weightSpace L ((chainTopCoeff (⇑α) β - (chainLength α β).succ) • ⇑α + ⇑β) = ⊥
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>hα : ¬α.IsZero<VAR>e : (chainLength α β).succ ≤ chainTopCoeff (⇑α) β<GOAL>weightSpace L (-((chainLength α β).succ • ⇑α) + ⇑(chainTop (⇑α) β)) = ⊥
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>d : TransversalPair G A B<VAR>a₁✝ a₂✝ : G<VAR>h : ((fun x x_1 => x • x_1) ∘ ⇑of) a₁✝ = ((fun x x_1 => x • x_1) ∘ ⇑of) a₂✝<GOAL>a₁✝ = a₂✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : InfConvergenceClass α<VAR>f : ι → α<VAR>a : α<VAR>h_anti : Antitone f<VAR>ha : IsGLB (range f) a<GOAL>Tendsto f atTop (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>s : Finset α<VAR>h : mulSupport f ⊆ ↑s<GOAL>⋯.toFinset ⊆ s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.96949, u_1} C<VAR>inst✝² : Category.{?u.96953, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S S₁ S₂ : ShortComplex C<VAR>s : S₁.Splitting<VAR>e : S₁ ≅ S₂<GOAL>S₂.f ≫ e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.96949, u_1} C<VAR>inst✝² : Category.{?u.96953, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S S₁ S₂ : ShortComplex C<VAR>s : S₁.Splitting<VAR>e : S₁ ≅ S₂<GOAL>(e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.96949, u_1} C<VAR>inst✝² : Category.{?u.96953, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S S₁ S₂ : ShortComplex C<VAR>s : S₁.Splitting<VAR>e : S₁ ≅ S₂<GOAL>(e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.96949, u_1} C<VAR>inst✝² : Category.{?u.96953, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S S₁ S₂ : ShortComplex C<VAR>s : S₁.Splitting<VAR>e : S₁ ≅ S₂<VAR>eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = e.inv.τ₂ ≫ 𝟙 S₁.X₂ ≫ e.hom.τ₂<GOAL>(e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.96949, u_1} C<VAR>inst✝² : Category.{?u.96953, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S S₁ S₂ : ShortComplex C<VAR>s : S₁.Splitting<VAR>e : S₁ ≅ S₂<VAR>eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = 𝟙 S₂.X₂<GOAL>(e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝³ : CommMonoid β<VAR>inst✝² : CommMonoid γ<VAR>G : Type u_6<VAR>inst✝¹ : FunLike G β γ<VAR>inst✝ : MonoidHomClass G β γ<VAR>g : G<VAR>f : α → β<VAR>s : Finset α<GOAL>g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝³ : CommMonoid β<VAR>inst✝² : CommMonoid γ<VAR>G : Type u_6<VAR>inst✝¹ : FunLike G β γ<VAR>inst✝ : MonoidHomClass G β γ<VAR>g : G<VAR>f : α → β<VAR>s : Finset α<GOAL>(Multiset.map (⇑g ∘ f) s.val).prod = (Multiset.map (fun x => g (f x)) s.val).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Finite α<VAR>r : α → α → Prop<VAR>inst✝¹ : IsTrans α r<VAR>inst✝ : IsIrrefl α r<GOAL>WellFounded r
<VAR>a b c✝ d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>c : ℕ<VAR>H : a % d = b % d<GOAL>(a + c) % d = (b + c) % d
<VAR>G : Type u_1<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : Group G<VAR>inst✝² : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>Measurable fun y => μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s))
<VAR>G : Type u_1<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : Group G<VAR>inst✝² : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>MeasurableSet ((fun z => (1, z.1 * z.2)) ⁻¹' univ ×ˢ s)
<VAR>G : Type u_1<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : Group G<VAR>inst✝² : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>MeasurableSpace G
<VAR>F : Type u_1<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>x : ℂ<VAR>A : SL(2, ℤ)<GOAL>IsBoundedAtImInfty (⇑(SlashInvariantForm.const x) ∣[0] A)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<GOAL>finInsepDegree F ↥⊥ = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>M' : Type u_3<VAR>N' : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass M'<VAR>inst✝¹ : MulOneClass N'<VAR>inst✝ : MulOneClass P<VAR>C : M ∗ N → Prop<VAR>m : M ∗ N<VAR>one : C 1<VAR>inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (inl m * x)<VAR>inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (inr n * x)<GOAL>C m
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>M' : Type u_3<VAR>N' : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass M'<VAR>inst✝¹ : MulOneClass N'<VAR>inst✝ : MulOneClass P<VAR>C : M ∗ N → Prop<VAR>one : C 1<VAR>inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (inl m * x)<VAR>inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (inr n * x)<VAR>x : FreeMonoid (M ⊕ N)<GOAL>C (mk x)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x✝ : α<VAR>l : List α<VAR>hl : 2 ≤ l.length<VAR>hn : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.formPerm.toList x ~r l
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x : α<VAR>l : List α<VAR>hl : 2 ≤ l.length<VAR>hn : l.Nodup<VAR>k : Fin l.length<VAR>hx : l.get k ∈ l<GOAL>l.formPerm.toList (l.get k) ~r l
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x : α<VAR>l : List α<VAR>hl : 2 ≤ l.length<VAR>hn : l.Nodup<VAR>k : Fin l.length<VAR>hx : l.get k ∈ l<VAR>hr : l ~r l.rotate ↑k<GOAL>l.formPerm.toList (l.get k) ~r l
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x : α<VAR>l : List α<VAR>hl : 2 ≤ l.length<VAR>hn : l.Nodup<VAR>k : Fin l.length<VAR>hx : l.get k ∈ l<VAR>hr : l ~r l.rotate ↑k<GOAL>(l.rotate ↑k).formPerm.toList (l.get k) ~r l
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x : α<VAR>l : List α<VAR>hl : 2 ≤ l.length<VAR>hn : l.Nodup<VAR>k : Fin l.length<VAR>hx : l.get k ∈ l<VAR>hr : l ~r l.rotate ↑k<GOAL>(l.rotate ↑k).formPerm.toList ((l.rotate ↑k).get ⟨(l.length - ↑k % l.length + ↑k) % l.length, ⋯⟩) ~r l
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x : α<VAR>l : List α<VAR>hl : 2 ≤ l.length<VAR>hn : l.Nodup<VAR>k : Fin l.length<VAR>hx : l.get k ∈ l<VAR>hr : l ~r l.rotate ↑k<GOAL>(l.rotate ↑k).formPerm.toList ((l.rotate ↑k).get ⟨0, ⋯⟩) ~r l
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x : α<VAR>l : List α<VAR>hl : 2 ≤ l.length<VAR>hn : l.Nodup<VAR>k : Fin l.length<VAR>hx : l.get k ∈ l<VAR>hr : l ~r l.rotate ↑k<GOAL>l.rotate ↑k ~r l
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x : α<VAR>l : List α<VAR>hl : 2 ≤ l.length<VAR>hn : l.Nodup<VAR>k : Fin l.length<VAR>hx : l.get k ∈ l<VAR>hr : l ~r l.rotate ↑k<GOAL>2 ≤ (l.rotate ↑k).length
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x : α<VAR>l : List α<VAR>hl : 2 ≤ l.length<VAR>hn : l.Nodup<VAR>k : Fin l.length<VAR>hx : l.get k ∈ l<VAR>hr : l ~r l.rotate ↑k<GOAL>(l.rotate ↑k).Nodup
<VAR>α : Type u_1<VAR>sel : Set α → Option α<VAR>n₁ n₂ : ℕ<VAR>a : α<VAR>s : Set α<VAR>h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s<VAR>h₁ : enumerate sel s n₁ = some a<VAR>h₂ : enumerate sel s n₂ = some a<GOAL>n₁ = n₂
<VAR>α : Type u_1<VAR>sel : Set α → Option α<VAR>n₁ n₂ : ℕ<VAR>a : α<VAR>s : Set α<VAR>h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s<VAR>h₁ : enumerate sel s n₁ = some a<VAR>h₂ : enumerate sel s n₂ = some a<VAR>hn : n₁ ≤ n₂<GOAL>n₁ = n₂
<VAR>α : Type u_1<VAR>sel : Set α → Option α<VAR>n₁ n₂ : ℕ<VAR>a : α<VAR>s : Set α<VAR>h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s<VAR>h₁ : enumerate sel s n₁ = some a<VAR>h₂ : enumerate sel s n₂ = some a<VAR>hn : n₂ ≤ n₁<GOAL>n₁ = n₂
<VAR>α : Type u_1<VAR>sel : Set α → Option α<VAR>n₂ n₁ : ℕ<VAR>a : α<VAR>s : Set α<VAR>h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s<VAR>h₂ : enumerate sel s n₂ = some a<VAR>h₁ : enumerate sel s n₁ = some a<VAR>hn : n₁ ≤ n₂<GOAL>n₂ = n₁
<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]<GOAL>Prime X
<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]<GOAL>X = X - C 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>n : ℕ<GOAL>Primrec fun a => (a.1 ::ᵥ a.2).toList
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type (max v u)<VAR>X✝¹ : C<VAR>R✝ : Presieve X✝¹<VAR>S✝ : Sieve X✝¹<VAR>inst✝¹ : R✝.hasPullbacks<VAR>P : Cᵒᵖ ⥤ Type w<VAR>X✝ : C<VAR>R : Presieve X✝<VAR>S : Sieve X✝<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>inst✝ : (Presieve.ofArrows X π).hasPullbacks<VAR>x : FirstObj P X<GOAL>Arrows.Compatible P π ((Types.productIso fun i => P.obj (op (X i))).hom x) ↔ firstMap P X π x = secondMap P X π x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type (max v u)<VAR>X✝¹ : C<VAR>R✝ : Presieve X✝¹<VAR>S✝ : Sieve X✝¹<VAR>inst✝¹ : R✝.hasPullbacks<VAR>P : Cᵒᵖ ⥤ Type w<VAR>X✝ : C<VAR>R : Presieve X✝<VAR>S : Sieve X✝<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>inst✝ : (Presieve.ofArrows X π).hasPullbacks<VAR>x : FirstObj P X<GOAL>Arrows.PullbackCompatible P π ((Types.productIso fun i => P.obj (op (X i))).hom x) ↔ firstMap P X π x = secondMap P X π x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasShift C ℤ<VAR>X : C<VAR>X✝ Y✝ : Triangle C<VAR>f : X✝ ⟶ Y✝<GOAL>(-(shiftFunctor C (-1)).map X✝.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X✝.obj₁) ≫ f.hom₁ = (shiftFunctor C (-1)).map f.hom₃ ≫ (-(shiftFunctor C (-1)).map Y✝.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app Y✝.obj₁)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasShift C ℤ<VAR>X : C<VAR>X✝ Y✝ : Triangle C<VAR>f : X✝ ⟶ Y✝<GOAL>(shiftFunctor C (-1)).map X✝.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X✝.obj₁ ≫ f.hom₁ = (shiftFunctor C (-1)).map (X✝.mor₃ ≫ (shiftFunctor C 1).map f.hom₁) ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app Y✝.obj₁
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasShift C ℤ<VAR>X : C<VAR>X✝ Y✝ : Triangle C<VAR>f : X✝ ⟶ Y✝<GOAL>(shiftFunctor C (-1)).map X✝.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X✝.obj₁ ≫ f.hom₁ = (shiftFunctor C (-1)).map X✝.mor₃ ≫ (shiftFunctor C (-1)).map ((shiftFunctor C 1).map f.hom₁) ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app Y✝.obj₁
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasShift C ℤ<VAR>X : C<VAR>X✝ Y✝ : Triangle C<VAR>f : X✝ ⟶ Y✝<GOAL>(shiftFunctor C (-1)).map X✝.mor₃ ≫ (shiftFunctor C 1 ⋙ shiftFunctor C (-1)).map f.1 ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app Y✝.obj₁ = (shiftFunctor C (-1)).map X✝.mor₃ ≫ (shiftFunctor C (-1)).map ((shiftFunctor C 1).map f.hom₁) ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app Y✝.obj₁
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasShift C ℤ<VAR>X : C<VAR>X✝ Y✝ : Triangle C<VAR>f : X✝ ⟶ Y✝<GOAL>X✝.invRotate.mor₃ ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map f.hom₃) = f.hom₂ ≫ Y✝.invRotate.mor₃
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasShift C ℤ<VAR>X : C<VAR>X✝ Y✝ : Triangle C<VAR>f : X✝ ⟶ Y✝<GOAL>X✝.mor₂ ≫ (𝟭 C).map f.hom₃ ≫ (shiftEquiv C 1).counitIso.inv.app Y✝.obj₃ = X✝.mor₂ ≫ f.hom₃ ≫ (shiftEquiv C 1).counitIso.inv.app Y✝.3
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>H : Type u_7<VAR>inst✝ : NormedAddCommGroup H<VAR>f : α → H<VAR>hf : Integrable f μ<GOAL>‖Integrable.toL1 f hf‖ = ∫ (a : α), ‖f a‖ ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>H : Type u_7<VAR>inst✝ : NormedAddCommGroup H<VAR>f : α → H<VAR>hf : Integrable f μ<GOAL>∫ (a : α), ‖↑↑(Integrable.toL1 f hf) a‖ ∂μ = ∫ (a : α), ‖f a‖ ∂μ
<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✝⁴ : CommSemiring A'<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R B<VAR>p q : R[X]<VAR>x✝ : A<VAR>f : A →ₐ[R] B<VAR>x : A<GOAL>(aeval (f x)) X = (f.comp (aeval x)) X
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝² : Mul M<VAR>s : Set M<VAR>inst✝¹ : Add A<VAR>t : Set A<VAR>S : Subsemigroup M<VAR>inst✝ : Subsingleton (Subsemigroup M)<VAR>x y : M<GOAL>x = y
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝² : Mul M<VAR>s : Set M<VAR>inst✝¹ : Add A<VAR>t : Set A<VAR>S : Subsemigroup M<VAR>inst✝ : Subsingleton (Subsemigroup M)<VAR>x y : M<VAR>this : ∀ (a : M), a ∈ ⊥<GOAL>x = y