ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h✝ : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>x : (ZMod ↑n)ˣ<VAR>pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) ↑n<VAR>h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen<VAR>key : zeta n K L ^ (↑((IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val = ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L)<GOAL>(IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) = x
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h✝ : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>x : (ZMod ↑n)ˣ<VAR>pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) ↑n<VAR>h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen<VAR>key : zeta n K L ^ (↑((IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val = ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L)<VAR>this : ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (IsPrimitiveRoot.powerBasis K hζ).gen = (IsPrimitiveRoot.powerBasis K ⋯).gen<GOAL>(IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) = x
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h✝ : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>x : (ZMod ↑n)ˣ<VAR>pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) ↑n<VAR>h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen<VAR>key : zeta n K L ^ (↑((IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val = ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L)<VAR>this : ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L) = (IsPrimitiveRoot.powerBasis K ⋯).gen<GOAL>(IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) = x
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h✝ : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>x : (ZMod ↑n)ˣ<VAR>pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) ↑n<VAR>h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen<VAR>key : zeta n K L ^ (↑((IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val = zeta n K L ^ (↑x).val<VAR>this : ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L) = (IsPrimitiveRoot.powerBasis K ⋯).gen<GOAL>(IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) = x
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h✝ : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>x : (ZMod ↑n)ˣ<VAR>pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) ↑n<VAR>h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen<VAR>key : ↑↑hζ.toRootsOfUnity ^ (↑((IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val = ↑↑hζ.toRootsOfUnity ^ (↑x).val<VAR>this : ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L) = (IsPrimitiveRoot.powerBasis K ⋯).gen<GOAL>(IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) = x
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h✝ : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>x : (ZMod ↑n)ˣ<VAR>pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) ↑n<VAR>h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen<VAR>this : ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L) = (IsPrimitiveRoot.powerBasis K ⋯).gen<VAR>key : ↑↑(hζ.toRootsOfUnity ^ (↑((IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val) = ↑↑(hζ.toRootsOfUnity ^ (↑x).val)<GOAL>(IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) = x
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h✝ : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>x : (ZMod ↑n)ˣ<VAR>pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) ↑n<VAR>h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen<VAR>this : ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L) = (IsPrimitiveRoot.powerBasis K ⋯).gen<VAR>key : hζ.toRootsOfUnity ^ (↑((IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val = hζ.toRootsOfUnity ^ (↑x).val<GOAL>(IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) = x
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h✝ : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>x : (ZMod ↑n)ˣ<VAR>pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) ↑n<VAR>h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen<VAR>this : ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L) = (IsPrimitiveRoot.powerBasis K ⋯).gen<VAR>key : ↑(↑((IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val = ↑(↑x).val<GOAL>(IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) = x
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h✝ : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n := zeta_spec n K L<VAR>hμ : ∀ (t : (ZMod ↑n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) ↑n := fun t => IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)<VAR>x : (ZMod ↑n)ˣ<VAR>pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) ↑n<VAR>h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen<VAR>this : ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L) = (IsPrimitiveRoot.powerBasis K ⋯).gen<VAR>key : ↑((IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h)) = ↑x<GOAL>(IsPrimitiveRoot.autToPow K hζ) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : Filter β<VAR>u : β → α<GOAL>IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u
<VAR>q : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (↑m / x) ↔ m ≠ 0 ∧ Irrational x
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>x : (𝓞 K)ˣ<VAR>n : ℤ<GOAL>((coeHom K).comp (map ↑(algebraMap (𝓞 K) K))) (x ^ n) = (algebraMap (𝓞 K) K) ↑x ^ n
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Field E<VAR>inst✝⁹ : Algebra F E<VAR>K✝ : Type w<VAR>inst✝⁸ : Field K✝<VAR>inst✝⁷ : Algebra F K✝<VAR>inst✝⁶ : Algebra E K✝<VAR>inst✝⁵ : IsScalarTower F E K✝<VAR>K : Type v<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsAlgebraic F E<GOAL>sepDegree F E * sepDegree E K = sepDegree F K
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : IsDomain A<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹³ : Field L<VAR>C : Type u_5<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : Algebra C L<VAR>inst✝⁷ : IsIntegralClosure C A L<VAR>inst✝⁶ : Algebra A C<VAR>inst✝⁵ : IsScalarTower A C L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι K L<VAR>hb_int : ∀ (i : ι), IsIntegral A (b i)<VAR>inst✝ : IsIntegrallyClosed A<GOAL>LinearMap.range (↑A (Algebra.linearMap C L)) ≤ Submodule.span A (Set.range ⇑((traceForm K L).dualBasis ⋯ b))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : IsDomain A<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹³ : Field L<VAR>C : Type u_5<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : Algebra C L<VAR>inst✝⁷ : IsIntegralClosure C A L<VAR>inst✝⁶ : Algebra A C<VAR>inst✝⁵ : IsScalarTower A C L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι K L<VAR>hb_int : ∀ (i : ι), IsIntegral A (b i)<VAR>inst✝ : IsIntegrallyClosed A<GOAL>Set.range ⇑b ⊆ ↑((traceForm K L).flip.dualSubmodule (LinearMap.range (↑A (Algebra.linearMap C L))))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : IsDomain A<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹³ : Field L<VAR>C : Type u_5<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : Algebra C L<VAR>inst✝⁷ : IsIntegralClosure C A L<VAR>inst✝⁶ : Algebra A C<VAR>inst✝⁵ : IsScalarTower A C L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι K L<VAR>hb_int : ∀ (i : ι), IsIntegral A (b i)<VAR>inst✝ : IsIntegrallyClosed A<VAR>i : ι<VAR>y : C<GOAL>((traceForm K L).flip (b i)) ((↑A (Algebra.linearMap C L)) y) ∈ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : IsDomain A<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹³ : Field L<VAR>C : Type u_5<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : Algebra C L<VAR>inst✝⁷ : IsIntegralClosure C A L<VAR>inst✝⁶ : Algebra A C<VAR>inst✝⁵ : IsScalarTower A C L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι K L<VAR>hb_int : ∀ (i : ι), IsIntegral A (b i)<VAR>inst✝ : IsIntegrallyClosed A<VAR>i : ι<VAR>y : C<GOAL>(trace K L) ((algebraMap C L) y * b i) ∈ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : IsDomain A<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹³ : Field L<VAR>C : Type u_5<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : Algebra C L<VAR>inst✝⁷ : IsIntegralClosure C A L<VAR>inst✝⁶ : Algebra A C<VAR>inst✝⁵ : IsScalarTower A C L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι K L<VAR>hb_int : ∀ (i : ι), IsIntegral A (b i)<VAR>inst✝ : IsIntegrallyClosed A<VAR>i : ι<VAR>y : C<GOAL>IsIntegral A ((trace K L) ((algebraMap C L) y * b i))
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝¹ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>F : Type u_5<VAR>inst✝ : FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>x : N<GOAL>x ∈ mker (inr M N) ↔ x ∈ ⊥
<VAR>t : Set GHSpace<VAR>C : ℝ<VAR>u : ℕ → ℝ<VAR>K : ℕ → ℕ<VAR>ulim : Tendsto u atTop (𝓝 0)<VAR>hdiam : ∀ p ∈ t, diam univ ≤ C<VAR>hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)<GOAL>TotallyBounded t
<VAR>t : Set GHSpace<VAR>C : ℝ<VAR>u : ℕ → ℝ<VAR>K : ℕ → ℕ<VAR>ulim : Tendsto u atTop (𝓝 0)<VAR>hdiam : ∀ p ∈ t, diam univ ≤ C<VAR>hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)<VAR>δ : ℝ<VAR>δpos : δ > 0<GOAL>∃ β x F, ∀ (x y : ↑t), F x = F y → dist ↑x ↑y < δ
<VAR>t : Set GHSpace<VAR>C : ℝ<VAR>u : ℕ → ℝ<VAR>K : ℕ → ℕ<VAR>ulim : Tendsto u atTop (𝓝 0)<VAR>hdiam : ∀ p ∈ t, diam univ ≤ C<VAR>hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>ε : ℝ := 1 / 5 * δ<VAR>εpos : 0 < ε<GOAL>∃ β x F, ∀ (x y : ↑t), F x = F y → dist ↑x ↑y < δ
<VAR>t : Set GHSpace<VAR>C : ℝ<VAR>u : ℕ → ℝ<VAR>K : ℕ → ℕ<VAR>ulim : Tendsto u atTop (𝓝 0)<VAR>hdiam : ∀ p ∈ t, diam univ ≤ C<VAR>hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>ε : ℝ := 1 / 5 * δ<VAR>εpos : 0 < ε<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε<GOAL>∃ β x F, ∀ (x y : ↑t), F x = F y → dist ↑x ↑y < δ
<VAR>t : Set GHSpace<VAR>C : ℝ<VAR>u : ℕ → ℝ<VAR>K : ℕ → ℕ<VAR>ulim : Tendsto u atTop (𝓝 0)<VAR>hdiam : ∀ p ∈ t, diam univ ≤ C<VAR>hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>ε : ℝ := 1 / 5 * δ<VAR>εpos : 0 < ε<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε<VAR>u_le_ε : u n ≤ ε<GOAL>∃ β x F, ∀ (x y : ↑t), F x = F y → dist ↑x ↑y < δ
<VAR>t : Set GHSpace<VAR>C : ℝ<VAR>u : ℕ → ℝ<VAR>K : ℕ → ℕ<VAR>ulim : Tendsto u atTop (𝓝 0)<VAR>hdiam : ∀ p ∈ t, diam univ ≤ C<VAR>hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>ε : ℝ := 1 / 5 * δ<VAR>εpos : 0 < ε<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε<VAR>u_le_ε : u n ≤ ε<VAR>s : (p : GHSpace) → Set p.Rep<VAR>N : GHSpace → ℕ<VAR>hN : ∀ (p : GHSpace), N p ≤ K n<VAR>E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)<VAR>hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)<VAR>M : ℕ := ⌊ε⁻¹ * max C 0⌋₊<GOAL>∃ β x F, ∀ (x y : ↑t), F x = F y → dist ↑x ↑y < δ
<VAR>t : Set GHSpace<VAR>C : ℝ<VAR>u : ℕ → ℝ<VAR>K : ℕ → ℕ<VAR>ulim : Tendsto u atTop (𝓝 0)<VAR>hdiam : ∀ p ∈ t, diam univ ≤ C<VAR>hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>ε : ℝ := 1 / 5 * δ<VAR>εpos : 0 < ε<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε<VAR>u_le_ε : u n ≤ ε<VAR>s : (p : GHSpace) → Set p.Rep<VAR>N : GHSpace → ℕ<VAR>hN : ∀ (p : GHSpace), N p ≤ K n<VAR>E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)<VAR>hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)<VAR>M : ℕ := ⌊ε⁻¹ * max C 0⌋₊<VAR>F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) := fun p => ⟨⟨N p, ⋯⟩, fun a b => ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩<GOAL>∃ β x F, ∀ (x y : ↑t), F x = F y → dist ↑x ↑y < δ
<VAR>t : Set GHSpace<VAR>C : ℝ<VAR>u : ℕ → ℝ<VAR>K : ℕ → ℕ<VAR>ulim : Tendsto u atTop (𝓝 0)<VAR>hdiam : ∀ p ∈ t, diam univ ≤ C<VAR>hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>ε : ℝ := 1 / 5 * δ<VAR>εpos : 0 < ε<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε<VAR>u_le_ε : u n ≤ ε<VAR>s : (p : GHSpace) → Set p.Rep<VAR>N : GHSpace → ℕ<VAR>hN : ∀ (p : GHSpace), N p ≤ K n<VAR>E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)<VAR>hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)<VAR>M : ℕ := ⌊ε⁻¹ * max C 0⌋₊<VAR>F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) := fun p => ⟨⟨N p, ⋯⟩, fun a b => ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩<VAR>p : GHSpace<VAR>pt : p ∈ t<VAR>q : GHSpace<VAR>qt : q ∈ t<VAR>hpq : (fun p => F ↑p) ⟨p, pt⟩ = (fun p => F ↑p) ⟨q, qt⟩<GOAL>dist ↑⟨p, pt⟩ ↑⟨q, qt⟩ < δ
<VAR>t : Set GHSpace<VAR>C : ℝ<VAR>u : ℕ → ℝ<VAR>K : ℕ → ℕ<VAR>ulim : Tendsto u atTop (𝓝 0)<VAR>hdiam : ∀ p ∈ t, diam univ ≤ C<VAR>hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>ε : ℝ := 1 / 5 * δ<VAR>εpos : 0 < ε<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε<VAR>u_le_ε : u n ≤ ε<VAR>s : (p : GHSpace) → Set p.Rep<VAR>N : GHSpace → ℕ<VAR>hN : ∀ (p : GHSpace), N p ≤ K n<VAR>E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)<VAR>hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)<VAR>M : ℕ := ⌊ε⁻¹ * max C 0⌋₊<VAR>F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) := fun p => ⟨⟨N p, ⋯⟩, fun a b => ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩<VAR>p : GHSpace<VAR>pt : p ∈ t<VAR>q : GHSpace<VAR>qt : q ∈ t<VAR>hpq : (fun p => F ↑p) ⟨p, pt⟩ = (fun p => F ↑p) ⟨q, qt⟩<VAR>Npq : N p = N q<GOAL>dist ↑⟨p, pt⟩ ↑⟨q, qt⟩ < δ
<VAR>t : Set GHSpace<VAR>C : ℝ<VAR>u : ℕ → ℝ<VAR>K : ℕ → ℕ<VAR>ulim : Tendsto u atTop (𝓝 0)<VAR>hdiam : ∀ p ∈ t, diam univ ≤ C<VAR>hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)<VAR>δ : ℝ<VAR>δpos : δ > 0<VAR>ε : ℝ := 1 / 5 * δ<VAR>εpos : 0 < ε<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε<VAR>u_le_ε : u n ≤ ε<VAR>s : (p : GHSpace) → Set p.Rep<VAR>N : GHSpace → ℕ<VAR>hN : ∀ (p : GHSpace), N p ≤ K n<VAR>E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)<VAR>hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)<VAR>M : ℕ := ⌊ε⁻¹ * max C 0⌋₊<VAR>F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) := fun p => ⟨⟨N p, ⋯⟩, fun a b => ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩<VAR>p : GHSpace<VAR>pt : p ∈ t<VAR>q : GHSpace<VAR>qt : q ∈ t<VAR>hpq : (fun p => F ↑p) ⟨p, pt⟩ = (fun p => F ↑p) ⟨q, qt⟩<VAR>Npq : N p = N q<VAR>Ψ : ↑(s p) → ↑(s q) := fun x => (E q).symm (Fin.cast Npq ((E p) x))<VAR>Φ : ↑(s p) → q.Rep := fun x => ↑(Ψ x)<VAR>main : ghDist p.Rep q.Rep ≤ ε + ε / 2 + ε<GOAL>dist ↑⟨p, pt⟩ ↑⟨q, qt⟩ < δ
<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>f : ↥(simpleFunc G 1 μ)<GOAL>‖f‖ = ∑ x ∈ (toSimpleFunc f).range, (μ (↑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖
<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>f : ↥(simpleFunc G 1 μ)<GOAL>(∫⁻ (x : α), ↑‖↑(toSimpleFunc f) x‖₊ ∂μ).toReal = ∑ x ∈ (toSimpleFunc f).range, (μ (↑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖
<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>f : ↥(simpleFunc G 1 μ)<VAR>h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊<GOAL>(∫⁻ (x : α), ↑‖↑(toSimpleFunc f) x‖₊ ∂μ).toReal = ∑ x ∈ (toSimpleFunc f).range, (μ (↑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖
<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>f : ↥(simpleFunc G 1 μ)<VAR>h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊<GOAL>(∫⁻ (x : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) x ∂μ).toReal = ∑ x ∈ (toSimpleFunc f).range, (μ (↑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖
<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>f : ↥(simpleFunc G 1 μ)<VAR>h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊<GOAL>∑ a ∈ (toSimpleFunc f).range, (↑‖a‖₊ * μ (↑(toSimpleFunc f) ⁻¹' {a})).toReal = ∑ x ∈ (toSimpleFunc f).range, (μ (↑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖