ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>γ : Type u_5<VAR>f g : α → γ<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs_zero : μ s = 0<VAR>h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}<GOAL>{x | (fun x => (fun x => if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>γ : Type u_5<VAR>f g : α → γ<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs_zero : μ s = 0<VAR>h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}<GOAL>{x | (fun x => (fun x => if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ sᶜᶜ
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I✝ : Ideal R<VAR>F F' : I✝.Filtration M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>i : ℕ<GOAL>I ^ (i + 1) • N ≤ I ^ i • N
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I✝ : Ideal R<VAR>F F' : I✝.Filtration M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>i : ℕ<GOAL>I ^ 1 • I ^ i • N ≤ I ^ i • N
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I✝ : Ideal R<VAR>F F' : I✝.Filtration M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>i : ℕ<GOAL>I • I ^ i • N ≤ I ^ (i + 1) • N
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : CommRing k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : PerfectRing k p<VAR>a : 𝕎 k<VAR>ha : a ≠ 0<GOAL>∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : CommRing k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : PerfectRing k p<VAR>a : 𝕎 k<VAR>ha : a ≠ 0<VAR>m : ℕ<VAR>c : 𝕎 k<VAR>hc : c.coeff 0 ≠ 0<VAR>hcm : a = (⇑verschiebung)^[m] c<GOAL>∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : CommRing k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : PerfectRing k p<VAR>a : 𝕎 k<VAR>ha : a ≠ 0<VAR>m : ℕ<VAR>b : 𝕎 k<VAR>hc : ((⇑frobenius)^[m] b).coeff 0 ≠ 0<VAR>hcm : a = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)<GOAL>∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : CommRing k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : PerfectRing k p<VAR>a : 𝕎 k<VAR>ha : a ≠ 0<VAR>m : ℕ<VAR>b : 𝕎 k<VAR>hc : b.coeff 0 ^ p ^ m ≠ 0<VAR>hcm : a = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)<GOAL>∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : CommRing k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : PerfectRing k p<VAR>a : 𝕎 k<VAR>ha : a ≠ 0<VAR>m : ℕ<VAR>b : 𝕎 k<VAR>hc : b.coeff 0 ^ p ^ m ≠ 0<VAR>hcm : a = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)<VAR>this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = ((⇑verschiebung)^[m] ∘ (⇑frobenius)^[m]) b<GOAL>∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : CommRing k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : PerfectRing k p<VAR>a : 𝕎 k<VAR>ha : a ≠ 0<VAR>m : ℕ<VAR>b : 𝕎 k<VAR>hc : b.coeff 0 ^ p ^ m ≠ 0<VAR>hcm : a = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)<VAR>this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)<GOAL>∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>ν : ProbabilityMeasure Ω<VAR>s : Set Ω<GOAL>↑(ν s) = ↑ν s
<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✝¹ : MeasurableSpace α<VAR>ι : Type u_5<VAR>inst✝ : Countable ι<VAR>f : ι → α → ℝ≥0∞<VAR>h : ∀ (i : ι), Measurable (f i)<GOAL>Measurable fun x => ∑' (i : ι), f i x
<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✝¹ : MeasurableSpace α<VAR>ι : Type u_5<VAR>inst✝ : Countable ι<VAR>f : ι → α → ℝ≥0∞<VAR>h : ∀ (i : ι), Measurable (f i)<GOAL>Measurable fun x => ⨆ s, ∑ i ∈ s, f i x
<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✝¹ : MeasurableSpace α<VAR>ι : Type u_5<VAR>inst✝ : Countable ι<VAR>f : ι → α → ℝ≥0∞<VAR>h : ∀ (i : ι), Measurable (f i)<GOAL>∀ (i : Finset ι), Measurable fun b => ∑ i ∈ i, f i b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.98000, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f g : W.LeftFraction X Y<GOAL>f.map (Q W) ⋯ = g.map (Q W) ⋯ ↔ LeftFractionRel f g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.98000, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f g : W.LeftFraction X Y<GOAL>(Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯ ↔ LeftFractionRel f g
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝ : GroupWithZero G₀<VAR>f g : ι → G₀<GOAL>(support fun a => f a / g a) = support f ∩ support g
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<GOAL>(shortComplexH0 A).Exact
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<GOAL>∀ (x₂ : ↑(shortComplexH0 A).X₂), (shortComplexH0 A).g x₂ = 0 → ∃ x₁, (shortComplexH0 A).f x₁ = x₂
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x : CoeSort.coe A<VAR>hx : (dZero A) x = 0<VAR>g : G<GOAL>(A.ρ g) x = x
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x : CoeSort.coe A<VAR>hx : (dZero A) x = 0<VAR>g : G<GOAL>(A.ρ g) x - x = 0
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M<VAR>b : Basis ι R M<VAR>f : M ≃ₗ[R] M'<VAR>v : ι → M'<GOAL>(b.map f).det v = b.det (⇑f.symm ∘ v)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>ι : Type u_2<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>s : Set β<GOAL>TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>ι : Type u_2<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>s : Set β<VAR>H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε<VAR>u : Set (α × α)<VAR>hu : u ∈ 𝓤 α<GOAL>∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>ι : Type u_2<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>s : Set β<VAR>H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε<VAR>u : Set (α × α)<VAR>hu : u ∈ 𝓤 α<VAR>ε : ℝ≥0∞<VAR>εpos : ε > 0<VAR>hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u<GOAL>∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>p : α → Prop<VAR>f g : α → β<VAR>inst✝ : (a : α) → Decidable (p a)<VAR>hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))<VAR>hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))<VAR>hf : ContinuousOn f {x | p x}<VAR>hg : ContinuousOn g {x | ¬p x}<GOAL>Continuous fun a => if p a then f a else g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>p : α → Prop<VAR>f g : α → β<VAR>inst✝ : (a : α) → Decidable (p a)<VAR>hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))<VAR>hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))<VAR>hf : ContinuousOn f {x | p x}<VAR>hg : ContinuousOn g {x | ¬p x}<GOAL>ContinuousOn (fun a => if p a then f a else g a) univ
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<GOAL>DifferentiableAt 𝕜 f y ↔ ∀ (i : ι), DifferentiableAt 𝕜 (fun x => f x i) y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<GOAL>(∀ (i : ι), DifferentiableAt 𝕜 (fun x => (⇑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) y) ↔ ∀ (i : ι), DifferentiableAt 𝕜 (fun x => f x i) y
<GOAL>ContinuousOn tan (Ioo (-(π / 2)) (π / 2))
<VAR>x : ℝ<GOAL>x ∈ Ioo (-(π / 2)) (π / 2) → x ∈ {x | cos x ≠ 0}
<VAR>x : ℝ<GOAL>-(π / 2) < x → x < π / 2 → ¬cos x = 0
<VAR>x : ℝ<GOAL>-(π / 2) < x → x < π / 2 → ¬∃ k, x = (2 * ↑k + 1) * π / 2
<VAR>x : ℝ<VAR>hx_gt : -(π / 2) < x<VAR>hx_lt : x < π / 2<VAR>r : ℤ<VAR>hxr_eq : x = (2 * ↑r + 1) * π / 2<GOAL>False
<VAR>x : ℝ<VAR>hx_gt : -(π / 2) < x<VAR>hx_lt : x < π / 2<VAR>r : ℤ<VAR>hxr_eq : x = (2 * ↑r + 1) * π / 2<VAR>h : 0 ≤ r<GOAL>False
<VAR>x : ℝ<VAR>hx_gt : -(π / 2) < x<VAR>hx_lt : x < π / 2<VAR>r : ℤ<VAR>hxr_eq : x = (2 * ↑r + 1) * π / 2<VAR>h : r < 0<GOAL>False
<VAR>y : ℝ<GOAL>0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤
<VAR>y : ℝ<VAR>H : 0 < y<GOAL>0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤
<GOAL>0 ^ 0 = if 0 < 0 then 0 else if 0 = 0 then 1 else ⊤
<VAR>y : ℝ<VAR>H : y < 0<GOAL>0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f : α → ℝ≥0∞<GOAL>∃ g, Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f g : α → ℝ≥0∞<VAR>hgm : Measurable g<VAR>hgf : g ≤ f<VAR>hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ<GOAL>∃ g, Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f g : α → ℝ≥0∞<VAR>hgm : Measurable g<VAR>hgf : g ≤ f<VAR>hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ<GOAL>μ.withDensity g = μ.withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f g : α → ℝ≥0∞<VAR>hgm : Measurable g<VAR>hgf : g ≤ f<VAR>hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.withDensity g) s = (μ.withDensity f) s
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z w : K<GOAL>re (z / w) = re z * re w / normSq w + im z * im w / normSq w
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>n : ℕ<GOAL>schnirelmannDensity A * ↑n ≤ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<GOAL>schnirelmannDensity A * ↑0 ≤ ↑(filter (fun x => x ∈ A) (Ioc 0 0)).card
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>schnirelmannDensity A * ↑n ≤ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>Lagrange.basis {i, j} v i = basisDivisor (v i) (v j)
<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✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<GOAL>p.closedBall 0 r = ⇑p ⁻¹' Metric.closedBall 0 r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : CompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : CompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : Nonempty γ<VAR>ι : Sort u_4<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iSup g)<VAR>Mf : Monotone f<VAR>fbot : f ⊥ = ⊥<GOAL>f (⨆ i, g i) = ⨆ i, f (g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : CompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : CompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : Nonempty γ<VAR>ι : Sort u_4<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iSup g)<VAR>Mf : Monotone f<VAR>fbot : f ⊥ = ⊥<GOAL>sSup (range (f ∘ g)) = sSup (range fun i => f (g i))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M : Mon_ C<VAR>Z : C<VAR>f : Z ⟶ M.X<GOAL>(M.one ⊗ f) ≫ M.mul = (λ_ Z).hom ≫ f
<VAR>R : Type u<VAR>S : Type u_1<VAR>A : Type v<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>x : S<VAR>inst✝ : Invertible x<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>hp' : (aeval x) p = 0<GOAL>(aeval ⅟x) p.reverse = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : 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<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x✝ : M<VAR>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<VAR>x : M<GOAL>(b.reindex e).sumCoords x = b.sumCoords x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : 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<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x✝ : M<VAR>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<VAR>x : M<GOAL>((Finsupp.mapDomain (⇑e) (b.repr x)).sum fun x => id) = (b.repr x).sum fun x => id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f p μ<VAR>hmeas : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ M, 0 < M ∧ eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f p μ<VAR>hmeas : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>M : ℝ<VAR>hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε<GOAL>∃ M, 0 < M ∧ eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f p μ<VAR>hmeas : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>M : ℝ<VAR>hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε<VAR>x : α<GOAL>‖{x | max M 1 ≤ ↑‖f x‖₊}.indicator f x‖ ≤ ‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f p μ<VAR>hmeas : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>M : ℝ<VAR>hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε<VAR>x : α<GOAL>{x | max M 1 ≤ ↑‖f x‖₊}.indicator (fun a => ‖f a‖) x ≤ {x | M ≤ ↑‖f x‖₊}.indicator (fun a => ‖f a‖) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f p μ<VAR>hmeas : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>M : ℝ<VAR>hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε<VAR>x✝ x : α<VAR>hx : x ∈ {x | max M 1 ≤ ↑‖f x‖₊}<GOAL>x ∈ {x | M ≤ ↑‖f x‖₊}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f p μ<VAR>hmeas : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>M : ℝ<VAR>hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε<VAR>x✝ x : α<VAR>hx : max M 1 ≤ ↑‖f x‖₊<GOAL>x ∈ {x | M ≤ ↑‖f x‖₊}
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : Semiring R₃<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : AddCommMonoid M₃<VAR>module_M : Module R M<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>re₂₃ : RingHomInvPair σ₂₃ σ₃₂<VAR>re₃₂ : RingHomInvPair σ₃₂ σ₂₃<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₁] M<VAR>e✝ : M ≃ₛₗ[σ₁₂] M₂<VAR>h : M₂ →ₛₗ[σ₂₃] M₃<VAR>p q : Submodule R M<VAR>inst✝ : Module R₂ M₂<VAR>e : ↥p ≃ₛₗ[σ₁₂] ↥⊥<GOAL>p = ⊥
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : Semiring R₃<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : AddCommMonoid M₃<VAR>module_M : Module R M<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>re₂₃ : RingHomInvPair σ₂₃ σ₃₂<VAR>re₃₂ : RingHomInvPair σ₃₂ σ₂₃<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₁] M<VAR>e✝ : M ≃ₛₗ[σ₁₂] M₂<VAR>h : M₂ →ₛₗ[σ₂₃] M₃<VAR>p q : Submodule R M<VAR>inst✝ : Module R₂ M₂<VAR>e : ↥p ≃ₛₗ[σ₁₂] ↥⊥<VAR>b : M<VAR>hb : b ∈ p<GOAL>b = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : Semiring R₃<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : AddCommMonoid M₃<VAR>module_M : Module R M<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>re₂₃ : RingHomInvPair σ₂₃ σ₃₂<VAR>re₃₂ : RingHomInvPair σ₃₂ σ₂₃<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₁] M<VAR>e✝ : M ≃ₛₗ[σ₁₂] M₂<VAR>h : M₂ →ₛₗ[σ₂₃] M₃<VAR>p q : Submodule R M<VAR>inst✝ : Module R₂ M₂<VAR>e : ↥p ≃ₛₗ[σ₁₂] ↥⊥<VAR>b : M<VAR>hb : b ∈ p<GOAL>e ⟨b, hb⟩ = 0
<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✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<VAR>c : 𝕜<GOAL>lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 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✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<GOAL>lineDeriv 𝕜 f x (0 • v) = 0 • lineDeriv 𝕜 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✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>‖(starRingEnd K) z‖ = ‖z‖
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>h e f : L<VAR>t : IsSl2Triple h e f<GOAL>f ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>h e f : L<VAR>t : IsSl2Triple h e f<VAR>this : h ≠ 0<GOAL>f ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>h e f : L<VAR>t : IsSl2Triple h e f<VAR>this : f = 0<GOAL>h = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring R₂<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>ι : Type u_9<VAR>s : Set ι<VAR>p : ι → Submodule R M<GOAL>⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i) = ⊤
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring R₂<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>ι : Type u_9<VAR>s : Set ι<VAR>p : ι → Submodule R M<VAR>x✝¹ : ↥(⨆ i ∈ s, p i)<VAR>x : M<VAR>hx : x ∈ ⨆ i ∈ s, p i<VAR>x✝ : ⟨x, hx⟩ ∈ ⊤<GOAL>⟨x, hx⟩ ∈ ⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring R₂<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>ι : Type u_9<VAR>s : Set ι<VAR>p : ι → Submodule R M<VAR>x✝¹ : ↥(⨆ i ∈ s, p i)<VAR>x : M<VAR>hx : x ∈ ⨆ i ∈ s, p i<VAR>x✝ : ⟨x, hx⟩ ∈ ⊤<GOAL>x ∈ map (⨆ i ∈ s, p i).subtype (⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i))
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring R₂<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>ι : Type u_9<VAR>s : Set ι<VAR>p : ι → Submodule R M<VAR>x✝¹ : ↥(⨆ i ∈ s, p i)<VAR>x : M<VAR>hx : x ∈ ⨆ i ∈ s, p i<VAR>x✝ : ⟨x, hx⟩ ∈ ⊤<GOAL>∀ i ∈ s, map (⨆ i ∈ s, p i).subtype (comap (⨆ i ∈ s, p i).subtype (p i)) = p i