ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>f g : α → ℝ≥0∞<VAR>ι : Type u_4<VAR>a : ι → ℝ≥0∞<VAR>tsum_ne_top : ∑' (i : ι), a i ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε_ne_zero : ε ≠ 0<VAR>h : ¬{i | ε ≤ a i}.Finite<GOAL>False
<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>f g : α → ℝ≥0∞<VAR>ι : Type u_4<VAR>a : ι → ℝ≥0∞<VAR>tsum_ne_top : ∑' (i : ι), a i ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε_ne_zero : ε ≠ 0<VAR>h : ¬{i | ε ≤ a i}.Finite<VAR>this : Infinite ↑{i | ε ≤ a i}<GOAL>False
<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>f g : α → ℝ≥0∞<VAR>ι : Type u_4<VAR>a : ι → ℝ≥0∞<VAR>tsum_ne_top : ∑' (i : ι), a i ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε_ne_zero : ε ≠ 0<VAR>h : ¬{i | ε ≤ a i}.Finite<VAR>this : Infinite ↑{i | ε ≤ a i}<GOAL>⊤ ≤ ∑' (i : ι), a i
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : Semiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>I : Ideal C(X, R)<VAR>x : X<GOAL>x ∉ setOfIdeal I ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → f x = 0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>hK : (H.subgroupOf K).Normal<VAR>HK : H ≤ K<VAR>x : G<VAR>hx : x ∈ K<VAR>y : G<VAR>yH : x * y * x⁻¹ ∈ H<GOAL>y ∈ H
<VAR>μ : YoungDiagram<GOAL>μ.rowLens.length = μ.colLen 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a b x : α<VAR>P : Set α → Prop<VAR>hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s<GOAL>s ∈ maximals (fun x x_1 => x ⊆ x_1) {t | P t} ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a b x : α<VAR>P : Set α → Prop<VAR>hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s<GOAL>P s → ((∀ ⦃y : Set α⦄, P y → s ⊆ y → s = y) ↔ ∀ x ∉ s, ¬P (insert x s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t✝ : Set α<VAR>a b x✝¹ : α<VAR>P : Set α → Prop<VAR>hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s<VAR>x✝ : P s<VAR>h : ∀ x ∉ s, ¬P (insert x s)<VAR>t : Set α<VAR>ht : P t<VAR>hst : s ⊆ t<VAR>x : α<VAR>hxt : x ∈ t<GOAL>x ∈ s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝¹ : R →+* S<VAR>f✝ : R →+* B<VAR>f : R →+* S<VAR>x y : S<VAR>hx : f.IsIntegralElem x<VAR>hy : f.IsIntegralElem y<GOAL>f.IsIntegralElem (x - y)
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>HasFTaylorSeriesUpTo ⊤ f p ↔ (∀ (x : E), (p x 0).uncurry0 = f x) ∧ ∀ (m : ℕ) (x : E), HasFDerivAt (fun y => p y m) (p x m.succ).curryLeft x
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁶ : LinearOrder ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : SecondCountableTopology ι<VAR>inst✝¹ : BorelSpace ι<VAR>inst✝ : TopologicalSpace β<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>h : ProgMeasurable f u<VAR>hτ : IsStoppingTime f τ<VAR>n : ι<VAR>hτ_le : ∀ (ω : Ω), τ ω ≤ n<GOAL>StronglyMeasurable (stoppedValue u τ)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁶ : LinearOrder ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : SecondCountableTopology ι<VAR>inst✝¹ : BorelSpace ι<VAR>inst✝ : TopologicalSpace β<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>h : ProgMeasurable f u<VAR>hτ : IsStoppingTime f τ<VAR>n : ι<VAR>hτ_le : ∀ (ω : Ω), τ ω ≤ n<VAR>this : stoppedValue u τ = (fun p => u (↑p.1) p.2) ∘ fun ω => (⟨τ ω, ⋯⟩, ω)<GOAL>StronglyMeasurable (stoppedValue u τ)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁶ : LinearOrder ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : SecondCountableTopology ι<VAR>inst✝¹ : BorelSpace ι<VAR>inst✝ : TopologicalSpace β<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>h : ProgMeasurable f u<VAR>hτ : IsStoppingTime f τ<VAR>n : ι<VAR>hτ_le : ∀ (ω : Ω), τ ω ≤ n<VAR>this : stoppedValue u τ = (fun p => u (↑p.1) p.2) ∘ fun ω => (⟨τ ω, ⋯⟩, ω)<GOAL>StronglyMeasurable ((fun p => u (↑p.1) p.2) ∘ fun ω => (⟨τ ω, ⋯⟩, ω))
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁶ : LinearOrder ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : SecondCountableTopology ι<VAR>inst✝¹ : BorelSpace ι<VAR>inst✝ : TopologicalSpace β<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>h : ProgMeasurable f u<VAR>hτ : IsStoppingTime f τ<VAR>n : ι<VAR>hτ_le : ∀ (ω : Ω), τ ω ≤ n<VAR>this : stoppedValue u τ = (fun p => u (↑p.1) p.2) ∘ fun ω => (⟨τ ω, ⋯⟩, ω)<GOAL>Measurable fun ω => (⟨τ ω, ⋯⟩, ω)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>x : α<GOAL>(dirac x).prod ν = map (Prod.mk x) ν
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>x : α<GOAL>(sum fun p => (dirac x).prod (sFiniteSeq ν p)) = sum fun i => map (Prod.mk x) (sFiniteSeq ν i)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>x : α<VAR>i : ℕ<GOAL>(dirac x).prod (sFiniteSeq ν i) = map (Prod.mk x) (sFiniteSeq ν i)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>x : α<VAR>i : ℕ<VAR>s : Set α<VAR>t : Set β<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>(map (Prod.mk x) (sFiniteSeq ν i)) (s ×ˢ t) = (dirac x) s * (sFiniteSeq ν i) t
<VAR>n : ℕ<VAR>hn : 2 ≤ n<GOAL>StrictConvexOn ℝ (Ici 0) fun x => x ^ n
<VAR>n : ℕ<VAR>hn : 2 ≤ n<GOAL>StrictMonoOn (deriv fun x => x ^ n) (interior (Ici 0))
<VAR>n : ℕ<VAR>hn : 2 ≤ n<GOAL>StrictMonoOn (fun x => ↑n * x ^ (n - 1)) (Ioi 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : SMulWithZero α β<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : PosSMulStrictMono α β<VAR>inst✝ : SMulPosStrictMono α β<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<VAR>h₂ : 0 < a₂<VAR>h₁ : 0 < b₁<VAR>h : a₁ • b₁ = a₂ • b₂<GOAL>a₁ = a₂ ∧ b₁ = b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : SMulWithZero α β<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : PosSMulStrictMono α β<VAR>inst✝ : SMulPosStrictMono α β<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<VAR>h₂ : 0 < a₂<VAR>h₁ : 0 < b₁<VAR>h : a₁ • b₁ = a₂ • b₂<GOAL>¬a₁ < a₂ ∧ ¬b₁ < b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : SMulWithZero α β<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : PosSMulStrictMono α β<VAR>inst✝ : SMulPosStrictMono α β<VAR>ha✝ : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<VAR>h₂ : 0 < a₂<VAR>h₁ : 0 < b₁<VAR>h : a₁ • b₁ = a₂ • b₂<VAR>ha : a₁ < a₂<GOAL>a₁ • b₁ < a₂ • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : SMulWithZero α β<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : PosSMulStrictMono α β<VAR>inst✝ : SMulPosStrictMono α β<VAR>ha : a₁ ≤ a₂<VAR>hb✝ : b₁ ≤ b₂<VAR>h₂ : 0 < a₂<VAR>h₁ : 0 < b₁<VAR>h : a₁ • b₁ = a₂ • b₂<VAR>hb : b₁ < b₂<GOAL>a₁ • b₁ < a₂ • b₂
<VAR>X Y B : LightProfinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>pullback.fst f g = ((pullback.isLimit f g).conePointUniqueUpToIso (limit.isLimit (cospan f g))).hom ≫ Limits.pullback.fst f g
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a} = ⊤
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>⊤ ≤ AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a}
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>AddSubmonoid.closure (⇑(toFinsuppIso R).symm.toAddEquiv '' {f | ∃ a b, f = Finsupp.single a b}) ≤ AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a}
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>{f | ∃ a b, f = Finsupp.single a b} ⊆ ⇑(toFinsuppIso R).symm.toAddEquiv ⁻¹' {p | ∃ n a, p = (monomial n) a}
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>a : R<GOAL>Finsupp.single n a ∈ ⇑(toFinsuppIso R).symm.toAddEquiv ⁻¹' {p | ∃ n a, p = (monomial n) a}
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>β : Sort u_1<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>e : F ≅ G<VAR>hobj : ∀ (X : C), F.obj X = G.obj X<VAR>happ : ∀ (X : C), e.hom.app X = eqToHom ⋯<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
<VAR>α : Type u_1<VAR>R I J X Y : Set α<VAR>N : Matroid α<VAR>h : N <r N<GOAL>False
<VAR>α : Type u_1<VAR>R I J X Y : Set α<VAR>N : Matroid α<VAR>h : { toMatroid := N } < { toMatroid := N }<GOAL>False
<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'<VAR>I₁ I₂ : LieIdeal R L<VAR>h : I₁ ≤ I₂<GOAL>map f I₁ ≤ map f I₂
<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'<VAR>I₁ I₂ : LieIdeal R L<VAR>h : ∀ ⦃x : L⦄, x ∈ I₁ → x ∈ I₂<GOAL>map f I₁ ≤ map f I₂
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>x : E<GOAL>x ∈ ⇑p ⁻¹' Metric.closedBall 0 r ↔ x ∈ {x | p x ≤ r}
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>a : α<GOAL>round (a - 1) = round a - 1
<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 : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<GOAL>IsZero T.obj₃ ↔ T.mor₂ = 0 ∧ T.mor₃ = 0
<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 : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<GOAL>T.rotate.mor₁ = 0 ∧ T.rotate.mor₂ = 0 ↔ T.mor₂ = 0 ∧ T.mor₃ = 0
<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 : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<GOAL>T.mor₂ = 0 ∧ T.mor₃ = 0 ↔ T.mor₂ = 0 ∧ T.mor₃ = 0
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk u w<GOAL>(p.reverseAux q).length = p.length + q.length
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>F : Filter α<GOAL>(map f F).NeBot ↔ F.NeBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<GOAL>s.encard + sᶜ.encard = univ.encard
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>inst✝ : Fintype ι<VAR>v : OrthonormalBasis (Fin 2) ℝ F<VAR>f : F ≃ₗᵢ[ℝ] F'<GOAL>isometryOfOrthonormal (v.map f) = (isometryOfOrthonormal v).trans f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>inst✝ : Fintype ι<VAR>v : OrthonormalBasis (Fin 2) ℝ F<VAR>f : F ≃ₗᵢ[ℝ] F'<GOAL>orthonormalBasisOneI.repr.trans (v.repr.symm.trans f) = (orthonormalBasisOneI.repr.trans v.repr.symm).trans f
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<GOAL>lineDeriv 𝕜 f x (-v) = -lineDeriv 𝕜 f x v
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α β : TypeVec.{u} n<VAR>g : α ⟹ β<VAR>a : P.mp.A<VAR>f : P.mp.B a ⟹ α<GOAL>dest P (g <$$> ⟨a, f⟩) = (g ::: fun x => g <$$> x) <$$> dest P ⟨a, f⟩
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α β : TypeVec.{u} n<VAR>g : α ⟹ β<VAR>a : P.mp.A<VAR>f : P.mp.B a ⟹ α<GOAL>dest P ⟨a, g ⊚ f⟩ = (g ::: fun x => g <$$> x) <$$> dest P ⟨a, f⟩
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α β : TypeVec.{u} n<VAR>g : α ⟹ β<VAR>a : P.mp.A<VAR>f : P.mp.B a ⟹ α<GOAL>dest P ⟨a, g ⊚ f⟩ = ⟨(PFunctor.M.dest ⟨a, f⟩.fst).fst, splitFun (g ⊚ pathDestLeft P ⋯ ⟨a, f⟩.snd) ((fun x => g <$$> x) ∘ fun x => ⟨(PFunctor.M.dest ⟨a, f⟩.fst).snd x, pathDestRight P ⋯ ⟨a, f⟩.snd x⟩)⟩
<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>g : F → G<VAR>g' : F →L[𝕜] G<VAR>L' : Filter F<VAR>hg : HasFDerivAtFilter g g' (f x) L'<VAR>hf : HasFDerivAtFilter f f' x L<VAR>hL : Tendsto f L L'<GOAL>HasFDerivAtFilter (g ∘ f) (g'.comp f') x L
<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>g : F → G<VAR>g' : F →L[𝕜] G<VAR>L' : Filter F<VAR>hg : HasFDerivAtFilter g g' (f x) L'<VAR>hf : HasFDerivAtFilter f f' x L<VAR>hL : Tendsto f L L'<VAR>eq₁ : (fun x' => g' (f x' - f x - f' (x' - x))) =o[L] fun x' => x' - x := IsBigO.trans_isLittleO (isBigO_comp g' (fun x' => f x' - f x - f' (x' - x)) L) hf.isLittleO<GOAL>HasFDerivAtFilter (g ∘ f) (g'.comp f') x L
<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>g : F → G<VAR>g' : F →L[𝕜] G<VAR>L' : Filter F<VAR>hg : HasFDerivAtFilter g g' (f x) L'<VAR>hf : HasFDerivAtFilter f f' x L<VAR>hL : Tendsto f L L'<VAR>eq₁ : (fun x' => g' (f x' - f x - f' (x' - x))) =o[L] fun x' => x' - x := IsBigO.trans_isLittleO (isBigO_comp g' (fun x' => f x' - f x - f' (x' - x)) L) hf.isLittleO<VAR>eq₂ : ((fun x' => g x' - g (f x) - g' (x' - f x)) ∘ f) =o[L] fun x' => x' - x := IsLittleO.trans_isBigO (IsLittleO.comp_tendsto hg.isLittleO hL) (isBigO_sub hf)<GOAL>HasFDerivAtFilter (g ∘ f) (g'.comp f') x L
<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>g : F → G<VAR>g' : F →L[𝕜] G<VAR>L' : Filter F<VAR>hg : HasFDerivAtFilter g g' (f x) L'<VAR>hf : HasFDerivAtFilter f f' x L<VAR>hL : Tendsto f L L'<VAR>eq₁ : (fun x' => g' (f x' - f x - f' (x' - x))) =o[L] fun x' => x' - x := IsBigO.trans_isLittleO (isBigO_comp g' (fun x' => f x' - f x - f' (x' - x)) L) hf.isLittleO<VAR>eq₂ : ((fun x' => g x' - g (f x) - g' (x' - f x)) ∘ f) =o[L] fun x' => x' - x := IsLittleO.trans_isBigO (IsLittleO.comp_tendsto hg.isLittleO hL) (isBigO_sub hf)<VAR>x' : E<GOAL>g' (f x' - f x - f' (x' - x)) = g' (f x' - f x) - (g'.comp f') (x' - x)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<GOAL>spanNorm R ⊤ = ⊤
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<GOAL>span {(Algebra.norm R) 1} = ⊤
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>D : Iᵒᵖ ⥤ C<VAR>F : C ⥤ Type u₂<VAR>inst✝¹ : HasColimit (D.rightOp ⋙ coyoneda)<VAR>inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))<VAR>f : colimit (D.rightOp ⋙ coyoneda) ⟶ F<VAR>i : I<GOAL>((colimitCoyonedaHomIsoLimit D F).hom ≫ limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) (op i)) f = { down := f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op i)))) }
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>D : Iᵒᵖ ⥤ C<VAR>F : C ⥤ Type u₂<VAR>inst✝¹ : HasColimit (D.rightOp ⋙ coyoneda)<VAR>inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))<VAR>f : colimit (D.rightOp ⋙ coyoneda) ⟶ F<VAR>i : I<GOAL>((colimitHomIsoLimitYoneda (D.rightOp ⋙ coyoneda) F).hom ≫ limit.π ((D.rightOp ⋙ coyoneda).op ⋙ yoneda.obj F) (op i) ≫ (isoWhiskerLeft (D ⋙ Prod.sectl C F) (coyonedaLemma C)).hom.app (op i)) f = { down := f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op i)))) }
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>D : Iᵒᵖ ⥤ C<VAR>F : C ⥤ Type u₂<VAR>inst✝¹ : HasColimit (D.rightOp ⋙ coyoneda)<VAR>inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))<VAR>f : colimit (D.rightOp ⋙ coyoneda) ⟶ F<VAR>i : I<GOAL>((coyoneda.map (colimit.ι (D.rightOp ⋙ coyoneda) i).op).app F ≫ (isoWhiskerLeft (D ⋙ Prod.sectl C F) (coyonedaLemma C)).hom.app (op i)) f = { down := f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op i)))) }
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>D : Iᵒᵖ ⥤ C<VAR>F : C ⥤ Type u₂<VAR>inst✝¹ : HasColimit (D.rightOp ⋙ coyoneda)<VAR>inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))<VAR>f : colimit (D.rightOp ⋙ coyoneda) ⟶ F<VAR>i : I<GOAL>Equiv.ulift.symm (coyonedaEquiv (colimit.ι (D.rightOp ⋙ coyoneda) i ≫ f)) = { down := f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op i)))) }
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>D : Iᵒᵖ ⥤ C<VAR>F : C ⥤ Type u₂<VAR>inst✝¹ : HasColimit (D.rightOp ⋙ coyoneda)<VAR>inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))<VAR>f : colimit (D.rightOp ⋙ coyoneda) ⟶ F<VAR>i : I<GOAL>Equiv.ulift.symm (f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op i))))) = { down := f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op i)))) }
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>hp0 : 0 < p<VAR>f : α → ℝ≥0∞<VAR>a : α<GOAL>funMulInvSnorm f p μ a ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>hp0 : 0 < p<VAR>f : α → ℝ≥0∞<VAR>a : α<GOAL>f a ^ p * ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>hp0 : 0 < p<VAR>f : α → ℝ≥0∞<VAR>a : α<GOAL>((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
<VAR>S : Type u_1<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>I J : Ideal S<VAR>coprime : IsCoprime I J<GOAL>cardQuot (I * J) = cardQuot I * cardQuot J
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<GOAL>s.SSameSide x y ↔ s.SSameSide y x