ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>(α_ R.X P.X S.X).inv ≫ (α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight ≫ P.actLeft = R.X ◁ P.actRight ≫ P.actLeft
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>hp : p ≠ 0<VAR>f : R[X]<VAR>n : ℕ<GOAL>(contract p f).coeff n = f.coeff (n * p)
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>hp : p ≠ 0<VAR>f : R[X]<VAR>n : ℕ<GOAL>f.natDegree + 1 ≤ n → 0 = f.coeff (n * p)
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>hp : p ≠ 0<VAR>f : R[X]<VAR>n : ℕ<VAR>hn : f.natDegree + 1 ≤ n<GOAL>0 = f.coeff (n * p)
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>hp : p ≠ 0<VAR>f : R[X]<VAR>n : ℕ<VAR>hn : f.natDegree + 1 ≤ n<GOAL>f.natDegree < n * p
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>G : Comonad C<VAR>A B : G.Coalgebra<VAR>f : A ⟶ B<VAR>inst✝ : IsIso f.f<GOAL>B.a ≫ G.map (inv f.f) = inv f.f ≫ A.a
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>G : Comonad C<VAR>A B : G.Coalgebra<VAR>f : A ⟶ B<VAR>inst✝ : IsIso f.f<GOAL>A.a ≫ G.map f.f ≫ G.map (inv f.f) = A.a
<VAR>q₁ q₂ : ℚ<GOAL>(q₁ * q₂).den ∣ q₁.den * q₂.den
<VAR>q₁ q₂ : ℚ<GOAL>{ num := q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)), den := q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den), den_nz := ⋯, reduced := ⋯ }.den ∣ q₁.den * q₂.den
<VAR>q₁ q₂ : ℚ<GOAL>(q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den) ∣ q₁.den * q₂.den
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>f : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>a : 𝕜'<VAR>ha : a ≠ 0<GOAL>logDeriv (fun z => a * f z) x = logDeriv f x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : CommMonoid N<VAR>inst✝¹ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝ : CommRing R<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℕ<GOAL>h.zmodEquivZPowers.symm (Additive.ofMul ⟨ζ ^ i, ⋯⟩) = ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Nat.card α = 1 ↔ ∃ x, ∀ (y : α), y = x
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Subsingleton α ∧ Nonempty α ↔ ∃ x, ∀ (y : α), y = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>c✝ c : ComplexMeasure α<VAR>μ : Measure α<GOAL>Integrable (c.rnDeriv μ) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>c✝ c : ComplexMeasure α<VAR>μ : Measure α<GOAL>Memℒp (fun x => RCLike.re (c.rnDeriv μ x)) 1 μ ∧ Memℒp (fun x => RCLike.im (c.rnDeriv μ x)) 1 μ
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : StrongRankCondition R<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>inst✝ : Infinite ι<VAR>κ : Type w<VAR>v : κ → M<VAR>i : LinearIndependent R v<GOAL>#κ ≤ #ι
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>h : p.trailingDegree = ↑n<GOAL>p.natTrailingDegree = n
<VAR>a b : Ordinal.{u_1}<GOAL>a.toPGame ⧏ b.toPGame → a < b
<VAR>a b : Ordinal.{u_1}<GOAL>¬a < b → ¬a.toPGame ⧏ b.toPGame
<VAR>a b : Ordinal.{u_1}<GOAL>b ≤ a → b.toPGame ≤ a.toPGame
<VAR>α β : PartOrd<VAR>e : ↑α ≃o ↑β<VAR>x : (forget PartOrd).obj α<GOAL>(↑e ≫ ↑e.symm) x = (𝟙 α) x
<VAR>α β : PartOrd<VAR>e : ↑α ≃o ↑β<VAR>x : (forget PartOrd).obj β<GOAL>(↑e.symm ≫ ↑e) x = (𝟙 β) x
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ right b<GOAL>((Finset.erase b m).erase (m.1 - 1, m.2)).card + 2 = Finset.card b
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ right b<GOAL>(Finset.erase b m).card - 1 + 2 = Finset.card b
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ right b<GOAL>Finset.card b - 1 - 1 + 2 = Finset.card b
<VAR>X : Type u<VAR>m₁ m₂ : X → X → X<VAR>e₁ e₂ : X<VAR>h₁ : IsUnital m₁ e₁<VAR>h₂ : IsUnital m₂ e₂<VAR>distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)<VAR>a b c : X<GOAL>m₂ (m₂ a b) c = m₂ a (m₂ b c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<GOAL>μ.singularPart ν = 0 ↔ μ ≪ ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)<GOAL>μ.singularPart ν = 0 ↔ μ ≪ ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)<VAR>h : μ.singularPart ν = 0<GOAL>μ ≪ ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>h_dec : μ = ν.withDensity (μ.rnDeriv ν)<VAR>h : μ.singularPart ν = 0<GOAL>μ ≪ ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>h_dec : μ = ν.withDensity (μ.rnDeriv ν)<VAR>h : μ.singularPart ν = 0<GOAL>ν.withDensity (μ.rnDeriv ν) ≪ ν
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>a₁ a₂ : A<VAR>p₁ p₂ : R[X]<GOAL>(toFunLinear R A) ((a₁ * a₂) ⊗ₜ[R] (p₁ * p₂)) = (toFunLinear R A) (a₁ ⊗ₜ[R] p₁) * (toFunLinear R A) (a₂ ⊗ₜ[R] p₂)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfg : f ≈ g<VAR>h : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))<VAR>hlt : padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))<VAR>hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))<VAR>i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfg : f ≈ g<VAR>h : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))<VAR>hlt : padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))<VAR>hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))<VAR>i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))<VAR>hi : N ≤ i<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfg : f ≈ g<VAR>h : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))<VAR>hlt : padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))<VAR>hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))<VAR>i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))<VAR>hi : N ≤ i<VAR>hN' : padicNorm p (↑(f - g) i) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfg : f ≈ g<VAR>hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))<VAR>N : ℕ<VAR>hlt : padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) < padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))<VAR>h : padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠ padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))<VAR>hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))<VAR>i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))<VAR>hi : N ≤ i<VAR>hN' : padicNorm p (↑(f - g) i) < padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) - padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfg : f ≈ g<VAR>hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))<VAR>N : ℕ<VAR>hlt : padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) < padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))<VAR>h : padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠ padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))<VAR>hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))<VAR>i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))<VAR>hi : N ≤ i<VAR>hN' : padicNorm p (↑(f - g) i) < padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) - padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))<VAR>hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfg : f ≈ g<VAR>hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))<VAR>N : ℕ<VAR>hlt : padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) < padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))<VAR>h : padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠ padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))<VAR>hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))<VAR>i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))<VAR>hi : N ≤ i<VAR>hN' : padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) < padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) - padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))<VAR>hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfg : f ≈ g<VAR>hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))<VAR>N : ℕ<VAR>hlt : padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) < padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))<VAR>h : padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠ padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))<VAR>hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))<VAR>i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))<VAR>hi : N ≤ i<VAR>hN' : padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) < padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) - padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))<VAR>hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)<VAR>this : padicNorm p (↑f i) < padicNorm p (↑f i)<GOAL>False
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : Monoid P<VAR>P' : Type u_4<VAR>inst✝ : Monoid P'<VAR>f : P →* P'<VAR>g₁ : M →* P<VAR>g₂ : N →* P<GOAL>(f.comp (lift g₁ g₂)).comp inl = (lift (f.comp g₁) (f.comp g₂)).comp inl
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : Monoid P<VAR>P' : Type u_4<VAR>inst✝ : Monoid P'<VAR>f : P →* P'<VAR>g₁ : M →* P<VAR>g₂ : N →* P<GOAL>(f.comp (lift g₁ g₂)).comp inr = (lift (f.comp g₁) (f.comp g₂)).comp inr
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E<VAR>H : φ₁.compMultilinearMap (tprod R) = φ₂.compMultilinearMap (tprod R)<GOAL>φ₁ = φ₂
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E<VAR>H : φ₁.compMultilinearMap (tprod R) = φ₂.compMultilinearMap (tprod R)<GOAL>∀ (x : ⨂[R] (i : ι), s i), φ₁ x = φ₂ x
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E<VAR>H : φ₁.compMultilinearMap (tprod R) = φ₂.compMultilinearMap (tprod R)<VAR>z : ⨂[R] (i : ι), s i<GOAL>∀ (r : R) (f : (i : ι) → s i), φ₁ (tprodCoeff R r f) = φ₂ (tprodCoeff R r f)
<VAR>i : ℕ<VAR>ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i<VAR>n : ℕ<GOAL>n.testBit (i + 1) = n.bits.getI (i + 1)
<VAR>i : ℕ<VAR>ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i<VAR>n : ℕ<GOAL>(bit n.bodd n.div2).testBit (i + 1) = n.bits.getI (i + 1)
<VAR>i : ℕ<VAR>ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i<VAR>n : ℕ<GOAL>n.bits.tail.getI i = n.bits.getI (i + 1)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>P Q R : C<VAR>f f' : P ⟶ Q<VAR>g g' : Q ⟶ R<VAR>inst✝ : IsIso f<GOAL>f ≫ g = 0 ↔ g = 0
<VAR>C✝ : Type u<VAR>inst✝³ : Category.{v, u} C✝<VAR>C : Type u<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : F.Final<GOAL>IsConnected C ↔ IsConnected D
<VAR>C✝ : Type u<VAR>inst✝³ : Category.{v, u} C✝<VAR>C : Type u<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : F.Final<GOAL>Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{(max v u v₂ u₂) + 1}) ↔ Nonempty (colimit (constPUnitFunctor D) ≅ PUnit.{(max v u v₂ u₂) + 1})
<VAR>α : Type u_1<VAR>inst✝⁵ : Mul α<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : CovariantClass α α (Function.swap HMul.hMul) LE.le<VAR>inst✝ : LocallyFiniteOrderTop α<VAR>a b : α<GOAL>↑(Ici a * Ici b) ⊆ ↑(Ici (a * b))
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : ContinuousConstSMul αᵐᵒᵖ α<VAR>s t : Set α<VAR>hs : IsOpen s<GOAL>IsOpen (s * t)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : ContinuousConstSMul αᵐᵒᵖ α<VAR>s t : Set α<VAR>hs : IsOpen s<GOAL>IsOpen (⋃ a ∈ t, op a • s)
<VAR>n : ℕ∞<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>y : E<VAR>hy : y ∈ ball 0 1<GOAL>ContDiffWithinAt ℝ n (↑univUnitBall.symm) (ball 0 1) y
<VAR>n : ℕ∞<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>y : E<VAR>hy : y ∈ ball 0 1<GOAL>ContDiffAt ℝ n (↑univUnitBall.symm) y
<VAR>n : ℕ∞<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>y : E<VAR>hy : y ∈ ball 0 1<GOAL>ContDiffAt ℝ n (fun y => (√(1 - ‖y‖ ^ 2))⁻¹) y
<VAR>n : ℕ∞<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>y : E<VAR>hy : y ∈ ball 0 1<VAR>h : 0 < 1 - ‖y‖ ^ 2<GOAL>ContDiffAt ℝ n (fun y => (√(1 - ‖y‖ ^ 2))⁻¹) y
<VAR>n : ℕ∞<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>y : E<VAR>hy : y ∈ ball 0 1<VAR>h : 0 < 1 - ‖y‖ ^ 2<GOAL>ContDiffAt ℝ n (fun y => √(1 - ‖y‖ ^ 2)) y
<VAR>n : ℕ∞<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>y : E<VAR>hy : y ∈ ball 0 1<VAR>h : 0 < 1 - ‖y‖ ^ 2<GOAL>ContDiffAt ℝ n (fun y => 1 - ‖y‖ ^ 2) y
<VAR>α✝ : Type u_1<VAR>inst✝³ : SemilatticeSup α✝<VAR>inst✝² : OrderBot α✝<VAR>inst✝¹ : DecidableEq α✝<VAR>α : Type u_2<VAR>inst✝ : DecidableEq α<VAR>m : Multiset (Multiset α)<GOAL>m.sup.Nodup ↔ ∀ a ∈ m, a.Nodup
<VAR>α✝ : Type u_1<VAR>inst✝³ : SemilatticeSup α✝<VAR>inst✝² : OrderBot α✝<VAR>inst✝¹ : DecidableEq α✝<VAR>α : Type u_2<VAR>inst✝ : DecidableEq α<GOAL>(sup 0).Nodup ↔ ∀ a ∈ 0, a.Nodup
<VAR>α✝ : Type u_1<VAR>inst✝³ : SemilatticeSup α✝<VAR>inst✝² : OrderBot α✝<VAR>inst✝¹ : DecidableEq α✝<VAR>α : Type u_2<VAR>inst✝ : DecidableEq α<VAR>a✝ : Multiset α<VAR>s✝ : Multiset (Multiset α)<VAR>h : s✝.sup.Nodup ↔ ∀ a ∈ s✝, a.Nodup<GOAL>(a✝ ::ₘ s✝).sup.Nodup ↔ ∀ a ∈ a✝ ::ₘ s✝, a.Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : SMulZeroClass α β<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : PosSMulStrictMono α β<VAR>inst✝ : PosSMulReflectLT α β<VAR>ha : 0 < a<GOAL>a • b < 0 ↔ b < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝³ : PseudoMetricSpace α<VAR>inst✝² : PseudoMetricSpace β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : DilationClass F α β<VAR>f : F<GOAL>Metric.diam (range ⇑f) = ↑(ratio f) * Metric.diam univ
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<VAR>ht : IsUpperSet t<GOAL>IsLowerSet (s / t)
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<VAR>ht : IsUpperSet t<GOAL>IsLowerSet (s * t⁻¹)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring R₂<VAR>inst✝¹¹ : Semiring R₃<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_11<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F τ₁₂ M M₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>range f = ⊥ ↔ f = 0
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : BilinForm R M<VAR>h : BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : BilinMap.toQuadraticMap B' = Q'' - Q'<VAR>x : CliffordAlgebra Q<GOAL>(changeForm ⋯) ((changeForm h) x) = x
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : BilinForm R M<VAR>h : BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : BilinMap.toQuadraticMap B' = Q'' - Q'<VAR>x : CliffordAlgebra Q'<GOAL>(changeForm h) ((changeForm ⋯) x) = x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 : P<VAR>hp1p2 : p1 ≠ p2<GOAL>∠ p1 (midpoint ℝ p1 p2) p2 = π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 : P<VAR>hp1p2 : p1 ≠ p2<GOAL>InnerProductGeometry.angle (p1 -ᵥ p2) (p2 -ᵥ p1) = π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 : P<VAR>hp1p2 : p1 ≠ p2<GOAL>InnerProductGeometry.angle (p1 -ᵥ p2) (-(p1 -ᵥ p2)) = π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 : P<VAR>hp1p2 : p1 ≠ p2<GOAL>p1 -ᵥ p2 ≠ 0
<VAR>x✝ y x : ℝ<GOAL>|sin x| = √(1 - cos x ^ 2)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<GOAL>h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯ = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<GOAL>leftRightHomologyComparison' h₁ h₂ = h₁.descH (h₂.liftH (h₁.i ≫ h₂.p) ⋯) ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>p : α → Prop<VAR>f : Filter α<VAR>hp : ∃ᶠ (x : α) in f, p x<GOAL>∃ x, p x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>p : α → Prop<VAR>f : Filter α<VAR>hp : ∃ᶠ (x : α) in f, p x<VAR>H : ¬∃ x, p x<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>p : α → Prop<VAR>f : Filter α<VAR>hp : ∃ᶠ (x : α) in f, p x<VAR>H : ∀ᶠ (x : α) in f, ¬p x<GOAL>False
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<GOAL>(homogeneousHull 𝒜 I).toIdeal = ⨆ i, span (⇑(GradedRing.proj 𝒜 i) '' ↑I)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<GOAL>(homogeneousHull 𝒜 I).toIdeal = span (⋃ i, ⇑(GradedRing.proj 𝒜 i) '' ↑I)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>x✝ : A<GOAL>x✝ ∈ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r} ↔ x✝ ∈ ⋃ i, ⇑(GradedRing.proj 𝒜 i) '' ↑I
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>x y z : ℤ_[p]<VAR>hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)<GOAL>‖z‖ ≤ 1
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>μ : Measure E<VAR>s : Set ↑(sphere 0 1)<VAR>hs : MeasurableSet s<GOAL>μ.toSphere s = ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s s' : Set β<VAR>h : s ⊆ s'<VAR>h0 : ¬(ν a) (countablePartitionSet n x) = 0<GOAL>((κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal ≤ ((κ a) (countablePartitionSet n x ×ˢ s') / (ν a) (countablePartitionSet n x)).toReal