ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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'.negDblY P = (-W'.dblU P) ^ 3
<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 * (W'.dblU P ^ 2 - P x * (W'.negY P - W'.negY P) ^ 2) + W'.negY P * (W'.negY P - W'.negY P) ^ 3 = (-W'.dblU P) ^ 3
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℂ<GOAL>Tendsto (fun x => cexp (f x)) l (𝓝 0) ↔ Tendsto (fun x => (f x).re) l atBot
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℂ<GOAL>Tendsto (re ∘ f) l atBot ↔ Tendsto (fun x => (f x).re) l atBot
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R n<VAR>a : ℕ<VAR>x : ZMod a<GOAL>(ringEquivCongr ⋯) x = x
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R n<VAR>a : ℕ<VAR>x : ZMod a<GOAL>(RingEquiv.refl (ZMod a)) x = x
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<GOAL>(p.concat h).reverse = cons ⋯ p.reverse
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>h : ContinuousWithinAt f s x<GOAL>{y | writtenInExtChartAt I I'' x (g ∘ f) y = (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) y} ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>h : ContinuousWithinAt f s x<GOAL>f ∘ ↑(extChartAt I x).symm ⁻¹' (extChartAt I' (f x)).source ⊆ {y | writtenInExtChartAt I I'' x (g ∘ f) y = (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) y}
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V<GOAL>IsNoetherian K V ↔ Module.rank K V < ℵ₀
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V<GOAL>IsNoetherian K V ↔ (Basis.ofVectorSpaceIndex K V).Finite
<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 : α<GOAL>multiplicity a b ≠ ⊤ ↔ Finite a b
<VAR>α : Type u_1<VAR>inst✝³ : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝² : UniformSpace β<VAR>pkg' : AbstractCompletion β<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace γ<VAR>f : α → β → γ<VAR>inst✝ : CompleteSpace γ<GOAL>UniformContinuous₂ (pkg.extend₂ pkg' f)
<VAR>α : Type u_1<VAR>inst✝³ : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝² : UniformSpace β<VAR>pkg' : AbstractCompletion β<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace γ<VAR>f : α → β → γ<VAR>inst✝ : CompleteSpace γ<GOAL>UniformContinuous ((pkg.prod pkg').extend (uncurry f))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Field K<VAR>R₁ : Type u_4<VAR>inst✝⁶ : CommRing R₁<VAR>inst✝⁵ : IsDomain R₁<VAR>inst✝⁴ : Algebra R₁ K<VAR>inst✝³ : IsFractionRing R₁ K<VAR>I J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R₁ K'<VAR>inst✝ : IsFractionRing R₁ K'<VAR>x : R₁<VAR>hx : x ≠ 0<GOAL>↑(Ideal.span {x}) / ↑(Ideal.span {x}) = 1
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Surjective (preimage f) ↔ Injective f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>h : Surjective (preimage f)<VAR>x x' : α<VAR>hx : f x = f x'<GOAL>x = x'
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>h : Surjective (preimage f)<VAR>x x' : α<VAR>hx : f x = f x'<VAR>s : Set β<VAR>hs : f ⁻¹' s = {x}<GOAL>x = x'
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>h : Surjective (preimage f)<VAR>x x' : α<VAR>hx : f x = f x'<VAR>s : Set β<VAR>hs : f ⁻¹' s = {x}<VAR>this : x ∈ {x}<GOAL>x = x'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K K₁ K₂ : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 ↥K₂<VAR>h : K₁ ≤ K₂<GOAL>finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K K₁ K₂ : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 ↥K₂<VAR>h : K₁ ≤ K₂<VAR>this : FiniteDimensional 𝕜 ↥K₁<GOAL>finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K K₁ K₂ : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 ↥K₂<VAR>h : K₁ ≤ K₂<VAR>this✝ : FiniteDimensional 𝕜 ↥K₁<VAR>this : ProperSpace ↥K₁<GOAL>finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K K₁ K₂ : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 ↥K₂<VAR>h : K₁ ≤ K₂<VAR>this✝ : FiniteDimensional 𝕜 ↥K₁<VAR>this : ProperSpace ↥K₁<VAR>hd : finrank 𝕜 ↥(K₁ ⊔ K₁ᗮ ⊓ K₂) + finrank 𝕜 ↥(K₁ ⊓ (K₁ᗮ ⊓ K₂)) = finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂)<GOAL>finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K K₁ K₂ : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 ↥K₂<VAR>h : K₁ ≤ K₂<VAR>this✝ : FiniteDimensional 𝕜 ↥K₁<VAR>this : ProperSpace ↥K₁<VAR>hd : finrank 𝕜 ↥K₂ + 0 = finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂)<GOAL>finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K K₁ K₂ : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 ↥K₂<VAR>h : K₁ ≤ K₂<VAR>this✝ : FiniteDimensional 𝕜 ↥K₁<VAR>this : ProperSpace ↥K₁<VAR>hd : finrank 𝕜 ↥K₂ = finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂)<GOAL>finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>s t : Set α<VAR>a b : α<VAR>inst✝¹ : PartialOrder γ<VAR>inst✝ : OrderTop γ<GOAL>upperBounds univ = {⊤}
<VAR>a b : Cardinal.{u_1}<VAR>hb : ℵ₀ ≤ b<VAR>ha : a ≤ b<GOAL>a + b = b
<VAR>a✝ b✝ c p q : ℚ<VAR>a b : ℤ<VAR>hb : 0 < b<VAR>n : ℤ<VAR>d : ℕ<VAR>hd : d ≠ 0<VAR>hnd : n.natAbs.Coprime d<VAR>hab : a /. b = { num := n, den := d, den_nz := hd, reduced := hnd }<GOAL>0 ≤ { num := n, den := d, den_nz := hd, reduced := hnd } ↔ 0 ≤ a
<VAR>a✝ b✝ c p q : ℚ<VAR>a b : ℤ<VAR>hb : 0 < b<VAR>n : ℤ<VAR>d : ℕ<VAR>hd : d ≠ 0<VAR>hnd : n.natAbs.Coprime d<VAR>hab : a * ↑d = n * b<GOAL>0 ≤ { num := n, den := d, den_nz := hd, reduced := hnd } ↔ 0 ≤ a
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>a : F<VAR>ha : a ≠ 0<GOAL>(quadraticChar F) a ^ 2 = 1
<VAR>k : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : Fintype k<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq k<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Semiring α<VAR>a : m<VAR>b : n<VAR>c : k<VAR>M : Matrix k l α<GOAL>(single a b).toMatrix * ((single b c).toMatrix * M) = (single a c).toMatrix * M
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : E → E<VAR>t₀ : ℝ<VAR>x₀ : E<VAR>inst✝ : CompleteSpace E<VAR>hv : ContDiffAt ℝ 1 v x₀<GOAL>∃ f, f t₀ = x₀ ∧ ∃ ε > 0, ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (v (f t)) t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : E → E<VAR>t₀ : ℝ<VAR>x₀ : E<VAR>inst✝ : CompleteSpace E<VAR>hv : ContDiffAt ℝ 1 v x₀<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>w✝² : ℝ≥0<VAR>w✝¹ w✝ : ℝ<VAR>hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ w✝² w✝¹ w✝<GOAL>∃ f, f t₀ = x₀ ∧ ∃ ε > 0, ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (v (f t)) t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : E → E<VAR>t₀ : ℝ<VAR>x₀ : E<VAR>inst✝ : CompleteSpace E<VAR>hv : ContDiffAt ℝ 1 v x₀<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>w✝² : ℝ≥0<VAR>w✝¹ w✝ : ℝ<VAR>hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ w✝² w✝¹ w✝<VAR>f : ℝ → E<VAR>hf1 : f t₀ = x₀<VAR>hf2 : ∀ t ∈ Icc (t₀ - ε) (t₀ + ε), HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t<GOAL>∃ f, f t₀ = x₀ ∧ ∃ ε > 0, ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (v (f t)) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f✝ g✝ : (i : α) → δ i<VAR>inst✝ : (j : α) → Decidable (j ∈ s)<VAR>f f' g : α → β<VAR>t : Set α<GOAL>EqOn (s.piecewise f f') g t ↔ EqOn f g (t ∩ s) ∧ EqOn f' g (t ∩ sᶜ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f✝ g✝ : (i : α) → δ i<VAR>inst✝ : (j : α) → Decidable (j ∈ s)<VAR>f f' g : α → β<VAR>t : Set α<GOAL>(∀ ⦃x : α⦄, x ∈ t → s.piecewise f f' x = g x) ↔ ∀ (x : α), (x ∈ t ∩ s → f x = g x) ∧ (x ∈ t ∩ sᶜ → f' x = g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f✝ g✝ : (i : α) → δ i<VAR>inst✝ : (j : α) → Decidable (j ∈ s)<VAR>f f' g : α → β<VAR>t : Set α<VAR>a : α<GOAL>a ∈ t → s.piecewise f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : α → Set β<VAR>t : α → Set γ<VAR>inst✝ : Preorder α<VAR>x : α<GOAL>⋃ y, ⋃ (_ : y ≤ x), Accumulate s y = ⋃ y, ⋃ (_ : y ≤ x), s y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : α → Set β<VAR>t : α → Set γ<VAR>inst✝ : Preorder α<VAR>x : α<GOAL>⋃ y, ⋃ (_ : y ≤ x), Accumulate s y ⊆ ⋃ y, ⋃ (_ : y ≤ x), s y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : α → Set β<VAR>t : α → Set γ<VAR>inst✝ : Preorder α<VAR>x : α<GOAL>⋃ y, ⋃ (_ : y ≤ x), s y ⊆ ⋃ y, ⋃ (_ : y ≤ x), Accumulate s y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : DecidableRel H.Adj<VAR>inst✝ : DecidableEq α<VAR>tris : Finset (Finset α)<VAR>htris : tris ⊆ G.cliqueFinset 3<VAR>pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton<VAR>hHG : H ≤ G<VAR>hH : H.CliqueFree 3<GOAL>tris.card ≤ G.edgeFinset.card - H.edgeFinset.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : DecidableRel H.Adj<VAR>inst✝ : DecidableEq α<VAR>tris : Finset (Finset α)<VAR>htris : tris ⊆ G.cliqueFinset 3<VAR>pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton<VAR>hHG : H ≤ G<VAR>hH : H.CliqueFree 3<GOAL>tris.attach.card ≤ (G.edgeFinset \ H.edgeFinset).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : DecidableRel H.Adj<VAR>inst✝ : DecidableEq α<VAR>tris : Finset (Finset α)<VAR>htris : tris ⊆ G.cliqueFinset 3<VAR>pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton<VAR>hHG : H ≤ G<VAR>hH : H.CliqueFree 3<VAR>hG : (G.edgeFinset \ H.edgeFinset).card < tris.attach.card<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : DecidableRel H.Adj<VAR>inst✝ : DecidableEq α<VAR>tris : Finset (Finset α)<VAR>htris : tris ⊆ G.cliqueFinset 3<VAR>pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton<VAR>hHG : H ≤ G<VAR>hH : H.CliqueFree 3<VAR>hG : (G.edgeFinset \ H.edgeFinset).card < tris.attach.card<VAR>this : ∀ ⦃t : Finset α⦄, t ∈ tris → ∃ x y, x ∈ t ∧ y ∈ t ∧ x ≠ y ∧ s(x, y) ∈ G.edgeFinset \ H.edgeFinset<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : DecidableRel H.Adj<VAR>inst✝ : DecidableEq α<VAR>tris : Finset (Finset α)<VAR>htris : tris ⊆ G.cliqueFinset 3<VAR>pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton<VAR>hHG : H ≤ G<VAR>hH : H.CliqueFree 3<VAR>hG : (G.edgeFinset \ H.edgeFinset).card < tris.attach.card<VAR>fx fy : ⦃t : Finset α⦄ → t ∈ tris → α<VAR>hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t<VAR>hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t<VAR>hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht<VAR>fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : DecidableRel H.Adj<VAR>inst✝ : DecidableEq α<VAR>tris : Finset (Finset α)<VAR>htris : tris ⊆ G.cliqueFinset 3<VAR>pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton<VAR>hHG : H ≤ G<VAR>hH : H.CliqueFree 3<VAR>hG : (G.edgeFinset \ H.edgeFinset).card < tris.attach.card<VAR>fx fy : ⦃t : Finset α⦄ → t ∈ tris → α<VAR>hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t<VAR>hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t<VAR>hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht<VAR>fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset<VAR>f : { x // x ∈ tris } → Sym2 α := fun t => s(fx ⋯, fy ⋯)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : DecidableRel H.Adj<VAR>inst✝ : DecidableEq α<VAR>tris : Finset (Finset α)<VAR>htris : tris ⊆ G.cliqueFinset 3<VAR>pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton<VAR>hHG : H ≤ G<VAR>hH : H.CliqueFree 3<VAR>hG : (G.edgeFinset \ H.edgeFinset).card < tris.attach.card<VAR>fx fy : ⦃t : Finset α⦄ → t ∈ tris → α<VAR>hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t<VAR>hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t<VAR>hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht<VAR>fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset<VAR>f : { x // x ∈ tris } → Sym2 α := fun t => s(fx ⋯, fy ⋯)<VAR>hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : DecidableRel H.Adj<VAR>inst✝ : DecidableEq α<VAR>tris : Finset (Finset α)<VAR>htris : tris ⊆ G.cliqueFinset 3<VAR>pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton<VAR>hHG : H ≤ G<VAR>hH : H.CliqueFree 3<VAR>hG : (G.edgeFinset \ H.edgeFinset).card < tris.attach.card<VAR>fx fy : ⦃t : Finset α⦄ → t ∈ tris → α<VAR>hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t<VAR>hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t<VAR>hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht<VAR>fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset<VAR>f : { x // x ∈ tris } → Sym2 α := fun t => s(fx ⋯, fy ⋯)<VAR>hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset<VAR>t₁ : Finset α<VAR>ht₁ : t₁ ∈ tris<VAR>t₂ : Finset α<VAR>ht₂ : t₂ ∈ tris<VAR>tne : ⟨t₁, ht₁⟩ ≠ ⟨t₂, ht₂⟩<VAR>t : s(fx ⋯, fy ⋯) = s(fx ⋯, fy ⋯)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : DecidableRel H.Adj<VAR>inst✝ : DecidableEq α<VAR>tris : Finset (Finset α)<VAR>htris : tris ⊆ G.cliqueFinset 3<VAR>pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton<VAR>hHG : H ≤ G<VAR>hH : H.CliqueFree 3<VAR>hG : (G.edgeFinset \ H.edgeFinset).card < tris.attach.card<VAR>fx fy : ⦃t : Finset α⦄ → t ∈ tris → α<VAR>hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t<VAR>hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t<VAR>hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht<VAR>fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset<VAR>f : { x // x ∈ tris } → Sym2 α := fun t => s(fx ⋯, fy ⋯)<VAR>hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset<VAR>t₁ : Finset α<VAR>ht₁ : t₁ ∈ tris<VAR>t₂ : Finset α<VAR>ht₂ : t₂ ∈ tris<VAR>tne : ⟨t₁, ht₁⟩ ≠ ⟨t₂, ht₂⟩<VAR>t : s(fx ⋯, fy ⋯) = s(fx ⋯, fy ⋯)<VAR>i : (fun x y => (↑x ∩ ↑y).Subsingleton) t₁ t₂<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : DecidableRel H.Adj<VAR>inst✝ : DecidableEq α<VAR>tris : Finset (Finset α)<VAR>htris : tris ⊆ G.cliqueFinset 3<VAR>pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton<VAR>hHG : H ≤ G<VAR>hH : H.CliqueFree 3<VAR>hG : (G.edgeFinset \ H.edgeFinset).card < tris.attach.card<VAR>fx fy : ⦃t : Finset α⦄ → t ∈ tris → α<VAR>hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t<VAR>hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t<VAR>hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht<VAR>fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset<VAR>f : { x // x ∈ tris } → Sym2 α := fun t => s(fx ⋯, fy ⋯)<VAR>hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset<VAR>t₁ : Finset α<VAR>ht₁ : t₁ ∈ tris<VAR>t₂ : Finset α<VAR>ht₂ : t₂ ∈ tris<VAR>tne : ⟨t₁, ht₁⟩ ≠ ⟨t₂, ht₂⟩<VAR>t : fx ⋯ = fx ⋯ ∧ fy ⋯ = fy ⋯ ∨ fx ⋯ = fy ⋯ ∧ fy ⋯ = fx ⋯<VAR>i : (↑t₁ ∩ ↑t₂).Subsingleton<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>s : β → Set α<VAR>hm : ∀ (i : β), NullMeasurableSet (s i) μ<VAR>hd : Pairwise (AEDisjoint μ on s)<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α) in ⋃ i, s i, f a ∂μ = ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ
<VAR>P : AffineTargetMorphismProperty<VAR>inst✝² : P.IsLocal<VAR>X Y UX UY : Scheme<VAR>inst✝¹ : IsAffine UY<VAR>f : X ⟶ Y<VAR>iY : UY ⟶ Y<VAR>inst✝ : IsOpenImmersion iY<VAR>iX : UX ⟶ X<VAR>f' : UX ⟶ UY<VAR>h : IsPullback iX f' f iY<VAR>hf : targetAffineLocally P f<GOAL>P f'
<VAR>P : AffineTargetMorphismProperty<VAR>inst✝² : P.IsLocal<VAR>X Y UX UY : Scheme<VAR>inst✝¹ : IsAffine UY<VAR>f : X ⟶ Y<VAR>iY : UY ⟶ Y<VAR>inst✝ : IsOpenImmersion iY<VAR>iX : UX ⟶ X<VAR>f' : UX ⟶ UY<VAR>h : IsPullback iX f' f iY<VAR>hf : targetAffineLocally P f<GOAL>P (pullback.snd f iY)
<VAR>M₀ : Type u_1<VAR>inst✝⁵ : MonoidWithZero M₀<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M₁ : Type u_4<VAR>R : Type u_5<VAR>R' : Type u_6<VAR>F : Type u_7<VAR>inst✝⁴ : MonoidWithZero M<VAR>inst✝³ : MonoidWithZero M'<VAR>inst✝² : CommMonoidWithZero M₁<VAR>inst✝¹ : Ring R<VAR>inst✝ : CommRing R'<VAR>r x : M₁<VAR>hr : r ∈ M₁⁰<GOAL>r * x = 0 ↔ x = 0
<VAR>R : Type u<VAR>A : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing A<VAR>p : R[X]<VAR>x : R<VAR>P : Ideal R<VAR>hP : x ∈ P<VAR>n✝ : ℕ<VAR>i : n✝ < (p.scaleRoots x).natDegree<GOAL>(p.scaleRoots x).coeff n✝ ∈ P
<VAR>R : Type u<VAR>A : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing A<VAR>p : R[X]<VAR>x : R<VAR>P : Ideal R<VAR>hP : x ∈ P<VAR>n✝ : ℕ<VAR>i : n✝ < (p.scaleRoots x).natDegree<GOAL>p.coeff n✝ * x ^ (p.natDegree - n✝) ∈ P
<VAR>R : Type u<VAR>A : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing A<VAR>p : R[X]<VAR>x : R<VAR>P : Ideal R<VAR>hP : x ∈ P<VAR>n✝ : ℕ<VAR>i : 0 < p.natDegree - n✝<GOAL>p.coeff n✝ * x ^ (p.natDegree - n✝) ∈ P
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<GOAL>count p 1 = if p 0 then 1 else 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<GOAL>∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>ha_ne_zero : Ideal.span {a} ≠ 0<GOAL>∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) = 0