ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹³ : NormedAddCommGroup D<VAR>inst✝¹² : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup X<VAR>inst✝⁴ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Fintype ι'<VAR>F' : ι → Type u_5<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)<VAR>pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj<GOAL>ContDiffWithinAt 𝕜 n Φ s x ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => Φ x i) s x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹³ : NormedAddCommGroup D<VAR>inst✝¹² : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup X<VAR>inst✝⁴ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Fintype ι'<VAR>F' : ι → Type u_5<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)<VAR>pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj<VAR>h : ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => Φ x i) s x<VAR>m : ℕ<VAR>hm : ↑m ≤ n<GOAL>∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) Φ p u
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹³ : NormedAddCommGroup D<VAR>inst✝¹² : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup X<VAR>inst✝⁴ : NormedSpace 𝕜 X<VAR>s s₁ t u✝ : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m✝ n : ℕ∞<VAR>p✝ : E → FormalMultilinearSeries 𝕜 E F<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Fintype ι'<VAR>F' : ι → Type u_5<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)<VAR>pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj<VAR>h : ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => Φ x i) s x<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>u : ι → Set E<VAR>hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x<VAR>p : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)<VAR>hp : ∀ (i : ι), HasFTaylorSeriesUpToOn (↑m) (fun x => Φ x i) (p i) (u i)<GOAL>∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) Φ p u
<VAR>α β : Type u<VAR>n : ℕ<VAR>a : Cardinal.{u}<GOAL>↑n < lift.{v, u} a ↔ ↑n < a
<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>l m r : List Char<VAR>h : ValidFor l m r x✝<GOAL>x✝.next { byteIdx := x✝.bsize } = { byteIdx := x✝.bsize }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : BorelSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : BorelSpace β<VAR>inst✝ : μ.Regular<VAR>f : α ≃ₜ β<GOAL>(map (⇑f) μ).Regular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : BorelSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : BorelSpace β<VAR>inst✝ : μ.Regular<VAR>f : α ≃ₜ β<VAR>this : (map (⇑f) μ).OuterRegular<GOAL>(map (⇑f) μ).Regular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : BorelSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : BorelSpace β<VAR>inst✝ : μ.Regular<VAR>f : α ≃ₜ β<VAR>this✝ : (map (⇑f) μ).OuterRegular<VAR>this : IsFiniteMeasureOnCompacts (map (⇑f) μ)<GOAL>(map (⇑f) μ).Regular
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>R.one ▷ X P Q ≫ actLeft P Q = (λ_ (X P Q)).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>(tensorLeft (𝟙_ C)).map (coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫ R.one ▷ X P Q ≫ actLeft P Q = (tensorLeft (𝟙_ C)).map (coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫ (λ_ (X P Q)).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>𝟙_ C ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ R.one ▷ coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ actLeft P Q = 𝟙_ C ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ (λ_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>(R.one ▷ (P.X ⊗ Q.X) ≫ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫ actLeft P Q = 𝟙_ C ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ (λ_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>R.one ▷ (P.X ⊗ Q.X) ≫ (α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = 𝟙_ C ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ (λ_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>(((α_ (𝟙_ C) P.X Q.X).inv ≫ R.one ▷ P.X ▷ Q.X) ≫ P.actLeft ▷ Q.X) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = 𝟙_ C ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ (λ_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>(α_ (𝟙_ C) P.X Q.X).inv ≫ (λ_ P.X).hom ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = 𝟙_ C ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ (λ_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<GOAL>(α_ (𝟙_ C) P.X Q.X).inv ≫ (λ_ P.X).hom ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = (λ_ (P.X ⊗ Q.X)).hom ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 1)<VAR>H : i ≤ j.castSucc<GOAL>X.map (SimplexCategory.σ j.succ).op ≫ X.map (SimplexCategory.δ i.castSucc).op = X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝² : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : DecidableEq α<VAR>d : α → Matrix m m R<VAR>i : m<VAR>i' : α<VAR>j : m<VAR>j' : α<VAR>h : (j, j').2 < (i, i').2<GOAL>blockDiagonal d (i, i') (j, j') = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝² : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : DecidableEq α<VAR>d : α → Matrix m m R<VAR>i : m<VAR>i' : α<VAR>j : m<VAR>j' : α<VAR>h : (j, j').2 < (i, i').2<GOAL>⟨j', j⟩.fst < ⟨i', i⟩.fst
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝³ : Monoid M<VAR>inst✝² : AddMonoid N<VAR>M' : Type u_3<VAR>inst✝¹ : Monoid M'<VAR>inst✝ : FG M<VAR>f : M →* M'<VAR>hf : Function.Surjective ⇑f<GOAL>FG M'
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CommMonoid M<VAR>f : α → M<VAR>a✝ b : α<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>a : α<GOAL>f a * ∏ x ∈ Iio a, f x = ∏ x ∈ Iic a, f x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<VAR>h : Codisjoint a b<GOAL>b ⇨ a ⊓ b = a
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>Integrable (fun x => cexp (-b * (↑x + ↑c * I) ^ 2)) volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>HasFiniteIntegral (fun x => cexp (-b * (↑x + ↑c * I) ^ 2)) volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>HasFiniteIntegral (fun a => ‖cexp (-b * (↑a + ↑c * I) ^ 2)‖) volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>HasFiniteIntegral (fun a => rexp (c ^ 2 * (b.im ^ 2 / b.re + b.re)) * rexp (-(b.re * (a - b.im * c / b.re) ^ 2))) volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>Integrable (fun x => rexp (-(b.re * x ^ 2))) volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>Integrable (fun x => rexp (-b.re * x ^ 2)) volume
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>s : Set α<GOAL>(frontier s).Nonempty ↔ s.Nonempty ∧ s ≠ univ
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X : Center C<GOAL>(ρ_ X).inv.f = (ρ_ X.fst).inv
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X : Center C<GOAL>(ρ_ X.fst).hom ≫ (ρ_ X).inv.f = 𝟙 (X ⊗ 𝟙_ (Center C)).fst
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X : Center C<GOAL>(𝟙 (X ⊗ 𝟙_ (Center C))).f = 𝟙 (X ⊗ 𝟙_ (Center C)).fst
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹³ : Ring k<VAR>inst✝¹² : AddCommGroup V1<VAR>inst✝¹¹ : Module k V1<VAR>inst✝¹⁰ : AffineSpace V1 P1<VAR>inst✝⁹ : AddCommGroup V2<VAR>inst✝⁸ : Module k V2<VAR>inst✝⁷ : AffineSpace V2 P2<VAR>inst✝⁶ : AddCommGroup V3<VAR>inst✝⁵ : Module k V3<VAR>inst✝⁴ : AffineSpace V3 P3<VAR>inst✝³ : AddCommGroup V4<VAR>inst✝² : Module k V4<VAR>inst✝¹ : AffineSpace V4 P4<VAR>inst✝ : NoZeroSMulDivisors k V1<VAR>p₀ p₁ : P1<VAR>c₁ c₂ : k<GOAL>(lineMap p₀ p₁) c₁ = (lineMap p₀ p₁) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>g : ContinuousMultilinearMap 𝕜 E₁ G<VAR>f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i<GOAL>‖g.compContinuousLinearMap fun i => ↑{ toLinearEquiv := (f i).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }‖ = ‖g‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>g : ContinuousMultilinearMap 𝕜 E₁ G<VAR>f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i<GOAL>‖g‖ ≤ ‖g.compContinuousLinearMap fun i => (f i).toLinearIsometry.toContinuousLinearMap‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>g : ContinuousMultilinearMap 𝕜 E₁ G<VAR>f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i<VAR>this : g = (g.compContinuousLinearMap fun i => ↑{ toLinearEquiv := (f i).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).compContinuousLinearMap fun i => ↑{ toLinearEquiv := (f i).symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }<GOAL>‖g‖ ≤ ‖g.compContinuousLinearMap fun i => (f i).toLinearIsometry.toContinuousLinearMap‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>g : ContinuousMultilinearMap 𝕜 E₁ G<VAR>f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i<VAR>this : g = (g.compContinuousLinearMap fun i => ↑{ toLinearEquiv := (f i).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).compContinuousLinearMap fun i => ↑{ toLinearEquiv := (f i).symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }<GOAL>‖(g.compContinuousLinearMap fun i => ↑{ toLinearEquiv := (f i).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).compContinuousLinearMap fun i => ↑{ toLinearEquiv := (f i).symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }‖ ≤ ‖g.compContinuousLinearMap fun i => (f i).toLinearIsometry.toContinuousLinearMap‖
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ : Measure β<VAR>s : Set β<GOAL>(Measure.comap f μ) (f ⁻¹' s) = μ (s ∩ range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i✝ j✝ : Set α<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : MeasurableSet i<VAR>hj : MeasurableSet j<VAR>hi' : restrict 0 i ≤ restrict s i ∧ restrict s iᶜ ≤ restrict 0 iᶜ<VAR>hj' : restrict 0 j ≤ restrict s j ∧ restrict s jᶜ ≤ restrict 0 jᶜ<GOAL>↑s (i ∆ j) = 0 ∧ ↑s (iᶜ ∆ jᶜ) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i✝ j✝ : Set α<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : MeasurableSet i<VAR>hj : MeasurableSet j<VAR>hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → ↑0 j ≤ ↑s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → ↑s j ≤ ↑0 j<VAR>hj' : (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → ↑0 j_1 ≤ ↑s j_1) ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → ↑s j_1 ≤ ↑0 j_1<GOAL>↑s (i ∆ j) = 0 ∧ ↑s (iᶜ ∆ jᶜ) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i✝ j✝ : Set α<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : MeasurableSet i<VAR>hj : MeasurableSet j<VAR>hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → ↑0 j ≤ ↑s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → ↑s j ≤ ↑0 j<VAR>hj' : restrict 0 j ≤ restrict s j ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → ↑s j_1 ≤ ↑0 j_1<GOAL>MeasurableSet j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i✝ j✝ : Set α<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : MeasurableSet i<VAR>hj : MeasurableSet j<VAR>hi' : restrict 0 i ≤ restrict s i ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → ↑s j ≤ ↑0 j<VAR>hj' : restrict 0 j ≤ restrict s j ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → ↑s j_1 ≤ ↑0 j_1<GOAL>MeasurableSet i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i✝ j✝ : Set α<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : MeasurableSet i<VAR>hj : MeasurableSet j<VAR>hi' : restrict 0 i ≤ restrict s i ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → ↑s j ≤ ↑0 j<VAR>hj' : restrict 0 j ≤ restrict s j ∧ restrict s jᶜ ≤ restrict 0 jᶜ<GOAL>MeasurableSet jᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i✝ j✝ : Set α<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : MeasurableSet i<VAR>hj : MeasurableSet j<VAR>hi' : restrict 0 i ≤ restrict s i ∧ restrict s iᶜ ≤ restrict 0 iᶜ<VAR>hj' : restrict 0 j ≤ restrict s j ∧ restrict s jᶜ ≤ restrict 0 jᶜ<GOAL>MeasurableSet iᶜ
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>J : I → Prop<VAR>h : ∀ a ∈ ↑l, J a<VAR>inst✝ : (j : I) → Decidable (J j)<VAR>x : ↑C<GOAL>(eval (π C J) l) (Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) = (eval C l) x
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>J : I → Prop<VAR>h : ∀ a ∈ ↑l, J a<VAR>inst✝ : (j : I) → Decidable (J j)<VAR>x : ↑C<GOAL>(if ∀ i ∈ ↑l, ↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) i = true then 1 else 0) = if ∀ i ∈ ↑l, ↑x i = true then 1 else 0
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>J : I → Prop<VAR>h : ∀ a ∈ ↑l, J a<VAR>inst✝ : (j : I) → Decidable (J j)<VAR>x : ↑C<GOAL>(∀ i ∈ ↑l, ↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) i = true) = ∀ i ∈ ↑l, ↑x i = true
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>J : I → Prop<VAR>h : ∀ a ∈ ↑l, J a<VAR>inst✝ : (j : I) → Decidable (J j)<VAR>x : ↑C<GOAL>∀ (a : I), (a ∈ ↑l → ↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) a = true) = (a ∈ ↑l → ↑x a = true)
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>J : I → Prop<VAR>h : ∀ a ∈ ↑l, J a<VAR>inst✝ : (j : I) → Decidable (J j)<VAR>x : ↑C<VAR>i : I<GOAL>(i ∈ ↑l → ↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) i = true) = (i ∈ ↑l → ↑x i = true)
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>J : I → Prop<VAR>h : ∀ a ∈ ↑l, J a<VAR>inst✝ : (j : I) → Decidable (J j)<VAR>x : ↑C<VAR>i : I<GOAL>i ∈ ↑l → (↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) i = true) = (↑x i = true)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K K₁ K₂ : Submodule 𝕜 E<VAR>h : K₁ ≤ K₂<VAR>inst✝ : HasOrthogonalProjection K₁<VAR>x : E<GOAL>x ∈ K₁ ⊔ K₁ᗮ ⊓ K₂ ↔ x ∈ K₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K K₁ K₂ : Submodule 𝕜 E<VAR>h : K₁ ≤ K₂<VAR>inst✝ : HasOrthogonalProjection K₁<VAR>x : E<GOAL>(∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K K₁ K₂ : Submodule 𝕜 E<VAR>h : K₁ ≤ K₂<VAR>inst✝ : HasOrthogonalProjection K₁<VAR>x : E<VAR>v : ↥K₁ := (orthogonalProjection K₁) x<GOAL>(∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K K₁ K₂ : Submodule 𝕜 E<VAR>h : K₁ ≤ K₂<VAR>inst✝ : HasOrthogonalProjection K₁<VAR>x : E<VAR>v : ↥K₁ := (orthogonalProjection K₁) x<VAR>hvm : x - ↑v ∈ K₁ᗮ<GOAL>(∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>h : b ≤ a<GOAL>b + (a - b) ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>h : b ≤ a<VAR>e : a - b = 0<GOAL>b + (a - b) ≤ a