ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H₁ : l.size = 0 → r.size ≤ 1<VAR>H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size<VAR>H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3<GOAL>Valid' o₁ (l.balanceL x r) o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H₁ : l.size = 0 → r.size ≤ 1<VAR>H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size<VAR>H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3<GOAL>Valid' o₁ (l.balance' x r) o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H₁ : l.size = 0 → r.size ≤ 1<VAR>H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size<VAR>H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3<GOAL>2 * r.size ≤ 9 * l.size + 5
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H₁ : l.size = 0 → r.size ≤ 1<VAR>H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size<VAR>H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3<VAR>r0 : r.size = 0<GOAL>2 * r.size ≤ 9 * l.size + 5
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H₁ : l.size = 0 → r.size ≤ 1<VAR>H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size<VAR>H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3<VAR>r0 : r.size > 0<GOAL>2 * r.size ≤ 9 * l.size + 5
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H₁ : l.size = 0 → r.size ≤ 1<VAR>H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size<VAR>H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3<VAR>r0 : r.size > 0<VAR>l0 : l.size = 0<GOAL>2 * r.size ≤ 9 * l.size + 5
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H₁ : l.size = 0 → r.size ≤ 1<VAR>H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size<VAR>H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3<VAR>r0 : r.size > 0<VAR>l0 : l.size > 0<GOAL>2 * r.size ≤ 9 * l.size + 5
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>a : α<VAR>ha : Irreducible a<GOAL>¬IsSquare a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>a : α<VAR>ha : Irreducible a<GOAL>¬∃ c, a = c ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>b : α<VAR>ha : Irreducible (b ^ 2)<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p : ℝ<GOAL>(deriv fun x => x ^ p * (1 + ε x)) =ᶠ[atTop] fun x => deriv (fun x => x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x => 1 + ε x) x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p x : ℝ<VAR>hx : 1 < x<GOAL>deriv (fun x => x ^ p * (1 + ε x)) x = deriv (fun x => x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x => 1 + ε x) x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p x : ℝ<VAR>hx : 1 < x<GOAL>DifferentiableAt ℝ (fun x => 1 + ε x) x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p : ℝ<GOAL>(fun x => deriv (fun x => x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x => 1 + ε x) x) =ᶠ[atTop] fun x => p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / log x ^ 2)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p x : ℝ<VAR>hx : 1 < x<VAR>hderiv : deriv (fun x => 1 + ε x) x = -x⁻¹ / log x ^ 2<GOAL>deriv (fun x => x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x => 1 + ε x) x = p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / log x ^ 2)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p : ℝ<GOAL>(fun x => p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / log x ^ 2)) =ᶠ[atTop] fun x => p * x ^ (p - 1) * (1 + ε x) - x ^ (p - 1) / log x ^ 2
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p x : ℝ<VAR>hx : 0 < x<GOAL>p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / log x ^ 2) = p * x ^ (p - 1) * (1 + ε x) - x ^ (p - 1) / log x ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set β<VAR>hg : ContinuousOn g s<VAR>hf : Continuous f<VAR>hs : ∀ (x : α), f x ∈ s<GOAL>Continuous (g ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set β<VAR>hg : ContinuousOn g s<VAR>hf : ContinuousOn f univ<VAR>hs : ∀ (x : α), f x ∈ s<GOAL>ContinuousOn (g ∘ f) univ
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>g : R[X]<GOAL>h.map (g %ₘ f) = h.map g
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>g : R[X]<GOAL>f ∣ f * (g /ₘ f)
<VAR>R : Type u<VAR>inst✝⁸ : Ring R<VAR>Q : Type v<VAR>inst✝⁷ : AddCommGroup Q<VAR>inst✝⁶ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝¹ : Fact (Function.Injective ⇑i)<VAR>inst✝ : Small.{v, u} R<VAR>inj : Injective R Q<VAR>I : Ideal R<VAR>g : ↥I →ₗ[R] Q<VAR>eI : Shrink.{v, u} ↥I ≃ₗ[R] ↥I := Shrink.linearEquiv (↥I) R<VAR>eR : Shrink.{v, u} R ≃ₗ[R] R := Shrink.linearEquiv R R<GOAL>∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩
<VAR>R : Type u<VAR>inst✝⁸ : Ring R<VAR>Q : Type v<VAR>inst✝⁷ : AddCommGroup Q<VAR>inst✝⁶ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝¹ : Fact (Function.Injective ⇑i)<VAR>inst✝ : Small.{v, u} R<VAR>inj : Injective R Q<VAR>I : Ideal R<VAR>g : ↥I →ₗ[R] Q<VAR>eI : Shrink.{v, u} ↥I ≃ₗ[R] ↥I := Shrink.linearEquiv (↥I) R<VAR>eR : Shrink.{v, u} R ≃ₗ[R] R := Shrink.linearEquiv R R<VAR>g' : Shrink.{v, u} R →ₗ[R] Q<VAR>hg' : ∀ (x : Shrink.{v, u} ↥I), g' ((↑eR.symm ∘ₗ Submodule.subtype I ∘ₗ ↑eI) x) = (g ∘ₗ ↑eI) x<GOAL>∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ioo a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (a₁ ⊔ a₂) (b₁ ⊓ b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ioi a₁ ∩ Iio b₁ ∩ (Ioi a₂ ∩ Iio b₂) = Ioi a₁ ∩ Ioi a₂ ∩ (Iio b₁ ∩ Iio b₂)
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : TopologicalSpace X<VAR>ι : Type u_3<VAR>inst✝² : SemilatticeSup L<VAR>inst✝¹ : OrderBot L<VAR>inst✝ : ContinuousSup L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>t : Set X<VAR>x : X<VAR>hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x<GOAL>ContinuousWithinAt (s.sup f) t x
<VAR>Ω : Type u_1<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : SFinite μ<VAR>s : Set Ω<GOAL>∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) s)) = 0
<VAR>Ω : Type u_1<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : SFinite μ<VAR>s : Set Ω<VAR>Rs : ℕ → ℝ<VAR>left✝ : StrictAnti Rs<VAR>Rs_pos : ∀ (n : ℕ), 0 < Rs n<VAR>Rs_lim : Tendsto Rs atTop (𝓝 0)<GOAL>∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) s)) = 0
<VAR>Ω : Type u_1<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : SFinite μ<VAR>s : Set Ω<VAR>Rs : ℕ → ℝ<VAR>left✝ : StrictAnti Rs<VAR>Rs_pos : ∀ (n : ℕ), 0 < Rs n<VAR>Rs_lim : Tendsto Rs atTop (𝓝 0)<VAR>obs : ∀ (n : ℕ), ∃ r ∈ Ioo 0 (Rs n), μ (frontier (Metric.thickening r s)) = 0<GOAL>∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) s)) = 0
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : Countable ((l : ℕ) × L.Functions l)<GOAL>CG L M ↔ Countable M
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DivisionRing α<VAR>inst✝¹ : FunLike F ℚ α<VAR>inst✝ : RingHomClass F ℚ α<VAR>f : F<VAR>q : ℚ<GOAL>f q = ↑q
<VAR>a b : Cardinal.{u_1}<VAR>ha : ℵ₀ ≤ a<VAR>hb : b ≤ a<VAR>hb' : b ≠ 0<GOAL>a * b = a
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) (Fin 2)<VAR>U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}<GOAL>∃ j g, f = LocallyConstant.comap (C.π.app j) g
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) (Fin 2)<VAR>U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}<VAR>hU : IsClopen U<GOAL>∃ j g, f = LocallyConstant.comap (C.π.app j) g
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) (Fin 2)<VAR>U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}<VAR>hU : IsClopen U<VAR>j : J<VAR>V : Set ↑(F.obj j).toTop<VAR>hV : IsClopen V<VAR>h : U = ⇑(C.π.app j) ⁻¹' V<GOAL>∃ j g, f = LocallyConstant.comap (C.π.app j) g
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) (Fin 2)<VAR>U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}<VAR>hU : IsClopen U<VAR>j : J<VAR>V : Set ↑(F.obj j).toTop<VAR>hV : IsClopen V<VAR>h : U = ⇑(C.π.app j) ⁻¹' V<GOAL>f = LocallyConstant.comap (C.π.app j) (LocallyConstant.ofIsClopen hV)
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) (Fin 2)<VAR>U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}<VAR>hU : IsClopen U<VAR>j : J<VAR>V : Set ↑(F.obj j).toTop<VAR>hV : IsClopen V<VAR>h : U = ⇑(C.π.app j) ⁻¹' V<GOAL>⇑f ⁻¹' {0} = ⇑(LocallyConstant.comap (C.π.app j) (LocallyConstant.ofIsClopen hV)) ⁻¹' {0}
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) (Fin 2)<VAR>U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}<VAR>hU : IsClopen U<VAR>j : J<VAR>V : Set ↑(F.obj j).toTop<VAR>hV : IsClopen V<VAR>h : U = ⇑(C.π.app j) ⁻¹' V<GOAL>⇑f ⁻¹' {0} = ⇑(C.π.app j) ⁻¹' V
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ p₃ p₄ p₅ : P<VAR>h₁ : p₁ ∈ affineSpan k {p₄, p₅}<VAR>h₂ : p₂ ∈ affineSpan k {p₄, p₅}<VAR>h₃ : p₃ ∈ affineSpan k {p₄, p₅}<GOAL>Collinear k {p₁, p₂, p₃, p₄}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ p₃ p₄ p₅ : P<VAR>h₁ : p₁ ∈ affineSpan k {p₄, p₅}<VAR>h₂ : p₂ ∈ affineSpan k {p₄, p₅}<VAR>h₃ : p₃ ∈ affineSpan k {p₄, p₅}<GOAL>{p₁, p₂, p₃, p₄} ⊆ {p₁, p₂, p₃, p₄, p₅}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ p₃ p₄ p₅ : P<VAR>h₁ : p₁ ∈ affineSpan k {p₄, p₅}<VAR>h₂ : p₂ ∈ affineSpan k {p₄, p₅}<VAR>h₃ : p₃ ∈ affineSpan k {p₄, p₅}<GOAL>{p₄} ⊆ {p₄, p₅}
<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>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>i : LinearIndependent R v<GOAL>LinearIndependent (ι := { x // x ∈ range v }) R Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>s : Set α<VAR>T : Set (Set β)<VAR>f : α → β<VAR>x : α<VAR>x✝ : x ∈ s<GOAL>Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>s : Set α<VAR>T : Set (Set β)<VAR>f : α → β<VAR>x : α<VAR>x✝ : x ∈ s<GOAL>(∀ (i : Set β), f x ∈ i → i ∈ T → ∀ᶠ (a : α) in 𝓝[s] x, f a ∈ i) ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N✝ : Type u_3<VAR>inst✝² : Monoid N✝<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : (i : ι) → G i →* N<VAR>s : Subgroup N<VAR>h : ∀ (i : ι), (f i).range ≤ s<VAR>x : CoprodI G<GOAL>(lift f) x ∈ s
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N✝ : Type u_3<VAR>inst✝² : Monoid N✝<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : (i : ι) → G i →* N<VAR>s : Subgroup N<VAR>h : ∀ (i : ι), (f i).range ≤ s<GOAL>(lift f) 1 ∈ s
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N✝ : Type u_3<VAR>inst✝² : Monoid N✝<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : (i : ι) → G i →* N<VAR>s : Subgroup N<VAR>h : ∀ (i : ι), (f i).range ≤ s<VAR>i : ι<VAR>x : G i<GOAL>(lift f) (of x) ∈ s
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N✝ : Type u_3<VAR>inst✝² : Monoid N✝<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : (i : ι) → G i →* N<VAR>s : Subgroup N<VAR>h : ∀ (i : ι), (f i).range ≤ s<VAR>x y : CoprodI G<VAR>hx : (lift f) x ∈ s<VAR>hy : (lift f) y ∈ s<GOAL>(lift f) (x * y) ∈ s
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>b : Basis ι R L<VAR>i j : ℕ<VAR>hij : i + j = finrank R M<VAR>inst✝ : Nontrivial R<GOAL>((φ.polyCharpoly b).coeff i).IsHomogeneous j
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>b : Basis ι R L<VAR>i j : ℕ<VAR>hij : i + j = Fintype.card (Module.Free.ChooseBasisIndex R M)<VAR>inst✝ : Nontrivial R<GOAL>((φ.polyCharpoly b).coeff i).IsHomogeneous j
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>b : Basis ι R L<VAR>i j : ℕ<VAR>hij : i + j = Fintype.card (Module.Free.ChooseBasisIndex R M)<VAR>inst✝ : Nontrivial R<GOAL>(↑(MvPolynomial.bind₁ (toMvPolynomial b (Module.Free.chooseBasis R M).end φ)) ((charpoly.univ R (Module.Free.ChooseBasisIndex R M)).coeff i)).IsHomogeneous (1 * j)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>b : Basis ι R L<VAR>i j : ℕ<VAR>hij : i + j = Fintype.card (Module.Free.ChooseBasisIndex R M)<VAR>inst✝ : Nontrivial R<GOAL>∀ (r : R), ((algebraMap R (MvPolynomial ι R)) r).IsHomogeneous 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>b : Basis ι R L<VAR>i j : ℕ<VAR>hij : i + j = Fintype.card (Module.Free.ChooseBasisIndex R M)<VAR>inst✝ : Nontrivial R<GOAL>∀ (i : Module.Free.ChooseBasisIndex R M × Module.Free.ChooseBasisIndex R M), (toMvPolynomial b (Module.Free.chooseBasis R M).end φ i).IsHomogeneous 1
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁✝ l₂✝ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List (Sigma β)<VAR>nd₁ : l₁.NodupKeys<VAR>nd₂ : l₂.NodupKeys<VAR>p : l₁ ~ l₂<GOAL>lookupAll a l₁ = lookupAll a l₂
<VAR>a b p q : ℝ≥0<VAR>h✝ h : p.IsConjExponent q<GOAL>q = p / (p - 1)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → ℝ<VAR>s : Set α<VAR>hf : MonotoneOn f s<VAR>a b : α<VAR>as : a ∈ s<VAR>bs : b ∈ s<GOAL>eVariationOn f (s ∩ Icc a b) ≤ ENNReal.ofReal (f b - f a)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → ℝ<VAR>s : Set α<VAR>hf : MonotoneOn f s<VAR>a b : α<VAR>as : a ∈ s<VAR>bs : b ∈ s<GOAL>∀ (i : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b }), ∑ i_1 ∈ Finset.range i.1, edist (f (↑i.2 (i_1 + 1))) (f (↑i.2 i_1)) ≤ ENNReal.ofReal (f b - f a)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → ℝ<VAR>s : Set α<VAR>hf : MonotoneOn f s<VAR>a b : α<VAR>as : a ∈ s<VAR>bs : b ∈ s<VAR>n : ℕ<VAR>u : ℕ → α<VAR>hu : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b<GOAL>∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i)) ≤ ENNReal.ofReal (f b - f a)
<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>r : α → α → Prop<VAR>a✝ b✝ c d : α<VAR>P : {a b : α} → ReflTransGen r a b → Prop<VAR>a b : α<VAR>h : ReflTransGen r a b<VAR>ih₁ : ∀ (a : α), P ⋯<VAR>ih₂ : ∀ {a b : α} (h : r a b), P ⋯<VAR>ih₃ : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), P h₁ → P h₂ → P ⋯<GOAL>P h
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>ca : Computation α<VAR>cb : Computation β<VAR>h : LiftRel R ca cb<VAR>a : α<VAR>b : β<VAR>ma : a ∈ ca<VAR>mb : b ∈ cb<GOAL>R a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>ca : Computation α<VAR>cb : Computation β<VAR>h : LiftRel R ca cb<VAR>a : α<VAR>b : β<VAR>ma : a ∈ ca<VAR>mb : b ∈ cb<VAR>b' : β<VAR>mb' : b' ∈ cb<VAR>ab : R a b'<GOAL>R a b
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : ι → Set X<VAR>hs : IsCompact s<VAR>U : X → Set X<VAR>hxU : ∀ (x : X), U x ∈ 𝓝 x<VAR>hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite<GOAL>{i | (f i ∩ s).Nonempty}.Finite
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>f : ι → Set X<VAR>hs : IsCompact s<VAR>U : X → Set X<VAR>hxU : ∀ (x : X), U x ∈ 𝓝 x<VAR>hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite<VAR>t : Finset X<VAR>hsU : s ⊆ ⋃ x ∈ t, U x<GOAL>{i | (f i ∩ s).Nonempty}.Finite
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>f : ι → Set X<VAR>hs : IsCompact s<VAR>U : X → Set X<VAR>hxU : ∀ (x : X), U x ∈ 𝓝 x<VAR>hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite<VAR>t : Finset X<VAR>hsU : s ⊆ ⋃ x ∈ t, U x<GOAL>{i | (f i ∩ s).Nonempty} ⊆ ⋃ i ∈ ↑t, {i_1 | (f i_1 ∩ U i).Nonempty}
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>f : ι → Set X<VAR>hs : IsCompact s<VAR>U : X → Set X<VAR>hxU : ∀ (x : X), U x ∈ 𝓝 x<VAR>hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite<VAR>t : Finset X<VAR>hsU : s ⊆ ⋃ x ∈ t, U x<VAR>i : ι<VAR>x : X<VAR>hx : x ∈ f i ∩ s<GOAL>i ∈ ⋃ i ∈ ↑t, {i_1 | (f i_1 ∩ U i).Nonempty}
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>f : ι → Set X<VAR>hs : IsCompact s<VAR>U : X → Set X<VAR>hxU : ∀ (x : X), U x ∈ 𝓝 x<VAR>hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite<VAR>t : Finset X<VAR>hsU : s ⊆ ⋃ x ∈ t, U x<VAR>i : ι<VAR>x : X<VAR>hx : x ∈ f i ∩ s<VAR>c : X<VAR>hct : c ∈ t<VAR>hcx : x ∈ U c<GOAL>i ∈ ⋃ i ∈ ↑t, {i_1 | (f i_1 ∩ U i).Nonempty}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b✝ x : α<VAR>inst✝ : PartialOrder α<VAR>a b : α<VAR>hab : a ≤ b<GOAL>minimals (fun x x_1 => x ≤ x_1) (Icc a b) = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b✝ x : α<VAR>inst✝ : PartialOrder α<VAR>a b : α<VAR>hab : a ≤ b<GOAL>minimals (fun x x_1 => x ≤ x_1) {x | x ≤ b ∧ a ≤ x} = {a}
<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_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)<GOAL>image2 f' ((fun a => a) '' s) (g' '' t) = image2 f' s (g' '' t)