ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝²⁶ : CommRing R<VAR>S : Type v<VAR>inst✝²⁵ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝²⁴ : Algebra R S<VAR>K : Type u_1<VAR>inst✝²³ : Field K<VAR>inst✝²² : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝²¹ : Field L<VAR>inst✝²⁰ : Algebra S L<VAR>inst✝¹⁹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : Module R V<VAR>inst✝¹⁶ : Module K V<VAR>inst✝¹⁵ : IsScalarTower R K V<VAR>inst✝¹⁴ : AddCommGroup V'<VAR>inst✝¹³ : Module R V'<VAR>inst✝¹² : Module S V'<VAR>inst✝¹¹ : IsScalarTower R S V'<VAR>inst✝¹⁰ : AddCommGroup V''<VAR>inst✝⁹ : Module R V''<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsDomain S<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : IsNoetherian R S<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : NoZeroSMulDivisors R K<VAR>hp : p ≠ ⊤<VAR>b : Set S<VAR>hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map (algebraMap R S) p) = ⊤<VAR>hRL : Function.Injective ⇑(algebraMap R L)<VAR>M : Submodule R S := Submodule.span R b<VAR>h : Module.Finite R (S ⧸ M) := Module.Finite.of_surjective M.mkQ (Submodule.Quotient.mk_surjective M)<VAR>n : ℕ<VAR>a : Fin n → S ⧸ M<VAR>ha : Submodule.span R (Set.range a) = ⊤<VAR>smul_top_eq : p • ⊤ = ⊤<GOAL>Submodule.span K (⇑(algebraMap S L) '' b) = ⊤
<VAR>R : Type u<VAR>inst✝²⁶ : CommRing R<VAR>S : Type v<VAR>inst✝²⁵ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝²⁴ : Algebra R S<VAR>K : Type u_1<VAR>inst✝²³ : Field K<VAR>inst✝²² : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝²¹ : Field L<VAR>inst✝²⁰ : Algebra S L<VAR>inst✝¹⁹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : Module R V<VAR>inst✝¹⁶ : Module K V<VAR>inst✝¹⁵ : IsScalarTower R K V<VAR>inst✝¹⁴ : AddCommGroup V'<VAR>inst✝¹³ : Module R V'<VAR>inst✝¹² : Module S V'<VAR>inst✝¹¹ : IsScalarTower R S V'<VAR>inst✝¹⁰ : AddCommGroup V''<VAR>inst✝⁹ : Module R V''<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsDomain S<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : IsNoetherian R S<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : NoZeroSMulDivisors R K<VAR>hp : p ≠ ⊤<VAR>b : Set S<VAR>hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map (algebraMap R S) p) = ⊤<VAR>hRL : Function.Injective ⇑(algebraMap R L)<VAR>M : Submodule R S := Submodule.span R b<VAR>h : Module.Finite R (S ⧸ M) := Module.Finite.of_surjective M.mkQ (Submodule.Quotient.mk_surjective M)<VAR>n : ℕ<VAR>a : Fin n → S ⧸ M<VAR>ha : Submodule.span R (Set.range a) = ⊤<VAR>smul_top_eq : p • ⊤ = ⊤<VAR>exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x<VAR>A' : Fin n → Fin n → R<VAR>hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p<VAR>hA' : ∀ (i : Fin n), ∑ i_1 : Fin n, A' i i_1 • a i_1 = a i<VAR>A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1<VAR>B : Matrix (Fin n) (Fin n) R := A.adjugate<GOAL>Submodule.span K (⇑(algebraMap S L) '' b) = ⊤
<VAR>R : Type u<VAR>inst✝²⁶ : CommRing R<VAR>S : Type v<VAR>inst✝²⁵ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝²⁴ : Algebra R S<VAR>K : Type u_1<VAR>inst✝²³ : Field K<VAR>inst✝²² : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝²¹ : Field L<VAR>inst✝²⁰ : Algebra S L<VAR>inst✝¹⁹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : Module R V<VAR>inst✝¹⁶ : Module K V<VAR>inst✝¹⁵ : IsScalarTower R K V<VAR>inst✝¹⁴ : AddCommGroup V'<VAR>inst✝¹³ : Module R V'<VAR>inst✝¹² : Module S V'<VAR>inst✝¹¹ : IsScalarTower R S V'<VAR>inst✝¹⁰ : AddCommGroup V''<VAR>inst✝⁹ : Module R V''<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsDomain S<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : IsNoetherian R S<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : NoZeroSMulDivisors R K<VAR>hp : p ≠ ⊤<VAR>b : Set S<VAR>hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map (algebraMap R S) p) = ⊤<VAR>hRL : Function.Injective ⇑(algebraMap R L)<VAR>M : Submodule R S := Submodule.span R b<VAR>h : Module.Finite R (S ⧸ M) := Module.Finite.of_surjective M.mkQ (Submodule.Quotient.mk_surjective M)<VAR>n : ℕ<VAR>a : Fin n → S ⧸ M<VAR>ha : Submodule.span R (Set.range a) = ⊤<VAR>smul_top_eq : p • ⊤ = ⊤<VAR>exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x<VAR>A' : Fin n → Fin n → R<VAR>hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p<VAR>hA' : ∀ (i : Fin n), ∑ i_1 : Fin n, A' i i_1 • a i_1 = a i<VAR>A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1<VAR>B : Matrix (Fin n) (Fin n) R := A.adjugate<VAR>A_smul : ∀ (i : Fin n), ∑ j : Fin n, A i j • a j = 0<GOAL>Submodule.span K (⇑(algebraMap S L) '' b) = ⊤
<VAR>R : Type u<VAR>inst✝²⁶ : CommRing R<VAR>S : Type v<VAR>inst✝²⁵ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝²⁴ : Algebra R S<VAR>K : Type u_1<VAR>inst✝²³ : Field K<VAR>inst✝²² : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝²¹ : Field L<VAR>inst✝²⁰ : Algebra S L<VAR>inst✝¹⁹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : Module R V<VAR>inst✝¹⁶ : Module K V<VAR>inst✝¹⁵ : IsScalarTower R K V<VAR>inst✝¹⁴ : AddCommGroup V'<VAR>inst✝¹³ : Module R V'<VAR>inst✝¹² : Module S V'<VAR>inst✝¹¹ : IsScalarTower R S V'<VAR>inst✝¹⁰ : AddCommGroup V''<VAR>inst✝⁹ : Module R V''<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsDomain S<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : IsNoetherian R S<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : NoZeroSMulDivisors R K<VAR>hp : p ≠ ⊤<VAR>b : Set S<VAR>hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map (algebraMap R S) p) = ⊤<VAR>hRL : Function.Injective ⇑(algebraMap R L)<VAR>M : Submodule R S := Submodule.span R b<VAR>h : Module.Finite R (S ⧸ M) := Module.Finite.of_surjective M.mkQ (Submodule.Quotient.mk_surjective M)<VAR>n : ℕ<VAR>a : Fin n → S ⧸ M<VAR>ha : Submodule.span R (Set.range a) = ⊤<VAR>smul_top_eq : p • ⊤ = ⊤<VAR>exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x<VAR>A' : Fin n → Fin n → R<VAR>hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p<VAR>hA' : ∀ (i : Fin n), ∑ i_1 : Fin n, A' i i_1 • a i_1 = a i<VAR>A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1<VAR>B : Matrix (Fin n) (Fin n) R := A.adjugate<VAR>A_smul : ∀ (i : Fin n), ∑ j : Fin n, A i j • a j = 0<VAR>d_smul : ∀ (i : Fin n), A.det • a i = 0<GOAL>Submodule.span K (⇑(algebraMap S L) '' b) = ⊤
<VAR>R : Type u<VAR>inst✝²⁶ : CommRing R<VAR>S : Type v<VAR>inst✝²⁵ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝²⁴ : Algebra R S<VAR>K : Type u_1<VAR>inst✝²³ : Field K<VAR>inst✝²² : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝²¹ : Field L<VAR>inst✝²⁰ : Algebra S L<VAR>inst✝¹⁹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : Module R V<VAR>inst✝¹⁶ : Module K V<VAR>inst✝¹⁵ : IsScalarTower R K V<VAR>inst✝¹⁴ : AddCommGroup V'<VAR>inst✝¹³ : Module R V'<VAR>inst✝¹² : Module S V'<VAR>inst✝¹¹ : IsScalarTower R S V'<VAR>inst✝¹⁰ : AddCommGroup V''<VAR>inst✝⁹ : Module R V''<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsDomain S<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : IsNoetherian R S<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : NoZeroSMulDivisors R K<VAR>hp : p ≠ ⊤<VAR>b : Set S<VAR>hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map (algebraMap R S) p) = ⊤<VAR>hRL : Function.Injective ⇑(algebraMap R L)<VAR>M : Submodule R S := Submodule.span R b<VAR>h : Module.Finite R (S ⧸ M) := Module.Finite.of_surjective M.mkQ (Submodule.Quotient.mk_surjective M)<VAR>n : ℕ<VAR>a : Fin n → S ⧸ M<VAR>ha : Submodule.span R (Set.range a) = ⊤<VAR>smul_top_eq : p • ⊤ = ⊤<VAR>exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x<VAR>A' : Fin n → Fin n → R<VAR>hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p<VAR>hA' : ∀ (i : Fin n), ∑ i_1 : Fin n, A' i i_1 • a i_1 = a i<VAR>A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1<VAR>B : Matrix (Fin n) (Fin n) R := A.adjugate<VAR>A_smul : ∀ (i : Fin n), ∑ j : Fin n, A i j • a j = 0<VAR>d_smul : ∀ (i : Fin n), A.det • a i = 0<VAR>span_d : Submodule.restrictScalars R (Submodule.span S {(algebraMap R S) A.det}) ≤ M<GOAL>Submodule.span K (⇑(algebraMap S L) '' b) = ⊤
<VAR>R : Type u<VAR>inst✝²⁶ : CommRing R<VAR>S : Type v<VAR>inst✝²⁵ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝²⁴ : Algebra R S<VAR>K : Type u_1<VAR>inst✝²³ : Field K<VAR>inst✝²² : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝²¹ : Field L<VAR>inst✝²⁰ : Algebra S L<VAR>inst✝¹⁹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : Module R V<VAR>inst✝¹⁶ : Module K V<VAR>inst✝¹⁵ : IsScalarTower R K V<VAR>inst✝¹⁴ : AddCommGroup V'<VAR>inst✝¹³ : Module R V'<VAR>inst✝¹² : Module S V'<VAR>inst✝¹¹ : IsScalarTower R S V'<VAR>inst✝¹⁰ : AddCommGroup V''<VAR>inst✝⁹ : Module R V''<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsDomain S<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : IsNoetherian R S<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : NoZeroSMulDivisors R K<VAR>hp : p ≠ ⊤<VAR>b : Set S<VAR>hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map (algebraMap R S) p) = ⊤<VAR>hRL : Function.Injective ⇑(algebraMap R L)<VAR>M : Submodule R S := Submodule.span R b<VAR>h : Module.Finite R (S ⧸ M) := Module.Finite.of_surjective M.mkQ (Submodule.Quotient.mk_surjective M)<VAR>n : ℕ<VAR>a : Fin n → S ⧸ M<VAR>ha : Submodule.span R (Set.range a) = ⊤<VAR>smul_top_eq : p • ⊤ = ⊤<VAR>exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x<VAR>A' : Fin n → Fin n → R<VAR>hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p<VAR>hA' : ∀ (i : Fin n), ∑ i_1 : Fin n, A' i i_1 • a i_1 = a i<VAR>A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1<VAR>B : Matrix (Fin n) (Fin n) R := A.adjugate<VAR>A_smul : ∀ (i : Fin n), ∑ j : Fin n, A i j • a j = 0<VAR>d_smul : ∀ (i : Fin n), A.det • a i = 0<VAR>span_d : Submodule.restrictScalars R (Submodule.span S {(algebraMap R S) A.det}) ≤ M<GOAL>⊤ = Submodule.restrictScalars K (span {(algebraMap R L) A.det})
<VAR>R : Type u<VAR>inst✝²⁶ : CommRing R<VAR>S : Type v<VAR>inst✝²⁵ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝²⁴ : Algebra R S<VAR>K : Type u_1<VAR>inst✝²³ : Field K<VAR>inst✝²² : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝²¹ : Field L<VAR>inst✝²⁰ : Algebra S L<VAR>inst✝¹⁹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : Module R V<VAR>inst✝¹⁶ : Module K V<VAR>inst✝¹⁵ : IsScalarTower R K V<VAR>inst✝¹⁴ : AddCommGroup V'<VAR>inst✝¹³ : Module R V'<VAR>inst✝¹² : Module S V'<VAR>inst✝¹¹ : IsScalarTower R S V'<VAR>inst✝¹⁰ : AddCommGroup V''<VAR>inst✝⁹ : Module R V''<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsDomain S<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : IsNoetherian R S<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : NoZeroSMulDivisors R K<VAR>hp : p ≠ ⊤<VAR>b : Set S<VAR>hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map (algebraMap R S) p) = ⊤<VAR>hRL : Function.Injective ⇑(algebraMap R L)<VAR>M : Submodule R S := Submodule.span R b<VAR>h : Module.Finite R (S ⧸ M) := Module.Finite.of_surjective M.mkQ (Submodule.Quotient.mk_surjective M)<VAR>n : ℕ<VAR>a : Fin n → S ⧸ M<VAR>ha : Submodule.span R (Set.range a) = ⊤<VAR>smul_top_eq : p • ⊤ = ⊤<VAR>exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x<VAR>A' : Fin n → Fin n → R<VAR>hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p<VAR>hA' : ∀ (i : Fin n), ∑ i_1 : Fin n, A' i i_1 • a i_1 = a i<VAR>A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1<VAR>B : Matrix (Fin n) (Fin n) R := A.adjugate<VAR>A_smul : ∀ (i : Fin n), ∑ j : Fin n, A i j • a j = 0<VAR>d_smul : ∀ (i : Fin n), A.det • a i = 0<VAR>span_d : Submodule.restrictScalars R (Submodule.span S {(algebraMap R S) A.det}) ≤ M<GOAL>Submodule.restrictScalars K (span {(algebraMap R L) A.det}) ≤ Submodule.span K (⇑(algebraMap S L) '' b)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝¹ : (i : ι) → PartialOrder (α i)<VAR>inst✝ : ∀ (i : ι), NoAtoms (μ i)<VAR>f g : (i : ι) → α i<GOAL>(univ.pi fun i => Ioo (f i) (g i)) =ᶠ[ae (Measure.pi μ)] Icc f g
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝¹ : (i : ι) → PartialOrder (α i)<VAR>inst✝ : ∀ (i : ι), NoAtoms (μ i)<VAR>f g : (i : ι) → α i<GOAL>(univ.pi fun i => Ioo (f i) (g i)) =ᶠ[ae (Measure.pi μ)] univ.pi fun i => Icc (f i) (g i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>i j : ι<VAR>h : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<GOAL>⋯.choose = j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>i j : ι<VAR>h : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<GOAL>root ⋯.choose = root j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>i j : ι<VAR>h : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<GOAL>(preReflection (root i) (p.toLin.flip (coroot i))) ((preReflection (root i) (p.toLin.flip (coroot i))) (root j)) = root j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a b : α<VAR>s t : Finset α<GOAL>(s ∪ t) ∩ s = s
<VAR>G : PGame<VAR>inst✝ : G.Impartial<GOAL>G ≈ 0 ∨ G ‖ 0
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>h : G < 0<GOAL>G ≈ 0 ∨ G ‖ 0
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>h : G ≈ 0<GOAL>G ≈ 0 ∨ G ‖ 0
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>h : 0 < G<GOAL>G ≈ 0 ∨ G ‖ 0
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>h : G ‖ 0<GOAL>G ≈ 0 ∨ G ‖ 0
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : PartialOrder β<VAR>inst✝² : OrderTop α<VAR>inst✝¹ : IsCoatomic α<VAR>inst✝ : OrderTop β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisInsertion l u<VAR>h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a<VAR>b : β<GOAL>IsCoatom (u b) ↔ IsCoatom b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : PartialOrder β<VAR>inst✝² : OrderTop α<VAR>inst✝¹ : IsCoatomic α<VAR>inst✝ : OrderTop β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisInsertion l u<VAR>h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a<VAR>b : β<VAR>hb : IsCoatom b<GOAL>IsCoatom (u b)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : PartialOrder β<VAR>inst✝² : OrderTop α<VAR>inst✝¹ : IsCoatomic α<VAR>inst✝ : OrderTop β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisInsertion l u<VAR>h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a<VAR>b : β<VAR>hb : IsCoatom b<VAR>a : α<VAR>ha : IsCoatom a<VAR>hab : u b ≤ a<GOAL>IsCoatom (u b)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : PartialOrder β<VAR>inst✝² : OrderTop α<VAR>inst✝¹ : IsCoatomic α<VAR>inst✝ : OrderTop β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisInsertion l u<VAR>h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a<VAR>b : β<VAR>hb : IsCoatom b<VAR>a : α<VAR>ha : IsCoatom a<VAR>hab : u b ≤ a<VAR>this : l a = b<GOAL>IsCoatom (u b)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<GOAL>BddAbove (norm ∘ F f ε '' verticalClosedStrip 0 1)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<GOAL>BddAbove ((fun a => ‖((↑ε + ↑(sSupNormIm f 0)) ^ (a - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-a)) • f a‖) '' verticalClosedStrip 0 1)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>hB : ∃ x, ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ x<GOAL>∃ x, ∀ y ∈ (fun a => ‖((↑ε + ↑(sSupNormIm f 0)) ^ (a - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-a)) • f a‖) '' verticalClosedStrip 0 1, y ≤ x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>B : ℝ<VAR>hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B<GOAL>∃ x, ∀ y ∈ (fun a => ‖((↑ε + ↑(sSupNormIm f 0)) ^ (a - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-a)) • f a‖) '' verticalClosedStrip 0 1, y ≤ x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>B : ℝ<VAR>hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B<GOAL>∀ y ∈ (fun a => ‖((↑ε + ↑(sSupNormIm f 0)) ^ (a - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-a)) • f a‖) '' verticalClosedStrip 0 1, y ≤ max 1 ((ε + sSupNormIm f 0) ^ (-1)) * max 1 ((ε + sSupNormIm f 1) ^ (-1)) * B
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>B : ℝ<VAR>hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B<GOAL>∀ a ∈ verticalClosedStrip 0 1, ‖((↑ε + ↑(sSupNormIm f 0)) ^ (a - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-a)) • f a‖ ≤ max 1 ((ε + sSupNormIm f 0) ^ (-1)) * max 1 ((ε + sSupNormIm f 1) ^ (-1)) * B
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>B : ℝ<VAR>hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B<VAR>z : ℂ<VAR>hset : z ∈ verticalClosedStrip 0 1<GOAL>‖((↑ε + ↑(sSupNormIm f 0)) ^ (z - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-z)) • f z‖ ≤ max 1 ((ε + sSupNormIm f 0) ^ (-1)) * max 1 ((ε + sSupNormIm f 1) ^ (-1)) * B
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>B : ℝ<VAR>z : ℂ<VAR>hset : z ∈ verticalClosedStrip 0 1<VAR>hB : ‖f z‖ ≤ B<GOAL>‖((↑ε + ↑(sSupNormIm f 0)) ^ (z - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-z)) • f z‖ ≤ max 1 ((ε + sSupNormIm f 0) ^ (-1)) * max 1 ((ε + sSupNormIm f 1) ^ (-1)) * B
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>B : ℝ<VAR>z : ℂ<VAR>hset : z ∈ verticalClosedStrip 0 1<VAR>hB : ‖f z‖ ≤ B<GOAL>‖↑(ε + sSupNormIm f 0) ^ (z - 1)‖ * ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ * ‖f z‖ ≤ max 1 ((ε + sSupNormIm f 0) ^ (-1)) * max 1 ((ε + sSupNormIm f 1) ^ (-1)) * B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : Ring α<VAR>inst✝ : Ring β<VAR>h : Antiperiodic f c<VAR>n : ℤ<GOAL>f (↑n * c - x) = ↑↑n.negOnePow * f (-x)
<VAR>P Q : Prop<GOAL>IsCompl P Q ↔ ¬(P ↔ Q)
<VAR>P Q : Prop<GOAL>¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>hf_temperate : Function.HasTemperateGrowth f<VAR>n : ℕ<GOAL>∃ k C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f x‖ ≤ C * (1 + ‖x‖) ^ k
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f✝ : E → F<VAR>hf_temperate : Function.HasTemperateGrowth f✝<VAR>n : ℕ<VAR>k : ℕ → ℕ<VAR>C : ℕ → ℝ<VAR>f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n<GOAL>∃ k C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f✝ x‖ ≤ C * (1 + ‖x‖) ^ k
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f✝ : E → F<VAR>hf_temperate : Function.HasTemperateGrowth f✝<VAR>n : ℕ<VAR>k : ℕ → ℕ<VAR>C : ℕ → ℝ<VAR>f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n<GOAL>∃ C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f✝ x‖ ≤ C * (1 + ‖x‖) ^ (Finset.range (n + 1)).sup k
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f✝ : E → F<VAR>hf_temperate : Function.HasTemperateGrowth f✝<VAR>n : ℕ<VAR>k : ℕ → ℕ<VAR>C : ℕ → ℝ<VAR>f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n<VAR>C' : ℝ := max 0 ((Finset.range (n + 1)).sup' ⋯ C)<GOAL>∃ C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f✝ x‖ ≤ C * (1 + ‖x‖) ^ (Finset.range (n + 1)).sup k
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f✝ : E → F<VAR>hf_temperate : Function.HasTemperateGrowth f✝<VAR>n : ℕ<VAR>k : ℕ → ℕ<VAR>C : ℕ → ℝ<VAR>f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n<VAR>C' : ℝ := max 0 ((Finset.range (n + 1)).sup' ⋯ C)<VAR>hC' : 0 ≤ C'<GOAL>∃ C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f✝ x‖ ≤ C * (1 + ‖x‖) ^ (Finset.range (n + 1)).sup k
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f✝ : E → F<VAR>hf_temperate : Function.HasTemperateGrowth f✝<VAR>n : ℕ<VAR>k : ℕ → ℕ<VAR>C : ℕ → ℝ<VAR>f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n<VAR>C' : ℝ := max 0 ((Finset.range (n + 1)).sup' ⋯ C)<VAR>hC' : 0 ≤ C'<GOAL>∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f✝ x‖ ≤ C' * (1 + ‖x‖) ^ (Finset.range (n + 1)).sup k