ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝¹ : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))<VAR>E : A<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J.sieves X<VAR>x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows<VAR>hx : x.Compatible<VAR>T : J.Cover X := ⟨S, hS⟩<VAR>hh : IsLimit (T.multifork P)<VAR>K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun I => x I.f ⋯) ⋯<GOAL>(fun t => x.IsAmalgamation t) (hh.lift K) ∧ ∀ (y : (P ⋙ coyoneda.obj (op E)).obj (op X)), (fun t => x.IsAmalgamation t) y → y = hh.lift K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<GOAL>s ∪ t =ᶠ[ae μ] s ↔ t ≤ᶠ[ae μ] s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<GOAL>s ∪ t =ᶠ[ae μ] s ↔ μ (t \ s) = 0
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>h : t.Nonempty<GOAL>image2 (fun x x_1 => x) s t = s
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>f : α → β → γ<VAR>l₁ : List α<VAR>l₂ : List β<VAR>i : ℕ<GOAL>(zipWith f l₁ l₂).get? i = (Option.map f (l₁.get? i)).bind fun g => Option.map g (l₂.get? i)
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>x y : ↑↑𝒰.gluedCover.glued.toPresheafedSpace<VAR>h : 𝒰.fromGlued.val.base x = 𝒰.fromGlued.val.base y<GOAL>x = y
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>y : ↑↑𝒰.gluedCover.glued.toPresheafedSpace<VAR>i : 𝒰.gluedCover.J<VAR>x : ↑↑(𝒰.gluedCover.U i).toPresheafedSpace<VAR>h : 𝒰.fromGlued.val.base ((𝒰.gluedCover.ι i).val.base x) = 𝒰.fromGlued.val.base y<GOAL>(𝒰.gluedCover.ι i).val.base x = y
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>i : 𝒰.gluedCover.J<VAR>x : ↑↑(𝒰.gluedCover.U i).toPresheafedSpace<VAR>j : 𝒰.gluedCover.J<VAR>y : ↑↑(𝒰.gluedCover.U j).toPresheafedSpace<VAR>h : 𝒰.fromGlued.val.base ((𝒰.gluedCover.ι i).val.base x) = 𝒰.fromGlued.val.base ((𝒰.gluedCover.ι j).val.base y)<GOAL>(𝒰.gluedCover.ι i).val.base x = (𝒰.gluedCover.ι j).val.base y
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>i : 𝒰.gluedCover.J<VAR>x : ↑↑(𝒰.gluedCover.U i).toPresheafedSpace<VAR>j : 𝒰.gluedCover.J<VAR>y : ↑↑(𝒰.gluedCover.U j).toPresheafedSpace<VAR>h : ((𝒰.gluedCover.ι i).val.base ≫ 𝒰.fromGlued.val.base) x = ((𝒰.gluedCover.ι j).val.base ≫ 𝒰.fromGlued.val.base) y<GOAL>(𝒰.gluedCover.ι i).val.base x = (𝒰.gluedCover.ι j).val.base y
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>i : 𝒰.gluedCover.J<VAR>x : ↑↑(𝒰.gluedCover.U i).toPresheafedSpace<VAR>j : 𝒰.gluedCover.J<VAR>y : ↑↑(𝒰.gluedCover.U j).toPresheafedSpace<VAR>h : (𝒰.gluedCover.ι i ≫ 𝒰.fromGlued).val.base x = (𝒰.gluedCover.ι j ≫ 𝒰.fromGlued).val.base y<GOAL>(𝒰.gluedCover.ι i).val.base x = (𝒰.gluedCover.ι j).val.base y
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>i : 𝒰.gluedCover.J<VAR>x : ↑↑(𝒰.gluedCover.U i).toPresheafedSpace<VAR>j : 𝒰.gluedCover.J<VAR>y : ↑↑(𝒰.gluedCover.U j).toPresheafedSpace<VAR>h : (𝒰.map i).val.base x = (𝒰.map j).val.base y<GOAL>(𝒰.gluedCover.ι i).val.base x = (𝒰.gluedCover.ι j).val.base y
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>i : 𝒰.gluedCover.J<VAR>x : ↑↑(𝒰.gluedCover.U i).toPresheafedSpace<VAR>j : 𝒰.gluedCover.J<VAR>y : ↑↑(𝒰.gluedCover.U j).toPresheafedSpace<VAR>h : (𝒰.map i).val.base x = (𝒰.map j).val.base y<VAR>e : (TopCat.pullbackCone (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).pt ≅ (PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.map i) (𝒰.map j))) (forgetToTop.map (pullback.snd (𝒰.map i) (𝒰.map j))) ⋯).pt := (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).conePointUniqueUpToIso (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.map i) (𝒰.map j))<GOAL>(𝒰.gluedCover.ι i).val.base x = (𝒰.gluedCover.ι j).val.base y
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>i : 𝒰.gluedCover.J<VAR>x : ↑↑(𝒰.gluedCover.U i).toPresheafedSpace<VAR>j : 𝒰.gluedCover.J<VAR>y : ↑↑(𝒰.gluedCover.U j).toPresheafedSpace<VAR>h : (𝒰.map i).val.base x = (𝒰.map j).val.base y<VAR>e : (TopCat.pullbackCone (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).pt ≅ (PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.map i) (𝒰.map j))) (forgetToTop.map (pullback.snd (𝒰.map i) (𝒰.map j))) ⋯).pt := (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).conePointUniqueUpToIso (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.map i) (𝒰.map j))<GOAL>𝒰.gluedCover.Rel ⟨i, x⟩ ⟨j, y⟩
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>i : 𝒰.gluedCover.J<VAR>x : ↑↑(𝒰.gluedCover.U i).toPresheafedSpace<VAR>j : 𝒰.gluedCover.J<VAR>y : ↑↑(𝒰.gluedCover.U j).toPresheafedSpace<VAR>h : (𝒰.map i).val.base x = (𝒰.map j).val.base y<VAR>e : (TopCat.pullbackCone (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).pt ≅ (PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.map i) (𝒰.map j))) (forgetToTop.map (pullback.snd (𝒰.map i) (𝒰.map j))) ⋯).pt := (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).conePointUniqueUpToIso (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.map i) (𝒰.map j))<GOAL>∃ x_1, (𝒰.gluedCover.f ⟨i, x⟩.fst ⟨j, y⟩.fst).val.base x_1 = ⟨i, x⟩.snd ∧ (𝒰.gluedCover.t ⟨i, x⟩.fst ⟨j, y⟩.fst ≫ 𝒰.gluedCover.f ⟨j, y⟩.fst ⟨i, x⟩.fst).val.base x_1 = ⟨j, y⟩.snd
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>i : 𝒰.gluedCover.J<VAR>x : ↑↑(𝒰.gluedCover.U i).toPresheafedSpace<VAR>j : 𝒰.gluedCover.J<VAR>y : ↑↑(𝒰.gluedCover.U j).toPresheafedSpace<VAR>h : (𝒰.map i).val.base x = (𝒰.map j).val.base y<VAR>e : (TopCat.pullbackCone (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).pt ≅ (PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.map i) (𝒰.map j))) (forgetToTop.map (pullback.snd (𝒰.map i) (𝒰.map j))) ⋯).pt := (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.map i)) (forgetToTop.map (𝒰.map j))).conePointUniqueUpToIso (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.map i) (𝒰.map j))<GOAL>(𝒰.gluedCover.f ⟨i, x⟩.fst ⟨j, y⟩.fst).val.base (e.hom ⟨(x, y), h⟩) = ⟨i, x⟩.snd ∧ (𝒰.gluedCover.t ⟨i, x⟩.fst ⟨j, y⟩.fst ≫ 𝒰.gluedCover.f ⟨j, y⟩.fst ⟨i, x⟩.fst).val.base (e.hom ⟨(x, y), h⟩) = ⟨j, y⟩.snd
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>x y : ↥H<VAR>hx : x ∈ Weight.ker<VAR>hy : y ∈ span K {coroot α}<GOAL>((traceForm K (↥H) L) x) y = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>x y : ↥H<VAR>hx : x ∈ Weight.ker<VAR>hy : y ∈ span K {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = ↑x}<GOAL>((traceForm K (↥H) L) x) y = 0
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<GOAL>(X • A.map ⇑C + B.map ⇑C).det.coeff 0 = B.det
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<GOAL>∑ b : Equiv.Perm n, (sign b • ∏ i : n, (X • A.map ⇑C + B.map ⇑C) (b i) i).coeff 0 = ∑ σ : Equiv.Perm n, sign σ • ∏ i : n, B (σ i) i
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<GOAL>∀ x ∈ Finset.univ, (sign x • ∏ i : n, (X • A.map ⇑C + B.map ⇑C) (x i) i).coeff 0 = sign x • ∏ i : n, B (x i) i
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>g : Equiv.Perm n<GOAL>(sign g • ∏ i : n, (X • A.map ⇑C + B.map ⇑C) (g i) i).coeff 0 = sign g • ∏ i : n, B (g i) i
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>g : Equiv.Perm n<GOAL>∏ i : n, B (g i) i = (∏ i : n, (X • A.map ⇑C + B.map ⇑C) (g i) i).coeff 0
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>g : Equiv.Perm n<GOAL>∏ i : n, B (g i) i = ∏ i : n, ((X • A.map ⇑C + B.map ⇑C) (g i) i).coeff 0
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>g : Equiv.Perm n<GOAL>∀ x ∈ Finset.univ, B (g x) x = ((X • A.map ⇑C + B.map ⇑C) (g x) x).coeff 0
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<GOAL>y ∈ ball x ε ↔ dist x y < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Finset ℕ<VAR>n✝ n : ℕ<VAR>hn : 2 ≤ n<VAR>a₁✝ a₂✝ : Finset ℕ<VAR>h : (fun s => ∑ i ∈ s, n ^ i) a₁✝ = (fun s => ∑ i ∈ s, n ^ i) a₂✝<GOAL>a₁✝ = a₂✝
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K F<VAR>ι : Type w<VAR>pb : PowerBasis R S<GOAL>(norm R) pb.gen = (-1) ^ pb.dim * (minpoly R pb.gen).coeff 0
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v✝ : K<VAR>n : ℕ<VAR>v : K<GOAL>(match (IntFractPair.of v, Stream'.Seq.tail ⟨IntFractPair.stream v, ⋯⟩) with | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).s.get? 0 = (IntFractPair.stream v 1).bind (some ∘ fun p => { a := 1, b := ↑p.b })
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v✝ : K<VAR>n : ℕ<VAR>v : K<GOAL>Option.map (fun p => { a := 1, b := ↑p.b }) ((IntFractPair.stream v).tail.get 0) = (IntFractPair.stream v 1).bind (some ∘ fun p => { a := 1, b := ↑p.b })
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v✝ : K<VAR>n : ℕ<VAR>v : K<GOAL>(match IntFractPair.stream v (Nat.succ 0) with | some x => some { a := 1, b := ↑x.b } | none => none) = (IntFractPair.stream v 1).bind (some ∘ fun p => { a := 1, b := ↑p.b })
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : HasAntidiagonal A<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>f g : A → α<VAR>inst✝¹ : T3Space α<VAR>inst✝ : TopologicalSemiring α<VAR>hf : Summable f<VAR>hg : Summable g<VAR>hfg : Summable fun x => f x.1 * g x.2<GOAL>(∑' (n : A), f n) * ∑' (n : A), g n = ∑' (n : A), ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : HasAntidiagonal A<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>f g : A → α<VAR>inst✝¹ : T3Space α<VAR>inst✝ : TopologicalSemiring α<VAR>hf : Summable f<VAR>hg : Summable g<VAR>hfg : Summable fun x => f x.1 * g x.2<GOAL>(∑' (n : A), f n) * ∑' (n : A), g n = ∑' (x : A) (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : HasAntidiagonal A<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>f g : A → α<VAR>inst✝¹ : T3Space α<VAR>inst✝ : TopologicalSemiring α<VAR>hf : Summable f<VAR>hg : Summable g<VAR>hfg : Summable fun x => f x.1 * g x.2<GOAL>∑' (c : (n : A) × { x // x ∈ antidiagonal n }), f (sigmaAntidiagonalEquivProd c).1 * g (sigmaAntidiagonalEquivProd c).2 = ∑' (x : A) (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e✝ : X ≃ₜ Y<VAR>e'✝ : Y ≃ₜ Z<VAR>e : X ≃ₜ Y<VAR>e' : Y ≃ₜ Z<VAR>f'' : PartialHomeomorph Z Z'<GOAL>(e.trans e').transPartialHomeomorph f'' = e.transPartialHomeomorph (e'.transPartialHomeomorph f'')
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f g : ι → N<VAR>s t : Finset ι<VAR>h : s ⊆ t<VAR>hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i<GOAL>∏ i ∈ s, f i ≤ ∏ i ∈ t, f i
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>∃ J, M.Basis J X ∧ I ⊆ J
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J✝ X Y : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hX : autoParam (X ⊆ M.E) _auto✝<VAR>J : Set α<VAR>hJmax : ∀ ⦃b : Set α⦄, b ∈ {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ X} → (fun x x_1 => x ⊆ x_1) J b → (fun x x_1 => x ⊆ x_1) b J<VAR>hJ : M.Indep J<VAR>hIJ : I ⊆ J<VAR>hJX : J ⊆ X<GOAL>∃ J, M.Basis J X ∧ I ⊆ J
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J✝ X Y : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hX : autoParam (X ⊆ M.E) _auto✝<VAR>J : Set α<VAR>hJmax : ∀ ⦃b : Set α⦄, b ∈ {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ X} → (fun x x_1 => x ⊆ x_1) J b → (fun x x_1 => x ⊆ x_1) b J<VAR>hJ : M.Indep J<VAR>hIJ : I ⊆ J<VAR>hJX : J ⊆ X<GOAL>M.Basis J X ∧ I ⊆ J
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J✝ X Y : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hX : autoParam (X ⊆ M.E) _auto✝<VAR>J : Set α<VAR>hJmax : ∀ ⦃b : Set α⦄, b ∈ {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ X} → (fun x x_1 => x ⊆ x_1) J b → (fun x x_1 => x ⊆ x_1) b J<VAR>hJ : M.Indep J<VAR>hIJ : I ⊆ J<VAR>hJX : J ⊆ X<GOAL>∀ (J_1 : Set α), M.Indep J_1 → J ⊆ J_1 → J_1 ⊆ X → J = J_1
<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<GOAL>Subsingleton (LieSubmodule R L M) ↔ Subsingleton (Submodule R M)
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ✝ : Type w₃<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>γ : Type w'<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>inst✝¹ : HasProduct f<VAR>inst✝ : HasProduct (f ∘ ⇑ε)<VAR>b : β<GOAL>(HasLimit.isoOfEquivalence (Discrete.equivalence ε) (Discrete.natIso fun x => Iso.refl (f (ε x.as)))).hom ≫ π f (ε b) = π (f ∘ ⇑ε) b
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ✝ : Type w₃<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>γ : Type w'<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>inst✝¹ : HasProduct f<VAR>inst✝ : HasProduct (f ∘ ⇑ε)<VAR>b : β<GOAL>limit.π (Discrete.functor (f ∘ ⇑ε)) { as := ε.symm (ε b) } ≫ (Discrete.functor f).map ((Discrete.equivalence ε).counit.app { as := ε b }) = π (f ∘ ⇑ε) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<GOAL>Continuous fun f => ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<GOAL>∀ (x : ↥(Lp E 1 ((κ ⊗ₖ η) a))), ContinuousAt (fun f => ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂η (a, x) ∂κ a) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 ((κ ⊗ₖ η) a))<GOAL>ContinuousAt (fun f => ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂η (a, x) ∂κ a) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 ((κ ⊗ₖ η) a))<GOAL>Tendsto (fun i => ∫⁻ (x : β), ↑‖∫ (y : γ), ↑↑i (x, y) ∂η (a, x) - ∫ (y : γ), ↑↑g (x, y) ∂η (a, x)‖₊ ∂κ a) (𝓝 g) (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 ((κ ⊗ₖ η) a))<GOAL>Tendsto (fun i => ∫⁻ (x : β), ↑‖∫ (y : γ), ↑↑i (x, y) - ↑↑g (x, y) ∂η (a, x)‖₊ ∂κ a) (𝓝 g) (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 ((κ ⊗ₖ η) a))<GOAL>↥(Lp E 1 ((κ ⊗ₖ η) a)) → ℝ≥0∞
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 ((κ ⊗ₖ η) a))<GOAL>Tendsto ?m.51003 (𝓝 g) (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 ((κ ⊗ₖ η) a))<GOAL>(fun i => ∫⁻ (x : β), ↑‖∫ (y : γ), ↑↑i (x, y) - ↑↑g (x, y) ∂η (a, x)‖₊ ∂κ a) ≤ ?m.51003
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 ((κ ⊗ₖ η) a))<GOAL>Tendsto (fun i => ∫⁻ (x : β), ∫⁻ (y : γ), ↑‖↑↑i (x, y) - ↑↑g (x, y)‖₊ ∂η (a, x) ∂κ a) (𝓝 g) (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 ((κ ⊗ₖ η) a))<VAR>this : ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η) a))), Measurable fun z => ↑‖↑↑i z - ↑↑g z‖₊<GOAL>Tendsto (fun i => ∫⁻ (x : β), ∫⁻ (y : γ), ↑‖↑↑i (x, y) - ↑↑g (x, y)‖₊ ∂η (a, x) ∂κ a) (𝓝 g) (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 ((κ ⊗ₖ η) a))<VAR>this : ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η) a))), Measurable fun z => ↑‖↑↑i z - ↑↑g z‖₊<GOAL>Tendsto (fun i => ENNReal.ofReal ‖i - g‖) (𝓝 g) (𝓝 (ENNReal.ofReal 0))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 ((κ ⊗ₖ η) a))<VAR>this : ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η) a))), Measurable fun z => ↑‖↑↑i z - ↑↑g z‖₊<GOAL>Tendsto (fun i => ‖i - g‖) (𝓝 g) (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 ((κ ⊗ₖ η) a))<VAR>this : ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η) a))), Measurable fun z => ↑‖↑↑i z - ↑↑g z‖₊<GOAL>Tendsto (fun i => i) (𝓝 g) (𝓝 g)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P Q : PresheafOfModules R<VAR>T : PresheafOfModules R<VAR>hom✝¹ : P.presheaf ⟶ Q.presheaf<VAR>map_smul✝¹ : ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)), (hom✝¹.app X) (r • x) = r • (hom✝¹.app X) x<VAR>hom✝ : P.presheaf ⟶ Q.presheaf<VAR>map_smul✝ : ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)), (hom✝.app X) (r • x) = r • (hom✝.app X) x<VAR>w : ∀ (X : Cᵒᵖ), { hom := hom✝¹, map_smul := map_smul✝¹ }.app X = { hom := hom✝, map_smul := map_smul✝ }.app X<VAR>X : Cᵒᵖ<VAR>x : ↑(P.presheaf.obj X)<GOAL>(hom✝¹.app X) x = (hom✝.app X) x
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>x : CofiniteTopology X<VAR>U : Set (CofiniteTopology X)<GOAL>U ∈ 𝓝 x ↔ U ∈ pure x ⊔ cofinite
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>x : CofiniteTopology X<VAR>U : Set (CofiniteTopology X)<GOAL>(∃ t ⊆ U, IsOpen t ∧ x ∈ t) ↔ U ∈ pure x ⊔ cofinite
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝ : L.Structure M<GOAL>CG L M ↔ ∃ S, S.Countable ∧ (closure L).toFun S = ⊤