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>γ : Type u_5<VAR>ι : Type u_6<VAR>x : ι → α<VAR>f : Filter α<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>hxy : ¬Tendsto x l f<VAR>s : Set α<VAR>hs : s ∈ f<VAR>hfreq : ∃ᶠ (n : ι) in l, x n ∉ s<VAR>y : ℕ → ι<VAR>hy_tendsto : Tendsto y atTop l<VAR>hy_freq : ∀ (n : ℕ), x (y n) ∉ s<VAR>ms : ℕ → ℕ<VAR>hms_tendsto : Tendsto (fun n => x (y (ms n))) atTop f<VAR>n : ℕ<VAR>hn : x (y (ms n)) ∈ s<GOAL>False
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y p₂ : P<VAR>h : p₂ ∈ s<GOAL>s.SOppSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y p₂ : P<VAR>h : p₂ ∈ s<GOAL>x ∉ s → y ∉ s → ((y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y p₂ : P<VAR>h : p₂ ∈ s<VAR>a✝ : x ∉ s<VAR>hy : y ∉ s<GOAL>(y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>R : Type u_12<VAR>R' : Type u_13<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<VAR>inst✝¹² : Norm E<VAR>inst✝¹¹ : Norm F<VAR>inst✝¹⁰ : Norm G<VAR>inst✝⁹ : SeminormedAddCommGroup E'<VAR>inst✝⁸ : SeminormedAddCommGroup F'<VAR>inst✝⁷ : SeminormedAddCommGroup G'<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedAddCommGroup F''<VAR>inst✝⁴ : NormedAddCommGroup G''<VAR>inst✝³ : SeminormedRing R<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedField 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g✝ : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>l l' : Filter α<VAR>f : α → 𝕜<VAR>g : α → 𝕜'<VAR>h : (fun x => (f x)⁻¹) =Θ[l] fun x => (g x)⁻¹<GOAL>f =Θ[l] g
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s : Multiset α<GOAL>s.toList = [] ↔ s = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤<GOAL>(μ.withDensity f) univ < ⊤
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>b⁻¹ * a < c ↔ a < b * c
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>i j : Fin 2<GOAL>(basisOneI.repr (![1, I] i)) j = (Finsupp.single i 1) j
<VAR>m n✝ n : ℕ<GOAL>(n + 1) * (n + 1) ^ n = (n + 1) ^ (n + 1)
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<GOAL>∃ g, ↑g 1 = cd ∧ ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<VAR>this : Nonempty { g // ↑g 1 = cd }<GOAL>∃ g, ↑g 1 = cd ∧ ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|
<VAR>g✝ : SL(2, ℤ)<VAR>z : ℍ<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<VAR>this : Nonempty { g // ↑g 1 = cd }<VAR>g : { g // ↑g 1 = cd }<VAR>hg : ∀ (a : { g // ↑g 1 = cd }), |(↑g • z).re| ≤ |(↑a • z).re|<GOAL>∃ g, ↑g 1 = cd ∧ ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|
<VAR>g✝ : SL(2, ℤ)<VAR>z : ℍ<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<VAR>this : Nonempty { g // ↑g 1 = cd }<VAR>g : { g // ↑g 1 = cd }<VAR>hg : ∀ (a : { g // ↑g 1 = cd }), |(↑g • z).re| ≤ |(↑a • z).re|<GOAL>∀ (g' : SL(2, ℤ)), ↑↑g 1 = ↑g' 1 → |(↑g • z).re| ≤ |(g' • z).re|
<VAR>g✝ : SL(2, ℤ)<VAR>z : ℍ<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<VAR>this : Nonempty { g // ↑g 1 = cd }<VAR>g : { g // ↑g 1 = cd }<VAR>hg : ∀ (a : { g // ↑g 1 = cd }), |(↑g • z).re| ≤ |(↑a • z).re|<VAR>g1 : SL(2, ℤ)<VAR>hg1 : ↑↑g 1 = ↑g1 1<GOAL>|(↑g • z).re| ≤ |(g1 • z).re|
<VAR>g✝ : SL(2, ℤ)<VAR>z : ℍ<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<VAR>this✝ : Nonempty { g // ↑g 1 = cd }<VAR>g : { g // ↑g 1 = cd }<VAR>hg : ∀ (a : { g // ↑g 1 = cd }), |(↑g • z).re| ≤ |(↑a • z).re|<VAR>g1 : SL(2, ℤ)<VAR>hg1 : ↑↑g 1 = ↑g1 1<VAR>this : g1 ∈ (fun g => ↑g 1) ⁻¹' {cd}<GOAL>|(↑g • z).re| ≤ |(g1 • z).re|
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type ?u.85209<VAR>inst✝ : MulAction R X<VAR>r : R<VAR>hr : r ∈ S<GOAL>r /ₒ ⟨r, hr⟩ = 1
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type ?u.85209<VAR>inst✝ : MulAction R X<VAR>r : R<VAR>hr : r ∈ S<GOAL>∃ u v, u • 1 = v • r ∧ ↑u * ↑1 = v * ↑⟨r, hr⟩
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁷ : Countable ι<VAR>f✝ g✝ : α✝ → β<VAR>mα : MeasurableSpace α✝<VAR>inst✝⁶ : TopologicalSpace β<VAR>α : Type u_5<VAR>E : Type u_6<VAR>x✝ : MeasurableSpace α<VAR>inst✝⁵ : AddGroup E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : PseudoMetrizableSpace E<VAR>g f : α → E<VAR>hg : Measurable g<VAR>φ : ℕ → α →ₛ E<VAR>hφ : ∀ (x : α), Tendsto (fun n => ↑(φ n) x) atTop (𝓝 (f x))<GOAL>Measurable (g + f)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁷ : Countable ι<VAR>f✝ g✝ : α✝ → β<VAR>mα : MeasurableSpace α✝<VAR>inst✝⁶ : TopologicalSpace β<VAR>α : Type u_5<VAR>E : Type u_6<VAR>x✝ : MeasurableSpace α<VAR>inst✝⁵ : AddGroup E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : PseudoMetrizableSpace E<VAR>g f : α → E<VAR>hg : Measurable g<VAR>φ : ℕ → α →ₛ E<VAR>hφ : ∀ (x : α), Tendsto (fun n => ↑(φ n) x) atTop (𝓝 (f x))<VAR>this : Tendsto (fun n x => g x + ↑(φ n) x) atTop (𝓝 (g + f))<GOAL>Measurable (g + f)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁷ : Countable ι<VAR>f✝ g✝ : α✝ → β<VAR>mα : MeasurableSpace α✝<VAR>inst✝⁶ : TopologicalSpace β<VAR>α : Type u_5<VAR>E : Type u_6<VAR>x✝ : MeasurableSpace α<VAR>inst✝⁵ : AddGroup E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : PseudoMetrizableSpace E<VAR>g f : α → E<VAR>hg : Measurable g<VAR>φ : ℕ → α →ₛ E<VAR>hφ : ∀ (x : α), Tendsto (fun n => ↑(φ n) x) atTop (𝓝 (f x))<VAR>this : Tendsto (fun n x => g x + ↑(φ n) x) atTop (𝓝 (g + f))<VAR>n : ℕ<GOAL>Measurable fun x => g x + ↑(φ n) x
<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 : α × β → γ<GOAL>Continuous f ↔ ∀ (a : α), Continuous fun x => f (a, x)
<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 : α × β → γ<GOAL>ContinuousOn f univ ↔ ∀ (a : α), ContinuousOn (fun x => f (a, x)) univ
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizationMonoid R<VAR>p : R[X]<VAR>hp : p.Monic<GOAL>normalize p = p
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : V<VAR>e : EuclideanSpace ℝ (Fin (FiniteDimensional.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm<GOAL>Integrable (fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫_ℝ)) volume
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : V<VAR>e : EuclideanSpace ℝ (Fin (FiniteDimensional.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm<GOAL>Integrable ((fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫_ℝ)) ∘ ⇑e) volume
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : V<VAR>e : EuclideanSpace ℝ (Fin (FiniteDimensional.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm<VAR>v : EuclideanSpace ℝ (Fin (FiniteDimensional.finrank ℝ V))<GOAL>((fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫_ℝ)) ∘ ⇑e) v = cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪e.symm w, v⟫_ℝ)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Nontrivial R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Module R A<VAR>inst✝² : IsScalarTower R A A<VAR>inst✝¹ : SMulCommClass R A A<VAR>inst✝ : NonUnitalContinuousFunctionalCalculus R p<VAR>f✝ g : R → R<VAR>a✝ : A<VAR>hf✝ : autoParam (ContinuousOn f✝ (σₙ R a✝)) _auto✝<VAR>hf0 : autoParam (f✝ 0 = 0) _auto✝<VAR>hg : autoParam (ContinuousOn g (σₙ R a✝)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>ha : autoParam (p a✝) _auto✝<VAR>f : R → R<VAR>a : A<VAR>hf : ¬f 0 = 0<GOAL>cfcₙ f a = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : OrderTop β<VAR>f : α → β<VAR>H : StrictMono f<VAR>a : α<VAR>h_top : f a = ⊤<VAR>x : α<VAR>p : β<GOAL>p ≤ ⊤
<VAR>x✝ y z x : ℝ<VAR>n : ℤ<GOAL>x ^ ↑n = x ^ n
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<VAR>hl : rdropWhile p l ≠ []<GOAL>¬p ((dropWhile p l.reverse).reverse.getLast ⋯) = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<VAR>hl : rdropWhile p l ≠ []<GOAL>¬p ((dropWhile p l.reverse).get ⟨0, ⋯⟩) = true
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝¹ s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝¹ g✝¹ : α✝ → β<VAR>inst✝² : CommMonoid β<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝¹ : CommMonoid α<VAR>s✝ : Finset ι<VAR>t✝ : Finset κ<VAR>f✝ : ι → α<VAR>g✝ : κ → α<VAR>inst✝ : DecidableEq κ<VAR>s : Finset ι<VAR>t : Finset κ<VAR>g : ι → κ<VAR>f : ι → α<GOAL>∏ j ∈ t, ∏ i ∈ filter (fun i => g i = j) s, f i = ∏ i ∈ filter (fun i => g i ∈ t) s, f i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>β✝² : ι → Type u_4<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<VAR>x : (i : ι) × α i<VAR>i j : ι<VAR>a✝ : α i<VAR>β✝¹ : Type u_5<VAR>inst✝ : CompleteLattice β✝¹<VAR>β✝ : Type u_6<VAR>β : ι → Type u_7<VAR>a : (i : ι) → α i<GOAL>(s.sigma fun i => insert (a i) (t i)) = (fun i => ⟨i, a i⟩) '' s ∪ s.sigma t
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b : σ<VAR>h : b ∈ eval f a<VAR>c : σ<VAR>left✝ : Reaches f a b<VAR>b0 : f b = none<VAR>b' : σ<VAR>h' : b' ∈ f b<GOAL>False
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>h : Nonempty ↑(Ioi a)<GOAL>(𝓝ˢ (Iic a)).HasBasis (fun x => a < x) Iio
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>h : Nonempty ↑(Ioi a)<VAR>s : Set α<VAR>hs : s ∈ 𝓝ˢ (Iic a)<GOAL>∃ i, a < i ∧ Iio i ⊆ s
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>h : Nonempty ↑(Ioi a)<VAR>s : Set α<VAR>hs : s ∈ 𝓝 a ∧ Iio a ⊆ s<GOAL>∃ i, a < i ∧ Iio i ⊆ s
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>h : Nonempty ↑(Ioi a)<VAR>s : Set α<VAR>hs : s ∈ 𝓝 a ∧ Iio a ⊆ s<VAR>b : α<VAR>hab : a < b<VAR>hbs : Ico a b ⊆ s<GOAL>∃ i, a < i ∧ Iio i ⊆ s
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x : ↑((inhomogeneousCochains A).X 1)<VAR>y : G × G<GOAL>(A.ρ y.1) (x ((Equiv.funUnique (Fin 1) G).symm y.2)) - x ((Equiv.funUnique (Fin 1) G).symm (y.1 * y.2)) + x ((Equiv.funUnique (Fin 1) G).symm y.1) = (A.ρ ((piFinTwoEquiv fun x => G).symm y 0)) (x fun i => (piFinTwoEquiv fun x => G).symm y i.succ) + ∑ j : Fin (1 + 1), (-1) ^ (↑j + 1) • x (j.contractNth (fun x x_1 => x * x_1) ((piFinTwoEquiv fun x => G).symm y))
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x : ↑((inhomogeneousCochains A).X 1)<VAR>y : G × G<GOAL>(A.ρ y.1) (x ((Equiv.funUnique (Fin 1) G).symm y.2)) - x ((Equiv.funUnique (Fin 1) G).symm (y.1 * y.2)) + x ((Equiv.funUnique (Fin 1) G).symm y.1) = (A.ρ ((piFinTwoEquiv fun x => G).symm y 0)) (x fun i => (piFinTwoEquiv fun x => G).symm y i.succ) + ((-1) ^ (↑0 + 1) • x (Fin.contractNth 0 (fun x x_1 => x * x_1) ((piFinTwoEquiv fun x => G).symm y)) + (-1) ^ (↑1 + 1) • x (Fin.contractNth 1 (fun x x_1 => x * x_1) ((piFinTwoEquiv fun x => G).symm y)))
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x : ↑((inhomogeneousCochains A).X 1)<VAR>y : G × G<GOAL>(A.ρ y.1) (x ((Equiv.funUnique (Fin 1) G).symm y.2)) + (-x ((Equiv.funUnique (Fin 1) G).symm (y.1 * y.2)) + x ((Equiv.funUnique (Fin 1) G).symm y.1)) = (A.ρ ((piFinTwoEquiv fun x => G).symm y 0)) (x fun i => (piFinTwoEquiv fun x => G).symm y i.succ) + (-x (Fin.contractNth 0 (fun x x_1 => x * x_1) ((piFinTwoEquiv fun x => G).symm y)) + x (Fin.contractNth 1 (fun x x_1 => x * x_1) ((piFinTwoEquiv fun x => G).symm y)))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>X.σ i ≫ PInfty.f (n + 1) = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>n + 1 ≤ ↑i + (n + 1)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Preorder ι<VAR>u✝ v : ι → Ω → β<VAR>f : Filtration ι m<VAR>inst✝¹ : MetrizableSpace β<VAR>mβ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>u : ι → Ω → β<VAR>hum : ∀ (i : ι), StronglyMeasurable (u i)<VAR>i : ι<GOAL>StronglyMeasurable (u i)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Preorder ι<VAR>u✝ v : ι → Ω → β<VAR>f : Filtration ι m<VAR>inst✝¹ : MetrizableSpace β<VAR>mβ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>u : ι → Ω → β<VAR>hum : ∀ (i : ι), StronglyMeasurable (u i)<VAR>i : ι<GOAL>Measurable (u i) ∧ IsSeparable (Set.range (u i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : PredOrder α<VAR>a b : α<VAR>k : ℕ<VAR>x : α<GOAL>pred^[k] x ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : PredOrder α<VAR>a b : α<VAR>k : ℕ<VAR>x : α<GOAL>pred^[k] x ≤ id^[k] x
<VAR>m n✝ a b c d n : ℕ<GOAL>n % 4 = 1 → n % 2 = 1
<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>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>∠ p₁ p₂ p₃ = π
<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>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
<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>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<VAR>r : ℝ<VAR>hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂<VAR>hr0 : 0 ≤ r<VAR>hr1 : r ≤ 1<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₃ : p₂ ≠ p₃<GOAL>p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
<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>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<VAR>r : ℝ<VAR>hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂<VAR>hr0 : 0 ≤ r<VAR>hr1 : r ≤ 1<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₃ : p₂ ≠ p₃<GOAL>-(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
<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>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<VAR>r : ℝ<VAR>hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂<VAR>hr0 : 0 ≤ r<VAR>hr1 : r ≤ 1<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₃ : p₂ ≠ p₃<VAR>hr0' : r ≠ 0<VAR>hr1' : r ≠ 1<GOAL>-(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
<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>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<VAR>r : ℝ<VAR>hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂<VAR>hr1 : r ≤ 1<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₃ : p₂ ≠ p₃<VAR>hr0' : r ≠ 0<VAR>hr1' : r ≠ 1<VAR>hr0 : 0 < r<GOAL>-(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
<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>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<VAR>r : ℝ<VAR>hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₃ : p₂ ≠ p₃<VAR>hr0' : r ≠ 0<VAR>hr1' : r ≠ 1<VAR>hr0 : 0 < r<VAR>hr1 : r < 1<GOAL>-(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
<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>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<VAR>r : ℝ<VAR>hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₃ : p₂ ≠ p₃<VAR>hr0' : r ≠ 0<VAR>hr1' : r ≠ 1<VAR>hr0 : 0 < r<VAR>hr1 : r < 1<GOAL>p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>ε' : 𝕜<VAR>h : ε ≤ ε'<VAR>hε : G.IsUniform ε s t<VAR>s' : Finset α<VAR>hs' : s' ⊆ s<VAR>t' : Finset α<VAR>ht' : t' ⊆ t<VAR>hs : ↑s.card * ε' ≤ ↑s'.card<VAR>ht : ↑t.card * ε' ≤ ↑t'.card<GOAL>|↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < ε'
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>inst✝ : l.NeBot<VAR>s : Set E<VAR>hs : IsOpen s<VAR>hf' : TendstoLocallyUniformlyOn (fderiv 𝕜 ∘ f) g' l s<VAR>hf : ∀ (n : ι), DifferentiableOn 𝕜 (f n) s<VAR>hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>hx : x ∈ s<GOAL>HasFDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>inst✝ : l.NeBot<VAR>s : Set E<VAR>hs : IsOpen s<VAR>hf' : TendstoLocallyUniformlyOn (fderiv 𝕜 ∘ f) g' l s<VAR>hf : ∀ (n : ι), DifferentiableOn 𝕜 (f n) s<VAR>hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>hx : x ∈ s<VAR>n : ι<VAR>z : E<VAR>hz : z ∈ s<GOAL>HasFDerivAt (f n) ((fderiv 𝕜 ∘ f) n z) z
<VAR>R S : Type u<VAR>M✝ : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁷ : Ring R<VAR>inst✝¹⁶ : CommRing S<VAR>inst✝¹⁵ : AddCommGroup M✝<VAR>inst✝¹⁴ : AddCommGroup M'<VAR>inst✝¹³ : AddCommGroup M₁<VAR>inst✝¹² : Module R M✝<VAR>inst✝¹¹ : Module R M'<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : StrongRankCondition R<VAR>inst✝⁸ : Module.Free R M✝<VAR>inst✝⁷ : (i : η) → AddCommGroup (φ i)<VAR>inst✝⁶ : (i : η) → Module R (φ i)<VAR>inst✝⁵ : ∀ (i : η), Module.Free R (φ i)<VAR>ι : Type v<VAR>inst✝⁴ : Fintype ι<VAR>M : ι → Type w<VAR>inst✝³ : (i : ι) → AddCommGroup (M i)<VAR>inst✝² : (i : ι) → Module R (M i)<VAR>inst✝¹ : ∀ (i : ι), Module.Free R (M i)<VAR>inst✝ : ∀ (i : ι), Module.Finite R (M i)<GOAL>finrank R ((i : ι) → M i) = ∑ i : ι, finrank R (M i)
<VAR>R S : Type u<VAR>M✝ : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁷ : Ring R<VAR>inst✝¹⁶ : CommRing S<VAR>inst✝¹⁵ : AddCommGroup M✝<VAR>inst✝¹⁴ : AddCommGroup M'<VAR>inst✝¹³ : AddCommGroup M₁<VAR>inst✝¹² : Module R M✝<VAR>inst✝¹¹ : Module R M'<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : StrongRankCondition R<VAR>inst✝⁸ : Module.Free R M✝<VAR>inst✝⁷ : (i : η) → AddCommGroup (φ i)<VAR>inst✝⁶ : (i : η) → Module R (φ i)<VAR>inst✝⁵ : ∀ (i : η), Module.Free R (φ i)<VAR>ι : Type v<VAR>inst✝⁴ : Fintype ι<VAR>M : ι → Type w<VAR>inst✝³ : (i : ι) → AddCommGroup (M i)<VAR>inst✝² : (i : ι) → Module R (M i)<VAR>inst✝¹ : ∀ (i : ι), Module.Free R (M i)<VAR>inst✝ : ∀ (i : ι), Module.Finite R (M i)<VAR>this : Nontrivial R := nontrivial_of_invariantBasisNumber R<GOAL>finrank R ((i : ι) → M i) = ∑ i : ι, finrank R (M i)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>inst✝ : PseudoMetricSpace β<VAR>t : Set β<VAR>f : α → β<VAR>a : α<VAR>b : β<GOAL>(∀ (ib : ℝ), 0 < ib → ∃ ia, 0 < ia ∧ ∀ x ∈ ball a ia ∩ s, f x ∈ ball b ib ∩ t) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → dist x a < δ → f x ∈ t ∧ dist (f x) b < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Denumerable α<VAR>inst✝ : Denumerable β<VAR>n : ℕ<GOAL>encode (ofNat α n) = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Denumerable α<VAR>inst✝ : Denumerable β<VAR>n : ℕ<VAR>a : α<VAR>h : a ∈ decode n<VAR>e : encode a = n<GOAL>encode (ofNat α n) = n
<VAR>x : ℝ<VAR>hx₁ : -(2 * π) < x<VAR>hx₂ : x < 2 * π<VAR>h : cos x = 1<GOAL>x = 0
<VAR>n : ℤ<VAR>hx₁ : -(2 * π) < ↑n * (2 * π)<VAR>hx₂ : ↑n * (2 * π) < 2 * π<VAR>h : cos (↑n * (2 * π)) = 1<GOAL>↑n * (2 * π) = 0
<VAR>n : ℤ<VAR>hx₁ : -(2 * π) < ↑n * (2 * π)<VAR>hx₂ : ↑n < 1<VAR>h : cos (↑n * (2 * π)) = 1<GOAL>↑n * (2 * π) = 0
<VAR>n : ℤ<VAR>hx₁ : -↑n < 1<VAR>hx₂ : ↑n < 1<VAR>h : cos (↑n * (2 * π)) = 1<GOAL>↑n * (2 * π) = 0
<VAR>n : ℤ<VAR>h : cos (↑n * (2 * π)) = 1<VAR>hx₁ : -n < 1<VAR>hx₂ : n < 1<GOAL>↑n * (2 * π) = 0
<VAR>h : cos (↑0 * (2 * π)) = 1<VAR>hx₁ : -0 < 1<VAR>hx₂ : 0 < 1<GOAL>↑0 * (2 * π) = 0
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>y : (n : ℕ) → E n<VAR>hy : y ∈ s<GOAL>0 < shortestPrefixDiff x s
<VAR>p : ℚ → Prop<VAR>h : ∀ (a b : ℤ), p (↑a / ↑b)<VAR>q : ℚ<VAR>this : p (↑q.num / ↑↑q.den)<GOAL>p q
<VAR>S : Type u'<VAR>T : Type u''<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Monoid R<VAR>inst✝³ : MulAction R M<VAR>inst✝² : SMul S R<VAR>inst✝¹ : SMul S M<VAR>inst✝ : IsScalarTower S R M<VAR>p : SubMulAction R M<VAR>s : S<VAR>x : M<VAR>h : x ∈ p<GOAL>s • x ∈ p
<VAR>S : Type u'<VAR>T : Type u''<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Monoid R<VAR>inst✝³ : MulAction R M<VAR>inst✝² : SMul S R<VAR>inst✝¹ : SMul S M<VAR>inst✝ : IsScalarTower S R M<VAR>p : SubMulAction R M<VAR>s : S<VAR>x : M<VAR>h : x ∈ p<GOAL>(s • 1) • x ∈ p