ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>l' : Filter β<VAR>f f' : ι → β → α<VAR>g g' : β → α<VAR>s : Set β<VAR>hf : UniformCauchySeqOn f l s<VAR>hf' : UniformCauchySeqOn f' l s<VAR>u : Set (α × α)<VAR>hu : u ∈ 𝓤 α<GOAL>∀ᶠ (m : ι × ι) in l ×ˢ l, ∀ x ∈ s, ((f / f') m.1 x, (f / f') m.2 x) ∈ u
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Finite ι<VAR>inst✝ : DecidableEq ι<VAR>e : M ≃ₗ[R] ι → R<VAR>i j : ι<GOAL>e ((ofEquivFun e) i) j = e (e.symm (update 0 i 1)) j
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>f : PiLp ⊤ β<GOAL>‖(WithLp.equiv ⊤ ((i : ι) → β i)) f‖₊ = ‖f‖₊
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>f : PiLp ⊤ β<GOAL>⨆ i, ‖(WithLp.equiv ⊤ ((i : ι) → β i)) f i‖₊ = ⨆ i, ‖f i‖₊
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q✝ r p q : R[X]<VAR>hp : p ≠ 0<VAR>hpq : p.degree < q.degree<VAR>hq : ¬q = 0<GOAL>p.natDegree < q.natDegree
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>inj : Function.Injective ⇑(algebraMap R B)<VAR>cl : ∀ {x : B}, IsIntegral R x ↔ ∃ y, (algebraMap R B) y = x<GOAL>IsIntegrallyClosedIn R A
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>inj : Function.Injective ⇑(algebraMap R B)<VAR>cl : ∀ {x : B}, IsIntegral R x ↔ ∃ y, (algebraMap R B) y = x<GOAL>Function.Injective (⇑f ∘ ⇑(algebraMap R A))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>inj : Function.Injective ⇑(algebraMap R B)<VAR>cl : ∀ {x : B}, IsIntegral R x ↔ ∃ y, (algebraMap R B) y = x<VAR>x✝ : A<VAR>hx : IsIntegral R x✝<GOAL>∃ y, (algebraMap R A) y = x✝
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>inj : Function.Injective ⇑(algebraMap R B)<VAR>cl : ∀ {x : B}, IsIntegral R x ↔ ∃ y, (algebraMap R B) y = x<VAR>x✝ : A<GOAL>(∃ y, (algebraMap R A) y = x✝) → IsIntegral R x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>i : Fin n<GOAL>Iio i.castSucc = map castSuccEmb (Iio i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>i : Fin n<GOAL>map valEmbedding (Iio i.castSucc) = map valEmbedding (map castSuccEmb (Iio i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>i : Fin n<GOAL>Iio ↑i.castSucc = map (castSuccEmb.trans valEmbedding) (Iio i)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<GOAL>M.Dep (insert e I) ↔ e ∈ M.closure I \ I
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<GOAL>e ∈ I → ¬M.Dep (insert e I)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>heI : e ∈ I<GOAL>¬M.Dep (insert e I)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>heI : e ∈ I<GOAL>¬M.Dep I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>c : Cardinal.{u_3}<GOAL>↑n ≤ toPartENat c ↔ ↑n ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : CommGroup α<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝ : CompleteSpace α<VAR>hf : Multipliable f<VAR>h : ∀ (b : β), g b = 1 ∨ g b = f b<GOAL>Multipliable g
<VAR>p : ℕ+<VAR>k✝ : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : NumberField K<VAR>k : ℕ+<VAR>hk : 1 < k<VAR>hζ : IsPrimitiveRoot ζ ↑k<GOAL>Nat.card (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) = ((Algebra.norm ℤ) (hζ.toInteger - 1)).natAbs
<VAR>p : ℕ+<VAR>k✝ : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : NumberField K<VAR>k : ℕ+<VAR>hk : 1 < k<VAR>hζ : IsPrimitiveRoot ζ ↑k<VAR>this : Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})<GOAL>Nat.card (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) = ((Algebra.norm ℤ) (hζ.toInteger - 1)).natAbs
<VAR>p : ℕ+<VAR>k✝ : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : NumberField K<VAR>k : ℕ+<VAR>hk : 1 < k<VAR>hζ : IsPrimitiveRoot ζ ↑k<VAR>this : Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})<VAR>x✝ : Fintype (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})<GOAL>Nat.card (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) = ((Algebra.norm ℤ) (hζ.toInteger - 1)).natAbs
<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✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>toDual (s.max' hs) = (image (⇑toDual) s).min' ⋯
<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✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>↑(toDual (s.max' hs)) = ↑((image (⇑toDual) s).min' ⋯)
<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✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>s.inf (WithTop.some ∘ fun x => toDual x) = s.inf ((WithTop.some ∘ fun x => x) ∘ ⇑toDual)
<VAR>i : (nim 1).LeftMoves<GOAL>toLeftMovesNim.symm i = ⟨0, ⋯⟩
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<GOAL>IsClosedMap f ↔ ∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J K L I : Ideal R<VAR>r : R<VAR>hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}<VAR>hri : r ∉ I.radical<VAR>hrm : r ∉ ⊤.radical<VAR>him : I ≤ ⊤<VAR>hm : ∀ z ∈ {K | r ∉ K.radical}, ⊤ ≤ z → z = ⊤<VAR>this : ∀ x ∉ ⊤, r ∈ (⊤ ⊔ span {x}).radical<GOAL>False
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J K L I : Ideal R<VAR>r : R<VAR>hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}<VAR>hri : r ∉ I.radical<VAR>hrm : r ∉ ⊤<VAR>him : I ≤ ⊤<VAR>hm : ∀ z ∈ {K | r ∉ K.radical}, ⊤ ≤ z → z = ⊤<VAR>this : ∀ x ∉ ⊤, r ∈ (⊤ ⊔ span {x}).radical<GOAL>False
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J K L I : Ideal R<VAR>r : R<VAR>hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}<VAR>hri : r ∉ I.radical<VAR>m : Ideal R<VAR>hrm : r ∉ m.radical<VAR>him : I ≤ m<VAR>hm : ∀ z ∈ {K | r ∉ K.radical}, m ≤ z → z = m<VAR>this : ∀ x ∉ m, r ∈ (m ⊔ span {x}).radical<VAR>x y : R<VAR>hxym : x * y ∈ m<VAR>hxm : x ∉ m<VAR>hym : y ∉ m<VAR>n : ℕ<VAR>hrn : r ^ n ∈ m ⊔ span {x}<VAR>p : R<VAR>hpm : p ∈ m<VAR>q : R<VAR>hq : q ∈ span {x}<VAR>hpqrn : p + q = r ^ n<VAR>c : R<VAR>hcxq : c * x = q<VAR>k : ℕ<VAR>hrk : r ^ k ∈ m ⊔ span {y}<VAR>f : R<VAR>hfm : f ∈ m<VAR>g : R<VAR>hg : g ∈ span {y}<VAR>hfgrk : f + g = r ^ k<VAR>d : R<VAR>hdyg : d * y = g<GOAL>r ^ (n + k) ∈ m
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J K L I : Ideal R<VAR>r : R<VAR>hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}<VAR>hri : r ∉ I.radical<VAR>m : Ideal R<VAR>hrm : r ∉ m.radical<VAR>him : I ≤ m<VAR>hm : ∀ z ∈ {K | r ∉ K.radical}, m ≤ z → z = m<VAR>this : ∀ x ∉ m, r ∈ (m ⊔ span {x}).radical<VAR>x y : R<VAR>hxym : x * y ∈ m<VAR>hxm : x ∉ m<VAR>hym : y ∉ m<VAR>n : ℕ<VAR>hrn : r ^ n ∈ m ⊔ span {x}<VAR>p : R<VAR>hpm : p ∈ m<VAR>q : R<VAR>hq : q ∈ span {x}<VAR>hpqrn : p + q = r ^ n<VAR>c : R<VAR>hcxq : c * x = q<VAR>k : ℕ<VAR>hrk : r ^ k ∈ m ⊔ span {y}<VAR>f : R<VAR>hfm : f ∈ m<VAR>g : R<VAR>hg : g ∈ span {y}<VAR>hfgrk : f + g = r ^ k<VAR>d : R<VAR>hdyg : d * y = g<GOAL>p * (f + d * y) + (c * x * f + c * d * (x * y)) ∈ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α ≃ Subtype p<VAR>g g₁ g₂ : Perm α<VAR>s t : Set α<VAR>h : LeftInvOn (⇑g₁) (⇑g₂) s<VAR>a : α<VAR>ha : a ∈ s<GOAL>(g₁.extendDomain f) ((g₂.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<GOAL>IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)<GOAL>IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)<VAR>x : CyclotomicField (p ^ k) ℚ<VAR>h : IsIntegral ℤ x<GOAL>x ∈ adjoin ℤ {b | b ^ ↑(p ^ k) = 1}
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)<VAR>x : CyclotomicField (p ^ k) ℚ<GOAL>(∃ y, (algebraMap (CyclotomicRing (p ^ k) ℤ ℚ) (CyclotomicField (p ^ k) ℚ)) y = x) → IsIntegral ℤ x
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : NormedGroup E<VAR>inst✝ : NormedGroup F<VAR>a b : E<GOAL>0 < ‖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>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : NormedGroup E<VAR>inst✝ : NormedGroup F<VAR>a b : E<GOAL>‖a / b‖ ≠ 0 ↔ a ≠ b
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>L' L₁' L₂' : LieSubalgebra R L<VAR>h : L₁'.toSubmodule = L₂'.toSubmodule<GOAL>L₁' = L₂'
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>L' L₁' L₂' : LieSubalgebra R L<VAR>h : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule<GOAL>L₁' = L₂'
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>L' L₁' L₂' : LieSubalgebra R L<VAR>h : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule<GOAL>↑L₁' = ↑L₂'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t u : Seq α<GOAL>(s.append t).append u = s.append (t.append u)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t u : Seq α<GOAL>IsBisimulation fun s1 s2 => ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t u : Seq α<GOAL>∃ s_1 t_1 u_1, (s.append t).append u = (s_1.append t_1).append u_1 ∧ s.append (t.append u) = s_1.append (t_1.append u_1)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : AddCommMonoid M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>x : M₃<GOAL>x ∈ range (f.coprod g) ↔ x ∈ range f ⊔ range g
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>h : S.HomologyData<VAR>inst✝ : S.HasHomology<GOAL>h.right.homologyIso = h.left.homologyIso ≪≫ h.iso
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>h : S.HomologyData<VAR>inst✝ : S.HasHomology<GOAL>h.iso = h.left.homologyIso.symm ≪≫ h.right.homologyIso
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>h : S.HomologyData<VAR>inst✝ : S.HasHomology<GOAL>h.iso.hom = h.left.homologyIso.inv ≫ h.right.homologyIso.hom
<VAR>x✝ y x : ℝ<VAR>hx : 0 < x<GOAL>sinh (log x) = (x - x⁻¹) / 2
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>h : 𝒜 ⊆ ℬ<VAR>x✝ : Finset α<GOAL>x✝ ∈ 𝒜.shatterer → x✝ ∈ ℬ.shatterer
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>a : R<GOAL>(monomial n) (-a) = -(monomial n) a
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>b c : ℝ<VAR>n : ℕ<VAR>hb : 0 ≠ b<GOAL>Tendsto (fun x => x ^ n / (b * rexp x + c)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>b c : ℝ<VAR>n : ℕ<VAR>hb : 0 ≠ b<VAR>H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)<GOAL>Tendsto (fun x => x ^ n / (b * rexp x + c)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>b c : ℝ<VAR>n : ℕ<VAR>hb : 0 ≠ b<VAR>H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)<VAR>h : 0 < b<GOAL>Tendsto (fun x => x ^ n / (b * rexp x + c)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>b c : ℝ<VAR>n : ℕ<VAR>hb : 0 ≠ b<VAR>H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)<VAR>h : 0 > b<GOAL>Tendsto (fun x => x ^ n / (b * rexp x + c)) atTop (𝓝 0)
<VAR>a b : ℕ+<GOAL>Fintype.card ↑(Set.Ico a b) = ↑b - ↑a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>a ≤ b⁻¹ ↔ b ≤ a⁻¹
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>X Y : C<VAR>inst✝ : Simple Y<VAR>f : X ⟶ Y<VAR>w : f ≠ 0<GOAL>cokernel.π f = 0
<VAR>a t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun n => rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t)
<VAR>a t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun x => ↑(rexp (-π * (↑x + a) ^ 2 * t))) (cexp (-↑π * ↑a ^ 2 * ↑t) * jacobiTheta₂ (↑a * I * ↑t) (I * ↑t))
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : ∀ (n : ℤ), ↑(rexp (-π * (↑n + a) ^ 2 * t)) = cexp (-↑π * ↑a ^ 2 * ↑t) * jacobiTheta₂_term n (↑a * I * ↑t) (I * ↑t)<GOAL>HasSum (fun x => ↑(rexp (-π * (↑x + a) ^ 2 * t))) (cexp (-↑π * ↑a ^ 2 * ↑t) * jacobiTheta₂ (↑a * I * ↑t) (I * ↑t))
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : ∀ (n : ℤ), ↑(rexp (-π * (↑n + a) ^ 2 * t)) = cexp (-↑π * ↑a ^ 2 * ↑t) * jacobiTheta₂_term n (↑a * I * ↑t) (I * ↑t)<GOAL>HasSum (fun x => cexp (-↑π * ↑a ^ 2 * ↑t) * jacobiTheta₂_term x (↑a * I * ↑t) (I * ↑t)) (cexp (-↑π * ↑a ^ 2 * ↑t) * jacobiTheta₂ (↑a * I * ↑t) (I * ↑t))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0∞<VAR>hr : r ≠ 0<VAR>hr_ne_top : r ≠ ⊤<GOAL>ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0∞<VAR>hr : r ≠ 0<VAR>hr_ne_top : r ≠ ⊤<VAR>h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ<GOAL>ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>inst✝² : Group α<VAR>inst✝¹ : LinearOrder α<VAR>a✝ b✝ : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>1 < mabs a ↔ a ≠ 1
<VAR>α : Type u_1<VAR>inst✝² : Group α<VAR>inst✝¹ : LinearOrder α<VAR>a✝ b✝ : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>ha : a < 1<GOAL>1 < mabs a ↔ a ≠ 1
<VAR>α : Type u_1<VAR>inst✝² : Group α<VAR>inst✝¹ : LinearOrder α<VAR>a b✝ : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>b c : α<GOAL>1 < mabs 1 ↔ 1 ≠ 1
<VAR>α : Type u_1<VAR>inst✝² : Group α<VAR>inst✝¹ : LinearOrder α<VAR>a✝ b✝ : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>ha : 1 < a<GOAL>1 < mabs a ↔ a ≠ 1
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁵ : UniformSpace α✝<VAR>inst✝⁴ : UniformSpace β<VAR>inst✝³ : UniformSpace γ<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : DiscreteTopology α<VAR>inst✝ : T0Space β<VAR>f : α → β<VAR>s : Set (β × β)<VAR>hs : s ∈ 𝓤 β<VAR>hf : Pairwise fun x y => (f x, f y) ∉ s<GOAL>ClosedEmbedding f
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : UniformSpace α✝<VAR>inst✝³ : UniformSpace β<VAR>inst✝² : UniformSpace γ<VAR>α : Type u_1<VAR>inst✝¹ : T0Space β<VAR>f : α → β<VAR>s : Set (β × β)<VAR>hs : s ∈ 𝓤 β<VAR>hf : Pairwise fun x y => (f x, f y) ∉ s<VAR>inst✝ : DiscreteTopology α<GOAL>ClosedEmbedding f
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : UniformSpace α✝<VAR>inst✝³ : UniformSpace β<VAR>inst✝² : UniformSpace γ<VAR>α : Type u_1<VAR>inst✝¹ : T0Space β<VAR>f : α → β<VAR>s : Set (β × β)<VAR>hs : s ∈ 𝓤 β<VAR>hf : Pairwise fun x y => (f x, f y) ∉ s<VAR>inst✝ : DiscreteTopology α<VAR>x✝ : UniformSpace α := ⊥<GOAL>ClosedEmbedding f
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>z x : ℂ<VAR>f : ℂ → ℂ<VAR>hx : x ∈ ball z R<VAR>hf : ContinuousOn f (sphere z R)<GOAL>∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>z x : ℂ<VAR>f : ℂ → ℂ<VAR>hx : x ∈ ball z R<VAR>hf : ContinuousOn f (sphere z R)<VAR>r : ℝ<VAR>hr : r < R<VAR>hrx : x ∈ ball z r<GOAL>∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>z x : ℂ<VAR>f : ℂ → ℂ<VAR>hx : x ∈ ball z R<VAR>hf : ContinuousOn f (sphere z R)<VAR>r : ℝ<VAR>hr : r < R<VAR>hrx : x ∈ ball z r<VAR>ε' : ℝ<VAR>hε' : ε' > 0<VAR>H : ball x ε' ⊆ ball z r<GOAL>∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>z x : ℂ<VAR>f : ℂ → ℂ<VAR>hx : x ∈ ball z R<VAR>hf : ContinuousOn f (sphere z R)<VAR>r : ℝ<VAR>hr : r < R<VAR>hrx : x ∈ ball z r<VAR>ε' : ℝ<VAR>hε' : ε' > 0<VAR>H : ball x ε' ⊆ ball z r<VAR>a : ℂ<VAR>b : ℝ<VAR>ha : (a, b).1 ∈ closedBall z r<VAR>hb : (a, b).2 ∈ [[0, 2 * π]]<VAR>hab : ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])), abs (circleTransformBoundingFunction R z ↑y) ≤ abs (circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩)<GOAL>∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>z x : ℂ<VAR>f : ℂ → ℂ<VAR>hx : x ∈ ball z R<VAR>hf : ContinuousOn f (sphere z R)<VAR>r : ℝ<VAR>hr : r < R<VAR>hrx : x ∈ ball z r<VAR>ε' : ℝ<VAR>hε' : ε' > 0<VAR>H : ball x ε' ⊆ ball z r<VAR>a : ℂ<VAR>b : ℝ<VAR>ha : (a, b).1 ∈ closedBall z r<VAR>hb : (a, b).2 ∈ [[0, 2 * π]]<VAR>hab : ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])), abs (circleTransformBoundingFunction R z ↑y) ≤ abs (circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩)<VAR>V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ<GOAL>∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>z x : ℂ<VAR>f : ℂ → ℂ<VAR>hx : x ∈ ball z R<VAR>hf : ContinuousOn f (sphere z R)<VAR>r : ℝ<VAR>hr : r < R<VAR>hrx : x ∈ ball z r<VAR>ε' : ℝ<VAR>hε' : ε' > 0<VAR>H : ball x ε' ⊆ ball z r<VAR>a : ℂ<VAR>b : ℝ<VAR>ha : (a, b).1 ∈ closedBall z r<VAR>hb : (a, b).2 ∈ [[0, 2 * π]]<VAR>hab : ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])), abs (circleTransformBoundingFunction R z ↑y) ≤ abs (circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩)<VAR>V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ<VAR>X : ℂ<VAR>HX2 : IsMaxOn (fun x => ‖f x‖) (sphere z R) X<GOAL>∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>z x : ℂ<VAR>f : ℂ → ℂ<VAR>hx : x ∈ ball z R<VAR>hf : ContinuousOn f (sphere z R)<VAR>r : ℝ<VAR>hr : r < R<VAR>hrx : x ∈ ball z r<VAR>ε' : ℝ<VAR>hε' : ε' > 0<VAR>H : ball x ε' ⊆ ball z r<VAR>a : ℂ<VAR>b : ℝ<VAR>ha : (a, b).1 ∈ closedBall z r<VAR>hb : (a, b).2 ∈ [[0, 2 * π]]<VAR>hab : ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])), abs (circleTransformBoundingFunction R z ↑y) ≤ abs (circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩)<VAR>V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ<VAR>X : ℂ<VAR>HX2 : IsMaxOn (fun x => ‖f x‖) (sphere z R) X<VAR>y : ℝ<VAR>v : ℂ<VAR>hv : v ∈ ball x ε'<GOAL>‖circleTransformDeriv R z v f y‖ ≤ abs (V b a) * abs (f X)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>z x : ℂ<VAR>f : ℂ → ℂ<VAR>hx : x ∈ ball z R<VAR>hf : ContinuousOn f (sphere z R)<VAR>r : ℝ<VAR>hr : r < R<VAR>hrx : x ∈ ball z r<VAR>ε' : ℝ<VAR>hε' : ε' > 0<VAR>H : ball x ε' ⊆ ball z r<VAR>a : ℂ<VAR>b : ℝ<VAR>ha : (a, b).1 ∈ closedBall z r<VAR>hb : (a, b).2 ∈ [[0, 2 * π]]<VAR>hab : ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])), abs (circleTransformBoundingFunction R z ↑y) ≤ abs (circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩)<VAR>V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ<VAR>X : ℂ<VAR>HX2 : IsMaxOn (fun x => ‖f x‖) (sphere z R) X<VAR>y : ℝ<VAR>v : ℂ<VAR>hv : v ∈ ball x ε'<VAR>y1 : ℝ<VAR>hy1 : y1 ∈ Ico 0 (2 * π)<VAR>hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1<GOAL>‖circleTransformDeriv R z v f y‖ ≤ abs (V b a) * abs (f X)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>z x : ℂ<VAR>f : ℂ → ℂ<VAR>hx : x ∈ ball z R<VAR>hf : ContinuousOn f (sphere z R)<VAR>r : ℝ<VAR>hr : r < R<VAR>hrx : x ∈ ball z r<VAR>ε' : ℝ<VAR>hε' : ε' > 0<VAR>H : ball x ε' ⊆ ball z r<VAR>a : ℂ<VAR>b : ℝ<VAR>ha : (a, b).1 ∈ closedBall z r<VAR>hb : (a, b).2 ∈ [[0, 2 * π]]<VAR>hab : ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])), abs (circleTransformBoundingFunction R z ↑y) ≤ abs (circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩)<VAR>V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ<VAR>X : ℂ<VAR>HX2 : IsMaxOn (fun x => ‖f x‖) (sphere z R) X<VAR>y : ℝ<VAR>v : ℂ<VAR>hv : v ∈ ball x ε'<VAR>y1 : ℝ<VAR>hy1 : y1 ∈ Ico 0 (2 * π)<VAR>hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1<VAR>hy2 : y1 ∈ [[0, 2 * π]]<GOAL>‖circleTransformDeriv R z v f y‖ ≤ abs (V b a) * abs (f X)