ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>q₁ q₂ : Λ'<VAR>s : Option Γ'<VAR>c d : List Γ'<VAR>v : List ℕ<VAR>n : ℕ<GOAL>Reaches₁ (TM2.step tr) { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum (↑n).succ' ++ Γ'.cons :: trList v) [] c d } { l := some q₂, var := none, stk := elim ((match ↑n with | Num.zero => [] | Num.pos n => trPosNum n) ++ Γ'.cons :: trList v) [] c d }
<VAR>q₁ q₂ : Λ'<VAR>s : Option Γ'<VAR>c d : List Γ'<VAR>v : List ℕ<VAR>n : ℕ<VAR>a : PosNum<GOAL>Reaches₁ (TM2.step tr) { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) [] c d } { l := some q₂, var := none, stk := elim (trPosNum a ++ Γ'.cons :: trList v) [] c d }
<VAR>q₁ q₂ : Λ'<VAR>s : Option Γ'<VAR>c d : List Γ'<VAR>v : List ℕ<VAR>n : ℕ<VAR>a : PosNum<GOAL>∀ (l₁ : List Γ'), ∃ l₁' l₂' s', l₁.reverseAux (trPosNum a) = l₁'.reverseAux l₂' ∧ Reaches₁ (TM2.step tr) { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) l₁ c d } { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>c : Ordinal.{max u v}<VAR>hc : ℵ₀ < c.cof<VAR>hc' : Cardinal.lift.{v, u} #ι < c.cof<VAR>hf : ∀ (i : ι), ∀ b < c, f i b < c<VAR>a : Ordinal.{max u v}<VAR>ha : a < c<GOAL>nfpFamily f a < c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>c : Ordinal.{max u v}<VAR>hc : ℵ₀ < c.cof<VAR>hc' : Cardinal.lift.{v, u} #ι < c.cof<VAR>hf : ∀ (i : ι), ∀ b < c, f i b < c<VAR>a : Ordinal.{max u v}<VAR>ha : a < c<GOAL>Cardinal.lift.{v, u} (max ℵ₀ #ι) < c.cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>c : Ordinal.{max u v}<VAR>hc : ℵ₀ < c.cof<VAR>hc' : Cardinal.lift.{v, u} #ι < c.cof<VAR>hf : ∀ (i : ι), ∀ b < c, f i b < c<VAR>a : Ordinal.{max u v}<VAR>ha : a < c<VAR>l : List ι<GOAL>List.foldr f a l < c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>S T : WSeq (WSeq α)<VAR>s1 s2 : WSeq α<VAR>h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)<GOAL>Computation.LiftRel (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 => ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)) s1.destruct s2.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>S T : WSeq (WSeq α)<VAR>s1 s2 : WSeq α<VAR>h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)<GOAL>∀ {ca cb : Computation (Option (α × WSeq α))}, (fun c1 c2 => ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct) ca cb → LiftRelAux (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 => ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)) (fun c1 c2 => ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct) ca.destruct cb.destruct
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>x : Subobject X<GOAL>(map (𝟙 X)).obj x = x
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>f : MonoOver X<GOAL>(map (𝟙 X)).obj (Quotient.mk'' f) = Quotient.mk'' f
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>e : ι ≃ ι₂<VAR>e' : ι₂ ≃ ι₃<GOAL>reindex R s e ≪≫ₗ reindex R (fun i => s (e.symm i)) e' = reindex R s (e.trans e')
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>e : ι ≃ ι₂<VAR>e' : ι₂ ≃ ι₃<GOAL>↑(reindex R s e ≪≫ₗ reindex R (fun i => s (e.symm i)) e') = ↑(reindex R s (e.trans e'))
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>e : ι ≃ ι₂<VAR>e' : ι₂ ≃ ι₃<VAR>f : (i : ι) → s i<GOAL>((↑(reindex R s e ≪≫ₗ reindex R (fun i => s (e.symm i)) e')).compMultilinearMap (tprod R)) f = ((↑(reindex R s (e.trans e'))).compMultilinearMap (tprod R)) f
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>e : ι ≃ ι₂<VAR>e' : ι₂ ≃ ι₃<VAR>f : (i : ι) → s i<GOAL>((tprod R) fun i => f (e.symm (e'.symm i))) = ((domDomCongrLinearEquiv' R R s (⨂[R] (i : ι₃), s ((e.trans e').symm i)) (e.trans e')).symm (tprod R)) f
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a b c : Ordinal.{u}<VAR>h_init : x ≤ f x<VAR>h_ab : a < b<VAR>h_ac : a ≤ c<VAR>h_fab : lfpApprox f x a = lfpApprox f x b<GOAL>lfpApprox f x c ∈ fixedPoints ⇑f
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a b c : Ordinal.{u}<VAR>h_init : x ≤ f x<VAR>h_ab : a < b<VAR>h_ac : a ≤ c<VAR>h_fab : lfpApprox f x a = lfpApprox f x b<VAR>lfpApprox_mem_fixedPoint : lfpApprox f x a ∈ fixedPoints ⇑f<GOAL>lfpApprox f x c ∈ fixedPoints ⇑f
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a b c : Ordinal.{u}<VAR>h_init : x ≤ f x<VAR>h_ab : a < b<VAR>h_ac : a ≤ c<VAR>h_fab : lfpApprox f x a = lfpApprox f x b<VAR>lfpApprox_mem_fixedPoint : lfpApprox f x a ∈ fixedPoints ⇑f<GOAL>lfpApprox f x ?m.12494 ∈ fixedPoints ⇑f
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a b c : Ordinal.{u}<VAR>h_init : x ≤ f x<VAR>h_ab : a < b<VAR>h_ac : a ≤ c<VAR>h_fab : lfpApprox f x a = lfpApprox f x b<VAR>lfpApprox_mem_fixedPoint : lfpApprox f x a ∈ fixedPoints ⇑f<GOAL>?m.12494 ≤ c
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a b c : Ordinal.{u}<VAR>h_init : x ≤ f x<VAR>h_ab : a < b<VAR>h_ac : a ≤ c<VAR>h_fab : lfpApprox f x a = lfpApprox f x b<VAR>lfpApprox_mem_fixedPoint : lfpApprox f x a ∈ fixedPoints ⇑f<GOAL>Ordinal.{u}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Module A M<VAR>f : R<GOAL>Subsingleton (LocalizedModule (Submonoid.powers f) M) ↔ Disjoint (↑(PrimeSpectrum.basicOpen f)) (Module.support R M)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Module A M<VAR>f : R<GOAL>Module.support R M ⊆ PrimeSpectrum.zeroLocus {f} ↔ Module.support R M ≤ PrimeSpectrum.zeroLocus {f}
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝² : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : AddGroup G<VAR>x✝ : G<GOAL>(0 ⋆[L, μ] g) x✝ = 0 x✝
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type ?u.136040<VAR>inst✝¹ : MulAction R X<VAR>T : Type u_2<VAR>inst✝ : Monoid T<VAR>f : R →* T<VAR>fS : ↥S →* Tˣ<VAR>hf : ∀ (s : ↥S), f ↑s = ↑(fS s)<VAR>r : R<GOAL>(universalMulHom f fS hf) (numeratorHom r) = f r
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>p : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hp : ∀ (i : ι), a i = 0 ∨ 0 < p i<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-p i * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / p i ^ s.re<GOAL>HasSum (fun i => Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>p : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hp : ∀ (i : ι), a i = 0 ∨ 0 < p i<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-p i * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / p i ^ s.re<GOAL>HasSum (fun i => Complex.Gamma s * a i / ↑(p i) ^ s) (∫ (x : ℝ) in Ioi 0, ∑' (x_1 : ι), ↑x ^ (s - 1) * (a x_1 * ↑(rexp (-p x_1 * x))) ∂volume)
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>p : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hp : ∀ (i : ι), a i = 0 ∨ 0 < p i<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-p i * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / p i ^ s.re<VAR>i : ι<GOAL>Complex.Gamma s * a i / ↑(p i) ^ s = ∫ (a_1 : ℝ) in Ioi 0, ↑a_1 ^ (s - 1) * (a i * ↑(rexp (-p i * a_1))) ∂volume
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>p : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hp : ∀ (i : ι), a i = 0 ∨ 0 < p i<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-p i * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / p i ^ s.re<VAR>i : ι<GOAL>Integrable ((fun i t => ↑t ^ (s - 1) * (a i * ↑(rexp (-p i * t)))) i) (volume.restrict (Ioi 0))
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>p : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hp : ∀ (i : ι), a i = 0 ∨ 0 < p i<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-p i * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / p i ^ s.re<GOAL>Summable fun i => ∫ (a_1 : ℝ) in Ioi 0, ‖(fun i t => ↑t ^ (s - 1) * (a i * ↑(rexp (-p i * t)))) i a_1‖ ∂volume
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : LT α<VAR>a✝ b : α<VAR>a : WithTop α<GOAL>¬⊤ < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : LT α<VAR>a✝ b : α<VAR>a : WithTop α<GOAL>¬WithTop.toDual a < WithTop.toDual ⊤
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k1 k2 : ℤ<VAR>A : ↥GL(2, ℝ)⁺<VAR>f g : ℍ → ℂ<VAR>x : ℍ<GOAL>((f * g) ∣[k1 + k2] A) x = ((↑↑A).det • f ∣[k1] A * g ∣[k2] A) x
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k1 k2 : ℤ<VAR>A : ↥GL(2, ℝ)⁺<VAR>f g : ℍ → ℂ<VAR>x : ℍ<GOAL>f (A • x) * g (A • x) * ↑(↑↑A).det ^ (k1 + k2 - 1) * denom A x ^ (-(k1 + k2)) = ↑(↑↑A).det * (f (A • x) * ↑(↑↑A).det ^ (k1 - 1) * denom A x ^ (-k1)) * (g (A • x) * ↑(↑↑A).det ^ (k2 - 1) * denom A x ^ (-k2))
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k1 k2 : ℤ<VAR>A : ↥GL(2, ℝ)⁺<VAR>f g : ℍ → ℂ<VAR>x : ℍ<VAR>d : ℂ := ↑(↑↑A).det<GOAL>f (A • x) * g (A • x) * d ^ (k1 + k2 - 1) * denom A x ^ (-(k1 + k2)) = d * (f (A • x) * d ^ (k1 - 1) * denom A x ^ (-k1)) * (g (A • x) * d ^ (k2 - 1) * denom A x ^ (-k2))
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k1 k2 : ℤ<VAR>A : ↥GL(2, ℝ)⁺<VAR>f g : ℍ → ℂ<VAR>x : ℍ<VAR>d : ℂ := ↑(↑↑A).det<VAR>h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)<GOAL>f (A • x) * g (A • x) * d ^ (k1 + k2 - 1) * denom A x ^ (-(k1 + k2)) = d * (f (A • x) * d ^ (k1 - 1) * denom A x ^ (-k1)) * (g (A • x) * d ^ (k2 - 1) * denom A x ^ (-k2))
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k1 k2 : ℤ<VAR>A : ↥GL(2, ℝ)⁺<VAR>f g : ℍ → ℂ<VAR>x : ℍ<VAR>d : ℂ := ↑(↑↑A).det<VAR>h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)<VAR>h22 : denom A x ^ (-(k1 + k2)) = denom A x ^ (-k1) * denom A x ^ (-k2)<GOAL>f (A • x) * g (A • x) * d ^ (k1 + k2 - 1) * denom A x ^ (-(k1 + k2)) = d * (f (A • x) * d ^ (k1 - 1) * denom A x ^ (-k1)) * (g (A • x) * d ^ (k2 - 1) * denom A x ^ (-k2))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : Scheme<VAR>f : X.Hom Y<VAR>H : IsOpenImmersion f<GOAL>f ''ᵁ ⊤ = f.opensRange
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : Scheme<VAR>f : X.Hom Y<VAR>H : IsOpenImmersion f<GOAL>↑(f ''ᵁ ⊤) = ↑f.opensRange
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<VAR>this : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet<GOAL>cs.simple i * cs.simple i = 1
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<VAR>this✝ : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet<VAR>this : ↑(FreeGroup.of i * FreeGroup.of i) = 1<GOAL>cs.simple i * cs.simple i = 1
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<VAR>this✝ : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet<VAR>this : ↑(FreeGroup.of i * FreeGroup.of i) = 1<GOAL>cs.mulEquiv.symm (PresentedGroup.of i) * cs.mulEquiv.symm (PresentedGroup.of i) = 1
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : a * p.leadingCoeff ≠ 0<GOAL>(C a * p).natDegree = p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : a * p.leadingCoeff ≠ 0<GOAL>p.natDegree ∈ (C a * p).support
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : a * p.leadingCoeff ≠ 0<GOAL>(C a * p).coeff p.natDegree ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : CommMonoid α<VAR>inst✝⁴ : TopologicalSpace α<VAR>f✝ g✝ : β → α<VAR>a✝ b : α<VAR>s : Finset β<VAR>inst✝³ : CommMonoid γ<VAR>inst✝² : TopologicalSpace γ<VAR>G : Type u_5<VAR>inst✝¹ : FunLike G α γ<VAR>inst✝ : MonoidHomClass G α γ<VAR>g : G<VAR>hg : Inducing ⇑g<VAR>f : β → α<VAR>a : α<GOAL>HasProd (⇑g ∘ f) (g a) ↔ HasProd f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : CommMonoid α<VAR>inst✝⁴ : TopologicalSpace α<VAR>f✝ g✝ : β → α<VAR>a✝ b : α<VAR>s : Finset β<VAR>inst✝³ : CommMonoid γ<VAR>inst✝² : TopologicalSpace γ<VAR>G : Type u_5<VAR>inst✝¹ : FunLike G α γ<VAR>inst✝ : MonoidHomClass G α γ<VAR>g : G<VAR>hg : Inducing ⇑g<VAR>f : β → α<VAR>a : α<GOAL>Tendsto (fun s => g (∏ x ∈ s, f x)) atTop (𝓝 (g a)) ↔ Tendsto (fun s => ∏ x ∈ s, f x) atTop (𝓝 a)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(W.ΨSq n).natDegree ≤ n.natAbs ^ 2 - 1
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : CommSemiring S<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : Semiring B<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<GOAL>FiniteType R (FreeAlgebra R ι)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : CommSemiring S<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : Semiring B<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>val✝ : Fintype ι<GOAL>FiniteType R (FreeAlgebra R ι)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>f : X → ℝ<VAR>hf : 0 ≤ᶠ[ae (μ.restrict s)] f<VAR>hfi : IntegrableOn f s μ<GOAL>0 < ∫ (x : X) in s, f x ∂μ ↔ 0 < μ (support f ∩ s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>f : X → ℝ<VAR>hf : 0 ≤ᶠ[ae (μ.restrict s)] f<VAR>hfi : IntegrableOn f s μ<GOAL>NullMeasurableSet (support f) (μ.restrict s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>f : X → ℝ<VAR>hf : 0 ≤ᶠ[ae (μ.restrict s)] f<VAR>hfi : IntegrableOn f s μ<GOAL>NullMeasurableSet (f ⁻¹' {0}ᶜ) (μ.restrict s)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.64705, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>j : ℤ<VAR>A : C<VAR>f : (mappingCone φ).X j ⟶ A<VAR>i : ℤ<VAR>hij : j + 1 = i<GOAL>f = (↑(fst φ)).v j i hij ≫ (inl φ).v i j ⋯ ≫ f + (snd φ).v j j ⋯ ≫ (inr φ).f j ≫ f
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs' : s ≠ 1 ∨ a ≠ 0<GOAL>DifferentiableAt ℂ (cosZeta a) s
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs'✝ : s ≠ 1 ∨ a ≠ 0<VAR>hs' : s ≠ 1<GOAL>DifferentiableAt ℂ (cosZeta a) s
<VAR>a : UnitAddCircle<VAR>hs' : 1 ≠ 1 ∨ a ≠ 0<GOAL>DifferentiableAt ℂ (cosZeta a) 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α<VAR>h✝ : a ∈ s<VAR>n : ℕ<VAR>h : some a ∈ s.get? n<GOAL>∃ s', some (a, s') ∈ (s.drop n).destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α<VAR>h✝ : a ∈ s<VAR>n : ℕ<VAR>h : some a ∈ s.get? n<VAR>o : Option (α × WSeq α)<VAR>om : o ∈ (s.drop n).destruct<GOAL>∃ s', some (a, s') ∈ (s.drop n).destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α<VAR>h✝ : a ∈ s<VAR>n : ℕ<VAR>h : some a ∈ s.get? n<VAR>o : Option (α × WSeq α)<VAR>om : o ∈ (s.drop n).destruct<VAR>this : Prod.fst <$> o = some a<GOAL>∃ s', some (a, s') ∈ (s.drop n).destruct
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a✝)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a✝)) _auto✝<VAR>r : R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun a => eval a (C r)) a = (algebraMap R A) r
<VAR>m n : ℕ<GOAL>Even (n + 1) ↔ ¬Even n
<VAR>R✝ : Type u_1<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : IsDomain R✝<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<GOAL>cyclotomic' 0 R = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<GOAL>𝓤 α = comap (fun x => x.1 / x.2) (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<GOAL>comap ((fun x => x.2 / x.1) ∘ Prod.swap) (𝓝 1) = comap (fun x => x.1 / x.2) (𝓝 1)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<GOAL>s.length = Computation.map List.length s.toList
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<GOAL>Computation.IsBisimulation fun c1 c2 => ∃ l s, c1 = Computation.corec (fun x => match x with | (n, s) => match Seq.destruct s with | none => Sum.inl n | some (none, s') => Sum.inr (n, s') | some (some val, s') => Sum.inr (n + 1, s')) (l.length, s) ∧ c2 = Computation.map List.length (Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, s))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s✝ : WSeq α<VAR>s1 s2 : Computation ℕ<VAR>l : List α<VAR>s : WSeq α<VAR>h : s1 = Computation.corec (fun x => match x with | (n, s) => match Seq.destruct s with | none => Sum.inl n | some (none, s') => Sum.inr (n, s') | some (some val, s') => Sum.inr (n + 1, s')) (l.length, s) ∧ s2 = Computation.map List.length (Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, s))<GOAL>Computation.BisimO (fun c1 c2 => ∃ l s, c1 = Computation.corec (fun x => match x with | (n, s) => match Seq.destruct s with | none => Sum.inl n | some (none, s') => Sum.inr (n, s') | some (some val, s') => Sum.inr (n + 1, s')) (l.length, s) ∧ c2 = Computation.map List.length (Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, s))) s1.destruct s2.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s✝ : WSeq α<VAR>s1 s2 : Computation ℕ<VAR>l : List α<VAR>s : WSeq α<VAR>h : s1 = Computation.corec (fun x => match x with | (n, s) => match Seq.destruct s with | none => Sum.inl n | some (none, s') => Sum.inr (n, s') | some (some val, s') => Sum.inr (n + 1, s')) (l.length, s) ∧ s2 = Computation.map List.length (Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, s))<GOAL>Computation.BisimO (fun c1 c2 => ∃ l s, c1 = Computation.corec (fun x => match x with | (n, s) => match Seq.destruct s with | none => Sum.inl n | some (none, s') => Sum.inr (n, s') | some (some val, s') => Sum.inr (n + 1, s')) (l.length, s) ∧ c2 = Computation.map List.length (Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, s))) (Computation.corec (fun x => match x with | (n, s) => match Seq.destruct s with | none => Sum.inl n | some (none, s') => Sum.inr (n, s') | some (some val, s') => Sum.inr (n + 1, s')) (l.length, s)).destruct (Computation.map List.length (Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, s))).destruct
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (a : α), f a ∂count = ∑' (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>inst✝ : MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∑' (i : α), ∫⁻ (a : α), f a ∂dirac i = ∑' (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>inst✝ : MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>(fun i => ∫⁻ (a : α), f a ∂dirac i) = fun a => f a
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝² : (ofArrows X c.inj).hasPullbacks<VAR>inst✝¹ : HasInitial C<VAR>inst✝ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>hF' : Nonempty (PreservesLimit (Discrete.functor fun x => op (X x)) F)<VAR>x✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F := hF'.some<GOAL>IsSheafFor F (ofArrows X c.inj)