ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid α<VAR>s t : Finset α<VAR>a : α<VAR>m n : ℕ<VAR>hst : s ⊆ t<GOAL>s ^ 0 ⊆ t ^ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid α<VAR>s t : Finset α<VAR>a : α<VAR>m n✝ : ℕ<VAR>hst : s ⊆ t<VAR>n : ℕ<GOAL>s ^ (n + 1) ⊆ t ^ (n + 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid α<VAR>s t : Finset α<VAR>a : α<VAR>m n✝ : ℕ<VAR>hst : s ⊆ t<VAR>n : ℕ<GOAL>s ^ n * s ⊆ t ^ (n + 1)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>refl : ∀ (x : α), R x x<VAR>symm : ∀ {x y : α}, R x y → R y x<VAR>trans : ∀ {x y z : α}, R x y → R y z → R x z<GOAL>∀ {x y : Computation α}, LiftRel R x y → LiftRel R y x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>refl : ∀ (x : α), R x x<VAR>symm : ∀ {x y : α}, R x y → R y x<VAR>trans : ∀ {x y z : α}, R x y → R y z → R x z<GOAL>Symmetric R
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>refl : ∀ (x : α), R x x<VAR>symm : ∀ {x y : α}, R x y → R y x<VAR>trans : ∀ {x y z : α}, R x y → R y z → R x z<GOAL>∀ {x y z : Computation α}, LiftRel R x y → LiftRel R y z → LiftRel R x z
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>refl : ∀ (x : α), R x x<VAR>symm : ∀ {x y : α}, R x y → R y x<VAR>trans : ∀ {x y z : α}, R x y → R y z → R x z<GOAL>Transitive R
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a r : ℝ<GOAL>volume (Metric.closedBall a r) = ofReal (2 * r)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle y (y - x) = ↑(Real.arcsin (‖x‖ / ‖y - x‖))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle y (y - x)).sign = 1<GOAL>o.oangle y (y - x) = ↑(Real.arcsin (‖x‖ / ‖y - x‖))
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝ : MulZeroClass M₀<VAR>f g : ι → M₀<VAR>x : ι<VAR>hfg : x ∈ support fun x => f x * g x<VAR>hf : f x = 0<GOAL>(fun x => f x * g x) x = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{?u.101289, u_1} C<VAR>inst✝⁶ : Category.{?u.101293, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>φ₃ : K₃ ⟶ L₃<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>comm : φ₁ ≫ b = a ≫ φ₂<VAR>a' : K₂ ⟶ K₃<VAR>b' : L₂ ⟶ L₃<VAR>comm' : φ₂ ≫ b' = a' ≫ φ₃<GOAL>φ₁ ≫ b ≫ b' = (a ≫ a') ≫ φ₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.101293, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>φ₃ : K₃ ⟶ L₃<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>comm : φ₁ ≫ b = a ≫ φ₂<VAR>a' : K₂ ⟶ K₃<VAR>b' : L₂ ⟶ L₃<VAR>comm' : φ₂ ≫ b' = a' ≫ φ₃<VAR>n : ℤ<GOAL>(map φ₁ φ₃ (a ≫ a') (b ≫ b') ⋯).f n = (map φ₁ φ₂ a b comm ≫ map φ₂ φ₃ a' b' comm').f n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K✝ L L' M : Set V<VAR>K : (Finset V)ᵒᵖ<VAR>C : G.componentComplFunctor.obj K<GOAL>(ComponentCompl.supp C).Infinite ↔ C ∈ G.componentComplFunctor.eventualRange K
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K✝ L L' M : Set V<VAR>K : (Finset V)ᵒᵖ<VAR>C : G.componentComplFunctor.obj K<GOAL>(∀ (L : Finset V) (h : Opposite.unop K ⊆ L), ∃ D, ComponentCompl.hom h D = C) ↔ ∀ (i : (Finset V)ᵒᵖ) (i_1 : i ⟶ K), ∃ y, ComponentCompl.hom ⋯ y = C
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>x y : R<VAR>x✝ : ∃ c, ↑c * x = ↑c * y<VAR>c : ↥M<VAR>h : (algebraMap R S) (↑c * x) = (algebraMap R S) (↑c * y)<GOAL>(algebraMap R S) x = (algebraMap R S) y
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>x y : R<VAR>x✝ : ∃ c, ↑c * x = ↑c * y<VAR>c : ↥M<VAR>h : (algebraMap R S) ↑c * (algebraMap R S) x = (algebraMap R S) ↑c * (algebraMap R S) y<GOAL>(algebraMap R S) x = (algebraMap R S) y
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>A : PointedGaloisObject F<VAR>σ : Aut A.obj<VAR>this : ∀ (i : PointedGaloisObject F), Finite ((autGaloisSystem F ⋙ forget Grp).obj i)<GOAL>∃ a, (π F A) a = σ
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>κ : Type u_1<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>h : κ → ι<VAR>hh : Function.Injective h<VAR>k : κ<VAR>x : β (h k)<VAR>i : κ<GOAL>(comapDomain h hh (single (h k) x)) i = (single k x) i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>κ : Type u_1<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>h : κ → ι<VAR>hh : Function.Injective h<VAR>k : κ<VAR>x : β (h k)<VAR>i : κ<GOAL>(single (h k) x) (h i) = (single k x) i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>κ : Type u_1<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>h : κ → ι<VAR>hh : Function.Injective h<VAR>i : κ<VAR>x : β (h i)<GOAL>(single (h i) x) (h i) = (single i x) i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>κ : Type u_1<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>h : κ → ι<VAR>hh : Function.Injective h<VAR>k : κ<VAR>x : β (h k)<VAR>i : κ<VAR>hik : i ≠ k<GOAL>(single (h k) x) (h i) = (single k x) i
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁹ : Category.{u_3, u_1} C<VAR>inst✝⁸ : Category.{u_4, u_2} D<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>inst✝⁶ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁵ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝⁴ : F.PreservesZeroMorphisms<VAR>inst✝³ : S₁.HasRightHomology<VAR>inst✝² : S₂.HasRightHomology<VAR>inst✝¹ : F.PreservesRightHomologyOf S₁<VAR>inst✝ : F.PreservesRightHomologyOf S₂<GOAL>rightHomologyMap' (F.mapShortComplex.map φ) (F.mapShortComplex.obj S₁).rightHomologyData (F.mapShortComplex.obj S₂).rightHomologyData ≫ rightHomologyMap' (𝟙 (S₂.map F)) (S₂.map F).rightHomologyData (S₂.rightHomologyData.map F) = rightHomologyMap' (𝟙 (S₁.map F)) (S₁.map F).rightHomologyData (S₁.rightHomologyData.map F) ≫ F.map (rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>f : ι → ℝ≥0∞<VAR>g : ι' → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>h : ∀ (i : ι) (j : ι'), f i + g j ≤ a<GOAL>iSup f + iSup g ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>f : ι → ℝ≥0∞<VAR>g : ι' → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>h : ∀ (i : ι) (j : ι'), f i + g j ≤ a<GOAL>⨆ b, ⨆ b_1, f b + g b_1 ≤ a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : ClosedIicTopology α<VAR>inst✝ : TopologicalSpace β<VAR>a b c : α<VAR>f : α → β<VAR>h : a < b<GOAL>ContinuousWithinAt f (Icc a b) b ↔ ContinuousWithinAt f (Iic b) b
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>M₄ : Type u_7<VAR>N : Type u_8<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₁<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid M₄<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Module R N<VAR>Q₁ : QuadraticMap R M₁ N<VAR>Q₂ : QuadraticMap R M₂ N<VAR>Q₃ : QuadraticMap R M₃ N<VAR>Q₄ : QuadraticMap R M₄ N<VAR>g : Q₂ →qᵢ Q₃<VAR>f : Q₁ →qᵢ Q₂<VAR>x : M₁<GOAL>Q₃ ({ toFun := fun x => g (f x), map_add' := ⋯, map_smul' := ⋯ }.toFun x) = Q₁ x
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g : α → F β<VAR>h : β → G γ<VAR>f : β → γ<VAR>x✝ : t β<VAR>η : ApplicativeTransformation F G<VAR>x : t (F α)<GOAL>(fun {α} => η.app α) (sequence x) = sequence ((fun {α} => η.app α) <$> x)
<VAR>ι : Type u<VAR>f✝ : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>f : ι → Ordinal.{max u u_1} → Ordinal.{max u u_1}<VAR>o : Ordinal.{max u_1 u}<GOAL>derivFamily f o < derivFamily f (succ o)
<VAR>ι : Type u<VAR>f✝ : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>f : ι → Ordinal.{max u u_1} → Ordinal.{max u u_1}<VAR>o : Ordinal.{max u_1 u}<GOAL>succ (derivFamily f o) ≤ nfpFamily f (succ (derivFamily f o))
<VAR>ι : Type u<VAR>f✝ : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>f : ι → Ordinal.{max u u_1} → Ordinal.{max u u_1}<VAR>o : Ordinal.{max u_1 u}<VAR>l : o.IsLimit<VAR>a : Ordinal.{max u_1 u}<GOAL>derivFamily f o ≤ a ↔ ∀ b < o, derivFamily f b ≤ a
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q : ℝ≥0<VAR>p : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>ENNReal.ofReal p < ↑n ↔ p < ↑n
<VAR>𝕜 : Type u_1<VAR>inst✝ : RCLike 𝕜<GOAL>Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>inst✝ : RCLike 𝕜<VAR>x✝ : ℕ<GOAL>(↑x✝)⁻¹ = (⇑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) x✝
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y ≠ 0<VAR>hxy : ‖x + y‖ ^ 2 ≠ 0<GOAL>angle x (x + y) = Real.arcsin (‖y‖ / ‖x + y‖)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y ≠ 0<VAR>hxy : ‖x + y‖ ^ 2 ≠ 0<GOAL>Real.arcsin √((‖x + y‖ ^ 2 - ‖x‖ ^ 2) / ‖x + y‖ ^ 2) = Real.arcsin (‖y‖ / ‖x + y‖)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y ≠ 0<VAR>hxy : ‖x + y‖ ^ 2 ≠ 0<GOAL>Real.arcsin √((‖x + y‖ * ‖x + y‖ - ‖x‖ ^ 2) / ‖x + y‖ ^ 2) = Real.arcsin (‖y‖ / ‖x + y‖)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>p : Finset α<GOAL>p ∈ filter (fun p => ¬p.card = s.card / P.parts.card + 1) P.parts ↔ p ∈ filter (fun p => p.card = s.card / P.parts.card) P.parts
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>p : Finset α<GOAL>p ∈ P.parts → (¬p.card = s.card / P.parts.card + 1 ↔ p.card = s.card / P.parts.card)
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p : P<GOAL>lineCount L p = order P L + 1
<VAR>J : Type w<VAR>K✝ : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>K : Type<VAR>inst✝¹ : Finite K<VAR>inst✝ : HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<VAR>j : Subtype pᶜ<VAR>k : Subtype p<GOAL>biproduct.ι (Subtype.restrict p f) k ≫ (biproduct.fromSubtype f p ≫ biproduct.toSubtype f pᶜ) ≫ biproduct.π (Subtype.restrict pᶜ f) j = biproduct.ι (Subtype.restrict p f) k ≫ 0 ≫ biproduct.π (Subtype.restrict pᶜ f) j
<VAR>J : Type w<VAR>K✝ : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>K : Type<VAR>inst✝¹ : Finite K<VAR>inst✝ : HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<VAR>j : Subtype pᶜ<VAR>k : Subtype p<GOAL>(if h : (p ↑k)ᶜ then biproduct.ι (Subtype.restrict pᶜ f) ⟨↑k, ⋯⟩ else 0) ≫ biproduct.π (Subtype.restrict pᶜ f) j = 0
<VAR>J : Type w<VAR>K✝ : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>K : Type<VAR>inst✝¹ : Finite K<VAR>inst✝ : HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<VAR>j : Subtype pᶜ<VAR>k : Subtype p<GOAL>0 ≫ biproduct.π (Subtype.restrict pᶜ f) j = 0
<VAR>J : Type w<VAR>K✝ : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>K : Type<VAR>inst✝¹ : Finite K<VAR>inst✝ : HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<VAR>j : Subtype pᶜ<VAR>k : Subtype p<GOAL>¬(p ↑k)ᶜ
<VAR>J : Type w<VAR>K✝ : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>K : Type<VAR>inst✝¹ : Finite K<VAR>inst✝ : HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<VAR>W : C<VAR>g' : ⨁ f ⟶ W<VAR>w : biproduct.fromSubtype f p ≫ g' = 0<VAR>j : K<GOAL>biproduct.ι f j ≫ biproduct.toSubtype f pᶜ ≫ (fun {W} g x => biproduct.fromSubtype f pᶜ ≫ g) g' w = biproduct.ι f j ≫ g'
<VAR>J : Type w<VAR>K✝ : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>K : Type<VAR>inst✝¹ : Finite K<VAR>inst✝ : HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<VAR>W : C<VAR>g' : ⨁ f ⟶ W<VAR>w : biproduct.fromSubtype f p ≫ g' = 0<VAR>j : K<GOAL>(if (p j)ᶜ then 𝟙 (f j) else 0) ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>hf : ContDiffOn 𝕜 (↑n) f s<VAR>hg : ContDiffOn 𝕜 (↑n) g s<GOAL>iteratedDerivWithin n (f - g) s x = iteratedDerivWithin n f s x - iteratedDerivWithin n g s x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a \ b = b \ a ↔ a = b
<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, 1 ≤ f i<GOAL>1 ≤ ∏ i ∈ s, 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>m₁ : α → γ<VAR>m₂ : β → δ<GOAL>∀ (x : γ × δ), x ∈ (m₁ '' s) ×ˢ (m₂ '' t) ↔ x ∈ (fun p => (m₁ p.1, m₂ p.2)) '' s ×ˢ t
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : Semiring S<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₁<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>inst✝⁵ : AddCommMonoid N₁<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : AddCommMonoid N₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module S M₃<VAR>σ : R →+* S<VAR>fₗ gₗ : M →ₗ[R] M₂<VAR>f✝ g✝ : M →ₛₗ[σ] M₃<VAR>f g : R →ₛₗ[σ] M₃<VAR>h : f 1 = g 1<VAR>x : R<GOAL>f x = g x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>c : ℝ<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>setToSimpleFunc T (c • f) = ∑ x ∈ f.range, (T (↑f ⁻¹' {x})) (c • x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>c : ℝ<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>c • 0 = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>c : ℝ<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>b : E<VAR>x✝ : b ∈ f.range<GOAL>(T (↑f ⁻¹' {b})) (c • b) = c • (T (↑f ⁻¹' {b})) b
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>c : ℝ<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>∑ x ∈ f.range, c • (T (↑f ⁻¹' {x})) x = c • setToSimpleFunc T f
<VAR>b n m : ℕ<VAR>h : n ≤ m<GOAL>clog b n ≤ clog b m
<VAR>b n m : ℕ<VAR>h : n ≤ m<VAR>hb : b ≤ 1<GOAL>clog b n ≤ clog b m
<VAR>b n m : ℕ<VAR>h : n ≤ m<VAR>hb : 1 < b<GOAL>clog b n ≤ clog b m
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ L : List α<VAR>i : ℕ<VAR>h : i < L.attach.length<GOAL>↑L.attach[i] = (map Subtype.val L.attach)[i]
<VAR>a b : Ordinal.{u_1}<VAR>h : a < b<GOAL>a.toPGame ⧏ b.toPGame
<VAR>a b : Ordinal.{u_1}<VAR>h : a < b<GOAL>a.toPGame = b.toPGame.moveLeft (toLeftMovesToPGame ⟨a, h⟩)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>χ₁ χ₂ : L → R<VAR>h : χ₁ ≠ χ₂<GOAL>Disjoint (weightSpace M χ₁) (weightSpace M χ₂)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>χ₁ χ₂ : L → R<VAR>h : χ₁ ≠ χ₂<VAR>x : L<VAR>hx : χ₁ x ≠ χ₂ x<GOAL>Disjoint (weightSpace M χ₁) (weightSpace M χ₂)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → ℂ<VAR>s : ℂ<VAR>hf : MellinConvergent f s<VAR>a : ℂ<GOAL>MellinConvergent (fun t => f t / a) s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : NormalSpace X<VAR>s t : Set X<VAR>hs : IsClosed s<VAR>ht : IsOpen t<VAR>hst : s ⊆ t<GOAL>∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : NormalSpace X<VAR>s t : Set X<VAR>hs : IsClosed s<VAR>ht : IsOpen t<VAR>hst : s ⊆ t<VAR>this : Disjoint s tᶜ<GOAL>∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : NormalSpace X<VAR>s t : Set X<VAR>hs : IsClosed s<VAR>ht : IsOpen t<VAR>hst : s ⊆ t<VAR>this : Disjoint s tᶜ<VAR>s' t' : Set X<VAR>hs' : IsOpen s'<VAR>ht' : IsOpen t'<VAR>hss' : s ⊆ s'<VAR>htt' : tᶜ ⊆ t'<VAR>hs't' : Disjoint s' t'<GOAL>∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : NormalSpace X<VAR>s t : Set X<VAR>hs : IsClosed s<VAR>ht : IsOpen t<VAR>hst : s ⊆ t<VAR>this : Disjoint s tᶜ<VAR>s' t' : Set X<VAR>hs' : IsOpen s'<VAR>ht' : IsOpen t'<VAR>hss' : s ⊆ s'<VAR>htt' : tᶜ ⊆ t'<VAR>hs't' : Disjoint s' t'<GOAL>s' ⊆ t'ᶜ
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>T : Type u_2<VAR>inst✝ : Category.{?u.78, u_2} T<VAR>C : HomologicalComplex (T ⥤ V) c<VAR>t : T<VAR>i j k : ι<VAR>x✝¹ : c.Rel i j<VAR>x✝ : c.Rel j k<GOAL>(fun i j => (C.d i j).app t) i j ≫ (fun i j => (C.d i j).app t) j k = 0
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>T : Type u_2<VAR>inst✝ : Category.{?u.78, u_2} T<VAR>C : HomologicalComplex (T ⥤ V) c<VAR>t : T<VAR>i j k : ι<VAR>x✝¹ : c.Rel i j<VAR>x✝ : c.Rel j k<VAR>this : C.d i j ≫ C.d j k = 0<GOAL>(fun i j => (C.d i j).app t) i j ≫ (fun i j => (C.d i j).app t) j k = 0
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>T : Type u_2<VAR>inst✝ : Category.{?u.78, u_2} T<VAR>C : HomologicalComplex (T ⥤ V) c<VAR>t : T<VAR>i j k : ι<VAR>x✝¹ : c.Rel i j<VAR>x✝ : c.Rel j k<VAR>this : ∀ (a : T), (C.d i j ≫ C.d j k).app a = NatTrans.app 0 a<GOAL>(fun i j => (C.d i j).app t) i j ≫ (fun i j => (C.d i j).app t) j k = 0
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>T : Type u_2<VAR>inst✝ : Category.{?u.78, u_2} T<VAR>C : HomologicalComplex (T ⥤ V) c<VAR>t : T<VAR>i j : ι<VAR>h : ¬c.Rel i j<GOAL>(fun i j => (C.d i j).app t) i j = 0
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>T : Type u_2<VAR>inst✝ : Category.{?u.78, u_2} T<VAR>C : HomologicalComplex (T ⥤ V) c<VAR>t : T<VAR>i j : ι<VAR>h : ¬c.Rel i j<VAR>this : C.d i j = 0<GOAL>(fun i j => (C.d i j).app t) i j = 0
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>T : Type u_2<VAR>inst✝ : Category.{?u.78, u_2} T<VAR>C : HomologicalComplex (T ⥤ V) c<VAR>t : T<VAR>i j : ι<VAR>h : ¬c.Rel i j<VAR>this : ∀ (a : T), (C.d i j).app a = NatTrans.app 0 a<GOAL>(fun i j => (C.d i j).app t) i j = 0
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>T : Type u_2<VAR>inst✝ : Category.{?u.78, u_2} T<VAR>C : HomologicalComplex (T ⥤ V) c<VAR>t : T<VAR>i : ι<GOAL>(C.X i).map (𝟙 t) = 𝟙 ((C.X i).obj t)
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>T : Type u_2<VAR>inst✝ : Category.{?u.78, u_2} T<VAR>C : HomologicalComplex (T ⥤ V) c<VAR>X✝ Y✝ Z✝ : T<VAR>h₁ : X✝ ⟶ Y✝<VAR>h₂ : Y✝ ⟶ Z✝<VAR>i : ι<GOAL>(C.X i).map (h₁ ≫ h₂) = (C.X i).map h₁ ≫ (C.X i).map h₂
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set X<VAR>t : Set Y<VAR>x : X<VAR>y : Y<GOAL>s ×ˢ t ∈ 𝓝 (x, y) ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y