ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_5, u_1} C<VAR>inst✝² : Category.{?u.33373, u_2} D<VAR>inst✝¹ : Category.{?u.33377, u_3} E<VAR>P : Cᵒᵖ ⥤ Type u_4<VAR>X B : C<VAR>π : X ⟶ B<VAR>inst✝ : HasPullback π π<GOAL>P.map π.op ≫ P.map (pullback.fst π π).op = P.map π.op ≫ P.map (pullback.snd π π).op
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H : ∃ l' r', BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')<GOAL>Valid' o₁ (l.balance x r) o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H : ∃ l' r', BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')<GOAL>Valid' o₁ (l.balance' x r) o₂
<VAR>x y : EReal<VAR>h : x ≤ y<VAR>hx : x ≠ ⊥<VAR>hy : y ≠ ⊤<GOAL>x.toReal ≤ y.toReal
<VAR>y : EReal<VAR>hy : y ≠ ⊤<VAR>x : ℝ<VAR>h : ↑x ≤ y<VAR>hx : ↑x ≠ ⊥<GOAL>(↑x).toReal ≤ y.toReal
<VAR>x : ℝ<VAR>hx : ↑x ≠ ⊥<VAR>y : ℝ<VAR>hy : ↑y ≠ ⊤<VAR>h : ↑x ≤ ↑y<GOAL>(↑x).toReal ≤ (↑y).toReal
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>N : Submodule R M<VAR>I : IsNoetherianRing R<VAR>hN : N.FG<VAR>s : Finset M<VAR>hs : span R ↑s = N<VAR>this✝ : DecidableEq M<VAR>this : DecidableEq R<GOAL>IsNoetherian R ↥N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>N : Submodule R M<VAR>I : IsNoetherianRing R<VAR>hN : N.FG<VAR>s : Finset M<VAR>hs : span R ↑s = N<VAR>this✝¹ : DecidableEq M<VAR>this✝ : DecidableEq R<VAR>this : ∀ x ∈ s, x ∈ N<GOAL>IsNoetherian R ↥N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>N : Submodule R M<VAR>I : IsNoetherianRing R<VAR>hN : N.FG<VAR>s : Finset M<VAR>hs : span R ↑s = N<VAR>this✝¹ : DecidableEq M<VAR>this✝ : DecidableEq R<VAR>this : ∀ x ∈ s, x ∈ N<GOAL>(↑↑s → R) →ₗ[R] ↥N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>N : Submodule R M<VAR>I : IsNoetherianRing R<VAR>hN : N.FG<VAR>s : Finset M<VAR>hs : span R ↑s = N<VAR>this✝¹ : DecidableEq M<VAR>this✝ : DecidableEq R<VAR>this : ∀ x ∈ s, x ∈ N<GOAL>LinearMap.range ?refine_1 = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>s₁ s₂ : Finset α<VAR>t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>x : α ⊕ β<GOAL>s.disjSum t = ∅ ↔ s = ∅ ∧ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ x : Fin n → ℕ<VAR>hx : x ∈ sphere n d k<GOAL>‖(WithLp.equiv 2 (Fin n → ℝ)).symm (Nat.cast ∘ x)‖ = √↑k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ x : Fin n → ℕ<VAR>hx : x ∈ sphere n d k<GOAL>√(∑ i : Fin n, ‖(WithLp.equiv 2 (Fin n → ℝ)).symm (Nat.cast ∘ x) i‖ ^ 2) = √↑k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ x : Fin n → ℕ<VAR>hx : x ∈ sphere n d k<GOAL>√(∑ i : Fin n, |↑(x i)| ^ 2) = √↑k
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>inst✝ : Algebra R S<VAR>hI : I.IsPrime<VAR>hIJ : I ≤ J<VAR>x : S<VAR>mem : x ∈ ↑J \ ↑I<VAR>p : R[X]<VAR>p_monic : p.Monic<VAR>hpx : eval₂ (algebraMap R S) x p = 0<GOAL>comap (algebraMap R S) I < comap (algebraMap R S) J
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>inst✝ : Algebra R S<VAR>hI : I.IsPrime<VAR>hIJ : I ≤ J<VAR>x : S<VAR>mem : x ∈ ↑J \ ↑I<VAR>p : R[X]<VAR>p_monic : p.Monic<VAR>hpx : eval₂ (algebraMap R S) x p = 0<GOAL>eval₂ (algebraMap R S) x p ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f : Perm α<GOAL>(∀ (x : α), p (f⁻¹ x) ↔ p (f (f⁻¹ x))) ↔ ∀ (x : α), p x ↔ p (f⁻¹ x)
<VAR>z✝ w : ℍ<VAR>r✝ R : ℝ<VAR>z : ℍ<VAR>r : ℝ<GOAL>dist ↑z ↑(z.center r) = z.im * (Real.cosh r - 1)
<VAR>z✝ w : ℍ<VAR>r✝ R : ℝ<VAR>z : ℍ<VAR>r : ℝ<GOAL>|(↑(z.center r)).im - (↑z).im| = z.im * Real.cosh r - z.im
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>inst✝ : R.hasPullbacks<VAR>x : FirstObj P R<GOAL>((firstObjEqFamily P R).hom x).Compatible ↔ firstMap P R x = secondMap P R x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>inst✝ : R.hasPullbacks<VAR>x : FirstObj P R<GOAL>((firstObjEqFamily P R).hom x).PullbackCompatible ↔ firstMap P R x = secondMap P R x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>L : List R[X]<VAR>hd : R[X]<VAR>tl : List R[X]<VAR>ih : 0 ∉ tl → tl.prod.roots = (↑tl).bind roots<VAR>H : 0 ∉ hd :: tl<GOAL>(hd :: tl).prod.roots = (↑(hd :: tl)).bind roots
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>L : List R[X]<VAR>hd : R[X]<VAR>tl : List R[X]<VAR>ih : 0 ∉ tl → tl.prod.roots = (↑tl).bind roots<VAR>H : ¬0 = hd ∧ 0 ∉ tl<GOAL>(hd :: tl).prod.roots = (↑(hd :: tl)).bind roots
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>map valEmbedding (Iic b) = Iic ↑b
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v✝ : E<VAR>v : ↑(sphere 0 1)<GOAL>↑(stereographic ⋯) v = 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v✝ : E<VAR>v : ↑(sphere 0 1)<GOAL>v = - -v
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝¹ : MulZeroOneClass M₀<VAR>s t : Set ι<VAR>i : ι<VAR>inst✝ : Nontrivial M₀<VAR>h : s.indicator 1 = t.indicator 1<VAR>x✝ : ι<GOAL>x✝ ∈ s ↔ x✝ ∈ t
<VAR>α β ι : Type u<VAR>f : ι → Cardinal.{v}<VAR>a : ι<GOAL>Nonempty (Quotient.out (f a) ≃ Quotient.out ((fun i => lift.{w, v} (f i)) a))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<GOAL>upcrossingStrat a b f N n ω ≤ 1
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<GOAL>(⋃ i ∈ Finset.range N, Set.Ico (lowerCrossingTime a b f N i ω) (upperCrossingTime a b f N (i + 1) ω)).indicator 1 n ≤ 1
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<GOAL>(↑(Finset.range N)).PairwiseDisjoint fun k => Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>i : ℕ<VAR>a✝¹ : i ∈ ↑(Finset.range N)<VAR>j : ℕ<VAR>a✝ : j ∈ ↑(Finset.range N)<VAR>hij : i ≠ j<GOAL>(Disjoint on fun k => Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)) i j
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>i : ℕ<VAR>a✝¹ : i ∈ ↑(Finset.range N)<VAR>j : ℕ<VAR>a✝ : j ∈ ↑(Finset.range N)<VAR>hij : i ≠ j<GOAL>min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤ max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>i : ℕ<VAR>a✝¹ : i ∈ ↑(Finset.range N)<VAR>j : ℕ<VAR>a✝ : j ∈ ↑(Finset.range N)<VAR>hij : i ≠ j<VAR>hij' : i < j<GOAL>min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤ max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>i : ℕ<VAR>a✝¹ : i ∈ ↑(Finset.range N)<VAR>j : ℕ<VAR>a✝ : j ∈ ↑(Finset.range N)<VAR>hij : i ≠ j<VAR>hij' : i > j<GOAL>min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤ max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>s t : SummableFamily Γ R α<VAR>g : Γ<GOAL>(s + t).hsum.coeff g = (s.hsum + t.hsum).coeff g
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>s t : SummableFamily Γ R α<VAR>g : Γ<GOAL>∑ᶠ (i : α), ((s i).coeff g + (t i).coeff g) = ∑ᶠ (i : α), (s i).coeff g + ∑ᶠ (i : α), (t i).coeff g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f : β → α<VAR>inst✝ : DecidableEq β<GOAL>(∅ ∪ s₂).lcm f = GCDMonoid.lcm (∅.lcm f) (s₂.lcm f)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>s✝ s₁ s₂ : Finset β<VAR>f : β → α<VAR>inst✝ : DecidableEq β<VAR>a : β<VAR>s : Finset β<VAR>x✝ : a ∉ s<VAR>ih : (s ∪ s₂).lcm f = GCDMonoid.lcm (s.lcm f) (s₂.lcm f)<GOAL>(insert a s ∪ s₂).lcm f = GCDMonoid.lcm ((insert a s).lcm f) (s₂.lcm f)
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommMonoid (β i)<VAR>M : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : SetLike S M<VAR>inst✝² : AddSubmonoidClass S M<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq M<VAR>A : ι → S<VAR>x : ⨁ (i : ι), ↥(A i)<VAR>m : ι<GOAL>(m ∈ support fun i => ↑(x i)) → m ∈ ↑(DFinsupp.support x)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R N<VAR>Q✝ : QuadraticMap R M N<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : Algebra S R<VAR>inst✝⁴ : Module S M<VAR>inst✝³ : IsScalarTower S R M<VAR>inst✝² : Module S N<VAR>inst✝¹ : IsScalarTower S R N<VAR>ι : Type u_8<VAR>inst✝ : DecidableEq ι<VAR>Q : QuadraticMap R M N<VAR>s : Finset ι<VAR>f : ι → M<GOAL>Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ Finset.filter (fun x => ¬x.IsDiag) s.sym2, Sym2.lift ⟨fun i j => polar (⇑Q) (f i) (f j), ⋯⟩ ij
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>C : TensorAlgebra R M → Prop<VAR>algebraMap : ∀ (r : R), C ((_root_.algebraMap R (TensorAlgebra R M)) r)<VAR>ι : ∀ (x : M), C ((TensorAlgebra.ι R) x)<VAR>mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)<VAR>add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)<VAR>a : TensorAlgebra R M<VAR>s : Subalgebra R (TensorAlgebra R M) := { carrier := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }<VAR>h : AddCommMonoid ↥s := inferInstanceAs (AddCommMonoid ↥(Subalgebra.toSubmodule s))<VAR>of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι<GOAL>C a
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>C : TensorAlgebra R M → Prop<VAR>algebraMap : ∀ (r : R), C ((_root_.algebraMap R (TensorAlgebra R M)) r)<VAR>ι : ∀ (x : M), C ((TensorAlgebra.ι R) x)<VAR>mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)<VAR>add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)<VAR>a : TensorAlgebra R M<VAR>s : Subalgebra R (TensorAlgebra R M) := { carrier := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }<VAR>h : AddCommMonoid ↥s := inferInstanceAs (AddCommMonoid ↥(Subalgebra.toSubmodule s))<VAR>of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι<VAR>of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp ((lift R) of)<GOAL>C a
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>C : TensorAlgebra R M → Prop<VAR>algebraMap : ∀ (r : R), C ((_root_.algebraMap R (TensorAlgebra R M)) r)<VAR>ι : ∀ (x : M), C ((TensorAlgebra.ι R) x)<VAR>mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)<VAR>add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)<VAR>a : TensorAlgebra R M<VAR>s : Subalgebra R (TensorAlgebra R M) := { carrier := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }<VAR>h : AddCommMonoid ↥s := inferInstanceAs (AddCommMonoid ↥(Subalgebra.toSubmodule s))<VAR>of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι<VAR>of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp ((lift R) of)<GOAL>C ((s.val.comp ((lift R) of)) a)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>x y z : α<VAR>h : ¬IsBounded s<GOAL>diam s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁵ : Zero α<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : SMulWithZero α β<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : SMulPosMono α β<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b₁<GOAL>0 ≤ a • b₁
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Bool<VAR>xs : List α<VAR>i : ℕ<VAR>h : i < xs.length<VAR>h2 : ∀ (j : ℕ) (hji : j < i), ¬p (xs.get ⟨j, ⋯⟩) = true<GOAL>i ≤ findIdx p xs
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Bool<VAR>xs : List α<VAR>i : ℕ<VAR>h : i < xs.length<VAR>h2 : ∀ (j : ℕ) (hji : j < i), ¬p (xs.get ⟨j, ⋯⟩) = true<VAR>f : findIdx p xs < i<GOAL>False
<VAR>z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im = 0<GOAL>ContinuousWithinAt log {z | 0 ≤ z.im} z
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S S' S'' : D<VAR>Y Y' Y'' : C<VAR>T T' : C ⥤ D<VAR>f : StructuredArrow S T<VAR>g : f.right ⟶ Y'<VAR>g' : Y' ⟶ Y''<GOAL>(f.homMk' (g ≫ g')).right = (f.homMk' g ≫ (mk (f.hom ≫ T.map g)).homMk' g' ≫ eqToHom ⋯).right
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<GOAL>↑⊥ = {0}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<GOAL>⨆ g, ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ = ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<GOAL>⨆ g, ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α), f a ∂μ ≤ ⨆ g, ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>p✝ : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<GOAL>AddGroupFilterBasis.toFilterBasis.filter = ⨅ i, comap (⇑(p i)) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>p✝ : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>i : ι<GOAL>AddGroupFilterBasis.toFilterBasis.filter ≤ comap (⇑(p i)) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>p✝ : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<GOAL>⨅ i, comap (⇑(p i)) (𝓝 0) ≤ AddGroupFilterBasis.toFilterBasis.filter
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<GOAL>∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<GOAL>∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, a ∈ s → ∃ b ≥ i, f^[b] a ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<VAR>n : ℕ<GOAL>∀ᵐ (a : α) ∂μ, a ∈ s → ∃ b ≥ n, f^[b] a ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<VAR>n : ℕ<GOAL>∀ (a : α), ¬(a ∈ s ∧ ∀ m ≥ n, f^[m] a ∉ s) → a ∈ s → ∃ b ≥ n, f^[b] a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : AddMonoidWithOne B<VAR>inst✝² : FunLike F ℕ A<VAR>inst✝¹ : AddMonoidWithOne A<VAR>inst✝ : AddMonoidHomClass F ℕ A<VAR>f : F<VAR>h1 : f 1 = 1<GOAL>f 0 = ↑0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : AddMonoidWithOne B<VAR>inst✝² : FunLike F ℕ A<VAR>inst✝¹ : AddMonoidWithOne A<VAR>inst✝ : AddMonoidHomClass F ℕ A<VAR>f : F<VAR>h1 : f 1 = 1<VAR>n : ℕ<GOAL>f (n + 1) = ↑(n + 1)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasShift C ℤ<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>a b : ℤ<GOAL>CategoryTheory.shiftFunctorAdd' (Triangle C) a b (a + b) ⋯ = shiftFunctorAdd' C a b (a + b) ⋯
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasShift C ℤ<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>a b : ℤ<GOAL>shiftFunctorAdd (Triangle C) a b = shiftFunctorAdd' C a b (a + b) ⋯
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this : Inhabited I<VAR>h : Products.eval (C' C ho) (↑l).Tail ∈ Submodule.span ℤ (Products.eval (C' C ho) '' {m | m < (↑l).Tail})<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this : Inhabited I<VAR>h : ∃ l_1 ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}, (Finsupp.total (Products I) (LocallyConstant ↑(C' C ho) ℤ) ℤ (Products.eval (C' C ho))) l_1 = (Linear_CC' C hsC ho) (Products.eval C ↑l)<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this : Inhabited I<VAR>m : Products I →₀ ℤ<VAR>hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}<VAR>hmsum : (Finsupp.total (Products I) (LocallyConstant ↑(C' C ho) ℤ) ℤ (Products.eval (C' C ho))) m = (Linear_CC' C hsC ho) (Products.eval C ↑l)<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this : Inhabited I<VAR>m : Products I →₀ ℤ<VAR>hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}<VAR>hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this✝ : Inhabited I<VAR>m : Products I →₀ ℤ<VAR>hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}<VAR>hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)<VAR>this : (Linear_CC' C hsC ho) (Products.eval C ↑l) = (Linear_CC' C hsC ho) (m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod)<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this✝ : Inhabited I<VAR>m : Products I →₀ ℤ<VAR>hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}<VAR>hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)<VAR>this : (Linear_CC' C hsC ho) (Products.eval C ↑l) = (Linear_CC' C hsC ho) (m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod)<VAR>hse : (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).Exact<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this✝ : Inhabited I<VAR>m : Products I →₀ ℤ<VAR>hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}<VAR>hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)<VAR>this : (Linear_CC' C hsC ho) (Products.eval C ↑l) = (Linear_CC' C hsC ho) (m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod)<VAR>hse : LinearMap.range (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).f = LinearMap.ker (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).g<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this✝ : Inhabited I<VAR>m : Products I →₀ ℤ<VAR>hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}<VAR>hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)<VAR>this : (Linear_CC' C hsC ho) (Products.eval C ↑l) = (Linear_CC' C hsC ho) (m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod)<VAR>hse : LinearMap.range (πs C o) = LinearMap.ker (Linear_CC' C hsC ho)<GOAL>False