ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>J : Type w<VAR>inst✝¹ : Category.{w', w} J<VAR>F : J ⥤ C<VAR>inst✝ : PreservesColimit F G<VAR>c₁ c₂ : Cocone F<VAR>t : IsColimit c₁<GOAL>∀ (j : J), (G.mapCocone c₁).ι.app j ≫ G.map (t.desc c₂) = (G.mapCocone c₂).ι.app j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>m : Set (Measure α)<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>m : Set (Measure α)<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<GOAL>OuterMeasure.sInfGen (toOuterMeasure '' m) (t ∩ s) + OuterMeasure.sInfGen (toOuterMeasure '' m) (t \ s) ≤ OuterMeasure.sInfGen (toOuterMeasure '' m) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>m : Set (Measure α)<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<GOAL>∀ ⦃x : Measure α⦄, x ∈ m → ∀ (i : Set α), t ⊆ i → MeasurableSet i → (⨅ μ ∈ toOuterMeasure '' m, μ (t ∩ s)) + ⨅ μ ∈ toOuterMeasure '' m, μ (t \ s) ≤ x i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>m : Set (Measure α)<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>μ : Measure α<VAR>hμ : μ ∈ m<VAR>u : Set α<VAR>htu : t ⊆ u<VAR>_hu : MeasurableSet u<GOAL>(⨅ μ ∈ toOuterMeasure '' m, μ (t ∩ s)) + ⨅ μ ∈ toOuterMeasure '' m, μ (t \ s) ≤ μ u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>m : Set (Measure α)<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>μ : Measure α<VAR>hμ : μ ∈ m<VAR>u : Set α<VAR>htu : t ⊆ u<VAR>_hu : MeasurableSet u<VAR>hm : ∀ {s t : Set α}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ μ t<GOAL>(⨅ μ ∈ toOuterMeasure '' m, μ (t ∩ s)) + ⨅ μ ∈ toOuterMeasure '' m, μ (t \ s) ≤ μ u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>m : Set (Measure α)<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>μ : Measure α<VAR>hμ : μ ∈ m<VAR>u : Set α<VAR>htu : t ⊆ u<VAR>_hu : MeasurableSet u<VAR>hm : ∀ {s t : Set α}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ μ t<GOAL>(⨅ μ ∈ toOuterMeasure '' m, μ (t ∩ s)) + ⨅ μ ∈ toOuterMeasure '' m, μ (t \ s) ≤ μ (u ∩ s) + μ (u \ s)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>p : α → Prop<VAR>x y z : α<VAR>x✝ : f.SameCycle x y<VAR>i : ℤ<VAR>hi : (f ^ i) x = y<GOAL>(f ^ (-i)) y = x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E✝ : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : AddCommGroup E✝<VAR>inst✝¹⁴ : Module 𝕜 E✝<VAR>inst✝¹³ : NormedField 𝕝<VAR>inst✝¹² : Module 𝕝 E✝<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : NormedField 𝕝₂<VAR>inst✝⁷ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁶ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝⁵ : RingHomIsometric τ₁₂<VAR>inst✝⁴ : Nonempty ι<VAR>inst✝³ : Nonempty ι'<VAR>E : Type u_10<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕝 E<VAR>inst✝ : TopologicalSpace F<VAR>q : ι → Seminorm 𝕝₂ F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : ∀ (i : ι), ∃ C, (q i).comp f ≤ C • normSeminorm 𝕝 E<GOAL>Continuous ⇑f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E✝ : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : AddCommGroup E✝<VAR>inst✝¹⁴ : Module 𝕜 E✝<VAR>inst✝¹³ : NormedField 𝕝<VAR>inst✝¹² : Module 𝕝 E✝<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : NormedField 𝕝₂<VAR>inst✝⁷ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁶ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝⁵ : RingHomIsometric τ₁₂<VAR>inst✝⁴ : Nonempty ι<VAR>inst✝³ : Nonempty ι'<VAR>E : Type u_10<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕝 E<VAR>inst✝ : TopologicalSpace F<VAR>q : ι → Seminorm 𝕝₂ F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : IsBounded (fun x => normSeminorm 𝕝 E) q f<GOAL>Continuous ⇑f
<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 S₁ S₂ : ShortComplex C<VAR>hS : S.ShortExact<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : PreservesFiniteLimits F<VAR>inst✝ : PreservesFiniteColimits F<GOAL>(S.map F).ShortExact
<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 S₁ S₂ : ShortComplex C<VAR>hS : S.ShortExact<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : PreservesFiniteLimits F<VAR>inst✝ : PreservesFiniteColimits F<VAR>this : Mono S.f<GOAL>(S.map F).ShortExact
<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 S₁ S₂ : ShortComplex C<VAR>hS : S.ShortExact<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : PreservesFiniteLimits F<VAR>inst✝ : PreservesFiniteColimits F<VAR>this✝ : Mono S.f<VAR>this : Epi S.g<GOAL>(S.map F).ShortExact
<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 S₁ S₂ : ShortComplex C<VAR>hS : S.ShortExact<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : PreservesFiniteLimits F<VAR>inst✝ : PreservesFiniteColimits F<VAR>this✝¹ : Mono S.f<VAR>this✝ : Epi S.g<VAR>this : Mono (F.map S.f)<GOAL>(S.map F).ShortExact
<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 S₁ S₂ : ShortComplex C<VAR>hS : S.ShortExact<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : PreservesFiniteLimits F<VAR>inst✝ : PreservesFiniteColimits F<VAR>this✝² : Mono S.f<VAR>this✝¹ : Epi S.g<VAR>this✝ : Mono (F.map S.f)<VAR>this : Epi (F.map S.g)<GOAL>(S.map F).ShortExact
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>deriv^[2] negMulLog x = -x⁻¹
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>deriv^[2] (fun x => -(x * log x)) x = -x⁻¹
<VAR>x : ℝ<VAR>hx : x ≠ 0<VAR>h : deriv^[2] (fun x => x * log x) x = x⁻¹<GOAL>deriv^[2] (fun x => -(x * log x)) x = -x⁻¹
<VAR>x : ℝ<VAR>hx : x ≠ 0<VAR>h : deriv (deriv fun x => x * log x) x = x⁻¹<GOAL>-deriv (deriv fun y => y * log y) x = -x⁻¹
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemiring α<VAR>m n : Num<GOAL>↑m = ↑n ↔ m = n
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<GOAL>¬s.Subsingleton ↔ s.Nontrivial
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝² : Add α<VAR>inst✝¹ : DivisionMonoid β<VAR>inst✝ : HasDistribNeg β<VAR>hf : Antiperiodic f c<VAR>hg : Antiperiodic g c<GOAL>Periodic (f / g) c
<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✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : SMulPosStrictMono α β<VAR>ha : a < 0<VAR>hb : 0 < b<GOAL>a • b < 0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<GOAL>(H ⊓ K).index ≤ H.index * K.index
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.59011, u_1} C<VAR>inst✝² : Category.{?u.59015, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : HasZeroMorphisms D<VAR>φ : S₁ ⟶ S₂<GOAL>φ.τ₃.op ≫ S₁.g.op = S₂.g.op ≫ φ.τ₂.op
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.59011, u_1} C<VAR>inst✝² : Category.{?u.59015, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : HasZeroMorphisms D<VAR>φ : S₁ ⟶ S₂<GOAL>φ.τ₂.op ≫ S₁.f.op = S₂.f.op ≫ φ.τ₁.op
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>m✝ m' : M<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>g g' : G<VAR>inst✝² : T2Space M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Countable β<VAR>inst✝ : CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 1<VAR>R : M → M → Prop<VAR>m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))<VAR>s₁ s₂ : α<GOAL>R (m (s₁ ⊔ s₂)) (m s₁ * m s₂)
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>m✝ m' : M<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>g g' : G<VAR>inst✝² : T2Space M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Countable β<VAR>inst✝ : CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 1<VAR>R : M → M → Prop<VAR>m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))<VAR>s₁ s₂ : α<GOAL>s₁ ⊔ s₂ = ⨆ b, bif b then s₁ else s₂
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>m✝ m' : M<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>g g' : G<VAR>inst✝² : T2Space M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Countable β<VAR>inst✝ : CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 1<VAR>R : M → M → Prop<VAR>m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))<VAR>s₁ s₂ : α<GOAL>m s₁ * m s₂ = ∏' (b : Bool), m (bif b then s₁ else s₂)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : Module R M✝<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>T : Type u_5<VAR>inst✝⁵ : AddCommGroup T<VAR>inst✝⁴ : Module (AdicCompletion I R) T<VAR>ι : Type u_6<VAR>inst✝³ : DecidableEq ι<VAR>M : ι → Type u_7<VAR>inst✝² : (i : ι) → AddCommGroup (M i)<VAR>inst✝¹ : (i : ι) → Module R (M i)<VAR>inst✝ : Fintype ι<VAR>f : AdicCauchySequence I (⨁ (j : ι), M j)<VAR>n : ℕ<GOAL>↑((sum I M ∘ₗ sumInv I M) ((mk I (⨁ (j : ι), M j)) f)) n = ↑(LinearMap.id ((mk I (⨁ (j : ι), M j)) f)) n
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : Module R M✝<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>T : Type u_5<VAR>inst✝⁵ : AddCommGroup T<VAR>inst✝⁴ : Module (AdicCompletion I R) T<VAR>ι : Type u_6<VAR>inst✝³ : DecidableEq ι<VAR>M : ι → Type u_7<VAR>inst✝² : (i : ι) → AddCommGroup (M i)<VAR>inst✝¹ : (i : ι) → Module R (M i)<VAR>inst✝ : Fintype ι<VAR>f : AdicCauchySequence I (⨁ (j : ι), M j)<VAR>n : ℕ<GOAL>↑((sum I M) ((sumInv I M) ((mk I (⨁ (j : ι), M j)) f))) n = Submodule.Quotient.mk (↑f n)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : Module R M✝<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>T : Type u_5<VAR>inst✝⁵ : AddCommGroup T<VAR>inst✝⁴ : Module (AdicCompletion I R) T<VAR>ι : Type u_6<VAR>inst✝³ : DecidableEq ι<VAR>M : ι → Type u_7<VAR>inst✝² : (i : ι) → AddCommGroup (M i)<VAR>inst✝¹ : (i : ι) → Module R (M i)<VAR>inst✝ : Fintype ι<VAR>f : AdicCauchySequence I (⨁ (j : ι), M j)<VAR>n : ℕ<GOAL>↑((sum I M) (∑ i : ι, (DirectSum.of (fun i => AdicCompletion I (M i)) i) (((sumInv I M) ((mk I (⨁ (j : ι), M j)) f)) i))) n = Submodule.Quotient.mk (↑f n)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : Module R M✝<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>T : Type u_5<VAR>inst✝⁵ : AddCommGroup T<VAR>inst✝⁴ : Module (AdicCompletion I R) T<VAR>ι : Type u_6<VAR>inst✝³ : DecidableEq ι<VAR>M : ι → Type u_7<VAR>inst✝² : (i : ι) → AddCommGroup (M i)<VAR>inst✝¹ : (i : ι) → Module R (M i)<VAR>inst✝ : Fintype ι<VAR>f : AdicCauchySequence I (⨁ (j : ι), M j)<VAR>n : ℕ<GOAL>∑ x : ι, Submodule.Quotient.mk ((lof R ι M x) ((component R ι M x) (↑f n))) = Submodule.Quotient.mk (↑f n)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : Module R M✝<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>T : Type u_5<VAR>inst✝⁵ : AddCommGroup T<VAR>inst✝⁴ : Module (AdicCompletion I R) T<VAR>ι : Type u_6<VAR>inst✝³ : DecidableEq ι<VAR>M : ι → Type u_7<VAR>inst✝² : (i : ι) → AddCommGroup (M i)<VAR>inst✝¹ : (i : ι) → Module R (M i)<VAR>inst✝ : Fintype ι<VAR>f : AdicCauchySequence I (⨁ (j : ι), M j)<VAR>n : ℕ<GOAL>(I ^ n • ⊤).mkQ (∑ x : ι, (lof R ι M x) ((component R ι M x) (↑f n))) = (I ^ n • ⊤).mkQ (↑f n)
<VAR>α β : BoolRing<VAR>e : ↑α ≃+* ↑β<VAR>x✝ : (forget BoolRing).obj α<GOAL>(↑e ≫ ↑e.symm) x✝ = (𝟙 α) x✝
<VAR>α β : BoolRing<VAR>e : ↑α ≃+* ↑β<VAR>x✝ : (forget BoolRing).obj β<GOAL>(↑e.symm ≫ ↑e) x✝ = (𝟙 β) x✝
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r : R[X]<VAR>p : R[ℕ]<GOAL>(C a * { toFinsupp := p }).coeff n = a * { toFinsupp := p }.coeff n
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r : R[X]<VAR>p : R[ℕ]<GOAL>(Finsupp.single 0 a * p) n = a * p n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜' F'<VAR>inst✝ : BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁ : k₁ =O[l] k₂<VAR>h₂ : f' =O[l] g'<GOAL>(fun x => k₁ x • f' x) =O[l] fun x => k₂ x • g' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c c' c₁✝ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜' F'<VAR>inst✝ : BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁✝ : k₁ =O[l] k₂<VAR>h₂ : f' =O[l] g'<VAR>c₁ : ℝ<VAR>h₁ : IsBigOWith c₁ l k₁ k₂<GOAL>(fun x => k₁ x • f' x) =O[l] fun x => k₂ x • g' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c c' c₁✝ c₂✝ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜' F'<VAR>inst✝ : BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁✝ : k₁ =O[l] k₂<VAR>h₂✝ : f' =O[l] g'<VAR>c₁ : ℝ<VAR>h₁ : IsBigOWith c₁ l k₁ k₂<VAR>c₂ : ℝ<VAR>h₂ : IsBigOWith c₂ l f' g'<GOAL>(fun x => k₁ x • f' x) =O[l] fun x => k₂ x • g' x
<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✝¹ : LeftCancelMonoid G<VAR>inst✝ : Finite G<VAR>x y : G<VAR>n✝ : ℕ<VAR>h : orderOf x = orderOf y<VAR>n : ℕ<GOAL>(powersEquivPowers h) ⟨x ^ n, ⋯⟩ = ⟨y ^ n, ⋯⟩
<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✝¹ : LeftCancelMonoid G<VAR>inst✝ : Finite G<VAR>x y : G<VAR>n✝ : ℕ<VAR>h : orderOf x = orderOf y<VAR>n : ℕ<GOAL>(finCongr h) ⟨n % orderOf x, ⋯⟩ = ⟨n % orderOf y, ⋯⟩
<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>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>inst✝⁸ : Algebra R R'<VAR>inst✝⁷ : Algebra S S'<VAR>inst✝⁶ : Algebra R S'<VAR>inst✝⁵ : IsScalarTower R R' S'<VAR>inst✝⁴ : IsScalarTower R S S'<VAR>T : Type uT<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>f g : P.Hom P'<VAR>x : P.Ring<GOAL>(f.sub g) (1 ⊗ₜ[P.Ring] (D R P.Ring) x) = Cotangent.mk ((f.subToKer g) x)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_5, u_1} C<VAR>inst✝² : Category.{?u.23250, u_2} D<VAR>inst✝¹ : Category.{?u.23254, u_3} E<VAR>P : Cᵒᵖ ⥤ Type u_4<VAR>X B : C<VAR>π : X ⟶ B<VAR>inst✝ : EffectiveEpi π<VAR>c : PullbackCone π π<VAR>hc : IsLimit c<VAR>this : HasPullback π π<VAR>hP : Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)<GOAL>Nonempty (IsLimit (Fork.ofι (P.map π.op) ⋯))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_5, u_1} C<VAR>inst✝² : Category.{?u.23250, u_2} D<VAR>inst✝¹ : Category.{?u.23254, u_3} E<VAR>P : Cᵒᵖ ⥤ Type u_4<VAR>X B : C<VAR>π : X ⟶ B<VAR>inst✝ : EffectiveEpi π<VAR>c : PullbackCone π π<VAR>hc : IsLimit c<VAR>this : HasPullback π π<VAR>hP : Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)<GOAL>∀ (y : P.obj (op X)), P.map c.fst.op y = P.map c.snd.op y → ∃! x, P.map π.op x = y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_5, u_1} C<VAR>inst✝² : Category.{?u.23250, u_2} D<VAR>inst✝¹ : Category.{?u.23254, u_3} E<VAR>P : Cᵒᵖ ⥤ Type u_4<VAR>X B : C<VAR>π : X ⟶ B<VAR>inst✝ : EffectiveEpi π<VAR>c : PullbackCone π π<VAR>hc : IsLimit c<VAR>this : HasPullback π π<VAR>hP : ∀ (b : ↑{x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}), ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = b<GOAL>∀ (y : P.obj (op X)), P.map c.fst.op y = P.map c.snd.op y → ∃! x, P.map π.op x = y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_5, u_1} C<VAR>inst✝² : Category.{?u.23250, u_2} D<VAR>inst✝¹ : Category.{?u.23254, u_3} E<VAR>P : Cᵒᵖ ⥤ Type u_4<VAR>X B : C<VAR>π : X ⟶ B<VAR>inst✝ : EffectiveEpi π<VAR>c : PullbackCone π π<VAR>hc : IsLimit c<VAR>this : HasPullback π π<VAR>hP : ∀ (b : ↑{x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}), ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = b<VAR>b : P.obj (op X)<VAR>hb : P.map c.fst.op b = P.map c.snd.op b<VAR>h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst = pullback.fst π π<GOAL>∃! x, P.map π.op x = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_5, u_1} C<VAR>inst✝² : Category.{?u.23250, u_2} D<VAR>inst✝¹ : Category.{?u.23254, u_3} E<VAR>P : Cᵒᵖ ⥤ Type u_4<VAR>X B : C<VAR>π : X ⟶ B<VAR>inst✝ : EffectiveEpi π<VAR>c : PullbackCone π π<VAR>hc : IsLimit c<VAR>this : HasPullback π π<VAR>hP : ∀ (b : ↑{x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}), ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = b<VAR>b : P.obj (op X)<VAR>hb : P.map c.fst.op b = P.map c.snd.op b<VAR>h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst = pullback.fst π π<VAR>hb' : P.map (pullback.fst π π).op b = P.map (pullback.snd π π).op b<GOAL>∃! x, P.map π.op x = b
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>m : ℕ<VAR>inst✝ : CharP R m<VAR>n✝ : ℕ<VAR>h : m ∣ n✝ + 1<VAR>a b : ZMod (n✝ + 1)<GOAL>↑a.val + ↑b.val = ↑(val (a + b))
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>m : ℕ<VAR>inst✝ : CharP R m<VAR>n✝ : ℕ<VAR>h : m ∣ n✝ + 1<VAR>a b : ZMod (n✝ + 1)<GOAL>m ∣ a.val + b.val - (a.val + b.val) % n✝.succ
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R N<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Qₙ : QuadraticForm R N<VAR>f₁ : Q₁ →qᵢ Qₙ<VAR>f₂ : Q₂ →qᵢ Qₙ<VAR>hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)<VAR>m₁ : CliffordAlgebra Q₁<VAR>m₂ : CliffordAlgebra Q₂<VAR>i₁ i₂ : ZMod 2<VAR>hm₁ : m₁ ∈ evenOdd Q₁ i₁<VAR>hm₂ : m₂ ∈ evenOdd Q₂ i₂<GOAL>(map f₁) m₁ * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) m₁)
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : BilinForm R M<VAR>h : BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : BilinMap.toQuadraticMap B' = Q'' - Q'<VAR>m : M<GOAL>(ι Q') m = ((changeFormAux Q' B) m) 1
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<GOAL>b ∈ ball a r ↔ ‖a / b‖ < r
<VAR>α : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>x : α<VAR>t : Ordnode α<VAR>h : t.Valid<GOAL>(insert' x t).Valid
<VAR>α : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>x : α<VAR>t : Ordnode α<VAR>h : t.Valid<GOAL>(insertWith id x t).Valid