ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w u' v' : V<VAR>p : G.Walk u' v'<GOAL>(p.copy ⋯ ⋯).IsPath ↔ p.IsPath
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>h : IsPurelyInseparable F K<GOAL>IsPurelyInseparable E K
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>h : IsPurelyInseparable F K<VAR>q : ℕ<VAR>h✝ : ExpChar F q<GOAL>IsPurelyInseparable E K
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>h : IsPurelyInseparable F K<VAR>q : ℕ<VAR>h✝ : ExpChar F q<VAR>this : ExpChar E q<GOAL>IsPurelyInseparable E K
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>q : ℕ<VAR>h : ∀ (x : K), ∃ n, x ^ q ^ n ∈ (algebraMap F K).range<VAR>h✝ : ExpChar F q<VAR>this : ExpChar E q<GOAL>∀ (x : K), ∃ n, x ^ q ^ n ∈ (algebraMap E K).range
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>q : ℕ<VAR>h✝¹ : ∀ (x : K), ∃ n, x ^ q ^ n ∈ (algebraMap F K).range<VAR>h✝ : ExpChar F q<VAR>this : ExpChar E q<VAR>x : K<VAR>n : ℕ<VAR>y : F<VAR>h : (algebraMap F K) y = x ^ q ^ n<GOAL>∃ n, x ^ q ^ n ∈ (algebraMap E K).range
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>hf : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : f' ≤ 0<VAR>x : ℝ<GOAL>deriv f x ≤ 0
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>hf : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : f' ≤ 0<VAR>x : ℝ<GOAL>f' x ≤ 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ≥0<GOAL>↑R ≤ (cauchyPowerSeries f c ↑R).radius
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ≥0<VAR>n : ℕ<GOAL>‖cauchyPowerSeries f c (↑R) n‖ * ↑R ^ n ≤ (2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ≥0<VAR>n : ℕ<GOAL>((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖) * |↑R|⁻¹ ^ n * ↑R ^ n ≤ (2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ≥0<VAR>n : ℕ<GOAL>((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖) * (↑R)⁻¹ ^ n * ↑R ^ n ≤ (2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ≥0<VAR>n : ℕ<VAR>hR : ↑R ^ n = 0<GOAL>((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖) * (↑R)⁻¹ ^ n * ↑R ^ n ≤ (2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ≥0<VAR>n : ℕ<VAR>hR : ↑R ^ n ≠ 0<GOAL>((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖) * (↑R)⁻¹ ^ n * ↑R ^ n ≤ (2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c (↑R) θ)‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>hq1 : 1 ≤ q<VAR>a : α<GOAL>↑‖(f + g) a‖₊ ≤ ((fun a => ↑‖f a‖₊) + fun a => ↑‖g a‖₊) a
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>R : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>c : R<VAR>hf : HasDerivAtFilter f f' x L<GOAL>HasDerivAtFilter (fun y => c • f y) (c • f') x L
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a b : R<VAR>m : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>ha : a < 0<VAR>k : ℕ<GOAL>a ^ (2 * k + 1) < 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a b : R<VAR>m : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>ha : a < 0<VAR>k : ℕ<GOAL>a ^ (2 * k) * a < 0
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>f : j ⟶ i<VAR>x : F.obj j<VAR>hx : x ∈ F.eventualRange j<GOAL>F.map f x ∈ F.eventualRange i
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>f : j ⟶ i<VAR>x : F.obj j<VAR>hx : ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ range (F.map f)<GOAL>∀ ⦃i_1 : J⦄ (f_1 : i_1 ⟶ i), F.map f x ∈ range (F.map f_1)
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k✝ : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>f : j ⟶ i<VAR>x : F.obj j<VAR>hx : ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ range (F.map f)<VAR>k : J<VAR>f' : k ⟶ i<GOAL>F.map f x ∈ range (F.map f')
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k✝ : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>f : j ⟶ i<VAR>x : F.obj j<VAR>hx : ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ range (F.map f)<VAR>k : J<VAR>f' : k ⟶ i<VAR>l : J<VAR>g : l ⟶ j<VAR>g' : l ⟶ k<VAR>he : g ≫ f = g' ≫ f'<GOAL>F.map f x ∈ range (F.map f')
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k✝ : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>f : j ⟶ i<VAR>k : J<VAR>f' : k ⟶ i<VAR>l : J<VAR>g : l ⟶ j<VAR>g' : l ⟶ k<VAR>he : g ≫ f = g' ≫ f'<VAR>x : F.obj l<VAR>hx : ∀ ⦃i : J⦄ (f : i ⟶ j), F.map g x ∈ range (F.map f)<GOAL>F.map f (F.map g x) ∈ range (F.map f')
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k✝ : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>f : j ⟶ i<VAR>k : J<VAR>f' : k ⟶ i<VAR>l : J<VAR>g : l ⟶ j<VAR>g' : l ⟶ k<VAR>he : g ≫ f = g' ≫ f'<VAR>x : F.obj l<VAR>hx : ∀ ⦃i : J⦄ (f : i ⟶ j), F.map g x ∈ range (F.map f)<GOAL>(F.map g' ≫ F.map f') x ∈ range (F.map f')
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁸ : NontriviallyNormedField R<VAR>inst✝⁷ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁶ : (x : B) → Module R (E x)<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace R F<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>inst✝ : FiberBundle F E<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>b✝ : B<VAR>a : F<VAR>i j : ι<VAR>b : B<VAR>hb : b ∈ Z.baseSet i<VAR>v : F<GOAL>(Z.localTriv i).symm b v = (Z.coordChange i (Z.indexAt b) b) v
<VAR>α : Type u_1<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ a b c : α<GOAL>mabs ((a ⊓ c) / (b ⊓ c)) ≤ mabs (a / b)
<VAR>α : Type u_1<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ a b c : α<GOAL>mabs ?m.27534 * mabs ((a ⊓ c) / (b ⊓ c)) ≤ mabs (a / b)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q✝ : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>p q : MvPolynomial σ R<VAR>x : σ<VAR>hx : x ∈ (p + q).vars<GOAL>x ∈ p.vars ∪ q.vars
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q✝ : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>p q : MvPolynomial σ R<VAR>x : σ<VAR>hx : x ∈ (p + q).degrees<GOAL>x ∈ p.degrees ∨ x ∈ q.degrees
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedRing R<VAR>a b n✝ : ℤ<VAR>x : R<VAR>n : ℤ<VAR>hx : |x| ≤ 1<GOAL>0 ≤ ↑n * x + ↑n * ↑n
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedRing R<VAR>a b n✝ : ℤ<VAR>x : R<VAR>n : ℤ<VAR>hx : |x| ≤ 1<VAR>hnx : 0 < n → 0 ≤ x + ↑n<GOAL>0 ≤ ↑n * x + ↑n * ↑n
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedRing R<VAR>a b n✝ : ℤ<VAR>x : R<VAR>n : ℤ<VAR>hx : |x| ≤ 1<VAR>hnx : 0 < n → 0 ≤ x + ↑n<VAR>hnx' : n < 0 → x + ↑n ≤ 0<GOAL>0 ≤ ↑n * x + ↑n * ↑n
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedRing R<VAR>a b n✝ : ℤ<VAR>x : R<VAR>n : ℤ<VAR>hx : |x| ≤ 1<VAR>hnx : 0 < n → 0 ≤ x + ↑n<VAR>hnx' : n < 0 → x + ↑n ≤ 0<GOAL>0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedRing R<VAR>a b n✝ : ℤ<VAR>x : R<VAR>n : ℤ<VAR>hx : |x| ≤ 1<VAR>hnx : 0 < n → 0 ≤ x + ↑n<VAR>hnx' : n < 0 → x + ↑n ≤ 0<VAR>h : n < 0<GOAL>0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedRing R<VAR>a b n : ℤ<VAR>x : R<VAR>hx : |x| ≤ 1<VAR>hnx : 0 < 0 → 0 ≤ x + ↑0<VAR>hnx' : 0 < 0 → x + ↑0 ≤ 0<GOAL>0 ≤ ↑0 ∧ 0 ≤ x + ↑0 ∨ ↑0 ≤ 0 ∧ x + ↑0 ≤ 0
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedRing R<VAR>a b n✝ : ℤ<VAR>x : R<VAR>n : ℤ<VAR>hx : |x| ≤ 1<VAR>hnx : 0 < n → 0 ≤ x + ↑n<VAR>hnx' : n < 0 → x + ↑n ≤ 0<VAR>h : 0 < n<GOAL>0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u<VAR>S : Type v<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>s : Set σ<VAR>x : R<GOAL>↑((supportedEquivMvPolynomial s).symm (C x)) = ↑((algebraMap R ↥(supported R s)) x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>hf : IsBoundedLinearMap 𝕜 f<GOAL>IsBoundedLinearMap 𝕜 fun e => -f e
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>hf : IsBoundedLinearMap 𝕜 f<GOAL>IsBoundedLinearMap 𝕜 fun e => -1 • f e
<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✝¹ f✝ : R →+* S<VAR>inst✝ : Algebra R S<VAR>f : A ≃ₐ[R] S<VAR>y : S<GOAL>y ∈ Subalgebra.map (↑f) (integralClosure R A) ↔ y ∈ integralClosure R S
<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✝¹ f✝ : R →+* S<VAR>inst✝ : Algebra R S<VAR>f : A ≃ₐ[R] S<VAR>y : S<GOAL>(∃ x ∈ integralClosure R A, ↑f x = y) ↔ y ∈ integralClosure R S
<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 s : Set M<VAR>r : R<VAR>hr : IsUnit r<GOAL>span R (r • s) = span R s
<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 s : Set M<VAR>r : R<VAR>hr : IsUnit r<GOAL>span R (r • s) ≤ span R s
<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 s : Set M<VAR>r : R<VAR>hr : IsUnit r<GOAL>span R s ≤ span R (r • s)
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<GOAL>μ s⁻¹ = 0 ↔ μ s = 0
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>hs : μ s⁻¹ = 0<GOAL>μ s = 0
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>hs : μ s⁻¹ = 0<GOAL>μ s⁻¹⁻¹ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<GOAL>image succ univ = {0}ᶜ
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂✝ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>s₂ : Finset ι<VAR>h : s₂ ⊆ s<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<GOAL>((s \ s₂).weightedVSubOfPoint p b) w - (s₂.weightedVSubOfPoint p b) (-w) = (s.weightedVSubOfPoint p b) w
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ : Measure α<VAR>f✝ : α → E<VAR>g✝ : α → F<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>g : α → F<VAR>hg : AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<VAR>hp_top : ¬p = ⊤<VAR>hp_zero : ¬p = 0<GOAL>eLpNorm (fun x => b (f x) (g x)) p μ ≤ eLpNorm f ⊤ μ * eLpNorm g p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ : Measure α<VAR>f✝ : α → E<VAR>g✝ : α → F<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>g : α → F<VAR>hg : AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<VAR>hp_top : ¬p = ⊤<VAR>hp_zero : ¬p = 0<GOAL>(∫⁻ (x : α), ↑‖b (f x) (g x)‖₊ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≤ essSup (fun x => ↑‖f x‖₊) μ * (∫⁻ (x : α), ↑‖g x‖₊ ^ p.toReal ∂μ) ^ (1 / p.toReal)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>f : α → β<VAR>inst✝ : Zero β<VAR>g : α → β<VAR>hs : MeasurableSet s<GOAL>f =ᶠ[ae (μ.restrict s)] g ↔ s.indicator f =ᶠ[ae μ] s.indicator g
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>f : α → β<VAR>inst✝ : Zero β<VAR>g : α → β<VAR>hs : MeasurableSet s<GOAL>(∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) ↔ s.indicator f =ᶠ[ae μ] s.indicator g
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>f : α → β<VAR>inst✝ : Zero β<VAR>g : α → β<VAR>hs : MeasurableSet s<VAR>h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x<VAR>x : α<VAR>hx : x ∈ s → f x = g x<GOAL>s.indicator f x = s.indicator g x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>f : α → β<VAR>inst✝ : Zero β<VAR>g : α → β<VAR>hs : MeasurableSet s<VAR>h : s.indicator f =ᶠ[ae μ] s.indicator g<VAR>x : α<VAR>hx : s.indicator f x = s.indicator g x<GOAL>x ∈ s → f x = g x
<VAR>α : Type u<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a b c : α<GOAL>a ≤ a⁻¹ ↔ a ≤ 1
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoMetricSpace α<GOAL>𝓤 (Completion α) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v✝ : V<VAR>G₁ G₂ : SimpleGraph V<VAR>H : SimpleGraph W<VAR>f✝ : G →g G'<VAR>f : ⊤ →g G'<VAR>v w : V<VAR>h : f v = f w<GOAL>v = w
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v✝ : V<VAR>G₁ G₂ : SimpleGraph V<VAR>H : SimpleGraph W<VAR>f✝ : G →g G'<VAR>f : ⊤ →g G'<VAR>v w : V<VAR>h : v ≠ w<GOAL>f v ≠ f w
<VAR>m n a✝ b✝ c d : ℕ<VAR>co : n.Coprime m<VAR>a b z : ℕ<VAR>hzan : z ≡ a [MOD n]<VAR>hzbm : z ≡ b [MOD m]<GOAL>z ≡ ↑(chineseRemainder co a b) [MOD n * m]
<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>I : FractionalIdeal S P<VAR>h : I = 0<VAR>x : P<VAR>hx : x ∈ I<GOAL>x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>a : α<GOAL>p a = 1 ↔ p.support = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>a : α<VAR>h : p a = 1<VAR>a' : α<VAR>ha' : a' ∈ p.support<VAR>ha : a' ∉ {a}<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>a : α<VAR>h : p a = 1<VAR>a' : α<VAR>ha' : a' ∈ p.support<VAR>ha : a' ∉ {a}<GOAL>1 < ∑' (a : α), p a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>a : α<VAR>h : p a = 1<VAR>a' : α<VAR>ha' : a' ∈ p.support<VAR>ha : a' ∉ {a}<VAR>this : 0 < ∑' (b : α), if b = a then 0 else p b<GOAL>1 < ∑' (a : α), p a
<VAR>p q : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hq0 : ↑q ≠ 0<GOAL>∑ a ∈ Ico 1 (p / 2).succ, a * q / p + ∑ a ∈ Ico 1 (q / 2).succ, a * p / q = p / 2 * (q / 2)
<VAR>p q : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hq0 : ↑q ≠ 0<VAR>hswap : (filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)).card = (filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ)).card<GOAL>∑ a ∈ Ico 1 (p / 2).succ, a * q / p + ∑ a ∈ Ico 1 (q / 2).succ, a * p / q = p / 2 * (q / 2)
<VAR>p q : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hq0 : ↑q ≠ 0<VAR>hswap : (filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)).card = (filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ)).card<VAR>hdisj : Disjoint (filter (fun x => x.2 * p ≤ x.1 * q) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ)) (filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))<GOAL>∑ a ∈ Ico 1 (p / 2).succ, a * q / p + ∑ a ∈ Ico 1 (q / 2).succ, a * p / q = p / 2 * (q / 2)
<VAR>p q : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hq0 : ↑q ≠ 0<VAR>hswap : (filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)).card = (filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ)).card<VAR>hdisj : Disjoint (filter (fun x => x.2 * p ≤ x.1 * q) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ)) (filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))<VAR>hunion : filter (fun x => x.2 * p ≤ x.1 * q) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ) ∪ filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ) = Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ<GOAL>∑ a ∈ Ico 1 (p / 2).succ, a * q / p + ∑ a ∈ Ico 1 (q / 2).succ, a * p / q = p / 2 * (q / 2)
<VAR>p q : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hq0 : ↑q ≠ 0<VAR>hswap : (filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)).card = (filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ)).card<VAR>hdisj : Disjoint (filter (fun x => x.2 * p ≤ x.1 * q) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ)) (filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))<VAR>hunion : filter (fun x => x.2 * p ≤ x.1 * q) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ) ∪ filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ) = Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ<GOAL>(Ico 1 (p / 2).succ).card * (Ico 1 (q / 2).succ).card = p / 2 * (q / 2)
<VAR>S : Set ℝ<VAR>hS : ∀ x ∈ S, 0 ≤ x<GOAL>0 ≤ sSup S
<VAR>hS : ∀ x ∈ ∅, 0 ≤ x<GOAL>0 ≤ sSup ∅
<VAR>S : Set ℝ<VAR>hS : ∀ x ∈ S, 0 ≤ x<VAR>y : ℝ<VAR>hy : y ∈ S<GOAL>0 ≤ sSup S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 ≤ ε<GOAL>Disjoint (closedBall x δ) (closedBall y ε) ↔ δ + ε < dist x y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 ≤ ε<VAR>h : Disjoint (closedBall x δ) (closedBall y ε)<VAR>hxy : δ + ε ≥ dist x y<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 ≤ ε<VAR>h : Disjoint (closedBall x δ) (closedBall y ε)<VAR>hxy : ε + δ ≥ dist x y<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z✝ : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 ≤ ε<VAR>h : Disjoint (closedBall x δ) (closedBall y ε)<VAR>hxy : ε + δ ≥ dist x y<VAR>z : E<VAR>hxz : dist x z ≤ δ<VAR>hzy : dist z y ≤ ε<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z✝ : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 ≤ ε<VAR>h : Disjoint (closedBall x δ) (closedBall y ε)<VAR>hxy : ε + δ ≥ dist x y<VAR>z : E<VAR>hxz : dist z x ≤ δ<VAR>hzy : dist z y ≤ ε<GOAL>False
<VAR>a x z✝ z : ℂ<GOAL>z.arg ∈ Ioc (-π) π
<VAR>a x z✝ z : ℂ<VAR>hπ : 0 < π<GOAL>z.arg ∈ Ioc (-π) π
<VAR>a x z : ℂ<VAR>hπ : 0 < π<GOAL>arg 0 ∈ Ioc (-π) π
<VAR>a x z✝ z : ℂ<VAR>hπ : 0 < π<VAR>hz : z ≠ 0<GOAL>z.arg ∈ Ioc (-π) π
<VAR>a x z✝ z : ℂ<VAR>hπ : 0 < π<VAR>hz : z ≠ 0<VAR>N : ℤ<VAR>hN : z.arg + N • (2 * π) ∈ Ioc (-π) (-π + 2 * π)<GOAL>z.arg ∈ Ioc (-π) π
<VAR>a x z✝ z : ℂ<VAR>hπ : 0 < π<VAR>hz : z ≠ 0<VAR>N : ℤ<VAR>hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π<GOAL>z.arg ∈ Ioc (-π) π
<VAR>a x z✝ z : ℂ<VAR>hπ : 0 < π<VAR>hz : z ≠ 0<VAR>N : ℤ<VAR>hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π<GOAL>(↑(abs z) * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg ∈ Ioc (-π) π
<VAR>a x z✝ z : ℂ<VAR>hπ : 0 < π<VAR>hz : z ≠ 0<VAR>N : ℤ<VAR>hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π<VAR>this : (↑(abs z) * (cos ↑(z.arg + ↑N * (2 * π)) + sin ↑(z.arg + ↑N * (2 * π)) * I)).arg = z.arg + ↑N * (2 * π)<GOAL>(↑(abs z) * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg ∈ Ioc (-π) π