ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : MulAction A M<VAR>inst✝¹ : SMul R M<VAR>inst✝ : IsScalarTower R A M<VAR>r : R<VAR>x : M<GOAL>(algebraMap R A) r • x = r • x
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g✝ : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i✝ : ι<VAR>f g : D ⟶ E<VAR>h : Homotopy f g<VAR>e : C ⟶ D<VAR>i j : ι<VAR>w : ¬c.Rel j i<GOAL>e.f i ≫ h.hom i j = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g✝ : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i✝ : ι<VAR>f g : D ⟶ E<VAR>h : Homotopy f g<VAR>e : C ⟶ D<VAR>i : ι<GOAL>(e ≫ f).f i = (((dNext i) fun i j => e.f i ≫ h.hom i j) + (prevD i) fun i j => e.f i ≫ h.hom i j) + (e ≫ g).f i
<VAR>α : Type u_1<VAR>b : Bool<VAR>n : ℕ<VAR>IH : Nat.binaryRec 0 (fun b x => bif b then Num.bit1 else Num.bit0) n = ↑n<GOAL>Nat.binaryRec 0 (fun b x => bif b then Num.bit1 else Num.bit0) (Nat.bit b n) = ↑(Nat.bit b n)
<VAR>α : Type u_1<VAR>b : Bool<VAR>n : ℕ<VAR>IH : Nat.binaryRec 0 (fun b x => bif b then Num.bit1 else Num.bit0) n = ↑n<GOAL>(bif b then Num.bit1 else Num.bit0) ↑n = ↑(Nat.bit b n)
<VAR>α : Type u_1<VAR>b : Bool<VAR>n : ℕ<VAR>IH : Nat.binaryRec 0 (fun b x => bif b then Num.bit1 else Num.bit0) n = ↑n<GOAL>(bif false then Num.bit1 else Num.bit0) 0 = 0
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ s' s : Cycle α<VAR>h : s.Nodup<VAR>x : α<VAR>hx : x ∈ s<GOAL>(s.formPerm h) x = s.next h x hx
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s s' : Cycle α<VAR>x : α<VAR>a✝ : List α<VAR>h : Nodup (Quot.mk Setoid.r a✝)<VAR>hx : x ∈ Quot.mk Setoid.r a✝<GOAL>(formPerm (Quot.mk Setoid.r a✝) h) x = next (Quot.mk Setoid.r a✝) h x hx
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R✝<VAR>m n : ℕ<VAR>inst✝² : CommSemiring R✝<VAR>p✝ q✝ : R✝[X]<VAR>x : R✝<VAR>inst✝¹ : CommSemiring S<VAR>f : R✝ →+* S<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>p q : R[X]<VAR>r : R<GOAL>(p.comp q).IsRoot r ↔ p.IsRoot (eval r q)
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x y : α<VAR>hy : IsFixedPt f y<GOAL>dist x y ≤ dist x (f x) / (1 - ↑K)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<GOAL>mgf (-X) μ t = mgf X μ (-t)
<VAR>κ : Type uκ<VAR>R : Type uR<VAR>M : Type uM<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Free R M<GOAL>Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (sum fun n => Module.rank R M ^ n)
<VAR>κ✝ : Type uκ<VAR>R : Type uR<VAR>M : Type uM<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Module.Free R M<VAR>κ : Type uM<VAR>b : Basis κ R M<GOAL>Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (sum fun n => Module.rank R M ^ n)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>b : BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>IsPushout 0 0 b.inl b.inr
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s✝ : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>g : γ → α<VAR>s : Finset γ<VAR>hi : Std.IdempotentOp op<GOAL>fold op b f (image g s) = fold op b (f ∘ g) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>g : γ → α<VAR>hi : Std.IdempotentOp op<GOAL>fold op b f (image g ∅) = fold op b (f ∘ g) ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>g : γ → α<VAR>hi : Std.IdempotentOp op<VAR>x : γ<VAR>xs : Finset γ<VAR>hx : x ∉ xs<VAR>ih : fold op b f (image g xs) = fold op b (f ∘ g) xs<GOAL>fold op b f (image g (cons x xs hx)) = fold op b (f ∘ g) (cons x xs hx)
<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<VAR>H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G<VAR>K₁ K₂ : Subgroup G'<GOAL>⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
<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<VAR>H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G<VAR>K₁ K₂ : Subgroup G'<GOAL>⁅H₁.prod K₁, H₂.prod K₂⁆ ≤ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
<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<VAR>H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G<VAR>K₁ K₂ : Subgroup G'<GOAL>⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>H : Type u_7<VAR>inst✝ : NormedAddCommGroup H<VAR>f : α → H<VAR>p : ℝ≥0∞<VAR>hp1 : p ≠ 0<VAR>hp2 : p ≠ ⊤<VAR>hf : Memℒp f p μ<GOAL>eLpNorm f p μ = ENNReal.ofReal ((∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>H : Type u_7<VAR>inst✝ : NormedAddCommGroup H<VAR>f : α → H<VAR>p : ℝ≥0∞<VAR>hp1 : p ≠ 0<VAR>hp2 : p ≠ ⊤<VAR>hf : Memℒp f p μ<VAR>A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ<GOAL>eLpNorm f p μ = ENNReal.ofReal ((∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>H : Type u_7<VAR>inst✝ : NormedAddCommGroup H<VAR>f : α → H<VAR>p : ℝ≥0∞<VAR>hp1 : p ≠ 0<VAR>hp2 : p ≠ ⊤<VAR>hf : Memℒp f p μ<VAR>A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ<GOAL>(∫⁻ (x : α), ↑‖f x‖₊ ^ p.toReal ∂μ) ^ p.toReal⁻¹ = ENNReal.ofReal ((∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>H : Type u_7<VAR>inst✝ : NormedAddCommGroup H<VAR>f : α → H<VAR>p : ℝ≥0∞<VAR>hp1 : p ≠ 0<VAR>hp2 : p ≠ ⊤<VAR>hf : Memℒp f p μ<VAR>A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ<GOAL>(∫⁻ (x : α), ↑‖f x‖₊ ^ p.toReal ∂μ) ^ p.toReal⁻¹ = ENNReal.ofReal ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ).toReal ^ p.toReal⁻¹)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>H : Type u_7<VAR>inst✝ : NormedAddCommGroup H<VAR>f : α → H<VAR>p : ℝ≥0∞<VAR>hp1 : p ≠ 0<VAR>hp2 : p ≠ ⊤<VAR>hf : Memℒp f p μ<VAR>A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ<GOAL>0 ≤ᶠ[ae μ] fun a => ‖f a‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>H : Type u_7<VAR>inst✝ : NormedAddCommGroup H<VAR>f : α → H<VAR>p : ℝ≥0∞<VAR>hp1 : p ≠ 0<VAR>hp2 : p ≠ ⊤<VAR>hf : Memℒp f p μ<VAR>A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ<GOAL>AEStronglyMeasurable (fun a => ‖f a‖ ^ p.toReal) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>H : Type u_7<VAR>inst✝ : NormedAddCommGroup H<VAR>f : α → H<VAR>p : ℝ≥0∞<VAR>hp1 : p ≠ 0<VAR>hp2 : p ≠ ⊤<VAR>hf : Memℒp f p μ<VAR>A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ ≠ ⊤
<VAR>a b c x : ℕ<GOAL>x ∈ Ico a b.succ ↔ x ∈ Icc a b
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹⁸ : Field F<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : Algebra F K<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹⁵ : Field F<VAR>inst✝¹⁴ : Field K₁<VAR>inst✝¹³ : Field K₂<VAR>inst✝¹² : Field K₃<VAR>inst✝¹¹ : Algebra F K₁<VAR>inst✝¹⁰ : Algebra F K₂<VAR>inst✝⁹ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>E : Type u_6<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra E K₁<VAR>inst✝⁵ : Algebra E K₂<VAR>inst✝⁴ : Algebra E K₃<VAR>inst✝³ : IsScalarTower F E K₁<VAR>inst✝² : IsScalarTower F E K₂<VAR>inst✝¹ : IsScalarTower F E K₃<VAR>inst✝ : Normal F E<VAR>x✝ : E<GOAL>(algebraMap E K₃) (((ψ.restrictNormal E).comp (ϕ.restrictNormal E)) x✝) = (algebraMap E K₃) (((ψ.comp ϕ).restrictNormal E) x✝)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>K : IntermediateField F E<VAR>h : K.toSubalgebra = Algebra.adjoin F S<GOAL>K = adjoin F S
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>K : IntermediateField F E<VAR>h : K.toSubalgebra = Algebra.adjoin F S<GOAL>K.toSubalgebra = (adjoin F S).toSubalgebra
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>K : IntermediateField F E<VAR>h : K.toSubalgebra = Algebra.adjoin F S<GOAL>Algebra.adjoin F S = (adjoin F S).toSubalgebra
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>K : IntermediateField F E<VAR>h : K.toSubalgebra = Algebra.adjoin F S<GOAL>∀ x ∈ Algebra.adjoin F S, x⁻¹ ∈ Algebra.adjoin F S
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>K : IntermediateField F E<VAR>h : K.toSubalgebra = Algebra.adjoin F S<VAR>x : E<GOAL>x ∈ Algebra.adjoin F S → x⁻¹ ∈ Algebra.adjoin F S
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a c : α<VAR>h : c < 0<GOAL>(fun x => c * x) ⁻¹' Iic a = Ici (a / c)
<VAR>n m : ℕ<VAR>h : n ≤ m<GOAL>Ico n (m + 1) = Ico n m ++ [m]
<VAR>n m : ℕ<VAR>h : n ≤ m<GOAL>m ≤ m + 1
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>U : Opens ↑↑(D.V (i, j))<GOAL>op (⋯.functor.obj (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).toPrefunctor.1 (unop (op U)))))) = (Opens.map (D.f i k).base).op.obj (op (⋯.functor.obj U))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>U : Opens ↑↑(D.V (i, j))<GOAL>op { carrier := ⇑(pullback.snd (D.f i j) (D.f i k)).base '' ↑{ carrier := ⇑(pullback.fst (D.f i j) (D.f i k)).base ⁻¹' ↑U, is_open' := ⋯ }, is_open' := ⋯ } = op { carrier := ⇑(D.f i k).base ⁻¹' ↑{ carrier := ⇑(D.f i j).base '' ↑U, is_open' := ⋯ }, is_open' := ⋯ }
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>U : Opens ↑↑(D.V (i, j))<GOAL>⇑(pullback.snd (D.f i j) (D.f i k)).base '' ↑{ carrier := ⇑(pullback.fst (D.f i j) (D.f i k)).base ⁻¹' ↑U, is_open' := ⋯ } = ⇑(D.f i k).base ⁻¹' ↑{ carrier := ⇑(D.f i j).base '' ↑U, is_open' := ⋯ }
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>U : Opens ↑↑(D.V (i, j))<GOAL>invApp (D.f i j) U ≫ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) = (pullback.fst (D.f i j) (D.f i k)).c.app (op U) ≫ invApp (pullback.snd (D.f i j) (D.f i k)) (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).toPrefunctor.1 (unop (op U))))) ≫ (D.V (i, k)).presheaf.map (eqToHom ⋯)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>U : Opens ↑↑(D.V (i, j))<VAR>this : ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ), (pullback.fst (D.f i j) (D.f i k) ≫ D.f i j).c.app U = (pullback.snd (D.f i j) (D.f i k) ≫ D.f i k).c.app U ≫ (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)<GOAL>invApp (D.f i j) U ≫ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) = (pullback.fst (D.f i j) (D.f i k)).c.app (op U) ≫ invApp (pullback.snd (D.f i j) (D.f i k)) (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).toPrefunctor.1 (unop (op U))))) ≫ (D.V (i, k)).presheaf.map (eqToHom ⋯)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>U : Opens ↑↑(D.V (i, j))<VAR>this : ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ), (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) = ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫ (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)<GOAL>invApp (D.f i j) U ≫ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) = (pullback.fst (D.f i j) (D.f i k)).c.app (op U) ≫ invApp (pullback.snd (D.f i j) (D.f i k)) (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).toPrefunctor.1 (unop (op U))))) ≫ (D.V (i, k)).presheaf.map (eqToHom ⋯)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>U : Opens ↑↑(D.V (i, j))<VAR>this : ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ), (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) = ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫ (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)<GOAL>(D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) = ((D.f i j).c.app (op ((opensFunctor (D.f i j)).obj U)) ≫ (D.V (i, j)).presheaf.map (eqToHom ⋯)) ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op U) ≫ invApp (pullback.snd (D.f i j) (D.f i k)) (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).toPrefunctor.1 (unop (op U))))) ≫ (D.V (i, k)).presheaf.map (eqToHom ⋯)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>U : Opens ↑↑(D.V (i, j))<VAR>this : ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ), (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) = ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫ (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)<GOAL>(D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) = (D.f i j).c.app (op ((opensFunctor (D.f i j)).obj U)) ≫ (D.V (i, j)).presheaf.map (eqToHom ⋯) ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op U) ≫ invApp (pullback.snd (D.f i j) (D.f i k)) ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).toPrefunctor.1 U) ≫ (D.V (i, k)).presheaf.map (eqToHom ⋯)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>U : Opens ↑↑(D.V (i, j))<VAR>this : ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ), (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) = ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫ (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)<GOAL>(D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) = (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) ≫ (D.V (i, k)).presheaf.map ((homOfLE ⋯).op ≫ (opensFunctor (pullback.snd (D.f i j) (D.f i k))).op.map (eqToHom ⋯ ≫ (Opens.map (pullback.fst (D.f i j) (D.f i k)).base).op.map (eqToHom ⋯)) ≫ eqToHom ⋯)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>U : Opens ↑↑(D.V (i, j))<VAR>this : ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ), (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) = ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫ (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)<GOAL>(D.V (i, k)).presheaf.map ((homOfLE ⋯).op ≫ (opensFunctor (pullback.snd (D.f i j) (D.f i k))).op.map (eqToHom ⋯ ≫ (Opens.map (pullback.fst (D.f i j) (D.f i k)).base).op.map (eqToHom ⋯)) ≫ eqToHom ⋯) = 𝟙 (((TopCat.Presheaf.pushforward C (D.f i k).base).obj (D.V (i, k)).presheaf).obj (op ((opensFunctor (D.f i j)).obj U)))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>U : Opens ↑↑(D.V (i, j))<VAR>this : ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ), (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) = ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫ (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)<GOAL>𝟙 ((D.V (i, k)).presheaf.obj (op ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))))) = 𝟙 (((TopCat.Presheaf.pushforward C (D.f i k).base).obj (D.V (i, k)).presheaf).obj (op ((opensFunctor (D.f i j)).obj 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>q : E → FormalMultilinearSeries 𝕜 E F<VAR>g : E → F<VAR>hf : HasFTaylorSeriesUpToOn n f p s<VAR>hg : HasFTaylorSeriesUpToOn n g q s<GOAL>HasFTaylorSeriesUpToOn n (f + g) (p + q) s
<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>f✝ : MultilinearMap 𝕜 E G<VAR>k n : ℕ<VAR>f : MultilinearMap 𝕜 (fun x => G) G'<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>z : G<VAR>C : ℝ<VAR>H : ∀ (m : Fin n → G), ‖f m‖ ≤ C * ∏ i : Fin n, ‖m i‖<VAR>v : Fin k → G<GOAL>‖(f.restr s hk z) v‖ ≤ C * ‖z‖ ^ (n - k) * ∏ i : Fin k, ‖v i‖
<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>f✝ : MultilinearMap 𝕜 E G<VAR>k n : ℕ<VAR>f : MultilinearMap 𝕜 (fun x => G) G'<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>z : G<VAR>C : ℝ<VAR>H : ∀ (m : Fin n → G), ‖f m‖ ≤ C * ∏ i : Fin n, ‖m i‖<VAR>v : Fin k → G<GOAL>‖(f.restr s hk z) v‖ ≤ C * ((∏ i : Fin k, ‖v i‖) * ‖z‖ ^ (n - k))
<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>f✝ : MultilinearMap 𝕜 E G<VAR>k n : ℕ<VAR>f : MultilinearMap 𝕜 (fun x => G) G'<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>z : G<VAR>C : ℝ<VAR>H : ∀ (m : Fin n → G), ‖f m‖ ≤ C * ∏ i : Fin n, ‖m i‖<VAR>v : Fin k → G<GOAL>(∏ i : Fin k, ‖v i‖) * ‖z‖ ^ (n - k) = ∏ i : Fin n, ‖if h : i ∈ s then v ((s.orderIsoOfFin hk).symm ⟨i, h⟩) else z‖