ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝² : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>R'' : Type u_3<VAR>inst✝ : CommRing R''<VAR>χ : MulChar R R'<VAR>f : R' →+* R''<VAR>hf : Function.Injective ⇑f<VAR>a : Rˣ<VAR>ha : χ ↑a ≠ 1<GOAL>(χ.ringHomComp f).IsNontrivial
<VAR>R : Type u_1<VAR>inst✝² : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>R'' : Type u_3<VAR>inst✝ : CommRing R''<VAR>χ : MulChar R R'<VAR>f : R' →+* R''<VAR>hf : Function.Injective ⇑f<VAR>a : Rˣ<VAR>ha : χ ↑a ≠ 1<GOAL>(χ.ringHomComp f) ↑a ≠ 1
<VAR>R : Type u_1<VAR>inst✝² : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>R'' : Type u_3<VAR>inst✝ : CommRing R''<VAR>χ : MulChar R R'<VAR>f : R' →+* R''<VAR>hf : Function.Injective ⇑f<VAR>a : Rˣ<VAR>ha : χ ↑a ≠ 1<GOAL>f (χ ↑a) ≠ f 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f✝ g : ι → Set X<VAR>π : X → Sort u_6<VAR>f : ℕ → (x : X) → π x<VAR>U : X → Set X<VAR>hUx : ∀ (x : X), U x ∈ 𝓝 x<VAR>hU : ∀ (x : X), {i | ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite<GOAL>∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.1 p.2 = F p.2
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f✝ g : ι → Set X<VAR>π : X → Sort u_6<VAR>f : ℕ → (x : X) → π x<VAR>U : X → Set X<VAR>hUx : ∀ (x : X), U x ∈ 𝓝 x<VAR>hU : ∀ (x : X), {i | ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite<VAR>N : X → ℕ<VAR>hN : ∀ (x : X), N x ∈ upperBounds {i | ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}<GOAL>∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.1 p.2 = F p.2
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f✝ g : ι → Set X<VAR>π : X → Sort u_6<VAR>f : ℕ → (x : X) → π x<VAR>U : X → Set X<VAR>hUx : ∀ (x : X), U x ∈ 𝓝 x<VAR>hU : ∀ (x : X), {i | ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite<VAR>N : X → ℕ<VAR>hN : ∀ (x : X), ∀ n > N x, ∀ y ∈ U x, f (n + 1) y = f n y<GOAL>∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.1 p.2 = F p.2
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f✝ g : ι → Set X<VAR>π : X → Sort u_6<VAR>f : ℕ → (x : X) → π x<VAR>U : X → Set X<VAR>hUx : ∀ (x : X), U x ∈ 𝓝 x<VAR>hU : ∀ (x : X), {i | ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite<VAR>N : X → ℕ<VAR>hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y<GOAL>∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.1 p.2 = F p.2
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f✝ g : ι → Set X<VAR>π : X → Sort u_6<VAR>f : ℕ → (x : X) → π x<VAR>U : X → Set X<VAR>hUx : ∀ (x : X), U x ∈ 𝓝 x<VAR>hU : ∀ (x : X), {i | ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite<VAR>N : X → ℕ<VAR>hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y<VAR>x : X<GOAL>∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.1 p.2 = (fun x => f (N x + 1) x) p.2
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f✝ g : ι → Set X<VAR>π : X → Sort u_6<VAR>f : ℕ → (x : X) → π x<VAR>U : X → Set X<VAR>hUx : ∀ (x : X), U x ∈ 𝓝 x<VAR>hU : ∀ (x : X), {i | ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite<VAR>N : X → ℕ<VAR>hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y<VAR>x : X<GOAL>∀ a ∈ {x_1 | N x < x_1} ×ˢ U x, f a.1 a.2 = f (N a.2 + 1) a.2
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f✝ g : ι → Set X<VAR>π : X → Sort u_6<VAR>f : ℕ → (x : X) → π x<VAR>U : X → Set X<VAR>hUx : ∀ (x : X), U x ∈ 𝓝 x<VAR>hU : ∀ (x : X), {i | ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite<VAR>N : X → ℕ<VAR>hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y<VAR>x : X<VAR>n : ℕ<VAR>y : X<VAR>hn : N x < n<VAR>hy : y ∈ U x<GOAL>f (n, y).1 (n, y).2 = f (N (n, y).2 + 1) (n, y).2
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝² : Category.{v'', u''} D<VAR>X Y : C<VAR>inst✝¹ : FinitaryPreExtensive C<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>F : Discrete ι ⥤ C<VAR>c : Cocone F<VAR>hc : IsColimit c<GOAL>IsUniversalColimit c
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝² : Category.{v'', u''} D<VAR>X Y : C<VAR>inst✝¹ : FinitaryPreExtensive C<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>F : Discrete ι ⥤ C<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>n : ℕ<VAR>e : ι ≃ Fin n<GOAL>IsUniversalColimit c
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝² : Category.{v'', u''} D<VAR>X Y : C<VAR>inst✝¹ : FinitaryPreExtensive C<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>F : Discrete ι ⥤ C<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>n : ℕ<VAR>e : ι ≃ Fin n<GOAL>IsUniversalColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝² : Category.{v'', u''} D<VAR>X Y : C<VAR>inst✝¹ : FinitaryPreExtensive C<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>F : Discrete ι ⥤ C<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>n : ℕ<VAR>e : ι ≃ Fin n<GOAL>IsColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a✝ b a : α<VAR>s : Finset α<VAR>h : a ∈ s<GOAL>s ∩ {a} = {a}
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MulZeroClass G₀<VAR>x y : G₀<GOAL>SemiconjBy 0 x y
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M A : Comon_ C<GOAL>A.counit.op ▷ op A.X ≫ A.comul.op = (λ_ (op A.X)).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M A : Comon_ C<GOAL>(λ_ A.X).inv.op = (λ_ (op A.X)).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M A : Comon_ C<GOAL>op A.X ◁ A.counit.op ≫ A.comul.op = (ρ_ (op A.X)).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M A : Comon_ C<GOAL>(ρ_ A.X).inv.op = (ρ_ (op A.X)).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M A : Comon_ C<GOAL>A.comul.op ▷ op A.X ≫ A.comul.op = (α_ (op A.X) (op A.X) (op A.X)).hom ≫ op A.X ◁ A.comul.op ≫ A.comul.op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M A : Comon_ C<GOAL>(α_ A.X A.X A.X).inv.op ≫ (A.X ◁ A.comul).op ≫ A.comul.op = (α_ A.X A.X A.X).inv.op ≫ (A.comul ≫ A.X ◁ A.comul).op
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<GOAL>IsClosedImmersion f ↔ IsPreimmersion f ∧ IsClosed (Set.range ⇑f.val.base)
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹² : AddCommGroup V<VAR>inst✝¹¹ : Module 𝕜 V<VAR>inst✝¹⁰ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝⁹ : AddCommGroup W<VAR>inst✝⁸ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℂ F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℂ G<VAR>inst✝¹ : MeasurableAdd V<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddRightInvariant<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>f : V → E<VAR>v₀ : V<VAR>w : W<GOAL>fourierIntegral e μ L (f ∘ fun v => v + v₀) w = e ((L v₀) w) • fourierIntegral e μ L f w
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹² : AddCommGroup V<VAR>inst✝¹¹ : Module 𝕜 V<VAR>inst✝¹⁰ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝⁹ : AddCommGroup W<VAR>inst✝⁸ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℂ F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℂ G<VAR>inst✝¹ : MeasurableAdd V<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddRightInvariant<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>f : V → E<VAR>v₀ : V<VAR>w : W<GOAL>∫ (v : V), ↑(e (-(L v) w)) • f (v + v₀) ∂μ = ↑(e ((L v₀) w)) • ∫ (v : V), ↑(e (-(L v) w)) • f v ∂μ
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹² : AddCommGroup V<VAR>inst✝¹¹ : Module 𝕜 V<VAR>inst✝¹⁰ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝⁹ : AddCommGroup W<VAR>inst✝⁸ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℂ F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℂ G<VAR>inst✝¹ : MeasurableAdd V<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddRightInvariant<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>f : V → E<VAR>v₀ : V<VAR>w : W<GOAL>∫ (v : V), ↑(e (-(L (v + v₀ - v₀)) w)) • f (v + v₀) ∂μ = ↑(e ((L v₀) w)) • ∫ (v : V), ↑(e (-(L v) w)) • f v ∂μ
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹² : AddCommGroup V<VAR>inst✝¹¹ : Module 𝕜 V<VAR>inst✝¹⁰ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝⁹ : AddCommGroup W<VAR>inst✝⁸ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℂ F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℂ G<VAR>inst✝¹ : MeasurableAdd V<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddRightInvariant<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>f : V → E<VAR>v₀ : V<VAR>w : W<GOAL>∫ (x : V), ↑(e (-(L (x - v₀)) w)) • f x ∂μ = ∫ (a : V), ↑(e ((L v₀) w)) • ↑(e (-(L a) w)) • f a ∂μ
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹² : AddCommGroup V<VAR>inst✝¹¹ : Module 𝕜 V<VAR>inst✝¹⁰ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝⁹ : AddCommGroup W<VAR>inst✝⁸ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℂ F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℂ G<VAR>inst✝¹ : MeasurableAdd V<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddRightInvariant<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>f : V → E<VAR>v₀ : V<VAR>w : W<VAR>v : V<GOAL>↑(e (-(L (v - v₀)) w)) • f v = ↑(e ((L v₀) w)) • ↑(e (-(L v) w)) • f v
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r : R[X]<VAR>x✝ : R<VAR>p : R[X]<VAR>x : R<GOAL>eval x p = ∑ i ∈ range (p.natDegree + 1), p.coeff i * x ^ i
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r : R[X]<VAR>x✝ : R<VAR>p : R[X]<VAR>x : R<GOAL>∀ (n : ℕ), 0 * x ^ n = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>s : Set X<VAR>h : IsPreconnected s<VAR>hs : s.Nontrivial<GOAL>s.Infinite
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>s : Set X<VAR>h : IsPreconnected s<VAR>hs : s.Nontrivial<VAR>hf : s.Finite<GOAL>Subsingleton ↑s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>s : Set X<VAR>h : IsPreconnected s<VAR>hs : s.Nontrivial<VAR>hf : s.Finite<VAR>this : DiscreteTopology ↑s<GOAL>Subsingleton ↑s
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝¹ : ReflectsColimit (span f g) F<VAR>inst✝ : F.Faithful<VAR>H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)<GOAL>F.map (f ≫ h) = F.map (g ≫ i)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ g f : Perm α<GOAL>f.support.card ≤ 1 ↔ f = 1
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X✝ Y Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>B A : C<VAR>X : Subobject B<VAR>f : A ⟶ B<VAR>inst✝ : Mono f<VAR>i : A ≅ underlying.obj X<VAR>w : i.hom ≫ X.arrow = f<GOAL>i.symm.hom ≫ f = X.arrow
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>S : Set (StarSubalgebra R A)<VAR>x : A<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeSup α<VAR>inst✝⁵ : OrderTop α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeSup β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) ↑s<VAR>ha : a ∈ s<GOAL>s.truncatedSup a = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeSup α<VAR>inst✝⁵ : OrderTop α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeSup β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) ↑s<VAR>ha : a ∈ s<GOAL>s.truncatedSup a ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeSup α<VAR>inst✝⁵ : OrderTop α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeSup β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) ↑s<VAR>ha : a ∈ s<GOAL>∀ (b : α), b ∈ s ∧ a ≤ b → id b ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeSup α<VAR>inst✝⁵ : OrderTop α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeSup β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a b✝ : α<VAR>inst✝ : DecidableEq α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) ↑s<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<VAR>hab : a ≤ b<GOAL>id b ≤ a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>comp 0 p = 0
<VAR>α : Type u<VAR>u : Ultrafilter (Ultrafilter α)<VAR>x : Ultrafilter α<GOAL>↑u ≤ 𝓝 x ↔ x = joinM u
<VAR>α : Type u<VAR>u : Ultrafilter (Ultrafilter α)<VAR>x : Ultrafilter α<GOAL>↑u ≤ 𝓝 x ↔ ↑(joinM u) ≤ ↑x
<VAR>α : Type u<VAR>u : Ultrafilter (Ultrafilter α)<VAR>x : Ultrafilter α<GOAL>↑u ≤ 𝓝 x ↔ ∀ s ∈ x, {v | s ∈ v} ∈ u
<VAR>α : Type u<VAR>u : Ultrafilter (Ultrafilter α)<VAR>x : Ultrafilter α<GOAL>(∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u) ↔ ∀ s ∈ x, {v | s ∈ v} ∈ u
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>f✝ : α → ℝ<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>x : α<GOAL>ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) = ↑⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>h1 : 0 ≤ c<VAR>h2 : c < 1<VAR>h3 : ∀ (n : ℕ), f n = true → g n = true<GOAL>cantorFunction c f ≤ cantorFunction c g
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>h1 : 0 ≤ c<VAR>h2 : c < 1<VAR>h3 : ∀ (n : ℕ), f n = true → g n = true<GOAL>∀ (i : ℕ), cantorFunctionAux c f i ≤ cantorFunctionAux c g i
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>y : α<VAR>xs : List α<VAR>w : xs.get? (findIdx p xs) = some y<GOAL>p y = true
<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>h : f =o[l] g<GOAL>∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℂ<VAR>hl_im : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |(g x).im|<VAR>hl : ∀ᶠ (x : α) in l, f x = 0 → (g x).re = 0 → g x = 0<GOAL>(let_fun this := fun x => abs (f x) ^ (g x).re / 1; this) =ᶠ[l] let_fun this := fun x => abs (f x) ^ (g x).re; this
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℂ<VAR>hl_im : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |(g x).im|<VAR>hl : ∀ᶠ (x : α) in l, f x = 0 → (g x).re = 0 → g x = 0<GOAL>(fun x => abs (f x) ^ (g x).re) =ᶠ[l] fun x => abs (f x) ^ (g x).re
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>c : F<GOAL>deriv (fun y => f y + c) x = deriv f x
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>i j✝ k : ι<VAR>φ : K ⟶ L<VAR>j : ι<VAR>inst✝² : K.HasHomology j<VAR>inst✝¹ : L.HasHomology j<VAR>inst✝ : Mono (φ.f j)<VAR>hj : ∀ (i : ι), ¬c.Rel i j<GOAL>¬c.Rel (c.prev j) j
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<GOAL>μ[f - g|m] =ᶠ[ae μ] μ[f|m] - μ[g|m]
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<GOAL>μ[f + -g|m] =ᶠ[ae μ] μ[f|m] + -μ[g|m]
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>x✝ : Nonempty (IsColimit (pUnitCocone C))<VAR>h : IsColimit (pUnitCocone C)<VAR>colimitCocone : ColimitCocone (constPUnitFunctor C) := { cocone := pUnitCocone C, isColimit := h }<VAR>this : HasColimit (constPUnitFunctor C)<GOAL>IsConnected C
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>x✝ : Nonempty (IsColimit (pUnitCocone C))<VAR>h : IsColimit (pUnitCocone C)<VAR>colimitCocone : ColimitCocone (constPUnitFunctor C) := { cocone := pUnitCocone C, isColimit := h }<VAR>this : HasColimit (constPUnitFunctor C)<GOAL>Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})
<VAR>m₁ m₂ n : ℕ<VAR>hm1 : m₁ ∈ n.smoothNumbers<VAR>hm2 : m₂ ∈ n.smoothNumbers<GOAL>m₁ * m₂ ∈ n.smoothNumbers
<VAR>m₁ m₂ n : ℕ<VAR>hm1 : m₁ ∈ factoredNumbers (Finset.range n)<VAR>hm2 : m₂ ∈ factoredNumbers (Finset.range n)<GOAL>m₁ * m₂ ∈ factoredNumbers (Finset.range n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I J : Ideal R<GOAL>I.minimalPrimes = comap (Quotient.mk I) '' minimalPrimes (R ⧸ I)
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : List (Sigma β)<GOAL>lookup a s.toFinmap = dlookup a s
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<GOAL>Function.swap dist = dist
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : α<GOAL>Function.swap dist x y = dist x y
<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>M : Type u_5<VAR>S : Type u_6<VAR>inst✝¹ : DivInvMonoid M<VAR>inst✝ : SetLike S M<VAR>hSM : SubgroupClass S M<VAR>H K : S<VAR>x y : M<VAR>hx : x ∈ H<VAR>hy : y ∈ H<GOAL>x / y ∈ H
<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>M : Type u_5<VAR>S : Type u_6<VAR>inst✝¹ : DivInvMonoid M<VAR>inst✝ : SetLike S M<VAR>hSM : SubgroupClass S M<VAR>H K : S<VAR>x y : M<VAR>hx : x ∈ H<VAR>hy : y ∈ H<GOAL>x * y⁻¹ ∈ H
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>S T : Submonoid M<GOAL>∀ {x : M}, x ∈ S → x ∈ S ⊔ T
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>S T : Submonoid M<GOAL>S ≤ S ⊔ T
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → β → β<VAR>b : β<VAR>x : α<VAR>xs : List α<GOAL>foldr f b (xs ++ [x]) = foldr f (f x b) xs
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>ι : Type u_9<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : Semiring R₂<VAR>inst✝⁹ : Semiring R₃<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f✝ : M →ₛₗ[σ₁₂] M₂<VAR>g✝ : M₂ →ₛₗ[σ₂₃] M₃<VAR>f g : M →ₗ[R] M<VAR>h : Commute f g<VAR>p : Submodule R M<VAR>hf : MapsTo ⇑f ↑p ↑p<VAR>hg : MapsTo ⇑g ↑p ↑p<GOAL>f.restrict hf * g.restrict hg = g.restrict hg * f.restrict hf
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>ι : Type u_9<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : Semiring R₂<VAR>inst✝⁹ : Semiring R₃<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f✝ : M →ₛₗ[σ₁₂] M₂<VAR>g✝ : M₂ →ₛₗ[σ₂₃] M₃<VAR>f g : M →ₗ[R] M<VAR>h : Commute f g<VAR>p : Submodule R M<VAR>hf : MapsTo ⇑f ↑p ↑p<VAR>hg : MapsTo ⇑g ↑p ↑p<GOAL>(g * f).restrict ⋯ = g.restrict hg * f.restrict hf
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : R<VAR>p : R[X][Y]<VAR>h : Polynomial.evalEval x y p = 0<VAR>g : R[X][Y]<GOAL>(evalEval h) ((mk p) g) = Polynomial.evalEval x y g
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>M : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>a : A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R A M<VAR>p : Submodule R M<VAR>hp : p ≤ Submodule.comap ((Algebra.lsmul R R M) a) p<VAR>q q₁ q₂ : Submodule R[X] (AEval R M a)<VAR>hq : (comapSubmodule R M a) q₁ = (comapSubmodule R M a) q₂<GOAL>q₁ = q₂
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>M : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>a : A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R A M<VAR>p : Submodule R M<VAR>hp : p ≤ Submodule.comap ((Algebra.lsmul R R M) a) p<VAR>q q₁ q₂ : Submodule R[X] (AEval R M a)<VAR>hq : (comapSubmodule R M a) q₁ = (comapSubmodule R M a) q₂<GOAL>mapSubmodule a ⋯ = mapSubmodule a ⋯