ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : RightHomologyMapData φ h₁ h₂ := rightHomologyMapData φ h₁ h₂<GOAL>(rightHomologyMap' φ h₁ h₂).op = leftHomologyMap' (opMap φ) h₂.op h₁.op
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>x y z : α<VAR>h : EMetric.diam s ≠ ⊤<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>dist x y ≤ diam s
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>x y z : α<VAR>h : EMetric.diam s ≠ ⊤<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>(edist x y).toReal ≤ (EMetric.diam s).toReal
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>x y z : α<VAR>h : EMetric.diam s ≠ ⊤<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>edist x y ≤ EMetric.diam s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>hf : (mulSupport f).Infinite<GOAL>∏ᶠ (i : α), f i = 1
<VAR>C : Type v₁<VAR>inst✝² : Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsCofilteredOrEmpty C<GOAL>F.Initial ↔ ∀ (d : D), IsCofiltered (CostructuredArrow F d)
<VAR>C : Type v₁<VAR>inst✝² : Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsCofilteredOrEmpty C<GOAL>F.Initial → ∀ (d : D), IsCofiltered (CostructuredArrow F d)
<VAR>C : Type v₁<VAR>inst✝² : Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsCofilteredOrEmpty C<GOAL>((∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) ∧ ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s') → ∀ (d : D), IsCofiltered (CostructuredArrow F d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>f✝ g✝ : α → M<VAR>a b : α<VAR>s t : Set α<VAR>inst✝ : DivisionCommMonoid G<VAR>f g : α → G<VAR>hf : (mulSupport f).Finite<VAR>hg : (mulSupport g).Finite<GOAL>∏ᶠ (i : α), f i / g i = (∏ᶠ (i : α), f i) / ∏ᶠ (i : α), g i
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace ℝ X<VAR>inst✝ : HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>hx : x ∈ closedBall c f.rIn<GOAL>↑f x = 1
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace ℝ X<VAR>inst✝ : HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>hx : x ∈ closedBall c f.rIn<GOAL>‖(fun x => f.rIn⁻¹ • (x - c)) x‖ ≤ 1
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>f : K[X]<VAR>hf1 : ¬IsUnit f<VAR>hf2 : ¬f = 0<GOAL>f.factor ∣ f
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>f : K[X]<VAR>hf1 : ¬IsUnit f<VAR>hf2 : ¬f = 0<GOAL>Classical.choose ⋯ ∣ f
<VAR>a b c d m✝ n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n m : ℕ<VAR>h : 0 < m<GOAL>1 ≤ m ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Fintype α<VAR>s t : Finset α<GOAL>univ = ∅ ↔ IsEmpty α
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>x y : M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>h : SameRay R x (-x)<VAR>a✝ : Nontrivial M<GOAL>x = 0
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>x y : M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>h : SameRay R x (-x)<VAR>a✝ : Nontrivial M<VAR>this : Nontrivial R<GOAL>x = 0
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>x y : M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>h : SameRay R x (-x)<VAR>a✝ : Nontrivial M<VAR>this : Nontrivial R<GOAL>SameRay R x (-1 • x)
<VAR>n✝ b n m r : ℕ<VAR>l : List ℕ<VAR>e : r + b * m = n<VAR>hr : r < b<VAR>h : b.digits m = l<VAR>b2 : 1 < b<VAR>m0 : 0 < m<VAR>b0 : 0 < b<VAR>n0 : 0 < n<GOAL>b.digits n = r :: l
<VAR>n✝ b n : ℕ<VAR>l : List ℕ<VAR>b2 : 1 < b<VAR>b0 : 0 < b<VAR>n0 : 0 < n<VAR>h : b.digits (n / b) = l<VAR>m0 : 0 < n / b<VAR>hr : n % b < b<VAR>e : n % b + b * (n / b) = n<GOAL>b.digits n = n % b :: l
<VAR>n✝ b n : ℕ<VAR>b2 : 1 < b<VAR>b0 : 0 < b<VAR>n0 : 0 < n<VAR>m0 : 0 < n / b<VAR>hr : n % b < b<VAR>e : n % b + b * (n / b) = n<GOAL>b.digits n = n % b :: b.digits (n / b)
<VAR>F : Type u_1<VAR>inst✝⁷ : AddCommGroup F<VAR>inst✝⁶ : Module ℝ F<VAR>inst✝⁵ : TopologicalSpace F<VAR>E✝ : Type u_2<VAR>inst✝⁴ : AddCommGroup E✝<VAR>inst✝³ : Module ℝ E✝<VAR>inst✝² : TopologicalSpace E✝<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : ContinuousSMul ℝ F<VAR>E : Submodule ℝ F<VAR>hcodim : 1 < Module.rank ℝ (F ⧸ E)<VAR>x : F<VAR>hx : x ∈ (↑E)ᶜ<GOAL>(convexHull ℝ) (connectedComponentIn (↑E)ᶜ x) = univ
<VAR>F : Type u_1<VAR>inst✝⁷ : AddCommGroup F<VAR>inst✝⁶ : Module ℝ F<VAR>inst✝⁵ : TopologicalSpace F<VAR>E✝ : Type u_2<VAR>inst✝⁴ : AddCommGroup E✝<VAR>inst✝³ : Module ℝ E✝<VAR>inst✝² : TopologicalSpace E✝<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : ContinuousSMul ℝ F<VAR>E : Submodule ℝ F<VAR>hcodim : 1 < Module.rank ℝ (F ⧸ E)<VAR>x : F<VAR>hx : x ∈ (↑E)ᶜ<GOAL>∀ (x : F), x ∈ (convexHull ℝ) (↑E)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a t : α<VAR>ts is : List α<VAR>IH1 : ∀ l ∈ ts.permutationsAux (t :: is), l ~ ts ++ t :: is<VAR>IH2 : ∀ l ∈ is.permutationsAux [], l ~ is ++ []<VAR>l : List α<VAR>m : l ∈ (t :: ts).permutationsAux is<GOAL>l ~ t :: ts ++ is
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a t : α<VAR>ts is : List α<VAR>IH1 : ∀ l ∈ ts.permutationsAux (t :: is), l ~ ts ++ t :: is<VAR>IH2 : ∀ l ∈ is.permutationsAux [], l ~ is ++ []<VAR>l : List α<VAR>m : l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is :: is.permutationsAux [] ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts<GOAL>l ~ t :: ts ++ is
<VAR>R : Type u<VAR>inst✝¹⁷ : CommRing R<VAR>S : Type v<VAR>inst✝¹⁶ : CommRing S<VAR>f✝ : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝¹⁵ : IsDedekindDomain S<VAR>inst✝¹⁴ : Algebra R S<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : IsDedekindDomain R<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra S L<VAR>inst✝⁷ : IsFractionRing S L<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : IsScalarTower R S L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : IsNoetherian R S<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : p.IsMaximal<VAR>hp0 : p ≠ ⊥<VAR>e : Ideal S → ℕ := ramificationIdx (algebraMap R S) p<VAR>f : Ideal S → [inst : p.IsMaximal] → ℕ := inertiaDeg (algebraMap R S) p<GOAL>∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, e P * f P = finrank K L
<VAR>R : Type u<VAR>inst✝¹⁷ : CommRing R<VAR>S : Type v<VAR>inst✝¹⁶ : CommRing S<VAR>f✝ : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝¹⁵ : IsDedekindDomain S<VAR>inst✝¹⁴ : Algebra R S<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : IsDedekindDomain R<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra S L<VAR>inst✝⁷ : IsFractionRing S L<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : IsScalarTower R S L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : IsNoetherian R S<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : p.IsMaximal<VAR>hp0 : p ≠ ⊥<VAR>e : Ideal S → ℕ := ramificationIdx (algebraMap R S) p<VAR>f : Ideal S → [inst : p.IsMaximal] → ℕ := inertiaDeg (algebraMap R S) p<VAR>inj_RL : Function.Injective ⇑(algebraMap R L)<GOAL>∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, e P * f P = finrank K L
<VAR>R : Type u<VAR>inst✝¹⁷ : CommRing R<VAR>S : Type v<VAR>inst✝¹⁶ : CommRing S<VAR>f✝ : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝¹⁵ : IsDedekindDomain S<VAR>inst✝¹⁴ : Algebra R S<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : IsDedekindDomain R<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra S L<VAR>inst✝⁷ : IsFractionRing S L<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : IsScalarTower R S L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : IsNoetherian R S<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : p.IsMaximal<VAR>hp0 : p ≠ ⊥<VAR>e : Ideal S → ℕ := ramificationIdx (algebraMap R S) p<VAR>f : Ideal S → [inst : p.IsMaximal] → ℕ := inertiaDeg (algebraMap R S) p<VAR>inj_RL : Function.Injective ⇑(algebraMap R L)<VAR>inj_RS : Function.Injective ⇑(algebraMap R S)<GOAL>∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, e P * f P = finrank K L
<VAR>R : Type u<VAR>inst✝¹⁷ : CommRing R<VAR>S : Type v<VAR>inst✝¹⁶ : CommRing S<VAR>f✝ : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝¹⁵ : IsDedekindDomain S<VAR>inst✝¹⁴ : Algebra R S<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : IsDedekindDomain R<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra S L<VAR>inst✝⁷ : IsFractionRing S L<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : IsScalarTower R S L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : IsNoetherian R S<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : p.IsMaximal<VAR>hp0 : p ≠ ⊥<VAR>e : Ideal S → ℕ := ramificationIdx (algebraMap R S) p<VAR>f : Ideal S → [inst : p.IsMaximal] → ℕ := inertiaDeg (algebraMap R S) p<VAR>inj_RL : Function.Injective ⇑(algebraMap R L)<VAR>inj_RS : Function.Injective ⇑(algebraMap R S)<GOAL>∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, e P * f P = ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset.attach, finrank (R ⧸ p) (S ⧸ ↑P ^ e ↑P)
<VAR>R : Type u<VAR>inst✝¹⁷ : CommRing R<VAR>S : Type v<VAR>inst✝¹⁶ : CommRing S<VAR>f✝ : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝¹⁵ : IsDedekindDomain S<VAR>inst✝¹⁴ : Algebra R S<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : IsDedekindDomain R<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra S L<VAR>inst✝⁷ : IsFractionRing S L<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : IsScalarTower R S L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : IsNoetherian R S<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : p.IsMaximal<VAR>hp0 : p ≠ ⊥<VAR>e : Ideal S → ℕ := ramificationIdx (algebraMap R S) p<VAR>f : Ideal S → [inst : p.IsMaximal] → ℕ := inertiaDeg (algebraMap R S) p<VAR>inj_RL : Function.Injective ⇑(algebraMap R L)<VAR>inj_RS : Function.Injective ⇑(algebraMap R S)<GOAL>finrank (R ⧸ p) ((P : { x // x ∈ (factors (map (algebraMap R S) p)).toFinset }) → S ⧸ ↑P ^ e ↑P) = finrank (R ⧸ p) (S ⧸ map (algebraMap R S) p)
<VAR>R : Type u<VAR>inst✝¹⁷ : CommRing R<VAR>S : Type v<VAR>inst✝¹⁶ : CommRing S<VAR>f✝ : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝¹⁵ : IsDedekindDomain S<VAR>inst✝¹⁴ : Algebra R S<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : IsDedekindDomain R<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra S L<VAR>inst✝⁷ : IsFractionRing S L<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : IsScalarTower R S L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : IsNoetherian R S<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : p.IsMaximal<VAR>hp0 : p ≠ ⊥<VAR>e : Ideal S → ℕ := ramificationIdx (algebraMap R S) p<VAR>f : Ideal S → [inst : p.IsMaximal] → ℕ := inertiaDeg (algebraMap R S) p<VAR>inj_RL : Function.Injective ⇑(algebraMap R L)<VAR>inj_RS : Function.Injective ⇑(algebraMap R S)<GOAL>finrank (R ⧸ p) (S ⧸ map (algebraMap R S) p) = finrank K L
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>m : ℕ<GOAL>normEDS b c d (2 * (↑m + 2) + 1) = normEDS b c d (↑m + 4) * normEDS b c d (↑m + 2) ^ 3 - normEDS b c d (↑m + 1) * normEDS b c d (↑m + 3) ^ 3
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>m : ℕ<GOAL>(preNormEDS' (b ^ 4) c d (2 * (m + 2) + 1) * if Even (2 * (m + 2) + 1) then b else 1) = (preNormEDS' (b ^ 4) c d (m + 4) * if Even (m + 4) then b else 1) * (preNormEDS' (b ^ 4) c d (m + 2) * if Even (m + 2) then b else 1) ^ 3 - (preNormEDS' (b ^ 4) c d (m + 1) * if Even (m + 1) then b else 1) * (preNormEDS' (b ^ 4) c d (m + 3) * if Even (m + 3) then b else 1) ^ 3
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>m : ℕ<GOAL>((preNormEDS' (b ^ 4) c d (m + 4) * preNormEDS' (b ^ 4) c d (m + 2) ^ 3 * if Even m then b ^ 4 else 1) - preNormEDS' (b ^ 4) c d (m + 1) * preNormEDS' (b ^ 4) c d (m + 3) ^ 3 * if Even m then 1 else b ^ 4) * 1 = (preNormEDS' (b ^ 4) c d (m + 4) * if Even m then b else 1) * (preNormEDS' (b ^ 4) c d (m + 2) * if Even m then b else 1) ^ 3 - (preNormEDS' (b ^ 4) c d (m + 1) * if Even m then 1 else b) * (preNormEDS' (b ^ 4) c d (m + 3) * if Even m then 1 else b) ^ 3
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝¹ : Monoid M<VAR>a✝ b c : M<VAR>m n : ℕ<VAR>P : Prop<VAR>inst✝ : Decidable P<VAR>a : M<GOAL>(a ^ if P then 1 else 0) = if P then a else 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>i f : N →ₗ[R] M<VAR>hi : Injective ⇑i<VAR>hf : Surjective ⇑f<GOAL>Injective ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>i f : N →ₗ[R] M<VAR>hi : Injective ⇑i<VAR>hf : Surjective ⇑f<VAR>this : IsNoetherian R N<GOAL>Injective ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>i f : N →ₗ[R] M<VAR>hi : Injective ⇑i<VAR>hf : Surjective ⇑f<VAR>this : IsNoetherian R N<VAR>n : ℕ<VAR>H : ∀ (m : ℕ), n ≤ m → { toFun := fun n => f.iterateMapComap i n ⊥, monotone' := ⋯ } n = { toFun := fun n => f.iterateMapComap i n ⊥, monotone' := ⋯ } m<GOAL>Injective ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>x : A<VAR>y : B<VAR>h : IsIntegral R y<GOAL>IsIntegral A (x ⊗ₜ[R] y)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>x : A<VAR>y : B<VAR>h : IsIntegral R y<GOAL>IsIntegral A (x • 1 ⊗ₜ[R] y)
<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>a b c p : α<VAR>hc : c ≠ 0<GOAL>a / c ≡ b / c [PMOD p] ↔ a ≡ b [PMOD p * c]
<VAR>α β : Type u<VAR>m n : ℕ<GOAL>↑(m ^ n) = ↑m ^ ↑n
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>X Y : Dial C<VAR>e₁ : X.src ≅ Y.src<VAR>e₂ : X.tgt ≅ Y.tgt<VAR>eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel<GOAL>(Subobject.pullback π(π₁, π₂ ≫ e₂.inv)).obj X.rel ≤ (Subobject.pullback (prod.map e₁.hom (𝟙 Y.tgt))).obj Y.rel
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>X Y : Dial C<VAR>e₁ : X.src ≅ Y.src<VAR>e₂ : X.tgt ≅ Y.tgt<VAR>eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel<GOAL>(Subobject.pullback (π(π₁, π₂ ≫ e₂.inv) ≫ prod.map e₁.hom e₂.hom)).obj Y.rel ≤ (Subobject.pullback (prod.map e₁.hom (𝟙 Y.tgt))).obj Y.rel
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>X Y : Dial C<VAR>e₁ : X.src ≅ Y.src<VAR>e₂ : X.tgt ≅ Y.tgt<VAR>eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel<GOAL>(Subobject.pullback (π(π₁, π₂ ≫ e₂.inv) ≫ prod.map e₁.hom e₂.hom)).obj Y.rel = (Subobject.pullback (prod.map e₁.hom (𝟙 Y.tgt))).obj Y.rel
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>X Y : Dial C<VAR>e₁ : X.src ≅ Y.src<VAR>e₂ : X.tgt ≅ Y.tgt<VAR>eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel<GOAL>(Subobject.pullback π(π₁, π₂ ≫ e₂.hom)).obj Y.rel ≤ (Subobject.pullback (prod.map e₁.inv (𝟙 X.tgt))).obj X.rel
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>X Y : Dial C<VAR>e₁ : X.src ≅ Y.src<VAR>e₂ : X.tgt ≅ Y.tgt<VAR>eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel<GOAL>(Subobject.pullback π(π₁, π₂ ≫ e₂.hom)).obj Y.rel ≤ (Subobject.pullback (prod.map e₁.inv (𝟙 X.tgt) ≫ prod.map e₁.hom e₂.hom)).obj Y.rel
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>X Y : Dial C<VAR>e₁ : X.src ≅ Y.src<VAR>e₂ : X.tgt ≅ Y.tgt<VAR>eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel<GOAL>(Subobject.pullback π(π₁, π₂ ≫ e₂.hom)).obj Y.rel = (Subobject.pullback (prod.map e₁.inv (𝟙 X.tgt) ≫ prod.map e₁.hom e₂.hom)).obj Y.rel
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝¹ : Category.{v₂, v₁} I<VAR>F : I ⥤ C<VAR>inst✝ : HasColimit F<VAR>i : I<GOAL>(coyonedaOpColimitIsoLimitCoyoneda F).hom ≫ limit.π (F.op ⋙ coyoneda) (op i) = coyoneda.map (colimit.ι F i).op
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>F : ι → α → G<VAR>f : α → G<VAR>bound : ι → α → ℝ<VAR>hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ<VAR>h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a<VAR>bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a<VAR>bound_integrable : Integrable (fun a => ∑' (n : ι), bound n a) μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)<GOAL>HasSum (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>F : ι → α → G<VAR>f : α → G<VAR>bound : ι → α → ℝ<VAR>hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ<VAR>h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a<VAR>bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a<VAR>bound_integrable : Integrable (fun a => ∑' (n : ι), bound n a) μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)<VAR>hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a<GOAL>HasSum (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>F : ι → α → G<VAR>f : α → G<VAR>bound : ι → α → ℝ<VAR>hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ<VAR>h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a<VAR>bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a<VAR>bound_integrable : Integrable (fun a => ∑' (n : ι), bound n a) μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)<VAR>hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a<VAR>hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun a => ∑' (n : ι), bound n a<GOAL>HasSum (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>F : ι → α → G<VAR>f : α → G<VAR>bound : ι → α → ℝ<VAR>hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ<VAR>h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a<VAR>bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a<VAR>bound_integrable : Integrable (fun a => ∑' (n : ι), bound n a) μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)<VAR>hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a<VAR>hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun a => ∑' (n : ι), bound n a<VAR>hF_integrable : ∀ (n : ι), Integrable (F n) μ<GOAL>HasSum (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>F : ι → α → G<VAR>f : α → G<VAR>bound : ι → α → ℝ<VAR>hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ<VAR>h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a<VAR>bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a<VAR>bound_integrable : Integrable (fun a => ∑' (n : ι), bound n a) μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)<VAR>hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a<VAR>hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun a => ∑' (n : ι), bound n a<VAR>hF_integrable : ∀ (n : ι), Integrable (F n) μ<GOAL>Tendsto (fun s => ∫ (a : α), ∑ i ∈ s, F i a ∂μ) atTop (𝓝 (∫ (a : α), f a ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>F : ι → α → G<VAR>f : α → G<VAR>bound : ι → α → ℝ<VAR>hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ<VAR>h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a<VAR>bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a<VAR>bound_integrable : Integrable (fun a => ∑' (n : ι), bound n a) μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)<VAR>hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a<VAR>hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun a => ∑' (n : ι), bound n a<VAR>hF_integrable : ∀ (n : ι), Integrable (F n) μ<GOAL>∀ᶠ (n : Finset ι) in atTop, AEStronglyMeasurable (fun a => ∑ i ∈ n, F i a) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>F : ι → α → G<VAR>f : α → G<VAR>bound : ι → α → ℝ<VAR>hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ<VAR>h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a<VAR>bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a<VAR>bound_integrable : Integrable (fun a => ∑' (n : ι), bound n a) μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)<VAR>hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a<VAR>hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun a => ∑' (n : ι), bound n a<VAR>hF_integrable : ∀ (n : ι), Integrable (F n) μ<GOAL>∀ᶠ (n : Finset ι) in atTop, ∀ᵐ (a : α) ∂μ, ‖∑ i ∈ n, F i a‖ ≤ (fun a => ∑' (n : ι), bound n a) a