ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : SeminormedAddCommGroup α<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : DecidableEq n<VAR>v : n → α<GOAL>‖diagonal v‖₊ = ‖v‖₊
<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>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : SeminormedAddCommGroup α<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : DecidableEq n<VAR>v : n → α<GOAL>(Finset.univ.sup fun b => Finset.univ.sup fun b_1 => ‖diagonal v b b_1‖₊) = Finset.univ.sup fun b => ‖v b‖₊
<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>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : SeminormedAddCommGroup α<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : DecidableEq n<VAR>v : n → α<VAR>i : n<GOAL>(Finset.univ.sup fun b => ‖diagonal v i b‖₊) = ‖v i‖₊
<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>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : SeminormedAddCommGroup α<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : DecidableEq n<VAR>v : n → α<VAR>i j : n<VAR>hj : j ∈ Finset.univ<GOAL>‖diagonal v i j‖₊ ≤ ‖v i‖₊
<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>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : SeminormedAddCommGroup α<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : DecidableEq n<VAR>v : n → α<VAR>i : n<GOAL>‖v i‖₊ ≤ Finset.univ.sup fun b => ‖diagonal v i b‖₊
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>ha : a ≠ 0<GOAL>(C a * X ^ 2 + C b * X + C c).degree = 2
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>ha : a ≠ 0<GOAL>↑2 = 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : ℕ → Set α<VAR>n : ℕ<VAR>s : Set α<VAR>hs : s ∈ memPartition t n<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : ℕ → Set α<VAR>n : ℕ<VAR>s : Set α<VAR>hs : s ∈ memPartition t n<GOAL>MeasurableSet (s \ t n ∪ s ∩ t n)
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<GOAL>rdropWhile p l = l ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<GOAL>(∀ (hl : 0 < l.reverse.length), ¬p (l.reverse.get ⟨0, hl⟩) = true) ↔ ∀ (hl : l ≠ []), ¬p (l.get ⟨l.length - 1, ⋯⟩) = true
<VAR>m n a b c d : ℕ<VAR>h₁ : a ≡ b [MOD n]<VAR>h₂ : c ≡ d [MOD n]<GOAL>a + c ≡ b + d [MOD n]
<VAR>m n a b c d : ℕ<VAR>h₁ : a ≡ b [MOD n]<VAR>h₂ : c ≡ d [MOD n]<GOAL>↑n ∣ ↑b - ↑a + (↑d - ↑c)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hJ : M.Indep J<VAR>hIJ : I.encard < J.encard<GOAL>∃ e ∈ J \ I, M.Indep (insert e I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hJ : M.Indep J<VAR>hIJ : I.encard < J.encard<VAR>he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)<GOAL>False
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hJ : M.Indep J<VAR>hIJ : I.encard < J.encard<VAR>he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)<VAR>hb : M.Basis I (I ∪ J)<GOAL>False
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hJ : M.Indep J<VAR>hIJ : I.encard < J.encard<VAR>he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)<VAR>hb : M.Basis I (I ∪ J)<VAR>J' : Set α<VAR>hJ' : M.Basis J' (I ∪ J)<VAR>hJJ' : J ⊆ J'<GOAL>False
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hJ : M.Indep J<VAR>he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)<VAR>hb : M.Basis I (I ∪ J)<VAR>J' : Set α<VAR>hIJ : J'.encard < J.encard<VAR>hJ' : M.Basis J' (I ∪ J)<VAR>hJJ' : J ⊆ J'<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>x y : α<GOAL>Inseparable x y ↔ ClusterPt (x, y) (𝓤 α)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>x y : α<VAR>h : ClusterPt (x, y) (𝓤 α)<GOAL>Inseparable x y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>x y : α<VAR>h : ClusterPt (x, y) (𝓤 α)<GOAL>∀ (i : Set (α × α)), (i ∈ 𝓤 α ∧ ∀ (a : α × α), ClusterPt a (𝓟 i) → a ∈ i) → (x, y) ∈ id i
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁴ : MonoidWithZero R<VAR>inst✝³ : MonoidWithZero R'<VAR>inst✝² : Zero M<VAR>inst✝¹ : MulActionWithZero R M<VAR>inst✝ : Subsingleton R<VAR>x y : M<GOAL>x = y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : ClosedEmbedding f<VAR>s : Set X<VAR>h : IsClosed (f '' s)<GOAL>IsClosed s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : ClosedEmbedding f<VAR>s : Set X<VAR>h : IsClosed (f '' s)<GOAL>IsClosed (f ⁻¹' (f '' s))
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I✝ : Ideal R<VAR>a b : R<VAR>S : Type v<VAR>x y : R<VAR>I : Ideal R<GOAL>IsDomain (R ⧸ I) ↔ I.IsPrime
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I✝ : Ideal R<VAR>a b : R<VAR>S : Type v<VAR>x y : R<VAR>I : Ideal R<VAR>H : IsDomain (R ⧸ I)<GOAL>0 ≠ 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I✝ : Ideal R<VAR>a b : R<VAR>S : Type v<VAR>x✝ y✝ : R<VAR>I : Ideal R<VAR>H : IsDomain (R ⧸ I)<VAR>x y : R<VAR>h : x * y ∈ I<GOAL>x ∈ I ∨ y ∈ I
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>hN : N.FG<VAR>hIN : N ≤ I • N<VAR>hIjac : I ≤ ⊥.jacobson<GOAL>N = ⊥
<VAR>p : ℕ<VAR>hp : Prime p<GOAL>(p ^ 2).divisors = {p ^ 2, p, 1}
<VAR>x : ℤ<VAR>x✝ : ∃ n, n * n = x<VAR>n : ℤ<VAR>hn : n * n = x<GOAL>sqrt x * sqrt x = x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → DecidableEq (α i)<VAR>inst✝¹ : (i : ι) → PartialOrder (α i)<VAR>inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)<VAR>b : (i : ι) → α i<GOAL>(Iio b).card = ∏ i : ι, (Iic (b i)).card - 1
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_3<VAR>inst✝ : Group N<VAR>g x✝ : G<GOAL>x✝ ∈ zpowers g ↔ x✝ ∈ closure {g}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : ℝ≥0∞<VAR>h : p ≤ 1<VAR>b : Bool<GOAL>(bernoulli p h).support = {b | bif b then p ≠ 0 else p ≠ 1}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : ℝ≥0∞<VAR>h : p ≤ 1<VAR>b✝ b : Bool<GOAL>b ∈ (bernoulli p h).support ↔ b ∈ {b | bif b then p ≠ 0 else p ≠ 1}
<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<VAR>h : ¬s = 1<GOAL>(2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹
<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<VAR>h : s - 1 ≠ 0<GOAL>(2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹
<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<VAR>h : s - 1 ≠ 0<VAR>h' : ∀ (n : ℕ), s - 1 ≠ -↑n<GOAL>(2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹
<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<VAR>h : s - 1 ≠ 0<VAR>h' : ∀ (n : ℕ), s - 1 ≠ -↑n<GOAL>(s - 1).Gammaℂ * sin (↑π * s / 2) * (s - 1).Gammaℝ⁻¹ = (s - 1).Gammaℂ * (s - 1) / 2 / ↑π * sin (↑π * s / 2) * ((s - 1).Gammaℝ * (s - 1) / 2 / ↑π)⁻¹
<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<VAR>h : s - 1 ≠ 0<VAR>h' : ∀ (n : ℕ), s - 1 ≠ -↑n<GOAL>(s - 1).Gammaℂ * sin (↑π * (s / 2)) * (s - 1).Gammaℝ⁻¹ = (s - 1).Gammaℂ * ((s - 1) / 2 / ↑π) * sin (↑π * (s / 2)) * ((s - 1).Gammaℝ⁻¹ * ((s - 1) / 2 / ↑π)⁻¹)
<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<VAR>h : s - 1 ≠ 0<VAR>h' : ∀ (n : ℕ), s - 1 ≠ -↑n<VAR>A : ℂ<GOAL>(s - 1).Gammaℂ * sin (↑π * (s / 2)) * A = (s - 1).Gammaℂ * ((s - 1) / 2 / ↑π) * sin (↑π * (s / 2)) * (A * ((s - 1) / 2 / ↑π)⁻¹)
<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<VAR>h : s - 1 ≠ 0<VAR>h' : ∀ (n : ℕ), s - 1 ≠ -↑n<VAR>A : ℂ<GOAL>(s - 1).Gammaℂ * sin (↑π * s / 2) * A * (2 * ↑π * (s - 1)) = (s - 1).Gammaℂ * (s - 1) * sin (↑π * s / 2) * (A * (2 * ↑π))
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>α' : Sort w<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq α'<VAR>f✝ g : (a : α) → β a<VAR>a✝ : α<VAR>b✝ : β a✝<VAR>f : (a : α) → β a<VAR>a : α<VAR>b : β a<VAR>p : (a : α) → β a → Prop<GOAL>(∀ (x : α), p x (update f a b x)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>α' : Sort w<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq α'<VAR>f✝ g : (a : α) → β a<VAR>a✝ : α<VAR>b✝ : β a✝<VAR>f : (a : α) → β a<VAR>a : α<VAR>b : β a<VAR>p : (a : α) → β a → Prop<GOAL>(p a b ∧ ∀ (b_1 : α), b_1 ≠ a → p b_1 (update f a b b_1)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝³ : CommRing P<VAR>inst✝² : Algebra R P<VAR>loc : IsLocalization S P<VAR>inst✝¹ : Nontrivial P<VAR>inst✝ : NoZeroSMulDivisors R P<VAR>I : FractionalIdeal S P<VAR>h_nz : ↑I.den ≠ 0<VAR>x : ↥I<GOAL>(Algebra.linearMap R P) ↑((equivNum h_nz) x) = I.den • ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>f : ι × ι' → α<GOAL>(s.product t).SupIndep f ↔ (s.SupIndep fun i => t.sup fun i' => f (i, i')) ∧ t.SupIndep fun i' => s.sup fun i => f (i, i')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>f : ι × ι' → α<GOAL>(s.product t).SupIndep f → (s.SupIndep fun i => t.sup fun i' => f (i, i')) ∧ t.SupIndep fun i' => s.sup fun i => f (i, i')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>f : ι × ι' → α<GOAL>(↑(s.product t)).PairwiseDisjoint f → ((↑s).PairwiseDisjoint fun i => t.sup fun i' => f (i, i')) ∧ (↑t).PairwiseDisjoint fun i' => s.sup fun i => f (i, i')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>f : ι × ι' → α<VAR>h : (↑(s.product t)).PairwiseDisjoint f<VAR>i : ι<VAR>hi : i ∈ ↑s<VAR>j : ι<VAR>hj : j ∈ ↑s<VAR>hij : i ≠ j<VAR>i' : ι'<VAR>hi' : i' ∈ t<VAR>j' : ι'<VAR>hj' : j' ∈ t<GOAL>Disjoint (f (i, i')) (f (j, j'))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>f : ι × ι' → α<VAR>h : (↑(s.product t)).PairwiseDisjoint f<VAR>i : ι'<VAR>hi : i ∈ ↑t<VAR>j : ι'<VAR>hj : j ∈ ↑t<VAR>hij : i ≠ j<VAR>i' : ι<VAR>hi' : i' ∈ s<VAR>j' : ι<VAR>hj' : j' ∈ s<GOAL>Disjoint (f (i', i)) (f (j', j))
<VAR>f g : ℝ → ℝ<VAR>hfg : f =ᶠ[atTop] g<VAR>hg : GrowsPolynomially g<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)<GOAL>∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
<VAR>f g : ℝ → ℝ<VAR>hfg : f =ᶠ[atTop] g<VAR>hg : GrowsPolynomially g<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)<VAR>x : ℝ<VAR>hx₁ : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)<VAR>hx₂ : ∀ (y : ℝ), b * id x ≤ y → f y = g y<VAR>hx₃ : f x = g x<GOAL>∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
<VAR>f g : ℝ → ℝ<VAR>hfg : f =ᶠ[atTop] g<VAR>hg : GrowsPolynomially g<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)<VAR>x : ℝ<VAR>hx₁ : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)<VAR>hx₂ : ∀ (y : ℝ), b * id x ≤ y → f y = g y<VAR>hx₃ : f x = g x<VAR>u : ℝ<VAR>hu : u ∈ Set.Icc (b * x) x<GOAL>f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
<VAR>f g : ℝ → ℝ<VAR>hfg : f =ᶠ[atTop] g<VAR>hg : GrowsPolynomially g<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)<VAR>x : ℝ<VAR>hx₁ : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)<VAR>hx₂ : ∀ (y : ℝ), b * id x ≤ y → f y = g y<VAR>hx₃ : f x = g x<VAR>u : ℝ<VAR>hu : u ∈ Set.Icc (b * x) x<GOAL>g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x y<VAR>a b : X<VAR>γ : Path a b<GOAL>γ.extend (min 0 1) = a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x✝ y<VAR>a b : X<VAR>γ : Path a b<VAR>x : ↑I<GOAL>(γ.truncate 0 1) x = (γ.cast ⋯ ⋯) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x✝ y<VAR>a b : X<VAR>γ : Path a b<VAR>x : ↑I<GOAL>(γ.truncate 0 1) x = γ x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x✝ y<VAR>a b : X<VAR>γ : Path a b<VAR>x : ↑I<VAR>this : ↑x ∈ Icc 0 1<GOAL>(γ.truncate 0 1) x = γ x
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddMonoid R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < y.orderTop<GOAL>(x + y).orderTop = x.orderTop
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddMonoid R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < y.orderTop<VAR>hx : x ≠ 0<GOAL>(x + y).orderTop = x.orderTop
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddMonoid R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < y.orderTop<VAR>hx : x ≠ 0<VAR>g : Γ := ⋯.min ⋯<GOAL>(x + y).orderTop = x.orderTop
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddMonoid R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < y.orderTop<VAR>hx : x ≠ 0<VAR>g : Γ := ⋯.min ⋯<VAR>hcxyne : (x + y).coeff g ≠ 0<GOAL>(x + y).orderTop = x.orderTop
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddMonoid R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < y.orderTop<VAR>hx : x ≠ 0<VAR>g : Γ := ⋯.min ⋯<VAR>hcxyne : (x + y).coeff g ≠ 0<VAR>hxyx : (x + y).orderTop ≤ x.orderTop<GOAL>(x + y).orderTop = x.orderTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : CommSemiring β<VAR>hf : SuperpolynomialDecay l k f<VAR>z : ℕ<VAR>s : Set β<VAR>hs : IsOpen s<VAR>hs0 : 0 ∈ s<VAR>x : α<VAR>hx : x ∈ (fun a => k a ^ (z + 1) * f a) ⁻¹' s<GOAL>x ∈ (fun a => k a ^ z * (k * f) a) ⁻¹' s
<VAR>α : Type u_1<VAR>a✝ b✝ c✝ d : α<VAR>inst✝¹ : MulZeroClass α<VAR>inst✝ : PartialOrder α<VAR>h✝ : ContravariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x x_1 => x < x_1<VAR>a : { x // 0 ≤ x }<VAR>b c : α<VAR>h : b * ↑a < c * ↑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 => y * ↑x) fun x x_1 => x < x_1<VAR>a : { x // 0 ≤ x }<VAR>b c : α<VAR>h : b * ↑a < c * ↑a<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 => y * ↑x) fun x x_1 => x < x_1<VAR>a : { x // 0 ≤ x }<VAR>b c : α<VAR>h : b * ↑a < c * ↑a<VAR>ha : 0 < ↑a<GOAL>b < c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>p q : α → Prop<VAR>x : α<GOAL>{x | x ∈ s ∧ p x} = {x | x ∈ s ∧ q x} ↔ ∀ x ∈ s, p x ↔ q x
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<GOAL>Measure.map (fun x => x * c) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<GOAL>Measure.map (fun x => c * x) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
<VAR>n : Type u_1<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Fintype K<VAR>M : Matrix n n K<GOAL>(M ^ Fintype.card K).trace = M.trace ^ Fintype.card K
<VAR>n : Type u_1<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Fintype K<VAR>M : Matrix n n K<VAR>h✝ : IsEmpty n<GOAL>(M ^ Fintype.card K).trace = M.trace ^ Fintype.card K
<VAR>n : Type u_1<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Fintype K<VAR>M : Matrix n n K<VAR>h✝ : Nonempty n<GOAL>(M ^ Fintype.card K).trace = M.trace ^ Fintype.card K
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f g : R⟦X⟧<GOAL>trunc n (f * ↑(trunc n g)) = trunc n (f * g)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : Cofork f g<GOAL>s.ι.app zero = g ≫ s.π
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<GOAL>(if hp : p = 0 then Eq.rec (motive := fun x x_1 => ↥(lp E x) → ℝ) (fun f => ↑⋯.toFinset.card) ⋯ f else if p = ⊤ then ⨆ i, ‖↑f i‖ else (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)) = (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p ∧ p < ⊤<VAR>f : ↥(lp E p)<GOAL>(if hp : p = 0 then Eq.rec (motive := fun x x_1 => ↥(lp E x) → ℝ) (fun f => ↑⋯.toFinset.card) ⋯ f else if p = ⊤ then ⨆ i, ‖↑f i‖ else (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)) = (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<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✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsPrincipalIdealRing R<VAR>N : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>h : I ≤ N.idealizer<VAR>x y : L<VAR>hy : y ∈ I<VAR>inst✝ : LieModule.IsTrivial ↥↑I ↥↑N<GOAL>(trace R M) (φ x ∘ₗ φ y) = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<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✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsPrincipalIdealRing R<VAR>N : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>h : I ≤ N.idealizer<VAR>x y : L<VAR>hy : y ∈ I<VAR>inst✝ : LieModule.IsTrivial ↥↑I ↥↑N<VAR>hy' : ∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N := fun m x_1 => N.lie_mem ((mem_idealizer N).mp (h hy) m)<GOAL>(trace R M) (φ x ∘ₗ φ y) = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<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✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsPrincipalIdealRing R<VAR>N : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>h : I ≤ N.idealizer<VAR>x y : L<VAR>hy : y ∈ I<VAR>inst✝ : LieModule.IsTrivial ↥↑I ↥↑N<VAR>hy' : ∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N := fun m x_1 => N.lie_mem ((mem_idealizer N).mp (h hy) m)<GOAL>(φ x ∘ₗ φ y).restrict hy' = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<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✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsPrincipalIdealRing R<VAR>N : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>h : I ≤ N.idealizer<VAR>x y : L<VAR>hy : y ∈ I<VAR>inst✝ : LieModule.IsTrivial ↥↑I ↥↑N<VAR>hy' : ∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N := fun m x_1 => N.lie_mem ((mem_idealizer N).mp (h hy) m)<VAR>n : ↥↑N<GOAL>⁅y, ↑n⁆ = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R B<VAR>f : R →+* S<VAR>inst✝ : Algebra.IsIntegral R A<VAR>h' : FiniteType R A<VAR>s : Finset A<VAR>hs : adjoin R ↑s = ⊤<GOAL>⊤.FG
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>K : ℝ<VAR>C : ℝ≥0 := doublingConstant μ<VAR>hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)<GOAL>∃ C, ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑C * μ (closedBall x ε)
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>K : ℝ<VAR>C : ℝ≥0 := doublingConstant μ<VAR>hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)<VAR>hK : K < 1<GOAL>∃ C, ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑C * μ (closedBall x ε)
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>K : ℝ<VAR>C : ℝ≥0 := doublingConstant μ<VAR>hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)<VAR>hK : 1 ≤ K<GOAL>∃ C, ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑C * μ (closedBall x ε)
<VAR>A : Type u_1<VAR>inst✝⁸ : PartialOrder A<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalRing A<VAR>inst✝³ : NormedAlgebra ℝ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℝ A<VAR>n : ℕ<VAR>a : A<VAR>ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x<VAR>ha₁ : autoParam (IsSelfAdjoint a) _auto✝<GOAL>log (a ^ n) = n • log a
<VAR>A : Type u_1<VAR>inst✝⁸ : PartialOrder A<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalRing A<VAR>inst✝³ : NormedAlgebra ℝ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℝ A<VAR>n : ℕ<VAR>a : A<VAR>ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x<VAR>ha₁ : autoParam (IsSelfAdjoint a) _auto✝<VAR>this : ∀ x ∈ spectrum ℝ a, x ≠ 0<GOAL>log (a ^ n) = n • log a