ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>l : Filter X<VAR>h : l = ⊥<GOAL>⊥.lift' closure = ⊥
<VAR>α : Type u_1<VAR>p : PosNum<GOAL>castNum <$> (pos p).ppred = (↑(pos p)).ppred
<VAR>α : Type u_1<VAR>p : PosNum<GOAL>(↑p.pred').succ = ↑(pos p)
<VAR>α : Type u_1<VAR>p : PosNum<GOAL>↑p = ↑(pos p)
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>f : R⟦X⟧<VAR>n a : ℕ<GOAL>trunc n (↑(trunc n f) ^ a) = trunc n (f ^ a)
<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>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : MDifferentiableAt I I' f x<GOAL>mfderiv I I' f x = fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (range ↑I) (↑(extChartAt I x) x)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hxz : x ≤ z<VAR>hyz : y ≤ z<VAR>h : z \ x = z \ y<GOAL>x = y
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<GOAL>G.dist u v = G.dist v u
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>x y : ι → ℝ<VAR>a✝¹ a✝ : Box ι<GOAL>↑↑a✝¹ ⊆ ↑↑a✝ ↔ ↑a✝¹ ≤ ↑a✝
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁹ : SeminormedAddCommGroup E<VAR>inst✝¹⁸ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁷ : SeminormedAddCommGroup F<VAR>inst✝¹⁶ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup G<VAR>inst✝¹⁴ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : NontriviallyNormedField 𝕜₂<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁸ : NormedSpace 𝕜₂ F<VAR>inst✝⁷ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁶ : NormedSpace 𝕜₃ G<VAR>inst✝⁵ : NormedSpace 𝕜 Gₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝³ : FunLike 𝓕 E F<VAR>inst✝² : RingHomIsometric σ₂₃<VAR>inst✝¹ : RingHomIsometric σ₁₃<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>L : E →L[𝕜] Fₗ →L[𝕜] Gₗ<GOAL>1 * ‖L‖ = ‖L‖
<VAR>a b : ℝ<VAR>n : ℕ<VAR>t : ℂ<VAR>ht : t ≠ -1<GOAL>∫ (x : ℝ) in a..b, ↑x * (1 + ↑x ^ 2) ^ t = (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + ↑a ^ 2) ^ (t + 1) / (2 * (t + 1))
<VAR>a b : ℝ<VAR>n : ℕ<VAR>t : ℂ<VAR>ht : t ≠ -1<VAR>this : t + 1 ≠ 0<GOAL>∫ (x : ℝ) in a..b, ↑x * (1 + ↑x ^ 2) ^ t = (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + ↑a ^ 2) ^ (t + 1) / (2 * (t + 1))
<VAR>a b : ℝ<VAR>n : ℕ<VAR>t : ℂ<VAR>ht : t ≠ -1<VAR>this : t + 1 ≠ 0<GOAL>∀ x ∈ [[a, b]], HasDerivAt (fun {b} => (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1))) (↑x * (1 + ↑x ^ 2) ^ t) x
<VAR>a b : ℝ<VAR>n : ℕ<VAR>t : ℂ<VAR>ht : t ≠ -1<VAR>this : t + 1 ≠ 0<GOAL>IntervalIntegrable (fun y => ↑y * (1 + ↑y ^ 2) ^ t) MeasureTheory.volume a b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<GOAL>padicValRat p (q / r) = padicValRat p q - padicValRat p r
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>s : Set (Submodule R M)<VAR>m : M<GOAL>m ∈ sSup s ↔ ∀ (N : Submodule R M), (∀ p ∈ s, p ≤ N) → m ∈ N
<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>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>z : DirectLimit G f<VAR>ind : ι<VAR>x✝ : FreeCommRing ((i : ι) × G i)<VAR>s✝ : Multiplicative (Multiset ((i : ι) × G i))<VAR>a : (i : ι) × G i<VAR>s : Multiset ((i : ι) × G i)<VAR>ih : ∃ i x, (of G f i) x = Quotient.mk'' (FreeAbelianGroup.of s)<VAR>i : ι<VAR>x : G i<VAR>j : ι<VAR>y : G j<VAR>hs : (of G f j) y = Quotient.mk'' (FreeAbelianGroup.of s)<VAR>k : ι<VAR>hik : i ≤ k<VAR>hjk : j ≤ k<GOAL>(of G f k) (f i k hik x * f j k hjk y) = Quotient.mk'' (FreeAbelianGroup.of (⟨i, x⟩ ::ₘ s))
<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>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>z : DirectLimit G f<VAR>ind : ι<VAR>x✝ : FreeCommRing ((i : ι) × G i)<VAR>s✝ : Multiplicative (Multiset ((i : ι) × G i))<VAR>a : (i : ι) × G i<VAR>s : Multiset ((i : ι) × G i)<VAR>ih : ∃ i x, (of G f i) x = Quotient.mk'' (FreeAbelianGroup.of s)<VAR>i : ι<VAR>x : G i<VAR>j : ι<VAR>y : G j<VAR>hs : (of G f j) y = Quotient.mk'' (FreeAbelianGroup.of s)<VAR>k : ι<VAR>hik : i ≤ k<VAR>hjk : j ≤ k<GOAL>(of G f i) x * Quotient.mk'' (FreeAbelianGroup.of s) = Quotient.mk'' (FreeAbelianGroup.of (⟨i, x⟩ ::ₘ s))
<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>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>z : DirectLimit G f<VAR>ind : ι<VAR>x✝ : FreeCommRing ((i : ι) × G i)<VAR>s✝ : Multiplicative (Multiset ((i : ι) × G i))<VAR>a : (i : ι) × G i<VAR>s : Multiset ((i : ι) × G i)<VAR>ih : ∃ i x, (of G f i) x = Quotient.mk'' (FreeAbelianGroup.of s)<VAR>i : ι<VAR>x : G i<VAR>j : ι<VAR>y : G j<VAR>hs : (of G f j) y = Quotient.mk'' (FreeAbelianGroup.of s)<VAR>k : ι<VAR>hik : i ≤ k<VAR>hjk : j ≤ k<GOAL>FreeAbelianGroup.of (⟨i, x⟩ ::ₘ s) = (fun x x_1 => x * x_1) (FreeCommRing.of ⟨i, x⟩) (FreeAbelianGroup.of s)
<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>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>z : DirectLimit G f<VAR>ind : ι<VAR>x✝¹ : FreeCommRing ((i : ι) × G i)<VAR>s : Multiplicative (Multiset ((i : ι) × G i))<VAR>x✝ : ∃ i x, (of G f i) x = Quotient.mk'' (FreeAbelianGroup.of s)<VAR>i : ι<VAR>x : G i<VAR>ih : (of G f i) x = Quotient.mk'' (FreeAbelianGroup.of s)<GOAL>(of G f i) (-x) = Quotient.mk'' (-FreeAbelianGroup.of s)
<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>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>z : DirectLimit G f<VAR>ind : ι<VAR>x✝¹ : FreeCommRing ((i : ι) × G i)<VAR>s : Multiplicative (Multiset ((i : ι) × G i))<VAR>x✝ : ∃ i x, (of G f i) x = Quotient.mk'' (FreeAbelianGroup.of s)<VAR>i : ι<VAR>x : G i<VAR>ih : (of G f i) x = Quotient.mk'' (FreeAbelianGroup.of s)<GOAL>-Quotient.mk'' (FreeAbelianGroup.of s) = Quotient.mk'' (-FreeAbelianGroup.of s)
<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>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>z : DirectLimit G f<VAR>ind : ι<VAR>x✝² : FreeCommRing ((i : ι) × G i)<VAR>p q : FreeAbelianGroup (Multiplicative (Multiset ((i : ι) × G i)))<VAR>x✝¹ : ∃ i x, (of G f i) x = Quotient.mk'' p<VAR>x✝ : ∃ i x, (of G f i) x = Quotient.mk'' q<VAR>i : ι<VAR>x : G i<VAR>ihx : (of G f i) x = Quotient.mk'' p<VAR>j : ι<VAR>y : G j<VAR>ihy : (of G f j) y = Quotient.mk'' q<VAR>k : ι<VAR>hik : i ≤ k<VAR>hjk : j ≤ k<GOAL>(of G f k) (f i k hik x + f j k hjk y) = Quotient.mk'' (p + q)
<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>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>z : DirectLimit G f<VAR>ind : ι<VAR>x✝² : FreeCommRing ((i : ι) × G i)<VAR>p q : FreeAbelianGroup (Multiplicative (Multiset ((i : ι) × G i)))<VAR>x✝¹ : ∃ i x, (of G f i) x = Quotient.mk'' p<VAR>x✝ : ∃ i x, (of G f i) x = Quotient.mk'' q<VAR>i : ι<VAR>x : G i<VAR>ihx : (of G f i) x = Quotient.mk'' p<VAR>j : ι<VAR>y : G j<VAR>ihy : (of G f j) y = Quotient.mk'' q<VAR>k : ι<VAR>hik : i ≤ k<VAR>hjk : j ≤ k<GOAL>Quotient.mk'' p + Quotient.mk'' q = Quotient.mk'' (p + q)
<VAR>a b : ℕ+<GOAL>Fintype.card ↑(Set.Icc a b) = ↑b + 1 - ↑a
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : Field k<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : AddTorsor E PE<VAR>f : k → PE<VAR>a b c : k<VAR>h : a ≠ c<GOAL>(lineMap (slope f a b) (slope f b c)) ((c - b) / (c - a)) = slope f a c
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>f : w.StructuredArrowRightwards g<GOAL>((w.structuredArrowDownwards X₂).obj (StructuredArrow.mk f.hom.left)).hom ≫ B.map f.right.hom = (StructuredArrow.mk g).hom
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>f₁ f₂ : w.StructuredArrowRightwards g<VAR>φ : f₁ ⟶ f₂<GOAL>f₁.hom.left ≫ T.map φ.right.left = f₂.hom.left
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>f₁ f₂ : w.StructuredArrowRightwards g<VAR>φ : f₁ ⟶ f₂<GOAL>f₁.hom.left ≫ T.map φ.right.left = (f₁.hom ≫ (w.costructuredArrowRightwards X₃).map φ.right).left
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>f₁ f₂ : w.StructuredArrowRightwards g<VAR>φ : f₁ ⟶ f₂<GOAL>((w.structuredArrowDownwards X₂).map (StructuredArrow.homMk φ.right.left ⋯) ≫ ((fun f => CostructuredArrow.mk (StructuredArrow.homMk f.right.hom ⋯)) f₂).hom).right = ((fun f => CostructuredArrow.mk (StructuredArrow.homMk f.right.hom ⋯)) f₁).hom.right
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>c : T₁.obj₃ ⟶ T₂.obj₃<VAR>comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃<GOAL>∃ b, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a✝ : T₁.obj₁ ⟶ T₂.obj₁<VAR>c : T₁.obj₃ ⟶ T₂.obj₃<VAR>comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃<VAR>a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃<VAR>ha₁ : T₁.invRotate.mor₂ ≫ a = a✝ ≫ T₂.invRotate.mor₂<VAR>ha₂ : T₁.invRotate.mor₃ ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) = a ≫ T₂.invRotate.mor₃<GOAL>∃ b, T₁.mor₁ ≫ b = a✝ ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a✝ : T₁.obj₁ ⟶ T₂.obj₁<VAR>c : T₁.obj₃ ⟶ T₂.obj₃<VAR>comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃<VAR>a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃<VAR>ha₁ : T₁.invRotate.mor₂ ≫ a = a✝ ≫ T₂.invRotate.mor₂<VAR>ha₂ : (T₁.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) = a ≫ T₂.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₂.3<GOAL>T₁.mor₂ ≫ c = a ≫ T₂.mor₂
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a✝ : T₁.obj₁ ⟶ T₂.obj₁<VAR>c : T₁.obj₃ ⟶ T₂.obj₃<VAR>comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃<VAR>a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃<VAR>ha₁ : T₁.invRotate.mor₂ ≫ a = a✝ ≫ T₂.invRotate.mor₂<VAR>ha₂ : (T₁.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) = a ≫ T₂.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₂.3<GOAL>T₁.mor₂ ≫ c ≫ (shiftEquiv C 1).counitIso.inv.app T₂.obj₃ = (T₁.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c)
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝³ : CommRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : _root_.Finite ι<VAR>b : Basis ι K V<GOAL>lift.{uK, uV} (Module.rank K V) = Module.rank K (Dual K V)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) = pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a : α<GOAL>(↑s).EquitableOn f ↔ ∀ a ∈ s, f a = (∑ i ∈ s, f i) / s.card ∨ f a = (∑ i ∈ s, f i) / s.card + 1
<VAR>S : Type u'<VAR>T : Type u''<VAR>R : Type u<VAR>M✝ : Type v<VAR>M : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>s : SubMulAction M α<GOAL>Set.range ⇑s.inclusion = s.carrier
<VAR>S : Type u'<VAR>T : Type u''<VAR>R : Type u<VAR>M✝ : Type v<VAR>M : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>s : SubMulAction M α<GOAL>Set.range Subtype.val = s.carrier
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀✝ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F → G<VAR>g : E → F<VAR>t : Set F<VAR>n : ℕ<VAR>x₀ : E<VAR>hf : ContDiffWithinAt 𝕜 (↑n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)<VAR>hg : ContDiffWithinAt 𝕜 (↑n) g s x₀<VAR>hgt : t ∈ 𝓝[g '' s] g x₀<GOAL>∃ v ∈ 𝓝[insert x₀ s] x₀, v ⊆ insert x₀ s ∧ ∃ f', (∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)) ∧ ContDiffWithinAt 𝕜 (↑n) (fun x => f' x) s x₀
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀✝ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F → G<VAR>g : E → F<VAR>t : Set F<VAR>n : ℕ<VAR>x₀ : E<VAR>hf : ContDiffWithinAt 𝕜 (↑n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)<VAR>hg : ContDiffWithinAt 𝕜 (↑n) g s x₀<VAR>hgt : t ∈ 𝓝[g '' s] g x₀<VAR>hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun x => (x, g x)) '' s] (x₀, g x₀)<GOAL>∃ v ∈ 𝓝[insert x₀ s] x₀, v ⊆ insert x₀ s ∧ ∃ f', (∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)) ∧ ContDiffWithinAt 𝕜 (↑n) (fun x => f' x) s x₀
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀✝ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F → G<VAR>g : E → F<VAR>t : Set F<VAR>n : ℕ<VAR>x₀ : E<VAR>hf : ContDiffWithinAt 𝕜 (↑n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)<VAR>hg : ContDiffWithinAt 𝕜 (↑n) g s x₀<VAR>hgt : t ∈ 𝓝[g '' s] g x₀<VAR>hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun x => (x, g x)) '' s] (x₀, g x₀)<VAR>v : Set (E × F)<VAR>hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)<VAR>hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)<VAR>f' : E × F → E × F →L[𝕜] G<VAR>hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x<VAR>hf' : ContDiffWithinAt 𝕜 (↑↑n) f' (insert x₀ s ×ˢ t) (x₀, g x₀)<GOAL>∃ v ∈ 𝓝[insert x₀ s] x₀, v ⊆ insert x₀ s ∧ ∃ f', (∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)) ∧ ContDiffWithinAt 𝕜 (↑n) (fun x => f' x) s x₀
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀✝ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F → G<VAR>g : E → F<VAR>t : Set F<VAR>n : ℕ<VAR>x₀ : E<VAR>hf : ContDiffWithinAt 𝕜 (↑n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)<VAR>hg : ContDiffWithinAt 𝕜 (↑n) g s x₀<VAR>hgt : t ∈ 𝓝[g '' s] g x₀<VAR>hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun x => (x, g x)) '' s] (x₀, g x₀)<VAR>v : Set (E × F)<VAR>hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)<VAR>hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)<VAR>f' : E × F → E × F →L[𝕜] G<VAR>hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x<VAR>hf' : ContDiffWithinAt 𝕜 (↑↑n) f' (insert x₀ s ×ˢ t) (x₀, g x₀)<GOAL>(fun z => (z, g z)) ⁻¹' v ∩ insert x₀ s ∈ 𝓝[insert x₀ s] x₀
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀✝ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F → G<VAR>g : E → F<VAR>t : Set F<VAR>n : ℕ<VAR>x₀ : E<VAR>hf : ContDiffWithinAt 𝕜 (↑n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)<VAR>hg : ContDiffWithinAt 𝕜 (↑n) g s x₀<VAR>hgt : t ∈ 𝓝[g '' s] g x₀<VAR>hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun x => (x, g x)) '' s] (x₀, g x₀)<VAR>v : Set (E × F)<VAR>hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)<VAR>hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)<VAR>f' : E × F → E × F →L[𝕜] G<VAR>hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x<VAR>hf' : ContDiffWithinAt 𝕜 (↑↑n) f' (insert x₀ s ×ˢ t) (x₀, g x₀)<GOAL>∀ x ∈ (fun z => (z, g z)) ⁻¹' v ∩ insert x₀ s, HasFDerivWithinAt (f x) ((fun z => (f' (z, g z)).comp (ContinuousLinearMap.inr 𝕜 E F)) x) t (g x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀✝ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F → G<VAR>g : E → F<VAR>t : Set F<VAR>n : ℕ<VAR>x₀ : E<VAR>hf : ContDiffWithinAt 𝕜 (↑n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)<VAR>hg : ContDiffWithinAt 𝕜 (↑n) g s x₀<VAR>hgt : t ∈ 𝓝[g '' s] g x₀<VAR>hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun x => (x, g x)) '' s] (x₀, g x₀)<VAR>v : Set (E × F)<VAR>hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)<VAR>hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)<VAR>f' : E × F → E × F →L[𝕜] G<VAR>hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x<VAR>hf' : ContDiffWithinAt 𝕜 (↑↑n) f' (insert x₀ s ×ˢ t) (x₀, g x₀)<GOAL>ContDiffWithinAt 𝕜 (↑n) (fun x => (fun z => (f' (z, g z)).comp (ContinuousLinearMap.inr 𝕜 E F)) x) s x₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<GOAL>s.diag.card = s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<GOAL>s.diag = image (fun a => (a, a)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<VAR>a₁ a₂ : α<GOAL>(a₁, a₂) ∈ s.diag ↔ (a₁, a₂) ∈ image (fun a => (a, a)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<VAR>a₁ a₂ : α<GOAL>(a₁, a₂).1 ∈ s ∧ (a₁, a₂).1 = (a₁, a₂).2 ↔ (a₁, a₂) ∈ image (fun a => (a, a)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<VAR>a₁ a₂ : α<VAR>h : (a₁, a₂).1 ∈ s ∧ (a₁, a₂).1 = (a₁, a₂).2<GOAL>∃ a ∈ s, (a, a) = (a₁, a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<VAR>a₁ a₂ : α<VAR>h : ∃ a ∈ s, (a, a) = (a₁, a₂)<GOAL>(a₁, a₂).1 ∈ s ∧ (a₁, a₂).1 = (a₁, a₂).2