ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : Submodule R P<VAR>h : I ≤ 1<VAR>b' : R<VAR>hb : (Algebra.linearMap R P) b' ∈ I<GOAL>IsInteger R ((Algebra.linearMap R P) b')
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>s : Submodule K V<VAR>inst✝ : Module.Free K ↥s<GOAL>Module.rank K ↥s ≤ 1 ↔ ∃ v₀ ∈ s, s ≤ span K {v₀}
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>s : Submodule K V<VAR>inst✝ : Module.Free K ↥s<GOAL>(∃ v₀, ∀ (v : ↥s), ∃ r, r • v₀ = v) ↔ ∃ v₀ ∈ s, ∀ v ∈ s, ∃ r, r • v₀ = v
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f g : Filter α<VAR>m : α → β<VAR>h : Injective m<GOAL>map m (f ⊓ g) = map m f ⊓ map m g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f g : Filter α<VAR>m : α → β<VAR>h : Injective m<GOAL>map m f ⊓ map m g ≤ map m (f ⊓ g)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f g : Filter α<VAR>m : α → β<VAR>h : Injective m<VAR>t : Set β<VAR>s₁ : Set α<VAR>hs₁ : s₁ ∈ f<VAR>s₂ : Set α<VAR>hs₂ : s₂ ∈ g<VAR>ht : m ⁻¹' t = s₁ ∩ s₂<GOAL>t ∈ map m f ⊓ map m g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f g : Filter α<VAR>m : α → β<VAR>h : Injective m<VAR>t : Set β<VAR>s₁ : Set α<VAR>hs₁ : s₁ ∈ f<VAR>s₂ : Set α<VAR>hs₂ : s₂ ∈ g<VAR>ht : m ⁻¹' t = s₁ ∩ s₂<GOAL>m '' s₁ ∩ m '' s₂ ⊆ t
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>f : V ≃ₗᵢ[ℝ] ℂ<VAR>hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation<VAR>x y : V<GOAL>o.oangle x y = ↑((starRingEnd ℂ) (f x) * f y).arg
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>f : V ≃ₗᵢ[ℝ] ℂ<VAR>hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation<VAR>x y : V<GOAL>o.oangle x y = o.oangle (f.symm (f x)) (f.symm (f y))
<VAR>m n✝ i n : ℕ<VAR>hi : 2 ≤ i<GOAL>i + (n + 1)! < (i + n + 1)!
<VAR>m n✝ i n : ℕ<VAR>hi : 2 ≤ i<GOAL>i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
<VAR>m n✝ i n : ℕ<VAR>hi : 2 ≤ i<VAR>this : i + n ≤ (i + n)!<GOAL>i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>h : L (fun n => ↑(ζ n)) s = 0<GOAL>False
<VAR>n : ℕ<GOAL>(unpair n).2 ≤ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>(sort (fun x x_1 => x ≤ x_1) s).length - 1 < (sort (fun x x_1 => x ≤ x_1) s).length
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : IsDomain A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : NoZeroSMulDivisors R A<VAR>inst✝ : Countable R<GOAL>{x | IsAlgebraic R x}.Countable
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : IsDomain A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : NoZeroSMulDivisors R A<VAR>inst✝ : Countable R<GOAL>lift.{?u.23919, v} #↑{x | IsAlgebraic R x} ≤ ℵ₀
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : IsDomain A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : NoZeroSMulDivisors R A<VAR>inst✝ : Countable R<GOAL>max (lift.{v, u} #R) ℵ₀ ≤ ℵ₀
<VAR>a : UnitAddCircle<GOAL>DifferentiableAt ℂ (fun s => hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) 1
<VAR>a : UnitAddCircle<GOAL>DifferentiableAt ℂ (fun s => completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
<VAR>a : UnitAddCircle<GOAL>DifferentiableAt ℂ (fun s => (completedHurwitzZetaEven a s - 1 / (s - 1)) * s.Gammaℝ⁻¹) 1
<VAR>a : UnitAddCircle<GOAL>DifferentiableAt ℂ (fun s => completedHurwitzZetaEven a s - 1 / (s - 1)) 1
<VAR>a : UnitAddCircle<GOAL>DifferentiableAt ℂ (fun s => completedHurwitzZetaEven₀ a s - ((if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1)))) 1
<VAR>a : UnitAddCircle<GOAL>DifferentiableAt ℂ (fun s => completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s) 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<VAR>a : αˣ<VAR>b : α<GOAL>Irreducible (b * ↑a) ↔ Irreducible b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<VAR>a : αˣ<VAR>b : α<GOAL>¬IsUnit b → ((∀ (a_2 b_1 : α), b * ↑a = a_2 * b_1 → IsUnit a_2 ∨ IsUnit b_1) ↔ ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1)
<VAR>l l' : List Char<VAR>h : l.asString = l'.asString<GOAL>l = l'
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>x : L<GOAL>x ∈ engel R x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>x : L<GOAL>∃ n, ((ad R L) x ^ n) x = 0
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : MonoidalCategory C<VAR>A✝ B X X' Y Y' Z : C<VAR>inst✝² : Closed A✝<VAR>inst✝¹ : Closed B<VAR>A : C<VAR>inst✝ : Closed A<GOAL>pre (𝟙 A) = 𝟙 (ihom A)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : MonoidalCategory C<VAR>A✝ B X X' Y Y' Z : C<VAR>inst✝² : Closed A✝<VAR>inst✝¹ : Closed B<VAR>A : C<VAR>inst✝ : Closed A<GOAL>(conjugateEquiv (ihom.adjunction A) (ihom.adjunction A)) (𝟙 ((tensoringLeft C).obj A)) = 𝟙 (ihom A)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : CharP R p<GOAL>↑p ≠ 0
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<GOAL>f ≤ f.sup g h
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<VAR>z₁ : ↥f.domain<VAR>z₂ : ↥(f.sup g h).domain<VAR>hz : ↑z₁ = ↑z₂<GOAL>↑f z₁ = ↑(f.sup g h) z₂
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<VAR>z₁ : ↥f.domain<VAR>z₂ : ↥(f.sup g h).domain<VAR>hz : ↑z₁ = ↑z₂<GOAL>↑f z₁ + ↑g 0 = ↑(f.sup g h) z₂
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<VAR>z₁ : ↥f.domain<VAR>z₂ : ↥(f.sup g h).domain<VAR>hz : ↑z₁ = ↑z₂<GOAL>↑z₁ + ↑0 = ↑z₂
<VAR>s : ℂ<GOAL>hurwitzZeta 0 s = riemannZeta s
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>x : P<VAR>I : FractionalIdeal S P<GOAL>spanSingleton S x ≤ I ↔ x ∈ I
<VAR>C : Type u_5<VAR>C' : Type ?u.64843<VAR>D : Type u_3<VAR>D' : Type ?u.64849<VAR>H : Type u_4<VAR>H' : Type ?u.64855<VAR>inst✝⁹ : Category.{u_6, u_5} C<VAR>inst✝⁸ : Category.{?u.64863, ?u.64843} C'<VAR>inst✝⁷ : Category.{u_1, u_3} D<VAR>inst✝⁶ : Category.{?u.64871, ?u.64849} D'<VAR>inst✝⁵ : Category.{u_2, u_4} H<VAR>inst✝⁴ : Category.{?u.64879, ?u.64855} H'<VAR>RF RF' RF'' : D ⥤ H<VAR>F F' F'' : C ⥤ H<VAR>e : F ≅ F'<VAR>L : C ⥤ D<VAR>α : F ⟶ L ⋙ RF<VAR>α' : F' ⟶ L ⋙ RF'<VAR>α'' : F'' ⟶ L ⋙ RF''<VAR>α'₂ : F ⟶ L ⋙ RF'<VAR>W : MorphismProperty C<VAR>inst✝³ : L.IsLocalization W<VAR>inst✝² : RF.IsRightDerivedFunctor α W<VAR>inst✝¹ : RF'.IsRightDerivedFunctor α' W<VAR>inst✝ : RF''.IsRightDerivedFunctor α'' W<VAR>G : D ⥤ H<VAR>β : F ⟶ L ⋙ G<GOAL>G.IsRightDerivedFunctor β W ↔ IsIso (RF.rightDerivedDesc α W G β)
<VAR>C : Type u_5<VAR>C' : Type ?u.64843<VAR>D : Type u_3<VAR>D' : Type ?u.64849<VAR>H : Type u_4<VAR>H' : Type ?u.64855<VAR>inst✝⁹ : Category.{u_6, u_5} C<VAR>inst✝⁸ : Category.{?u.64863, ?u.64843} C'<VAR>inst✝⁷ : Category.{u_1, u_3} D<VAR>inst✝⁶ : Category.{?u.64871, ?u.64849} D'<VAR>inst✝⁵ : Category.{u_2, u_4} H<VAR>inst✝⁴ : Category.{?u.64879, ?u.64855} H'<VAR>RF RF' RF'' : D ⥤ H<VAR>F F' F'' : C ⥤ H<VAR>e : F ≅ F'<VAR>L : C ⥤ D<VAR>α : F ⟶ L ⋙ RF<VAR>α' : F' ⟶ L ⋙ RF'<VAR>α'' : F'' ⟶ L ⋙ RF''<VAR>α'₂ : F ⟶ L ⋙ RF'<VAR>W : MorphismProperty C<VAR>inst✝³ : L.IsLocalization W<VAR>inst✝² : RF.IsRightDerivedFunctor α W<VAR>inst✝¹ : RF'.IsRightDerivedFunctor α' W<VAR>inst✝ : RF''.IsRightDerivedFunctor α'' W<VAR>G : D ⥤ H<VAR>β : F ⟶ L ⋙ G<GOAL>G.IsLeftKanExtension β ↔ IsIso (RF.rightDerivedDesc α W G β)
<VAR>C : Type u_5<VAR>C' : Type ?u.64843<VAR>D : Type u_3<VAR>D' : Type ?u.64849<VAR>H : Type u_4<VAR>H' : Type ?u.64855<VAR>inst✝⁹ : Category.{u_6, u_5} C<VAR>inst✝⁸ : Category.{?u.64863, ?u.64843} C'<VAR>inst✝⁷ : Category.{u_1, u_3} D<VAR>inst✝⁶ : Category.{?u.64871, ?u.64849} D'<VAR>inst✝⁵ : Category.{u_2, u_4} H<VAR>inst✝⁴ : Category.{?u.64879, ?u.64855} H'<VAR>RF RF' RF'' : D ⥤ H<VAR>F F' F'' : C ⥤ H<VAR>e : F ≅ F'<VAR>L : C ⥤ D<VAR>α : F ⟶ L ⋙ RF<VAR>α' : F' ⟶ L ⋙ RF'<VAR>α'' : F'' ⟶ L ⋙ RF''<VAR>α'₂ : F ⟶ L ⋙ RF'<VAR>W : MorphismProperty C<VAR>inst✝³ : L.IsLocalization W<VAR>inst✝² : RF.IsRightDerivedFunctor α W<VAR>inst✝¹ : RF'.IsRightDerivedFunctor α' W<VAR>inst✝ : RF''.IsRightDerivedFunctor α'' W<VAR>G : D ⥤ H<VAR>β : F ⟶ L ⋙ G<VAR>this : RF.IsLeftKanExtension α<GOAL>G.IsLeftKanExtension β ↔ IsIso (RF.rightDerivedDesc α W G β)
<VAR>α : Type u<VAR>m : ℕ<VAR>f : Fin m → α<GOAL>ofFn f = ofFn fun i => f (Fin.cast ⋯ i)
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>(baseChange W B).toAffine.polynomialY = Polynomial.map (mapRingHom ↑f) (baseChange W A).toAffine.polynomialY
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f : α →ₛ E<VAR>g : α →ₛ F<GOAL>Integrable (↑f) μ → Integrable (↑g) μ → Integrable (↑(f.pair g)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>val✝ : Multiset α<VAR>l : List α<VAR>hs : Multiset.Nodup (Quot.mk Setoid.r l)<VAR>f : Equiv.Perm α<GOAL>f ∈ permsOfFinset { val := Quot.mk Setoid.r l, nodup := hs } ↔ ∀ {x : α}, f x ≠ x → x ∈ { val := Quot.mk Setoid.r l, nodup := hs }
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>X Y : C<VAR>inst✝¹ : Simple X<VAR>f : X ⟶ Y<VAR>inst✝ : HasKernel f<VAR>w : f ≠ 0<GOAL>kernel.ι f = 0
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>m' _mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>s t : Set Ω<VAR>a✝ : s ∈ {s | MeasurableSet s}<VAR>ht : t ∈ {s | MeasurableSet s}<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>m' _mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>s t : Set Ω<VAR>a✝ : s ∈ {s | MeasurableSet s}<VAR>ht : t = ∅ ∨ t = Set.univ<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>m' _mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>s t : Set Ω<VAR>a✝ : s ∈ {s | MeasurableSet s}<VAR>ht : t = ∅ ∨ t = Set.univ<VAR>a : α<GOAL>(κ a) (s ∩ t) = (κ a) s * (κ a) t
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : SemilatticeInf β<VAR>f : F<VAR>inst✝ : InfHomClass F α β<VAR>hf : Injective ⇑f<VAR>x y : α<GOAL>f x ≤ f y ↔ x ≤ y
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : SemilatticeInf β<VAR>f : F<VAR>inst✝ : InfHomClass F α β<VAR>hf : Injective ⇑f<VAR>x y : α<VAR>h : f x ≤ f y<GOAL>x ≤ y
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>X Y Z : C<GOAL>(BinaryFan.associatorOfLimitCone ℬ X Y Z).hom ≫ ((ℬ X (tensorObj ℬ Y Z)).isLimit.conePointUniqueUpToIso (ℬ (tensorObj ℬ Y Z) X).isLimit.swapBinaryFan).hom ≫ (BinaryFan.associatorOfLimitCone ℬ Y Z X).hom = (ℬ (ℬ Y X).cone.pt Z).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ (ℬ X Y).cone.pt Z).cone ≫ ((ℬ X Y).isLimit.conePointUniqueUpToIso (ℬ Y X).isLimit.swapBinaryFan).hom) (BinaryFan.snd (ℬ (ℬ X Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫ (BinaryFan.associatorOfLimitCone ℬ Y X Z).hom ≫ (ℬ Y (ℬ Z X).cone.pt).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ Y (ℬ X Z).cone.pt).cone ≫ 𝟙 Y) (BinaryFan.snd (ℬ Y (ℬ X Z).cone.pt).cone ≫ ((ℬ X Z).isLimit.conePointUniqueUpToIso (ℬ Z X).isLimit.swapBinaryFan).hom))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>X Y Z : C<GOAL>∀ (j : Discrete WalkingPair), ((BinaryFan.associatorOfLimitCone ℬ X Y Z).hom ≫ ((ℬ X (tensorObj ℬ Y Z)).isLimit.conePointUniqueUpToIso (ℬ (tensorObj ℬ Y Z) X).isLimit.swapBinaryFan).hom ≫ (BinaryFan.associatorOfLimitCone ℬ Y Z X).hom) ≫ (ℬ Y (ℬ Z X).cone.pt).cone.π.app j = ((ℬ (ℬ Y X).cone.pt Z).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ (ℬ X Y).cone.pt Z).cone ≫ ((ℬ X Y).isLimit.conePointUniqueUpToIso (ℬ Y X).isLimit.swapBinaryFan).hom) (BinaryFan.snd (ℬ (ℬ X Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫ (BinaryFan.associatorOfLimitCone ℬ Y X Z).hom ≫ (ℬ Y (ℬ Z X).cone.pt).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ Y (ℬ X Z).cone.pt).cone ≫ 𝟙 Y) (BinaryFan.snd (ℬ Y (ℬ X Z).cone.pt).cone ≫ ((ℬ X Z).isLimit.conePointUniqueUpToIso (ℬ Z X).isLimit.swapBinaryFan).hom))) ≫ (ℬ Y (ℬ Z X).cone.pt).cone.π.app j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>L : List (List α)<VAR>i : Fin L.length<GOAL>drop (take (↑i) (map length L)).sum (take (take (↑i + 1) (map length L)).sum L.join) = L.get i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>L : List (List α)<VAR>i : Fin L.length<GOAL>L[↑i] = L.get i
<VAR>a b c✝ d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>c : ℕ<VAR>H : a % d = b % d<GOAL>(c + a) % d = (c + b) % d
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>m₂ m : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>p1 p2 : Set (Set Ω)<VAR>h2 : m₂ ≤ m<VAR>hp2 : IsPiSystem p2<VAR>hpm2 : m₂ = generateFrom p2<VAR>hyp : IndepSets p1 p2 κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ p1<VAR>ht1m : MeasurableSet t1<VAR>ht2m : MeasurableSet t2<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>m₂ m : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>p1 p2 : Set (Set Ω)<VAR>h2 : m₂ ≤ m<VAR>hp2 : IsPiSystem p2<VAR>hpm2 : m₂ = generateFrom p2<VAR>hyp : IndepSets p1 p2 κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ p1<VAR>ht1m : MeasurableSet t1<VAR>ht2m : MeasurableSet t2<GOAL>(fun t => ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t) = (κ a) t1 * (κ a) t) ∅
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>m₂ m : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>p1 p2 : Set (Set Ω)<VAR>h2 : m₂ ≤ m<VAR>hp2 : IsPiSystem p2<VAR>hpm2 : m₂ = generateFrom p2<VAR>hyp : IndepSets p1 p2 κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ p1<VAR>ht1m : MeasurableSet t1<VAR>ht2m : MeasurableSet t2<GOAL>∀ t ∈ p2, (fun t => ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t) = (κ a) t1 * (κ a) t) t
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>m₂ m : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>p1 p2 : Set (Set Ω)<VAR>h2 : m₂ ≤ m<VAR>hp2 : IsPiSystem p2<VAR>hpm2 : m₂ = generateFrom p2<VAR>hyp : IndepSets p1 p2 κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ p1<VAR>ht1m : MeasurableSet t1<VAR>ht2m : MeasurableSet t2<GOAL>∀ (t : Set Ω), MeasurableSet t → (fun t => ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t) = (κ a) t1 * (κ a) t) t → (fun t => ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t) = (κ a) t1 * (κ a) t) tᶜ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>m₂ m : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>p1 p2 : Set (Set Ω)<VAR>h2 : m₂ ≤ m<VAR>hp2 : IsPiSystem p2<VAR>hpm2 : m₂ = generateFrom p2<VAR>hyp : IndepSets p1 p2 κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ p1<VAR>ht1m : MeasurableSet t1<VAR>ht2m : MeasurableSet t2<GOAL>∀ (f : ℕ → Set Ω), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), (fun t => ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t) = (κ a) t1 * (κ a) t) (f i)) → (fun t => ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t) = (κ a) t1 * (κ a) t) (⋃ i, f i)
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<VAR>n : ℕ<GOAL>↑(↑n).toNNReal = ↑↑n
<VAR>ι : Type u_1<VAR>k : Type u_2<VAR>V : Type u_3<VAR>P : Type u_4<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : Fintype ι<VAR>p1 : P<VAR>p : ι → P<VAR>h : p1 ∈ affineSpan k (Set.range p)<GOAL>∃ w, ∑ i : ι, w i = 1 ∧ p1 = (Finset.affineCombination k Finset.univ p) w
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : OrderTop R<VAR>s : Multiset R<GOAL>trop s.inf = (map trop s).sum
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : OrderTop R<GOAL>trop (inf 0) = (map trop 0).sum
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : OrderTop R<VAR>s : R<VAR>x : Multiset R<VAR>IH : trop x.inf = (map trop x).sum<GOAL>trop (s ::ₘ x).inf = (map trop (s ::ₘ x)).sum
<VAR>ι : Sort u_1<VAR>f g : ι → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>a - ⨅ i, f i = ⨆ i, a - f i
<VAR>ι : Sort u_1<VAR>f g : ι → ℝ≥0∞<VAR>a b c✝ d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>c : ℝ≥0∞<GOAL>a - ⨅ i, f i ≤ c ↔ ⨆ i, a - f i ≤ c
<VAR>ι : Sort u_1<VAR>f g : ι → ℝ≥0∞<VAR>a b c✝ d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>c : ℝ≥0∞<GOAL>a ≤ ⨅ i, f i + c ↔ ⨆ i, a - f i ≤ c
<VAR>α : Type u_1<VAR>inst✝ : Monoid α<VAR>a b : α<VAR>u : αˣ<VAR>x✝ : a ∣ b * ↑u<VAR>c : α<VAR>Eq : b * ↑u = a * c<GOAL>b = a * (c * ↑u⁻¹)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f p : R[X]<VAR>t : R<GOAL>(C t + p).reverse = C t * X ^ p.natDegree + p.reverse
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>M✝ N : Submodule R A<VAR>m n a : A<VAR>M : Submodule R A<GOAL>Set.up {a} • M = map (LinearMap.mulLeft R a) M
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>M✝ N : Submodule R A<VAR>m n a : A<VAR>M : Submodule R A<GOAL>Set.up {a} • span R ↑M = map (LinearMap.mulLeft R a) M
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>M✝ N : Submodule R A<VAR>m n a : A<VAR>M : Submodule R A<GOAL>span R ((fun x => a * x) '' ↑M) = map (LinearMap.mulLeft R a) M
<VAR>a✝ b✝ c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b : ℕ<GOAL>a ^ 2 - b ^ 2 = (a + b) * (a - b)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>s✝ s₁ s₂ t✝ t₁ t₂ : Finset α<VAR>a b : α<VAR>hr✝ hr : Symmetric r<VAR>s t : Finset α<GOAL>edgeDensity r s t = edgeDensity r t s
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.reverse.support = p.support.reverse
<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 : HasFDerivAt l l' (f x)<VAR>hf : HasDerivAt f f' x<VAR>hy : y = f x<GOAL>HasDerivAt (l ∘ f) (l' f') x
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q : R[X]<VAR>h : 0 = 1<VAR>p : R[X]<GOAL>p = 0
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>S : Set (HeightOneSpectrum R)<VAR>K : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>x✝ : K<GOAL>x✝ ∈ {x | ∀ v ∉ S, v.valuation x ≤ 1} ↔ x✝ ∈ ↑(⨅ v, ⨅ (_ : v ∉ S), v.valuation.valuationSubring.toSubring)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : AddGroup N<VAR>f f₁ f₂ g g₁ g₂ : α →₀ N<GOAL>(f₁ - g).neLocus (f₂ - g) = f₁.neLocus f₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ : S₁ ⟶ S₂<VAR>φ₂ : S₂ ⟶ S₃<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>h₃ : S₃.RightHomologyData<VAR>γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂<VAR>γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃<GOAL>opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = opcyclesMap' φ₁ h₁ h₂ ≫ opcyclesMap' φ₂ h₂ h₃
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrableOn f s μ<GOAL>∃ T, T.Countable ∧ (∀ u ∈ T, IsOpen u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrableOn f s μ<VAR>this : ∀ (x : ↑s), ∃ u, IsOpen u ∧ ↑x ∈ u ∧ IntegrableOn f (u ∩ s) μ<GOAL>∃ T, T.Countable ∧ (∀ u ∈ T, IsOpen u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ