ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : InnerProductSpace 𝕜 E'<VAR>inst✝⁹ : CompleteSpace E'<VAR>inst✝⁸ : NormedSpace ℝ E'<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace 𝕜 F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>inst✝ : NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(Lp F p μ) → Prop<VAR>h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)<VAR>h_add : ∀ ⦃f g : α → F⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), StronglyMeasurable f → StronglyMeasurable g → Disjoint (Function.support f) (Function.support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P ↑f}<VAR>f✝ : ↥(Lp F p μ)<VAR>hf✝ : AEStronglyMeasurable' m (↑↑f✝) μ<VAR>f g : α → F<VAR>hf : Memℒp f p μ<VAR>hg : Memℒp g p μ<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>hgm : AEStronglyMeasurable' m g μ<VAR>h_disj✝ : Disjoint (Function.support f) (Function.support g)<VAR>s_f : Set α := Function.support (AEStronglyMeasurable'.mk f hfm)<VAR>hs_f : MeasurableSet s_f<VAR>hs_f_eq : s_f =ᶠ[ae μ] Function.support f<VAR>s_g : Set α := Function.support (AEStronglyMeasurable'.mk g hgm)<VAR>hs_g : MeasurableSet s_g<VAR>hs_g_eq : s_g =ᶠ[ae μ] Function.support g<VAR>h_inter_empty : s_f ∩ s_g =ᶠ[ae μ] ∅<VAR>f' : α → F := (s_f \ s_g).indicator (AEStronglyMeasurable'.mk f hfm)<VAR>hff' : f =ᶠ[ae μ] f'<VAR>hf'_meas : StronglyMeasurable f'<VAR>hf'_Lp : Memℒp f' p μ<VAR>hPf : P (Memℒp.toLp f' hf'_Lp)<VAR>g' : α → F := (s_g \ s_f).indicator (AEStronglyMeasurable'.mk g hgm)<VAR>hgg' : g =ᶠ[ae μ] g'<VAR>hg'_meas : StronglyMeasurable g'<VAR>hg'_Lp : Memℒp g' p μ<VAR>hPg : P (Memℒp.toLp g' hg'_Lp)<VAR>h_disj : Disjoint (Function.support f') (Function.support g')<GOAL>P (Memℒp.toLp f' hf'_Lp + Memℒp.toLp g' hg'_Lp)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u✝ : Multiset α<VAR>a b : α<VAR>s t u : Multiset α<GOAL>s ∩ t + u = (s + u) ∩ (t + u)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u✝ : Multiset α<VAR>a b : α<VAR>s t u : Multiset α<VAR>h : ¬s ∩ t + u = (s + u) ∩ (t + u)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u✝ : Multiset α<VAR>a✝ b : α<VAR>s t u : Multiset α<VAR>h : ¬s ∩ t + u = (s + u) ∩ (t + u)<VAR>a : α<VAR>hl : a ::ₘ (s ∩ t + u) ≤ (s + u) ∩ (t + u)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u✝ : Multiset α<VAR>a✝ b : α<VAR>s t u : Multiset α<VAR>h : ¬s ∩ t + u = (s + u) ∩ (t + u)<VAR>a : α<VAR>hl : a ::ₘ s ∩ t + u ≤ (s + u) ∩ (t + u)<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Group α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(mulETransformRight e x).1 * (mulETransformRight e x).2 ⊆ x.1 * x.2
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Group α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>op e • x.1 * e⁻¹ • x.2 ⊆ x.1 * x.2
<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>𝒰 : X.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>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>∀ (i : 𝒰.J), pullback.map (𝒰.map i ≫ f) g f g (𝒰.map i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ = (Iso.refl ((fun i => pullback (𝒰.map i ≫ f) g) i)).hom ≫ ((gluing 𝒰 f g).openCover.pushforwardIso (limit.isoLimitCone { cone := PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯, isLimit := gluedIsLimit 𝒰 f g }).inv).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>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>i : 𝒰.J<GOAL>pullback.map (𝒰.map i ≫ f) g f g (𝒰.map i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ = (Iso.refl ((fun i => pullback (𝒰.map i ≫ f) g) i)).hom ≫ ((gluing 𝒰 f g).openCover.pushforwardIso (limit.isoLimitCone { cone := PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯, isLimit := gluedIsLimit 𝒰 f g }).inv).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>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>i : 𝒰.J<GOAL>pullback.map (𝒰.map i ≫ f) g f g (𝒰.map i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ = (Iso.refl (pullback (𝒰.map i ≫ f) g)).hom ≫ (gluing 𝒰 f g).ι ((Equiv.refl 𝒰.J) i) ≫ (limit.isoLimitCone { cone := PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯, isLimit := gluedIsLimit 𝒰 f g }).inv
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>hn : ¬n = 0<GOAL>IsSolvable (X ^ n - 1).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<GOAL>IsSolvable (X ^ n - 1).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : X ^ n - 1 ≠ 0<GOAL>IsSolvable (X ^ n - 1).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : X ^ n - 1 ≠ 0<GOAL>∀ (a b : (X ^ n - 1).Gal), a * b = b * a
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : X ^ n - 1 ≠ 0<VAR>σ τ : (X ^ n - 1).Gal<VAR>a : (X ^ n - 1).SplittingField<VAR>ha : a ∈ (X ^ n - 1).rootSet (X ^ n - 1).SplittingField<GOAL>(σ * τ) a = (τ * σ) a
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : X ^ n - 1 ≠ 0<VAR>σ τ : (X ^ n - 1).Gal<VAR>a : (X ^ n - 1).SplittingField<VAR>ha : a ^ n = 1<GOAL>(σ * τ) a = (τ * σ) a
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : X ^ n - 1 ≠ 0<VAR>σ τ : (X ^ n - 1).Gal<VAR>a : (X ^ n - 1).SplittingField<VAR>ha : a ^ n = 1<VAR>key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m<GOAL>(σ * τ) a = (τ * σ) a
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : X ^ n - 1 ≠ 0<VAR>σ τ : (X ^ n - 1).Gal<VAR>a : (X ^ n - 1).SplittingField<VAR>ha : a ^ n = 1<VAR>key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m<VAR>c : ℕ<VAR>hc : σ a = a ^ c<VAR>d : ℕ<VAR>hd : τ a = a ^ d<GOAL>(σ * τ) a = (τ * σ) a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>r : ℝ<VAR>ha : 0 ≤ r<VAR>f : ι → ℝ<GOAL>(⨆ i, f i) * r = ⨆ i, f i * r
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>J : Type w<VAR>inst✝² : Category.{w', w} J<VAR>F : J ⥤ C<VAR>inst✝¹ : PreservesLimit F G<VAR>inst✝ : HasLimit F<VAR>t : Cone F<VAR>j✝ : J<GOAL>(G.map (limit.lift F t) ≫ (preservesLimitIso G F).hom) ≫ limit.π (F ⋙ G) j✝ = limit.lift (F ⋙ G) (G.mapCone t) ≫ limit.π (F ⋙ G) j✝
<VAR>a✝ b c a n : ℕ<VAR>ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))<GOAL>Set.InjOn (fun x => x % a) ↑(Ico (n + 1) (n + 1 + a))
<VAR>a✝ b c a n : ℕ<VAR>ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))<GOAL>Set.InjOn (fun x => x % a) ↑((insert (n + a) (Ico n (n + a))).erase n)
<VAR>a✝ b c a n : ℕ<VAR>ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))<VAR>k : ℕ<VAR>hk : k ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)<VAR>l : ℕ<VAR>hl : l ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)<VAR>hkl : k % a = l % a<GOAL>k = l
<VAR>a✝ b c a n : ℕ<VAR>ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))<VAR>k : ℕ<VAR>hk : k ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)<VAR>l : ℕ<VAR>hl : l ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)<VAR>hkl : k % a = l % a<VAR>ha : 0 < a<GOAL>k = l
<VAR>a✝ b c a n : ℕ<VAR>ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))<VAR>k l : ℕ<VAR>hkl : k % a = l % a<VAR>ha : 0 < a<VAR>hk : k ≠ n ∧ (k = n + a ∨ k ∈ Ico n (n + a))<VAR>hl : l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))<GOAL>k = l
<GOAL>∀ {x y z : ℝ}, x ∈ univ → z ∈ univ → x < y → y < z → (rexp y - rexp x) / (y - x) < (rexp z - rexp y) / (z - y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (LowerSet α)<VAR>s t : LowerSet α<VAR>a : α<VAR>f : (i : ι) → κ i → LowerSet α<GOAL>a ∈ ⨅ i, ⨅ j, f i j ↔ ∀ (i : ι) (j : κ i), a ∈ f i j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝⁷ : Category.{?u.284, u_1} C<VAR>inst✝⁶ : Category.{?u.288, u_2} D<VAR>inst✝⁵ : Category.{?u.292, u_3} E<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasShift D ℤ<VAR>inst✝² : HasShift E ℤ<VAR>F : C ⥤ D<VAR>inst✝¹ : F.CommShift ℤ<VAR>G : D ⥤ E<VAR>inst✝ : G.CommShift ℤ<VAR>X✝ Y✝ : Triangle C<VAR>f : X✝ ⟶ Y✝<GOAL>F.map X✝.mor₁ ≫ F.map f.hom₂ = F.map f.hom₁ ≫ F.map Y✝.mor₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝⁷ : Category.{?u.284, u_1} C<VAR>inst✝⁶ : Category.{?u.288, u_2} D<VAR>inst✝⁵ : Category.{?u.292, u_3} E<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasShift D ℤ<VAR>inst✝² : HasShift E ℤ<VAR>F : C ⥤ D<VAR>inst✝¹ : F.CommShift ℤ<VAR>G : D ⥤ E<VAR>inst✝ : G.CommShift ℤ<VAR>X✝ Y✝ : Triangle C<VAR>f : X✝ ⟶ Y✝<GOAL>F.map X✝.mor₂ ≫ F.map f.hom₃ = F.map f.hom₂ ≫ F.map Y✝.mor₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝⁷ : Category.{?u.284, u_1} C<VAR>inst✝⁶ : Category.{?u.288, u_2} D<VAR>inst✝⁵ : Category.{?u.292, u_3} E<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasShift D ℤ<VAR>inst✝² : HasShift E ℤ<VAR>F : C ⥤ D<VAR>inst✝¹ : F.CommShift ℤ<VAR>G : D ⥤ E<VAR>inst✝ : G.CommShift ℤ<VAR>X✝ Y✝ : Triangle C<VAR>f : X✝ ⟶ Y✝<GOAL>(F.map X✝.mor₃ ≫ (F.commShiftIso 1).hom.app X✝.obj₁) ≫ (shiftFunctor D 1).map (F.map f.hom₁) = F.map f.hom₃ ≫ F.map Y✝.mor₃ ≫ (F.commShiftIso 1).hom.app Y✝.obj₁
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x✝ : M<VAR>c✝ c : M'<VAR>x : M<GOAL>HasMFDerivAt I I' (fun x => c) x 0
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x✝ : M<VAR>c✝ c : M'<VAR>x : M<GOAL>HasFDerivWithinAt (writtenInExtChartAt I I' x fun x => c) 0 (range ↑I) (↑(extChartAt I x) x)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>φ : R⟦X⟧<GOAL>X ^ n ∣ φ ↔ ∀ m < n, (coeff R m) φ = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>φ : R⟦X⟧<GOAL>(∀ m < n, (coeff R m) φ = 0) ↔ ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff R m) φ = 0
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>e✝ : Basis ι R M<VAR>f : M ≃ₗ[R] M<VAR>e : M ≃ₗ[R] M'<GOAL>LinearEquiv.det (e.symm ≪≫ₗ f ≪≫ₗ e) = LinearEquiv.det f
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : m ≤ k * n<GOAL>m / k ≤ n
<VAR>a b c d m n : ℕ<VAR>p q : ℕ → Prop<VAR>h : m ≤ 0 * n<GOAL>m / 0 ≤ n
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : m ≤ k * n<VAR>hk : k > 0<GOAL>m / k ≤ n
<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>I J : FractionalIdeal S P<VAR>i j : P<VAR>hi : i ∈ I<VAR>hj : j ∈ J<GOAL>i * j ∈ I * J
<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>I J : FractionalIdeal S P<VAR>i j : P<VAR>hi : i ∈ I<VAR>hj : j ∈ J<GOAL>i * j ∈ ⟨↑I * ↑J, ⋯⟩
<VAR>α✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : MeasurableSpace X<VAR>inst✝⁹ : BorelSpace X<VAR>inst✝⁸ : R1Space X<VAR>inst✝⁷ : TopologicalSpace Y<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : BorelSpace Y<VAR>inst✝⁴ : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure ν<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>inst✝ : Fact (1 ≤ p)<VAR>α : Type u_5<VAR>l : Filter α<VAR>f : α → ↥(Lp E p ν)<VAR>f₀ : ↥(Lp E p ν)<VAR>g : α → C(X, Y)<VAR>g₀ : C(X, Y)<VAR>hf : Tendsto f l (𝓝 f₀)<VAR>hg : Tendsto g l (𝓝 g₀)<VAR>hgm : ∀ (a : α), MeasurePreserving (⇑(g a)) μ ν<VAR>hgm₀ : MeasurePreserving (⇑g₀) μ ν<VAR>hp : p ≠ ⊤<GOAL>Tendsto (fun a => (Lp.compMeasurePreserving ⇑(g a) ⋯) (f a)) l (𝓝 ((Lp.compMeasurePreserving (⇑g₀) hgm₀) f₀))
<VAR>α✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : MeasurableSpace X<VAR>inst✝⁹ : BorelSpace X<VAR>inst✝⁸ : R1Space X<VAR>inst✝⁷ : TopologicalSpace Y<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : BorelSpace Y<VAR>inst✝⁴ : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure ν<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>inst✝ : Fact (1 ≤ p)<VAR>α : Type u_5<VAR>l : Filter α<VAR>f : α → ↥(Lp E p ν)<VAR>f₀ : ↥(Lp E p ν)<VAR>g : α → C(X, Y)<VAR>g₀ : C(X, Y)<VAR>hf : Tendsto f l (𝓝 f₀)<VAR>hg : Tendsto g l (𝓝 g₀)<VAR>hgm : ∀ (a : α), MeasurePreserving (⇑(g a)) μ ν<VAR>hgm₀ : MeasurePreserving (⇑g₀) μ ν<VAR>hp : p ≠ ⊤<VAR>this : Tendsto (fun gf => (Lp.compMeasurePreserving ⇑↑gf.2 ⋯) gf.1) (𝓝 (f₀, ⟨g₀, hgm₀⟩)) (𝓝 ((Lp.compMeasurePreserving ⇑↑(f₀, ⟨g₀, hgm₀⟩).2 ⋯) (f₀, ⟨g₀, hgm₀⟩).1))<GOAL>Tendsto (fun a => (Lp.compMeasurePreserving ⇑(g a) ⋯) (f a)) l (𝓝 ((Lp.compMeasurePreserving (⇑g₀) hgm₀) f₀))
<VAR>α✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : MeasurableSpace X<VAR>inst✝⁹ : BorelSpace X<VAR>inst✝⁸ : R1Space X<VAR>inst✝⁷ : TopologicalSpace Y<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : BorelSpace Y<VAR>inst✝⁴ : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure ν<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>inst✝ : Fact (1 ≤ p)<VAR>α : Type u_5<VAR>l : Filter α<VAR>f : α → ↥(Lp E p ν)<VAR>f₀ : ↥(Lp E p ν)<VAR>g : α → C(X, Y)<VAR>g₀ : C(X, Y)<VAR>hf : Tendsto f l (𝓝 f₀)<VAR>hgm : ∀ (a : α), MeasurePreserving (⇑(g a)) μ ν<VAR>hgm₀ : MeasurePreserving (⇑g₀) μ ν<VAR>hp : p ≠ ⊤<VAR>this : Tendsto (fun gf => (Lp.compMeasurePreserving ⇑↑gf.2 ⋯) gf.1) (𝓝 (f₀, ⟨g₀, hgm₀⟩)) (𝓝 ((Lp.compMeasurePreserving ⇑↑(f₀, ⟨g₀, hgm₀⟩).2 ⋯) (f₀, ⟨g₀, hgm₀⟩).1))<VAR>hg : Tendsto (fun a => ⟨g a, ⋯⟩) l (𝓝 ⟨g₀, hgm₀⟩)<GOAL>Tendsto (fun a => (Lp.compMeasurePreserving ⇑(g a) ⋯) (f a)) l (𝓝 ((Lp.compMeasurePreserving (⇑g₀) hgm₀) f₀))
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ x✝¹ L₁✝ L₂✝ : List (α × Bool)<VAR>x✝ : α<VAR>b✝ : Bool<GOAL>Step (x✝¹ ++ (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝)) (x✝¹ ++ (L₁✝ ++ L₂✝))
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ x✝¹ L₁✝ L₂✝ : List (α × Bool)<VAR>x✝ : α<VAR>b✝ : Bool<GOAL>Step (x✝¹ ++ L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝) (x✝¹ ++ L₁✝ ++ L₂✝)
<VAR>q : ℚ<VAR>x y : ℝ<VAR>h : Irrational (↑q - x)<GOAL>Irrational (↑q + -x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f g : α → β<VAR>hf : AEStronglyMeasurable f μ<GOAL>∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f g : α → β<VAR>hf : AEStronglyMeasurable f μ<GOAL>∀ᵐ (x : α) ∂μ, f x ∈ range (AEStronglyMeasurable.mk f hf)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f g : α → β<VAR>hf : AEStronglyMeasurable f μ<VAR>x : α<VAR>hx : f x = AEStronglyMeasurable.mk f hf x<GOAL>f x ∈ range (AEStronglyMeasurable.mk f hf)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g volume t₁ t₂<VAR>hT : 0 < T<VAR>t : ℝ<VAR>ε : ℝ := Int.fract (t / T) * T<GOAL>sInf ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x ≤ ∫ (x : ℝ) in 0 ..t, g x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g volume t₁ t₂<VAR>hT : 0 < T<VAR>t : ℝ<VAR>ε : ℝ := Int.fract (t / T) * T<GOAL>sInf ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x ≤ (∫ (x : ℝ) in 0 ..ε, g x) + ∫ (x : ℝ) in ε..Int.fract (t / T) * T + ⌊t / T⌋ • T, g x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g volume t₁ t₂<VAR>hT : 0 < T<VAR>t : ℝ<VAR>ε : ℝ := Int.fract (t / T) * T<GOAL>sInf ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) ≤ ∫ (x : ℝ) in 0 ..ε, g x
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>l : Type u_4<VAR>E : Type u_5<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>U : Matrix n n 𝕜<VAR>hU : U ∈ Matrix.unitaryGroup n 𝕜<VAR>i j : n<VAR>norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2<GOAL>‖U i j‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>l : Type u_4<VAR>E : Type u_5<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>U : Matrix n n 𝕜<VAR>hU : U ∈ Matrix.unitaryGroup n 𝕜<VAR>i j : n<VAR>norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2<VAR>diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)<GOAL>‖U i j‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>l : Type u_4<VAR>E : Type u_5<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>U : Matrix n n 𝕜<VAR>hU : U ∈ Matrix.unitaryGroup n 𝕜<VAR>i j : n<VAR>norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2<VAR>diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)<VAR>re_diag_eq_norm_sum : RCLike.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2<GOAL>‖U i j‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>l : Type u_4<VAR>E : Type u_5<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>U : Matrix n n 𝕜<VAR>hU : U ∈ Matrix.unitaryGroup n 𝕜<VAR>i j : n<VAR>norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2<VAR>diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)<VAR>re_diag_eq_norm_sum : RCLike.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2<VAR>mul_eq_one : U * Uᴴ = 1<GOAL>‖U i j‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>l : Type u_4<VAR>E : Type u_5<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>U : Matrix n n 𝕜<VAR>hU : U ∈ Matrix.unitaryGroup n 𝕜<VAR>i j : n<VAR>norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2<VAR>diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)<VAR>re_diag_eq_norm_sum : RCLike.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2<VAR>mul_eq_one : U * Uᴴ = 1<VAR>diag_eq_one : RCLike.re ((U * Uᴴ) i i) = 1<GOAL>‖U i j‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>l : Type u_4<VAR>E : Type u_5<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>U : Matrix n n 𝕜<VAR>hU : U ∈ Matrix.unitaryGroup n 𝕜<VAR>i j : n<VAR>norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2<VAR>diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)<VAR>re_diag_eq_norm_sum : RCLike.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2<VAR>mul_eq_one : U * Uᴴ = 1<VAR>diag_eq_one : RCLike.re ((U * Uᴴ) i i) = 1<GOAL>‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<VAR>s : Set M<VAR>κ : Cardinal.{w'}<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w', w} #↑s ≤ lift.{w, w'} κ<VAR>h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ<VAR>h4 : lift.{w, w'} κ ≤ lift.{w', w} #M<GOAL>∃ S, s ⊆ ↑S ∧ lift.{w', w} #↥S = lift.{w, w'} κ
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<VAR>s : Set M<VAR>κ : Cardinal.{w'}<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w', w} #↑s ≤ lift.{w, w'} κ<VAR>h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ<VAR>h4 : lift.{w, w'} κ ≤ lift.{w', w} #M<VAR>s' : Set (ULift.{w', w} M)<VAR>hs' : #↑s' = lift.{w, w'} κ<GOAL>∃ S, s ⊆ ↑S ∧ lift.{w', w} #↥S = lift.{w, w'} κ
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<VAR>s : Set M<VAR>κ : Cardinal.{w'}<VAR>h1 : ℵ₀ ≤ lift.{w, w'} κ<VAR>h2 : lift.{w', w} #↑s ≤ lift.{w, w'} κ<VAR>h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ<VAR>h4 : lift.{w, w'} κ ≤ lift.{w', w} #M<VAR>s' : Set (ULift.{w', w} M)<VAR>hs' : #↑s' = lift.{w, w'} κ<GOAL>∃ S, s ⊆ ↑S ∧ lift.{w', w} #↥S = lift.{w, w'} κ
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<VAR>s : Set M<VAR>κ : Cardinal.{w'}<VAR>h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ<VAR>h4 : lift.{w, w'} κ ≤ lift.{w', w} #M<VAR>s' : Set (ULift.{w', w} M)<VAR>h2 : lift.{w', w} #↑s ≤ #↑s'<VAR>h1 : ℵ₀ ≤ #↑s'<VAR>hs' : #↑s' = lift.{w, w'} κ<GOAL>∃ S, s ⊆ ↑S ∧ lift.{w', w} #↥S = #↑s'
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<VAR>s : Set M<VAR>κ : Cardinal.{w'}<VAR>h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ<VAR>h4 : lift.{w, w'} κ ≤ lift.{w', w} #M<VAR>s' : Set (ULift.{w', w} M)<VAR>h2 : lift.{w', w} #↑s ≤ #↑s'<VAR>h1 : ℵ₀ ≤ #↑s'<VAR>hs' : #↑s' = lift.{w, w'} κ<GOAL>lift.{w', w} #↥((closure (L.sum L.skolem₁)).toFun (s ∪ ⇑Equiv.ulift '' s')).elementarySkolem₁Reduct = #↑s'