ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α✝<VAR>s✝ t u v : Finset α✝<VAR>a b : α✝<VAR>α : Type u_4<VAR>p : Finset α → Prop<VAR>empty : p ∅<VAR>cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), p s → p (Finset.cons a s h)<VAR>s : Multiset α<VAR>nd : s.Nodup<GOAL>p { val := s, nodup := nd }
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a : PosNum<GOAL>↑(a.sub' 1) = ↑a - ↑1
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a : PosNum<GOAL>↑(↑a - 1) = ↑a - ↑1
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>b : PosNum<GOAL>↑(sub' 1 b) = ↑1 - ↑b
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>b : PosNum<GOAL>↑(↑b - 1) = ↑b - ↑1
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a b : PosNum<GOAL>↑(a.bit0.sub' b.bit0) = ↑a.bit0 - ↑b.bit0
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a b : PosNum<GOAL>↑a - ↑b + (↑a - ↑b) = ↑a.bit0 - ↑b.bit0
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a b : PosNum<VAR>this : ↑(↑a + -↑b + (↑a + -↑b)) = ↑a + ↑a + (-↑b + -↑b)<GOAL>↑a - ↑b + (↑a - ↑b) = ↑a.bit0 - ↑b.bit0
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a b : PosNum<GOAL>↑(a.bit0.sub' b.bit1) = ↑a.bit0 - ↑b.bit1
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a b : PosNum<GOAL>↑a - ↑b + (↑a - ↑b) - 1 = ↑a.bit0 - ↑b.bit1
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a b : PosNum<VAR>this : ↑(-↑b + (↑a + (-↑b + -1))) = ↑(↑a + -1 + (-↑b + -↑b))<GOAL>↑a - ↑b + (↑a - ↑b) - 1 = ↑a.bit0 - ↑b.bit1
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a b : PosNum<GOAL>↑(a.bit1.sub' b.bit0) = ↑a.bit1 - ↑b.bit0
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a b : PosNum<GOAL>↑a - ↑b + (↑a - ↑b) + 1 = ↑a.bit1 - ↑b.bit0
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a b : PosNum<VAR>this : ↑(-↑b + (↑a + (-↑b + 1))) = ↑(↑a + 1 + (-↑b + -↑b))<GOAL>↑a - ↑b + (↑a - ↑b) + 1 = ↑a.bit1 - ↑b.bit0
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a b : PosNum<GOAL>↑(a.bit1.sub' b.bit1) = ↑a.bit1 - ↑b.bit1
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a b : PosNum<GOAL>↑a - ↑b + (↑a - ↑b) = ↑a.bit1 - ↑b.bit1
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a b : PosNum<VAR>this : ↑(-↑b + (↑a + -↑b)) = ↑a + (-↑b + -↑b)<GOAL>↑a - ↑b + (↑a - ↑b) = ↑a.bit1 - ↑b.bit1
<VAR>n : ℕ<VAR>x : ℕ × ℕ<VAR>h : x ∈ n.divisorsAntidiagonal<GOAL>x.2 ∈ n.divisors
<VAR>n : ℕ<VAR>x : ℕ × ℕ<VAR>h : x.1 * x.2 = n ∧ n ≠ 0<GOAL>x.2 ∈ n.divisors
<VAR>R✝ : Type u_1<VAR>inst✝² : CommSemiring R✝<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝¹ : Fintype n<VAR>R : Type u_6<VAR>inst✝ : CommRing R<VAR>M : Matrix m n R<GOAL>(Function.Injective fun x => M *ᵥ x) ↔ LinearIndependent R fun i => Mᵀ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝ : LT α<VAR>hM : M.BlockTriangular b<VAR>hN : N.BlockTriangular b<VAR>i j : m<VAR>h : b j < b i<GOAL>(M - N) i j = 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (𝓞 K)ˣ<VAR>w : InfinitePlace K<GOAL>↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑x)) = 0 ↔ w ((algebraMap (𝓞 K) K) ↑x) = 1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (𝓞 K)ˣ<VAR>w : InfinitePlace K<GOAL>¬w ((algebraMap (𝓞 K) K) ↑x) = -1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (𝓞 K)ˣ<VAR>w : InfinitePlace K<GOAL>¬w ((algebraMap (𝓞 K) K) ↑x) = 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (𝓞 K)ˣ<VAR>w : InfinitePlace K<GOAL>¬↑w.mult = 0
<VAR>g : SL(2, ℤ)<GOAL>↑(T⁻¹ * g) 1 = ↑g 1
<VAR>x✝ y✝ x y : ℕ<VAR>h : 0 < x<VAR>IH : ∀ (s t s' t' : ℤ), ((y % x).xgcdAux s t x s' t').1 = (y % x).gcd x<VAR>s t s' t' : ℤ<GOAL>(x.xgcdAux s t y s' t').1 = x.gcd y
<VAR>x✝ y✝ x y : ℕ<VAR>h : 0 < x<VAR>IH : ∀ (s t s' t' : ℤ), ((y % x).xgcdAux s t x s' t').1 = (y % x).gcd x<VAR>s t s' t' : ℤ<GOAL>(y % x).gcd x = x.gcd y
<VAR>X₁ : Type u₁<VAR>inst✝⁴ : TopologicalSpace X₁<VAR>X : Type u<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>e : X₁ → X<VAR>he : ClosedEmbedding e<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TietzeExtension Y<VAR>f : C(X₁, Y)<VAR>e' : X₁ ≃ₜ ↑(Set.range e) := Homeomorph.ofEmbedding e ⋯<GOAL>∃ g, g.comp { toFun := e, continuous_toFun := ⋯ } = f
<VAR>X₁ : Type u₁<VAR>inst✝⁴ : TopologicalSpace X₁<VAR>X : Type u<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>e : X₁ → X<VAR>he : ClosedEmbedding e<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TietzeExtension Y<VAR>f : C(X₁, Y)<VAR>e' : X₁ ≃ₜ ↑(Set.range e) := Homeomorph.ofEmbedding e ⋯<VAR>g : C(X, Y)<VAR>hg : restrict (Set.range e) g = f.comp e'.symm.toContinuousMap<GOAL>∃ g, g.comp { toFun := e, continuous_toFun := ⋯ } = f
<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_5<VAR>Bₘ : Type u_6<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✝⁵ : IsDomain Aₘ<VAR>inst✝⁴ : IsIntegrallyClosed Aₘ<VAR>inst✝³ : IsDomain Bₘ<VAR>inst✝² : IsIntegrallyClosed Bₘ<VAR>inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝ : Module.Finite Aₘ Bₘ<VAR>x : B<VAR>hM : 0 ∉ M<GOAL>(algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B 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_5<VAR>Bₘ : Type u_6<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✝⁵ : IsDomain Aₘ<VAR>inst✝⁴ : IsIntegrallyClosed Aₘ<VAR>inst✝³ : IsDomain Bₘ<VAR>inst✝² : IsIntegrallyClosed Bₘ<VAR>inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝ : Module.Finite Aₘ Bₘ<VAR>x : B<VAR>hM : M ≤ A⁰<GOAL>(algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B 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_5<VAR>Bₘ : Type u_6<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✝⁵ : IsDomain Aₘ<VAR>inst✝⁴ : IsIntegrallyClosed Aₘ<VAR>inst✝³ : IsDomain Bₘ<VAR>inst✝² : IsIntegrallyClosed Bₘ<VAR>inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝ : Module.Finite Aₘ Bₘ<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this : IsIntegralClosure B A L<GOAL>(algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B 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_5<VAR>Bₘ : Type u_6<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✝⁵ : IsDomain Aₘ<VAR>inst✝⁴ : IsIntegrallyClosed Aₘ<VAR>inst✝³ : IsDomain Bₘ<VAR>inst✝² : IsIntegrallyClosed Bₘ<VAR>inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝ : Module.Finite Aₘ Bₘ<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝ : IsIntegralClosure B A L<VAR>this : IsLocalization (algebraMapSubmonoid B A⁰) L<GOAL>(algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B 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_5<VAR>Bₘ : Type u_6<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✝⁵ : IsDomain Aₘ<VAR>inst✝⁴ : IsIntegrallyClosed Aₘ<VAR>inst✝³ : IsDomain Bₘ<VAR>inst✝² : IsIntegrallyClosed Bₘ<VAR>inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝ : Module.Finite Aₘ Bₘ<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝¹ : IsIntegralClosure B A L<VAR>this✝ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this : Algebra Aₘ K := f.toAlgebra<GOAL>(algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B 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_5<VAR>Bₘ : Type u_6<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✝⁵ : IsDomain Aₘ<VAR>inst✝⁴ : IsIntegrallyClosed Aₘ<VAR>inst✝³ : IsDomain Bₘ<VAR>inst✝² : IsIntegrallyClosed Bₘ<VAR>inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝ : Module.Finite Aₘ Bₘ<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝² : IsIntegralClosure B A L<VAR>this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝ : Algebra Aₘ K := f.toAlgebra<VAR>this : IsScalarTower A Aₘ K<GOAL>(algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B 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_5<VAR>Bₘ : Type u_6<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✝⁵ : IsDomain Aₘ<VAR>inst✝⁴ : IsIntegrallyClosed Aₘ<VAR>inst✝³ : IsDomain Bₘ<VAR>inst✝² : IsIntegrallyClosed Bₘ<VAR>inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝ : Module.Finite Aₘ Bₘ<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝³ : IsIntegralClosure B A L<VAR>this✝² : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝¹ : Algebra Aₘ K := f.toAlgebra<VAR>this✝ : IsScalarTower A Aₘ K<VAR>this : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<GOAL>(algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B 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_5<VAR>Bₘ : Type u_6<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✝⁵ : IsDomain Aₘ<VAR>inst✝⁴ : IsIntegrallyClosed Aₘ<VAR>inst✝³ : IsDomain Bₘ<VAR>inst✝² : IsIntegrallyClosed Bₘ<VAR>inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝ : Module.Finite Aₘ Bₘ<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝³ : IsIntegralClosure B A L<VAR>this✝² : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝¹ : Algebra Aₘ K := f.toAlgebra<VAR>this✝ : IsScalarTower A Aₘ K<VAR>this : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<GOAL>(algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B 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_5<VAR>Bₘ : Type u_6<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✝⁵ : IsDomain Aₘ<VAR>inst✝⁴ : IsIntegrallyClosed Aₘ<VAR>inst✝³ : IsDomain Bₘ<VAR>inst✝² : IsIntegrallyClosed Bₘ<VAR>inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝ : Module.Finite Aₘ Bₘ<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝⁴ : IsIntegralClosure B A L<VAR>this✝³ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝² : Algebra Aₘ K := f.toAlgebra<VAR>this✝¹ : IsScalarTower A Aₘ K<VAR>this✝ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this : Algebra Bₘ L := g.toAlgebra<GOAL>(algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B 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_5<VAR>Bₘ : Type u_6<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✝⁵ : IsDomain Aₘ<VAR>inst✝⁴ : IsIntegrallyClosed Aₘ<VAR>inst✝³ : IsDomain Bₘ<VAR>inst✝² : IsIntegrallyClosed Bₘ<VAR>inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝ : Module.Finite Aₘ Bₘ<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝⁵ : IsIntegralClosure B A L<VAR>this✝⁴ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝³ : Algebra Aₘ K := f.toAlgebra<VAR>this✝² : IsScalarTower A Aₘ K<VAR>this✝¹ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this✝ : Algebra Bₘ L := g.toAlgebra<VAR>this : IsScalarTower B Bₘ L<GOAL>(algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B 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_5<VAR>Bₘ : Type u_6<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✝⁵ : IsDomain Aₘ<VAR>inst✝⁴ : IsIntegrallyClosed Aₘ<VAR>inst✝³ : IsDomain Bₘ<VAR>inst✝² : IsIntegrallyClosed Bₘ<VAR>inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝ : Module.Finite Aₘ Bₘ<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝⁶ : IsIntegralClosure B A L<VAR>this✝⁵ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝⁴ : Algebra Aₘ K := f.toAlgebra<VAR>this✝³ : IsScalarTower A Aₘ K<VAR>this✝² : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this✝¹ : Algebra Bₘ L := g.toAlgebra<VAR>this✝ : IsScalarTower B Bₘ L<VAR>this : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra<GOAL>(algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)