ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Module R V<VAR>inst✝² : Module A V<VAR>inst✝¹ : IsScalarTower R A V<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticForm R V<VAR>x : CliffordAlgebra (QuadraticForm.baseChange A Q)<VAR>this : ((AlgHom.op (toBaseChange A Q)).comp reverseOp) x = ((↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp).comp (toBaseChange A Q))) x<GOAL>(toBaseChange A Q) (reverse x) = (TensorProduct.map LinearMap.id reverse) ((toBaseChange A Q) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Module R V<VAR>inst✝² : Module A V<VAR>inst✝¹ : IsScalarTower R A V<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticForm R V<VAR>x : CliffordAlgebra (QuadraticForm.baseChange A Q)<VAR>this : ((AlgHom.op (toBaseChange A Q)).comp reverseOp) x = ((↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp).comp (toBaseChange A Q))) x<GOAL>unop (((↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp).comp (toBaseChange A Q))) x) = (TensorProduct.map LinearMap.id reverse) ((toBaseChange A Q) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Module R V<VAR>inst✝² : Module A V<VAR>inst✝¹ : IsScalarTower R A V<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticForm R V<VAR>x : CliffordAlgebra (QuadraticForm.baseChange A Q)<GOAL>unop (((↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp).comp (toBaseChange A Q))) x) = (TensorProduct.map LinearMap.id reverse) ((toBaseChange A Q) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Module R V<VAR>inst✝² : Module A V<VAR>inst✝¹ : IsScalarTower R A V<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticForm R V<VAR>x : CliffordAlgebra (QuadraticForm.baseChange A Q)<GOAL>(TensorProduct.AlgebraTensorModule.map (↑(opLinearEquiv A).symm ∘ₗ (↑(AlgEquiv.toOpposite A A)).toLinearMap) (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap)) (↑(toBaseChange A Q) x) = (TensorProduct.map LinearMap.id reverse) ((toBaseChange A Q) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Module R V<VAR>inst✝² : Module A V<VAR>inst✝¹ : IsScalarTower R A V<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticForm R V<VAR>x : CliffordAlgebra (QuadraticForm.baseChange A Q)<GOAL>(TensorProduct.AlgebraTensorModule.map (↑(opLinearEquiv A).symm ∘ₗ ↑(opLinearEquiv A)) (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap)) (↑(toBaseChange A Q) x) = (TensorProduct.map LinearMap.id (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap)) ((toBaseChange A Q) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Module R V<VAR>inst✝² : Module A V<VAR>inst✝¹ : IsScalarTower R A V<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticForm R V<VAR>x : CliffordAlgebra (QuadraticForm.baseChange A Q)<GOAL>(TensorProduct.AlgebraTensorModule.map (↑(opLinearEquiv A ≪≫ₗ (opLinearEquiv A).symm)) (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap)) ((toBaseChange A Q) x) = (TensorProduct.map LinearMap.id (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap)) ((toBaseChange A Q) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Module R V<VAR>inst✝² : Module A V<VAR>inst✝¹ : IsScalarTower R A V<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticForm R V<VAR>x : CliffordAlgebra (QuadraticForm.baseChange A Q)<GOAL>(TensorProduct.AlgebraTensorModule.map (↑(LinearEquiv.refl A A)) (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap)) ((toBaseChange A Q) x) = (TensorProduct.map LinearMap.id (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap)) ((toBaseChange A Q) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>x : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>z : ↑(CommRingCat.of (A⁰_ f))<GOAL>z ∈ ((toSpec 𝒜 f) (FromSpec.toFun f_deg hm x)).asIdeal ↔ z ∈ x.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>x : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>HomogeneousLocalization.mk z ∈ ((toSpec 𝒜 f) (FromSpec.toFun f_deg hm x)).asIdeal ↔ HomogeneousLocalization.mk z ∈ x.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>x : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>HomogeneousLocalization.mk z ∈ ((toSpec 𝒜 f) (FromSpec.toFun f_deg hm x)).asIdeal ↔ ↑z.num ∈ FromSpec.carrier f_deg x
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasForget₂ C Ab<VAR>inst✝³ : Preadditive C<VAR>inst✝² : (forget₂ C Ab).Additive<VAR>inst✝¹ : (forget₂ C Ab).PreservesHomology<VAR>inst✝ : HasZeroObject C<VAR>S : ShortComplex C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>Mono f ↔ Function.Injective ((forget C).map f)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasForget₂ C Ab<VAR>inst✝³ : Preadditive C<VAR>inst✝² : (forget₂ C Ab).Additive<VAR>inst✝¹ : (forget₂ C Ab).PreservesHomology<VAR>inst✝ : HasZeroObject C<VAR>S : ShortComplex C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>Mono ⇑((forget₂ C Ab).map f) ↔ Mono ((forget C).map f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s t x : Set α<VAR>f : ι → Filter α<GOAL>x ∈ iSup f ↔ ∀ (i : ι), x ∈ f i
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : CompleteSpace F<VAR>f g : E → F<VAR>s : Set E<VAR>x : E<VAR>hf : AnalyticWithinAt 𝕜 f s x<VAR>hs : f =ᶠ[𝓝[s] x] g<VAR>hx : f x = g x<GOAL>AnalyticWithinAt 𝕜 g s x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : CompleteSpace F<VAR>f g : E → F<VAR>s : Set E<VAR>x : E<VAR>hf : AnalyticWithinAt 𝕜 f s x<VAR>hs : f =ᶠ[𝓝[s] x] g<VAR>hx : f x = g x<VAR>f' : E → F<VAR>fx : f x = f' x<VAR>ef : f =ᶠ[𝓝[s] x] f'<VAR>hf' : AnalyticAt 𝕜 f' x<GOAL>AnalyticWithinAt 𝕜 g s x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : CompleteSpace F<VAR>f g : E → F<VAR>s : Set E<VAR>x : E<VAR>hf : AnalyticWithinAt 𝕜 f s x<VAR>hs : f =ᶠ[𝓝[s] x] g<VAR>hx : f x = g x<VAR>f' : E → F<VAR>fx : f x = f' x<VAR>ef : f =ᶠ[𝓝[s] x] f'<VAR>hf' : AnalyticAt 𝕜 f' x<GOAL>ContinuousWithinAt g s x ∧ ∃ g_1, g =ᶠ[𝓝[s] x] g_1 ∧ AnalyticAt 𝕜 g_1 x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : CompleteSpace F<VAR>f g : E → F<VAR>s : Set E<VAR>x : E<VAR>hf : AnalyticWithinAt 𝕜 f s x<VAR>hs : f =ᶠ[𝓝[s] x] g<VAR>hx : f x = g x<VAR>f' : E → F<VAR>fx : f x = f' x<VAR>ef : f =ᶠ[𝓝[s] x] f'<VAR>hf' : AnalyticAt 𝕜 f' x<VAR>eg : g =ᶠ[𝓝[s] x] f'<GOAL>ContinuousWithinAt g s x ∧ ∃ g_1, g =ᶠ[𝓝[s] x] g_1 ∧ AnalyticAt 𝕜 g_1 x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : CompleteSpace F<VAR>f g : E → F<VAR>s : Set E<VAR>x : E<VAR>hf : AnalyticWithinAt 𝕜 f s x<VAR>hs : f =ᶠ[𝓝[s] x] g<VAR>hx : f x = g x<VAR>f' : E → F<VAR>fx : f x = f' x<VAR>ef : f =ᶠ[𝓝[s] x] f'<VAR>hf' : AnalyticAt 𝕜 f' x<VAR>eg : g =ᶠ[𝓝[s] x] f'<GOAL>ContinuousWithinAt g s x
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : NonAssocRing R<VAR>inst✝ : Nontrivial R<VAR>hR : ringChar R ≠ 2<GOAL>Set.InjOn Int.cast {0, 1, -1}
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : NonAssocRing R<VAR>inst✝ : Nontrivial R<VAR>hR : ringChar R ≠ 2<VAR>h : 1 = -1<GOAL>False
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : NonAssocRing R<VAR>inst✝ : Nontrivial R<VAR>hR : ringChar R ≠ 2<VAR>h : -1 = 1<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s✝ t : Finset α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>Set.InjOn (fun a => insert a s) ↑sᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s✝ t : Finset α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>Set.InjOn (fun a => insert a s) (↑s)ᶜ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : NonAssocSemiring α<VAR>n : α<GOAL>n * 1 + n * 1 = n + n
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>hV : IsHilbertSum 𝕜 G V<VAR>i : ι<VAR>x : G i<GOAL>hV.linearIsometryEquiv.symm (lp.single 2 i x) = (V i) x
<VAR>𝕂 : Type u_1<VAR>𝕂' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝⁶ : Field 𝕂<VAR>inst✝⁵ : Field 𝕂'<VAR>inst✝⁴ : Ring 𝔸<VAR>inst✝³ : Algebra 𝕂 𝔸<VAR>inst✝² : Algebra 𝕂' 𝔸<VAR>inst✝¹ : TopologicalSpace 𝔸<VAR>inst✝ : TopologicalRing 𝔸<VAR>n : ℕ<VAR>x : 𝔸<GOAL>((expSeries 𝕂 𝔸 n) fun x_1 => x) = (expSeries 𝕂' 𝔸 n) fun x_1 => x
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f✝ f g : α → Option α<VAR>a : α<VAR>l : List α<VAR>H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1<GOAL>lookmap f (a :: l) = lookmap g (a :: l)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f✝ f g : α → Option α<VAR>a : α<VAR>l : List α<VAR>H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1<VAR>H₁ : f a = g a<VAR>H₂ : ∀ (x : α), x ∈ l → f x = g x<GOAL>lookmap f (a :: l) = lookmap g (a :: l)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hba : b ∣ a + 1<GOAL>(a + 1) / b = a / b + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Finset α<GOAL>(∏ᶠ (i : α) (_ : i ∈ ↑s ∪ ↑t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ ↑t), f i = (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : Module R M✝<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>T : Type u_5<VAR>inst✝⁵ : AddCommGroup T<VAR>inst✝⁴ : Module (AdicCompletion I R) T<VAR>ι : Type u_6<VAR>inst✝³ : DecidableEq ι<VAR>M : ι → Type u_7<VAR>inst✝² : (i : ι) → AddCommGroup (M i)<VAR>inst✝¹ : (i : ι) → Module R (M i)<VAR>inst✝ : Fintype ι<VAR>x : AdicCompletion I ((j : ι) → M j)<GOAL>(piEquivOfFintype I M) x = (pi I M) x
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x y : M<GOAL>SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x y : M<GOAL>SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpTo n f p<VAR>hmn : m ≤ n<GOAL>HasFTaylorSeriesUpTo m f p
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p univ<VAR>hmn : m ≤ n<GOAL>HasFTaylorSeriesUpToOn m f p univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → ℕ → σ<VAR>g : α → List σ → Option σ<VAR>hg : Computable₂ g<VAR>H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)<VAR>this : Computable₂ fun a n => List.map (f a) (List.range n)<VAR>a : α × ℕ<GOAL>(fun a b => (List.map (f (a, b).1) (List.range (a, b).2.succ)).get? (a, b).2) a.1 a.2 = Option.some (f a.1 a.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → ℕ → σ<VAR>g : α → List σ → Option σ<VAR>hg : Computable₂ g<VAR>H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)<VAR>a : α × ℕ<VAR>n : ℕ<VAR>IH : Nat.rec (Option.some []) (fun y IH => (a, y, IH).2.2.bind fun b => Option.map (fun b_1 => (((a, y, IH), b), b_1).1.2 ++ [(((a, y, IH), b), b_1).2]) (g ((a, y, IH), b).1.1.1 ((a, y, IH), b).2)) n = Option.some ((fun a n => List.map (f a) (List.range n)) a.1 n)<GOAL>Nat.rec (Option.some []) (fun y IH => (a, y, IH).2.2.bind fun b => Option.map (fun b_1 => (((a, y, IH), b), b_1).1.2 ++ [(((a, y, IH), b), b_1).2]) (g ((a, y, IH), b).1.1.1 ((a, y, IH), b).2)) (n + 1) = Option.some ((fun a n => List.map (f a) (List.range n)) a.1 (n + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a✝ b : α<VAR>a : α × α<VAR>h : a ∈ s.offDiag<GOAL>¬(Sym2.mk a).IsDiag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a✝ b : α<VAR>a : α × α<VAR>h : a ∈ s.offDiag<GOAL>¬a.1 = a.2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : NormedSpace ℝ E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f g : G → E<VAR>f' g' : G →L[ℝ] E<VAR>s : Set G<VAR>x : G<VAR>n : ℕ∞<VAR>hf : DifferentiableAt ℝ f x<VAR>hg : DifferentiableAt ℝ g x<VAR>y : G<GOAL>(fderiv ℝ (fun t => ⟪f t, g t⟫_𝕜) x) y = ⟪f x, (fderiv ℝ g x) y⟫_𝕜 + ⟪(fderiv ℝ f x) y, g x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : NormedSpace ℝ E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f g : G → E<VAR>f' g' : G →L[ℝ] E<VAR>s : Set G<VAR>x : G<VAR>n : ℕ∞<VAR>hf : DifferentiableAt ℝ f x<VAR>hg : DifferentiableAt ℝ g x<VAR>y : G<GOAL>((fderivInnerCLM 𝕜 (f x, g x)).comp ((fderiv ℝ f x).prod (fderiv ℝ g x))) y = ⟪f x, (fderiv ℝ g x) y⟫_𝕜 + ⟪(fderiv ℝ f x) y, g x⟫_𝕜
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x y : F (α ::: Cofix F α)<VAR>h : mk x = mk y<GOAL>x = y
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>I : Ideal R<GOAL>∃ Z, (Multiset.map asIdeal Z).prod ≤ I
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>I M : Ideal R<VAR>hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J<GOAL>(fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) M
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>I M : Ideal R<VAR>hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J<VAR>h_prM : ¬M.IsPrime<VAR>htop : ¬M = ⊤<GOAL>(fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) M
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>I M : Ideal R<VAR>hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J<VAR>h_prM : ¬M.IsPrime<VAR>htop : ¬M = ⊤<VAR>lt_add : ∀ z ∉ M, M < M + span R {z}<GOAL>(fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) M
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>I M : Ideal R<VAR>hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J<VAR>h_prM : ¬M.IsPrime<VAR>htop : ¬M = ⊤<VAR>lt_add : ∀ z ∉ M, M < M + span R {z}<VAR>x : R<VAR>hx : x ∉ M<VAR>y : R<VAR>hy : y ∉ M<VAR>hxy : x * y ∈ M<GOAL>(fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) M
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>I M : Ideal R<VAR>hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J<VAR>h_prM : ¬M.IsPrime<VAR>htop : ¬M = ⊤<VAR>lt_add : ∀ z ∉ M, M < M + span R {z}<VAR>x : R<VAR>hx : x ∉ M<VAR>y : R<VAR>hy : y ∉ M<VAR>hxy : x * y ∈ M<VAR>Wx : Multiset (PrimeSpectrum R)<VAR>h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + span R {x}<VAR>Wy : Multiset (PrimeSpectrum R)<VAR>h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}<GOAL>(fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) M
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>I M : Ideal R<VAR>hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J<VAR>h_prM : ¬M.IsPrime<VAR>htop : ¬M = ⊤<VAR>lt_add : ∀ z ∉ M, M < M + span R {z}<VAR>x : R<VAR>hx : x ∉ M<VAR>y : R<VAR>hy : y ∉ M<VAR>hxy : x * y ∈ M<VAR>Wx : Multiset (PrimeSpectrum R)<VAR>h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + span R {x}<VAR>Wy : Multiset (PrimeSpectrum R)<VAR>h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}<GOAL>(Multiset.map asIdeal (Wx + Wy)).prod ≤ M
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>I M : Ideal R<VAR>hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J<VAR>h_prM : ¬M.IsPrime<VAR>htop : ¬M = ⊤<VAR>lt_add : ∀ z ∉ M, M < M + span R {z}<VAR>x : R<VAR>hx : x ∉ M<VAR>y : R<VAR>hy : y ∉ M<VAR>hxy : x * y ∈ M<VAR>Wx : Multiset (PrimeSpectrum R)<VAR>h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + span R {x}<VAR>Wy : Multiset (PrimeSpectrum R)<VAR>h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}<GOAL>(Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≤ M
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>I M : Ideal R<VAR>hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J<VAR>h_prM : ¬M.IsPrime<VAR>htop : ¬M = ⊤<VAR>lt_add : ∀ z ∉ M, M < M + span R {z}<VAR>x : R<VAR>hx : x ∉ M<VAR>y : R<VAR>hy : y ∉ M<VAR>hxy : x * y ∈ M<VAR>Wx : Multiset (PrimeSpectrum R)<VAR>h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + span R {x}<VAR>Wy : Multiset (PrimeSpectrum R)<VAR>h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}<GOAL>(M + span R {x}) * (M + span R {y}) ≤ M
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>I M : Ideal R<VAR>hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J<VAR>h_prM : ¬M.IsPrime<VAR>htop : ¬M = ⊤<VAR>lt_add : ∀ z ∉ M, M < M + span R {z}<VAR>x : R<VAR>hx : x ∉ M<VAR>y : R<VAR>hy : y ∉ M<VAR>hxy : x * y ∈ M<VAR>Wx : Multiset (PrimeSpectrum R)<VAR>h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + span R {x}<VAR>Wy : Multiset (PrimeSpectrum R)<VAR>h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}<GOAL>M * (M + span R {y}) + span R {x} * (M + span R {y}) ≤ M