ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrableOn f s μ<VAR>u : ↑s → Set X<VAR>u_open : ∀ (x : ↑s), IsOpen (u x)<VAR>xu : ∀ (x : ↑s), ↑x ∈ u x<VAR>hu : ∀ (x : ↑s), IntegrableOn f (u x ∩ s) μ<GOAL>∃ T, T.Countable ∧ (∀ u ∈ T, IsOpen u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrableOn f s μ<VAR>u : ↑s → Set X<VAR>u_open : ∀ (x : ↑s), IsOpen (u x)<VAR>xu : ∀ (x : ↑s), ↑x ∈ u x<VAR>hu : ∀ (x : ↑s), IntegrableOn f (u x ∩ s) μ<VAR>T : Set ↑s<VAR>T_count : T.Countable<VAR>hT : s ⊆ ⋃ i ∈ T, u i<GOAL>∃ T, T.Countable ∧ (∀ u ∈ T, IsOpen u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrableOn f s μ<VAR>u : ↑s → Set X<VAR>u_open : ∀ (x : ↑s), IsOpen (u x)<VAR>xu : ∀ (x : ↑s), ↑x ∈ u x<VAR>hu : ∀ (x : ↑s), IntegrableOn f (u x ∩ s) μ<VAR>T : Set ↑s<VAR>T_count : T.Countable<VAR>hT : s ⊆ ⋃ i ∈ T, u i<GOAL>∀ u_1 ∈ u '' T, IsOpen u_1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrableOn f s μ<VAR>u : ↑s → Set X<VAR>u_open : ∀ (x : ↑s), IsOpen (u x)<VAR>xu : ∀ (x : ↑s), ↑x ∈ u x<VAR>hu : ∀ (x : ↑s), IntegrableOn f (u x ∩ s) μ<VAR>T : Set ↑s<VAR>T_count : T.Countable<VAR>hT : s ⊆ ⋃ i ∈ T, u i<GOAL>∀ u_1 ∈ u '' T, IntegrableOn f (u_1 ∩ s) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : Ordinal.{u_4} → Ordinal.{u_5}<VAR>o : Ordinal.{u_5}<VAR>H : IsNormal f<VAR>p : Set α<VAR>p0 : p.Nonempty<VAR>g : α → Ordinal.{u_4}<VAR>b : Ordinal.{u_4}<VAR>H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, g a ≤ o<GOAL>f b ≤ o ↔ ∀ a ∈ p, f (g a) ≤ o
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Finite α<VAR>p q : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>e : { x // p x } ≃ { x // q x }<VAR>x : α<VAR>hx : ¬p x<GOAL>(e.subtypeCongr e.toCompl) x = ↑(e.toCompl ⟨x, hx⟩)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Finite α<VAR>p q : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>e : { x // p x } ≃ { x // q x }<VAR>x : α<VAR>hx : ¬p x<GOAL>(sumCompl q) (Sum.map (⇑e) (⇑e.toCompl) ((sumCompl p).symm x)) = ↑(e.toCompl ⟨x, hx⟩)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<GOAL>(hf.stieltjesFunction a).measure univ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<GOAL>(hf.stieltjesFunction a).measure univ = ENNReal.ofReal (1 - 0)
<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 : ℚ<GOAL>↑n = 0 ↔ n = 0
<VAR>n : ℕ<GOAL>map Prod.swap (antidiagonal n) = antidiagonal n
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : DivisionRing 𝕜<VAR>inst✝³ : HasKernels C<VAR>inst✝² : Linear 𝕜 C<VAR>X Y : C<VAR>inst✝¹ : Simple X<VAR>inst✝ : Simple Y<VAR>h : (X ≅ Y) → False<VAR>f : X ⟶ Y<GOAL>f = 0
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : DivisionRing 𝕜<VAR>inst✝³ : HasKernels C<VAR>inst✝² : Linear 𝕜 C<VAR>X Y : C<VAR>inst✝¹ : Simple X<VAR>inst✝ : Simple Y<VAR>h : (X ≅ Y) → False<VAR>f : X ⟶ Y<VAR>p : ¬IsIso f ↔ ¬f ≠ 0<GOAL>f = 0
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : DivisionRing 𝕜<VAR>inst✝³ : HasKernels C<VAR>inst✝² : Linear 𝕜 C<VAR>X Y : C<VAR>inst✝¹ : Simple X<VAR>inst✝ : Simple Y<VAR>h : (X ≅ Y) → False<VAR>f : X ⟶ Y<VAR>p : ¬IsIso f ↔ f = 0<GOAL>f = 0
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<GOAL>volume = StieltjesFunction.id.measure
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>this : StieltjesFunction.id.measure.IsAddLeftInvariant<GOAL>volume = StieltjesFunction.id.measure
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>this : StieltjesFunction.id.measure.IsAddLeftInvariant<VAR>A : StieltjesFunction.id.measure ↑(stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped = 1<GOAL>volume = StieltjesFunction.id.measure
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>this : StieltjesFunction.id.measure.IsAddLeftInvariant<VAR>A : StieltjesFunction.id.measure ↑(stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped = 1<GOAL>volume = 1 • addHaarMeasure (stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Nontrivial M<VAR>f : End R M<VAR>hf : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<GOAL>∃ μ, f.HasEigenvalue μ
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Nontrivial M<VAR>f : End R M<VAR>hf : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<VAR>contra : ∀ (μ : R), ¬f.HasEigenvalue μ<GOAL>False
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Nontrivial M<VAR>f : End R M<VAR>hf : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<VAR>contra : ∀ (μ : R), ¬f.HasEigenvalue μ<VAR>μ : R<GOAL>⨆ k, (f.genEigenspace μ) k = ⊥
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Nontrivial M<VAR>f : End R M<VAR>hf : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<VAR>μ : R<VAR>contra : ∀ (k : ℕ), (f.genEigenspace μ) k = ⊥<GOAL>⨆ k, (f.genEigenspace μ) k = ⊥
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>m n : ℕ<VAR>h : m ≤ n<VAR>x : ℤ_[p]<GOAL>((toZModPow n) x).cast = (toZModPow m) x
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>m n : ℕ<VAR>h : m ≤ n<VAR>x : ℤ_[p]<GOAL>((toZModPow n) x).cast = ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) x
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Balanced<VAR>hr : r.Balanced<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'<GOAL>(l.balanceR x r).size = l.size + r.size + 1
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>inst✝ : DivisionRing K<VAR>n_le_m : n ≤ m<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.dens m = g.dens 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<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * g ↑n ≤ sumTransform (p a b) g (r i n) 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>c₁ : ℝ<VAR>hc₁_mem : c₁ ∈ Set.Ioo 0 1<VAR>hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * g ↑n ≤ sumTransform (p a b) g (r i n) 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>c₁ : ℝ<VAR>hc₁_mem : c₁ ∈ Set.Ioo 0 1<VAR>hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * g ↑n ≤ sumTransform (p a b) g (r i n) 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>c₁ : ℝ<VAR>hc₁_mem : c₁ ∈ Set.Ioo 0 1<VAR>hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u<VAR>c₃ : ℝ<VAR>hc₃_mem : c₃ ∈ Set.Ioo 0 1<VAR>hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * g ↑n ≤ sumTransform (p a b) g (r i n) 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>c₁ : ℝ<VAR>hc₁_mem : c₁ ∈ Set.Ioo 0 1<VAR>hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u<VAR>c₃ : ℝ<VAR>hc₃_mem : c₃ ∈ Set.Ioo 0 1<VAR>hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n<VAR>hc₁_pos : 0 < c₁<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * g ↑n ≤ sumTransform (p a b) g (r i n) 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>c₁ : ℝ<VAR>hc₁_mem : c₁ ∈ Set.Ioo 0 1<VAR>hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u<VAR>c₃ : ℝ<VAR>hc₃_mem : c₃ ∈ Set.Ioo 0 1<VAR>hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n<VAR>hc₁_pos : 0 < c₁<VAR>hc₃' : 0 < 1 - c₃<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * g ↑n ≤ sumTransform (p a b) g (r i n) 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>c₁ : ℝ<VAR>hc₁_mem : c₁ ∈ Set.Ioo 0 1<VAR>hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u<VAR>c₃ : ℝ<VAR>hc₃_mem : c₃ ∈ Set.Ioo 0 1<VAR>hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n<VAR>hc₁_pos : 0 < c₁<VAR>hc₃' : 0 < 1 - c₃<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g ↑n ≤ sumTransform (p a b) g (r i n) 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>c₁ : ℝ<VAR>hc₁_mem : c₁ ∈ Set.Ioo 0 1<VAR>hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u<VAR>c₃ : ℝ<VAR>hc₃_mem : c₃ ∈ Set.Ioo 0 1<VAR>hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n<VAR>hc₁_pos : 0 < c₁<VAR>hc₃' : 0 < 1 - c₃<VAR>n : ℕ<VAR>hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u<VAR>hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n<VAR>hrpos : ∀ (i : α), 0 < r i n<VAR>hr_lt_n : ∀ (i : α), r i n < n<VAR>hn_pos : 0 < n<GOAL>∀ (i : α), min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g ↑n ≤ sumTransform (p a b) g (r i n) 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>c₁ : ℝ<VAR>hc₁_mem : c₁ ∈ Set.Ioo 0 1<VAR>hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u<VAR>c₃ : ℝ<VAR>hc₃_mem : c₃ ∈ Set.Ioo 0 1<VAR>hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n<VAR>hc₁_pos : 0 < c₁<VAR>hc₃' : 0 < 1 - c₃<VAR>n : ℕ<VAR>hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u<VAR>hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n<VAR>hrpos : ∀ (i : α), 0 < r i n<VAR>hr_lt_n : ∀ (i : α), r i n < n<VAR>hn_pos : 0 < n<VAR>i : α<VAR>hrpos_i : 0 < r i n<GOAL>min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g ↑n ≤ sumTransform (p a b) g (r i n) 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>c₁ : ℝ<VAR>hc₁_mem : c₁ ∈ Set.Ioo 0 1<VAR>hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u<VAR>c₃ : ℝ<VAR>hc₃_mem : c₃ ∈ Set.Ioo 0 1<VAR>hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n<VAR>hc₁_pos : 0 < c₁<VAR>hc₃' : 0 < 1 - c₃<VAR>n : ℕ<VAR>hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u<VAR>hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n<VAR>hrpos : ∀ (i : α), 0 < r i n<VAR>hr_lt_n : ∀ (i : α), r i n < n<VAR>hn_pos : 0 < n<VAR>i : α<VAR>hrpos_i : 0 < r i n<VAR>g_nonneg : 0 ≤ g ↑n<GOAL>min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g ↑n ≤ sumTransform (p a b) g (r i n) n
<VAR>α : Type u_1<VAR>f : α → ℝ≥0<VAR>a : ℝ≥0<GOAL>↑(∑' (x : α), f x * a) = ↑((∑' (x : α), f x) * a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>h : ∀ x ∈ s, s ∈ 𝓝[>] x<VAR>M : α → α<VAR>hM : ∀ x ∈ s, x < M x<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>h : ∀ x ∈ s, s ∈ 𝓝[>] x<VAR>M : α → α<VAR>hM : ∀ x ∈ s, x < M x<GOAL>(s \ interior s).Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>h : ∀ x ∈ s, s ∈ 𝓝[>] x<VAR>M : α → α<VAR>hM : ∀ x ∈ s, x < M x<VAR>A : ∀ x ∈ s, ∃ y ∈ Ioi x, Ioo x y ⊆ s<GOAL>(s \ interior s).Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>h : ∀ x ∈ s, s ∈ 𝓝[>] x<VAR>M : α → α<VAR>hM : ∀ x ∈ s, x < M x<VAR>y : α → α<VAR>hy : ∀ x ∈ s, y x ∈ Ioi x<VAR>h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s<VAR>B : (s \ interior s).PairwiseDisjoint fun x => Ioo x (y x)<GOAL>(s \ interior s).Countable
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>x y : α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : SemilatticeSup β<VAR>hf : MonotoneOn f s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>f (x ⊔ y) = f x ⊔ f y
<VAR>s : ℂ<GOAL>DifferentiableAt ℂ (fun s => (Gamma s)⁻¹) s
<VAR>s : ℂ<VAR>n : ℕ<VAR>hs : -s.re < ↑n<GOAL>DifferentiableAt ℂ (fun s => (Gamma s)⁻¹) s
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p n : ℕ<VAR>inst✝ : ExpChar R p<VAR>f : R[X]<GOAL>Multiset.map (⇑(frobenius R p)) ((expand R p) f).roots ≤ p • f.roots
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p n : ℕ<VAR>inst✝ : ExpChar R p<VAR>f : R[X]<GOAL>Multiset.map (⇑(iterateFrobenius R p 1)) ((expand R p) f).roots ≤ p • f.roots
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type w<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : Ring S<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module.Free R M<VAR>inst✝⁷ : Module.Finite R M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Module S N<VAR>inst✝³ : SMulCommClass R S N<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : StrongRankCondition S<VAR>inst✝ : Module.Free S N<GOAL>Module.rank S (M →ₗ[R] N) = lift.{w, v} (Module.rank R M) * lift.{v, w} (Module.rank S N)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : CliffordAlgebra Q<VAR>a b : M<VAR>h : QuadraticMap.IsOrtho Q a b<GOAL>x * (ι Q) a * (ι Q) b = -(x * (ι Q) b * (ι Q) a)
<VAR>n k : ℕ<GOAL>(n + 1).ascFactorial k = k ! * (n + k).choose k
<VAR>n k : ℕ<GOAL>(n + 1).ascFactorial k = (n + k).choose k * k !
<VAR>n k : ℕ<GOAL>(n + 1).ascFactorial k * (n + k - k)! = (n + k).choose k * k ! * (n + k - k)!
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : BiheytingAlgebra α<VAR>inst✝² : BiheytingAlgebra β<VAR>inst✝¹ : BiheytingAlgebra γ<VAR>inst✝ : BiheytingAlgebra δ<VAR>f f₁ f₂ : BiheytingHom α β<VAR>g g₁ g₂ : BiheytingHom β γ<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n✝ : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁴ : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq n✝<VAR>inst✝ : Fintype n✝<VAR>n : ℕ<VAR>p : Fin n → R[X]<VAR>h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i<VAR>x✝ j : Fin n<VAR>h : id j < id x✝<GOAL>of (fun i j => (p j).coeff ↑i) x✝ j = 0
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμν : μ univ = ν univ<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)<GOAL>μ = ν
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a✝ b✝ x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμν : μ univ = ν univ<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)<VAR>a b : αᵒᵈ<VAR>hab : a < b<GOAL>μ (Ico a b) = ν (Ico a b)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a✝ b✝ x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμν : μ univ = ν univ<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)<VAR>a b : αᵒᵈ<VAR>hab : a < b<GOAL>μ (⇑OrderDual.ofDual ⁻¹' Ioc b a) = ν (⇑OrderDual.ofDual ⁻¹' Ioc b a)
<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>inst✝ : DecidableEq ι<VAR>i j : ι<GOAL>b.toMatrix (⇑b) i j = 1 i j
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>‖↑n‖ = ↑n
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>s : Multiset α<VAR>t : Multiset γ<VAR>f : γ → β<GOAL>Rel r s (map f t) ↔ Rel (fun a b => r a (f b)) s t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>s : Multiset α<VAR>t : Multiset γ<VAR>f : γ → β<GOAL>Rel (flip fun a b => flip r (f a) b) s t ↔ Rel (fun a b => r a (f b)) s t
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>proj : Z → B<VAR>e✝ : Pretrivialization F proj<VAR>x : Z<VAR>e e' : Pretrivialization F proj<GOAL>(e.symm.trans e'.toPartialEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ univ
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>R X✝ Y✝ Z✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>a b : R ⟶ X✝<VAR>X Y Z A : C<VAR>g : Y ⟶ Z<VAR>a₁ a₂ : A ⟶ Y<VAR>h : IsKernelPair g a₁ a₂<VAR>f : X ⟶ Z<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPullback f (a₁ ≫ g)<GOAL>IsKernelPair (pullback.fst f g) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>R X✝ Y✝ Z✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>a b : R ⟶ X✝<VAR>X Y Z A : C<VAR>g : Y ⟶ Z<VAR>a₁ a₂ : A ⟶ Y<VAR>h : IsKernelPair g a₁ a₂<VAR>f : X ⟶ Z<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPullback f (a₁ ≫ g)<VAR>s : PullbackCone (pullback.fst f g) (pullback.fst f g)<GOAL>(s.fst ≫ pullback.snd f g) ≫ g = (s.snd ≫ pullback.snd f g) ≫ g
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>R X✝ Y✝ Z✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>a b : R ⟶ X✝<VAR>X Y Z A : C<VAR>g : Y ⟶ Z<VAR>a₁ a₂ : A ⟶ Y<VAR>h : IsKernelPair g a₁ a₂<VAR>f : X ⟶ Z<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPullback f (a₁ ≫ g)<VAR>s : PullbackCone (pullback.fst f g) (pullback.fst f g)<GOAL>(s.fst ≫ pullback.fst f g) ≫ f = h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ?refine_1 ≫ a₁ ≫ g
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>R X✝ Y✝ Z✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>a b : R ⟶ X✝<VAR>X Y Z A : C<VAR>g : Y ⟶ Z<VAR>a₁ a₂ : A ⟶ Y<VAR>h : IsKernelPair g a₁ a₂<VAR>f : X ⟶ Z<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPullback f (a₁ ≫ g)<VAR>s : PullbackCone (pullback.fst f g) (pullback.fst f g)<GOAL>(fun s => pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯) s ≫ (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).fst = s.fst