ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.121039, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : CategoryWithHomology C<VAR>K : CochainComplex C ℤ<VAR>A : C<VAR>n i : ℤ<VAR>f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i<VAR>j : ℤ<VAR>hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0<VAR>i' : ℤ<VAR>hi' : n + i = i'<VAR>j' : ℤ<VAR>hj : i + 1 = j<VAR>hj' : i' + 1 = j'<GOAL>(f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) ≫ K.d i' j' = 0
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.121039, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : CategoryWithHomology C<VAR>K : CochainComplex C ℤ<VAR>A : C<VAR>n i : ℤ<VAR>f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i<VAR>j : ℤ<VAR>hf : f ≫ (n.negOnePow • K.d (i + n) (j + n)) = 0<VAR>hj : i + 1 = j<VAR>hi' : n + i = i + n<VAR>hj' : i + n + 1 = j + n<GOAL>(f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n) = 0
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.121039, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : CategoryWithHomology C<VAR>K : CochainComplex C ℤ<VAR>A : C<VAR>n i : ℤ<VAR>f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i<VAR>j : ℤ<VAR>hj : i + 1 = j<VAR>hi' : n + i = i + n<VAR>hj' : i + n + 1 = j + n<VAR>hf : n.negOnePow • f ≫ K.d (i + n) (j + n) = 0<GOAL>(f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n) = 0
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.121039, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : CategoryWithHomology C<VAR>K : CochainComplex C ℤ<VAR>A : C<VAR>n i : ℤ<VAR>f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i<VAR>j : ℤ<VAR>hj : i + 1 = j<VAR>hi' : n + i = i + n<VAR>hj' : i + n + 1 = j + n<VAR>hf : n.negOnePow • f ≫ K.d (i + n) (j + n) = 0<GOAL>1 • (f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n) = 0
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : CategoryWithHomology C<VAR>K : CochainComplex C ℤ<VAR>A : C<VAR>n i : ℤ<VAR>f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i<VAR>j : ℤ<VAR>hj : (up ℤ).next i = j<VAR>hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0<VAR>i' : ℤ<VAR>hi' : n + i = i'<VAR>j' : ℤ<VAR>hj' : (up ℤ).next i' = j'<GOAL>liftCycles ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) f j hj hf ≫ homologyπ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i = liftCycles K (f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) j' hj' ⋯ ≫ homologyπ K i' ≫ ((homologyFunctor C (up ℤ) 0).shiftIso n i i' hi').inv.app K
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : CategoryWithHomology C<VAR>K : CochainComplex C ℤ<VAR>A : C<VAR>n i : ℤ<VAR>f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i<VAR>j : ℤ<VAR>hj : (up ℤ).next i = j<VAR>hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0<VAR>i' : ℤ<VAR>hi' : n + i = i'<VAR>j' : ℤ<VAR>hj' : (up ℤ).next i' = j'<GOAL>(sc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i).liftCycles f ⋯ ≫ (sc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i).homologyπ = ((shiftFunctor C n ⋙ shortComplexFunctor C (up ℤ) i).obj K).liftCycles f ⋯ ≫ ((shiftFunctor C n ⋙ shortComplexFunctor C (up ℤ) i).obj K).homologyπ
<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>iso : E ≃L[𝕜] F<VAR>f : G → E<GOAL>Differentiable 𝕜 (⇑iso ∘ f) ↔ Differentiable 𝕜 f
<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>iso : E ≃L[𝕜] F<VAR>f : G → E<GOAL>DifferentiableOn 𝕜 (⇑iso ∘ f) univ ↔ DifferentiableOn 𝕜 f univ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<VAR>hne : ∀ (i : ι), (f i).Nonempty<GOAL>univ.Countable
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<VAR>hne : ∀ (i : ι), (f i).Nonempty<VAR>this : ∀ (n : ℕ), {i | (f i ∩ compactCovering X n).Nonempty}.Finite<GOAL>univ.Countable
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<VAR>hne : ∀ (i : ι), (f i).Nonempty<VAR>this : ∀ (n : ℕ), {i | (f i ∩ compactCovering X n).Nonempty}.Finite<VAR>i : ι<VAR>x✝ : i ∈ univ<GOAL>i ∈ ⋃ i, {i_1 | (f i_1 ∩ compactCovering X i).Nonempty}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<VAR>hne : ∀ (i : ι), (f i).Nonempty<VAR>this : ∀ (n : ℕ), {i | (f i ∩ compactCovering X n).Nonempty}.Finite<VAR>i : ι<VAR>x✝ : i ∈ univ<VAR>x : X<VAR>hx : x ∈ f i<GOAL>i ∈ ⋃ i, {i_1 | (f i_1 ∩ compactCovering X i).Nonempty}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<VAR>hne : ∀ (i : ι), (f i).Nonempty<VAR>this : ∀ (n : ℕ), {i | (f i ∩ compactCovering X n).Nonempty}.Finite<VAR>i : ι<VAR>x✝ : i ∈ univ<VAR>x : X<VAR>hx : x ∈ f i<VAR>n : ℕ<VAR>hn : x ∈ compactCovering X n<GOAL>i ∈ ⋃ i, {i_1 | (f i_1 ∩ compactCovering X i).Nonempty}
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>u : Set X<VAR>hu : IsOpen u<GOAL>IsOpen (inl '' u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SFinite ν<VAR>s : Set α<GOAL>∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = ((ν.withDensity (μ.rnDeriv ν)) s).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SFinite ν<VAR>s : Set α<GOAL>(∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ((ν.withDensity (μ.rnDeriv ν)) s).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SFinite ν<VAR>s : Set α<GOAL>∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ⊤
<VAR>a b : ℝ<VAR>h : 0 < b<GOAL>IntegrableOn (fun x => rexp (-b * x)) (Ioi a) volume
<VAR>a b : ℝ<VAR>h : 0 < b<VAR>this : Tendsto (fun x => -rexp (-b * x) / b) atTop (𝓝 (-0 / b))<GOAL>IntegrableOn (fun x => rexp (-b * x)) (Ioi a) volume
<VAR>a b : ℝ<VAR>h : 0 < b<VAR>this : Tendsto (fun x => -rexp (-b * x) / b) atTop (𝓝 (-0 / b))<VAR>x : ℝ<VAR>x✝ : x ∈ Ici a<GOAL>HasDerivAt (fun x => -rexp (-b * x) / b) (rexp (-b * x)) x
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>F₁ F₂ : W.Localization ⥤ D<VAR>τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂<GOAL>∀ ⦃X Y : W.Localization⦄ (f : X ⟶ Y), F₁.map f ≫ NatTransExtension.app τ Y = NatTransExtension.app τ X ≫ F₂.map f
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>F₁ F₂ : W.Localization ⥤ D<VAR>τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂<GOAL>MorphismProperty.naturalityProperty (NatTransExtension.app τ) = ⊤
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>F₁ F₂ : W.Localization ⥤ D<VAR>τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂<GOAL>∀ ⦃X Y : C⦄ (f : X ⟶ Y), MorphismProperty.naturalityProperty (NatTransExtension.app τ) (W.Q.map f)
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>F₁ F₂ : W.Localization ⥤ D<VAR>τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>F₁.map (W.Q.map f) ≫ NatTransExtension.app τ (W.Q.obj Y) = NatTransExtension.app τ (W.Q.obj X) ≫ F₂.map (W.Q.map f)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<GOAL>‖x + y‖ = ‖x - y‖ ↔ angle x y = π / 2
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<GOAL>‖x‖ ^ 2 + 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2 ↔ ⟪x, y⟫_ℝ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c✝ : α<VAR>h : a ⩿ b<VAR>c : α<GOAL>c ∈ Icc a b ↔ c ∈ {a, b}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>M' : Type u_5<VAR>N' : Type u_6<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>τ : Type u_9<VAR>ι' : Type u_10<VAR>κ' : Type u_11<VAR>inst✝¹⁸ : DecidableEq ι<VAR>inst✝¹⁷ : DecidableEq κ<VAR>inst✝¹⁶ : DecidableEq τ<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype κ<VAR>inst✝¹³ : Fintype τ<VAR>inst✝¹² : Finite ι'<VAR>inst✝¹¹ : Finite κ'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup N'<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R N'<VAR>bM : Basis ι R M<VAR>bN : Basis κ R N<VAR>bP : Basis τ R P<VAR>bM' : Basis ι' R M'<VAR>bN' : Basis κ' R N'<VAR>f : M →ₗ[R] M'<VAR>g : N →ₗ[R] N'<VAR>i : ι'<VAR>j : κ'<VAR>i' : ι<VAR>j' : κ<GOAL>(toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN')) (map f g) (i, j) (i', j') = kroneckerMap (fun x x_1 => x * x_1) ((toMatrix bM bM') f) ((toMatrix bN bN') g) (i, j) (i', j')
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>M' : Type u_5<VAR>N' : Type u_6<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>τ : Type u_9<VAR>ι' : Type u_10<VAR>κ' : Type u_11<VAR>inst✝¹⁸ : DecidableEq ι<VAR>inst✝¹⁷ : DecidableEq κ<VAR>inst✝¹⁶ : DecidableEq τ<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype κ<VAR>inst✝¹³ : Fintype τ<VAR>inst✝¹² : Finite ι'<VAR>inst✝¹¹ : Finite κ'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup N'<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R N'<VAR>bM : Basis ι R M<VAR>bN : Basis κ R N<VAR>bP : Basis τ R P<VAR>bM' : Basis ι' R M'<VAR>bN' : Basis κ' R N'<VAR>f : M →ₗ[R] M'<VAR>g : N →ₗ[R] N'<VAR>i : ι'<VAR>j : κ'<VAR>i' : ι<VAR>j' : κ<GOAL>(bN'.repr (g (bN j'))) j • (bM'.repr (f (bM i'))) i = (bM'.repr (f (bM i'))) i * (bN'.repr (g (bN j'))) j
<VAR>α : Sort u_1<VAR>r : α → α → Prop<VAR>motive : α → Sort u_2<VAR>intro : α<VAR>a : Acc r intro<VAR>t : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → motive y) → motive x<GOAL>a.ndrecOn t = Acc.ndrecOnC a t
<VAR>n b : ℕ<VAR>l1 l2 : List ℕ<VAR>h : l1.length = l2.length<GOAL>ofDigits b l1 + ofDigits b l2 = ofDigits b (List.zipWith (fun x x_1 => x + x_1) l1 l2)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t✝ u : Set α✝<VAR>inst✝⁸ : TopologicalSpace α✝<VAR>inst✝⁷ : MeasurableSpace α✝<VAR>inst✝⁶ : OpensMeasurableSpace α✝<VAR>inst✝⁵ : MeasurableSpace δ<VAR>inst✝⁴ : LinearOrder α✝<VAR>inst✝³ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderClosedTopology α<VAR>s t : Set α<GOAL>MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S} ≤ borel α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t✝ u : Set α✝<VAR>inst✝⁸ : TopologicalSpace α✝<VAR>inst✝⁷ : MeasurableSpace α✝<VAR>inst✝⁶ : OpensMeasurableSpace α✝<VAR>inst✝⁵ : MeasurableSpace δ<VAR>inst✝⁴ : LinearOrder α✝<VAR>inst✝³ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderClosedTopology α<VAR>s t : Set α<GOAL>∀ t_1 ∈ {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S}, MeasurableSet t_1
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t✝ u : Set α✝<VAR>inst✝⁸ : TopologicalSpace α✝<VAR>inst✝⁷ : MeasurableSpace α✝<VAR>inst✝⁶ : OpensMeasurableSpace α✝<VAR>inst✝⁵ : MeasurableSpace δ<VAR>inst✝⁴ : LinearOrder α✝<VAR>inst✝³ : OrderClosedTopology α✝<VAR>a✝ b✝ x : α✝<VAR>α : Type u_5<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderClosedTopology α<VAR>s t : Set α<VAR>this✝¹ : MeasurableSpace α := borel α<VAR>this✝ : BorelSpace α<VAR>a b : α<GOAL>MeasurableSet (Ico a b)
<VAR>X : Type u_1<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Zero X<VAR>A : Type u_2<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A<VAR>f g : C(X, ℝ)₀<GOAL>{ toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun (f * g) = { toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun f * { toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun g
<VAR>X : Type u_1<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Zero X<VAR>A : Type u_2<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A<VAR>f g : C(X, ℝ)₀<VAR>this : φ ((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) = φ ((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal)<GOAL>{ toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun (f * g) = { toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun f * { toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun g
<VAR>X : Type u_1<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Zero X<VAR>A : Type u_2<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A<VAR>f g : C(X, ℝ)₀<VAR>this : φ (f * g).toNNReal + φ (-f).toNNReal * φ g.toNNReal + φ f.toNNReal * φ (-g).toNNReal = φ (-(f * g)).toNNReal + φ f.toNNReal * φ g.toNNReal + φ (-f).toNNReal * φ (-g).toNNReal<GOAL>φ (f * g).toNNReal - φ (-(f * g)).toNNReal = φ f.toNNReal * φ g.toNNReal - φ (-f).toNNReal * φ g.toNNReal - (φ f.toNNReal * φ (-g).toNNReal - φ (-f).toNNReal * φ (-g).toNNReal)
<VAR>X : Type u_1<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Zero X<VAR>A : Type u_2<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A<VAR>f g : C(X, ℝ)₀<VAR>this : φ (f * g).toNNReal + φ (-f).toNNReal * φ g.toNNReal + φ f.toNNReal * φ (-g).toNNReal - (φ (-(f * g)).toNNReal + φ f.toNNReal * φ g.toNNReal + φ (-f).toNNReal * φ (-g).toNNReal) = 0<GOAL>φ (f * g).toNNReal - φ (-(f * g)).toNNReal - (φ f.toNNReal * φ g.toNNReal - φ (-f).toNNReal * φ g.toNNReal - (φ f.toNNReal * φ (-g).toNNReal - φ (-f).toNNReal * φ (-g).toNNReal)) = 0
<VAR>X : Type u_1<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Zero X<VAR>A : Type u_2<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A<VAR>f g : C(X, ℝ)₀<GOAL>{ toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_smul' := ⋯ }.toFun (f + g) = { toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_smul' := ⋯ }.toFun f + { toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_smul' := ⋯ }.toFun g
<VAR>X : Type u_1<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Zero X<VAR>A : Type u_2<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A<VAR>f g : C(X, ℝ)₀<VAR>this : φ ((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) = φ ((-(f + g)).toNNReal + f.toNNReal + g.toNNReal)<GOAL>{ toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_smul' := ⋯ }.toFun (f + g) = { toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_smul' := ⋯ }.toFun f + { toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_smul' := ⋯ }.toFun g
<VAR>X : Type u_1<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Zero X<VAR>A : Type u_2<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A<VAR>f g : C(X, ℝ)₀<VAR>this : φ (f + g).toNNReal + φ (-f).toNNReal + φ (-g).toNNReal = φ (-(f + g)).toNNReal + φ f.toNNReal + φ g.toNNReal<GOAL>φ (f + g).toNNReal - φ (-(f + g)).toNNReal = φ f.toNNReal - φ (-f).toNNReal + (φ g.toNNReal - φ (-g).toNNReal)
<VAR>X : Type u_1<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Zero X<VAR>A : Type u_2<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A<VAR>f g : C(X, ℝ)₀<VAR>this : φ (f + g).toNNReal + φ (-f).toNNReal + φ (-g).toNNReal - (φ (-(f + g)).toNNReal + φ f.toNNReal + φ g.toNNReal) = 0<GOAL>φ (f + g).toNNReal - φ (-(f + g)).toNNReal - (φ f.toNNReal - φ (-f).toNNReal + (φ g.toNNReal - φ (-g).toNNReal)) = 0
<VAR>X : Type u_1<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Zero X<VAR>A : Type u_2<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A<VAR>r : ℝ<VAR>f : C(X, ℝ)₀<GOAL>(fun f => φ f.toNNReal - φ (-f).toNNReal) (r • f) = (MonoidHom.id ℝ) r • (fun f => φ f.toNNReal - φ (-f).toNNReal) f
<VAR>X : Type u_1<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Zero X<VAR>A : Type u_2<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A<VAR>r : ℝ<VAR>f : C(X, ℝ)₀<GOAL>φ (r • f).toNNReal - φ (-(r • f)).toNNReal = r • (φ f.toNNReal - φ (-f).toNNReal)
<VAR>X : Type u_1<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Zero X<VAR>A : Type u_2<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A<VAR>f : C(X, ℝ)₀<GOAL>{ toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }.toFun (star f) = star ({ toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }.toFun f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(fun x => κ.density ν a x s) =ᶠ[ae (ν a)] Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (countableFiltration γ) (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ : Set ℕ<VAR>inst✝² : Infinite ↑s✝<VAR>inst✝¹ : DecidablePred fun x => x ∈ s✝<VAR>s : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x : ↑s<GOAL>Nat.Subtype.toFunAux x = (Finset.filter (fun x => x ∈ s) (Finset.range ↑x)).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ : Set ℕ<VAR>inst✝² : Infinite ↑s✝<VAR>inst✝¹ : DecidablePred fun x => x ∈ s✝<VAR>s : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x : ↑s<GOAL>(List.filter (fun x => decide (x ∈ s)) (List.range ↑x)).length = (Finset.filter (fun x => x ∈ s) (Finset.range ↑x)).card
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<VAR>σ : Equiv.Perm (Fin n)<GOAL>σ = sort f ↔ Monotone (f ∘ ⇑σ) ∧ ∀ (i j : Fin n), i < j → f (σ i) = f (σ j) → σ i < σ j
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<VAR>σ : Equiv.Perm (Fin n)<GOAL>StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f)) ↔ Monotone (f ∘ ⇑σ) ∧ ∀ (i j : Fin n), i < j → f (σ i) = f (σ j) → σ i < σ j
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<VAR>σ : Equiv.Perm (Fin n)<VAR>h : StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))<VAR>i j : Fin n<VAR>hij : i < j<VAR>hfij : f (σ i) = f (σ j)<GOAL>σ i < σ j
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<VAR>σ : Equiv.Perm (Fin n)<VAR>h : Monotone (f ∘ ⇑σ) ∧ ∀ (i j : Fin n), i < j → f (σ i) = f (σ j) → σ i < σ j<VAR>i j : Fin n<VAR>hij : i < j<GOAL>(Equiv.trans σ (graphEquiv₁ f)) i < (Equiv.trans σ (graphEquiv₁ f)) j
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<GOAL>MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x ↔ DifferentiableWithinAt 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<GOAL>ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f s x
<VAR>d n : ℕ<VAR>h : d < n<GOAL>∃ᶠ (m : ℕ) in atTop, m % n = d
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<GOAL>x ∈ M.closure I ↔ M.Dep (insert x I) ∨ x ∈ I
<VAR>x y z : ZFSet<GOAL>z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y
<VAR>x y z : ZFSet<GOAL>z ∈ (x ∪ y).toSet ↔ z ∈ x ∨ z ∈ y
<VAR>R : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>t : (ι →₀ M) ⊗[R] N<VAR>i : ι<GOAL>((finsuppLeft R M N ι) t) i = (rTensor N (Finsupp.lapply i)) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s t : Set α<VAR>f : α → β<VAR>hf : Injective f<GOAL>f '' s ⊆ f '' t ↔ s ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s t : Set α<VAR>f : α → β<VAR>hf : Injective f<VAR>h : f '' s ⊆ f '' t<GOAL>s ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s t : Set α<VAR>f : α → β<VAR>hf : Injective f<VAR>h : f '' s ⊆ f '' t<GOAL>f ⁻¹' (f '' s) ⊆ f ⁻¹' (f '' t)