ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>inst✝¹¹ : SmallCategory J<VAR>inst✝¹⁰ : Category.{v₂, u₂} K<VAR>inst✝⁹ : Small.{v, u₂} K<VAR>inst✝⁸ : FinCategory J<VAR>F✝ : J × K ⥤ Type v<VAR>inst✝⁷ : IsFiltered K<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasLimitsOfShape J C<VAR>inst✝³ : HasColimitsOfShape K C<VAR>inst✝² : ReflectsLimitsOfShape J (forget C)<VAR>inst✝¹ : PreservesColimitsOfShape K (forget C)<VAR>inst✝ : PreservesLimitsOfShape J (forget C)<VAR>F : J ⥤ K ⥤ C<VAR>a : K<VAR>b : J<GOAL>colimit.ι (F.obj b) a ≫ (HasColimit.isoOfNatIso (flipCompEvaluation F b)).inv ≫ (colimitObjIsoColimitCompEvaluation F.flip b).inv = (colimit.ι F.flip a).app b
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>inst✝¹¹ : SmallCategory J<VAR>inst✝¹⁰ : Category.{v₂, u₂} K<VAR>inst✝⁹ : Small.{v, u₂} K<VAR>inst✝⁸ : FinCategory J<VAR>F✝ : J × K ⥤ Type v<VAR>inst✝⁷ : IsFiltered K<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasLimitsOfShape J C<VAR>inst✝³ : HasColimitsOfShape K C<VAR>inst✝² : ReflectsLimitsOfShape J (forget C)<VAR>inst✝¹ : PreservesColimitsOfShape K (forget C)<VAR>inst✝ : PreservesLimitsOfShape J (forget C)<VAR>F : J ⥤ K ⥤ C<VAR>a : K<VAR>b : J<GOAL>colimit.ι (F.obj b) a = (flipCompEvaluation F b).hom.app a ≫ colimit.ι (F.obj b) a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Group G<VAR>x y : G<VAR>i : ℤ<VAR>h : IsOfFinOrder x<VAR>h' : y ∈ zpowers x<GOAL>IsOfFinOrder y
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Group G<VAR>x : G<VAR>i : ℤ<VAR>h : IsOfFinOrder x<VAR>k : ℤ<VAR>h' : x ^ k ∈ zpowers x<GOAL>IsOfFinOrder (x ^ k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>borel ℝ = generateFrom (⋃ a, {Iio ↑a})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>generateFrom (range Iio) = generateFrom (⋃ a, {Iio ↑a})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>∀ t ∈ range Iio, MeasurableSet t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>a : ℝ<GOAL>MeasurableSet (Iio a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>a : ℝ<VAR>this : IsLUB (range Rat.cast ∩ Iio a) a<GOAL>MeasurableSet (Iio a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>a : ℝ<VAR>this : IsLUB (range Rat.cast ∩ Iio a) a<GOAL>MeasurableSet (⋃ y ∈ Rat.cast ⁻¹' Iio a, Iio ↑y)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N₁<VAR>inst✝² : Monoid S<VAR>inst✝¹ : DistribMulAction S M<VAR>inst✝ : SMulCommClass R S M<VAR>f : Module.End R M<VAR>m : M<VAR>k l : ℕ<VAR>hk : k ≤ l<VAR>hm : (f ^ k) m = 0<GOAL>(f ^ l) m = 0
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>H N : Subgroup G<VAR>hN : N.Normal<GOAL>↑(H ⊔ N) = ↑H * ↑N
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>H N : Subgroup G<VAR>hN : N.Normal<GOAL>↑(closure (↑H * ↑N)) = ↑H * ↑N
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>H N : Subgroup G<VAR>hN : N.Normal<VAR>x : G<VAR>hx : x ∈ ↑(closure (↑H * ↑N))<GOAL>x ∈ ↑H * ↑N
<VAR>α : Type u_1<VAR>inst✝ : CommSemigroup α<VAR>s t : Set α<VAR>a : α<VAR>x : α × α<GOAL>x.swap ∈ s.mulAntidiagonal t a ↔ x ∈ t.mulAntidiagonal s a
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>hX : AEMeasurable X μ<GOAL>evariance X μ = 0 ↔ X =ᶠ[ae μ] fun x => ∫ (x : Ω), X x ∂μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>hX : AEMeasurable X μ<GOAL>(fun ω => ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2) =ᶠ[ae μ] 0 ↔ X =ᶠ[ae μ] fun x => ∫ (x : Ω), X x ∂μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>hX : AEMeasurable X μ<GOAL>AEMeasurable (fun ω => ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2) μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>hX✝ : AEMeasurable X μ<VAR>hX : (fun ω => ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2) =ᶠ[ae μ] 0<VAR>ω : Ω<VAR>hω : ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2 = 0 ω<GOAL>X ω = ∫ (x : Ω), X x ∂μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>hX✝ : AEMeasurable X μ<VAR>hX : X =ᶠ[ae μ] fun x => ∫ (x : Ω), X x ∂μ<VAR>ω : Ω<VAR>hω : X ω = ∫ (x : Ω), X x ∂μ<GOAL>↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2 = 0 ω
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLinearOrder α<VAR>s : Set α<VAR>f : ι → α<VAR>x : α<VAR>hlim : ¬IsPredLimit (sInf s)<GOAL>sInf s ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLinearOrder α<VAR>s : Set α<VAR>f : ι → α<VAR>x : α<VAR>hlim : ¬IsPredLimit (sInf s)<VAR>y : α<VAR>hy : sInf s ⋖ y<GOAL>sInf s ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLinearOrder α<VAR>s : Set α<VAR>f : ι → α<VAR>x : α<VAR>hlim : ¬IsPredLimit (sInf s)<VAR>y : α<VAR>hy : sInf s ⋖ y<VAR>i : α<VAR>his : i ∈ s<VAR>hi : i < y<GOAL>sInf s ∈ s
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>n : ℕ<GOAL>A ^ (- -[n+1]) = (A ^ -[n+1])⁻¹
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>n : ℕ<GOAL>IsUnit (A ^ (n + 1)).det
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>n : ℕ<GOAL>IsUnit (A.det ^ (n + 1))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : Archimedean α<VAR>a : α<GOAL>⋃ n, Ioc (↑n) (↑n + 1) = univ
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>P✝ : Generators R S<VAR>T : Type ?u.55681<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>P : Generators R T<VAR>s : T<GOAL>(aeval P.val) ((fun x => (MvPolynomial.map (algebraMap R S)) (P.σ x)) s) = s
<VAR>a b c : ℤ<VAR>ha : a ≠ 0<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>h3a : 3 ∣ a<VAR>HF : a ^ 3 + b ^ 3 + c ^ 3 = 0<VAR>H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3<GOAL>3 ∣ b
<VAR>a b c : ℤ<VAR>ha : a ≠ 0<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>h3a : 3 ∣ a<VAR>HF : a ^ 3 + b ^ 3 + c ^ 3 = 0<VAR>H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3<VAR>hbc : IsCoprime (-b) (-c)<GOAL>3 ∣ b
<VAR>a b c : ℤ<VAR>ha : a ≠ 0<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>h3a : 3 ∣ a<VAR>HF : a ^ 3 + b ^ 3 + c ^ 3 = 0<VAR>H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3<VAR>hbc : IsCoprime (-b) (-c)<VAR>h3b : ¬3 ∣ b<GOAL>False
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : NormedOrderedGroup α<VAR>s : Set α<VAR>hs : IsLowerSet s<VAR>ε : ℝ<GOAL>IsLowerSet (thickening ε s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : NormedOrderedGroup α<VAR>s : Set α<VAR>hs : IsLowerSet s<VAR>ε : ℝ<GOAL>IsLowerSet (ball 1 ε * s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>a : α<VAR>m : α → Filter β<GOAL>(pure a).bind m = m a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : SemilatticeSup α<VAR>inst✝² : SemilatticeSup β<VAR>ι : Sort u_4<VAR>S : Set (Set α)<VAR>f✝ : ι → Set α<VAR>s t : Set α<VAR>a : α<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : SupHomClass F α β<VAR>f : F<GOAL>SupClosed (range ⇑f)
<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>y : E<VAR>h : s =ᶠ[𝓝[{y}ᶜ] x] t<GOAL>𝓝[s \ {y}] x = 𝓝[t \ {y}] x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group G'<VAR>f : G →* G'<VAR>inst✝ : IsSimpleGroup G<VAR>n : ℕ<VAR>ih : derivedSeries G n.succ = _root_.commutator G<GOAL>derivedSeries G (n + 1).succ = _root_.commutator G
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group G'<VAR>f : G →* G'<VAR>inst✝ : IsSimpleGroup G<VAR>n : ℕ<VAR>ih : derivedSeries G n.succ = _root_.commutator G<GOAL>⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group G'<VAR>f : G →* G'<VAR>inst✝ : IsSimpleGroup G<VAR>n : ℕ<VAR>ih : derivedSeries G n.succ = _root_.commutator G<VAR>h : ⁅⊤, ⊤⁆ = ⊥<GOAL>⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group G'<VAR>f : G →* G'<VAR>inst✝ : IsSimpleGroup G<VAR>n : ℕ<VAR>ih : derivedSeries G n.succ = _root_.commutator G<VAR>h : ⁅⊤, ⊤⁆ = ⊤<GOAL>⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>ha : ∃ l, l < a<GOAL>𝓝[≤] a = ⨅ l, ⨅ (_ : l < a), 𝓟 (Ioc l 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>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ n₁₂ : ℤ<VAR>z₁ : Cochain F G n₁<VAR>z₂ : Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<VAR>p₁ p₂ p₃ : ℤ<VAR>h₁ : p₁ + n₁ = p₂<VAR>h₂ : p₂ + n₂ = p₃<GOAL>p₁ + n₁₂ = p₃
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μs_lim : Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize)<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)<GOAL>Tendsto μs F (𝓝 μ)
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μs_lim : Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize)<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)<GOAL>∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<GOAL>b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<GOAL>c ⊓ (b ⊓ a) ≤ c
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasForget₂ C Ab<VAR>inst✝³ : Preadditive C<VAR>inst✝² : (forget₂ C Ab).Additive<VAR>inst✝¹ : (forget₂ C Ab).PreservesHomology<VAR>inst✝ : HasZeroObject C<VAR>S : ShortComplex C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>Epi f ↔ Function.Surjective ((forget C).map f)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasForget₂ C Ab<VAR>inst✝³ : Preadditive C<VAR>inst✝² : (forget₂ C Ab).Additive<VAR>inst✝¹ : (forget₂ C Ab).PreservesHomology<VAR>inst✝ : HasZeroObject C<VAR>S : ShortComplex C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>Epi ⇑((forget₂ C Ab).map f) ↔ Epi ((forget C).map f)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasForget₂ C Ab<VAR>inst✝³ : Preadditive C<VAR>inst✝² : (forget₂ C Ab).Additive<VAR>inst✝¹ : (forget₂ C Ab).PreservesHomology<VAR>inst✝ : HasZeroObject C<VAR>S : ShortComplex C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>Arrow.mk ⇑((forget₂ C Ab).map f) ≅ Arrow.mk ((forget C).map f)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasForget₂ C Ab<VAR>inst✝³ : Preadditive C<VAR>inst✝² : (forget₂ C Ab).Additive<VAR>inst✝¹ : (forget₂ C Ab).PreservesHomology<VAR>inst✝ : HasZeroObject C<VAR>S : ShortComplex C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>e : forget₂ C Ab ⋙ forget Ab ≅ forget C<GOAL>Arrow.mk ⇑((forget₂ C Ab).map f) ≅ Arrow.mk ((forget C).map f)
<VAR>a : Bool<VAR>m : ℤ<VAR>b : Bool<VAR>n : ℤ<GOAL>(bit a m).xor (bit b n) = bit (xor a b) (m.xor n)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasShift C ℤ<VAR>X : Cᵒᵖ<VAR>a₁ a₂ a₃ : ℤ<VAR>h : a₁ + a₂ = a₃<VAR>b₁ b₂ b₃ : ℤ<VAR>h₁ : a₁ + b₁ = 0<VAR>h₂ : a₂ + b₂ = 0<VAR>h₃ : a₃ + b₃ = 0<GOAL>(shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app X = (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫ ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((shiftFunctor C b₁).toPrefunctor.1 (Opposite.unop X))) ≫ (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C a₁ b₁ h₁).inv.app X)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasShift C ℤ<VAR>X : Cᵒᵖ<VAR>a₁ a₂ a₃ : ℤ<VAR>h : a₁ + a₂ = a₃<VAR>b₁ b₂ b₃ : ℤ<VAR>h₁ : a₁ + b₁ = 0<VAR>h₂ : a₂ + b₂ = 0<VAR>h₃ : a₃ + b₃ = 0<GOAL>(pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n => -n) CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux.proof_1) a₃ b₃ ⋯).hom.app X ≫ (shiftFunctorAdd' (OppositeShift C ℤ) b₁ b₂ b₃ ⋯).hom.app X ≫ (pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n => -n) CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux.proof_1) a₂ b₂ ⋯).inv.app ((shiftFunctor (OppositeShift C ℤ) b₁).obj X) ≫ (shiftFunctor (PullbackShift (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n => -n) CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux.proof_1)) a₂).map ((pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n => -n) CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux.proof_1) a₁ b₁ ⋯).inv.app X) = (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫ ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((shiftFunctor C b₁).toPrefunctor.1 (Opposite.unop X))) ≫ (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C a₁ b₁ h₁).inv.app X)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasShift C ℤ<VAR>X : Cᵒᵖ<VAR>a₁ a₂ a₃ : ℤ<VAR>h : a₁ + a₂ = a₃<VAR>b₁ b₂ b₃ : ℤ<VAR>h₁ : a₁ + b₁ = 0<VAR>h₂ : a₂ + b₂ = 0<VAR>h₃ : a₃ + b₃ = 0<GOAL>(pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n => -n) CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux.proof_1) a₃ b₃ ⋯).hom.app X ≫ ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫ (pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n => -n) CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux.proof_1) a₂ b₂ ⋯).inv.app ((shiftFunctor (OppositeShift C ℤ) b₁).obj X) ≫ (shiftFunctor (PullbackShift (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n => -n) CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux.proof_1)) a₂).map ((pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n => -n) CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux.proof_1) a₁ b₁ ⋯).inv.app X) = (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫ ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((shiftFunctor C b₁).toPrefunctor.1 (Opposite.unop X))) ≫ (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C a₁ b₁ h₁).inv.app X)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>a : α<VAR>x : γ<GOAL>κ.rnDeriv η a x = ⊤ ↔ x ∈ κ.mutuallySingularSetSlice η a
<VAR>R : Type u_1<VAR>inst✝ : MulZeroClass R<VAR>a b : R<VAR>hb : IsLeftRegular b<GOAL>b * a = 0 ↔ a = 0
<VAR>R : Type u_1<VAR>inst✝ : MulZeroClass R<VAR>a b : R<VAR>hb : IsLeftRegular b<GOAL>b * a = b * 0 ↔ a = 0
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Preorder M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x a : M<VAR>n m : ℕ<VAR>ha : 1 ≤ a<VAR>h : n ≤ m<VAR>k : ℕ<VAR>hk : n + k = m<GOAL>a ^ n * a ^ k = a ^ m
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>M : Monad C<VAR>x✝ : C<GOAL>(MonoidalCategory.whiskerRight M.μ M.toFunctor ≫ M.μ).app x✝ = ((MonoidalCategory.associator M.toFunctor M.toFunctor M.toFunctor).hom ≫ MonoidalCategory.whiskerLeft M.toFunctor M.μ ≫ M.μ).app x✝
<VAR>C : Type u'<VAR>inst✝ : Category.{v', u'} C<VAR>R R' : Cᵒᵖ ⥤ RingCat<VAR>M' : PresheafOfModules R'<VAR>α : R ⟶ R'<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>r : ↑(R.obj X)<VAR>x : ↑((fun X => (ModuleCat.restrictScalars (α.app X)).obj (M'.obj X)) X)<GOAL>{ toFun := ⇑(M'.map f), map_add' := ⋯ }.toFun (r • x) = (RingHom.id ↑(R.obj X)) r • { toFun := ⇑(M'.map f), map_add' := ⋯ }.toFun x
<VAR>C : Type u'<VAR>inst✝ : Category.{v', u'} C<VAR>R R' : Cᵒᵖ ⥤ RingCat<VAR>M' : PresheafOfModules R'<VAR>α : R ⟶ R'<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>r : ↑(R.obj X)<VAR>x : ↑((fun X => (ModuleCat.restrictScalars (α.app X)).obj (M'.obj X)) X)<VAR>eq : (R.map f ≫ α.app Y) r = (α.app X ≫ R'.map f) r<GOAL>{ toFun := ⇑(M'.map f), map_add' := ⋯ }.toFun (r • x) = (RingHom.id ↑(R.obj X)) r • { toFun := ⇑(M'.map f), map_add' := ⋯ }.toFun x
<VAR>C : Type u'<VAR>inst✝ : Category.{v', u'} C<VAR>R R' : Cᵒᵖ ⥤ RingCat<VAR>M' : PresheafOfModules R'<VAR>α : R ⟶ R'<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>r : ↑(R.obj X)<VAR>x : ↑((fun X => (ModuleCat.restrictScalars (α.app X)).obj (M'.obj X)) X)<VAR>eq : (R.map f ≫ α.app Y) r = (α.app X ≫ R'.map f) r<GOAL>(R'.map f) ((α.app X) r) • (M'.presheaf.map f) x = (RingHom.id ↑(R.obj X)) r • { toFun := ⇑(M'.map f), map_add' := ⋯ }.toFun x
<VAR>C : Type u'<VAR>inst✝ : Category.{v', u'} C<VAR>R R' : Cᵒᵖ ⥤ RingCat<VAR>M' : PresheafOfModules R'<VAR>α : R ⟶ R'<VAR>X : Cᵒᵖ<VAR>x : ↑((fun X => (ModuleCat.restrictScalars (α.app X)).obj (M'.obj X)) X)<GOAL>((fun {X Y} f => { toFun := ⇑(M'.map f), map_add' := ⋯, map_smul' := ⋯ }) (𝟙 X)) x = ((ModuleCat.restrictScalarsId' (R.map (𝟙 X)) ⋯).inv.app ((fun X => (ModuleCat.restrictScalars (α.app X)).obj (M'.obj X)) X)) x
<VAR>C : Type u'<VAR>inst✝ : Category.{v', u'} C<VAR>R R' : Cᵒᵖ ⥤ RingCat<VAR>M' : PresheafOfModules R'<VAR>α : R ⟶ R'<VAR>X✝ Y✝ Z✝ : Cᵒᵖ<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>x : ↑((fun X => (ModuleCat.restrictScalars (α.app X)).obj (M'.obj X)) X✝)<GOAL>((fun {X Y} f => { toFun := ⇑(M'.map f), map_add' := ⋯, map_smul' := ⋯ }) (f ≫ g)) x = ((fun {X Y} f => { toFun := ⇑(M'.map f), map_add' := ⋯, map_smul' := ⋯ }) f ≫ (ModuleCat.restrictScalars (R.map f)).map ((fun {X Y} f => { toFun := ⇑(M'.map f), map_add' := ⋯, map_smul' := ⋯ }) g) ≫ (ModuleCat.restrictScalarsComp' (R.map f) (R.map g) (R.map (f ≫ g)) ⋯).inv.app ((fun X => (ModuleCat.restrictScalars (α.app X)).obj (M'.obj X)) Z✝)) x
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Mul β<VAR>f g : FreeSemigroup α →ₙ* β<VAR>h : ⇑f ∘ of = ⇑g ∘ of<VAR>x✝ : FreeSemigroup α<VAR>x : α<VAR>y : FreeSemigroup α<VAR>hx : f (of x) = g (of x)<VAR>hy : f y = g y<GOAL>f (of x * y) = g (of x * y)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>V : Rep k G<VAR>g : G<VAR>x : CoeSort.coe V<GOAL>(RestrictScalars.addEquiv k (MonoidAlgebra k G) V.ρ.asModule).symm (V.ρ.asModuleEquiv.symm ((V.ρ g) x)) = ((Representation.ofModule ↑(ModuleCat.of (MonoidAlgebra k G) V.ρ.asModule)) g) ((RestrictScalars.addEquiv k (MonoidAlgebra k G) V.ρ.asModule).symm (V.ρ.asModuleEquiv.symm x))
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>V : Rep k G<VAR>g : G<VAR>x : CoeSort.coe V<GOAL>(MonoidAlgebra.of k G) g • V.ρ.asModuleEquiv.symm x = ((Representation.ofModule ↑(ModuleCat.of (MonoidAlgebra k G) V.ρ.asModule)) g) ((RestrictScalars.addEquiv k (MonoidAlgebra k G) V.ρ.asModule).symm (V.ρ.asModuleEquiv.symm x))
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝¹ : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : IsAffine Y<VAR>ι : Type u_1<VAR>U : ι → ↑X.affineOpens<VAR>hU : ⨆ i, ↑(U i) = ⊤<VAR>H : ∀ (i : ι), Q (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯)<GOAL>P f
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝¹ : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : IsAffine Y<VAR>ι : Type u_1<VAR>U : ι → ↑X.affineOpens<VAR>hU : ⨆ i, ↑(U i) = ⊤<VAR>H : ∀ (i : ι), Q (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯)<VAR>this : ∀ (i : (X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).J), IsAffine ((X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).obj i)<GOAL>P f
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝¹ : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : IsAffine Y<VAR>ι : Type u_1<VAR>U : ι → ↑X.affineOpens<VAR>hU : ⨆ i, ↑(U i) = ⊤<VAR>H : ∀ (i : ι), Q (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯)<VAR>this : ∀ (i : (X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).J), IsAffine ((X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).obj i)<VAR>i : (X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).J<GOAL>Q (Scheme.Hom.app ((X.openCoverOfISupEqTop (fun i => ↑(U i)) hU).map i ≫ f) ⊤)
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f : CauSeq β abv<GOAL>(-f - const abv (-f.lim)).LimZero
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f : CauSeq β abv<GOAL>(const abv f.lim - f).LimZero
<VAR>α β : Type u<VAR>a : Cardinal.{u}<GOAL>0 < lift.{v, u} a ↔ 0 < a
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : CompleteSpace F<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<VAR>g'inv : G →L[𝕜] E<VAR>hg'inv : φ.rightDeriv.comp g'inv = ContinuousLinearMap.id 𝕜 G<VAR>hg'invf : φ.leftDeriv.comp g'inv = 0<GOAL>HasStrictFDerivAt (φ.implicitFunction (φ.leftFun φ.pt)) g'inv (φ.rightFun φ.pt)
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : CompleteSpace F<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<VAR>g'inv : G →L[𝕜] E<VAR>hg'inv : φ.rightDeriv.comp g'inv = ContinuousLinearMap.id 𝕜 G<VAR>hg'invf : φ.leftDeriv.comp g'inv = 0<VAR>this : HasStrictFDerivAt (HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) φ.pt ⋯) (↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm) (φ.prodFun φ.pt)<GOAL>HasStrictFDerivAt (φ.implicitFunction (φ.leftFun φ.pt)) g'inv (φ.rightFun φ.pt)