ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : Type u_1<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>M : Matrix n n (ZMod p)<VAR>h : (M ^ Fintype.card (ZMod p)).charpoly = M.charpoly<GOAL>(M ^ p).charpoly = M.charpoly
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ : Box ι<VAR>i✝ : ι<VAR>x✝ : ℝ<VAR>y : ι → ℝ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>Disjoint (I.splitLower i x) (I.splitUpper i x)
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ : Box ι<VAR>i✝ : ι<VAR>x✝ : ℝ<VAR>y : ι → ℝ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>Disjoint (↑I ∩ {y | y i ≤ x}) (↑I ∩ {y | x < y i})
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ : Box ι<VAR>i✝ : ι<VAR>x✝ : ℝ<VAR>y : ι → ℝ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>Disjoint {y | y i ≤ x} {y | x < y i}
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ : Box ι<VAR>i✝ : ι<VAR>x✝ : ℝ<VAR>y : ι → ℝ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>∀ ⦃a : ι → ℝ⦄, a ∈ {y | y i ≤ x} → a ∉ {y | x < y i}
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R C : ℝ<VAR>hR : 0 < R<VAR>hc : ContinuousOn f (sphere c R)<VAR>hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C<VAR>hlt : ∃ z ∈ sphere c R, ‖f z‖ < C<GOAL>‖∮ (z : ℂ) in C(c, R), f z‖ < 2 * π * R * C
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R C : ℝ<VAR>hR : 0 < R<VAR>hc : ContinuousOn f (sphere c R)<VAR>hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C<VAR>hlt : ∃ z ∈ circleMap c R '' Ioc 0 (2 * π), ‖f z‖ < C<GOAL>‖∮ (z : ℂ) in C(c, R), f z‖ < 2 * π * R * C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>s✝ t : Set α<VAR>s : Set β<VAR>h : Disjoint s (range f)<GOAL>f ⁻¹' s = ∅
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝¹ : Monoid α<VAR>inst✝ : HasDistribNeg α<VAR>a✝ b a : α<VAR>u : αˣ<GOAL>-(a /ₚ u) = -a /ₚ u
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : AffineSpace V1 P1<VAR>inst✝⁹ : AddCommGroup V2<VAR>inst✝⁸ : AffineSpace V2 P2<VAR>inst✝⁷ : AddCommGroup V3<VAR>inst✝⁶ : AffineSpace V3 P3<VAR>inst✝⁵ : Module k V1<VAR>inst✝⁴ : Module k V2<VAR>inst✝³ : Module k V3<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Module R V2<VAR>inst✝ : SMulCommClass k R V2<VAR>f : V1 →ᵃ[k] V2<VAR>p✝ : V1<GOAL>((fun p => p.2.toAffineMap + const k V1 p.1) ({ toFun := fun f => (f 0, f.linear), map_add' := ⋯, map_smul' := ⋯ }.toFun f)) p✝ = f p✝
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : AffineSpace V1 P1<VAR>inst✝⁹ : AddCommGroup V2<VAR>inst✝⁸ : AffineSpace V2 P2<VAR>inst✝⁷ : AddCommGroup V3<VAR>inst✝⁶ : AffineSpace V3 P3<VAR>inst✝⁵ : Module k V1<VAR>inst✝⁴ : Module k V2<VAR>inst✝³ : Module k V3<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Module R V2<VAR>inst✝ : SMulCommClass k R V2<VAR>f : V1 →ᵃ[k] V2<VAR>p✝ : V1<GOAL>((fun p => p.2.toAffineMap + const k V1 p.1) ({ toFun := fun f => (f 0, f.linear), map_add' := ⋯, map_smul' := ⋯ }.toFun f)) p✝ = (⇑f.linear + fun x => f 0) p✝
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : AffineSpace V1 P1<VAR>inst✝⁹ : AddCommGroup V2<VAR>inst✝⁸ : AffineSpace V2 P2<VAR>inst✝⁷ : AddCommGroup V3<VAR>inst✝⁶ : AffineSpace V3 P3<VAR>inst✝⁵ : Module k V1<VAR>inst✝⁴ : Module k V2<VAR>inst✝³ : Module k V3<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Module R V2<VAR>inst✝ : SMulCommClass k R V2<VAR>v : V2<VAR>f : V1 →ₗ[k] V2<GOAL>{ toFun := fun f => (f 0, f.linear), map_add' := ⋯, map_smul' := ⋯ }.toFun ((fun p => p.2.toAffineMap + const k V1 p.1) (v, f)) = (v, f)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasInitial C<VAR>X : C<VAR>f : X ⟶ ⊥_ C<GOAL>f = default
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c✝ : α<VAR>n : ℤ<VAR>c : α<GOAL>toIcoMod hp c a = toIcoMod hp c b ↔ a ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq α<VAR>f : α →₀ ℕ<GOAL>(toMultiset f).toFinset = f.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq α<VAR>f : α →₀ ℕ<GOAL>(toMultiset 0).toFinset = support 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq α<VAR>f : α →₀ ℕ<GOAL>∀ (a : α) (b : ℕ) (f : α →₀ ℕ), a ∉ f.support → b ≠ 0 → (toMultiset f).toFinset = f.support → (toMultiset (single a b + f)).toFinset = (single a b + f).support
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>p q r✝ : R[X]<VAR>r : R<GOAL>(C ((algebraMap R A) r)).toFinsupp = (algebraMap R (AddMonoidAlgebra A ℕ)) r
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>p q r✝ : R[X]<VAR>r : R<GOAL>AddMonoidAlgebra.single 0 ((algebraMap R A) r) = (algebraMap R (AddMonoidAlgebra A ℕ)) r
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_2<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : α → ℝ<VAR>hint : Integrable g μ<VAR>ℱ : ι → MeasurableSpace α<VAR>hℱ : ∀ (i : ι), ℱ i ≤ m0<VAR>A : MeasurableSpace α := m0<GOAL>UniformIntegrable (fun i => μ[g|ℱ i]) 1 μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_2<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : α → ℝ<VAR>hint : Integrable g μ<VAR>ℱ : ι → MeasurableSpace α<VAR>hℱ : ∀ (i : ι), ℱ i ≤ m0<VAR>A : MeasurableSpace α := m0<VAR>hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}<GOAL>UniformIntegrable (fun i => μ[g|ℱ i]) 1 μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_2<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : α → ℝ<VAR>hint : Integrable g μ<VAR>ℱ : ι → MeasurableSpace α<VAR>hℱ : ∀ (i : ι), ℱ i ≤ m0<VAR>A : MeasurableSpace α := m0<VAR>hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}<VAR>hg : Memℒp g 1 μ<GOAL>UniformIntegrable (fun i => μ[g|ℱ i]) 1 μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_2<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : α → ℝ<VAR>hint : Integrable g μ<VAR>ℱ : ι → MeasurableSpace α<VAR>hℱ : ∀ (i : ι), ℱ i ≤ m0<VAR>A : MeasurableSpace α := m0<VAR>hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}<VAR>hg : Memℒp g 1 μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖(μ[g|ℱ i]) x‖₊}.indicator (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_2<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : α → ℝ<VAR>hint : Integrable g μ<VAR>ℱ : ι → MeasurableSpace α<VAR>hℱ : ∀ (i : ι), ℱ i ≤ m0<VAR>A : MeasurableSpace α := m0<VAR>hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}<VAR>hg : Memℒp g 1 μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hne : ¬eLpNorm g 1 μ = 0<GOAL>∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖(μ[g|ℱ i]) x‖₊}.indicator (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_2<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : α → ℝ<VAR>hint : Integrable g μ<VAR>ℱ : ι → MeasurableSpace α<VAR>hℱ : ∀ (i : ι), ℱ i ≤ m0<VAR>A : MeasurableSpace α := m0<VAR>hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}<VAR>hg : Memℒp g 1 μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hne : ¬eLpNorm g 1 μ = 0<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε<GOAL>∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖(μ[g|ℱ i]) x‖₊}.indicator (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_2<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : α → ℝ<VAR>hint : Integrable g μ<VAR>ℱ : ι → MeasurableSpace α<VAR>hℱ : ∀ (i : ι), ℱ i ≤ m0<VAR>A : MeasurableSpace α := m0<VAR>hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}<VAR>hg : Memℒp g 1 μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hne : ¬eLpNorm g 1 μ = 0<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε<VAR>C : ℝ≥0 := ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal<VAR>hC : C = ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal<GOAL>∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖(μ[g|ℱ i]) x‖₊}.indicator (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_2<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : α → ℝ<VAR>hint : Integrable g μ<VAR>ℱ : ι → MeasurableSpace α<VAR>hℱ : ∀ (i : ι), ℱ i ≤ m0<VAR>A : MeasurableSpace α := m0<VAR>hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}<VAR>hg : Memℒp g 1 μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hne : ¬eLpNorm g 1 μ = 0<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε<VAR>C : ℝ≥0 := ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal<VAR>hC : C = ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal<VAR>hCpos : 0 < C<GOAL>∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖(μ[g|ℱ i]) x‖₊}.indicator (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_2<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : α → ℝ<VAR>hint : Integrable g μ<VAR>ℱ : ι → MeasurableSpace α<VAR>hℱ : ∀ (i : ι), ℱ i ≤ m0<VAR>A : MeasurableSpace α := m0<VAR>hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}<VAR>hg : Memℒp g 1 μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hne : ¬eLpNorm g 1 μ = 0<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε<VAR>C : ℝ≥0 := ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal<VAR>hC : C = ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal<VAR>hCpos : 0 < C<VAR>this : ∀ (n : ι), μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ<GOAL>∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖(μ[g|ℱ i]) x‖₊}.indicator (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_2<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : α → ℝ<VAR>hint : Integrable g μ<VAR>ℱ : ι → MeasurableSpace α<VAR>hℱ : ∀ (i : ι), ℱ i ≤ m0<VAR>A : MeasurableSpace α := m0<VAR>hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}<VAR>hg : Memℒp g 1 μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hne : ¬eLpNorm g 1 μ = 0<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε<VAR>C : ℝ≥0 := ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal<VAR>hC : C = ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal<VAR>hCpos : 0 < C<VAR>this : ∀ (n : ι), μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ<VAR>n : ι<GOAL>eLpNorm ({x | C ≤ ‖(μ[g|ℱ n]) x‖₊}.indicator (μ[g|ℱ n])) 1 μ ≤ eLpNorm ({x | C ≤ ‖(μ[g|ℱ n]) x‖₊}.indicator g) 1 μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_2<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : α → ℝ<VAR>hint : Integrable g μ<VAR>ℱ : ι → MeasurableSpace α<VAR>hℱ : ∀ (i : ι), ℱ i ≤ m0<VAR>A : MeasurableSpace α := m0<VAR>hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}<VAR>hg : Memℒp g 1 μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hne : ¬eLpNorm g 1 μ = 0<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε<VAR>C : ℝ≥0 := ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal<VAR>hC : C = ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal<VAR>hCpos : 0 < C<VAR>this : ∀ (n : ι), μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ<VAR>n : ι<VAR>hmeasℱ : MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}<GOAL>eLpNorm ({x | C ≤ ‖(μ[g|ℱ n]) x‖₊}.indicator (μ[g|ℱ n])) 1 μ ≤ eLpNorm ({x | C ≤ ‖(μ[g|ℱ n]) x‖₊}.indicator g) 1 μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_2<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : α → ℝ<VAR>hint : Integrable g μ<VAR>ℱ : ι → MeasurableSpace α<VAR>hℱ : ∀ (i : ι), ℱ i ≤ m0<VAR>A : MeasurableSpace α := m0<VAR>hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}<VAR>hg : Memℒp g 1 μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hne : ¬eLpNorm g 1 μ = 0<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε<VAR>C : ℝ≥0 := ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal<VAR>hC : C = ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal<VAR>hCpos : 0 < C<VAR>this : ∀ (n : ι), μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ<VAR>n : ι<VAR>hmeasℱ : MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}<GOAL>eLpNorm (μ[{x | C ≤ ‖(μ[g|ℱ n]) x‖₊}.indicator g|ℱ n]) 1 μ ≤ eLpNorm ({x | C ≤ ‖(μ[g|ℱ n]) x‖₊}.indicator g) 1 μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : AntivaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i • g i ≤ ∑ i ∈ s, f (σ i) • g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : AntivaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f (σ i) • g i = ∑ i ∈ s, f i • g (σ⁻¹ i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra R B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Nontrivial B<VAR>x : A<VAR>p : R[X]<GOAL>(aeval ((algebraMap A B) x)) p = 0 ↔ (aeval x) p = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s t : Finset α<VAR>inst✝ : DecidableEq α<VAR>a : α<GOAL>a ∉ sᶜ ↔ a ∈ s
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v w : V<VAR>e : Sym2 V<VAR>G₁ G₂ : SimpleGraph V<VAR>x✝ : Sym2 V<VAR>x y : V<GOAL>Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ ⊔ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet ∪ G₂.edgeSet
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖y‖ / (o.oangle x (x + y)).tan = ‖x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle x (x + y)).sign = 1<GOAL>‖y‖ / (o.oangle x (x + y)).tan = ‖x‖
<VAR>α : Type u<VAR>x : FreeRing α<GOAL>↑(-x) = -↑x
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle x (x + y) = ↑(Real.arcsin (‖y‖ / ‖x + y‖))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle x (x + y)).sign = 1<GOAL>o.oangle x (x + y) = ↑(Real.arcsin (‖y‖ / ‖x + y‖))
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F : PrelaxFunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>F.map₂ (eqToHom ⋯) = eqToHom ⋯
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>limsup f (ae (μ.trim hm)) = limsup f (ae μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>sInf {a | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} = sInf {a | ∀ᵐ (n : α) ∂μ, f n ≤ a}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : ℝ≥0∞<GOAL>a ∈ {a | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} ↔ a ∈ {a | ∀ᵐ (n : α) ∂μ, f n ≤ a}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : ℝ≥0∞<GOAL>μ {x | ¬f x ≤ a} = (μ.trim hm) {x | ¬f x ≤ a}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : ℝ≥0∞<GOAL>MeasurableSet {x | ¬f x ≤ a}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : ℝ≥0∞<GOAL>Measurable fun x => a
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>x : (n : ℕ) → E n<VAR>n : ℕ<GOAL>IsOpen (cylinder x n)
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>x : (n : ℕ) → E n<VAR>n : ℕ<GOAL>IsOpen ((↑(Finset.range n)).pi fun i => {x i})
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁴ : Semiring α<VAR>inst✝³ : Preorder α<VAR>a b c d : α<VAR>inst✝² : ZeroLEOneClass α<VAR>inst✝¹ : MulPosMono α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a2 : 2 ≤ a<VAR>b0 : 0 ≤ b<GOAL>a + (a + a * b) ≤ a * (2 + b)
<VAR>l : List ℕ<VAR>h : ∀ p ∈ l, Nat.Prime p<GOAL>↑(ofNatList l h).prod = l.prod
<VAR>l : List ℕ<VAR>h : ∀ p ∈ l, Nat.Prime p<VAR>this : ↑(ofNatMultiset (↑l) h).prod = (↑l).prod<GOAL>↑(ofNatList l h).prod = l.prod
<VAR>l : List ℕ<VAR>h : ∀ p ∈ l, Nat.Prime p<VAR>this : ↑(ofNatMultiset (↑l) h).prod = l.prod<GOAL>↑(ofNatList l h).prod = l.prod
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : Group H<VAR>inst✝⁸ : MulAction G α<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MulAction H β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>s t✝ : Set α<VAR>μ : Measure α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : MeasurableSMul G α<VAR>inst✝¹ : SMulInvariantMeasure G α μ<VAR>inst✝ : Countable G<VAR>ν : Measure α<VAR>h : IsFundamentalDomain G s μ<VAR>f : α → ℝ≥0∞<VAR>t : Set α<GOAL>∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂μ.restrict t = ∑' (g : G), ∫⁻ (x : α) in t ∩ g • s, f x ∂μ
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfg : f ≈ g<GOAL>padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfg : f ≈ g<VAR>h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfg : f ≈ g<VAR>h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))<VAR>hlt : padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfg : f ≈ g<VAR>h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))<VAR>hnlt : ¬padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ x y : List α<GOAL>y = x ++ y ↔ x = []
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<GOAL>(homologyMap' φ S₁.homologyData S₂.homologyData).op = (S₂.op.leftHomologyIso.symm ≪≫ S₂.leftHomologyOpIso ≪≫ S₂.rightHomologyIso.symm.op).inv ≫ homologyMap' (opMap φ) S₂.op.homologyData S₁.op.homologyData ≫ (S₁.op.leftHomologyIso.symm ≪≫ S₁.leftHomologyOpIso ≪≫ S₁.rightHomologyIso.symm.op).hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<GOAL>S₂.homologyData.iso.inv.op ≫ homologyMap' (opMap φ) S₂.homologyData.op S₁.homologyData.op ≫ S₁.homologyData.iso.hom.op = (S₂.op.leftHomologyIso.symm ≪≫ S₂.leftHomologyOpIso ≪≫ S₂.rightHomologyIso.symm.op).inv ≫ homologyMap' (opMap φ) S₂.op.homologyData S₁.op.homologyData ≫ (S₁.op.leftHomologyIso.symm ≪≫ S₁.leftHomologyOpIso ≪≫ S₁.rightHomologyIso.symm.op).hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<GOAL>S₂.homologyData.iso.inv.op ≫ leftHomologyMap' (opMap φ) S₂.homologyData.op.left S₁.homologyData.op.left ≫ S₁.homologyData.iso.hom.op = (((rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData S₂.homologyData.right ≫ S₂.homologyData.iso.inv).op ≫ leftHomologyMap' (𝟙 S₂.op) S₂.rightHomologyData.op S₂.op.leftHomologyData) ≫ leftHomologyMap' (𝟙 S₂.op) S₂.op.leftHomologyData S₂.op.homologyData.left) ≫ leftHomologyMap' (opMap φ) S₂.op.homologyData.left S₁.op.homologyData.left ≫ leftHomologyMap' (𝟙 S₁.op) S₁.op.homologyData.left S₁.op.leftHomologyData ≫ leftHomologyMap' (𝟙 S₁.op) S₁.op.leftHomologyData S₁.rightHomologyData.op ≫ (S₁.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₁) S₁.homologyData.right S₁.rightHomologyData).op
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hc : c < 0<GOAL>a ≤ b / c ↔ b ≤ c * a
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε<VAR>ε : ℝ≥0∞<VAR>ε0 : ε > 0<GOAL>∃ t, t.Countable ∧ ⋃ x ∈ t, EMetric.closedBall x ε = univ
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε<VAR>ε : ℝ≥0∞<VAR>ε0 : ε > 0<VAR>ε' : ℝ≥0<VAR>ε'0 : 0 < ↑ε'<VAR>ε'ε : ↑ε' < ε<GOAL>∃ t, t.Countable ∧ ⋃ x ∈ t, EMetric.closedBall x ε = univ
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε<VAR>ε : ℝ≥0∞<VAR>ε0 : ε > 0<VAR>ε' : ℝ≥0<VAR>ε'0 : 0 < ↑ε'<VAR>ε'ε : ↑ε' < ε<VAR>s : Set α<VAR>hsc : s.Countable<VAR>y : α → α<VAR>hys : ∀ (x : α), y x ∈ s<VAR>hyx : ∀ (x : α), dist x (y x) ≤ ↑ε'<GOAL>∃ t, t.Countable ∧ ⋃ x ∈ t, EMetric.closedBall x ε = univ
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε<VAR>ε : ℝ≥0∞<VAR>ε0 : ε > 0<VAR>ε' : ℝ≥0<VAR>ε'0 : 0 < ↑ε'<VAR>ε'ε : ↑ε' < ε<VAR>s : Set α<VAR>hsc : s.Countable<VAR>y : α → α<VAR>hys : ∀ (x : α), y x ∈ s<VAR>hyx : ∀ (x : α), dist x (y x) ≤ ↑ε'<VAR>x : α<GOAL>edist x (y x) ≤ ↑ε'
<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>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>x : γ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable ((fun p => κ.density ν p.1 p.2 s) ∘ fun a => (a, x))