ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB : B.Nondegenerate<VAR>hB₀ : B.IsRefl<VAR>W : Submodule K V<GOAL>finrank K ↥(B.orthogonal W) = finrank K V - finrank K ↥W
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB : B.Nondegenerate<VAR>hB₀ : B.IsRefl<VAR>W : Submodule K V<VAR>this : finrank K ↥W + finrank K ↥(B.orthogonal W) = finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤)<GOAL>finrank K ↥(B.orthogonal W) = finrank K V - finrank K ↥W
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB : B.Nondegenerate<VAR>hB₀ : B.IsRefl<VAR>W : Submodule K V<VAR>this : finrank K ↥W + finrank K ↥(B.orthogonal W) = finrank K V<GOAL>finrank K ↥(B.orthogonal W) = finrank K V - finrank K ↥W
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB : B.Nondegenerate<VAR>hB₀ : B.IsRefl<VAR>W : Submodule K V<VAR>this✝ : finrank K ↥W + finrank K ↥(B.orthogonal W) = finrank K V<VAR>this : finrank K ↥W ≤ finrank K V<GOAL>finrank K ↥(B.orthogonal W) = finrank K V - finrank K ↥W
<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 α<VAR>t : α → Set β<GOAL>⋃ x ∈ ⋃ i, s i, t x = ⋃ i, ⋃ x ∈ s i, t x
<VAR>Γ₀ : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>h : Nontrivial Γ₀ˣ<VAR>f : Γ₀ →*₀ ℝ≥0<VAR>hf : StrictMono ⇑f<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>∃ d, ↑(f ↑d) < r
<VAR>Γ₀ : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>h : Nontrivial Γ₀ˣ<VAR>f : Γ₀ →*₀ ℝ≥0<VAR>hf : StrictMono ⇑f<VAR>r : ℝ<VAR>hr : 0 < r<VAR>s : ℝ≥0 := ⟨r, ⋯⟩<GOAL>∃ d, ↑(f ↑d) < r
<VAR>Γ₀ : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>h : Nontrivial Γ₀ˣ<VAR>f : Γ₀ →*₀ ℝ≥0<VAR>hf : StrictMono ⇑f<VAR>r : ℝ<VAR>hr : 0 < r<VAR>s : ℝ≥0 := ⟨r, ⋯⟩<VAR>hs : 0 < s<GOAL>∃ d, ↑(f ↑d) < r
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : DivisionRing k<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module k V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : Fintype ι<VAR>p : ι → P<VAR>hi : AffineIndependent k p<VAR>sp : AffineSubspace k P<VAR>inst✝ : FiniteDimensional k ↥sp.direction<VAR>hle : affineSpan k (Set.range p) ≤ sp<VAR>hc : Fintype.card ι = finrank k ↥sp.direction + 1<GOAL>affineSpan k (Set.range p) = sp
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).b₈ = φ W.b₈
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<GOAL>φ W.a₁ ^ 2 * φ W.a₆ + 4 * φ W.a₂ * φ W.a₆ - φ W.a₁ * φ W.a₃ * φ W.a₄ + φ W.a₂ * φ W.a₃ ^ 2 - φ W.a₄ ^ 2 = φ (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2)
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : AddCommMonoid M<VAR>s : Finset (ι →₀ M)<GOAL>(s.sum id).support ⊆ s.sup Finsupp.support
<VAR>α : Type u_1<VAR>m n : Num<GOAL>n.cmp m = Ordering.lt ↔ m.cmp n = Ordering.gt
<VAR>α : Type u_1<VAR>m n : Num<GOAL>(m.cmp n).swap = Ordering.lt ↔ m.cmp n = Ordering.gt
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3<GOAL>W'.dblX P = W'.dblU P ^ 2
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3<GOAL>W'.dblU P ^ 2 - W'.a₁ * W'.dblU P * P z * (W'.negY P - W'.negY P) - W'.a₂ * P z ^ 2 * (W'.negY P - W'.negY P) ^ 2 - 2 * P x * (W'.negY P - W'.negY P) ^ 2 = W'.dblU P ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>hs : Convex 𝕜 s<VAR>z : E<GOAL>Convex 𝕜 (z +ᵥ s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>hs : Convex 𝕜 s<VAR>z : E<GOAL>Convex 𝕜 ({z} + s)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>β : Type u_4<VAR>u : ι ⊕ β → ↑S.X₂<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range (⇑S.g ∘ u ∘ Sum.inr))<VAR>m : ↑S.X₂<VAR>a✝ : m ∈ ⊤<GOAL>m ∈ span R (range u)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>β : Type u_4<VAR>u : ι ⊕ β → ↑S.X₂<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range (⇑S.g ∘ u ∘ Sum.inr))<VAR>m : ↑S.X₂<VAR>a✝ : m ∈ ⊤<VAR>hgm : S.g m ∈ span R (range (⇑S.g ∘ u ∘ Sum.inr))<GOAL>m ∈ span R (range u)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>β : Type u_4<VAR>u : ι ⊕ β → ↑S.X₂<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range (⇑S.g ∘ u ∘ Sum.inr))<VAR>m : ↑S.X₂<VAR>a✝ : m ∈ ⊤<VAR>hgm : ∃ c, (c.sum fun i a => a • (⇑S.g ∘ u ∘ Sum.inr) i) = S.g m<GOAL>m ∈ span R (range u)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>β : Type u_4<VAR>u : ι ⊕ β → ↑S.X₂<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range (⇑S.g ∘ u ∘ Sum.inr))<VAR>m : ↑S.X₂<VAR>a✝ : m ∈ ⊤<VAR>cm : β →₀ R<VAR>hm : (cm.sum fun i a => a • (⇑S.g ∘ u ∘ Sum.inr) i) = S.g m<VAR>m' : ↑S.X₂ := cm.sum fun j a => a • u (Sum.inr j)<GOAL>m ∈ span R (range u)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>β : Type u_4<VAR>u : ι ⊕ β → ↑S.X₂<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range (⇑S.g ∘ u ∘ Sum.inr))<VAR>m : ↑S.X₂<VAR>a✝ : m ∈ ⊤<VAR>cm : β →₀ R<VAR>hm : (cm.sum fun i a => a • (⇑S.g ∘ u ∘ Sum.inr) i) = S.g m<VAR>m' : ↑S.X₂ := cm.sum fun j a => a • u (Sum.inr j)<VAR>hsub : m - m' ∈ LinearMap.range S.f<GOAL>m ∈ span R (range u)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>β : Type u_4<VAR>u : ι ⊕ β → ↑S.X₂<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range (⇑S.g ∘ u ∘ Sum.inr))<VAR>m : ↑S.X₂<VAR>a✝ : m ∈ ⊤<VAR>cm : β →₀ R<VAR>hm : (cm.sum fun i a => a • (⇑S.g ∘ u ∘ Sum.inr) i) = S.g m<VAR>m' : ↑S.X₂ := cm.sum fun j a => a • u (Sum.inr j)<VAR>n : ↑S.X₁<VAR>hnm : S.f n = m - m'<GOAL>m ∈ span R (range u)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>β : Type u_4<VAR>u : ι ⊕ β → ↑S.X₂<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range (⇑S.g ∘ u ∘ Sum.inr))<VAR>m : ↑S.X₂<VAR>a✝ : m ∈ ⊤<VAR>cm : β →₀ R<VAR>hm : (cm.sum fun i a => a • (⇑S.g ∘ u ∘ Sum.inr) i) = S.g m<VAR>m' : ↑S.X₂ := cm.sum fun j a => a • u (Sum.inr j)<VAR>n : ↑S.X₁<VAR>hnm : S.f n = m - m'<VAR>hn : n ∈ span R (range v)<GOAL>m ∈ span R (range u)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>β : Type u_4<VAR>u : ι ⊕ β → ↑S.X₂<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range (⇑S.g ∘ u ∘ Sum.inr))<VAR>m : ↑S.X₂<VAR>a✝ : m ∈ ⊤<VAR>cm : β →₀ R<VAR>hm : (cm.sum fun i a => a • (⇑S.g ∘ u ∘ Sum.inr) i) = S.g m<VAR>m' : ↑S.X₂ := cm.sum fun j a => a • u (Sum.inr j)<VAR>n : ↑S.X₁<VAR>hnm : S.f n = m - m'<VAR>hn : ∃ c, (c.sum fun i a => a • v i) = n<GOAL>m ∈ span R (range u)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>β : Type u_4<VAR>u : ι ⊕ β → ↑S.X₂<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range (⇑S.g ∘ u ∘ Sum.inr))<VAR>m : ↑S.X₂<VAR>a✝ : m ∈ ⊤<VAR>cm : β →₀ R<VAR>hm : (cm.sum fun i a => a • (⇑S.g ∘ u ∘ Sum.inr) i) = S.g m<VAR>m' : ↑S.X₂ := cm.sum fun j a => a • u (Sum.inr j)<VAR>n : ↑S.X₁<VAR>hnm : S.f n = m - m'<VAR>cn : ι →₀ R<VAR>hn : (cn.sum fun i a => a • v i) = n<GOAL>m ∈ span R (range u)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>β : Type u_4<VAR>u : ι ⊕ β → ↑S.X₂<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range (⇑S.g ∘ u ∘ Sum.inr))<VAR>m : ↑S.X₂<VAR>a✝ : m ∈ ⊤<VAR>cm : β →₀ R<VAR>hm : (cm.sum fun i a => a • (⇑S.g ∘ u ∘ Sum.inr) i) = S.g m<VAR>m' : ↑S.X₂ := cm.sum fun j a => a • u (Sum.inr j)<VAR>n : ↑S.X₁<VAR>cn : ι →₀ R<VAR>hnm : (cn.sum fun a b => S.f (b • v a)) = m - m'<VAR>hn : (cn.sum fun i a => a • v i) = n<GOAL>m ∈ span R (range u)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>β : Type u_4<VAR>u : ι ⊕ β → ↑S.X₂<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range (⇑S.g ∘ u ∘ Sum.inr))<VAR>m : ↑S.X₂<VAR>a✝ : m ∈ ⊤<VAR>cm : β →₀ R<VAR>hm : (cm.sum fun i a => a • (⇑S.g ∘ u ∘ Sum.inr) i) = S.g m<VAR>m' : ↑S.X₂ := cm.sum fun j a => a • u (Sum.inr j)<VAR>n : ↑S.X₁<VAR>cn : ι →₀ R<VAR>hnm : (cn.sum fun a b => S.f (b • v a)) = m - m'<VAR>hn : (cn.sum fun i a => a • v i) = n<GOAL>(cn.sum fun a b => S.f (b • v a)) + m' ∈ span R (range u)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>β : Type u_4<VAR>u : ι ⊕ β → ↑S.X₂<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range (⇑S.g ∘ u ∘ Sum.inr))<VAR>m : ↑S.X₂<VAR>a✝ : m ∈ ⊤<VAR>cm : β →₀ R<VAR>hm : (cm.sum fun i a => a • (⇑S.g ∘ u ∘ Sum.inr) i) = S.g m<VAR>m' : ↑S.X₂ := cm.sum fun j a => a • u (Sum.inr j)<VAR>n : ↑S.X₁<VAR>cn : ι →₀ R<VAR>hnm : (cn.sum fun a b => S.f (b • v a)) = m - m'<VAR>hn : (cn.sum fun i a => a • v i) = n<GOAL>(cn.sum fun a b => b • S.f (v a)) + m' ∈ span R (range u)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>β : Type u_4<VAR>u : ι ⊕ β → ↑S.X₂<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range (⇑S.g ∘ u ∘ Sum.inr))<VAR>m : ↑S.X₂<VAR>a✝ : m ∈ ⊤<VAR>cm : β →₀ R<VAR>hm : (cm.sum fun i a => a • (⇑S.g ∘ u ∘ Sum.inr) i) = S.g m<VAR>m' : ↑S.X₂ := cm.sum fun j a => a • u (Sum.inr j)<VAR>n : ↑S.X₁<VAR>cn : ι →₀ R<VAR>hnm : (cn.sum fun a b => S.f (b • v a)) = m - m'<VAR>hn : (cn.sum fun i a => a • v i) = n<VAR>hn' : (cn.sum fun a b => b • S.f (v a)) = cn.sum fun a b => b • u (Sum.inl a)<GOAL>(cn.sum fun a b => b • S.f (v a)) + m' ∈ span R (range u)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>β : Type u_4<VAR>u : ι ⊕ β → ↑S.X₂<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range (⇑S.g ∘ u ∘ Sum.inr))<VAR>m : ↑S.X₂<VAR>a✝ : m ∈ ⊤<VAR>cm : β →₀ R<VAR>hm : (cm.sum fun i a => a • (⇑S.g ∘ u ∘ Sum.inr) i) = S.g m<VAR>m' : ↑S.X₂ := cm.sum fun j a => a • u (Sum.inr j)<VAR>n : ↑S.X₁<VAR>cn : ι →₀ R<VAR>hnm : (cn.sum fun a b => S.f (b • v a)) = m - m'<VAR>hn : (cn.sum fun i a => a • v i) = n<VAR>hn' : (cn.sum fun a b => b • S.f (v a)) = cn.sum fun a b => b • u (Sum.inl a)<GOAL>(cn.sum fun a b => b • u (Sum.inl a)) + m' ∈ span R (range u)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>β : Type u_4<VAR>u : ι ⊕ β → ↑S.X₂<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range (⇑S.g ∘ u ∘ Sum.inr))<VAR>m : ↑S.X₂<VAR>a✝ : m ∈ ⊤<VAR>cm : β →₀ R<VAR>hm : (cm.sum fun i a => a • (⇑S.g ∘ u ∘ Sum.inr) i) = S.g m<VAR>m' : ↑S.X₂ := cm.sum fun j a => a • u (Sum.inr j)<VAR>n : ↑S.X₁<VAR>cn : ι →₀ R<VAR>hnm : (cn.sum fun a b => S.f (b • v a)) = m - m'<VAR>hn : (cn.sum fun i a => a • v i) = n<VAR>hn' : (cn.sum fun a b => b • S.f (v a)) = cn.sum fun a b => b • u (Sum.inl a)<GOAL>(cn.sum fun a b => b • u (Sum.inl a)) ∈ span R (range u)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>β : Type u_4<VAR>u : ι ⊕ β → ↑S.X₂<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range (⇑S.g ∘ u ∘ Sum.inr))<VAR>m : ↑S.X₂<VAR>a✝ : m ∈ ⊤<VAR>cm : β →₀ R<VAR>hm : (cm.sum fun i a => a • (⇑S.g ∘ u ∘ Sum.inr) i) = S.g m<VAR>m' : ↑S.X₂ := cm.sum fun j a => a • u (Sum.inr j)<VAR>n : ↑S.X₁<VAR>cn : ι →₀ R<VAR>hnm : (cn.sum fun a b => S.f (b • v a)) = m - m'<VAR>hn : (cn.sum fun i a => a • v i) = n<VAR>hn' : (cn.sum fun a b => b • S.f (v a)) = cn.sum fun a b => b • u (Sum.inl a)<GOAL>m' ∈ span R (range u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>C : α<VAR>hf : Tendsto f l (𝓝 C)<VAR>hg : Tendsto g l atTop<VAR>a✝ : Nontrivial α<GOAL>Tendsto (fun x => f x + g x) l atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>C : α<VAR>hf : Tendsto f l (𝓝 C)<VAR>hg : Tendsto g l atTop<VAR>a✝ : Nontrivial α<VAR>C' : α<VAR>hC' : C' < C<GOAL>Tendsto (fun x => f x + g x) l atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>C : α<VAR>hf : Tendsto f l (𝓝 C)<VAR>hg : Tendsto g l atTop<VAR>a✝ : Nontrivial α<VAR>C' : α<VAR>hC' : C' < C<GOAL>∀ᶠ (x : β) in l, C' ≤ f x
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>y : α<VAR>inst✝ : BEq α<GOAL>indexesOf y (x :: xs) = bif x == y then 0 :: map (fun x => x + 1) (indexesOf y xs) else map (fun x => x + 1) (indexesOf y xs)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>inst✝ : BorelSpace γ<VAR>p : ℝ≥0∞<VAR>h : IdentDistrib f g μ ν<VAR>hf : Memℒp f p μ<GOAL>Memℒp g p ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>inst✝ : BorelSpace γ<VAR>p : ℝ≥0∞<VAR>h : IdentDistrib f g μ ν<VAR>hf : Memℒp f p μ<GOAL>eLpNorm g p ν < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>inst✝ : BorelSpace γ<VAR>p : ℝ≥0∞<VAR>h : IdentDistrib f g μ ν<VAR>hf : Memℒp f p μ<GOAL>eLpNorm 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>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>c : G<VAR>p : ℝ≥0∞<GOAL>eLpNorm (s.indicator fun x => c) p μ ≤ ↑‖c‖₊ * μ s ^ (1 / p.toReal)
<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>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>c : G<GOAL>eLpNorm (s.indicator fun x => c) 0 μ ≤ ↑‖c‖₊ * μ s ^ (1 / ENNReal.toReal 0)
<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>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>c : G<VAR>p : ℝ≥0∞<VAR>hp : p ≠ 0<GOAL>eLpNorm (s.indicator fun x => c) p μ ≤ ↑‖c‖₊ * μ s ^ (1 / p.toReal)
<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>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>c : G<VAR>hp : ⊤ ≠ 0<GOAL>eLpNorm (s.indicator fun x => c) ⊤ μ ≤ ↑‖c‖₊ * μ s ^ (1 / ⊤.toReal)
<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>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>c : G<VAR>p : ℝ≥0∞<VAR>hp : p ≠ 0<VAR>h'p : p ≠ ⊤<GOAL>eLpNorm (s.indicator fun x => c) p μ ≤ ↑‖c‖₊ * μ s ^ (1 / p.toReal)
<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>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>c : G<VAR>p : ℝ≥0∞<VAR>hp : p ≠ 0<VAR>h'p : p ≠ ⊤<VAR>t : Set α := toMeasurable μ s<GOAL>eLpNorm (s.indicator fun x => c) p μ ≤ ↑‖c‖₊ * μ s ^ (1 / p.toReal)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : CommRing k<VAR>inst✝ : CharP k p<VAR>n : ℕ<GOAL>∃ f, ∀ (x y : 𝕎 k), f (truncateFun (n + 1) x) (truncateFun (n + 1) y) = (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : CommRing k<VAR>inst✝ : CharP k p<VAR>n : ℕ<GOAL>∃ f, ∀ (x y : 𝕎 k), f (truncateFun (n + 1) x) (truncateFun (n + 1) y) = peval (polyOfInterest p n) ![fun i => x.coeff i, fun i => y.coeff i]
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : CommRing k<VAR>inst✝ : CharP k p<VAR>n : ℕ<VAR>f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k<VAR>hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)<GOAL>∃ f, ∀ (x y : 𝕎 k), f (truncateFun (n + 1) x) (truncateFun (n + 1) y) = peval (polyOfInterest p n) ![fun i => x.coeff i, fun i => y.coeff i]
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : CommRing k<VAR>inst✝ : CharP k p<VAR>n : ℕ<VAR>f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k<VAR>hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)<VAR>this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b<GOAL>∃ f, ∀ (x y : 𝕎 k), f (truncateFun (n + 1) x) (truncateFun (n + 1) y) = peval (polyOfInterest p n) ![fun i => x.coeff i, fun i => y.coeff i]
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : CommRing k<VAR>inst✝ : CharP k p<VAR>n : ℕ<VAR>f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k<VAR>hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)<VAR>this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b<VAR>f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k := fun x y => f₀ fun a => Subtype.casesOn a fun a ha => Function.uncurry ![x, y] (a.1, ⟨a.2, ⋯⟩)<GOAL>∃ f, ∀ (x y : 𝕎 k), f (truncateFun (n + 1) x) (truncateFun (n + 1) y) = peval (polyOfInterest p n) ![fun i => x.coeff i, fun i => y.coeff i]
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : CommRing k<VAR>inst✝ : CharP k p<VAR>n : ℕ<VAR>f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k<VAR>hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)<VAR>this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b<VAR>f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k := fun x y => f₀ fun a => Subtype.casesOn a fun a ha => Function.uncurry ![x, y] (a.1, ⟨a.2, ⋯⟩)<GOAL>∀ (x y : 𝕎 k), f (truncateFun (n + 1) x) (truncateFun (n + 1) y) = peval (polyOfInterest p n) ![fun i => x.coeff i, fun i => y.coeff i]
<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>p : R[X]<VAR>x : S<VAR>h : p ≠ 0<GOAL>(normalizeScaleRoots p).coeff (normalizeScaleRoots p).natDegree = 1
<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>p : R[X]<VAR>x : S<VAR>h : p ≠ 0<GOAL>(normalizeScaleRoots p).coeff p.natDegree = 1