ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp✝ : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)<VAR>s : O<VAR>hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)<VAR>h1p : 0 < 1 / ↑p<VAR>hvp : 0 < v ↑p<GOAL>1 / ↑p + 1 / ↑p ≤ 1
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp✝ : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)<VAR>s : O<VAR>hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)<VAR>h1p : 0 < 1 / ↑p<VAR>hvp : 0 < v ↑p<GOAL>1 + 1 ≤ ↑p
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : Cone F<VAR>X : C<VAR>h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones<VAR>s : Cone F<GOAL>(limitCone h).extend (homOfCone h s) = s
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : Cone F<VAR>X : C<VAR>h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones<VAR>s : Cone F<GOAL>(limitCone h).extend (homOfCone h (coneOfHom h (homOfCone h s))) = coneOfHom h (homOfCone h s)
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : Cone F<VAR>X : C<VAR>h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones<VAR>s : Cone F<GOAL>(limitCone h).extend (homOfCone h s) = coneOfHom h (homOfCone h s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>u : ℕ → ℝ<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : ∀ k < n, c * u k < u (k + 1)<GOAL>c ^ n * u 0 < u n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>u : ℕ → ℝ<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : ∀ k < n, c * u k < u (k + 1)<GOAL>c ^ 0 * u 0 ≤ u 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>u : ℕ → ℝ<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : ∀ k < n, c * u k < u (k + 1)<GOAL>∀ k < n, c ^ (k + 1) * u 0 ≤ c * (c ^ k * u 0)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : α<GOAL>nndist x y = (dist x y).toNNReal
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : PartialOrder α<VAR>a✝ b : α<VAR>a : ↑(Iic b)<GOAL>IsCoatom a ↔ ↑a ⋖ b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : PartialOrder α<VAR>a✝ b : α<VAR>a : ↑(Iic b)<GOAL>a ⋖ ⊤ ↔ ↑a ⋖ b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : PartialOrder α<VAR>a✝ b : α<VAR>a : ↑(Iic b)<GOAL>(range ⇑(OrderEmbedding.subtype fun c => c ≤ b)).OrdConnected
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : AddCommMonoid Q<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Module R P<VAR>inst✝² : Module R Q<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R M<VAR>f : Dual R M<VAR>m : M<VAR>f' : Dual R M<VAR>m' : M<GOAL>((Dual.transpose ((dualTensorHom R M M) (f ⊗ₜ[R] m))) f') m' = (((dualTensorHom R (Dual R M) (Dual R M)) ((Dual.eval R M) m ⊗ₜ[R] f)) f') m'
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : AddCommMonoid Q<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Module R P<VAR>inst✝² : Module R Q<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R M<VAR>f : Dual R M<VAR>m : M<VAR>f' : Dual R M<VAR>m' : M<GOAL>f m' * f' m = f' m * f m'
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n : ℕ<VAR>ha : 0 ≤ a<VAR>hn : n ≠ 0<GOAL>1 < a ^ n ↔ 1 < a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>inst✝¹ : RingHomInvPair σ σ'<VAR>inst✝ : RingHomInvPair σ' σ<VAR>e : M ≃+ M₂<VAR>as : List R<VAR>bs : List S<VAR>h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs<GOAL>IsRegular M as ↔ IsRegular M₂ bs
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>inst✝¹ : RingHomInvPair σ σ'<VAR>inst✝ : RingHomInvPair σ' σ<VAR>e : M ≃+ M₂<VAR>as : List R<VAR>bs : List S<VAR>h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs<GOAL>IsWeaklyRegular M as ∧ ¬Subsingleton (M ⧸ Ideal.ofList as • ⊤) ↔ IsWeaklyRegular M₂ bs ∧ ¬Subsingleton (M₂ ⧸ Ideal.ofList bs • ⊤)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>inst✝¹ : RingHomInvPair σ σ'<VAR>inst✝ : RingHomInvPair σ' σ<VAR>e : M ≃+ M₂<VAR>as : List R<VAR>bs : List S<VAR>h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs<VAR>e' : M ⧸ (Ideal.ofList as • ⊤).toAddSubgroup ≃+ M₂ ⧸ (Ideal.ofList bs • ⊤).toAddSubgroup := QuotientAddGroup.congr (Ideal.ofList as • ⊤).toAddSubgroup (Ideal.ofList bs • ⊤).toAddSubgroup e ⋯<GOAL>IsWeaklyRegular M as ∧ ¬Subsingleton (M ⧸ Ideal.ofList as • ⊤) ↔ IsWeaklyRegular M₂ bs ∧ ¬Subsingleton (M₂ ⧸ Ideal.ofList bs • ⊤)
<VAR>c : Char<VAR>cs : List Char<VAR>i : Pos<GOAL>{ s := { data := c :: cs }, i := i + c }.hasNext = { s := { data := cs }, i := i }.hasNext
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>ps : Set P<VAR>hps : ps ⊆ ↑s<VAR>p : P<GOAL>(∃ r, ∀ p1 ∈ ps, dist p1 p = r) ↔ ∃ r, ∀ p1 ∈ ps, dist p1 ↑((orthogonalProjection s) p) = r
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>ps : Set P<VAR>hps : ps ⊆ ↑s<VAR>p : P<VAR>h : (ps.Pairwise fun p1 p2 => dist p1 p = dist p2 p) ↔ ps.Pairwise fun p1 p2 => dist p1 ↑((orthogonalProjection s) p) = dist p2 ↑((orthogonalProjection s) p)<GOAL>(∃ r, ∀ p1 ∈ ps, dist p1 p = r) ↔ ∃ r, ∀ p1 ∈ ps, dist p1 ↑((orthogonalProjection s) p) = r
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>ps : Set P<VAR>hps : ps ⊆ ↑s<VAR>p : P<VAR>h : (∃ z, ∀ x ∈ ps, dist x p = z) ↔ ∃ z, ∀ x ∈ ps, dist x ↑((orthogonalProjection s) p) = z<GOAL>(∃ r, ∀ p1 ∈ ps, dist p1 p = r) ↔ ∃ r, ∀ p1 ∈ ps, dist p1 ↑((orthogonalProjection s) p) = r
<VAR>m n : ℤ<GOAL>m >>> (-n) = m <<< n
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Subgroup G<VAR>f g : (i : ι) → ↥(H i)<VAR>hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y<VAR>hind : CompleteLattice.Independent H<GOAL>Function.Injective ⇑(noncommPiCoprod hcomm)
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Subgroup G<VAR>f g : (i : ι) → ↥(H i)<VAR>hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y<VAR>hind : CompleteLattice.Independent H<GOAL>CompleteLattice.Independent fun i => (H i).subtype.range
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Subgroup G<VAR>f g : (i : ι) → ↥(H i)<VAR>hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y<VAR>hind : CompleteLattice.Independent H<GOAL>∀ (i : ι), Function.Injective ⇑(H i).subtype
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x val✝ : α<VAR>property✝ : val✝ ∈ Iic b<GOAL>projIic b ↑⟨val✝, property✝⟩ = ⟨val✝, property✝⟩
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype K<VAR>inst✝ : Finite σ<GOAL>Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1)) = ⊤
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype K<VAR>inst✝ : Finite σ<VAR>val✝ : Fintype σ<GOAL>Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1)) = ⊤
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype K<VAR>inst✝ : Finite σ<VAR>val✝ : Fintype σ<VAR>e : (σ → K) → K<VAR>x✝ : e ∈ ⊤<GOAL>∃ y ∈ restrictDegree σ K (Fintype.card K - 1), (evalₗ K σ) y = e
<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : ArithmeticFunction R<VAR>x : ℕ<GOAL>((↑ζ).pmul f) x = f x
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Add G<VAR>a b : Multiplicative G<GOAL>(fun a => single a 1) (a * b) = (fun a => single a 1) a * (fun a => single a 1) b
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Add G<VAR>a b : Multiplicative G<GOAL>single (a * b) 1 = single (a + b) 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>hu : ∀ x ∈ U, f ∈ x.asIdeal.primeCompl<VAR>x : ↥(unop (op U))<GOAL>(algebraMap R (Localizations R ↑x)) 0 = ↑0 x * (algebraMap R (Localizations R ↑x)) ↑⟨f, ⋯⟩
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>hu : ∀ x ∈ U, f ∈ x.asIdeal.primeCompl<VAR>x : ↥(unop (op U))<GOAL>0 = ↑0 x * (algebraMap R (Localizations R ↑x)) ↑⟨f, ⋯⟩
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>A : Matrix m n α<GOAL>‖A‖ = ↑(Finset.univ.sup fun i => Finset.univ.sup fun j => ‖A i j‖₊)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.4190, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.ShortExact<GOAL>Mono S.op.f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.4190, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.ShortExact<VAR>this : Epi S.g<GOAL>Mono S.op.f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.4190, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.ShortExact<GOAL>Epi S.op.g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.4190, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.ShortExact<VAR>this : Mono S.f<GOAL>Epi S.op.g
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x✝ : E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf' : UniformCauchySeqOn f' l s<VAR>hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y<VAR>x₀ x : E<VAR>hx₀ : x₀ ∈ s<VAR>hx : x ∈ s<VAR>hfg : Cauchy (map (fun n => f n x₀) l)<GOAL>Cauchy (map (fun n => f n x) l)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x✝ : E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf' : UniformCauchySeqOn f' l s<VAR>hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y<VAR>x₀ x : E<VAR>hx₀ : x₀ ∈ s<VAR>hx : x ∈ s<VAR>hfg : Cauchy (map (fun n => f n x₀) l)<VAR>this : l.NeBot<GOAL>Cauchy (map (fun n => f n x) l)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x✝ : E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf' : UniformCauchySeqOn f' l s<VAR>hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y<VAR>x₀ x : E<VAR>hx₀ : x₀ ∈ s<VAR>hx : x ∈ s<VAR>hfg : Cauchy (map (fun n => f n x₀) l)<VAR>this : l.NeBot<VAR>t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}<GOAL>Cauchy (map (fun n => f n x) l)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x✝ : E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf' : UniformCauchySeqOn f' l s<VAR>hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y<VAR>x₀ x : E<VAR>hx₀ : x₀ ∈ s<VAR>hx : x ∈ s<VAR>hfg : Cauchy (map (fun n => f n x₀) l)<VAR>this : l.NeBot<VAR>t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}<GOAL>s ⊆ t
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x✝ : E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf' : UniformCauchySeqOn f' l s<VAR>hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y<VAR>x₀ x : E<VAR>hx₀ : x₀ ∈ s<VAR>hx : x ∈ s<VAR>hfg : Cauchy (map (fun n => f n x₀) l)<VAR>this : l.NeBot<VAR>t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}<VAR>A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t<GOAL>s ⊆ t
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x✝ : E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf' : UniformCauchySeqOn f' l s<VAR>hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y<VAR>x₀ x : E<VAR>hx₀ : x₀ ∈ s<VAR>hx : x ∈ s<VAR>hfg : Cauchy (map (fun n => f n x₀) l)<VAR>this : l.NeBot<VAR>t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}<VAR>A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t<VAR>open_t : IsOpen t<GOAL>s ⊆ t
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x✝ : E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf' : UniformCauchySeqOn f' l s<VAR>hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y<VAR>x₀ x : E<VAR>hx₀ : x₀ ∈ s<VAR>hx : x ∈ s<VAR>hfg : Cauchy (map (fun n => f n x₀) l)<VAR>this : l.NeBot<VAR>t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}<VAR>A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t<VAR>open_t : IsOpen t<VAR>st_nonempty : (s ∩ t).Nonempty<GOAL>s ⊆ t
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x✝ : E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf' : UniformCauchySeqOn f' l s<VAR>hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y<VAR>x₀ x : E<VAR>hx₀ : x₀ ∈ s<VAR>hx : x ∈ s<VAR>hfg : Cauchy (map (fun n => f n x₀) l)<VAR>this : l.NeBot<VAR>t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}<VAR>A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t<VAR>open_t : IsOpen t<VAR>st_nonempty : (s ∩ t).Nonempty<GOAL>closure t ∩ s ⊆ t
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x✝¹ : E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf' : UniformCauchySeqOn f' l s<VAR>hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y<VAR>x₀ x✝ : E<VAR>hx₀ : x₀ ∈ s<VAR>hx : x✝ ∈ s<VAR>hfg : Cauchy (map (fun n => f n x₀) l)<VAR>this : l.NeBot<VAR>t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}<VAR>A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t<VAR>open_t : IsOpen t<VAR>st_nonempty : (s ∩ t).Nonempty<VAR>x : E<VAR>xt : x ∈ closure t<VAR>xs : x ∈ s<GOAL>x ∈ t
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x✝¹ : E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf' : UniformCauchySeqOn f' l s<VAR>hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y<VAR>x₀ x✝ : E<VAR>hx₀ : x₀ ∈ s<VAR>hx : x✝ ∈ s<VAR>hfg : Cauchy (map (fun n => f n x₀) l)<VAR>this : l.NeBot<VAR>t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}<VAR>A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t<VAR>open_t : IsOpen t<VAR>st_nonempty : (s ∩ t).Nonempty<VAR>x : E<VAR>xt : x ∈ closure t<VAR>xs : x ∈ s<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : Metric.ball x ε ⊆ s<GOAL>x ∈ t
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x✝¹ : E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf' : UniformCauchySeqOn f' l s<VAR>hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y<VAR>x₀ x✝ : E<VAR>hx₀ : x₀ ∈ s<VAR>hx : x✝ ∈ s<VAR>hfg : Cauchy (map (fun n => f n x₀) l)<VAR>this : l.NeBot<VAR>t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}<VAR>A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t<VAR>open_t : IsOpen t<VAR>st_nonempty : (s ∩ t).Nonempty<VAR>x : E<VAR>xt : x ∈ closure t<VAR>xs : x ∈ s<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : Metric.ball x ε ⊆ s<VAR>y : E<VAR>yt : y ∈ t<VAR>hxy : dist x y < ε / 2<GOAL>x ∈ t
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x✝¹ : E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf' : UniformCauchySeqOn f' l s<VAR>hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y<VAR>x₀ x✝ : E<VAR>hx₀ : x₀ ∈ s<VAR>hx : x✝ ∈ s<VAR>hfg : Cauchy (map (fun n => f n x₀) l)<VAR>this : l.NeBot<VAR>t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}<VAR>A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t<VAR>open_t : IsOpen t<VAR>st_nonempty : (s ∩ t).Nonempty<VAR>x : E<VAR>xt : x ∈ closure t<VAR>xs : x ∈ s<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : Metric.ball x ε ⊆ s<VAR>y : E<VAR>yt : y ∈ t<VAR>hxy : dist x y < ε / 2<VAR>B : Metric.ball y (ε / 2) ⊆ Metric.ball x ε<GOAL>x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : SemilatticeInf β<VAR>inst✝ : ContinuousInf β<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → C(α, β)<VAR>x✝ : α<GOAL>(s.inf' H f) x✝ = s.inf' H (fun i => ⇑(f i)) x✝
<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>t : Type u → Type u → Type u<VAR>inst✝⁵ : Bitraversable t<VAR>β : Type u<VAR>F G : Type u → Type u<VAR>inst✝⁴ : Applicative F<VAR>inst✝³ : Applicative G<VAR>inst✝² : LawfulBitraversable t<VAR>inst✝¹ : LawfulApplicative F<VAR>inst✝ : LawfulApplicative G<VAR>α β₀ β₁ β₂ : Type u<VAR>g : β₀ → F β₁<VAR>g' : β₁ → G β₂<VAR>x : t α β₀<GOAL>Comp.mk (tsnd g' <$> tsnd g x) = tsnd (Comp.mk ∘ map g' ∘ g) x
<VAR>t : Type u → Type u → Type u<VAR>inst✝⁵ : Bitraversable t<VAR>β : Type u<VAR>F G : Type u → Type u<VAR>inst✝⁴ : Applicative F<VAR>inst✝³ : Applicative G<VAR>inst✝² : LawfulBitraversable t<VAR>inst✝¹ : LawfulApplicative F<VAR>inst✝ : LawfulApplicative G<VAR>α β₀ β₁ β₂ : Type u<VAR>g : β₀ → F β₁<VAR>g' : β₁ → G β₂<VAR>x : t α β₀<GOAL>bitraverse (Comp.mk ∘ map pure ∘ pure) (Comp.mk ∘ map g' ∘ g) x = tsnd (Comp.mk ∘ map g' ∘ g) x
<VAR>t : Type u → Type u → Type u<VAR>inst✝⁵ : Bitraversable t<VAR>β : Type u<VAR>F G : Type u → Type u<VAR>inst✝⁴ : Applicative F<VAR>inst✝³ : Applicative G<VAR>inst✝² : LawfulBitraversable t<VAR>inst✝¹ : LawfulApplicative F<VAR>inst✝ : LawfulApplicative G<VAR>α β₀ β₁ β₂ : Type u<VAR>g : β₀ → F β₁<VAR>g' : β₁ → G β₂<VAR>x : t α β₀<GOAL>bitraverse (fun x => Comp.mk (pure (pure x))) (fun x => Comp.mk (g' <$> g x)) x = tsnd (fun x => Comp.mk (g' <$> g x)) x
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : LinearOrderedRing R<VAR>inst✝⁴ : FloorRing R<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : OrderTopology R<VAR>inst✝¹ : MeasurableSpace R<VAR>inst✝ : OpensMeasurableSpace R<VAR>x : R<GOAL>MeasurableSet (ceil ⁻¹' {⌈x⌉})
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Module R V<VAR>inst✝² : Module A V<VAR>inst✝¹ : IsScalarTower R A V<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticForm R V<VAR>v : V<GOAL>(toBaseChange A Q) ((ofBaseChange A Q) (1 ⊗ₜ[R] (ι Q) v)) = 1 ⊗ₜ[R] (ι Q) v
<VAR>N : ℕ<GOAL>N.smoothNumbersᶜ \ {0} ⊆ {n | N ≤ n}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν✝ : Measure α<VAR>mb : MeasurableSpace β<VAR>ν : Measure β<VAR>g : α → β<VAR>hg : MeasurePreserving g μ ν<VAR>hge : MeasurableEmbedding g<VAR>f : β → ℝ≥0∞<GOAL>∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν