ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>inst✝³ : NormedSpace 𝕜 Gₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : RingHomIsometric σ₁₃<VAR>f : E →SL[σ₁₂] F<VAR>g : E →SL[σ₁₃] G<VAR>h : ∀ (x : E), ‖f x‖ = ‖g x‖<VAR>x : E<GOAL>‖g x‖ ≤ ‖g‖ * ‖x‖
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<GOAL>(fun x => a + x) '' [[b, c]] = [[a + b, a + c]]
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S✝ : Sieve X<VAR>R : Presieve X<VAR>S : Sieve X<VAR>x : FamilyOfElements P S.arrows<VAR>t : x.Compatible<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<VAR>Z : C<VAR>g : Z ⟶ Y<GOAL>x (g ≫ f) ⋯ = P.map g.op (x f hf)
<VAR>R : Type u_1<VAR>inst✝ : Ring R<GOAL>cyclotomic 3 R = X ^ 2 + X + 1
<VAR>x : ℝ<VAR>h : x ≠ -1<GOAL>HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Ici x) x
<VAR>h : 1 ≠ -1<GOAL>HasDerivWithinAt arcsin (1 / √(1 - 1 ^ 2)) (Ici 1) 1
<VAR>x : ℝ<VAR>h : x ≠ -1<VAR>h' : x ≠ 1<GOAL>HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Ici x) x
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : Category.{v₄, u₄} F<VAR>G : C ⥤ E<VAR>H : D ⥤ F<VAR>L₁ : C ⥤ D<VAR>R₁ : D ⥤ C<VAR>L₂ : E ⥤ F<VAR>R₂ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>x✝ : C<GOAL>((fun β => { app := fun X => (G ⋙ L₂).map (adj₁.unit.app X), naturality := ⋯ } ≫ { app := fun X => L₂.map ({ app := fun X => β.app (L₁.obj X), naturality := ⋯ }.app X), naturality := ⋯ } ≫ { app := fun X => adj₂.counit.app ((L₁ ⋙ H).obj X), naturality := ⋯ }) ((fun α => { app := fun X => adj₂.unit.app ((R₁ ⋙ G).obj X), naturality := ⋯ } ≫ { app := fun X => R₂.map ({ app := fun X => α.app (R₁.obj X), naturality := ⋯ }.app X), naturality := ⋯ } ≫ { app := fun X => (H ⋙ R₂).map (adj₁.counit.app X), naturality := ⋯ }) α)).app x✝ = α.app x✝
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : Category.{v₄, u₄} F<VAR>G : C ⥤ E<VAR>H : D ⥤ F<VAR>L₁ : C ⥤ D<VAR>R₁ : D ⥤ C<VAR>L₂ : E ⥤ F<VAR>R₂ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>x✝ : C<GOAL>L₂.map (G.map (adj₁.unit.app x✝)) ≫ α.app (R₁.obj (L₁.obj x✝)) ≫ H.map (adj₁.counit.app (L₁.obj x✝)) = α.app x✝
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : Category.{v₄, u₄} F<VAR>G : C ⥤ E<VAR>H : D ⥤ F<VAR>L₁ : C ⥤ D<VAR>R₁ : D ⥤ C<VAR>L₂ : E ⥤ F<VAR>R₂ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>x✝ : C<GOAL>α.app x✝ ≫ 𝟙 (H.obj (L₁.obj x✝)) = α.app x✝
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : Category.{v₄, u₄} F<VAR>G : C ⥤ E<VAR>H : D ⥤ F<VAR>L₁ : C ⥤ D<VAR>R₁ : D ⥤ C<VAR>L₂ : E ⥤ F<VAR>R₂ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>β : R₁ ⋙ G ⟶ H ⋙ R₂<VAR>x✝ : D<GOAL>((fun α => { app := fun X => adj₂.unit.app ((R₁ ⋙ G).obj X), naturality := ⋯ } ≫ { app := fun X => R₂.map ({ app := fun X => α.app (R₁.obj X), naturality := ⋯ }.app X), naturality := ⋯ } ≫ { app := fun X => (H ⋙ R₂).map (adj₁.counit.app X), naturality := ⋯ }) ((fun β => { app := fun X => (G ⋙ L₂).map (adj₁.unit.app X), naturality := ⋯ } ≫ { app := fun X => L₂.map ({ app := fun X => β.app (L₁.obj X), naturality := ⋯ }.app X), naturality := ⋯ } ≫ { app := fun X => adj₂.counit.app ((L₁ ⋙ H).obj X), naturality := ⋯ }) β)).app x✝ = β.app x✝
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : Category.{v₄, u₄} F<VAR>G : C ⥤ E<VAR>H : D ⥤ F<VAR>L₁ : C ⥤ D<VAR>R₁ : D ⥤ C<VAR>L₂ : E ⥤ F<VAR>R₂ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>β : R₁ ⋙ G ⟶ H ⋙ R₂<VAR>x✝ : D<GOAL>G.map (adj₁.unit.app (R₁.obj x✝)) ≫ β.app (L₁.obj (R₁.obj x✝)) ≫ R₂.map (H.map (adj₁.counit.app x✝)) = β.app x✝
<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 : M →ₗ⁅R,L⁆ M'<VAR>N N₂ : LieSubmodule R L M<VAR>N' : LieSubmodule R L M'<GOAL>comap N.incl N₂ = ⊤ ↔ N ≤ N₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<GOAL>Measurable dirac
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>Measurable fun b => (dirac b) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>Measurable fun b => s.indicator 1 b
<VAR>α : Type u_1<VAR>inst✝ : Field α<VAR>n k e : α<VAR>h2 : e ≠ 0<VAR>h3 : n * e = k<GOAL>k * e⁻¹ = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>x✝ : α × Vector α n<VAR>a : α<VAR>l : Vector α n<GOAL>ContinuousAt (fun p => Vector.insertNth p.1 i p.2) (a, l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>x✝ : α × Vector α n<VAR>a : α<VAR>l : Vector α n<GOAL>Tendsto (fun p => Vector.insertNth p.1 i p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (Vector.insertNth (a, l).1 i (a, l).2))
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>a b : Γ<GOAL>((single b) r * x).coeff (a + b) = r * x.coeff a
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>a b : Γ<GOAL>((HahnModule.of R).symm ((single b) r • (HahnModule.of R) x)).coeff (b +ᵥ a) = r * x.coeff a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>s : ι → Set X<VAR>x : X<VAR>h : (𝓝 x).HasBasis p s<GOAL>⋂ i, ⋂ (_ : p i), s i = {x}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<GOAL>s ⊆ {a, b} ↔ ∀ x ∈ s, x = a ∨ x = b
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : LieRing L<VAR>inst✝¹² : LieAlgebra R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup N<VAR>inst✝⁹ : AddCommGroup P<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R N<VAR>inst✝⁶ : Module R P<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieRingModule L N<VAR>inst✝³ : LieRingModule L P<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : LieModule R L N<VAR>inst✝ : LieModule R L P<VAR>f_inv : N → M<VAR>f : M → N<VAR>map_add'✝¹ : ∀ (x y : M), f (x + y) = f x + f y<VAR>map_smul'✝¹ : ∀ (m : R) (x : M), { toFun := f, map_add' := map_add'✝¹ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := map_add'✝¹ }.toFun x<VAR>map_lie'✝¹ : ∀ {x : L} {m : M}, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun ⁅x, m⁆ = ⁅x, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun m⁆<VAR>left_inv✝¹ : LeftInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun<VAR>right_inv✝¹ : Function.RightInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun<VAR>g_inv : N → M<VAR>g : M → N<VAR>map_add'✝ : ∀ (x y : M), g (x + y) = g x + g y<VAR>map_smul'✝ : ∀ (m : R) (x : M), { toFun := g, map_add' := map_add'✝ }.toFun (m • x) = (RingHom.id R) m • { toFun := g, map_add' := map_add'✝ }.toFun x<VAR>map_lie'✝ : ∀ {x : L} {m : M}, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun ⁅x, m⁆ = ⁅x, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun m⁆<VAR>left_inv✝ : LeftInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun<VAR>right_inv✝ : Function.RightInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun<VAR>h : { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹, invFun := f_inv, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toEquiv = { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝, invFun := g_inv, left_inv := left_inv✝, right_inv := right_inv✝ }.toEquiv<GOAL>{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹, invFun := f_inv, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } = { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝, invFun := g_inv, left_inv := left_inv✝, right_inv := right_inv✝ }
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : LieRing L<VAR>inst✝¹² : LieAlgebra R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup N<VAR>inst✝⁹ : AddCommGroup P<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R N<VAR>inst✝⁶ : Module R P<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieRingModule L N<VAR>inst✝³ : LieRingModule L P<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : LieModule R L N<VAR>inst✝ : LieModule R L P<VAR>f_inv : N → M<VAR>f : M → N<VAR>map_add'✝¹ : ∀ (x y : M), f (x + y) = f x + f y<VAR>map_smul'✝¹ : ∀ (m : R) (x : M), { toFun := f, map_add' := map_add'✝¹ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := map_add'✝¹ }.toFun x<VAR>map_lie'✝¹ : ∀ {x : L} {m : M}, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun ⁅x, m⁆ = ⁅x, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun m⁆<VAR>left_inv✝¹ : LeftInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun<VAR>right_inv✝¹ : Function.RightInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun<VAR>g_inv : N → M<VAR>g : M → N<VAR>map_add'✝ : ∀ (x y : M), g (x + y) = g x + g y<VAR>map_smul'✝ : ∀ (m : R) (x : M), { toFun := g, map_add' := map_add'✝ }.toFun (m • x) = (RingHom.id R) m • { toFun := g, map_add' := map_add'✝ }.toFun x<VAR>map_lie'✝ : ∀ {x : L} {m : M}, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun ⁅x, m⁆ = ⁅x, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun m⁆<VAR>left_inv✝ : LeftInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun<VAR>right_inv✝ : Function.RightInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun<VAR>h : f = g ∧ f_inv = g_inv<GOAL>{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹, invFun := f_inv, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } = { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝, invFun := g_inv, left_inv := left_inv✝, right_inv := right_inv✝ }
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : LieRing L<VAR>inst✝¹² : LieAlgebra R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup N<VAR>inst✝⁹ : AddCommGroup P<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R N<VAR>inst✝⁶ : Module R P<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieRingModule L N<VAR>inst✝³ : LieRingModule L P<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : LieModule R L N<VAR>inst✝ : LieModule R L P<VAR>f_inv : N → M<VAR>f : M → N<VAR>map_add'✝¹ : ∀ (x y : M), f (x + y) = f x + f y<VAR>map_smul'✝¹ : ∀ (m : R) (x : M), { toFun := f, map_add' := map_add'✝¹ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := map_add'✝¹ }.toFun x<VAR>map_lie'✝¹ : ∀ {x : L} {m : M}, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun ⁅x, m⁆ = ⁅x, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun m⁆<VAR>left_inv✝¹ : LeftInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun<VAR>right_inv✝¹ : Function.RightInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun<VAR>g_inv : N → M<VAR>g : M → N<VAR>map_add'✝ : ∀ (x y : M), g (x + y) = g x + g y<VAR>map_smul'✝ : ∀ (m : R) (x : M), { toFun := g, map_add' := map_add'✝ }.toFun (m • x) = (RingHom.id R) m • { toFun := g, map_add' := map_add'✝ }.toFun x<VAR>map_lie'✝ : ∀ {x : L} {m : M}, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun ⁅x, m⁆ = ⁅x, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun m⁆<VAR>left_inv✝ : LeftInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun<VAR>right_inv✝ : Function.RightInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun<VAR>h : f = g ∧ f_inv = g_inv<GOAL>f = g
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : LieRing L<VAR>inst✝¹² : LieAlgebra R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup N<VAR>inst✝⁹ : AddCommGroup P<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R N<VAR>inst✝⁶ : Module R P<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieRingModule L N<VAR>inst✝³ : LieRingModule L P<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : LieModule R L N<VAR>inst✝ : LieModule R L P<VAR>f_inv : N → M<VAR>f : M → N<VAR>map_add'✝¹ : ∀ (x y : M), f (x + y) = f x + f y<VAR>map_smul'✝¹ : ∀ (m : R) (x : M), { toFun := f, map_add' := map_add'✝¹ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := map_add'✝¹ }.toFun x<VAR>map_lie'✝¹ : ∀ {x : L} {m : M}, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun ⁅x, m⁆ = ⁅x, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun m⁆<VAR>left_inv✝¹ : LeftInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun<VAR>right_inv✝¹ : Function.RightInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun<VAR>g_inv : N → M<VAR>g : M → N<VAR>map_add'✝ : ∀ (x y : M), g (x + y) = g x + g y<VAR>map_smul'✝ : ∀ (m : R) (x : M), { toFun := g, map_add' := map_add'✝ }.toFun (m • x) = (RingHom.id R) m • { toFun := g, map_add' := map_add'✝ }.toFun x<VAR>map_lie'✝ : ∀ {x : L} {m : M}, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun ⁅x, m⁆ = ⁅x, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun m⁆<VAR>left_inv✝ : LeftInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun<VAR>right_inv✝ : Function.RightInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun<VAR>h : f = g ∧ f_inv = g_inv<GOAL>f_inv = g_inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>s : Set α<GOAL>((e.restr s).trans e').source = ((e.trans e').restr s).source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g : α → ℝ<GOAL>Integrable g (μ.withDensity f) ↔ Integrable (fun x => g x * (f x).toReal) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g : α → ℝ<VAR>this : (fun x => g x * (f x).toReal) = fun x => (f x).toReal • g x<GOAL>Integrable g (μ.withDensity f) ↔ Integrable (fun x => g x * (f x).toReal) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g : α → ℝ<VAR>this : (fun x => g x * (f x).toReal) = fun x => (f x).toReal • g x<GOAL>Integrable g (μ.withDensity f) ↔ Integrable (fun x => (f x).toReal • g x) μ
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : Monoid P<VAR>f : M →* P<VAR>g : N →* P<VAR>comm : ∀ (m : M) (n : N), Commute (f m) (g n)<GOAL>(fun mn => f mn.1 * g mn.2) 1 = 1
<VAR>R A : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroSMulDivisors R A<GOAL>#{ x // IsAlgebraic R x } ≤ #R[X] * ℵ₀
<VAR>R A : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroSMulDivisors R A<GOAL>lift.{u, u} #{ x // IsAlgebraic R x } ≤ lift.{u, u} #R[X] * ℵ₀
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁ : InfinitePlace K<VAR>B : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<VAR>n : ℕ<GOAL>((Algebra.norm ℤ) ↑(seq K w₁ hB n)).natAbs ≤ B
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace Y<VAR>f : OnePoint X → Y<GOAL>Tendsto (f ∘ some) (coclosedCompact X) (𝓝 (f ∞)) ↔ ∀ s ∈ 𝓝 (f ∞), ∃ t, IsClosed t ∧ IsCompact t ∧ MapsTo (f ∘ some) tᶜ s
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X : Cᵒᵖ<GOAL>limMap (whiskerLeft F (restriction R (𝟙 X))) ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map (𝟙 X))) (F ⋙ evaluation R X)).inv = (ModuleCat.restrictScalarsId'App (R.map (𝟙 X)) ⋯ (limit (F ⋙ evaluation R X))).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X : Cᵒᵖ<GOAL>limMap (whiskerLeft F (restriction R (𝟙 X))) = (ModuleCat.restrictScalarsId'App (R.map (𝟙 X)) ⋯ (limit (F ⋙ evaluation R X))).inv ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map (𝟙 X))) (F ⋙ evaluation R X)).hom
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X : Cᵒᵖ<GOAL>∀ (j : J), limMap (whiskerLeft F (restriction R (𝟙 X))) ≫ limit.π (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (R.map (𝟙 X))) j = ((ModuleCat.restrictScalarsId'App (R.map (𝟙 X)) ⋯ (limit (F ⋙ evaluation R X))).inv ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map (𝟙 X))) (F ⋙ evaluation R X)).hom) ≫ limit.π (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (R.map (𝟙 X))) j
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X : Cᵒᵖ<VAR>j : J<GOAL>limMap (whiskerLeft F (restriction R (𝟙 X))) ≫ limit.π (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (R.map (𝟙 X))) j = ((ModuleCat.restrictScalarsId'App (R.map (𝟙 X)) ⋯ (limit (F ⋙ evaluation R X))).inv ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map (𝟙 X))) (F ⋙ evaluation R X)).hom) ≫ limit.π (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (R.map (𝟙 X))) j
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X : Cᵒᵖ<VAR>j : J<GOAL>limit.π (F ⋙ evaluation R X) j ≫ restrictionApp (𝟙 X) (F.obj j) = (ModuleCat.restrictScalarsId'App (R.map (𝟙 X)) ⋯ (limit (F ⋙ evaluation R X))).inv ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map (𝟙 X))) (F ⋙ evaluation R X)).hom ≫ limit.π (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (R.map (𝟙 X))) j
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X : Cᵒᵖ<VAR>j : J<GOAL>limit.π (F ⋙ evaluation R X) j ≫ restrictionApp (𝟙 X) (F.obj j) = (ModuleCat.restrictScalarsId'App (R.map (𝟙 X)) ⋯ (limit (F ⋙ evaluation R X))).inv ≫ (ModuleCat.restrictScalars (R.map (𝟙 X))).map (limit.π (F ⋙ evaluation R X) j)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X : Cᵒᵖ<VAR>j : J<GOAL>limit.π (F ⋙ evaluation R X) j ≫ (ModuleCat.restrictScalarsId' (R.map (𝟙 X)) ⋯).inv.app ((F.obj j).obj X) = limit.π (F ⋙ evaluation R X) j ≫ (ModuleCat.restrictScalarsId'App (R.map (𝟙 X)) ⋯ ((F ⋙ evaluation R X).obj j)).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>limMap (whiskerLeft F (restriction R (f ≫ g))) ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map (f ≫ g))) (F ⋙ evaluation R Z)).inv = (limMap (whiskerLeft F (restriction R f)) ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map f)) (F ⋙ evaluation R Y)).inv) ≫ (ModuleCat.restrictScalars (R.map f)).map (limMap (whiskerLeft F (restriction R g)) ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map g)) (F ⋙ evaluation R Z)).inv) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ (limit (F ⋙ evaluation R Z))).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>limMap (whiskerLeft F (restriction R (f ≫ g))) = limMap (whiskerLeft F (restriction R f)) ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map f)) (F ⋙ evaluation R Y)).inv ≫ (ModuleCat.restrictScalars (R.map f)).map (limMap (whiskerLeft F (restriction R g)) ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map g)) (F ⋙ evaluation R Z)).inv) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ (limit (F ⋙ evaluation R Z))).inv ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map (f ≫ g))) (F ⋙ evaluation R Z)).hom