ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>G✝ : Type u_1<VAR>inst✝³ : NormedAddCommGroup G✝<VAR>inst✝² : NormedSpace 𝕜 G✝<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>G : Type u_2<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>c' : F →L[𝕜] G<VAR>d : 𝕜 → E →L[𝕜] F<VAR>d' : E →L[𝕜] F<VAR>u : 𝕜 → F<VAR>u' : F<VAR>hc : HasDerivAt c c' x<VAR>hu : HasDerivAt u u' x<GOAL>HasDerivAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') x
<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>G✝ : Type u_1<VAR>inst✝³ : NormedAddCommGroup G✝<VAR>inst✝² : NormedSpace 𝕜 G✝<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>G : Type u_2<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>c' : F →L[𝕜] G<VAR>d : 𝕜 → E →L[𝕜] F<VAR>d' : E →L[𝕜] F<VAR>u : 𝕜 → F<VAR>u' : F<VAR>hc : HasDerivAt c c' x<VAR>hu : HasDerivAt u u' x<VAR>this : HasDerivAt (fun y => (c y) (u y)) (((c x).comp (smulRight 1 u') + (smulRight 1 c').flip (u x)) 1) x<GOAL>HasDerivAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') x
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>hf : Measurable f<GOAL>MeasurableSet {p | p.2 = f p.1}
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>X : C<VAR>inst✝ : Simple X<VAR>Y Z : C<VAR>i : X ≅ Y ⊞ Z<GOAL>IsZero Y ∨ IsZero Z
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>X : C<VAR>inst✝ : Simple X<VAR>Y Z : C<VAR>i : X ≅ Y ⊞ Z<VAR>h : ¬IsZero Y<GOAL>IsZero Z
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>X : C<VAR>inst✝ : Simple X<VAR>Y Z : C<VAR>i : X ≅ Y ⊞ Z<VAR>h : ¬biprod.inl = 0<GOAL>IsZero Z
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>X : C<VAR>inst✝ : Simple X<VAR>Y Z : C<VAR>i : X ≅ Y ⊞ Z<VAR>h : biprod.inl ≠ 0<GOAL>IsZero Z
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>X : C<VAR>inst✝ : Simple X<VAR>Y Z : C<VAR>i : X ≅ Y ⊞ Z<VAR>h : biprod.inl ≠ 0<VAR>this : Simple (Y ⊞ Z)<GOAL>IsZero Z
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>X : C<VAR>inst✝ : Simple X<VAR>Y Z : C<VAR>i : X ≅ Y ⊞ Z<VAR>h : IsIso biprod.inl<VAR>this : Simple (Y ⊞ Z)<GOAL>IsZero Z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f✝¹ : α → β<VAR>μa μa' : Measure α<VAR>μb μb' : Measure β<VAR>μc : Measure γ<VAR>f✝ : α → β<VAR>f : α → α<VAR>hf : QuasiMeasurePreserving f μ μ<VAR>hs : f ⁻¹' s =ᵐ[μ] s<VAR>n : ℕ<VAR>ih : (preimage f)^[n] s =ᵐ[μ] s<GOAL>(preimage f)^[n + 1] s =ᵐ[μ] s
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f✝ : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedAddCommGroup R<VAR>inst✝ : Archimedean R<VAR>f : α → ℤ<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<GOAL>Tendsto (fun x => f x • r) l atTop
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f✝ : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedAddCommGroup R<VAR>inst✝ : Archimedean R<VAR>f : α → ℤ<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<VAR>s : R<GOAL>∀ᶠ (a : α) in l, s ≤ f a • r
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f✝ : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedAddCommGroup R<VAR>inst✝ : Archimedean R<VAR>f : α → ℤ<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<VAR>s : R<VAR>n : ℕ<VAR>hn : s ≤ n • r<GOAL>∀ᶠ (a : α) in l, s ≤ f a • r
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f✝ : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedAddCommGroup R<VAR>inst✝ : Archimedean R<VAR>f : α → ℤ<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<VAR>s : R<VAR>n : ℕ<VAR>hn : s ≤ ↑n • r<GOAL>∀ᶠ (a : α) in l, s ≤ f a • r
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : Module R M₃<VAR>φ : ι → Type i<VAR>inst✝⁵ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝⁴ : (i : ι) → Module R (φ i)<VAR>inst✝³ : Finite ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f g : ((i : ι) → φ i) →ₗ[R] M<VAR>h : ∀ (i : ι), f ∘ₗ single i = g ∘ₗ single i<GOAL>f = g
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : Module R M₃<VAR>φ : ι → Type i<VAR>inst✝⁵ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝⁴ : (i : ι) → Module R (φ i)<VAR>inst✝³ : Finite ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f g : ((i : ι) → φ i) →ₗ[R] M<VAR>h : ∀ (i : ι), f ∘ₗ single i = g ∘ₗ single i<VAR>i : ι<VAR>x : φ i<GOAL>f (Pi.single i x) = g (Pi.single i x)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_5, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.41266, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_4, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(F.shift n₀).map φ.hom₃ ≫ F.shiftMap T'.mor₃ n₀ n₁ ⋯ = F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁
<VAR>m n a✝ b✝ c d : ℤ<VAR>a b : ℕ<GOAL>↑a * a.gcdA b ≡ ↑(a.gcd b) [ZMOD ↑b]
<VAR>m n a✝ b✝ c d : ℤ<VAR>a b : ℕ<GOAL>↑a * a.gcdA b + 0 ≡ ↑a * a.gcdA b + ↑b * a.gcdB b [ZMOD ↑b]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝¹ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hs : μ (⋃ n, s n) ≠ 0<GOAL>∃ n, 0 < μ (s n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝¹ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), μ (s n) ≤ 0<GOAL>μ (⋃ n, s n) = 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>tensorObj : Mon_ C → Mon_ C → Mon_ C := fun M N => { X := M.X ⊗ N.X, one := (λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one), mul := tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul), one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }<VAR>X₁ Y₁ X₂ Y₂ : Mon_ C<VAR>f : X₁ ⟶ Y₁<VAR>g : X₂ ⟶ Y₂<GOAL>((λ_ (𝟙_ C)).inv ≫ (X₁.one ⊗ X₂.one)) ≫ (f.hom ⊗ g.hom) = (λ_ (𝟙_ C)).inv ≫ (Y₁.one ⊗ Y₂.one)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>tensorObj : Mon_ C → Mon_ C → Mon_ C := fun M N => { X := M.X ⊗ N.X, one := (λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one), mul := tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul), one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }<VAR>X₁ Y₁ X₂ Y₂ : Mon_ C<VAR>f : X₁ ⟶ Y₁<VAR>g : X₂ ⟶ Y₂<GOAL>(tensor_μ C (X₁.X, X₂.X) (X₁.X, X₂.X) ≫ (X₁.mul ⊗ X₂.mul)) ≫ (f.hom ⊗ g.hom) = ((f.hom ⊗ g.hom) ⊗ f.hom ⊗ g.hom) ≫ tensor_μ C (Y₁.X, Y₂.X) (Y₁.X, Y₂.X) ≫ (Y₁.mul ⊗ Y₂.mul)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>tensorObj : Mon_ C → Mon_ C → Mon_ C := fun M N => { X := M.X ⊗ N.X, one := (λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one), mul := tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul), one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }<VAR>X₁ Y₁ X₂ Y₂ : Mon_ C<VAR>f : X₁ ⟶ Y₁<VAR>g : X₂ ⟶ Y₂<GOAL>(tensor_μ C (X₁.X, X₂.X) (X₁.X, X₂.X) ≫ (X₁.mul ⊗ X₂.mul)) ≫ (f.hom ⊗ g.hom) = (tensor_μ C (X₁.X, X₂.X) (X₁.X, X₂.X) ≫ ((f.hom ⊗ f.hom) ⊗ g.hom ⊗ g.hom)) ≫ (Y₁.mul ⊗ Y₂.mul)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>tensorObj : Mon_ C → Mon_ C → Mon_ C := fun M N => { X := M.X ⊗ N.X, one := (λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one), mul := tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul), one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }<VAR>X₁ Y₁ X₂ Y₂ : Mon_ C<VAR>f : X₁ ⟶ Y₁<VAR>g : X₂ ⟶ Y₂<GOAL>tensor_μ C (X₁.X, X₂.X) (X₁.X, X₂.X) ≫ ((f.hom ⊗ f.hom) ⊗ g.hom ⊗ g.hom) ≫ (Y₁.mul ⊗ Y₂.mul) = (tensor_μ C (X₁.X, X₂.X) (X₁.X, X₂.X) ≫ ((f.hom ⊗ f.hom) ⊗ g.hom ⊗ g.hom)) ≫ (Y₁.mul ⊗ Y₂.mul)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>hX : Measurable X<VAR>hY : AEMeasurable Y μ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>lintegral (μ.restrict (X ⁻¹' t)) ((fun a => ((condDistrib Y X μ) a) s) ∘ X) = μ (X ⁻¹' t ∩ Y ⁻¹' s)
<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>h : IsKernelPair f a b<VAR>inst✝ : Mono f<GOAL>IsIso a
<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>h : IsKernelPair f a b<VAR>inst✝ : Mono f<GOAL>IsIso ((IsPullback.isLimit ⋯).conePointUniqueUpToIso (IsPullback.isLimit h)).inv
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact ↑U<VAR>f : ↑Γ(X, U)<GOAL>IsNilpotent f ↔ X.basicOpen f = ⊥
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact ↑U<VAR>f : ↑Γ(X, U)<VAR>hf : X.basicOpen f = ⊥<GOAL>IsNilpotent f
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact ↑U<VAR>f : ↑Γ(X, U)<VAR>hf : X.basicOpen f = ⊥<VAR>h : (1 |_ X.basicOpen f) ⋯ = 0<GOAL>IsNilpotent f
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact ↑U<VAR>f : ↑Γ(X, U)<VAR>hf : X.basicOpen f = ⊥<VAR>h : (1 |_ X.basicOpen f) ⋯ = 0<VAR>n : ℕ<VAR>hn : f ^ n * 1 = 0<GOAL>IsNilpotent f
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact ↑U<VAR>f : ↑Γ(X, U)<VAR>hf : X.basicOpen f = ⊥<VAR>h : (1 |_ X.basicOpen f) ⋯ = 0<VAR>n : ℕ<VAR>hn : f ^ n = 0<GOAL>IsNilpotent f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : CommMonoid α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : ContinuousMul α<VAR>inst✝ : T3Space α<VAR>f : β → γ → α<VAR>h : Multipliable (uncurry f)<VAR>h₁ : ∀ (b : β), Multipliable (f b)<VAR>h₂ : ∀ (c : γ), Multipliable fun b => f b c<GOAL>∏' (c : γ) (b : β), f b c = ∏' (b : β) (c : γ), f b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : CommMonoid α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : ContinuousMul α<VAR>inst✝ : T3Space α<VAR>f : β → γ → α<VAR>h : Multipliable (uncurry f)<VAR>h₁ : ∀ (b : β), Multipliable (f b)<VAR>h₂ : ∀ (c : γ), Multipliable fun b => f b c<GOAL>∏' (p : γ × β), uncurry f p.swap = ∏' (c : γ × β), uncurry f ((Equiv.prodComm γ β) c)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.30241, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>𝟙 S.X₂ ≫ S.g = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.30241, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>S.f ≫ 𝟙 S.X₂ = 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<VAR>f : (i : ι) → α i<GOAL>f ∈ (cylinder s S)ᶜ ↔ f ∈ cylinder s Sᶜ
<VAR>p x t : ℝ<GOAL>‖↑(t * x)‖ = |t| * ‖↑x‖
<VAR>p x t : ℝ<VAR>aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)<GOAL>‖↑(t * x)‖ = |t| * ‖↑x‖
<VAR>p x : ℝ<VAR>aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)<GOAL>‖↑(0 * x)‖ = |0| * ‖↑x‖
<VAR>p x t : ℝ<VAR>aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)<VAR>ht : t ≠ 0<GOAL>‖↑(t * x)‖ = |t| * ‖↑x‖
<VAR>p x t : ℝ<VAR>aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)<VAR>ht : t ≠ 0<VAR>ht' : |t| ≠ 0<GOAL>‖↑(t * x)‖ = |t| * ‖↑x‖
<VAR>p x t : ℝ<VAR>aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)<VAR>ht : t ≠ 0<VAR>ht' : |t| ≠ 0<GOAL>sInf ((fun a => |a|) '' {m | ↑m = ↑(t * x)}) = |t| * sInf ((fun a => |a|) '' {m | ↑m = ↑x})
<VAR>p x t : ℝ<VAR>aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)<VAR>ht : t ≠ 0<VAR>ht' : |t| ≠ 0<GOAL>sInf ((fun a => |a|) '' {m | ↑m = ↑(t * x)}) = sInf (|t| • (fun a => |a|) '' {m | ↑m = ↑x})
<VAR>p x t : ℝ<VAR>aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)<VAR>ht : t ≠ 0<VAR>ht' : |t| ≠ 0<GOAL>sInf ((fun a => |a|) '' {m | m - t * x ∈ zmultiples (t * p)}) = sInf (|t| • (fun a => |a|) '' {m | m - x ∈ zmultiples p})
<VAR>p x t : ℝ<VAR>aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)<VAR>ht : t ≠ 0<VAR>ht' : |t| ≠ 0<VAR>z : ℝ<GOAL>z ∈ (fun a => |a|) '' {m | m - t * x ∈ zmultiples (t * p)} ↔ z ∈ |t| • (fun a => |a|) '' {m | m - x ∈ zmultiples p}
<VAR>p x t : ℝ<VAR>aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)<VAR>ht : t ≠ 0<VAR>ht' : |t| ≠ 0<VAR>z : ℝ<GOAL>z ∈ (fun a => |a|) '' {m | m - t * x ∈ zmultiples (t * p)} ↔ |t|⁻¹ • z ∈ (fun a => |a|) '' {m | m - x ∈ zmultiples p}
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A B : M<VAR>h : Commute A B<VAR>n : ℕ<GOAL>(A * B) ^ ↑n = A ^ ↑n * B ^ ↑n
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A B : M<VAR>h : Commute A B<VAR>n : ℕ<GOAL>(A * B) ^ -[n+1] = A ^ -[n+1] * B ^ -[n+1]
<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>a : α<VAR>x : γ<VAR>s : Set β<GOAL>0 ≤ κ.density ν a x 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>a : α<VAR>x : γ<VAR>s : Set β<GOAL>∃ᶠ (x_1 : ℕ) in atTop, 0 ≤ κ.densityProcess ν x_1 a x 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>a : α<VAR>x : γ<VAR>s : Set β<GOAL>IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun n => κ.densityProcess ν n a x s
<VAR>s n step : Nat<GOAL>range' s (n + 1) step = s :: range' (s + step) n step
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<VAR>h : M.E = E ∧ M.Indep E<GOAL>M = freeOn E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<VAR>h : M.E = E ∧ M.Indep E<GOAL>∀ I ⊆ E, M.Indep I ↔ I ⊆ E
<VAR>α : Type u_1<VAR>f : α → α<VAR>a : α<VAR>n : ℕ<VAR>b : α<GOAL>b ∈ iterate f a n ↔ ∃ m < n, b = f^[m] a
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝³ : CommRing A<VAR>inst✝² : Module A M<VAR>κ : Type u_6<VAR>inst✝¹ : Fintype κ<VAR>inst✝ : Subsingleton M<VAR>f : M →ₗ[R] M<VAR>b : Basis (Fin 0) R M<GOAL>LinearMap.det f = 1
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝³ : CommRing A<VAR>inst✝² : Module A M<VAR>κ : Type u_6<VAR>inst✝¹ : Fintype κ<VAR>inst✝ : Subsingleton M<VAR>f : M →ₗ[R] M<VAR>b : Basis (Fin 0) R M<GOAL>((toMatrix b b) f).det = 1
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>(p + q).support ⊆ p.support ∪ q.support
<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₁ f₂ : α → E'<VAR>g₁ g₂ : α → F'<VAR>h₁ : IsBigOWith c₁ l f₁ g<VAR>h₂ : IsBigOWith c₂ l f₂ g<GOAL>IsBigOWith (c₁ + c₂) l (fun x => f₁ x - f₂ x) g
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>f : k⟦X⟧<VAR>hf : f ≠ 0<GOAL>Inv_divided_by_X_pow_order hf * divided_by_X_pow_order hf = 1
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>f : k⟦X⟧<VAR>hf : f ≠ 0<GOAL>divided_by_X_pow_order hf * Inv_divided_by_X_pow_order hf = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<GOAL>l ≤ cofinite ↔ ∀ (x : α), {x}ᶜ ∈ l
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>h : ∀ (x : α), {x}ᶜ ∈ l<VAR>s : Set α<VAR>hs : sᶜ.Finite<GOAL>s ∈ l
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>h : ∀ (x : α), {x}ᶜ ∈ l<VAR>s : Set α<VAR>hs : sᶜ.Finite<GOAL>∀ i ∈ sᶜ, {i}ᶜ ∈ l
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<GOAL>1 ≤ ↑r ↔ 1 ≤ r
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H H' : G.Subgraph<VAR>hle : ∀ (v w : V), H.Adj v w → H'.Adj v w<VAR>hv : H.verts = H'.verts<VAR>h : H.Connected<GOAL>H'.Connected
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>x y : 𝕎 R<GOAL>verschiebung (x * frobenius y) = verschiebung x * y
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>x y : 𝕎 R<VAR>this : IsPoly₂ p fun {R} [CommRing R] x y => verschiebung (x * frobenius y)<GOAL>verschiebung (x * frobenius y) = verschiebung x * y
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>x y : 𝕎 R<VAR>this✝ : IsPoly₂ p fun {R} [CommRing R] x y => verschiebung (x * frobenius y)<VAR>this : IsPoly₂ p fun {R} [CommRing R] x y => verschiebung x * y<GOAL>verschiebung (x * frobenius y) = verschiebung x * y
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>this✝ : IsPoly₂ p fun {R} [CommRing R] x y => verschiebung (x * frobenius y)<VAR>this : IsPoly₂ p fun {R} [CommRing R] x y => verschiebung x * y<VAR>R : Type u_1<VAR>R._inst : CommRing R<VAR>x y : 𝕎 R<GOAL>∀ (n : ℕ), (ghostComponent n) (verschiebung (x * frobenius y)) = (ghostComponent n) (verschiebung x * y)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>a = n.sqrt ↔ a ^ 2 ≤ n ∧ n < (a + 1) ^ 2
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>X₁ X₂ : C<VAR>inst✝¹ : HasBinaryProduct X₁ X₂<VAR>inst✝ : PreservesLimit (pair X₁ X₂) (forget C)<VAR>x : (forget C).obj X₁ × (forget C).obj X₂<GOAL>prod.fst ((prodEquiv X₁ X₂).symm x) = x.1
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>X₁ X₂ : C<VAR>inst✝¹ : HasBinaryProduct X₁ X₂<VAR>inst✝ : PreservesLimit (pair X₁ X₂) (forget C)<VAR>y : (forget C).obj (X₁ ⨯ X₂)<GOAL>prod.fst ((prodEquiv X₁ X₂).symm ((prodEquiv X₁ X₂) y)) = ((prodEquiv X₁ X₂) y).1
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>a < c / b ↔ a * b < c
<VAR>ι : Type u_1<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Fintype ι<VAR>x : EuclideanSpace ℝ ι<VAR>r : ℝ<GOAL>volume (Metric.ball x r) = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Fintype ι<VAR>x : EuclideanSpace ℝ ι<VAR>r : ℝ<VAR>hr : r ≤ 0<GOAL>volume (Metric.ball x r) = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Fintype ι<VAR>x : EuclideanSpace ℝ ι<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>volume (Metric.ball x r) = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>αs : ι → Type u_13<VAR>inst✝ : Zero M<VAR>l : (i : ι) × αs i →₀ M<GOAL>l.support = l.splitSupport.sigma fun i => (l.split i).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>αs : ι → Type u_13<VAR>inst✝ : Zero M<VAR>l : (i : ι) × αs i →₀ M<GOAL>∀ (a : ι) (b : αs a), ⟨a, b⟩ ∈ l.support ↔ (∃ a_1 ∈ l.support, a_1.fst = a) ∧ ⟨a, b⟩ ∈ l.support
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group H<VAR>inst✝¹ : MulAction G α<VAR>a : G<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>a ∈ stabilizer G s ↔ s ⊆ a • s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<GOAL>LpAddConst p = 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<GOAL>p ∉ Set.Ioo 0 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>h : p ∈ Set.Ioo 0 1<GOAL>False
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t✝ : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>s t : Set X<GOAL>frontier (s ∪ t) ⊆ frontier s ∩ closure tᶜ ∪ closure sᶜ ∩ frontier t
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>hx : AlgebraicIndependent R x<GOAL>AlgebraicIndependent R Subtype.val
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s₁✝ s₂✝ : Finmap β<VAR>s₁ s₂ : AList β<VAR>h : ∀ (x : α), lookup x ⟦s₁⟧ = lookup x ⟦s₂⟧<GOAL>⟦s₁⟧ = ⟦s₂⟧