ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F✝<VAR>inst✝³ : NormedSpace ℝ F✝<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>u : E → E<VAR>u_meas : Measurable u<VAR>uf : EqOn u f s<VAR>u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x<VAR>F : ↑s → E := u ∘ Subtype.val<VAR>hF : F = u ∘ Subtype.val<VAR>A : Measure.map F (Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) = μ.restrict (f '' s)<GOAL>Measure.map (s.restrict f) (Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) = μ.restrict (f '' s)
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F✝<VAR>inst✝³ : NormedSpace ℝ F✝<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>u : E → E<VAR>u_meas : Measurable u<VAR>uf : EqOn u f s<VAR>u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x<VAR>F : ↑s → E := u ∘ Subtype.val<VAR>hF : F = u ∘ Subtype.val<VAR>A : Measure.map F (Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) = μ.restrict (f '' s)<VAR>this : F = s.restrict f<GOAL>Measure.map (s.restrict f) (Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) = μ.restrict (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<GOAL>s.ncard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<GOAL>↑s.encard.toNat = 2 ↔ s.encard = 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s✝ t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSingletonClass α<VAR>s : Set α<VAR>hs : s.Countable<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s✝ t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSingletonClass α<VAR>s : Set α<VAR>hs : s.Countable<GOAL>MeasurableSet (⋃ x ∈ s, {x})
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>l : List α<VAR>h : Nodup ⟦l⟧<GOAL>(powerset ⟦l⟧).Nodup
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>l : List α<VAR>h : Nodup ⟦l⟧<GOAL>(List.map ofList l.sublists').Nodup
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>l : List α<VAR>h : Nodup ⟦l⟧<GOAL>∀ x ∈ l.sublists', ∀ y ∈ l.sublists', ↑x = ↑y → x = y
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>f : α → ι<VAR>g : (Perm α)ᵈᵐᵃ<GOAL>g ∈ stabilizer (Perm α)ᵈᵐᵃ f ↔ f ∘ ⇑(mk.symm g) = f
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>f : α → ι<VAR>g : (Perm α)ᵈᵐᵃ<GOAL>g • f = f ↔ f ∘ ⇑(mk.symm g) = f
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<GOAL>M.Basis I X ↔ (M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E
<VAR>n✝ b b' : ℕ<VAR>h : b' % b = 1<VAR>n : ℕ<GOAL>b ∣ n ↔ b ∣ (b'.digits n).sum
<VAR>n✝ b b' : ℕ<VAR>h : b' % b = 1<VAR>n : ℕ<GOAL>b ∣ n ↔ b ∣ ofDigits 1 (b'.digits n)
<VAR>n✝ b b' : ℕ<VAR>h : b' % b = 1<VAR>n : ℕ<GOAL>b ∣ ofDigits b' (b'.digits n) ↔ b ∣ ofDigits 1 (b'.digits n)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α β : TypeVec.{u} n<VAR>g : α ⟹ β<VAR>a : P.A<VAR>f' : P.drop.B a ⟹ α<VAR>f : P.last.B a → P.W α<GOAL>g <$$> P.wMk a f' f = P.wMk a (g ⊚ f') (MvFunctor.map g ∘ f)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α β : TypeVec.{u} n<VAR>g : α ⟹ β<VAR>a : P.A<VAR>f' : P.drop.B a ⟹ α<VAR>f : P.last.B a → P.W α<VAR>this : MvFunctor.map g ∘ f = fun i => ⟨(f i).fst, g ⊚ (f i).snd⟩<GOAL>g <$$> P.wMk a f' f = P.wMk a (g ⊚ f') (MvFunctor.map g ∘ f)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α β : TypeVec.{u} n<VAR>g : α ⟹ β<VAR>a : P.A<VAR>f' : P.drop.B a ⟹ α<VAR>f : P.last.B a → P.W α<VAR>this✝ : MvFunctor.map g ∘ f = fun i => ⟨(f i).fst, g ⊚ (f i).snd⟩<VAR>this : f = fun i => ⟨(f i).fst, (f i).snd⟩<GOAL>(g <$$> P.wMk a f' fun i => ⟨(f i).fst, (f i).snd⟩) = P.wMk a (g ⊚ f') fun i => ⟨(f i).fst, g ⊚ (f i).snd⟩
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α β : TypeVec.{u} n<VAR>g : α ⟹ β<VAR>a : P.A<VAR>f' : P.drop.B a ⟹ α<VAR>f : P.last.B a → P.W α<VAR>this✝ : MvFunctor.map g ∘ f = fun i => ⟨(f i).fst, g ⊚ (f i).snd⟩<VAR>this : f = fun i => ⟨(f i).fst, (f i).snd⟩<GOAL>g <$$> ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn f' fun i => (f i).snd⟩ = ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn (g ⊚ f') fun i => g ⊚ (f i).snd⟩
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α β : TypeVec.{u} n<VAR>g : α ⟹ β<VAR>a : P.A<VAR>f' : P.drop.B a ⟹ α<VAR>f : P.last.B a → P.W α<VAR>this✝ : MvFunctor.map g ∘ f = fun i => ⟨(f i).fst, g ⊚ (f i).snd⟩<VAR>this : f = fun i => ⟨(f i).fst, (f i).snd⟩<VAR>h : ∀ (a : P.wp.A) (f : P.wp.B a ⟹ α), g <$$> ⟨a, f⟩ = ⟨a, g ⊚ f⟩<GOAL>g <$$> ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn f' fun i => (f i).snd⟩ = ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn (g ⊚ f') fun i => g ⊚ (f i).snd⟩
<VAR>n i : ℕ<GOAL>n &&& 2 ^ i = (n.testBit i).toNat * 2 ^ i
<VAR>n i j : ℕ<GOAL>(n &&& 2 ^ i).testBit j = ((n.testBit i).toNat * 2 ^ i).testBit j
<VAR>n i : ℕ<VAR>h : n.testBit i = false<GOAL>(n &&& 2 ^ i).testBit i = (false.toNat * 2 ^ i).testBit i
<VAR>n i : ℕ<VAR>h : n.testBit i = true<GOAL>(n &&& 2 ^ i).testBit i = (true.toNat * 2 ^ i).testBit i
<VAR>n i j : ℕ<VAR>hij : i ≠ j<VAR>h : n.testBit i = false<GOAL>(n &&& 2 ^ i).testBit j = (false.toNat * 2 ^ i).testBit j
<VAR>n i j : ℕ<VAR>hij : i ≠ j<VAR>h : n.testBit i = true<GOAL>(n &&& 2 ^ i).testBit j = (true.toNat * 2 ^ i).testBit j
<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>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>j : StructuredArrow (op X) G.op<GOAL>lift hF hR s ≫ R.map j.hom ≫ α.app j.right = liftAux hF α s j.hom.unop
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Monoid (G i)<VAR>inst✝ : Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>f : (i : ι) → G i →* K<VAR>k : H →* K<VAR>hf : ∀ (i : ι), (f i).comp (φ i) = k<VAR>g : H<GOAL>((con φ).lift (Coprod.lift (CoprodI.lift f) k) ⋯) (((con φ).mk'.comp inr) g) = k g
<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>N : Type u_5<VAR>inst✝ : Group N<VAR>f✝ f : G →* N<VAR>H K : Subgroup G<GOAL>map f H ≤ map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker
<VAR>α : Type u_1<VAR>a✝ b✝ c✝ d : α<VAR>inst✝¹ : MulZeroClass α<VAR>inst✝ : PartialOrder α<VAR>h✝ : ContravariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x x_1 => x < x_1<VAR>a : { x // 0 ≤ x }<VAR>b c : α<VAR>h : ↑a * b < ↑a * c<GOAL>b < c
<VAR>α : Type u_1<VAR>a✝ b✝ c✝ d : α<VAR>inst✝¹ : MulZeroClass α<VAR>inst✝ : PartialOrder α<VAR>h✝ : ContravariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x x_1 => x < x_1<VAR>a : { x // 0 ≤ x }<VAR>b c : α<VAR>h : ↑a * b < ↑a * c<VAR>ha : 0 = ↑a<GOAL>b < c
<VAR>α : Type u_1<VAR>a✝ b✝ c✝ d : α<VAR>inst✝¹ : MulZeroClass α<VAR>inst✝ : PartialOrder α<VAR>h✝ : ContravariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x x_1 => x < x_1<VAR>a : { x // 0 ≤ x }<VAR>b c : α<VAR>h : ↑a * b < ↑a * c<VAR>ha : 0 < ↑a<GOAL>b < c
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>inst✝⁵ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝⁴ : DecidableEq I₁₂<VAR>inst✝³ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝² : K.HasTotal c₁₂<VAR>inst✝¹ : L.HasTotal c₁₂<VAR>inst✝ : M.HasTotal c₁₂<GOAL>map (φ ≫ ψ) c₁₂ = map φ c₁₂ ≫ map ψ c₁₂
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>inst✝⁵ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝⁴ : DecidableEq I₁₂<VAR>inst✝³ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝² : K.HasTotal c₁₂<VAR>inst✝¹ : L.HasTotal c₁₂<VAR>inst✝ : M.HasTotal c₁₂<GOAL>(HomologicalComplex.forget C c₁₂).map (map (φ ≫ ψ) c₁₂) = (HomologicalComplex.forget C c₁₂).map (map φ c₁₂ ≫ map ψ c₁₂)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : MulOneClass P<VAR>g : N →* P<VAR>f₁ f₂ : M →* N<VAR>hg : Function.Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>x : M<GOAL>g (f₁ x) = g (f₂ x)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>b : Basis ι R L<VAR>inst✝ : Nontrivial R<GOAL>(φ.polyCharpoly b).coeff (φ.nilRankAux b) ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>b : Basis ι R L<VAR>inst✝ : Nontrivial R<GOAL>φ.polyCharpoly b ≠ 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁✝ s₂✝ t✝ t₁ t₂ u t s₁ s₂ : Set α<VAR>h : s₁ ⊆ s₂<VAR>x : α<GOAL>x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t
<VAR>N : ℕ<VAR>a u v : Fin 2 → ZMod N<VAR>huv : u ≠ v<GOAL>(Disjoint on gammaSet N) u v
<VAR>N : ℕ<VAR>a u v : Fin 2 → ZMod N<VAR>huv : ¬(Disjoint on gammaSet N) u v<GOAL>u = v
<VAR>N : ℕ<VAR>a u v : Fin 2 → ZMod N<VAR>huv : ¬(Disjoint on gammaSet N) u v<VAR>f : Fin 2 → ℤ<VAR>hf : f ∈ gammaSet N u ∧ f ∈ gammaSet N v<GOAL>u = v
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : OpensMeasurableSpace X<VAR>hs : IsClosed s<GOAL>LocallyIntegrableOn f s μ ↔ LocallyIntegrable f (μ.restrict s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : OpensMeasurableSpace X<VAR>hs : IsClosed s<VAR>hf : LocallyIntegrableOn f s μ<VAR>x : X<GOAL>IntegrableAtFilter f (𝓝 x) (μ.restrict s)
<VAR>R✝ : Type u<VAR>inst✝¹ : CommRing R✝<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : PrimeSpectrum R<VAR>h : x ⤳ y<GOAL>(toOpen R ⊤ ≫ (structureSheaf R).presheaf.germ ⟨y, True.intro⟩) ≫ (structureSheaf R).presheaf.stalkSpecializes h = toOpen R ⊤ ≫ (structureSheaf R).presheaf.germ ⟨x, True.intro⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁✝ s₂✝ t✝ t₁ t₂ u t s₁ s₂ s : Set α<GOAL>t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s
<VAR>R : Type uR<VAR>inst✝⁶ : Semiring R<VAR>S : Type uS<VAR>inst✝⁵ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝² : Semiring T<VAR>B : Type u₄<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra S B<VAR>s : A → A → Prop<VAR>f : A →ₐ[S] B<VAR>h : ∀ ⦃x y : A⦄, s x y → f x = f y<VAR>x : RingQuot s<VAR>a✝ b✝ : A<VAR>r : Rel s a✝ b✝<GOAL>f a✝ = f b✝
<VAR>R : Type uR<VAR>inst✝⁶ : Semiring R<VAR>S : Type uS<VAR>inst✝⁵ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra S A<VAR>r : R → R → Prop<VAR>inst✝² : Semiring T<VAR>B : Type u₄<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra S B<VAR>s : A → A → Prop<VAR>f : A →ₐ[S] B<VAR>h : ∀ ⦃x y : A⦄, s x y → f x = f y<GOAL>(↑{ toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯ }).toFun 0 = 0
<VAR>R : Type uR<VAR>inst✝⁶ : Semiring R<VAR>S : Type uS<VAR>inst✝⁵ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra S A<VAR>r : R → R → Prop<VAR>inst✝² : Semiring T<VAR>B : Type u₄<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra S B<VAR>s : A → A → Prop<VAR>f : A →ₐ[S] B<VAR>h : ∀ ⦃x y : A⦄, s x y → f x = f y<VAR>toQuot✝¹ : Quot (Rel s)<VAR>x : A<VAR>toQuot✝ : Quot (Rel s)<VAR>y : A<GOAL>(↑{ toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯ }).toFun ({ toQuot := Quot.mk (Rel s) x } + { toQuot := Quot.mk (Rel s) y }) = (↑{ toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯ }).toFun { toQuot := Quot.mk (Rel s) x } + (↑{ toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯ }).toFun { toQuot := Quot.mk (Rel s) y }
<VAR>R : Type uR<VAR>inst✝⁶ : Semiring R<VAR>S : Type uS<VAR>inst✝⁵ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra S A<VAR>r : R → R → Prop<VAR>inst✝² : Semiring T<VAR>B : Type u₄<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra S B<VAR>s : A → A → Prop<VAR>f : A →ₐ[S] B<VAR>h : ∀ ⦃x y : A⦄, s x y → f x = f y<GOAL>(fun x => Quot.lift ⇑f ⋯ x.toQuot) 1 = 1
<VAR>R : Type uR<VAR>inst✝⁶ : Semiring R<VAR>S : Type uS<VAR>inst✝⁵ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra S A<VAR>r : R → R → Prop<VAR>inst✝² : Semiring T<VAR>B : Type u₄<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra S B<VAR>s : A → A → Prop<VAR>f : A →ₐ[S] B<VAR>h : ∀ ⦃x y : A⦄, s x y → f x = f y<VAR>toQuot✝¹ : Quot (Rel s)<VAR>x : A<VAR>toQuot✝ : Quot (Rel s)<VAR>y : A<GOAL>{ toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯ }.toFun ({ toQuot := Quot.mk (Rel s) x } * { toQuot := Quot.mk (Rel s) y }) = { toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯ }.toFun { toQuot := Quot.mk (Rel s) x } * { toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯ }.toFun { toQuot := Quot.mk (Rel s) y }
<VAR>R : Type uR<VAR>inst✝⁶ : Semiring R<VAR>S : Type uS<VAR>inst✝⁵ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra S A<VAR>r : R → R → Prop<VAR>inst✝² : Semiring T<VAR>B : Type u₄<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra S B<VAR>s : A → A → Prop<VAR>f : A →ₐ[S] B<VAR>h : ∀ ⦃x y : A⦄, s x y → f x = f y<VAR>x : S<GOAL>(↑↑{ toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }).toFun ((algebraMap S (RingQuot s)) x) = (algebraMap S B) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y : α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderTopology α<VAR>x : α<GOAL>Tendsto f (𝓝[<] x) (𝓝[≤] leftLim f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y : α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderTopology α<VAR>x : α<GOAL>∀ᶠ (x_1 : α) in 𝓝[<] x, f x_1 ∈ Iic (leftLim f x)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : StrictOrderedSemiring Γ<VAR>r : R<VAR>n : Γ<GOAL>((ofPowerSeries Γ R) ((PowerSeries.C R) r)).coeff n = (C r).coeff n
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : StrictOrderedSemiring Γ<VAR>r : R<VAR>n : Γ<GOAL>(embDomain { toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } (toPowerSeries.symm ((PowerSeries.C R) r))).coeff n = if n = 0 then r else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>a : α<VAR>b : β<VAR>x✝¹ x✝ : α × β<VAR>a₁ : α<VAR>b₁ : β<VAR>a₂ : α<VAR>b₂ : β<GOAL>GameAdd rβ rα (a₁, b₁).swap (a₂, b₂).swap ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
<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>g : G ≃ₗᵢ[𝕜] E<VAR>f : E → F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>x : G<VAR>hx : g x ∈ s<VAR>i : ℕ<GOAL>‖iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x‖ = ‖iteratedFDerivWithin 𝕜 i f s (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>g : G ≃ₗᵢ[𝕜] E<VAR>f : E → F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>x : G<VAR>hx : g x ∈ s<VAR>i : ℕ<VAR>this : iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x = (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x => ↑{ toLinearEquiv := g.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }<GOAL>‖iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x‖ = ‖iteratedFDerivWithin 𝕜 i f s (g x)‖
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>f : β → α<VAR>s t : Set α<VAR>x y : α<VAR>hs : s.WellFoundedOn r<VAR>hx : x ∈ s<VAR>P : α → Prop<VAR>hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y<VAR>Q : ↑s → Prop := fun y => P ↑y<GOAL>Q ⟨x, hx⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>f : β → α<VAR>s t : Set α<VAR>x y : α<VAR>hs : s.WellFoundedOn r<VAR>hx : x ∈ s<VAR>P : α → Prop<VAR>hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y<VAR>Q : ↑s → Prop := fun y => P ↑y<GOAL>∀ (x : ↑s), (∀ (y : ↑s), r ↑y ↑x → Q y) → Q x
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>β : Type u_2<VAR>m' : MeasurableSpace β<VAR>μ' : Measure β<VAR>s' : Set β<VAR>g : α → β<VAR>hg : MeasurePreserving g μ μ'<VAR>hf : PreErgodic f μ<VAR>f' : β → β<VAR>h_comm : g ∘ f = f' ∘ g<VAR>s : Set β<VAR>hs₀ : MeasurableSet s<VAR>hs₁ : f' ⁻¹' s = s<GOAL>s =ᶠ[ae μ'] ∅ ∨ s =ᶠ[ae μ'] univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>β : Type u_2<VAR>m' : MeasurableSpace β<VAR>μ' : Measure β<VAR>s' : Set β<VAR>g : α → β<VAR>hg : MeasurePreserving g μ μ'<VAR>hf : PreErgodic f μ<VAR>f' : β → β<VAR>h_comm : g ∘ f = f' ∘ g<VAR>s : Set β<VAR>hs₀ : MeasurableSet s<VAR>hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s<GOAL>s =ᶠ[ae μ'] ∅ ∨ s =ᶠ[ae μ'] univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>β : Type u_2<VAR>m' : MeasurableSpace β<VAR>μ' : Measure β<VAR>s' : Set β<VAR>g : α → β<VAR>hg : MeasurePreserving g μ μ'<VAR>hf : PreErgodic f μ<VAR>f' : β → β<VAR>h_comm : g ∘ f = f' ∘ g<VAR>s : Set β<VAR>hs₀ : MeasurableSet s<VAR>hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s<VAR>hs₂ : g ⁻¹' s =ᶠ[ae μ] ∅<GOAL>s =ᶠ[ae μ'] ∅
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>β : Type u_2<VAR>m' : MeasurableSpace β<VAR>μ' : Measure β<VAR>s' : Set β<VAR>g : α → β<VAR>hg : MeasurePreserving g μ μ'<VAR>hf : PreErgodic f μ<VAR>f' : β → β<VAR>h_comm : g ∘ f = f' ∘ g<VAR>s : Set β<VAR>hs₀ : MeasurableSet s<VAR>hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s<VAR>hs₂ : g ⁻¹' s =ᶠ[ae μ] univ<GOAL>s =ᶠ[ae μ'] univ
<VAR>a b c p q : ℚ<GOAL>a ≤ b ∨ b ≤ a
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝ : S.HasHomology<VAR>h : S.LeftHomologyData<GOAL>h.leftHomologyIso.hom ≫ (S.leftHomologyIso.symm ≪≫ h.leftHomologyIso).inv = S.leftHomologyIso.hom
<VAR>J : Type u<VAR>inst✝³ : Category.{w, u} J<VAR>inst✝² : IsCofilteredOrEmpty J<VAR>F : J ⥤ Type v<VAR>inst✝¹ : ∀ (j : J), Finite (F.obj j)<VAR>inst✝ : ∀ (j : J), Nonempty (F.obj j)<VAR>J' : Type (max w v u) := AsSmall J<VAR>down : J' ⥤ J := AsSmall.down<VAR>F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}<VAR>this : ∀ (i : J'), Nonempty (F'.obj i)<GOAL>F.sections.Nonempty
<VAR>J : Type u<VAR>inst✝³ : Category.{w, u} J<VAR>inst✝² : IsCofilteredOrEmpty J<VAR>F : J ⥤ Type v<VAR>inst✝¹ : ∀ (j : J), Finite (F.obj j)<VAR>inst✝ : ∀ (j : J), Nonempty (F.obj j)<VAR>J' : Type (max w v u) := AsSmall J<VAR>down : J' ⥤ J := AsSmall.down<VAR>F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}<VAR>this✝ : ∀ (i : J'), Nonempty (F'.obj i)<VAR>this : ∀ (i : J'), Finite (F'.obj i)<GOAL>F.sections.Nonempty
<VAR>J : Type u<VAR>inst✝³ : Category.{w, u} J<VAR>inst✝² : IsCofilteredOrEmpty J<VAR>F : J ⥤ Type v<VAR>inst✝¹ : ∀ (j : J), Finite (F.obj j)<VAR>inst✝ : ∀ (j : J), Nonempty (F.obj j)<VAR>J' : Type (max w v u) := AsSmall J<VAR>down : J' ⥤ J := AsSmall.down<VAR>F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}<VAR>this✝ : ∀ (i : J'), Nonempty (F'.obj i)<VAR>this : ∀ (i : J'), Finite (F'.obj i)<VAR>h✝ : IsEmpty J<GOAL>F.sections.Nonempty
<VAR>J : Type u<VAR>inst✝³ : Category.{w, u} J<VAR>inst✝² : IsCofilteredOrEmpty J<VAR>F : J ⥤ Type v<VAR>inst✝¹ : ∀ (j : J), Finite (F.obj j)<VAR>inst✝ : ∀ (j : J), Nonempty (F.obj j)<VAR>J' : Type (max w v u) := AsSmall J<VAR>down : J' ⥤ J := AsSmall.down<VAR>F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}<VAR>this✝ : ∀ (i : J'), Nonempty (F'.obj i)<VAR>this : ∀ (i : J'), Finite (F'.obj i)<VAR>h✝ : Nonempty J<GOAL>F.sections.Nonempty
<VAR>J : Type u<VAR>inst✝³ : Category.{w, u} J<VAR>inst✝² : IsCofilteredOrEmpty J<VAR>F : J ⥤ Type v<VAR>inst✝¹ : ∀ (j : J), Finite (F.obj j)<VAR>inst✝ : ∀ (j : J), Nonempty (F.obj j)<VAR>J' : Type (max w v u) := AsSmall J<VAR>down : J' ⥤ J := AsSmall.down<VAR>F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}<VAR>this✝¹ : ∀ (i : J'), Nonempty (F'.obj i)<VAR>this✝ : ∀ (i : J'), Finite (F'.obj i)<VAR>h✝ : Nonempty J<VAR>this : IsCofiltered J<GOAL>F.sections.Nonempty
<VAR>J : Type u<VAR>inst✝³ : Category.{w, u} J<VAR>inst✝² : IsCofilteredOrEmpty J<VAR>F : J ⥤ Type v<VAR>inst✝¹ : ∀ (j : J), Finite (F.obj j)<VAR>inst✝ : ∀ (j : J), Nonempty (F.obj j)<VAR>J' : Type (max w v u) := AsSmall J<VAR>down : J' ⥤ J := AsSmall.down<VAR>F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}<VAR>this✝¹ : ∀ (i : J'), Nonempty (F'.obj i)<VAR>this✝ : ∀ (i : J'), Finite (F'.obj i)<VAR>h✝ : Nonempty J<VAR>this : IsCofiltered J<VAR>u : (j : J') → F'.obj j<VAR>hu : u ∈ F'.sections<GOAL>F.sections.Nonempty