ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝ : Submodule 𝕜 E<VAR>K : Submodule ℝ F<VAR>u v : F<VAR>hv : v ∈ K<VAR>h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0<VAR>this : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0<GOAL>Convex ℝ ↑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✝ : Submodule 𝕜 E<VAR>K : Submodule ℝ F<VAR>u v : F<VAR>hv : v ∈ K<VAR>h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0<VAR>this : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0<GOAL>v ∈ ↑K
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c d : ℂ<VAR>this : (-b).re < 0<GOAL>Integrable (fun x => cexp (-b * ↑x ^ 2 + c * ↑x + d)) volume
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : DiscreteTopology X<VAR>hs : IsCompact s<GOAL>s.Finite
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : DiscreteTopology X<VAR>hs : IsCompact s<VAR>this : ∀ (x : X), {x} ∈ 𝓝 x<GOAL>s.Finite
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>inst✝ : DiscreteTopology X<VAR>hs : IsCompact s<VAR>this : ∀ (x : X), {x} ∈ 𝓝 x<VAR>t : Finset X<VAR>left✝ : ∀ x ∈ t, x ∈ s<VAR>hst : s ⊆ ⋃ x ∈ t, {x}<GOAL>s.Finite
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>inst✝ : DiscreteTopology X<VAR>hs : IsCompact s<VAR>this : ∀ (x : X), {x} ∈ 𝓝 x<VAR>t : Finset X<VAR>left✝ : ∀ x ∈ t, x ∈ s<VAR>hst : s ⊆ ↑t<GOAL>s.Finite
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a✝ b c : α<VAR>hn : Even n<VAR>a : α<GOAL>|a| ^ n = a ^ n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a✝ b c : α<VAR>hn : Even n<VAR>a : α<GOAL>0 ≤ a ^ n
<VAR>α : Sort u_2<VAR>β : Sort u_1<VAR>a : α<VAR>C : α → Sort u_1<VAR>x : β<VAR>y : C a<GOAL>HEq x (⋯ ▸ y) ↔ HEq x y
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>p : ⦃i : Fin2 n⦄ → α i → Prop<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>h₀ : x = abs ⟨a, f⟩<VAR>h₁ : ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)<GOAL>LiftP p x
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>p : ⦃i : Fin2 n⦄ → α i → Prop<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>h₀ : x = abs ⟨a, f⟩<VAR>h₁ : ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)<GOAL>(fun i => Subtype.val) <$$> abs ⟨a, fun i j => ⟨f i j, ⋯⟩⟩ = x
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>p : ⦃i : Fin2 n⦄ → α i → Prop<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>h₀ : x = abs ⟨a, f⟩<VAR>h₁ : ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)<GOAL>abs ((fun i => Subtype.val) <$$> ⟨a, fun i j => ⟨f i j, ⋯⟩⟩) = abs ⟨a, f⟩
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : M →* N<VAR>h : ∀ (y : ↥S), IsUnit (f ↑y)<VAR>y : ↥S<VAR>w z : N<GOAL>w * ↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ = z ↔ w = f ↑y * z
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : M →* N<VAR>h : ∀ (y : ↥S), IsUnit (f ↑y)<VAR>y : ↥S<VAR>w z : N<GOAL>↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ * w = z ↔ w = f ↑y * z
<VAR>R : Type u_1<VAR>S✝ : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S✝<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S✝ M<VAR>inst✝¹ : SMul S✝ R<VAR>inst✝ : IsScalarTower S✝ R M<VAR>p q S T : Submodule R M<GOAL>∀ {x : M}, x ∈ S → x ∈ S ⊔ T
<VAR>R : Type u_1<VAR>S✝ : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S✝<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S✝ M<VAR>inst✝¹ : SMul S✝ R<VAR>inst✝ : IsScalarTower S✝ R M<VAR>p q S T : Submodule R M<VAR>this : S ≤ S ⊔ T<GOAL>∀ {x : M}, x ∈ S → x ∈ S ⊔ T
<VAR>I : Type u<VAR>inst✝¹⁰ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝⁹ : Category.{?u.46109, u_1} C<VAR>inst✝⁸ : MonoidalCategory C<VAR>Z : C<VAR>X₁ X₂ X₃ : GradedObject I C<VAR>inst✝⁷ : X₁.HasTensor X₂<VAR>inst✝⁶ : X₂.HasTensor X₃<VAR>inst✝⁵ : (tensorObj X₁ X₂).HasTensor X₃<VAR>inst✝⁴ : X₁.HasTensor (tensorObj X₂ X₃)<VAR>Y₁ Y₂ Y₃ : GradedObject I C<VAR>inst✝³ : Y₁.HasTensor Y₂<VAR>inst✝² : Y₂.HasTensor Y₃<VAR>inst✝¹ : (tensorObj Y₁ Y₂).HasTensor Y₃<VAR>inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)<VAR>i₁ i₂ i₃ j : I<VAR>h : i₁ + i₂ + i₃ = j<VAR>i₂₃ : I<VAR>h' : i₂ + i₃ = i₂₃<GOAL>i₁ + i₂₃ = j
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : SemilatticeInf γ<VAR>f g : α → γ<VAR>hf : Tendsto f atBot atBot<VAR>hg : Tendsto g atBot atBot<GOAL>Tendsto (Prod.map f g) atBot atBot
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : SemilatticeInf γ<VAR>f g : α → γ<VAR>hf : Tendsto f atBot atBot<VAR>hg : Tendsto g atBot atBot<GOAL>Tendsto (Prod.map f g) (atBot ×ˢ atBot) atBot
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>b x : α<GOAL>x ∈ Iic b ↔ x ≤ b
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>S : Set (RingCon R)<VAR>x✝¹ x✝ : R<GOAL>(sInf S) x✝¹ x✝ ↔ sInf (DFunLike.coe '' S) x✝¹ x✝
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>S : Set (RingCon R)<VAR>x✝¹ x✝ : R<GOAL>(sInf S) x✝¹ x✝ ↔ ∀ i ∈ S, i x✝¹ x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>r : ℝ≥0<GOAL>(↑r • s).toJordanDecomposition = ↑r • s.toJordanDecomposition
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>r : ℝ≥0<GOAL>(↑r • s).toJordanDecomposition = (r • s).toJordanDecomposition
<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>f : α → ℝ<VAR>hf : Integrable f μ<VAR>f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf<GOAL>∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).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>f : α → ℝ<VAR>hf : Integrable f μ<VAR>f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf<VAR>eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖<GOAL>∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).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>f : α → ℝ<VAR>hf : Integrable f μ<VAR>f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf<VAR>eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖<VAR>eq₂ : (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal = ‖Lp.negPart f₁‖<GOAL>∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).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>f : α → ℝ<VAR>hf : Integrable f μ<VAR>f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf<VAR>eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖<VAR>eq₂ : (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal = ‖Lp.negPart f₁‖<GOAL>L1.integral (Integrable.toL1 (fun a => f a) ?hc) = ‖Lp.posPart f₁‖ - ‖Lp.negPart f₁‖
<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>f : α → ℝ<VAR>hf : Integrable f μ<VAR>f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf<VAR>eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖<VAR>eq₂ : (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal = ‖Lp.negPart f₁‖<GOAL>Integrable (fun a => f a) μ
<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>f : α → ℝ<VAR>hf : Integrable f μ<VAR>f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf<VAR>eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖<VAR>eq₂ : (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal = ‖Lp.negPart f₁‖<GOAL>CompleteSpace ℝ
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>g : F → E<VAR>a : F<VAR>hg : ContinuousAt g a<VAR>hf : HasStrictFDerivAt f (↑f') (g a)<VAR>hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y<GOAL>HasStrictFDerivAt g (↑f'.symm) a
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>g : F → E<VAR>a : F<VAR>hf : HasStrictFDerivAt f (↑f') (g a)<VAR>hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y<VAR>hg : ContinuousAt (fun p => (g p.1, g p.2)) (a, a)<GOAL>HasStrictFDerivAt g (↑f'.symm) a
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>g : F → E<VAR>a : F<VAR>hf : HasStrictFDerivAt f (↑f') (g a)<VAR>hg : ContinuousAt (fun p => (g p.1, g p.2)) (a, a)<VAR>hfg : ∀ᶠ (p : F × F) in 𝓝 (a, a), f (g p.1) = p.1 ∧ f (g p.2) = p.2<GOAL>HasStrictFDerivAt g (↑f'.symm) a
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>g : F → E<VAR>a : F<VAR>hf : HasStrictFDerivAt f (↑f') (g a)<VAR>hg : ContinuousAt (fun p => (g p.1, g p.2)) (a, a)<VAR>hfg : ∀ᶠ (p : F × F) in 𝓝 (a, a), f (g p.1) = p.1 ∧ f (g p.2) = p.2<VAR>this : (fun p => g p.1 - g p.2 - f'.symm (p.1 - p.2)) =O[𝓝 (a, a)] fun p => f' (g p.1 - g p.2) - (p.1 - p.2)<GOAL>HasStrictFDerivAt g (↑f'.symm) a
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>g : F → E<VAR>a : F<VAR>hf : HasStrictFDerivAt f (↑f') (g a)<VAR>hg : ContinuousAt (fun p => (g p.1, g p.2)) (a, a)<VAR>hfg : ∀ᶠ (p : F × F) in 𝓝 (a, a), f (g p.1) = p.1 ∧ f (g p.2) = p.2<VAR>this : (fun p => g p.1 - g p.2 - f'.symm (p.1 - p.2)) =O[𝓝 (a, a)] fun p => f' (g p.1 - g p.2) - (p.1 - p.2)<GOAL>(fun p => f' (g p.1 - g p.2) - (p.1 - p.2)) =o[𝓝 (a, a)] fun p => p.1 - p.2
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>g : F → E<VAR>a : F<VAR>hf : HasStrictFDerivAt f (↑f') (g a)<VAR>hg : ContinuousAt (fun p => (g p.1, g p.2)) (a, a)<VAR>hfg : ∀ᶠ (p : F × F) in 𝓝 (a, a), f (g p.1) = p.1 ∧ f (g p.2) = p.2<GOAL>(fun p => f' (g p.1 - g p.2) - (p.1 - p.2)) =o[𝓝 (a, a)] fun p => p.1 - p.2
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>g : F → E<VAR>a : F<VAR>hf : HasStrictFDerivAt f (↑f') (g a)<VAR>hg : ContinuousAt (fun p => (g p.1, g p.2)) (a, a)<VAR>hfg : ∀ᶠ (p : F × F) in 𝓝 (a, a), f (g p.1) = p.1 ∧ f (g p.2) = p.2<GOAL>∀ (x : F × F), f (g x.1) = x.1 ∧ f (g x.2) = x.2 → (fun x => ↑f' (((fun p => (g p.1, g p.2)) x).1 - ((fun p => (g p.1, g p.2)) x).2) - (f ((fun p => (g p.1, g p.2)) x).1 - f ((fun p => (g p.1, g p.2)) x).2)) x = f' (g x.1 - g x.2) - (x.1 - x.2)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>g : F → E<VAR>a : F<VAR>hf : HasStrictFDerivAt f (↑f') (g a)<VAR>hg : ContinuousAt (fun p => (g p.1, g p.2)) (a, a)<VAR>hfg : ∀ᶠ (p : F × F) in 𝓝 (a, a), f (g p.1) = p.1 ∧ f (g p.2) = p.2<GOAL>((fun p => p.1 - p.2) ∘ fun p => (g p.1, g p.2)) =O[𝓝 (a, a)] fun p => p.1 - p.2
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α✝<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α✝<VAR>s✝ s' t : Set α✝<VAR>f : α✝ → β<VAR>G : Type u_8<VAR>α : Type u_9<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s<VAR>h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ<VAR>g₁ g₂ : G<VAR>hg : g₁ ≠ g₂<VAR>g : G := g₂⁻¹ * g₁<GOAL>(AEDisjoint μ on fun g => g • s) g₁ g₂
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α✝<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α✝<VAR>s✝ s' t : Set α✝<VAR>f : α✝ → β<VAR>G : Type u_8<VAR>α : Type u_9<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s<VAR>h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ<VAR>g₁ g₂ : G<VAR>g : G := g₂⁻¹ * g₁<VAR>hg : g ≠ 1<GOAL>(AEDisjoint μ on fun g => g • s) g₁ g₂
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α✝<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α✝<VAR>s✝ s' t : Set α✝<VAR>f : α✝ → β<VAR>G : Type u_8<VAR>α : Type u_9<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s<VAR>h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ<VAR>g₁ g₂ : G<VAR>g : G := g₂⁻¹ * g₁<VAR>hg : g ≠ 1<VAR>this : (fun x => g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s<GOAL>μ (g₁ • s ∩ g₂ • s) = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>s : Set A<GOAL>AlgebraicIndependent R Subtype.val ↔ ∀ p ∈ supported R s, (aeval _root_.id) p = 0 → p = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ n₁₂ : ℤ<VAR>z₁ : Cochain F G n₁<VAR>z₂ z₂' : Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<VAR>p q : ℤ<VAR>hpq : p + n₁₂ = q<GOAL>(z₁.comp (z₂ - z₂') h).v p q hpq = (z₁.comp z₂ h - z₁.comp z₂' h).v p q hpq
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>p q : R[X]<GOAL>(-p).mirror = -p.mirror
<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>v : V<GOAL>(toBaseChange A Q) (involute ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v))) = (Algebra.TensorProduct.map (AlgHom.id A A) involute) ((toBaseChange A Q) ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)))
<VAR>θ : Angle<GOAL>θ.sign = 0 ↔ θ = 0 ∨ θ = ↑π
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α✝<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>inst✝ : SigmaFinite μ<VAR>f : α → E<GOAL>Integrable (fun x => (μ.rnDeriv ν x).toReal • f x) ν ↔ Integrable f μ
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α✝<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>inst✝ : SigmaFinite μ<VAR>f : α → E<GOAL>Integrable (fun x => (μ.rnDeriv ν x).toReal • f x) ν ↔ Integrable f (ν.withDensity (μ.rnDeriv ν))
<VAR>a : ℤ<VAR>e b : ℕ<GOAL>J(a ^ zero | b) = J(a | b) ^ zero
<VAR>a : ℤ<VAR>e b x✝ : ℕ<VAR>ih : J(a ^ x✝ | b) = J(a | b) ^ x✝<GOAL>J(a ^ x✝.succ | b) = J(a | b) ^ x✝.succ
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝ : LinearOrder α<GOAL>Unbounded (fun x x_1 => x ≤ x_1) s ↔ ∀ (a : α), ∃ b ∈ s, a < b
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>y : PrimeSpectrum ↑Γ(X, U)<VAR>hy : hU.fromSpec.val.base y ∈ U<GOAL>IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec.val.base y))) y.asIdeal
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>y : PrimeSpectrum ↑Γ(X, U)<VAR>hy : hU.fromSpec.val.base y ∈ U<GOAL>IsLocalization y.asIdeal.primeCompl ↑((Spec Γ(X, U)).presheaf.stalk y)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>y : PrimeSpectrum ↑Γ(X, U)<VAR>hy : hU.fromSpec.val.base y ∈ U<GOAL>IsLocalization y.asIdeal.primeCompl ↑((Spec Γ(X, U)).presheaf.stalk y) ↔ IsLocalization y.asIdeal.primeCompl ↑((structureSheaf ↑Γ(X, U)).presheaf.stalk y)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>y : PrimeSpectrum ↑Γ(X, U)<VAR>hy : hU.fromSpec.val.base y ∈ U<GOAL>IsLocalization y.asIdeal.primeCompl ↑((Spec Γ(X, U)).presheaf.stalk y) = IsLocalization y.asIdeal.primeCompl ↑((structureSheaf ↑Γ(X, U)).presheaf.stalk y)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>y : PrimeSpectrum ↑Γ(X, U)<VAR>hy : hU.fromSpec.val.base y ∈ U<GOAL>(asIso (Scheme.Hom.stalkMap hU.fromSpec y)).commRingCatIsoToRingEquiv.toRingHom.comp (algebraMap ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec.val.base y))) = StructureSheaf.toStalk (↑Γ(X, U)) y
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>y : PrimeSpectrum ↑Γ(X, U)<VAR>hy : hU.fromSpec.val.base y ∈ U<GOAL>(asIso (Scheme.Hom.stalkMap hU.fromSpec y)).commRingCatIsoToRingEquiv.toRingHom.comp (X.presheaf.germ ⟨hU.fromSpec.val.base y, hy⟩) = StructureSheaf.toStalk (↑Γ(X, U)) y
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>y : PrimeSpectrum ↑Γ(X, U)<VAR>hy : hU.fromSpec.val.base y ∈ U<GOAL>hU.fromSpec.val.c.app (op U) ≫ (Spec Γ(X, U)).presheaf.germ ⟨y, hy⟩ = StructureSheaf.toStalk (↑Γ(X, U)) y