ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<GOAL>ker (lTensor.inverse Q hfg hg ∘ₗ lTensor Q g) = ker (lTensor Q g)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<GOAL>ker (lTensor.inverse Q hfg hg) = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<GOAL>Injective ⇑(lTensor.inverse Q hfg hg)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>k : ℕ<GOAL>↑k ≤ multiplicity a b → a ^ k ∣ b
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N : Type u_5<VAR>P : Type u_6<VAR>inst✝¹ : Group N<VAR>inst✝ : Group P<VAR>K : Subgroup G<VAR>f : G →* N<GOAL>(f.restrict K).range = map f K
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U : X.Opens<GOAL>𝟙 X ∣_ U = 𝟙 ↑(𝟙 X ⁻¹ᵁ U)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U : X.Opens<GOAL>(𝟙 X ⁻¹ᵁ U).ι = U.ι
<VAR>x y : ℝ<VAR>hx : x < -1<GOAL>0 < log x
<VAR>x y : ℝ<VAR>hx : x < -1<GOAL>0 < log (-x)
<VAR>x y : ℝ<VAR>hx : x < -1<VAR>this : 1 < -x<GOAL>0 < log (-x)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>x : ⨂[R] (i : ι), s i<VAR>p : FreeAddMonoid (R × ((i : ι) → s i))<VAR>h : p ∈ x.lifts<VAR>a : R<GOAL>List.map (fun y => (a * y.1, y.2)) p ∈ (a • x).lifts
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>x : ⨂[R] (i : ι), s i<VAR>p : FreeAddMonoid (R × ((i : ι) → s i))<VAR>h : (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum = x<VAR>a : R<GOAL>(List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) (List.map (fun y => (a * y.1, y.2)) p)).sum = a • x
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>x : ⨂[R] (i : ι), s i<VAR>p : FreeAddMonoid (R × ((i : ι) → s i))<VAR>h : (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum = x<VAR>a : R<GOAL>(List.map ((fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) ∘ fun y => (a * y.1, y.2)) p).sum = (List.map ((fun x => a • x) ∘ fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>x : ⨂[R] (i : ι), s i<VAR>p : FreeAddMonoid (R × ((i : ι) → s i))<VAR>h : (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum = x<VAR>a : R<VAR>x✝ : R × ((i : ι) → s i)<GOAL>((fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) ∘ fun y => (a * y.1, y.2)) x✝ = ((fun x => a • x) ∘ fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) x✝
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>a : Kˣ<VAR>h : a ∈ A.principalUnitGroup<GOAL>a ∈ A.unitGroup
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝ : (i : ι) → PartialOrder (β i)<VAR>x y : (i : ι) → β i<VAR>i✝ : ι<VAR>a✝ : β i✝<VAR>a b : (i : ι) → β i<VAR>h : a ≤ b<VAR>hne : ¬toLex a = toLex b<VAR>i : ι<VAR>hi : i ∈ {i | a i ≠ b i}<VAR>hl : ∀ x ∈ {i | a i ≠ b i}, ¬x < i<VAR>j : ι<VAR>hj : (fun x x_1 => x < x_1) j i<GOAL>toLex a j = toLex b j
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝ : (i : ι) → PartialOrder (β i)<VAR>x y : (i : ι) → β i<VAR>i✝ : ι<VAR>a✝ : β i✝<VAR>a b : (i : ι) → β i<VAR>h : a ≤ b<VAR>hne : ¬toLex a = toLex b<VAR>i : ι<VAR>hi : i ∈ {i | a i ≠ b i}<VAR>j : ι<VAR>hj : (fun x x_1 => x < x_1) j i<VAR>hl : toLex a j ≠ toLex b j<GOAL>∃ x ∈ {i | a i ≠ b i}, x < i
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β✝ : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β✝<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>β : Type u_7<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hs : MeasurableSet s<GOAL>t ∈ Filter.map f (ae (μ.restrict s)) ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<GOAL>μ ≪ μ.toFinite
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<GOAL>Measure.sum (sFiniteSeq μ) ≪ μ.toFinite
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hf : AEStronglyMeasurable' m f μ<VAR>hfg : Integrable (f * g) μ<VAR>hg : Integrable g μ<GOAL>μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hf : AEStronglyMeasurable' m f μ<VAR>hfg : Integrable (f * g) μ<VAR>hg : Integrable g μ<VAR>this : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable'.mk f hf * g|m]<GOAL>μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hf : AEStronglyMeasurable' m f μ<VAR>hfg : Integrable (f * g) μ<VAR>hg : Integrable g μ<VAR>this : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable'.mk f hf * g|m]<GOAL>μ[AEStronglyMeasurable'.mk f hf * g|m] =ᶠ[ae μ] f * μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hf : AEStronglyMeasurable' m f μ<VAR>hfg : Integrable (f * g) μ<VAR>hg : Integrable g μ<VAR>this✝ : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable'.mk f hf * g|m]<VAR>this : f * μ[g|m] =ᶠ[ae μ] AEStronglyMeasurable'.mk f hf * μ[g|m]<GOAL>μ[AEStronglyMeasurable'.mk f hf * g|m] =ᶠ[ae μ] f * μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hf : AEStronglyMeasurable' m f μ<VAR>hfg : Integrable (f * g) μ<VAR>hg : Integrable g μ<VAR>this✝ : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable'.mk f hf * g|m]<VAR>this : f * μ[g|m] =ᶠ[ae μ] AEStronglyMeasurable'.mk f hf * μ[g|m]<GOAL>Integrable (AEStronglyMeasurable'.mk f hf * g) μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hf : AEStronglyMeasurable' m f μ<VAR>hfg : Integrable (f * g) μ<VAR>hg : Integrable g μ<VAR>this✝ : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable'.mk f hf * g|m]<VAR>this : f * μ[g|m] =ᶠ[ae μ] AEStronglyMeasurable'.mk f hf * μ[g|m]<GOAL>f * g =ᶠ[ae μ] AEStronglyMeasurable'.mk f hf * g
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>q n : ℕ<VAR>hqn : n ≤ q<GOAL>(Q (q + 1)).f n = (Q q).f n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : (s ∩ t).Finite<GOAL>s.encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.27982, u_1} C<VAR>inst✝ : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>P : Karoubi (HomologicalComplex C c)<VAR>i j : ι<VAR>x✝ : c.Rel i j<GOAL>P.p.f i ≫ P.p.f i ≫ P.X.d i j = P.X.d i j ≫ P.p.f j
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.27982, u_1} C<VAR>inst✝ : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>P : Karoubi (HomologicalComplex C c)<VAR>n : ι<GOAL>P.p.f n = P.p.f n ≫ P.p.f n ≫ P.p.f n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.27982, u_1} C<VAR>inst✝ : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>P Q : Karoubi (HomologicalComplex C c)<VAR>φ : P ⟶ Q<VAR>i✝ : ι<GOAL>φ.f.f i✝ ≫ Q.p.f i✝ = P.p.f i✝ ≫ φ.f.f i✝
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.27982, u_1} C<VAR>inst✝ : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>P : Karoubi (HomologicalComplex C c)<VAR>i j : ι<VAR>x✝ : c.Rel i j<GOAL>P.p.f i ≫ P.X.d i j = (P.p.f i ≫ P.X.d i j) ≫ P.p.f j
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.27982, u_1} C<VAR>inst✝ : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>x✝ : Karoubi (HomologicalComplex C c)<VAR>i✝ : ι<GOAL>x✝.p.f i✝ ≫ x✝.p.f i✝ = x✝.p.f i✝
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<GOAL>IsIntegralClosure ↥(adjoin ℤ {ζ}) ℤ K
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ 1} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ 1)<GOAL>IsIntegralClosure ↥(adjoin ℤ {ζ}) ℤ K
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<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✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>n : ℕ<VAR>a : Composition n<VAR>b : Composition a.length<GOAL>(List.map sum (a.blocks.splitWrtComposition b)).length = b.blocks.length
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>M₁₁ : Matrix m m R<VAR>M₁₂ : Matrix m n R<VAR>M₂₁ : Matrix n m R<VAR>M₂₂ M : Matrix n n R<VAR>i j : n<GOAL>(fromBlocks M₁₁ M₁₂ 0 M₂₂).charpoly = M₁₁.charpoly * M₂₂.charpoly
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>β : Type u_7<VAR>inst✝ : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>hC : 0 ≤ C<GOAL>DominatedFinMeasAdditive μ 0 C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>β : Type u_7<VAR>inst✝ : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>hC : 0 ≤ C<VAR>s : Set α<VAR>x✝¹ : MeasurableSet s<VAR>x✝ : μ s < ⊤<GOAL>‖0 s‖ ≤ C * (μ s).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>β : Type u_7<VAR>inst✝ : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>hC : 0 ≤ C<VAR>s : Set α<VAR>x✝¹ : MeasurableSet s<VAR>x✝ : μ s < ⊤<GOAL>0 ≤ C * (μ s).toReal
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : DivisionRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module Rᵐᵒᵖ M<VAR>inst✝¹ : Module R M<VAR>inst✝ : SMulCommClass R Rᵐᵒᵖ M<VAR>x : tsze R M<GOAL>(-x)⁻¹ = -x⁻¹
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>ha : AffineIndependent k p<GOAL>AffineIndependent k fun x => ↑x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>f : ↑(Set.range p) → ι := fun x => Exists.choose ⋯<GOAL>AffineIndependent k fun x => ↑x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>f : ↑(Set.range p) → ι := fun x => Exists.choose ⋯<VAR>hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x<GOAL>AffineIndependent k fun x => ↑x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>f : ↑(Set.range p) → ι := fun x => Exists.choose ⋯<VAR>hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x<VAR>fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := ⋯ }<GOAL>AffineIndependent k fun x => ↑x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>f : ↑(Set.range p) → ι := fun x => Exists.choose ⋯<VAR>hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x<VAR>fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := ⋯ }<VAR>x✝ : ↑(Set.range p)<GOAL>Subtype.val = p ∘ ⇑fe
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>W : Set γ<VAR>f : α × β → γ<GOAL>s ×ˢ t ⊆ f ⁻¹' W ↔ ∀ (a : α) (b : β), a ∈ s → b ∈ t → f (a, b) ∈ W
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>a : Stream' M<VAR>S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}<GOAL>∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>a : Stream' M<VAR>S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}<VAR>h : ∃ m ∈ S, m * m = m<GOAL>∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>a : Stream' M<VAR>S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}<GOAL>∀ (r : Ultrafilter M), Continuous fun x => x * r
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>a : Stream' M<VAR>S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}<GOAL>S.Nonempty
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>a : Stream' M<VAR>S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}<GOAL>IsCompact S
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>a : Stream' M<VAR>S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}<GOAL>∀ x ∈ S, ∀ y ∈ S, x * y ∈ S
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E✝ B I✝ X R J I E : Set α<GOAL>(uniqueBaseOn I E)✶ = uniqueBaseOn (E \ I) E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E✝ B I✝ X R J I E : Set α<GOAL>(uniqueBaseOn (I ∩ E) E)✶ = uniqueBaseOn (E \ I) E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E✝ B✝ I✝ X R J I E B : Set α<VAR>hB : B ⊆ E<GOAL>(uniqueBaseOn (I ∩ E) E)✶.Base B ↔ (uniqueBaseOn (E \ I) E).Base B
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E✝ B✝ I✝ X R J I E B : Set α<VAR>hB : B ⊆ E<GOAL>E \ B = I ∩ E ↔ B = E \ I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>l l' la : Filter α<VAR>lb : Filter β<VAR>f : Filter α<GOAL>f.smallSets = generate (powerset '' f.sets)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι✝ : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ q : Seminorm 𝕜 E<VAR>x✝ : E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<VAR>hp : BddAbove (range p)<VAR>x : E<GOAL>(⨆ i, p i) x = ⨆ i, (p i) x
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>s : Set α<VAR>hs : span s = ⊤<VAR>n : ℕ<GOAL>span ((fun x => x ^ n) '' s) = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>s : Set α<VAR>hs : span s = ⊤<VAR>n : ℕ<GOAL>1 ∈ span ((fun x => x ^ n) '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>s : Set α<VAR>hs : span s = ⊤<VAR>n : ℕ<GOAL>1 ∈ span ((fun x => x ^ (n + 1)) '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>s : Set α<VAR>hs : ∃ l, (Finsupp.total (↑s) α α Subtype.val) l = 1<VAR>n : ℕ<GOAL>1 ∈ span ((fun x => x ^ (n + 1)) '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>s : Set α<VAR>n : ℕ<VAR>f : ↑s →₀ α<VAR>hf✝ : (Finsupp.total (↑s) α α Subtype.val) f = 1<VAR>hf : ∑ a ∈ f.support, f a * ↑a = 1<GOAL>1 ∈ span ((fun x => x ^ (n + 1)) '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>s : Set α<VAR>n : ℕ<VAR>f : ↑s →₀ α<VAR>hf✝ : (Finsupp.total (↑s) α α Subtype.val) f = 1<VAR>hf : ∑ a ∈ f.support, f a * ↑a = 1<VAR>this : (∑ i ∈ f.support, f i * ↑i) ^ (f.support.card * n + 1) ∈ span ((fun i => (f i * ↑i) ^ (n + 1)) '' ↑f.support)<GOAL>1 ∈ span ((fun x => x ^ (n + 1)) '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>s : Set α<VAR>n : ℕ<VAR>f : ↑s →₀ α<VAR>hf✝ : (Finsupp.total (↑s) α α Subtype.val) f = 1<VAR>hf : ∑ a ∈ f.support, f a * ↑a = 1<VAR>this : 1 ∈ span ((fun i => (f i * ↑i) ^ (n + 1)) '' ↑f.support)<GOAL>1 ∈ span ((fun x => x ^ (n + 1)) '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>s : Set α<VAR>n : ℕ<VAR>f : ↑s →₀ α<VAR>hf✝ : (Finsupp.total (↑s) α α Subtype.val) f = 1<VAR>hf : ∑ a ∈ f.support, f a * ↑a = 1<VAR>this : 1 ∈ span ((fun i => (f i * ↑i) ^ (n + 1)) '' ↑f.support)<GOAL>(fun i => (f i * ↑i) ^ (n + 1)) '' ↑f.support ⊆ ↑(span ((fun x => x ^ (n + 1)) '' s))
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>s : Set α<VAR>n : ℕ<VAR>f : ↑s →₀ α<VAR>hf✝ : (Finsupp.total (↑s) α α Subtype.val) f = 1<VAR>hf : ∑ a ∈ f.support, f a * ↑a = 1<VAR>this : 1 ∈ span ((fun i => (f i * ↑i) ^ (n + 1)) '' ↑f.support)<VAR>a✝ : α<VAR>hx : a✝ ∈ (fun i => (f i * ↑i) ^ (n + 1)) '' ↑f.support<GOAL>a✝ ∈ ↑(span ((fun x => x ^ (n + 1)) '' s))
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>s : Set α<VAR>n : ℕ<VAR>f : ↑s →₀ α<VAR>hf✝ : (Finsupp.total (↑s) α α Subtype.val) f = 1<VAR>hf : ∑ a ∈ f.support, f a * ↑a = 1<VAR>this : 1 ∈ span ((fun i => (f i * ↑i) ^ (n + 1)) '' ↑f.support)<VAR>a✝ : α<VAR>hx : ∃ x ∈ ↑f.support, (f x * ↑x) ^ (n + 1) = a✝<GOAL>a✝ ∈ ↑(span ((fun x => x ^ (n + 1)) '' s))
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>s : Set α<VAR>n : ℕ<VAR>f : ↑s →₀ α<VAR>hf✝ : (Finsupp.total (↑s) α α Subtype.val) f = 1<VAR>hf : ∑ a ∈ f.support, f a * ↑a = 1<VAR>this : 1 ∈ span ((fun i => (f i * ↑i) ^ (n + 1)) '' ↑f.support)<VAR>x : ↑s<VAR>left✝ : x ∈ ↑f.support<GOAL>(f x * ↑x) ^ (n + 1) ∈ ↑(span ((fun x => x ^ (n + 1)) '' s))
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>s : Set α<VAR>n : ℕ<VAR>f : ↑s →₀ α<VAR>hf✝ : (Finsupp.total (↑s) α α Subtype.val) f = 1<VAR>hf : ∑ a ∈ f.support, f a * ↑a = 1<VAR>this✝ : 1 ∈ span ((fun i => (f i * ↑i) ^ (n + 1)) '' ↑f.support)<VAR>x : ↑s<VAR>left✝ : x ∈ ↑f.support<VAR>this : span {↑x ^ (n + 1)} ≤ span ((fun x => x ^ (n + 1)) '' s)<GOAL>(f x * ↑x) ^ (n + 1) ∈ ↑(span ((fun x => x ^ (n + 1)) '' s))
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>s : Set α<VAR>n : ℕ<VAR>f : ↑s →₀ α<VAR>hf✝ : (Finsupp.total (↑s) α α Subtype.val) f = 1<VAR>hf : ∑ a ∈ f.support, f a * ↑a = 1<VAR>this✝ : 1 ∈ span ((fun i => (f i * ↑i) ^ (n + 1)) '' ↑f.support)<VAR>x : ↑s<VAR>left✝ : x ∈ ↑f.support<VAR>this : span {↑x ^ (n + 1)} ≤ span ((fun x => x ^ (n + 1)) '' s)<GOAL>(f x * ↑x) ^ (n + 1) ∈ span {↑x ^ (n + 1)}
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>s : Set α<VAR>n : ℕ<VAR>f : ↑s →₀ α<VAR>hf✝ : (Finsupp.total (↑s) α α Subtype.val) f = 1<VAR>hf : ∑ a ∈ f.support, f a * ↑a = 1<VAR>this✝ : 1 ∈ span ((fun i => (f i * ↑i) ^ (n + 1)) '' ↑f.support)<VAR>x : ↑s<VAR>left✝ : x ∈ ↑f.support<VAR>this : span {↑x ^ (n + 1)} ≤ span ((fun x => x ^ (n + 1)) '' s)<GOAL>↑x ^ (n + 1) ∣ f x ^ (n + 1) * ↑x ^ (n + 1)
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s : Set α<GOAL>(inducedOuterMeasure m P0 m0) s = ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s : Set α<GOAL>(inducedOuterMeasure m P0 m0) s ≤ ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s : Set α<GOAL>⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ (inducedOuterMeasure m P0 m0) s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f g : ι → Set X<VAR>hf : LocallyFinite f<VAR>hc : ∀ (i : ι), IsClosed (f i)<GOAL>IsClosed (⋃ i, f i)