ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>e : PartialHomeomorph M H<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : E<VAR>y : H<GOAL>ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ ↑I.symm ∘ ↑(extChartAt 𝓘(𝕜, E) x).symm) ((extChartAt 𝓘(𝕜, E) x).target ∩ ↑(extChartAt 𝓘(𝕜, E) x).symm ⁻¹' (range ↑I ∩ ↑I.symm ⁻¹' (extChartAt I y).source))
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>e : PartialHomeomorph M H<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : E<VAR>y : H<GOAL>ContDiffOn 𝕜 n (↑I ∘ ↑I.symm) (range ↑I)
<VAR>x y : ℂ<GOAL>sinh (2 * x) = 2 * sinh x * cosh x
<VAR>x y : ℂ<GOAL>sinh x * cosh x + cosh x * sinh x = 2 * sinh x * cosh x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹ : UniformSpace 𝕜<VAR>β : Type u_4<VAR>inst✝ : UniformSpace β<VAR>f : β → Matrix m n 𝕜<GOAL>UniformContinuous f ↔ ∀ (i : m) (j : n), UniformContinuous fun x => f x i j
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹ : UniformSpace 𝕜<VAR>β : Type u_4<VAR>inst✝ : UniformSpace β<VAR>f : β → Matrix m n 𝕜<GOAL>(∀ (i : m) (i_1 : n), Filter.Tendsto ((fun a => (a.1 i i_1, a.2 i i_1)) ∘ fun x => (f x.1, f x.2)) (𝓤 β) (𝓤 𝕜)) ↔ ∀ (i : m) (j : n), Filter.Tendsto (fun x => (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I✝ I J : Ideal R<VAR>h : I ≤ J<VAR>x : R<VAR>hx : x ∈ I.jacobson<GOAL>x ∈ J.jacobson
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I✝ I J : Ideal R<VAR>h : I ≤ J<VAR>x : R<VAR>hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1<GOAL>∀ ⦃I : Ideal R⦄, I ∈ {J_1 | J ≤ J_1 ∧ J_1.IsMaximal} → x ∈ I
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>ι : Type u_3<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f : ι → Set X<GOAL>closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<GOAL>u ~[l] 0 ↔ u =O[l] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<VAR>h : u =O[l] 0<GOAL>u ~[l] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<VAR>h : u =O[l] 0<GOAL>∃ s ∈ l, Set.EqOn u 0 s
<VAR>α : Type u_1<VAR>f g h : Perm α<VAR>l : List (Perm α)<VAR>h1 : 1 ∉ l<VAR>h2 : List.Pairwise Disjoint l<GOAL>l.Nodup
<VAR>α : Type u_1<VAR>f g h : Perm α<VAR>l : List (Perm α)<VAR>h1 : 1 ∉ l<VAR>h2 : List.Pairwise Disjoint l<GOAL>∀ {a b : Perm α}, a ∈ l → b ∈ l → a.Disjoint b → a ≠ b
<VAR>α : Type u_1<VAR>f g h : Perm α<VAR>l : List (Perm α)<VAR>h1 : 1 ∉ l<VAR>h2 : List.Pairwise Disjoint l<VAR>σ : Perm α<VAR>a✝ h_mem : σ ∈ l<VAR>h_disjoint : σ.Disjoint σ<GOAL>σ = 1
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m✝ : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>m : α → γ → δ<VAR>n : β → γ<GOAL>map₂ m f (map n g) = map₂ (fun a b => m a (n b)) f g
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>Γ₀ : Type u_2<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>inst✝ : v.RankOne<VAR>x : Γ₀<VAR>h : x = 0<GOAL>(hom v) x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f g : β → α<VAR>a✝ b✝ : α<VAR>s : Finset β<VAR>b : β<VAR>inst✝ : DecidablePred fun x => x = b<VAR>a : α<GOAL>HasProd (fun b' => if b' = b then a else 1) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f g : β → α<VAR>a✝ b✝ : α<VAR>s : Finset β<VAR>b : β<VAR>inst✝ : DecidablePred fun x => x = b<VAR>a : α<GOAL>a = if b = b then a else 1
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<GOAL>LiouvilleWith p (x - ↑n) ↔ LiouvilleWith p x
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>P : Type u₁<VAR>inst✝¹ : CommRing P<VAR>g : (i : ι) → G i →+* P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>F : DirectLimit G f →+* P<VAR>x✝ : DirectLimit G f<VAR>i j : ι<VAR>hij : i ≤ j<VAR>x : G i<GOAL>((fun i => F.comp (of G f i)) j) (f i j hij x) = ((fun i => F.comp (of G f i)) i) x
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>P : Type u₁<VAR>inst✝¹ : CommRing P<VAR>g : (i : ι) → G i →+* P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>F : DirectLimit G f →+* P<VAR>x : DirectLimit G f<GOAL>F x = (lift G f P (fun i => F.comp (of G f i)) ⋯) x
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>P : Type u₁<VAR>inst✝¹ : CommRing P<VAR>g : (i : ι) → G i →+* P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>F : DirectLimit G f →+* P<VAR>x : DirectLimit G f<VAR>h✝ : IsEmpty ι<GOAL>F x = (lift G f P (fun i => F.comp (of G f i)) ⋯) x
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>P : Type u₁<VAR>inst✝¹ : CommRing P<VAR>g : (i : ι) → G i →+* P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>F : DirectLimit G f →+* P<VAR>x : DirectLimit G f<VAR>h✝ : Nonempty ι<GOAL>F x = (lift G f P (fun i => F.comp (of G f i)) ⋯) x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>α : L → R<VAR>β : Weight R L M<VAR>hα : α ≠ 0<VAR>n : ℕ<VAR>hn : n ≤ chainBotCoeff α β<GOAL>weightSpace M (-↑n • α + ⇑β) ≠ ⊥
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h₁ : 0 < a<VAR>h₂ : a < 1<GOAL>1 < a⁻¹
<VAR>x✝ y✝ x y : ℝ<VAR>hy : y ∈ Ioo (-(π / 2)) (π / 2)<GOAL>arcsin x = y ↔ x = sin y
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<GOAL>IsIso (pullback.snd f g)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<GOAL>IsIso (forgetToSheafedSpace.map (pullback.snd f g))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<GOAL>IsIso (SheafedSpace.forgetToPresheafedSpace.map (forgetToSheafedSpace.map (pullback.snd f g)))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<GOAL>IsIso ((PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) f g).hom ≫ pullback.snd ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map f) ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map g))
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some ⁻¹' Ioc ⊥ ↑a = Iic a
<VAR>ι : Sort u_1<VAR>f✝ f : ι → ℝ≥0<VAR>a : ℝ≥0<GOAL>a * iInf f = ⨅ i, a * f i
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>x : ↥f.domain<GOAL>(↑f x, ↑x) ∈ f.inverse.graph
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>x : ↥f.domain<GOAL>∃ a b, (∃ (h : a ∈ f.domain), ↑f ⟨a, ⋯⟩ = b) ∧ b = ↑f x ∧ a = ↑x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X✝ Y✝ : Set α<VAR>e : α<VAR>M : Matroid α<VAR>X Y : Set α<GOAL>M.closure (M.closure X ∪ M.closure Y) = M.closure (X ∪ Y)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X✝ Y✝ : Set α<VAR>e : α<VAR>M : Matroid α<VAR>X Y : Set α<GOAL>M.closure (⋃ i, M.closure (bif i then X else Y)) = M.closure (⋃ b, bif b then M.closure X else M.closure Y)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f g : ι → N<VAR>s t : Finset ι<VAR>h : ∀ i ∈ s, f i ≤ 1<GOAL>∏ i ∈ s, 1 = 1
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<VAR>motive : (m : ℕ) → n ≤ m → Sort u_1<VAR>refl : motive n ⋯<VAR>le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯<GOAL>leRec refl le_succ_of_le ⋯ = le_succ_of_le ⋯ refl
<VAR>S : Set ℝ<VAR>h₁ : S.Nonempty<VAR>h₂ : BddBelow S<GOAL>IsGLB S (sInf S)
<VAR>S : Set ℝ<VAR>h₁ : S.Nonempty<VAR>h₂ : BddBelow S<GOAL>IsLUB (-S) (sSup (-S))
<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 c : M<VAR>b d : ↥S<GOAL>mk a b = mk c d ↔ (r S) (a, b) (c, d)
<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 c : M<VAR>b d : ↥S<GOAL>(∃ u v, u • c = v • a ∧ ↑u * ↑d = v * ↑b) ↔ Setoid.r (a, b) (c, d)
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>inst✝¹ : FiniteDimensional K V<VAR>f : End K V<VAR>inst✝ : PerfectField K<GOAL>∃ n ∈ adjoin K {f}, ∃ s ∈ adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>inst✝¹ : FiniteDimensional K V<VAR>f : End K V<VAR>inst✝ : PerfectField K<VAR>g : K[X]<VAR>k : ℕ<VAR>sep : Squarefree g<VAR>nil : minpoly K f ∣ g ^ k<GOAL>∃ n ∈ adjoin K {f}, ∃ s ∈ adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>inst✝¹ : FiniteDimensional K V<VAR>f : End K V<VAR>inst✝ : PerfectField K<VAR>g : K[X]<VAR>k : ℕ<VAR>sep : g.Separable<VAR>nil : minpoly K f ∣ g ^ k<GOAL>∃ n ∈ adjoin K {f}, ∃ s ∈ adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>A B : Set (Finset α)<VAR>s : Finset α<VAR>r : ℕ<VAR>f : ι → Set (Finset α)<GOAL>Sized r (⋃ i, f i) ↔ ∀ (i : ι), Sized r (f i)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>A B : Set (Finset α)<VAR>s : Finset α<VAR>r : ℕ<VAR>f : ι → Set (Finset α)<GOAL>(∀ ⦃x : Finset α⦄ (x_1 : ι), x ∈ f x_1 → x.card = r) ↔ ∀ (i : ι) ⦃x : Finset α⦄, x ∈ f i → x.card = r
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>T : Type u_1<VAR>inst✝⁴ : NonUnitalNonAssocRing R<VAR>inst✝³ : NonUnitalNonAssocRing S<VAR>inst✝² : NonUnitalNonAssocRing T<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : NonUnitalRingHomClass F R S<VAR>g : S →ₙ+* T<VAR>f : R →ₙ+* S<VAR>s : NonUnitalSubring S<VAR>x : R × S<GOAL>x ∈ ⊤.prod s ↔ x ∈ comap (NonUnitalRingHom.snd R S) s
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<GOAL>(eval P) W'.polynomialZ = W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 - (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<GOAL>(eval P) (C W'.a₁ * X x * X y + C (3 * W'.a₃) * X y * X z ^ 2 - (C (2 * W'.a₂) * X x ^ 2 * X z + C (4 * W'.a₄) * X x * X z ^ 3 + C (6 * W'.a₆) * X z ^ 5)) = W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 - (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5)
<VAR>n : ℕ<GOAL>antidiagonal (n + 1) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<GOAL>cobounded ℝ = atBot ⊔ atTop
<VAR>k : Type u<VAR>inst✝⁷ : Field k<VAR>G : Type u<VAR>inst✝⁶ : Fintype G<VAR>inst✝⁵ : Invertible ↑(Fintype.card G)<VAR>inst✝⁴ : Group G<VAR>V : Type u<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module (MonoidAlgebra k G) V<VAR>W : Type u<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module (MonoidAlgebra k G) W<VAR>p : Submodule (MonoidAlgebra k G) V<GOAL>∃ q, IsCompl p q
<VAR>k : Type u<VAR>inst✝⁷ : Field k<VAR>G : Type u<VAR>inst✝⁶ : Fintype G<VAR>inst✝⁵ : Invertible ↑(Fintype.card G)<VAR>inst✝⁴ : Group G<VAR>V : Type u<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module (MonoidAlgebra k G) V<VAR>W : Type u<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module (MonoidAlgebra k G) W<VAR>p : Submodule (MonoidAlgebra k G) V<VAR>f : V →ₗ[MonoidAlgebra k G] ↥p<VAR>hf : f ∘ₗ p.subtype = LinearMap.id<GOAL>∃ q, IsCompl p q
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>hs : (𝓓 a 𝒜).Shatters s<VAR>u : Finset α<VAR>hu : u ∈ 𝓓 a 𝒜<VAR>ht : s ∩ u ⊆ s<GOAL>∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>hs : (𝓓 a 𝒜).Shatters s<VAR>u : Finset α<VAR>hu : u ∈ 𝒜 ∧ u.erase a ∈ 𝒜 ∨ u ∉ 𝒜 ∧ insert a u ∈ 𝒜<VAR>ht : s ∩ u ⊆ s<GOAL>∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : Category.{u_5, u_1} C<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>F G : C ⥤ D<VAR>e : F ≅ G<VAR>A : Type u_4<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift C A<VAR>inst✝¹ : HasShift D A<VAR>inst✝ : F.CommShift A<VAR>this : G.CommShift A := ofIso e A<VAR>a : A<GOAL>(iso a).hom ≫ whiskerRight e.hom (shiftFunctor D a) = whiskerLeft (shiftFunctor C a) e.hom ≫ whiskerLeft (shiftFunctor C a) e.inv ≫ (iso a).hom ≫ whiskerRight e.hom (shiftFunctor D a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>a : α<GOAL>IsPrimal (Associates.mk a) ↔ IsPrimal a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>a : α<GOAL>(∀ (a_1 a_2 : α), a ∣ a_1 * a_2 → ∃ x x_1, x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Associates.mk a = Associates.mk (x * x_1)) ↔ ∀ ⦃b c : α⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel j i<GOAL>inlX φ i j hij ≫ sndX φ j = 0
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>j : ι<VAR>hij : c.Rel j (c.next j)<GOAL>inlX φ (c.next j) j hij ≫ sndX φ j = 0
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CommSq f i p g<GOAL>sq.HasLift → Nonempty sq.LiftStruct
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CommSq f i p g<GOAL>Nonempty sq.LiftStruct → sq.HasLift
<VAR>x✝ y z x : ℝ<GOAL>rexp 1 ^ x = rexp x
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>J : C<GOAL>Injective J ↔ (yoneda.obj J).PreservesEpimorphisms
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>J : C<GOAL>(coyoneda.obj (op (op J))).PreservesEpimorphisms ↔ (yoneda.obj J).PreservesEpimorphisms
<VAR>α : Type u_1<VAR>n : Num<GOAL>↑n.succ'.pred' = ↑n
<VAR>x : ℂ<VAR>hx : abs x ≤ 1<GOAL>abs (cexp x - 1) = abs (cexp x - ∑ m ∈ range 1, x ^ m / ↑m.factorial)
<VAR>x : ℂ<VAR>hx : abs x ≤ 1<GOAL>abs x ^ 1 * (↑(Nat.succ 1) * (↑(Nat.factorial 1) * ↑1)⁻¹) = 2 * abs x
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>I✝ J : Ideal R<VAR>N P : Submodule R M<VAR>I : Ideal R<VAR>m x : M<VAR>hx : x ∈ I • span R {m}<VAR>m1 m2 : M<VAR>x✝¹ : ∃ y ∈ I, y • m = m1<VAR>x✝ : ∃ y ∈ I, y • m = m2<VAR>y1 : R<VAR>hyi1 : y1 ∈ I<VAR>hy1 : y1 • m = m1<VAR>y2 : R<VAR>hyi2 : y2 ∈ I<VAR>hy2 : y2 • m = m2<GOAL>(y1 + y2) • m = m1 + m2
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a b : EReal<VAR>h : ContinuousAt (fun p => p.1 * p.2) (a, b)<VAR>this : (fun p => p.1 * p.2) = (fun x => -x) ∘ (fun p => p.1 * p.2) ∘ fun p => (-p.1, p.2)<GOAL>ContinuousAt ((fun x => -x) ∘ (fun p => p.1 * p.2) ∘ fun p => (-p.1, p.2)) (-a, b)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a b : EReal<VAR>h : ContinuousAt (fun p => p.1 * p.2) (a, b)<VAR>this : (fun p => p.1 * p.2) = (fun x => -x) ∘ (fun p => p.1 * p.2) ∘ fun p => (-p.1, p.2)<GOAL>ContinuousAt (fun p => p.1 * p.2) (-(-a, b).1, id (-a, b).2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>a : α<GOAL>count a l.dedup = if a ∈ l then 1 else 0
<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>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p1 p2 : P<VAR>hp1 : p1 ∈ s<GOAL>dist p1 p2 * dist p1 p2 = dist p1 ↑((orthogonalProjection s) p2) * dist p1 ↑((orthogonalProjection s) p2) + dist p2 ↑((orthogonalProjection s) p2) * dist p2 ↑((orthogonalProjection s) 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>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p1 p2 : P<VAR>hp1 : p1 ∈ s<GOAL>⟪p1 -ᵥ ↑((orthogonalProjection s) p2), ↑((orthogonalProjection s) p2) -ᵥ p2⟫_ℝ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α →ₛ ℝ≥0∞<VAR>x : ℝ≥0∞<GOAL>∑ r ∈ f.range, x * r * μ (↑f ⁻¹' {r}) = x * ∑ r ∈ f.range, r * μ (↑f ⁻¹' {r})
<VAR>Ω : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁹ : SMul R ℝ≥0<VAR>inst✝⁸ : SMul R ℝ≥0∞<VAR>inst✝⁷ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝⁶ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝⁵ : TopologicalSpace Ω<VAR>inst✝⁴ : OpensMeasurableSpace Ω<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0<VAR>inst✝² : PseudoMetricSpace R<VAR>inst✝¹ : Zero R<VAR>inst✝ : BoundedSMul R ℝ≥0<VAR>μ : FiniteMeasure Ω<VAR>c : R<VAR>f : Ω →ᵇ ℝ≥0<GOAL>μ.testAgainstNN (c • f) = c • μ.testAgainstNN f
<VAR>Ω : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁹ : SMul R ℝ≥0<VAR>inst✝⁸ : SMul R ℝ≥0∞<VAR>inst✝⁷ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝⁶ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝⁵ : TopologicalSpace Ω<VAR>inst✝⁴ : OpensMeasurableSpace Ω<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0<VAR>inst✝² : PseudoMetricSpace R<VAR>inst✝¹ : Zero R<VAR>inst✝ : BoundedSMul R ℝ≥0<VAR>μ : FiniteMeasure Ω<VAR>c : R<VAR>f : Ω →ᵇ ℝ≥0<GOAL>∫⁻ (ω : Ω), c • ↑(f ω) ∂↑μ = c • ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ
<VAR>Ω : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁹ : SMul R ℝ≥0<VAR>inst✝⁸ : SMul R ℝ≥0∞<VAR>inst✝⁷ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝⁶ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝⁵ : TopologicalSpace Ω<VAR>inst✝⁴ : OpensMeasurableSpace Ω<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0<VAR>inst✝² : PseudoMetricSpace R<VAR>inst✝¹ : Zero R<VAR>inst✝ : BoundedSMul R ℝ≥0<VAR>μ : FiniteMeasure Ω<VAR>c : R<VAR>f : Ω →ᵇ ℝ≥0<GOAL>∫⁻ (ω : Ω), c • 1 * ↑(f ω) ∂↑μ = c • 1 * ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ
<VAR>s : String<GOAL>s.back = s.data.getLastD default
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀✝ x₀ : X<VAR>hx₀ : x₀ ∈ s<GOAL>∑ i ∈ ρ.finsupport x₀, (ρ i) x₀ = 1
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x y : M<GOAL>Q (x - y) = Q (y - x)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.map' 0 2 ⋯ ⋯ = 0<VAR>hR₁' : Epi (R₁.map' 1 2 ⋯ ⋯)<VAR>hR₂ : R₂.Exact<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁ : Mono (app' φ 1 ⋯)<GOAL>Mono (app' φ 2 ⋯)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.map' 0 2 ⋯ ⋯ = 0<VAR>hR₁' : Epi (R₁.map' 1 2 ⋯ ⋯)<VAR>hR₂ : R₂.Exact<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁ : Mono (app' φ 1 ⋯)<VAR>ψ : mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 ⟶ mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 := homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) (𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 ⋯)) ⋯ ⋯ ⋯<GOAL>Mono (app' φ 2 ⋯)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.map' 0 2 ⋯ ⋯ = 0<VAR>hR₁' : Epi (R₁.map' 1 2 ⋯ ⋯)<VAR>hR₂ : R₂.Exact<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁ : Mono (app' φ 1 ⋯)<VAR>ψ : mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 ⟶ mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 := homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) (𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 ⋯)) ⋯ ⋯ ⋯<GOAL>(mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 0 2 ⋯ ⋯ = 0