ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : AddCommMonoid B<VAR>inst✝³ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0✝ : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g✝ : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H✝ : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero M'<VAR>inst✝ : CommMonoid N<VAR>f : M → M'<VAR>hf : f 0 = 0<VAR>g : α →₀ M<VAR>h : α → M' → N<VAR>h0 : ∀ (a : α), h a 0 = 1<VAR>x✝¹ : α<VAR>x✝ : x✝¹ ∈ g.support<VAR>H : x✝¹ ∉ (mapRange f hf g).support<GOAL>h x✝¹ ((mapRange f hf g) x✝¹) = 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>a b x : α<GOAL>↑(sign x) * x = |x|
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t✝ : Set V<VAR>x y z : V<VAR>t : Finset V<VAR>hs : LinearIndependent K fun (x : ↑s) => ↑x<VAR>hst : s ⊆ ↑(span K ↑t)<GOAL>∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<GOAL>volume (fundamentalDomain (fractionalIdealLatticeBasis K I)) = ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * volume (fundamentalDomain (latticeBasis K))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>e : Module.Free.ChooseBasisIndex ℤ ↥↑↑I ≃ Module.Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯<GOAL>volume (fundamentalDomain (fractionalIdealLatticeBasis K I)) = ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * volume (fundamentalDomain (latticeBasis K))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>e : Module.Free.ChooseBasisIndex ℤ ↥↑↑I ≃ Module.Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯<GOAL>ENNReal.ofReal |?b₀.det ⇑((fractionalIdealLatticeBasis K I).reindex e)| * volume (fundamentalDomain ?b₀) = ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * volume (fundamentalDomain (latticeBasis K))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>e : Module.Free.ChooseBasisIndex ℤ ↥↑↑I ≃ Module.Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯<GOAL>Basis (Module.Free.ChooseBasisIndex ℤ (𝓞 K)) ℝ (({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ))
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Zero M<VAR>a : α<VAR>m : M<GOAL>(singleton a m).lookupFinsupp = Finsupp.single a m
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f✝ : β → α<VAR>t : Finset γ<VAR>h : (s ×ˢ t).Nonempty<VAR>f : β × γ → α<VAR>a : α<GOAL>(s ×ˢ t).sup' h f ≤ a ↔ (s.sup' ⋯ fun i => t.sup' ⋯ fun i' => f (i, i')) ≤ a
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ right b<GOAL>Finset.card (moveRight b m) / 2 < Finset.card b / 2
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝³ : CommRing R₂<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R₂ M₂<VAR>e : Basis ι R M<VAR>v : ι' → M<VAR>i✝ : ι<VAR>j✝ : ι'<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<GOAL>(e.repr (e j)) i = 1 i j
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x✝ : Z<VAR>x : B × F<GOAL>x ∈ e.target ↔ x.1 ∈ e.baseSet
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hf : AEMeasurable f ν<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤<GOAL>(ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hf : AEMeasurable f ν<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤<GOAL>(ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hf : AEMeasurable f ν<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤<VAR>hν_ac : ν ≪ ν.withDensity f<GOAL>(ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hf : AEMeasurable f ν<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤<VAR>hν_ac : ν ≪ ν.withDensity f<GOAL>(ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae (ν.withDensity f)] (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hf : AEMeasurable f ν<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤<VAR>hν_ac : ν ≪ ν.withDensity f<VAR>this : SigmaFinite (ν.withDensity f)<GOAL>(ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae (ν.withDensity f)] (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hf : AEMeasurable f ν<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤<VAR>hν_ac : ν ≪ ν.withDensity f<VAR>this : SigmaFinite (ν.withDensity f)<GOAL>μ.singularPart ν ⟂ₘ ν.withDensity f
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<GOAL>volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) < r} = ENNReal.ofReal r ^ (2 * card ι) * ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<VAR>h₂ : ∀ (x : ι → ℂ), 0 ≤ (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p)<GOAL>volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) < r} = ENNReal.ofReal r ^ (2 * card ι) * ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<VAR>h₂ : ∀ (x : ι → ℂ), 0 ≤ (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p)<VAR>hr : r ≤ 0<GOAL>volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) < r} = ENNReal.ofReal r ^ (2 * card ι) * ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<VAR>h₂ : ∀ (x : ι → ℂ), 0 ≤ (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p)<VAR>hr : 0 < r<GOAL>volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) < r} = ENNReal.ofReal r ^ (2 * card ι) * ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>M : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : TopologicalSpace M<VAR>v : VectorMeasure α M<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>j : Set α<VAR>hj : MeasurableSet j<VAR>hij : j ⊆ i<GOAL>↑(v.restrict i) j = ↑v j
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a✝ b✝ c d a b : α<GOAL>min a b = a ∨ min a b = b
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v w : V<VAR>e : Sym2 V<VAR>H✝ : SimpleGraph V<VAR>s s₁ s₂ : Set (Sym2 V)<VAR>H : SimpleGraph V<VAR>h : H ≤ G<GOAL>G.deleteEdges (G.edgeSet \ H.edgeSet) = H
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>b : K<VAR>nth_partDen_eq : (of v).partDens.get? n = some b<GOAL>b * ((of v).contsAux (n + 1)).b ≤ ((of v).contsAux (n + 2)).b
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>gp_n : Pair K<VAR>nth_s_eq : (of v).s.get? n = some gp_n<VAR>nth_partDen_eq : (of v).partDens.get? n = some gp_n.b<GOAL>gp_n.b * ((of v).contsAux (n + 1)).b ≤ ((of v).contsAux (n + 2)).b
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : Inhabited α<VAR>l : List α<VAR>h : l ≠ []<GOAL>l.head! ∈ l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : Inhabited α<VAR>l : List α<VAR>h : l ≠ []<VAR>h' : l.head! ∈ l.head! :: l.tail<GOAL>l.head! ∈ l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>i j : ℕ<VAR>h : i ≠ j<VAR>a : α<VAR>hj : j < (l.set i a).length<GOAL>(l.set i a)[j] = l[j]
<VAR>q r : ℕ+<VAR>hqr : q ≤ r<VAR>H : 1 < sumInv {2, q, r}<VAR>h4 : 0 < 4<GOAL>q < 4
<VAR>q r : ℕ+<VAR>hqr : q ≤ r<VAR>h4 : 0 < 4<VAR>H : 4 ≤ q<GOAL>sumInv {2, q, r} ≤ 1
<VAR>q r : ℕ+<VAR>hqr : q ≤ r<VAR>h4 : 0 < 4<VAR>H : 4 ≤ q<GOAL>(↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
<VAR>q r : ℕ+<VAR>hqr : q ≤ r<VAR>h4 : 0 < 4<VAR>H : 4 ≤ q<VAR>h4r : 4 ≤ r<VAR>hq : (↑↑q)⁻¹ ≤ 4⁻¹<VAR>hr : (↑↑r)⁻¹ ≤ 4⁻¹<GOAL>(↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
<VAR>x : ℝ≥0<VAR>hx : x ≠ 0<GOAL>x⁻¹ < 1 ↔ 1 < x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>h : 0 < multiplicity a b<GOAL>a ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>h : 0 < multiplicity a b<GOAL>a ^ 1 ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>h : 0 < multiplicity a b<GOAL>↑1 ≤ multiplicity a b
<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>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<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✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<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>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → E'<VAR>g₁ g₂ : α → F'<VAR>h₁ : IsBigOWith c₁ l f₁ g<VAR>h₂ : f₂ =o[l] g<VAR>hc : c₁ < c₂<GOAL>IsBigOWith c₂ l (fun x => f₁ x - f₂ x) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : (α → ℕ) → ℤ<GOAL>IsPoly f → IsPoly (-f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : (α → ℕ) → ℤ<GOAL>IsPoly f → IsPoly (0 - f)
<VAR>xl xr : Type u<VAR>y z : PGame<VAR>h : y ⧏ z<VAR>x : PGame<GOAL>x + y ⧏ x + z
<VAR>xl xr : Type u<VAR>y z : PGame<VAR>h : y ⧏ z<VAR>x : PGame<GOAL>y + x ⧏ z + x
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>ha : G.Adj s t<GOAL>(G.replaceVertex s t).edgeFinset.card = G.edgeFinset.card + G.degree s - G.degree t - 1
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>ha : G.Adj s t<VAR>inc : G.incidenceFinset t ⊆ G.edgeFinset<GOAL>(G.replaceVertex s t).edgeFinset.card = G.edgeFinset.card + G.degree s - G.degree t - 1
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>ha : G.Adj s t<VAR>inc : G.incidenceFinset t ⊆ G.edgeFinset<GOAL>G.edgeFinset.card + (image (fun x => s(x, t)) (G.neighborFinset s)).card - G.degree t - {s(t, t)}.card = G.edgeFinset.card + G.degree s - G.degree t - 1
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>ha : G.Adj s t<VAR>inc : G.incidenceFinset t ⊆ G.edgeFinset<GOAL>G.edgeFinset.card + (image (fun x => s(x, t)) (G.neighborFinset s)).card = G.edgeFinset.card + G.degree s
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>ha : G.Adj s t<VAR>inc : G.incidenceFinset t ⊆ G.edgeFinset<GOAL>Function.Injective fun x => s(x, t)
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I✝ : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<VAR>f : Module.End R M<VAR>I : Ideal R<VAR>hI : LinearMap.range f ≤ I • ⊤<GOAL>∃ M_1, (toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I✝ : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<VAR>f : Module.End R M<VAR>I : Ideal R<VAR>hI : LinearMap.range f ≤ I • ⊤<VAR>this : ∀ (x : M), f x ∈ LinearMap.range (Ideal.finsuppTotal ι M I b)<GOAL>∃ M_1, (toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I✝ : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<VAR>f : Module.End R M<VAR>I : Ideal R<VAR>hI : LinearMap.range f ≤ I • ⊤<VAR>bM' : M → ι →₀ ↥I<VAR>hbM' : ∀ (x : M), (Ideal.finsuppTotal ι M I b) (bM' x) = f x<VAR>A : Matrix ι ι R := fun i j => ↑((bM' (b j)) i)<GOAL>∃ M_1, (toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I✝ : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<VAR>f : Module.End R M<VAR>I : Ideal R<VAR>hI : LinearMap.range f ≤ I • ⊤<VAR>bM' : M → ι →₀ ↥I<VAR>hbM' : ∀ (x : M), (Ideal.finsuppTotal ι M I b) (bM' x) = f x<VAR>A : Matrix ι ι R := fun i j => ↑((bM' (b j)) i)<VAR>this : Represents b A f<GOAL>∃ M_1, (toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>inst✝ : IsDedekindDomain S<VAR>i : ℕ<VAR>a d d' e e' : S<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>e_mem : e ∈ P ^ (i + 1)<VAR>e'_mem : e' ∈ P ^ (i + 1)<VAR>h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)<GOAL>d - d' ∈ P
<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>inst✝ : IsDedekindDomain S<VAR>i : ℕ<VAR>a d d' e e' : S<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>e_mem : e ∈ P ^ (i + 1)<VAR>e'_mem : e' ∈ P ^ (i + 1)<VAR>h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)<VAR>h' : a * (d - d') ∈ P ^ (i + 1)<GOAL>d - d' ∈ P
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>n : ℕ<VAR>c d : 𝕜<GOAL>Tendsto (fun x => c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>c d : 𝕜<GOAL>Tendsto (fun x => c * x ^ 0) atTop (𝓝 d) ↔ (c = 0 ∨ 0 = 0) ∧ c = d
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>n : ℕ<VAR>c d : 𝕜<VAR>hn : n ≠ 0<GOAL>Tendsto (fun x => c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>n : ℕ<VAR>c d : 𝕜<VAR>hn : n ≠ 0<VAR>hc : c < 0<GOAL>Tendsto (fun x => c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>n : ℕ<VAR>d : 𝕜<VAR>hn : n ≠ 0<GOAL>Tendsto (fun x => 0 * x ^ n) atTop (𝓝 d) ↔ (0 = 0 ∨ n = 0) ∧ 0 = d
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>n : ℕ<VAR>c d : 𝕜<VAR>hn : n ≠ 0<VAR>hc : 0 < c<GOAL>Tendsto (fun x => c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ ≃ τ<VAR>p : MvPolynomial σ R<GOAL>(rename ⇑f.symm) ((rename ⇑f) p) = p
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ ≃ τ<VAR>p : MvPolynomial τ R<GOAL>(rename ⇑f) ((rename ⇑f.symm) p) = p
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hs : Convex R s<GOAL>(∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hs : Convex R s<GOAL>(∀ i ∈ ∅, 0 ≤ w i) → 0 < ∑ i ∈ ∅, w i → (∀ i ∈ ∅, z i ∈ s) → ∅.centerMass w z ∈ s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i✝ j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hs : Convex R s<VAR>i : ι<VAR>t : Finset ι<VAR>hi : i ∉ t<VAR>ht : (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s<GOAL>(∀ i_1 ∈ insert i t, 0 ≤ w i_1) → 0 < ∑ i ∈ insert i t, w i → (∀ i_1 ∈ insert i t, z i_1 ∈ s) → (insert i t).centerMass w z ∈ s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i✝ j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hs : Convex R s<VAR>i : ι<VAR>t : Finset ι<VAR>hi : i ∉ t<VAR>ht : (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s<VAR>h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1<VAR>hpos : 0 < ∑ i ∈ insert i t, w i<VAR>hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s<GOAL>(insert i t).centerMass w z ∈ s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i✝ j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hs : Convex R s<VAR>i : ι<VAR>t : Finset ι<VAR>hi : i ∉ t<VAR>ht : (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s<VAR>h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1<VAR>hpos : 0 < ∑ i ∈ insert i t, w i<VAR>hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s<VAR>zi : z i ∈ s<GOAL>(insert i t).centerMass w z ∈ s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i✝ j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hs : Convex R s<VAR>i : ι<VAR>t : Finset ι<VAR>hi : i ∉ t<VAR>ht : (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s<VAR>h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1<VAR>hpos : 0 < ∑ i ∈ insert i t, w i<VAR>hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s<VAR>zi : z i ∈ s<VAR>hs₀ : ∀ j ∈ t, 0 ≤ w j<GOAL>(insert i t).centerMass w z ∈ s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i✝ j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hs : Convex R s<VAR>i : ι<VAR>t : Finset ι<VAR>hi : i ∉ t<VAR>ht : (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s<VAR>h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1<VAR>hpos : 0 < w i + ∑ x ∈ t, w x<VAR>hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s<VAR>zi : z i ∈ s<VAR>hs₀ : ∀ j ∈ t, 0 ≤ w j<GOAL>(insert i t).centerMass w z ∈ s
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P✝ Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>P : Cᵒᵖ ⥤ Type v₁<GOAL>(∀ (x : FamilyOfElements P S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t) ↔ ∀ (f : S.functor ⟶ P), ∃! g, S.functorInclusion ≫ g = f