ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>0 < -x ↔ x < 0
<VAR>x : ℝ*<VAR>h0 : ¬x = 0<VAR>h1 : ¬x.Infinitesimal<VAR>h2 : ¬x.Infinite<GOAL>x⁻¹.st = x.st⁻¹
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b : σ<VAR>ab : Reaches f a b<GOAL>eval f a = eval f b
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b : σ<VAR>ab : Reaches f a b<VAR>x✝ : σ<VAR>h : x✝ ∈ eval f a<GOAL>x✝ ∈ eval f b
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b : σ<VAR>ab : Reaches f a b<VAR>x✝ : σ<VAR>h : x✝ ∈ eval f b<GOAL>x✝ ∈ eval f a
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L✝ : HomologicalComplex C c<VAR>i j k : ι<VAR>hK : K.ExactAt i<VAR>L : HomologicalComplex C c<VAR>e : K ≅ L<GOAL>L.ExactAt i
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L✝ : HomologicalComplex C c<VAR>i j k : ι<VAR>hK : (K.sc i).Exact<VAR>L : HomologicalComplex C c<VAR>e : K ≅ L<GOAL>(L.sc i).Exact
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<GOAL>a < sup f ↔ ∃ i, a < f i
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroObject C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>inst✝ : HasBinaryProduct X Y<GOAL>(pullbackZeroZeroIso X Y).hom ≫ prod.fst = pullback.fst 0 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>f '' (f ⁻¹' t ∩ s) = t ∩ f '' s
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>t : Finset σ × σ<VAR>h : t ∈ MvPolynomial.NewtonIdentities.pairs σ k<GOAL>MvPolynomial.NewtonIdentities.pairMap σ t ∈ MvPolynomial.NewtonIdentities.pairs σ k
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>t : Finset σ × σ<VAR>h : t.1.card ≤ k ∧ (t.1.card = k → t.2 ∈ t.1)<GOAL>(MvPolynomial.NewtonIdentities.pairMap σ t).1.card ≤ k ∧ ((MvPolynomial.NewtonIdentities.pairMap σ t).1.card = k → (MvPolynomial.NewtonIdentities.pairMap σ t).2 ∈ (MvPolynomial.NewtonIdentities.pairMap σ t).1)
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>inst✝ : Ring R<VAR>s : Set Rᵐᵒᵖ<GOAL>(closure s).unop = closure (MulOpposite.op ⁻¹' s)
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>inst✝ : Ring R<VAR>s : Set Rᵐᵒᵖ<GOAL>sInf {a | s ⊆ MulOpposite.unop ⁻¹' ↑a} = sInf {S | MulOpposite.op ⁻¹' s ⊆ ↑S}
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>inst✝ : Ring R<VAR>s : Set Rᵐᵒᵖ<VAR>a : Subring R<GOAL>a ∈ {a | s ⊆ MulOpposite.unop ⁻¹' ↑a} ↔ a ∈ {S | MulOpposite.op ⁻¹' s ⊆ ↑S}
<VAR>x : ℂ<GOAL>∃ a, sin a = x
<VAR>z : ℂ<GOAL>∃ a, sin a = cos z
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>g : Set α → Filter β<VAR>hg : Monotone g<GOAL>(𝓝 x).lift g = (𝓤 α).lift fun s => g {y | (y, x) ∈ s}
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>g : Set α → Filter β<VAR>hg : Monotone g<GOAL>(𝓤 α).lift (g ∘ preimage fun y => (y, x)) = (𝓤 α).lift fun s => g {y | (y, x) ∈ s}
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocMod hp (p + a) b = p + toIocMod hp a b
<VAR>R : Type u<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : OrzechProperty R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module.Finite R M<VAR>N : Type w<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>i f : N →ₗ[R] M<VAR>hi : Injective ⇑i<VAR>hf : Surjective ⇑f<GOAL>Injective ⇑f
<VAR>R : Type u<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : OrzechProperty R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module.Finite R M<VAR>N : Type w<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>i f : N →ₗ[R] M<VAR>hi : Injective ⇑i<VAR>hf : Surjective ⇑f<VAR>n : ℕ<VAR>g : (Fin n → R) →ₗ[R] M<VAR>hg : Surjective ⇑g<GOAL>Injective ⇑f
<VAR>R : Type u<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : OrzechProperty R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module.Finite R M<VAR>N : Type w<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>i f : N →ₗ[R] M<VAR>hi : Injective ⇑i<VAR>hf : Surjective ⇑f<VAR>n : ℕ<VAR>g : (Fin n → R) →ₗ[R] M<VAR>hg : Surjective ⇑g<VAR>this : Small.{u, v} M<GOAL>Injective ⇑f
<VAR>R : Type u<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : OrzechProperty R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module.Finite R M<VAR>N : Type w<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>i f : N →ₗ[R] M<VAR>hi : Injective ⇑i<VAR>hf : Surjective ⇑f<VAR>n : ℕ<VAR>g : (Fin n → R) →ₗ[R] M<VAR>hg : Surjective ⇑g<VAR>this✝¹ : Small.{u, v} M<VAR>this✝ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid<VAR>this : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm<VAR>j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm<GOAL>Injective ⇑f
<VAR>R : Type u<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : OrzechProperty R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module.Finite R M<VAR>N : Type w<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>i f : N →ₗ[R] M<VAR>hi : Injective ⇑i<VAR>hf : Surjective ⇑f<VAR>n : ℕ<VAR>g : (Fin n → R) →ₗ[R] M<VAR>hg : Surjective ⇑g<VAR>this✝² : Small.{u, v} M<VAR>this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid<VAR>this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm<VAR>j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm<VAR>this : Module.Finite R (Shrink.{u, v} M)<GOAL>Injective ⇑f
<VAR>R : Type u<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : OrzechProperty R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module.Finite R M<VAR>N : Type w<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>i f : N →ₗ[R] M<VAR>n : ℕ<VAR>g : (Fin n → R) →ₗ[R] M<VAR>hg : Surjective ⇑g<VAR>this✝² : Small.{u, v} M<VAR>this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid<VAR>this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm<VAR>j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm<VAR>this : Module.Finite R (Shrink.{u, v} M)<VAR>i' : N →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ i<VAR>hi : Injective ⇑i'<VAR>f' : ↥(LinearMap.range i') →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ f ∘ₗ ↑(LinearEquiv.ofInjective i' hi).symm<VAR>hf : Surjective ⇑f'<GOAL>Injective ⇑f
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>K : Type u_3<VAR>C : Type u_4<VAR>inst✝³ : Category.{u_5, u_4} C<VAR>X Y Z : GradedObject I C<VAR>φ✝ : X ⟶ Y<VAR>e : X ≅ Y<VAR>ψ : Y ⟶ Z<VAR>p : I → J<VAR>j✝ : J<VAR>inst✝² : X.HasMap p<VAR>inst✝¹ : Y.HasMap p<VAR>inst✝ : Z.HasMap p<VAR>A : C<VAR>j : J<VAR>φ : (i : I) → p i = j → (X i ⟶ A)<VAR>i : I<VAR>hi : p i = j<GOAL>X.ιMapObj p i j hi ≫ X.descMapObj p φ = φ i hi
<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✝ : NonUnitalNonAssocRing α<VAR>u v w : m → α<GOAL>u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w
<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 p : P<VAR>hx : x ∉ s<VAR>hp : p ∈ s<VAR>y : P<GOAL>y ∈ {y | s.SSameSide x y} ↔ y ∈ Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) ↑s
<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 p : P<VAR>hx : x ∉ s<VAR>hp : p ∈ s<VAR>y : P<GOAL>s.SSameSide x y ↔ ∃ a, 0 < a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
<VAR>α : Type u_1<VAR>inst✝ : AddCommMonoid α<VAR>c n : ℕ<VAR>x a : α<VAR>n' : ℕ<VAR>a' : α<VAR>h₁ : c * n = n'<VAR>h₂ : smul c a = a'<GOAL>smul c (term n x a) = term n' x a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝ : IsFiniteKernel κ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<GOAL>∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω), f x ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝ : IsFiniteKernel κ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<GOAL>∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω), f x ∂(κ.fst ⊗ₖ κ.condKernel) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<GOAL>𝓝 [] = pure []
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Semiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f✝ : F<VAR>I✝ J : Ideal R<VAR>K L : Ideal S<VAR>G : Type u_2<VAR>inst✝ : FunLike G S R<VAR>rcg : RingHomClass G S R<VAR>ι : Sort u_3<VAR>I : Ideal R<VAR>f : R ≃+* S<GOAL>map (↑f.symm) (map (↑f) I) = I
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>hc : ¬IsConnected X<VAR>hi : IsInitial X → False<GOAL>∃ Y v, (IsInitial Y → False) ∧ Mono v ∧ ¬IsIso v
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>hi : IsInitial X → False<VAR>hc : ∀ (Y : C) (v : Y ⟶ X), (IsInitial Y → False) → Mono v → IsIso v<GOAL>IsConnected X
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a b m : ℝ<VAR>x y : E<VAR>f g : E → ℝ<VAR>hf : UniformConcaveOn s φ f<VAR>hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r<GOAL>StrictConcaveOn ℝ s f
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a✝ b✝ m : ℝ<VAR>x✝ y✝ : E<VAR>f g : E → ℝ<VAR>hf : UniformConcaveOn s φ f<VAR>hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>0 < a * b * φ ‖x - y‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a✝ b✝ m : ℝ<VAR>x✝ y✝ : E<VAR>f g : E → ℝ<VAR>hf : UniformConcaveOn s φ f<VAR>hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : 0 < ‖x - y‖<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>0 < a * b * φ ‖x - y‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a✝ b✝ m : ℝ<VAR>x✝ y✝ : E<VAR>f g : E → ℝ<VAR>hf : UniformConcaveOn s φ f<VAR>hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : 0 < ‖x - y‖<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>this : 0 < φ ‖x - y‖<GOAL>0 < a * b * φ ‖x - y‖
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>h : s.PartiallyWellOrderedOn r<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ∈ s<GOAL>∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>h : s.PartiallyWellOrderedOn r<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ∈ s<VAR>g : ℕ ↪o ℕ<VAR>h1 : ∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))<GOAL>∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>h : s.PartiallyWellOrderedOn r<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ∈ s<VAR>g : ℕ ↪o ℕ<VAR>h2 : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))<GOAL>∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>hf : UniformInducing f<GOAL>CompleteSpace α ↔ IsComplete (range f)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p✝ q✝ : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>p q : ℝ≥0∞<VAR>hpq : p.toReal.IsConjExponent q.toReal<VAR>f : ↥(lp E p)<VAR>g : ↥(lp E q)<GOAL>(Summable fun i => ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p✝ q✝ : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>p q : ℝ≥0∞<VAR>hpq : p.toReal.IsConjExponent q.toReal<VAR>f : ↥(lp E p)<VAR>g : ↥(lp E q)<VAR>hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖<GOAL>(Summable fun i => ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p✝ q✝ : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>p q : ℝ≥0∞<VAR>hpq : p.toReal.IsConjExponent q.toReal<VAR>f : ↥(lp E p)<VAR>g : ↥(lp E q)<VAR>hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖<VAR>hg₁ : ∀ (i : α), 0 ≤ ‖↑g i‖<GOAL>(Summable fun i => ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p✝ q✝ : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>p q : ℝ≥0∞<VAR>hpq : p.toReal.IsConjExponent q.toReal<VAR>f : ↥(lp E p)<VAR>g : ↥(lp E q)<VAR>hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖<VAR>hg₁ : ∀ (i : α), 0 ≤ ‖↑g i‖<VAR>hf₂ : HasSum (fun i => ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)<GOAL>(Summable fun i => ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p✝ q✝ : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>p q : ℝ≥0∞<VAR>hpq : p.toReal.IsConjExponent q.toReal<VAR>f : ↥(lp E p)<VAR>g : ↥(lp E q)<VAR>hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖<VAR>hg₁ : ∀ (i : α), 0 ≤ ‖↑g i‖<VAR>hf₂ : HasSum (fun i => ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)<VAR>hg₂ : HasSum (fun i => ‖↑g i‖ ^ q.toReal) (‖g‖ ^ q.toReal)<GOAL>(Summable fun i => ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p✝ q✝ : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>p q : ℝ≥0∞<VAR>hpq : p.toReal.IsConjExponent q.toReal<VAR>f : ↥(lp E p)<VAR>g : ↥(lp E q)<VAR>hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖<VAR>hg₁ : ∀ (i : α), 0 ≤ ‖↑g i‖<VAR>hf₂ : HasSum (fun i => ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)<VAR>hg₂ : HasSum (fun i => ‖↑g i‖ ^ q.toReal) (‖g‖ ^ q.toReal)<VAR>C : ℝ<VAR>hC' : C ≤ ‖f‖ * ‖g‖<VAR>hC : HasSum (fun i => ‖↑f i‖ * ‖↑g i‖) C<GOAL>(Summable fun i => ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p✝ q✝ : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>p q : ℝ≥0∞<VAR>hpq : p.toReal.IsConjExponent q.toReal<VAR>f : ↥(lp E p)<VAR>g : ↥(lp E q)<VAR>hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖<VAR>hg₁ : ∀ (i : α), 0 ≤ ‖↑g i‖<VAR>hf₂ : HasSum (fun i => ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)<VAR>hg₂ : HasSum (fun i => ‖↑g i‖ ^ q.toReal) (‖g‖ ^ q.toReal)<VAR>C : ℝ<VAR>hC' : ∑' (b : α), ‖↑f b‖ * ‖↑g b‖ ≤ ‖f‖ * ‖g‖<VAR>hC : HasSum (fun i => ‖↑f i‖ * ‖↑g i‖) C<GOAL>(Summable fun i => ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖
<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>a✝ b✝ : ℚ<VAR>h : dist a✝ b✝ < ε<GOAL>dist |a✝| |b✝| ≤ dist a✝ b✝
<VAR>n m : ℕ<VAR>h : n < m<GOAL>Ico n m = n :: Ico (n + 1) m
<VAR>n m : ℕ<VAR>h : n < m<GOAL>[n] ++ Ico n.succ m = n :: Ico (n + 1) m
<VAR>K : Type u_1<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : TopologicalSpace K<VAR>α : Type u_2<VAR>𝕜 : Type u_3<VAR>f g : α → 𝕜<VAR>S : Set α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace 𝕜<VAR>inst✝² : T1Space 𝕜<VAR>inst✝¹ : Ring 𝕜<VAR>inst✝ : NoZeroDivisors 𝕜<VAR>hS : IsPreconnected S<VAR>hf : ContinuousOn f S<VAR>hsq : EqOn (f ^ 2) 1 S<VAR>this : DiscreteTopology ↑{1, -1}<GOAL>EqOn f 1 S ∨ EqOn f (-1) S
<VAR>K : Type u_1<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : TopologicalSpace K<VAR>α : Type u_2<VAR>𝕜 : Type u_3<VAR>f g : α → 𝕜<VAR>S : Set α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace 𝕜<VAR>inst✝² : T1Space 𝕜<VAR>inst✝¹ : Ring 𝕜<VAR>inst✝ : NoZeroDivisors 𝕜<VAR>hS : IsPreconnected S<VAR>hf : ContinuousOn f S<VAR>hsq : EqOn (f ^ 2) 1 S<VAR>this : DiscreteTopology ↑{1, -1}<VAR>hmaps : MapsTo f S {1, -1}<GOAL>EqOn f 1 S ∨ EqOn f (-1) S
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>(W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧ (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := fun {m n} {p q} => natDegree_mul_le_of_le<GOAL>(W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧ (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := fun {m n} {p q} => natDegree_mul_le_of_le<VAR>dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n<GOAL>(W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧ (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := fun {m n} {p q} => natDegree_mul_le_of_le<VAR>dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n<VAR>cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := fun {m n} {p q} => coeff_mul_of_natDegree_le<GOAL>(W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧ (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := fun {m n} {p q} => natDegree_mul_le_of_le<VAR>dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n<VAR>cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := fun {m n} {p q} => coeff_mul_of_natDegree_le<VAR>cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := fun {m n} {p} => coeff_pow_of_natDegree_le<GOAL>(W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧ (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : 1 < r<GOAL>(fun n => ↑n ^ k) =o[atTop] fun n => r ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : 1 < r<VAR>this : Tendsto (fun x => x ^ k) (𝓝[>] 1) (𝓝 1)<GOAL>(fun n => ↑n ^ k) =o[atTop] fun n => r ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : 1 < r<VAR>this : Tendsto (fun x => x ^ k) (𝓝[>] 1) (𝓝 1)<VAR>r' : ℝ<VAR>hr' : r' ^ k < r<VAR>h1 : 1 < r'<GOAL>(fun n => ↑n ^ k) =o[atTop] fun n => r ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : 1 < r<VAR>this : Tendsto (fun x => x ^ k) (𝓝[>] 1) (𝓝 1)<VAR>r' : ℝ<VAR>hr' : r' ^ k < r<VAR>h1 : 1 < r'<VAR>h0 : 0 ≤ r'<GOAL>(fun n => ↑n ^ k) =o[atTop] fun n => r ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : 1 < r<VAR>this : Tendsto (fun x => x ^ k) (𝓝[>] 1) (𝓝 1)<VAR>r' : ℝ<VAR>hr' : r' ^ k < r<VAR>h1 : 1 < r'<VAR>h0 : 0 ≤ r'<GOAL>(fun n => ↑n ^ k) =O[atTop] fun n => (r' ^ k) ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : 1 < r<VAR>this : Tendsto (fun x => x ^ k) (𝓝[>] 1) (𝓝 1)<VAR>r' : ℝ<VAR>hr' : r' ^ k < r<VAR>h1 : 1 < r'<VAR>h0 : 0 ≤ r'<GOAL>(fun n => ↑n ^ k) =O[atTop] fun n => (r' ^ n) ^ k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : 1 < r<VAR>this : Tendsto (fun x => x ^ k) (𝓝[>] 1) (𝓝 1)<VAR>r' : ℝ<VAR>hr' : r' ^ k < r<VAR>h1 : 1 < r'<VAR>h0 : 0 ≤ r'<GOAL>∀ (n : ℕ), ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖1‖ * ‖r' ^ n‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : 1 < r<VAR>this : Tendsto (fun x => x ^ k) (𝓝[>] 1) (𝓝 1)<VAR>r' : ℝ<VAR>hr' : r' ^ k < r<VAR>h1 : 1 < r'<VAR>h0 : 0 ≤ r'<VAR>n : ℕ<GOAL>‖↑n‖ ≤ (r' - 1)⁻¹ * ‖1‖ * ‖r' ^ n‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : 1 < r<VAR>this : Tendsto (fun x => x ^ k) (𝓝[>] 1) (𝓝 1)<VAR>r' : ℝ<VAR>hr' : r' ^ k < r<VAR>h1 : 1 < r'<VAR>h0 : 0 ≤ r'<VAR>n : ℕ<GOAL>‖↑n‖ ≤ (r' - 1)⁻¹ * ‖r' ^ n‖ * ‖1‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : 1 < r<VAR>this : Tendsto (fun x => x ^ k) (𝓝[>] 1) (𝓝 1)<VAR>r' : ℝ<VAR>hr' : r' ^ k < r<VAR>h1 : 1 < r'<VAR>h0 : 0 ≤ r'<VAR>n : ℕ<GOAL>↑n ≤ (r' - 1)⁻¹ * ‖r' ^ n‖
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : ∀ (i : ι), (S.map (eval C c i)).Exact<GOAL>S.Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : ∀ (i : ι), IsZero (S.map (eval C c i)).homology<GOAL>IsZero S.homology
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : ∀ (i : ι), IsZero (S.map (eval C c i)).homology<GOAL>𝟙 S.homology = 0
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : ∀ (i : ι), IsZero (S.map (eval C c i)).homology<VAR>i : ι<GOAL>(𝟙 S.homology).f i = Hom.f 0 i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → ℝ≥0<VAR>sf sg : ℝ≥0<VAR>i : α<VAR>h : ∀ (a : α), f a ≤ g a<VAR>hi : f i < g i<VAR>hf : HasSum f sf<VAR>hg : HasSum g sg<GOAL>sf < sg
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → ℝ≥0<VAR>sf sg : ℝ≥0<VAR>i : α<VAR>h : ∀ (a : α), f a ≤ g a<VAR>hi : f i < g i<VAR>hf : HasSum f sf<VAR>hg : HasSum g sg<VAR>A : ∀ (a : α), ↑(f a) ≤ ↑(g a)<GOAL>sf < sg
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → ℝ≥0<VAR>sf sg : ℝ≥0<VAR>i : α<VAR>h : ∀ (a : α), f a ≤ g a<VAR>hi : f i < g i<VAR>hf : HasSum f sf<VAR>hg : HasSum g sg<VAR>A : ∀ (a : α), ↑(f a) ≤ ↑(g a)<VAR>this : ↑sf < ↑sg<GOAL>sf < sg
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.39934, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.v₁₂.τ₂ ≫ S.v₂₃.τ₂ = 0