ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>inst✝ : IsDedekindDomain S<VAR>i : ℕ<VAR>ih : cardQuot (P ^ i) = cardQuot P ^ i<VAR>this : P ^ (i + 1) < P ^ i<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>f g : (c : S) → c ∈ P ^ i → S<VAR>hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)<VAR>hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c<VAR>k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S<VAR>hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i<VAR>hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'<GOAL>Function.Surjective fun c' => Quotient.mk'' (f (k ↑c' ⋯) ⋯)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : SFinite ν<VAR>f : α × β → E<VAR>hf : StronglyMeasurable f<GOAL>StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂ν
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : SFinite ν<VAR>f : α × β → E<VAR>hf : StronglyMeasurable (uncurry (Function.curry f))<GOAL>StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂ν
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : CommRing α<VAR>A✝ B : Matrix n n α<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>A : Matrix m m α<VAR>e₁ e₂ : n ≃ m<GOAL>IsUnit (A.submatrix ⇑e₁ ⇑e₂) ↔ IsUnit A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : y ∈ EMetric.ball x r<GOAL>AnalyticAt 𝕜 f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : y ∈ EMetric.ball x r<VAR>this : ↑‖y - x‖₊ < r<GOAL>AnalyticAt 𝕜 f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : y ∈ EMetric.ball x r<VAR>this✝ : ↑‖y - x‖₊ < r<VAR>this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) (x + (y - x)) (r - ↑‖y - x‖₊)<GOAL>AnalyticAt 𝕜 f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : y ∈ EMetric.ball x r<VAR>this✝ : ↑‖y - x‖₊ < r<VAR>this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) y (r - ↑‖y - x‖₊)<GOAL>AnalyticAt 𝕜 f y
<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>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : 𝓝[s \ {x}] x = ⊥<GOAL>HasFDerivWithinAt f f' s x
<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>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : 𝓝[s \ {x}] x = ⊥<GOAL>(fun x' => f x' - f x - f' (x' - x)) =o[⊥] fun x' => x' - x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s : Set M<GOAL>sSup ((fun x => lieSpan R L {x}) '' ↑N) = N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s : Set M<GOAL>N ≤ sSup ((fun x => lieSpan R L {x}) '' ↑N)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s : Set M<GOAL>↑N ≤ sSup {x | ∃ s, (∃ x ∈ N, lieSpan R L {x} = s) ∧ ↑s = x}
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N'✝ : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s : Set M<VAR>m : M<VAR>hm : m ∈ ↑N<VAR>N' : Submodule R M<VAR>hN' : ∀ p ∈ {x | ∃ s, (∃ x ∈ N, lieSpan R L {x} = s) ∧ ↑s = x}, p ≤ N'<GOAL>m ∈ N'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N'✝ : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s : Set M<VAR>m : M<VAR>hm : m ∈ ↑N<VAR>N' : Submodule R M<VAR>hN' : ∀ m ∈ N, ↑(lieSpan R L {m}) ≤ N'<GOAL>m ∈ N'
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝³ : RCLike 𝕂<VAR>inst✝² : NormedCommRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → 𝔸<GOAL>exp 𝕂 (∑ i ∈ s, f i) = ∏ i ∈ s, exp 𝕂 (f i)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝³ : RCLike 𝕂<VAR>inst✝² : NormedCommRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → 𝔸<GOAL>(↑s).Pairwise fun i j => Commute (f i) (f j)
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>hI : I.IsPrime<VAR>x y : α<VAR>h : x ∈ I<GOAL>x * y ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>hI : I.IsPrime<VAR>x y : α<VAR>h : y ∈ I<GOAL>x * y ∈ I
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>T R (n - 1) = 2 * X * T R n - T R (n + 1)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>n : ℕ<VAR>x : α<VAR>s : Multiset α<VAR>y : α<GOAL>count y (replicate n x ∩ s) = count y (replicate (min n (count x s)) x)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>n : ℕ<VAR>x : α<VAR>s : Multiset α<VAR>y : α<GOAL>min (if y = x then n else 0) (count y s) = if y = x then min n (count x s) else 0
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝ : ConcreteCategory C<VAR>F : Presheaf C X<VAR>U V : Opens ↑X<VAR>x : ↑X<VAR>hxU : x ∈ U<VAR>hxV : x ∈ V<VAR>W : Opens ↑X<VAR>hxW : x ∈ W<VAR>iWU : W ⟶ U<VAR>iWV : W ⟶ V<VAR>sU : (forget C).obj (F.obj (op U))<VAR>sV : (forget C).obj (F.obj (op V))<VAR>ih : (F.map iWU.op) sU = (F.map iWV.op) sV<GOAL>(F.germ ⟨x, hxU⟩) sU = (F.germ ⟨x, hxV⟩) sV
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F G : C ⥤ Type w<VAR>a : C<VAR>x✝ : (F ⨿ G).obj a<GOAL>(fun z => (binaryCoproductIso F G).inv.app a z) ((fun z => (binaryCoproductIso F G).hom.app a z) x✝) = x✝
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F G : C ⥤ Type w<VAR>a : C<VAR>x✝ : F.obj a ⊕ G.obj a<GOAL>(fun z => (binaryCoproductIso F G).hom.app a z) ((fun z => (binaryCoproductIso F G).inv.app a z) x✝) = x✝
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : Semiring R<VAR>r : R<VAR>n : ℕ<GOAL>(ascPochhammer ℕ n).smeval r = eval r (ascPochhammer R n)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i j : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootPairing ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>hc : range ⇑P₁.coroot = range ⇑P₂.coroot<GOAL>P₁ = P₂
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i j : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootPairing ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>hc : range ⇑P₁.coroot = range ⇑P₂.coroot<VAR>hp : P₁.coroot = P₂.coroot → P₁.reflection_perm = P₂.reflection_perm<GOAL>P₁ = P₂
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i j : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootPairing ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>hc : range ⇑P₁.coroot = range ⇑P₂.coroot<VAR>hp : P₁.coroot = P₂.coroot → P₁.reflection_perm = P₂.reflection_perm<GOAL>P₁.coroot = P₂.coroot
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i j : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootPairing ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>hc : range ⇑P₁.coroot = range ⇑P₂.coroot<VAR>hp : P₁.coroot = P₂.coroot → P₁.reflection_perm = P₂.reflection_perm<VAR>this : NoZeroSMulDivisors ℤ M<GOAL>P₁.coroot = P₂.coroot
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootPairing ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>hc : range ⇑P₁.coroot = range ⇑P₂.coroot<VAR>hp : P₁.coroot = P₂.coroot → P₁.reflection_perm = P₂.reflection_perm<VAR>this : NoZeroSMulDivisors ℤ M<VAR>i : ι<GOAL>P₁.coroot i = P₂.coroot i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootPairing ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>hc : range ⇑P₁.coroot = range ⇑P₂.coroot<VAR>hp : P₁.coroot = P₂.coroot → P₁.reflection_perm = P₂.reflection_perm<VAR>this : NoZeroSMulDivisors ℤ M<VAR>i : ι<GOAL>((span R (range ⇑P₁.root)).subtype.dualMap ∘ₗ P₁.toLin.flip) (P₁.coroot i) = ((span R (range ⇑P₁.root)).subtype.dualMap ∘ₗ P₁.toLin.flip) (P₂.coroot i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootPairing ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>hc : range ⇑P₁.coroot = range ⇑P₂.coroot<VAR>hp : P₁.coroot = P₂.coroot → P₁.reflection_perm = P₂.reflection_perm<VAR>this : NoZeroSMulDivisors ℤ M<VAR>i : ι<GOAL>(span R (range ⇑P₁.root)).subtype.dualMap (P₁.toLin.flip (P₁.coroot i)) = (span R (range ⇑P₁.root)).subtype.dualMap (P₁.toLin.flip (P₂.coroot i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootPairing ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>hc : range ⇑P₁.coroot = range ⇑P₂.coroot<VAR>hp : P₁.coroot = P₂.coroot → P₁.reflection_perm = P₂.reflection_perm<VAR>this : NoZeroSMulDivisors ℤ M<VAR>i : ι<GOAL>P₁.root i ∈ span R (range ⇑P₁.root)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootPairing ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>hc : range ⇑P₁.coroot = range ⇑P₂.coroot<VAR>hp : P₁.coroot = P₂.coroot → P₁.reflection_perm = P₂.reflection_perm<VAR>this : NoZeroSMulDivisors ℤ M<VAR>i : ι<GOAL>(P₁.toLin.flip (P₁.coroot i)) (P₁.root i) = 2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootPairing ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>hc : range ⇑P₁.coroot = range ⇑P₂.coroot<VAR>hp : P₁.coroot = P₂.coroot → P₁.reflection_perm = P₂.reflection_perm<VAR>this : NoZeroSMulDivisors ℤ M<VAR>i : ι<GOAL>MapsTo (⇑(preReflection (P₁.root i) (P₁.toLin.flip (P₁.coroot i)))) (range ⇑P₁.root) (range ⇑P₁.root)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootPairing ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>hc : range ⇑P₁.coroot = range ⇑P₂.coroot<VAR>hp : P₁.coroot = P₂.coroot → P₁.reflection_perm = P₂.reflection_perm<VAR>this : NoZeroSMulDivisors ℤ M<VAR>i : ι<GOAL>(P₁.toLin.flip (P₂.coroot i)) (P₁.root i) = 2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootPairing ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>hc : range ⇑P₁.coroot = range ⇑P₂.coroot<VAR>hp : P₁.coroot = P₂.coroot → P₁.reflection_perm = P₂.reflection_perm<VAR>this : NoZeroSMulDivisors ℤ M<VAR>i : ι<GOAL>MapsTo (⇑(preReflection (P₁.root i) (P₁.toLin.flip (P₂.coroot i)))) (range ⇑P₁.root) (range ⇑P₁.root)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁹ : Category.{u_5, u_1} C<VAR>inst✝⁸ : Category.{u_7, u_2} D<VAR>inst✝⁷ : Category.{u_6, u_3} A<VAR>L : C ⥤ D<VAR>F : D ⥤ A<VAR>G : C ⥤ A<VAR>e : L ⋙ F ≅ G<VAR>M : Type u_4<VAR>inst✝⁶ : AddMonoid M<VAR>inst✝⁵ : HasShift C M<VAR>inst✝⁴ : HasShift D M<VAR>inst✝³ : L.CommShift M<VAR>inst✝² : G.ShiftSequence M<VAR>F' : M → D ⥤ A<VAR>e' : (m : M) → L ⋙ F' m ≅ G.shift m<VAR>inst✝¹ : ((whiskeringLeft C D A).obj L).Full<VAR>inst✝ : ((whiskeringLeft C D A).obj L).Faithful<VAR>n : M<VAR>X Y : C<VAR>f : X ⟶ (shiftFunctor C n).obj Y<VAR>a a' : M<VAR>h : n + a = a'<GOAL>(F.shift a).map (L.map f ≫ (L.commShiftIso n).hom.app Y) ≫ (F.shiftIso n a a' h).hom.app (L.obj Y) = (e' a).hom.app X ≫ ((G.shift a).map f ≫ (G.shiftIso n a a' h).hom.app Y) ≫ (e' a').inv.app Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁹ : Category.{u_5, u_1} C<VAR>inst✝⁸ : Category.{u_7, u_2} D<VAR>inst✝⁷ : Category.{u_6, u_3} A<VAR>L : C ⥤ D<VAR>F : D ⥤ A<VAR>G : C ⥤ A<VAR>e : L ⋙ F ≅ G<VAR>M : Type u_4<VAR>inst✝⁶ : AddMonoid M<VAR>inst✝⁵ : HasShift C M<VAR>inst✝⁴ : HasShift D M<VAR>inst✝³ : L.CommShift M<VAR>inst✝² : G.ShiftSequence M<VAR>F' : M → D ⥤ A<VAR>e' : (m : M) → L ⋙ F' m ≅ G.shift m<VAR>inst✝¹ : ((whiskeringLeft C D A).obj L).Full<VAR>inst✝ : ((whiskeringLeft C D A).obj L).Faithful<VAR>n : M<VAR>X Y : C<VAR>f : X ⟶ (shiftFunctor C n).obj Y<VAR>a a' : M<VAR>h : n + a = a'<GOAL>(F.shift a).map (L.map f) ≫ (F.shift a).map ((L.commShiftIso n).hom.app Y) ≫ (F.shift a).map ((L.commShiftIso n).inv.app Y) ≫ (e' a).hom.app ((shiftFunctor C n).obj Y) ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y = (e' a).hom.app X ≫ (G.shift a).map f ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁹ : Category.{u_5, u_1} C<VAR>inst✝⁸ : Category.{u_7, u_2} D<VAR>inst✝⁷ : Category.{u_6, u_3} A<VAR>L : C ⥤ D<VAR>F : D ⥤ A<VAR>G : C ⥤ A<VAR>e : L ⋙ F ≅ G<VAR>M : Type u_4<VAR>inst✝⁶ : AddMonoid M<VAR>inst✝⁵ : HasShift C M<VAR>inst✝⁴ : HasShift D M<VAR>inst✝³ : L.CommShift M<VAR>inst✝² : G.ShiftSequence M<VAR>F' : M → D ⥤ A<VAR>e' : (m : M) → L ⋙ F' m ≅ G.shift m<VAR>inst✝¹ : ((whiskeringLeft C D A).obj L).Full<VAR>inst✝ : ((whiskeringLeft C D A).obj L).Faithful<VAR>n : M<VAR>X Y : C<VAR>f : X ⟶ (shiftFunctor C n).obj Y<VAR>a a' : M<VAR>h : n + a = a'<GOAL>(F.shift a).map (L.map f) ≫ (F.shift a).map ((L.commShiftIso n).hom.app Y ≫ (L.commShiftIso n).inv.app Y) ≫ (e' a).hom.app ((shiftFunctor C n).obj Y) ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y = (e' a).hom.app X ≫ (G.shift a).map f ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁹ : Category.{u_5, u_1} C<VAR>inst✝⁸ : Category.{u_7, u_2} D<VAR>inst✝⁷ : Category.{u_6, u_3} A<VAR>L : C ⥤ D<VAR>F : D ⥤ A<VAR>G : C ⥤ A<VAR>e : L ⋙ F ≅ G<VAR>M : Type u_4<VAR>inst✝⁶ : AddMonoid M<VAR>inst✝⁵ : HasShift C M<VAR>inst✝⁴ : HasShift D M<VAR>inst✝³ : L.CommShift M<VAR>inst✝² : G.ShiftSequence M<VAR>F' : M → D ⥤ A<VAR>e' : (m : M) → L ⋙ F' m ≅ G.shift m<VAR>inst✝¹ : ((whiskeringLeft C D A).obj L).Full<VAR>inst✝ : ((whiskeringLeft C D A).obj L).Faithful<VAR>n : M<VAR>X Y : C<VAR>f : X ⟶ (shiftFunctor C n).obj Y<VAR>a a' : M<VAR>h : n + a = a'<GOAL>(F.shift a).map (L.map f) ≫ (e' a).hom.app ((shiftFunctor C n).obj Y) ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y = (e' a).hom.app X ≫ (G.shift a).map f ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>e : α ≃ β<VAR>s : Set α<VAR>t : Set β<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>x : α<GOAL>(swap a b) x ∈ s ↔ x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>f : α →₀ M<VAR>a a' : α<VAR>ha : a ≠ a'<VAR>b : M<GOAL>erase a (f.update a' b) = (erase a f).update a' b
<VAR>R : Type u_1<VAR>n : ℕ<VAR>h0 : n ≠ 0<GOAL>ω n = Ω n ↔ Squarefree n
<VAR>R : Type u_1<VAR>n : ℕ<VAR>h0 : n ≠ 0<GOAL>n.primeFactorsList.dedup.length = Ω n ↔ n.primeFactorsList.Nodup
<VAR>b✝ x y a b : ℝ<VAR>h₁ : a ≠ 0<VAR>h₂ : b ≠ 0<VAR>c : ℝ<GOAL>(logb (a / b) c)⁻¹ = (logb a c)⁻¹ - (logb b c)⁻¹
<VAR>b✝ x y a b : ℝ<VAR>h₁ : a ≠ 0<VAR>h₂ : b ≠ 0<VAR>c : ℝ<GOAL>logb c (a / b) = logb c a - logb c b
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>G : C<GOAL>IsCoseparator G ↔ (preadditiveYoneda.obj G).Faithful
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>G : C<GOAL>(preadditiveYoneda.obj G ⋙ forget AddCommGrp).Faithful ↔ (preadditiveYoneda.obj G).Faithful
<VAR>R : Type u_1<VAR>inst✝¹⁵ : Semiring R<VAR>M : Type u_2<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : Module R M<VAR>N : Type u_3<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : Module R N<VAR>P : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid P<VAR>inst✝⁹ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>N' : Type u_6<VAR>inst✝⁶ : AddCommGroup N'<VAR>inst✝⁵ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝² : AddCommMonoid M₃<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Nonempty ι<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>x✝ : ι → M₂<GOAL>(f.compLinearMap 0) x✝ = 0 x✝
<VAR>R : Type u_1<VAR>inst✝¹⁵ : Semiring R<VAR>M : Type u_2<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : Module R M<VAR>N : Type u_3<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : Module R N<VAR>P : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid P<VAR>inst✝⁹ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>N' : Type u_6<VAR>inst✝⁶ : AddCommGroup N'<VAR>inst✝⁵ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝² : AddCommMonoid M₃<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Nonempty ι<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>x✝ : ι → M₂<GOAL>f 0 = 0
<VAR>X : Scheme<VAR>inst✝ : IsReduced X<VAR>H : IrreducibleSpace ↑↑X.toPresheafedSpace<VAR>U : X.Opens<VAR>hU : Nonempty ↑↑(↑U).toPresheafedSpace<GOAL>IsDomain ↑Γ(X, U)
<VAR>X : Scheme<VAR>inst✝ : IsReduced X<VAR>H : IrreducibleSpace ↑↑X.toPresheafedSpace<VAR>U : X.Opens<VAR>hU : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>this : ∃ x y, x ≠ y<GOAL>IsDomain ↑Γ(X, U)
<VAR>X : Scheme<VAR>inst✝ : IsReduced X<VAR>H : IrreducibleSpace ↑↑X.toPresheafedSpace<VAR>U : X.Opens<VAR>hU : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>this✝ : ∃ x y, x ≠ y<VAR>this : NoZeroDivisors ↑(X.presheaf.obj (op U))<GOAL>IsDomain ↑Γ(X, U)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : OrderedAddCommMonoid M<VAR>inst✝ : OrderClosedTopology M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (n : ℕ), MeasurableSet (f n)<VAR>hf₂ : ∀ (n : ℕ), v.restrict (f n) ≤ w.restrict (f n)<GOAL>v.restrict (⋃ n, f n) ≤ w.restrict (⋃ n, f n)