ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>ι : Type u_10<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : Zero R<VAR>inst✝¹ : Zero M<VAR>inst✝ : SMulWithZero R M<VAR>s : ι → X → R<VAR>h✝ : LocallyFinite fun i => support (s i)<VAR>f : ι → X → M<VAR>i : ι<VAR>x : X<VAR>h : s i x = 0<GOAL>(s i • f i) x = 0
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : MonoidalCategory D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : MonoidalCategory E<VAR>F : LaxMonoidalFunctor C D<VAR>G : LaxMonoidalFunctor D E<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>X' : C<GOAL>__src✝.map f ▷ __src✝.obj X' ≫ (fun X Y => G.μ (F.obj X) (F.obj Y) ≫ G.map (F.μ X Y)) Y X' = (fun X Y => G.μ (F.obj X) (F.obj Y) ≫ G.map (F.μ X Y)) X X' ≫ __src✝.map (f ▷ X')
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : MonoidalCategory D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : MonoidalCategory E<VAR>F : LaxMonoidalFunctor C D<VAR>G : LaxMonoidalFunctor D E<VAR>X Y f : C<VAR>X' : X ⟶ Y<GOAL>__src✝.obj f ◁ __src✝.map X' ≫ (fun X Y => G.μ (F.obj X) (F.obj Y) ≫ G.map (F.μ X Y)) f Y = (fun X Y => G.μ (F.obj X) (F.obj Y) ≫ G.map (F.μ X Y)) f X ≫ __src✝.map (f ◁ X')
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : MonoidalCategory D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : MonoidalCategory E<VAR>F : LaxMonoidalFunctor C D<VAR>G : LaxMonoidalFunctor D E<VAR>X Y Z : C<GOAL>(G.μ (F.obj X) (F.obj Y) ≫ G.map (F.μ X Y)) ▷ G.obj (F.obj Z) ≫ (G.μ (F.obj (X ⊗ Y)) (F.obj Z) ≫ G.map (F.μ (X ⊗ Y) Z)) ≫ G.map (F.map (α_ X Y Z).hom) = (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom ≫ G.obj (F.obj X) ◁ (G.μ (F.obj Y) (F.obj Z) ≫ G.map (F.μ Y Z)) ≫ G.μ (F.obj X) (F.obj (Y ⊗ Z)) ≫ G.map (F.μ X (Y ⊗ Z))
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : MonoidalCategory D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : MonoidalCategory E<VAR>F : LaxMonoidalFunctor C D<VAR>G : LaxMonoidalFunctor D E<VAR>X Y Z : C<GOAL>G.μ (F.obj X) (F.obj Y) ▷ G.obj (F.obj Z) ≫ G.μ (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (F.μ X Y ▷ F.obj Z) ≫ G.map (F.μ (X ⊗ Y) Z) ≫ G.map (F.map (α_ X Y Z).hom) = (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom ≫ G.obj (F.obj X) ◁ G.μ (F.obj Y) (F.obj Z) ≫ G.μ (F.obj X) (F.obj Y ⊗ F.obj Z) ≫ G.map (F.obj X ◁ F.μ Y Z) ≫ G.map (F.μ X (Y ⊗ Z))
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : MonoidalCategory D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : MonoidalCategory E<VAR>F : LaxMonoidalFunctor C D<VAR>G : LaxMonoidalFunctor D E<VAR>X Y Z : C<GOAL>G.μ (F.obj X) (F.obj Y) ▷ G.obj (F.obj Z) ≫ G.μ (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (F.μ X Y ▷ F.obj Z) ≫ G.map (F.μ (X ⊗ Y) Z) ≫ G.map (F.map (α_ X Y Z).hom) = ((G.μ (F.obj X) (F.obj Y) ▷ G.obj (F.obj Z) ≫ G.μ (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) ≫ G.map (F.obj X ◁ F.μ Y Z)) ≫ G.map (F.μ X (Y ⊗ Z))
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CharP R 2<VAR>s : Finset ι<VAR>f : ι → R<GOAL>(∑ i ∈ s, f i) * ∑ i ∈ s, f i = ∑ i ∈ s, f i * f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : (α → ℕ) → ℤ<VAR>hf : IsPoly f<VAR>hg : IsPoly g<GOAL>IsPoly (f + g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : (α → ℕ) → ℤ<VAR>hf : IsPoly f<VAR>hg : IsPoly g<GOAL>IsPoly (f - -g)
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : CommSemiring α<VAR>inst✝² : LinearOrder α<VAR>a b✝ c✝ d : α<VAR>inst✝¹ : PosMulMono α<VAR>inst✝ : MulPosMono α<VAR>b c : α<VAR>ha : 0 ≤ a<VAR>hd : 0 ≤ d<VAR>ba : b * a ≤ max d b * max c a<VAR>cd : c * d ≤ max a c * max b d<GOAL>a * b ≤ max a c * max d b
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : CommSemiring α<VAR>inst✝² : LinearOrder α<VAR>a b✝ c✝ d : α<VAR>inst✝¹ : PosMulMono α<VAR>inst✝ : MulPosMono α<VAR>b c : α<VAR>ha : 0 ≤ a<VAR>hd : 0 ≤ d<VAR>ba : b * a ≤ max d b * max c a<VAR>cd : c * d ≤ max a c * max b d<GOAL>d * c ≤ max a c * max d b
<VAR>n✝ : ℕ<VAR>c : Composition n✝<VAR>n : ℕ<VAR>h : 0 < n<VAR>i : Fin (single n h).length<GOAL>(single n h).blocksFun i = n
<VAR>p : ℝ[X]<GOAL>Tendsto (fun x => eval x p / rexp x) atTop (𝓝 0)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<GOAL>(bind₁ (frobeniusPoly p)) (wittPolynomial p ℤ n) = wittPolynomial p ℤ (n + 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<GOAL>(MvPolynomial.map (Int.castRingHom ℚ)) ((bind₁ (frobeniusPoly p)) (wittPolynomial p ℤ n)) = (MvPolynomial.map (Int.castRingHom ℚ)) (wittPolynomial p ℤ (n + 1))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasBinaryProducts C<VAR>X Y Z : C<GOAL>(α_ X Y Z).inv ≫ prod.fst ≫ prod.snd = prod.snd ≫ prod.fst
<VAR>α : Type u_1<VAR>inst✝ : PartialOrder α<VAR>s : Set α<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>¬(s ∩ Icc x y).OrdConnected ↔ ∃ z ∉ s, z ∈ Ioo x y
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>r : Rˣ<VAR>a : Aˣ<VAR>h : ↑r ∈ resolventSet R ↑a<GOAL>↑r⁻¹ ∈ resolventSet R ↑a⁻¹
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>r : Rˣ<VAR>a : Aˣ<VAR>h : IsUnit (r • 1 - ↑a)<GOAL>IsUnit (r⁻¹ • 1 - ↑a⁻¹)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>r : Rˣ<VAR>a : Aˣ<VAR>h : IsUnit (r • 1 - ↑a)<GOAL>IsUnit (r • ↑a⁻¹ - 1)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>r : Rˣ<VAR>a : Aˣ<VAR>h : IsUnit (r • 1 - ↑a)<VAR>h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a<GOAL>IsUnit (r • ↑a⁻¹ - 1)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>r : Rˣ<VAR>a : Aˣ<VAR>h : IsUnit (r • 1 - ↑a)<VAR>h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a<VAR>h₂ : (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a<GOAL>IsUnit (r • ↑a⁻¹ - 1)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>r : Rˣ<VAR>a : Aˣ<VAR>h : IsUnit (r • 1 - ↑a)<VAR>h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a<VAR>h₂ : (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a<VAR>hcomm : Commute (↑a) (r • ↑a⁻¹ - 1)<GOAL>IsUnit (r • ↑a⁻¹ - 1)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : LocalRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : LocalRing S<VAR>inst✝¹ : CommRing T<VAR>inst✝ : LocalRing T<VAR>x : R<GOAL>(residue R) x = 0 ↔ x ∈ maximalIdeal R
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>ε : ℚ<VAR>hε : 0 < ε<GOAL>∃ N, ∀ i ≥ N, (f - const (padicNorm p) (↑f i)).norm < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm<GOAL>False
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε<GOAL>False
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε<VAR>i : ℕ<VAR>hi : i ≥ N<VAR>hge : ε ≤ (f - const (padicNorm p) (↑f i)).norm<GOAL>False
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε<VAR>i : ℕ<VAR>hi : i ≥ N<VAR>hge : ε ≤ (f - const (padicNorm p) (↑f i)).norm<VAR>hne : ¬f - const (padicNorm p) (↑f i) ≈ 0<GOAL>False
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε<VAR>i : ℕ<VAR>hi : i ≥ N<VAR>hne : ¬f - const (padicNorm p) (↑f i) ≈ 0<VAR>hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))<GOAL>False
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε<VAR>i : ℕ<VAR>hi : i ≥ N<VAR>hne : ¬f - const (padicNorm p) (↑f i) ≈ 0<VAR>hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))<GOAL>ε > padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Ring α<VAR>inst✝⁴ : LinearOrder α<VAR>a b : α<VAR>inst✝³ : PosMulStrictMono α<VAR>inst✝² : MulPosStrictMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 ≤ a * b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Ring α<VAR>inst✝⁴ : LinearOrder α<VAR>a b : α<VAR>inst✝³ : PosMulStrictMono α<VAR>inst✝² : MulPosStrictMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>(0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<VAR>n : ℕ∞<GOAL>ContDiff 𝕜 n f ↔ ∀ (i : ι), ContDiff 𝕜 n fun x => f x i
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<VAR>n : ℕ∞<GOAL>(∀ (i : ι), ContDiff 𝕜 n fun x => (⇑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) ↔ ∀ (i : ι), ContDiff 𝕜 n fun x => f x i
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>n : ℕ<VAR>m : M<VAR>a : α<GOAL>m ^ (period m a + n) • a = m ^ n • a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝² : Ring R<VAR>p✝ q : R[X]<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p : R[X]<VAR>a : R<GOAL>(fun h => Nat.find ⋯) = fun h => Nat.find ⋯
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝² : Ring R<VAR>p✝ q : R[X]<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p : R[X]<VAR>a : R<VAR>x✝ : ¬p = 0<GOAL>Nat.find ⋯ = Nat.find ⋯
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x : K<VAR>hx : x ≠ 0<GOAL>Associated (num A x) ↑(den A x⁻¹)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x : K<VAR>hx : x ≠ 0<VAR>this : Associated (num A x⁻¹⁻¹) ↑(den A x⁻¹)<GOAL>Associated (num A x) ↑(den A x⁻¹)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x : K<VAR>hx : x ≠ 0<VAR>this : Associated (num A x) ↑(den A x⁻¹)<GOAL>Associated (num A x) ↑(den A x⁻¹)
<VAR>G : Type u<VAR>inst✝¹ : Monoid G<VAR>H : Type u_1<VAR>inst✝ : Monoid H<VAR>e : G →* H<VAR>e_inj : Function.Injective ⇑e<VAR>g : G<GOAL>e (g ^ exponent H) = e 1
<VAR>z : ℂ<VAR>hz : 0 < z.re<GOAL>ContinuousAt (fun x => x.1 ^ x.2) (0, z)
<VAR>z : ℂ<VAR>hz : 0 < z.re<VAR>hz₀ : z ≠ 0<GOAL>ContinuousAt (fun x => x.1 ^ x.2) (0, z)
<VAR>z : ℂ<VAR>hz : 0 < z.re<VAR>hz₀ : z ≠ 0<GOAL>Tendsto (fun x => ‖x.1 ^ x.2‖) (𝓝 (0, z)) (𝓝 0)
<VAR>z : ℂ<VAR>hz : 0 < z.re<VAR>hz₀ : z ≠ 0<GOAL>Tendsto (fun x => abs x.1 ^ x.2.re / rexp (x.1.arg * x.2.im)) (𝓝 (0, z)) (𝓝 0)
<VAR>z : ℂ<VAR>hz : 0 < z.re<VAR>hz₀ : z ≠ 0<GOAL>Tendsto (fun x => abs x.1 ^ x.2.re * rexp (-(x.1.arg * x.2.im))) (𝓝 (0, z)) (𝓝 0)
<VAR>z : ℂ<VAR>hz : 0 < z.re<VAR>hz₀ : z ≠ 0<GOAL>Tendsto (fun x => abs x.1 ^ x.2.re) (𝓝 (0, z)) (𝓝 0)
<VAR>z : ℂ<VAR>hz : 0 < z.re<VAR>hz₀ : z ≠ 0<GOAL>IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝 (0, z)) ((fun x => ‖x‖) ∘ fun x => rexp (-(x.1.arg * x.2.im)))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>hs : s.OrdConnected<GOAL>volume (frontier s) = 0
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>hs : s.OrdConnected<GOAL>volume (frontier (↑(upperClosure s) ∩ ↑(lowerClosure s))) = 0
<VAR>α : Type u_1<VAR>α₁ : Type u_2<VAR>α₂ : Type u_3<VAR>β : α → Type u_4<VAR>β₁ : α₁ → Type u_5<VAR>β₂ : α₂ → Type u_6<VAR>f₁ : α₁ → α₂<VAR>f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)<VAR>h₁ : Surjective f₁<VAR>h₂ : ∀ (a : α₁), Surjective (f₂ a)<GOAL>Surjective (Sigma.map f₁ f₂)
<VAR>α : Type u_1<VAR>α₁ : Type u_2<VAR>α₂ : Type u_3<VAR>β : α → Type u_4<VAR>β₁ : α₁ → Type u_5<VAR>β₂ : α₂ → Type u_6<VAR>f₁ : α₁ → α₂<VAR>f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)<VAR>h₁ : Surjective f₁<VAR>h₂ : ∀ (a : α₁), Surjective (f₂ a)<GOAL>∀ (x : α₁) (b : β₂ (f₁ x)), ∃ a, Sigma.map f₁ f₂ a = ⟨f₁ x, b⟩
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>g : β → γ<VAR>f : α → β<VAR>l : List α<VAR>n✝ : ℕ<VAR>a✝ : γ<GOAL>a✝ ∈ ((map g ∘ map f) l)[n✝]? ↔ a✝ ∈ (map (g ∘ f) l)[n✝]?
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<GOAL>Perm ∘r Perm = Perm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a✝ : α<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>a c : List α<GOAL>(Perm ∘r Perm) a c = (a ~ c)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s✝ : Set E<VAR>x✝ : E<VAR>s : Set F<VAR>hs : Convex 𝕜 s<VAR>f : E →ₗ[𝕜] F<VAR>x : E<VAR>hx : x ∈ ⇑f ⁻¹' s<VAR>y : E<VAR>hy : y ∈ ⇑f ⁻¹' s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ ⇑f ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s✝ : Set E<VAR>x✝ : E<VAR>s : Set F<VAR>hs : Convex 𝕜 s<VAR>f : E →ₗ[𝕜] F<VAR>x : E<VAR>hx : x ∈ ⇑f ⁻¹' s<VAR>y : E<VAR>hy : y ∈ ⇑f ⁻¹' s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • f x + b • f y ∈ s
<VAR>cmp✝ : ?m.2679 → ?m.2679 → Ordering<VAR>inst✝¹ : TransCmp cmp✝<VAR>x✝ : Sort ?u.2677<VAR>cmp : x✝ → x✝ → Ordering<VAR>inst✝ : TransCmp cmp<VAR>x y z : x✝<VAR>h₁ : cmp x y ≠ Ordering.lt<VAR>h₂ : cmp y z ≠ Ordering.lt<GOAL>cmp x z ≠ Ordering.lt
<VAR>cmp✝ : ?m.2679 → ?m.2679 → Ordering<VAR>inst✝¹ : TransCmp cmp✝<VAR>x✝ : Sort ?u.2677<VAR>cmp : x✝ → x✝ → Ordering<VAR>inst✝ : TransCmp cmp<VAR>x y z : x✝<VAR>h₁ : cmp x y ≠ Ordering.lt<VAR>h₂ : cmp y z ≠ Ordering.lt<VAR>this : cmp z y ≠ Ordering.gt → cmp y x ≠ Ordering.gt → cmp z x ≠ Ordering.gt<GOAL>cmp x z ≠ Ordering.lt
<VAR>cmp✝ : ?m.2679 → ?m.2679 → Ordering<VAR>inst✝¹ : TransCmp cmp✝<VAR>x✝ : Sort ?u.2677<VAR>cmp : x✝ → x✝ → Ordering<VAR>inst✝ : TransCmp cmp<VAR>x y z : x✝<VAR>h₁ : ¬cmp x y = Ordering.lt<VAR>h₂ : ¬cmp y z = Ordering.lt<VAR>this : ¬cmp y z = Ordering.lt → ¬cmp x y = Ordering.lt → ¬cmp x z = Ordering.lt<GOAL>¬cmp x z = Ordering.lt
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>inst✝¹ : CommRing T<VAR>inst✝ : Algebra R T<VAR>h : IsAdjoinRoot S f<VAR>h' : IsAdjoinRoot T f<GOAL>(h.aequiv h') h.root = h'.root
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x y y' : M<GOAL>polar (⇑Q) x (y - y') = polar (⇑Q) x y - polar (⇑Q) x y'
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<GOAL>toDFinsupp s ≤ toDFinsupp t ↔ s ≤ t
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>h : Disjoint s t<VAR>hs : MeasurableSet s<GOAL>μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁸ : Category.{u_14, u_1} C₁<VAR>inst✝⁷ : Category.{u_13, u_2} C₂<VAR>inst✝⁶ : Category.{u_12, u_3} C₃<VAR>inst✝⁵ : Category.{u_11, u_4} C₄<VAR>inst✝⁴ : Category.{u_15, u_5} C₁₂<VAR>inst✝³ : Category.{?u.187592, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂<VAR>G : C₁₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₁₂ : BifunctorComp₁₂IndexData r<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝² : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p<VAR>inst✝¹ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q<VAR>H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃<VAR>inst✝ : ((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<GOAL>ιMapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ (CofanMapObjFun.iso (isColimitCofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)).inv = ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>(insert t ↑(hC.diffFinset hs ht)).PairwiseDisjoint id
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>h : (↑(hC.diffFinset hs ht)).PairwiseDisjoint id<GOAL>(insert t ↑(hC.diffFinset hs ht)).PairwiseDisjoint id
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>h : (↑(hC.diffFinset hs ht)).PairwiseDisjoint id<VAR>u : Set α<VAR>hu : u ∈ ↑(hC.diffFinset hs ht)<GOAL>Disjoint (id t) (id u)
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>h : (↑(hC.diffFinset hs ht)).PairwiseDisjoint id<VAR>u : Set α<VAR>hu : u ∈ ↑(hC.diffFinset hs ht)<GOAL>Disjoint t u
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>h : (↑(hC.diffFinset hs ht)).PairwiseDisjoint id<VAR>u : Set α<VAR>hu : u ∈ ↑(hC.diffFinset hs ht)<GOAL>u ≤ ⋃₀ ↑(hC.diffFinset hs ht)
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>h : (↑(hC.diffFinset hs ht)).PairwiseDisjoint id<VAR>u : Set α<VAR>hu : u ∈ ↑(hC.diffFinset hs ht)<GOAL>u ⊆ ⋃₀ ↑(hC.diffFinset hs ht)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ✝ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ✝<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f✝ f' : α → β → γ✝<VAR>g✝ g'✝ : α → β → γ✝ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u✝ u' : Finset γ✝<VAR>a a' : α<VAR>b b' : β<VAR>c : γ✝<VAR>γ : Type u_14<VAR>u : Finset γ<VAR>f : δ → γ → ε<VAR>g : α → β → δ<VAR>f₁ : α → γ → α'<VAR>f₂ : β → γ → β'<VAR>g' : α' → β' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)<GOAL>image2 f (image2 g ↑s ↑t) ↑u ⊆ image2 g' (image2 f₁ ↑s ↑u) (image2 f₂ ↑t ↑u)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : SMul αᵐᵒᵖ β<VAR>inst✝¹ : SMul β γ<VAR>inst✝ : SMul α γ<VAR>a : α<VAR>s : Set β<VAR>t : Set γ<VAR>h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c<VAR>x✝ : γ<GOAL>x✝ ∈ (op a • s) • t ↔ x✝ ∈ s • a • t
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝² : Preorder ι<VAR>G : ι → Type w<VAR>inst✝¹ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>α : Type u_1<VAR>x : α → Σˣ f<VAR>i j : ι<VAR>ij : i ≤ j<VAR>h : i ∈ upperBounds (range (Sigma.fst ∘ x))<VAR>a : α<GOAL>(⇑(f i j ij) ∘ unify f x i h) a = unify f x j ⋯ a
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x✝ y : E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<VAR>x : E<GOAL>s / closedBall x δ = x⁻¹ • cthickening δ s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>ι : Type u_3<VAR>p : ι → Ideal R<VAR>S : Finset ι<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<VAR>q : ι → R<VAR>hq : (↑S).Pairwise (IsCoprime on q)<GOAL>⨆ i ∈ S, torsionBy R M (q i) = torsionBy R M (∏ i ∈ S, q i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>ι : Type u_3<VAR>p : ι → Ideal R<VAR>S : Finset ι<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<VAR>q : ι → R<VAR>hq : (↑S).Pairwise (IsCoprime on q)<GOAL>⨆ i ∈ S, torsionBy R M (q i) = ⨆ i ∈ S, torsionBySet R M ↑(Ideal.span {q i})
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>ι : Type u_3<VAR>p : ι → Ideal R<VAR>S : Finset ι<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<VAR>q : ι → R<VAR>hq : (↑S).Pairwise (IsCoprime on q)<GOAL>(↑S).Pairwise fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<GOAL>(convexHull 𝕜) s = ⋂ t, ⋂ (_ : s ⊆ t), ⋂ (_ : Convex 𝕜 t), t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderClosedTopology α<VAR>f g : β → α<VAR>inst✝ : TopologicalSpace β<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>frontier {b | f b ≤ g b} ⊆ {b | f b = g b}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderClosedTopology α<VAR>f g : β → α<VAR>inst✝ : TopologicalSpace β<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>{b | f b ≤ g b} ∩ closure {b | f b ≤ g b}ᶜ ⊆ {b | f b = g b}