ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id R A) g)<GOAL>Ideal.comap (↑(map (AlgHom.id R A) g)) (RingHom.ker ↑(map f (AlgHom.id R D))) = Ideal.map includeLeft (RingHom.ker ↑f) ⊔ Ideal.map includeRight (RingHom.ker ↑g)
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id R A) g)<GOAL>Ideal.comap (↑(map (AlgHom.id R A) g)) (RingHom.ker (map f (AlgHom.id R D))) = Ideal.map includeLeft (RingHom.ker f) ⊔ Ideal.map includeRight (RingHom.ker g)
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id R A) g)<GOAL>Ideal.comap (↑(map (AlgHom.id R A) g)) (RingHom.ker (map f (AlgHom.id R D))) = Ideal.map includeLeft (RingHom.ker f) ⊔ Ideal.comap (map (AlgHom.id R A) g) ⊥
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id R A) g)<GOAL>Ideal.comap (↑(map (AlgHom.id R A) g)) (RingHom.ker (map f (AlgHom.id R D))) = Ideal.comap (map (AlgHom.id R A) g) (Ideal.map (map (AlgHom.id R A) g) (Ideal.map includeLeft (RingHom.ker f)))
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id R A) g)<GOAL>Ideal.comap (↑(map (AlgHom.id R A) g)) (Ideal.map includeLeft (RingHom.ker f)) = Ideal.comap (map (AlgHom.id R A) g) (Ideal.map (map (AlgHom.id R A) g) (Ideal.map includeLeft (RingHom.ker f)))
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id R A) g)<GOAL>Ideal.map includeLeft (RingHom.ker f) = Ideal.map (map (AlgHom.id R A) g) (Ideal.map includeLeft (RingHom.ker f))
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id R A) g)<GOAL>Ideal.map (↑includeLeft) (RingHom.ker f) = Ideal.map ((↑(map (AlgHom.id R A) g)).comp ↑includeLeft) (RingHom.ker f)
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id R A) g)<GOAL>Ideal.map (↑includeLeft) (RingHom.ker f) = Ideal.map (↑(includeLeft.comp (AlgHom.id R A))) (RingHom.ker f)
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>f : ℕ → α → β<VAR>a : α<GOAL>mapIdx f (a :: l) = f 0 a :: mapIdx (fun i => f (i + 1)) l
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁵ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>inst✝ : RingHomSurjective σ₁₂<VAR>f : F<VAR>x : M<VAR>s : Set M<VAR>hf : Injective ⇑f<GOAL>f x ∈ span R₂ (⇑f '' s) ↔ x ∈ span R s
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hba : b ∣ a<GOAL>a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>x : R<VAR>hpq : eval x (p /ₘ (X - C x) ^ rootMultiplicity x p) * eval x (q /ₘ (X - C x) ^ rootMultiplicity x q) ≠ 0<GOAL>rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>x : R<VAR>hpq : (p.comp (X + C x)).trailingCoeff * (q.comp (X + C x)).trailingCoeff ≠ 0<GOAL>rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁰ : CommRing A<VAR>inst✝²⁹ : CommRing B<VAR>inst✝²⁸ : Algebra A B<VAR>inst✝²⁷ : Field K<VAR>inst✝²⁶ : Field L<VAR>inst✝²⁵ : Algebra A K<VAR>inst✝²⁴ : IsFractionRing A K<VAR>inst✝²³ : Algebra B L<VAR>inst✝²² : Algebra K L<VAR>inst✝²¹ : Algebra A L<VAR>inst✝²⁰ : IsScalarTower A B L<VAR>inst✝¹⁹ : IsScalarTower A K L<VAR>inst✝¹⁸ : IsIntegralClosure B A L<VAR>inst✝¹⁷ : FiniteDimensional K L<VAR>Aₘ : Type ?u.752508<VAR>Bₘ : Type ?u.752511<VAR>inst✝¹⁶ : CommRing Aₘ<VAR>inst✝¹⁵ : CommRing Bₘ<VAR>inst✝¹⁴ : Algebra Aₘ Bₘ<VAR>inst✝¹³ : Algebra A Aₘ<VAR>inst✝¹² : Algebra B Bₘ<VAR>inst✝¹¹ : Algebra A Bₘ<VAR>inst✝¹⁰ : IsScalarTower A Aₘ Bₘ<VAR>inst✝⁹ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁸ : IsLocalization M Aₘ<VAR>inst✝⁷ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : IsGalois (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this : IsIntegralClosure B A (FractionRing B)<GOAL>(algebraMap A B) ((intNorm A B) x) = ∏ σ : B ≃ₐ[A] B, σ x
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁰ : CommRing A<VAR>inst✝²⁹ : CommRing B<VAR>inst✝²⁸ : Algebra A B<VAR>inst✝²⁷ : Field K<VAR>inst✝²⁶ : Field L<VAR>inst✝²⁵ : Algebra A K<VAR>inst✝²⁴ : IsFractionRing A K<VAR>inst✝²³ : Algebra B L<VAR>inst✝²² : Algebra K L<VAR>inst✝²¹ : Algebra A L<VAR>inst✝²⁰ : IsScalarTower A B L<VAR>inst✝¹⁹ : IsScalarTower A K L<VAR>inst✝¹⁸ : IsIntegralClosure B A L<VAR>inst✝¹⁷ : FiniteDimensional K L<VAR>Aₘ : Type ?u.752508<VAR>Bₘ : Type ?u.752511<VAR>inst✝¹⁶ : CommRing Aₘ<VAR>inst✝¹⁵ : CommRing Bₘ<VAR>inst✝¹⁴ : Algebra Aₘ Bₘ<VAR>inst✝¹³ : Algebra A Aₘ<VAR>inst✝¹² : Algebra B Bₘ<VAR>inst✝¹¹ : Algebra A Bₘ<VAR>inst✝¹⁰ : IsScalarTower A Aₘ Bₘ<VAR>inst✝⁹ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁸ : IsLocalization M Aₘ<VAR>inst✝⁷ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : IsGalois (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this✝ : IsIntegralClosure B A (FractionRing B)<VAR>this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<GOAL>(algebraMap A B) ((intNorm A B) x) = ∏ σ : B ≃ₐ[A] B, σ x
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁰ : CommRing A<VAR>inst✝²⁹ : CommRing B<VAR>inst✝²⁸ : Algebra A B<VAR>inst✝²⁷ : Field K<VAR>inst✝²⁶ : Field L<VAR>inst✝²⁵ : Algebra A K<VAR>inst✝²⁴ : IsFractionRing A K<VAR>inst✝²³ : Algebra B L<VAR>inst✝²² : Algebra K L<VAR>inst✝²¹ : Algebra A L<VAR>inst✝²⁰ : IsScalarTower A B L<VAR>inst✝¹⁹ : IsScalarTower A K L<VAR>inst✝¹⁸ : IsIntegralClosure B A L<VAR>inst✝¹⁷ : FiniteDimensional K L<VAR>Aₘ : Type ?u.752508<VAR>Bₘ : Type ?u.752511<VAR>inst✝¹⁶ : CommRing Aₘ<VAR>inst✝¹⁵ : CommRing Bₘ<VAR>inst✝¹⁴ : Algebra Aₘ Bₘ<VAR>inst✝¹³ : Algebra A Aₘ<VAR>inst✝¹² : Algebra B Bₘ<VAR>inst✝¹¹ : Algebra A Bₘ<VAR>inst✝¹⁰ : IsScalarTower A Aₘ Bₘ<VAR>inst✝⁹ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁸ : IsLocalization M Aₘ<VAR>inst✝⁷ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : IsGalois (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this✝¹ : IsIntegralClosure B A (FractionRing B)<VAR>this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this : FiniteDimensional (FractionRing A) (FractionRing B)<GOAL>(algebraMap A B) ((intNorm A B) x) = ∏ σ : B ≃ₐ[A] B, σ x
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁰ : CommRing A<VAR>inst✝²⁹ : CommRing B<VAR>inst✝²⁸ : Algebra A B<VAR>inst✝²⁷ : Field K<VAR>inst✝²⁶ : Field L<VAR>inst✝²⁵ : Algebra A K<VAR>inst✝²⁴ : IsFractionRing A K<VAR>inst✝²³ : Algebra B L<VAR>inst✝²² : Algebra K L<VAR>inst✝²¹ : Algebra A L<VAR>inst✝²⁰ : IsScalarTower A B L<VAR>inst✝¹⁹ : IsScalarTower A K L<VAR>inst✝¹⁸ : IsIntegralClosure B A L<VAR>inst✝¹⁷ : FiniteDimensional K L<VAR>Aₘ : Type ?u.752508<VAR>Bₘ : Type ?u.752511<VAR>inst✝¹⁶ : CommRing Aₘ<VAR>inst✝¹⁵ : CommRing Bₘ<VAR>inst✝¹⁴ : Algebra Aₘ Bₘ<VAR>inst✝¹³ : Algebra A Aₘ<VAR>inst✝¹² : Algebra B Bₘ<VAR>inst✝¹¹ : Algebra A Bₘ<VAR>inst✝¹⁰ : IsScalarTower A Aₘ Bₘ<VAR>inst✝⁹ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁸ : IsLocalization M Aₘ<VAR>inst✝⁷ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : IsGalois (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this✝¹ : IsIntegralClosure B A (FractionRing B)<VAR>this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this : FiniteDimensional (FractionRing A) (FractionRing B)<GOAL>(algebraMap A B) ((intNorm A B) x) = ∏ i : FractionRing B ≃ₐ[FractionRing A] FractionRing B, ((galRestrict A (FractionRing A) (FractionRing B) B).toEquiv i) x
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁰ : CommRing A<VAR>inst✝²⁹ : CommRing B<VAR>inst✝²⁸ : Algebra A B<VAR>inst✝²⁷ : Field K<VAR>inst✝²⁶ : Field L<VAR>inst✝²⁵ : Algebra A K<VAR>inst✝²⁴ : IsFractionRing A K<VAR>inst✝²³ : Algebra B L<VAR>inst✝²² : Algebra K L<VAR>inst✝²¹ : Algebra A L<VAR>inst✝²⁰ : IsScalarTower A B L<VAR>inst✝¹⁹ : IsScalarTower A K L<VAR>inst✝¹⁸ : IsIntegralClosure B A L<VAR>inst✝¹⁷ : FiniteDimensional K L<VAR>Aₘ : Type ?u.752508<VAR>Bₘ : Type ?u.752511<VAR>inst✝¹⁶ : CommRing Aₘ<VAR>inst✝¹⁵ : CommRing Bₘ<VAR>inst✝¹⁴ : Algebra Aₘ Bₘ<VAR>inst✝¹³ : Algebra A Aₘ<VAR>inst✝¹² : Algebra B Bₘ<VAR>inst✝¹¹ : Algebra A Bₘ<VAR>inst✝¹⁰ : IsScalarTower A Aₘ Bₘ<VAR>inst✝⁹ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁸ : IsLocalization M Aₘ<VAR>inst✝⁷ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : IsGalois (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this✝¹ : IsIntegralClosure B A (FractionRing B)<VAR>this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this : FiniteDimensional (FractionRing A) (FractionRing B)<GOAL>(algebraMap A B) ((intNorm A B) x) = ∏ x_1 : FractionRing B ≃ₐ[FractionRing A] FractionRing B, ((galRestrict A (FractionRing A) (FractionRing B) B) x_1) x
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroSMulDivisors R A<GOAL>lift.{u, v} #{ x // IsAlgebraic R x } ≤ lift.{v, u} #R[X] * ℵ₀
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroSMulDivisors R A<GOAL>#(ULift.{u, v} { x // IsAlgebraic R x }) ≤ #(ULift.{v, u} R[X]) * ℵ₀
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroSMulDivisors R A<VAR>g : ↑{x | IsAlgebraic R x} → R[X]<VAR>hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0<VAR>hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), (aeval ↑x) (g x) = 0<GOAL>#(ULift.{u, v} { x // IsAlgebraic R x }) ≤ #(ULift.{v, u} R[X]) * ℵ₀
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroSMulDivisors R A<VAR>g : ↑{x | IsAlgebraic R x} → R[X]<VAR>hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0<VAR>hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), (aeval ↑x) (g x) = 0<VAR>f : R[X]<GOAL>lift.{u, v} #↑(g ⁻¹' {f}) ≤ ℵ₀
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroSMulDivisors R A<VAR>g : ↑{x | IsAlgebraic R x} → R[X]<VAR>hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0<VAR>hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), (aeval ↑x) (g x) = 0<VAR>f : R[X]<GOAL>(g ⁻¹' {f}).Countable
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroSMulDivisors R A<VAR>g : ↑{x | IsAlgebraic R x} → R[X]<VAR>hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0<VAR>hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), (aeval ↑x) (g x) = 0<VAR>f : R[X]<GOAL>MapsTo Subtype.val (g ⁻¹' {f}) (f.rootSet A)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroSMulDivisors R A<VAR>g : ↑{x | IsAlgebraic R x} → R[X]<VAR>hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0<VAR>hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), (aeval ↑x) (g x) = 0<VAR>x : ↑{x | IsAlgebraic R x}<GOAL>↑x ∈ (g x).rootSet A
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i<GOAL>p.leftInv i = p.removeZero.leftInv i
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i<GOAL>p.removeZero.leftInv i = p.removeZero.rightInv i
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i<GOAL>p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i<GOAL>p.removeZero.rightInv i = p.rightInv i
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>s : ι → Set α<VAR>t : Set ι<VAR>ht : t.Countable<VAR>f g : α → δ<GOAL>f =ᶠ[ae (μ.restrict (⋃ i ∈ t, s i))] g ↔ ∀ i ∈ t, f =ᶠ[ae (μ.restrict (s i))] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f✝ f : α →. β<VAR>s : Set β<VAR>x : ↑f.Dom<GOAL>x ∈ f.asSubtype ⁻¹' s ↔ x ∈ Subtype.val ⁻¹' f.preimage s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f✝ f : α →. β<VAR>s : Set β<VAR>x : ↑f.Dom<GOAL>f.fn ↑x ⋯ ∈ s ↔ ∃ y ∈ s, y ∈ f ↑x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H✝ K✝ : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>H K : Subgroup G<GOAL>H.subgroupOf K = ⊤ ↔ K ≤ H
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s t : Set α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>inst✝¹ : SigmaCompactSpace β<VAR>inst✝ : R1Space β<VAR>μ : Measure β<VAR>f : β → E<VAR>hf : Integrable f μ<VAR>h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t : Set α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>inst✝¹ : SigmaCompactSpace β<VAR>inst✝ : R1Space β<VAR>μ : Measure β<VAR>f : β → E<VAR>hf : Integrable f μ<VAR>h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0<VAR>s : Set β<VAR>hs : IsClosed s<GOAL>∫ (x : β) in s, f x ∂μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t✝ : Set α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>inst✝¹ : SigmaCompactSpace β<VAR>inst✝ : R1Space β<VAR>μ : Measure β<VAR>f : β → E<VAR>hf : Integrable f μ<VAR>h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0<VAR>s : Set β<VAR>hs : IsClosed s<VAR>t : ℕ → Set β := fun n => closure (compactCovering β n) ∩ s<GOAL>∫ (x : β) in s, f x ∂μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t✝ : Set α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>inst✝¹ : SigmaCompactSpace β<VAR>inst✝ : R1Space β<VAR>μ : Measure β<VAR>f : β → E<VAR>hf : Integrable f μ<VAR>h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0<VAR>s : Set β<VAR>hs : IsClosed s<VAR>t : ℕ → Set β := fun n => closure (compactCovering β n) ∩ s<GOAL>Tendsto (fun n => ∫ (x : β) in t n, f x ∂μ) atTop (𝓝 (∫ (x : β) in s, f x ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t✝ : Set α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>inst✝¹ : SigmaCompactSpace β<VAR>inst✝ : R1Space β<VAR>μ : Measure β<VAR>f : β → E<VAR>hf : Integrable f μ<VAR>h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0<VAR>s : Set β<VAR>hs : IsClosed s<VAR>t : ℕ → Set β := fun n => closure (compactCovering β n) ∩ s<VAR>B : s = ⋃ n, t n<GOAL>Tendsto (fun n => ∫ (x : β) in t n, f x ∂μ) atTop (𝓝 (∫ (x : β) in s, f x ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t✝ : Set α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>inst✝¹ : SigmaCompactSpace β<VAR>inst✝ : R1Space β<VAR>μ : Measure β<VAR>f : β → E<VAR>hf : Integrable f μ<VAR>h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0<VAR>s : Set β<VAR>hs : IsClosed s<VAR>t : ℕ → Set β := fun n => closure (compactCovering β n) ∩ s<VAR>B : s = ⋃ n, t n<GOAL>Tendsto (fun n => ∫ (x : β) in t n, f x ∂μ) atTop (𝓝 (∫ (x : β) in ⋃ n, t n, f x ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t✝ : Set α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>inst✝¹ : SigmaCompactSpace β<VAR>inst✝ : R1Space β<VAR>μ : Measure β<VAR>f : β → E<VAR>hf : Integrable f μ<VAR>h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0<VAR>s : Set β<VAR>hs : IsClosed s<VAR>t : ℕ → Set β := fun n => closure (compactCovering β n) ∩ s<VAR>B : s = ⋃ n, t n<GOAL>∀ (i : ℕ), MeasurableSet (t i)