ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>M : Type u_5<VAR>inst✝ : CommMonoidWithZero M<VAR>S : Finset α<VAR>p : M<VAR>pp : Prime p<VAR>g : α → M<VAR>hS : ∀ a ∈ S, ¬p ∣ g a<GOAL>¬p ∣ S.prod g
<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<GOAL>LinearIndependent ℤ (eval C) ↔ LinearIndependent ℤ (SumEval C ho)
<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<GOAL>LinearIndependent ℤ (eval C ∘ ⇑(sum_equiv C hsC ho)) ↔ LinearIndependent ℤ (eval C ∘ (sum_equiv C hsC ho).toFun)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a : α i<GOAL>update f i '' Ioo a (f i) = Ioo (update f i a) f
<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>f : ι → α<VAR>a : α<GOAL>a ≤ s.sup' H f ↔ ∃ b ∈ s, a ≤ f b
<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>f : ι → α<VAR>a : α<GOAL>(∃ b ∈ s, ↑a ≤ (WithBot.some ∘ f) b) ↔ ∃ b ∈ s, a ≤ f b
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ✝ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>k : ℕ<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hpri : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)<VAR>h : p ≠ 2<GOAL>(Algebra.norm K) (ζ - 1) = ↑↑p
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X X' : C<VAR>φ : X ≅ X'<VAR>p : X ⟶ X<VAR>p' : X' ⟶ X'<VAR>hpp' : p ≫ φ.hom = φ.hom ≫ p'<VAR>Y : C<VAR>i : Y ⟶ X<VAR>e : X ⟶ Y<VAR>h₁ : i ≫ e = 𝟙 Y<VAR>h₂ : e ≫ i = p<GOAL>∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X X' : C<VAR>φ : X ≅ X'<VAR>p : X ⟶ X<VAR>p' : X' ⟶ X'<VAR>hpp' : p ≫ φ.hom = φ.hom ≫ p'<VAR>Y : C<VAR>i : Y ⟶ X<VAR>e : X ⟶ Y<VAR>h₁ : i ≫ e = 𝟙 Y<VAR>h₂ : e ≫ i = p<GOAL>(i ≫ φ.hom) ≫ φ.inv ≫ e = 𝟙 Y ∧ (φ.inv ≫ e) ≫ i ≫ φ.hom = p'
<VAR>a b c : EReal<VAR>h : b > 0<VAR>h' : b ≠ ⊤<GOAL>a ≤ c / b ↔ a * b ≤ c
<VAR>a b c : EReal<VAR>h : b > 0<VAR>h' : b ≠ ⊤<GOAL>b * (a / b) ≤ c / b ↔ a * b ≤ c
<VAR>a b c : EReal<VAR>h : b > 0<VAR>h' : b ≠ ⊤<GOAL>b * a / b ≤ c / b ↔ b * a ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>h : a < b<GOAL>Ico a b \ Ioo a b = {a}
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b c d : α<GOAL>Icc a b * Ico c d ⊆ Ico (a * c) (b * d)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b c d : α<VAR>this : ∀ (M : Type ?u.3042) (N : Type ?u.3041) (μ : M → N → N) [inst : PartialOrder N] [inst_1 : CovariantClass M N μ fun x x_1 => x < x_1], CovariantClass M N μ fun x x_1 => x ≤ x_1<GOAL>Icc a b * Ico c d ⊆ Ico (a * c) (b * d)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b c d : α<VAR>this : ∀ (M : Type ?u.3042) (N : Type ?u.3041) (μ : M → N → N) [inst : PartialOrder N] [inst_1 : CovariantClass M N μ fun x x_1 => x < x_1], CovariantClass M N μ fun x x_1 => x ≤ x_1<VAR>y : α<VAR>hya : a ≤ y<VAR>hyb : y ≤ b<VAR>z : α<VAR>hzc : c ≤ z<VAR>hzd : z < d<GOAL>(fun x x_1 => x * x_1) y z ∈ Ico (a * c) (b * d)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<GOAL>coborder s ∩ closure s = s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<GOAL>s ⊆ closure s
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>c : F<VAR>m x✝ : E<GOAL>(fderiv 𝕜 (fun x => c) m) x✝ = (0 m) x✝
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>c : F<VAR>m x✝ : E<GOAL>0 x✝ = (0 m) x✝
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<GOAL>IsCofiltered C ↔ ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<GOAL>(∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)) ↔ ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))
<VAR>α✝ : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>inst✝¹ : LinearOrder α✝<VAR>s✝ : Set α✝<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Nonempty ι<VAR>f : ι → Set α<VAR>h : Directed (fun x x_1 => x ⊆ x_1) f<VAR>s : Finset α<VAR>hs : ↑s ⊆ ⋃ i, f i<GOAL>∃ i, ↑s ⊆ f i
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s : Set α<VAR>hs : Dense s<GOAL>IsSeparable s ↔ SeparableSpace α
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>S : Submonoid α<VAR>disjoint : Disjoint ↑⊤ ↑S<VAR>maximally_disjoint : ∀ (J : Ideal α), ⊤ < J → ¬Disjoint ↑J ↑S<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>S : Submonoid α<VAR>disjoint : Disjoint ↑⊤ ↑S<VAR>maximally_disjoint : ∀ (J : Ideal α), ⊤ < J → ¬Disjoint ↑J ↑S<VAR>this : 1 ∈ ↑S<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>S : Submonoid α<VAR>disjoint : Disjoint ↑I ↑S<VAR>maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S<VAR>x y : α<VAR>hxy : x * y ∈ I<GOAL>x ∈ I ∨ y ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>S : Submonoid α<VAR>disjoint : Disjoint ↑I ↑S<VAR>maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S<VAR>x y : α<VAR>hxy : x * y ∈ I<VAR>rid : x ∉ I ∧ y ∉ I<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>S : Submonoid α<VAR>disjoint : Disjoint ↑I ↑S<VAR>maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S<VAR>x y : α<VAR>hxy : x * y ∈ I<VAR>rid : x ∉ I ∧ y ∉ I<VAR>hx : ¬Disjoint ↑(I ⊔ span {x}) ↑S<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>S : Submonoid α<VAR>disjoint : Disjoint ↑I ↑S<VAR>maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S<VAR>x y : α<VAR>hxy : x * y ∈ I<VAR>rid : x ∉ I ∧ y ∉ I<VAR>hx : ¬Disjoint ↑(I ⊔ span {x}) ↑S<VAR>hy : ¬Disjoint ↑(I ⊔ span {y}) ↑S<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>S : Submonoid α<VAR>disjoint : Disjoint ↑I ↑S<VAR>maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S<VAR>x y : α<VAR>hxy : x * y ∈ I<VAR>rid : x ∉ I ∧ y ∉ I<VAR>hx : ∃ x_1, (∃ y ∈ I, ∃ z, x ∣ z ∧ y + z = x_1) ∧ x_1 ∈ S<VAR>hy : ∃ x, (∃ y_1 ∈ I, ∃ z, y ∣ z ∧ y_1 + z = x) ∧ x ∈ S<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>S : Submonoid α<VAR>disjoint : Disjoint ↑I ↑S<VAR>maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S<VAR>x y : α<VAR>hxy : x * y ∈ I<VAR>rid : x ∉ I ∧ y ∉ I<VAR>s₁ : α<VAR>hs₁ : s₁ ∈ S<VAR>i₁ : α<VAR>hi₁ : i₁ ∈ I<VAR>r₁ : α<VAR>hr₁ : i₁ + x * r₁ = s₁<VAR>s₂ : α<VAR>hs₂ : s₂ ∈ S<VAR>i₂ : α<VAR>hi₂ : i₂ ∈ I<VAR>r₂ : α<VAR>hr₂ : i₂ + y * r₂ = s₂<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>S : Submonoid α<VAR>disjoint : Disjoint ↑I ↑S<VAR>maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S<VAR>x y : α<VAR>hxy : x * y ∈ I<VAR>rid : x ∉ I ∧ y ∉ I<VAR>s₁ : α<VAR>hs₁ : s₁ ∈ S<VAR>i₁ : α<VAR>hi₁ : i₁ ∈ I<VAR>r₁ : α<VAR>hr₁ : i₁ + x * r₁ = s₁<VAR>s₂ : α<VAR>hs₂ : s₂ ∈ S<VAR>i₂ : α<VAR>hi₂ : i₂ ∈ I<VAR>r₂ : α<VAR>hr₂ : i₂ + y * r₂ = s₂<GOAL>(i₁ + x * r₁) * i₂ + (i₁ * (y * r₂) + x * y * (r₁ * r₂)) = s₁ * s₂
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : X<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * r₁ = ra * ↑s₂<VAR>rb : R<VAR>sb : ↥S<VAR>hb : ↑sb * r₂ = rb * ↑s₃<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * ra = rc * ↑sb<GOAL>(ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂))
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : X<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * r₁ = ra * ↑s₂<VAR>rb : R<VAR>sb : ↥S<VAR>hb : ↑sb * r₂ = rb * ↑s₃<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * ra = rc * ↑sb<GOAL>(rc * rb) • r₃ /ₒ (sc * (sa * s₁)) = (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂))
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : X<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * r₁ = ra * ↑s₂<VAR>rb : R<VAR>sb : ↥S<VAR>hb : ↑sb * r₂ = rb * ↑s₃<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * ra = rc * ↑sb<GOAL>↑sc * (ra * r₂) = rc * rb * ↑s₃
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : X<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * r₁ = ra * ↑s₂<VAR>rb : R<VAR>sb : ↥S<VAR>hb : ↑sb * r₂ = rb * ↑s₃<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * ra = rc * ↑sb<GOAL>rc • rb • r₃ /ₒ (sc * sa * s₁) = (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂))
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : X<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * r₁ = ra * ↑s₂<VAR>rb : R<VAR>sb : ↥S<VAR>hb : ↑sb * r₂ = rb * ↑s₃<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * ra = rc * ↑sb<GOAL>(r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂)) = rc • rb • r₃ /ₒ (sc * sa * s₁)
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : X<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * r₁ = ra * ↑s₂<VAR>rb : R<VAR>sb : ↥S<VAR>hb : ↑sb * r₂ = rb * ↑s₃<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * ra = rc * ↑sb<GOAL>↑(sc * sa) * r₁ = rc * ↑(sb * s₂)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f g : α → ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x<GOAL>⨍⁻ (x : α) in s, f x ∂μ = ⨍⁻ (x : α) in s, g x ∂μ
<VAR>p x : ℝ<GOAL>‖↑x‖ = ‖↑x‖
<VAR>p x : ℝ<GOAL>‖↑(-1 * x)‖ = ‖↑x‖
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁶ : Field 𝕜<VAR>inst✝¹⁵ : CharZero 𝕜<VAR>inst✝¹⁴ : Ring R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Algebra 𝕜 R<VAR>inst✝¹¹ : Module 𝕜 M<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module Rᵐᵒᵖ M<VAR>inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝⁷ : IsScalarTower 𝕜 R M<VAR>inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup M<VAR>inst✝¹ : ContinuousSMul R M<VAR>inst✝ : ContinuousSMul Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd<VAR>e : R<VAR>h : HasSum (fun n => (expSeries 𝕜 R n) fun x_1 => x.fst) e<GOAL>HasSum (fun n => ((expSeries 𝕜 (tsze R M) n) fun x_1 => x).snd) (e • x.snd)
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁶ : Field 𝕜<VAR>inst✝¹⁵ : CharZero 𝕜<VAR>inst✝¹⁴ : Ring R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Algebra 𝕜 R<VAR>inst✝¹¹ : Module 𝕜 M<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module Rᵐᵒᵖ M<VAR>inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝⁷ : IsScalarTower 𝕜 R M<VAR>inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup M<VAR>inst✝¹ : ContinuousSMul R M<VAR>inst✝ : ContinuousSMul Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd<VAR>e : R<VAR>h : HasSum (fun n => (expSeries 𝕜 R n) fun x_1 => x.fst) e<GOAL>HasSum (fun n => ((expSeries 𝕜 (tsze R M) (n + 1)) fun x_1 => x).snd) (e • x.snd - ∑ i ∈ Finset.range 1, ((expSeries 𝕜 (tsze R M) i) fun x_1 => x).snd)
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁶ : Field 𝕜<VAR>inst✝¹⁵ : CharZero 𝕜<VAR>inst✝¹⁴ : Ring R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Algebra 𝕜 R<VAR>inst✝¹¹ : Module 𝕜 M<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module Rᵐᵒᵖ M<VAR>inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝⁷ : IsScalarTower 𝕜 R M<VAR>inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup M<VAR>inst✝¹ : ContinuousSMul R M<VAR>inst✝ : ContinuousSMul Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd<VAR>e : R<VAR>h : HasSum (fun n => (expSeries 𝕜 R n) fun x_1 => x.fst) e<GOAL>HasSum (fun n => ((expSeries 𝕜 R n) fun x_1 => x.fst) • x.snd) (e • x.snd - ∑ x_1 ∈ Finset.range 1, ((expSeries 𝕜 (tsze R M) x_1) fun x_2 => x).snd)
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁶ : Field 𝕜<VAR>inst✝¹⁵ : CharZero 𝕜<VAR>inst✝¹⁴ : Ring R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Algebra 𝕜 R<VAR>inst✝¹¹ : Module 𝕜 M<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module Rᵐᵒᵖ M<VAR>inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝⁷ : IsScalarTower 𝕜 R M<VAR>inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup M<VAR>inst✝¹ : ContinuousSMul R M<VAR>inst✝ : ContinuousSMul Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd<VAR>e : R<VAR>h : HasSum (fun n => (↑n.factorial)⁻¹ • x.fst ^ n) e<GOAL>HasSum (fun n => ((↑n.factorial)⁻¹ • x.fst ^ n) • x.snd) (e • x.snd - ∑ x_1 ∈ Finset.range 1, ((↑x_1.factorial)⁻¹ • x ^ x_1).snd)
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁶ : Field 𝕜<VAR>inst✝¹⁵ : CharZero 𝕜<VAR>inst✝¹⁴ : Ring R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Algebra 𝕜 R<VAR>inst✝¹¹ : Module 𝕜 M<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module Rᵐᵒᵖ M<VAR>inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝⁷ : IsScalarTower 𝕜 R M<VAR>inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup M<VAR>inst✝¹ : ContinuousSMul R M<VAR>inst✝ : ContinuousSMul Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd<VAR>e : R<VAR>h : HasSum (fun n => (↑n.factorial)⁻¹ • x.fst ^ n) e<GOAL>HasSum (fun n => ((↑n.factorial)⁻¹ • x.fst ^ n) • x.snd) (e • x.snd)
<VAR>m₁ m₂ n : ℕ<GOAL>qrSign (m₁ * m₂) n = qrSign m₁ n * qrSign m₂ n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>(fromPadicInt p).comp (toPadicInt p) = RingHom.id (𝕎 (ZMod p))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>∀ (k : ℕ), (truncate k).comp ((fromPadicInt p).comp (toPadicInt p)) = (truncate k).comp (RingHom.id (𝕎 (ZMod p)))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(truncate n).comp ((fromPadicInt p).comp (toPadicInt p)) = (truncate n).comp (RingHom.id (𝕎 (ZMod p)))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(zmodEquivTrunc p n).toRingHom.comp ((PadicInt.toZModPow n).comp (toPadicInt p)) = (truncate n).comp (RingHom.id (𝕎 (ZMod p)))
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>t u v w : V<VAR>p : G.Walk v w<VAR>he : s(t, u) ∈ p.edges<GOAL>u ∈ p.support
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>t u v w : V<VAR>p : G.Walk v w<VAR>he : s(u, t) ∈ p.edges<GOAL>u ∈ p.support
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>f : G' →* G<VAR>hf : Injective ⇑f<VAR>inst✝ : H.IsCommutative<VAR>a b : ↥(comap f H)<GOAL>↑(a * b) = ↑(b * a)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>f : G' →* G<VAR>hf : Injective ⇑f<VAR>inst✝ : H.IsCommutative<VAR>a b : ↥(comap f H)<VAR>this : ⟨f ↑a, ⋯⟩ * ⟨f ↑b, ⋯⟩ = ⟨f ↑b, ⋯⟩ * ⟨f ↑a, ⋯⟩<GOAL>↑(a * b) = ↑(b * a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b c : Ordinal.{u_4}<GOAL>a + b = a + c ↔ b = c
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>x y : ModP K v O hv p<VAR>hx : x ^ p ≠ 0<VAR>hy : y ^ p ≠ 0<GOAL>x * y ≠ 0
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>y : ModP K v O hv p<VAR>hy : y ^ p ≠ 0<VAR>r : O<VAR>hx : (Ideal.Quotient.mk (Ideal.span {↑p})) r ^ p ≠ 0<GOAL>(Ideal.Quotient.mk (Ideal.span {↑p})) r * y ≠ 0
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx : (Ideal.Quotient.mk (Ideal.span {↑p})) r ^ p ≠ 0<VAR>s : O<VAR>hy : (Ideal.Quotient.mk (Ideal.span {↑p})) s ^ p ≠ 0<GOAL>(Ideal.Quotient.mk (Ideal.span {↑p})) r * (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx : (Ideal.Quotient.mk (Ideal.span {↑p})) r ^ p ≠ 0<VAR>s : O<VAR>hy : (Ideal.Quotient.mk (Ideal.span {↑p})) s ^ p ≠ 0<VAR>h1p : 0 < 1 / ↑p<GOAL>(Ideal.Quotient.mk (Ideal.span {↑p})) r * (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx : (Ideal.Quotient.mk (Ideal.span {↑p})) r ^ p ≠ 0<VAR>s : O<VAR>hy : (Ideal.Quotient.mk (Ideal.span {↑p})) s ^ p ≠ 0<VAR>h1p : 0 < 1 / ↑p<GOAL>(Ideal.Quotient.mk (Ideal.span {↑p})) (r * s) ≠ 0
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx : (Ideal.Quotient.mk (Ideal.span {↑p})) (r ^ p) ≠ 0<VAR>s : O<VAR>hy : (Ideal.Quotient.mk (Ideal.span {↑p})) (s ^ p) ≠ 0<VAR>h1p : 0 < 1 / ↑p<GOAL>(Ideal.Quotient.mk (Ideal.span {↑p})) (r * s) ≠ 0
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx : v ↑p < v ((algebraMap O K) (r ^ p))<VAR>s : O<VAR>hy : v ↑p < v ((algebraMap O K) (s ^ p))<VAR>h1p : 0 < 1 / ↑p<GOAL>v ↑p < v ((algebraMap O K) (r * s))
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)<VAR>s : O<VAR>hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)<VAR>h1p : 0 < 1 / ↑p<GOAL>v ↑p < v ((algebraMap O K) (r * s))
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)<VAR>s : O<VAR>hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)<VAR>h1p : 0 < 1 / ↑p<GOAL>v ↑p < v ((algebraMap O K) r) * v ((algebraMap O K) s)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)<VAR>s : O<VAR>hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)<VAR>h1p : 0 < 1 / ↑p<GOAL>v ↑p ≤ v ↑p ^ (1 / ↑p) * v ↑p ^ (1 / ↑p)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp✝ : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)<VAR>s : O<VAR>hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)<VAR>h1p : 0 < 1 / ↑p<VAR>hvp : ¬v ↑p = 0<GOAL>v ↑p ≤ v ↑p ^ (1 / ↑p) * v ↑p ^ (1 / ↑p)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp✝ : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)<VAR>s : O<VAR>hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)<VAR>h1p : 0 < 1 / ↑p<VAR>hvp : 0 < v ↑p<GOAL>v ↑p ≤ v ↑p ^ (1 / ↑p) * v ↑p ^ (1 / ↑p)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp✝ : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)<VAR>s : O<VAR>hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)<VAR>h1p : 0 < 1 / ↑p<VAR>hvp : 0 < v ↑p<GOAL>v ↑p ^ 1 ≤ v ↑p ^ (1 / ↑p) * v ↑p ^ (1 / ↑p)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp✝ : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)<VAR>s : O<VAR>hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)<VAR>h1p : 0 < 1 / ↑p<VAR>hvp : 0 < v ↑p<GOAL>v ↑p ^ 1 ≤ v ↑p ^ (1 / ↑p + 1 / ↑p)