ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝²⁷ : AddCommMonoid M<VAR>inst✝²⁶ : AddCommMonoid N<VAR>inst✝²⁵ : CommSemiring R<VAR>inst✝²⁴ : CommSemiring S<VAR>inst✝²³ : Algebra R S<VAR>inst✝²² : Module R M<VAR>inst✝²¹ : Module R N<VAR>inst✝²⁰ : Module S N<VAR>inst✝¹⁹ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q✝ : Type u_3<VAR>inst✝¹⁸ : AddCommMonoid P<VAR>inst✝¹⁷ : Module R P<VAR>inst✝¹⁶ : AddCommMonoid Q✝<VAR>inst✝¹⁵ : Module S Q✝<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝¹⁴ : CommSemiring T<VAR>inst✝¹³ : Algebra R T<VAR>inst✝¹² : Algebra S T<VAR>inst✝¹¹ : IsScalarTower R S T<VAR>inst✝¹⁰ : AddCommMonoid O<VAR>inst✝⁹ : Module R O<VAR>inst✝⁸ : Module S O<VAR>inst✝⁷ : Module T O<VAR>inst✝⁶ : IsScalarTower S T O<VAR>inst✝⁵ : IsScalarTower R S O<VAR>inst✝⁴ : IsScalarTower R T O<VAR>f : M →ₗ[R] N<VAR>hf : IsBaseChange S f<VAR>g : N →ₗ[S] O<VAR>hg : IsBaseChange T g<VAR>Q : Type (max v₁ u_5 u_4)<VAR>inst✝³ : AddCommMonoid Q<VAR>inst✝² : Module R Q<VAR>inst✝¹ : Module T Q<VAR>inst✝ : IsScalarTower R T Q<VAR>i : M →ₗ[R] Q<VAR>this✝ : Module S Q := Module.compHom Q (algebraMap S T)<VAR>this : IsScalarTower S T Q<GOAL>∃! g', ↑R g' ∘ₗ ↑R g ∘ₗ f = i
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝²⁷ : AddCommMonoid M<VAR>inst✝²⁶ : AddCommMonoid N<VAR>inst✝²⁵ : CommSemiring R<VAR>inst✝²⁴ : CommSemiring S<VAR>inst✝²³ : Algebra R S<VAR>inst✝²² : Module R M<VAR>inst✝²¹ : Module R N<VAR>inst✝²⁰ : Module S N<VAR>inst✝¹⁹ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q✝ : Type u_3<VAR>inst✝¹⁸ : AddCommMonoid P<VAR>inst✝¹⁷ : Module R P<VAR>inst✝¹⁶ : AddCommMonoid Q✝<VAR>inst✝¹⁵ : Module S Q✝<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝¹⁴ : CommSemiring T<VAR>inst✝¹³ : Algebra R T<VAR>inst✝¹² : Algebra S T<VAR>inst✝¹¹ : IsScalarTower R S T<VAR>inst✝¹⁰ : AddCommMonoid O<VAR>inst✝⁹ : Module R O<VAR>inst✝⁸ : Module S O<VAR>inst✝⁷ : Module T O<VAR>inst✝⁶ : IsScalarTower S T O<VAR>inst✝⁵ : IsScalarTower R S O<VAR>inst✝⁴ : IsScalarTower R T O<VAR>f : M →ₗ[R] N<VAR>hf : IsBaseChange S f<VAR>g : N →ₗ[S] O<VAR>hg : IsBaseChange T g<VAR>Q : Type (max v₁ u_5 u_4)<VAR>inst✝³ : AddCommMonoid Q<VAR>inst✝² : Module R Q<VAR>inst✝¹ : Module T Q<VAR>inst✝ : IsScalarTower R T Q<VAR>i : M →ₗ[R] Q<VAR>this✝¹ : Module S Q := Module.compHom Q (algebraMap S T)<VAR>this✝ : IsScalarTower S T Q<VAR>this : IsScalarTower R S Q<GOAL>∃! g', ↑R g' ∘ₗ ↑R g ∘ₗ f = i
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝²⁷ : AddCommMonoid M<VAR>inst✝²⁶ : AddCommMonoid N<VAR>inst✝²⁵ : CommSemiring R<VAR>inst✝²⁴ : CommSemiring S<VAR>inst✝²³ : Algebra R S<VAR>inst✝²² : Module R M<VAR>inst✝²¹ : Module R N<VAR>inst✝²⁰ : Module S N<VAR>inst✝¹⁹ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q✝ : Type u_3<VAR>inst✝¹⁸ : AddCommMonoid P<VAR>inst✝¹⁷ : Module R P<VAR>inst✝¹⁶ : AddCommMonoid Q✝<VAR>inst✝¹⁵ : Module S Q✝<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝¹⁴ : CommSemiring T<VAR>inst✝¹³ : Algebra R T<VAR>inst✝¹² : Algebra S T<VAR>inst✝¹¹ : IsScalarTower R S T<VAR>inst✝¹⁰ : AddCommMonoid O<VAR>inst✝⁹ : Module R O<VAR>inst✝⁸ : Module S O<VAR>inst✝⁷ : Module T O<VAR>inst✝⁶ : IsScalarTower S T O<VAR>inst✝⁵ : IsScalarTower R S O<VAR>inst✝⁴ : IsScalarTower R T O<VAR>f : M →ₗ[R] N<VAR>hf : IsBaseChange S f<VAR>g : N →ₗ[S] O<VAR>hg : IsBaseChange T g<VAR>Q : Type (max v₁ u_5 u_4)<VAR>inst✝³ : AddCommMonoid Q<VAR>inst✝² : Module R Q<VAR>inst✝¹ : Module T Q<VAR>inst✝ : IsScalarTower R T Q<VAR>i : M →ₗ[R] Q<VAR>this✝¹ : Module S Q := Module.compHom Q (algebraMap S T)<VAR>this✝ : IsScalarTower S T Q<VAR>this : IsScalarTower R S Q<GOAL>∀ (y : O →ₗ[T] Q), (fun g' => ↑R g' ∘ₗ ↑R g ∘ₗ f = i) y → y = hg.lift (hf.lift i)
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝²⁷ : AddCommMonoid M<VAR>inst✝²⁶ : AddCommMonoid N<VAR>inst✝²⁵ : CommSemiring R<VAR>inst✝²⁴ : CommSemiring S<VAR>inst✝²³ : Algebra R S<VAR>inst✝²² : Module R M<VAR>inst✝²¹ : Module R N<VAR>inst✝²⁰ : Module S N<VAR>inst✝¹⁹ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q✝ : Type u_3<VAR>inst✝¹⁸ : AddCommMonoid P<VAR>inst✝¹⁷ : Module R P<VAR>inst✝¹⁶ : AddCommMonoid Q✝<VAR>inst✝¹⁵ : Module S Q✝<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝¹⁴ : CommSemiring T<VAR>inst✝¹³ : Algebra R T<VAR>inst✝¹² : Algebra S T<VAR>inst✝¹¹ : IsScalarTower R S T<VAR>inst✝¹⁰ : AddCommMonoid O<VAR>inst✝⁹ : Module R O<VAR>inst✝⁸ : Module S O<VAR>inst✝⁷ : Module T O<VAR>inst✝⁶ : IsScalarTower S T O<VAR>inst✝⁵ : IsScalarTower R S O<VAR>inst✝⁴ : IsScalarTower R T O<VAR>f : M →ₗ[R] N<VAR>hf : IsBaseChange S f<VAR>g : N →ₗ[S] O<VAR>hg : IsBaseChange T g<VAR>Q : Type (max v₁ u_5 u_4)<VAR>inst✝³ : AddCommMonoid Q<VAR>inst✝² : Module R Q<VAR>inst✝¹ : Module T Q<VAR>inst✝ : IsScalarTower R T Q<VAR>i : M →ₗ[R] Q<VAR>this✝¹ : Module S Q := Module.compHom Q (algebraMap S T)<VAR>this✝ : IsScalarTower S T Q<VAR>this : IsScalarTower R S Q<VAR>g' : O →ₗ[T] Q<VAR>e : ↑R g' ∘ₗ ↑R g ∘ₗ f = i<GOAL>g' = hg.lift (hf.lift i)
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝²⁷ : AddCommMonoid M<VAR>inst✝²⁶ : AddCommMonoid N<VAR>inst✝²⁵ : CommSemiring R<VAR>inst✝²⁴ : CommSemiring S<VAR>inst✝²³ : Algebra R S<VAR>inst✝²² : Module R M<VAR>inst✝²¹ : Module R N<VAR>inst✝²⁰ : Module S N<VAR>inst✝¹⁹ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q✝ : Type u_3<VAR>inst✝¹⁸ : AddCommMonoid P<VAR>inst✝¹⁷ : Module R P<VAR>inst✝¹⁶ : AddCommMonoid Q✝<VAR>inst✝¹⁵ : Module S Q✝<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝¹⁴ : CommSemiring T<VAR>inst✝¹³ : Algebra R T<VAR>inst✝¹² : Algebra S T<VAR>inst✝¹¹ : IsScalarTower R S T<VAR>inst✝¹⁰ : AddCommMonoid O<VAR>inst✝⁹ : Module R O<VAR>inst✝⁸ : Module S O<VAR>inst✝⁷ : Module T O<VAR>inst✝⁶ : IsScalarTower S T O<VAR>inst✝⁵ : IsScalarTower R S O<VAR>inst✝⁴ : IsScalarTower R T O<VAR>f : M →ₗ[R] N<VAR>hf : IsBaseChange S f<VAR>g : N →ₗ[S] O<VAR>hg : IsBaseChange T g<VAR>Q : Type (max v₁ u_5 u_4)<VAR>inst✝³ : AddCommMonoid Q<VAR>inst✝² : Module R Q<VAR>inst✝¹ : Module T Q<VAR>inst✝ : IsScalarTower R T Q<VAR>i : M →ₗ[R] Q<VAR>this✝¹ : Module S Q := Module.compHom Q (algebraMap S T)<VAR>this✝ : IsScalarTower S T Q<VAR>this : IsScalarTower R S Q<VAR>g' : O →ₗ[T] Q<VAR>e : ↑R g' ∘ₗ ↑R g ∘ₗ f = i<GOAL>↑R (↑S g' ∘ₗ g) ∘ₗ f = ↑R (↑S (hg.lift (hf.lift i)) ∘ₗ g) ∘ₗ f
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝²⁷ : AddCommMonoid M<VAR>inst✝²⁶ : AddCommMonoid N<VAR>inst✝²⁵ : CommSemiring R<VAR>inst✝²⁴ : CommSemiring S<VAR>inst✝²³ : Algebra R S<VAR>inst✝²² : Module R M<VAR>inst✝²¹ : Module R N<VAR>inst✝²⁰ : Module S N<VAR>inst✝¹⁹ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q✝ : Type u_3<VAR>inst✝¹⁸ : AddCommMonoid P<VAR>inst✝¹⁷ : Module R P<VAR>inst✝¹⁶ : AddCommMonoid Q✝<VAR>inst✝¹⁵ : Module S Q✝<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝¹⁴ : CommSemiring T<VAR>inst✝¹³ : Algebra R T<VAR>inst✝¹² : Algebra S T<VAR>inst✝¹¹ : IsScalarTower R S T<VAR>inst✝¹⁰ : AddCommMonoid O<VAR>inst✝⁹ : Module R O<VAR>inst✝⁸ : Module S O<VAR>inst✝⁷ : Module T O<VAR>inst✝⁶ : IsScalarTower S T O<VAR>inst✝⁵ : IsScalarTower R S O<VAR>inst✝⁴ : IsScalarTower R T O<VAR>f : M →ₗ[R] N<VAR>hf : IsBaseChange S f<VAR>g : N →ₗ[S] O<VAR>hg : IsBaseChange T g<VAR>Q : Type (max v₁ u_5 u_4)<VAR>inst✝³ : AddCommMonoid Q<VAR>inst✝² : Module R Q<VAR>inst✝¹ : Module T Q<VAR>inst✝ : IsScalarTower R T Q<VAR>i : M →ₗ[R] Q<VAR>this✝¹ : Module S Q := Module.compHom Q (algebraMap S T)<VAR>this✝ : IsScalarTower S T Q<VAR>this : IsScalarTower R S Q<VAR>g' : O →ₗ[T] Q<VAR>e : ↑R g' ∘ₗ ↑R g ∘ₗ f = i<GOAL>↑R (↑S g' ∘ₗ g) ∘ₗ f = ↑R g' ∘ₗ ↑R g ∘ₗ f
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : ∀ (a : α), Finite (β a)<VAR>h : IsEmpty α<GOAL>#(WType β) ≤ max (lift.{v, u} #α) ℵ₀
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : ∀ (a : α), Finite (β a)<VAR>h : IsEmpty α<GOAL>0 ≤ max (lift.{v, u} #α) ℵ₀
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : ∀ (a : α), Finite (β a)<VAR>hn : Nonempty α<VAR>m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀<GOAL>Order.succ 0 ≤ ⨆ a, m ^ lift.{u, v} #(β a)
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : ∀ (a : α), Finite (β a)<VAR>hn : Nonempty α<VAR>m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀<GOAL>1 ≤ ⨆ a, m ^ lift.{u, v} #(β a)
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : ∀ (a : α), Finite (β a)<VAR>m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀<VAR>a : α<GOAL>1 ≤ ⨆ a, m ^ lift.{u, v} #(β a)
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : ∀ (a : α), Finite (β a)<VAR>m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀<VAR>a : α<GOAL>1 ≤ m ^ lift.{u, v} #(β a)
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : ∀ (a : α), Finite (β a)<VAR>m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀<VAR>a : α<GOAL>?m.3905 ^ 0 ≤ m ^ lift.{u, v} #(β a)
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : ∀ (a : α), Finite (β a)<VAR>m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀<VAR>a : α<GOAL>Cardinal.{max u v}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>a b : α<VAR>P : α → Prop<VAR>m : α<VAR>h0 : P m<VAR>h1 : ∀ (n : α), m ≤ n → P n → P (succ n)<VAR>n : α<VAR>hmn : m ≤ n<GOAL>P n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>a b : α<VAR>P : α → Prop<VAR>m : α<VAR>h0 : P m<VAR>h1 : ∀ (n : α), m ≤ n → P n → P (succ n)<VAR>n : ℕ<VAR>hmn : m ≤ succ^[n] m<GOAL>P (succ^[n] m)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>b : ↥B<GOAL>of ↑(φ.symm b) = t⁻¹ * of ↑b * t
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>b : ↥B<GOAL>of ↑(φ.symm b) = t⁻¹ * (t * of ↑(φ.symm b))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<GOAL>volume {x | ∑ i : ι, ‖x i‖ ^ p < 1} = ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<GOAL>volume {x | ∑ i : ι, ‖x i‖ ^ p < 1} = ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ i : ι, ‖x i‖ ^ (ENNReal.ofReal p).toReal) ^ (1 / (ENNReal.ofReal p).toReal)<GOAL>volume {x | ∑ i : ι, ‖x i‖ ^ p < 1} = ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<GOAL>volume {x | ∑ i : ι, ‖x i‖ ^ p < 1} = ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<GOAL>volume {x | ∑ i : ι, ‖x i‖ ^ p < 1} = ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>nm_zero : ‖0‖ = 0<GOAL>volume {x | ∑ i : ι, ‖x i‖ ^ p < 1} = ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>nm_zero : ‖0‖ = 0<VAR>eq_zero : ∀ (x : ι → ℂ), ‖x‖ = 0 ↔ x = 0<GOAL>volume {x | ∑ i : ι, ‖x i‖ ^ p < 1} = ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>nm_zero : ‖0‖ = 0<VAR>eq_zero : ∀ (x : ι → ℂ), ‖x‖ = 0 ↔ x = 0<VAR>nm_neg : ∀ (x : ι → ℂ), ‖-x‖ = ‖x‖<GOAL>volume {x | ∑ i : ι, ‖x i‖ ^ p < 1} = ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>nm_zero : ‖0‖ = 0<VAR>eq_zero : ∀ (x : ι → ℂ), ‖x‖ = 0 ↔ x = 0<VAR>nm_neg : ∀ (x : ι → ℂ), ‖-x‖ = ‖x‖<VAR>nm_add : ∀ (x y : ι → ℂ), ‖x + y‖ ≤ ‖x‖ + ‖y‖<GOAL>volume {x | ∑ i : ι, ‖x i‖ ^ p < 1} = ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, ‖0 x‖ ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖(-x) x_1‖ ^ p) ^ (1 / p) = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℂ), (∑ x_1 : ι, ‖(x + y) x_1‖ ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) + (∑ x : ι, ‖y x‖ ^ p) ^ (1 / p)<GOAL>volume {x | ∑ i : ι, ‖x i‖ ^ p < 1} = ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, ‖0 x‖ ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖(-x) x_1‖ ^ p) ^ (1 / p) = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℂ), (∑ x_1 : ι, ‖(x + y) x_1‖ ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) + (∑ x : ι, ‖y x‖ ^ p) ^ (1 / p)<VAR>nm_smul : ∀ (r : ℝ) (x : ι → ℂ), ‖r • x‖ ≤ ‖r‖ * ‖x‖<GOAL>volume {x | ∑ i : ι, ‖x i‖ ^ p < 1} = ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, ‖0 x‖ ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖(-x) x_1‖ ^ p) ^ (1 / p) = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℂ), (∑ x_1 : ι, ‖(x + y) x_1‖ ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) + (∑ x : ι, ‖y x‖ ^ p) ^ (1 / p)<VAR>nm_smul : ∀ (r : ℝ) (x : ι → ℂ), (∑ x_1 : ι, abs ((r • x) x_1) ^ p) ^ (1 / p) ≤ ‖r‖ * (∑ x_1 : ι, abs (x x_1) ^ p) ^ (1 / p)<GOAL>volume {x | ∑ i : ι, ‖x i‖ ^ p < 1} = ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, ‖0 x‖ ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖(-x) x_1‖ ^ p) ^ (1 / p) = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℂ), (∑ x_1 : ι, ‖(x + y) x_1‖ ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) + (∑ x : ι, ‖y x‖ ^ p) ^ (1 / p)<VAR>nm_smul : ∀ (r : ℝ) (x : ι → ℂ), (∑ x_1 : ι, abs ((r • x) x_1) ^ p) ^ (1 / p) ≤ ‖r‖ * (∑ x_1 : ι, abs (x x_1) ^ p) ^ (1 / p)<VAR>x✝ : ι → ℂ<GOAL>∑ i : ι, ‖x✝ i‖ ^ p < 1 ↔ (∑ i : ι, ‖x✝ i‖ ^ p) ^ (1 / p) < 1
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, ‖0 x‖ ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖(-x) x_1‖ ^ p) ^ (1 / p) = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℂ), (∑ x_1 : ι, ‖(x + y) x_1‖ ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) + (∑ x : ι, ‖y x‖ ^ p) ^ (1 / p)<VAR>nm_smul : ∀ (r : ℝ) (x : ι → ℂ), (∑ x_1 : ι, abs ((r • x) x_1) ^ p) ^ (1 / p) ≤ ‖r‖ * (∑ x_1 : ι, abs (x x_1) ^ p) ^ (1 / p)<GOAL>(π * Real.Gamma (2 / p + 1)) ^ card ι = ∫ (x : ι → ℂ), rexp (-((∑ i : ι, ‖x i‖ ^ p) ^ (1 / p)) ^ p)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, ‖0 x‖ ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖(-x) x_1‖ ^ p) ^ (1 / p) = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℂ), (∑ x_1 : ι, ‖(x + y) x_1‖ ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) + (∑ x : ι, ‖y x‖ ^ p) ^ (1 / p)<VAR>nm_smul : ∀ (r : ℝ) (x : ι → ℂ), (∑ x_1 : ι, abs ((r • x) x_1) ^ p) ^ (1 / p) ≤ ‖r‖ * (∑ x_1 : ι, abs (x x_1) ^ p) ^ (1 / p)<GOAL>2 * ↑(card ι) / p + 1 = ↑(finrank ℝ (ι → ℂ)) / p + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b c : Ordinal.{u_4}<VAR>c0 : c ≠ 0<GOAL>a ≤ b / c ↔ c * a ≤ b
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M'✝ : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M'✝<VAR>inst✝⁶ : AddCommMonoid M''<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'✝<VAR>inst✝³ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>R' : Type u_8<VAR>M' : Type u_9<VAR>inst✝² : Semiring R'<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R' M'<VAR>hv : LinearIndependent R v<VAR>i : R' → R<VAR>j : M →+ M'<VAR>hi : ∀ (r : R'), i r = 0 → r = 0<VAR>hj : ∀ (m : M), j m = 0 → m = 0<VAR>hc : ∀ (r : R') (m : M), j (i r • m) = r • j m<GOAL>LinearIndependent R' (⇑j ∘ v)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M'✝ : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M'✝<VAR>inst✝⁶ : AddCommMonoid M''<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'✝<VAR>inst✝³ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>R' : Type u_8<VAR>M' : Type u_9<VAR>inst✝² : Semiring R'<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R' M'<VAR>hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0<VAR>i : R' → R<VAR>j : M →+ M'<VAR>hi : ∀ (r : R'), i r = 0 → r = 0<VAR>hj : ∀ (m : M), j m = 0 → m = 0<VAR>hc : ∀ (r : R') (m : M), j (i r • m) = r • j m<GOAL>∀ (s : Finset ι) (g : ι → R'), ∑ i ∈ s, g i • (⇑j ∘ v) i = 0 → ∀ i ∈ s, g i = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M'✝ : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M'✝<VAR>inst✝⁶ : AddCommMonoid M''<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'✝<VAR>inst✝³ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>R' : Type u_8<VAR>M' : Type u_9<VAR>inst✝² : Semiring R'<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R' M'<VAR>hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0<VAR>i : R' → R<VAR>j : M →+ M'<VAR>hi : ∀ (r : R'), i r = 0 → r = 0<VAR>hj : ∀ (m : M), j m = 0 → m = 0<VAR>hc : ∀ (r : R') (m : M), j (i r • m) = r • j m<VAR>S : Finset ι<VAR>r' : ι → R'<VAR>H : ∑ i ∈ S, r' i • (⇑j ∘ v) i = 0<VAR>s : ι<VAR>hs : s ∈ S<GOAL>r' s = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M'✝ : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M'✝<VAR>inst✝⁶ : AddCommMonoid M''<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'✝<VAR>inst✝³ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>R' : Type u_8<VAR>M' : Type u_9<VAR>inst✝² : Semiring R'<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R' M'<VAR>hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0<VAR>i : R' → R<VAR>j : M →+ M'<VAR>hi : ∀ (r : R'), i r = 0 → r = 0<VAR>hj : ∀ (m : M), j m = 0 → m = 0<VAR>hc : ∀ (r : R') (m : M), j (i r • m) = r • j m<VAR>S : Finset ι<VAR>r' : ι → R'<VAR>s : ι<VAR>hs : s ∈ S<VAR>H : j (∑ x ∈ S, i (r' x) • v x) = 0<GOAL>r' s = 0
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : MinimalAxioms α<VAR>s : Set α<VAR>a✝ b a : α<VAR>f : ι → α<GOAL>a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i
<VAR>x y : ℝ<GOAL>↑(cos (x + y)) = ↑(cos x * cos y - sin x * sin y)
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : K[X]<VAR>hfm : f.Monic<VAR>hgm : g.Monic<VAR>hf : Irreducible f<VAR>hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))<GOAL>Irreducible (f.comp g)
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : K[X]<VAR>hfm : f.Monic<VAR>hgm : g.Monic<VAR>hf : Irreducible f<VAR>hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))<VAR>hf' : f.natDegree ≠ 0<GOAL>Irreducible (f.comp g)
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : K[X]<VAR>hfm : f.Monic<VAR>hgm : g.Monic<VAR>hf : Irreducible f<VAR>hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))<VAR>hf' : f.natDegree ≠ 0<VAR>hg' : g.natDegree ≠ 0<GOAL>Irreducible (f.comp g)
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : K[X]<VAR>hfm : f.Monic<VAR>hgm : g.Monic<VAR>hf : Irreducible f<VAR>hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))<VAR>hf' : f.natDegree ≠ 0<VAR>hg' : g.natDegree ≠ 0<VAR>H₁ : f.comp g ≠ 0<GOAL>Irreducible (f.comp g)