ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>φ : ℕ → Set α<VAR>hφ : AECover μ atTop φ<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<GOAL>Tendsto (fun x => ∫⁻ (x : α) in φ x, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>φ : ℕ → Set α<VAR>hφ : AECover μ atTop φ<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>lim₁ : Tendsto (fun i => ∫⁻ (x : α) in ⋂ k ∈ Ici i, φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))<GOAL>Tendsto (fun x => ∫⁻ (x : α) in φ x, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>φ : ℕ → Set α<VAR>hφ : AECover μ atTop φ<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>lim₁ : Tendsto (fun i => ∫⁻ (x : α) in ⋂ k ∈ Ici i, φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))<VAR>lim₂ : Tendsto (fun i => ∫⁻ (x : α) in ⋃ k ∈ Iic i, φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))<GOAL>Tendsto (fun x => ∫⁻ (x : α) in φ x, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>φ : ℕ → Set α<VAR>hφ : AECover μ atTop φ<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>lim₁ : Tendsto (fun i => ∫⁻ (x : α) in ⋂ k ∈ Ici i, φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))<VAR>lim₂ : Tendsto (fun i => ∫⁻ (x : α) in ⋃ k ∈ Iic i, φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))<VAR>n : ℕ<GOAL>∫⁻ (x : α) in ⋂ k ∈ Ici n, φ k, f x ∂μ ≤ ∫⁻ (x : α) in φ n, f x ∂μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>φ : ℕ → Set α<VAR>hφ : AECover μ atTop φ<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>lim₁ : Tendsto (fun i => ∫⁻ (x : α) in ⋂ k ∈ Ici i, φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))<VAR>lim₂ : Tendsto (fun i => ∫⁻ (x : α) in ⋃ k ∈ Iic i, φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))<VAR>n : ℕ<GOAL>∫⁻ (x : α) in φ n, f x ∂μ ≤ ∫⁻ (x : α) in ⋃ k ∈ Iic n, φ k, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f f₁ f₂ : Filter α<VAR>h✝ h₁ h₂ g : Set α → Set β<VAR>h : Set β → Filter γ<VAR>hg : Monotone g<VAR>hh : Monotone h<GOAL>(f.lift fun s => (𝓟 (g s)).lift h) = f.lift fun s => h (g s)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a : ℝ<VAR>h : 0 < a<GOAL>ContinuousAt (fun p => p.1 * p.2) (⊤, ↑a)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a : ℝ<VAR>h : 0 < a<GOAL>∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ↑a), ↑x < a.1 * a.2
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a : ℝ<VAR>h : 0 < a<VAR>x : ℝ<GOAL>∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ↑a), ↑x < a.1 * a.2
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a : ℝ<VAR>h : 0 < a<VAR>x : ℝ<GOAL>∃ t, (∀ y ∈ t, ↑x < y.1 * y.2) ∧ IsOpen t ∧ (⊤, ↑a) ∈ t
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a : ℝ<VAR>h : 0 < a<VAR>x : ℝ<GOAL>(∀ y ∈ Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2), ↑x < y.1 * y.2) ∧ IsOpen (Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2)) ∧ (⊤, ↑a) ∈ Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2)
<VAR>x : ℂ<VAR>h : cos x = 0<GOAL>deriv tan x = 1 / cos x ^ 2
<VAR>x : ℂ<VAR>h : cos x = 0<VAR>this : ¬DifferentiableAt ℂ tan x<GOAL>deriv tan x = 1 / cos x ^ 2
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i✝ i : ι<VAR>b : β i<GOAL>(single i b) i = b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoMod hp a (b - p) = toIcoMod hp a b
<VAR>u v m n : ℤ<GOAL>Even (m - n) ↔ (Even m ↔ Even n)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<GOAL>f.eraseLead.coeff f.natDegree = 0
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>a : R<VAR>s : Set R<VAR>h : ∀ a ∈ s, star a ∈ s<VAR>ha : a ∈ s.centralizer<VAR>y : R<VAR>hy : y ∈ s<GOAL>y * star a = star a * y
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<VAR>x : ℝ<GOAL>(f ^ (n + 1)) x = (⇑f)^[n + 1] x
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>inst✝ : HasGroupoid M G<VAR>s✝ s : Opens M<VAR>hs : Nonempty ↥s<VAR>e : PartialHomeomorph (↥s) H<VAR>xset : Set (PartialHomeomorph (↥s) H)<VAR>he : e ∈ xset<VAR>x : ↥s<VAR>hx : (fun x => {(chartAt H ↑x).subtypeRestr ⋯}) x = xset<GOAL>∃ x, e = (chartAt H ↑x).subtypeRestr hs
<VAR>ι : Sort u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝² : PartialOrder α✝<VAR>α : Type u_4<VAR>a b : α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : IsStronglyAtomic α<VAR>s : Set α<VAR>h : s.OrdConnected<VAR>c : α<VAR>hc : c ∈ s<VAR>d : α<VAR>hd : d ∈ s<VAR>hcd : ⟨c, hc⟩ < ⟨d, hd⟩<GOAL>∃ x, ⟨c, hc⟩ ⋖ x ∧ x ≤ ⟨d, hd⟩
<VAR>ι : Sort u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝² : PartialOrder α✝<VAR>α : Type u_4<VAR>a b : α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : IsStronglyAtomic α<VAR>s : Set α<VAR>h : s.OrdConnected<VAR>c : α<VAR>hc : c ∈ s<VAR>d : α<VAR>hd : d ∈ s<VAR>hcd : ⟨c, hc⟩ < ⟨d, hd⟩<VAR>x : α<VAR>hcx : c ⋖ x<VAR>hxd : x ≤ d<GOAL>∃ x, ⟨c, hc⟩ ⋖ x ∧ x ≤ ⟨d, hd⟩
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>inst✝³ : DivisionSemiring α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSemiring α<VAR>f g : ι → α<VAR>a a₁ a₂ : α<VAR>inst✝ : T2Space α<VAR>hf : ¬Summable f<VAR>ha : ¬a = 0<GOAL>∑' (x : ι), a * f x = a * ∑' (x : ι), f x
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>W X X' : D<VAR>Y : C<VAR>f : W ⟶ X<VAR>g : X ⟶ G.obj Y<VAR>f' : W ⟶ X'<VAR>g' : X' ⟶ G.obj Y<GOAL>f ≫ g ≫ α.inv.app Y = f' ≫ g' ≫ α.inv.app Y ↔ f ≫ g = f' ≫ g'
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>this✝ : DecidableEq ι := Classical.decEq ι<VAR>this : (i : ι) → DecidableEq (G i) := fun i => Classical.decEq (G i)<GOAL>Injective prod
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra A B<VAR>inst✝⁵ : IsCyclotomicExtension {n} A B<VAR>inst✝⁴ : Field K<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>(IsPrimitiveRoot.powerBasis K hζ).gen ∈ adjoin K {ζ - 1}
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra A B<VAR>inst✝⁵ : IsCyclotomicExtension {n} A B<VAR>inst✝⁴ : Field K<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>∃ x, (aeval (ζ - 1)) x = ζ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : LocallyCompactSpace α<GOAL>TendstoLocallyUniformly F f p ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn F f p K
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : 𝕎 R<VAR>n : ℕ<GOAL>init n (x - y) = init n (init n x - init n y)
<VAR>p : ℝ<VAR>hp : 0 < p<GOAL>∫ (x : ℝ) in Ioi 0, rexp (-x ^ p) = Gamma (1 / p + 1)
<VAR>p : ℝ<VAR>hp : 0 < p<GOAL>∫ (x : ℝ) in Ioi 0, rexp (-x ^ p) = ∫ (x : ℝ) in Ioi 0, x ^ 0 * rexp (-x ^ p)
<VAR>p : ℝ<VAR>hp : 0 < p<GOAL>Gamma (1 / p + 1) = 1 / p * Gamma ((0 + 1) / p)
<VAR>I : Type u<VAR>inst✝¹⁰ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝⁹ : Category.{u_2, u_1} C<VAR>inst✝⁸ : MonoidalCategory C<VAR>Z : C<VAR>X₁ X₂ X₃ : GradedObject I C<VAR>inst✝⁷ : X₁.HasTensor X₂<VAR>inst✝⁶ : X₂.HasTensor X₃<VAR>inst✝⁵ : (tensorObj X₁ X₂).HasTensor X₃<VAR>inst✝⁴ : X₁.HasTensor (tensorObj X₂ X₃)<VAR>Y₁ Y₂ Y₃ : GradedObject I C<VAR>inst✝³ : Y₁.HasTensor Y₂<VAR>inst✝² : Y₂.HasTensor Y₃<VAR>inst✝¹ : (tensorObj Y₁ Y₂).HasTensor Y₃<VAR>inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)<VAR>j : I<VAR>A : C<VAR>f g : tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A<VAR>H : X₁.HasGoodTensorTensor₂₃ X₂ X₃<VAR>h : ∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j), ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f = ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ g<GOAL>f = g
<VAR>I : Type u<VAR>inst✝¹⁰ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝⁹ : Category.{u_2, u_1} C<VAR>inst✝⁸ : MonoidalCategory C<VAR>Z : C<VAR>X₁ X₂ X₃ : GradedObject I C<VAR>inst✝⁷ : X₁.HasTensor X₂<VAR>inst✝⁶ : X₂.HasTensor X₃<VAR>inst✝⁵ : (tensorObj X₁ X₂).HasTensor X₃<VAR>inst✝⁴ : X₁.HasTensor (tensorObj X₂ X₃)<VAR>Y₁ Y₂ Y₃ : GradedObject I C<VAR>inst✝³ : Y₁.HasTensor Y₂<VAR>inst✝² : Y₂.HasTensor Y₃<VAR>inst✝¹ : (tensorObj Y₁ Y₂).HasTensor Y₃<VAR>inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)<VAR>j : I<VAR>A : C<VAR>f g : tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A<VAR>H : X₁.HasGoodTensorTensor₂₃ X₂ X₃<VAR>h : ∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j), ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f = ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ g<GOAL>∀ (i₁ i₂ i₃ : I) (h : r₁₂₃ (i₁, i₂, i₃) = j), ιMapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = ιMapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Lattice β<VAR>inst✝ : Lattice γ<VAR>L✝ M✝ : Sublattice α<VAR>f✝ : LatticeHom α β<VAR>s t : Set α<VAR>a : α<VAR>L M : Sublattice α<VAR>f : LatticeHom α β<VAR>hf : Injective ⇑f<GOAL>map f (L ⊓ M) = map f L ⊓ map f M
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Lattice β<VAR>inst✝ : Lattice γ<VAR>L✝ M✝ : Sublattice α<VAR>f✝ : LatticeHom α β<VAR>s t : Set α<VAR>a : α<VAR>L M : Sublattice α<VAR>f : LatticeHom α β<VAR>hf : Injective ⇑f<GOAL>↑(map f (L ⊓ M)) = ↑(map f L ⊓ map f M)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>β : Type u_5<VAR>inst✝ : CommMonoid β<VAR>u a b : β<VAR>hu : IsUnit u<GOAL>u * a ~ᵤ b ↔ a ~ᵤ b
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>β : Type u_5<VAR>inst✝ : CommMonoid β<VAR>u a b : β<VAR>hu : IsUnit u<GOAL>a * u ~ᵤ b ↔ a ~ᵤ b
<VAR>x : ℝ<VAR>hx : Liouville x<VAR>n : ℕ<GOAL>∃ᶠ (b : ℕ) in atTop, ∃ a, x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n
<VAR>x : ℝ<VAR>hx : Liouville x<VAR>n : ℕ<VAR>H : ¬∃ᶠ (b : ℕ) in atTop, ∃ a, x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n<GOAL>False
<VAR>x : ℝ<VAR>hx : Liouville x<VAR>n : ℕ<VAR>H : ∃ a, ∀ b ≥ a, ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|<GOAL>False
<VAR>x : ℝ<VAR>hx : Liouville x<VAR>n N : ℕ<VAR>hN : ∀ b ≥ N, ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|<GOAL>False
<VAR>x : ℝ<VAR>hx : Liouville x<VAR>n N : ℕ<VAR>hN : ∀ b ≥ N, ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|<VAR>this : ∀ b > 1, ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<GOAL>False
<VAR>x : ℝ<VAR>hx : Liouville x<VAR>n N : ℕ<VAR>hN : ∀ b ≥ N, ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|<VAR>this✝ : ∀ b > 1, ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>this : ∀ᶠ (m : ℕ) in atTop, ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<GOAL>False
<VAR>x : ℝ<VAR>hx : Liouville x<VAR>n N : ℕ<VAR>hN : ∀ b ≥ N, ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|<VAR>this✝ : ∀ b > 1, ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>this : ∀ᶠ (m : ℕ) in atTop, ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>m : ℕ<VAR>hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>hnm : n ≤ m<GOAL>False
<VAR>x : ℝ<VAR>hx : Liouville x<VAR>n N : ℕ<VAR>hN : ∀ b ≥ N, ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|<VAR>this✝ : ∀ b > 1, ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>this : ∀ᶠ (m : ℕ) in atTop, ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>m : ℕ<VAR>hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>hnm : n ≤ m<VAR>a b : ℤ<VAR>hb : 1 < b<VAR>hne : x ≠ ↑a / ↑b<VAR>hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m<GOAL>False
<VAR>x : ℝ<VAR>hx : Liouville x<VAR>n N : ℕ<VAR>hN : ∀ b ≥ N, ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|<VAR>this✝ : ∀ b > 1, ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>this : ∀ᶠ (m : ℕ) in atTop, ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>m : ℕ<VAR>hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>hnm : n ≤ m<VAR>a : ℤ<VAR>b : ℕ<VAR>hb : 1 < ↑b<VAR>hne : x ≠ ↑a / ↑↑b<VAR>hlt : |x - ↑a / ↑↑b| < 1 / ↑↑b ^ m<GOAL>False
<VAR>x : ℝ<VAR>hx : Liouville x<VAR>n N : ℕ<VAR>hN : ∀ b ≥ N, ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|<VAR>this✝ : ∀ b > 1, ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>this : ∀ᶠ (m : ℕ) in atTop, ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>m : ℕ<VAR>hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>hnm : n ≤ m<VAR>a : ℤ<VAR>b : ℕ<VAR>hb : 1 < b<VAR>hne : x ≠ ↑a / ↑b<VAR>hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m<GOAL>False
<VAR>x : ℝ<VAR>hx : Liouville x<VAR>n N : ℕ<VAR>hN : ∀ b ≥ N, ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|<VAR>this✝ : ∀ b > 1, ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>this : ∀ᶠ (m : ℕ) in atTop, ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>m : ℕ<VAR>hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>hnm : n ≤ m<VAR>a : ℤ<VAR>b : ℕ<VAR>hb : 1 < b<VAR>hne : x ≠ ↑a / ↑b<VAR>hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m<VAR>h : N ≤ b<GOAL>False
<VAR>x : ℝ<VAR>hx : Liouville x<VAR>n N : ℕ<VAR>hN : ∀ b ≥ N, ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|<VAR>this✝ : ∀ b > 1, ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>this : ∀ᶠ (m : ℕ) in atTop, ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>m : ℕ<VAR>hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|<VAR>hnm : n ≤ m<VAR>a : ℤ<VAR>b : ℕ<VAR>hb : 1 < b<VAR>hne : x ≠ ↑a / ↑b<VAR>hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m<VAR>h : b < N<GOAL>False
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝ : CommMonoid β<VAR>p : α → Prop<VAR>x✝ : DecidablePred p<VAR>h : ∀ i ∈ s, p i<VAR>f : (i : α) → p i → β<VAR>g : (i : α) → ¬p i → β<GOAL>(∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i : { x // x ∈ s }, f ↑i ⋯
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : CategoryWithHomology C<VAR>n a a' : ℤ<VAR>ha' : n + a = a'<VAR>K : CochainComplex C ℤ<GOAL>𝟙 (((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).obj K).homology a) ≫ 𝟙 ((shortComplexFunctor C (up ℤ) a).obj ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).obj K)).homology ≫ ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').hom.app K) ≫ 𝟙 (homology K a') = ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').hom.app K)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>x : (i : Fin (n + 1)) → α i<VAR>s : (i : Fin (n + 1)) → Finset (α i)<GOAL>x ∈ piFinset s ↔ x 0 ∈ s 0 ∧ tail x ∈ piFinset (tail s)
<VAR>l r : List Char<VAR>it : Iterator<VAR>h : ValidFor l r it<GOAL>it.curr = r.headD default
<VAR>l r : List Char<VAR>h : ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }<GOAL>{ s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }.curr = r.headD default
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hI' : ¬M.Basis I X<VAR>hJ : M.Basis J X<GOAL>∃ e ∈ J \ I, M.Indep (insert e I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hI' : ¬(M ↾ X).Base I<VAR>hJ : M.Basis J X<GOAL>∃ e ∈ J \ I, M.Indep (insert e I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hI' : ¬(M ↾ X).Base I<VAR>hJ : (M ↾ X).Base J<GOAL>∃ e ∈ J \ I, M.Indep (insert e I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e✝ : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hI' : ¬(M ↾ X).Base I<VAR>hJ : (M ↾ X).Base J<VAR>e : α<VAR>he : e ∈ J \ I<VAR>hi : (M ↾ X).Indep (insert e I)<GOAL>∃ e ∈ J \ I, M.Indep (insert e I)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), AnalyticSet (s n)<GOAL>AnalyticSet (⋃ n, s n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), AnalyticSet (s n)<VAR>β : ι → Type<VAR>hβ : (n : ι) → TopologicalSpace (β n)<VAR>h'β : ∀ (n : ι), PolishSpace (β n)<VAR>f : (n : ι) → β n → α<VAR>f_cont : ∀ (n : ι), Continuous (f n)<VAR>f_range : ∀ (n : ι), range (f n) = s n<GOAL>AnalyticSet (⋃ n, s n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), AnalyticSet (s n)<VAR>β : ι → Type<VAR>hβ : (n : ι) → TopologicalSpace (β n)<VAR>h'β : ∀ (n : ι), PolishSpace (β n)<VAR>f : (n : ι) → β n → α<VAR>f_cont : ∀ (n : ι), Continuous (f n)<VAR>f_range : ∀ (n : ι), range (f n) = s n<VAR>γ : Type u_2 := (n : ι) × β n<VAR>F : γ → α := fun x => match x with | ⟨n, x⟩ => f n x<GOAL>AnalyticSet (⋃ n, s n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), AnalyticSet (s n)<VAR>β : ι → Type<VAR>hβ : (n : ι) → TopologicalSpace (β n)<VAR>h'β : ∀ (n : ι), PolishSpace (β n)<VAR>f : (n : ι) → β n → α<VAR>f_cont : ∀ (n : ι), Continuous (f n)<VAR>f_range : ∀ (n : ι), range (f n) = s n<VAR>γ : Type u_2 := (n : ι) × β n<VAR>F : γ → α := fun x => match x with | ⟨n, x⟩ => f n x<VAR>F_cont : Continuous F<GOAL>AnalyticSet (⋃ n, s n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), AnalyticSet (s n)<VAR>β : ι → Type<VAR>hβ : (n : ι) → TopologicalSpace (β n)<VAR>h'β : ∀ (n : ι), PolishSpace (β n)<VAR>f : (n : ι) → β n → α<VAR>f_cont : ∀ (n : ι), Continuous (f n)<VAR>f_range : ∀ (n : ι), range (f n) = s n<VAR>γ : Type u_2 := (n : ι) × β n<VAR>F : γ → α := fun x => match x with | ⟨n, x⟩ => f n x<VAR>F_cont : Continuous F<VAR>F_range : range F = ⋃ n, s n<GOAL>AnalyticSet (⋃ n, s n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), AnalyticSet (s n)<VAR>β : ι → Type<VAR>hβ : (n : ι) → TopologicalSpace (β n)<VAR>h'β : ∀ (n : ι), PolishSpace (β n)<VAR>f : (n : ι) → β n → α<VAR>f_cont : ∀ (n : ι), Continuous (f n)<VAR>f_range : ∀ (n : ι), range (f n) = s n<VAR>γ : Type u_2 := (n : ι) × β n<VAR>F : γ → α := fun x => match x with | ⟨n, x⟩ => f n x<VAR>F_cont : Continuous F<VAR>F_range : range F = ⋃ n, s n<GOAL>AnalyticSet (range F)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : LieRing L'<VAR>inst✝² : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>inst✝¹ : IsSolvable R L<VAR>inst✝ : Nontrivial L<GOAL>derivedSeries R L 1 < ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : LieRing L'<VAR>inst✝² : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>inst✝¹ : IsSolvable R L<VAR>inst✝ : Nontrivial L<VAR>n : ℕ<VAR>hn : derivedSeries R L n = ⊥<GOAL>derivedSeries R L 1 < ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : LieRing L'<VAR>inst✝² : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>inst✝¹ : IsSolvable R L<VAR>inst✝ : Nontrivial L<VAR>n : ℕ<VAR>hn : derivedSeries R L n = ⊥<GOAL>derivedSeries R L 1 ≠ ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : LieRing L'<VAR>inst✝² : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>inst✝¹ : IsSolvable R L<VAR>inst✝ : Nontrivial L<VAR>n : ℕ<VAR>hn : derivedSeries R L n = ⊥<VAR>contra : derivedSeries R L 1 = ⊤<GOAL>False
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : LieRing L'<VAR>inst✝² : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>inst✝¹ : IsSolvable R L<VAR>inst✝ : Nontrivial L<VAR>n : ℕ<VAR>hn : ⊤ = ⊥<VAR>contra : derivedSeries R L 1 = ⊤<GOAL>False
<VAR>F✝ : Type u_1<VAR>inst✝⁵ : Field F✝<VAR>E : Type u_2<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F✝ E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>ι : Type u_5<VAR>t : ι → IntermediateField K L<VAR>p : ι → K[X]<VAR>s : Finset ι<VAR>h0 : ∏ i ∈ s, p i ≠ 0<VAR>h : ∀ i ∈ s, IsSplittingField K (↥(t i)) (p i)<VAR>F : IntermediateField K L := ⨆ i ∈ s, t i<GOAL>IsSplittingField K (↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i)
<VAR>F✝ : Type u_1<VAR>inst✝⁵ : Field F✝<VAR>E : Type u_2<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F✝ E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>ι : Type u_5<VAR>t : ι → IntermediateField K L<VAR>p : ι → K[X]<VAR>s : Finset ι<VAR>h0 : ∏ i ∈ s, p i ≠ 0<VAR>h : ∀ i ∈ s, IsSplittingField K (↥(t i)) (p i)<VAR>F : IntermediateField K L := ⨆ i ∈ s, t i<VAR>hF : ∀ i ∈ s, t i ≤ F<GOAL>IsSplittingField K (↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i)
<VAR>F✝ : Type u_1<VAR>inst✝⁵ : Field F✝<VAR>E : Type u_2<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F✝ E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>ι : Type u_5<VAR>t : ι → IntermediateField K L<VAR>p : ι → K[X]<VAR>s : Finset ι<VAR>h0 : ∏ i ∈ s, p i ≠ 0<VAR>F : IntermediateField K L := ⨆ i ∈ s, t i<VAR>hF : ∀ i ∈ s, t i ≤ F<VAR>h : ∀ i ∈ s, Splits (algebraMap K ↥(t i)) (p i) ∧ t i = adjoin K ((p i).rootSet L)<GOAL>Splits (algebraMap K ↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i) ∧ ⨆ i ∈ s, t i = adjoin K ((∏ i ∈ s, p i).rootSet L)
<VAR>F✝ : Type u_1<VAR>inst✝⁵ : Field F✝<VAR>E : Type u_2<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F✝ E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>ι : Type u_5<VAR>t : ι → IntermediateField K L<VAR>p : ι → K[X]<VAR>s : Finset ι<VAR>h0 : ∏ i ∈ s, p i ≠ 0<VAR>F : IntermediateField K L := ⨆ i ∈ s, t i<VAR>hF : ∀ i ∈ s, t i ≤ F<VAR>h : ∀ i ∈ s, Splits (algebraMap K ↥(t i)) (p i) ∧ t i = adjoin K ((p i).rootSet L)<GOAL>⨆ i ∈ s, t i = adjoin K ((∏ i ∈ s, p i).rootSet L)
<VAR>F✝ : Type u_1<VAR>inst✝⁵ : Field F✝<VAR>E : Type u_2<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F✝ E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>ι : Type u_5<VAR>t : ι → IntermediateField K L<VAR>p : ι → K[X]<VAR>s : Finset ι<VAR>h0 : ∏ i ∈ s, p i ≠ 0<VAR>F : IntermediateField K L := ⨆ i ∈ s, t i<VAR>hF : ∀ i ∈ s, t i ≤ F<VAR>h : ∀ i ∈ s, Splits (algebraMap K ↥(t i)) (p i) ∧ t i = adjoin K ((p i).rootSet L)<GOAL>⨆ i ∈ s, t i = ⨆ i ∈ s, adjoin K ((p i).rootSet L)