ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = (x / y).re / abs (x / y)
<VAR>a x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>this : abs x ≠ 0<GOAL>⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = (x / y).re / abs (x / y)
<VAR>a x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>this✝ : abs x ≠ 0<VAR>this : abs y ≠ 0<GOAL>⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = (x / y).re / abs (x / y)
<VAR>a x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>this✝ : abs x ≠ 0<VAR>this : abs y ≠ 0<GOAL>(x.re * y.re + x.im * y.im) * ((abs y)⁻¹ * (abs x)⁻¹) = (x.re * (y.re * (abs y ^ 2)⁻¹) + x.im * (y.im * (abs y ^ 2)⁻¹)) * (abs y * (abs x)⁻¹)
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝⁵ : Category.{v₁, u₁} 𝒮<VAR>inst✝⁴ : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ✝ : a ⟶ b<VAR>inst✝³ : p.IsCartesian f φ✝<VAR>φ : a ⟶ b<VAR>inst✝² : p.IsCartesian f φ<VAR>a' : 𝒳<VAR>ψ ψ' : a' ⟶ a<VAR>inst✝¹ : p.IsHomLift (𝟙 R) ψ<VAR>inst✝ : p.IsHomLift (𝟙 R) ψ'<VAR>h : ψ ≫ φ = ψ' ≫ φ<GOAL>ψ = ψ'
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<GOAL>IsComplement univ S ↔ ∃ g, S = {g}
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h : IsComplement univ S<GOAL>S.Nonempty
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h : IsComplement univ S<VAR>a : G<VAR>ha : a ∈ S<VAR>b : G<VAR>hb : b ∈ S<GOAL>a = b
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<GOAL>(∃ g, S = {g}) → IsComplement univ S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>a : S<VAR>b : R<VAR>hb : b ≠ 0<GOAL>∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>a : S<VAR>b : R<VAR>hb : b ≠ 0<VAR>dim_pos : 0 < Fintype.card ι<GOAL>∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>a : S<VAR>b : R<VAR>hb : b ≠ 0<VAR>dim_pos : 0 < Fintype.card ι<VAR>ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<GOAL>∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>a : S<VAR>b : R<VAR>hb : b ≠ 0<VAR>dim_pos : 0 < Fintype.card ι<VAR>ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>hε : 0 < ε<GOAL>∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>a : S<VAR>b : R<VAR>hb : b ≠ 0<VAR>dim_pos : 0 < Fintype.card ι<VAR>ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>hε : 0 < ε<VAR>ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)<VAR>μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm<VAR>hμ : μ = distinctElems bS adm<VAR>s : ι →₀ R := bS.repr a<VAR>s_eq : ∀ (i : ι), s i = (bS.repr a) i<VAR>qs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i / b<VAR>rs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i % b<VAR>r_eq : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b<GOAL>∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>a : S<VAR>b : R<VAR>hb : b ≠ 0<VAR>dim_pos : 0 < Fintype.card ι<VAR>ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>hε : 0 < ε<VAR>ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)<VAR>μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm<VAR>hμ : μ = distinctElems bS adm<VAR>s : ι →₀ R := bS.repr a<VAR>s_eq : ∀ (i : ι), s i = (bS.repr a) i<VAR>qs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i / b<VAR>rs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i % b<VAR>r_eq : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b<VAR>μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i<GOAL>∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>a : S<VAR>b : R<VAR>hb : b ≠ 0<VAR>dim_pos : 0 < Fintype.card ι<VAR>ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>hε : 0 < ε<VAR>ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)<VAR>μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm<VAR>hμ : μ = distinctElems bS adm<VAR>s : ι →₀ R := bS.repr a<VAR>s_eq : ∀ (i : ι), s i = (bS.repr a) i<VAR>qs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i / b<VAR>rs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i % b<VAR>r_eq : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b<VAR>μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i<VAR>μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i : ι, qs j i • bS i + ∑ i : ι, rs j i • bS i<GOAL>∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>a : S<VAR>b : R<VAR>hb : b ≠ 0<VAR>dim_pos : 0 < Fintype.card ι<VAR>ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>hε : 0 < ε<VAR>ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)<VAR>μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm<VAR>hμ : μ = distinctElems bS adm<VAR>s : ι →₀ R := bS.repr a<VAR>s_eq : ∀ (i : ι), s i = (bS.repr a) i<VAR>qs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i / b<VAR>rs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i % b<VAR>r_eq : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b<VAR>μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i<VAR>μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i : ι, qs j i • bS i + ∑ i : ι, rs j i • bS i<VAR>j k : Fin (adm.card ε ^ Fintype.card ι).succ<VAR>j_ne_k : j ≠ k<VAR>hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε<GOAL>∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>a : S<VAR>b : R<VAR>hb : b ≠ 0<VAR>dim_pos : 0 < Fintype.card ι<VAR>ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>hε : 0 < ε<VAR>ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)<VAR>μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm<VAR>hμ : μ = distinctElems bS adm<VAR>s : ι →₀ R := bS.repr a<VAR>s_eq : ∀ (i : ι), s i = (bS.repr a) i<VAR>qs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i / b<VAR>rs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i % b<VAR>r_eq✝ : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b<VAR>μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i<VAR>μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i : ι, qs j i • bS i + ∑ i : ι, rs j i • bS i<VAR>j k : Fin (adm.card ε ^ Fintype.card ι).succ<VAR>j_ne_k : j ≠ k<VAR>hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε<VAR>hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε<VAR>q : S := ∑ i : ι, (qs k i - qs j i) • bS i<VAR>r : R := μ k - μ j<VAR>r_eq : r = μ k - μ j<GOAL>∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>a : S<VAR>b : R<VAR>hb : b ≠ 0<VAR>dim_pos : 0 < Fintype.card ι<VAR>ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>hε : 0 < ε<VAR>ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)<VAR>μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm<VAR>hμ : μ = distinctElems bS adm<VAR>s : ι →₀ R := bS.repr a<VAR>s_eq : ∀ (i : ι), s i = (bS.repr a) i<VAR>qs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i / b<VAR>rs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i % b<VAR>r_eq✝ : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b<VAR>μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i<VAR>μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i : ι, qs j i • bS i + ∑ i : ι, rs j i • bS i<VAR>j k : Fin (adm.card ε ^ Fintype.card ι).succ<VAR>j_ne_k : j ≠ k<VAR>hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε<VAR>hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε<VAR>q : S := ∑ i : ι, (qs k i - qs j i) • bS i<VAR>r : R := μ k - μ j<VAR>r_eq : r = μ k - μ j<GOAL>∃ i j, i ≠ j ∧ (distinctElems bS adm) i - (distinctElems bS adm) j = r
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>a : S<VAR>b : R<VAR>hb : b ≠ 0<VAR>dim_pos : 0 < Fintype.card ι<VAR>ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>hε : 0 < ε<VAR>ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)<VAR>μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm<VAR>hμ : μ = distinctElems bS adm<VAR>s : ι →₀ R := bS.repr a<VAR>s_eq : ∀ (i : ι), s i = (bS.repr a) i<VAR>qs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i / b<VAR>rs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i % b<VAR>r_eq✝ : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b<VAR>μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i<VAR>μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i : ι, qs j i • bS i + ∑ i : ι, rs j i • bS i<VAR>j k : Fin (adm.card ε ^ Fintype.card ι).succ<VAR>j_ne_k : j ≠ k<VAR>hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε<VAR>hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε<VAR>q : S := ∑ i : ι, (qs k i - qs j i) • bS i<VAR>r : R := μ k - μ j<VAR>r_eq : r = μ k - μ j<GOAL>abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>a : S<VAR>b : R<VAR>hb : b ≠ 0<VAR>dim_pos : 0 < Fintype.card ι<VAR>ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>hε : 0 < ε<VAR>ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)<VAR>μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm<VAR>hμ : μ = distinctElems bS adm<VAR>s : ι →₀ R := bS.repr a<VAR>s_eq : ∀ (i : ι), s i = (bS.repr a) i<VAR>qs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i / b<VAR>rs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i % b<VAR>r_eq✝ : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b<VAR>μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i<VAR>μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i : ι, qs j i • bS i + ∑ i : ι, rs j i • bS i<VAR>j k : Fin (adm.card ε ^ Fintype.card ι).succ<VAR>j_ne_k : j ≠ k<VAR>hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε<VAR>hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε<VAR>q : S := ∑ i : ι, (qs k i - qs j i) • bS i<VAR>r : R := μ k - μ j<VAR>r_eq : r = μ k - μ j<VAR>this : r • a - b • q = ∑ x : ι, (rs k x • bS x - rs j x • bS x)<GOAL>abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>a : S<VAR>b : R<VAR>hb : b ≠ 0<VAR>dim_pos : 0 < Fintype.card ι<VAR>ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>hε : 0 < ε<VAR>ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)<VAR>μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm<VAR>hμ : μ = distinctElems bS adm<VAR>s : ι →₀ R := bS.repr a<VAR>s_eq : ∀ (i : ι), s i = (bS.repr a) i<VAR>qs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i / b<VAR>rs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i % b<VAR>r_eq✝ : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b<VAR>μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i<VAR>μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i : ι, qs j i • bS i + ∑ i : ι, rs j i • bS i<VAR>j k : Fin (adm.card ε ^ Fintype.card ι).succ<VAR>j_ne_k : j ≠ k<VAR>hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε<VAR>hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε<VAR>q : S := ∑ i : ι, (qs k i - qs j i) • bS i<VAR>r : R := μ k - μ j<VAR>r_eq : r = μ k - μ j<VAR>this : r • a - b • q = ∑ x : ι, (rs k x • bS x - rs j x • bS x)<GOAL>abv ((Algebra.norm R) (∑ x : ι, (rs k x • bS x - rs j x • bS x))) < abv b ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>a : S<VAR>b : R<VAR>hb : b ≠ 0<VAR>dim_pos : 0 < Fintype.card ι<VAR>ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>hε : 0 < ε<VAR>ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)<VAR>μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm<VAR>hμ : μ = distinctElems bS adm<VAR>s : ι →₀ R := bS.repr a<VAR>s_eq : ∀ (i : ι), s i = (bS.repr a) i<VAR>qs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i / b<VAR>rs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i % b<VAR>r_eq✝ : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b<VAR>μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i<VAR>μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i : ι, qs j i • bS i + ∑ i : ι, rs j i • bS i<VAR>j k : Fin (adm.card ε ^ Fintype.card ι).succ<VAR>j_ne_k : j ≠ k<VAR>hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε<VAR>hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε<VAR>q : S := ∑ i : ι, (qs k i - qs j i) • bS i<VAR>r : R := μ k - μ j<VAR>r_eq : r = μ k - μ j<VAR>this : r • a - b • q = ∑ x : ι, (rs k x • bS x - rs j x • bS x)<VAR>i : ι<GOAL>↑(abv ((bS.repr (∑ x : ι, (rs k x • bS x - rs j x • bS x))) i)) ≤ ↑(abv (rs k i - rs j i))