ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus✝ : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this✝³ : (insert x s ∪ v) \ u ∈ 𝒜<VAR>hsv : Disjoint s v<VAR>hvu : Disjoint v u<VAR>hxv : x ∉ v<VAR>this✝² : v \ u = v<VAR>this✝¹ : x ∉ u<VAR>hus : u ⊆ s<VAR>w : α<VAR>hwB : w ∈ s ∪ v → w ∈ u<VAR>hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'<VAR>this✝ : v ⊆ insert w ((s ∪ v) \ u)<VAR>hwu : w ∉ u<VAR>this : (insert w ((s ∪ v) \ u) ∪ u) \ v ∈ 𝒜<GOAL>insert w s = (insert w ((s ∪ v) \ u) ∪ u) \ v
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>a b n : ℤ<GOAL>n + (a + b) = n + b + a
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>a b n : ℤ<GOAL>((shiftFunctorAdd (CochainComplex C ℤ) a b).hom.app K).f n = (XIsoOfEq K ⋯).hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>a b n : ℤ<VAR>this : IsIso (((shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n)<GOAL>((shiftFunctorAdd (CochainComplex C ℤ) a b).hom.app K).f n = (XIsoOfEq K ⋯).hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>a b n : ℤ<VAR>this : IsIso (((shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n)<GOAL>𝟙 (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) (a + b)).obj K).X n) = (XIsoOfEq K ⋯).hom ≫ (XIsoOfEq K ⋯).hom
<VAR>R : Type u<VAR>X : Type v<VAR>inst✝³ : CommRing R<VAR>S : Type u_1<VAR>inst✝² : Monoid S<VAR>inst✝¹ : DistribMulAction S R<VAR>inst✝ : IsScalarTower S R R<VAR>t : S<VAR>a b : lib R X<VAR>h : Rel R X a b<GOAL>Rel R X (t • a) (t • b)
<VAR>R : Type u<VAR>X : Type v<VAR>inst✝³ : CommRing R<VAR>S : Type u_1<VAR>inst✝² : Monoid S<VAR>inst✝¹ : DistribMulAction S R<VAR>inst✝ : IsScalarTower S R R<VAR>t : S<VAR>a b : lib R X<VAR>h : Rel R X a b<GOAL>Rel R X ((t • 1) • a) ((t • 1) • b)
<GOAL>StrictConcaveOn ℝ≥0 univ ⇑sqrt
<VAR>this : ⇑sqrt = fun x => x ^ (1 / 2)<GOAL>StrictConcaveOn ℝ≥0 univ ⇑sqrt
<VAR>this : ⇑sqrt = fun x => x ^ (1 / 2)<GOAL>StrictConcaveOn ℝ≥0 univ fun x => x ^ (1 / 2)
<VAR>n : ℕ<VAR>f : Vector ℕ n →. ℕ<VAR>pf : Partrec' f<GOAL>_root_.Partrec f
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M✝ : Type u_2<VAR>M'✝ : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M✝<VAR>inst✝¹⁵ : AddCommMonoid M'✝<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'✝<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M✝<VAR>inst✝⁸ : Module R M'✝<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'✝<VAR>f✝ : M✝ →ₗ[R] M'✝<VAR>g : M✝ →ₗ[R] M''<VAR>inst✝⁵ : IsLocalizedModule S f✝<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>inst✝⁴ : Semiring M<VAR>inst✝³ : Semiring M'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Algebra R M'<VAR>f : M →ₗ[R] M'<VAR>hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂<VAR>inst✝ : IsLocalizedModule S f<VAR>m₁ m₂ : M<VAR>s₁ s₂ : ↥S<GOAL>mk' f (m₁ * m₂) (s₁ * s₂) = mk' f m₁ s₁ * mk' f m₂ s₂
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M✝ : Type u_2<VAR>M'✝ : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M✝<VAR>inst✝¹⁵ : AddCommMonoid M'✝<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'✝<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M✝<VAR>inst✝⁸ : Module R M'✝<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'✝<VAR>f✝ : M✝ →ₗ[R] M'✝<VAR>g : M✝ →ₗ[R] M''<VAR>inst✝⁵ : IsLocalizedModule S f✝<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>inst✝⁴ : Semiring M<VAR>inst✝³ : Semiring M'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Algebra R M'<VAR>f : M →ₗ[R] M'<VAR>hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂<VAR>inst✝ : IsLocalizedModule S f<VAR>m₁ m₂ : M<VAR>s₁ s₂ : ↥S<GOAL>f (m₁ * m₂, s₁ * s₂).1 = ↑(m₁ * m₂, s₁ * s₂).2 • (mk' f m₁ s₁ * mk' f m₂ s₂)
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M✝ : Type u_2<VAR>M'✝ : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M✝<VAR>inst✝¹⁵ : AddCommMonoid M'✝<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'✝<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M✝<VAR>inst✝⁸ : Module R M'✝<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'✝<VAR>f✝ : M✝ →ₗ[R] M'✝<VAR>g : M✝ →ₗ[R] M''<VAR>inst✝⁵ : IsLocalizedModule S f✝<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>inst✝⁴ : Semiring M<VAR>inst✝³ : Semiring M'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Algebra R M'<VAR>f : M →ₗ[R] M'<VAR>hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂<VAR>inst✝ : IsLocalizedModule S f<VAR>m₁ m₂ : M<VAR>s₁ s₂ : ↥S<GOAL>f (m₁ • m₂) = (↑s₁ • ↑s₂) • mk' f m₁ s₁ • mk' f m₂ s₂
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M✝ : Type u_2<VAR>M'✝ : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M✝<VAR>inst✝¹⁵ : AddCommMonoid M'✝<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'✝<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M✝<VAR>inst✝⁸ : Module R M'✝<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'✝<VAR>f✝ : M✝ →ₗ[R] M'✝<VAR>g : M✝ →ₗ[R] M''<VAR>inst✝⁵ : IsLocalizedModule S f✝<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>inst✝⁴ : Semiring M<VAR>inst✝³ : Semiring M'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Algebra R M'<VAR>f : M →ₗ[R] M'<VAR>hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂<VAR>inst✝ : IsLocalizedModule S f<VAR>m₁ m₂ : M<VAR>s₁ s₂ : ↥S<GOAL>f (m₁ • m₂) = mk' f (↑s₁ • m₁) s₁ • mk' f (↑s₂ • m₂) s₂
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<VAR>w : W<GOAL>cs.length (w * t) ≠ cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<VAR>w : W<GOAL>cs.lengthParity (w * t) ≠ cs.lengthParity w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w✝ w : W<VAR>i : B<GOAL>cs.lengthParity (w✝ * (w * cs.simple i * w⁻¹)) ≠ cs.lengthParity w✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>s t : Set α<VAR>E : Type u_3<VAR>inst✝¹ : EquivLike E α β<VAR>inst✝ : OrderIsoClass E α β<VAR>e : E<GOAL>(range ⇑e).OrdConnected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>s t : Set α<VAR>E : Type u_3<VAR>inst✝¹ : EquivLike E α β<VAR>inst✝ : OrderIsoClass E α β<VAR>e : E<GOAL>(⇑e '' univ).OrdConnected
<GOAL>SurjOn sin (Icc (-(π / 2)) (π / 2)) (Icc (-1) 1)
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>f✝ f : M →ₗ[R] N →ₗ[R] P<VAR>m : M<VAR>n : N<GOAL>((uncurry R M N P) f) (m ⊗ₜ[R] n) = (f m) n
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>f✝ f : M →ₗ[R] N →ₗ[R] P<VAR>m : M<VAR>n : N<GOAL>(((LinearMap.lflip ∘ₗ LinearMap.id.flip) m) n) f = (f m) n
<VAR>m n : ℤ<VAR>h : m.gcd n = 1<VAR>hm : m % 2 = 1<VAR>hn : n % 2 = 0<GOAL>(m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
<VAR>m n : ℤ<VAR>h : m.gcd n = 1<VAR>hm : m % 2 = 1<VAR>hn : n % 2 = 0<GOAL>(-(m ^ 2 - n ^ 2)).natAbs.gcd (2 * m * n).natAbs = 1
<VAR>m n : ℤ<VAR>h : m.gcd n = 1<VAR>hm : m % 2 = 1<VAR>hn : n % 2 = 0<GOAL>(n ^ 2 - m ^ 2).natAbs.gcd (2 * n * m).natAbs = 1
<VAR>m n : ℤ<VAR>h : m.gcd n = 1<VAR>hm : m % 2 = 1<VAR>hn : n % 2 = 0<GOAL>n.gcd m = 1
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>Γ₀ : Type u_2<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>inst✝ : v.RankOne<GOAL>unit v ≠ 1
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>Γ₀ : Type u_2<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>inst✝ : v.RankOne<GOAL>¬↑(unit v) = 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : T2Space X<VAR>S : Set X<GOAL>IsIrreducible S ↔ ∃ x, S = {x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>v w : F<GOAL>((innerSL ℝ).flip v) w = ((innerSL ℝ) v) w
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>P : (H → H') → Set H → H → Prop<VAR>f : M → M'<VAR>x : M<GOAL>LiftPropAt P f x ↔ ContinuousAt f x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H 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 L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>x : E<VAR>hh : HasStrictDerivAt h₂ h₂' (f x)<VAR>hf : HasStrictFDerivAt f f' x<VAR>hy : y = f x<GOAL>HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝² : RCLike K<VAR>z : K<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace K E<VAR>n : ℕ<VAR>x : E<GOAL>‖n • x‖ = n • ‖x‖
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : R →+* S<VAR>x y : 𝕎 R<VAR>n : ℕ<GOAL>mapFun (⇑f) (x ^ n) = mapFun (⇑f) x ^ n
<VAR>α : Type u<VAR>c : Cardinal.{u}<GOAL>#{ t // #↑t ≤ c } ≤ max #α ℵ₀ ^ c
<VAR>α : Type u<VAR>c : Cardinal.{u}<GOAL>#(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ max #α ℵ₀ ^ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝³ : DecidableRel r<VAR>inst✝² : IsTrans α r<VAR>inst✝¹ : IsAntisymm α r<VAR>inst✝ : IsTotal α r<VAR>s : Finset α<GOAL>sort r s ~ s.toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝³ : DecidableRel r<VAR>inst✝² : IsTrans α r<VAR>inst✝¹ : IsAntisymm α r<VAR>inst✝ : IsTotal α r<VAR>s : Finset α<GOAL>↑(sort r s) = ↑s.toList
<VAR>x y : ℝ<GOAL>Real.toEReal '' Ioc x y = Ioc ↑x ↑y
<VAR>x y : ℝ<GOAL>WithBot.some '' (WithTop.some '' Ioc x y) = Ioc ↑x ↑y
<VAR>x y : ℝ<GOAL>Ioc ↑↑x ↑↑y = Ioc ↑x ↑y
<VAR>A : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>inst✝² : Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F G : A ⥤ B<VAR>H I : C ⥤ D<VAR>α : F ⟶ G<VAR>β : H ⟶ I<VAR>fst✝¹ : A<VAR>snd✝¹ : C<VAR>fst✝ : A<VAR>snd✝ : C<VAR>f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)<GOAL>(F.prod H).map f ≫ (fun X => (α.app X.1, β.app X.2)) (fst✝, snd✝) = (fun X => (α.app X.1, β.app X.2)) (fst✝¹, snd✝¹) ≫ (G.prod I).map f
<VAR>A : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>inst✝² : Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F G : A ⥤ B<VAR>H I : C ⥤ D<VAR>α : F ⟶ G<VAR>β : H ⟶ I<VAR>fst✝¹ : A<VAR>snd✝¹ : C<VAR>fst✝ : A<VAR>snd✝ : C<VAR>f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)<GOAL>(F.map f.1 ≫ α.app fst✝, H.map f.2 ≫ β.app snd✝) = (α.app fst✝¹ ≫ G.map f.1, β.app snd✝¹ ≫ I.map f.2)
<VAR>A : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>inst✝² : Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F G : A ⥤ B<VAR>H I : C ⥤ D<VAR>α : F ⟶ G<VAR>β : H ⟶ I<VAR>fst✝¹ : A<VAR>snd✝¹ : C<VAR>fst✝ : A<VAR>snd✝ : C<VAR>f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)<GOAL>F.map f.1 ≫ α.app fst✝ = α.app fst✝¹ ≫ G.map f.1 ∧ H.map f.2 ≫ β.app snd✝ = β.app snd✝¹ ≫ I.map f.2
<VAR>A : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>inst✝² : Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F G : A ⥤ B<VAR>H I : C ⥤ D<VAR>α : F ⟶ G<VAR>β : H ⟶ I<VAR>fst✝¹ : A<VAR>snd✝¹ : C<VAR>fst✝ : A<VAR>snd✝ : C<VAR>f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)<GOAL>F.map f.1 ≫ α.app fst✝ = α.app fst✝¹ ≫ G.map f.1
<VAR>A : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>inst✝² : Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F G : A ⥤ B<VAR>H I : C ⥤ D<VAR>α : F ⟶ G<VAR>β : H ⟶ I<VAR>fst✝¹ : A<VAR>snd✝¹ : C<VAR>fst✝ : A<VAR>snd✝ : C<VAR>f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)<GOAL>H.map f.2 ≫ β.app snd✝ = β.app snd✝¹ ≫ I.map f.2
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<GOAL>(l.node4R x m y r).dual = r.dual.node4L y m.dual x l.dual
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>a : ↑A<GOAL>g (f a) = h (f a)
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>a : ↑A<VAR>this : f a ∈ {b | h b = g b}<GOAL>g (f a) = h (f a)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>h : Function.Surjective ⇑f<VAR>x✝¹ : Ideal S<VAR>x✝ : x✝¹ ≠ ⊤<VAR>s : S<VAR>r : R<VAR>hr : f r = s<GOAL>1 ∉ x✝¹
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>h : Function.Surjective ⇑f<VAR>x✝¹ : Ideal S<VAR>x✝ : x✝¹ ≠ ⊤<VAR>s : S<VAR>r : R<VAR>hr : f r = s<GOAL>f 1 ∉ x✝¹
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>l : List M<VAR>f : M →ₗ[R] N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x<VAR>n : N<GOAL>((foldl Q f hf) n) (List.map (⇑(ι Q)) l).prod = List.foldl (fun m n => (f n) m) n l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>h : ∃ a, o = succ a<VAR>a : Ordinal.{u_4}<VAR>e : o = succ a<GOAL>o.pred ≤ o
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>h : ∃ a, o = succ a<VAR>a : Ordinal.{u_4}<VAR>e : o = succ a<GOAL>a ≤ succ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>h : ¬∃ a, o = succ a<GOAL>o.pred ≤ o
<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>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>f : M → M'<VAR>s : Set M<VAR>x : M<GOAL>MDifferentiableWithinAt I I' f s x ↔ ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
<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>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>f : M → M'<VAR>s : Set M<VAR>x : M<GOAL>ContinuousWithinAt f s x ∧ DifferentiableWithinAtProp I I' (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔ ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<GOAL>(N₁Γ₀.hom.app K).f.f n = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv.f.f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<GOAL>((Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom).f.f n = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv.f.f n
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<GOAL>Splits i f ↔ f = 0 ∨ ∀ {g : L[X]}, Irreducible g → g ∣ map i f → g.degree = 1
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I I₂ : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>I ≤ comap f (map f I)
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>s : Set α<VAR>hs : a ∈ s ↔ b ∈ s<GOAL>BijOn (⇑(swap a b)) s s
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>s : Set α<VAR>hs : a ∈ s ↔ b ∈ s<VAR>x : α<VAR>hx : x ∈ s<GOAL>(swap a b) x ∈ s
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>s : Set α<VAR>hs : a ∈ s ↔ b ∈ s<VAR>x : α<VAR>hx : x ∈ s<GOAL>x ∈ ⇑(swap a b) '' s
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>b : α<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>hs : x ∈ s ↔ b ∈ s<GOAL>x ∈ ⇑(swap x b) '' s
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>s : Set α<VAR>hs : a ∈ s ↔ b ∈ s<VAR>x : α<VAR>hx : x ∈ s<VAR>hxa : x ≠ a<GOAL>x ∈ ⇑(swap a b) '' s
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>hxa : x ≠ a<VAR>hs : a ∈ s ↔ x ∈ s<GOAL>x ∈ ⇑(swap a x) '' s
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>s : Set α<VAR>hs : a ∈ s ↔ b ∈ s<VAR>x : α<VAR>hx : x ∈ s<VAR>hxa : x ≠ a<VAR>hxb : x ≠ b<GOAL>x ∈ ⇑(swap a b) '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>δ : ι → Type u_5<VAR>φ : (i : ι) → δ i → α<VAR>𝔗 : (i : ι) → Set (Set (δ i))<VAR>h_image : ∀ (i : ι), MapsTo (fun x => φ i '' x) (𝔗 i) 𝔖<VAR>h_preimage : ∀ (i : ι), MapsTo (fun x => φ i ⁻¹' x) 𝔖 (𝔗 i)<VAR>h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)<VAR>ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i => S.restrictPreimage (φ i)<VAR>this : ∀ S ∈ 𝔖, UniformFun.uniformSpace (↑S) β = ⨅ i, UniformSpace.comap (fun x => x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)<GOAL>uniformSpace α β 𝔖 = ⨅ i, UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun x => x ∘ φ i) ∘ ⇑(toFun 𝔖)) (uniformSpace (δ i) β (𝔗 i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>δ : ι → Type u_5<VAR>φ : (i : ι) → δ i → α<VAR>𝔗 : (i : ι) → Set (Set (δ i))<VAR>h_image : ∀ (i : ι), MapsTo (fun x => φ i '' x) (𝔗 i) 𝔖<VAR>h_preimage : ∀ (i : ι), MapsTo (fun x => φ i ⁻¹' x) 𝔖 (𝔗 i)<VAR>h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)<VAR>ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i => S.restrictPreimage (φ i)<VAR>this : ∀ S ∈ 𝔖, UniformFun.uniformSpace (↑S) β = ⨅ i, UniformSpace.comap (fun x => x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)<VAR>i : ι<GOAL>uniformSpace α β 𝔖 ≤ UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun x => x ∘ φ i) ∘ ⇑(toFun 𝔖)) (uniformSpace (δ i) β (𝔗 i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>δ : ι → Type u_5<VAR>φ : (i : ι) → δ i → α<VAR>𝔗 : (i : ι) → Set (Set (δ i))<VAR>h_image : ∀ (i : ι), MapsTo (fun x => φ i '' x) (𝔗 i) 𝔖<VAR>h_preimage : ∀ (i : ι), MapsTo (fun x => φ i ⁻¹' x) 𝔖 (𝔗 i)<VAR>h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)<VAR>ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i => S.restrictPreimage (φ i)<VAR>this : ∀ S ∈ 𝔖, UniformFun.uniformSpace (↑S) β = ⨅ i, UniformSpace.comap (fun x => x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)<VAR>S : Set α<VAR>hS : S ∈ 𝔖<GOAL>⨅ i, UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun x => x ∘ φ i) ∘ ⇑(toFun 𝔖)) (uniformSpace (δ i) β (𝔗 i)) ≤ UniformSpace.comap (⇑UniformFun.ofFun ∘ S.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑S) β)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>r : A<VAR>x : ProjectiveSpectrum 𝒜<GOAL>x ∈ ↑(basicOpen 𝒜 r) ↔ x ∈ (zeroLocus 𝒜 {r})ᶜ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>r : A<VAR>x : ProjectiveSpectrum 𝒜<GOAL>x ∈ ↑(basicOpen 𝒜 r) ↔ r ∉ ↑x.asHomogeneousIdeal