ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<GOAL>1 < s.card ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<GOAL>(∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
<VAR>n p : ℕ<VAR>hp : Prime p<VAR>a b : ℤ<VAR>h : ↑p ∣ a * b<GOAL>↑p ∣ a ∨ ↑p ∣ b
<VAR>n p : ℕ<VAR>hp : Prime p<VAR>a b : ℤ<VAR>h : p ∣ a.natAbs ∨ p ∣ b.natAbs<GOAL>↑p ∣ a ∨ ↑p ∣ b
<VAR>n p : ℕ<VAR>hp : _root_.Prime ↑p<VAR>h : p = 1<GOAL>False
<VAR>n p : ℕ<VAR>hp : _root_.Prime ↑p<VAR>a b : ℕ<GOAL>p ∣ a * b → p ∣ a ∨ p ∣ b
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>inst✝² : DecidablePred p<VAR>H : ∃ n, p n<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h₁ : ∃ n, p n<VAR>h₂ : ∃ n, p (n + 1)<VAR>h0 : ¬p 0<GOAL>Nat.find h₁ = Nat.find h₂ + 1
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>inst✝² : DecidablePred p<VAR>H : ∃ n, p n<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h₁ : ∃ n, p n<VAR>h₂ : ∃ n, p (n + 1)<VAR>h0 : ¬p 0<VAR>n : ℕ<VAR>hn : n < Nat.find h₂ + 1<GOAL>¬p n
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>inst✝² : DecidablePred p<VAR>H : ∃ n, p n<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h₁ : ∃ n, p n<VAR>h₂ : ∃ n, p (n + 1)<VAR>h0 : ¬p 0<VAR>hn : 0 < Nat.find h₂ + 1<GOAL>¬p 0
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>inst✝² : DecidablePred p<VAR>H : ∃ n, p n<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h₁ : ∃ n, p n<VAR>h₂ : ∃ n, p (n + 1)<VAR>h0 : ¬p 0<VAR>n✝ : ℕ<VAR>hn : n✝ + 1 < Nat.find h₂ + 1<GOAL>¬p (n✝ + 1)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<GOAL>hζ.integralPowerBasis.dim = φ (↑p ^ k)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>γ : Sort u_3<VAR>t : γ → Set (ProjectiveSpectrum 𝒜)<GOAL>(vanishingIdeal (⋃ i, t i)).toIdeal = (⨅ i, vanishingIdeal (t i)).toIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>γ : Sort u_3<VAR>t : γ → Set (ProjectiveSpectrum 𝒜)<GOAL>(⨅ i, vanishingIdeal (t i)).toIdeal = ⨅ i, (vanishingIdeal (t i)).toIdeal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → ℝ≥0∞<VAR>a : α<GOAL>∫⁻ (x : α) in {a}, f x ∂μ = f a * μ {a}
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : F.IsEquivalence<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>F.map (F.inv.map f) = F.asEquivalence.counit.app X ≫ f ≫ F.asEquivalence.counitInv.app Y
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : F.IsEquivalence<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>F.map (F.inv.map f) = (F.asEquivalence.inverse ⋙ F.asEquivalence.functor).map f
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : Semiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>I : Ideal C(X, R)<VAR>x : X<GOAL>x ∈ setOfIdeal I ↔ ∃ f ∈ I, f x ≠ 0
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : Semiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>I : Ideal C(X, R)<VAR>x : X<GOAL>(¬∀ f ∈ I, f x = 0) ↔ ∃ f ∈ I, f x ≠ 0
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : Semiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>I : Ideal C(X, R)<VAR>x : X<GOAL>(∃ f ∈ I, f x ≠ 0) ↔ ∃ f ∈ I, f x ≠ 0
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m n : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : Integrable f' volume<VAR>hbot : Tendsto f atBot (𝓝 m)<VAR>htop : Tendsto f atTop (𝓝 n)<GOAL>∫ (x : ℝ), f' x = n - m
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m n : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : Integrable f' volume<VAR>hbot : Tendsto f atBot (𝓝 m)<VAR>htop : Tendsto f atTop (𝓝 n)<GOAL>f 0 - m + (n - f 0) = n - m
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>x y : α<VAR>inst✝² : BEq α<VAR>inst✝¹ : LawfulBEq α<VAR>inst✝ : BEqCmp cmp<GOAL>cmp x y = Ordering.eq ↔ x = y
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>w x y z : R<GOAL>span {w, x} * span {y, z} = span {w * y, w * z, x * y, x * z}
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰✝ : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g✝ : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰✝.J), HasPullback (𝒰✝.map i ≫ f✝) g✝<VAR>s : PullbackCone f✝ g✝<VAR>𝒰 : Y.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(pullback f g).OpenCover
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰✝ : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g✝ : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰✝.J), HasPullback (𝒰✝.map i ≫ f✝) g✝<VAR>s : PullbackCone f✝ g✝<VAR>𝒰 : Y.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>∀ (i : 𝒰.J), pullback.map f (𝒰.map i ≫ g) f g (𝟙 X) (𝒰.map i) (𝟙 Z) ⋯ ⋯ = (pullbackSymmetry f (𝒰.map i ≫ g)).hom ≫ ((openCoverOfLeft 𝒰 g f).pushforwardIso (pullbackSymmetry g f).hom).map ((Equiv.refl 𝒰.J) i)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰✝ : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g✝ : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰✝.J), HasPullback (𝒰✝.map i ≫ f✝) g✝<VAR>s : PullbackCone f✝ g✝<VAR>𝒰 : Y.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>i : 𝒰.J<GOAL>pullback.map f (𝒰.map i ≫ g) f g (𝟙 X) (𝒰.map i) (𝟙 Z) ⋯ ⋯ = (pullbackSymmetry f (𝒰.map i ≫ g)).hom ≫ pullback.map (𝒰.map i ≫ g) f g f (𝒰.map i) (𝟙 X) (𝟙 Z) ⋯ ⋯ ≫ (pullbackSymmetry g f).hom
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>s : Setoid α<VAR>x : Quotient s<VAR>y : α<GOAL>x = ⟦y⟧ ↔ x.out ≈ y
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>s : Setoid α<VAR>x : Quotient s<VAR>y : α<GOAL>x = ⟦y⟧ ↔ ⟦x.out⟧ = ⟦y⟧
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>s : Set α<VAR>a : α<VAR>t : Set α<GOAL>t ∈ 𝒫 insert a s ↔ t ∈ 𝒫 s ∪ insert a '' 𝒫 s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>s : Set α<VAR>a : α<VAR>t : Set α<GOAL>t ⊆ insert a s ↔ t ⊆ s ∨ ∃ x ⊆ s, insert a x = t
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>α : L → R<VAR>β : Weight R L M<VAR>hα : α ≠ 0<GOAL>chainTopCoeff α β + 1 = Nat.find ⋯
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : NonUnitalSemiring A<VAR>inst✝⁶ : Module R A<VAR>inst✝⁵ : SMulCommClass R A A<VAR>inst✝⁴ : IsScalarTower R A A<VAR>inst✝³ : NonUnitalSemiring B<VAR>inst✝² : Module R B<VAR>inst✝¹ : SMulCommClass R B B<VAR>inst✝ : IsScalarTower R B B<VAR>x y z : A ⊗[R] B<GOAL>(mul ((mul x) y)) z = (mul x) ((mul y) z)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : NonUnitalSemiring A<VAR>inst✝⁶ : Module R A<VAR>inst✝⁵ : SMulCommClass R A A<VAR>inst✝⁴ : IsScalarTower R A A<VAR>inst✝³ : NonUnitalSemiring B<VAR>inst✝² : Module R B<VAR>inst✝¹ : SMulCommClass R B B<VAR>inst✝ : IsScalarTower R B B<VAR>x y z : A ⊗[R] B<GOAL>(LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B)) mul ∘ₗ mul = (((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)) LinearMap.lflip) ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B)) mul.flip ∘ₗ mul)).flip
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NonUnitalNormedRing A<VAR>inst✝² : NormedSpace 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>x : Unitization 𝕜 A<GOAL>(x.fst + 0, (lift (NonUnitalAlgHom.Lmul 𝕜 A)).toRingHom x) = (x.fst, (algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (mul 𝕜 A) x.snd)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NonUnitalNormedRing A<VAR>inst✝² : NormedSpace 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>x : Unitization 𝕜 A<GOAL>(x.fst, (lift (NonUnitalAlgHom.Lmul 𝕜 A)).toRingHom x) = (x.fst, (algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (mul 𝕜 A) x.snd)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Field K<VAR>R₁ : Type u_4<VAR>inst✝⁶ : CommRing R₁<VAR>inst✝⁵ : IsDomain R₁<VAR>inst✝⁴ : Algebra R₁ K<VAR>inst✝³ : IsFractionRing R₁ K<VAR>I J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R₁ K'<VAR>inst✝ : IsFractionRing R₁ K'<VAR>x : K<VAR>hx : x ≠ 0<GOAL>spanSingleton R₁⁰ x * (spanSingleton R₁⁰ x)⁻¹ = 1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>I : Ideal A<GOAL>Submodule.restrictScalars R (map includeLeft I) = LinearMap.range (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>I : Ideal A<GOAL>(Submodule.restrictScalars R (map includeLeft I)).carrier = (LinearMap.range (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype)).carrier
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>I : Ideal A<GOAL>(Submodule.restrictScalars R (map includeLeft I)).carrier ≤ (LinearMap.range (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype)).carrier
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>I : Ideal A<GOAL>(LinearMap.range (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype)).carrier ≤ (Submodule.restrictScalars R (map includeLeft I)).carrier
<VAR>n a : ℕ<VAR>a1 : a ≠ 1<VAR>j : ℕ<VAR>hp : Prime (a * j)<GOAL>a * j = a
<VAR>n a : ℕ<VAR>a1 : a ≠ 1<VAR>left✝ : Prime a<VAR>hp : Prime (a * 1)<GOAL>a * 1 = a
<VAR>n j : ℕ<VAR>left✝ : Prime j<VAR>a1 : 1 ≠ 1<VAR>hp : Prime (1 * j)<GOAL>1 * j = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ↪o β<VAR>he : (range ⇑e).OrdConnected<VAR>x y : α<GOAL>⇑e '' Icc x y = Icc (e x) (e y)
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>v w : V<VAR>hvw : G.Adj v w<VAR>a : V<VAR>ha : a ∈ (G.subgraphOfAdj hvw).verts<VAR>b : V<VAR>hb : b ∈ (G.subgraphOfAdj hvw).verts<GOAL>(G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>v w : V<VAR>hvw : G.Adj v w<VAR>a : V<VAR>ha✝ : a ∈ (G.subgraphOfAdj hvw).verts<VAR>b : V<VAR>hb✝ : b ∈ (G.subgraphOfAdj hvw).verts<VAR>ha : a = v ∨ a = w<VAR>hb : b = v ∨ b = w<GOAL>(G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha✝⟩ ⟨b, hb✝⟩
<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>M : Type u_13<VAR>inst✝¹ : Zero M<VAR>P : α → Prop<VAR>inst✝ : DecidablePred P<VAR>f : Subtype P →₀ M<VAR>x : α<GOAL>x ∈ ↑f.extendDomain.support → x ∈ {x | P x}
<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>M : Type u_13<VAR>inst✝¹ : Zero M<VAR>P : α → Prop<VAR>inst✝ : DecidablePred P<VAR>f : Subtype P →₀ M<VAR>x : α<GOAL>(∃ a ∈ f.support, ↑a = x) → x ∈ {x | P x}
<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>M : Type u_13<VAR>inst✝¹ : Zero M<VAR>P : α → Prop<VAR>inst✝ : DecidablePred P<VAR>f : Subtype P →₀ M<VAR>x : Subtype P<GOAL>↑x ∈ {x | P x}
<VAR>α β : Type u<VAR>ι : Type v<VAR>f : ι → Cardinal.{w}<VAR>hf : BddAbove (range f)<VAR>t : Cardinal.{max u w}<GOAL>lift.{u, w} (iSup f) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t
<VAR>α β : Type u<VAR>ι : Type v<VAR>f : ι → Cardinal.{w}<VAR>hf : BddAbove (range f)<VAR>t : Cardinal.{max u w}<GOAL>⨆ i, lift.{u, w} (f i) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>R : Type u_1<VAR>inst✝ : SMul R (FractionRing K[X])<VAR>c : R<VAR>toFractionRing✝ : FractionRing K[X]<GOAL>(c • { toFractionRing := toFractionRing✝ }).toFractionRing = c • { toFractionRing := toFractionRing✝ }.toFractionRing
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>A B : Type u<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R B<VAR>inst✝² : FormallyUnramified R A<VAR>e : A ≃ₐ[R] B<VAR>C : Type u<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra R C<VAR>I : Ideal C<VAR>hI : I ^ 2 = ⊥<VAR>f₁ f₂ : B →ₐ[R] C<VAR>e' : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂<GOAL>f₁ = f₂
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>A B : Type u<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R B<VAR>inst✝² : FormallyUnramified R A<VAR>e : A ≃ₐ[R] B<VAR>C : Type u<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra R C<VAR>I : Ideal C<VAR>hI : I ^ 2 = ⊥<VAR>f₁ f₂ : B →ₐ[R] C<VAR>e' : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂<GOAL>(f₁.comp ↑e).comp ↑e.symm = (f₂.comp ↑e).comp ↑e.symm
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>A B : Type u<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R B<VAR>inst✝² : FormallyUnramified R A<VAR>e : A ≃ₐ[R] B<VAR>C : Type u<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra R C<VAR>I : Ideal C<VAR>hI : I ^ 2 = ⊥<VAR>f₁ f₂ : B →ₐ[R] C<VAR>e' : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂<GOAL>f₁.comp ↑e = f₂.comp ↑e
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>A B : Type u<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R B<VAR>inst✝² : FormallyUnramified R A<VAR>e : A ≃ₐ[R] B<VAR>C : Type u<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra R C<VAR>I : Ideal C<VAR>hI : I ^ 2 = ⊥<VAR>f₁ f₂ : B →ₐ[R] C<VAR>e' : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂<GOAL>(Ideal.Quotient.mkₐ R I).comp (f₁.comp ↑e) = (Ideal.Quotient.mkₐ R I).comp (f₂.comp ↑e)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>inst✝⁴ : SeminormedAddCommGroup V<VAR>inst✝³ : SeminormedAddCommGroup W<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V₁ V₂<VAR>g : NormedAddGroupHom V₂ V₃<VAR>h : g.comp f = 0<VAR>v : V₁<GOAL>f v ∈ g.ker
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>inst✝⁴ : SeminormedAddCommGroup V<VAR>inst✝³ : SeminormedAddCommGroup W<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V₁ V₂<VAR>g : NormedAddGroupHom V₂ V₃<VAR>h : g.comp f = 0<VAR>v w : V₁<GOAL>(fun v => ⟨f v, ⋯⟩) (v + w) = (fun v => ⟨f v, ⋯⟩) v + (fun v => ⟨f v, ⋯⟩) w
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : LinearOrderedSemifield β<VAR>s : Set ι<VAR>f f₁ f₂ : ι → α<VAR>g g₁ g₂ : ι → β<VAR>hg : ∀ i ∈ s, 0 < g i<VAR>i : ι<VAR>hi : i ∈ s<VAR>j : ι<VAR>hj : j ∈ s<GOAL>g⁻¹ j < g⁻¹ i → f j ≤ f i ↔ g i < g j → f j ≤ f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>fst✝¹ : α<VAR>snd✝¹ : β<VAR>fst✝ : α<VAR>snd✝ : β<GOAL>(fst✝¹, snd✝¹) ⩿ (fst✝, snd✝) ↔ (fst✝¹, snd✝¹).1 ⩿ (fst✝, snd✝).1 ∧ (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2 ∨ (fst✝¹, snd✝¹).2 ⩿ (fst✝, snd✝).2 ∧ (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1
<VAR>M✝ : Type u_1<VAR>N : Type u_2<VAR>A✝ : Type u_3<VAR>inst✝⁴ : MulOneClass M✝<VAR>s : Set M✝<VAR>inst✝³ : AddZeroClass A✝<VAR>t : Set A✝<VAR>M : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SetLike A M<VAR>inst✝ : SubmonoidClass A M<VAR>S : A<VAR>x : M<VAR>hx : x ∈ S<GOAL>x ^ 0 ∈ S
<VAR>M✝ : Type u_1<VAR>N : Type u_2<VAR>A✝ : Type u_3<VAR>inst✝⁴ : MulOneClass M✝<VAR>s : Set M✝<VAR>inst✝³ : AddZeroClass A✝<VAR>t : Set A✝<VAR>M : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SetLike A M<VAR>inst✝ : SubmonoidClass A M<VAR>S : A<VAR>x : M<VAR>hx : x ∈ S<GOAL>1 ∈ S
<VAR>M✝ : Type u_1<VAR>N : Type u_2<VAR>A✝ : Type u_3<VAR>inst✝⁴ : MulOneClass M✝<VAR>s : Set M✝<VAR>inst✝³ : AddZeroClass A✝<VAR>t : Set A✝<VAR>M : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SetLike A M<VAR>inst✝ : SubmonoidClass A M<VAR>S : A<VAR>x : M<VAR>hx : x ∈ S<VAR>n : ℕ<GOAL>x ^ (n + 1) ∈ S
<VAR>M✝ : Type u_1<VAR>N : Type u_2<VAR>A✝ : Type u_3<VAR>inst✝⁴ : MulOneClass M✝<VAR>s : Set M✝<VAR>inst✝³ : AddZeroClass A✝<VAR>t : Set A✝<VAR>M : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SetLike A M<VAR>inst✝ : SubmonoidClass A M<VAR>S : A<VAR>x : M<VAR>hx : x ∈ S<VAR>n : ℕ<GOAL>x ^ n * x ∈ S
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>f : R[X]<VAR>inst✝¹ : CommRing S<VAR>i : R →+* S<VAR>a : S<VAR>h : eval₂ i a f = 0<VAR>inst✝ : Algebra R S<VAR>hfx : (aeval a) f = 0<VAR>r : R<GOAL>(of (C r * X - 1)) r * root (C r * X - 1) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>hst : s ⊆ t<VAR>hsn : s.card ≤ n<VAR>hnt : n ≤ t.card<GOAL>∃ u, s ⊆ u ∧ u ⊆ t ∧ u.card = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : 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>inst✝² : One M<VAR>inst✝¹ : One N<VAR>inst✝ : One P<VAR>f : α × β → M<GOAL>mulSupport (curry f) = Prod.fst '' mulSupport f
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)<GOAL>(⇑derivative)^[n + 1] (p * q) = ∑ k ∈ range (n + 1).succ, (n + 1).choose k • ((⇑derivative)^[n + 1 - k] p * (⇑derivative)^[k] q)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)<GOAL>∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k + 1] p * (⇑derivative)^[k] q) + ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) = ∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) + 1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q) + ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : CommSemiring k<VAR>inst✝⁵ : Monoid G<VAR>inst✝⁴ : Monoid H<VAR>A : Type u₃<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra k A<VAR>B : Type u_3<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra k B<VAR>F : G →* A<VAR>f : MonoidAlgebra k G<GOAL>((lift k G A) F) f = sum f fun a b => b • F a
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ_[p]<GOAL>↑(padicNormE (q + r)) ≤ max ↑(padicNormE q) ↑(padicNormE r)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<GOAL>(∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M') ↔ IsArtinian R M
<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✝ f g : α → E<VAR>hf : Memℒp f p μ<VAR>hg : Memℒp g p μ<GOAL>Memℒp (f - g) p μ
<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✝ f g : α → E<VAR>hf : Memℒp f p μ<VAR>hg : Memℒp g p μ<GOAL>Memℒp (f + -g) p μ
<VAR>R : Type u_1<VAR>inst✝⁵ : AddCommGroupWithOne R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : ZeroLEOneClass R<VAR>inst✝¹ : NeZero 1<VAR>inst✝ : Nontrivial R<VAR>m n : ℤ<GOAL>0 < ↑n ↔ 0 < n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : TruncatedWittVector p n R<GOAL>WittVector.truncateFun n x.out = x
<VAR>θ : Angle<GOAL>Real.cos θ.toReal = θ.cos
<VAR>T : ℝ<GOAL>Periodic (fun x => expMapCircle (2 * π / T * x)) T
<GOAL>Periodic (fun x => expMapCircle (2 * π / 0 * x)) 0
<VAR>T : ℝ<VAR>hT : T ≠ 0<GOAL>Periodic (fun x => expMapCircle (2 * π / T * x)) T
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NonUnitalRing α<VAR>a b c : α<VAR>h : a ∣ b<GOAL>a ∣ b - c ↔ a ∣ c
<VAR>R : Type u_1<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : GCDMonoid R<VAR>p✝ q✝ p q : R<VAR>hp : p ≠ 0<GOAL>p / GCDMonoid.gcd p q ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : GCDMonoid R<VAR>p✝ q✝ p q : R<VAR>hp : p ≠ 0<VAR>r : R<VAR>hr : p = GCDMonoid.gcd p q * r<GOAL>p / GCDMonoid.gcd p q ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : GCDMonoid R<VAR>p✝ q✝ p q : R<VAR>hp : p ≠ 0<VAR>r : R<VAR>hr : p = GCDMonoid.gcd p q * r<VAR>pq0 : GCDMonoid.gcd p q ≠ 0<VAR>r0 : r ≠ 0<GOAL>p / GCDMonoid.gcd p q ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : GCDMonoid R<VAR>p✝ q✝ p q : R<VAR>hp : p ≠ 0<VAR>r : R<VAR>hr : p = GCDMonoid.gcd p q * r<VAR>pq0 : GCDMonoid.gcd p q ≠ 0<VAR>r0 : r ≠ 0<GOAL>GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : GCDMonoid R<VAR>p✝ q✝ p q : R<VAR>hp : p ≠ 0<VAR>r : R<VAR>hr : p = GCDMonoid.gcd p q * r<VAR>pq0 : GCDMonoid.gcd p q ≠ 0<VAR>r0 : r ≠ 0<GOAL>r ≠ 0
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>n : ℕ<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<VAR>x m : Fin 0 → G<GOAL>(curry0 𝕜 G (f x)) m = f m