ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>x : 𝕜<VAR>m : ℕ<VAR>hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x<VAR>n : ℕ<VAR>hg : AnalyticAt 𝕜 (fun z => (z - x) ^ n • g z) x<VAR>this : (fun z => (z - x) ^ max m n • (f + g) z) = fun z => (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z<GOAL>AnalyticAt 𝕜 (fun z => (z - x) ^ max m n • (f + g) z) x
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>x : 𝕜<VAR>m : ℕ<VAR>hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x<VAR>n : ℕ<VAR>hg : AnalyticAt 𝕜 (fun z => (z - x) ^ n • g z) x<VAR>this : (fun z => (z - x) ^ max m n • (f + g) z) = fun z => (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z<GOAL>AnalyticAt 𝕜 (fun z => (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z) x
<VAR>α : Type u_1<VAR>as : List (Option α)<VAR>as' : List α<GOAL>as.fillNones as' = as.fillNonesTR as'
<VAR>α : Type u_1<VAR>as✝ : List (Option α)<VAR>as' : List α<VAR>acc : Array α<VAR>as : List (Option α)<GOAL>fillNonesTR.go (none :: as) [] acc = acc.data ++ (none :: as).fillNones []
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>f : α → α → β<VAR>comm : ∀ (x y : α), f x y = f y x<VAR>l l' : List α<GOAL>zipWith f l l' = zipWith f l' l
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>f : α → α → β<VAR>comm : ∀ (x y : α), f x y = f y x<VAR>l l' : List α<GOAL>zipWith (fun b a => f a b) l' l = zipWith f l' l
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsFilteredOrEmpty C<VAR>j₁ j₂ k₁ k₂ : C<VAR>f₁ : j₁ ⟶ k₁<VAR>g₁ : j₁ ⟶ k₂<VAR>f₂ : j₂ ⟶ k₁<VAR>g₂ : j₂ ⟶ k₂<GOAL>∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsFilteredOrEmpty C<VAR>j₁ j₂ k₁ k₂ : C<VAR>f₁ : j₁ ⟶ k₁<VAR>g₁ : j₁ ⟶ k₂<VAR>f₂ : j₂ ⟶ k₁<VAR>g₂ : j₂ ⟶ k₂<VAR>t : C<VAR>k₁t : k₁ ⟶ t<VAR>k₂t : k₂ ⟶ t<VAR>ht : f₁ ≫ k₁t = g₁ ≫ k₂t<GOAL>∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsFilteredOrEmpty C<VAR>j₁ j₂ k₁ k₂ : C<VAR>f₁ : j₁ ⟶ k₁<VAR>g₁ : j₁ ⟶ k₂<VAR>f₂ : j₂ ⟶ k₁<VAR>g₂ : j₂ ⟶ k₂<VAR>t : C<VAR>k₁t : k₁ ⟶ t<VAR>k₂t : k₂ ⟶ t<VAR>ht : f₁ ≫ k₁t = g₁ ≫ k₂t<VAR>s : C<VAR>ts : t ⟶ s<VAR>hs : (f₂ ≫ k₁t) ≫ ts = (g₂ ≫ k₂t) ≫ ts<GOAL>∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsFilteredOrEmpty C<VAR>j₁ j₂ k₁ k₂ : C<VAR>f₁ : j₁ ⟶ k₁<VAR>g₁ : j₁ ⟶ k₂<VAR>f₂ : j₂ ⟶ k₁<VAR>g₂ : j₂ ⟶ k₂<VAR>t : C<VAR>k₁t : k₁ ⟶ t<VAR>k₂t : k₂ ⟶ t<VAR>ht : f₁ ≫ k₁t = g₁ ≫ k₂t<VAR>s : C<VAR>ts : t ⟶ s<VAR>hs : f₂ ≫ k₁t ≫ ts = g₂ ≫ k₂t ≫ ts<GOAL>∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f✝ g✝ : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>𝕜' : Type u_1<VAR>inst✝² : NormedField 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' G<VAR>inst✝ : SMulCommClass 𝕜 𝕜' G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>g : ContinuousMultilinearMap 𝕜 E G'<VAR>x✝ : ℝ≥0<GOAL>‖f.prod g‖₊ ≤ x✝ ↔ max ‖f‖₊ ‖g‖₊ ≤ x✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : LocallyCompactPair X Y<VAR>f : X → Y<VAR>K : Set X<VAR>U : Set Y<VAR>hf : Continuous f<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : MapsTo f K U<GOAL>∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : LocallyCompactPair X Y<VAR>f : X → Y<VAR>K : Set X<VAR>U : Set Y<VAR>hf : Continuous f<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : MapsTo f K U<VAR>V : X → Set X<VAR>hxV : ∀ x ∈ K, V x ∈ 𝓝 x<VAR>hVc : ∀ x ∈ K, IsCompact (V x)<VAR>hVU : ∀ x ∈ K, MapsTo f (V x) U<GOAL>∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : LocallyCompactPair X Y<VAR>f : X → Y<VAR>K : Set X<VAR>U : Set Y<VAR>hf : Continuous f<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : MapsTo f K U<VAR>V : X → Set X<VAR>hxV : ∀ x ∈ K, V x ∈ 𝓝 x<VAR>hVc : ∀ x ∈ K, IsCompact (V x)<VAR>hVU : ∀ x ∈ K, MapsTo f (V x) U<VAR>s : Finset X<VAR>hsK : ∀ x ∈ s, x ∈ K<VAR>hKs : ⋃ x ∈ s, V x ∈ 𝓝ˢ K<GOAL>∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n✝ : ℕ<VAR>x : List α<VAR>n : ℕ<VAR>hn : n < x.length<VAR>w✝ : List α<GOAL>x[n] = (x ++ w✝)[n]
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<GOAL>0 ≤ (of v).dens n
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<GOAL>0 ≤ ((of v).contsAux (n + 1)).b
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M N : Matrix n n R<GOAL>(M * N).det = ∑ p : n → n, ∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, M (σ i) (p i) * N (p i) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M N : Matrix n n R<GOAL>∑ x : Perm n, ∑ i : n → n, ↑↑(sign x) * ∏ i_1 : n, M (x i_1) (i i_1) * N (i i_1) i_1 = ∑ p : n → n, ∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, M (σ i) (p i) * N (p i) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M N : Matrix n n R<VAR>f : n → n<VAR>x✝ : f ∈ univ<VAR>hbij : f ∉ filter Bijective univ<GOAL>¬Bijective f
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M N : Matrix n n R<GOAL>∑ τ : Perm n, ∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, M (σ i) (τ i) * N (τ i) i = ∑ σ : Perm n, ∑ τ : Perm n, (∏ i : n, N (σ i) i) * ↑↑(sign τ) * ∏ j : n, M (τ j) (σ j)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M N : Matrix n n R<VAR>σ : Perm n<VAR>x✝ : σ ∈ univ<VAR>τ : Perm n<GOAL>(∏ i : n, N (σ i) i) * ↑↑(sign τ) * ∏ j : n, M (τ j) (σ j) = (∏ i : n, N (σ i) i) * (↑↑(sign σ) * ↑↑(sign ((Equiv.mulRight σ⁻¹) τ))) * ∏ i : n, M (((Equiv.mulRight σ⁻¹) τ) i) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M N : Matrix n n R<VAR>σ : Perm n<VAR>x✝ : σ ∈ univ<VAR>τ : Perm n<VAR>this : ∏ j : n, M (τ j) (σ j) = ∏ j : n, M ((τ * σ⁻¹) j) j<GOAL>(∏ i : n, N (σ i) i) * ↑↑(sign τ) * ∏ j : n, M (τ j) (σ j) = (∏ i : n, N (σ i) i) * (↑↑(sign σ) * ↑↑(sign ((Equiv.mulRight σ⁻¹) τ))) * ∏ i : n, M (((Equiv.mulRight σ⁻¹) τ) i) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M N : Matrix n n R<VAR>σ : Perm n<VAR>x✝ : σ ∈ univ<VAR>τ : Perm n<VAR>this : ∏ j : n, M (τ j) (σ j) = ∏ j : n, M ((τ * σ⁻¹) j) j<VAR>h : ↑↑(sign σ) * ↑↑(sign (τ * σ⁻¹)) = ↑↑(sign τ)<GOAL>(∏ i : n, N (σ i) i) * ↑↑(sign τ) * ∏ j : n, M (τ j) (σ j) = (∏ i : n, N (σ i) i) * (↑↑(sign σ) * ↑↑(sign ((Equiv.mulRight σ⁻¹) τ))) * ∏ i : n, M (((Equiv.mulRight σ⁻¹) τ) i) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M N : Matrix n n R<VAR>σ : Perm n<VAR>x✝ : σ ∈ univ<VAR>τ : Perm n<VAR>this : ∏ j : n, M (τ j) (σ j) = ∏ j : n, M ((τ * σ⁻¹) j) j<VAR>h : ↑↑(sign σ) * ↑↑(sign (τ * σ⁻¹)) = ↑↑(sign τ)<GOAL>(∏ i : n, N (σ i) i) * ↑↑(sign τ) * ∏ j : n, M (τ j) (σ j) = (∏ i : n, N (σ i) i) * ↑↑(sign τ) * ∏ x : n, M ((τ * σ⁻¹) x) x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M N : Matrix n n R<GOAL>∑ σ : Perm n, ∑ τ : Perm n, (∏ i : n, N (σ i) i) * (↑↑(sign σ) * ↑↑(sign τ)) * ∏ i : n, M (τ i) i = M.det * N.det
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>ha : ∃ u, a < u<GOAL>𝓝[≥] a = ⨅ u, ⨅ (_ : a < u), 𝓟 (Ico a u)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : Summable fun i => f i ^ p<VAR>hg : Summable fun i => g i ^ p<GOAL>(Summable fun i => (f i + g i) ^ p) ∧ (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : Summable fun i => f i ^ p<VAR>hg : Summable fun i => g i ^ p<VAR>pos : 0 < p<GOAL>(Summable fun i => (f i + g i) ^ p) ∧ (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : Summable fun i => f i ^ p<VAR>hg : Summable fun i => g i ^ p<VAR>pos : 0 < p<VAR>H₁ : ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p<GOAL>(Summable fun i => (f i + g i) ^ p) ∧ (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : Summable fun i => f i ^ p<VAR>hg : Summable fun i => g i ^ p<VAR>pos : 0 < p<VAR>H₁ : ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p<VAR>bdd : BddAbove (Set.range fun s => ∑ i ∈ s, (f i + g i) ^ p)<GOAL>(Summable fun i => (f i + g i) ^ p) ∧ (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : Summable fun i => f i ^ p<VAR>hg : Summable fun i => g i ^ p<VAR>pos : 0 < p<VAR>H₁ : ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p<VAR>bdd : BddAbove (Set.range fun s => ∑ i ∈ s, (f i + g i) ^ p)<VAR>H₂ : Summable fun i => (f i + g i) ^ p<GOAL>(Summable fun i => (f i + g i) ^ p) ∧ (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : Summable fun i => f i ^ p<VAR>hg : Summable fun i => g i ^ p<VAR>pos : 0 < p<VAR>H₁ : ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p<VAR>bdd : BddAbove (Set.range fun s => ∑ i ∈ s, (f i + g i) ^ p)<VAR>H₂ : Summable fun i => (f i + g i) ^ p<GOAL>(∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : Summable fun i => f i ^ p<VAR>hg : Summable fun i => g i ^ p<VAR>pos : 0 < p<VAR>H₁ : ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p<VAR>bdd : BddAbove (Set.range fun s => ∑ i ∈ s, (f i + g i) ^ p)<VAR>H₂ : Summable fun i => (f i + g i) ^ p<GOAL>∑' (i : ι), (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hp0_lt : 0 < p<VAR>hq0 : 0 ≤ q<VAR>f g : α → ℝ≥0∞<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ⊤<VAR>hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0<GOAL>∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hp0_lt : 0 < p<VAR>hq0 : 0 ≤ q<VAR>f g : α → ℝ≥0∞<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ⊤<VAR>hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0<GOAL>⊤ = (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hp0_lt : 0 < p<VAR>hq0 : 0 ≤ q<VAR>f g : α → ℝ≥0∞<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ⊤<VAR>hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0<VAR>hp0_inv_lt : 0 < 1 / p<GOAL>⊤ = (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hp0_lt : 0 < p<VAR>hq0 : 0 ≤ q<VAR>f g : α → ℝ≥0∞<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ⊤<VAR>hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0<VAR>hp0_inv_lt : 0 < 1 / p<GOAL>⊤ = ⊤ * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>W✝ X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : PushoutCocone f g<VAR>ht : IsColimit t<VAR>inst✝ : Epi g<VAR>W : C<VAR>h k : t.pt ⟶ W<VAR>i : t.inl ≫ h = t.inl ≫ k<GOAL>t.inr ≫ h = t.inr ≫ k
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>x y : P<GOAL>x ∈ spanSingleton S y ↔ ∃ z, z • y = x
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>x y : P<GOAL>x ∈ ⟨span R {y}, ⋯⟩ ↔ ∃ z, z • y = x
<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>s s' t : Set α<VAR>f f' : α → β<VAR>inst✝ : (x : α) → Decidable (x ∈ t)<VAR>h : ContinuousOn f (s ∩ closure t)<VAR>h' : ContinuousOn f' (s' ∩ closure tᶜ)<VAR>H : s ∩ frontier t = s' ∩ frontier t<VAR>Heq : EqOn f f' (s ∩ frontier t)<GOAL>ContinuousOn (t.piecewise f f') (t.ite s s')
<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>s s' t : Set α<VAR>f f' : α → β<VAR>inst✝ : (x : α) → Decidable (x ∈ t)<VAR>h : ContinuousOn f (s ∩ closure t)<VAR>h' : ContinuousOn f' (s' ∩ closure tᶜ)<VAR>H : s ∩ frontier t = s' ∩ frontier t<VAR>Heq : EqOn f f' (s ∩ frontier t)<GOAL>∀ a ∈ t.ite s s' ∩ frontier t, f a = f' 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>s s' t : Set α<VAR>f f' : α → β<VAR>inst✝ : (x : α) → Decidable (x ∈ t)<VAR>h : ContinuousOn f (s ∩ closure t)<VAR>h' : ContinuousOn f' (s' ∩ closure tᶜ)<VAR>H : s ∩ frontier t = s' ∩ frontier t<VAR>Heq : EqOn f f' (s ∩ frontier t)<GOAL>ContinuousOn f (t.ite s s' ∩ closure t)
<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>s s' t : Set α<VAR>f f' : α → β<VAR>inst✝ : (x : α) → Decidable (x ∈ t)<VAR>h : ContinuousOn f (s ∩ closure t)<VAR>h' : ContinuousOn f' (s' ∩ closure tᶜ)<VAR>H : s ∩ frontier t = s' ∩ frontier t<VAR>Heq : EqOn f f' (s ∩ frontier t)<GOAL>ContinuousOn f' (t.ite s s' ∩ closure tᶜ)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type w'<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>P : Type u_1<VAR>inst✝¹ : L.Structure P<VAR>Q : Type u_2<VAR>inst✝ : L.Structure Q<VAR>h : N ≃[L] P<VAR>f g : M ≃[L] N<VAR>hfg : h.comp f = h.comp g<VAR>x : M<GOAL>f x = g x
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : R<GOAL>↑r ∈ adicCompletionIntegers K v
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : R<GOAL>v.intValuationDef r ≤ 1
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s : Multiset ℤ<VAR>n : ℤ<GOAL>s.prod % n = (map (fun x => x % n) s).prod % n
<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>inst✝ : Fintype ι<VAR>hfg : Monovary f g<GOAL>∑ i : ι, f (σ i) • g i = ∑ i : ι, f i • g i ↔ Monovary (f ∘ ⇑σ) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : AddZeroClass δ<VAR>inst✝ : Min δ<VAR>C : Cost α β δ<VAR>x : α<VAR>xs : List α<VAR>ys : List β<GOAL>(suffixLevenshtein C (x :: xs) ys).val = levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>f : (i : ι) → F' i<GOAL>DifferentiableAt 𝕜 (fun f => f i) f
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>f : (i : ι) → F' i<VAR>h : DifferentiableAt 𝕜 (fun f i' => f i') f → ∀ (i : ι), DifferentiableAt 𝕜 (fun x => x i) f<GOAL>DifferentiableAt 𝕜 (fun f => f i) f
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>f : (i : ι) → F' i<VAR>h : DifferentiableAt 𝕜 (fun f i' => f i') f → ∀ (i : ι), DifferentiableAt 𝕜 (fun x => x i) f<GOAL>DifferentiableAt 𝕜 (fun f i' => f i') f
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra A K<VAR>inst✝⁹ : IsFractionRing A K<VAR>inst✝⁸ : Algebra B L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A B L<VAR>inst✝⁴ : IsScalarTower A K L<VAR>inst✝³ : IsIntegralClosure B A L<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : IsGalois K L<VAR>inst✝ : IsIntegrallyClosed A<VAR>x : B<GOAL>∏ σ : L ≃ₐ[K] L, ((galRestrict A K L B) σ) x = (algebraMap A B) (IsIntegralClosure.mk' A ((Algebra.norm K) ((algebraMap B L) x)) ⋯)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra A K<VAR>inst✝⁹ : IsFractionRing A K<VAR>inst✝⁸ : Algebra B L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A B L<VAR>inst✝⁴ : IsScalarTower A K L<VAR>inst✝³ : IsIntegralClosure B A L<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : IsGalois K L<VAR>inst✝ : IsIntegrallyClosed A<VAR>x : B<GOAL>(algebraMap B L) (∏ σ : L ≃ₐ[K] L, ((galRestrict A K L B) σ) x) = (algebraMap B L) ((algebraMap A B) (IsIntegralClosure.mk' A ((Algebra.norm K) ((algebraMap B L) x)) ⋯))
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra A K<VAR>inst✝⁹ : IsFractionRing A K<VAR>inst✝⁸ : Algebra B L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A B L<VAR>inst✝⁴ : IsScalarTower A K L<VAR>inst✝³ : IsIntegralClosure B A L<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : IsGalois K L<VAR>inst✝ : IsIntegrallyClosed A<VAR>x : B<GOAL>(algebraMap B L) (∏ σ : L ≃ₐ[K] L, ((galRestrict A K L B) σ) x) = ((algebraMap K L).comp (algebraMap A K)) (IsIntegralClosure.mk' A ((Algebra.norm K) ((algebraMap B L) x)) ⋯)
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing A<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Algebra R A<VAR>inst✝⁷ : Module R M₁<VAR>inst✝⁶ : Module A M₁<VAR>inst✝⁵ : SMulCommClass R A M₁<VAR>inst✝⁴ : SMulCommClass A R M₁<VAR>inst✝³ : IsScalarTower R A M₁<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Invertible 2<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticForm R M₂<GOAL>polarBilin (QuadraticForm.baseChange A Q) = BilinMap.baseChange A (polarBilin Q)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P✝ : Fin 3 → R<VAR>u✝ : R<VAR>hu : IsUnit u✝<VAR>u : R<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<GOAL>W'.Equation (u • P)