ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ : C ⥤ D<VAR>R₁ R₂ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : L₂ ⟶ L₁<VAR>c : C<GOAL>adj₁.unit.app c ≫ 𝟙 (R₁.obj (L₁.obj c)) ≫ (adj₂.unit.app (R₁.obj (L₁.obj c)) ≫ R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫ R₂.map (adj₁.counit.app (L₁.obj c))) ≫ 𝟙 (R₂.obj (L₁.obj c)) = adj₂.unit.app c ≫ R₂.map (α.app c)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ : C ⥤ D<VAR>R₁ R₂ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : L₂ ⟶ L₁<VAR>c : C<GOAL>adj₁.unit.app c ≫ adj₂.unit.app (R₁.obj (L₁.obj c)) ≫ R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫ R₂.map (adj₁.counit.app (L₁.obj c)) = adj₂.unit.app c ≫ R₂.map (α.app c)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ : C ⥤ D<VAR>R₁ R₂ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : L₂ ⟶ L₁<VAR>c : C<VAR>this : (𝟭 C).map (adj₁.unit.app c) ≫ ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)).app (L₁.obj c) = adj₂.unit.app ((𝟭 C).obj ((𝟭 C).obj c)) ≫ R₂.map ((L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv).app ((𝟭 C).obj c))<GOAL>adj₁.unit.app c ≫ adj₂.unit.app (R₁.obj (L₁.obj c)) ≫ R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫ R₂.map (adj₁.counit.app (L₁.obj c)) = adj₂.unit.app c ≫ R₂.map (α.app c)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>|a - c| = |a - b + (b - c)|
<VAR>n m : ℕ<GOAL>Nontrivial (Fin n) ↔ 2 ≤ n
<VAR>a b : Ordinal.{u_1}<GOAL>a ^ (1 + b) = a * a ^ b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁴ : EuclideanDomain R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : IsDomain S<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>a : S<VAR>y : ℤ<VAR>hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y<GOAL>abv ((Algebra.norm R) a) ≤ normBound abv bS * y ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁴ : EuclideanDomain R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : IsDomain S<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>a : S<VAR>y : ℤ<VAR>hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y<GOAL>abv ((Algebra.norm R) (∑ i : ι, (bS.repr a) i • bS i)) ≤ normBound abv bS * y ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁴ : EuclideanDomain R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : IsDomain S<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>a : S<VAR>y : ℤ<VAR>hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y<GOAL>abv ((LinearMap.toMatrix bS bS) ((Algebra.lmul R S) (∑ i : ι, (bS.repr a) i • bS i))).det ≤ normBound abv bS * y ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁴ : EuclideanDomain R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : IsDomain S<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>a : S<VAR>y : ℤ<VAR>hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y<GOAL>abv (∑ x : ι, (bS.repr a) x • (LinearMap.toMatrix bS bS) ((Algebra.lmul R S) (bS x))).det ≤ (Fintype.card ι).factorial • (Fintype.card ι • ((Finset.image (fun ijk => abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯ * y)) ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁴ : EuclideanDomain R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : IsDomain S<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>a : S<VAR>y : ℤ<VAR>hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y<GOAL>Fintype.card ι • ((Finset.image (fun ijk => abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯ * y) = Finset.univ.card • y * ?convert_5
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁴ : EuclideanDomain R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : IsDomain S<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>a : S<VAR>y : ℤ<VAR>hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y<GOAL>ℤ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁴ : EuclideanDomain R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : IsDomain S<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>a : S<VAR>y : ℤ<VAR>hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y<GOAL>∀ (k i j : ι), abv ((LinearMap.toMatrix bS bS) ((Algebra.lmul R S) (bS k)) i j) ≤ ?convert_5
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a \ b ≤ b ↔ a ≤ b
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>J : Type v₁<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : FinCategory J<VAR>K : J ⥤ C<VAR>F : C ⥤ D<VAR>inst✝ : RepresentablyFlat F<VAR>c : Cone K<VAR>hc : IsLimit c<VAR>s : Cone (K ⋙ F)<VAR>x : J<GOAL>lift F hc s ≫ (F.mapCone c).π.app x = s.π.app x
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>n : ℤ := modPart p r<GOAL>‖⟨↑r, h⟩ - ↑(modPart p r)‖ < 1
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>n : ℤ := modPart p r<GOAL>↑p ∣ (⟨↑r, h⟩ - ↑(modPart p r)) * ↑r.den
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>n : ℤ := modPart p r<GOAL>↑p ∣ r.num - n * ↑r.den
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : AddCommMonoid M₃<VAR>inst✝² : Module R M₃<VAR>φ : ι → Type i<VAR>inst✝¹ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝ : (i : ι) → Module R (φ i)<VAR>a : (i : ι) → φ i<VAR>h : a ∈ ⨅ i, ker (proj i)<GOAL>a ∈ ⊥
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : AddCommMonoid M₃<VAR>inst✝² : Module R M₃<VAR>φ : ι → Type i<VAR>inst✝¹ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝ : (i : ι) → Module R (φ i)<VAR>a : (i : ι) → φ i<VAR>h : ∀ (i : ι), a i = 0<GOAL>a ∈ ⊥
<VAR>d : ℤ<VAR>x : ℤ√d<GOAL>↑(-x).norm = ↑x.norm
<VAR>x y : PartENat<VAR>hx : x ≠ ⊤<GOAL>x < x + y ↔ 0 < y
<VAR>x y : PartENat<VAR>hx : x ≠ ⊤<GOAL>x < x + y ↔ x + 0 < x + y
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<GOAL>y ∈ cylinder x n ↔ dist y x ≤ (1 / 2) ^ n
<VAR>E : ℕ → Type u_1<VAR>y : (n : ℕ) → E n<VAR>n : ℕ<GOAL>y ∈ cylinder y n ↔ dist y y ≤ (1 / 2) ^ n
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<VAR>hne : y ≠ x<GOAL>y ∈ cylinder x n ↔ dist y x ≤ (1 / 2) ^ n
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<VAR>hne : y ≠ x<GOAL>(∀ i < n, y i = x i) ↔ n ≤ firstDiff y x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.27894, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.Exact<VAR>X Y : C<VAR>a : X ⟶ S.X₂<VAR>ha : a ≫ S.g = 0<VAR>b : S.X₂ ⟶ Y<VAR>hb : S.f ≫ b = 0<GOAL>a ≫ b = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.27894, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.Exact<VAR>X Y : C<VAR>a : X ⟶ S.X₂<VAR>ha : a ≫ S.g = 0<VAR>b : S.X₂ ⟶ Y<VAR>hb : S.f ≫ b = 0<VAR>this : S.HasHomology<GOAL>a ≫ b = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.27894, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.Exact<VAR>X Y : C<VAR>a : X ⟶ S.X₂<VAR>ha : a ≫ S.g = 0<VAR>b : S.X₂ ⟶ Y<VAR>hb : S.f ≫ b = 0<VAR>this : S.HasHomology<VAR>eq : S.Exact<GOAL>a ≫ b = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.27894, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.Exact<VAR>X Y : C<VAR>a : X ⟶ S.X₂<VAR>ha : a ≫ S.g = 0<VAR>b : S.X₂ ⟶ Y<VAR>hb : S.f ≫ b = 0<VAR>this : S.HasHomology<VAR>eq : S.iCycles ≫ S.pOpcycles = 0<GOAL>a ≫ b = 0
<VAR>a : ℕ<VAR>a1 : 1 < a<GOAL>yn a1 0 ≡ 0 [MOD a - 1]
<VAR>a : ℕ<VAR>a1 : 1 < a<GOAL>yn a1 1 ≡ 1 [MOD a - 1]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>yn a1 (n + 2) + yn a1 n ≡ n + 2 + n [MOD a - 1]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>2 * a * yn a1 (n + 1) ≡ 2 * (n + 1) [MOD a - 1]
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>inst✝⁸ : Ring k<VAR>inst✝⁷ : AddCommGroup V₁<VAR>inst✝⁶ : AddCommGroup V₂<VAR>inst✝⁵ : Module k V₁<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AddTorsor V₁ P₁<VAR>inst✝² : AddTorsor V₂ P₂<VAR>φ : P₁ →ᵃ[k] P₂<VAR>E : AffineSubspace k P₁<VAR>F : AffineSubspace k P₂<VAR>inst✝¹ : Nonempty ↥E<VAR>inst✝ : Nonempty ↥F<VAR>h : AffineSubspace.map φ E = F<VAR>x : P₂<VAR>hx : x ∈ F<GOAL>∃ a, (φ.restrict ⋯) a = ⟨x, hx⟩
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>inst✝⁸ : Ring k<VAR>inst✝⁷ : AddCommGroup V₁<VAR>inst✝⁶ : AddCommGroup V₂<VAR>inst✝⁵ : Module k V₁<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AddTorsor V₁ P₁<VAR>inst✝² : AddTorsor V₂ P₂<VAR>φ : P₁ →ᵃ[k] P₂<VAR>E : AffineSubspace k P₁<VAR>F : AffineSubspace k P₂<VAR>inst✝¹ : Nonempty ↥E<VAR>inst✝ : Nonempty ↥F<VAR>h : AffineSubspace.map φ E = F<VAR>x : P₂<VAR>hx✝ : x ∈ F<VAR>hx : ∃ y ∈ E, φ y = x<GOAL>∃ a, (φ.restrict ⋯) a = ⟨x, hx✝⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>F' : ι → α → β<VAR>hf : TendstoUniformlyOn F f p s<VAR>hff' : ∀ᶠ (n : ι) in p, EqOn (F n) (F' n) s<GOAL>TendstoUniformlyOn F' f p s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>F' : ι → α → β<VAR>hf : TendstoUniformlyOnFilter F f p (𝓟 s)<VAR>hff' : ∀ᶠ (n : ι) in p, EqOn (F n) (F' n) s<GOAL>TendstoUniformlyOnFilter F' f p (𝓟 s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>F' : ι → α → β<VAR>hf : TendstoUniformlyOnFilter F f p (𝓟 s)<VAR>hff' : ∀ᶠ (n : ι) in p, EqOn (F n) (F' n) s<GOAL>∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, F n.1 n.2 = F' n.1 n.2
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>F' : ι → α → β<VAR>hf : TendstoUniformlyOnFilter F f p (𝓟 s)<VAR>hff' : {x | EqOn (F x) (F' x) s} ∈ p<GOAL>{x | F x.1 x.2 = F' x.1 x.2} ∈ p ×ˢ 𝓟 s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>F' : ι → α → β<VAR>hf : TendstoUniformlyOnFilter F f p (𝓟 s)<VAR>hff' : {x | ∀ ⦃x_1 : α⦄, x_1 ∈ s → F x x_1 = F' x x_1} ∈ p<GOAL>{x | F x.1 x.2 = F' x.1 x.2} ∈ p ×ˢ 𝓟 s
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f g : α → β → β<VAR>b : β<VAR>hd : α<VAR>tl : List α<VAR>ih : (∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b) → foldr f b tl = foldr g b tl<VAR>H : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), f a b = g a b<GOAL>foldr f b (hd :: tl) = foldr g b (hd :: tl)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f g : α → β → β<VAR>b : β<VAR>hd : α<VAR>tl : List α<VAR>ih : (∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b) → foldr f b tl = foldr g b tl<VAR>H : (∀ (b : β), f hd b = g hd b) ∧ ∀ (x : α), x ∈ tl → ∀ (b : β), f x b = g x b<GOAL>foldr f b (hd :: tl) = foldr g b (hd :: tl)
<VAR>N : ℕ<VAR>inst✝ : NeZero N<VAR>χ : DirichletCharacter ℂ N<VAR>k : ZMod N<GOAL>𝓕 (⇑χ) k = gaussSum χ (stdAddChar.mulShift (-k))
<VAR>N : ℕ<VAR>inst✝ : NeZero N<VAR>χ : DirichletCharacter ℂ N<VAR>k : ZMod N<GOAL>∑ j : ZMod N, toCircle (-(j * k)) • χ j = gaussSum χ (stdAddChar.mulShift (-k))
<VAR>N : ℕ<VAR>inst✝ : NeZero N<VAR>χ : DirichletCharacter ℂ N<VAR>k j : ZMod N<GOAL>toCircle (-(j * k)) • χ j = χ j * (stdAddChar.mulShift (-k)) j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>xt : x ≠ ⊤<GOAL>(𝓝 x).HasBasis (fun x => 0 < x) fun ε => Icc (x - ε) (x + ε)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w✝ : ι → R<VAR>z : ι → E<VAR>s : Finset ι<VAR>f : ι → α<VAR>w : ι → R<VAR>hw₀ : ∀ i ∈ s, 0 ≤ w i<VAR>hw₁ : 0 < ∑ i ∈ s, w i<GOAL>s.centerMass w f ≤ s.sup' ⋯ f
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w✝ : ι → R<VAR>z : ι → E<VAR>s : Finset ι<VAR>f : ι → α<VAR>w : ι → R<VAR>hw₀ : ∀ i ∈ s, 0 ≤ w i<VAR>hw₁ : 0 < ∑ i ∈ s, w i<GOAL>∑ i ∈ s, w i • f i ≤ ∑ i ∈ s, w i • s.sup' ⋯ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>h : b ≠ 0<GOAL>a < b * succ (a / b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>h : b ≠ 0<GOAL>a < b * succ (sInf {o | a < b * succ o})
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>s : WSeq α<GOAL>(map f s).destruct = Computation.map (Option.map (Prod.map f (map f))) s.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>s : WSeq α<GOAL>Computation.IsBisimulation fun c1 c2 => ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>s : WSeq α<GOAL>∃ s_1, (map f s).destruct = (map f s_1).destruct ∧ Computation.map (Option.map (Prod.map f (map f))) s.destruct = Computation.map (Option.map (Prod.map f (map f))) s_1.destruct
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>a : α<VAR>s : Multiset α<GOAL>(map (fun x => a * x) s).gcd = normalize a * s.gcd
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>a : α<VAR>s : Multiset α<GOAL>(map (fun x => a * x) 0).gcd = normalize a * gcd 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>a : α<VAR>s✝ : Multiset α<VAR>b : α<VAR>s : Multiset α<VAR>ih : (map (fun x => a * x) s).gcd = normalize a * s.gcd<GOAL>(map (fun x => a * x) (b ::ₘ s)).gcd = normalize a * (b ::ₘ s).gcd
<VAR>μ : YoungDiagram<VAR>i j : ℕ<GOAL>(i, j) ∈ (ofRowLens μ.rowLens ⋯).cells ↔ (i, j) ∈ μ.cells
<VAR>μ : YoungDiagram<VAR>i j : ℕ<GOAL>(∃ (h : i < μ.colLen 0), j < μ.rowLens.get ⟨i, ⋯⟩) ↔ (i, j) ∈ μ
<VAR>x n : ℂ<VAR>hx : x.arg ≠ π<GOAL>x⁻¹ ^ n = (x ^ n)⁻¹
<VAR>β✝ : Type w<VAR>α : Type w₂<VAR>γ : Type w₃<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>β : Type w<VAR>f : β → C<VAR>inst✝ : HasCoproduct f<VAR>P : C<VAR>p : (b : β) → f b ⟶ P<VAR>b : β<GOAL>ι f b ≫ desc p = p b
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : Associates α<VAR>a✝ : Nontrivial α<GOAL>(a.factors ⊔ b.factors).prod * (a.factors ⊓ b.factors).prod = a * b
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : Associates α<VAR>a✝ : Nontrivial α<GOAL>((a.factors ⊔ b.factors).prod * (a.factors ⊓ b.factors).prod).factors = (a * b).factors
<VAR>a : ℤ<GOAL>(↑a)⁻¹.num = a.sign
<VAR>a : ℤ<VAR>lt : a < 0<GOAL>(↑a)⁻¹.num = a.sign
<GOAL>(↑0)⁻¹.num = Int.sign 0
<VAR>a : ℤ<VAR>gt : 0 < a<GOAL>(↑a)⁻¹.num = a.sign
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>x : FamilyOfElements P (generate R).arrows<VAR>t : x.Compatible<GOAL>(FamilyOfElements.restrict ⋯ x).sieveExtend = x
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>x : FamilyOfElements P (generate R).arrows<VAR>t : x.SieveCompatible<GOAL>(FamilyOfElements.restrict ⋯ x).sieveExtend = x
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>x : FamilyOfElements P (generate R).arrows<VAR>t : x.SieveCompatible<VAR>x✝¹ : C<VAR>x✝ : x✝¹ ⟶ X<VAR>h : (generate R).arrows x✝<GOAL>(FamilyOfElements.restrict ⋯ x).sieveExtend x✝ h = x x✝ h
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>x : FamilyOfElements P (generate R).arrows<VAR>t : x.SieveCompatible<VAR>x✝¹ : C<VAR>x✝ : x✝¹ ⟶ X<VAR>h : (generate R).arrows x✝<GOAL>x (⋯.choose ≫ ⋯.choose) ⋯ = x x✝ h
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>x : FamilyOfElements P (generate R).arrows<VAR>t : x.SieveCompatible<VAR>x✝¹ : C<VAR>x✝ : x✝¹ ⟶ X<VAR>h : (generate R).arrows x✝<GOAL>⋯.choose ≫ ⋯.choose = x✝
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>hI : M.Basis I X<VAR>hXY : X ⊆ Y<GOAL>(M ↾ Y).Basis I X
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : TopologicalSpace M₂<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>e : M ≃L[R] M₂<VAR>h : ∃ e', ↑e' = ↑e<GOAL>(↑e).inverse = ↑e.symm
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : TopologicalSpace M₂<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>e : M ≃L[R] M₂<VAR>h : ∃ e', ↑e' = ↑e<GOAL>↑(Classical.choose h).symm = ↑e.symm
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : TopologicalSpace M₂<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>e : M ≃L[R] M₂<VAR>h : ∃ e', ↑e' = ↑e<GOAL>Classical.choose h = e
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : MeasurableSpace F<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : BorelSpace F<VAR>inst✝¹ : SecondCountableTopology F<VAR>inst✝ : SigmaCompactSpace F<VAR>b : Basis ι ℝ E<VAR>f : E ≃L[ℝ] F<GOAL>Measure.map (⇑f) b.addHaar = (b.map f.toLinearEquiv).addHaar
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : MeasurableSpace F<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : BorelSpace F<VAR>inst✝¹ : SecondCountableTopology F<VAR>inst✝ : SigmaCompactSpace F<VAR>b : Basis ι ℝ E<VAR>f : E ≃L[ℝ] F<VAR>this : (Measure.map (⇑f) b.addHaar).IsAddHaarMeasure<GOAL>Measure.map (⇑f) b.addHaar = (b.map f.toLinearEquiv).addHaar
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : MeasurableSpace F<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : BorelSpace F<VAR>inst✝¹ : SecondCountableTopology F<VAR>inst✝ : SigmaCompactSpace F<VAR>b : Basis ι ℝ E<VAR>f : E ≃L[ℝ] F<VAR>this : (Measure.map (⇑f) b.addHaar).IsAddHaarMeasure<GOAL>b.addHaar (⇑f ⁻¹' _root_.parallelepiped (⇑f.toLinearEquiv ∘ ⇑b)) = 1
<VAR>a r x : ℝ<VAR>hx : x < 0<GOAL>gammaPDF a r x = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : EquivLike F α β<VAR>inst✝ : OrderIsoClass F α β<VAR>f : F<VAR>a : α<VAR>b : β<GOAL>EquivLike.inv f b < a ↔ b < f a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : EquivLike F α β<VAR>inst✝ : OrderIsoClass F α β<VAR>f : F<VAR>a : α<VAR>b : β<GOAL>f (EquivLike.inv f b) < f a ↔ b < f a