ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝ : Nontrivial R<VAR>M' : Submodule R M<VAR>this✝ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>x✝¹ : { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>s : Set (M ⧸ M')<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>x✝ : { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>t : Set ↥M'<VAR>ht : LinearIndependent (ι := { x // x ∈ t }) R Subtype.val<GOAL>#↑↑⟨s, hs⟩ + #↑↑⟨t, ht⟩ ≤ Module.rank R M
<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✝ : Nontrivial R<VAR>M' : Submodule R M<VAR>this✝ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>x✝¹ : { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>s : Set (M ⧸ M')<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>x✝ : { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>t : Set ↥M'<VAR>ht : LinearIndependent (ι := { x // x ∈ t }) R Subtype.val<VAR>f : M ⧸ M' → M<VAR>hf : ∀ (b : M ⧸ M'), Submodule.Quotient.mk (f b) = b<GOAL>#↑↑⟨s, hs⟩ + #↑↑⟨t, ht⟩ ≤ Module.rank R M
<VAR>F✝ : Type u_1<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Z' : Type x<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>f₀✝ f₁✝ f₂ : C(X, Y)<VAR>S : Set X<VAR>f₀ f₁ g₀ g₁ : C(X, Y)<VAR>F : f₀.HomotopyRel f₁ S<VAR>h₀ : f₀ = g₀<VAR>h₁ : f₁ = g₁<VAR>t : ↑I<VAR>x : X<VAR>hx : x ∈ S<GOAL>{ toFun := fun x => (F.cast h₀ h₁).toFun (t, x), continuous_toFun := ⋯ } x = g₀ x
<VAR>α : Type u_1<VAR>l l₁ l₂ : List α<VAR>p : α → Prop<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<VAR>h : xs ⊆ ys<GOAL>xs ∪ ys = ys
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν ν₁ ν₂ μ : Measure α<VAR>inst✝² : SigmaFinite ν₁<VAR>inst✝¹ : SigmaFinite ν₂<VAR>inst✝ : SigmaFinite μ<GOAL>(ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν ν₁ ν₂ μ : Measure α<VAR>inst✝² : SigmaFinite ν₁<VAR>inst✝¹ : SigmaFinite ν₂<VAR>inst✝ : SigmaFinite μ<GOAL>μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν ν₁ ν₂ μ : Measure α<VAR>inst✝² : SigmaFinite ν₁<VAR>inst✝¹ : SigmaFinite ν₂<VAR>inst✝ : SigmaFinite μ<GOAL>AEMeasurable ((ν₁ + ν₂).rnDeriv μ) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν ν₁ ν₂ μ : Measure α<VAR>inst✝² : SigmaFinite ν₁<VAR>inst✝¹ : SigmaFinite ν₂<VAR>inst✝ : SigmaFinite μ<GOAL>AEMeasurable (ν₁.rnDeriv μ + ν₂.rnDeriv μ) μ
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>r : ℝ<GOAL>(fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) =O[𝓝[>] 0] fun x => x ^ r
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>r : ℝ<VAR>this : ((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) =O[𝓝[>] 0] ((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹)<GOAL>(fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) =O[𝓝[>] 0] fun x => x ^ r
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>r : ℝ<VAR>this : ∃ c, ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ c * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖<GOAL>∃ c, ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ c * ‖x ^ r‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>r C : ℝ<VAR>hC : ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖<GOAL>∃ c, ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ c * ‖x ^ r‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>r C : ℝ<VAR>hC : ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖<GOAL>∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>r C : ℝ<VAR>hC : ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖<VAR>x : ℝ<VAR>hC' : x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖<VAR>hx : 0 < x<GOAL>‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>r C : ℝ<VAR>hC : ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖<VAR>x : ℝ<VAR>hC' : x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖<VAR>hx : 0 < x<VAR>h_nv2 : ↑(x ^ P.k) ≠ 0<GOAL>‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>r C : ℝ<VAR>hC : ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖<VAR>x : ℝ<VAR>hC' : x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖<VAR>hx : 0 < x<VAR>h_nv2 : ↑(x ^ P.k) ≠ 0<VAR>h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0<GOAL>‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>r C : ℝ<VAR>hC : ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖<VAR>x : ℝ<VAR>hx : 0 < x<VAR>h_nv2 : ↑(x ^ P.k) ≠ 0<VAR>h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0<VAR>hC' : ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖<GOAL>‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>r C : ℝ<VAR>hC : ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖<VAR>x : ℝ<VAR>hx : 0 < x<VAR>h_nv2 : ↑(x ^ P.k) ≠ 0<VAR>h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0<VAR>hC' : ‖(P.ε⁻¹ * ↑(x ^ P.k)) • P.f x - P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖<GOAL>‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>r C : ℝ<VAR>hC : ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖<VAR>x : ℝ<VAR>hx : 0 < x<VAR>h_nv2 : ↑(x ^ P.k) ≠ 0<VAR>h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0<VAR>hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖<GOAL>‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<GOAL>∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in b..c, f x ∂μ = ∫ (x : ℝ) in a..c, f x ∂μ
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>h : IsUnramified k w<GOAL>Stab w = ⊥
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>h : IsUnramified k w<GOAL>∀ ⦃x : K ≃ₐ[k] K⦄, x ∈ Stab (mk w.embedding) → x ∈ ⊥
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>h : IsUnramified k w<GOAL>∀ (a : K ≃ₐ[k] K), ComplexEmbedding.IsConj w.embedding a → a = 1
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>(↑n).toZNumNeg = -↑n
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<VAR>n : ℕ<VAR>hn : hf.toFinset.card ≤ n<GOAL>nth p n = 0
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<VAR>n : ℕ<VAR>hn : hf.toFinset.card ≤ n<GOAL>(sort (fun x x_1 => x ≤ x_1) hf.toFinset).length ≤ n
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t✝ : Set Ω<VAR>hms : MeasurableSet s<VAR>t : Set Ω<GOAL>μ[|s] (s ∩ t) = μ[|s] t
<VAR>α : Type u_1<VAR>m n : Num<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>α : Type u_1<VAR>m n : Num<GOAL>¬↑n < ↑m ↔ m ≤ n
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>m v : E<VAR>h : v ∈ span ℤ (Set.range ⇑b)<GOAL>fract b (v + m) = fract b m
<VAR>α : Type u_1<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ a b c : α<GOAL>mabs ((a ⊔ c) / (b ⊔ c)) ≤ mabs (a / b)
<VAR>α : Type u_1<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ a b c : α<GOAL>mabs ((a ⊔ c) / (b ⊔ c)) * mabs ?m.25410 ≤ mabs (a / b)
<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>f : α → β → γ<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set β<GOAL>image2 f (⋂ i, ⋂ j, s i j) t ⊆ ⋂ i, ⋂ j, image2 f (s i j) 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>f : α → β → γ<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set β<GOAL>∀ (x : α), (∀ (i : ι) (i_1 : κ i), x ∈ s i i_1) → ∀ y ∈ t, ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f (s i i_1) t
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n✝ m n : ℤ<VAR>z₁ : Cochain F G n<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>(z₁.comp (ofHom (𝟙 G)) ⋯).v p q hpq = z₁.v p q hpq
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<VAR>ht : IsUpperSet t<GOAL>IsUpperSet (s * t)
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<VAR>ht : IsUpperSet t<GOAL>IsUpperSet (⋃ a ∈ s, a • t)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>t' 𝒰 f g i j k ≫ pullback.fst (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map k) ≫ pullback.fst (𝒰.map j ≫ f) g = pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>ha : ¬a = 0<GOAL>p / (C a * q) = C a⁻¹ * (p / q)
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>ha : ¬a = 0<GOAL>C a⁻¹ * (C q.leadingCoeff⁻¹ * (p /ₘ (C a * (q * (C a⁻¹ * C q.leadingCoeff⁻¹))))) = C a⁻¹ * (C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹)))
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>ha : ¬a = 0<GOAL>C a * (q * (C a⁻¹ * C q.leadingCoeff⁻¹)) = q * C q.leadingCoeff⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)<VAR>hs : (s ∩ mulSupport f).Finite<VAR>ht : (t ∩ mulSupport f).Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
<VAR>I : MulticospanIndex (Type u)<VAR>c : Multifork I<VAR>hc : IsLimit c<VAR>s : I.sections<VAR>i : I.L<GOAL>c.ι i ((sectionsEquiv hc) s) = s.val i
<VAR>I : MulticospanIndex (Type u)<VAR>c : Multifork I<VAR>hc : IsLimit c<VAR>i : I.L<VAR>x : c.pt<GOAL>c.ι i ((sectionsEquiv hc) ((sectionsEquiv hc).symm x)) = ((sectionsEquiv hc).symm x).val i
<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 z : P<VAR>hyz : s.WOppSide y z<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)<GOAL>s.WOppSide x z
<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 z : P<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hyz : ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ z)<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)<GOAL>s.WOppSide x z
<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 z : P<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)<VAR>p₃ : P<VAR>hp₃ : p₃ ∈ s<VAR>hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)<GOAL>s.WOppSide x z
<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 z : P<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)<VAR>p₃ : P<VAR>hp₃ : p₃ ∈ s<VAR>hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)<GOAL>y -ᵥ p₂ = 0 → x -ᵥ p₁ = 0 ∨ p₃ -ᵥ z = 0
<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 z : P<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)<VAR>p₃ : P<VAR>hp₃ : p₃ ∈ s<VAR>hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)<VAR>h : y -ᵥ p₂ = 0<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 z : P<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)<VAR>p₃ : P<VAR>hp₃ : p₃ ∈ s<VAR>hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)<VAR>h : y = p₂<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr : Ordnode α<VAR>hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂<VAR>H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1<VAR>H2 : delta * l.size < (Ordnode.node rs rl rx rr).size<VAR>H3 : 2 * (Ordnode.node rs rl rx rr).size ≤ 9 * l.size + 5 ∨ (Ordnode.node rs rl rx rr).size ≤ 3<GOAL>Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr : Ordnode α<VAR>hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂<VAR>H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1<VAR>H2 : delta * l.size ≤ rl.size + rr.size<VAR>H3 : 2 * (Ordnode.node rs rl rx rr).size ≤ 9 * l.size + 5 ∨ (Ordnode.node rs rl rx rr).size ≤ 3<GOAL>Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr : Ordnode α<VAR>hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂<VAR>H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1<VAR>H2 : delta * l.size ≤ rl.size + rr.size<VAR>H3 : 2 * (rl.size + rr.size + 1) ≤ 9 * l.size + 5 ∨ rl.size + rr.size + 1 ≤ 3<GOAL>Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr : Ordnode α<VAR>hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂<VAR>H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1<VAR>H2 : delta * l.size ≤ rl.size + rr.size<VAR>H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2<GOAL>Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr : Ordnode α<VAR>hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂<VAR>H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1<VAR>H2 : delta * l.size ≤ rl.size + rr.size<VAR>H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2<VAR>H3_0 : l.size = 0 → rl.size + rr.size ≤ 2<GOAL>Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr : Ordnode α<VAR>hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂<VAR>H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1<VAR>H2 : delta * l.size ≤ rl.size + rr.size<VAR>H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2<VAR>H3_0 : l.size = 0 → rl.size + rr.size ≤ 2<VAR>H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3<GOAL>Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr : Ordnode α<VAR>hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂<VAR>H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1<VAR>H2 : delta * l.size ≤ rl.size + rr.size<VAR>H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2<VAR>H3_0 : l.size = 0 → rl.size + rr.size ≤ 2<VAR>H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3<VAR>ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1<GOAL>Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr : Ordnode α<VAR>hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂<VAR>H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1<VAR>H2 : delta * l.size ≤ rl.size + rr.size<VAR>H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2<VAR>H3_0 : l.size = 0 → rl.size + rr.size ≤ 2<VAR>H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3<VAR>ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1<VAR>hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1<GOAL>Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr : Ordnode α<VAR>hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂<VAR>H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1<VAR>H2 : delta * l.size ≤ rl.size + rr.size<VAR>H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2<VAR>H3_0 : l.size = 0 → rl.size + rr.size ≤ 2<VAR>H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3<VAR>ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1<VAR>hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1<GOAL>Valid' o₁ (if rl.size < ratio * rr.size then l.node3L x rl rx rr else l.node4L x rl rx rr) o₂
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : Fintype V<VAR>inst✝³ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Field R<VAR>inst✝ : CharZero R<VAR>x : V → R<GOAL>(((toLinearMap₂' R) (lapMatrix R G)) x) x = (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : Fintype V<VAR>inst✝³ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Field R<VAR>inst✝ : CharZero R<VAR>x : V → R<GOAL>(∑ x_1 : V, ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) = (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : Fintype V<VAR>inst✝³ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Field R<VAR>inst✝ : CharZero R<VAR>x : V → R<GOAL>((∑ x_1 : V, ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) + ∑ x_1 : V, ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) / 2 = (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : Fintype V<VAR>inst✝³ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Field R<VAR>inst✝ : CharZero R<VAR>x : V → R<GOAL>((∑ x_1 : V, ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) + ∑ i : V, ∑ j : V, if G.Adj j i then x i * x i - x i * x j else 0) / 2 = (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2