ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>hdomain : IsDomain R<VAR>r s : R<VAR>p q : R[X]<VAR>f : RatFunc R<VAR>p✝ q✝ : R[X]<VAR>hq✝ : q✝ ≠ 0<GOAL>(laurent r) ((laurent s) ((algebraMap R[X] (RatFunc R)) p✝ / (algebraMap R[X] (RatFunc R)) q✝)) = (laurent (r + s)) ((algebraMap R[X] (RatFunc R)) p✝ / (algebraMap R[X] (RatFunc R)) q✝)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>μ : K<GOAL>f.HasEigenvalue μ ↔ μ ∈ spectrum K f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>a : α<GOAL>{a}.min = ↑a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>a : α<GOAL>(insert a ∅).min = ↑a
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → G<VAR>C✝ : ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>C : ℝ≥0<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C<VAR>hs : Convex ℝ s<GOAL>LipschitzOnWith C f s
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → G<VAR>C✝ : ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>C : ℝ≥0<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C<VAR>hs : Convex ℝ s<GOAL>∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → G<VAR>C✝ : ℝ<VAR>s : Set E<VAR>x✝ y✝ : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>C : ℝ≥0<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C<VAR>hs : Convex ℝ s<VAR>x : E<VAR>x_in : x ∈ s<VAR>y : E<VAR>y_in : y ∈ s<GOAL>‖f x - f y‖ ≤ ↑C * ‖x - y‖
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>inst✝ : l.NeBot<VAR>s : Set 𝕜<VAR>hs : IsOpen s<VAR>hf' : TendstoLocallyUniformlyOn f' g' l s<VAR>hf : ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) (f' n x) x<VAR>hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>hx : x ∈ s<GOAL>HasDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>inst✝ : l.NeBot<VAR>s : Set 𝕜<VAR>hs : IsOpen s<VAR>hf' : TendstoLocallyUniformlyOn f' g' l s<VAR>hf : ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) (f' n x) x<VAR>hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>hx : x ∈ s<VAR>h1 : s ∈ 𝓝 x<GOAL>HasDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>inst✝ : l.NeBot<VAR>s : Set 𝕜<VAR>hs : IsOpen s<VAR>hf' : TendstoLocallyUniformlyOn f' g' l s<VAR>hf : ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) (f' n x) x<VAR>hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>hx : x ∈ s<VAR>h1 : s ∈ 𝓝 x<VAR>h2 : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2<GOAL>HasDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>inst✝ : l.NeBot<VAR>s : Set 𝕜<VAR>hs : IsOpen s<VAR>hf' : TendstoLocallyUniformlyOn f' g' l s<VAR>hf : ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) (f' n x) x<VAR>hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>hx : x ∈ s<VAR>h1 : s ∈ 𝓝 x<VAR>h2 : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2<GOAL>TendstoUniformlyOnFilter f' g' l (𝓝 x)
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>ι : Type u_2<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<GOAL>IsZero ((quotient V c).obj C) ↔ Nonempty (Homotopy (𝟙 C) 0)
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>ι : Type u_2<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<GOAL>𝟙 ((quotient V c).obj C) = 0 ↔ Nonempty (Homotopy (𝟙 C) 0)
<VAR>a b c d m n✝ : ℤ<VAR>n : ℕ<GOAL>m ∣ ↑n ↔ m.natAbs ∣ n
<VAR>E✝ : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E✝<VAR>inst✝⁸ : NormedSpace ℝ E✝<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 E✝<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>f✝ g : E✝ → G<VAR>C✝ : ℝ<VAR>s : Set E✝<VAR>x y : E✝<VAR>f' g' : E✝ → E✝ →L[𝕜] G<VAR>φ : E✝ →L[𝕜] G<VAR>E : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : E → G<VAR>C : ℝ≥0<VAR>hf : Differentiable 𝕜 f<VAR>bound : ∀ (x : E), ‖fderiv 𝕜 f x‖₊ ≤ C<VAR>A : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E<GOAL>LipschitzWith C f
<VAR>E✝ : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E✝<VAR>inst✝⁸ : NormedSpace ℝ E✝<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 E✝<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>f✝ g : E✝ → G<VAR>C✝ : ℝ<VAR>s : Set E✝<VAR>x y : E✝<VAR>f' g' : E✝ → E✝ →L[𝕜] G<VAR>φ : E✝ →L[𝕜] G<VAR>E : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : E → G<VAR>C : ℝ≥0<VAR>hf : Differentiable 𝕜 f<VAR>bound : ∀ (x : E), ‖fderiv 𝕜 f x‖₊ ≤ C<VAR>A : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E<GOAL>LipschitzOnWith C f univ
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P<VAR>hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>X Y S : Scheme<VAR>inst✝² : IsAffine X<VAR>inst✝¹ : IsAffine Y<VAR>inst✝ : IsAffine S<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : P (Scheme.Hom.app g ⊤)<GOAL>P (Scheme.Hom.app (pullback.fst f g) ⊤)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P<VAR>hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>X Y S : Scheme<VAR>inst✝² : IsAffine X<VAR>inst✝¹ : IsAffine Y<VAR>inst✝ : IsAffine S<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : P (Scheme.Hom.app g ⊤)<GOAL>P (Scheme.Hom.app ((PreservesPullback.iso AffineScheme.forgetToScheme (AffineScheme.ofHom f) (AffineScheme.ofHom g)).inv ≫ AffineScheme.forgetToScheme.map (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g))) ⊤)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P<VAR>hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>X Y S : Scheme<VAR>inst✝² : IsAffine X<VAR>inst✝¹ : IsAffine Y<VAR>inst✝ : IsAffine S<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : P (Scheme.Hom.app g ⊤)<GOAL>P (Scheme.Hom.app (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)) ⊤)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P<VAR>hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>X Y S : Scheme<VAR>inst✝² : IsAffine X<VAR>inst✝¹ : IsAffine Y<VAR>inst✝ : IsAffine S<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : P (Scheme.Hom.app g ⊤)<VAR>this : ((PreservesPullback.iso AffineScheme.Γ.rightOp (AffineScheme.ofHom f) (AffineScheme.ofHom g)).hom ≫ pullback.fst (AffineScheme.Γ.rightOp.map (AffineScheme.ofHom f)) (AffineScheme.Γ.rightOp.map (AffineScheme.ofHom g))).unop = (AffineScheme.Γ.rightOp.map (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g))).unop<GOAL>P (Scheme.Hom.app (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)) ⊤)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P<VAR>hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>X Y S : Scheme<VAR>inst✝² : IsAffine X<VAR>inst✝¹ : IsAffine Y<VAR>inst✝ : IsAffine S<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : P (Scheme.Hom.app g ⊤)<VAR>this : (pullback.fst (Scheme.Hom.app (AffineScheme.ofHom f) ⊤).op (Scheme.Hom.app (AffineScheme.ofHom g) ⊤).op).unop ≫ (PreservesPullback.iso (AffineScheme.forgetToScheme.op ⋙ Scheme.Γ).rightOp (AffineScheme.ofHom f) (AffineScheme.ofHom g)).hom.unop = Scheme.Hom.app (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)) ⊤<GOAL>P (Scheme.Hom.app (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)) ⊤)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P<VAR>hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>X Y S : Scheme<VAR>inst✝² : IsAffine X<VAR>inst✝¹ : IsAffine Y<VAR>inst✝ : IsAffine S<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : P (Scheme.Hom.app g ⊤)<VAR>this : (pullback.fst (Scheme.Hom.app (AffineScheme.ofHom f) ⊤).op (Scheme.Hom.app (AffineScheme.ofHom g) ⊤).op).unop ≫ (PreservesPullback.iso (AffineScheme.forgetToScheme.op ⋙ Scheme.Γ).rightOp (AffineScheme.ofHom f) (AffineScheme.ofHom g)).hom.unop = Scheme.Hom.app (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)) ⊤<GOAL>P (pushout.inl (Scheme.Hom.app (AffineScheme.ofHom f) ⊤) (Scheme.Hom.app (AffineScheme.ofHom g) ⊤))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>h : LipschitzOnWith K f s<GOAL>dimH (f '' s) ≤ dimH s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ t : Finset α<VAR>a : α<VAR>s : Finset α<GOAL>s.powerset ⊼ s.powerset = s.powerset
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Lattice α<VAR>a b c d : α<GOAL>a ⊔ b = b ↔ a ⊓ b = a
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hcd : IntervalIntegrable f μ c d<VAR>hac : IntervalIntegrable f μ a c<GOAL>∫ (x : ℝ) in a..b, f x ∂μ - ∫ (x : ℝ) in c..d, f x ∂μ = ∫ (x : ℝ) in d..b, f x ∂μ - ∫ (x : ℝ) in c..a, f x ∂μ
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>k n : ℕ<GOAL>(X ^ k).coeff n = if n = k then 1 else 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>M : Matrix n n 𝕜<VAR>hM : M.PosDef<GOAL>0 < M.det
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>M : Matrix n n 𝕜<VAR>hM : M.PosDef<GOAL>0 < ∏ i : n, ↑(⋯.eigenvalues i)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>M : Matrix n n 𝕜<VAR>hM : M.PosDef<GOAL>∀ i ∈ Finset.univ, 0 < ↑(⋯.eigenvalues i)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>M : Matrix n n 𝕜<VAR>hM : M.PosDef<VAR>i : n<VAR>a✝ : i ∈ Finset.univ<GOAL>0 < ↑(⋯.eigenvalues i)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : CommRing M<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : Algebra R M<VAR>x✝ : L<VAR>int✝ : IsIntegral R x✝<VAR>h✝ : Splits (algebraMap R K) (minpoly R x✝)<VAR>inst✝³ : Algebra K M<VAR>inst✝² : IsScalarTower R K M<VAR>x : M<VAR>int : IsIntegral R x<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsScalarTower R K L<VAR>h : Splits (algebraMap R L) (minpoly R x)<GOAL>Splits (algebraMap K L) (minpoly K x)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : CommRing M<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : Algebra R M<VAR>x✝ : L<VAR>int✝ : IsIntegral R x✝<VAR>h✝ : Splits (algebraMap R K) (minpoly R x✝)<VAR>inst✝³ : Algebra K M<VAR>inst✝² : IsScalarTower R K M<VAR>x : M<VAR>int : IsIntegral R x<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsScalarTower R K L<VAR>h : Splits ((algebraMap K L).comp (algebraMap R K)) (minpoly R x)<GOAL>Splits (algebraMap K L) (minpoly K x)
<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✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ q : Seminorm 𝕜 E<VAR>x : E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<VAR>hp : BddAbove (range p)<GOAL>⇑(⨆ i, p i) = ⨆ i, ⇑(p i)
<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✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ q : Seminorm 𝕜 E<VAR>x : E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<VAR>hp : BddAbove (range p)<GOAL>⨆ p_1, ⇑↑p_1 = ⨆ i, ⇑(p i)
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>inst✝ : CompleteLattice α<VAR>f : ℝ≥0∞ → α<GOAL>⨅ x, ⨅ (_ : x ≠ ⊤), f x = ⨅ x, f ↑x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : Semiring R₂<VAR>inst✝⁹ : Semiring R₃<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>M' : Type u_11<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>O : Submodule R M<VAR>ϕ : ↥O →ₗ[R] M'<VAR>N : Submodule R M<VAR>hNO : N ≤ O<GOAL>ϕ.submoduleImage N = range (ϕ ∘ₗ Submodule.inclusion hNO)
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>r : α<VAR>A : Matrix n n α<GOAL>(r • A).adjugate = r ^ (Fintype.card n - 1) • A.adjugate
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>r : α<VAR>A : Matrix n n α<GOAL>(of fun i => (r ^ (Fintype.card n - 1) • Aᵀ.cramer) (Pi.single i 1)) = r ^ (Fintype.card n - 1) • of fun i => Aᵀ.cramer (Pi.single i 1)
<VAR>p q : ℚ<VAR>s t : Set ℚ<VAR>a✝ : (𝓝 ∞).IsCountablyGenerated<VAR>this : (comap OnePoint.some (𝓝 ∞)).IsCountablyGenerated<GOAL>False
<VAR>p q : ℚ<VAR>s t : Set ℚ<VAR>a✝ : (𝓝 ∞).IsCountablyGenerated<VAR>this : (cocompact ℚ).IsCountablyGenerated<GOAL>False
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝² : DivInvMonoid M<VAR>inst✝¹ : PseudoMetricSpace M<VAR>inst✝ : IsometricSMul Mᵐᵒᵖ M<VAR>a b c : M<GOAL>dist (a / c) (b / c) = dist a b
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>S : Set C(X, α)<VAR>hS1 : IsCompact (ContinuousMap.toFun '' S)<VAR>hS2 : Equicontinuous fun x => ⇑↑x<GOAL>IsCompact S
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>S : Set C(X, α)<VAR>hS1 : IsCompact (ContinuousMap.toFun '' S)<VAR>hS2 : Equicontinuous fun x => ⇑↑x<GOAL>Inducing ⇑(Equiv.Set.image DFunLike.coe S ⋯)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>S : Set C(X, α)<VAR>hS1 : IsCompact (ContinuousMap.toFun '' S)<VAR>hS2 : Equicontinuous fun x => ⇑↑x<GOAL>Inducing (⇑(UniformOnFun.ofFun ?m.51400) ∘ Subtype.val ∘ ⇑(Equiv.Set.image DFunLike.coe S ⋯))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>S : Set C(X, α)<VAR>hS1 : IsCompact (ContinuousMap.toFun '' S)<VAR>hS2 : Equicontinuous fun x => ⇑↑x<GOAL>Set (Set X)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>S : Set C(X, α)<VAR>hS1 : IsCompact (ContinuousMap.toFun '' S)<VAR>hS2 : Equicontinuous fun x => ⇑↑x<GOAL>⋃₀ ?m.51400 = univ
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>S : Set C(X, α)<VAR>hS1 : IsCompact (ContinuousMap.toFun '' S)<VAR>hS2 : Equicontinuous fun x => ⇑↑x<GOAL>∀ K ∈ ?m.51400, IsCompact K
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>S : Set C(X, α)<VAR>hS1 : IsCompact (ContinuousMap.toFun '' S)<VAR>hS2 : Equicontinuous fun x => ⇑↑x<GOAL>∀ K ∈ ?m.51400, EquicontinuousOn (Subtype.val ∘ ⇑(Equiv.Set.image DFunLike.coe S ⋯)) K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>a b : α<VAR>ha : a ∉ s<VAR>hb : b ∈ s<GOAL>(insert a (s \ {b})).encard = s.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>a b : α<VAR>ha : a ∉ s<VAR>hb : b ∈ s<GOAL>a ∉ s \ {b}
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>c : ℝ≥0∞<GOAL>∫ (x : ℝ) in a..b, f x ∂c • μ = c.toReal • ∫ (x : ℝ) in a..b, f x ∂μ
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle x (x + y)).cos = ‖x‖ / ‖x + y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle x (x + y)).sign = 1<GOAL>(o.oangle x (x + y)).cos = ‖x‖ / ‖x + y‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ↥(Lp E p μ)<GOAL>‖-f‖₊ = ‖f‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : AddCommMonoid L<VAR>inst✝⁷ : TopologicalSpace L<VAR>inst✝⁶ : AddCommMonoid M✝<VAR>inst✝⁵ : TopologicalSpace M✝<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : TopologicalSpace N<VAR>v : VectorMeasure α M✝<VAR>w✝ : VectorMeasure α N<VAR>M : Type u_6<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : TopologicalAddGroup M<VAR>v₁ v₂ : VectorMeasure α M<VAR>w : VectorMeasure α N<VAR>hv₁ : v₁ ≪ᵥ w<VAR>hv₂ : v₂ ≪ᵥ w<VAR>s : Set α<VAR>hs : ↑w s = 0<GOAL>↑(v₁ - v₂) s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>inst✝¹ : PseudoMetricSpace α<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>x₀ : β<VAR>b : β → ℝ<VAR>b_lim : Tendsto b (𝓝 x₀) (𝓝 0)<VAR>F : ι → β → α<VAR>H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x<GOAL>EquicontinuousAt F x₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>inst✝¹ : PseudoMetricSpace α<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>x₀ : β<VAR>b : β → ℝ<VAR>b_lim : Tendsto b (𝓝 x₀) (𝓝 0)<VAR>F : ι → β → α<VAR>H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x<GOAL>∀ ε > 0, ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>inst✝¹ : PseudoMetricSpace α<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>x₀ : β<VAR>b : β → ℝ<VAR>b_lim : Tendsto b (𝓝 x₀) (𝓝 0)<VAR>F : ι → β → α<VAR>H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x<VAR>ε : ℝ<VAR>ε0 : ε > 0<GOAL>∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε
<VAR>m n : ℕ<GOAL>m.psub n = none ↔ m < n
<VAR>m n : ℕ<VAR>s : m.psub n = none<GOAL>m < n
<VAR>m n val✝ : ℕ<VAR>s : m.psub n = some val✝<GOAL>n ≤ m
<VAR>x : ℝ<VAR>n : ℕ<GOAL>↑(↑n * x) = n • ↑x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 β<VAR>f : E →ₗ[𝕜] β<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x✝⁸ : E<VAR>x✝⁷ : x✝⁸ ∈ s<VAR>x✝⁶ : E<VAR>x✝⁵ : x✝⁶ ∈ s<VAR>x✝⁴ x✝³ : 𝕜<VAR>x✝² : 0 ≤ x✝⁴<VAR>x✝¹ : 0 ≤ x✝³<VAR>x✝ : x✝⁴ + x✝³ = 1<GOAL>x✝⁴ • f x✝⁸ + x✝³ • f x✝⁶ ≤ f (x✝⁴ • x✝⁸ + x✝³ • x✝⁶)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : CompleteSpace E<VAR>f : ι → E<VAR>g : ι → ℝ<VAR>hg : Summable g<VAR>h : ∀ (i : ι), ‖f i‖ ≤ g i<GOAL>Summable f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : CompleteSpace E<VAR>f : ι → E<VAR>g : ι → ℝ<VAR>hg : Summable g<VAR>h : ∀ (i : ι), ‖f i‖ ≤ g i<GOAL>CauchySeq fun s => ∑ b ∈ s, f b
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ι → ℝ<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>volume (Metric.ball a r) = ofReal ((2 * r) ^ Fintype.card ι)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ι → ℝ<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>ofReal (2 * r) ^ Finset.univ.card = ofReal ((2 * r) ^ Fintype.card ι)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>f : α → Bool<GOAL>l.length = (filter f l).length + (filter (fun x => !f x) l).length