ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>inst✝¹⁰ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝⁹ : (i : ι) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ≥0<VAR>hp : (↑(finrank ℝ E)).IsConjExponent p<VAR>h0p : 0 < ↑p<GOAL>∫⁻ (x : E), ↑‖u x‖₊ ^ ↑p ∂μ ≤ ↑(lintegralPowLePowLIntegralFDerivConst μ ↑p) * (∫⁻ (x : E), ↑‖fderiv ℝ u x‖₊ ∂μ) ^ ↑p
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m₁✝ m₂✝ : M × R<VAR>m₁ : M<VAR>r₁ : R<VAR>m₂ : M<VAR>r₂ : R<GOAL>↑((toEven Q) ((ofEven Q) (((even.ι (Q' Q)).bilin (m₁, r₁)) (m₂, r₂)))) = (e0 Q * (v Q) m₁ + (algebraMap R (CliffordAlgebra (Q' Q))) r₁) * (e0 Q * (v Q) m₂ - (algebraMap R (CliffordAlgebra (Q' Q))) r₂)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m₁✝ m₂✝ : M × R<VAR>m₁ : M<VAR>r₁ : R<VAR>m₂ : M<VAR>r₂ : R<GOAL>(e0 Q * (v Q) m₁ + (algebraMap R (CliffordAlgebra (Q' Q))) r₁) * (e0 Q * (v Q) m₂ - (algebraMap R (CliffordAlgebra (Q' Q))) r₂) = e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + r₁ • e0 Q * (v Q) m₂ - r₂ • e0 Q * (v Q) m₁ - (algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m₁✝ m₂✝ : M × R<VAR>m₁ : M<VAR>r₁ : R<VAR>m₂ : M<VAR>r₂ : R<GOAL>e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + r₁ • e0 Q * (v Q) m₂ - r₂ • e0 Q * (v Q) m₁ - (algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂) = (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + (v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m₁✝ m₂✝ : M × R<VAR>m₁ : M<VAR>r₁ : R<VAR>m₂ : M<VAR>r₂ : R<VAR>h1 : e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) = (v Q) m₁ * (v Q) m₂<GOAL>e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + r₁ • e0 Q * (v Q) m₂ - r₂ • e0 Q * (v Q) m₁ - (algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂) = (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + (v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m₁✝ m₂✝ : M × R<VAR>m₁ : M<VAR>r₁ : R<VAR>m₂ : M<VAR>r₂ : R<VAR>h1 : e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) = (v Q) m₁ * (v Q) m₂<VAR>h2 : -(r₂ • e0 Q * (v Q) m₁) = (v Q) m₁ * r₂ • e0 Q<GOAL>e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + r₁ • e0 Q * (v Q) m₂ - r₂ • e0 Q * (v Q) m₁ - (algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂) = (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + (v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m₁✝ m₂✝ : M × R<VAR>m₁ : M<VAR>r₁ : R<VAR>m₂ : M<VAR>r₂ : R<VAR>h1 : e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) = (v Q) m₁ * (v Q) m₂<VAR>h2 : -(r₂ • e0 Q * (v Q) m₁) = (v Q) m₁ * r₂ • e0 Q<VAR>h3 : -(algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂) = r₁ • e0 Q * r₂ • e0 Q<GOAL>e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + r₁ • e0 Q * (v Q) m₂ - r₂ • e0 Q * (v Q) m₁ - (algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂) = (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + (v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m₁✝ m₂✝ : M × R<VAR>m₁ : M<VAR>r₁ : R<VAR>m₂ : M<VAR>r₂ : R<GOAL>(v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + (v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q = (ι (Q' Q)) (m₁, r₁) * (ι (Q' Q)) (m₂, r₂)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f'✝ : α → β → γ<VAR>g✝ g'✝ : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>g : γ → δ<VAR>f' : β → α' → δ<VAR>g' : α → α'<VAR>h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)<GOAL>image2 f' ((fun b => b) '' t) (g' '' s) = image2 f' t (g' '' s)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>a x y : 𝕜<VAR>ha : a ∈ s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxa : x ≠ a<VAR>hya : y ≠ a<VAR>hxy : x < y<GOAL>(f y - f a) / (y - a) < (f x - f a) / (x - a)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>a x y : 𝕜<VAR>ha : a ∈ s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxa : x ≠ a<VAR>hya : y ≠ a<VAR>hxy : x < y<VAR>key : ((-f) x - (-f) a) / (x - a) < ((-f) y - (-f) a) / (y - a)<GOAL>(f y - f a) / (y - a) < (f x - f a) / (x - a)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>a x y : 𝕜<VAR>ha : a ∈ s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxa : x ≠ a<VAR>hya : y ≠ a<VAR>hxy : x < y<VAR>key : (-f x - -f a) / (x - a) < (-f y - -f a) / (y - a)<GOAL>(f y - f a) / (y - a) < (f x - f a) / (x - a)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>a x y : 𝕜<VAR>ha : a ∈ s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxa : x ≠ a<VAR>hya : y ≠ a<VAR>hxy : x < y<VAR>key : (-f x - -f a) / (x - a) < (-f y - -f a) / (y - a)<GOAL>-((f x - f a) / (x - a)) < -((f y - f a) / (y - a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>F✝ : ℕ → α → β<VAR>f✝ : α → β<VAR>bound✝ : α → ℝ<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>bound_hasFiniteIntegral : HasFiniteIntegral bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))<GOAL>HasFiniteIntegral f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>F✝ : ℕ → α → β<VAR>f✝ : α → β<VAR>bound✝ : α → ℝ<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>bound_hasFiniteIntegral : HasFiniteIntegral bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))<GOAL>∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ⊤
<VAR>α : Type u_1<VAR>l : List α<VAR>x : Multiset α × Multiset α<VAR>h : x ∈ (powersetAux' l).revzip<GOAL>x.1 + x.2 = ↑l
<VAR>α : Type u_1<VAR>l : List α<VAR>x : Multiset α × Multiset α<VAR>h : ∃ a ∈ l.sublists'.revzip, Prod.map ofList ofList a = x<GOAL>x.1 + x.2 = ↑l
<VAR>α : Type u_1<VAR>l : List α<VAR>x : Multiset α × Multiset α<VAR>h : ∃ a b, (a, b) ∈ l.sublists'.revzip ∧ (↑a, ↑b) = x<GOAL>x.1 + x.2 = ↑l
<VAR>α : Type u_1<VAR>l l₁ l₂ : List α<VAR>h : (l₁, l₂) ∈ l.sublists'.revzip<GOAL>(↑l₁, ↑l₂).1 + (↑l₁, ↑l₂).2 = ↑l
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<VAR>hs : Splits i f<VAR>hf0 : (map i f).natDegree ≠ 0<VAR>x : L<VAR>hx : eval₂ i x f = 0<VAR>h : (map i f).roots = 0<GOAL>False
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<VAR>hs : Splits i f<VAR>hf0 : (map i f).natDegree ≠ 0<VAR>x : L<VAR>hx : eval x (map i f) = 0<VAR>h : (map i f).roots = 0<GOAL>False
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<VAR>hs : Splits i f<VAR>hf0 : (map i f).natDegree ≠ 0<VAR>x : L<VAR>hx : eval x (map i f) = 0<VAR>h : (map i f).roots = 0<VAR>this : map i f ≠ 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<VAR>a b : α<VAR>h : a ∈ s<GOAL>(b ::ₘ s).erase a = b ::ₘ s.erase a
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<VAR>a : α<VAR>h : a ∈ s<GOAL>(a ::ₘ s).erase a = a ::ₘ s.erase a
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<VAR>a b : α<VAR>h : a ∈ s<VAR>hab : a ≠ b<GOAL>(b ::ₘ s).erase a = b ::ₘ s.erase a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p✝ : G.Walk a b<VAR>p : G.Walk a a<VAR>hp : p.IsHamiltonianCycle<VAR>h : a ≠ b<GOAL>List.count b p.support = 1
<VAR>p q : ℚ<VAR>hp : 0 ≤ p<GOAL>(p / q).toNNRat = p.toNNRat / q.toNNRat
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b✝ : α<VAR>s : Set α<VAR>b c : α<VAR>H₁ : (Iio c).Nonempty<VAR>H₂ : b ≤ c<GOAL>b ∈ closure (Iio c)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝¹⁰ : LinearOrder ι<VAR>μ : Measure Ω<VAR>ℱ : Filtration ι m<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : CompleteSpace E<VAR>f : Ω → E<VAR>inst✝⁶ : atTop.IsCountablyGenerated<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : OrderTopology ι<VAR>inst✝³ : MeasurableSpace ι<VAR>inst✝² : SecondCountableTopology ι<VAR>inst✝¹ : BorelSpace ι<VAR>hτ : IsStoppingTime ℱ τ<VAR>hσ : IsStoppingTime ℱ σ<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>this : SigmaFinite (μ.trim ⋯)<GOAL>μ[f|⋯.measurableSpace] =ᶠ[ae (μ.restrict {x | τ x ≤ σ x})] μ[f|hτ.measurableSpace]
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝¹⁰ : LinearOrder ι<VAR>μ : Measure Ω<VAR>ℱ : Filtration ι m<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : CompleteSpace E<VAR>f : Ω → E<VAR>inst✝⁶ : atTop.IsCountablyGenerated<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : OrderTopology ι<VAR>inst✝³ : MeasurableSpace ι<VAR>inst✝² : SecondCountableTopology ι<VAR>inst✝¹ : BorelSpace ι<VAR>hτ : IsStoppingTime ℱ τ<VAR>hσ : IsStoppingTime ℱ σ<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>this : SigmaFinite (μ.trim ⋯)<VAR>t : Set Ω<GOAL>MeasurableSet ({ω | τ ω ≤ σ ω} ∩ t) ↔ MeasurableSet ({ω | τ ω ≤ σ ω} ∩ t)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝¹⁰ : LinearOrder ι<VAR>μ : Measure Ω<VAR>ℱ : Filtration ι m<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : CompleteSpace E<VAR>f : Ω → E<VAR>inst✝⁶ : atTop.IsCountablyGenerated<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : OrderTopology ι<VAR>inst✝³ : MeasurableSpace ι<VAR>inst✝² : SecondCountableTopology ι<VAR>inst✝¹ : BorelSpace ι<VAR>hτ : IsStoppingTime ℱ τ<VAR>hσ : IsStoppingTime ℱ σ<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>this : SigmaFinite (μ.trim ⋯)<VAR>t : Set Ω<GOAL>IsStoppingTime ℱ σ
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>h : p %ₘ q = 0<GOAL>q ∣ p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>h : p %ₘ q = 0<GOAL>q ∣ q * (p /ₘ q)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>h : q ∣ p<VAR>a✝ : Nontrivial R<GOAL>p %ₘ q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>h : q ∣ p<VAR>a✝ : Nontrivial R<VAR>r : R[X]<VAR>hr : p = q * r<GOAL>p %ₘ q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>h : q ∣ p<VAR>a✝ : Nontrivial R<VAR>r : R[X]<VAR>hr : p = q * r<VAR>hpq0 : ¬p %ₘ q = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>h : q ∣ p<VAR>a✝ : Nontrivial R<VAR>r : R[X]<VAR>hr : p = q * r<VAR>hpq0 : ¬p %ₘ q = 0<VAR>hmod : p %ₘ q = q * (r - p /ₘ q)<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>h : q ∣ p<VAR>a✝ : Nontrivial R<VAR>r : R[X]<VAR>hr : p = q * r<VAR>hpq0 : ¬p %ₘ q = 0<VAR>hmod : p %ₘ q = q * (r - p /ₘ q)<VAR>this : (q * (r - p /ₘ q)).degree < q.degree<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>h : q ∣ p<VAR>a✝ : Nontrivial R<VAR>r : R[X]<VAR>hr : p = q * r<VAR>hpq0 : ¬p %ₘ q = 0<VAR>hmod : p %ₘ q = q * (r - p /ₘ q)<VAR>this : (q * (r - p /ₘ q)).degree < q.degree<VAR>hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>h : q ∣ p<VAR>a✝ : Nontrivial R<VAR>r : R[X]<VAR>hr : p = q * r<VAR>hpq0 : ¬p %ₘ q = 0<VAR>hmod : p %ₘ q = q * (r - p /ₘ q)<VAR>this : (q * (r - p /ₘ q)).degree < q.degree<VAR>hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0<VAR>hlc : q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>h : q ∣ p<VAR>a✝ : Nontrivial R<VAR>r : R[X]<VAR>hr : p = q * r<VAR>hpq0 : ¬p %ₘ q = 0<VAR>hmod : p %ₘ q = q * (r - p /ₘ q)<VAR>this : ↑q.natDegree + ↑(r - p /ₘ q).natDegree < ↑q.natDegree<VAR>hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0<VAR>hlc : q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0<GOAL>False
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>s : Set α<VAR>p : α →₀ M<VAR>this : DecidablePred fun x => x ∈ s<GOAL>p ∈ supported M R s ↔ ∀ x ∉ s, p x = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t s : Set M<GOAL>(span R s).toAddSubmonoid = closure (univ • s)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t s : Set M<GOAL>univ • s ⊆ ↑(span R s).toAddSubmonoid
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t s : Set M<VAR>x : M<VAR>hx : x ∈ (span R s).toAddSubmonoid<VAR>r : R<VAR>m : M<VAR>hm : m ∈ closure (univ • s)<GOAL>∀ x ∈ univ • s, r • x ∈ closure (univ • s)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t s : Set M<VAR>x : M<VAR>hx : x ∈ (span R s).toAddSubmonoid<VAR>r : R<VAR>m : M<VAR>hm : m ∈ closure (univ • s)<GOAL>r • 0 ∈ closure (univ • s)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝² : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t s : Set M<VAR>x : M<VAR>hx : x ∈ (span R s).toAddSubmonoid<VAR>r : R<VAR>m : M<VAR>hm : m ∈ closure (univ • s)<VAR>x✝¹ x✝ : M<VAR>h : r • x✝¹ ∈ closure (univ • s)<VAR>h' : r • x✝ ∈ closure (univ • s)<GOAL>r • (x✝¹ + x✝) ∈ closure (univ • s)
<VAR>F : Type u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵇ ℝ<VAR>x : α<GOAL>(fun f => f.toFun) 0 x ≤ (fun f => f.toFun) (f + const α ‖f‖) x
<VAR>F : Type u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵇ ℝ<VAR>x : α<GOAL>0 ≤ f x + ‖f‖
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : DivisionRing α<VAR>inst✝ : CharZero α<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>d₁0 : d₁ ≠ 0<VAR>c₁ : n₁.natAbs.Coprime d₁<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>d₂0 : d₂ ≠ 0<VAR>c₂ : n₂.natAbs.Coprime d₂<VAR>h : ↑{ num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } = ↑{ num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }<GOAL>{ num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } = { num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : DivisionRing α<VAR>inst✝ : CharZero α<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>d₁0 : d₁ ≠ 0<VAR>c₁ : n₁.natAbs.Coprime d₁<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>d₂0 : d₂ ≠ 0<VAR>c₂ : n₂.natAbs.Coprime d₂<VAR>h : ↑{ num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } = ↑{ num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }<VAR>d₁a : ↑d₁ ≠ 0<GOAL>{ num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } = { num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : DivisionRing α<VAR>inst✝ : CharZero α<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>d₁0 : d₁ ≠ 0<VAR>c₁ : n₁.natAbs.Coprime d₁<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>d₂0 : d₂ ≠ 0<VAR>c₂ : n₂.natAbs.Coprime d₂<VAR>h : ↑{ num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } = ↑{ num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }<VAR>d₁a : ↑d₁ ≠ 0<VAR>d₂a : ↑d₂ ≠ 0<GOAL>{ num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } = { num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : DivisionRing α<VAR>inst✝ : CharZero α<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>d₁0 : d₁ ≠ 0<VAR>c₁ : n₁.natAbs.Coprime d₁<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>d₂0 : d₂ ≠ 0<VAR>c₂ : n₂.natAbs.Coprime d₂<VAR>h : ↑(n₁ /. ↑d₁) = ↑(n₂ /. ↑d₂)<VAR>d₁a : ↑d₁ ≠ 0<VAR>d₂a : ↑d₂ ≠ 0<GOAL>n₁ /. ↑d₁ = n₂ /. ↑d₂
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : DivisionRing α<VAR>inst✝ : CharZero α<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>d₁0 : d₁ ≠ 0<VAR>c₁ : n₁.natAbs.Coprime d₁<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>d₂0 : d₂ ≠ 0<VAR>c₂ : n₂.natAbs.Coprime d₂<VAR>d₁a : ↑d₁ ≠ 0<VAR>d₂a : ↑d₂ ≠ 0<VAR>h : ↑n₁ / ↑d₁ = ↑n₂ / ↑d₂<GOAL>mkRat n₁ d₁ = mkRat n₂ d₂
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeInf α<VAR>a b c d : α<GOAL>a ⊓ b ≤ a ∧ a ≤ a ⊓ b ↔ a ≤ b
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : Zero α<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq l<VAR>d : m → α<VAR>e : l → m<VAR>he : Function.Injective e<VAR>i j : l<GOAL>(diagonal d).submatrix e e i j = diagonal (d ∘ e) i j
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : Zero α<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq l<VAR>d : m → α<VAR>e : l → m<VAR>he : Function.Injective e<VAR>i j : l<GOAL>diagonal d (e i) (e j) = diagonal (d ∘ e) i j
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p✝ q p : R[X]<VAR>a : R<VAR>hp : p ≠ 0<GOAL>eval a (p /ₘ (X - C a) ^ rootMultiplicity a p) ≠ 0
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<GOAL>Function.Injective supp
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<GOAL>∀ (v w : ↑Kᶜ), supp ((induce Kᶜ G).connectedComponentMk v) = supp ((induce Kᶜ G).connectedComponentMk w) → (induce Kᶜ G).connectedComponentMk v = (induce Kᶜ G).connectedComponentMk w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>v : V<VAR>hv : v ∈ Kᶜ<VAR>w : V<VAR>hw : w ∈ Kᶜ<VAR>h : supp ((induce Kᶜ G).connectedComponentMk ⟨v, hv⟩) = supp ((induce Kᶜ G).connectedComponentMk ⟨w, hw⟩)<GOAL>(induce Kᶜ G).connectedComponentMk ⟨v, hv⟩ = (induce Kᶜ G).connectedComponentMk ⟨w, hw⟩
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>v : V<VAR>hv : v ∈ Kᶜ<VAR>w : V<VAR>hw : w ∈ Kᶜ<VAR>h : ∀ (x : V), (∃ (h : x ∉ K), (induce Kᶜ G).Reachable ⟨x, ⋯⟩ ⟨v, hv⟩) ↔ ∃ (h : x ∉ K), (induce Kᶜ G).Reachable ⟨x, ⋯⟩ ⟨w, hw⟩<GOAL>(induce Kᶜ G).Reachable ⟨v, hv⟩ ⟨w, hw⟩
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝³ : CommRing A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : Nontrivial B<GOAL>(minpoly A x).degree = 1 ↔ x ∈ (algebraMap A B).range
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝³ : CommRing A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : Nontrivial B<GOAL>x ∈ (algebraMap A B).range → (minpoly A x).degree = 1
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝³ : CommRing A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : Nontrivial B<VAR>x : A<GOAL>(minpoly A ((algebraMap A B) x)).degree = 1
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝³ : CommRing A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : Nontrivial B<VAR>x : A<VAR>this : Nontrivial A<GOAL>(minpoly A ((algebraMap A B) x)).degree = 1
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>v : V<VAR>inst✝ : Fintype ↑(G.neighborSet v)<GOAL>0 < G.degree v ↔ ∃ w, G.Adj v w
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>hn : n ≠ 0<GOAL>primitiveCharacter 1 = 1
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : AffineSpace V P<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : Module k V<VAR>b : AffineBasis ι k P<VAR>ι' : Type u_1<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : Finite ι'<VAR>inst✝ : DecidableEq ι'<VAR>p : ι' → P<VAR>A : Matrix ι ι' k<VAR>hA : b.toMatrix p * A = 1<GOAL>AffineIndependent k p
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : AffineSpace V P<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : Module k V<VAR>b : AffineBasis ι k P<VAR>ι' : Type u_1<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : Finite ι'<VAR>inst✝ : DecidableEq ι'<VAR>p : ι' → P<VAR>A : Matrix ι ι' k<VAR>hA : b.toMatrix p * A = 1<VAR>val✝ : Fintype ι'<GOAL>AffineIndependent k p