ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>inst✝ : CompleteSpace E<VAR>t : ↑(Icc v.tMin v.tMax)<VAR>this✝ : Fact (↑t ∈ Icc v.tMin v.tMax)<VAR>this : HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..x, f.vComp τ) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t<VAR>a✝ : ℝ<VAR>ht' : a✝ ∈ Icc v.tMin v.tMax<GOAL>∫ (τ : ℝ) in ↑v.t₀..↑(v.proj a✝), f.vComp τ = ∫ (τ : ℝ) in ↑v.t₀..a✝, f.vComp τ
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι✝ : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ q : Seminorm 𝕜 E<VAR>x : E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<GOAL>BddAbove (range p) ↔ ∀ (x : E), BddAbove (range fun i => (p i) x)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι✝ : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ q : Seminorm 𝕜 E<VAR>x : E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<GOAL>(∀ (a : E), BddAbove (range fun i => (DFunLike.coe ∘ p) i a)) ↔ ∀ (x : E), BddAbove (range fun i => (p i) x)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>Real.cos (angle x (x - y)) = ‖x‖ / ‖x - y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<GOAL>Real.cos (angle x (x - y)) = ‖x‖ / ‖x - y‖
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : TopologicalSpace F<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F TotalSpace.proj<VAR>x : TotalSpace F E<VAR>b✝ : B<VAR>y : E b✝<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : Module R F<VAR>inst✝³ : (x : B) → AddCommMonoid (E x)<VAR>inst✝² : (x : B) → Module R (E x)<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : Trivialization.IsLinear R e<VAR>inst✝ : Trivialization.IsLinear R e'<VAR>b : B<VAR>hb : b ∈ e'.baseSet ∩ e.baseSet<GOAL>(coordChangeL R e e' b).symm = coordChangeL R e' e b
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : TopologicalSpace F<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F TotalSpace.proj<VAR>x : TotalSpace F E<VAR>b✝ : B<VAR>y : E b✝<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : Module R F<VAR>inst✝³ : (x : B) → AddCommMonoid (E x)<VAR>inst✝² : (x : B) → Module R (E x)<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : Trivialization.IsLinear R e<VAR>inst✝ : Trivialization.IsLinear R e'<VAR>b : B<VAR>hb : b ∈ e'.baseSet ∩ e.baseSet<GOAL>(coordChangeL R e e' b).symm.toLinearEquiv = (coordChangeL R e' e b).toLinearEquiv
<VAR>α : Type u<VAR>f g : Filter α<VAR>s t : Set α<VAR>h : ∀ (s : Set α), s ∈ f ↔ s ∈ g<GOAL>f = g
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>s.powerset = {∅} ↔ s = ∅
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>h : LineDifferentiableAt 𝕜 f x v<VAR>hL : f₁ =ᶠ[𝓝 x] f<GOAL>LineDifferentiableAt 𝕜 f₁ x v
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>h : LineDifferentiableAt 𝕜 f x v<VAR>hL : f₁ =ᶠ[𝓝 x] f<GOAL>(fun t => f₁ (x + t • v)) =ᶠ[𝓝 0] fun t => f (x + t • v)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F✝ : Type u_2<VAR>inst✝³ : NormedAddCommGroup F✝<VAR>inst✝² : NormedSpace 𝕜 F✝<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F✝<VAR>f' : F✝<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F✝<VAR>h : LineDifferentiableAt 𝕜 f x v<VAR>F : 𝕜 → E := fun t => x + t • v<VAR>hL : f₁ =ᶠ[𝓝 (F 0)] f<GOAL>(fun t => f₁ (x + t • v)) =ᶠ[𝓝 0] fun t => f (x + t • v)
<VAR>a✝ b✝ c : ℕ<VAR>α : Type u_1<VAR>inst✝ : DivisionSemiring α<VAR>a : α<VAR>b : ℤ<VAR>nb ne : ℕ<VAR>pb : IsNat b nb<VAR>pe' : IsNat (a ^ nb) ne<GOAL>IsNat (a ^ b) ne
<VAR>x y z : ℝ<GOAL>sinh x < 0 ↔ x < 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>t : Set F<VAR>x : E<VAR>y : F<VAR>hx : x ∈ (convexHull R) s<VAR>hy : y ∈ (convexHull R) t<GOAL>(x, y) ∈ (convexHull R) (s ×ˢ t)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>t : Set F<VAR>x : E<VAR>y : F<VAR>hx : ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x<VAR>hy : ∃ ι x w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ t) ∧ ∑ i : ι, w i • z i = y<GOAL>∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s ×ˢ t) ∧ ∑ i : ι, w i • z i = (x, y)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι✝ : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι✝<VAR>c : R<VAR>t✝ : Finset ι✝<VAR>w✝² : ι✝ → R<VAR>z : ι✝ → E<VAR>t : Set F<VAR>x : E<VAR>y : F<VAR>ι : Type<VAR>w✝¹ : Fintype ι<VAR>w : ι → R<VAR>f : ι → E<VAR>hw₀ : ∀ (i : ι), 0 ≤ w i<VAR>hw₁ : ∑ i : ι, w i = 1<VAR>hfs : ∀ (i : ι), f i ∈ s<VAR>hf : ∑ i : ι, w i • f i = x<VAR>κ : Type<VAR>w✝ : Fintype κ<VAR>v : κ → R<VAR>g : κ → F<VAR>hv₀ : ∀ (i : κ), 0 ≤ v i<VAR>hv₁ : ∑ i : κ, v i = 1<VAR>hgt : ∀ (i : κ), g i ∈ t<VAR>hg : ∑ i : κ, v i • g i = y<GOAL>∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s ×ˢ t) ∧ ∑ i : ι, w i • z i = (x, y)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι✝ : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι✝<VAR>c : R<VAR>t✝ : Finset ι✝<VAR>w✝² : ι✝ → R<VAR>z : ι✝ → E<VAR>t : Set F<VAR>x : E<VAR>y : F<VAR>ι : Type<VAR>w✝¹ : Fintype ι<VAR>w : ι → R<VAR>f : ι → E<VAR>hw₀ : ∀ (i : ι), 0 ≤ w i<VAR>hw₁ : ∑ i : ι, w i = 1<VAR>hfs : ∀ (i : ι), f i ∈ s<VAR>hf : ∑ i : ι, w i • f i = x<VAR>κ : Type<VAR>w✝ : Fintype κ<VAR>v : κ → R<VAR>g : κ → F<VAR>hv₀ : ∀ (i : κ), 0 ≤ v i<VAR>hv₁ : ∑ i : κ, v i = 1<VAR>hgt : ∀ (i : κ), g i ∈ t<VAR>hg : ∑ i : κ, v i • g i = y<VAR>h_sum : ∑ i : ι × κ, w i.1 * v i.2 = 1<GOAL>∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s ×ˢ t) ∧ ∑ i : ι, w i • z i = (x, y)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f✝ f : R →+* S<VAR>p : R[X]<VAR>n : ℕ<GOAL>eval (↑n) (map f p) = f (eval (↑n) p)
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → ℝ<VAR>s : Set ℝ<VAR>hcs : IsCompact s<VAR>huX : IsUniform X s ℙ volume<VAR>hnt : ¬(volume s = 0 ∨ volume s = ⊤)<GOAL>Integrable (fun x => x * (pdf X ℙ volume x).toReal) volume
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → ℝ<VAR>s : Set ℝ<VAR>hcs : IsCompact s<VAR>huX : IsUniform X s ℙ volume<VAR>hnt : ¬volume s = 0 ∧ ¬volume s = ⊤<GOAL>Integrable (fun x => x * (pdf X ℙ volume x).toReal) volume
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → ℝ<VAR>s : Set ℝ<VAR>hcs : IsCompact s<VAR>huX : IsUniform X s ℙ volume<VAR>hnt : ¬volume s = 0 ∧ ¬volume s = ⊤<VAR>this : IsProbabilityMeasure ℙ<GOAL>Integrable (fun x => x * (pdf X ℙ volume x).toReal) volume
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → ℝ<VAR>s : Set ℝ<VAR>hcs : IsCompact s<VAR>huX : IsUniform X s ℙ volume<VAR>hnt : ¬volume s = 0 ∧ ¬volume s = ⊤<VAR>this : IsProbabilityMeasure ℙ<GOAL>HasFiniteIntegral (fun x => x * (pdf X ℙ volume x).toReal) volume
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → ℝ<VAR>s : Set ℝ<VAR>hcs : IsCompact s<VAR>huX : IsUniform X s ℙ volume<VAR>hnt : ¬volume s = 0 ∧ ¬volume s = ⊤<VAR>this : IsProbabilityMeasure ℙ<GOAL>∫⁻ (x : ℝ), ↑‖x‖₊ * s.indicator ((volume s)⁻¹ • 1) x ≠ ⊤
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → ℝ<VAR>s : Set ℝ<VAR>hcs : IsCompact s<VAR>huX : IsUniform X s ℙ volume<VAR>hnt : ¬volume s = 0 ∧ ¬volume s = ⊤<VAR>this : IsProbabilityMeasure ℙ<VAR>ind : ℝ → ℝ≥0∞ := (volume s)⁻¹ • 1<GOAL>∫⁻ (x : ℝ), ↑‖x‖₊ * s.indicator ind x ≠ ⊤
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → ℝ<VAR>s : Set ℝ<VAR>hcs : IsCompact s<VAR>huX : IsUniform X s ℙ volume<VAR>hnt : ¬volume s = 0 ∧ ¬volume s = ⊤<VAR>this✝ : IsProbabilityMeasure ℙ<VAR>ind : ℝ → ℝ≥0∞ := (volume s)⁻¹ • 1<VAR>this : ∀ (x : ℝ), ↑‖x‖₊ * s.indicator ind x = s.indicator (fun x => ↑‖x‖₊ * ind x) x<GOAL>∫⁻ (x : ℝ), ↑‖x‖₊ * s.indicator ind x ≠ ⊤
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → ℝ<VAR>s : Set ℝ<VAR>hcs : IsCompact s<VAR>huX : IsUniform X s ℙ volume<VAR>hnt : ¬volume s = 0 ∧ ¬volume s = ⊤<VAR>this✝ : IsProbabilityMeasure ℙ<VAR>ind : ℝ → ℝ≥0∞ := (volume s)⁻¹ • 1<VAR>this : ∀ (x : ℝ), ↑‖x‖₊ * s.indicator ind x = s.indicator (fun x => ↑‖x‖₊ * ind x) x<GOAL>∫⁻ (x : ℝ) in s, ↑‖x‖₊ * (volume s)⁻¹ ∂volume ≠ ⊤
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → ℝ<VAR>s : Set ℝ<VAR>hcs : IsCompact s<VAR>huX : IsUniform X s ℙ volume<VAR>hnt : ¬volume s = 0 ∧ ¬volume s = ⊤<VAR>this✝ : IsProbabilityMeasure ℙ<VAR>ind : ℝ → ℝ≥0∞ := (volume s)⁻¹ • 1<VAR>this : ∀ (x : ℝ), ↑‖x‖₊ * s.indicator ind x = s.indicator (fun x => ↑‖x‖₊ * ind x) x<GOAL>(∫⁻ (a : ℝ) in s, ↑‖a‖₊ ∂volume) * (volume s)⁻¹ ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f : α →. β ⊕ α<VAR>a : α<VAR>b : β<VAR>h : b ∈ f.fix a<GOAL>Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f : α →. β ⊕ α<VAR>a : α<VAR>b : β<VAR>h : b ∈ f.fix a<VAR>h₁ : Acc (fun x y => Sum.inr x ∈ f y) a<VAR>h₂ : b ∈ WellFounded.fixF (fun a IH => Part.assert (f a).Dom fun hf => match e : (f a).get hf with | Sum.inl b => Part.some b | Sum.inr a' => IH a' ⋯) a h₁<GOAL>Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f : α →. β ⊕ α<VAR>a : α<VAR>b : β<VAR>h : b ∈ f.fix a<VAR>h₁ : Acc (fun x y => Sum.inr x ∈ f y) a<VAR>h₂ : b ∈ Part.assert (f a).Dom fun hf => match e : (f a).get hf with | Sum.inl b => Part.some b | Sum.inr a' => (fun y p => WellFounded.fixF (fun a IH => Part.assert (f a).Dom fun hf => match e : (f a).get hf with | Sum.inl b => Part.some b | Sum.inr a' => IH a' ⋯) y ⋯) a' ⋯<GOAL>Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f : α →. β ⊕ α<VAR>a : α<VAR>b : β<VAR>h : b ∈ f.fix a<VAR>h₁ : Acc (fun x y => Sum.inr x ∈ f y) a<VAR>h₂ : ∃ (h : (f a).Dom), b ∈ match e : (f a).get h with | Sum.inl b => Part.some b | Sum.inr a' => WellFounded.fixF (fun a IH => Part.assert (f a).Dom fun hf => match e : (f a).get hf with | Sum.inl b => Part.some b | Sum.inr a' => IH a' ⋯) a' ⋯<GOAL>Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f : α →. β ⊕ α<VAR>a : α<VAR>b : β<VAR>h : b ∈ f.fix a<VAR>h₁ : Acc (fun x y => Sum.inr x ∈ f y) a<VAR>h₂ : (f a).Dom<VAR>b✝ : β<VAR>heq✝ : (f a).get h₂ = Sum.inl b✝<VAR>h₃ : b ∈ Part.some b✝<GOAL>Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f : α →. β ⊕ α<VAR>a : α<VAR>b : β<VAR>h : b ∈ f.fix a<VAR>h₁ : Acc (fun x y => Sum.inr x ∈ f y) a<VAR>h₂ : (f a).Dom<VAR>a'✝ : α<VAR>heq✝ : (f a).get h₂ = Sum.inr a'✝<VAR>h₃ : b ∈ WellFounded.fixF (fun a IH => Part.assert (f a).Dom fun hf => match e : (f a).get hf with | Sum.inl b => Part.some b | Sum.inr a' => IH a' ⋯) a'✝ ⋯<GOAL>Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f : α →. β ⊕ α<VAR>a : α<VAR>b : β<VAR>h : Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'<GOAL>b ∈ f.fix a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f : α →. β ⊕ α<VAR>a : α<VAR>b : β<VAR>h : Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'<GOAL>∃ (h : Acc (fun x y => Sum.inr x ∈ f y) a), b ∈ WellFounded.fixF (fun a IH => Part.assert (f a).Dom fun hf => match e : (f a).get hf with | Sum.inl b => Part.some b | Sum.inr a' => IH a' ⋯) a h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : LT α<VAR>a b : α<GOAL>↑a < ↑b ↔ a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : α → E<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑((μ.withDensityᵥ f).trim hm) i = ∫ (x : α) in i, f x ∂μ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>U R (n + 1) = 2 * X * U R n - U R (n - 1)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha : ↑a ≠ 0<VAR>x y : ZMod p<VAR>hy : y ≠ 0<VAR>hxy : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = 0 * y⁻¹ ^ 2<GOAL>legendreSym p a = 1
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha : ↑a ≠ 0<VAR>x y : ZMod p<VAR>hy : y ≠ 0<VAR>hxy : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = 0<GOAL>legendreSym p a = 1
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha : ↑a ≠ 0<VAR>x y : ZMod p<VAR>hy : y ≠ 0<VAR>hxy : x * y⁻¹ * (x * y⁻¹) = ↑a<GOAL>legendreSym p a = 1
<VAR>f : [0] ⟶ [0]<VAR>x✝ : Fin ([0].len + 1)<GOAL>(Hom.toOrderHom f) x✝ = (Hom.toOrderHom (𝟙 [0])) x✝
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁶ : Ring k<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module k V<VAR>inst✝³ : AffineSpace V P<VAR>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>s : Set P<VAR>e : P ≃ᵃ[k] P₂<VAR>this : ⇑e ∘ Subtype.val = Subtype.val ∘ ⇑((↑e).image s)<GOAL>AffineIndependent k Subtype.val ↔ AffineIndependent k Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>f : α → β<VAR>g : β → α<VAR>h : LeftInverse g f<VAR>s : Set α<GOAL>g '' (f '' s) = s
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝² : Monoid N<VAR>inst✝¹ : (i : ι) → DecidableEq (M i)<VAR>inst✝ : DecidableEq ι<VAR>C : Word M → Prop<VAR>h_empty : C empty<VAR>h_smul : ∀ (i : ι) (m : M i) (w : Word M), C w → C (of m • w)<VAR>w : Word M<GOAL>C w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : α → β → ℝ≥0<VAR>g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>a : α<GOAL>(κ.withDensity fun a x => ↑(f a x) * g a x) a = ((κ.withDensity fun a x => ↑(f a x)).withDensity g) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : α → β → ℝ≥0<VAR>g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>a : α<GOAL>((κ a).withDensity fun x => ↑(f a x) * g a x) = ((κ.withDensity fun a x => ↑(f a x)).withDensity g) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : α → β → ℝ≥0<VAR>g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>a : α<GOAL>Measurable (Function.uncurry fun a x => ↑(f a x) * g a x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : α → β → ℝ≥0<VAR>g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>a : α<GOAL>(κ a).withDensity ((fun x => ↑(f a x)) * fun x => g a x) = ((κ.withDensity fun a x => ↑(f a x)).withDensity g) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : α → β → ℝ≥0<VAR>g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>a : α<GOAL>(((κ a).withDensity fun x => ↑(f a x)).withDensity fun x => g a x) = ((κ.withDensity fun a x => ↑(f a x)).withDensity g) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : α → β → ℝ≥0<VAR>g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>a : α<GOAL>Measurable fun x => ↑(f a x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : α → β → ℝ≥0<VAR>g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>a : α<GOAL>Measurable fun x => g a x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁹ : Category.{?u.91944, u_1} C<VAR>inst✝⁸ : Category.{?u.91948, u_2} D<VAR>inst✝⁷ : Category.{?u.91952, u_3} E<VAR>inst✝⁶ : Category.{?u.91956, u_4} E'<VAR>A : Type u_5<VAR>inst✝⁵ : AddMonoid A<VAR>inst✝⁴ : HasShift D A<VAR>inst✝³ : HasShift E A<VAR>inst✝² : HasShift E' A<VAR>F G✝ H : SingleFunctors C D A<VAR>G : D ⥤ E<VAR>G' : E ⥤ E'<VAR>inst✝¹ : G.CommShift A<VAR>inst✝ : G'.CommShift A<VAR>n a a' : A<VAR>ha' : n + a = a'<VAR>X : C<GOAL>((((F.postcomp G).postcomp G').shiftIso n a a' ha').hom ≫ ((fun a => (F.functor a).associator G G') a).hom).app X = (whiskerRight ((fun a => (F.functor a).associator G G') a').hom (shiftFunctor E' n) ≫ ((F.postcomp (G ⋙ G')).shiftIso n a a' ha').hom).app X
<VAR>x✝ y z : ℝ<VAR>n : ℕ<VAR>x : ℝ<GOAL>x ^ 2 = x ^ 2
<VAR>x✝ y z : ℝ<VAR>n : ℕ<VAR>x : ℝ<GOAL>x ^ 2 = x ^ ↑2
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{?u.2006, u_1} C<VAR>inst✝⁶ : Category.{?u.2010, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>p q : ℤ<VAR>hpq : p + -1 = q<GOAL>p = q + 1
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.2010, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>p q : ℤ<VAR>hpq : p + -1 = q<GOAL>(inl φ).v p q hpq ≫ (triangle φ).mor₃.f q = -(K.shiftFunctorObjXIso 1 q p ⋯).inv
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>A✝ : Type u_2<VAR>inst✝² : AddGroup A✝<VAR>N : Type u_3<VAR>inst✝¹ : Group N<VAR>A : Type u_4<VAR>inst✝ : AddGroupWithOne A<VAR>a : A<GOAL>a ∈ (castAddHom A).range ↔ a ∈ AddSubgroup.zmultiples 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁸ : Monoid γ✝<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : AddCommMonoid α<VAR>inst✝⁵ : DistribMulAction γ✝ α<VAR>inst✝⁴ : ContinuousConstSMul γ✝ α<VAR>f : β → α<VAR>γ : Type u_5<VAR>inst✝³ : Group γ<VAR>inst✝² : DistribMulAction γ α<VAR>inst✝¹ : ContinuousConstSMul γ α<VAR>inst✝ : T2Space α<VAR>g : γ<VAR>hf : ¬Summable f<GOAL>∑' (i : β), g • f i = g • ∑' (i : β), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁸ : Monoid γ✝<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : AddCommMonoid α<VAR>inst✝⁵ : DistribMulAction γ✝ α<VAR>inst✝⁴ : ContinuousConstSMul γ✝ α<VAR>f : β → α<VAR>γ : Type u_5<VAR>inst✝³ : Group γ<VAR>inst✝² : DistribMulAction γ α<VAR>inst✝¹ : ContinuousConstSMul γ α<VAR>inst✝ : T2Space α<VAR>g : γ<VAR>hf : ¬Summable f<GOAL>∑' (i : β), g • f i = g • 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁸ : Monoid γ✝<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : AddCommMonoid α<VAR>inst✝⁵ : DistribMulAction γ✝ α<VAR>inst✝⁴ : ContinuousConstSMul γ✝ α<VAR>f : β → α<VAR>γ : Type u_5<VAR>inst✝³ : Group γ<VAR>inst✝² : DistribMulAction γ α<VAR>inst✝¹ : ContinuousConstSMul γ α<VAR>inst✝ : T2Space α<VAR>g : γ<VAR>hf : ¬Summable f<GOAL>∑' (i : β), g • f i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁸ : Monoid γ✝<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : AddCommMonoid α<VAR>inst✝⁵ : DistribMulAction γ✝ α<VAR>inst✝⁴ : ContinuousConstSMul γ✝ α<VAR>f : β → α<VAR>γ : Type u_5<VAR>inst✝³ : Group γ<VAR>inst✝² : DistribMulAction γ α<VAR>inst✝¹ : ContinuousConstSMul γ α<VAR>inst✝ : T2Space α<VAR>g : γ<VAR>hf : ¬Summable f<VAR>mul_g : α ≃+ α := DistribMulAction.toAddEquiv α g<GOAL>∑' (i : β), g • f i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁸ : Monoid γ✝<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : AddCommMonoid α<VAR>inst✝⁵ : DistribMulAction γ✝ α<VAR>inst✝⁴ : ContinuousConstSMul γ✝ α<VAR>f : β → α<VAR>γ : Type u_5<VAR>inst✝³ : Group γ<VAR>inst✝² : DistribMulAction γ α<VAR>inst✝¹ : ContinuousConstSMul γ α<VAR>inst✝ : T2Space α<VAR>g : γ<VAR>hf : ¬Summable f<VAR>mul_g : α ≃+ α := DistribMulAction.toAddEquiv α g<GOAL>¬Summable fun b => g • f b