ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>hK : NormedField K<VAR>h : IsNonarchimedean (sorryAx (K → ℝ) true)<VAR>L : Type u_2<VAR>inst✝¹ : Field L<VAR>Γ₀ : Type u_3<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>val : Valued L Γ₀<VAR>hv : v.RankOne<VAR>x : L<VAR>hx : norm x = 0<GOAL>x = 0
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι✝ : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>ι : Sort u_3<VAR>c : ι → Set α<VAR>hs : IsCompact s<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : s ⊆ ⋃ i, c i<GOAL>∃ δ > 0, ∀ x ∈ s, ∃ i, ball x δ ⊆ c i
<VAR>α : Type u_1<VAR>f g h σ τ : Perm α<VAR>hστ : σ.Disjoint τ<GOAL>σ * τ = 1 ↔ σ = 1 ∧ τ = 1
<VAR>n : ℕ<VAR>hn : 2 < n<GOAL>Even (φ n)
<VAR>n : ℕ<VAR>hn : 2 < n<VAR>this : Fact (1 < n)<GOAL>Even (φ n)
<VAR>n : ℕ<VAR>hn : 2 < n<VAR>this✝ : Fact (1 < n)<VAR>this : NeZero n<GOAL>Even (φ n)
<VAR>n : ℕ<VAR>hn : 2 < n<VAR>this✝ : Fact (1 < n)<VAR>this : NeZero n<GOAL>2 = orderOf (-1)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>G : Cᵒᵖ ⥤ Grp<VAR>X : C<VAR>I : Type w'<VAR>U : I → C<VAR>γ : OneCocycle G U<VAR>i : I<VAR>T : C<VAR>a : T ⟶ U i<GOAL>γ.ev i i a a = 1
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>Real.cosh (dist z w) = ((z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2) / (2 * z.im * w.im)
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>2 * z.im * w.im + ((z.re - w.re) * (z.re - w.re) + (z.im - w.im) * (z.im - w.im)) = (z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>((γ.rightShift a n' hn').leftShift a n hn').v p q hpq = ((a * n + a * (a - 1) / 2).negOnePow • γ.shift a).v p q hpq
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>(a * n + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (q + a) ⋯ ≫ (L.shiftFunctorObjXIso a q (q + a) ⋯).inv = (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>(a * n + a * (a - 1) / 2).negOnePow • 𝟙 (K.X (p + a)) ≫ γ.v (p + a) (q + a) ⋯ ≫ 𝟙 (L.X (q + a)) = (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(⇑f)^[n] x ≤ x + ↑n * ↑m ↔ f x ≤ x + ↑m
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>M₁₁ : Matrix m m R<VAR>M₁₂ : Matrix m n R<VAR>M₂₁ : Matrix n m R<VAR>M₂₂ M : Matrix n n R<VAR>i✝ j✝ : n<VAR>k : ℕ<VAR>i j : n<GOAL>(matPolyEquiv M.charmatrix).coeff k i j = (X - C M).coeff k i j
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>M₁₁ : Matrix m m R<VAR>M₁₂ : Matrix m n R<VAR>M₂₁ : Matrix n m R<VAR>M₂₂ M : Matrix n n R<VAR>i✝ j✝ : n<VAR>k : ℕ<VAR>i j : n<GOAL>(M.charmatrix i j).coeff k = (X.coeff k - (C M).coeff k) i j
<VAR>s : String<VAR>p : Char → Bool<GOAL>s.any p = true ↔ ∃ c, c ∈ s.data ∧ p c = true
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : Unique αˣ<VAR>s : Finset α<VAR>n : α<VAR>h : ∀ a ∈ s, Prime a<VAR>div : ∀ a ∈ s, a ∣ n<GOAL>∏ p ∈ s, p ∣ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l.dedup<GOAL>¬∀ b ∈ pwFilter (fun x x_1 => x ≠ x_1) l, a ≠ b
<VAR>R : Type u<VAR>inst✝ : AddGroupWithOne R<VAR>n : ℕ<GOAL>↑(negOfNat n) = -↑n
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>S : Type u_4<VAR>inst✝⁴ : Monoid S<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DistribMulAction S M<VAR>sR : Set R<VAR>s : Set S<VAR>N : Submodule R M<VAR>inst✝ : SMulCommClass S R M<VAR>r : S<GOAL>{r} • N = r • N
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>S : Type u_4<VAR>inst✝⁴ : Monoid S<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DistribMulAction S M<VAR>sR : Set R<VAR>s : Set S<VAR>N : Submodule R M<VAR>inst✝ : SMulCommClass S R M<VAR>r : S<GOAL>∀ ⦃r_1 : S⦄ ⦃n : M⦄, r_1 ∈ {r} → n ∈ N → r_1 • n ∈ r • N
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>S : Type u_4<VAR>inst✝⁴ : Monoid S<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DistribMulAction S M<VAR>sR : Set R<VAR>s : Set S<VAR>N : Submodule R M<VAR>inst✝ : SMulCommClass S R M<VAR>r : S<GOAL>r • N ≤ {r} • N
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<GOAL>¬s.Terminates ↔ ∀ (n : ℕ), (s.get? n).isSome = true
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>X Y : C<VAR>hX : IsTerminal X<VAR>hY : IsTerminal Y<VAR>f : X ⟶ Y<GOAL>f ≫ hX.from Y = 𝟙 X ∧ hX.from Y ≫ f = 𝟙 Y
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>X Y : C<VAR>hX : IsTerminal X<VAR>hY : IsTerminal Y<VAR>f : X ⟶ Y<GOAL>hX.from Y ≫ f = 𝟙 Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>f_cont : Continuous f<VAR>f_inj : Injective f<GOAL>IsProperMap f ↔ IsClosedMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>f_cont : Continuous f<VAR>f_inj : Injective f<VAR>h : IsClosedMap f<GOAL>IsProperMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>f_cont : Continuous f<VAR>f_inj : Injective f<VAR>h : IsClosedMap f<GOAL>Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝⁹ : DecidableEq ι<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra A B<VAR>inst✝⁵ : CommRing C<VAR>inst✝⁴ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝³ : Fintype ι'<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq ι'<VAR>inst✝ : IsDomain A<VAR>b : ι → B<VAR>hli : ¬LinearIndependent A b<GOAL>discr A b = 0
<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>n : ℤ<VAR>hn : ↑n ≠ 0<VAR>k : ℤ<VAR>this : n ≠ 0<GOAL>↑(n * k / n) = ↑(n * k) / ↑n
<VAR>x y z : ℝ<VAR>n✝ : ℕ<VAR>hx : 0 ≤ x<VAR>n : ℤ<VAR>h : y + ↑n ≠ 0<GOAL>x ^ (y + ↑n) = x ^ y * x ^ n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>p : Submodule R M<VAR>f : M →ₗ[R] M<VAR>hf : ∀ (x : M), f x ∈ p<VAR>hf' : optParam (∀ x ∈ p, f x ∈ p) ⋯<VAR>ι : Type u_2 := Module.Free.ChooseBasisIndex R M<VAR>n : ℕ<VAR>snf : Basis.SmithNormalForm p ι n<GOAL>(trace R ↥p) (f.restrict hf') = (trace R M) f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>p : Submodule R M<VAR>f : M →ₗ[R] M<VAR>hf : ∀ (x : M), f x ∈ p<VAR>hf' : optParam (∀ x ∈ p, f x ∈ p) ⋯<VAR>ι : Type u_2 := Module.Free.ChooseBasisIndex R M<VAR>n : ℕ<VAR>snf : Basis.SmithNormalForm p ι n<GOAL>((toMatrix snf.bN snf.bN) (f.restrict hf')).trace = ((toMatrix snf.bM snf.bM) f).trace
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>p : Submodule R M<VAR>f : M →ₗ[R] M<VAR>hf : ∀ (x : M), f x ∈ p<VAR>hf' : optParam (∀ x ∈ p, f x ∈ p) ⋯<VAR>ι : Type u_2 := Module.Free.ChooseBasisIndex R M<VAR>n : ℕ<VAR>snf : Basis.SmithNormalForm p ι n<VAR>A : Matrix (Fin n) (Fin n) R := (toMatrix snf.bN snf.bN) (f.restrict hf')<VAR>B : Matrix ι ι R := (toMatrix snf.bM snf.bM) f<GOAL>A.trace = B.trace
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>p : Submodule R M<VAR>f : M →ₗ[R] M<VAR>hf : ∀ (x : M), f x ∈ p<VAR>hf' : optParam (∀ x ∈ p, f x ∈ p) ⋯<VAR>ι : Type u_2 := Module.Free.ChooseBasisIndex R M<VAR>n : ℕ<VAR>snf : Basis.SmithNormalForm p ι n<VAR>A : Matrix (Fin n) (Fin n) R := (toMatrix snf.bN snf.bN) (f.restrict hf')<VAR>B : Matrix ι ι R := (toMatrix snf.bM snf.bM) f<VAR>aux : ∀ (i : ι), B i i ≠ 0 → i ∈ Set.range ⇑snf.f<GOAL>A.trace = B.trace
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>p : Submodule R M<VAR>f : M →ₗ[R] M<VAR>hf : ∀ (x : M), f x ∈ p<VAR>hf' : optParam (∀ x ∈ p, f x ∈ p) ⋯<VAR>ι : Type u_2 := Module.Free.ChooseBasisIndex R M<VAR>n : ℕ<VAR>snf : Basis.SmithNormalForm p ι n<VAR>A : Matrix (Fin n) (Fin n) R := (toMatrix snf.bN snf.bN) (f.restrict hf')<VAR>B : Matrix ι ι R := (toMatrix snf.bM snf.bM) f<VAR>aux : ∀ (i : ι), B i i ≠ 0 → i ∈ Set.range ⇑snf.f<GOAL>∑ i : Fin n, A i i = ∑ i : ι, B i i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>p : Submodule R M<VAR>f : M →ₗ[R] M<VAR>hf : ∀ (x : M), f x ∈ p<VAR>hf' : optParam (∀ x ∈ p, f x ∈ p) ⋯<VAR>ι : Type u_2 := Module.Free.ChooseBasisIndex R M<VAR>n : ℕ<VAR>snf : Basis.SmithNormalForm p ι n<VAR>A : Matrix (Fin n) (Fin n) R := (toMatrix snf.bN snf.bN) (f.restrict hf')<VAR>B : Matrix ι ι R := (toMatrix snf.bM snf.bM) f<VAR>aux : ∀ (i : ι), B i i ≠ 0 → i ∈ Set.range ⇑snf.f<GOAL>∑ i : Fin n, A i i = ∑ x ∈ Finset.filter (fun j => j ∈ Set.range ⇑snf.f) Finset.univ, B x x
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>c : F<GOAL>deriv (fun y => c + f y) x = deriv f x
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>ι : Sort u_2<VAR>S : ι → NonUnitalSubalgebra R A<VAR>x : A<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>R✝ : Type u_1<VAR>inst✝³ : CommRing R✝<VAR>n : ℕ<VAR>inst✝² : IsDomain R✝<VAR>h : 0 < n<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>ζ : R<GOAL>ζ ^ n = 1 ↔ ∃ i ∈ n.divisors, (cyclotomic i R).IsRoot ζ
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>toIcoDiv hp a (b - m • p) = toIcoDiv hp a b - m
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>G_obj : D → C<VAR>e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)<VAR>he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g<VAR>Y Y' Y'' : D<VAR>g : Y ⟶ Y'<VAR>g' : Y' ⟶ Y''<GOAL>{ obj := G_obj, map := fun {Y Y'} g => (e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map (g ≫ g') = { obj := G_obj, map := fun {Y Y'} g => (e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map g ≫ { obj := G_obj, map := fun {Y Y'} g => (e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map g'
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>G_obj : D → C<VAR>e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)<VAR>he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g<VAR>Y Y' Y'' : D<VAR>g : Y ⟶ Y'<VAR>g' : Y' ⟶ Y''<GOAL>(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' = F.map ({ obj := G_obj, map := fun {Y Y'} g => (e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map g) ≫ (e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>G_obj : D → C<VAR>e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)<VAR>he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g<VAR>Y Y' Y'' : D<VAR>g : Y ⟶ Y'<VAR>g' : Y' ⟶ Y''<GOAL>(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' = ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) ≫ g'
<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>γ : Type u_1<VAR>hf : UniformCauchySeqOnFilter F p p'<VAR>g : γ → α<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<GOAL>∀ᶠ (m : (ι × ι) × γ) in (p ×ˢ p) ×ˢ comap g p', ((fun n => F n ∘ g) m.1.1 m.2, (fun n => F n ∘ g) m.1.2 m.2) ∈ u
<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>γ : Type u_1<VAR>hf : UniformCauchySeqOnFilter F p p'<VAR>g : γ → α<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>pa : ι × ι → Prop<VAR>hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x<VAR>pb : α → Prop<VAR>hpb : ∀ᶠ (y : α) in p', pb y<VAR>hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u<GOAL>∀ᶠ (m : (ι × ι) × γ) in (p ×ˢ p) ×ˢ comap g p', ((fun n => F n ∘ g) m.1.1 m.2, (fun n => F n ∘ g) m.1.2 m.2) ∈ u
<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>γ : Type u_1<VAR>hf : UniformCauchySeqOnFilter F p p'<VAR>g : γ → α<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>pa : ι × ι → Prop<VAR>hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x<VAR>pb : α → Prop<VAR>hpb : ∀ᶠ (y : α) in p', pb y<VAR>hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u<GOAL>∃ pa, (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧ ∃ pb, (∀ᶠ (y : γ) in comap g p', pb y) ∧ ∀ {x : ι × ι}, pa x → ∀ {y : γ}, pb y → ((fun n => F n ∘ g) (x, y).1.1 (x, y).2, (fun n => F n ∘ g) (x, y).1.2 (x, y).2) ∈ u
<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>γ : Type u_1<VAR>hf : UniformCauchySeqOnFilter F p p'<VAR>g : γ → α<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>pa : ι × ι → Prop<VAR>hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x<VAR>pb : α → Prop<VAR>hpb : ∀ᶠ (y : α) in p', pb y<VAR>hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u<GOAL>∀ᶠ (y : γ) in comap g p', (pb ∘ g) y
<VAR>α : Type u_1<VAR>xs ys zs : LazyList α<GOAL>(xs.append { fn := fun x => ys }).append { fn := fun x => zs } = xs.append { fn := fun x => ys.append { fn := fun x => zs } }
<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>a : ↥S<GOAL>1 = mk (↑a) a
<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>a : ↥S<GOAL>(r S) (1, 1) (↑a, a)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>x : α<VAR>hx : r x x<VAR>n : Nat<GOAL>Pairwise r (replicate (n + 1) x)
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : MonotoneOn f (Icc ↑a ↑b)<GOAL>∫ (x : ℝ) in ↑a..↑b, f x ≤ ∑ i ∈ Finset.Ico a b, f ↑(i + 1)
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : MonotoneOn f (Icc ↑a ↑b)<GOAL>∑ x ∈ Finset.Ico a b, -f ↑(x + 1) ≤ ∫ (x : ℝ) in ↑a..↑b, -f x
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : Preadditive D<VAR>F : C ⥤ D<VAR>inst✝² : HasBinaryProducts C<VAR>inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>inst✝ : F.PreservesZeroMorphisms<GOAL>F.Additive
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : Preadditive D<VAR>F : C ⥤ D<VAR>inst✝² : HasBinaryProducts C<VAR>inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>this : HasBinaryBiproducts C<GOAL>F.Additive
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : Preadditive D<VAR>F : C ⥤ D<VAR>inst✝² : HasBinaryProducts C<VAR>inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>this✝ : HasBinaryBiproducts C<VAR>this : PreservesBinaryBiproducts F<GOAL>F.Additive
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ⊤
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R<GOAL>∀ (i i_1 : ℚ), i < i_1 → ∀ᵐ (x : Ω) ∂μ, upcrossings (↑i) (↑i_1) f x < ⊤
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a✝ b✝ : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R<VAR>a b : ℚ<VAR>hab : a < b<GOAL>∀ᵐ (x : Ω) ∂μ, upcrossings (↑a) (↑b) f x < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n✝ : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁴ : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq n✝<VAR>inst✝ : Fintype n✝<VAR>n : ℕ<VAR>p : Fin n → R[X]<VAR>h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i<VAR>h_monic : ∀ (i : Fin n), (p i).Monic<GOAL>(of fun i j => (p j).coeff ↑i).det = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n✝ : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁴ : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq n✝<VAR>inst✝ : Fintype n✝<VAR>n : ℕ<VAR>p : Fin n → R[X]<VAR>h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i<VAR>h_monic : ∀ (i : Fin n), (p i).Monic<GOAL>∏ i : Fin n, of (fun i j => (p j).coeff ↑i) i i = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n✝ : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁴ : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq n✝<VAR>inst✝ : Fintype n✝<VAR>n : ℕ<VAR>p : Fin n → R[X]<VAR>h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i<VAR>h_monic : ∀ (i : Fin n), (p i).Monic<VAR>x : Fin n<VAR>a✝ : x ∈ univ<GOAL>of (fun i j => (p j).coeff ↑i) x x = 1
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' G'' : G.Subgraph<VAR>s s' : Set V<GOAL>G'.induce s ≤ G'.induce (s ∪ s')
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a a' : α<VAR>s✝ : Finmap β<VAR>s : AList β<GOAL>(erase a (erase a' ⟦s⟧)).entries = (erase a' (erase a ⟦s⟧)).entries
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝ : DecidableEq α<VAR>hxy : x ≠ y<GOAL>(swap x y) y ≠ y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝ : DecidableEq α<VAR>hxy : x ≠ y<VAR>a : α<VAR>ha : (if a = x then y else if a = y then x else a) ≠ a<VAR>hya : ¬y = a<GOAL>(swap x y ^ 1) y = a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝ : DecidableEq α<VAR>hxy : x ≠ y<VAR>a : α<VAR>ha : (if a = x then y else if a = y then x else a) ≠ a<VAR>hya : ¬y = a<GOAL>(if y = x then y else if y = y then x else y) = a
<VAR>o o' : ONote<VAR>m : ℕ<VAR>inst✝ : o.NF<VAR>h : o.split = (o', m)<VAR>a : ONote<VAR>n : ℕ<VAR>e : o.split' = (a, n)<GOAL>o'.NF ∧ o.repr = o'.repr + ↑m
<VAR>o o' : ONote<VAR>m : ℕ<VAR>inst✝ : o.NF<VAR>h : o.split = (o', m)<VAR>a : ONote<VAR>n : ℕ<VAR>e : o.split' = (a, n)<VAR>s₁ : a.NF<VAR>s₂ : o.repr = ω * a.repr + ↑n<GOAL>o'.NF ∧ o.repr = o'.repr + ↑m
<VAR>o o' : ONote<VAR>m : ℕ<VAR>inst✝ : o.NF<VAR>a : ONote<VAR>n : ℕ<VAR>h : (scale 1 a, n) = (o', m)<VAR>e : o.split' = (a, n)<VAR>s₁ : a.NF<VAR>s₂ : o.repr = ω * a.repr + ↑n<GOAL>o'.NF ∧ o.repr = o'.repr + ↑m
<VAR>o : ONote<VAR>m : ℕ<VAR>inst✝ : o.NF<VAR>a : ONote<VAR>s₁ : a.NF<VAR>e : o.split' = (a, m)<VAR>s₂ : o.repr = ω * a.repr + ↑m<GOAL>(scale 1 a).NF ∧ o.repr = (scale 1 a).repr + ↑m
<VAR>o : ONote<VAR>m : ℕ<VAR>inst✝ : o.NF<VAR>a : ONote<VAR>s₁ : a.NF<VAR>e : o.split' = (a, m)<VAR>s₂ : o.repr = ω * a.repr + ↑m<GOAL>(scale 1 a).NF
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : NonUnitalSeminormedRing α<VAR>β : Type u_5<VAR>inst✝¹ : NormedRing β<VAR>inst✝ : Nontrivial β<GOAL>‖1‖ ≤ ‖1‖ * ‖1‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hf : AEStronglyMeasurable f μ<GOAL>eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal) = eLpNorm f q μ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ ↑n
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<GOAL>(uIcc s t).card = ∏ i ∈ s.toFinset ∪ t.toFinset, ((↑(count i t) - ↑(count i s)).natAbs + 1)
<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 α<GOAL>x ∈ sphere y ε ↔ y ∈ sphere x ε
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s✝ s : Set (α → M)<VAR>φ : L[[↑A]].Formula α<VAR>hφ : s = setOf φ.Realize<VAR>v : α → M<GOAL>v ∈ sᶜ ↔ v ∈ setOf φ.not.Realize