ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : α → E<VAR>hf : Integrable f μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>↑{ measureOf' := fun s => if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ } s = ∫ (x : α) in s, f x ∂μ
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f₁ f₂ f₃ : ArithmeticFunction R<VAR>x✝ : ℕ<GOAL>((f₁.pmul f₂).pmul f₃) x✝ = (f₁.pmul (f₂.pmul f₃)) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<GOAL>Nat.card { x // x ∈ s } = s.card
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : IsArtinian R M<VAR>s : Set M<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<GOAL>s.Finite
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : IsArtinian R M<VAR>s : Set M<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>hf : ¬s.Finite<GOAL>(fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : IsArtinian R M<VAR>s : Set M<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>hf : ¬s.Finite<VAR>f : ℕ ↪ ↑s<GOAL>(fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : IsArtinian R M<VAR>s : Set M<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>hf : ¬s.Finite<VAR>f : ℕ ↪ ↑s<VAR>this : ∀ (n : ℕ), Subtype.val ∘ ⇑f '' {m | n ≤ m} ⊆ s<GOAL>(fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : IsArtinian R M<VAR>s : Set M<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>hf : ¬s.Finite<VAR>f : ℕ ↪ ↑s<VAR>this✝ : ∀ (n : ℕ), Subtype.val ∘ ⇑f '' {m | n ≤ m} ⊆ s<VAR>this : ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ⇑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ⇑f '' {m | a ≤ m})<GOAL>(fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>X₀ X₁ X₂ : V<VAR>d₀ : X₀ ⟶ X₁<VAR>d₁ : X₁ ⟶ X₂<VAR>s : d₀ ≫ d₁ = 0<VAR>succ : (S : ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0<GOAL>(if 1 = 0 + 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>h : μ ≪ ν<GOAL>ν.withDensity (μ.rnDeriv ν) = μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>h : μ ≪ ν<GOAL>μ.singularPart ν = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>h : μ ≪ ν<GOAL>(μ.singularPart ν) Set.univ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>h : μ ≪ ν<VAR>h_sing : μ.singularPart ν ⟂ₘ ν<GOAL>(μ.singularPart ν) Set.univ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>h : μ ≪ ν<VAR>h_sing : μ.singularPart ν ⟂ₘ ν<GOAL>(μ.singularPart ν) h_sing.nullSet + (μ.singularPart ν) h_sing.nullSetᶜ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>h : μ ≪ ν<VAR>h_sing : μ.singularPart ν ⟂ₘ ν<GOAL>(μ.singularPart ν) h_sing.nullSetᶜ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>h : μ ≪ ν<VAR>h_sing : μ.singularPart ν ⟂ₘ ν<GOAL>(μ.singularPart ν) h_sing.nullSetᶜ ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>h : μ ≪ ν<VAR>h_sing : μ.singularPart ν ⟂ₘ ν<GOAL>μ h_sing.nullSetᶜ = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : HasPullback f g<GOAL>(pullbackSymmetry f g).inv ≫ pullback.fst f g = pullback.snd g f
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>constantCoeff (W_ R n) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(∑ x ∈ range (n + 1), if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>∀ x ∈ range (n + 1), (if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>hp : Fact (Nat.Prime p)<VAR>n i : ℕ<VAR>a✝ : i ∈ range (n + 1)<GOAL>(if single i (p ^ (n - i)) = 0 then ↑p ^ i else 0) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>hp : Fact (Nat.Prime p)<VAR>n i : ℕ<VAR>a✝ : i ∈ range (n + 1)<GOAL>¬single i (p ^ (n - i)) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>hp : Fact (Nat.Prime p)<VAR>n i : ℕ<VAR>a✝ : i ∈ range (n + 1)<GOAL>¬p ^ (n - i) = 0
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>inst✝² : ConcreteCategory D<VAR>J : GrothendieckTopology C<VAR>F₁ F₂ : Sheaf J D<VAR>φ : F₁ ⟶ F₂<VAR>inst✝¹ : J.HasSheafCompose (forget D)<VAR>inst✝ : IsLocallyInjective φ<GOAL>Mono φ
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>inst✝² : ConcreteCategory D<VAR>J : GrothendieckTopology C<VAR>F₁ F₂ : Sheaf J D<VAR>φ : F₁ ⟶ F₂<VAR>inst✝¹ : J.HasSheafCompose (forget D)<VAR>inst✝ : IsLocallyInjective φ<GOAL>∀ (X : Cᵒᵖ), Function.Injective ⇑(φ.val.app X)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>inst✝² : ConcreteCategory D<VAR>J : GrothendieckTopology C<VAR>F₁ F₂ : Sheaf J D<VAR>φ : F₁ ⟶ F₂<VAR>inst✝¹ : J.HasSheafCompose (forget D)<VAR>inst✝ : IsLocallyInjective φ<GOAL>IsLocallyInjective φ
<VAR>R : CommRingCatᵒᵖ<GOAL>locallyRingedSpaceMap (𝟙 (unop R)) = 𝟙 (locallyRingedSpaceObj (unop R))
<VAR>X✝ Y✝ Z✝ : CommRingCatᵒᵖ<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>locallyRingedSpaceMap (g.unop ≫ f.unop) = locallyRingedSpaceMap f.unop ≫ locallyRingedSpaceMap g.unop
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c✝ c d : Con M<GOAL>c ⊔ d = conGen fun x y => c x y ∨ d x y
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c✝ c d : Con M<GOAL>c ⊔ d = sInf {s | ∀ (x y : M), c x y ∨ d x y → s x y}
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c✝ c d : Con M<GOAL>{x | c ≤ x ∧ d ≤ x} = {s | ∀ (x y : M), c x y ∨ d x y → s x y}
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t✝ t : Set G<VAR>h : tᶜ * closure {1} = tᶜ<GOAL>t * closure {1} = t
<VAR>a b c d a' b' : Ordinal.{u}<VAR>ha : a' < a<VAR>hb : b' < b<GOAL>a' ⨳ b ♯ a ⨳ b' < a ⨳ b ♯ a' ⨳ b'
<VAR>a b c d a' b' : Ordinal.{u}<VAR>ha : a' < a<VAR>hb : b' < b<GOAL>a' ⨳ b ♯ a ⨳ b' < sInf {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} ♯ a' ⨳ b'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : PseudoEMetricSpace α<VAR>f g : α → ℝ<VAR>Kf Kg : ℝ≥0<VAR>hf : LipschitzWith Kf f<VAR>a : ℝ<GOAL>LipschitzWith Kf fun x => min a (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<GOAL>∀ u ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b}, IsOpen u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : ℝ<VAR>v : Set ℝ<VAR>hav : a ∈ v<VAR>hv : IsOpen v<VAR>l u : ℝ<VAR>hl : l < a<VAR>hu : a < u<VAR>h : Ioo l u ⊆ v<VAR>q : ℚ<VAR>hlq : l < ↑q<VAR>hqa : ↑q < a<VAR>p : ℚ<VAR>hap : a < ↑p<VAR>hpu : ↑p < u<GOAL>Ioo ↑q ↑p ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : ℝ<VAR>v : Set ℝ<VAR>hav : a ∈ v<VAR>hv : IsOpen v<VAR>l u : ℝ<VAR>hl : l < a<VAR>hu : a < u<VAR>h : Ioo l u ⊆ v<VAR>q : ℚ<VAR>hlq : l < ↑q<VAR>hqa : ↑q < a<VAR>p : ℚ<VAR>hap : a < ↑p<VAR>hpu : ↑p < u<GOAL>∃ i i_1, ∃ (_ : i < i_1), Ioo ↑q ↑p ∈ {Ioo ↑i ↑i_1}
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>s : Finset ι<VAR>f : Π₀ (i : ι), α i<VAR>t : (i : ι) → Finset (α i)<VAR>inst✝ : (i : ι) → DecidableEq (α i)<GOAL>f ∈ s.dfinsupp t ↔ f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>s : Finset ι<VAR>f : Π₀ (i : ι), α i<VAR>t : (i : ι) → Finset (α i)<VAR>inst✝ : (i : ι) → DecidableEq (α i)<GOAL>(∃ a ∈ s.pi t, { toFun := fun f => DFinsupp.mk s fun i => f ↑i ⋯, inj' := ⋯ } a = f) → f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>s : Finset ι<VAR>f : Π₀ (i : ι), α i<VAR>t : (i : ι) → Finset (α i)<VAR>inst✝ : (i : ι) → DecidableEq (α i)<GOAL>(f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i) → ∃ a ∈ s.pi t, { toFun := fun f => DFinsupp.mk s fun i => f ↑i ⋯, inj' := ⋯ } a = f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>K : SimplicialComplex 𝕜 E<VAR>s t : Finset E<VAR>x : E<VAR>hx : x ∈ K.vertices<VAR>hs : s ∈ K.faces<GOAL>x ∈ (convexHull 𝕜) ↑s ↔ x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>K : SimplicialComplex 𝕜 E<VAR>s t : Finset E<VAR>x : E<VAR>hx : x ∈ K.vertices<VAR>hs : s ∈ K.faces<VAR>h : x ∈ (convexHull 𝕜) ↑s<GOAL>x ∈ s
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<GOAL>Disjoint (G.edgeFinset \ G.incidenceFinset t) (image (fun x => s(x, t)) (G.neighborFinset s))
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<GOAL>∀ a ∈ G.edgeFinset \ G.incidenceFinset t, ∀ b ∈ image (fun x => s(x, t)) (G.neighborFinset s), a ≠ b
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>e : Sym2 V<VAR>he : e ∈ G.edgeFinset \ G.incidenceFinset t<GOAL>∀ b ∈ image (fun x => s(x, t)) (G.neighborFinset s), e ≠ b
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>e : Sym2 V<VAR>he : e ∈ G.edgeFinset \ G.incidenceFinset t<VAR>this : t ∉ e<GOAL>∀ b ∈ image (fun x => s(x, t)) (G.neighborFinset s), e ≠ b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : StrictOrderedCommRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x y z : E<VAR>h : x ∈ [y-[𝕜]z]<GOAL>SameRay 𝕜 (x - y) (z - x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : StrictOrderedCommRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x y z : E<VAR>h : x ∈ (fun θ => y + θ • (z - y)) '' Icc 0 1<GOAL>SameRay 𝕜 (x - y) (z - x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : StrictOrderedCommRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>y z : E<VAR>θ : 𝕜<VAR>hθ₀ : 0 ≤ θ<VAR>hθ₁ : θ ≤ 1<GOAL>SameRay 𝕜 ((fun θ => y + θ • (z - y)) θ - y) (z - (fun θ => y + θ • (z - y)) θ)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x y : HahnSeries Γ R<VAR>a : Γ<VAR>ha : a ∈ (x + y).support<GOAL>a ∈ x.support ∪ y.support
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x y : HahnSeries Γ R<VAR>a : Γ<VAR>ha : x.coeff a + y.coeff a ≠ 0<GOAL>a ∈ x.support ∪ y.support
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x y : HahnSeries Γ R<VAR>a : Γ<VAR>ha : x.coeff a + y.coeff a ≠ 0<GOAL>x.coeff a ≠ 0 ∨ y.coeff a ≠ 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x y : HahnSeries Γ R<VAR>a : Γ<VAR>ha : x.coeff a = 0 ∧ y.coeff a = 0<GOAL>x.coeff a + y.coeff a = 0
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>(lsub f).cof ≤ Cardinal.lift.{v, u} #ι
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>(lsub f).cof ≤ #(ULift.{v, u} ι)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>lsub f = lsub fun i => f i.down
<VAR>x : WithBot ℕ<GOAL>¬x < 1 ↔ ¬x ≤ 0
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>r : R<VAR>b : CliffordAlgebra Q<GOAL>(contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r * b) = (algebraMap R (CliffordAlgebra Q)) r * (contractLeft d) b
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype o<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>A : Matrix m m R<VAR>B : Matrix m n R<VAR>hA : IsUnit A.det<VAR>b : Basis m R (m → R) := Pi.basisFun R m<GOAL>(A * B).rank = B.rank
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype o<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>A : Matrix m m R<VAR>B : Matrix m n R<VAR>b : Basis m R (m → R) := Pi.basisFun R m<VAR>hA : IsUnit ((LinearMap.toMatrix b b) A.mulVecLin).det<GOAL>(A * B).rank = B.rank
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype o<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>A : Matrix m m R<VAR>B : Matrix m n R<VAR>b : Basis m R (m → R) := Pi.basisFun R m<VAR>hA : IsUnit ((LinearMap.toMatrix b b) A.mulVecLin).det<VAR>hAB : (A * B).mulVecLin = ↑(LinearEquiv.ofIsUnitDet hA) ∘ₗ B.mulVecLin<GOAL>(A * B).rank = B.rank
<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>q : ℝ → ℝ<VAR>hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>hq_poly : GrowsPolynomially fun x => ‖deriv q x‖<VAR>i : α<VAR>b' : ℝ := b (min_bi b) / 2<GOAL>(fun n => q ↑(r i n) - q (b i * ↑n)) =O[atTop] fun n => deriv q ↑n * (↑(r i n) - b i * ↑n)
<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>q : ℝ → ℝ<VAR>hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>hq_poly : GrowsPolynomially fun x => ‖deriv q x‖<VAR>i : α<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<GOAL>(fun n => q ↑(r i n) - q (b i * ↑n)) =O[atTop] fun n => deriv q ↑n * (↑(r i n) - b i * ↑n)
<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>q : ℝ → ℝ<VAR>hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>hq_poly : GrowsPolynomially fun x => ‖deriv q x‖<VAR>i : α<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>hb_lt_one : b' < 1<GOAL>(fun n => q ↑(r i n) - q (b i * ↑n)) =O[atTop] fun n => deriv q ↑n * (↑(r i n) - b i * ↑n)
<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>q : ℝ → ℝ<VAR>hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>hq_poly : GrowsPolynomially fun x => ‖deriv q x‖<VAR>i : α<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>hb_lt_one : b' < 1<VAR>hb : b' ∈ Set.Ioo 0 1<GOAL>(fun n => q ↑(r i n) - q (b i * ↑n)) =O[atTop] fun n => deriv q ↑n * (↑(r i n) - b i * ↑n)
<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>q : ℝ → ℝ<VAR>hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>hq_poly : GrowsPolynomially fun x => ‖deriv q x‖<VAR>i : α<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>hb_lt_one : b' < 1<VAR>hb : b' ∈ Set.Ioo 0 1<VAR>hb' : ∀ (i : α), b' ≤ b i<GOAL>(fun n => q ↑(r i n) - q (b i * ↑n)) =O[atTop] fun n => deriv q ↑n * (↑(r i n) - b i * ↑n)
<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>q : ℝ → ℝ<VAR>hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>hq_poly✝ : GrowsPolynomially fun x => ‖deriv q x‖<VAR>i : α<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>hb_lt_one : b' < 1<VAR>hb : b' ∈ Set.Ioo 0 1<VAR>hb' : ∀ (i : α), b' ≤ b i<VAR>c₁ : ℝ<VAR>left✝¹ : c₁ > 0<VAR>c₂ : ℝ<VAR>left✝ : c₂ > 0<VAR>hq_poly : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b' * x) x, (fun x => ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x => ‖deriv q x‖) x) (c₂ * (fun x => ‖deriv q x‖) x)<GOAL>(fun n => q ↑(r i n) - q (b i * ↑n)) =O[atTop] fun n => deriv q ↑n * (↑(r i n) - b i * ↑n)
<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>q : ℝ → ℝ<VAR>hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>hq_poly✝ : GrowsPolynomially fun x => ‖deriv q x‖<VAR>i : α<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>hb_lt_one : b' < 1<VAR>hb : b' ∈ Set.Ioo 0 1<VAR>hb' : ∀ (i : α), b' ≤ b i<VAR>c₁ : ℝ<VAR>left✝¹ : c₁ > 0<VAR>c₂ : ℝ<VAR>left✝ : c₂ > 0<VAR>hq_poly : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b' * x) x, (fun x => ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x => ‖deriv q x‖) x) (c₂ * (fun x => ‖deriv q x‖) x)<GOAL>∃ c, ∀ᶠ (x : ℕ) in atTop, ‖q ↑(r i x) - q (b i * ↑x)‖ ≤ c * ‖deriv q ↑x * (↑(r i x) - b i * ↑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>q : ℝ → ℝ<VAR>hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>hq_poly✝ : GrowsPolynomially fun x => ‖deriv q x‖<VAR>i : α<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>hb_lt_one : b' < 1<VAR>hb : b' ∈ Set.Ioo 0 1<VAR>hb' : ∀ (i : α), b' ≤ b i<VAR>c₁ : ℝ<VAR>left✝¹ : c₁ > 0<VAR>c₂ : ℝ<VAR>left✝ : c₂ > 0<VAR>hq_poly : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b' * x) x, (fun x => ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x => ‖deriv q x‖) x) (c₂ * (fun x => ‖deriv q x‖) x)<GOAL>∀ᶠ (x : ℕ) in atTop, ‖q ↑(r i x) - q (b i * ↑x)‖ ≤ c₂ * ‖deriv q ↑x * (↑(r i x) - b i * ↑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>q : ℝ → ℝ<VAR>hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>hq_poly✝ : GrowsPolynomially fun x => ‖deriv q x‖<VAR>i : α<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>hb_lt_one : b' < 1<VAR>hb : b' ∈ Set.Ioo 0 1<VAR>hb' : ∀ (i : α), b' ≤ b i<VAR>c₁ : ℝ<VAR>left✝¹ : c₁ > 0<VAR>c₂ : ℝ<VAR>left✝ : c₂ > 0<VAR>hq_poly : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b' * x) x, (fun x => ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x => ‖deriv q x‖) x) (c₂ * (fun x => ‖deriv q x‖) x)<VAR>h_tendsto : Tendsto (fun x => b' * x) atTop atTop<GOAL>∀ᶠ (x : ℕ) in atTop, ‖q ↑(r i x) - q (b i * ↑x)‖ ≤ c₂ * ‖deriv q ↑x * (↑(r i x) - b i * ↑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>q : ℝ → ℝ<VAR>hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>hq_poly✝ : GrowsPolynomially fun x => ‖deriv q x‖<VAR>i : α<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>hb_lt_one : b' < 1<VAR>hb : b' ∈ Set.Ioo 0 1<VAR>hb' : ∀ (i : α), b' ≤ b i<VAR>c₁ : ℝ<VAR>left✝¹ : c₁ > 0<VAR>c₂ : ℝ<VAR>left✝ : c₂ > 0<VAR>hq_poly : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b' * x) x, (fun x => ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x => ‖deriv q x‖) x) (c₂ * (fun x => ‖deriv q x‖) x)<VAR>h_tendsto : Tendsto (fun x => b' * x) atTop atTop<VAR>n : ℕ<VAR>hn : ∀ u ∈ Set.Icc (b' * ↑n) ↑n, ‖deriv q u‖ ∈ Set.Icc (c₁ * ‖deriv q ↑n‖) (c₂ * ‖deriv q ↑n‖)<VAR>h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)<VAR>h_ge_n₀ : R.n₀ ≤ n<VAR>h_n_pos : 0 < n<VAR>h_bn : 1 < b' * ↑n<GOAL>‖q ↑(r i n) - q (b i * ↑n)‖ ≤ c₂ * ‖deriv q ↑n * (↑(r i n) - b i * ↑n)‖
<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>q : ℝ → ℝ<VAR>hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>hq_poly✝ : GrowsPolynomially fun x => ‖deriv q x‖<VAR>i : α<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>hb_lt_one : b' < 1<VAR>hb : b' ∈ Set.Ioo 0 1<VAR>hb' : ∀ (i : α), b' ≤ b i<VAR>c₁ : ℝ<VAR>left✝¹ : c₁ > 0<VAR>c₂ : ℝ<VAR>left✝ : c₂ > 0<VAR>hq_poly : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b' * x) x, (fun x => ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x => ‖deriv q x‖) x) (c₂ * (fun x => ‖deriv q x‖) x)<VAR>h_tendsto : Tendsto (fun x => b' * x) atTop atTop<VAR>n : ℕ<VAR>hn : ∀ u ∈ Set.Icc (b' * ↑n) ↑n, ‖deriv q u‖ ∈ Set.Icc (c₁ * ‖deriv q ↑n‖) (c₂ * ‖deriv q ↑n‖)<VAR>h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)<VAR>h_ge_n₀ : R.n₀ ≤ n<VAR>h_n_pos : 0 < n<VAR>h_bn : 1 < b' * ↑n<GOAL>‖q ↑(r i n) - q (b i * ↑n)‖ ≤ c₂ * ‖deriv q ↑n‖ * ‖↑(r i n) - b i * ↑n‖
<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>q : ℝ → ℝ<VAR>hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>hq_poly✝ : GrowsPolynomially fun x => ‖deriv q x‖<VAR>i : α<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>hb_lt_one : b' < 1<VAR>hb : b' ∈ Set.Ioo 0 1<VAR>hb' : ∀ (i : α), b' ≤ b i<VAR>c₁ : ℝ<VAR>left✝¹ : c₁ > 0<VAR>c₂ : ℝ<VAR>left✝ : c₂ > 0<VAR>hq_poly : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b' * x) x, (fun x => ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x => ‖deriv q x‖) x) (c₂ * (fun x => ‖deriv q x‖) x)<VAR>h_tendsto : Tendsto (fun x => b' * x) atTop atTop<VAR>n : ℕ<VAR>hn : ∀ u ∈ Set.Icc (b' * ↑n) ↑n, ‖deriv q u‖ ∈ Set.Icc (c₁ * ‖deriv q ↑n‖) (c₂ * ‖deriv q ↑n‖)<VAR>h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)<VAR>h_ge_n₀ : R.n₀ ≤ n<VAR>h_n_pos : 0 < n<VAR>h_bn : 1 < b' * ↑n<VAR>z : ℝ<VAR>hz : z ∈ Set.Icc (b' * ↑n) ↑n<GOAL>DifferentiableAt ℝ q z