ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u<VAR>B✝ : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝²² : DecidableEq ι<VAR>inst✝²¹ : CommRing A<VAR>inst✝²⁰ : CommRing B✝<VAR>inst✝¹⁹ : Algebra A B✝<VAR>inst✝¹⁸ : CommRing C<VAR>inst✝¹⁷ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁶ : Fintype ι'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Field E<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra K E<VAR>inst✝⁸ : Module.Finite K L<VAR>inst✝⁷ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>R : Type z<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed R<VAR>inst✝ : IsFractionRing R K<VAR>B : PowerBasis K L<VAR>hint : IsIntegral R B.gen<VAR>z : L<VAR>hz : IsIntegral R z<VAR>hinv : IsUnit (traceMatrix K ⇑B.basis).det<VAR>H : (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z = (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)<VAR>cramer : (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i => (trace K L) (z * B.basis i)) = (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)<GOAL>discr K ⇑B.basis • z ∈ adjoin R {B.gen}
<VAR>A : Type u<VAR>B✝ : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝²² : DecidableEq ι<VAR>inst✝²¹ : CommRing A<VAR>inst✝²⁰ : CommRing B✝<VAR>inst✝¹⁹ : Algebra A B✝<VAR>inst✝¹⁸ : CommRing C<VAR>inst✝¹⁷ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁶ : Fintype ι'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Field E<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra K E<VAR>inst✝⁸ : Module.Finite K L<VAR>inst✝⁷ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>R : Type z<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed R<VAR>inst✝ : IsFractionRing R K<VAR>B : PowerBasis K L<VAR>hint : IsIntegral R B.gen<VAR>z : L<VAR>hz : IsIntegral R z<VAR>hinv : IsUnit (traceMatrix K ⇑B.basis).det<VAR>H : (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z = (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)<VAR>cramer : (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i => (trace K L) (z * B.basis i)) = (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)<GOAL>∀ (i : Fin B.dim), ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥
<VAR>A : Type u<VAR>B✝ : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝²² : DecidableEq ι<VAR>inst✝²¹ : CommRing A<VAR>inst✝²⁰ : CommRing B✝<VAR>inst✝¹⁹ : Algebra A B✝<VAR>inst✝¹⁸ : CommRing C<VAR>inst✝¹⁷ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁶ : Fintype ι'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Field E<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra K E<VAR>inst✝⁸ : Module.Finite K L<VAR>inst✝⁷ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>R : Type z<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed R<VAR>inst✝ : IsFractionRing R K<VAR>B : PowerBasis K L<VAR>hint : IsIntegral R B.gen<VAR>z : L<VAR>hz : IsIntegral R z<VAR>hinv : IsUnit (traceMatrix K ⇑B.basis).det<VAR>H : (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z = (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)<VAR>cramer : (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i => (trace K L) (z * B.basis i)) = (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)<VAR>i : Fin B.dim<GOAL>((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥
<VAR>A : Type u<VAR>B✝ : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝²² : DecidableEq ι<VAR>inst✝²¹ : CommRing A<VAR>inst✝²⁰ : CommRing B✝<VAR>inst✝¹⁹ : Algebra A B✝<VAR>inst✝¹⁸ : CommRing C<VAR>inst✝¹⁷ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁶ : Fintype ι'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Field E<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra K E<VAR>inst✝⁸ : Module.Finite K L<VAR>inst✝⁷ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>R : Type z<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed R<VAR>inst✝ : IsFractionRing R K<VAR>B : PowerBasis K L<VAR>hint : IsIntegral R B.gen<VAR>z : L<VAR>hz : IsIntegral R z<VAR>hinv : IsUnit (traceMatrix K ⇑B.basis).det<VAR>H : (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z = (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)<VAR>cramer : (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i => (trace K L) (z * B.basis i)) = traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).det • B.basis.equivFun z<VAR>i : Fin B.dim<GOAL>((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥
<VAR>A : Type u<VAR>B✝ : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝²² : DecidableEq ι<VAR>inst✝²¹ : CommRing A<VAR>inst✝²⁰ : CommRing B✝<VAR>inst✝¹⁹ : Algebra A B✝<VAR>inst✝¹⁸ : CommRing C<VAR>inst✝¹⁷ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁶ : Fintype ι'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Field E<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra K E<VAR>inst✝⁸ : Module.Finite K L<VAR>inst✝⁷ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>R : Type z<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed R<VAR>inst✝ : IsFractionRing R K<VAR>B : PowerBasis K L<VAR>hint : IsIntegral R B.gen<VAR>z : L<VAR>hz : IsIntegral R z<VAR>hinv : IsUnit (traceMatrix K ⇑B.basis).det<VAR>H : (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z = (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)<VAR>i : Fin B.dim<VAR>cramer : ((traceMatrix K ⇑B.basis)⁻¹ *ᵥ traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i => (trace K L) (z * B.basis i)) = (traceMatrix K ⇑B.basis)⁻¹ *ᵥ traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).det • B.basis.equivFun z<GOAL>((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥
<VAR>A : Type u<VAR>B✝ : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝²² : DecidableEq ι<VAR>inst✝²¹ : CommRing A<VAR>inst✝²⁰ : CommRing B✝<VAR>inst✝¹⁹ : Algebra A B✝<VAR>inst✝¹⁸ : CommRing C<VAR>inst✝¹⁷ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁶ : Fintype ι'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Field E<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra K E<VAR>inst✝⁸ : Module.Finite K L<VAR>inst✝⁷ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>R : Type z<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed R<VAR>inst✝ : IsFractionRing R K<VAR>B : PowerBasis K L<VAR>hint : IsIntegral R B.gen<VAR>z : L<VAR>hz : IsIntegral R z<VAR>hinv : IsUnit (traceMatrix K ⇑B.basis).det<VAR>H : (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z = (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)<VAR>i : Fin B.dim<VAR>cramer : ((traceMatrix K ⇑B.basis).cramer fun i => (trace K L) (z * B.basis i)) = (traceMatrix K ⇑B.basis).det • B.basis.equivFun z<GOAL>((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥
<VAR>A : Type u<VAR>B✝ : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝²² : DecidableEq ι<VAR>inst✝²¹ : CommRing A<VAR>inst✝²⁰ : CommRing B✝<VAR>inst✝¹⁹ : Algebra A B✝<VAR>inst✝¹⁸ : CommRing C<VAR>inst✝¹⁷ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁶ : Fintype ι'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Field E<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra K E<VAR>inst✝⁸ : Module.Finite K L<VAR>inst✝⁷ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>R : Type z<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed R<VAR>inst✝ : IsFractionRing R K<VAR>B : PowerBasis K L<VAR>hint : IsIntegral R B.gen<VAR>z : L<VAR>hz : IsIntegral R z<VAR>hinv : IsUnit (traceMatrix K ⇑B.basis).det<VAR>H : (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z = (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)<VAR>i : Fin B.dim<VAR>cramer : ((traceMatrix K ⇑B.basis).cramer fun i => (trace K L) (z * B.basis i)) = (traceMatrix K ⇑B.basis).det • B.basis.equivFun z<GOAL>∑ σ : Equiv.Perm (Fin B.dim), Equiv.Perm.sign σ • ∏ i_1 : Fin B.dim, (traceMatrix K ⇑B.basis).updateColumn i (fun i => (trace K L) (z * B.basis i)) (σ i_1) i_1 ∈ ⊥
<VAR>A : Type u<VAR>B✝ : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝²² : DecidableEq ι<VAR>inst✝²¹ : CommRing A<VAR>inst✝²⁰ : CommRing B✝<VAR>inst✝¹⁹ : Algebra A B✝<VAR>inst✝¹⁸ : CommRing C<VAR>inst✝¹⁷ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁶ : Fintype ι'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Field E<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra K E<VAR>inst✝⁸ : Module.Finite K L<VAR>inst✝⁷ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>R : Type z<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed R<VAR>inst✝ : IsFractionRing R K<VAR>B : PowerBasis K L<VAR>hint : IsIntegral R B.gen<VAR>z : L<VAR>hz : IsIntegral R z<VAR>hinv : IsUnit (traceMatrix K ⇑B.basis).det<VAR>H : (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z = (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)<VAR>i : Fin B.dim<VAR>cramer : ((traceMatrix K ⇑B.basis).cramer fun i => (trace K L) (z * B.basis i)) = (traceMatrix K ⇑B.basis).det • B.basis.equivFun z<VAR>σ : Equiv.Perm (Fin B.dim)<VAR>x✝¹ : σ ∈ univ<VAR>j : Fin B.dim<VAR>x✝ : j ∈ univ<GOAL>(traceMatrix K ⇑B.basis).updateColumn i (fun i => (trace K L) (z * B.basis i)) (σ j) j ∈ ⊥
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>a : R<GOAL>((monomial n) a).support ⊆ {n}
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>a : R<GOAL>(match { toFinsupp := Finsupp.single n a } with | { toFinsupp := p } => p.support) ⊆ {n}
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>φ ψ : L.Formula α<VAR>v : α → M<VAR>R : L.Relations 2<VAR>t₁ t₂ : L.Term α<GOAL>(R.formula₂ t₁ t₂).Realize v ↔ RelMap R ![Term.realize v t₁, Term.realize v t₂]
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>φ ψ : L.Formula α<VAR>v : α → M<VAR>R : L.Relations 2<VAR>t₁ t₂ : L.Term α<GOAL>(RelMap R fun i => Term.realize v (![t₁, t₂] i)) = RelMap R ![Term.realize v t₁, Term.realize v t₂]
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>φ ψ : L.Formula α<VAR>v : α → M<VAR>R : L.Relations 2<VAR>t₁ t₂ : L.Term α<GOAL>Term.realize v (![t₁, t₂] 0) = ![Term.realize v t₁, Term.realize v t₂] 0
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>φ ψ : L.Formula α<VAR>v : α → M<VAR>R : L.Relations 2<VAR>t₁ t₂ : L.Term α<GOAL>∀ (i : Fin 1), Term.realize v (![t₁, t₂] i.succ) = ![Term.realize v t₁, Term.realize v t₂] i.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h : min c d ≤ b<GOAL>Iic b ∪ Icc c d = Iic (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hcd : c ≤ d<VAR>h : c ≤ b<GOAL>Iic b ∪ Icc c d = Iic (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hcd : d < c<VAR>h : c ≤ b ∨ d ≤ b<GOAL>Iic b ∪ Icc c d = Iic (max b d)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : E → ℝ≥0∞<GOAL>∫⁻ (x : E) in f '' s, g x ∂μ = ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * g (f x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : E → ℝ≥0∞<GOAL>∫⁻ (a : ↑s), g (s.restrict f a) ∂Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|) = ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * g (f x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : E → ℝ≥0∞<GOAL>∫⁻ (a : ↑s), (g ∘ f) ↑a ∂Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|) = ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * (g ∘ f) x ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : E → ℝ≥0∞<GOAL>∫⁻ (a : E) in s, ((fun x => ENNReal.ofReal |(f' x).det|) * g ∘ f) a ∂μ = ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * (g ∘ f) x ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : E → ℝ≥0∞<GOAL>∀ᵐ (x : E) ∂μ.restrict s, ENNReal.ofReal |(f' x).det| < ⊤
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : E → ℝ≥0∞<GOAL>AEMeasurable (fun x => ENNReal.ofReal |(f' x).det|) (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝² : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝¹ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝ : NormedSpace ℝ E<VAR>f : β × γ → E<VAR>hf : AEStronglyMeasurable f ((κ ⊗ₖ η) a)<GOAL>(fun x => ∫ (y : γ), f (x, y) ∂η (a, x)) =ᶠ[ae (κ a)] fun x => ∫ (y : γ), AEStronglyMeasurable.mk f hf (x, y) ∂η (a, x)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>r : R<GOAL>(opRingEquiv R) (op ((monomial n) r)) = (monomial n) (op r)
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<VAR>x : ↑X.toTopCat<GOAL>toStalk (↑(unop (op (Γ.obj (op X))))) (X.toΓSpecSheafedSpace.base x) ≫ (stalkFunctor CommRingCat (X.toΓSpecSheafedSpace.base x)).map X.toΓSpecSheafedSpace.c ≫ stalkPushforward CommRingCat X.toΓSpecSheafedSpace.base X.presheaf x = X.presheaf.Γgerm x
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<VAR>x : ↑X.toTopCat<GOAL>(toOpen (↑(Γ.obj (op X))) (basicOpen 1) ≫ (structureSheaf ↑(Γ.obj (op X))).presheaf.germ ⟨X.toΓSpecFun x, ⋯⟩) ≫ (stalkFunctor CommRingCat (X.toΓSpecSheafedSpace.base x)).map X.toΓSpecSheafedSpace.c ≫ stalkPushforward CommRingCat X.toΓSpecSheafedSpace.base X.presheaf x = X.presheaf.Γgerm x
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<VAR>x : ↑X.toTopCat<GOAL>(toOpen (↑(Γ.obj (op X))) (basicOpen 1) ≫ (structureSheaf ↑(Γ.obj (op X))).presheaf.germ ⟨X.toΓSpecFun x, ⋯⟩ ≫ (stalkFunctor CommRingCat (X.toΓSpecSheafedSpace.base x)).map X.toΓSpecSheafedSpace.c) ≫ stalkPushforward CommRingCat X.toΓSpecSheafedSpace.base X.presheaf x = X.presheaf.Γgerm x
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<VAR>x : ↑X.toTopCat<GOAL>(toOpen (↑(Γ.obj (op X))) (basicOpen 1) ≫ X.toΓSpecSheafedSpace.c.app (op (basicOpen 1)) ≫ ((pushforward CommRingCat X.toΓSpecSheafedSpace.base).obj X.presheaf).germ ⟨X.toΓSpecFun x, ⋯⟩) ≫ stalkPushforward CommRingCat X.toΓSpecSheafedSpace.base X.presheaf x = X.presheaf.Γgerm x
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<VAR>x : ↑X.toTopCat<GOAL>(X.toToΓSpecMapBasicOpen 1 ≫ ((pushforward CommRingCat X.toΓSpecSheafedSpace.base).obj X.presheaf).germ ⟨X.toΓSpecFun x, ⋯⟩) ≫ stalkPushforward CommRingCat X.toΓSpecSheafedSpace.base X.presheaf x = X.presheaf.germ ⟨x, ⋯⟩
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<VAR>x : ↑X.toTopCat<GOAL>(X.toToΓSpecMapBasicOpen 1 ≫ ((pushforward CommRingCat X.toΓSpecSheafedSpace.base).obj X.presheaf).germ ⟨X.toΓSpecFun x, ⋯⟩) ≫ stalkPushforward CommRingCat X.toΓSpecSheafedSpace.base X.presheaf x = ((pushforward CommRingCat X.toΓSpecBase).obj X.presheaf).germ ⟨X.toΓSpecBase ↑⟨x, ⋯⟩, ⋯⟩ ≫ stalkPushforward CommRingCat X.toΓSpecBase X.presheaf ↑⟨x, ⋯⟩
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<VAR>x : ↑X.toTopCat<GOAL>X.toToΓSpecMapBasicOpen 1 ≫ ((pushforward CommRingCat X.toΓSpecSheafedSpace.base).obj X.presheaf).germ ⟨X.toΓSpecFun x, ⋯⟩ = ((pushforward CommRingCat X.toΓSpecBase).obj X.presheaf).germ ⟨X.toΓSpecBase ↑⟨x, ⋯⟩, ⋯⟩
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<VAR>x : ↑X.toTopCat<GOAL>((pushforward CommRingCat X.toΓSpecBase).obj X.presheaf).map ⋯.hom.op ≫ ((pushforward CommRingCat X.toΓSpecSheafedSpace.base).obj X.presheaf).germ ⟨X.toΓSpecFun x, ⋯⟩ = ((pushforward CommRingCat X.toΓSpecBase).obj X.presheaf).germ ⟨X.toΓSpecBase ↑⟨x, ⋯⟩, ⋯⟩
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>M₃ : Type u_4<VAR>ι₁ : Type u_5<VAR>ι₂ : Type u_6<VAR>ι₃ : Type u_7<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : AddCommGroup M₃<VAR>inst✝⁷ : Module R M₁<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : Module R M₃<VAR>inst✝⁴ : Fintype ι₁<VAR>inst✝³ : Fintype ι₂<VAR>inst✝² : Finite ι₃<VAR>inst✝¹ : DecidableEq ι₁<VAR>inst✝ : DecidableEq ι₂<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>b₃ : Basis ι₃ R M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>f : M₁ →ₗ[R] M₂<VAR>i : ι₃<GOAL>toMvPolynomial b₁ b₃ (g ∘ₗ f) i = (bind₁ (toMvPolynomial b₁ b₂ f)) (toMvPolynomial b₂ b₃ g i)
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>M₃ : Type u_4<VAR>ι₁ : Type u_5<VAR>ι₂ : Type u_6<VAR>ι₃ : Type u_7<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : AddCommGroup M₃<VAR>inst✝⁷ : Module R M₁<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : Module R M₃<VAR>inst✝⁴ : Fintype ι₁<VAR>inst✝³ : Fintype ι₂<VAR>inst✝² : Finite ι₃<VAR>inst✝¹ : DecidableEq ι₁<VAR>inst✝ : DecidableEq ι₂<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>b₃ : Basis ι₃ R M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>f : M₁ →ₗ[R] M₂<VAR>i : ι₃<GOAL>(bind₁ ((toMatrix b₁ b₂) f).toMvPolynomial) (((toMatrix b₂ b₃) g).toMvPolynomial i) = (bind₁ (toMvPolynomial b₁ b₂ f)) (((toMatrix b₂ b₃) g).toMvPolynomial i)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>F G : Cᵒᵖ ⥤ A<VAR>X : C<VAR>φ : { obj := fun X => (Over.forget (unop X)).op ⋙ F ⟶ (Over.forget (unop X)).op ⋙ G, map := fun {X Y} f => whiskerLeft (Over.map f.unop).op }.obj (op X)<VAR>Y : Over (unop (op X))<GOAL>({ obj := fun X => (Over.forget (unop X)).op ⋙ F ⟶ (Over.forget (unop X)).op ⋙ G, map := fun {X Y} f => whiskerLeft (Over.map f.unop).op }.map (𝟙 (op X)) φ).app (op Y) = (𝟙 ({ obj := fun X => (Over.forget (unop X)).op ⋙ F ⟶ (Over.forget (unop X)).op ⋙ G, map := fun {X Y} f => whiskerLeft (Over.map f.unop).op }.obj (op X)) φ).app (op Y)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>F G : Cᵒᵖ ⥤ A<VAR>X Y Z : C<VAR>f : Y ⟶ X<VAR>g : Z ⟶ Y<VAR>φ : { obj := fun X => (Over.forget (unop X)).op ⋙ F ⟶ (Over.forget (unop X)).op ⋙ G, map := fun {X Y} f => whiskerLeft (Over.map f.unop).op }.obj (op X)<VAR>W : Over (unop (op Z))<GOAL>({ obj := fun X => (Over.forget (unop X)).op ⋙ F ⟶ (Over.forget (unop X)).op ⋙ G, map := fun {X Y} f => whiskerLeft (Over.map f.unop).op }.map (op f ≫ op g) φ).app (op W) = (({ obj := fun X => (Over.forget (unop X)).op ⋙ F ⟶ (Over.forget (unop X)).op ⋙ G, map := fun {X Y} f => whiskerLeft (Over.map f.unop).op }.map (op f) ≫ { obj := fun X => (Over.forget (unop X)).op ⋙ F ⟶ (Over.forget (unop X)).op ⋙ G, map := fun {X Y} f => whiskerLeft (Over.map f.unop).op }.map (op g)) φ).app (op W)
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>n : ℤ<GOAL>(T n).degree = ↑n
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>n : ℤ<GOAL>(C 1 * T n).degree = ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : GroupWithZero α<VAR>inst✝¹ : MulAction α β<VAR>s✝ t : Finset β<VAR>a✝ : α<VAR>b : β<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>(op a • s)⁻¹ = a⁻¹ • s⁻¹
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : GroupWithZero α<VAR>inst✝¹ : MulAction α β<VAR>s✝ t : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>(op 0 • s)⁻¹ = 0⁻¹ • s⁻¹
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : GroupWithZero α<VAR>inst✝¹ : MulAction α β<VAR>s✝ t : Finset β<VAR>a✝ : α<VAR>b : β<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>ha : a ≠ 0<GOAL>(op a • s)⁻¹ = a⁻¹ • s⁻¹
<VAR>x y : ℝ<VAR>hx : 0 < x<GOAL>log x = expOrderIso.symm ⟨x, hx⟩
<VAR>x y : ℝ<VAR>hx : 0 < x<GOAL>expOrderIso.symm ⟨|x|, ⋯⟩ = expOrderIso.symm ⟨x, hx⟩