ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>a : FiniteAdeleRing R K<VAR>S : Set (HeightOneSpectrum R) := {v | (fun v => ↑a v) v ∉ adicCompletionIntegers K v}<VAR>b : (v : HeightOneSpectrum R) → adicCompletion K v → R<VAR>hb : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), b v a ∈ R⁰<VAR>h : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), a * ↑(b v a) ∈ adicCompletionIntegers K v<VAR>p : R := ∏ᶠ (v : HeightOneSpectrum R) (_ : v ∈ S), b v ((fun v => ↑a v) v)<VAR>hp : p ∈ R⁰<GOAL>∃ c, a * ↑↑⟨p, hp⟩ = ↑c
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>a : FiniteAdeleRing R K<VAR>S : Set (HeightOneSpectrum R) := {v | (fun v => ↑a v) v ∉ adicCompletionIntegers K v}<VAR>b : (v : HeightOneSpectrum R) → adicCompletion K v → R<VAR>hb : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), b v a ∈ R⁰<VAR>h : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), a * ↑(b v a) ∈ adicCompletionIntegers K v<VAR>p : R := ∏ᶠ (v : HeightOneSpectrum R) (_ : v ∈ S), b v ((fun v => ↑a v) v)<VAR>hp : p ∈ R⁰<GOAL>∀ (v : HeightOneSpectrum R), (fun v => ↑(a * ↑↑⟨p, hp⟩) v) v ∈ adicCompletionIntegers K v
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s' s t : Multiset α<GOAL>CutExpand r (s' + t) (s + t) ↔ CutExpand r s' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g✝ : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f : ℕ → E''<VAR>g : ℕ → F''<VAR>h : ∀ (x : ℕ), g x = 0 → f x = 0<GOAL>f =O[atTop] g ↔ ∃ C, ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : TopologicalSpace E<VAR>f : E → F<VAR>D : Set E<VAR>x : E<VAR>hf : ContinuousWithinAt f D x<GOAL>oscillationWithin f D x = 0
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : TopologicalSpace E<VAR>f : E → F<VAR>D : Set E<VAR>x : E<VAR>hf : ContinuousWithinAt f D x<VAR>ε : NNReal<VAR>hε : 0 < ε<VAR>x✝ : 0 < ⊤<GOAL>oscillationWithin f D x ≤ 0 + ↑ε
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : TopologicalSpace E<VAR>f : E → F<VAR>D : Set E<VAR>x : E<VAR>hf : ContinuousWithinAt f D x<VAR>ε : NNReal<VAR>hε : 0 < ε<VAR>x✝ : 0 < ⊤<GOAL>oscillationWithin f D x ≤ ↑ε
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : TopologicalSpace E<VAR>f : E → F<VAR>D : Set E<VAR>x : E<VAR>hf : ContinuousWithinAt f D x<VAR>ε : NNReal<VAR>hε : 0 < ε<VAR>x✝ : 0 < ⊤<VAR>this : ball (f x) (↑ε / 2) ∈ Filter.map f (𝓝[D] x)<GOAL>oscillationWithin f D x ≤ ↑ε
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : TopologicalSpace E<VAR>f : E → F<VAR>D : Set E<VAR>x : E<VAR>hf : ContinuousWithinAt f D x<VAR>ε : NNReal<VAR>hε : 0 < ε<VAR>x✝ : 0 < ⊤<VAR>this : ball (f x) (↑ε / 2) ∈ Filter.map f (𝓝[D] x)<GOAL>2 * (↑ε / 2) = ↑ε
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>a b : α<GOAL>Setoid.r a b ↔ a⁻¹ * b ∈ s
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ coequalizer.desc P.actLeft ⋯ ≫ (λ_ P.X).inv ≫ R.one ▷ P.X ≫ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) = coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ 𝟙 (coequalizer (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>((P.actLeft ≫ (λ_ P.X).inv) ≫ R.one ▷ P.X) ≫ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) = coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ 𝟙 (coequalizer (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>(((λ_ (R.X ⊗ P.X)).inv ≫ 𝟙_ C ◁ P.actLeft) ≫ R.one ▷ P.X) ≫ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) = coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ 𝟙 (coequalizer (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>(λ_ (R.X ⊗ P.X)).inv ≫ (R.one ▷ (R.X ⊗ P.X) ≫ R.X ◁ P.actLeft) ≫ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) = coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ 𝟙 (coequalizer (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>(λ_ (R.X ⊗ P.X)).inv ≫ R.one ▷ (R.X ⊗ P.X) ≫ ((α_ R.X R.X P.X).inv ≫ (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) = coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ 𝟙 (coequalizer (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>(λ_ (R.X ⊗ P.X)).inv ≫ R.one ▷ (R.X ⊗ P.X) ≫ (α_ R.X R.X P.X).inv ≫ R.mul ▷ P.X ≫ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) = coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ 𝟙 (coequalizer (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>(λ_ (R.X ⊗ P.X)).inv ≫ (((α_ (𝟙_ C) R.X P.X).inv ≫ R.one ▷ R.X ▷ P.X) ≫ R.mul ▷ P.X) ≫ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) = coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ 𝟙 (coequalizer (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>(λ_ (R.X ⊗ P.X)).inv ≫ (α_ (𝟙_ C) R.X P.X).inv ≫ (λ_ R.X).hom ▷ P.X ≫ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) = coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ 𝟙 (coequalizer (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>(λ_ (R.X ⊗ P.X)).inv ≫ (α_ (𝟙_ C) R.X P.X).inv ≫ (λ_ R.X).hom ▷ P.X ≫ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) = coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G✝ : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>G : SimpleGraph V<GOAL>∀ {a b : ↑Set.univ}, G.Adj ((Equiv.Set.univ V) a) ((Equiv.Set.univ V) b) ↔ (induce Set.univ G).Adj a b
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>l : List α<VAR>x : α<VAR>n k : ℕ<VAR>hn : k < n<VAR>hk : k < l.length<VAR>hk' : optParam (k < (insertNth n x l).length) ⋯<GOAL>(insertNth n x l).get ⟨k, hk'⟩ = l.get ⟨k, hk⟩
<VAR>n m k : ℕ<VAR>h₁ : k ≤ n<GOAL>map (fun x => x - k) (Ico n m) = Ico (n - k) (m - k)
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>h : ¬DifferentiableAt 𝕜 f x<GOAL>(fderiv 𝕜 f x) 1 = 0
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>h : ¬DifferentiableAt 𝕜 f x<GOAL>0 1 = 0
<VAR>m k : ℕ+<VAR>h : k ∣ m<GOAL>k * m.divExact k = m
<VAR>m k : ℕ+<VAR>h : k ∣ m<GOAL>↑(k * m.divExact k) = ↑m
<VAR>m k : ℕ+<VAR>h : k ∣ m<GOAL>↑k * ↑(m.divExact k) = ↑m
<VAR>m k : ℕ+<VAR>h : k ∣ m<GOAL>↑k * (m.div k).succ = ↑m
<VAR>ι : Type u_1<VAR>inst✝ : LinearOrder ι<VAR>j i : ι<VAR>hij : j < succFn i<GOAL>j ≤ i
<VAR>ι : Type u_1<VAR>inst✝ : LinearOrder ι<VAR>j i : ι<VAR>hij : ∃ c ∈ lowerBounds (Set.Ioi i), j < c<GOAL>j ≤ i
<VAR>ι : Type u_1<VAR>inst✝ : LinearOrder ι<VAR>j i k : ι<VAR>hk_lb : k ∈ lowerBounds (Set.Ioi i)<VAR>hk : j < k<GOAL>j ≤ i
<VAR>ι : Type u_1<VAR>inst✝ : LinearOrder ι<VAR>j i k : ι<VAR>hk_lb : ∀ x ∈ Set.Ioi i, k ≤ x<VAR>hk : j < k<GOAL>j ≤ i
<VAR>a : Bool<VAR>m : ℤ<VAR>b : Bool<VAR>n : ℤ<GOAL>(bit a m).ldiff (bit b n) = bit (a && !b) (m.ldiff n)
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r✝ : X<VAR>s✝ : ↥S<GOAL>r✝ /ₒ s✝ + 0 = r✝ /ₒ s✝
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r✝ : X<VAR>s✝ : ↥S<GOAL>(r✝ + 0) /ₒ s✝ = r✝ /ₒ s✝
<VAR>o b : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>ho : Principal (fun x x_1 => x * x_1) (b ^ o)<VAR>x y : Ordinal.{u_1}<VAR>hx : x < o<VAR>hy : y < o<GOAL>(fun x x_1 => x + x_1) x y < o
<VAR>o b : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>ho : Principal (fun x x_1 => x * x_1) (b ^ o)<VAR>x y : Ordinal.{u_1}<VAR>hx : x < o<VAR>hy : y < o<VAR>this : (fun x x_1 => x * x_1) (b ^ x) (b ^ y) < b ^ o<GOAL>(fun x x_1 => x + x_1) x y < o
<VAR>o b : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>ho : Principal (fun x x_1 => x * x_1) (b ^ o)<VAR>x y : Ordinal.{u_1}<VAR>hx : x < o<VAR>hy : y < o<VAR>this : b ^ x * b ^ y < b ^ o<GOAL>x + y < o
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff + q.leadingCoeff ≠ 0<VAR>hlt : p.degree < q.degree<GOAL>max p.degree q.degree ≤ (p + q).degree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff + q.leadingCoeff ≠ 0<VAR>HEq : p.degree = q.degree<VAR>hlt : max p.degree q.degree > (p + q).degree<GOAL>p.leadingCoeff + q.leadingCoeff = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff + q.leadingCoeff ≠ 0<VAR>HEq : p.degree = q.degree<VAR>hlt : q.degree > (p + q).degree<GOAL>p.leadingCoeff + q.leadingCoeff = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff + q.leadingCoeff ≠ 0<VAR>HEq : p.degree = q.degree<VAR>hlt : q.degree > (p + q).degree<GOAL>(p + q).coeff q.natDegree = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff + q.leadingCoeff ≠ 0<VAR>hlt : q.degree < p.degree<GOAL>max p.degree q.degree ≤ (p + q).degree
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝ : MeasurableSpace α<VAR>f : α → Bool<VAR>h : MeasurableSet (f ⁻¹' {true})<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝ : MeasurableSpace α<VAR>f : α → Bool<VAR>h : MeasurableSet (f ⁻¹' {true})<GOAL>∀ (x : Bool), MeasurableSet (f ⁻¹' {x})
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : HeytingAlgebra α<VAR>a b c : α<GOAL>a ≤ bᶜ ↔ b ≤ aᶜ
<VAR>n : ℕ<VAR>n1 : 1 ≤ n<VAR>s : ℕ := n.sqrt<GOAL>(unpair n).1 < n
<VAR>n : ℕ<VAR>n1 : 1 ≤ n<VAR>s : ℕ := n.sqrt<GOAL>(if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 < n
<GOAL>0 ∈ ∅ ∨ ∅ = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : Measure α<VAR>a b : α<VAR>hb : μ {b} ≠ ⊤<GOAL>IntegrableOn f (Iic b) μ ↔ IntegrableOn f (Iio b) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>u : Set ↑t<GOAL>t.restrictPreimage f ⁻¹' u = (fun a => f ↑a) ⁻¹' (Subtype.val '' u)
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>cmp (a / b) 1 = cmp a b
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>inst✝ : S.HasLeftHomology<GOAL>S.leftHomologyData.π ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData h = cyclesMap' (𝟙 S) S.leftHomologyData h ≫ h.π
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : 0 ≤ r₁<VAR>hr₂ : r₁ ≤ r₂<GOAL>Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : 0 ≤ r₁<VAR>hr₂ : r₁ ≤ r₂<GOAL>(lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : 0 ≤ r₁<VAR>hr₂ : r₁ ≤ r₂<VAR>h : ¬r₁ = 0<GOAL>(lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<VAR>h : DirectedOn (fun x x_1 => x ≤ x_1) s<GOAL>a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<VAR>h : DirectedOn (fun x x_1 => x ≤ x_1) s<GOAL>∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b
<VAR>R : Type u_1<VAR>m n : ℕ<VAR>hmn : m.Coprime n<GOAL>(m * n).divisors.card = m.divisors.card * n.divisors.card
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f✝ g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>f : X → α<VAR>hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y<VAR>l : Filter α<GOAL>Tendsto (lift f hf) (𝓝 (mk x)) l ↔ Tendsto f (𝓝 x) l
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<GOAL>∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x ↑(δ x) ⊆ U i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>δ : C(X, ℝ)<VAR>hδ₀ : ∀ (x : X), 0 < δ x<VAR>hδ : ∀ (i : ι), ∀ x ∈ K i, closedBall x (ENNReal.ofReal (δ x)) ⊆ U i<GOAL>∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x ↑(δ x) ⊆ U i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>δ : C(X, ℝ≥0)<VAR>hδ₀ : ∀ (x : X), 0 < (ContinuousMap.coeNNRealReal.comp δ) x<VAR>hδ : ∀ (i : ι), ∀ x ∈ K i, closedBall x (ENNReal.ofReal ((ContinuousMap.coeNNRealReal.comp δ) x)) ⊆ U i<VAR>i : ι<VAR>x : X<VAR>hi : x ∈ K i<GOAL>closedBall x ↑(δ x) ⊆ U i
<VAR>f g : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>n : ℕ<GOAL>Continuous ⇑(f ^ n)
<VAR>f g : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>n : ℕ<GOAL>Continuous (⇑f)^[n]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>a b c : α<VAR>h : a ≤ b<GOAL>¬a ⩿ b ↔ ∃ c, a < c ∧ c < b
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z : ℝ≥0∞<VAR>h1 : y ≠ 0<VAR>h2 : y ≠ ⊤<GOAL>x / y ≤ z ↔ x ≤ y * z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<GOAL>a / b = a ↔ b = 1
<VAR>I : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : I → Type v₁<VAR>g✝ : I → Type v₂<VAR>h : I → Type v₃<VAR>x y : (i : I) → f✝ i<VAR>i : I<VAR>inst✝ : Inv γ<VAR>f : α → β<VAR>g : α → γ<VAR>e : β → γ<GOAL>extend f g⁻¹ e⁻¹ = (extend f g e)⁻¹
<VAR>n : ℕ<VAR>h₁ : 0 < 4 * (↑n + 1) ^ 2<VAR>h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2<GOAL>Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤ 1 / (4 * ↑(n + 1) ^ 2)
<VAR>n : ℕ<VAR>h₁ : 0 < 4 * (↑n + 1) ^ 2<VAR>h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2<VAR>h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2<GOAL>Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤ 1 / (4 * ↑(n + 1) ^ 2)
<VAR>n : ℕ<VAR>h₁ : 0 < 4 * (↑n + 1) ^ 2<VAR>h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2<VAR>h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2<GOAL>(1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2) ≤ 1 / (4 * ↑(n + 1) ^ 2)
<VAR>n : ℕ<VAR>h₁ : 0 < 4 * (↑n + 1) ^ 2<VAR>h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2<VAR>h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2<GOAL>(1 / (2 * (↑n + 1) + 1)) ^ 2 / (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2) ≤ 1 / (4 * (↑n + 1) ^ 2)
<VAR>n : ℕ<VAR>h₁ : 0 < 4 * (↑n + 1) ^ 2<VAR>h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2<VAR>h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2<GOAL>(1 / (2 * (↑n + 1) + 1)) ^ 2 * (4 * (↑n + 1) ^ 2) ≤ 1 * (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2)
<VAR>n : ℕ<VAR>h₁ : 0 < 4 * (↑n + 1) ^ 2<VAR>h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2<VAR>h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2<GOAL>4 * (↑n + 1) ^ 2 / (2 * (↑n + 1) + 1) ^ 2 ≤ ((2 * (↑n + 1) + 1) ^ 2 - 1) / (2 * (↑n + 1) + 1) ^ 2
<VAR>n : ℕ<VAR>h₁ : 0 < 4 * (↑n + 1) ^ 2<VAR>h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2<VAR>h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2<GOAL>4 * (↑n + 1) ^ 2 ≤ (2 * (↑n + 1) + 1) ^ 2 - 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>h : s.card = n + 1<VAR>a : α<VAR>has : a ∈ s<GOAL>(s.erase a).card = n
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N✝ N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N : LieSubmodule R L M<GOAL>Nontrivial ↥↑N ↔ N ≠ ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N✝ N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N : LieSubmodule R L M<GOAL>N = ⊥ → ¬Nontrivial ↥↑N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N✝ N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N : LieSubmodule R L M<GOAL>¬Nontrivial ↥↑N → N = ⊥
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>g : ℝ → F<VAR>a : ℝ<GOAL>∫ (x : ℝ), g (a * x) = |a⁻¹| • ∫ (y : ℝ), g y
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU✝ : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>f : ℕ → Set α<VAR>hm : ∀ (i : ℕ), P (f i)<VAR>mU : m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>i : ℕ<GOAL>m (f i) ⋯ = extend m (f i)
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Fintype P<VAR>inst✝ : Finite L<GOAL>Fintype.card P = order P L ^ 2 + order P L + 1
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Fintype P<VAR>inst✝ : Finite L<VAR>val✝ : Fintype L<GOAL>Fintype.card P = order P L ^ 2 + order P L + 1
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Fintype P<VAR>inst✝ : Finite L<VAR>val✝ : Fintype L<VAR>p : P<GOAL>Fintype.card P = order P L ^ 2 + order P L + 1
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Fintype P<VAR>inst✝ : Finite L<VAR>val✝ : Fintype L<VAR>p : P<VAR>ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } := { toFun := fun q => ⟨⟨mkLine ⋯, ⋯⟩, ⟨↑q, ⋯⟩⟩, invFun := fun lq => ⟨↑lq.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }<GOAL>Fintype.card P = order P L ^ 2 + order P L + 1
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s✝ : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : NonUnitalNonAssocSemiring R<VAR>inst✝ : NonUnitalNonAssocSemiring S<VAR>b : S<VAR>s : α →₀ R<VAR>f : α → R → S<GOAL>s.sum f * b = s.sum fun a c => f a c * b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>((rename (Prod.mk 0)) (wittPolynomial p ℤ n) * (rename (Prod.mk 1)) (wittPolynomial p ℤ n)).vars ⊆ univ ×ˢ range (n + 1)