ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>r : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re<VAR>hs₁ : s ≠ 0<VAR>hs₂ : 0 < (s + 1).re<GOAL>HasSum (fun i => (s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s) (mellin F ((s + 1) / 2))
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>r : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re<VAR>hs₁ : s ≠ 0<VAR>hs₂ : 0 < (s + 1).re<VAR>hs₃ : s + 1 ≠ 0<GOAL>HasSum (fun i => (s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s) (mellin F ((s + 1) / 2))
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>r : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re<VAR>hs₁ : s ≠ 0<VAR>hs₂ : 0 < (s + 1).re<VAR>hs₃ : s + 1 ≠ 0<VAR>this : ∀ (i : ι) (t : ℝ), a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))<GOAL>HasSum (fun i => (s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s) (mellin F ((s + 1) / 2))
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>r : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re<VAR>hs₁ : s ≠ 0<VAR>hs₂ : 0 < (s + 1).re<VAR>hs₃ : s + 1 ≠ 0<VAR>this : ∀ (i : ι) (t : ℝ), a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))<VAR>i : ι<GOAL>(s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s = (s + 1).Gammaℝ * (a i * ↑(r i)) / ↑|r i| ^ (s + 1)
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>r : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re<VAR>hs₁ : s ≠ 0<VAR>hs₂ : 0 < (s + 1).re<VAR>hs₃ : s + 1 ≠ 0<VAR>this : ∀ (i : ι) (t : ℝ), a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))<GOAL>Summable fun i => ‖a i * ↑(r i)‖ / |r i| ^ (s + 1).re
<VAR>ι : Type u_1<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>s : Finset ι<VAR>a : ι → ℤ<VAR>hs : s.card = 2 * p - 1<GOAL>∃ t ⊆ s, t.card = p ∧ ↑p ∣ ∑ i ∈ t, a i
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>x✝ : α 0<VAR>q : (i : Fin (n + 1)) → α i<VAR>p✝ : (i : Fin n) → α i.succ<VAR>i✝ : Fin n<VAR>y : α i✝.succ<VAR>z : α 0<VAR>inst✝ : (i : Fin (n + 1)) → Preorder (α i)<VAR>i : Fin (n + 1)<VAR>x : α i<VAR>p : (j : Fin n) → α (i.succAbove j)<VAR>q₁ q₂ : (j : Fin (n + 1)) → α j<GOAL>i.insertNth x p ∈ Icc q₁ q₂ ↔ x ∈ Icc (q₁ i) (q₂ i) ∧ p ∈ Icc (fun j => q₁ (i.succAbove j)) fun j => q₂ (i.succAbove j)
<VAR>R : CommRingCat<GOAL>(locallyRingedSpaceMap (𝟙 R)).val = (𝟙 (locallyRingedSpaceObj R)).val
<VAR>R : CommRingCat<GOAL>𝟙 (sheafedSpaceObj R) = (𝟙 (locallyRingedSpaceObj R)).val
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : NonUnitalSemiring A<VAR>inst✝² : Module R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>x : ↥(unitsFstOne R A)<GOAL>equiv.symm (equiv (↑↑x).snd * equiv (↑↑x⁻¹).snd) = equiv.symm 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : NonUnitalSemiring A<VAR>inst✝² : Module R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>x : ↥(unitsFstOne R A)<GOAL>equiv.symm (equiv (↑↑x⁻¹).snd * equiv (↑↑x).snd) = equiv.symm 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : NonUnitalSemiring A<VAR>inst✝² : Module R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>x : (PreQuasiregular A)ˣ<GOAL>(1 + ↑(equiv.symm ↑x)) * (1 + ↑(equiv.symm ↑x⁻¹)) = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : NonUnitalSemiring A<VAR>inst✝² : Module R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>x : (PreQuasiregular A)ˣ<GOAL>(1 + ↑(equiv.symm ↑x)) * (1 + ↑(equiv.symm ↑x⁻¹)) = 1 + ↑((↑x⁻¹).val + (↑x).val + (↑x).val * (↑x⁻¹).val)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : NonUnitalSemiring A<VAR>inst✝² : Module R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>x : (PreQuasiregular A)ˣ<GOAL>1 = 1 + ↑0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : NonUnitalSemiring A<VAR>inst✝² : Module R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>x : (PreQuasiregular A)ˣ<GOAL>(1 + ↑(equiv.symm ↑x⁻¹)) * (1 + ↑(equiv.symm ↑x)) = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : NonUnitalSemiring A<VAR>inst✝² : Module R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>x : (PreQuasiregular A)ˣ<GOAL>(1 + ↑(equiv.symm ↑x⁻¹)) * (1 + ↑(equiv.symm ↑x)) = 1 + ↑((↑x).val + (↑x⁻¹).val + (↑x⁻¹).val * (↑x).val)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : NonUnitalSemiring A<VAR>inst✝² : Module R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>x : ↥(unitsFstOne R A)<GOAL>↑↑((fun x => ⟨{ val := 1 + ↑(equiv.symm ↑x), inv := 1 + ↑(equiv.symm ↑x⁻¹), val_inv := ⋯, inv_val := ⋯ }, ⋯⟩) ((fun x => { val := equiv (↑↑x).snd, inv := equiv (↑↑x⁻¹).snd, val_inv := ⋯, inv_val := ⋯ }) x)) = ↑↑x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : NonUnitalSemiring A<VAR>inst✝² : Module R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>x : (PreQuasiregular A)ˣ<GOAL>↑((fun x => { val := equiv (↑↑x).snd, inv := equiv (↑↑x⁻¹).snd, val_inv := ⋯, inv_val := ⋯ }) ((fun x => ⟨{ val := 1 + ↑(equiv.symm ↑x), inv := 1 + ↑(equiv.symm ↑x⁻¹), val_inv := ⋯, inv_val := ⋯ }, ⋯⟩) x)) = ↑x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<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>n : ℕ<VAR>p : ContinuousMultilinearMap 𝕜 (fun i => E) F<VAR>h : (fun y => p fun x => y) =O[𝓝 0] fun y => ‖y‖ ^ (n + 1)<VAR>y : E<GOAL>(p fun x => y) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<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>n : ℕ<VAR>p : ContinuousMultilinearMap 𝕜 (fun i => E) F<VAR>h : (fun y => p fun x => y) =O[𝓝 0] fun y => ‖y‖ ^ (n + 1)<VAR>y : E<VAR>c : ℝ<VAR>c_pos : c > 0<VAR>hc : IsBigOWith c (𝓝 0) (fun y => p fun x => y) fun y => ‖y‖ ^ (n + 1)<GOAL>(p fun x => y) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<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>n : ℕ<VAR>p : ContinuousMultilinearMap 𝕜 (fun i => E) F<VAR>h : (fun y => p fun x => y) =O[𝓝 0] fun y => ‖y‖ ^ (n + 1)<VAR>y : E<VAR>c : ℝ<VAR>c_pos : c > 0<VAR>hc : IsBigOWith c (𝓝 0) (fun y => p fun x => y) fun y => ‖y‖ ^ (n + 1)<VAR>t : Set E<VAR>ht : ∀ y ∈ t, ‖p fun x => y‖ ≤ c * ‖‖y‖ ^ (n + 1)‖<VAR>t_open : IsOpen t<VAR>z_mem : 0 ∈ t<GOAL>(p fun x => y) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<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>n : ℕ<VAR>p : ContinuousMultilinearMap 𝕜 (fun i => E) F<VAR>h : (fun y => p fun x => y) =O[𝓝 0] fun y => ‖y‖ ^ (n + 1)<VAR>y : E<VAR>c : ℝ<VAR>c_pos : c > 0<VAR>hc : IsBigOWith c (𝓝 0) (fun y => p fun x => y) fun y => ‖y‖ ^ (n + 1)<VAR>t : Set E<VAR>ht : ∀ y ∈ t, ‖p fun x => y‖ ≤ c * ‖‖y‖ ^ (n + 1)‖<VAR>t_open : IsOpen t<VAR>z_mem : 0 ∈ t<VAR>δ : ℝ<VAR>δ_pos : δ > 0<VAR>δε : Metric.ball 0 δ ⊆ t<GOAL>(p fun x => y) = 0
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Fintype ι₁<VAR>inst✝¹ : Finite ι₂<VAR>inst✝ : DecidableEq ι₁<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>i : ι₂<VAR>c : ι₁ →₀ R<GOAL>(eval ⇑c) (toMvPolynomial b₁ b₂ f i) = (b₂.repr (f (b₁.repr.symm c))) i
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X : C<VAR>j : J<GOAL>(rightDistributor f X).hom ≫ biproduct.π (fun j => f j ⊗ X) j = biproduct.π f j ▷ X
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr : Tendsto r atTop (𝓝 0)<VAR>hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i<GOAL>blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr : Tendsto r atTop (𝓝 0)<VAR>hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i<VAR>h₁ : blimsup (fun i => cthickening (r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p<GOAL>blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr : Tendsto r atTop (𝓝 0)<VAR>hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i<VAR>h₁ : blimsup (fun i => cthickening (r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p<VAR>h₂ : blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => cthickening (r i) (s i)) atTop p<GOAL>blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i<VAR>h₁ : blimsup (fun i => cthickening (r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p<VAR>h₂ : blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => cthickening (r i) (s i)) atTop p<VAR>hr : Tendsto (fun i => M * r i) atTop (𝓝 0)<GOAL>blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>h₁ : blimsup (fun i => cthickening (r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p<VAR>h₂ : blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => cthickening (r i) (s i)) atTop p<VAR>hr : Tendsto (fun i => M * r i) atTop (𝓝 0)<VAR>hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < M * r i<GOAL>blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>h₁ : blimsup (fun i => cthickening (r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p<VAR>h₂ : blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => cthickening (r i) (s i)) atTop p<VAR>hr : Tendsto (fun i => M * r i) atTop (𝓝 0)<VAR>hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < M * r i<VAR>h₃ : blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (M * r i) (s i)) atTop p<GOAL>blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.112788, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X✝ Y✝ : Split C<VAR>Φ : X✝ ⟶ Y✝<VAR>n : ℕ<GOAL>Φ.f n ≫ (Y✝.s.cofan (op [n])).inj (Splitting.IndexSet.id (op [n])) ≫ PInfty.f n = ((X✝.s.cofan (op [n])).inj (Splitting.IndexSet.id (op [n])) ≫ PInfty.f n) ≫ PInfty.f n ≫ Φ.F.app (op [n])
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.112788, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X✝ Y✝ : Split C<VAR>Φ : X✝ ⟶ Y✝<VAR>n : ℕ<GOAL>Φ.f n ≫ (Y✝.s.cofan (op [n])).inj (Splitting.IndexSet.id (op [n])) ≫ PInfty.f n = (X✝.s.cofan (op [n])).inj (Splitting.IndexSet.id (op [n])) ≫ PInfty.f n ≫ Φ.F.app (op [n])
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.112788, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X✝ Y✝ : Split C<VAR>Φ : X✝ ⟶ Y✝<VAR>n : ℕ<GOAL>(X✝.s.cofan (op [n])).inj (Splitting.IndexSet.id (op [n])) ≫ Φ.F.app (op [n]) ≫ PInfty.f n = (X✝.s.cofan (op [n])).inj (Splitting.IndexSet.id (op [n])) ≫ PInfty.f n ≫ Φ.F.app (op [n])
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>x : ↥M<GOAL>↑((toInvSubmonoid M S) x) = mk' S 1 x
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>x : ↥M<GOAL>↑((toInvSubmonoid M S) x) * (algebraMap R S) ↑x = mk' S 1 x * (algebraMap R S) ↑x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<GOAL>dist p ↑((orthogonalProjection s) p) = 0 ↔ p ∈ s
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : AddGroupWithOne α<VAR>inst✝ : CharZero α<VAR>m n : ℤ<GOAL>↑n = 1 ↔ n = 1
<VAR>n : ℤ<VAR>hn : n.natAbs ≠ 1<GOAL>∃ p, Prime p ∧ p ∣ n
<VAR>n : ℤ<VAR>hn : n.natAbs ≠ 1<VAR>p : ℕ<VAR>pp : Nat.Prime p<VAR>pd : p ∣ n.natAbs<GOAL>∃ p, Prime p ∧ p ∣ n
<VAR>X✝ Y✝ Z X Y : TopCat<VAR>H : X ≅ Y<VAR>U : Opens ↑Y<GOAL>(𝟭 (Opens ↑Y)).obj U = (map H.hom ⋙ map H.inv).obj U
<VAR>X✝ Y✝ Z X Y : TopCat<VAR>H : X ≅ Y<VAR>U : Opens ↑X<GOAL>(map H.inv ⋙ map H.hom).obj U = (𝟭 (Opens ↑X)).obj U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set α<GOAL>f '' s ⊆ range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set α<GOAL>f '' s ⊆ f '' univ
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : ∀ (p : ℕ), a.factorization p = b.factorization p<GOAL>a.primeFactorsList ~ b.primeFactorsList
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<GOAL>Monotone (f ∘ ⇑(sort f))
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<GOAL>Monotone (graph.proj ∘ ⇑(graphEquiv₂ f))
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>inst✝¹² : Fintype m<VAR>inst✝¹¹ : Fintype m₁<VAR>inst✝¹⁰ : Fintype m₂<VAR>inst✝⁹ : Fintype n<VAR>inst✝⁸ : Fintype n₁<VAR>inst✝⁷ : Fintype n₂<VAR>inst✝⁶ : DecidableEq m<VAR>inst✝⁵ : DecidableEq m₁<VAR>inst✝⁴ : DecidableEq m₂<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq n₁<VAR>inst✝¹ : DecidableEq n₂<VAR>inst✝ : CommRing R<VAR>e : n ≃ n₁ ⊕ n₂<VAR>A₁ : Matrix n n₁ R<VAR>A₂ : Matrix n n₂ R<VAR>B₁ : Matrix n₁ n R<VAR>B₂ : Matrix n₂ n R<GOAL>A₁.fromColumns A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromColumns A₂ = 1
<VAR>d : ℤ<VAR>h_nonsquare : ∀ (n : ℤ), d ≠ n * n<VAR>a : ℤ√d<GOAL>a.norm = 0 ↔ a = 0
<VAR>d : ℤ<VAR>h_nonsquare : ∀ (n : ℤ), d ≠ n * n<VAR>a : ℤ√d<VAR>ha : a.norm = 0<GOAL>a.re = re 0 ∧ a.im = im 0
<VAR>d : ℤ<VAR>h_nonsquare : ∀ (n : ℤ), d ≠ n * n<VAR>a : ℤ√d<VAR>ha : a.re * a.re - d * a.im * a.im = 0<GOAL>a.re = re 0 ∧ a.im = im 0
<VAR>d : ℤ<VAR>h_nonsquare : ∀ (n : ℤ), d ≠ n * n<VAR>a : ℤ√d<VAR>ha : a.re * a.re = d * a.im * a.im<GOAL>a.re = re 0 ∧ a.im = im 0
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>inst✝ : FiniteDimensional ℝ F<VAR>hf : LipschitzOnWith C f s<GOAL>∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g✝ : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>inst✝ : FiniteDimensional ℝ F<VAR>hf : LipschitzOnWith C f s<VAR>g : E → ℝ<VAR>g_lip : LipschitzWith C g<VAR>hg : EqOn f g s<GOAL>∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g✝ : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>inst✝ : FiniteDimensional ℝ F<VAR>hf : LipschitzOnWith C f s<VAR>g : E → ℝ<VAR>g_lip : LipschitzWith C g<VAR>hg : EqOn f g s<VAR>x : E<VAR>hx : DifferentiableAt ℝ g x<VAR>xs : x ∈ s<GOAL>DifferentiableWithinAt ℝ f s x
<VAR>n m d : ℕ<VAR>hm : n ∣ m<VAR>hd : m ∣ d<GOAL>(unitsMap hm).comp (unitsMap hd) = unitsMap ⋯
<VAR>n m d : ℕ<VAR>hm : n ∣ m<VAR>hd : m ∣ d<GOAL>(Units.map ↑(castHom hm (ZMod n))).comp (Units.map ↑(castHom hd (ZMod m))) = Units.map ↑(castHom ⋯ (ZMod n))
<VAR>n m d : ℕ<VAR>hm : n ∣ m<VAR>hd : m ∣ d<GOAL>Units.map ((↑(castHom hm (ZMod n))).comp ↑(castHom hd (ZMod m))) = Units.map ↑(castHom ⋯ (ZMod n))
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>inst✝¹ : IsFiniteMeasure ℙ<VAR>X : Ω → ℝ<VAR>inst✝ : HasPDF X ℙ volume<VAR>x : ℝ<GOAL>x * (pdf X ℙ volume x).toReal = (pdf X ℙ volume x).toReal * x
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h✝ h : F.Stable<VAR>h' : F'.Stable<VAR>e : F.N 0 = F'.N 0<GOAL>∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h✝ h : F.Stable<VAR>h' : F'.Stable<VAR>e : F.N 0 = F'.N 0<VAR>n₁ : ℕ<VAR>h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n<GOAL>∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h✝ h : F.Stable<VAR>h' : F'.Stable<VAR>e : F.N 0 = F'.N 0<VAR>n₁ : ℕ<VAR>h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n<VAR>n₂ : ℕ<VAR>h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n<GOAL>∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h✝ h : F.Stable<VAR>h' : F'.Stable<VAR>e : F.N 0 = F'.N 0<VAR>n₁ : ℕ<VAR>h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n<VAR>n₂ : ℕ<VAR>h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n<GOAL>∀ (n : ℕ), F.N (n + max n₁ n₂) ≤ F'.N n ∧ F'.N (n + max n₁ n₂) ≤ F.N n
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h✝ h : F.Stable<VAR>h' : F'.Stable<VAR>e : F.N 0 = F'.N 0<VAR>n₁ : ℕ<VAR>h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n<VAR>n₂ : ℕ<VAR>h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n<VAR>n : ℕ<GOAL>F.N (n + max n₁ n₂) ≤ F'.N n ∧ F'.N (n + max n₁ n₂) ≤ F.N n
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>S : Set (Set X)<VAR>hS : S.Finite<GOAL>closure (⋃₀ S) = ⋃ s ∈ S, closure s
<VAR>P : PFunctor.{u}<VAR>α : Type u<VAR>p : α → Prop<VAR>x : ↑P α<VAR>a : P.A<VAR>f : P.B a → α<VAR>xeq : x = ⟨a, f⟩<VAR>pf : ∀ (i : P.B a), p (f i)<GOAL>Liftp p x
<VAR>P : PFunctor.{u}<VAR>α : Type u<VAR>p : α → Prop<VAR>x : ↑P α<VAR>a : P.A<VAR>f : P.B a → α<VAR>xeq : x = ⟨a, f⟩<VAR>pf : ∀ (i : P.B a), p (f i)<GOAL>Subtype.val <$> ⟨a, fun i => ⟨f i, ⋯⟩⟩ = x
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H K : G.Subgraph<VAR>hH : H.Connected<VAR>hK : K.Connected<VAR>hn : (H ⊓ K).verts.Nonempty<GOAL>(H ⊔ K).Connected
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H K : G.Subgraph<VAR>hH : H.Connected<VAR>hK : K.Connected<VAR>hn : (H ⊓ K).verts.Nonempty<GOAL>∃ v, ∀ (w : ↑(H ⊔ K).verts), (H ⊔ K).coe.Reachable v w
<GOAL>Principal (fun x x_1 => x * x_1) 1
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>IsClosed (frontier s)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>IsClosed (closure s ∩ closure sᶜ)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[cocompact ℝ] fun x => |x| ^ (-b)<VAR>K : Compacts ℝ<GOAL>(fun x => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x => |x| ^ (-b)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[cocompact ℝ] fun x => |x| ^ (-b)<VAR>K : Compacts ℝ<VAR>r : ℝ<VAR>hr : ↑K ⊆ Metric.closedBall 0 r<GOAL>(fun x => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x => |x| ^ (-b)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[cocompact ℝ] fun x => |x| ^ (-b)<VAR>K : Compacts ℝ<VAR>r : ℝ<VAR>hr : ↑K ⊆ Icc (-r) r<GOAL>(fun x => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x => |x| ^ (-b)