ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α✝ : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : Div G<VAR>m✝ : MeasurableSpace α<VAR>f✝ g✝ : α → G<VAR>μ : Measure α<VAR>m : MeasurableSpace α<VAR>E : Type u_4<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : AddGroup E<VAR>inst✝¹ : MeasurableSingletonClass E<VAR>inst✝ : MeasurableSub₂ E<VAR>f g : α → E<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>x✝ : α<GOAL>x✝ ∈ {x | f x = g x} ↔ x✝ ∈ {x | (f - g) x = 0}
<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>r : α → α → Prop<VAR>a b c d : α<VAR>hab : ReflTransGen r a b<VAR>hbc : TransGen r b c<GOAL>TransGen r a c
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<GOAL>(∀ (f : ℕ →o (Submodule R M)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m) ↔ IsArtinian R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<GOAL>(∀ (f : ℕ →o (Submodule R M)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m) ↔ WellFounded fun x x_1 => x < x_1
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S T : Set E<GOAL>restrictScalars F (adjoin (↥(adjoin F S)) T) = adjoin F (S ∪ T)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S T : Set E<GOAL>↑(restrictScalars F (adjoin (↥(adjoin F S)) T)) = ↑(adjoin F (S ∪ T))
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S T : Set E<GOAL>↑(adjoin (↥(adjoin F S)) T) = ↑(adjoin F (S ∪ T))
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S T : Set E<GOAL>Set.range ⇑(algebraMap (↥(adjoin F S)) E) ⊆ ↑(adjoin F (S ∪ T))
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S T : Set E<GOAL>T ⊆ ↑(adjoin F (S ∪ T))
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S T : Set E<GOAL>Set.range ⇑(algebraMap F E) ⊆ ↑(adjoin (↥(adjoin F S)) T)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S T : Set E<GOAL>S ∪ T ⊆ ↑(adjoin (↥(adjoin F S)) T)
<VAR>α : Type u_1<VAR>inst1 inst2 : BEq α<VAR>inst✝¹ : LawfulBEq α<VAR>inst✝ : LawfulBEq α<GOAL>inst1 = inst2
<VAR>α : Type u_1<VAR>inst1 inst2 : BEq α<VAR>inst✝¹ : LawfulBEq α<VAR>inst✝ : LawfulBEq α<GOAL>∀ (x y : α), (x == y) = (x == y)
<VAR>α : Type u_1<VAR>inst1 inst2 : BEq α<VAR>inst✝¹ : LawfulBEq α<VAR>inst✝ : LawfulBEq α<VAR>x y : α<GOAL>(x == y) = (x == y)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>hBf : ∃ c < a, ∃ B, f =O[cobounded ℂ ⊓ l] fun z => expR (B * Complex.abs z ^ c)<VAR>hBg : ∃ c < a, ∃ B, g =O[cobounded ℂ ⊓ l] fun z => expR (B * Complex.abs z ^ c)<GOAL>∃ c < a, ∃ B, (f - g) =O[cobounded ℂ ⊓ l] fun z => expR (B * Complex.abs z ^ c)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>hBf : ∃ c < a, ∃ B, f =O[cobounded ℂ ⊓ l] fun z => expR (B * Complex.abs z ^ c)<VAR>hBg : ∃ c < a, ∃ B, g =O[cobounded ℂ ⊓ l] fun z => expR (B * Complex.abs z ^ c)<VAR>this : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z => expR (B₁ * Complex.abs z ^ c₁)) =O[cobounded ℂ ⊓ l] fun z => expR (B₂ * Complex.abs z ^ c₂)<GOAL>∃ c < a, ∃ B, (f - g) =O[cobounded ℂ ⊓ l] fun z => expR (B * Complex.abs z ^ c)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>this : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z => expR (B₁ * Complex.abs z ^ c₁)) =O[cobounded ℂ ⊓ l] fun z => expR (B₂ * Complex.abs z ^ c₂)<VAR>cf : ℝ<VAR>hcf : cf < a<VAR>Bf : ℝ<VAR>hOf : f =O[cobounded ℂ ⊓ l] fun z => expR (Bf * Complex.abs z ^ cf)<VAR>cg : ℝ<VAR>hcg : cg < a<VAR>Bg : ℝ<VAR>hOg : g =O[cobounded ℂ ⊓ l] fun z => expR (Bg * Complex.abs z ^ cg)<GOAL>∃ c < a, ∃ B, (f - g) =O[cobounded ℂ ⊓ l] fun z => expR (B * Complex.abs z ^ c)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>this : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z => expR (B₁ * Complex.abs z ^ c₁)) =O[cobounded ℂ ⊓ l] fun z => expR (B₂ * Complex.abs z ^ c₂)<VAR>cf : ℝ<VAR>hcf : cf < a<VAR>Bf : ℝ<VAR>hOf : f =O[cobounded ℂ ⊓ l] fun z => expR (Bf * Complex.abs z ^ cf)<VAR>cg : ℝ<VAR>hcg : cg < a<VAR>Bg : ℝ<VAR>hOg : g =O[cobounded ℂ ⊓ l] fun z => expR (Bg * Complex.abs z ^ cg)<GOAL>(f - g) =O[cobounded ℂ ⊓ l] fun z => expR (max 0 (max Bf Bg) * Complex.abs z ^ max cf cg)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>this : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z => expR (B₁ * Complex.abs z ^ c₁)) =O[cobounded ℂ ⊓ l] fun z => expR (B₂ * Complex.abs z ^ c₂)<VAR>cf : ℝ<VAR>hcf : cf < a<VAR>Bf : ℝ<VAR>hOf : f =O[cobounded ℂ ⊓ l] fun z => expR (Bf * Complex.abs z ^ cf)<VAR>cg : ℝ<VAR>hcg : cg < a<VAR>Bg : ℝ<VAR>hOg : g =O[cobounded ℂ ⊓ l] fun z => expR (Bg * Complex.abs z ^ cg)<GOAL>cf ≤ max cf cg
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>this : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z => expR (B₁ * Complex.abs z ^ c₁)) =O[cobounded ℂ ⊓ l] fun z => expR (B₂ * Complex.abs z ^ c₂)<VAR>cf : ℝ<VAR>hcf : cf < a<VAR>Bf : ℝ<VAR>hOf : f =O[cobounded ℂ ⊓ l] fun z => expR (Bf * Complex.abs z ^ cf)<VAR>cg : ℝ<VAR>hcg : cg < a<VAR>Bg : ℝ<VAR>hOg : g =O[cobounded ℂ ⊓ l] fun z => expR (Bg * Complex.abs z ^ cg)<GOAL>0 ≤ max 0 (max Bf Bg)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>this : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z => expR (B₁ * Complex.abs z ^ c₁)) =O[cobounded ℂ ⊓ l] fun z => expR (B₂ * Complex.abs z ^ c₂)<VAR>cf : ℝ<VAR>hcf : cf < a<VAR>Bf : ℝ<VAR>hOf : f =O[cobounded ℂ ⊓ l] fun z => expR (Bf * Complex.abs z ^ cf)<VAR>cg : ℝ<VAR>hcg : cg < a<VAR>Bg : ℝ<VAR>hOg : g =O[cobounded ℂ ⊓ l] fun z => expR (Bg * Complex.abs z ^ cg)<GOAL>Bf ≤ max 0 (max Bf Bg)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>this : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z => expR (B₁ * Complex.abs z ^ c₁)) =O[cobounded ℂ ⊓ l] fun z => expR (B₂ * Complex.abs z ^ c₂)<VAR>cf : ℝ<VAR>hcf : cf < a<VAR>Bf : ℝ<VAR>hOf : f =O[cobounded ℂ ⊓ l] fun z => expR (Bf * Complex.abs z ^ cf)<VAR>cg : ℝ<VAR>hcg : cg < a<VAR>Bg : ℝ<VAR>hOg : g =O[cobounded ℂ ⊓ l] fun z => expR (Bg * Complex.abs z ^ cg)<GOAL>cg ≤ max cf cg
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>this : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z => expR (B₁ * Complex.abs z ^ c₁)) =O[cobounded ℂ ⊓ l] fun z => expR (B₂ * Complex.abs z ^ c₂)<VAR>cf : ℝ<VAR>hcf : cf < a<VAR>Bf : ℝ<VAR>hOf : f =O[cobounded ℂ ⊓ l] fun z => expR (Bf * Complex.abs z ^ cf)<VAR>cg : ℝ<VAR>hcg : cg < a<VAR>Bg : ℝ<VAR>hOg : g =O[cobounded ℂ ⊓ l] fun z => expR (Bg * Complex.abs z ^ cg)<GOAL>Bg ≤ max 0 (max Bf Bg)
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a : ℍ[R]<GOAL>a ^ 2 = -↑(normSq a) ↔ a.re = 0
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a : ℍ[R]<GOAL>a ^ 2 = -↑(normSq a) ↔ star a = -a
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<GOAL>0 ^ 2 = -↑(normSq 0) ↔ star 0 = -0
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a : ℍ[R]<VAR>hq0 : a ≠ 0<GOAL>a ^ 2 = -↑(normSq a) ↔ star a = -a
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f✝ f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>inst✝ : Finite ι<VAR>f : (i : ι) → α i<GOAL>(pi fun x => pure (f x)) = pure f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ : α → E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>hp_ne_top : p ≠ ⊤<VAR>P : (α → E) → Prop<VAR>h0P : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x => c) p μ ≤ ε ∧ P g<VAR>h1P : ∀ (f g : α → E), P f → P g → P (f + g)<VAR>h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ g, eLpNorm (f - g) p μ ≤ ε ∧ P g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ : α → E<VAR>μ : Measure α<VAR>P : (α → E) → Prop<VAR>h1P : ∀ (f g : α → E), P f → P g → P (f + g)<VAR>h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ<VAR>f : α → E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hp_ne_top : 0 ≠ ⊤<VAR>h0P : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x => c) 0 μ ≤ ε ∧ P g<VAR>hf : Memℒp f 0 μ<GOAL>∃ g, eLpNorm (f - g) 0 μ ≤ ε ∧ P g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ : α → E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>hp_ne_top : p ≠ ⊤<VAR>P : (α → E) → Prop<VAR>h0P : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x => c) p μ ≤ ε ∧ P g<VAR>h1P : ∀ (f g : α → E), P f → P g → P (f + g)<VAR>h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hp_pos : p ≠ 0<GOAL>∃ g, eLpNorm (f - g) p μ ≤ ε ∧ P g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ : α → E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>hp_ne_top : p ≠ ⊤<VAR>P : (α → E) → Prop<VAR>h0P : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x => c) p μ ≤ ε ∧ P g<VAR>h1P : ∀ (f g : α → E), P f → P g → P (f + g)<VAR>h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hp_pos : p ≠ 0<GOAL>∀ (f' : α →ₛ E) (δ : ℝ≥0∞), δ ≠ 0 → Memℒp (↑f') p μ → ∃ g, eLpNorm (↑f' - g) p μ ≤ δ ∧ P g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ : α → E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>hp_ne_top : p ≠ ⊤<VAR>P : (α → E) → Prop<VAR>h0P : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x => c) p μ ≤ ε ∧ P g<VAR>h1P : ∀ (f g : α → E), P f → P g → P (f + g)<VAR>h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hp_pos : p ≠ 0<GOAL>∀ (c : E) {s : Set α} (hs : MeasurableSet s) (δ : ℝ≥0∞), δ ≠ 0 → Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ → ∃ g, eLpNorm (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) - g) p μ ≤ δ ∧ P g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ : α → E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>hp_ne_top : p ≠ ⊤<VAR>P : (α → E) → Prop<VAR>h0P : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x => c) p μ ≤ ε ∧ P g<VAR>h1P : ∀ (f g : α → E), P f → P g → P (f + g)<VAR>h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hp_pos : p ≠ 0<GOAL>∀ ⦃f g : α →ₛ E⦄, Disjoint (support ↑f) (support ↑g) → (∀ (δ : ℝ≥0∞), δ ≠ 0 → Memℒp (↑f) p μ → ∃ g, eLpNorm (↑f - g) p μ ≤ δ ∧ P g) → (∀ (δ : ℝ≥0∞), δ ≠ 0 → Memℒp (↑g) p μ → ∃ g_1, eLpNorm (↑g - g_1) p μ ≤ δ ∧ P g_1) → ∀ (δ : ℝ≥0∞), δ ≠ 0 → Memℒp (↑(f + g)) p μ → ∃ g_1, eLpNorm (↑(f + g) - g_1) p μ ≤ δ ∧ P g_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set α<VAR>t : Set β<GOAL>(𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
<VAR>n : ℕ<VAR>b : Bool<GOAL>bit b n ≠ 0 ↔ n = 0 → b = true
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s✝ t : Set α<VAR>f✝ g f : α → E<VAR>s : Set α<GOAL>⨍ (x : α) in s, f x ∂μ = (μ s).toReal⁻¹ • ∫ (x : α) in s, f x ∂μ
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>z : R<VAR>f : (i : ι) → s i<GOAL>tprodCoeff R z f = z • (tprod R) f
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>z : R<VAR>f : (i : ι) → s i<VAR>this : z = z • 1<GOAL>tprodCoeff R z f = z • (tprod R) f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w : σ → M<VAR>m n : M<GOAL>weightedHomogeneousSubmodule R w m * weightedHomogeneousSubmodule R w n ≤ weightedHomogeneousSubmodule R w (m + n)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁹ : SeminormedAddCommGroup E<VAR>inst✝¹⁸ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁷ : SeminormedAddCommGroup F<VAR>inst✝¹⁶ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup G<VAR>inst✝¹⁴ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : NontriviallyNormedField 𝕜₂<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁸ : NormedSpace 𝕜₂ F<VAR>inst✝⁷ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁶ : NormedSpace 𝕜₃ G<VAR>inst✝⁵ : NormedSpace 𝕜 Gₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝³ : FunLike 𝓕 E F<VAR>inst✝² : RingHomIsometric σ₂₃<VAR>inst✝¹ : RingHomIsometric σ₁₃<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>L : E →L[𝕜] Fₗ →L[𝕜] Gₗ<GOAL>‖precompL Eₗ L‖ ≤ ‖L‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁹ : SeminormedAddCommGroup E<VAR>inst✝¹⁸ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁷ : SeminormedAddCommGroup F<VAR>inst✝¹⁶ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup G<VAR>inst✝¹⁴ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : NontriviallyNormedField 𝕜₂<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁸ : NormedSpace 𝕜₂ F<VAR>inst✝⁷ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁶ : NormedSpace 𝕜₃ G<VAR>inst✝⁵ : NormedSpace 𝕜 Gₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝³ : FunLike 𝓕 E F<VAR>inst✝² : RingHomIsometric σ₂₃<VAR>inst✝¹ : RingHomIsometric σ₁₃<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>L : E →L[𝕜] Fₗ →L[𝕜] Gₗ<GOAL>‖precompR Eₗ L.flip‖ ≤ ‖L.flip‖
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<VAR>s t : Set E<VAR>x : E<VAR>hs : s ⊆ t<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hp : HasFPowerSeriesWithinAt f p t x<GOAL>AnalyticWithinAt 𝕜 f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>inst✝ : NoMaxOrder α<VAR>a b : α<GOAL>interior (Ioc a b) = Ioo a b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>A : Type u_4<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module A N<VAR>inst✝ : IsScalarTower R A N<VAR>l : M →ₗ[R] N<GOAL>range (liftBaseChange A l) = Submodule.span A ↑(range l)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>A : Type u_4<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module A N<VAR>inst✝ : IsScalarTower R A N<VAR>l : M →ₗ[R] N<GOAL>range (liftBaseChange A l) ≤ Submodule.span A ↑(range l)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>A : Type u_4<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module A N<VAR>inst✝ : IsScalarTower R A N<VAR>l : M →ₗ[R] N<GOAL>Submodule.span A ↑(range l) ≤ range (liftBaseChange A l)
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>padicValNat p (p * (n / p))! = padicValNat p n !
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>padicValNat p (p * (n / p))! = padicValNat p (p * (n / p) + n % p)!
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<GOAL>a * ⊤ = if a = 0 then 0 else ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s✝ t : Set α<VAR>a b x y : α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>ha : a ∈ s<VAR>n : ℕ<GOAL>(f ^ n) a = a ↔ s.card ∣ n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<VAR>n : ℕ<VAR>hf : f.IsCycleOn ↑{a}<VAR>ha : a ∈ {a}<GOAL>(f ^ n) a = a ↔ {a}.card ∣ n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s✝ t : Set α<VAR>a b x y : α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>ha : a ∈ s<VAR>n : ℕ<VAR>hs : s.Nontrivial<GOAL>(f ^ n) a = a ↔ s.card ∣ n
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n✝ : Type u_4<VAR>R : Type u_5<VAR>α : Type u_6<VAR>n : Type u_7<VAR>inst✝³ : Zero α<VAR>inst✝² : One α<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : AddGroup n<VAR>i j : n<GOAL>circulant (Pi.single 0 1) i j = 1 i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝ : AddZeroClass α<VAR>h : Periodic f c<GOAL>f c = f 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑↑X<GOAL>op U = (Opens.map f.base).op.obj (op ((opensFunctor f).obj U))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑↑X<GOAL>invApp f U ≫ f.c.app (op ((opensFunctor f).obj U)) = X.presheaf.map (eqToHom ⋯)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝⁶ : Fintype α<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>S : Type u_4<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M<VAR>inst✝ : SMulCommClass R S M<VAR>v : α → M<GOAL>LinearMap.range ((Fintype.total R S) v) = span R (Set.range v)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Inhabited α<VAR>l✝ : List α<VAR>a : α<VAR>l : List α<GOAL>(a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>s : Set α<VAR>f✝ : ι → α<VAR>a✝ : α<VAR>f : ι → α<VAR>a : α<VAR>h : a < ⨆ i, f i<GOAL>∃ i, a < f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>s : Set α<VAR>f✝ : ι → α<VAR>a✝ : α<VAR>f : ι → α<VAR>a : α<VAR>h : ∀ (i : ι), f i ≤ a<GOAL>⨆ i, f i ≤ a
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>a : α<GOAL>‖f‖ = sInf {C | ∀ (x : α), ‖f x‖ ≤ C}
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>a : α<GOAL>sInf {C | 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C} = sInf {C | ∀ (x : α), ‖f x‖ ≤ C}
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>a : α<VAR>x✝ : ℝ<GOAL>x✝ ∈ {C | 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C} ↔ x✝ ∈ {C | ∀ (x : α), ‖f x‖ ≤ C}
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>a : α<VAR>x✝ : ℝ<GOAL>(∀ (x : α), ‖f x‖ ≤ x✝) → 0 ≤ x✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : TotallyDisconnectedSpace X<GOAL>IsTopologicalBasis {s | IsClopen s}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : TotallyDisconnectedSpace X<GOAL>∀ (a : X) (u : Set X), a ∈ u → IsOpen u → ∃ v ∈ fun U => IsClosed U ∧ IsOpen U, a ∈ v ∧ v ⊆ u
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : TotallyDisconnectedSpace X<VAR>x : X<VAR>U : Set X<VAR>hxU : x ∈ U<VAR>U_op : IsOpen U<GOAL>∃ v ∈ fun U => IsClosed U ∧ IsOpen U, x ∈ v ∧ v ⊆ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : TotallyDisconnectedSpace X<VAR>x : X<VAR>U : Set X<VAR>hxU : x ∈ U<VAR>U_op : IsOpen U<VAR>this : U ∈ 𝓝 x<GOAL>∃ v ∈ fun U => IsClosed U ∧ IsOpen U, x ∈ v ∧ v ⊆ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : TotallyDisconnectedSpace X<VAR>x : X<VAR>U : Set X<VAR>hxU : x ∈ U<VAR>U_op : IsOpen U<VAR>this : U ∈ 𝓝 x<VAR>V : Set X<VAR>hVU : V ⊆ U<VAR>hxV : x ∈ V<VAR>hV : IsClopen V<GOAL>∃ v ∈ fun U => IsClosed U ∧ IsOpen U, x ∈ v ∧ v ⊆ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : TotallyDisconnectedSpace X<VAR>x : X<VAR>U : Set X<VAR>hxU : x ∈ U<VAR>U_op : IsOpen U<VAR>this : U ∈ 𝓝 x<VAR>V : Set X<VAR>hVU : V ⊆ U<VAR>hxV : x ∈ V<VAR>hV : IsClopen V<GOAL>(V ∈ fun U => IsClosed U ∧ IsOpen U) ∧ x ∈ V ∧ V ⊆ U
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>h : q.degree < p.degree<GOAL>(p - q).degree = p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>h : (-q).degree < p.degree<GOAL>(p - q).degree = p.degree
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f g : TensorAlgebra R M →ₐ[R] A<VAR>w : f.toLinearMap ∘ₗ ι R = g.toLinearMap ∘ₗ ι R<GOAL>f = g
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f g : TensorAlgebra R M →ₐ[R] A<VAR>w : (lift R).symm f = (lift R).symm g<GOAL>f = g