ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>inst✝ : PolishSpace α<VAR>s : ℕ → Set α<VAR>m : ℕ → TopologicalSpace α<VAR>mt : ∀ (n : ℕ), m n ≤ t<VAR>m_polish : ∀ (n : ℕ), PolishSpace α<VAR>h✝ : ∀ (n : ℕ), IsClosed (s n)<VAR>m_open : ∀ (n : ℕ), IsOpen (s n)<VAR>t' : TopologicalSpace α<VAR>t'm : ∀ (n : ℕ), t' ≤ m n<VAR>t'_polish : PolishSpace α<GOAL>IsClopenable (⋃ n, s n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>inst✝ : PolishSpace α<VAR>s : ℕ → Set α<VAR>m : ℕ → TopologicalSpace α<VAR>mt : ∀ (n : ℕ), m n ≤ t<VAR>m_polish : ∀ (n : ℕ), PolishSpace α<VAR>h✝ : ∀ (n : ℕ), IsClosed (s n)<VAR>m_open : ∀ (n : ℕ), IsOpen (s n)<VAR>t' : TopologicalSpace α<VAR>t'm : ∀ (n : ℕ), t' ≤ m n<VAR>t'_polish : PolishSpace α<VAR>A : IsOpen (⋃ n, s n)<GOAL>IsClopenable (⋃ n, s n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>inst✝ : PolishSpace α<VAR>s : ℕ → Set α<VAR>m : ℕ → TopologicalSpace α<VAR>mt : ∀ (n : ℕ), m n ≤ t<VAR>m_polish : ∀ (n : ℕ), PolishSpace α<VAR>h✝ : ∀ (n : ℕ), IsClosed (s n)<VAR>m_open : ∀ (n : ℕ), IsOpen (s n)<VAR>t' : TopologicalSpace α<VAR>t'm : ∀ (n : ℕ), t' ≤ m n<VAR>t'_polish : PolishSpace α<VAR>A : IsOpen (⋃ n, s n)<VAR>t'' : TopologicalSpace α<VAR>t''_le : t'' ≤ t'<VAR>t''_polish : PolishSpace α<VAR>h1 : IsClosed (⋃ n, s n)<VAR>h2 : IsOpen (⋃ n, s n)<GOAL>IsClopenable (⋃ n, s n)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field L'<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K L'<VAR>S✝ : IntermediateField K L<VAR>S : Subalgebra K L<VAR>inv_mem : ∀ x ∈ S, x⁻¹ ∈ S<VAR>x✝ : L<GOAL>x✝ ∈ (S.toIntermediateField inv_mem).toSubalgebra ↔ x✝ ∈ S
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : FunLike F G G'<VAR>inst✝ : MonoidHomClass F G G'<VAR>f : F<VAR>g₁ g₂ g₃ g : G<GOAL>⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁
<VAR>R : Type u_1<VAR>inst✝³ : AddGroup R<VAR>inst✝² : Fintype R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>ψ : AddChar R R'<VAR>hψ : ψ ≠ 1<GOAL>∑ a : R, ψ a = 0
<VAR>R : Type u_1<VAR>inst✝³ : AddGroup R<VAR>inst✝² : Fintype R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>ψ : AddChar R R'<VAR>hψ : ψ ≠ 1<VAR>b : R<VAR>hb : ψ b ≠ 1<GOAL>∑ a : R, ψ a = 0
<VAR>R : Type u_1<VAR>inst✝³ : AddGroup R<VAR>inst✝² : Fintype R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>ψ : AddChar R R'<VAR>hψ : ψ ≠ 1<VAR>b : R<VAR>hb : ψ b ≠ 1<VAR>h₁ : ∑ a : R, ψ (b + a) = ∑ a : R, ψ a<GOAL>∑ a : R, ψ a = 0
<VAR>R : Type u_1<VAR>inst✝³ : AddGroup R<VAR>inst✝² : Fintype R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>ψ : AddChar R R'<VAR>hψ : ψ ≠ 1<VAR>b : R<VAR>hb : ψ b ≠ 1<VAR>h₁ : ∑ x : R, ψ b * ψ x = ∑ a : R, ψ a<GOAL>∑ a : R, ψ a = 0
<VAR>R : Type u_1<VAR>inst✝³ : AddGroup R<VAR>inst✝² : Fintype R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>ψ : AddChar R R'<VAR>hψ : ψ ≠ 1<VAR>b : R<VAR>hb : ψ b ≠ 1<VAR>h₁ : ∑ x : R, ψ b * ψ x = ∑ a : R, ψ a<VAR>h₂ : ∑ a : R, ψ a = Finset.univ.sum ⇑ψ<GOAL>∑ a : R, ψ a = 0
<VAR>R : Type u_1<VAR>inst✝³ : AddGroup R<VAR>inst✝² : Fintype R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>ψ : AddChar R R'<VAR>hψ : ψ ≠ 1<VAR>b : R<VAR>hb : ψ b ≠ 1<VAR>h₁ : ψ b * Finset.univ.sum ⇑ψ = Finset.univ.sum ⇑ψ<VAR>h₂ : ∑ a : R, ψ a = Finset.univ.sum ⇑ψ<GOAL>∑ a : R, ψ a = 0
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Set X<VAR>hs : IsOpen s<VAR>hse : s ⊆ e.source<GOAL>IsOpen (↑e '' s)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Set X<VAR>hs : IsOpen s<VAR>hse : s ⊆ e.source<GOAL>IsOpen (e.target ∩ ↑e.symm ⁻¹' s)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>s : Finset α<VAR>n : ℤ<VAR>f : α → ℤ<GOAL>(Multiset.map (fun x => x % n) (Multiset.map (fun i => f i) s.val)).sum % n = (∑ i ∈ s, f i % n) % n
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>s : Finset α<VAR>n : ℤ<VAR>f : α → ℤ<GOAL>(Multiset.map ((fun x => x % n) ∘ fun i => f i) s.val).sum % n = (Multiset.map (fun i => f i % n) s.val).sum % n
<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>x : Dual R M'<GOAL>x ∈ ker f.dualMap ↔ x ∈ (range (Dual.eval R M' ∘ₗ f)).dualCoannihilator
<VAR>d : ℤ<VAR>x : ℤ√d<GOAL>↑(star x).norm = ↑x.norm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : Zero M<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α →₀ M<GOAL>filter p 0 = 0
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>inst✝⁵ : HasPullback f₁ f₂<VAR>inst✝⁴ : HasPullback f₃ f₄<VAR>inst✝³ : HasPullback (sorryAx (?m.158489 ⟶ X₂) true ≫ f₃) f₄<VAR>inst✝² : HasPullback f₁ (sorryAx (?m.163940 ⟶ X₂) true ≫ f₂)<VAR>inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)<GOAL>(pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄ = pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>inst✝⁵ : HasPullback f₁ f₂<VAR>inst✝⁴ : HasPullback f₃ f₄<VAR>inst✝³ : HasPullback (sorryAx (?m.158489 ⟶ X₂) true ≫ f₃) f₄<VAR>inst✝² : HasPullback f₁ (sorryAx (?m.163940 ⟶ X₂) true ≫ f₂)<VAR>inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)<GOAL>(pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄ = pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂) (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯ ≫ pullback.snd f₃ f₄
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>inst✝⁵ : HasPullback f₁ f₂<VAR>inst✝⁴ : HasPullback f₃ f₄<VAR>inst✝³ : HasPullback (sorryAx (?m.158489 ⟶ X₂) true ≫ f₃) f₄<VAR>inst✝² : HasPullback f₁ (sorryAx (?m.163940 ⟶ X₂) true ≫ f₂)<VAR>inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)<GOAL>pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂) (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯ ≫ pullback.snd f₃ f₄ = pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄
<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 z : M<VAR>f g : M → E'<VAR>f' g' : TangentSpace I z →L[𝕜] E'<VAR>hf : HasMFDerivAt I 𝓘(𝕜, E') (-f) z (-f')<GOAL>HasMFDerivAt I 𝓘(𝕜, E') f z f'
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<GOAL>LinearMap.range (mapBaseChange R A B) = LinearMap.ker (map R A B B)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<GOAL>LinearMap.range (mapBaseChange R A B) ≤ LinearMap.ker (map R A B B)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<GOAL>LinearMap.ker (map R A B B) ≤ LinearMap.range (mapBaseChange R A B)
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>hs : x ∈ (chartAt H c).source<VAR>hd : dist (↑(extChartAt I c) x) (↑(extChartAt I c) c) < f.rIn<GOAL>↑f =ᶠ[𝓝 x] 1
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>hs : x ∈ (chartAt H c).source<VAR>hd : dist (↑(extChartAt I c) x) (↑(extChartAt I c) c) < f.rIn<GOAL>∀ a ∈ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rIn, ↑f a = 1 a
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>hs : x ∈ (chartAt H c).source<VAR>hd : dist (↑(extChartAt I c) x) (↑(extChartAt I c) c) < f.rIn<VAR>z : M<VAR>hzs : z ∈ (chartAt H c).source<VAR>hzd : z ∈ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rIn<GOAL>↑f z = 1 z
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>hf : HasDerivAtFilter f f' x L<VAR>hg : HasDerivAtFilter g g' x L<GOAL>HasDerivAtFilter (fun y => f y + g y) (f' + g') x L
<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✝¹⁸ : SeminormedRing 𝕜<VAR>inst✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>C : ℝ≥0<VAR>x : E<GOAL>(s.sup (C • p)) x = (C • s.sup p) 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✝¹⁸ : SeminormedRing 𝕜<VAR>inst✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>C : ℝ≥0<VAR>x : E<GOAL>↑(s.sup fun i => ⟨((C • p) i) x, ⋯⟩) = C • ↑(s.sup fun i => ⟨(p i) 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✝¹⁸ : SeminormedRing 𝕜<VAR>inst✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>C : ℝ≥0<VAR>x : E<GOAL>C • ↑(s.sup fun i => ⟨(p i) x, ⋯⟩) = ↑(s.sup fun i => ⟨((C • p) i) x, ⋯⟩)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>x : M<VAR>y : M₂<GOAL>(x, y) ∈ map (inl R M M₂) p ↔ (x, y) ∈ p.prod ⊥
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDedekindDomain R<VAR>inst✝⁴ : Module.Free ℤ R<VAR>inst✝³ : Module.Finite ℤ R<VAR>K : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>I₀ : Ideal R<GOAL>absNorm ↑I₀ = ↑(Ideal.absNorm I₀)
<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₃ X₄ : GradedObject I C<VAR>inst✝³ : X₃.HasTensor X₄<VAR>inst✝² : X₂.HasTensor (tensorObj X₃ X₄)<VAR>inst✝¹ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))<VAR>j : I<VAR>A : C<VAR>f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A<VAR>inst✝ : X₂.HasGoodTensorTensor₂₃ X₃ X₄<VAR>H : X₁.HasTensor₄ObjExt X₂ X₃ X₄<VAR>h : ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j), ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g<GOAL>f = g
<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₃ X₄ : GradedObject I C<VAR>inst✝³ : X₃.HasTensor X₄<VAR>inst✝² : X₂.HasTensor (tensorObj X₃ X₄)<VAR>inst✝¹ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))<VAR>j : I<VAR>A : C<VAR>f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A<VAR>inst✝ : X₂.HasGoodTensorTensor₂₃ X₃ X₄<VAR>H : X₁.HasTensor₄ObjExt X₂ X₃ X₄<VAR>h : ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j), ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g<GOAL>∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂ j hi ≫ f = ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂ j hi ≫ g
<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₃ X₄ : GradedObject I C<VAR>inst✝³ : X₃.HasTensor X₄<VAR>inst✝² : X₂.HasTensor (tensorObj X₃ X₄)<VAR>inst✝¹ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))<VAR>j : I<VAR>A : C<VAR>f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A<VAR>inst✝ : X₂.HasGoodTensorTensor₂₃ X₃ X₄<VAR>H : X₁.HasTensor₄ObjExt X₂ X₃ X₄<VAR>h : ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j), ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g<VAR>i₁ i₂₃₄ : I<VAR>h' : i₁ + i₂₃₄ = j<GOAL>ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ f = ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ g
<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₃ X₄ : GradedObject I C<VAR>inst✝³ : X₃.HasTensor X₄<VAR>inst✝² : X₂.HasTensor (tensorObj X₃ X₄)<VAR>inst✝¹ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))<VAR>j : I<VAR>A : C<VAR>f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A<VAR>inst✝ : X₂.HasGoodTensorTensor₂₃ X₃ X₄<VAR>H : X₁.HasTensor₄ObjExt X₂ X₃ X₄<VAR>h : ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j), ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g<VAR>i₁ i₂₃₄ : I<VAR>h' : i₁ + i₂₃₄ = j<GOAL>∀ (i₁_1 i₂ i₃ : I) (h : i₁_1 + i₂ + i₃ = i₂₃₄), X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₁_1 i₂ i₃ i₂₃₄ h ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ f = X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₁_1 i₂ i₃ i₂₃₄ h ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ g
<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₃ X₄ : GradedObject I C<VAR>inst✝³ : X₃.HasTensor X₄<VAR>inst✝² : X₂.HasTensor (tensorObj X₃ X₄)<VAR>inst✝¹ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))<VAR>j : I<VAR>A : C<VAR>f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A<VAR>inst✝ : X₂.HasGoodTensorTensor₂₃ X₃ X₄<VAR>H : X₁.HasTensor₄ObjExt X₂ X₃ X₄<VAR>h : ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j), ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g<VAR>i₁ i₂₃₄ : I<VAR>h' : i₁ + i₂₃₄ = j<VAR>i₂ i₃ i₄ : I<VAR>h'' : i₂ + i₃ + i₄ = i₂₃₄<GOAL>X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ h'' ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ f = X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ h'' ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ g
<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₃ X₄ : GradedObject I C<VAR>inst✝³ : X₃.HasTensor X₄<VAR>inst✝² : X₂.HasTensor (tensorObj X₃ X₄)<VAR>inst✝¹ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))<VAR>j : I<VAR>A : C<VAR>f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A<VAR>inst✝ : X₂.HasGoodTensorTensor₂₃ X₃ X₄<VAR>H : X₁.HasTensor₄ObjExt X₂ X₃ X₄<VAR>h : ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j), ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g<VAR>i₁ i₂₃₄ : I<VAR>h' : i₁ + i₂₃₄ = j<VAR>i₂ i₃ i₄ : I<VAR>h'' : i₂ + i₃ + i₄ = i₂₃₄<VAR>hj : i₁ + i₂ + i₃ + i₄ = j<GOAL>X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ h'' ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ f = X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ h'' ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>w : ι → ℝ≥0<GOAL>∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>w δ' : ι → ℝ≥0<VAR>Hpos : ∀ (i : ι), 0 < δ' i<VAR>Hsum : ∑' (i : ι), ↑(δ' i) < ε<GOAL>∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>w δ' : ι → ℝ≥0<VAR>Hpos : ∀ (i : ι), 0 < δ' i<VAR>Hsum : ∑' (i : ι), ↑(δ' i) < ε<VAR>this : ∀ (i : ι), 0 < max 1 (w i)<GOAL>∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>w δ' : ι → ℝ≥0<VAR>Hpos : ∀ (i : ι), 0 < δ' i<VAR>Hsum : ∑' (i : ι), ↑(δ' i) < ε<VAR>this : ∀ (i : ι), 0 < max 1 (w i)<GOAL>∑' (i : ι), (fun i => ↑(w i)) i * ↑((fun i => δ' i / max 1 (w i)) i) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>w δ' : ι → ℝ≥0<VAR>Hpos : ∀ (i : ι), 0 < δ' i<VAR>Hsum : ∑' (i : ι), ↑(δ' i) < ε<VAR>this : ∀ (i : ι), 0 < max 1 (w i)<VAR>i : ι<GOAL>(fun i => ↑(w i)) i * ↑((fun i => δ' i / max 1 (w i)) i) ≤ ↑(δ' i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>w δ' : ι → ℝ≥0<VAR>Hpos : ∀ (i : ι), 0 < δ' i<VAR>Hsum : ∑' (i : ι), ↑(δ' i) < ε<VAR>this : ∀ (i : ι), 0 < max 1 (w i)<VAR>i : ι<GOAL>(fun i => ↑(w i)) i * (↑(δ' i) / ↑(max 1 (w i))) ≤ ↑(δ' i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>w δ' : ι → ℝ≥0<VAR>Hpos : ∀ (i : ι), 0 < δ' i<VAR>Hsum : ∑' (i : ι), ↑(δ' i) < ε<VAR>this : ∀ (i : ι), 0 < max 1 (w i)<VAR>i : ι<GOAL>(fun i => ↑(w i)) i ≤ ↑(max 1 (w i))
<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>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(lpMeasSubgroup F m p μ)<GOAL>↑↑↑(lpTrimToLpMeasSubgroup F p μ hm (lpMeasSubgroupToLpTrim F p μ hm f)) =ᶠ[ae μ] ↑↑↑f
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>(e.restr s).toPartialEquiv = e.restr s