ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_7, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.119255, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : ℱ ⟶ ℱ'.val<VAR>X : Dᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj (ℱ.obj X)).obj U<VAR>Y : D<VAR>f : Y ⟶ unop X<VAR>hf : (Sieve.coverByImage G (unop X)).arrows f<GOAL>(ℱ'.val ⋙ coyoneda.obj (op (unop U))).map ((Nonempty.some hf).lift ≫ (Nonempty.some hf).map).op (let_fun this := (yoneda.map (α.app X)).app U a✝; this) = pushforwardFamily (homOver (whiskerLeft G.op α) (unop U)) a✝ f hf
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>hs : IsClosed s<GOAL>IsClosed (μ.everywherePosSubset s)
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>hs : IsClosed s<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>hu : μ.everywherePosSubset s = s \ u<GOAL>IsClosed (μ.everywherePosSubset s)
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>hs : IsClosed s<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>hu : μ.everywherePosSubset s = s \ u<GOAL>IsClosed (s \ u)
<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>s : Set β<GOAL>f ⁻¹' (range f ∩ s) = f ⁻¹' s
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<GOAL>IsEmpty (PProd α β) ↔ IsEmpty α ∨ IsEmpty β
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Finite α<GOAL>Submonoid.closure {σ | σ.IsSwap} = ⊤
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>val✝ : Fintype α<GOAL>Submonoid.closure {σ | σ.IsSwap} = ⊤
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>val✝ : Fintype α<VAR>x : Perm α<VAR>x✝ : x ∈ ⊤<GOAL>x ∈ Submonoid.closure {σ | σ.IsSwap}
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>val✝ : Fintype α<VAR>x : Perm α<VAR>x✝ : x ∈ ⊤<VAR>h1 : (↑x.truncSwapFactors.out).prod = x<VAR>h2 : ∀ g ∈ ↑x.truncSwapFactors.out, g.IsSwap<GOAL>x ∈ Submonoid.closure {σ | σ.IsSwap}
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>val✝ : Fintype α<VAR>x : Perm α<VAR>x✝ : x ∈ ⊤<VAR>h1 : (↑x.truncSwapFactors.out).prod = x<VAR>h2 : ∀ g ∈ ↑x.truncSwapFactors.out, g.IsSwap<GOAL>(↑x.truncSwapFactors.out).prod ∈ Submonoid.closure {σ | σ.IsSwap}
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x : RatFunc K<VAR>hx : x ≠ 0<VAR>s : K[X]<VAR>hs : s ≠ 0<GOAL>↑(x.num * s).natDegree - ↑(s * x.denom).natDegree = x.intDegree
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x : RatFunc K<VAR>hx : x ≠ 0<VAR>s : K[X]<VAR>hs : s ≠ 0<GOAL>x.num * s * x.denom = x.num * (s * x.denom)
<VAR>x : ℂ<GOAL>cos (↑π / 2 - x) = sin x
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>p : J → Prop<VAR>inst✝ : HasBiproduct (Subtype.restrict p f)<GOAL>fromSubtype f p ≫ toSubtype f p = 𝟙 (⨁ Subtype.restrict p f)
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>p : J → Prop<VAR>inst✝ : HasBiproduct (Subtype.restrict p f)<VAR>j : Subtype p<GOAL>(fromSubtype f p ≫ toSubtype f p) ≫ π (Subtype.restrict p f) j = 𝟙 (⨁ Subtype.restrict p f) ≫ π (Subtype.restrict p f) j
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>s t : Set α<VAR>l : Filter α<GOAL>s ∩ t =ᶠ[l] s ↔ ∀ᶠ (x : α) in l, x ∈ s → x ∈ t
<VAR>M✝ : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>α : Type u_4<VAR>M : Type u_5<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : SMul α M<VAR>inst✝ : IsScalarTower α M M<VAR>c : Con M<VAR>a : α<VAR>w x : M<VAR>h : c w x<GOAL>c (a • w) (a • x)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : Fintype ι<VAR>f : E → 𝕜<VAR>inst✝¹ : MeasureSpace E<VAR>inst✝ : SigmaFinite volume<GOAL>∫ (x : ι → E), ∏ i : ι, f (x i) = (∫ (x : E), f x) ^ card ι
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<GOAL>T2Space X ↔ IsClosed (diagonal X)
<VAR>n : ℕ<VAR>c : Composition n<VAR>i : Fin (ones n).length<VAR>h : 0 < (ones n).blocksFun i<GOAL>↑(((ones n).embedding i) ⟨0, h⟩) = ↑⟨↑i, ⋯⟩
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n : ℕ<VAR>hf : Adapted ℱ f<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<GOAL>Martingale (martingalePart f ℱ μ) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n : ℕ<VAR>hf : Adapted ℱ f<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>i j : ℕ<VAR>hij : i ≤ j<GOAL>μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ] martingalePart f ℱ μ i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n : ℕ<VAR>hf : Adapted ℱ f<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>h_eq_sum : μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ] f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i])<GOAL>μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ] martingalePart f ℱ μ i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n : ℕ<VAR>hf : Adapted ℱ f<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>h_eq_sum : μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ] f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i])<GOAL>f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i]) =ᶠ[ae μ] martingalePart f ℱ μ i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n : ℕ<VAR>hf : Adapted ℱ f<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>h_eq_sum : μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ] f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i])<VAR>h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] 0<GOAL>f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i]) =ᶠ[ae μ] martingalePart f ℱ μ i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n : ℕ<VAR>hf : Adapted ℱ f<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>h_eq_sum : μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ] f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i])<VAR>h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] 0<VAR>h_lt : ∀ k < i, μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] f (k + 1) - f k - μ[f (k + 1) - f k|↑ℱ k]<GOAL>f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i]) =ᶠ[ae μ] martingalePart f ℱ μ i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n : ℕ<VAR>hf : Adapted ℱ f<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>h_eq_sum : μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ] f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i])<VAR>h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] 0<VAR>h_lt : ∀ k < i, μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] f (k + 1) - f k - μ[f (k + 1) - f k|↑ℱ k]<GOAL>f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i]) =ᶠ[ae μ] (fun n => f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i|↑ℱ i])) i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n : ℕ<VAR>hf : Adapted ℱ f<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>h_eq_sum : μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ] f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i])<VAR>h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] 0<VAR>h_lt : ∀ k < i, μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] f (k + 1) - f k - μ[f (k + 1) - f k|↑ℱ k]<GOAL>∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i]) =ᶠ[ae μ] ∑ i ∈ Finset.range i, (f (i + 1) - f i - μ[f (i + 1) - f i|↑ℱ i])
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n : ℕ<VAR>hf : Adapted ℱ f<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>h_eq_sum : μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ] f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i])<VAR>h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] 0<VAR>h_lt : ∀ k < i, μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] f (k + 1) - f k - μ[f (k + 1) - f k|↑ℱ k]<GOAL>∑ k ∈ Finset.range i, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i]) + ∑ k ∈ Finset.Ico i j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i]) =ᶠ[ae μ] ∑ i ∈ Finset.range i, (f (i + 1) - f i - μ[f (i + 1) - f i|↑ℱ i]) + 0
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n : ℕ<VAR>hf : Adapted ℱ f<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>h_eq_sum : μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ] f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i])<VAR>h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] 0<VAR>h_lt : ∀ k < i, μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] f (k + 1) - f k - μ[f (k + 1) - f k|↑ℱ k]<GOAL>∑ k ∈ Finset.Ico i j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i]) =ᶠ[ae μ] 0
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n : ℕ<VAR>hf : Adapted ℱ f<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>h_eq_sum : μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ] f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i])<VAR>h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] 0<VAR>h_lt : ∀ k < i, μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] f (k + 1) - f k - μ[f (k + 1) - f k|↑ℱ k]<GOAL>∑ i ∈ Finset.Ico i j, 0 =ᶠ[ae μ] 0
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n : ℕ<VAR>hf : Adapted ℱ f<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>h_eq_sum : μ[martingalePart f ℱ μ j|↑ℱ i] =ᶠ[ae μ] f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i])<VAR>h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] 0<VAR>h_lt : ∀ k < i, μ[f (k + 1) - f k|↑ℱ i] - μ[μ[f (k + 1) - f k|↑ℱ k]|↑ℱ i] =ᶠ[ae μ] f (k + 1) - f k - μ[f (k + 1) - f k|↑ℱ k]<GOAL>0 =ᶠ[ae μ] 0
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>p✝ : R[X]<VAR>r : R<VAR>p q : R[X]<VAR>S : Type u_2<VAR>inst✝⁵ : NonAssocSemiring S<VAR>inst✝⁴ : Module R S<VAR>inst✝³ : IsScalarTower R S S<VAR>inst✝² : SMulCommClass R S S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>x : S<GOAL>(p * X ^ 0).smeval x = p.smeval x * x ^ 0
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>p✝ : R[X]<VAR>r : R<VAR>p q : R[X]<VAR>S : Type u_2<VAR>inst✝⁵ : NonAssocSemiring S<VAR>inst✝⁴ : Module R S<VAR>inst✝³ : IsScalarTower R S S<VAR>inst✝² : SMulCommClass R S S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>x : S<VAR>n : ℕ<GOAL>(p * X ^ (n + 1)).smeval x = p.smeval x * x ^ (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f f₁ f₂ : Filter α<VAR>h h₁ h₂ : Set α → Set β<VAR>a : α<VAR>hh : Monotone h<GOAL>(pure a).lift' h = 𝓟 (h {a})
<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>n : ℕ<GOAL>fderiv 𝕜 (iteratedFDeriv 𝕜 n f) = ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ iteratedFDeriv 𝕜 (n + 1) f
<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>n : ℕ<GOAL>fderiv 𝕜 (iteratedFDeriv 𝕜 n f) = ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)
<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>n : ℕ<VAR>x : E<GOAL>fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x = (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f✝ g✝ f g : α → E<VAR>hf : Memℒp f p μ<VAR>hg : Memℒp g p μ<GOAL>LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ) < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f✝ g✝ f g : α → E<VAR>hf : Memℒp f p μ<VAR>hg : Memℒp g p μ<GOAL>eLpNorm f p μ + eLpNorm g p μ ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d x✝ : α<GOAL>x✝ ∈ Ioo a b ∩ Iio c ↔ x✝ ∈ Ioo a (min b c)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf : MeasurableEmbedding f<VAR>g : E → ℝ<VAR>hg : ∀ᵐ (x : E) ∂μ, x ∈ f '' s → 0 ≤ g x<VAR>hg_int : IntegrableOn g (f '' s) μ<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<GOAL>(Measure.comap f (μ.withDensity fun x => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf : MeasurableEmbedding f<VAR>g : E → ℝ<VAR>hg : ∀ᵐ (x : E) ∂μ, x ∈ f '' s → 0 ≤ g x<VAR>hg_int : IntegrableOn g (f '' s) μ<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<GOAL>ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ) = ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t✝ u✝ : Set α<VAR>s : Set (Set α)<VAR>t : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>hs : t = TopologicalSpace.generateFrom s<VAR>u : Set α<VAR>hu : TopologicalSpace.IsOpen u<GOAL>MeasurableSet u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>E : Type u_4<VAR>inst✝ : One M<VAR>s t : Set α<VAR>f g : α → M<VAR>a : α<VAR>l : Filter α<VAR>hf : f =ᶠ[l ⊓ 𝓟 s] g<VAR>hs : s =ᶠ[l] t<VAR>x : α<VAR>hst : x ∈ s ↔ x ∈ t<VAR>hfg : x ∈ s → f x = g x<VAR>hxs : x ∈ s<GOAL>s.mulIndicator f x = t.mulIndicator g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>E : Type u_4<VAR>inst✝ : One M<VAR>s t : Set α<VAR>f g : α → M<VAR>a : α<VAR>l : Filter α<VAR>hf : f =ᶠ[l ⊓ 𝓟 s] g<VAR>hs : s =ᶠ[l] t<VAR>x : α<VAR>hst : x ∈ s ↔ x ∈ t<VAR>hfg : x ∈ s → f x = g x<VAR>hxs : x ∉ s<GOAL>s.mulIndicator f x = t.mulIndicator g x
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>b : α<VAR>s : Multiset α<GOAL>∀ (a : List α), countP p (b ::ₘ Quot.mk Setoid.r a) = countP p (Quot.mk Setoid.r a) + if p b then 1 else 0
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<GOAL>P2 x₁ x₂ y ↔ P2 x₁ x₂ (-y)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s t u v : Finset α<GOAL>s ○ (t ○ u) = t ○ (s ○ u)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>p✝ p' : Submodule R M<VAR>q✝ : Submodule R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>p q : Submodule R M<VAR>h : p ≤ q<GOAL>range (inclusion h) = comap q.subtype p
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : Fork f g<VAR>W : C<VAR>k l : W ⟶ s.pt<VAR>h : k ≫ s.ι = l ≫ s.ι<VAR>this : k ≫ s.ι ≫ f = l ≫ s.ι ≫ f<GOAL>k ≫ s.π.app one = l ≫ s.π.app one
<VAR>C : Type u'<VAR>inst✝⁴ : Category.{v', u'} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>inst✝¹ : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝ : HasWeakSheafify J AddCommGrp<VAR>M₀ : PresheafOfModules R₀<GOAL>({ obj := fun M₀ => sheafify α (CategoryTheory.toSheafify J M₀.presheaf), map := fun {X Y} f => sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Y.presheaf) f ((presheafToSheaf J AddCommGrp).map f.hom) ⋯ }.map (𝟙 M₀)).val = (𝟙 ({ obj := fun M₀ => sheafify α (CategoryTheory.toSheafify J M₀.presheaf), map := fun {X Y} f => sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Y.presheaf) f ((presheafToSheaf J AddCommGrp).map f.hom) ⋯ }.obj M₀)).val
<VAR>C : Type u'<VAR>inst✝⁴ : Category.{v', u'} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>inst✝¹ : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝ : HasWeakSheafify J AddCommGrp<VAR>M₀ : PresheafOfModules R₀<GOAL>(toPresheaf R.val).map ({ obj := fun M₀ => sheafify α (CategoryTheory.toSheafify J M₀.presheaf), map := fun {X Y} f => sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Y.presheaf) f ((presheafToSheaf J AddCommGrp).map f.hom) ⋯ }.map (𝟙 M₀)).val = (toPresheaf R.val).map (𝟙 ({ obj := fun M₀ => sheafify α (CategoryTheory.toSheafify J M₀.presheaf), map := fun {X Y} f => sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Y.presheaf) f ((presheafToSheaf J AddCommGrp).map f.hom) ⋯ }.obj M₀)).val
<VAR>C : Type u'<VAR>inst✝⁴ : Category.{v', u'} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>inst✝¹ : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝ : HasWeakSheafify J AddCommGrp<VAR>X✝ Y✝ Z✝ : PresheafOfModules R₀<VAR>x✝¹ : X✝ ⟶ Y✝<VAR>x✝ : Y✝ ⟶ Z✝<GOAL>({ obj := fun M₀ => sheafify α (CategoryTheory.toSheafify J M₀.presheaf), map := fun {X Y} f => sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Y.presheaf) f ((presheafToSheaf J AddCommGrp).map f.hom) ⋯ }.map (x✝¹ ≫ x✝)).val = ({ obj := fun M₀ => sheafify α (CategoryTheory.toSheafify J M₀.presheaf), map := fun {X Y} f => sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Y.presheaf) f ((presheafToSheaf J AddCommGrp).map f.hom) ⋯ }.map x✝¹ ≫ { obj := fun M₀ => sheafify α (CategoryTheory.toSheafify J M₀.presheaf), map := fun {X Y} f => sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Y.presheaf) f ((presheafToSheaf J AddCommGrp).map f.hom) ⋯ }.map x✝).val