ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module S N<VAR>inst✝³ : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝² : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝¹ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>inst✝ : IsDomain R<GOAL>∃ s, #↑s = Module.rank R M ∧ LinearIndependent (ι := ↑s) R Subtype.val
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module S N<VAR>inst✝³ : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝² : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝¹ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>inst✝ : IsDomain R<VAR>w : Module.Free.ChooseBasisIndex (FractionRing R) (LocalizedModule R⁰ M) → M<VAR>hw : LinearIndependent R w<GOAL>∃ s, #↑s = Module.rank R M ∧ LinearIndependent (ι := ↑s) R Subtype.val
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module S N<VAR>inst✝³ : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝² : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝¹ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>inst✝ : IsDomain R<VAR>w : Module.Free.ChooseBasisIndex (FractionRing R) (LocalizedModule R⁰ M) → M<VAR>hw : LinearIndependent R w<GOAL>#↑(Set.range w) = Module.rank R M
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module S N<VAR>inst✝³ : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝² : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝¹ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>inst✝ : IsDomain R<VAR>w : Module.Free.ChooseBasisIndex (FractionRing R) (LocalizedModule R⁰ M) → M<VAR>hw : LinearIndependent R w<GOAL>lift.{max u v, v} #↑(Set.range w) = lift.{max u v, v} (Module.rank R M)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>h : ∃ a, b = succ a<VAR>c : Ordinal.{u_4}<VAR>e : b = succ c<GOAL>a < b.pred ↔ succ a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>h : ¬∃ a, b = succ a<GOAL>a < b.pred ↔ succ a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>q : ℚ<GOAL>Integrable (fun t => ⨅ r, f (a, t) ↑r) (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>q : ℚ<GOAL>Memℒp (fun t => ⨅ r, f (a, t) ↑r) 1 (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>q : ℚ<GOAL>eLpNorm (fun t => ⨅ r, f (a, t) ↑r) 1 (ν a) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>q : ℚ<GOAL>eLpNorm (fun t => ⨅ r, f (a, t) ↑r) 1 (ν a) ≤ (ν a) univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>q : ℚ<GOAL>∀ᵐ (x : β) ∂ν a, ‖⨅ r, f (a, x) ↑r‖ ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>q : ℚ<VAR>t : β<VAR>hbdd_below : ∀ (q : ℚ), BddBelow (range fun r => f (a, t) ↑r)<VAR>h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q<VAR>h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1<GOAL>‖⨅ r, f (a, t) ↑r‖ ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>q : ℚ<VAR>t : β<VAR>hbdd_below : ∀ (q : ℚ), BddBelow (range fun r => f (a, t) ↑r)<VAR>h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q<VAR>h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1<GOAL>⨅ r, f (a, t) ↑r ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>q : ℚ<VAR>t : β<VAR>hbdd_below : ∀ (q : ℚ), BddBelow (range fun r => f (a, t) ↑r)<VAR>h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q<VAR>h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1<GOAL>0 ≤ ⨅ r, f (a, t) ↑r
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁ J₂ : GrothendieckTopology C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>S : Sieve X<GOAL>J₁.close (Sieve.pullback f S) = Sieve.pullback f (J₁.close S)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁ J₂ : GrothendieckTopology C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>S : Sieve X<GOAL>J₁.close (Sieve.pullback f S) ≤ Sieve.pullback f (J₁.close S)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁ J₂ : GrothendieckTopology C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>S : Sieve X<GOAL>Sieve.pullback f (J₁.close S) ≤ J₁.close (Sieve.pullback f S)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type w<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : Flat R M<VAR>e : N ≃ₗ[R] M<VAR>h : ↑e.symm ∘ₗ ↑e = LinearMap.id<GOAL>Flat R N
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCancelCommMonoid E<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>c : E<GOAL>StrictConcaveOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : Field A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : IsReduced B<VAR>n : ℕ<VAR>p : A[X]<VAR>dvd : minpoly A x ∣ p ^ n<GOAL>minpoly A x ∣ p
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : Field A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : IsReduced B<VAR>n : ℕ<VAR>p : A[X]<VAR>dvd : (Polynomial.aeval x) (p ^ n) = 0<GOAL>(Polynomial.aeval x) p = 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : Field A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : IsReduced B<VAR>n : ℕ<VAR>p : A[X]<VAR>dvd : (Polynomial.aeval x) p ^ n = 0<GOAL>(Polynomial.aeval x) p = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>f : ℕ → ℕ<VAR>h1 : Monotone f<VAR>B : ℕ<VAR>h2 : ∀ (n : ℕ), f n ≤ B<VAR>h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)<GOAL>∀ (k : ℕ), B ≤ k → f k = f B
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>f : ℕ → ℕ<VAR>h1 : Monotone f<VAR>B : ℕ<VAR>h2 : ∀ (n : ℕ), f n ≤ B<VAR>h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)<VAR>key : ∃ n ≤ B, f n = f (n + 1)<GOAL>∀ (k : ℕ), B ≤ k → f k = f B
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>f : ℕ → ℕ<VAR>h1 : Monotone f<VAR>B : ℕ<VAR>h2 : ∀ (n : ℕ), f n ≤ B<VAR>h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)<VAR>n : ℕ<VAR>hn1 : n ≤ B<VAR>hn2 : f n = f (n + 1)<GOAL>∀ (k : ℕ), B ≤ k → f k = f B
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>f : ℕ → ℕ<VAR>h1 : Monotone f<VAR>B : ℕ<VAR>h2 : ∀ (n : ℕ), f n ≤ B<VAR>h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)<VAR>n : ℕ<VAR>hn1 : n ≤ B<VAR>hn2 : f n = f (n + 1)<VAR>key : ∀ (k : ℕ), f (n + k) = f (n + k + 1) ∧ f (n + k) = f n<GOAL>∀ (k : ℕ), B ≤ k → f k = f B
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>f : ℕ → ℕ<VAR>h1 : Monotone f<VAR>B : ℕ<VAR>h2 : ∀ (n : ℕ), f n ≤ B<VAR>h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)<VAR>n : ℕ<VAR>hn1 : n ≤ B<VAR>hn2 : f n = f (n + 1)<VAR>key : ∀ (k : ℕ), n ≤ k → f k = f n<GOAL>∀ (k : ℕ), B ≤ k → f k = f B
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁶ : NormedField 𝕜<VAR>inst✝⁵ : NormedRing 𝕝<VAR>inst✝⁴ : NormedSpace 𝕜 𝕝<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : SMulWithZero 𝕝 E<VAR>inst✝ : IsScalarTower 𝕜 𝕝 E<VAR>s t u v A B : Set E<VAR>x : E<VAR>a b : 𝕜<VAR>hA : Balanced 𝕜 A<VAR>ha : 1 ≤ ‖a‖<GOAL>A ⊆ a • A
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁶ : NormedField 𝕜<VAR>inst✝⁵ : NormedRing 𝕝<VAR>inst✝⁴ : NormedSpace 𝕜 𝕝<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : SMulWithZero 𝕝 E<VAR>inst✝ : IsScalarTower 𝕜 𝕝 E<VAR>s t u v A B : Set E<VAR>x : E<VAR>a b : 𝕜<VAR>hA : Balanced 𝕜 A<VAR>ha : ‖1‖ ≤ ‖a‖<GOAL>A ⊆ a • A
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<GOAL>s.pi t₁ ⊆ s.pi t₂ ↔ (∀ i ∈ s, t₁ i ⊆ t₂ i) ∨ s.pi t₁ = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>h : s.pi t₁ ⊆ s.pi t₂<GOAL>¬s.pi t₁ = ∅ → ∀ i ∈ s, t₁ i ⊆ t₂ i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>h : s.pi t₁ ⊆ s.pi t₂<GOAL>(s.pi t₁).Nonempty → ∀ i ∈ s, t₁ i ⊆ t₂ i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i✝ : ι<VAR>h : s.pi t₁ ⊆ s.pi t₂<VAR>hne : (s.pi t₁).Nonempty<VAR>i : ι<VAR>hi : i ∈ s<GOAL>t₁ i ⊆ t₂ i
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : dist p₁ p₂ = dist p₁ p₃<GOAL>∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖<GOAL>∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β✝ : Type u_3<VAR>γ✝ : Type u_4<VAR>δ✝ : Type u_5<VAR>inst✝⁶ : LE α✝<VAR>inst✝⁵ : LE β✝<VAR>inst✝⁴ : LE γ✝<VAR>α : Type ?u.63266<VAR>β : Type ?u.63269<VAR>γ : Type ?u.63272<VAR>δ : Type ?u.63275<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : Preorder γ<VAR>inst✝ : Preorder δ<VAR>f : α ≃o γ<VAR>g : β ≃o δ<VAR>p : α →o β<GOAL>(⇑g.symm ∘ ⇑g) ∘ ⇑p ∘ ⇑f.symm ∘ ⇑f = ⇑p
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β✝ : Type u_3<VAR>γ✝ : Type u_4<VAR>δ✝ : Type u_5<VAR>inst✝⁶ : LE α✝<VAR>inst✝⁵ : LE β✝<VAR>inst✝⁴ : LE γ✝<VAR>α : Type ?u.63266<VAR>β : Type ?u.63269<VAR>γ : Type ?u.63272<VAR>δ : Type ?u.63275<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : Preorder γ<VAR>inst✝ : Preorder δ<VAR>f : α ≃o γ<VAR>g : β ≃o δ<VAR>p : γ →o δ<GOAL>(⇑g ∘ ⇑g.symm) ∘ ⇑p ∘ ⇑f ∘ ⇑f.symm = ⇑p
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β✝ : Type u_3<VAR>γ✝ : Type u_4<VAR>δ✝ : Type u_5<VAR>inst✝⁶ : LE α✝<VAR>inst✝⁵ : LE β✝<VAR>inst✝⁴ : LE γ✝<VAR>α : Type ?u.63266<VAR>β : Type ?u.63269<VAR>γ : Type ?u.63272<VAR>δ : Type ?u.63275<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : Preorder γ<VAR>inst✝ : Preorder δ<VAR>f : α ≃o γ<VAR>g : β ≃o δ<VAR>p q : α →o β<GOAL>{ toFun := fun p => (↑g).comp (p.comp ↑f.symm), invFun := fun p => (↑g.symm).comp (p.comp ↑f), left_inv := ⋯, right_inv := ⋯ } p ≤ { toFun := fun p => (↑g).comp (p.comp ↑f.symm), invFun := fun p => (↑g.symm).comp (p.comp ↑f), left_inv := ⋯, right_inv := ⋯ } q ↔ p ≤ q
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β✝ : Type u_3<VAR>γ✝ : Type u_4<VAR>δ✝ : Type u_5<VAR>inst✝⁶ : LE α✝<VAR>inst✝⁵ : LE β✝<VAR>inst✝⁴ : LE γ✝<VAR>α : Type ?u.63266<VAR>β : Type ?u.63269<VAR>γ : Type ?u.63272<VAR>δ : Type ?u.63275<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : Preorder γ<VAR>inst✝ : Preorder δ<VAR>f : α ≃o γ<VAR>g : β ≃o δ<VAR>p q : α →o β<GOAL>(∀ (x : γ), p (f.symm x) ≤ q (f.symm x)) ↔ ∀ (x : α), p x ≤ q x
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>m = n + 1 → n ≤ m
<VAR>a b c d n k : ℕ<VAR>p q : ℕ → Prop<GOAL>n ≤ n + 1
<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<GOAL>(deriv fun x => 1 - ε x) =ᶠ[atTop] -deriv ε
<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>x : ℝ<VAR>hx : 1 < x<GOAL>deriv (fun x => 1 - ε x) x = (-deriv ε) 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<GOAL>-deriv ε =ᶠ[atTop] fun x => 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>x : ℝ<VAR>hx : 1 < x<GOAL>(-deriv ε) x = x⁻¹ / log x ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : β → E<VAR>μ : Measure β<VAR>a : α<VAR>s : Set β<GOAL>∫ (x : β) in s, f x ∂(const α μ) a = ∫ (x : β) in s, f x ∂μ
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<GOAL>edist x y ≤ edist x z + edist y z
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<GOAL>edist x y ≤ edist x z + edist z y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<GOAL>𝓝ˢ s = 𝓟 s ↔ IsOpen s
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>s : Set V<VAR>u : V<VAR>hu : u ∈ s<VAR>patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩<GOAL>(induce s G).Connected
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>s : Set V<VAR>u : V<VAR>hu : u ∈ s<VAR>patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩<GOAL>∃ v, ∀ (w : ↑s), (induce s G).Reachable v w
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>s : Set V<VAR>u : V<VAR>hu : u ∈ s<VAR>patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩<VAR>v : V<VAR>hv : v ∈ s<VAR>sv : Set V<VAR>svs : sv ⊆ s<VAR>hu' : u ∈ sv<VAR>hv' : v ∈ sv<VAR>uv : (induce sv G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩<GOAL>(induce s G).Reachable ⟨u, hu⟩ ⟨v, hv⟩
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>l : ι →₀ 𝕜<VAR>v : ι → E<VAR>x : E<GOAL>⟪l.sum fun i a => a • v i, x⟫_𝕜 = l.sum fun i a => (starRingEnd 𝕜) a • ⟪v i, 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✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>l : ι →₀ 𝕜<VAR>v : ι → E<VAR>x : E<GOAL>(l.sum fun i a => (starRingEnd 𝕜) a • ⟪v i, x⟫_𝕜) = ∑ i ∈ l.support, ⟪l i • v i, x⟫_𝕜
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : DecidableEq o<VAR>inst✝¹ : Zero α<VAR>inst✝ : Zero β<VAR>M : (i : o) → Matrix (m' i) (n' i) α<VAR>ii : o<VAR>ix : n' ii<VAR>ji : o<VAR>jx : m' ji<GOAL>(blockDiagonal' M)ᵀ ⟨ii, ix⟩ ⟨ji, jx⟩ = blockDiagonal' (fun k => (M k)ᵀ) ⟨ii, ix⟩ ⟨ji, jx⟩
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : DecidableEq o<VAR>inst✝¹ : Zero α<VAR>inst✝ : Zero β<VAR>M : (i : o) → Matrix (m' i) (n' i) α<VAR>ii : o<VAR>ix : n' ii<VAR>ji : o<VAR>jx : m' ji<GOAL>(if h : ji = ii then M ji jx (cast ⋯ ix) else 0) = if h : ii = ji then M ii (cast ⋯ jx) ix else 0
<VAR>a : PartENat<VAR>ha : a.Dom<VAR>b : ℕ<GOAL>a.get ha = b ↔ a = ↑b
<VAR>a : PartENat<VAR>ha : a.Dom<VAR>b : ℕ<GOAL>a = ↑b ↔ a = ↑b
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F✝ G✝ : C ⥤ D<VAR>F G : Cᵒᵖ ⥤ Dᵒᵖ<VAR>α : F.unop ⟶ G.unop<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>(G.map f ≫ (fun X => (α.app (unop X)).op) Y).unop = ((fun X => (α.app (unop X)).op) X ≫ F.map f).unop
<VAR>a b m n p : ℕ<GOAL>0 < a.factorizationLCMLeft b
<VAR>a b m n p : ℕ<GOAL>a.factorizationLCMLeft b ≠ 0
<VAR>a b m n p : ℕ<GOAL>∀ i ∈ (a.lcm b).factorization.support, (if b.factorization i ≤ a.factorization i then i ^ (a.lcm b).factorization i else 1) ≠ 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s t : Multiset α<GOAL>s ≤ t + s
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>h : constantCoeff Φ = 0<VAR>n : ℕ<GOAL>constantCoeff (wittStructureInt p Φ n) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>h : constantCoeff Φ = 0<VAR>n : ℕ<VAR>inj : Function.Injective ⇑(Int.castRingHom ℚ)<GOAL>constantCoeff (wittStructureInt p Φ n) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>h : constantCoeff Φ = 0<VAR>n : ℕ<VAR>inj : Function.Injective ⇑(Int.castRingHom ℚ)<GOAL>(Int.castRingHom ℚ) (constantCoeff (wittStructureInt p Φ n)) = (Int.castRingHom ℚ) 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>h : constantCoeff Φ = 0<VAR>n : ℕ<VAR>inj : Function.Injective ⇑(Int.castRingHom ℚ)<GOAL>constantCoeff ((map (Int.castRingHom ℚ)) Φ) = 0
<VAR>a b c d a' b' c' : Ordinal.{u}<VAR>ha : a' ≤ a<VAR>hb : b' ≤ b<VAR>hc : c' ≤ c<GOAL>a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') ≤ a ⨳ (b ⨳ c) ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')
<VAR>a b c d a' b' c' : Ordinal.{u}<VAR>ha : a' ≤ a<VAR>hb : b' ≤ b<VAR>hc : c' ≤ c<GOAL>b ⨳ c ⨳ a' ♯ b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b' ⨳ c' ⨳ a' ≤ b ⨳ c ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a' ♯ b' ⨳ c' ⨳ a
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)<GOAL>Tendsto μs F (𝓝 0)
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)<GOAL>∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (testAgainstNN 0 f))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)<VAR>f : Ω →ᵇ ℝ≥0<GOAL>Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (testAgainstNN 0 f))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)<VAR>f : Ω →ᵇ ℝ≥0<GOAL>testAgainstNN 0 f = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x y : ℝ<VAR>s s' : Set ℝ<VAR>hs'_unique : UniqueDiffWithinAt ℝ s' y<VAR>hs_unique : UniqueDiffOn ℝ s<VAR>hs' : s' ∈ 𝓝[s] y<VAR>hy : y ∈ s'<VAR>h : s' ⊆ s<VAR>k : ℕ<VAR>hk : ContDiffOn ℝ (↑k) f s → DifferentiableWithinAt ℝ (iteratedDerivWithin k f s) s y → HasDerivWithinAt (fun t => taylorWithinEval f k s t x) (((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y<VAR>hf : ContDiffOn ℝ (↑(k + 1)) f s<VAR>hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y<GOAL>HasDerivWithinAt (fun t => taylorWithinEval f (k + 1) s t x) (((↑(k + 1)!)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 1 + 1) f s y) s' y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x y : ℝ<VAR>s s' : Set ℝ<VAR>hs'_unique : UniqueDiffWithinAt ℝ s' y<VAR>hs_unique : UniqueDiffOn ℝ s<VAR>hs' : s' ∈ 𝓝[s] y<VAR>hy : y ∈ s'<VAR>h : s' ⊆ s<VAR>k : ℕ<VAR>hk : ContDiffOn ℝ (↑k) f s → DifferentiableWithinAt ℝ (iteratedDerivWithin k f s) s y → HasDerivWithinAt (fun t => taylorWithinEval f k s t x) (((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y<VAR>hf : ContDiffOn ℝ (↑(k + 1)) f s<VAR>hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y<GOAL>HasDerivWithinAt (fun t => taylorWithinEval f k s t x + (((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t) (((↑(k + 0).succ !)⁻¹ * (x - y) ^ (k + 0).succ) • iteratedDerivWithin ((k + 0).succ + 0).succ f s y) s' y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x y : ℝ<VAR>s s' : Set ℝ<VAR>hs'_unique : UniqueDiffWithinAt ℝ s' y<VAR>hs_unique : UniqueDiffOn ℝ s<VAR>hs' : s' ∈ 𝓝[s] y<VAR>hy : y ∈ s'<VAR>h : s' ⊆ s<VAR>k : ℕ<VAR>hk : ContDiffOn ℝ (↑k) f s → DifferentiableWithinAt ℝ (iteratedDerivWithin k f s) s y → HasDerivWithinAt (fun t => taylorWithinEval f k s t x) (((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y<VAR>hf : ContDiffOn ℝ (↑(k + 1)) f s<VAR>hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y<GOAL>HasDerivWithinAt (fun t => taylorWithinEval f k s t x + (((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t) ((((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ k.succ) • iteratedDerivWithin k.succ.succ f s y) s' y