ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<GOAL>↑(⊥.prod ⊥) = ↑⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>s : Set α<VAR>h : ∃ a ∈ s, a ∈ p.support<VAR>a : α<VAR>ha : a ∉ s<GOAL>(p.filter s h) a = 0
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : a.primeFactorsList ~ b.primeFactorsList<GOAL>a = b
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type w<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : Small.{v, u} R<GOAL>Flat R M ↔ ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (L : N →ₗ[R] N'), Function.Injective ⇑L → Function.Injective ⇑(rTensor M L)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.L₀'.Exact
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₀'.X₂), x₂ ≫ S.L₀'.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀'.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A : C<VAR>x₂ : A ⟶ S.P<VAR>hx₂ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = 0<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀'.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A : C<VAR>x₂ : A ⟶ S.P<VAR>hx₂ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = 0<VAR>A' : C<VAR>π : A' ⟶ A<VAR>hπ : Epi π<VAR>x₁ : A' ⟶ S.L₁.X₁<VAR>fac : π ≫ x₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃ = x₁ ≫ S.L₁.f<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀'.f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>x : E<VAR>hx : x ∈ s<GOAL>x ∈ 1 • s
<VAR>G₀ : Type u<VAR>M₀ : Type u_1<VAR>M₀' : Type u_2<VAR>G₀' : Type u_3<VAR>inst✝² : CommMonoidWithZero M₀<VAR>inst✝¹ : Div M₀<VAR>inst✝ : MulDivCancelClass M₀<VAR>a b✝ b : M₀<VAR>ha : a ≠ 0<GOAL>a * b / a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>f : β → α<VAR>s : Cycle β<VAR>a : β<VAR>l : List β<GOAL>Chain r (map f (Quotient.mk'' (a :: l))) ↔ Chain (fun a b => r (f a) (f b)) (Quotient.mk'' (a :: l))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>f : β → α<VAR>s : Cycle β<VAR>a : β<VAR>l : List β<GOAL>List.Chain r (f a) (List.map f l ++ [f a]) ↔ List.Chain (fun a b => r (f a) (f b)) a (l ++ [a])
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>f : β → α<VAR>s : Cycle β<VAR>a : β<VAR>l : List β<GOAL>List.Chain (fun a b => r (f a) (f b)) a (l.concat a) ↔ List.Chain (fun a b => r (f a) (f b)) a (l ++ [a])
<VAR>α : Type u_1<VAR>inst✝³ : Semifield α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : PosMulReflectLT α<VAR>inst✝ : ZeroLEOneClass α<VAR>a✝ b a : α<VAR>ha : 0 < a<GOAL>a * 0 < a * a⁻¹
<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>hP : W'.Equation P<GOAL>W'.addX P (W'.neg P) = W'.dblZ P ^ 2
<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>hP : W'.Equation P<GOAL>P x * P x ^ 2 * P z ^ 2 - 2 * P y * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z * P z + P x ^ 2 * P x * P z ^ 2 - W'.a₁ * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 2 * P z - W'.a₁ * P y * P x * P z * P z ^ 2 + 2 * W'.a₂ * P x * P x * P z ^ 2 * P z ^ 2 - W'.a₃ * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 4 * P z - W'.a₃ * P y * P z * P z ^ 4 + W'.a₄ * P x * P z ^ 4 * P z ^ 2 + W'.a₄ * P x * P z ^ 2 * P z ^ 4 + 2 * W'.a₆ * P z ^ 4 * P z ^ 4 = (P z * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3))) ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p✝ : G.Walk a b<VAR>p : G.Walk a a<VAR>hp : p.IsHamiltonianCycle<GOAL>List.count a p.support = 2
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>a : R<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>(coeff R n) ((C R) a) = 0
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>bernoulli' n = (-1) ^ n * bernoulli n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin b<GOAL>Ioc a (pred b) = Ioo a b
<VAR>u✝ : Lean.Level<VAR>arg : Q(Type u✝)<VAR>sα✝ : Q(CommSemiring «$arg»)<VAR>u : Lean.Level<VAR>α : Q(Type u)<VAR>sα : Q(CommSemiring «$α»)<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>a a' a₁ a₂ a₃ b b' b₁✝ b₂✝ b₃ c : R<VAR>b₁ b₂ : ℕ<GOAL>a ^ (b₁ + b₂) = a ^ b₁ * a ^ b₂
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 1<VAR>hb : b % 2 = 0<VAR>hc : b / 2 = c<VAR>hr : jacobiSymNat a c = r<GOAL>jacobiSymNat a b = r
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 1<VAR>hb : b % 2 = 0<VAR>hc : b / 2 = c<VAR>hr : jacobiSymNat a c = r<VAR>ha' : legendreSym 2 ↑a = 1<GOAL>jacobiSymNat a b = r
<VAR>a b : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 1<VAR>hb : b % 2 = 0<VAR>ha' : legendreSym 2 ↑a = 1<VAR>hc : b / 2 = 0<VAR>hr : jacobiSymNat a 0 = r<GOAL>jacobiSymNat a b = r
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 1<VAR>hb : b % 2 = 0<VAR>hc : b / 2 = c<VAR>hr : jacobiSymNat a c = r<VAR>ha' : legendreSym 2 ↑a = 1<VAR>hc' : c ≠ 0<GOAL>jacobiSymNat a b = r
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>hp0 : p ≠ 0<GOAL>p.divX.degree < p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>hp0 : p ≠ 0<VAR>this : Nontrivial R<GOAL>p.divX.degree < p.degree
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>v1 v3 : ℕ<GOAL>padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f (max v1 (max (stationaryPoint hf) v3)))
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>v1 v3 : ℕ<GOAL>stationaryPoint hf ≤ max v1 (max (stationaryPoint hf) v3)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>v1 v3 : ℕ<GOAL>stationaryPoint hf ≤ stationaryPoint hf
<VAR>X Y : CommRingCat<VAR>f : X ⟶ Y<GOAL>(𝟭 CommRingCat).map f ≫ ((fun R => asIso (toSpecΓ R)) Y).hom = ((fun R => asIso (toSpecΓ R)) X).hom ≫ (Spec.toLocallyRingedSpace.rightOp ⋙ Γ).map f
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a✝ a : α<VAR>ha : a ∉ s<GOAL>s ⋖ cons a s ha
<VAR>J : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>G : J ⥤ C<VAR>α✝ : F✝ ⟶ G<VAR>inst✝ : HasLimitsOfShape K C<VAR>F : J ⥤ C<VAR>E₁ E₂ : K ⥤ J<VAR>α : E₁ ⟶ E₂<VAR>j✝ : K<GOAL>pre F E₂ ≫ π (E₂ ⋙ F) j✝ = (pre F E₁ ≫ lim.map (whiskerRight α F)) ≫ π (E₂ ⋙ F) j✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>g : α → γ<VAR>hg : HasFiniteIntegral g μ<VAR>h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖<GOAL>HasFiniteIntegral f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>g : α → γ<VAR>h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖<VAR>hg : ∫⁻ (a : α), ENNReal.ofReal ‖g a‖ ∂μ < ⊤<GOAL>∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ⊤
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : LieAlgebra.IsNilpotent R L<VAR>χ : L → R<VAR>hχ : weightSpace M χ ≠ ⊥<GOAL>0 < finrank R ↥↑(weightSpace M χ)
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : SeminormedAddCommGroup V<VAR>inst✝⁷ : PseudoMetricSpace P<VAR>inst✝⁶ : NormedAddTorsor V P<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : MetricSpace Q<VAR>inst✝³ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<VAR>p q : P<GOAL>dist ((Equiv.pointReflection p) q) p = dist p q
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>h₁ : a₁ ≤ b₁<GOAL>Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → E<GOAL>Memℒp f 0 μ ↔ AEStronglyMeasurable f μ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : SeminormFamily 𝕜 (E →WOT[𝕜]F) (E × NormedSpace.Dual 𝕜 F) := seminormFamily 𝕜 E F<GOAL>(𝓝 0).HasBasis (seminormFamily 𝕜 E F).basisSets id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : SeminormFamily 𝕜 (E →WOT[𝕜]F) (E × NormedSpace.Dual 𝕜 F) := seminormFamily 𝕜 E F<GOAL>(Filter.comap (⇑(inducingFn 𝕜 E F)) (Filter.pi fun i => 𝓝 ((inducingFn 𝕜 E F) 0 i))).HasBasis (seminormFamily 𝕜 E F).basisSets id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : SeminormFamily 𝕜 (E →WOT[𝕜]F) (E × NormedSpace.Dual 𝕜 F) := seminormFamily 𝕜 E F<GOAL>(Filter.comap (⇑(inducingFn 𝕜 E F)) (Filter.pi fun i => 𝓝 0)).HasBasis (seminormFamily 𝕜 E F).basisSets id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : SeminormFamily 𝕜 (E →WOT[𝕜]F) (E × NormedSpace.Dual 𝕜 F) := seminormFamily 𝕜 E F<VAR>h : (Filter.comap (⇑(inducingFn 𝕜 E F)) (Filter.pi fun x => 𝓝 0)).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun i => ⇑(inducingFn 𝕜 E F) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)<GOAL>(Filter.comap (⇑(inducingFn 𝕜 E F)) (Filter.pi fun i => 𝓝 0)).HasBasis (seminormFamily 𝕜 E F).basisSets id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : SeminormFamily 𝕜 (E →WOT[𝕜]F) (E × NormedSpace.Dual 𝕜 F) := seminormFamily 𝕜 E F<VAR>h : (Filter.comap (⇑(inducingFn 𝕜 E F)) (Filter.pi fun x => 𝓝 0)).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun i => ⇑(inducingFn 𝕜 E F) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)<GOAL>∀ (i : Set (E × NormedSpace.Dual 𝕜 F) × (E × NormedSpace.Dual 𝕜 F → ℝ)), (i.1.Finite ∧ ∀ i_1 ∈ i.1, 0 < i.2 i_1) → ∃ i', (seminormFamily 𝕜 E F).basisSets i' ∧ id i' ⊆ ⇑(inducingFn 𝕜 E F) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : SeminormFamily 𝕜 (E →WOT[𝕜]F) (E × NormedSpace.Dual 𝕜 F) := seminormFamily 𝕜 E F<VAR>h : (Filter.comap (⇑(inducingFn 𝕜 E F)) (Filter.pi fun x => 𝓝 0)).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun i => ⇑(inducingFn 𝕜 E F) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)<GOAL>∀ (i' : Set (E →WOT[𝕜]F)), (seminormFamily 𝕜 E F).basisSets i' → id i' ∈ Filter.comap (⇑(inducingFn 𝕜 E F)) (Filter.pi fun x => 𝓝 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>u v : E<GOAL>⟪↑((orthogonalProjection K) u), v⟫_𝕜 = ⟪u, ↑((orthogonalProjection K) v)⟫_𝕜
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifIntegrable f p μ<VAR>hg : UnifIntegrable g p μ<VAR>hp : 1 ≤ p<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifIntegrable f p μ<VAR>hg : UnifIntegrable g p μ<VAR>hp : 1 ≤ p<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε2 : 0 < ε / 2<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifIntegrable f p μ<VAR>hg : UnifIntegrable g p μ<VAR>hp : 1 ≤ p<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε2 : 0 < ε / 2<VAR>δ₁ : ℝ<VAR>hδ₁_pos : 0 < δ₁<VAR>hfδ₁ : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)<VAR>δ₂ : ℝ<VAR>hδ₂_pos : 0 < δ₂<VAR>hgδ₂ : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifIntegrable f p μ<VAR>hg : UnifIntegrable g p μ<VAR>hp : 1 ≤ p<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε2 : 0 < ε / 2<VAR>δ₁ : ℝ<VAR>hδ₁_pos : 0 < δ₁<VAR>hfδ₁ : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)<VAR>δ₂ : ℝ<VAR>hδ₂_pos : 0 < δ₂<VAR>hgδ₂ : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)<VAR>i : ι<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)<GOAL>eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifIntegrable f p μ<VAR>hg : UnifIntegrable g p μ<VAR>hp : 1 ≤ p<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε2 : 0 < ε / 2<VAR>δ₁ : ℝ<VAR>hδ₁_pos : 0 < δ₁<VAR>hfδ₁ : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)<VAR>δ₂ : ℝ<VAR>hδ₂_pos : 0 < δ₂<VAR>hgδ₂ : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)<VAR>i : ι<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)<GOAL>eLpNorm (s.indicator (f i) + s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifIntegrable f p μ<VAR>hg : UnifIntegrable g p μ<VAR>hp : 1 ≤ p<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε2 : 0 < ε / 2<VAR>δ₁ : ℝ<VAR>hδ₁_pos : 0 < δ₁<VAR>hfδ₁ : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)<VAR>δ₂ : ℝ<VAR>hδ₂_pos : 0 < δ₂<VAR>hgδ₂ : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)<VAR>i : ι<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)<GOAL>eLpNorm (s.indicator (f i)) p μ + eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifIntegrable f p μ<VAR>hg : UnifIntegrable g p μ<VAR>hp : 1 ≤ p<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε2 : 0 < ε / 2<VAR>δ₁ : ℝ<VAR>hδ₁_pos : 0 < δ₁<VAR>hfδ₁ : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)<VAR>δ₂ : ℝ<VAR>hδ₂_pos : 0 < δ₂<VAR>hgδ₂ : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)<VAR>i : ι<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)<VAR>hε_halves : ENNReal.ofReal ε = ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2)<GOAL>eLpNorm (s.indicator (f i)) p μ + eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifIntegrable f p μ<VAR>hg : UnifIntegrable g p μ<VAR>hp : 1 ≤ p<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε2 : 0 < ε / 2<VAR>δ₁ : ℝ<VAR>hδ₁_pos : 0 < δ₁<VAR>hfδ₁ : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)<VAR>δ₂ : ℝ<VAR>hδ₂_pos : 0 < δ₂<VAR>hgδ₂ : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)<VAR>i : ι<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)<VAR>hε_halves : ENNReal.ofReal ε = ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2)<GOAL>eLpNorm (s.indicator (f i)) p μ + eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>v : E<GOAL>(reflection Kᗮ) v = -(reflection K) v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>v : E<GOAL>2 • v - 2 • ↑((orthogonalProjection K) v) - v = v - 2 • ↑((orthogonalProjection K) v)
<VAR>k : ℕ<GOAL>mersenne k + 1 = 2 ^ k
<VAR>k : ℕ<GOAL>1 ≤ 2 ^ k
<VAR>G : Type u_1<VAR>inst✝ : Mul G<VAR>A B : Finset G<VAR>h : 1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2<VAR>hA : A.Nonempty<VAR>hB : B.Nonempty<VAR>hc : ¬(A.card ≤ 1 ∧ B.card ≤ 1)<GOAL>∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
<VAR>G : Type u_1<VAR>inst✝ : Mul G<VAR>A B : Finset G<VAR>h : 1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2<VAR>hA : A.Nonempty<VAR>hB : B.Nonempty<VAR>hc : 1 < A.card ∨ 1 < B.card<GOAL>∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
<VAR>G : Type u_1<VAR>inst✝ : Mul G<VAR>A B : Finset G<VAR>h : 1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2<VAR>hA : 0 < A.card<VAR>hB : 0 < B.card<VAR>hc : 1 < A.card ∨ 1 < B.card<GOAL>∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
<VAR>G : Type u_1<VAR>inst✝ : Mul G<VAR>A B : Finset G<VAR>h : 1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2<VAR>hA : 0 < A.card<VAR>hB : 0 < B.card<VAR>hc : 1 < A.card ∨ 1 < B.card<VAR>p : G × G<VAR>hp : p ∈ A ×ˢ B<VAR>w✝ : G × G<VAR>left✝¹ : w✝ ∈ A ×ˢ B<VAR>left✝ : p ≠ w✝<VAR>hu : UniqueMul A B p.1 p.2<VAR>right✝ : UniqueMul A B w✝.1 w✝.2<GOAL>∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
<VAR>G : Type u_1<VAR>inst✝ : Mul G<VAR>A B : Finset G<VAR>h : 1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2<VAR>hA : 0 < A.card<VAR>hB : 0 < B.card<VAR>hc : 1 < A.card ∨ 1 < B.card<VAR>p : G × G<VAR>hp : p.1 ∈ A ∧ p.2 ∈ B<VAR>w✝ : G × G<VAR>left✝¹ : w✝ ∈ A ×ˢ B<VAR>left✝ : p ≠ w✝<VAR>hu : UniqueMul A B p.1 p.2<VAR>right✝ : UniqueMul A B w✝.1 w✝.2<GOAL>∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>m : M<GOAL>‖(mk' S) m‖ = 0 ↔ m ∈ closure ↑S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>m : M<GOAL>(↑S).Nonempty
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>w : InfinitePlace K<VAR>c : ℝ<GOAL>(normAtPlace w) (fun x => c, fun x => ↑c) = |c|
<VAR>o : Ordinal.{u_1}<VAR>ho : o ≠ 0<GOAL>CNF 1 o = [(0, o)]
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : R[X]<VAR>hn : f.natDegree < n<GOAL>trunc n ↑f = f
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : R[X]<VAR>hn : f.natDegree < n<GOAL>↑(trunc n ↑f) = ↑f
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : R[X]<VAR>hn : f.natDegree < n<VAR>m : ℕ<GOAL>(coeff R m) ↑(trunc n ↑f) = (coeff R m) ↑f
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : R[X]<VAR>hn : f.natDegree < n<VAR>m : ℕ<GOAL>(if m < n then (coeff R m) ↑f else 0) = (coeff R m) ↑f
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : R[X]<VAR>hn : f.natDegree < n<VAR>m : ℕ<VAR>h✝ : ¬m < n<GOAL>0 = (coeff R m) ↑f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g : α → β<VAR>μ ν : Measure α<VAR>s t : Set α<GOAL>AEMeasurable f (μ.restrict (s ∪ t)) ↔ AEMeasurable f (μ.restrict s) ∧ AEMeasurable f (μ.restrict t)
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α : Type v<VAR>inst✝¹ : CommRing α<VAR>inst✝ : StarRing α<VAR>A : Matrix n n α<GOAL>A ∈ unitaryGroup n α ↔ A * star A = 1
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α : Type v<VAR>inst✝¹ : CommRing α<VAR>inst✝ : StarRing α<VAR>A : Matrix n n α<VAR>hA : A * star A = 1<GOAL>star A * A = 1
<VAR>z τ : ℂ<GOAL>jacobiTheta₂ (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * jacobiTheta₂ z τ
<VAR>z τ : ℂ<GOAL>jacobiTheta₂ (z + τ) τ = ∑' (c : ℤ), cexp (-↑π * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1) c) z τ
<VAR>z τ : ℂ<VAR>n : ℤ<GOAL>jacobiTheta₂_term n (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1) n) z τ