ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝ : Fintype ι<VAR>x✝ : ι → R<GOAL>(MultilinearMap.mkPiRing R ι 0) x✝ = 0 x✝
<VAR>n : ℕ<GOAL>↑↑(n + 1) = n + 1
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{u_4, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>f₁ f₂ : X ⟶ Y<GOAL>L.map (f₁ + f₂) = L.map f₁ + L.map f₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{u_4, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>f₁ f₂ : X ⟶ Y<GOAL>L.map (f₁ + f₂) = add W (Iso.refl (L.obj X)) (Iso.refl (L.obj Y)) (L.map f₁) (L.map f₂)
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>S : Type u_2<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>hf : Surjective ⇑f<VAR>H : IsNoetherianRing R<GOAL>IsNoetherianRing S
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>S : Type u_2<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>hf : Surjective ⇑f<VAR>H : WellFounded fun x x_1 => x > x_1<GOAL>WellFounded fun x x_1 => x > x_1
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<GOAL>J₁ ∈ π.restrict J ↔ ∃ J' ∈ π, ↑J₁ = ↑J ⊓ ↑J'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.22533, u_2} D<VAR>W : MorphismProperty C<VAR>X Y : C<VAR>z₁ z₂ z₃ : W.LeftFraction X Y<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>Z₄ : C<VAR>t₁ : z₁.Y' ⟶ Z₄<VAR>t₂ : z₂.Y' ⟶ Z₄<VAR>hst : z₁.s ≫ t₁ = z₂.s ≫ t₂<VAR>hft : z₁.f ≫ t₁ = z₂.f ≫ t₂<VAR>ht : W (z₁.s ≫ t₁)<VAR>Z₅ : C<VAR>u₂ : z₂.Y' ⟶ Z₅<VAR>u₃ : z₃.Y' ⟶ Z₅<VAR>hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃<VAR>hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃<VAR>hu : W (z₂.s ≫ u₂)<GOAL>LeftFractionRel z₁ z₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.22533, u_2} D<VAR>W : MorphismProperty C<VAR>X Y : C<VAR>z₁ z₂ z₃ : W.LeftFraction X Y<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>Z₄ : C<VAR>t₁ : z₁.Y' ⟶ Z₄<VAR>t₂ : z₂.Y' ⟶ Z₄<VAR>hst : z₁.s ≫ t₁ = z₂.s ≫ t₂<VAR>hft : z₁.f ≫ t₁ = z₂.f ≫ t₂<VAR>ht : W (z₁.s ≫ t₁)<VAR>Z₅ : C<VAR>u₂ : z₂.Y' ⟶ Z₅<VAR>u₃ : z₃.Y' ⟶ Z₅<VAR>hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃<VAR>hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃<VAR>hu : W (z₂.s ≫ u₂)<VAR>Y'✝ : C<VAR>v₄ : Z₄ ⟶ Y'✝<VAR>v₅ : Z₅ ⟶ Y'✝<VAR>hv₅ : W v₅<VAR>fac : (RightFraction.mk (z₁.s ≫ t₁) ht (z₃.s ≫ u₃)).f ≫ (LeftFraction.mk v₄ v₅ hv₅).s = (RightFraction.mk (z₁.s ≫ t₁) ht (z₃.s ≫ u₃)).s ≫ (LeftFraction.mk v₄ v₅ hv₅).f<GOAL>LeftFractionRel z₁ z₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.22533, u_2} D<VAR>W : MorphismProperty C<VAR>X Y : C<VAR>z₁ z₂ z₃ : W.LeftFraction X Y<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>Z₄ : C<VAR>t₁ : z₁.Y' ⟶ Z₄<VAR>t₂ : z₂.Y' ⟶ Z₄<VAR>hst : z₁.s ≫ t₁ = z₂.s ≫ t₂<VAR>hft : z₁.f ≫ t₁ = z₂.f ≫ t₂<VAR>ht : W (z₁.s ≫ t₁)<VAR>Z₅ : C<VAR>u₂ : z₂.Y' ⟶ Z₅<VAR>u₃ : z₃.Y' ⟶ Z₅<VAR>hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃<VAR>hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃<VAR>hu : W (z₂.s ≫ u₂)<VAR>Y'✝ : C<VAR>v₄ : Z₄ ⟶ Y'✝<VAR>v₅ : Z₅ ⟶ Y'✝<VAR>hv₅ : W v₅<VAR>fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄<GOAL>LeftFractionRel z₁ z₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.22533, u_2} D<VAR>W : MorphismProperty C<VAR>X Y : C<VAR>z₁ z₂ z₃ : W.LeftFraction X Y<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>Z₄ : C<VAR>t₁ : z₁.Y' ⟶ Z₄<VAR>t₂ : z₂.Y' ⟶ Z₄<VAR>hst : z₁.s ≫ t₁ = z₂.s ≫ t₂<VAR>hft : z₁.f ≫ t₁ = z₂.f ≫ t₂<VAR>ht : W (z₁.s ≫ t₁)<VAR>Z₅ : C<VAR>u₂ : z₂.Y' ⟶ Z₅<VAR>u₃ : z₃.Y' ⟶ Z₅<VAR>hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃<VAR>hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃<VAR>hu : W (z₂.s ≫ u₂)<VAR>Y'✝ : C<VAR>v₄ : Z₄ ⟶ Y'✝<VAR>v₅ : Z₅ ⟶ Y'✝<VAR>hv₅ : W v₅<VAR>fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄<VAR>eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄<GOAL>LeftFractionRel z₁ z₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.22533, u_2} D<VAR>W : MorphismProperty C<VAR>X Y : C<VAR>z₁ z₂ z₃ : W.LeftFraction X Y<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>Z₄ : C<VAR>t₁ : z₁.Y' ⟶ Z₄<VAR>t₂ : z₂.Y' ⟶ Z₄<VAR>hst : z₁.s ≫ t₁ = z₂.s ≫ t₂<VAR>hft : z₁.f ≫ t₁ = z₂.f ≫ t₂<VAR>ht : W (z₁.s ≫ t₁)<VAR>Z₅ : C<VAR>u₂ : z₂.Y' ⟶ Z₅<VAR>u₃ : z₃.Y' ⟶ Z₅<VAR>hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃<VAR>hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃<VAR>hu : W (z₂.s ≫ u₂)<VAR>Y'✝ : C<VAR>v₄ : Z₄ ⟶ Y'✝<VAR>v₅ : Z₅ ⟶ Y'✝<VAR>hv₅ : W v₅<VAR>fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄<VAR>eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄<VAR>Z₇ : C<VAR>w : Y'✝ ⟶ Z₇<VAR>hw : W w<VAR>fac' : (u₂ ≫ v₅) ≫ w = (t₂ ≫ v₄) ≫ w<GOAL>LeftFractionRel z₁ z₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.22533, u_2} D<VAR>W : MorphismProperty C<VAR>X Y : C<VAR>z₁ z₂ z₃ : W.LeftFraction X Y<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>Z₄ : C<VAR>t₁ : z₁.Y' ⟶ Z₄<VAR>t₂ : z₂.Y' ⟶ Z₄<VAR>hst : z₁.s ≫ t₁ = z₂.s ≫ t₂<VAR>hft : z₁.f ≫ t₁ = z₂.f ≫ t₂<VAR>ht : W (z₁.s ≫ t₁)<VAR>Z₅ : C<VAR>u₂ : z₂.Y' ⟶ Z₅<VAR>u₃ : z₃.Y' ⟶ Z₅<VAR>hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃<VAR>hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃<VAR>hu : W (z₂.s ≫ u₂)<VAR>Y'✝ : C<VAR>v₄ : Z₄ ⟶ Y'✝<VAR>v₅ : Z₅ ⟶ Y'✝<VAR>hv₅ : W v₅<VAR>fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄<VAR>eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄<VAR>Z₇ : C<VAR>w : Y'✝ ⟶ Z₇<VAR>hw : W w<VAR>fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w<GOAL>LeftFractionRel z₁ z₃
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>min a b = if b ≤ a then b else a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>(if a ≤ b then a else b) = if b ≤ a then b else a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>lt : a < b<GOAL>(if a ≤ b then a else b) = if b ≤ a then b else a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>eq : a = b<GOAL>(if a ≤ b then a else b) = if b ≤ a then b else a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>gt : b < a<GOAL>(if a ≤ b then a else b) = if b ≤ a then b else a
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>x : (i : ι) → π i<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>hst : Disjoint s t<VAR>y : (i : { x // x ∈ s }) → π ↑i<VAR>z : (i : { x // x ∈ t }) → π ↑i<VAR>e : { x // x ∈ s } ⊕ { x // x ∈ t } ≃ { x // x ∈ s ∪ t } := Finset.union s t hst<VAR>i : ι<GOAL>updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>x : (i : ι) → π i<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>hst : Disjoint s t<VAR>y : (i : { x // x ∈ s }) → π ↑i<VAR>z : (i : { x // x ∈ t }) → π ↑i<VAR>e : { x // x ∈ s } ⊕ { x // x ∈ t } ≃ { x // x ∈ s ∪ t } := Finset.union s t hst<VAR>i : ι<VAR>his : i ∈ s<VAR>hit : i ∈ t<GOAL>z ⟨i, ⋯⟩ = (piFinsetUnion π hst) (y, z) ⟨i, ⋯⟩
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>x : (i : ι) → π i<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>hst : Disjoint s t<VAR>y : (i : { x // x ∈ s }) → π ↑i<VAR>z : (i : { x // x ∈ t }) → π ↑i<VAR>e : { x // x ∈ s } ⊕ { x // x ∈ t } ≃ { x // x ∈ s ∪ t } := Finset.union s t hst<VAR>i : ι<VAR>his : i ∈ s<VAR>hit : i ∉ t<GOAL>y ⟨i, ⋯⟩ = (piFinsetUnion π hst) (y, z) ⟨i, ⋯⟩
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>x : (i : ι) → π i<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>hst : Disjoint s t<VAR>y : (i : { x // x ∈ s }) → π ↑i<VAR>z : (i : { x // x ∈ t }) → π ↑i<VAR>e : { x // x ∈ s } ⊕ { x // x ∈ t } ≃ { x // x ∈ s ∪ t } := Finset.union s t hst<VAR>i : ι<VAR>his : i ∉ s<VAR>hit : i ∈ t<GOAL>z ⟨i, ⋯⟩ = (piFinsetUnion π hst) (y, z) ⟨i, ⋯⟩
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>U : Set R<GOAL>U ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ U
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>U : Set R<GOAL>(∃ i ∈ RingFilterBasis.toAddGroupFilterBasis, id i ⊆ U) ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ U
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : PullbackCone f g<GOAL>pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst = s.fst
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : PullbackCone f g<GOAL>(pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).base = s.fst.base
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : PullbackCone f g<VAR>x : (Opens ↑↑X)ᵒᵖ<GOAL>((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).c ≫ whiskerRight (eqToHom ⋯) s.pt.presheaf).app x = s.fst.c.app x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<GOAL>P ∈ R[X]⁰ ↔ ∀ (a : R), a • P = 0 → a = 0
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι✝ → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>ι : Type u_9<VAR>f : ι → A<VAR>hf : AlgebraicIndependent R f<VAR>a✝ : Nontrivial R<GOAL>AlgebraicIndependent R Subtype.val
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>l : F → E<VAR>l' : F →L[𝕜] E<VAR>y : F<VAR>hl : DifferentiableAt 𝕜 l (f x)<VAR>hf : DifferentiableAt 𝕜 f x<VAR>hy : y = f x<GOAL>deriv (l ∘ f) x = (fderiv 𝕜 l (f x)) (deriv f x)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i✝ : ι<VAR>c : R<VAR>x : M<VAR>S : Type u_10<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M'<VAR>inst✝ : SMulCommClass R S M'<VAR>f : M' →ₗ[R] M'<VAR>v : ι → M'<VAR>i : ι<GOAL>((b.constr S) (⇑f ∘ v)) (b i) = (f ∘ₗ (b.constr S) v) (b i)
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x : ℝ≥0∞<GOAL>x.toReal = 0 ↔ x = 0 ∨ x = ⊤
<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>M✝ : Type u_7<VAR>inst✝¹ : MulOneClass M✝<VAR>M : Type u_8<VAR>inst✝ : Monoid M<VAR>f : G →* M<VAR>x : G<GOAL>x ∈ f.toHomUnits.ker ↔ x ∈ f.ker
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddMonoid R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hxy : x + y ≠ 0<GOAL>min (⋯.min ⋯) (⋯.min ⋯) ≤ ⋯.min ⋯
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddMonoid R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hxy : x + y ≠ 0<GOAL>⋯.min ⋯ ≤ ⋯.min ⋯
<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>(limitRightOpIsoOpColimit F).hom ≫ (colimit.ι F (op i)).op = limit.π F.rightOp i
<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>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>μ' : Measure α<VAR>hT_add : DominatedFinMeasAdditive (μ + μ') T C'<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>f : α → E<VAR>hf : Integrable f (μ + μ')<GOAL>setToFun (μ + μ') T hT_add f = setToFun μ T hT f
<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>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>μ' : Measure α<VAR>hT_add : DominatedFinMeasAdditive (μ + μ') T C'<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>f : α → E<VAR>hf : Integrable f (μ + μ')<GOAL>μ ≤ 1 • (μ + μ')
<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>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>μ' : Measure α<VAR>hT_add : DominatedFinMeasAdditive (μ + μ') T C'<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>f : α → E<VAR>hf : Integrable f (μ + μ')<GOAL>μ ≤ μ + μ'
<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>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>μ' : Measure α<VAR>hT_add : DominatedFinMeasAdditive (μ + μ') T C'<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>f : α → E<VAR>hf : Integrable f (μ + μ')<GOAL>μ + 0 ≤ μ + μ'
<VAR>p : ℝ[X]<VAR>x : ℝ<GOAL>HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) (Polynomial.eval x⁻¹ (X ^ 2 * (p - derivative p)) * expNegInvGlue x) x
<VAR>p : ℝ[X]<VAR>x : ℝ<VAR>hx : x < 0<GOAL>HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) (Polynomial.eval x⁻¹ (X ^ 2 * (p - derivative p)) * expNegInvGlue x) x
<VAR>p : ℝ[X]<GOAL>HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) (Polynomial.eval 0⁻¹ (X ^ 2 * (p - derivative p)) * expNegInvGlue 0) 0
<VAR>p : ℝ[X]<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) (Polynomial.eval x⁻¹ (X ^ 2 * (p - derivative p)) * expNegInvGlue x) x
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<GOAL>toIcoDiv hp (a - c) b = toIcoDiv hp a (b + c)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>p p'✝ : Submodule R M<VAR>q : Submodule R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>p' : Submodule R ↥p<GOAL>map p.subtype p' ≤ p
<VAR>x✝ : Iterator<VAR>h : x✝.Valid<VAR>hn : x✝.hasNext = true<GOAL>x✝.next.Valid
<VAR>x✝ : Iterator<VAR>h✝ : x✝.Valid<VAR>hn : x✝.hasNext = true<VAR>l r : List Char<VAR>h : ValidFor l r x✝<GOAL>x✝.next.Valid
<VAR>x✝ : Iterator<VAR>h✝ : x✝.Valid<VAR>hn : x✝.hasNext = true<VAR>l : List Char<VAR>c : Char<VAR>r : List Char<VAR>h : ValidFor l (c :: r) x✝<GOAL>x✝.next.Valid
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype o<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>A : Matrix m n R<VAR>v₁ : Basis m R M₁<VAR>v₂ : Basis n R M₂<GOAL>A.rank = finrank R ↥(LinearMap.range ((toLin v₂ v₁) A))
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype o<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>A : Matrix m n R<VAR>v₁ : Basis m R M₁<VAR>v₂ : Basis n R M₂<VAR>val✝ : Fintype m<GOAL>A.rank = finrank R ↥(LinearMap.range ((toLin v₂ v₁) A))
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype o<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>A : Matrix m n R<VAR>v₁ : Basis m R M₁<VAR>v₂ : Basis n R M₂<VAR>val✝ : Fintype m<VAR>e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)<VAR>e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)<GOAL>A.rank = finrank R ↥(LinearMap.range ((toLin v₂ v₁) A))
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype o<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>A : Matrix m n R<VAR>v₁ : Basis m R M₁<VAR>v₂ : Basis n R M₂<VAR>val✝ : Fintype m<VAR>e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)<VAR>e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)<VAR>range_e₂ : LinearMap.range e₂ = ⊤<GOAL>A.rank = finrank R ↥(LinearMap.range ((toLin v₂ v₁) A))
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype o<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>A : Matrix m n R<VAR>v₁ : Basis m R M₁<VAR>v₂ : Basis n R M₂<VAR>val✝ : Fintype m<VAR>e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)<VAR>e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)<VAR>range_e₂ : LinearMap.range e₂ = ⊤<GOAL>Submodule.map (↑e₁) (LinearMap.range A.mulVecLin) = LinearMap.range ((toLin v₂ v₁) A)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype o<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>A : Matrix m n R<VAR>v₁ : Basis m R M₁<VAR>v₂ : Basis n R M₂<VAR>val✝ : Fintype m<VAR>e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)<VAR>e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)<VAR>range_e₂ : LinearMap.range e₂ = ⊤<GOAL>LinearMap.range (↑e₁ ∘ₗ A.mulVecLin) = LinearMap.range ((toLin v₂ v₁) A ∘ₗ ↑e₂)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype o<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>A : Matrix m n R<VAR>v₁ : Basis m R M₁<VAR>v₂ : Basis n R M₂<VAR>val✝ : Fintype m<VAR>e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)<VAR>e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)<VAR>range_e₂ : LinearMap.range e₂ = ⊤<GOAL>↑e₁ ∘ₗ A.mulVecLin = (toLin v₂ v₁) A ∘ₗ ↑e₂
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype o<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>A : Matrix m n R<VAR>v₁ : Basis m R M₁<VAR>v₂ : Basis n R M₂<VAR>val✝ : Fintype m<VAR>e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)<VAR>e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)<VAR>range_e₂ : LinearMap.range e₂ = ⊤<GOAL>∀ (i : n), (↑e₁ ∘ₗ A.mulVecLin) ∘ₗ LinearMap.single i = ((toLin v₂ v₁) A ∘ₗ ↑e₂) ∘ₗ LinearMap.single i
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype o<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>A : Matrix m n R<VAR>v₁ : Basis m R M₁<VAR>v₂ : Basis n R M₂<VAR>val✝ : Fintype m<VAR>e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)<VAR>e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)<VAR>range_e₂ : LinearMap.range e₂ = ⊤<VAR>i : n<GOAL>(↑e₁ ∘ₗ A.mulVecLin) ∘ₗ LinearMap.single i = ((toLin v₂ v₁) A ∘ₗ ↑e₂) ∘ₗ LinearMap.single i
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype o<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>A : Matrix m n R<VAR>v₁ : Basis m R M₁<VAR>v₂ : Basis n R M₂<VAR>val✝ : Fintype m<VAR>e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)<VAR>e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)<VAR>range_e₂ : LinearMap.range e₂ = ⊤<VAR>i : n<GOAL>((↑e₁ ∘ₗ A.mulVecLin) ∘ₗ LinearMap.single i) 1 = (((toLin v₂ v₁) A ∘ₗ ↑e₂) ∘ₗ LinearMap.single i) 1
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype o<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>A : Matrix m n R<VAR>v₁ : Basis m R M₁<VAR>v₂ : Basis n R M₂<VAR>val✝ : Fintype m<VAR>e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)<VAR>e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)<VAR>range_e₂ : LinearMap.range e₂ = ⊤<VAR>i : n<VAR>aux₁ : ((toLin (Pi.basisFun R n) (Pi.basisFun R m)) A) ((Pi.basisFun R n) i) = ∑ j : m, A j i • (Pi.basisFun R m) j<GOAL>((↑e₁ ∘ₗ A.mulVecLin) ∘ₗ LinearMap.single i) 1 = (((toLin v₂ v₁) A ∘ₗ ↑e₂) ∘ₗ LinearMap.single i) 1