ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>inst✝ : Finite ι<VAR>I : Box ι<VAR>π : Prepartition I<VAR>h : π.IsPartition<GOAL>∃ s, splitMany I s ≤ π
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>inst✝ : Finite ι<VAR>I : Box ι<VAR>π : Prepartition I<VAR>h : π.IsPartition<VAR>s : Finset (ι × ℝ)<VAR>hs : π ⊓ splitMany I s = (splitMany I s).filter fun J => ↑J ⊆ π.iUnion<GOAL>splitMany I s ≤ π
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>inst✝ : Finite ι<VAR>I : Box ι<VAR>π : Prepartition I<VAR>h : π.IsPartition<VAR>s : Finset (ι × ℝ)<VAR>hs : π ⊓ splitMany I s = (splitMany I s).filter fun J => ↑J ⊆ ↑I<GOAL>∀ J ∈ splitMany I s, ↑J ⊆ ↑I
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>g : α<VAR>s : Set ℤ := {n | n • a ≤ g}<GOAL>∃! k, k • a ≤ g ∧ g < (k + 1) • a
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>g : α<VAR>s : Set ℤ := {n | n • a ≤ g}<VAR>k : ℕ<VAR>hk : -g ≤ k • a<GOAL>∃! k, k • a ≤ g ∧ g < (k + 1) • a
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>g : α<VAR>s : Set ℤ := {n | n • a ≤ g}<VAR>k : ℕ<VAR>hk : -g ≤ k • a<VAR>h_ne : s.Nonempty<GOAL>∃! k, k • a ≤ g ∧ g < (k + 1) • a
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>g : α<VAR>s : Set ℤ := {n | n • a ≤ g}<VAR>k✝ : ℕ<VAR>hk✝ : -g ≤ k✝ • a<VAR>h_ne : s.Nonempty<VAR>k : ℕ<VAR>hk : g ≤ k • a<GOAL>∃! k, k • a ≤ g ∧ g < (k + 1) • a
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>g : α<VAR>s : Set ℤ := {n | n • a ≤ g}<VAR>k✝ : ℕ<VAR>hk✝ : -g ≤ k✝ • a<VAR>h_ne : s.Nonempty<VAR>k : ℕ<VAR>hk : g ≤ k • a<VAR>h_bdd : ∀ n ∈ s, n ≤ ↑k<GOAL>∃! k, k • a ≤ g ∧ g < (k + 1) • a
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>g : α<VAR>s : Set ℤ := {n | n • a ≤ g}<VAR>k✝ : ℕ<VAR>hk✝ : -g ≤ k✝ • a<VAR>h_ne : s.Nonempty<VAR>k : ℕ<VAR>hk : g ≤ k • a<VAR>h_bdd : ∀ n ∈ s, n ≤ ↑k<VAR>m : ℤ<VAR>hm : m ∈ s<VAR>hm' : ∀ z ∈ s, z ≤ m<GOAL>∃! k, k • a ≤ g ∧ g < (k + 1) • a
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>g : α<VAR>s : Set ℤ := {n | n • a ≤ g}<VAR>k✝ : ℕ<VAR>hk✝ : -g ≤ k✝ • a<VAR>h_ne : s.Nonempty<VAR>k : ℕ<VAR>hk : g ≤ k • a<VAR>h_bdd : ∀ n ∈ s, n ≤ ↑k<VAR>m : ℤ<VAR>hm : m ∈ s<VAR>hm' : ∀ z ∈ s, z ≤ m<VAR>hm'' : g < (m + 1) • a<GOAL>∃! k, k • a ≤ g ∧ g < (k + 1) • a
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>g : α<VAR>s : Set ℤ := {n | n • a ≤ g}<VAR>k✝ : ℕ<VAR>hk✝ : -g ≤ k✝ • a<VAR>h_ne : s.Nonempty<VAR>k : ℕ<VAR>hk : g ≤ k • a<VAR>h_bdd : ∀ n ∈ s, n ≤ ↑k<VAR>m : ℤ<VAR>hm : m ∈ s<VAR>hm' : ∀ z ∈ s, z ≤ m<VAR>hm'' : g < (m + 1) • a<VAR>n : ℤ<VAR>hn : (fun k => k • a ≤ g ∧ g < (k + 1) • a) n<GOAL>m < n + 1
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>g : α<VAR>s : Set ℤ := {n | n • a ≤ g}<VAR>k✝ : ℕ<VAR>hk✝ : -g ≤ k✝ • a<VAR>h_ne : s.Nonempty<VAR>k : ℕ<VAR>hk : g ≤ k • a<VAR>h_bdd : ∀ n ∈ s, n ≤ ↑k<VAR>m : ℤ<VAR>hm : m ∈ s<VAR>hm' : ∀ z ∈ s, z ≤ m<VAR>hm'' : g < (m + 1) • a<VAR>n : ℤ<VAR>hn : (fun k => k • a ≤ g ∧ g < (k + 1) • a) n<GOAL>m • a < (n + 1) • a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>U : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace ↥U<VAR>b : OrthonormalBasis ι 𝕜 ↥U<VAR>x : E<GOAL>(orthogonalProjection U) x = ∑ i : ι, ⟪↑(b i), x⟫_𝕜 • b i
<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>h : TendstoUniformlyOnFilter F f p p'<VAR>hx : 𝓟 {x} ≤ p'<GOAL>Tendsto (fun n => F n x) p (𝓝 (f x))
<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>h : TendstoUniformlyOnFilter F f p p'<VAR>hx : 𝓟 {x} ≤ p'<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<GOAL>(fun x_1 => (f x, F x_1 x)) ⁻¹' u ∈ p
<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>h : TendstoUniformlyOnFilter F f p p'<VAR>hx : 𝓟 {x} ≤ p'<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<GOAL>∀ (a : ι), (∀ᶠ (y : α) in p', (f y, F a y) ∈ u) → a ∈ (fun x_1 => (f x, F x_1 x)) ⁻¹' 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>h✝ : TendstoUniformlyOnFilter F f p p'<VAR>hx : 𝓟 {x} ≤ p'<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>i : ι<VAR>h : ∀ᶠ (y : α) in p', (f y, F i y) ∈ u<GOAL>i ∈ (fun x_1 => (f x, F x_1 x)) ⁻¹' u
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(mulDysonETransform e x).1 * (mulDysonETransform e x).2 ⊆ x.1 * x.2
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>e • x.2 * e⁻¹ • x.1 ⊆ x.1 * x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝³ : CommRing α<VAR>inst✝² : StarRing α<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>A : Matrix m m α<VAR>hA : A.IsHermitian<GOAL>A.adjugate.IsHermitian
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>inst✝ : Denumerable ι<VAR>κs : ι → Kernel α β<VAR>hκs : ∀ (n : ι), IsSFiniteKernel (κs n)<VAR>e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm<GOAL>Kernel.sum κs = Kernel.sum fun n => (κs (e n).1).seq (e n).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>inst✝ : Denumerable ι<VAR>κs : ι → Kernel α β<VAR>hκs : ∀ (n : ι), IsSFiniteKernel (κs n)<VAR>e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm<VAR>hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (κs n).seq<GOAL>Kernel.sum κs = Kernel.sum fun n => (κs (e n).1).seq (e n).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>inst✝ : Denumerable ι<VAR>κs : ι → Kernel α β<VAR>hκs : ∀ (n : ι), IsSFiniteKernel (κs n)<VAR>e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm<VAR>hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (κs n).seq<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((Kernel.sum fun n => Kernel.sum (κs n).seq) a) s = ((Kernel.sum fun n => (κs (e n).1).seq (e n).2) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>inst✝ : Denumerable ι<VAR>κs : ι → Kernel α β<VAR>hκs : ∀ (n : ι), IsSFiniteKernel (κs n)<VAR>e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm<VAR>hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (κs n).seq<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∑' (n : ι) (n_1 : ℕ), (((κs n).seq n_1) a) s = ∑' (n : ℕ), (((κs (e n).1).seq (e n).2) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>inst✝ : Denumerable ι<VAR>κs : ι → Kernel α β<VAR>hκs : ∀ (n : ι), IsSFiniteKernel (κs n)<VAR>e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm<VAR>hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (κs n).seq<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∑' (i : ι) (m : ℕ), (((κs i).seq m) a) s = ∑' (n : ℕ), (fun im => (((κs im.1).seq im.2) a) s) (e n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<VAR>x : α<VAR>u : αˣ<GOAL>x * ↑u * ↑u⁻¹ = x
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>f : M →ₗ[R] M<VAR>g : N →ₗ[R] N<GOAL>(trace R (M × N)) (f.prodMap g) = (trace R M) f + (trace R N) g
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>f : M →ₗ[R] M<VAR>g : N →ₗ[R] N<VAR>h : (trace R (M × N) ∘ₗ prodMapLinear R M N M N R) (f, g) = (id.coprod id ∘ₗ (trace R M).prodMap (trace R N)) (f, g)<GOAL>(trace R (M × N)) (f.prodMap g) = (trace R M) f + (trace R N) g
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>f : M →ₗ[R] M<VAR>g : N →ₗ[R] N<VAR>h : (trace R (M × N)) (f.prodMap g) = { toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ } ((trace R M) f) + { toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ } ((trace R N) g)<GOAL>(trace R (M × N)) (f.prodMap g) = (trace R M) f + (trace R N) g
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>β : Type w<VAR>f : β → C<VAR>inst✝ : HasProduct f<GOAL>IsCoseparator (∏ᶜ f) ↔ IsCoseparating (Set.range f)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>β : Type w<VAR>f : β → C<VAR>inst✝ : HasProduct f<VAR>h : IsCoseparator (∏ᶜ f)<VAR>X Y : C<VAR>u v : X ⟶ Y<VAR>huv : ∀ G ∈ Set.range f, ∀ (h : Y ⟶ G), u ≫ h = v ≫ h<GOAL>u = v
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>β : Type w<VAR>f : β → C<VAR>inst✝ : HasProduct f<VAR>h : IsCoseparating (Set.range f)<VAR>X Y : C<VAR>u v : X ⟶ Y<VAR>huv : ∀ (h : Y ⟶ ∏ᶜ f), u ≫ h = v ≫ h<VAR>Z : C<VAR>hZ : Z ∈ Set.range f<VAR>g : Y ⟶ Z<GOAL>u ≫ g = v ≫ g
<VAR>α' : Type u_1<VAR>β' : Type u_2<VAR>e✝ : Perm α'<VAR>p : β' → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α' ≃ Subtype p<VAR>e e' : Perm α'<GOAL>Equiv.trans (e.extendDomain f) (e'.extendDomain f) = extendDomain (Equiv.trans e e') f
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>v : ι → M<VAR>hv : Submodule.span R (Set.range v) = ⊤<VAR>inst✝ : Fintype ι<VAR>f : ι →₀ ↥I<GOAL>(finsuppTotal ι M I v) f = ∑ i : ι, ↑(f i) • v i
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>v : ι → M<VAR>hv : Submodule.span R (Set.range v) = ⊤<VAR>inst✝ : Fintype ι<VAR>f : ι →₀ ↥I<GOAL>∀ (i : ι), ↑0 • v i = 0
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>n : ℕ<VAR>h : Module.rank R M < ↑n<GOAL>finrank R M < n
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>n : ℕ<VAR>h : Module.rank R M < ↑n<GOAL>Module.rank R M < ℵ₀
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>n : ℕ<VAR>h : Module.rank R M < ↑n<GOAL>↑n < ℵ₀
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasPullbacks C<VAR>P : MorphismProperty C<VAR>inst✝¹ : P.IsStableUnderComposition<VAR>inst✝ : P.RespectsIso<VAR>hP'' : P.StableUnderBaseChange<VAR>X✝ Y✝ Z✝ : C<VAR>x✝¹ : X✝ ⟶ Y✝<VAR>x✝ : Y✝ ⟶ Z✝<VAR>h₁ : P.diagonal x✝¹<VAR>h₂ : P.diagonal x✝<GOAL>P.diagonal (x✝¹ ≫ x✝)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasPullbacks C<VAR>P : MorphismProperty C<VAR>inst✝¹ : P.IsStableUnderComposition<VAR>inst✝ : P.RespectsIso<VAR>hP'' : P.StableUnderBaseChange<VAR>X✝ Y✝ Z✝ : C<VAR>x✝¹ : X✝ ⟶ Y✝<VAR>x✝ : Y✝ ⟶ Z✝<VAR>h₁ : P.diagonal x✝¹<VAR>h₂ : P.diagonal x✝<GOAL>P (pullback.diagonal x✝¹ ≫ (pullbackDiagonalMapIdIso x✝¹ x✝¹ x✝).inv ≫ pullback.snd (pullback.diagonal x✝) (pullback.map (x✝¹ ≫ x✝) (x✝¹ ≫ x✝) x✝ x✝ x✝¹ x✝¹ (𝟙 Z✝) ⋯ ⋯))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t✝ : Set α<VAR>a : α<VAR>hs : s.Finite<VAR>ht : t✝.Finite<VAR>t : Finset α<GOAL>hs.toFinset ⊆ t ↔ s ⊆ ↑t
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : CharZero R<VAR>n : ℕ<VAR>a b : R<VAR>h : ↑n * a = ↑n * b<GOAL>n = 0 ∨ a = b
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : CharZero R<VAR>n : ℕ<VAR>a b : R<VAR>h : ↑n = 0 ∨ a = b<GOAL>n = 0 ∨ a = b
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝¹ : Category.{?u.12278, u_1} D<VAR>P : MorphismProperty C<VAR>hP : P.RespectsIso<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : IsIso g<VAR>h : P (f ≫ g)<GOAL>P f
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>a b : G<VAR>h : Commute a b<GOAL>a⁻¹ * b * a = b
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h : F.Stable<GOAL>F.Stable ↔ ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h✝ : F.Stable<VAR>h : ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀<VAR>n : ℕ<VAR>hn : n ≥ h.choose<GOAL>I • F.N n = F.N (n + 1)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C : VariableChange R<GOAL>W.variableChange VariableChange.id = W
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C : VariableChange R<GOAL>{ a₁ := 1 * (W.a₁ + 2 * { u := 1, r := 0, s := 0, t := 0 }.s), a₂ := 1 ^ 2 * (W.a₂ - { u := 1, r := 0, s := 0, t := 0 }.s * W.a₁ + 3 * { u := 1, r := 0, s := 0, t := 0 }.r - { u := 1, r := 0, s := 0, t := 0 }.s ^ 2), a₃ := 1 ^ 3 * (W.a₃ + { u := 1, r := 0, s := 0, t := 0 }.r * W.a₁ + 2 * { u := 1, r := 0, s := 0, t := 0 }.t), a₄ := 1 ^ 4 * (W.a₄ - { u := 1, r := 0, s := 0, t := 0 }.s * W.a₃ + 2 * { u := 1, r := 0, s := 0, t := 0 }.r * W.a₂ - ({ u := 1, r := 0, s := 0, t := 0 }.t + { u := 1, r := 0, s := 0, t := 0 }.r * { u := 1, r := 0, s := 0, t := 0 }.s) * W.a₁ + 3 * { u := 1, r := 0, s := 0, t := 0 }.r ^ 2 - 2 * { u := 1, r := 0, s := 0, t := 0 }.s * { u := 1, r := 0, s := 0, t := 0 }.t), a₆ := 1 ^ 6 * (W.a₆ + { u := 1, r := 0, s := 0, t := 0 }.r * W.a₄ + { u := 1, r := 0, s := 0, t := 0 }.r ^ 2 * W.a₂ + { u := 1, r := 0, s := 0, t := 0 }.r ^ 3 - { u := 1, r := 0, s := 0, t := 0 }.t * W.a₃ - { u := 1, r := 0, s := 0, t := 0 }.t ^ 2 - { u := 1, r := 0, s := 0, t := 0 }.r * { u := 1, r := 0, s := 0, t := 0 }.t * W.a₁) } = W
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>dual A K I ≤ dual A K J ↔ J ≤ I
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>dual A K I ≤ dual A K J ↔ J ≤ dual A K (dual A K I)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>x : E<VAR>a✝ : Nontrivial E<GOAL>fderivWithin 𝕜 f univ x = fderiv 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>x : E<VAR>a✝ : Nontrivial E<VAR>H : 𝓝[univ \ {x}] x ≠ ⊥<GOAL>fderivWithin 𝕜 f univ x = fderiv 𝕜 f x
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<VAR>hs' : a ≠ 0 ∨ s ≠ 1<GOAL>hurwitzZetaEven a (1 - s) = 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.cos (↑π * s / 2) * cosZeta a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<VAR>hs' : a ≠ 0 ∨ s ≠ 1<VAR>this : hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (1 - s).Gammaℝ⁻¹<GOAL>hurwitzZetaEven a (1 - s) = 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.cos (↑π * s / 2) * cosZeta a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<VAR>hs' : a ≠ 0 ∨ s ≠ 1<VAR>this : hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (1 - s).Gammaℝ⁻¹<GOAL>completedCosZeta a s * (s.Gammaℂ * Complex.cos (↑π * s / 2) * s.Gammaℝ⁻¹) = s.Gammaℂ * Complex.cos (↑π * s / 2) * (completedCosZeta a s / s.Gammaℝ)
<VAR>X : Type u_1<VAR>inst✝² : NormedAddCommGroup X<VAR>M : Type u_2<VAR>inst✝¹ : Ring M<VAR>inst✝ : Module M X<VAR>P : { P // IsLprojection X P }<GOAL>↑P * ↑Pᶜ = 0
<VAR>n n✝ : ℕ<VAR>hi : n✝ + 1 < n + 1<VAR>h0 : ⟨n✝ + 1, hi⟩ ≠ 0<GOAL>⟨n✝ + 1, hi⟩.cycleRange.cycleType = {↑⟨n✝ + 1, hi⟩ + 1}
<VAR>n n✝ : ℕ<VAR>hi : n✝ + 1 < n + 1<VAR>h0 : ⟨n✝ + 1, hi⟩ ≠ 0<GOAL>(finRotate (↑⟨n✝ + 1, hi⟩ + 1)).cycleType = {↑⟨n✝ + 1, hi⟩ + 1}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>h : dist p1 p2 = dist p1 p3<GOAL>∠ p1 p2 p3 = ∠ p1 p3 p2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>h : ‖p1 -ᵥ p2‖ = ‖p1 -ᵥ p3‖<GOAL>∠ p1 p2 p3 = ∠ p1 p3 p2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>h : ‖p1 -ᵥ p2‖ = ‖p1 -ᵥ p3‖<GOAL>InnerProductGeometry.angle (p1 -ᵥ p2) (p3 -ᵥ p2) = InnerProductGeometry.angle (p1 -ᵥ p3) (p2 -ᵥ p3)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>h : ‖p1 -ᵥ p2‖ = ‖p1 -ᵥ p3‖<GOAL>p3 -ᵥ p2 = p1 -ᵥ p2 - (p1 -ᵥ p3)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>h : ‖p1 -ᵥ p2‖ = ‖p1 -ᵥ p3‖<GOAL>p2 -ᵥ p3 = p1 -ᵥ p3 - (p1 -ᵥ p2)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>Icc a b = {c} ↔ a = c ∧ b = c
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedRing A<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hf : IntervalIntegrable f volume a b<VAR>c : ℝ<GOAL>IntervalIntegrable (fun x => f (c + x)) volume (a - c) (b - c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>s t : Set α<GOAL>DirSupClosed s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) d → d ⊆ s → sSup d ∈ s
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s t : Set E<VAR>x : E<VAR>hx : x ≠ 0<GOAL>IsConnected {y | SameRay ℝ x y ∧ y ≠ 0}
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s t : Set E<VAR>x : E<VAR>hx : x ≠ 0<GOAL>IsConnected {y | ∃ r, 0 < r ∧ r • x = y}
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>d : ℕ<GOAL>∀ {p : S[X]}, p ∈ lifts f → p.natDegree = d → ∃ q, map f q = p ∧ q.degree = p.degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ {p : S[X]}, p ∈ lifts f → p.natDegree = m → ∃ q, map f q = p ∧ q.degree = p.degree<GOAL>∀ {p : S[X]}, p ∈ lifts f → p.natDegree = n → ∃ q, map f q = p ∧ q.degree = p.degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ {p : S[X]}, p ∈ lifts f → p.natDegree = m → ∃ q, map f q = p ∧ q.degree = p.degree<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hdeg : p.natDegree = n<VAR>erase_zero : ¬p.eraseLead = 0<GOAL>∃ q, map f q = p ∧ q.degree = p.degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ {p : S[X]}, p ∈ lifts f → p.natDegree = m → ∃ q, map f q = p ∧ q.degree = p.degree<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hdeg : p.natDegree = n<VAR>erase_zero : ¬p.eraseLead = 0<VAR>deg_erase : p.eraseLead.natDegree < p.natDegree<GOAL>∃ q, map f q = p ∧ q.degree = p.degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ {p : S[X]}, p ∈ lifts f → p.natDegree = m → ∃ q, map f q = p ∧ q.degree = p.degree<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hdeg : p.natDegree = n<VAR>erase_zero : ¬p.eraseLead = 0<VAR>deg_erase : p.eraseLead.natDegree < p.natDegree<VAR>pzero : p ≠ 0<GOAL>∃ q, map f q = p ∧ q.degree = p.degree