ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>ha : a ≤ 0<GOAL>↑⌊a⌋ ≤ 0
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁴ : CommRing P<VAR>inst✝³ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝² : CommRing R₁<VAR>K : Type u_4<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>I : Submodule R₁ K<VAR>hI : I ≤ ↑0<GOAL>I.FG
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁴ : CommRing P<VAR>inst✝³ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝² : CommRing R₁<VAR>K : Type u_4<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>I : Submodule R₁ K<VAR>hI : I = ⊥<GOAL>I.FG
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁴ : CommRing P<VAR>inst✝³ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝² : CommRing R₁<VAR>K : Type u_4<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>I : Submodule R₁ K<VAR>hI : I = ⊥<GOAL>⊥.FG
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f : X → ℝ<VAR>s✝ s : Set X<VAR>hs : MeasurableSet s<VAR>hf : StronglyMeasurable f<VAR>hfi : Integrable f μ<GOAL>∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in {y | 0 ≤ f y}, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f : X → ℝ<VAR>s✝ s : Set X<VAR>hs : MeasurableSet s<VAR>hf : StronglyMeasurable f<VAR>hfi : Integrable f μ<GOAL>∫ (x : X), s.indicator f x ∂μ ≤ ∫ (x : X), {a | 0 ≤ f a}.indicator f x ∂μ
<VAR>I : Type u<VAR>inst✝⁵ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : MonoidalCategory C<VAR>X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C<VAR>f₁ : X₁ ⟶ X₂<VAR>f₂ : X₂ ⟶ X₃<VAR>g₁ : Y₁ ⟶ Y₂<VAR>g₂ : Y₂ ⟶ Y₃<VAR>inst✝² : X₁.HasTensor Y₁<VAR>inst✝¹ : X₂.HasTensor Y₂<VAR>inst✝ : X₃.HasTensor Y₃<GOAL>(mapMap (((mapBifunctor (curriedTensor C) I I).map (f₁ ≫ f₂)).app Y₁ ≫ ((mapBifunctor (curriedTensor C) I I).obj X₃).map (g₁ ≫ g₂)) fun x => x.1 + x.2) = (mapMap (((mapBifunctor (curriedTensor C) I I).map f₁).app Y₁ ≫ ((mapBifunctor (curriedTensor C) I I).obj X₂).map g₁) fun x => x.1 + x.2) ≫ mapMap (((mapBifunctor (curriedTensor C) I I).map f₂).app Y₂ ≫ ((mapBifunctor (curriedTensor C) I I).obj X₃).map g₂) fun x => x.1 + x.2
<VAR>I : Type u<VAR>inst✝⁵ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : MonoidalCategory C<VAR>X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C<VAR>f₁ : X₁ ⟶ X₂<VAR>f₂ : X₂ ⟶ X₃<VAR>g₁ : Y₁ ⟶ Y₂<VAR>g₂ : Y₂ ⟶ Y₃<VAR>inst✝² : X₁.HasTensor Y₁<VAR>inst✝¹ : X₂.HasTensor Y₂<VAR>inst✝ : X₃.HasTensor Y₃<GOAL>(mapMap (((mapBifunctor (curriedTensor C) I I).map (f₁ ≫ f₂)).app Y₁ ≫ ((mapBifunctor (curriedTensor C) I I).obj X₃).map (g₁ ≫ g₂)) fun x => x.1 + x.2) = mapMap ((((mapBifunctor (curriedTensor C) I I).map f₁).app Y₁ ≫ ((mapBifunctor (curriedTensor C) I I).obj X₂).map g₁) ≫ ((mapBifunctor (curriedTensor C) I I).map f₂).app Y₂ ≫ ((mapBifunctor (curriedTensor C) I I).obj X₃).map g₂) fun x => x.1 + x.2
<VAR>I : Type u<VAR>inst✝⁵ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : MonoidalCategory C<VAR>X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C<VAR>f₁ : X₁ ⟶ X₂<VAR>f₂ : X₂ ⟶ X₃<VAR>g₁ : Y₁ ⟶ Y₂<VAR>g₂ : Y₂ ⟶ Y₃<VAR>inst✝² : X₁.HasTensor Y₁<VAR>inst✝¹ : X₂.HasTensor Y₂<VAR>inst✝ : X₃.HasTensor Y₃<GOAL>((mapBifunctor (curriedTensor C) I I).map (f₁ ≫ f₂)).app Y₁ ≫ ((mapBifunctor (curriedTensor C) I I).obj X₃).map (g₁ ≫ g₂) = (((mapBifunctor (curriedTensor C) I I).map f₁).app Y₁ ≫ ((mapBifunctor (curriedTensor C) I I).obj X₂).map g₁) ≫ ((mapBifunctor (curriedTensor C) I I).map f₂).app Y₂ ≫ ((mapBifunctor (curriedTensor C) I I).obj X₃).map g₂
<VAR>z : ℂ<GOAL>-z.re = abs z ↔ z ≤ 0
<VAR>z : ℂ<GOAL>0 ≤ -z ↔ z ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t✝ u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<GOAL>(s \ t).card + t.card = (s ∪ t).card
<VAR>ι✝ : Type u'<VAR>ι'✝ : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι✝ → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>s : Set ι<VAR>f : ι → ι'<VAR>g : ι' → M<VAR>hs : LinearIndependent R fun (x : ↑s) => g (f ↑x)<VAR>a✝ : Nontrivial R<GOAL>LinearIndependent R fun (x : ↑(f '' s)) => g ↑x
<VAR>ι✝ : Type u'<VAR>ι'✝ : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι✝ → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>s : Set ι<VAR>f : ι → ι'<VAR>g : ι' → M<VAR>hs : LinearIndependent R fun (x : ↑s) => g (f ↑x)<VAR>a✝ : Nontrivial R<VAR>this : InjOn f s<GOAL>LinearIndependent R fun (x : ↑(f '' s)) => g ↑x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Surjective ⇑(range f).subtype.dualMap<GOAL>range f.dualMap = (ker f).dualAnnihilator
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Surjective ⇑(range f).subtype.dualMap<VAR>rr_surj : Function.Surjective ⇑f.rangeRestrict<GOAL>range f.dualMap = (ker f).dualAnnihilator
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Surjective ⇑(range f).subtype.dualMap<VAR>rr_surj : Function.Surjective ⇑f.rangeRestrict<VAR>this : range f.rangeRestrict.dualMap = (ker f.rangeRestrict).dualAnnihilator<GOAL>range f.dualMap = (ker f).dualAnnihilator
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f : Filter α<VAR>a : α<GOAL>f ≤ pure a ↔ {a} ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<GOAL>∀ {s t : WSeq α}, s ~ʷ t → s.head ~ t.head
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<GOAL>∀ {s t : WSeq α}, s ~ʷ t → ∀ {o : Option α}, o ∈ s.head → o ∈ t.head
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : WSeq α<VAR>h : s ~ʷ t<VAR>o : Option α<VAR>ho : o ∈ s.head<GOAL>o ∈ t.head
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : WSeq α<VAR>h : s ~ʷ t<VAR>o : Option α<VAR>ho : o ∈ s.head<VAR>ds : Option (α × WSeq α)<VAR>dsm : ds ∈ s.destruct<VAR>dse : Prod.fst <$> ds = o<GOAL>o ∈ t.head
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : WSeq α<VAR>h : s ~ʷ t<VAR>o : Option α<VAR>ho : o ∈ s.head<VAR>ds : Option (α × WSeq α)<VAR>dsm : ds ∈ s.destruct<VAR>dse : Prod.fst <$> ds = o<GOAL>Prod.fst <$> ds ∈ t.head
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : WSeq α<VAR>h : s ~ʷ t<VAR>o : Option α<VAR>ho : o ∈ s.head<VAR>ds : Option (α × WSeq α)<VAR>dsm : ds ∈ s.destruct<VAR>dse : Prod.fst <$> ds = o<VAR>l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b, b ∈ t.destruct ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b<VAR>r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a, a ∈ s.destruct ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b<GOAL>Prod.fst <$> ds ∈ t.head
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<GOAL>Tendsto rexp (𝓝 0) (𝓝 1)
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<GOAL>1 = rexp 0
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>a : ℤ<GOAL>(↑a).coeff n = ↑(if n = 0 then a else 0)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f✝ : ↑Γ(X, U)<VAR>V : X.Opens<VAR>hV : IsAffineOpen V<VAR>f : op U ⟶ op V<VAR>this✝ : IsAffine (X.restrictFunctor.obj U).left<VAR>this : IsAffine ↑V<GOAL>Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f✝ : ↑Γ(X, U)<VAR>V : X.Opens<VAR>hV : IsAffineOpen V<VAR>f : op U ⟶ op V<VAR>this✝ : IsAffine (X.restrictFunctor.obj U).left<VAR>this : IsAffine ↑V<GOAL>Spec.map (X.presheaf.map f) ≫ hU.fromSpec = Spec.map (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op)) ≫ (X.restrictFunctor.obj (unop (op U))).left.isoSpec.inv ≫ (unop (op U)).ι
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f✝ : ↑Γ(X, U)<VAR>V : X.Opens<VAR>hV : IsAffineOpen V<VAR>f : op U ⟶ op V<VAR>this✝ : IsAffine (X.restrictFunctor.obj U).left<VAR>this : IsAffine ↑V<GOAL>Spec.map (X.presheaf.map ((eqToHom ⋯).op ≫ f)) ≫ (↑U).isoSpec.inv ≫ U.ι = Spec.map (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op)) ≫ (X.restrictFunctor.obj (unop (op U))).left.isoSpec.inv ≫ (unop (op U)).ι
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b : β<VAR>q✝ : ℚ<VAR>ha : 0 < a<VAR>q : ℚ<VAR>hb : q ∈ {t | ↑t < a * a}<GOAL>↑q ≤ inducedMap α β a * inducedMap α β a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b : β<VAR>q✝ : ℚ<VAR>ha : 0 < a<VAR>q : ℚ<VAR>hb : q ∈ {t | ↑t < a * a}<VAR>q' : ℚ<VAR>hq' : 0 < q'<VAR>hqq' : ↑q < ↑q' ^ 2<VAR>hqa : ↑q' ^ 2 < a * a<GOAL>↑q ≤ inducedMap α β a * inducedMap α β a
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<VAR>hx' : x < 1<GOAL>0 < logb b x
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<VAR>hx' : x < 1<GOAL>x < 1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝³ : Semiring R<VAR>p✝ q✝ r : R[X]<VAR>inst✝² : Monoid S<VAR>inst✝¹ : DistribMulAction S R<VAR>inst✝ : IsScalarTower S R R<VAR>s : S<VAR>p q : R[X]<GOAL>(s • p).comp q = s • p.comp q
<VAR>n m : ℕ<GOAL>n ∈ m.properDivisors ↔ n ∣ m ∧ n < m
<VAR>n : ℕ<GOAL>n ∈ properDivisors 0 ↔ n ∣ 0 ∧ n < 0
<VAR>n m : ℕ<VAR>hm : m ≠ 0<GOAL>n ∈ m.properDivisors ↔ n ∣ m ∧ n < m
<VAR>α✝ : Type u_1<VAR>a : α✝<VAR>l m : List α✝<GOAL>a :: l ⊆ m ↔ a ∈ m ∧ l ⊆ m
<VAR>p n : ℕ<VAR>hpp : Prime p<VAR>hp : p ∣ n<VAR>hs : IsSquare (-1)<GOAL>p % 4 ≠ 3
<VAR>p n : ℕ<VAR>hpp : Prime p<VAR>hp : p ∣ n<VAR>hs : IsSquare (-1)<VAR>y : ZMod p<VAR>h : -1 = y * y<GOAL>p % 4 ≠ 3
<VAR>p n : ℕ<VAR>hpp : Prime p<VAR>hp : p ∣ n<VAR>hs : IsSquare (-1)<VAR>y : ZMod p<VAR>h : y ^ 2 = -1 ^ 2<GOAL>p % 4 ≠ 3
<VAR>p n : ℕ<VAR>hpp : Prime p<VAR>hp : p ∣ n<VAR>hs : IsSquare (-1)<VAR>y : ZMod p<VAR>h : y ^ 2 = -1 ^ 2<VAR>this : Fact (Prime p)<GOAL>p % 4 ≠ 3
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι✝ : Type u_12<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : SeminormedRing 𝕝<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : Module 𝕝 E<VAR>ι : Sort u_13<VAR>inst✝² : UniformSpace E<VAR>inst✝¹ : UniformAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>p' : ι → Prop<VAR>s : ι → Set E<VAR>p : Seminorm 𝕜 E<VAR>hb : (𝓝 0).HasBasis p' s<VAR>h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0<VAR>h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i<GOAL>inst✝² = PseudoMetricSpace.toUniformSpace
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι✝ : Type u_12<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : SeminormedRing 𝕝<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : Module 𝕝 E<VAR>ι : Sort u_13<VAR>inst✝² : UniformSpace E<VAR>inst✝¹ : UniformAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>p' : ι → Prop<VAR>s : ι → Set E<VAR>p : Seminorm 𝕜 E<VAR>hb : (𝓝 0).HasBasis p' s<VAR>h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0<VAR>h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i<GOAL>𝓝 0 = 𝓝 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι✝ : Type u_12<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : SeminormedRing 𝕝<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : Module 𝕝 E<VAR>ι : Sort u_13<VAR>inst✝² : UniformSpace E<VAR>inst✝¹ : UniformAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>p' : ι → Prop<VAR>s : ι → Set E<VAR>p : Seminorm 𝕜 E<VAR>hb : (𝓝 0).HasBasis p' s<VAR>h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0<VAR>h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i<GOAL>𝓝 0 ≤ 𝓝 0
<VAR>x y z✝ : ZFSet<VAR>hx : x.IsTransitive<VAR>hy : y.IsTransitive<VAR>z : ZFSet<VAR>hz : z ∈ x ∩ y<VAR>w : ZFSet<VAR>hw : w ∈ z<GOAL>w ∈ x ∩ y
<VAR>x y z✝ : ZFSet<VAR>hx : x.IsTransitive<VAR>hy : y.IsTransitive<VAR>z : ZFSet<VAR>hz : z ∈ x ∧ z ∈ y<VAR>w : ZFSet<VAR>hw : w ∈ z<GOAL>w ∈ x ∧ w ∈ y
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>i1 : ι<VAR>n1 : A<VAR>hn1 : n1 ∈ 𝒜 i1<VAR>d1 : A<VAR>hd1 : d1 ∈ 𝒜 i1<VAR>h1 : ↑⟨d1, hd1⟩ ∈ x<VAR>i2 : ι<VAR>n2 : A<VAR>hn2 : n2 ∈ 𝒜 i2<VAR>d2 : A<VAR>hd2 : d2 ∈ 𝒜 i2<VAR>h2 : ↑⟨d2, hd2⟩ ∈ x<VAR>hdeg : { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.deg = { deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }.deg<VAR>hnum : ↑{ deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.num = ↑{ deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }.num<VAR>hden : ↑{ deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.den = ↑{ deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }.den<GOAL>{ deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 } = { deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>i1 : ι<VAR>n1 : A<VAR>hn1 : n1 ∈ 𝒜 i1<VAR>d1 : A<VAR>hd1 : d1 ∈ 𝒜 i1<VAR>h1 : ↑⟨d1, hd1⟩ ∈ x<VAR>i2 : ι<VAR>n2 : A<VAR>hn2 : n2 ∈ 𝒜 i2<VAR>d2 : A<VAR>hd2 : d2 ∈ 𝒜 i2<VAR>h2 : ↑⟨d2, hd2⟩ ∈ x<VAR>hdeg : i1 = i2<VAR>hnum : n1 = n2<VAR>hden : d1 = d2<GOAL>{ deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 } = { deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>u : ↥K<VAR>v : E<GOAL>⟪u, (orthogonalProjection K) v⟫_𝕜 = ⟪↑u, v⟫_𝕜
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<VAR>h : j ≤ n<GOAL>xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<VAR>h : j ≤ n<VAR>h1 : xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * yz a1 (n - j) + xz a1 j<GOAL>xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<VAR>h : j ≤ n<VAR>h1 : xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * yz a1 (n - j) + xz a1 j<GOAL>xn a1 n * xn a1 (n - j) + (Pell.d a1 * yn a1 n * yn a1 (n - j) + xn a1 j) ≡ 0 + 0 [MOD xn a1 n]
<VAR>z✝ : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z w : ℂ<VAR>h : z.im = w.im<GOAL>dist z w = dist z.re w.re
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s<VAR>Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s<VAR>x : E<VAR>hx : x ∈ s<VAR>m : ℕ<VAR>hm : ↑m ≤ n<GOAL>∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s<VAR>Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s<VAR>x : E<VAR>hx : x ∈ s<VAR>m : ℕ<VAR>hm : ↑m ≤ n<GOAL>∃ u ∈ 𝓝[s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s<VAR>Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s<VAR>x : E<VAR>hx : x ∈ s<VAR>m : ℕ<VAR>hm : ↑m ≤ n<GOAL>HasFTaylorSeriesUpToOn (↑m) f (ftaylorSeriesWithin 𝕜 f s) s
<VAR>L : Type u_1<VAR>inst✝² : SemilatticeSup L<VAR>inst✝¹ : TopologicalSpace L<VAR>inst✝ : ContinuousSup L<VAR>α : Type u_2<VAR>l : Filter α<VAR>f : ℕ → α → L<VAR>g : ℕ → L<VAR>n : ℕ<VAR>hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))<GOAL>Tendsto ((partialSups f) n) l (𝓝 ((partialSups g) n))
<VAR>L : Type u_1<VAR>inst✝² : SemilatticeSup L<VAR>inst✝¹ : TopologicalSpace L<VAR>inst✝ : ContinuousSup L<VAR>α : Type u_2<VAR>l : Filter α<VAR>f : ℕ → α → L<VAR>g : ℕ → L<VAR>n : ℕ<VAR>hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))<GOAL>Tendsto ((Finset.range (n + 1)).sup' ⋯ f) l (𝓝 ((Finset.range (n + 1)).sup' ⋯ g))
<VAR>L : Type u_1<VAR>inst✝² : SemilatticeSup L<VAR>inst✝¹ : TopologicalSpace L<VAR>inst✝ : ContinuousSup L<VAR>α : Type u_2<VAR>l : Filter α<VAR>f : ℕ → α → L<VAR>g : ℕ → L<VAR>n : ℕ<VAR>hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))<GOAL>∀ i ∈ Finset.range (n + 1), Tendsto (f i) l (𝓝 (g i))
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a : α<VAR>h : 0 < a<VAR>b c : α<GOAL>(fun x => a * x) '' Icc b c = Icc (a * b) (a * c)
<VAR>u : ℤˣ<GOAL>u = 1 ∨ u = -1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : IsAtom I<GOAL>IsCompl I (orthogonal Φ hΦ_inv I)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>H : Type u_5<VAR>inst✝ : NormedAddCommGroup H<VAR>m0 : MeasurableSpace α<VAR>μ' : Measure α<VAR>f : α → H<VAR>hm : m ≤ m0<VAR>hf_int : Integrable f μ'<VAR>hf : StronglyMeasurable f<GOAL>Integrable f (μ'.trim hm)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>H : Type u_5<VAR>inst✝ : NormedAddCommGroup H<VAR>m0 : MeasurableSpace α<VAR>μ' : Measure α<VAR>f : α → H<VAR>hm : m ≤ m0<VAR>hf_int : Integrable f μ'<VAR>hf : StronglyMeasurable f<GOAL>HasFiniteIntegral f (μ'.trim hm)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>H : Type u_5<VAR>inst✝ : NormedAddCommGroup H<VAR>m0 : MeasurableSpace α<VAR>μ' : Measure α<VAR>f : α → H<VAR>hm : m ≤ m0<VAR>hf_int : Integrable f μ'<VAR>hf : StronglyMeasurable f<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ∂μ' < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>H : Type u_5<VAR>inst✝ : NormedAddCommGroup H<VAR>m0 : MeasurableSpace α<VAR>μ' : Measure α<VAR>f : α → H<VAR>hm : m ≤ m0<VAR>hf_int : Integrable f μ'<VAR>hf : StronglyMeasurable f<GOAL>Measurable fun a => ↑‖f a‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t✝ u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<GOAL>(s ∩ t).card = s.card + t.card - (s ∪ t).card
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : SemilatticeSup M<VAR>inst✝ : OrderBot M<VAR>w : σ → M<VAR>p : MvPolynomial σ R<VAR>hp : weightedTotalDegree w p = ⊥<VAR>d : σ →₀ ℕ<VAR>hd : coeff d p ≠ 0<GOAL>(weight w) d = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : SemilatticeSup M<VAR>inst✝ : OrderBot M<VAR>w : σ → M<VAR>p : MvPolynomial σ R<VAR>hp : weightedTotalDegree w p = ⊥<VAR>d : σ →₀ ℕ<VAR>hd : coeff d p ≠ 0<VAR>h : weightedTotalDegree' w p = ↑(weightedTotalDegree w p)<GOAL>(weight w) d = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : SemilatticeSup M<VAR>inst✝ : OrderBot M<VAR>w : σ → M<VAR>p : MvPolynomial σ R<VAR>hp : weightedTotalDegree w p = ⊥<VAR>d : σ →₀ ℕ<VAR>hd : coeff d p ≠ 0<VAR>h : (p.support.sup fun s => ↑((weight w) s)) = ↑⊥<GOAL>(weight w) d = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : SemilatticeSup M<VAR>inst✝ : OrderBot M<VAR>w : σ → M<VAR>p : MvPolynomial σ R<VAR>hp : weightedTotalDegree w p = ⊥<VAR>d : σ →₀ ℕ<VAR>hd : coeff d p ≠ 0<VAR>h : (p.support.sup fun s => ↑((weight w) s)) = ↑⊥<GOAL>↑((weight w) d) ≤ p.support.sup fun s => ↑((weight w) s)
<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>x y✝ z : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>y : E<VAR>hy : y ∈ s<GOAL>x ∈ s
<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>x y✝ z : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>y : E<VAR>hy : y ∈ s<GOAL>x = 1 • x + 0 • y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<VAR>hf : f.IsCycleOn s<VAR>hs : s.Nontrivial<VAR>ha : a ∈ s<GOAL>f a ≠ a