ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₃<VAR>f g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x : E<VAR>x✝¹ : Set E × ℝ<VAR>s : Set E<VAR>r : ℝ<VAR>x✝ : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2<VAR>hs : IsVonNBounded 𝕜 (s, r).1<VAR>hr : 0 < (s, r).2<GOAL>∃ r_1 > 0, ContinuousLinearMap.seminorm.ball 0 r_1 ⊆ {f | ∀ x ∈ (s, r).1, f x ∈ closedBall 0 (s, r).2}
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝ : LinearOrder α<VAR>f : α → β<VAR>h : ∀ (x y : α), x < y → f x ≠ f y<VAR>x y : α<VAR>hf : f x = f y<GOAL>x = y
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝ : LinearOrder α<VAR>f : α → β<VAR>h : ∀ (x y : α), x < y → f x ≠ f y<VAR>x y : α<VAR>hf : f x = f y<VAR>hxy : x < y<GOAL>x = y
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝ : LinearOrder α<VAR>f : α → β<VAR>h : ∀ (x y : α), x < y → f x ≠ f y<VAR>x : α<VAR>hf : f x = f x<GOAL>x = x
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝ : LinearOrder α<VAR>f : α → β<VAR>h : ∀ (x y : α), x < y → f x ≠ f y<VAR>x y : α<VAR>hf : f x = f y<VAR>hxy : y < x<GOAL>x = y
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁵ : NontriviallyNormedField 𝕂<VAR>inst✝⁴ : NormedRing 𝔸<VAR>inst✝³ : NormedRing 𝔹<VAR>inst✝² : NormedAlgebra 𝕂 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔹<VAR>inst✝ : CompleteSpace 𝔸<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>HasSum (fun n => (↑n !)⁻¹ • x ^ n) (exp 𝕂 x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁵ : NontriviallyNormedField 𝕂<VAR>inst✝⁴ : NormedRing 𝔸<VAR>inst✝³ : NormedRing 𝔹<VAR>inst✝² : NormedAlgebra 𝕂 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔹<VAR>inst✝ : CompleteSpace 𝔸<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>HasSum (fun n => (expSeries 𝕂 𝔸 n) fun x_1 => x) (exp 𝕂 x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r : α → α → Prop<VAR>f g : Filter α<GOAL>IsBounded r ⊤ ↔ ∃ t, ∀ (x : α), r x t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : LinearOrderedSemifield β<VAR>s : Set ι<VAR>f f₁ f₂ : ι → α<VAR>g g₁ g₂ : ι → β<VAR>hg : ∀ i ∈ s, 0 < g i<VAR>i : ι<VAR>hi : i ∈ s<VAR>j : ι<VAR>hj : j ∈ s<GOAL>g⁻¹ j < g⁻¹ i → f i ≤ f j ↔ g i < g j → f i ≤ f j
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>i j : ℕ<VAR>a : ⨂[R]^i M<VAR>b : ⨂[R]^j M<GOAL>toTensorAlgebra (GradedMonoid.GMul.mul a b) = toTensorAlgebra a * toTensorAlgebra b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>i j : ℕ<VAR>a : ⨂[R]^i M<VAR>b : ⨂[R]^j M<GOAL>((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra) a) b = (((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra) a) b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>i j : ℕ<VAR>a : ⨂[R]^i M<VAR>b : ⨂[R]^j M<GOAL>((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra = (LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>i j : ℕ<VAR>a : Fin i → M<VAR>b : Fin j → M<GOAL>((((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra).compMultilinearMap (PiTensorProduct.tprod R)) a).compMultilinearMap (PiTensorProduct.tprod R)) b = (((((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra).compMultilinearMap (PiTensorProduct.tprod R)) a).compMultilinearMap (PiTensorProduct.tprod R)) b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>i j : ℕ<VAR>a : Fin i → M<VAR>b : Fin j → M<GOAL>((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra) ((PiTensorProduct.tprod R) a)) ((PiTensorProduct.tprod R) b) = (((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra) ((PiTensorProduct.tprod R) a)) ((PiTensorProduct.tprod R) b)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>i j : ℕ<VAR>a : Fin i → M<VAR>b : Fin j → M<GOAL>toTensorAlgebra (GradedMonoid.GMul.mul ((PiTensorProduct.tprod R) a) ((PiTensorProduct.tprod R) b)) = (((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra) ((PiTensorProduct.tprod R) a)) ((PiTensorProduct.tprod R) b)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>i j : ℕ<VAR>a : Fin i → M<VAR>b : Fin j → M<GOAL>(List.ofFn fun i_1 => (TensorAlgebra.ι R) (Fin.append a b i_1)).prod = (List.ofFn fun i => (TensorAlgebra.ι R) (a i)).prod * (List.ofFn fun i => (TensorAlgebra.ι R) (b i)).prod
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>i j : ℕ<VAR>a : Fin i → M<VAR>b : Fin j → M<GOAL>(List.ofFn fun i_1 => (TensorAlgebra.ι R) (Fin.append a b i_1)).prod = ((List.ofFn fun i => (TensorAlgebra.ι R) (a i)) ++ List.ofFn fun i => (TensorAlgebra.ι R) (b i)).prod
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>i j : ℕ<VAR>a : Fin i → M<VAR>b : Fin j → M<GOAL>(List.ofFn fun i_1 => (TensorAlgebra.ι R) (Fin.append a b i_1)) = (List.ofFn fun i => (TensorAlgebra.ι R) (a i)) ++ List.ofFn fun i => (TensorAlgebra.ι R) (b i)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>a : α<VAR>h𝒜 : ∀ s ∈ 𝒜, a ∉ s<VAR>s : Finset α<GOAL>s ∈ memberSubfamily a (image (insert a) 𝒜) ↔ s ∈ 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>a : α<VAR>h𝒜 : ∀ s ∈ 𝒜, a ∉ s<VAR>s : Finset α<GOAL>(∃ a_1 ∈ 𝒜, insert a a_1 = insert a s) ∧ a ∉ s ↔ s ∈ 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>a : α<VAR>h𝒜 : ∀ s ∈ 𝒜, a ∉ s<VAR>s : Finset α<VAR>hs : a ∉ s<VAR>t : Finset α<VAR>ht : t ∈ 𝒜<VAR>hts : insert a t = insert a s<GOAL>s ∈ 𝒜
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}<GOAL>o.blsub f = 0 ↔ o = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}<GOAL>IsEmpty (Quotient.out o).α ↔ o = 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<VAR>n : ℕ<GOAL>↑n ≤ o.card ↔ ↑n ≤ o
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>s✝ : Set α<VAR>a : α<VAR>inst✝¹ : Countable α<VAR>inst✝ : MeasurableSingletonClass α<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∑' (x : α), s.indicator (fun x => μ {x}) x = (sum fun a => μ {a} • dirac a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>s✝ : Set α<VAR>a : α<VAR>inst✝¹ : Countable α<VAR>inst✝ : MeasurableSingletonClass α<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(sum fun a => μ {a} • dirac a) s = μ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>g : β → α<VAR>hfg : LeftInverse g f<VAR>F : Filter α<GOAL>map g (map f F) = F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s✝ : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>s : Set (Set α)<VAR>U : Set α<GOAL>U ∈ generate s ↔ ∃ i, (i.Finite ∧ i ⊆ s) ∧ ⋂₀ i ⊆ U
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<GOAL>Tendsto (fun x => ⌈x⌉₊) atTop atTop
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>x : ℕ<GOAL>x ≤ ⌈↑x⌉₊
<VAR>x : ℂ<VAR>h : x ≠ 0<GOAL>0 ^ x = 0
<GOAL>ord ∘ aleph' = enumOrd {b | b.card.ord = b}
<GOAL>StrictMono (ord ∘ aleph') ∧ (∀ (a : Ordinal.{u_1}), (ord ∘ aleph') a ∈ {b | b.card.ord = b}) ∧ ∀ b ∈ {b | b.card.ord = b}, ∃ a, (ord ∘ aleph') a = b
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V₁<VAR>f : Dual K V₁<VAR>hf : f ≠ 0<GOAL>finrank K ↥(LinearMap.ker f) + 1 = finrank K V₁
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V₁<VAR>f : Dual K V₁<VAR>hf : f ≠ 0<GOAL>finrank K ↥(LinearMap.range f) = 1
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x₁ x₂ : α<VAR>r₁ r₂ : Ordnode α<VAR>H : Raised r₁.size r₂.size<GOAL>Raised (l.node' x₁ r₁).size (l.node' x₂ r₂).size
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x₁ x₂ : α<VAR>r₁ r₂ : Ordnode α<VAR>H : Raised r₁.size r₂.size<GOAL>Raised (l.size + r₁.size + 1) (l.size + r₂.size + 1)
<VAR>m n : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i j p : Fin n<VAR>a b : Fin (n + 1)<VAR>H : a ≤ b<VAR>ha : p.castSucc < a<VAR>hb : p.castSucc < b<GOAL>a.pred ⋯ ≤ b.pred ⋯
<VAR>m n : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i j p : Fin n<VAR>a b : Fin (n + 1)<VAR>H : a ≤ b<VAR>ha : p.castSucc < a<VAR>hb : ¬p.castSucc < b<GOAL>a.pred ⋯ ≤ b.castPred ⋯
<VAR>m n : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i j p : Fin n<VAR>a b : Fin (n + 1)<VAR>H : a ≤ b<VAR>ha : ¬p.castSucc < a<VAR>hb : p.castSucc < b<GOAL>a.castPred ⋯ ≤ b.pred ⋯
<VAR>m n : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i j p : Fin n<VAR>a b : Fin (n + 1)<VAR>H : a ≤ b<VAR>ha : ¬p.castSucc < a<VAR>hb : ¬p.castSucc < b<GOAL>a.castPred ⋯ ≤ b.castPred ⋯
<VAR>m n : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i j p : Fin n<VAR>a b : Fin (n + 1)<VAR>H : a ≤ b<VAR>ha : p.castSucc < a<VAR>hb : p.castSucc < b<GOAL>↑a - 1 ≤ ↑b - 1
<VAR>m n : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i j p : Fin n<VAR>a b : Fin (n + 1)<VAR>H : a ≤ b<VAR>ha : p.castSucc < a<VAR>hb : ¬p.castSucc < b<GOAL>↑a - 1 ≤ ↑(b.castPred ⋯)
<VAR>m n : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i j p : Fin n<VAR>a b : Fin (n + 1)<VAR>H : a ≤ b<VAR>ha : ¬p.castSucc < a<VAR>hb : p.castSucc < b<GOAL>↑(a.castPred ⋯) ≤ ↑b - 1
<VAR>m n : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i j p : Fin n<VAR>a b : Fin (n + 1)<VAR>H : a ≤ b<VAR>ha : ¬p.castSucc < a<VAR>hb : ¬p.castSucc < b<GOAL>↑(a.castPred ⋯) ≤ ↑(b.castPred ⋯)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>x : A<VAR>hx : IsIntegral R x<GOAL>Algebra.adjoin R {x} ≤ integralClosure R A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>x : A<VAR>hx : IsIntegral R x<GOAL>{x} ⊆ ↑(integralClosure R A)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>x : A<VAR>hx : IsIntegral R x<GOAL>x ∈ integralClosure R A
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A B : Finset (G × G)<VAR>a✝ b✝ c✝ d x y : G<VAR>n : ℕ<VAR>ε : ℝ<VAR>hs : IsCornerFree ↑A<VAR>a a' b b' c c' : G<VAR>ha : (a', b, c) ∈ Corners.triangleIndices A<VAR>hb : (a, b', c) ∈ Corners.triangleIndices A<VAR>hc : (a, b, c') ∈ Corners.triangleIndices A<GOAL>a = a' ∨ b = b' ∨ c = c'
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A B : Finset (G × G)<VAR>a✝ b✝ c✝ d x y : G<VAR>n : ℕ<VAR>ε : ℝ<VAR>hs : IsCornerFree ↑A<VAR>a a' b b' c c' : G<VAR>ha : (a', b) ∈ A ∧ c = a' + b<VAR>hb : (a, b') ∈ A ∧ c = a + b'<VAR>hc : (a, b) ∈ A ∧ c' = a + b<GOAL>a = a' ∨ b = b' ∨ c = c'
<VAR>G : Type u_1<VAR>inst✝ : AddMonoid G<VAR>a x✝ : G<GOAL>((fun c => Multiplicative.toAdd c +ᵥ AddConstMap.id) 1) x✝ = 1 x✝
<VAR>G : Type u_1<VAR>inst✝ : AddMonoid G<VAR>a : G<VAR>x✝² x✝¹ : Multiplicative G<VAR>x✝ : G<GOAL>({ toFun := fun c => Multiplicative.toAdd c +ᵥ AddConstMap.id, map_one' := ⋯ }.toFun (x✝² * x✝¹)) x✝ = ({ toFun := fun c => Multiplicative.toAdd c +ᵥ AddConstMap.id, map_one' := ⋯ }.toFun x✝² * { toFun := fun c => Multiplicative.toAdd c +ᵥ AddConstMap.id, map_one' := ⋯ }.toFun x✝¹) x✝
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>a b✝ : α<VAR>m n : ℕ<VAR>b : α<GOAL>a = 2 * b + 1 ↔ a = 2 * b + 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : CommRing S'<VAR>inst✝⁵ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝⁴ : Algebra R R'<VAR>inst✝³ : Algebra S S'<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : IsScalarTower R R' S'<VAR>inst✝ : IsScalarTower R S S'<VAR>f : P.Hom P'<VAR>x : S<VAR>y : P.Ring<GOAL>(CotangentSpace.map f) (x ⊗ₜ[P.Ring] (D R P.Ring) y) = (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom y)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : CommRing S'<VAR>inst✝⁵ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝⁴ : Algebra R R'<VAR>inst✝³ : Algebra S S'<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : IsScalarTower R R' S'<VAR>inst✝ : IsScalarTower R S S'<VAR>f : P.Hom P'<VAR>x : S<VAR>y : P.Ring<GOAL>x • 1 ⊗ₜ[P'.Ring] (D R' P'.Ring) ((algebraMap P.Ring P'.Ring) y) = (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom y)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : CommRing S'<VAR>inst✝⁵ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝⁴ : Algebra R R'<VAR>inst✝³ : Algebra S S'<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : IsScalarTower R R' S'<VAR>inst✝ : IsScalarTower R S S'<VAR>f : P.Hom P'<VAR>x : S<VAR>y : P.Ring<GOAL>(algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) ((algebraMap P.Ring P'.Ring) y) = (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : AddZeroClass δ<VAR>inst✝ : Min δ<VAR>C : Cost α β δ<VAR>y : β<VAR>ys : List β<GOAL>(List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩ ys).val.getLast ⋯ = (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩ ys).val[0]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : AddZeroClass δ<VAR>inst✝ : Min δ<VAR>C : Cost α β δ<VAR>y : β<VAR>ys : List β<GOAL>(List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩ ys).val.get ⟨(List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩ ys).val.length - 1, ⋯⟩ = (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩ ys).val[0]
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : Semiring R<VAR>x y : R<VAR>p : R[X]<GOAL>evalEval x y (C p) = eval x p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a✝ b✝ c✝ d a b c : G<GOAL>a / c * (b * c) = a * b
<VAR>M : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Bornology M<VAR>s₁ s₂ t₁ t₂ : Set E<VAR>inst✝¹ : AddZeroClass E<VAR>inst✝ : DistribSMul M E<VAR>h₁ : Absorbs M s₁ t₁<VAR>h₂ : Absorbs M s₂ t₂<VAR>x : M<VAR>hx₁ : t₁ ⊆ x • s₁<VAR>hx₂ : t₂ ⊆ x • s₂<GOAL>t₁ + t₂ ⊆ x • (s₁ + s₂)
<VAR>M : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Bornology M<VAR>s₁ s₂ t₁ t₂ : Set E<VAR>inst✝¹ : AddZeroClass E<VAR>inst✝ : DistribSMul M E<VAR>h₁ : Absorbs M s₁ t₁<VAR>h₂ : Absorbs M s₂ t₂<VAR>x : M<VAR>hx₁ : t₁ ⊆ x • s₁<VAR>hx₂ : t₂ ⊆ x • s₂<GOAL>t₁ + t₂ ⊆ x • s₁ + x • s₂
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>n : ℕ<VAR>h : p ≠ 0<VAR>hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t<VAR>hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R<GOAL>n < rootMultiplicity t p
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>n : ℕ<VAR>h : p ≠ 0<VAR>hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t<VAR>hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R<GOAL>↑n.factorial ∈ nonZeroDivisors R
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>init n x + tail n x = x
<VAR>a : ℂ<VAR>ha : a.re < -1<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>∫ (t : ℝ) in Ioi c, ↑t ^ a = -↑c ^ (a + 1) / (a + 1)
<VAR>a : ℂ<VAR>ha : a.re < -1<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>Tendsto (fun i => ∫ (x : ℝ) in c..id i, ↑x ^ a) atTop (𝓝 (-↑c ^ (a + 1) / (a + 1)))
<VAR>a : ℂ<VAR>ha : a.re < -1<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>Tendsto (fun x => (↑x ^ (a + 1) - ↑c ^ (a + 1)) / (a + 1)) atTop (𝓝 (-↑c ^ (a + 1) / (a + 1)))
<VAR>a : ℂ<VAR>ha : a.re < -1<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>Tendsto (fun x => ↑x ^ (a + 1) / (a + 1) - ↑c ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1) - ↑c ^ (a + 1) / (a + 1)))
<VAR>a : ℂ<VAR>ha : a.re < -1<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>Tendsto (fun x => ↑x ^ (a + 1)) atTop (𝓝 0)
<VAR>a : ℂ<VAR>ha : a.re < -1<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>Tendsto (fun x => ‖↑x ^ (a + 1)‖) atTop (𝓝 0)
<VAR>a : ℂ<VAR>ha : a.re < -1<VAR>c : ℝ<VAR>hc : 0 < c<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>x ^ (- -(a.re + 1)) = (fun x => ‖↑x ^ (a + 1)‖) x
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Submartingale f ℱ μ<GOAL>Supermartingale (-f) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Submartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>-μ[f j|↑ℱ i] ≤ᶠ[ae μ] (-f) i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Submartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>a✝¹ : Ω<VAR>a✝ : f i a✝¹ ≤ (μ[f j|↑ℱ i]) a✝¹<GOAL>(-μ[f j|↑ℱ i]) a✝¹ ≤ (-f) i a✝¹
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m✝ : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>m : δ → γ → ε<VAR>n : α → β → δ<VAR>m' : α → γ → δ'<VAR>n' : δ' → β → ε<VAR>h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b<GOAL>map₂ m (map₂ n f g) h = map₂ n' (map₂ m' f h) g
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m✝ : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>m : δ → γ → ε<VAR>n : α → β → δ<VAR>m' : α → γ → δ'<VAR>n' : δ' → β → ε<VAR>h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b<GOAL>map₂ m (map₂ (fun a b => n b a) g f) h = map₂ (fun a b => n' b a) g (map₂ m' f h)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>s : Set (Filter α)<VAR>l : Filter α<GOAL>l ∈ closure s ↔ ∀ t ∈ l, ∃ l' ∈ s, t ∈ l'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : E<GOAL>⟪x, x⟫_𝕜 = 0 ↔ x = 0
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Semiring S<VAR>I : Ideal R[X]<VAR>n : ℕ<VAR>x : R<GOAL>x ∈ I.leadingCoeffNth n ↔ ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Semiring S<VAR>I : Ideal R[X]<VAR>n : ℕ<VAR>x : R<GOAL>(∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x) ↔ ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>inst✝⁵ : CommRing Rₘ<VAR>inst✝⁴ : CommRing Sₘ<VAR>inst✝³ : Algebra R Rₘ<VAR>inst✝² : IsLocalization M Rₘ<VAR>inst✝¹ : Algebra S Sₘ<VAR>inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>p : Rₘ[X]<VAR>hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range<GOAL>p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff)) ∈ lifts (algebraMap R Rₘ)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>inst✝⁵ : CommRing Rₘ<VAR>inst✝⁴ : CommRing Sₘ<VAR>inst✝³ : Algebra R Rₘ<VAR>inst✝² : IsLocalization M Rₘ<VAR>inst✝¹ : Algebra S Sₘ<VAR>inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>p : Rₘ[X]<VAR>hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range<GOAL>∀ (n : ℕ), (p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))).coeff n ∈ Set.range ⇑(algebraMap R Rₘ)