ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology β<VAR>f : α × β → γ<VAR>s : Set (α × β)<VAR>x : α × β<GOAL>Tendsto f (map (fun a => (a, x.2)) (𝓝 x.1 ⊓ 𝓟 ((fun a => (a, x.2)) ⁻¹' s))) (𝓝 (f (x.1, x.2))) ↔ Tendsto (fun x_1 => f (x_1, x.2)) (𝓝 x.1 ⊓ 𝓟 {a | (a, x.2) ∈ s}) (𝓝 (f (x.1, x.2)))
<VAR>m n : ℕ<VAR>h : n ≠ 0<GOAL>n.div2 < n
<VAR>m n : ℕ<VAR>h : n ≠ 0<GOAL>n / 2 < n
<VAR>m n : ℕ<VAR>h : n ≠ 0<GOAL>n < n * succ 1
<VAR>m n : ℕ<VAR>h : n ≠ 0<VAR>this : n * 1 < n * succ 1<GOAL>n < n * succ 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>A : Type ?u.14973<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<GOAL>IsLocallyInjective f ↔ IsOpen (Function.pullbackDiagonal f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>A : Type ?u.14973<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<GOAL>(∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U) ↔ ∀ (a b : X) (b_1 : f a = f b), ⟨(a, b), b_1⟩ ∈ Function.pullbackDiagonal f → ∃ t ∈ 𝓝 a ×ˢ 𝓝 b, Subtype.val ⁻¹' t ⊆ Function.pullbackDiagonal f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x : E<GOAL>x ∈ toCone s hs ↔ ∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : QuasiErgodic f μ<VAR>hsm : NullMeasurableSet s μ<VAR>hs : f ⁻¹' s =ᶠ[ae μ] s<GOAL>s =ᶠ[ae μ] univ → ∀ᵐ (x : α) ∂μ, x ∈ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : QuasiErgodic f μ<VAR>hsm : NullMeasurableSet s μ<VAR>hs : f ⁻¹' s =ᶠ[ae μ] s<GOAL>s =ᶠ[ae μ] ∅ → ∀ᵐ (x : α) ∂μ, x ∉ s
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CommSemiring T<VAR>f✝ f : σ → MvPolynomial τ R<VAR>d : σ →₀ ℕ<VAR>r : R<GOAL>(bind₁ f) ((monomial d) r) = C r * ∏ i ∈ d.support, f i ^ d i
<VAR>τ : Type u_1<VAR>inst✝³ : TopologicalSpace τ<VAR>inst✝² : AddMonoid τ<VAR>inst✝¹ : ContinuousAdd τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : Filter τ<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>hf : ∀ (t : τ), Tendsto (fun x => t + x) f f<GOAL>IsInvariant ϕ.toFun (ω f ϕ.toFun s)
<VAR>τ : Type u_1<VAR>inst✝³ : TopologicalSpace τ<VAR>inst✝² : AddMonoid τ<VAR>inst✝¹ : ContinuousAdd τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : Filter τ<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>hf : ∀ (t : τ), Tendsto (fun x => t + x) f f<VAR>t : τ<GOAL>MapsTo (ϕ.toFun t) (ω f ϕ.toFun s) (ω f (fun t_1 x => ϕ.toFun (t + t_1) x) s)
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>inst✝¹ : SeminormedGroup G<VAR>s✝ : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<VAR>s t : Set α<VAR>f : α → E<VAR>x : α<GOAL>edist (s.mulIndicator f x) (t.mulIndicator f x) = ↑‖(s ∆ t).mulIndicator f x‖₊
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ✝ Δ'✝ Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>Δ Δ' : SimplexCategoryᵒᵖ<VAR>A : Splitting.IndexSet Δ<VAR>θ : Δ ⟶ Δ'<GOAL>((splitting K).cofan Δ).inj A ≫ (obj K).map θ = Termwise.mapMono K (image.ι (θ.unop ≫ A.e)) ≫ ((splitting K).cofan Δ').inj (A.pull θ)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ✝ Δ'✝ Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>Δ Δ' : SimplexCategoryᵒᵖ<VAR>A : Splitting.IndexSet Δ<VAR>θ : Δ ⟶ Δ'<GOAL>factorThruImage (θ.unop ≫ A.e) ≫ image.ι (θ.unop ≫ A.e) = θ.unop ≫ A.e
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.φ 1 = C X
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q a x✝ : ℝ≥0<VAR>h : ↑a < ↑x✝<GOAL>(↑x✝)⁻¹ < (↑a)⁻¹
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q a x✝ : ℝ≥0<VAR>h : a < x✝<GOAL>(↑x✝)⁻¹ < (↑a)⁻¹
<VAR>a b c d : ℝ≥0∞<VAR>r p q x✝ : ℝ≥0<VAR>h : 0 < x✝<GOAL>(↑x✝)⁻¹ < (↑0)⁻¹
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q a x✝ : ℝ≥0<VAR>h : a < x✝<VAR>ha : a ≠ 0<GOAL>(↑x✝)⁻¹ < (↑a)⁻¹
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q a x✝ : ℝ≥0<VAR>h : a < x✝<VAR>ha : a ≠ 0<GOAL>x✝⁻¹ < a⁻¹
<VAR>p m : ℕ+<VAR>pp : p.Prime<GOAL>m ∣ p ↔ m = 1 ∨ m = p
<VAR>p m : ℕ+<VAR>pp : p.Prime<GOAL>↑m ∣ ↑p ↔ m = 1 ∨ m = p
<VAR>p m : ℕ+<VAR>pp : p.Prime<GOAL>↑m = 1 ∨ ↑m = ↑p ↔ m = 1 ∨ m = p
<VAR>R : Type u<VAR>inst✝ : Semiring R<VAR>q : ℕ<VAR>x y : R<VAR>h : Commute x y<VAR>hprime : Nat.Prime q<VAR>hchar✝ : CharP R q<VAR>this : Fact (Nat.Prime q)<GOAL>(x + y) ^ q = x ^ q + y ^ q
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} D'<VAR>L : C ⥤ D<VAR>inst✝ : L.IsLocalization W<VAR>X Y Z : C<GOAL>HasSmallLocalizedHom W X Y
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} D'<VAR>L : C ⥤ D<VAR>inst✝ : L.IsLocalization W<VAR>X Y Z : C<GOAL>Small.{v₂, v₂} (L.obj X ⟶ L.obj Y)
<VAR>a b c : Ordinal.{u_1}<VAR>b0 : b ≠ 0<VAR>h : c.IsLimit<GOAL>a < b ^ c ↔ ∃ c' < c, a < b ^ c'
<VAR>a b c : Ordinal.{u_1}<VAR>b0 : b ≠ 0<VAR>h : c.IsLimit<GOAL>¬a < b ^ c ↔ ∀ (x : Ordinal.{u_1}), ¬(x < c ∧ a < b ^ x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>S : Set (Set α)<VAR>hS : S.Nonempty<VAR>t : Set β<GOAL>⋂₀ S ×ˢ t = ⋂ s ∈ S, s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>S : Set (Set α)<VAR>hS : S.Nonempty<VAR>t : Set β<GOAL>⋂ r ∈ S ×ˢ {t}, r.1 ×ˢ r.2 = ⋂ s ∈ S, s ×ˢ t
<VAR>n m : ℕ<VAR>x : ℝ<VAR>e₁ : n + 1 = m<VAR>h : |x| ≤ 1<GOAL>|rexp x - expNear m x 0| ≤ |x| ^ m / ↑m.factorial * ((↑m + 1) / ↑m)
<VAR>n m : ℕ<VAR>x : ℝ<VAR>e₁ : n + 1 = m<VAR>h : |x| ≤ 1<GOAL>|rexp x - ∑ m ∈ range m, x ^ m / ↑m.factorial| ≤ |x| ^ m / ↑m.factorial * ((↑m + 1) / ↑m)
<VAR>n m : ℕ<VAR>x : ℝ<VAR>e₁ : n + 1 = m<VAR>h : |x| ≤ 1<GOAL>|x| ^ m / ↑m.factorial * ((↑m + 1) / ↑m) = |x| ^ m * (↑m.succ / (↑m.factorial * ↑m))
<VAR>n m : ℕ<VAR>x : ℝ<VAR>e₁ : n + 1 = m<VAR>h : |x| ≤ 1<GOAL>0 < m
<VAR>α : Type u_1<VAR>inst✝³ : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝² : UniformSpace β<VAR>f : α → β<VAR>inst✝¹ : CompleteSpace β<VAR>inst✝ : T0Space β<VAR>hf : UniformContinuous f<VAR>g : pkg.space → β<VAR>hg : UniformContinuous g<VAR>h : ∀ (a : α), f a = g (pkg.coe a)<GOAL>pkg.extend f = g
<VAR>α : Type u_1<VAR>inst✝³ : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝² : UniformSpace β<VAR>f : α → β<VAR>inst✝¹ : CompleteSpace β<VAR>inst✝ : T0Space β<VAR>hf : UniformContinuous f<VAR>g : pkg.space → β<VAR>hg : UniformContinuous g<VAR>h : ∀ (a : α), f a = g (pkg.coe a)<GOAL>∀ (a : α), pkg.extend f (pkg.coe a) = g (pkg.coe a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : Algebra R Rₘ<VAR>inst✝⁹ : CommRing Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>M : Submonoid R<VAR>inst✝⁷ : IsLocalization M Rₘ<VAR>inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : Algebra R Sₘ<VAR>inst✝³ : IsScalarTower R Rₘ Sₘ<VAR>inst✝² : IsScalarTower R S Sₘ<VAR>inst✝¹ : Module.Free R S<VAR>inst✝ : Module.Finite R S<VAR>a : S<GOAL>(norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm R) a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : Algebra R Rₘ<VAR>inst✝⁹ : CommRing Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>M : Submonoid R<VAR>inst✝⁷ : IsLocalization M Rₘ<VAR>inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : Algebra R Sₘ<VAR>inst✝³ : IsScalarTower R Rₘ Sₘ<VAR>inst✝² : IsScalarTower R S Sₘ<VAR>inst✝¹ : Module.Free R S<VAR>inst✝ : Module.Finite R S<VAR>a : S<VAR>h✝ : Subsingleton R<GOAL>(norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm R) a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : Algebra R Rₘ<VAR>inst✝⁹ : CommRing Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>M : Submonoid R<VAR>inst✝⁷ : IsLocalization M Rₘ<VAR>inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : Algebra R Sₘ<VAR>inst✝³ : IsScalarTower R Rₘ Sₘ<VAR>inst✝² : IsScalarTower R S Sₘ<VAR>inst✝¹ : Module.Free R S<VAR>inst✝ : Module.Finite R S<VAR>a : S<VAR>h✝ : Nontrivial R<GOAL>(norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm R) a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : Algebra R Rₘ<VAR>inst✝⁹ : CommRing Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>M : Submonoid R<VAR>inst✝⁷ : IsLocalization M Rₘ<VAR>inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : Algebra R Sₘ<VAR>inst✝³ : IsScalarTower R Rₘ Sₘ<VAR>inst✝² : IsScalarTower R S Sₘ<VAR>inst✝¹ : Module.Free R S<VAR>inst✝ : Module.Finite R S<VAR>a : S<VAR>h✝ : Nontrivial R<VAR>b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S<VAR>this : DecidableEq (Module.Free.ChooseBasisIndex R S) := Classical.decEq (Module.Free.ChooseBasisIndex R S)<GOAL>(norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm R) a)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : LinearOrderedRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>h : AffineIndependent k p<VAR>w w₁ w₂ : ι → k<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>hs : (affineCombination k s p) w ∈ affineSpan k {(affineCombination k s p) w₁, (affineCombination k s p) w₂}<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>hi0 : w₁ i = 0<VAR>hj0 : w₁ j = 0<VAR>hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)<GOAL>SignType.sign (w i) = SignType.sign (w j)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : LinearOrderedRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>h : AffineIndependent k p<VAR>w w₁ w₂ : ι → k<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>hs : ∃ r, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>hi0 : w₁ i = 0<VAR>hj0 : w₁ j = 0<VAR>hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)<GOAL>SignType.sign (w i) = SignType.sign (w j)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : LinearOrderedRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>h : AffineIndependent k p<VAR>w w₁ w₂ : ι → k<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>hi0 : w₁ i = 0<VAR>hj0 : w₁ j = 0<VAR>hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)<VAR>r : k<VAR>hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i<GOAL>SignType.sign (w i) = SignType.sign (w j)
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>N : s.Normal<VAR>g a : α<GOAL>a ∈ g • ↑s ↔ a ∈ op g • ↑s
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>u v w : m → α<VAR>x : α<VAR>i : m<GOAL>Pi.single i x ⬝ᵥ v = x * v i
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>u v w : m → α<VAR>x : α<VAR>i : m<VAR>this : ∀ (j : m), j ≠ i → Pi.single i x j * v j = 0<GOAL>Pi.single i x ⬝ᵥ v = x * v i
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w : V<VAR>e✝ : Sym2 V<VAR>inst✝ : DecidableEq V<VAR>v : V<VAR>e : Sym2 V<VAR>he : e ∈ G.edgeSet<VAR>hv : v ∈ e<GOAL>G.otherVertexOfIncident ⋯ ∈ G.neighborSet v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>r : ℚ<GOAL>(fun a => ENNReal.ofReal (↑(condCDF ρ a) ↑r)) =ᶠ[ae ρ.fst] preCDF ρ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>r : ℚ<VAR>a : α<VAR>ha : ↑(condCDF ρ a) ↑r = (preCDF ρ r a).toReal<VAR>ha_le_one : ∀ (r : ℚ), preCDF ρ r a ≤ 1<GOAL>ENNReal.ofReal (↑(condCDF ρ a) ↑r) = preCDF ρ r a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>r : ℚ<VAR>a : α<VAR>ha : ↑(condCDF ρ a) ↑r = (preCDF ρ r a).toReal<VAR>ha_le_one : ∀ (r : ℚ), preCDF ρ r a ≤ 1<GOAL>preCDF ρ r 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>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>f g : α → E<VAR>h : Disjoint (support f) (support g)<VAR>hf : StronglyMeasurable f<VAR>hg : StronglyMeasurable g<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<GOAL>Memℒp (f + g) p μ ↔ Memℒp f p μ ∧ Memℒp g p μ
<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>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>f g : α → E<VAR>h : Disjoint (support f) (support g)<VAR>hf : StronglyMeasurable f<VAR>hg : StronglyMeasurable g<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>hfg : Memℒp (f + g) p μ<GOAL>Memℒp f p μ
<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>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>f g : α → E<VAR>h : Disjoint (support f) (support g)<VAR>hf : StronglyMeasurable f<VAR>hg : StronglyMeasurable g<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>hfg : Memℒp (f + g) p μ<GOAL>Memℒp g p μ
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>inst✝² : F.IsEquivalence<VAR>inst✝¹ : SplitEpiCategory C<VAR>X Y : D<VAR>f : X ⟶ Y<VAR>inst✝ : Epi f<GOAL>IsSplitEpi f
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>inst✝² : F.IsEquivalence<VAR>inst✝¹ : SplitEpiCategory C<VAR>X Y : D<VAR>f : X ⟶ Y<VAR>inst✝ : Epi f<GOAL>IsSplitEpi (F.inv.map f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁵ : Zero α<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : SMulZeroClass α β<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : PosSMulStrictMono α β<VAR>ha : 0 < a<VAR>hb : b < 0<GOAL>a • b < 0
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝⁵ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a✝ : 𝕜<VAR>inst✝² : Archimedean 𝕜<VAR>x : AddCircle p<VAR>hx : x ≠ ↑a✝<VAR>inst✝¹ : DiscreteTopology ↥(zmultiples p)<VAR>inst✝ : DenselyOrdered 𝕜<VAR>a : 𝕜<GOAL>∃ e, a ∈ e.source ∧ QuotientAddGroup.mk = ↑e
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝⁵ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a✝ : 𝕜<VAR>inst✝² : Archimedean 𝕜<VAR>x : AddCircle p<VAR>hx : x ≠ ↑a✝<VAR>inst✝¹ : DiscreteTopology ↥(zmultiples p)<VAR>inst✝ : DenselyOrdered 𝕜<VAR>a b : 𝕜<VAR>hb1 : a - p < b<VAR>hb2 : b < a<GOAL>∃ e, a ∈ e.source ∧ QuotientAddGroup.mk = ↑e
<VAR>R : Type u_2<VAR>K : Type ?u.11266<VAR>L : Type ?u.11269<VAR>S : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra K L<VAR>x : S<VAR>hx : IsIntegral R x<VAR>inst✝ : Nontrivial S<VAR>e : minpolyDiv R x = 0<GOAL>False
<VAR>R : Type u_2<VAR>K : Type ?u.11266<VAR>L : Type ?u.11269<VAR>S : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra K L<VAR>x : S<VAR>hx : IsIntegral R x<VAR>inst✝ : Nontrivial S<VAR>e : minpolyDiv R x = 0<VAR>this : minpolyDiv R x * (X - C x) = map (algebraMap R S) (minpoly R x)<GOAL>False
<VAR>R : Type u_2<VAR>K : Type ?u.11266<VAR>L : Type ?u.11269<VAR>S : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra K L<VAR>x : S<VAR>hx : IsIntegral R x<VAR>inst✝ : Nontrivial S<VAR>e : minpolyDiv R x = 0<VAR>this : 0 = map (algebraMap R S) (minpoly R x)<GOAL>False
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>g : G<GOAL>index ((fun h => g * h) '' K) V ≤ index K V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>g : G<VAR>s : Finset G<VAR>h1s : K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K V<GOAL>index ((fun h => g * h) '' K) V ≤ index K V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>g : G<VAR>s : Finset G<VAR>h1s : K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K V<GOAL>index ((fun h => g * h) '' K) V ≤ s.card
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>g : G<VAR>s : Finset G<VAR>h1s : K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K V<GOAL>s.card ∈ Finset.card '' {t | (fun h => g * h) '' K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>g : G<VAR>s : Finset G<VAR>h1s : K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K V<GOAL>∃ x ∈ {t | (fun h => g * h) '' K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}, x.card = s.card
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>g : G<VAR>s : Finset G<VAR>h1s : K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K V<GOAL>Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s ∈ {t | (fun h => g * h) '' K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>g : G<VAR>s : Finset G<VAR>h1s : K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K V<GOAL>(fun h => g * h) '' K ⊆ ⋃ g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s, (fun h => g_1 * h) ⁻¹' V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>g : G<VAR>s : Finset G<VAR>h1s : K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K V<GOAL>(fun h => g * h) '' ⋃ g ∈ s, (fun h => g * h) ⁻¹' V ⊆ ⋃ g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s, (fun h => g_1 * h) ⁻¹' V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>g : G<VAR>s : Finset G<VAR>h1s : K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K V<VAR>g₁ g₂ : G<VAR>hg₂ : g₂ ∈ s<VAR>hg₁ : g₁ ∈ (fun h => (fun h => g₂ * h) ⁻¹' V) hg₂<GOAL>(fun h => g * h) g₁ ∈ ⋃ g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s, (fun h => g_1 * h) ⁻¹' V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>g : G<VAR>s : Finset G<VAR>h1s : K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K V<VAR>g₁ g₂ : G<VAR>hg₂ : g₂ ∈ s<VAR>hg₁ : g₂ * g₁ ∈ V<GOAL>(fun h => g * h) g₁ ∈ ⋃ g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s, (fun h => g_1 * h) ⁻¹' V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>g : G<VAR>s : Finset G<VAR>h1s : K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K V<VAR>g₁ g₂ : G<VAR>hg₂ : g₂ ∈ s<VAR>hg₁ : g₂ * g₁ ∈ V<GOAL>∃ a ∈ s, a * g⁻¹ * (g * g₁) ∈ V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>g : G<VAR>s : Finset G<VAR>h1s : K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K V<VAR>g₁ g₂ : G<VAR>hg₂ : g₂ ∈ s<VAR>hg₁ : g₂ * g₁ ∈ V<GOAL>g₂ * g⁻¹ * (g * g₁) ∈ V
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>U : Comonad C<VAR>X Y x✝ : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ x✝<GOAL>U.ε.app X ≫ f ≫ g = U.δ.app X ≫ U.map (U.ε.app X ≫ f) ≫ U.ε.app Y ≫ g
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>z : 𝕜<VAR>hz : z ∈ s<VAR>hxz : x < z<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>y : 𝕜 := a * x + b * z<GOAL>f (a • x + b • z) ≤ a • f x + b • f z
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>z : 𝕜<VAR>hz : z ∈ s<VAR>hxz : x < z<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>y : 𝕜 := a * x + b * z<VAR>hxy : x < y<GOAL>f (a • x + b • z) ≤ a • f x + b • f z
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>z : 𝕜<VAR>hz : z ∈ s<VAR>hxz : x < z<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>y : 𝕜 := a * x + b * z<VAR>hxy : x < y<VAR>hyz : y < z<GOAL>f (a • x + b • z) ≤ a • f x + b • f z