ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f : γ → α<VAR>g✝ : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T2Space γ<VAR>b : β<VAR>g : β → γ<VAR>di : DenseInducing i<VAR>hg : ContinuousAt g b<VAR>s : Set γ<VAR>hs : s ∈ 𝓝 (g b)<GOAL>∀ᶠ (x : α) in comap i (𝓝 b), g (i x) ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f : γ → α<VAR>g✝ : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T2Space γ<VAR>b : β<VAR>g : β → γ<VAR>di : DenseInducing i<VAR>hg : ContinuousAt g b<VAR>s : Set γ<VAR>hs : s ∈ 𝓝 (g b)<GOAL>∀ (x : β), s (g x) → ∀ (a : α), i a = x → g (i a) ∈ s
<GOAL>StrictConcaveOn ℝ (Icc (-(π / 2)) (π / 2)) cos
<VAR>x : ℝ<VAR>hx : x ∈ interior (Icc (-(π / 2)) (π / 2))<GOAL>deriv^[2] cos x < 0
<VAR>x : ℝ<VAR>hx : x ∈ Ioo (-(π / 2)) (π / 2)<GOAL>deriv^[2] cos x < 0
<VAR>u v m n : ℤ<GOAL>Even (m * n) ↔ Even m ∨ Even n
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 3)<VAR>H : i.castSucc < j<VAR>hj : j = 0<GOAL>False
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 3)<VAR>H : i.castSucc < j<GOAL>X.map (SimplexCategory.δ j).op ≫ X.map (SimplexCategory.δ i).op = X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ (j.pred ⋯)).op
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>R : ℝ<VAR>f : X → ℝ<VAR>hR : 0 ≤ R<VAR>hfint : IntegrableOn f {x | R < f x} μ<VAR>hμ : μ {x | R < f x} ≠ 0<GOAL>(μ {x | R < f x}).toReal * R < ∫ (x : X) in {x | R < f x}, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>R : ℝ<VAR>f : X → ℝ<VAR>hR : 0 ≤ R<VAR>hfint : IntegrableOn f {x | R < f x} μ<VAR>hμ : μ {x | R < f x} ≠ 0<VAR>this : IntegrableOn (fun x => R) {x | R < f x} μ<GOAL>(μ {x | R < f x}).toReal * R < ∫ (x : X) in {x | R < f x}, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>R : ℝ<VAR>f : X → ℝ<VAR>hR : 0 ≤ R<VAR>hfint : IntegrableOn f {x | R < f x} μ<VAR>hμ : μ {x | R < f x} ≠ 0<VAR>this : IntegrableOn (fun x => R) {x | R < f x} μ<GOAL>0 < μ ((support fun a => f a - R) ∩ {x | R < f x})
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>R : ℝ<VAR>f : X → ℝ<VAR>hR : 0 ≤ R<VAR>hfint : IntegrableOn f {x | R < f x} μ<VAR>hμ : μ {x | R < f x} ≠ 0<VAR>this : IntegrableOn (fun x => R) {x | R < f x} μ<GOAL>0 ≤ᶠ[ae (μ.restrict {x | R < f x})] fun a => f a - R
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>R : ℝ<VAR>f : X → ℝ<VAR>hR : 0 ≤ R<VAR>hfint : IntegrableOn f {x | R < f x} μ<VAR>hμ : μ {x | R < f x} ≠ 0<VAR>this : IntegrableOn (fun x => R) {x | R < f x} μ<GOAL>IntegrableOn (fun a => f a - R) {x | R < f x} μ
<VAR>n : ℕ<VAR>c : Composition n<VAR>n₁ : ℕ<VAR>c₁ : Composition n₁<VAR>i₁ i₂ : Fin c₁.length<VAR>hi : ↑i₁ = ↑i₂<GOAL>i₁ = i₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>I : HomogeneousIdeal 𝒜<VAR>t : (Set (ProjectiveSpectrum 𝒜))ᵒᵈ<GOAL>(fun I => zeroLocus 𝒜 ↑I) I ≤ t ↔ I ≤ (fun t => vanishingIdeal t) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<GOAL>{ ofColex := s } < { ofColex := {a} } ↔ ∀ b ∈ s, b < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<GOAL>(∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ s ≠ {a} ↔ ∀ b ∈ s, b < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>b✝ b : α<VAR>hb : b ∈ s<VAR>h : (∀ b_1 ∈ s, b_1 ≤ b ∧ (b ∈ s → b_1 = b)) ∧ s ≠ {b}<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>t u : Finset α<VAR>a b : α<VAR>h : ∀ b ∈ {a}, b < a<GOAL>False
<VAR>η : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ : Type u_4<VAR>l✝ : Line α✝ ι✝<VAR>i : ι✝<VAR>a x✝ : α✝<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>l : Line α ι<VAR>l' : Line α ι'<VAR>x : α<GOAL>(fun x i => ((l.prod l').idxFun i).getD x) x = Sum.elim ((fun x i => (l.idxFun i).getD x) x) ((fun x i => (l'.idxFun i).getD x) x)
<VAR>η : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ : Type u_4<VAR>l✝ : Line α✝ ι✝<VAR>i✝ : ι✝<VAR>a x✝ : α✝<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>l : Line α ι<VAR>l' : Line α ι'<VAR>x : α<VAR>i : ι ⊕ ι'<GOAL>(fun x i => ((l.prod l').idxFun i).getD x) x i = Sum.elim ((fun x i => (l.idxFun i).getD x) x) ((fun x i => (l'.idxFun i).getD x) x) i
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i✝ : ι<VAR>b : B<VAR>a : F<VAR>i : ι<GOAL>(Z.localTrivAsPartialEquiv i).source ∈ ⋃ i, ⋃ s, ⋃ (_ : IsOpen s), {(Z.localTrivAsPartialEquiv i).source ∩ ↑(Z.localTrivAsPartialEquiv i) ⁻¹' s}
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i✝ : ι<VAR>b : B<VAR>a : F<VAR>i : ι<GOAL>∃ i_1 i_2, IsOpen i_2 ∧ (Z.localTrivAsPartialEquiv i).source = (Z.localTrivAsPartialEquiv i_1).source ∩ ↑(Z.localTrivAsPartialEquiv i_1) ⁻¹' i_2
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i✝ : ι<VAR>b : B<VAR>a : F<VAR>i : ι<GOAL>(Z.localTrivAsPartialEquiv i).source = (Z.localTrivAsPartialEquiv i).source ∩ ↑(Z.localTrivAsPartialEquiv i) ⁻¹' Z.baseSet i ×ˢ univ
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i✝ : ι<VAR>b : B<VAR>a : F<VAR>i : ι<VAR>p : Z.TotalSpace<GOAL>p ∈ (Z.localTrivAsPartialEquiv i).source ↔ p ∈ (Z.localTrivAsPartialEquiv i).source ∩ ↑(Z.localTrivAsPartialEquiv i) ⁻¹' Z.baseSet i ×ˢ univ
<VAR>K : Type u_1<VAR>inst✝¹ : DivisionRing K<VAR>inst✝ : CharZero K<VAR>a : ℕ<GOAL>↑(a.choose 2) = ↑a * (↑a - 1) / 2
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>n : ℕ<VAR>a : R<GOAL>Multiset.card (nthRoots n a) ≤ n
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : Field k<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : AddTorsor E PE<VAR>f : k → E<VAR>a b : k<VAR>h : a ≠ b<GOAL>slope (fun x => (x - a) • f x) a b = f b
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S : Cᵒᵖ ⥤ CommRingCat<VAR>F : C ⥤ D<VAR>S' R : Dᵒᵖ ⥤ CommRingCat<VAR>M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)<VAR>φ : S ⟶ F.op ⋙ R<VAR>φ' : S' ⟶ R<VAR>d : M.Derivation φ<VAR>X : Dᵒᵖ<GOAL>d.d 1 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : autoParam s.Finite _auto✝<GOAL>2 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n t : ℕ<VAR>h : yn a1 n * yn a1 n ∣ yn a1 t<VAR>nt : n ∣ t<VAR>n0l : 0 < n<VAR>k : ℕ<VAR>ke : t = n * k<GOAL>yn a1 n ∣ t
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n t : ℕ<VAR>h : yn a1 n * yn a1 n ∣ yn a1 t<VAR>nt : n ∣ t<VAR>n0l : 0 < n<VAR>k : ℕ<VAR>ke : t = n * k<VAR>this : yn a1 n ∣ k * xn a1 n ^ (k - 1)<GOAL>yn a1 n ∣ t
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n t : ℕ<VAR>h : yn a1 n * yn a1 n ∣ yn a1 t<VAR>nt : n ∣ t<VAR>n0l : 0 < n<VAR>k : ℕ<VAR>ke : t = n * k<VAR>this : yn a1 n ∣ k * xn a1 n ^ (k - 1)<GOAL>yn a1 n ∣ n * k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → δ<VAR>g : δ → β<VAR>hg : AEStronglyMeasurable g (Measure.map f μ)<VAR>hf : AEMeasurable f μ<GOAL>Integrable g (Measure.map f μ) ↔ Integrable (g ∘ f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → δ<VAR>g : δ → β<VAR>hg : AEStronglyMeasurable g (Measure.map f μ)<VAR>hf : AEMeasurable f μ<GOAL>Memℒp g 1 (Measure.map f μ) ↔ Memℒp (g ∘ f) 1 μ
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>g g' : G<VAR>inst✝² : UniformSpace G<VAR>inst✝¹ : UniformGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : ℤ → G<GOAL>Multipliable f ↔ (Multipliable fun n => f ↑n) ∧ Multipliable fun n => f (-↑n)
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>g g' : G<VAR>inst✝² : UniformSpace G<VAR>inst✝¹ : UniformGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : ℤ → G<VAR>p : Multipliable f<GOAL>Injective fun n => -↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a : α<VAR>ha : ¬IsUnit a<VAR>ha0 : a ≠ 0<GOAL>multiplicity a a = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a : α<VAR>ha : ¬IsUnit a<VAR>ha0 : a ≠ 0<GOAL>multiplicity a a = ↑1
<VAR>n m l : ℕ<VAR>hln : l ≤ n<VAR>k : ℕ<VAR>hk : k ∈ Ico n m<GOAL>¬decide (k < l) = true
<VAR>n m l : ℕ<VAR>hln : l ≤ n<VAR>k : ℕ<VAR>hk : k ∈ Ico n m<GOAL>n ≤ k
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Bool<VAR>xs : List α<GOAL>findIdx p xs < xs.length ↔ ∃ x ∈ xs, p x = true
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Bool<VAR>xs : List α<GOAL>xs.length ≤ findIdx p xs ↔ ¬∃ x ∈ xs, p x = true
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Bool<VAR>xs : List α<VAR>this : findIdx p xs = xs.length ↔ findIdx p xs ≤ xs.length ∧ xs.length ≤ findIdx p xs<GOAL>xs.length ≤ findIdx p xs ↔ ¬∃ x ∈ xs, p x = true
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Bool<VAR>xs : List α<VAR>this : findIdx p xs = xs.length ↔ xs.length ≤ findIdx p xs<GOAL>xs.length ≤ findIdx p xs ↔ ¬∃ x ∈ xs, p x = true
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Bool<VAR>xs : List α<VAR>this : findIdx p xs = xs.length ↔ xs.length ≤ findIdx p xs<GOAL>(∀ x ∈ xs, ¬p x = true) ↔ ∀ (x : α), ¬(x ∈ xs ∧ p x = true)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring 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>a b : R<VAR>x y : M<VAR>s : Set M<VAR>f : M →ₗ[R] M'<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<VAR>hf_inj : Disjoint (span R s) (ker f)<GOAL>LinearIndependent R fun (x : ↑(⇑f '' s)) => ↑x
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring 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>a b : R<VAR>x y : M<VAR>s : Set M<VAR>f : M →ₗ[R] M'<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<VAR>hf_inj : Disjoint (span R (Set.range Subtype.val)) (ker f)<GOAL>LinearIndependent R fun (x : ↑(⇑f '' s)) => ↑x
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring 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>a b : R<VAR>x y : M<VAR>s : Set M<VAR>f : M →ₗ[R] M'<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<VAR>hf_inj : Disjoint (span R (Set.range Subtype.val)) (ker f)<GOAL>Set.range (⇑f ∘ fun x => ↑x) = ⇑f '' s
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n✝ : A<VAR>n : ℕ<GOAL>M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<GOAL>M.toAddSubmonoid ^ 0 ≤ (M ^ 0).toAddSubmonoid
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n✝ : A<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid
<VAR>R S : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module S M<VAR>inst✝³ : IsScalarTower R S M<VAR>inst✝² : FormallyUnramified R S<VAR>inst✝¹ : EssFiniteType R S<VAR>I : Type u_2<VAR>inst✝ : DecidableEq I<VAR>b : Basis I R S<VAR>f : I →₀ S<VAR>x : S<VAR>a : I → I →₀ R<VAR>ha : a = fun i => b.repr (b i * x)<GOAL>(1 ⊗ₜ[R] x * f.sum fun i y => y ⊗ₜ[R] b i) = ∑ k ∈ f.support.biUnion fun i => (a i).support, (b.repr (f.sum fun i y => (a i) k • y)).sum fun j c => c • b j ⊗ₜ[R] b k
<VAR>R S : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module S M<VAR>inst✝³ : IsScalarTower R S M<VAR>inst✝² : FormallyUnramified R S<VAR>inst✝¹ : EssFiniteType R S<VAR>I : Type u_2<VAR>inst✝ : DecidableEq I<VAR>b : Basis I R S<VAR>f : I →₀ S<VAR>x : S<VAR>a : I → I →₀ R<VAR>ha : a = fun i => b.repr (b i * x)<GOAL>∑ i ∈ f.support, 1 ⊗ₜ[R] x * f i ⊗ₜ[R] b i = ∑ k ∈ f.support.biUnion fun i => (a i).support, (b.repr (f.sum fun i y => (a i) k • y)).sum fun j c => c • b j ⊗ₜ[R] b k
<VAR>R S : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module S M<VAR>inst✝³ : IsScalarTower R S M<VAR>inst✝² : FormallyUnramified R S<VAR>inst✝¹ : EssFiniteType R S<VAR>I : Type u_2<VAR>inst✝ : DecidableEq I<VAR>b : Basis I R S<VAR>f : I →₀ S<VAR>x : S<VAR>a : I → I →₀ R := fun i => b.repr (b i * x)<GOAL>∑ i ∈ f.support, 1 ⊗ₜ[R] x * f i ⊗ₜ[R] b i = ∑ k ∈ f.support.biUnion fun i => ((fun i => b.repr (b i * x)) i).support, (b.repr (f.sum fun i y => ((fun i => b.repr (b i * x)) i) k • y)).sum fun j c => c • b j ⊗ₜ[R] b k
<VAR>R S : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module S M<VAR>inst✝³ : IsScalarTower R S M<VAR>inst✝² : FormallyUnramified R S<VAR>inst✝¹ : EssFiniteType R S<VAR>I : Type u_2<VAR>inst✝ : DecidableEq I<VAR>b : Basis I R S<VAR>f : I →₀ S<VAR>x : S<VAR>a : I → I →₀ R := fun i => b.repr (b i * x)<GOAL>∑ i ∈ f.support, f i ⊗ₜ[R] (Finsupp.total I S R ⇑b) (a i) = ∑ k ∈ f.support.biUnion fun i => ((fun i => b.repr (b i * x)) i).support, (b.repr (f.sum fun i y => ((fun i => b.repr (b i * x)) i) k • y)).sum fun j c => c • b j ⊗ₜ[R] b k
<VAR>R S : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module S M<VAR>inst✝³ : IsScalarTower R S M<VAR>inst✝² : FormallyUnramified R S<VAR>inst✝¹ : EssFiniteType R S<VAR>I : Type u_2<VAR>inst✝ : DecidableEq I<VAR>b : Basis I R S<VAR>f : I →₀ S<VAR>x : S<VAR>a : I → I →₀ R := fun i => b.repr (b i * x)<GOAL>∑ x ∈ f.support, ∑ x_1 ∈ (a x).support, ((a x) x_1 • f x) ⊗ₜ[R] b x_1 = ∑ k ∈ f.support.biUnion fun i => ((fun i => b.repr (b i * x)) i).support, (b.repr (f.sum fun i y => ((fun i => b.repr (b i * x)) i) k • y)).sum fun j c => c • b j ⊗ₜ[R] b k
<VAR>R S : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module S M<VAR>inst✝³ : IsScalarTower R S M<VAR>inst✝² : FormallyUnramified R S<VAR>inst✝¹ : EssFiniteType R S<VAR>I : Type u_2<VAR>inst✝ : DecidableEq I<VAR>b : Basis I R S<VAR>f : I →₀ S<VAR>x : S<VAR>a : I → I →₀ R := fun i => b.repr (b i * x)<VAR>h₁ : ∀ (k : I), ((f.sum fun i y => (a i) k • b.repr y).sum fun j z => z • b j ⊗ₜ[R] b k) = f.sum fun i y => (b.repr y).sum fun j z => (a i) k • z • b j ⊗ₜ[R] b k<GOAL>∑ x ∈ f.support, ∑ x_1 ∈ (a x).support, ((a x) x_1 • f x) ⊗ₜ[R] b x_1 = ∑ k ∈ f.support.biUnion fun i => ((fun i => b.repr (b i * x)) i).support, (b.repr (f.sum fun i y => ((fun i => b.repr (b i * x)) i) k • y)).sum fun j c => c • b j ⊗ₜ[R] b k
<VAR>R S : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module S M<VAR>inst✝³ : IsScalarTower R S M<VAR>inst✝² : FormallyUnramified R S<VAR>inst✝¹ : EssFiniteType R S<VAR>I : Type u_2<VAR>inst✝ : DecidableEq I<VAR>b : Basis I R S<VAR>f : I →₀ S<VAR>x : S<VAR>a : I → I →₀ R := fun i => b.repr (b i * x)<VAR>h₁ : ∀ (k : I), ((f.sum fun i y => (a i) k • b.repr y).sum fun j z => z • b j ⊗ₜ[R] b k) = f.sum fun i y => (b.repr y).sum fun j z => (a i) k • z • b j ⊗ₜ[R] b k<VAR>h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x<GOAL>∑ x ∈ f.support, ∑ x_1 ∈ (a x).support, ((a x) x_1 • f x) ⊗ₜ[R] b x_1 = ∑ k ∈ f.support.biUnion fun i => ((fun i => b.repr (b i * x)) i).support, (b.repr (f.sum fun i y => ((fun i => b.repr (b i * x)) i) k • y)).sum fun j c => c • b j ⊗ₜ[R] b k
<VAR>R S : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module S M<VAR>inst✝³ : IsScalarTower R S M<VAR>inst✝² : FormallyUnramified R S<VAR>inst✝¹ : EssFiniteType R S<VAR>I : Type u_2<VAR>inst✝ : DecidableEq I<VAR>b : Basis I R S<VAR>f : I →₀ S<VAR>x : S<VAR>a : I → I →₀ R := fun i => b.repr (b i * x)<VAR>h₁ : ∀ (k : I), ((f.sum fun i y => (a i) k • b.repr y).sum fun j z => z • b j ⊗ₜ[R] b k) = f.sum fun i y => (b.repr y).sum fun j z => (a i) k • z • b j ⊗ₜ[R] b k<VAR>h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x<GOAL>∑ x ∈ f.support, ∑ x_1 ∈ (a x).support, ((a x) x_1 • f x) ⊗ₜ[R] b x_1 = ∑ x_1 ∈ f.support, ∑ x ∈ f.support.biUnion fun i => (b.repr (b i * x)).support, ((a x_1) x • f x_1) ⊗ₜ[R] b x
<VAR>R S : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module S M<VAR>inst✝³ : IsScalarTower R S M<VAR>inst✝² : FormallyUnramified R S<VAR>inst✝¹ : EssFiniteType R S<VAR>I : Type u_2<VAR>inst✝ : DecidableEq I<VAR>b : Basis I R S<VAR>f : I →₀ S<VAR>x : S<VAR>a : I → I →₀ R := fun i => b.repr (b i * x)<VAR>h₁ : ∀ (k : I), ((f.sum fun i y => (a i) k • b.repr y).sum fun j z => z • b j ⊗ₜ[R] b k) = f.sum fun i y => (b.repr y).sum fun j z => (a i) k • z • b j ⊗ₜ[R] b k<VAR>h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x<GOAL>∀ x_1 ∈ f.support, ∑ x ∈ (a x_1).support, ((a x_1) x • f x_1) ⊗ₜ[R] b x = ∑ x ∈ f.support.biUnion fun i => (b.repr (b i * x)).support, ((a x_1) x • f x_1) ⊗ₜ[R] b x
<VAR>R S : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module S M<VAR>inst✝³ : IsScalarTower R S M<VAR>inst✝² : FormallyUnramified R S<VAR>inst✝¹ : EssFiniteType R S<VAR>I : Type u_2<VAR>inst✝ : DecidableEq I<VAR>b : Basis I R S<VAR>f : I →₀ S<VAR>x : S<VAR>a : I → I →₀ R := fun i => b.repr (b i * x)<VAR>h₁ : ∀ (k : I), ((f.sum fun i y => (a i) k • b.repr y).sum fun j z => z • b j ⊗ₜ[R] b k) = f.sum fun i y => (b.repr y).sum fun j z => (a i) k • z • b j ⊗ₜ[R] b k<VAR>h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x<VAR>i : I<VAR>hi : i ∈ f.support<GOAL>∑ x ∈ (a i).support, ((a i) x • f i) ⊗ₜ[R] b x = ∑ x ∈ f.support.biUnion fun i => (b.repr (b i * x)).support, ((a i) x • f i) ⊗ₜ[R] b x
<VAR>R S : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module S M<VAR>inst✝³ : IsScalarTower R S M<VAR>inst✝² : FormallyUnramified R S<VAR>inst✝¹ : EssFiniteType R S<VAR>I : Type u_2<VAR>inst✝ : DecidableEq I<VAR>b : Basis I R S<VAR>f : I →₀ S<VAR>x : S<VAR>a : I → I →₀ R := fun i => b.repr (b i * x)<VAR>h₁ : ∀ (k : I), ((f.sum fun i y => (a i) k • b.repr y).sum fun j z => z • b j ⊗ₜ[R] b k) = f.sum fun i y => (b.repr y).sum fun j z => (a i) k • z • b j ⊗ₜ[R] b k<VAR>h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x<VAR>i : I<VAR>hi : i ∈ f.support<GOAL>(a i).support ⊆ f.support.biUnion fun i => (b.repr (b i * x)).support
<VAR>R S : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module S M<VAR>inst✝³ : IsScalarTower R S M<VAR>inst✝² : FormallyUnramified R S<VAR>inst✝¹ : EssFiniteType R S<VAR>I : Type u_2<VAR>inst✝ : DecidableEq I<VAR>b : Basis I R S<VAR>f : I →₀ S<VAR>x : S<VAR>a : I → I →₀ R := fun i => b.repr (b i * x)<VAR>h₁ : ∀ (k : I), ((f.sum fun i y => (a i) k • b.repr y).sum fun j z => z • b j ⊗ₜ[R] b k) = f.sum fun i y => (b.repr y).sum fun j z => (a i) k • z • b j ⊗ₜ[R] b k<VAR>h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x<VAR>i : I<VAR>hi : i ∈ f.support<GOAL>∀ x_1 ∈ (f.support.biUnion fun i => (b.repr (b i * x)).support) \ (a i).support, ((a i) x_1 • f i) ⊗ₜ[R] b x_1 = 0
<VAR>R S : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module S M<VAR>inst✝³ : IsScalarTower R S M<VAR>inst✝² : FormallyUnramified R S<VAR>inst✝¹ : EssFiniteType R S<VAR>I : Type u_2<VAR>inst✝ : DecidableEq I<VAR>b : Basis I R S<VAR>f : I →₀ S<VAR>x : S<VAR>a : I → I →₀ R := fun i => b.repr (b i * x)<VAR>h₁ : ∀ (k : I), ((f.sum fun i y => (a i) k • b.repr y).sum fun j z => z • b j ⊗ₜ[R] b k) = f.sum fun i y => (b.repr y).sum fun j z => (a i) k • z • b j ⊗ₜ[R] b k<VAR>h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x<VAR>i : I<VAR>hi : i ∈ f.support<GOAL>∀ x ∈ (a i).support, ((a i) x • f i) ⊗ₜ[R] b x = ((a i) x • f i) ⊗ₜ[R] b x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>K : Type u_5<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<GOAL>∑' (n : ℕ), ↑(↑(eapproxDiff f n) a) = f a
<VAR>ds₁ ds₂ ds₃ is : List ℕ<VAR>h : Forall₂ (fun x x_1 => x < x_1) is (ds₁ ++ ds₂ ++ ds₃)<GOAL>↑(assocRight ⟨is, h⟩).drop.take = ↑(take ⟨is, h⟩).drop