ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>y : γ ⊕ δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>d : δ<VAR>w✝ : α<VAR>h₂ : (inl w✝).isLeft = true<VAR>h₁ : ∃ a c, r a c ∧ inl w✝ = inl a ∧ y = inl c<GOAL>∃ a c, r a c ∧ inl w✝ = inl a ∧ y = inl c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : T0Space β<VAR>f : α → β<VAR>h : UniformContinuous f<VAR>a : α<GOAL>lift' f (mk a) = f a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : ClosedIciTopology α<VAR>inst✝ : TopologicalSpace β<VAR>a b c : α<VAR>f : α → β<VAR>h : a < b<GOAL>ContinuousWithinAt f (Ico a b) a ↔ ContinuousWithinAt f (Ici a) a
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C<VAR>him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C<VAR>hz_re : z.re ≤ 0<VAR>hz_im : 0 ≤ z.im<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C<VAR>him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : (z * I).re ≤ 0<VAR>hz_im : 0 ≤ (z * I).im<GOAL>‖f (z * I)‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C<VAR>him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : 0 ≤ z.im<VAR>hz_im : 0 ≤ z.re<GOAL>‖f (z * I)‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)<VAR>hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C<VAR>him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : 0 ≤ z.im<VAR>hz_im : 0 ≤ z.re<VAR>H : MapsTo (fun x => x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)<VAR>c : ℝ<VAR>hc : c < 2<VAR>B : ℝ<VAR>hO : f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<GOAL>‖(f ∘ fun x => x * I) z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)<VAR>hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C<VAR>him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : 0 ≤ z.im<VAR>hz_im : 0 ≤ z.re<VAR>H : MapsTo (fun x => x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)<VAR>c : ℝ<VAR>hc : c < 2<VAR>B : ℝ<VAR>hO : f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<GOAL>(f ∘ fun x => x * I) =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)<VAR>hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C<VAR>him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : 0 ≤ z.im<VAR>hz_im : 0 ≤ z.re<VAR>H : MapsTo (fun x => x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)<VAR>c : ℝ<VAR>hc : c < 2<VAR>B : ℝ<VAR>hO : f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>x : ℝ<VAR>hx : 0 ≤ x<GOAL>‖(f ∘ fun x => x * I) (↑x * I)‖ ≤ C
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>J : Type u_4<VAR>inst✝² : Category.{u_5, u_1} C<VAR>inst✝¹ : Category.{u_7, u_2} D<VAR>inst✝ : Category.{u_6, u_3} E<VAR>X Y✝ : GradedObject J C<VAR>e : X ≅ Y✝<VAR>F : C ⥤ D ⥤ E<VAR>j : J<VAR>Y : D<GOAL>(F.map (e.inv j)).app Y ≫ (F.map (e.hom j)).app Y = 𝟙 ((F.obj (Y✝ j)).obj Y)
<VAR>n : Type u_1<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>S : Type u_2<VAR>inst✝ : LinearOrderedCommRing S<VAR>A : Matrix n n S<VAR>h1 : Pairwise fun i j => A i j < 0<VAR>h2 : ∀ (i : n), 0 < ∑ j : n, A i j<GOAL>A.det ≠ 0
<VAR>n : Type u_1<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>S : Type u_2<VAR>inst✝ : LinearOrderedCommRing S<VAR>A : Matrix n n S<VAR>h1 : Pairwise fun i j => A i j < 0<VAR>h2 : ∀ (i : n), 0 < ∑ j : n, A i j<GOAL>Aᵀ.det ≠ 0
<VAR>n : Type u_1<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>S : Type u_2<VAR>inst✝ : LinearOrderedCommRing S<VAR>A : Matrix n n S<VAR>h1 : Pairwise fun i j => A i j < 0<VAR>h2 : ∀ (i : n), 0 < ∑ j : n, A i j<GOAL>Pairwise fun i j => Aᵀ i j < 0
<VAR>n : Type u_1<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>S : Type u_2<VAR>inst✝ : LinearOrderedCommRing S<VAR>A : Matrix n n S<VAR>h1 : Pairwise fun i j => A i j < 0<VAR>h2 : ∀ (i : n), 0 < ∑ j : n, A i j<GOAL>∀ (j : n), 0 < ∑ i : n, Aᵀ i j
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.trailingCoeff * q.trailingCoeff ≠ 0<GOAL>(p * q).trailingDegree = p.trailingDegree + q.trailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.trailingCoeff * q.trailingCoeff ≠ 0<VAR>hp : p ≠ 0<GOAL>(p * q).trailingDegree = p.trailingDegree + q.trailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.trailingCoeff * q.trailingCoeff ≠ 0<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<GOAL>(p * q).trailingDegree = p.trailingDegree + q.trailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.trailingCoeff * q.trailingCoeff ≠ 0<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<GOAL>(p * q).trailingDegree ≤ p.trailingDegree + q.trailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.trailingCoeff * q.trailingCoeff ≠ 0<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<GOAL>(p * q).trailingDegree ≤ ↑(p.natTrailingDegree + q.natTrailingDegree)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.trailingCoeff * q.trailingCoeff ≠ 0<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<GOAL>(p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) ≠ 0
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<GOAL>(⨆ i, p i).toAddSubmonoid = ⨆ i, (p i).toAddSubmonoid
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>x : M<GOAL>x ∈ (⨆ i, p i).toAddSubmonoid → x ∈ ⨆ i, (p i).toAddSubmonoid
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>x : M<GOAL>x ∈ span R (⋃ i, ↑(p i)) → x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>x : M<VAR>hx : x ∈ span R (⋃ i, ↑(p i))<GOAL>x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝¹ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>x✝ : M<VAR>hx✝ : x✝ ∈ span R (⋃ i, ↑(p i))<VAR>x : M<VAR>hx : x ∈ ⋃ i, ↑(p i)<GOAL>x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>x : M<VAR>hx : x ∈ span R (⋃ i, ↑(p i))<GOAL>0 ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝¹ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>x✝ : M<VAR>hx✝ : x✝ ∈ span R (⋃ i, ↑(p i))<VAR>x y : M<VAR>hx : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))<VAR>hy : y ∈ AddSubmonoid.closure (⋃ i, ↑(p i))<GOAL>x + y ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝¹ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>x✝ : M<VAR>hx✝ : x✝ ∈ span R (⋃ i, ↑(p i))<VAR>r : R<VAR>x : M<VAR>hx : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))<GOAL>r • x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l✝ : Filter α<VAR>f : α → β<VAR>l : Filter β<VAR>p : α → Prop<VAR>s : Set α<GOAL>(∃ᶠ (a : α) in comap f l, p a) ↔ ∃ᶠ (b : β) in l, ∃ a, f a = b ∧ p a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : HeytingAlgebra α<VAR>a b c : α<GOAL>⊥ᶜ = ⊤
<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>inst✝¹ : MeasurableSpace E<VAR>inst✝ : OpensMeasurableSpace E<VAR>R : ℝ≥0<VAR>p : ℝ≥0∞<VAR>hp : p ≠ 0<VAR>f : ℕ → α → E<VAR>hfmeas : ∀ (n : ℕ), Measurable (f n)<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R<VAR>hp' : ¬p = ⊤<GOAL>∀ᵐ (x : α) ∂μ, liminf (fun n => ↑‖f n x‖₊) atTop < ⊤
<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>inst✝¹ : MeasurableSpace E<VAR>inst✝ : OpensMeasurableSpace E<VAR>R : ℝ≥0<VAR>p : ℝ≥0∞<VAR>hp : p ≠ 0<VAR>f : ℕ → α → E<VAR>hfmeas : ∀ (n : ℕ), Measurable (f n)<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R<VAR>hp' : ¬p = ⊤<VAR>x : α<VAR>hx : liminf (fun n => ↑‖f n x‖₊ ^ p.toReal) atTop < ⊤<GOAL>liminf (fun n => ↑‖f n x‖₊) atTop < ⊤
<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>inst✝¹ : MeasurableSpace E<VAR>inst✝ : OpensMeasurableSpace E<VAR>R : ℝ≥0<VAR>p : ℝ≥0∞<VAR>hp : p ≠ 0<VAR>f : ℕ → α → E<VAR>hfmeas : ∀ (n : ℕ), Measurable (f n)<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R<VAR>hp' : ¬p = ⊤<VAR>x : α<VAR>hx : liminf (fun n => ↑‖f n x‖₊ ^ p.toReal) atTop < ⊤<VAR>hppos : 0 < p.toReal<GOAL>liminf (fun n => ↑‖f n x‖₊) atTop < ⊤
<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>inst✝¹ : MeasurableSpace E<VAR>inst✝ : OpensMeasurableSpace E<VAR>R : ℝ≥0<VAR>p : ℝ≥0∞<VAR>hp : p ≠ 0<VAR>f : ℕ → α → E<VAR>hfmeas : ∀ (n : ℕ), Measurable (f n)<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R<VAR>hp' : ¬p = ⊤<VAR>x : α<VAR>hx : liminf (fun n => ↑‖f n x‖₊ ^ p.toReal) atTop < ⊤<VAR>hppos : 0 < p.toReal<VAR>this : liminf (fun n => ↑‖f n x‖₊ ^ p.toReal) atTop = liminf (fun n => ↑‖f n x‖₊) atTop ^ p.toReal<GOAL>liminf (fun n => ↑‖f n x‖₊) atTop < ⊤
<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>inst✝¹ : MeasurableSpace E<VAR>inst✝ : OpensMeasurableSpace E<VAR>R : ℝ≥0<VAR>p : ℝ≥0∞<VAR>hp : p ≠ 0<VAR>f : ℕ → α → E<VAR>hfmeas : ∀ (n : ℕ), Measurable (f n)<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R<VAR>hp' : ¬p = ⊤<VAR>x : α<VAR>hx : liminf (fun n => ↑‖f n x‖₊) atTop ^ p.toReal < ⊤<VAR>hppos : 0 < p.toReal<VAR>this : liminf (fun n => ↑‖f n x‖₊ ^ p.toReal) atTop = liminf (fun n => ↑‖f n x‖₊) atTop ^ p.toReal<GOAL>liminf (fun n => ↑‖f n x‖₊) atTop < ⊤
<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>inst✝¹ : MeasurableSpace E<VAR>inst✝ : OpensMeasurableSpace E<VAR>R : ℝ≥0<VAR>p : ℝ≥0∞<VAR>hp : p ≠ 0<VAR>f : ℕ → α → E<VAR>hfmeas : ∀ (n : ℕ), Measurable (f n)<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R<VAR>hp' : ¬p = ⊤<VAR>x : α<VAR>hx : liminf (fun n => ↑‖f n x‖₊) atTop ^ p.toReal < ⊤<VAR>hppos : 0 < p.toReal<VAR>this : liminf (fun n => ↑‖f n x‖₊ ^ p.toReal) atTop = liminf (fun n => ↑‖f n x‖₊) atTop ^ p.toReal<GOAL>(liminf (fun n => ↑‖f n x‖₊) atTop ^ p.toReal) ^ p.toReal⁻¹ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝² : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝¹ : SemilatticeSup ι<VAR>inst✝ : Nonempty ι<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>n : ℕ<GOAL>μ (s ∩ ⋂ j, notConvergentSeq f g n j) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝² : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝¹ : SemilatticeSup ι<VAR>inst✝ : Nonempty ι<VAR>n : ℕ<VAR>hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0<GOAL>μ (s ∩ ⋂ j, notConvergentSeq f g n j) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝² : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝¹ : SemilatticeSup ι<VAR>inst✝ : Nonempty ι<VAR>n : ℕ<VAR>hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0<GOAL>μ (s ∩ ⋂ j, notConvergentSeq f g n j) ≤ μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝² : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝¹ : SemilatticeSup ι<VAR>inst✝ : Nonempty ι<VAR>n : ℕ<VAR>hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0<VAR>x : α<GOAL>x ∈ s ∩ ⋂ j, notConvergentSeq f g n j → x ∈ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝² : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝¹ : SemilatticeSup ι<VAR>inst✝ : Nonempty ι<VAR>n : ℕ<VAR>hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0<VAR>x : α<GOAL>(x ∈ s ∧ ∀ (i : ι), ∃ k ≥ i, 1 / (↑n + 1) < dist (f k x) (g x)) → x ∈ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝² : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝¹ : SemilatticeSup ι<VAR>inst✝ : Nonempty ι<VAR>n : ℕ<VAR>hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0<VAR>x : α<VAR>hmem : x ∈ s<VAR>hx : ∀ (i : ι), ∃ k ≥ i, 1 / (↑n + 1) < dist (f k x) (g x)<GOAL>x ∈ {a | a ∈ s ∧ ∃ ε > 0, ∀ (N : ι), ∃ n ≥ N, ε ≤ dist (f n a) (g a)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝² : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝¹ : SemilatticeSup ι<VAR>inst✝ : Nonempty ι<VAR>n : ℕ<VAR>hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0<VAR>x : α<VAR>hmem : x ∈ s<VAR>hx : ∀ (i : ι), ∃ k ≥ i, 1 / (↑n + 1) < dist (f k x) (g x)<VAR>N : ι<GOAL>∃ n_1 ≥ N, 1 / (↑n + 1) ≤ dist (f n_1 x) (g x)
<VAR>m n✝¹ n✝ a✝ n : ℕ<VAR>a b : ZMod (n + 1)<GOAL>(a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs
<VAR>m n✝¹ n✝ a✝ n : ℕ<VAR>a b : ZMod (n + 1)<GOAL>↑(a + b).valMinAbs = ↑(a.valMinAbs + b.valMinAbs)
<VAR>m n✝¹ n✝ a✝ n : ℕ<VAR>a b : ZMod (n + 1)<GOAL>(a + b).valMinAbs.natAbs ≤ n.succ / 2
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : MulAction G α<VAR>s : Set α<VAR>x : α<GOAL>Pairwise (Disjoint on fun g => g • fundamentalInterior G s)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : MulAction G α<VAR>s : Set α<VAR>x : α<VAR>a b : G<VAR>hab : a ≠ b<GOAL>∀ ⦃a_1 : α⦄, a_1 ∈ (fun g => g • fundamentalInterior G s) a → a_1 ∉ (fun g => g • fundamentalInterior G s) b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : MulAction G α<VAR>s : Set α<VAR>x✝ : α<VAR>a b : G<VAR>hab : a ≠ b<VAR>x : α<VAR>hx : x ∈ fundamentalInterior G s<VAR>y : α<VAR>hy : y ∈ fundamentalInterior G s<VAR>hxy : (fun x => b • x) y = (fun x => a • x) x<GOAL>False
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : MulAction G α<VAR>s : Set α<VAR>x✝ : α<VAR>a b : G<VAR>hab : a ≠ b<VAR>x : α<VAR>hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s<VAR>y : α<VAR>hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s<VAR>hxy : (fun x => b • x) y = (fun x => a • x) x<GOAL>False
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : MulAction G α<VAR>s : Set α<VAR>x✝ : α<VAR>a b : G<VAR>hab : a ≠ b<VAR>x : α<VAR>hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s<VAR>y : α<VAR>hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s<VAR>hxy : (fun x => b • x) y = (fun x => a • x) x<GOAL>a⁻¹ * b ≠ 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : MulAction G α<VAR>s : Set α<VAR>x✝ : α<VAR>a b : G<VAR>hab : a ≠ b<VAR>x : α<VAR>hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s<VAR>y : α<VAR>hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s<VAR>hxy : (fun x => b • x) y = (fun x => a • x) x<GOAL>x ∈ (a⁻¹ * b) • s
<VAR>s : ℂ<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>hs : 1 < s.re<GOAL>HasProd (fun p => (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) (L (fun n => χ ↑n) s)
<VAR>s : ℂ<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>hs : 1 < s.re<GOAL>HasProd (fun p => (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) (∑' (n : ℕ), (dirichletSummandHom χ ⋯) n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝⁴ : CommRing α<VAR>inst✝³ : StarRing α<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq m<VAR>A : Matrix m m α<VAR>inst✝ : Invertible A<VAR>h : A⁻¹.IsHermitian<GOAL>A.IsHermitian
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝⁴ : CommRing α<VAR>inst✝³ : StarRing α<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq m<VAR>A : Matrix m m α<VAR>inst✝ : Invertible A<VAR>h : A⁻¹.IsHermitian<GOAL>A⁻¹⁻¹.IsHermitian
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ioc a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (a₁ ⊔ a₂) (b₁ ⊓ b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ioi a₁ ∩ Iic b₁ ∩ (Ioi a₂ ∩ Iic b₂) = Ioi a₁ ∩ Ioi a₂ ∩ (Iic b₁ ∩ Iic b₂)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : CommSemiring α<VAR>a✝ b✝ c a b : α<GOAL>(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>p✝ : R[X]<VAR>r : R<VAR>p q : R[X]<VAR>S : Type u_2<VAR>inst✝⁵ : NonAssocSemiring S<VAR>inst✝⁴ : Module R S<VAR>inst✝³ : IsScalarTower R S S<VAR>inst✝² : SMulCommClass R S S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>x : S<GOAL>(p * X).smeval x = p.smeval x * x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>a b : α<VAR>h : a ≠ b<GOAL>{a, b}.ncard = 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>a b : α<VAR>h : a ≠ b<GOAL>a ∉ {b}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>E X I : Set α<VAR>M : Matroid α<VAR>hIX : I ⊆ X<GOAL>(M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>E X I : Set α<VAR>M : Matroid α<VAR>hIX : I ⊆ X<GOAL>I ⊆ range Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>C : ℝ≥0∞<VAR>hC : C ≠ ⊤<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<GOAL>edist (f 0) a ≤ 2 * C
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Group α<VAR>s t : Set α<VAR>a b : α<GOAL>IsUnit s ↔ ∃ a, s = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f g : β → α<VAR>a b : α<VAR>s✝ : Finset β<VAR>inst✝ : ContinuousMul α<VAR>s t : Set β<VAR>hs : Disjoint s t<VAR>ha : HasProd (f ∘ Subtype.val) a<VAR>hb : HasProd (f ∘ Subtype.val) b<GOAL>HasProd (f ∘ Subtype.val) (a * b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f g : β → α<VAR>a b : α<VAR>s✝ : Finset β<VAR>inst✝ : ContinuousMul α<VAR>s t : Set β<VAR>hs : Disjoint s t<VAR>ha : HasProd (s.mulIndicator f) a<VAR>hb : HasProd (t.mulIndicator f) b<GOAL>HasProd ((s ∪ t).mulIndicator f) (a * b)