ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₂✝ : Epi (app' φ 2 ⋯)<VAR>h₃✝ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>g₁ : A ⟶ R₂.obj' 1 ⋯<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝³ : Epi π₁<VAR>f₂ : A₁ ⟶ R₁.obj' 2 ⋯<VAR>h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>w✝² : Epi π₂<VAR>f₁ : A₂ ⟶ R₁.obj 1<VAR>h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)<VAR>h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0<VAR>A₃ : C<VAR>π₃ : A₃ ⟶ A₂<VAR>w✝¹ : Epi π₃<VAR>g₀ : A₃ ⟶ R₂.obj 0<VAR>h₅ : π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE ⋯)<VAR>A₄ : C<VAR>π₄ : A₄ ⟶ A₃<VAR>w✝ : Epi π₄<VAR>f₀ : A₄ ⟶ R₁.obj' 0 ⋯<VAR>h₆ : π₄ ≫ g₀ = f₀ ≫ app' φ 0 ⋯<GOAL>(π₄ ≫ π₃ ≫ π₂ ≫ π₁) ≫ g₁ = (π₄ ≫ π₃ ≫ f₁ + f₀ ≫ R₁.map' 0 1 ⋯ ⋯) ≫ app' φ 1 ⋯
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₂✝ : Epi (app' φ 2 ⋯)<VAR>h₃✝ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>g₁ : A ⟶ R₂.obj' 1 ⋯<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝³ : Epi π₁<VAR>f₂ : A₁ ⟶ R₁.obj' 2 ⋯<VAR>h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>w✝² : Epi π₂<VAR>f₁ : A₂ ⟶ R₁.obj 1<VAR>h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)<VAR>h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0<VAR>A₃ : C<VAR>π₃ : A₃ ⟶ A₂<VAR>w✝¹ : Epi π₃<VAR>g₀ : A₃ ⟶ R₂.obj 0<VAR>h₅ : π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE ⋯)<VAR>A₄ : C<VAR>π₄ : A₄ ⟶ A₃<VAR>w✝ : Epi π₄<VAR>f₀ : A₄ ⟶ R₁.obj' 0 ⋯<VAR>h₆ : π₄ ≫ g₀ = f₀ ≫ app' φ 0 ⋯<GOAL>π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ = π₄ ≫ π₃ ≫ f₁ ≫ app' φ 1 ⋯ + (π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₂✝ : Epi (app' φ 2 ⋯)<VAR>h₃✝ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>g₁ : A ⟶ R₂.obj' 1 ⋯<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝³ : Epi π₁<VAR>f₂ : A₁ ⟶ R₁.obj' 2 ⋯<VAR>h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 ⋯<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>w✝² : Epi π₂<VAR>f₁ : A₂ ⟶ R₁.obj 1<VAR>h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)<VAR>h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0<VAR>A₃ : C<VAR>π₃ : A₃ ⟶ A₂<VAR>w✝¹ : Epi π₃<VAR>g₀ : A₃ ⟶ R₂.obj 0<VAR>h₅ : π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE ⋯)<VAR>A₄ : C<VAR>π₄ : A₄ ⟶ A₃<VAR>w✝ : Epi π₄<VAR>f₀ : A₄ ⟶ R₁.obj' 0 ⋯<VAR>h₆ : π₄ ≫ g₀ = f₀ ≫ app' φ 0 ⋯<GOAL>π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ = π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1 + (π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B X R J : Set α<VAR>hX : X ⊆ E<GOAL>(loopyOn E).Basis ∅ X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B X R J : Set α<VAR>hX : X ⊆ E<GOAL>(loopyOn E).Indep ∅ ∧ ∅ ⊆ X ∧ ∀ (J : Set α), (loopyOn E).Indep J → ∅ ⊆ J → J ⊆ X → ∅ = J
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulReflectLE α β<VAR>h : a • b₁ ≤ a • b₂<VAR>ha : a < 0<GOAL>b₂ ≤ b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulReflectLE α β<VAR>h : -a • b₂ ≤ -a • b₁<VAR>ha : a < 0<GOAL>b₂ ≤ b₁
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁷ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>F : Type u_4<VAR>inst✝³ : NormedLatticeAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : OrderedSMul ℝ F<VAR>f : ι → Ω → F<VAR>c : ℝ<VAR>hc : c ≤ 0<VAR>hf : Submartingale f ℱ μ<GOAL>Supermartingale (c • f) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁷ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>F : Type u_4<VAR>inst✝³ : NormedLatticeAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : OrderedSMul ℝ F<VAR>f : ι → Ω → F<VAR>c : ℝ<VAR>hc : c ≤ 0<VAR>hf : Submartingale f ℱ μ<GOAL>Supermartingale (-(-c • f)) ℱ μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b✝ : α<VAR>n✝ : ℕ<VAR>ha : a ∈ s<VAR>n : ℕ<VAR>b : α<VAR>hb : b ∈ Sym.replicate n a<GOAL>b ∈ s
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>s s₁ s₂ : Finset ι<VAR>t t₁ t₂ : (i : ι) → Finset (α i)<GOAL>s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>a : α<VAR>l : List α<VAR>f : Equiv.Perm α<VAR>h✝ : f ∈ permsOfList (a :: l)<VAR>x : α<VAR>h : f ∈ l.bind fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)<VAR>hx : f x ≠ x<VAR>y : α<VAR>hy : y ∈ l<VAR>hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)<VAR>g : Equiv.Perm α<VAR>hg₁ : g ∈ permsOfList l<VAR>hg₂ : Equiv.swap a y * g = f<VAR>hxa : ¬x = a<VAR>hxy : ¬x = y<GOAL>g x ≠ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>a : α<VAR>l : List α<VAR>f : Equiv.Perm α<VAR>h✝ : f ∈ permsOfList (a :: l)<VAR>x : α<VAR>h : f ∈ l.bind fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)<VAR>hx : f x ≠ x<VAR>y : α<VAR>hy : y ∈ l<VAR>hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)<VAR>g : Equiv.Perm α<VAR>hg₁ : g ∈ permsOfList l<VAR>hg₂ : Equiv.swap a y * g = f<VAR>hxa : ¬x = a<VAR>hxy : ¬x = y<GOAL>(if f x = a then y else if f x = y then a else f x) ≠ x
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>a : α<VAR>l : List α<VAR>s : Stream' α<GOAL>drop (a :: l).length (a :: l ++ₛ s) = s
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>k n : ℕ<VAR>φ : R⟦X⟧<VAR>h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ<GOAL>(coeff R n) (φ ^ k) = ∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff R (l i)) φ
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>k n : ℕ<VAR>φ : R⟦X⟧<VAR>h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ<VAR>h₂ : ∀ (i : ℕ), ∏ j ∈ range i, Function.const ℕ φ j = φ ^ i<GOAL>(coeff R n) (φ ^ k) = ∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff R (l i)) φ
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>k n : ℕ<VAR>φ : R⟦X⟧<VAR>h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ<VAR>h₂ : ∀ (i : ℕ), ∏ j ∈ range i, Function.const ℕ φ j = φ ^ i<GOAL>(coeff R n) (∏ j ∈ range k, Function.const ℕ (Function.const ℕ φ k) j) = ∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff R (l i)) (Function.const ℕ φ k)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ✝ : Measure Ω<VAR>s t : Set Ω<VAR>inst✝³ : Fintype α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : DiscreteMeasurableSpace α<VAR>X : Ω → α<VAR>hX : Measurable X<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>E : Set Ω<VAR>hE : MeasurableSet E<GOAL>(∑ x : α, μ (X ⁻¹' {x}) • μ[|X ⁻¹' {x}]) E = μ E
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{u_6, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E : L.LeftExtension F<VAR>E' : ?m.37693<VAR>h✝ h : E.IsPointwiseLeftKanExtension<VAR>G : L.LeftExtension F<VAR>f₁ f₂ : E ⟶ G<VAR>Y : D<GOAL>f₁.right.app Y = f₂.right.app Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{u_6, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E : L.LeftExtension F<VAR>E' : ?m.37693<VAR>h✝ h : E.IsPointwiseLeftKanExtension<VAR>G : L.LeftExtension F<VAR>f₁ f₂ : E ⟶ G<VAR>Y : D<GOAL>∀ (j : CostructuredArrow L Y), (E.coconeAt Y).ι.app j ≫ f₁.right.app Y = (E.coconeAt Y).ι.app j ≫ f₂.right.app Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{u_6, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E : L.LeftExtension F<VAR>E' : ?m.37693<VAR>h✝ h : E.IsPointwiseLeftKanExtension<VAR>G : L.LeftExtension F<VAR>f₁ f₂ : E ⟶ G<VAR>Y : D<VAR>X : CostructuredArrow L Y<GOAL>(E.coconeAt Y).ι.app X ≫ f₁.right.app Y = (E.coconeAt Y).ι.app X ≫ f₂.right.app Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{u_6, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E : L.LeftExtension F<VAR>E' : ?m.37693<VAR>h✝ h : E.IsPointwiseLeftKanExtension<VAR>G : L.LeftExtension F<VAR>f₁ f₂ : E ⟶ G<VAR>Y : D<VAR>X : CostructuredArrow L Y<VAR>eq₁ : (E.hom ≫ ((whiskeringLeft C D H).obj L).map f₁.right).app X.left = G.hom.app X.left<GOAL>(E.coconeAt Y).ι.app X ≫ f₁.right.app Y = (E.coconeAt Y).ι.app X ≫ f₂.right.app Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{u_6, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E : L.LeftExtension F<VAR>E' : ?m.37693<VAR>h✝ h : E.IsPointwiseLeftKanExtension<VAR>G : L.LeftExtension F<VAR>f₁ f₂ : E ⟶ G<VAR>Y : D<VAR>X : CostructuredArrow L Y<VAR>eq₁ : (E.hom ≫ ((whiskeringLeft C D H).obj L).map f₁.right).app X.left = G.hom.app X.left<VAR>eq₂ : (E.hom ≫ ((whiskeringLeft C D H).obj L).map f₂.right).app X.left = G.hom.app X.left<GOAL>(E.coconeAt Y).ι.app X ≫ f₁.right.app Y = (E.coconeAt Y).ι.app X ≫ f₂.right.app Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{u_6, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E : L.LeftExtension F<VAR>E' : ?m.37693<VAR>h✝ h : E.IsPointwiseLeftKanExtension<VAR>G : L.LeftExtension F<VAR>f₁ f₂ : E ⟶ G<VAR>Y : D<VAR>X : CostructuredArrow L Y<VAR>eq₁ : E.hom.app X.left ≫ f₁.right.app (L.obj X.left) = G.hom.app X.left<VAR>eq₂ : E.hom.app X.left ≫ f₂.right.app (L.obj X.left) = G.hom.app X.left<GOAL>(E.hom.app X.left ≫ E.right.map X.hom) ≫ f₁.right.app Y = (E.hom.app X.left ≫ E.right.map X.hom) ≫ f₂.right.app Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{u_6, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E : L.LeftExtension F<VAR>E' : ?m.37693<VAR>h✝ h : E.IsPointwiseLeftKanExtension<VAR>G : L.LeftExtension F<VAR>f₁ f₂ : E ⟶ G<VAR>Y : D<VAR>X : CostructuredArrow L Y<VAR>eq₁ : E.hom.app X.left ≫ f₁.right.app (L.obj X.left) = G.hom.app X.left<VAR>eq₂ : E.hom.app X.left ≫ f₂.right.app (L.obj X.left) = G.hom.app X.left<GOAL>E.hom.app X.left ≫ f₁.right.app (L.obj X.left) ≫ G.right.map X.hom = E.hom.app X.left ≫ f₂.right.app (L.obj X.left) ≫ G.right.map X.hom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s✝ t : ι → α<VAR>a b : α<VAR>s : Set β<VAR>f : β → α<GOAL>IsGLB (f '' s) (⨅ x ∈ s, f x)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>U : X → Set X<VAR>hU : ∀ x ∈ s, U x ∈ 𝓝 x<GOAL>∃ t, t.Countable ∧ (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>hs : IsLindelof s<VAR>U : X → Set X<VAR>hU : ∀ x ∈ s, U x ∈ 𝓝 x<VAR>t : Set ↑s<VAR>htc : t.Countable<VAR>htsub : s ⊆ ⋃ x ∈ t, U ↑x<GOAL>∃ t, t.Countable ∧ (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>hs : IsLindelof s<VAR>U : X → Set X<VAR>hU : ∀ x ∈ s, U x ∈ 𝓝 x<VAR>t : Set ↑s<VAR>htc : t.Countable<VAR>htsub : s ⊆ ⋃ x ∈ t, U ↑x<GOAL>(∀ x ∈ Subtype.val '' t, x ∈ s) ∧ s ⊆ ⋃ x ∈ Subtype.val '' t, U x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>g : β → γ<VAR>hg : Continuous g<VAR>f : α →ₘ[μ] β<GOAL>comp g hg f = mk (g ∘ ↑f) ⋯
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>h : 0 < c<GOAL>(fun x => c * x) ⁻¹' Ico a b = Ico (a / c) (b / c)
<VAR>E : Type u_1<VAR>L✝ : Type u_2<VAR>inst✝⁶ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>inst✝ : Countable ↥L<VAR>fund : IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h : μ F * 2 ^ finrank ℝ E < μ s<GOAL>∃ x, x ≠ 0 ∧ ↑x ∈ s
<VAR>E : Type u_1<VAR>L✝ : Type u_2<VAR>inst✝⁶ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>inst✝ : Countable ↥L<VAR>fund : IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h : μ F * 2 ^ finrank ℝ E < μ s<VAR>h_vol : μ F < μ (2⁻¹ • s)<GOAL>∃ x, x ≠ 0 ∧ ↑x ∈ s
<VAR>E : Type u_1<VAR>L✝ : Type u_2<VAR>inst✝⁶ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>inst✝ : Countable ↥L<VAR>fund : IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h✝ : μ F * 2 ^ finrank ℝ E < μ s<VAR>h_vol : μ F < μ (2⁻¹ • s)<VAR>x y : ↥L<VAR>hxy : x ≠ y<VAR>h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)<GOAL>∃ x, x ≠ 0 ∧ ↑x ∈ s
<VAR>E : Type u_1<VAR>L✝ : Type u_2<VAR>inst✝⁶ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>inst✝ : Countable ↥L<VAR>fund : IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h✝ : μ F * 2 ^ finrank ℝ E < μ s<VAR>h_vol : μ F < μ (2⁻¹ • s)<VAR>x y : ↥L<VAR>hxy : x ≠ y<VAR>h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)<VAR>v : E<VAR>hv : v ∈ 2⁻¹ • s<VAR>w : E<VAR>hw : w ∈ 2⁻¹ • s<VAR>hvw : (fun x => y +ᵥ x) w = (fun x_1 => x +ᵥ x_1) v<GOAL>∃ x, x ≠ 0 ∧ ↑x ∈ s
<VAR>E : Type u_1<VAR>L✝ : Type u_2<VAR>inst✝⁶ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>inst✝ : Countable ↥L<VAR>fund : IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h✝ : μ F * 2 ^ finrank ℝ E < μ s<VAR>h_vol : μ F < μ (2⁻¹ • s)<VAR>x y : ↥L<VAR>hxy : x ≠ y<VAR>h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)<VAR>v : E<VAR>hv : v ∈ 2⁻¹ • s<VAR>w : E<VAR>hw : w ∈ 2⁻¹ • s<VAR>hvw : (fun x => y +ᵥ x) w = (fun x_1 => x +ᵥ x_1) v<GOAL>↑(x - y) ∈ s
<VAR>E : Type u_1<VAR>L✝ : Type u_2<VAR>inst✝⁶ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>inst✝ : Countable ↥L<VAR>fund : IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h✝ : μ F * 2 ^ finrank ℝ E < μ s<VAR>h_vol : μ F < μ (2⁻¹ • s)<VAR>x y : ↥L<VAR>hxy : x ≠ y<VAR>h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)<VAR>v : E<VAR>hv : 2 • v ∈ s<VAR>w : E<VAR>hw : 2 • w ∈ s<VAR>hvw : (fun x => y +ᵥ x) w = (fun x_1 => x +ᵥ x_1) v<GOAL>↑(x - y) ∈ s
<VAR>E : Type u_1<VAR>L✝ : Type u_2<VAR>inst✝⁶ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>inst✝ : Countable ↥L<VAR>fund : IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h✝ : μ F * 2 ^ finrank ℝ E < μ s<VAR>h_vol : μ F < μ (2⁻¹ • s)<VAR>x y : ↥L<VAR>hxy : x ≠ y<VAR>h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)<VAR>v : E<VAR>hv : 2 • v ∈ s<VAR>w : E<VAR>hw : 2 • w ∈ s<VAR>hvw : w - v = ↑(x - y)<GOAL>↑(x - y) ∈ s
<VAR>E : Type u_1<VAR>L✝ : Type u_2<VAR>inst✝⁶ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>inst✝ : Countable ↥L<VAR>fund : IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h✝ : μ F * 2 ^ finrank ℝ E < μ s<VAR>h_vol : μ F < μ (2⁻¹ • s)<VAR>x y : ↥L<VAR>hxy : x ≠ y<VAR>h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)<VAR>v : E<VAR>hv : 2 • v ∈ s<VAR>w : E<VAR>hw : 2 • w ∈ s<VAR>hvw : w - v = ↑(x - y)<GOAL>2⁻¹ • 2 • w + 2⁻¹ • -(2 • v) ∈ s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝²² : Category.{u_4, u_1} C<VAR>inst✝²¹ : Category.{u_6, u_2} D<VAR>inst✝²⁰ : Category.{u_5, u_3} E<VAR>inst✝¹⁹ : HasShift C ℤ<VAR>inst✝¹⁸ : HasShift D ℤ<VAR>inst✝¹⁷ : HasShift E ℤ<VAR>F : C ⥤ D<VAR>inst✝¹⁶ : F.CommShift ℤ<VAR>G : D ⥤ E<VAR>inst✝¹⁵ : G.CommShift ℤ<VAR>inst✝¹⁴ : HasZeroObject C<VAR>inst✝¹³ : HasZeroObject D<VAR>inst✝¹² : HasZeroObject E<VAR>inst✝¹¹ : Preadditive C<VAR>inst✝¹⁰ : Preadditive D<VAR>inst✝⁹ : Preadditive E<VAR>inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁷ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor E n).Additive<VAR>inst✝⁵ : Pretriangulated C<VAR>inst✝⁴ : Pretriangulated D<VAR>inst✝³ : Pretriangulated E<VAR>inst✝² : (F ⋙ G).IsTriangulated<VAR>inst✝¹ : F.IsTriangulated<VAR>inst✝ : F.mapArrow.EssSurj<VAR>T : Triangle D<VAR>hT : T ∈ distinguishedTriangles<GOAL>G.mapTriangle.obj T ∈ distinguishedTriangles
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝²² : Category.{u_4, u_1} C<VAR>inst✝²¹ : Category.{u_6, u_2} D<VAR>inst✝²⁰ : Category.{u_5, u_3} E<VAR>inst✝¹⁹ : HasShift C ℤ<VAR>inst✝¹⁸ : HasShift D ℤ<VAR>inst✝¹⁷ : HasShift E ℤ<VAR>F : C ⥤ D<VAR>inst✝¹⁶ : F.CommShift ℤ<VAR>G : D ⥤ E<VAR>inst✝¹⁵ : G.CommShift ℤ<VAR>inst✝¹⁴ : HasZeroObject C<VAR>inst✝¹³ : HasZeroObject D<VAR>inst✝¹² : HasZeroObject E<VAR>inst✝¹¹ : Preadditive C<VAR>inst✝¹⁰ : Preadditive D<VAR>inst✝⁹ : Preadditive E<VAR>inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁷ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor E n).Additive<VAR>inst✝⁵ : Pretriangulated C<VAR>inst✝⁴ : Pretriangulated D<VAR>inst✝³ : Pretriangulated E<VAR>inst✝² : (F ⋙ G).IsTriangulated<VAR>inst✝¹ : F.IsTriangulated<VAR>inst✝ : F.mapArrow.EssSurj<VAR>T : Triangle D<VAR>hT : T ∈ distinguishedTriangles<VAR>T' : Triangle C<VAR>hT' : T' ∈ distinguishedTriangles<VAR>e : F.mapTriangle.obj T' ≅ T<GOAL>G.mapTriangle.obj T ∈ distinguishedTriangles
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some '' Ici a = Ici ↑a
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : HasDerivWithinAt f f' S x<GOAL>slope f x y ≤ f'
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : HasDerivWithinAt f f' S x<GOAL>S ∈ 𝓝[>] x
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : HasDerivWithinAt f f' S x<GOAL>∃ u ∈ Ioi x, Ioc x u ⊆ S
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : LieAlgebra.IsNilpotent R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>χ : Weight R L M<VAR>x : L<GOAL>((toEnd R L M) x).HasEigenvalue (χ x)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : LieAlgebra.IsNilpotent R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>χ : Weight R L M<VAR>x : L<VAR>k : ℕ<VAR>hk : (((toEnd R L M) x).genEigenspace (χ x)) k ≠ ⊥<GOAL>((toEnd R L M) x).HasEigenvalue (χ x)
<VAR>c : Char<VAR>cs₁ cs₂ : List Char<VAR>i₁ i₂ : Pos<GOAL>ltb { s := { data := c :: cs₁ }, i := i₁ + c } { s := { data := c :: cs₂ }, i := i₂ + c } = ltb { s := { data := cs₁ }, i := i₁ } { s := { data := cs₂ }, i := i₂ }
<VAR>c : Char<VAR>cs₁✝ cs₂✝ : List Char<VAR>i₁✝ i₂✝ : Pos<VAR>cs₁ cs₂ : List Char<VAR>i₁ i₂ : Pos<VAR>a✝³ : { s := { data := cs₂ }, i := i₂ }.hasNext = true<VAR>a✝² : { s := { data := cs₁ }, i := i₁ }.hasNext = true<VAR>a✝¹ : { data := cs₁ }.get i₁ = { data := cs₂ }.get i₂<VAR>a✝ : ltb { s := { data := c :: { s := { data := cs₁ }, i := i₁ }.next.1.data }, i := { s := { data := cs₁ }, i := i₁ }.next.i + c } { s := { data := c :: { s := { data := cs₂ }, i := i₂ }.next.1.data }, i := { s := { data := cs₂ }, i := i₂ }.next.i + c } = ltb { s := { data := { s := { data := cs₁ }, i := i₁ }.next.1.data }, i := { s := { data := cs₁ }, i := i₁ }.next.i } { s := { data := { s := { data := cs₂ }, i := i₂ }.next.1.data }, i := { s := { data := cs₂ }, i := i₂ }.next.i }<GOAL>(if { s := { data := c :: cs₁ }, i := i₁ + c }.curr = { s := { data := c :: cs₂ }, i := i₂ + c }.curr then ltb { s := { data := c :: cs₁ }, i := i₁ + c }.next { s := { data := c :: cs₂ }, i := i₂ + c }.next else decide ({ s := { data := c :: cs₁ }, i := i₁ + c }.curr < { s := { data := c :: cs₂ }, i := i₂ + c }.curr)) = if { s := { data := cs₁ }, i := i₁ }.curr = { s := { data := cs₂ }, i := i₂ }.curr then ltb { s := { data := cs₁ }, i := i₁ }.next { s := { data := cs₂ }, i := i₂ }.next else decide ({ s := { data := cs₁ }, i := i₁ }.curr < { s := { data := cs₂ }, i := i₂ }.curr)
<VAR>c : Char<VAR>cs₁✝ cs₂✝ : List Char<VAR>i₁✝ i₂✝ : Pos<VAR>cs₁ cs₂ : List Char<VAR>i₁ i₂ : Pos<VAR>a✝² : { s := { data := cs₂ }, i := i₂ }.hasNext = true<VAR>a✝¹ : { s := { data := cs₁ }, i := i₁ }.hasNext = true<VAR>a✝ : ¬{ data := cs₁ }.get i₁ = { data := cs₂ }.get i₂<GOAL>(if { s := { data := c :: cs₁ }, i := i₁ + c }.curr = { s := { data := c :: cs₂ }, i := i₂ + c }.curr then ltb { s := { data := c :: cs₁ }, i := i₁ + c }.next { s := { data := c :: cs₂ }, i := i₂ + c }.next else decide ({ s := { data := c :: cs₁ }, i := i₁ + c }.curr < { s := { data := c :: cs₂ }, i := i₂ + c }.curr)) = if { s := { data := cs₁ }, i := i₁ }.curr = { s := { data := cs₂ }, i := i₂ }.curr then ltb { s := { data := cs₁ }, i := i₁ }.next { s := { data := cs₂ }, i := i₂ }.next else decide ({ s := { data := cs₁ }, i := i₁ }.curr < { s := { data := cs₂ }, i := i₂ }.curr)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>x✝² x✝¹ x✝ : ℤ<GOAL>id (x✝² + x✝¹) * id (x✝² - x✝¹) * id x✝ ^ 2 = id (x✝² + x✝) * id (x✝² - x✝) * id x✝¹ ^ 2 - id (x✝¹ + x✝) * id (x✝¹ - x✝) * id x✝² ^ 2