ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>hzint : IsIntegral R z<VAR>this✝ : Module.Finite K L<VAR>P : R[X] := minpoly R B.gen<VAR>hei : P.IsEisensteinAt (Submodule.span R {p})<VAR>hndiv : ¬p ^ 2 ∣ P.coeff 0<VAR>hP : P = minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>this : NoZeroSMulDivisors R L<VAR>x✝ : L[X] := Polynomial.map (algebraMap R L) P<VAR>Q₁ : R[X]<VAR>hQ : (aeval B.gen).toRingHom Q₁ = p • z<VAR>Q : R[X] := Q₁ %ₘ P<VAR>hQ₁ : Q = Q₁ %ₘ P<GOAL>z ∈ adjoin R {B.gen}
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>hzint : IsIntegral R z<VAR>this✝ : Module.Finite K L<VAR>P : R[X] := minpoly R B.gen<VAR>hei : P.IsEisensteinAt (Submodule.span R {p})<VAR>hndiv : ¬p ^ 2 ∣ P.coeff 0<VAR>hP : P = minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>this : NoZeroSMulDivisors R L<VAR>x✝ : L[X] := Polynomial.map (algebraMap R L) P<VAR>Q₁ : R[X]<VAR>Q : R[X] := Q₁ %ₘ P<VAR>hQ₁ : Q = Q₁ %ₘ P<VAR>hQ : (aeval B.gen) Q = p • z<GOAL>z ∈ adjoin R {B.gen}
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>hzint : IsIntegral R z<VAR>this✝ : Module.Finite K L<VAR>P : R[X] := minpoly R B.gen<VAR>hei : P.IsEisensteinAt (Submodule.span R {p})<VAR>hndiv : ¬p ^ 2 ∣ P.coeff 0<VAR>hP : P = minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>this : NoZeroSMulDivisors R L<VAR>x✝ : L[X] := Polynomial.map (algebraMap R L) P<VAR>Q₁ : R[X]<VAR>Q : R[X] := Q₁ %ₘ P<VAR>hQ₁ : Q = Q₁ %ₘ P<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hQzero : ¬Q = 0<GOAL>z ∈ adjoin R {B.gen}
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>hzint : IsIntegral R z<VAR>this✝ : Module.Finite K L<VAR>P : R[X] := minpoly R B.gen<VAR>hei : P.IsEisensteinAt (Submodule.span R {p})<VAR>hndiv : ¬p ^ 2 ∣ P.coeff 0<VAR>hP : P = minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>this : NoZeroSMulDivisors R L<VAR>x✝ : L[X] := Polynomial.map (algebraMap R L) P<VAR>Q₁ : R[X]<VAR>Q : R[X] := Q₁ %ₘ P<VAR>hQ₁ : Q = Q₁ %ₘ P<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hQzero : ¬Q = 0<VAR>i : ℕ<GOAL>i ∈ range (Q.natDegree + 1) → p ∣ Q.coeff i
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>hzint : IsIntegral R z<VAR>this✝ : Module.Finite K L<VAR>P : R[X] := minpoly R B.gen<VAR>hei : P.IsEisensteinAt (Submodule.span R {p})<VAR>hndiv : ¬p ^ 2 ∣ P.coeff 0<VAR>hP : P = minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>this : NoZeroSMulDivisors R L<VAR>x✝ : L[X] := Polynomial.map (algebraMap R L) P<VAR>Q₁ : R[X]<VAR>Q : R[X] := Q₁ %ₘ P<VAR>hQ₁ : Q = Q₁ %ₘ P<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hQzero : ¬Q = 0<GOAL>0 ∈ range (Q.natDegree + 1) → p ∣ Q.coeff 0
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>hzint : IsIntegral R z<VAR>this✝ : Module.Finite K L<VAR>P : R[X] := minpoly R B.gen<VAR>hei : P.IsEisensteinAt (Submodule.span R {p})<VAR>hndiv : ¬p ^ 2 ∣ P.coeff 0<VAR>hP : P = minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>this : NoZeroSMulDivisors R L<VAR>x✝ : L[X] := Polynomial.map (algebraMap R L) P<VAR>Q₁ : R[X]<VAR>Q : R[X] := Q₁ %ₘ P<VAR>hQ₁ : Q = Q₁ %ₘ P<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hQzero : ¬Q = 0<VAR>j : ℕ<VAR>hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m<GOAL>j.succ ∈ range (Q.natDegree + 1) → p ∣ Q.coeff j.succ
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>y : E<VAR>ε : ℝ<VAR>a : E<GOAL>a ∈ ball y ε ↔ a ∈ {x | ‖x / y‖ < ε}
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝¹ : Category.{v', u'} A<VAR>H : J.OneHypercoverFamily<VAR>inst✝ : H.IsGenerating<VAR>P : Cᵒᵖ ⥤ A<VAR>hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J.sieves X<VAR>T : A<VAR>x y : T ⟶ P.obj (Opposite.op X)<VAR>h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.arrows f → x ≫ P.map f.op = y ≫ P.map f.op<GOAL>x = y
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝¹ : Category.{v', u'} A<VAR>H : J.OneHypercoverFamily<VAR>inst✝ : H.IsGenerating<VAR>P : Cᵒᵖ ⥤ A<VAR>hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J.sieves X<VAR>T : A<VAR>x y : T ⟶ P.obj (Opposite.op X)<VAR>h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.arrows f → x ≫ P.map f.op = y ≫ P.map f.op<VAR>E : J.OneHypercover X<VAR>hE : H E<VAR>le : E.sieve₀ ≤ S<GOAL>x = y
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a : A<VAR>X : C<GOAL>(shiftFunctorAdd' C 0 a a ⋯).inv.app X = (shiftFunctor C a).map ((shiftFunctorZero C A).hom.app X)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝⁴ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝³ : TopologicalSpace 𝕜<VAR>inst✝² : OrderTopology 𝕜<VAR>p a : 𝕜<VAR>hp : Fact (0 < p)<VAR>inst✝¹ : Archimedean 𝕜<VAR>inst✝ : TopologicalSpace B<VAR>f : 𝕜 → B<VAR>hf : f 0 = f p<VAR>hc : ContinuousOn f (Icc 0 p)<GOAL>f 0 = f (0 + p)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝⁴ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝³ : TopologicalSpace 𝕜<VAR>inst✝² : OrderTopology 𝕜<VAR>p a : 𝕜<VAR>hp : Fact (0 < p)<VAR>inst✝¹ : Archimedean 𝕜<VAR>inst✝ : TopologicalSpace B<VAR>f : 𝕜 → B<VAR>hf : f 0 = f p<VAR>hc : ContinuousOn f (Icc 0 p)<GOAL>ContinuousOn f (Icc 0 (0 + p))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq : p ≤ q<VAR>hf : AEStronglyMeasurable f μ<GOAL>eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq : p ≤ q<VAR>hf : AEStronglyMeasurable f μ<VAR>hq0_lt : 0 < q<GOAL>eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq : p ≤ q<VAR>hf : AEStronglyMeasurable f μ<VAR>hq0_lt : 0 < q<VAR>hpq_eq : ¬p = q<GOAL>eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq✝ : p ≤ q<VAR>hf : AEStronglyMeasurable f μ<VAR>hq0_lt : 0 < q<VAR>hpq_eq : ¬p = q<VAR>hpq : p < q<GOAL>eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq✝ : p ≤ q<VAR>hf : AEStronglyMeasurable f μ<VAR>hq0_lt : 0 < q<VAR>hpq_eq : ¬p = q<VAR>hpq : p < q<VAR>g : α → ℝ≥0∞ := fun x => 1<GOAL>eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq✝ : p ≤ q<VAR>hf : AEStronglyMeasurable f μ<VAR>hq0_lt : 0 < q<VAR>hpq_eq : ¬p = q<VAR>hpq : p < q<VAR>g : α → ℝ≥0∞ := fun x => 1<VAR>h_rw : ∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ<GOAL>eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq✝ : p ≤ q<VAR>hf : AEStronglyMeasurable f μ<VAR>hq0_lt : 0 < q<VAR>hpq_eq : ¬p = q<VAR>hpq : p < q<VAR>g : α → ℝ≥0∞ := fun x => 1<VAR>h_rw : ∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ<VAR>r : ℝ := p * q / (q - p)<GOAL>(∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * μ Set.univ ^ (1 / p - 1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq✝ : p ≤ q<VAR>hf : AEStronglyMeasurable f μ<VAR>hq0_lt : 0 < q<VAR>hpq_eq : ¬p = q<VAR>hpq : p < q<VAR>g : α → ℝ≥0∞ := fun x => 1<VAR>h_rw : ∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ<VAR>r : ℝ := p * q / (q - p)<VAR>hpqr : 1 / p = 1 / q + 1 / r<GOAL>(∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * μ Set.univ ^ (1 / p - 1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G''<VAR>inst✝² : NormedSpace ℝ G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T T' : Set α → E →L[ℝ] G''<VAR>hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>setToSimpleFunc T f ≤ setToSimpleFunc T' f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G''<VAR>inst✝² : NormedSpace ℝ G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T T' : Set α → E →L[ℝ] G''<VAR>hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>i : E<VAR>x✝ : i ∈ f.range<GOAL>(T (↑f ⁻¹' {i})) i ≤ (T' (↑f ⁻¹' {i})) i
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β → β<VAR>b : β<VAR>as : List α<GOAL>foldrIdx f b as = foldr (uncurry f) b as.enum
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>i j : Fin f.natDegree<GOAL>(Finsupp.comapDomain Fin.val (h.modByMonicHom (h.root ^ ↑i)).toFinsupp ⋯) j = (Finsupp.single i 1) j
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>i j : Fin f.natDegree<GOAL>(X ^ ↑i).toFinsupp ↑j = (Finsupp.single i 1) j
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>i j : Fin f.natDegree<GOAL>↑i < f.natDegree
<VAR>a : Ordinal.{u_1}<GOAL>0 ^ a = 1 - a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ ≤ ‖⟪x, y⟫_ℝ‖ * ‖⟪y, x⟫_ℝ‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪y, x⟫_ℝ * ⟪y, x⟫_ℝ ≤ ‖⟪y, x⟫_ℝ * ⟪y, x⟫_ℝ‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N✝ : Type u_5<VAR>inst✝⁸ : AddCommMonoid L<VAR>inst✝⁷ : TopologicalSpace L<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : AddCommMonoid N✝<VAR>inst✝³ : TopologicalSpace N✝<VAR>v✝ : VectorMeasure α M<VAR>w✝ : VectorMeasure α N✝<VAR>N : Type u_6<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : TopologicalSpace N<VAR>inst✝ : TopologicalAddGroup N<VAR>v : VectorMeasure α M<VAR>w : VectorMeasure α N<VAR>h : v ≪ᵥ w<VAR>s : Set α<VAR>hs : ↑(-w) s = 0<GOAL>↑v s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N✝ : Type u_5<VAR>inst✝⁸ : AddCommMonoid L<VAR>inst✝⁷ : TopologicalSpace L<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : AddCommMonoid N✝<VAR>inst✝³ : TopologicalSpace N✝<VAR>v✝ : VectorMeasure α M<VAR>w✝ : VectorMeasure α N✝<VAR>N : Type u_6<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : TopologicalSpace N<VAR>inst✝ : TopologicalAddGroup N<VAR>v : VectorMeasure α M<VAR>w : VectorMeasure α N<VAR>h : v ≪ᵥ w<VAR>s : Set α<VAR>hs : ↑w s = 0<GOAL>↑v s = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>p : α → Prop<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>(∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ.restrict {x | f x ≠ 0}, p x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>p : α → Prop<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>(∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≠ 0} → p x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>p : α → Prop<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>NullMeasurableSet {x | f x ≠ 0} μ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f✝ : β → α<VAR>t : Finset γ<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>f : β → γ → α<VAR>a : α<GOAL>(s.sup' hs fun b => t.sup' ht (f b)) ≤ a ↔ (t.sup' ht fun c => s.sup' hs fun b => f b c) ≤ a
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M : NFA α σ<VAR>x : List α<GOAL>x ∈ M.accepts ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (extendScalars f).obj X ⟶ Y<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<GOAL>HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g) = g
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (extendScalars f).obj X ⟶ Y<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<GOAL>∀ (x : ↑((extendScalars f).obj X)), (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g)) x = g x
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (extendScalars f).obj X ⟶ Y<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<VAR>z : ↑((extendScalars f).obj X)<GOAL>(HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g)) z = g z
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (extendScalars f).obj X ⟶ Y<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<GOAL>(HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g)) 0 = g 0
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (extendScalars f).obj X ⟶ Y<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<VAR>x : ↑((restrictScalars f).obj (mk S))<VAR>s : ↑X<GOAL>(HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g)) (x ⊗ₜ[R] s) = g (x ⊗ₜ[R] s)
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (extendScalars f).obj X ⟶ Y<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<VAR>z1 z2 : ↑((restrictScalars f).obj (mk S)) ⊗[R] ↑X<VAR>ih1 : (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g)) z1 = g z1<VAR>ih2 : (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g)) z2 = g z2<GOAL>(HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g)) (z1 + z2) = g (z1 + z2)
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : X ⟶ (restrictScalars f).obj Y<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<GOAL>HomEquiv.toRestrictScalars f (HomEquiv.fromExtendScalars f g) = g
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : X ⟶ (restrictScalars f).obj Y<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<GOAL>∀ (x : ↑X), (HomEquiv.toRestrictScalars f (HomEquiv.fromExtendScalars f g)) x = g x
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : X ⟶ (restrictScalars f).obj Y<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<VAR>x : ↑X<GOAL>(HomEquiv.toRestrictScalars f (HomEquiv.fromExtendScalars f g)) x = g x
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : X ⟶ (restrictScalars f).obj Y<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<VAR>x : ↑X<GOAL>({ toFun := fun s => HomEquiv.evalAt f s g, map_add' := ⋯ } 1).toAddHom x = g x
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : X ⟶ (restrictScalars f).obj Y<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<VAR>x : ↑X<GOAL>1 • g x = g x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>i : ChooseBasisIndex ℤ (𝓞 K)<GOAL>((latticeBasis K).repr ((mixedEmbedding K) x)) i = ↑(((integralBasis K).repr x) i)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>i : ChooseBasisIndex ℤ (𝓞 K)<GOAL>((Basis.restrictScalars ℚ (latticeBasis K)).repr ⟨(mixedEmbedding K) x, ⋯⟩) i = ((integralBasis K).repr x) i
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>i : ChooseBasisIndex ℤ (𝓞 K)<VAR>f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) := LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (mixedEmbedding K).toRatAlgHom.toLinearMap ⋯<GOAL>((Basis.restrictScalars ℚ (latticeBasis K)).repr ⟨(mixedEmbedding K) x, ⋯⟩) i = ((integralBasis K).repr x) i
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>i : ChooseBasisIndex ℤ (𝓞 K)<VAR>f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) := LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (mixedEmbedding K).toRatAlgHom.toLinearMap ⋯<GOAL>↑(Basis.restrictScalars ℚ (latticeBasis K)).repr ∘ₗ f = ↑(integralBasis K).repr
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>i✝ : ChooseBasisIndex ℤ (𝓞 K)<VAR>f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) := LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (mixedEmbedding K).toRatAlgHom.toLinearMap ⋯<VAR>i : ChooseBasisIndex ℤ (𝓞 K)<GOAL>(↑(Basis.restrictScalars ℚ (latticeBasis K)).repr ∘ₗ f) ((integralBasis K) i) = ↑(integralBasis K).repr ((integralBasis K) i)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>i✝ : ChooseBasisIndex ℤ (𝓞 K)<VAR>f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) := LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (mixedEmbedding K).toRatAlgHom.toLinearMap ⋯<VAR>i : ChooseBasisIndex ℤ (𝓞 K)<VAR>this : f ((integralBasis K) i) = (Basis.restrictScalars ℚ (latticeBasis K)) i<GOAL>(↑(Basis.restrictScalars ℚ (latticeBasis K)).repr ∘ₗ f) ((integralBasis K) i) = ↑(integralBasis K).repr ((integralBasis K) i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>f : α → β<GOAL>range (map f) = {l | ∀ x ∈ l, x ∈ range f}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ : List α<VAR>f : α → β<VAR>l : List β<VAR>hl : l ∈ {l | ∀ x ∈ l, x ∈ range f}<GOAL>l ∈ range (map f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ : List α<VAR>f : α → β<VAR>a : β<VAR>l : List β<VAR>ihl : l ∈ {l | ∀ x ∈ l, x ∈ range f} → l ∈ range (map f)<VAR>hl : a :: l ∈ {l | ∀ x ∈ l, x ∈ range f}<GOAL>a :: l ∈ range (map f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ : List α<VAR>f : α → β<VAR>a : β<VAR>l : List α<VAR>ihl : map f l ∈ {l | ∀ x ∈ l, x ∈ range f} → map f l ∈ range (map f)<VAR>hl : a :: map f l ∈ {l | ∀ x ∈ l, x ∈ range f}<GOAL>a :: map f l ∈ range (map f)