ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>g : { g // 0 ≤ g }<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hg_memℒp : Memℒp (↑↑↑g) p μ<VAR>zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}<VAR>this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})<VAR>g_meas : Measurable ↑↑↑g<VAR>x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n<VAR>hx_nonneg : ∀ (n : ℕ), 0 ≤ x n<VAR>hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p μ<GOAL>∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 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>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>g : { g // 0 ≤ g }<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hg_memℒp : Memℒp (↑↑↑g) p μ<VAR>zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}<VAR>this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})<VAR>g_meas : Measurable ↑↑↑g<VAR>x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n<VAR>hx_nonneg : ∀ (n : ℕ), 0 ≤ x n<VAR>hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p μ<VAR>h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) ⋯) =ᶠ[ae μ] ↑(x n)<GOAL>∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 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>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>g : { g // 0 ≤ g }<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hg_memℒp : Memℒp (↑↑↑g) p μ<VAR>zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}<VAR>this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})<VAR>g_meas : Measurable ↑↑↑g<VAR>x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n<VAR>hx_nonneg : ∀ (n : ℕ), 0 ≤ x n<VAR>hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p μ<VAR>h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) ⋯) =ᶠ[ae μ] ↑(x n)<VAR>hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) ⋯<GOAL>∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 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>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>g : { g // 0 ≤ g }<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hg_memℒp : Memℒp (↑↑↑g) p μ<VAR>zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}<VAR>this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})<VAR>g_meas : Measurable ↑↑↑g<VAR>x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n<VAR>hx_nonneg : ∀ (n : ℕ), 0 ≤ x n<VAR>hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p μ<VAR>h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) ⋯) =ᶠ[ae μ] ↑(x n)<VAR>hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) ⋯<VAR>hx_tendsto : Tendsto (fun n => eLpNorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)<GOAL>∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 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>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>g : { g // 0 ≤ g }<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hg_memℒp : Memℒp (↑↑↑g) p μ<VAR>zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}<VAR>this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})<VAR>g_meas : Measurable ↑↑↑g<VAR>x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n<VAR>hx_nonneg : ∀ (n : ℕ), 0 ≤ x n<VAR>hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p μ<VAR>h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) ⋯) =ᶠ[ae μ] ↑(x n)<VAR>hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) ⋯<VAR>hx_tendsto : Tendsto (fun n => eLpNorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)<GOAL>Tendsto (fun n => coeSimpleFuncNonnegToLpNonneg p μ G ⟨toLp (x n) ⋯, ⋯⟩) atTop (𝓝 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>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>g : { g // 0 ≤ g }<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hg_memℒp : Memℒp (↑↑↑g) p μ<VAR>zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}<VAR>this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})<VAR>g_meas : Measurable ↑↑↑g<VAR>x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n<VAR>hx_nonneg : ∀ (n : ℕ), 0 ≤ x n<VAR>hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p μ<VAR>h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) ⋯) =ᶠ[ae μ] ↑(x n)<VAR>hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) ⋯<VAR>hx_tendsto : Tendsto (fun n => eLpNorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)<GOAL>Tendsto (fun n => ↑(toLp (x n) ⋯)) atTop (𝓝 ↑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>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>g : { g // 0 ≤ g }<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hg_memℒp : Memℒp (↑↑↑g) p μ<VAR>zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}<VAR>this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})<VAR>g_meas : Measurable ↑↑↑g<VAR>x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n<VAR>hx_nonneg : ∀ (n : ℕ), 0 ≤ x n<VAR>hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p μ<VAR>h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) ⋯) =ᶠ[ae μ] ↑(x n)<VAR>hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) ⋯<VAR>hx_tendsto : Tendsto (fun n => eLpNorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)<GOAL>Tendsto (fun n => eLpNorm (↑↑↑(toLp (x n) ⋯) - ↑↑↑g) p μ) atTop (𝓝 0)
<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>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>g : { g // 0 ≤ g }<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hg_memℒp : Memℒp (↑↑↑g) p μ<VAR>zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}<VAR>this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})<VAR>g_meas : Measurable ↑↑↑g<VAR>x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n<VAR>hx_nonneg : ∀ (n : ℕ), 0 ≤ x n<VAR>hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p μ<VAR>h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) ⋯) =ᶠ[ae μ] ↑(x n)<VAR>hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) ⋯<VAR>hx_tendsto : Tendsto (fun n => eLpNorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)<VAR>n : ℕ<GOAL>↑(x n) =ᶠ[ae μ] ↑↑↑(toLp (x n) ⋯)
<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>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>g : { g // 0 ≤ g }<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hg_memℒp : Memℒp (↑↑↑g) p μ<VAR>zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}<VAR>this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})<VAR>g_meas : Measurable ↑↑↑g<VAR>x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n<VAR>hx_nonneg : ∀ (n : ℕ), 0 ≤ x n<VAR>hx_memℒp : ∀ (n : ℕ), Memℒp (↑(x n)) p μ<VAR>h_toLp : ∀ (n : ℕ), ↑↑(Memℒp.toLp ↑(x n) ⋯) =ᶠ[ae μ] ↑(x n)<VAR>hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ toLp (x n) ⋯<VAR>hx_tendsto : Tendsto (fun n => eLpNorm (↑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)<VAR>n : ℕ<GOAL>↑↑↑g =ᶠ[ae μ] ↑↑↑g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>limit.lift (D.diagramOverOpen U) { pt := (D.U i).presheaf.obj (op U), π := { app := fun j => D.ιInvAppπApp U (unop j), naturality := ⋯ } } ≫ D.diagramOverOpenπ U i = (D.U i).presheaf.map (eqToHom ⋯)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>{ pt := (D.U i).presheaf.obj (op U), π := { app := fun j => D.ιInvAppπApp U (unop j), naturality := ⋯ } }.π.app (op (WalkingMultispan.right i)) = (D.U i).presheaf.map (eqToHom ⋯)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>(D.f i i).c.app (op U) ≫ (D.t i i).c.app (op ((Opens.map (D.f i i).base).obj U)) ≫ invApp (D.f i i) ((Opens.map (D.t i i).base).toPrefunctor.1 ((Opens.map (D.f i i).base).obj U)) ≫ (D.U i).presheaf.map (eqToHom ⋯).op = (D.U i).presheaf.map (eqToHom ⋯)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>(D.f i i).c.app (op U) ≫ (D.V (i, i)).presheaf.map (𝟙 (op ((Opens.map (D.f i i).base).obj U)) ≫ eqToHom ⋯) ≫ invApp (D.f i i) ((Opens.map (D.t i i).base).toPrefunctor.1 ((Opens.map (D.f i i).base).obj U)) ≫ (D.U i).presheaf.map (eqToHom ⋯).op = (D.U i).presheaf.map (eqToHom ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : OrderBot β<VAR>f : γ → α →ₛ β<VAR>s : Finset γ<VAR>a : α<GOAL>↑(s.sup f) a = s.sup fun c => ↑(f c) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : OrderBot β<VAR>f : γ → α →ₛ β<VAR>s : Finset γ<VAR>a : α<GOAL>∀ ⦃a_1 : γ⦄ {s : Finset γ}, a_1 ∉ s → (↑(s.sup f) a = s.sup fun c => ↑(f c) a) → ↑((insert a_1 s).sup f) a = (insert a_1 s).sup fun c => ↑(f c) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : OrderBot β<VAR>f : γ → α →ₛ β<VAR>s✝ : Finset γ<VAR>a✝¹ : α<VAR>a : γ<VAR>s : Finset γ<VAR>a✝ : a ∉ s<VAR>ih : ↑(s.sup f) a✝¹ = s.sup fun c => ↑(f c) a✝¹<GOAL>↑((insert a s).sup f) a✝¹ = (insert a s).sup fun c => ↑(f c) a✝¹
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<GOAL>Measure.map id (ProbabilityTheory.cond μ s) = ProbabilityTheory.cond μ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : ContinuousMul M<VAR>f : ι → X → M<VAR>s : Multiset ι<VAR>t : Set X<VAR>l : List ι<GOAL>(∀ i ∈ Quot.mk Setoid.r l, ContinuousOn (f i) t) → ContinuousOn (fun a => (Multiset.map (fun i => f i a) (Quot.mk Setoid.r l)).prod) t
<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>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₁<VAR>w : Set M<VAR>hw : w.Finite<VAR>s : span R w = ⊤<VAR>ι : Type w<VAR>b : Basis ι R M<GOAL>Finite ι
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>inst✝¹ : Lattice α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>x✝ : Interval α<GOAL>↑(⊥ ⊓ x✝) = ↑⊥ ∩ ↑x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>inst✝¹ : Lattice α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>x✝ : Interval α<GOAL>↑⊥ = ↑⊥ ∩ ↑x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>inst✝¹ : Lattice α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : NonemptyInterval α<GOAL>↑(↑s ⊓ ⊥) = ↑↑s ∩ ↑⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>inst✝¹ : Lattice α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : NonemptyInterval α<GOAL>↑⊥ = ↑↑s ∩ ↑⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>inst✝¹ : Lattice α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : NonemptyInterval α<GOAL>↑(↑s ⊓ ↑t) = ↑↑s ∩ ↑↑t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>inst✝¹ : Lattice α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : NonemptyInterval α<GOAL>↑(if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then ↑{ toProd := (s.toProd.1 ⊔ t.toProd.1, s.toProd.2 ⊓ t.toProd.2), fst_le_snd := ⋯ } else ⊥) = Icc (s.toProd.1 ⊔ t.toProd.1) (s.toProd.2 ⊓ t.toProd.2)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Preadditive C<VAR>M : Mat_ C<VAR>i : M.ι<GOAL>𝟙 M i i = 𝟙 (M.X i)
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>h : p ≠ 0<GOAL>1 < rootMultiplicity t p ↔ p.IsRoot t ∧ (derivative p).IsRoot t
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>h : p ≠ 0<GOAL>(∀ m ≤ 1, ((⇑derivative)^[m] p).IsRoot t) ↔ p.IsRoot t ∧ (derivative p).IsRoot t
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : Fintype τ<GOAL>psum σ R 1 = ∑ i : σ, X i
<VAR>α✝ α : Type u<VAR>inst✝ : OrderedCommGroup α<VAR>a b c : α<VAR>bc : swap (fun x x_1 => x * x_1) a b ≤ swap (fun x x_1 => x * x_1) a c<GOAL>b ≤ c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>m : α → β<VAR>t : Set α<VAR>f g : Filter ↑t<VAR>h : Injective (m ∘ Subtype.val)<GOAL>map m (map Subtype.val f ⊓ map Subtype.val g) = map m (map Subtype.val f) ⊓ map m (map Subtype.val g)
<VAR>x y : ℂ<GOAL>tanh (-x) = -tanh x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>o : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>M : Matrix m n R<VAR>i : m<GOAL>(M.map ⇑f).toMvPolynomial i = (MvPolynomial.map f) (M.toMvPolynomial i)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>T T' T'' : D<VAR>Y Y' Y'' : C<VAR>S S' : C ⥤ D<VAR>f : T ⟶ T'<VAR>f' : T' ⟶ T''<VAR>h : CostructuredArrow S T<GOAL>(map (f ≫ f')).obj h = (map f').obj ((map f).obj h)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>T T' T'' : D<VAR>Y Y' Y'' : C<VAR>S S' : C ⥤ D<VAR>f : T ⟶ T'<VAR>f' : T' ⟶ T''<VAR>h : CostructuredArrow S T<GOAL>(map (f ≫ f')).obj (mk h.hom) = (map f').obj ((map f).obj (mk h.hom))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a✝ b a : α<VAR>s t : Finset α<GOAL>s ∩ t.erase a = (s ∩ t).erase a
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c a : G₀<VAR>h : a ≠ 0<VAR>g : G₀<GOAL>(fun g => g * a) (g * a⁻¹) = g
<VAR>G : Type u_1<VAR>hG : Group G<VAR>inst✝ : Finite G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : IsPGroup p G<GOAL>Group.IsNilpotent G
<VAR>G : Type u_1<VAR>hG : Group G<VAR>inst✝ : Finite G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : IsPGroup p G<VAR>val✝ : Fintype G<GOAL>Group.IsNilpotent G
<VAR>x y : SimplexCategory<VAR>f : x ⟶ y<VAR>hyp_f_epi : Epi f<GOAL>y.len ≤ x.len
<VAR>x y : SimplexCategory<VAR>f : x ⟶ y<VAR>hyp_f_epi : Epi f<VAR>f_surj : Function.Surjective (Hom.toOrderHom f).toFun<GOAL>y.len ≤ x.len
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>m : M<GOAL>(TensorAlgebra.ι R) m ∈ LinearMap.range (TensorAlgebra.ι R) ^ 1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₂ p₃ p₁).tan * dist p₃ p₂ = dist p₁ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₂ p₃ p₁).sign = 1<GOAL>(∡ p₂ p₃ p₁).tan * dist p₃ p₂ = dist p₁ p₂
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : Perm (Subtype p)<VAR>h : f.IsSwap<VAR>x : α<VAR>hx : p x<VAR>y : α<VAR>hy : p y<VAR>hxy : ⟨x, hx⟩ ≠ ⟨y, hy⟩ ∧ f = swap ⟨x, hx⟩ ⟨y, hy⟩<GOAL>x ≠ y
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : Perm (Subtype p)<VAR>h : f.IsSwap<VAR>x : α<VAR>hx : p x<VAR>y : α<VAR>hy : p y<VAR>hxy : ¬x = y ∧ f = swap ⟨x, hx⟩ ⟨y, hy⟩<GOAL>x ≠ y
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : Perm (Subtype p)<VAR>h : f.IsSwap<VAR>x : α<VAR>hx : p x<VAR>y : α<VAR>hy : p y<VAR>hxy : ⟨x, hx⟩ ≠ ⟨y, hy⟩ ∧ f = swap ⟨x, hx⟩ ⟨y, hy⟩<GOAL>ofSubtype f = swap x y
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : MulOneClass G<VAR>inst✝ : ContinuousMul G<VAR>K U : Set G<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>∃ V ∈ 𝓝 1, V * K ⊆ U
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : MulOneClass G<VAR>inst✝ : ContinuousMul G<VAR>K U : Set G<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<VAR>V : Set Gᵐᵒᵖ<VAR>hV : V ∈ 𝓝 (op 1)<VAR>hV' : op '' K * V ⊆ op '' U<GOAL>∃ V ∈ 𝓝 1, V * K ⊆ U
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : MulOneClass G<VAR>inst✝ : ContinuousMul G<VAR>K U : Set G<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<VAR>V : Set Gᵐᵒᵖ<VAR>hV : V ∈ 𝓝 (op 1)<VAR>hV' : op '' K * V ⊆ op '' U<GOAL>op ⁻¹' V * K ⊆ U
<VAR>f : ℝ → ℝ<VAR>x f' : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hx : f x ≠ 0<GOAL>HasDerivWithinAt (fun y => Real.log (f y)) (f' / f x) s x
<VAR>f : ℝ → ℝ<VAR>x f' : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hx : f x ≠ 0<GOAL>HasDerivWithinAt (fun y => Real.log (f y)) ((f x)⁻¹ * f') s x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<GOAL>μ.restrict (⋃ i, s i) = ν.restrict (⋃ i, s i) ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)<GOAL>μ.restrict (⋃ i, s i) = ν.restrict (⋃ i, s i)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>D : Directed (fun x x_1 => x ⊆ x_1) fun t => ⋃ i ∈ t, s i<GOAL>(μ.restrict (⋃ i, s i)) t = (ν.restrict (⋃ i, s i)) t
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>D : Directed (fun x x_1 => x ⊆ x_1) fun t => ⋃ i ∈ t, s i<GOAL>(μ.restrict (⋃ t, ⋃ i ∈ t, s i)) t = (ν.restrict (⋃ t, ⋃ i ∈ t, s i)) t
<VAR>p : ℝ<VAR>hp₀ : 0 < p<VAR>hp₁ : p < 1<GOAL>StrictConcaveOn ℝ (Ici 0) fun x => x ^ p
<VAR>p : ℝ<VAR>hp₀ : 0 < p<VAR>hp₁ : p < 1<VAR>x : ℝ<VAR>hx : x ∈ Ici 0<VAR>y : ℝ<VAR>hy : y ∈ Ici 0<VAR>hxy : x ≠ y<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
<VAR>p : ℝ<VAR>hp₀ : 0 < p<VAR>hp₁ : p < 1<VAR>x : ℝ<VAR>hx : x ∈ Ici 0<VAR>y : ℝ<VAR>hy : y ∈ Ici 0<VAR>hxy : x ≠ y<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>x' : ℝ≥0 := ⟨x, hx⟩<VAR>y' : ℝ≥0 := ⟨y, hy⟩<VAR>a' : ℝ≥0 := ⟨a, ⋯⟩<VAR>b' : ℝ≥0 := ⟨b, ⋯⟩<GOAL>a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
<VAR>p : ℝ<VAR>hp₀ : 0 < p<VAR>hp₁ : p < 1<VAR>x : ℝ<VAR>hx : x ∈ Ici 0<VAR>y : ℝ<VAR>hy : y ∈ Ici 0<VAR>hxy : x ≠ y<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>x' : ℝ≥0 := ⟨x, hx⟩<VAR>y' : ℝ≥0 := ⟨y, hy⟩<VAR>a' : ℝ≥0 := ⟨a, ⋯⟩<VAR>b' : ℝ≥0 := ⟨b, ⋯⟩<VAR>hxy' : x' ≠ y'<GOAL>a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
<VAR>p : ℝ<VAR>hp₀ : 0 < p<VAR>hp₁ : p < 1<VAR>x : ℝ<VAR>hx : x ∈ Ici 0<VAR>y : ℝ<VAR>hy : y ∈ Ici 0<VAR>hxy : x ≠ y<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>x' : ℝ≥0 := ⟨x, hx⟩<VAR>y' : ℝ≥0 := ⟨y, hy⟩<VAR>a' : ℝ≥0 := ⟨a, ⋯⟩<VAR>b' : ℝ≥0 := ⟨b, ⋯⟩<VAR>hxy' : x' ≠ y'<VAR>hab' : a' + b' = 1<GOAL>a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Surjective ⇑f<VAR>S : Subalgebra R B<GOAL>S ≤ f.range
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>h : a < b<GOAL>Ioc a b \ Ioo a b = {b}
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>a b : α<VAR>l l₁ l₂ : List α<VAR>h : (a :: b :: l).split = (l₁, l₂)<VAR>l₁' l₂' : List α<VAR>e : l.split = (l₁', l₂')<GOAL>l₁.length < (a :: b :: l).length ∧ l₂.length < (a :: b :: l).length