ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>hG : ExponentExists G<VAR>he : exponent G ≠ 0<VAR>hne : (Set.range orderOf).Nonempty<VAR>hfin : (Set.range orderOf).Finite<VAR>t : G<VAR>ht : orderOf t = sSup (Set.range orderOf)<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>k : ℕ := (orderOf t).factorization p<VAR>hpe : k < (exponent G).factorization p<VAR>hk : k = (orderOf t).factorization p<VAR>g : G<VAR>hg : orderOf g = p ^ (exponent G).factorization p<VAR>hpk : p ^ k ∣ orderOf t<VAR>hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k<VAR>a : ℕ<VAR>ha : (exponent G).factorization p = k + a + 1<VAR>hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)<GOAL>p ^ (orderOf t).factorization p ∣ orderOf t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : DivisionMonoid K<VAR>inst✝ : HasDistribNeg K<VAR>a b : K<GOAL>(-a)⁻¹ = -a⁻¹
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h : (∫⁻ (a : α), (∑' (i : ℕ), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i<GOAL>∀ᵐ (x : α) ∂μ, ∑' (i : ℕ), ↑‖f (i + 1) x - f i x‖₊ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h : (∫⁻ (a : α), (∑' (i : ℕ), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i<VAR>hp_pos : 0 < p<GOAL>∀ᵐ (x : α) ∂μ, ∑' (i : ℕ), ↑‖f (i + 1) x - f i x‖₊ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h : (∫⁻ (a : α), (∑' (i : ℕ), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i<VAR>hp_pos : 0 < p<VAR>h_integral : ∫⁻ (a : α), (∑' (i : ℕ), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ < ⊤<GOAL>∀ᵐ (x : α) ∂μ, ∑' (i : ℕ), ↑‖f (i + 1) x - f i x‖₊ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h : (∫⁻ (a : α), (∑' (i : ℕ), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i<VAR>hp_pos : 0 < p<VAR>h_integral : ∫⁻ (a : α), (∑' (i : ℕ), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ < ⊤<VAR>rpow_ae_lt_top : ∀ᵐ (x : α) ∂μ, (∑' (i : ℕ), ↑‖f (i + 1) x - f i x‖₊) ^ p < ⊤<GOAL>∀ᵐ (x : α) ∂μ, ∑' (i : ℕ), ↑‖f (i + 1) x - f i x‖₊ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h : (∫⁻ (a : α), (∑' (i : ℕ), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i<VAR>hp_pos : 0 < p<VAR>h_integral : ∫⁻ (a : α), (∑' (i : ℕ), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ < ⊤<VAR>rpow_ae_lt_top : ∀ᵐ (x : α) ∂μ, (∑' (i : ℕ), ↑‖f (i + 1) x - f i x‖₊) ^ p < ⊤<VAR>x : α<VAR>hx : (∑' (i : ℕ), ↑‖f (i + 1) x - f i x‖₊) ^ p < ⊤<GOAL>∑' (i : ℕ), ↑‖f (i + 1) x - f i x‖₊ < ⊤
<VAR>α : Type u_1<VAR>R✝ : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>R : Type u_9<VAR>inst✝ : NonAssocSemiring R<VAR>m : ℕ<GOAL>m • 1 = ↑m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ts : List α<GOAL>map (map f) ts.permutations' = (map f ts).permutations'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>E B I : Set α<GOAL>(N.comapOn E f).Indep I ↔ N.Indep (f '' I) ∧ InjOn f I ∧ I ⊆ E
<VAR>C : Type u'<VAR>inst✝³ : Category.{v', u'} C<VAR>J✝ : GrothendieckTopology C<VAR>R : Sheaf J✝ RingCat<VAR>inst✝² : HasWeakSheafify J✝ AddCommGrp<VAR>inst✝¹ : J✝.WEqualsLocallyBijective AddCommGrp<VAR>inst✝ : J✝.HasSheafCompose (forget₂ RingCat AddCommGrp)<VAR>I J : Type u<VAR>f : I → J<VAR>i : I<GOAL>sectionsMap (freeMap f) (freeSection i) = freeSection (f i)
<VAR>J : Type u_1<VAR>inst✝ : Category.{u_2, u_1} J<VAR>K : J ⥤ Type u<VAR>c : Cocone K<VAR>hc : IsColimit c<VAR>lc : Cocone (K ⋙ uliftFunctor.{v, u})<VAR>f : c.pt → lc.pt<GOAL>f = descFun hc lc ↔ ∀ (j : J), f ∘ c.ι.app j = lc.ι.app j ∘ ULift.up
<VAR>J : Type u_1<VAR>inst✝ : Category.{u_2, u_1} J<VAR>K : J ⥤ Type u<VAR>c : Cocone K<VAR>hc : IsColimit c<VAR>lc : Cocone (K ⋙ uliftFunctor.{v, u})<VAR>f : c.pt → lc.pt<GOAL>f = descFun hc lc → ∀ (j : J), f ∘ c.ι.app j = lc.ι.app j ∘ ULift.up
<VAR>J : Type u_1<VAR>inst✝ : Category.{u_2, u_1} J<VAR>K : J ⥤ Type u<VAR>c : Cocone K<VAR>hc : IsColimit c<VAR>lc : Cocone (K ⋙ uliftFunctor.{v, u})<VAR>f : c.pt → lc.pt<VAR>he : ∀ (j : J), f ∘ c.ι.app j = lc.ι.app j ∘ ULift.up<VAR>x : c.pt<GOAL>x ∈ descSet hc {f x}
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<GOAL>X.Separable
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<GOAL>IsCoprime X 1
<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>m : MeasurableSpace α<VAR>f : β → Set α<VAR>s : Set β<VAR>hs : s.Countable<VAR>h : ∀ b ∈ s, MeasurableSet (f b)<GOAL>MeasurableSet (⋃ b ∈ s, f b)
<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>m : MeasurableSpace α<VAR>f : β → Set α<VAR>s : Set β<VAR>hs : s.Countable<VAR>h : ∀ b ∈ s, MeasurableSet (f b)<GOAL>MeasurableSet (⋃ x, f ↑x)
<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>m : MeasurableSpace α<VAR>f : β → Set α<VAR>s : Set β<VAR>hs : s.Countable<VAR>h : ∀ b ∈ s, MeasurableSet (f b)<VAR>this : Countable ↑s<GOAL>MeasurableSet (⋃ x, f ↑x)
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3<GOAL>(fun a => a * Q z ^ 3) (P y) = (fun a => a * Q z ^ 3) (W'.negY P)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>f✝ : α → α<VAR>s : Set α<VAR>μ✝ : Measure α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>inst✝ : OpensMeasurableSpace α<VAR>f : α → α<VAR>μ : Measure α<VAR>h : Conservative f μ<GOAL>∀ᵐ (x : α) ∂μ, ∀ s ∈ 𝓝 x, ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>f✝ : α → α<VAR>s : Set α<VAR>μ✝ : Measure α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>inst✝ : OpensMeasurableSpace α<VAR>f : α → α<VAR>μ : Measure α<VAR>h : Conservative f μ<VAR>this : ∀ s ∈ countableBasis α, ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s<GOAL>∀ᵐ (x : α) ∂μ, ∀ s ∈ 𝓝 x, ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>f✝ : α → α<VAR>s✝ : Set α<VAR>μ✝ : Measure α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>inst✝ : OpensMeasurableSpace α<VAR>f : α → α<VAR>μ : Measure α<VAR>h : Conservative f μ<VAR>this : ∀ s ∈ countableBasis α, ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s<VAR>x : α<VAR>hx : ∀ i ∈ countableBasis α, x ∈ i → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ i<VAR>s : Set α<VAR>hs : s ∈ 𝓝 x<GOAL>∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>f✝ : α → α<VAR>s✝ : Set α<VAR>μ✝ : Measure α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>inst✝ : OpensMeasurableSpace α<VAR>f : α → α<VAR>μ : Measure α<VAR>h : Conservative f μ<VAR>this : ∀ s ∈ countableBasis α, ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s<VAR>x : α<VAR>hx : ∀ i ∈ countableBasis α, x ∈ i → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ i<VAR>s : Set α<VAR>hs : s ∈ 𝓝 x<VAR>o : Set α<VAR>hoS : o ∈ countableBasis α<VAR>hxo : x ∈ o<VAR>hos : o ⊆ s<GOAL>∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1
<VAR>n : ℕ<VAR>α : Type u<VAR>σ : Perm (Fin n)<VAR>f : Fin n → α<GOAL>ofFn (f ∘ ⇑σ) ~ ofFn f
<VAR>n : ℕ<VAR>α : Type u<VAR>σ : Perm (Fin n)<VAR>f : Fin n → α<GOAL>map f (map (⇑σ) (finRange n)) ~ map f (finRange n)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>eval (v i) (derivative (nodal s v)) = eval (v i) (nodal (s.erase i) v)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>∑ x ∈ s.erase i, eval (v i) (nodal (s.erase x) v) = 0
<VAR>x : ℝ<VAR>h : 1 ≤ x<GOAL>expNegInvGlue x = expNegInvGlue x + expNegInvGlue (1 - x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<GOAL>HasMFDerivWithinAt I I' f univ x f' ↔ HasMFDerivAt I I' f x f'
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocMod hp (a + p) b = toIocMod hp a b + p
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>A : ι → Type u_3<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GMonoid A<VAR>l : List α<VAR>f : α → GradedMonoid A<GOAL>(List.map f l).prod = mk (l.dProdIndex fun i => (f i).fst) (l.dProd (fun i => (f i).fst) fun i => (f i).snd)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>A : ι → Type u_3<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GMonoid A<VAR>l : List α<VAR>f : α → GradedMonoid A<GOAL>(List.map f l).prod = (List.map (fun a => ⟨(f a).fst, (f a).snd⟩) l).prod
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : HasContDiffBump E<VAR>inst✝⁴ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<GOAL>tsupport (f.normed μ) = closedBall c f.rOut
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>inst✝ : Field k<GOAL>X = normalize X
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>s : Finset ι<VAR>f : ι → Set α<GOAL>(⋃ i ∈ s, f i).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedCommRing β<VAR>inst✝ : OrderTopology β<VAR>hf : SuperpolynomialDecay l k f<VAR>hfg : abs ∘ g ≤ᶠ[l] abs ∘ f<GOAL>SuperpolynomialDecay l k g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedCommRing β<VAR>inst✝ : OrderTopology β<VAR>hf : ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)<VAR>hfg : abs ∘ g ≤ᶠ[l] abs ∘ f<GOAL>∀ (n : ℕ), Tendsto (fun a => |k a ^ n * g a|) l (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedCommRing β<VAR>inst✝ : OrderTopology β<VAR>hf : ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)<VAR>hfg : abs ∘ g ≤ᶠ[l] abs ∘ f<VAR>z : ℕ<VAR>x : α<VAR>hx : (abs ∘ g) x ≤ (abs ∘ f) x<GOAL>|k x ^ z * g x| ≤ |k x ^ z * 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✝² : Module.Finite R L<VAR>inst✝¹ : Module.Free R L<VAR>inst✝ : Nontrivial R<GOAL>(φ.polyCharpoly b).coeff φ.nilRank ≠ 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✝² : Module.Finite R L<VAR>inst✝¹ : Module.Free R L<VAR>inst✝ : Nontrivial R<GOAL>(φ.polyCharpoly b).coeff (φ.polyCharpoly b).natTrailingDegree ≠ 0
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : J(a | b) = -1<VAR>x✝ : IsSquare ↑a<VAR>r : ZMod b<VAR>ha : ↑a = r * r<GOAL>False
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : J(a | b) = -1<VAR>x✝ : IsSquare ↑a<VAR>r : ZMod b<VAR>ha : a % ↑b = r.valMinAbs ^ 2 % ↑b<GOAL>False
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : J(a | b) = -1<VAR>x✝ : IsSquare ↑a<VAR>r : ZMod b<VAR>ha : a % ↑b = r.valMinAbs ^ 2 % ↑b<GOAL>0 ≤ -1
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : J(a | b) = -1<VAR>x✝ : IsSquare ↑a<VAR>r : ZMod b<VAR>ha : a % ↑b = r.valMinAbs ^ 2 % ↑b<GOAL>0 ≤ J(r.valMinAbs | b) ^ 2
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace G✝<VAR>inst✝⁵ : Group G✝<VAR>inst✝⁴ : TopologicalGroup G✝<VAR>inst✝³ : TopologicalSpace α<VAR>f : α → G✝<VAR>s : Set α<VAR>x : α<VAR>G : Type u_1<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : MulOneClass G<VAR>inst✝ : ContinuousMul G<VAR>g h : G<VAR>hg : g ∈ connectedComponent 1<VAR>hh : h ∈ connectedComponent 1<GOAL>g * h ∈ connectedComponent 1
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace G✝<VAR>inst✝⁵ : Group G✝<VAR>inst✝⁴ : TopologicalGroup G✝<VAR>inst✝³ : TopologicalSpace α<VAR>f : α → G✝<VAR>s : Set α<VAR>x : α<VAR>G : Type u_1<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : MulOneClass G<VAR>inst✝ : ContinuousMul G<VAR>g h : G<VAR>hg : g ∈ connectedComponent 1<VAR>hh : h ∈ connectedComponent 1<GOAL>g * h ∈ connectedComponent g
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace G✝<VAR>inst✝⁵ : Group G✝<VAR>inst✝⁴ : TopologicalGroup G✝<VAR>inst✝³ : TopologicalSpace α<VAR>f : α → G✝<VAR>s : Set α<VAR>x : α<VAR>G : Type u_1<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : MulOneClass G<VAR>inst✝ : ContinuousMul G<VAR>g h : G<VAR>hg : g ∈ connectedComponent 1<VAR>hh : h ∈ connectedComponent 1<VAR>hmul : g ∈ connectedComponent (g * h)<GOAL>g * h ∈ connectedComponent g
<VAR>m n✝ n : ℕ<VAR>u : (ZMod (n + 1))ˣ<GOAL>(↑u).val.Coprime (n + 1)
<VAR>m n✝ n : ℕ<VAR>u : (ZMod (n + 1))ˣ<GOAL>(↑u).val * (↑u⁻¹).val ≡ 1 [MOD n + 1]
<VAR>m n✝ n : ℕ<VAR>u : (ZMod (n + 1))ˣ<VAR>this : ↑(u * u⁻¹) = ↑1<GOAL>(↑u).val * (↑u⁻¹).val ≡ 1 [MOD n + 1]
<VAR>m n✝ n : ℕ<VAR>u : (ZMod (n + 1))ˣ<VAR>this : ↑(u * u⁻¹) = 1<GOAL>(↑u).val * (↑u⁻¹).val ≡ 1 [MOD n + 1]
<VAR>m n✝ n : ℕ<VAR>u : (ZMod (n + 1))ˣ<VAR>this : ↑(u * u⁻¹) = 1<GOAL>↑((↑u).val * (↑u⁻¹).val) = ↑(u * u⁻¹)
<VAR>m n✝ n : ℕ<VAR>u : (ZMod (n + 1))ˣ<GOAL>↑((↑u).val * (↑u⁻¹).val) = ↑(u * u⁻¹)
<VAR>m n✝ n : ℕ<VAR>u : (ZMod (n + 1))ˣ<GOAL>↑((↑u).val * (↑u⁻¹).val) = ↑(↑(u * u⁻¹)).val
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>hφ : φ.IsSymmetric<VAR>e : σ ≃ τ<VAR>x✝ : Perm τ<GOAL>(rename ⇑x✝) ((rename ⇑e) φ) = (rename ⇑e) φ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>hφ : φ.IsSymmetric<VAR>e : σ ≃ τ<VAR>x✝ : Perm τ<GOAL>(rename ⇑e.symm) ((rename ⇑x✝) ((rename ⇑e) φ)) = (rename ⇑e.symm) ((rename ⇑e) φ)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>hφ : φ.IsSymmetric<VAR>e : σ ≃ τ<VAR>x✝ : Perm τ<GOAL>(rename ⇑((e.trans x✝).trans e.symm)) φ = φ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : InfSet α<VAR>f : ι → α<VAR>hf : BddBelow (range f)<GOAL>↑(⨅ i, f i) = ⨅ i, ↑(f i)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : ContinuousMul G<VAR>Γ : Subgroup G<VAR>x : G ⧸ Γ<GOAL>Continuous fun g => g • x
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : ContinuousMul G<VAR>Γ : Subgroup G<VAR>z✝ : G<GOAL>Continuous fun g => g • ↑z✝
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : ClosedIicTopology α<VAR>inst✝ : NoMaxOrder α<VAR>f : β → α<VAR>s : Set β<VAR>hs : IsCompact s<VAR>hf : ContinuousOn f s<VAR>a : α<VAR>hf' : ∀ b ∈ s, a < f b<GOAL>∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : ClosedIicTopology α<VAR>inst✝ : NoMaxOrder α<VAR>f : β → α<VAR>a : α<VAR>hs : IsCompact ∅<VAR>hf : ContinuousOn f ∅<VAR>hf' : ∀ b ∈ ∅, a < f b<GOAL>∃ a', a < a' ∧ ∀ b ∈ ∅, a' ≤ f b
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : ClosedIicTopology α<VAR>inst✝ : NoMaxOrder α<VAR>f : β → α<VAR>s : Set β<VAR>hs : IsCompact s<VAR>hf : ContinuousOn f s<VAR>a : α<VAR>hf' : ∀ b ∈ s, a < f b<VAR>hs' : s.Nonempty<GOAL>∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t✝ : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<GOAL>μ s + μ (t \ s) = μ (s ∪ t)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X₁✝ X₂✝ Y₁✝ Y₂✝ : C<VAR>f₁₁✝ : X₁✝ ⟶ Y₁✝<VAR>f₁₂✝ : X₁✝ ⟶ Y₂✝<VAR>f₂₁✝ : X₂✝ ⟶ Y₁✝<VAR>f₂₂✝ : X₂✝ ⟶ Y₂✝<VAR>X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C<VAR>f₁₁ : X₁ ⟶ Y₁<VAR>f₁₂ : X₁ ⟶ Y₂<VAR>f₂₁ : X₂ ⟶ Y₁<VAR>f₂₂ : X₂ ⟶ Y₂<VAR>g₁₁ : Y₁ ⟶ Z₁<VAR>g₁₂ : Y₁ ⟶ Z₂<VAR>g₂₁ : Y₂ ⟶ Z₁<VAR>g₂₂ : Y₂ ⟶ Z₂<GOAL>(biprod.fst ≫ f₁₁ ≫ biprod.inl + biprod.fst ≫ f₁₂ ≫ biprod.inr + biprod.snd ≫ f₂₁ ≫ biprod.inl + biprod.snd ≫ f₂₂ ≫ biprod.inr) ≫ (biprod.fst ≫ g₁₁ ≫ biprod.inl + biprod.fst ≫ g₁₂ ≫ biprod.inr + biprod.snd ≫ g₂₁ ≫ biprod.inl + biprod.snd ≫ g₂₂ ≫ biprod.inr) = biprod.fst ≫ (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) ≫ biprod.inl + biprod.fst ≫ (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) ≫ biprod.inr + biprod.snd ≫ (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) ≫ biprod.inl + biprod.snd ≫ (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) ≫ biprod.inr
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<GOAL>(mulEquivOfQuotient f).symm (f.mk' x y) = mk x y
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<GOAL>(mulEquivOfQuotient f).symm (f.mk' x y) = (monoidOf S).mk' x y
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : NonUnitalNonAssocSemiring A<VAR>inst✝⁴ : NonUnitalNonAssocSemiring B<VAR>inst✝³ : NonUnitalNonAssocSemiring C<VAR>inst✝² : Module R A<VAR>inst✝¹ : Module R B<VAR>inst✝ : Module R C<VAR>S T : NonUnitalSubalgebra R A<VAR>h : S.toSubmodule = T.toSubmodule<VAR>x : A<GOAL>x ∈ S ↔ x ∈ T
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>S : Finset ι<VAR>q : ι → R<VAR>hq : (↑S).Pairwise (IsCoprime on q)<VAR>hM : Module.IsTorsionBy R M (∏ i ∈ S, q i)<GOAL>DirectSum.IsInternal fun i => torsionBy R M (q ↑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>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>S : Finset ι<VAR>q : ι → R<VAR>hq : (↑S).Pairwise (IsCoprime on q)<VAR>hM : Module.IsTorsionBySet R M ↑(⨅ a ∈ S, Ideal.span {q a})<GOAL>DirectSum.IsInternal fun i => torsionBy R M (q ↑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>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>S : Finset ι<VAR>q : ι → R<VAR>hq : (↑S).Pairwise (IsCoprime on q)<VAR>hM : Module.IsTorsionBySet R M ↑(⨅ a ∈ S, Ideal.span {q a})<VAR>x✝ : { x // x ∈ S }<GOAL>torsionBy R M (q ↑x✝) = torsionBySet R M ↑(Ideal.span {q ↑x✝})
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y z : F<GOAL>⟪x, y - z⟫_𝕜 = ⟪x, y⟫_𝕜 - ⟪x, z⟫_𝕜
<VAR>m n : ℕ<GOAL>¬Even n ↔ n % 2 = 1
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<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>a b : R<VAR>x y : M<VAR>s : Set (Set M)<VAR>hs : DirectedOn (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ a ∈ s, LinearIndependent (ι := { x // x ∈ a }) R Subtype.val<GOAL>LinearIndependent R fun (x : ↑(⋃₀ s)) => ↑x
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<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>a b : R<VAR>x y : M<VAR>s : Set (Set M)<VAR>hs : DirectedOn (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ a ∈ s, LinearIndependent (ι := { x // x ∈ a }) R Subtype.val<GOAL>LinearIndependent R fun (x : ↑(⋃ i, ↑i)) => ↑x