ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>inst✝¹ : K.HasHomology j<VAR>inst✝ : (K.sc' i j k).HasHomology<GOAL>(K.sc j).pOpcycles = K.pOpcycles j
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : Fintype m<VAR>inst✝¹ : Fintype n<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>u v w : m → α<VAR>x y : n → α<VAR>e : n ≃ m<GOAL>u ⬝ᵥ x ∘ ⇑e.symm = u ∘ ⇑e ⬝ᵥ x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝²⁰ : CommRing R<VAR>inst✝¹⁹ : CommRing S<VAR>inst✝¹⁸ : CommRing T<VAR>inst✝¹⁷ : Algebra R S<VAR>inst✝¹⁶ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹² : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra L F<VAR>inst✝⁸ : Algebra R F<VAR>inst✝⁷ : IsScalarTower R L F<VAR>inst✝⁶ : Algebra K F<VAR>inst✝⁵ : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsAlgClosed E<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>x : L<GOAL>(algebraMap K E) ((Algebra.trace K L) x) = ∑ σ : L →ₐ[K] E, σ x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝²⁰ : CommRing R<VAR>inst✝¹⁹ : CommRing S<VAR>inst✝¹⁸ : CommRing T<VAR>inst✝¹⁷ : Algebra R S<VAR>inst✝¹⁶ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹² : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra L F<VAR>inst✝⁸ : Algebra R F<VAR>inst✝⁷ : IsScalarTower R L F<VAR>inst✝⁶ : Algebra K F<VAR>inst✝⁵ : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsAlgClosed E<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>x : L<VAR>hx : IsIntegral K x<GOAL>(algebraMap K E) ((Algebra.trace K L) x) = ∑ σ : L →ₐ[K] E, σ x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝²⁰ : CommRing R<VAR>inst✝¹⁹ : CommRing S<VAR>inst✝¹⁸ : CommRing T<VAR>inst✝¹⁷ : Algebra R S<VAR>inst✝¹⁶ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹² : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra L F<VAR>inst✝⁸ : Algebra R F<VAR>inst✝⁷ : IsScalarTower R L F<VAR>inst✝⁶ : Algebra K F<VAR>inst✝⁵ : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsAlgClosed E<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>x : L<VAR>hx : IsIntegral K x<VAR>pb : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis hx<GOAL>(algebraMap K E) ((Algebra.trace K L) x) = ∑ σ : L →ₐ[K] E, σ x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝²⁰ : CommRing R<VAR>inst✝¹⁹ : CommRing S<VAR>inst✝¹⁸ : CommRing T<VAR>inst✝¹⁷ : Algebra R S<VAR>inst✝¹⁶ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹² : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra L F<VAR>inst✝⁸ : Algebra R F<VAR>inst✝⁷ : IsScalarTower R L F<VAR>inst✝⁶ : Algebra K F<VAR>inst✝⁵ : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsAlgClosed E<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>x : L<VAR>hx : IsIntegral K x<VAR>pb : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis hx<GOAL>(algebraMap K E) ((algebraMap ℕ K) (finrank (↥K⟮x⟯) L)) * ∑ σ : ↥K⟮x⟯ →ₐ[K] E, σ pb.gen = ∑ σ : L →ₐ[K] E, σ x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝²⁰ : CommRing R<VAR>inst✝¹⁹ : CommRing S<VAR>inst✝¹⁸ : CommRing T<VAR>inst✝¹⁷ : Algebra R S<VAR>inst✝¹⁶ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹² : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra L F<VAR>inst✝⁸ : Algebra R F<VAR>inst✝⁷ : IsScalarTower R L F<VAR>inst✝⁶ : Algebra K F<VAR>inst✝⁵ : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsAlgClosed E<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>x : L<VAR>hx : IsIntegral K x<VAR>pb : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis hx<GOAL>IsSeparable K pb.gen
<VAR>α β : Type u<VAR>f : ℕ → Cardinal.{u}<GOAL>sum f = f 0 + sum fun i => f (i + 1)
<VAR>α β : Type u<VAR>f : ℕ → Cardinal.{u}<GOAL>#(Quotient.out (f 0) ⊕ (n : ℕ) × Quotient.out (f (n + 1))) = f 0 + sum fun i => f (i + 1)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<GOAL>HasIntegral I l (fun x => 0) vol 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Finset ℕ<VAR>n : ℕ<VAR>s : Finset ℕ<GOAL>(∑ i ∈ s, 2 ^ i).bitIndices.toFinset = s
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>t : Set Ω<VAR>h_indep : IndepSet t t μ<GOAL>μ t = 0 ∨ μ t = 1 ∨ μ t = ⊤
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : StarRing α<VAR>d : ℕ<GOAL>(↑d)ᴴ = ↑d
<VAR>n k : ℕ<VAR>hk : n + 1 < k + 1<GOAL>(n + 1).choose (k + 1) = 0
<VAR>n k : ℕ<VAR>hk : n + 1 < k + 1<VAR>hnk : n < k<GOAL>(n + 1).choose (k + 1) = 0
<VAR>n k : ℕ<VAR>hk : n + 1 < k + 1<VAR>hnk : n < k<VAR>hnk1 : n < k + 1<GOAL>(n + 1).choose (k + 1) = 0
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fintype n<VAR>P : Matrix n n 𝕜 → Prop<VAR>M : Matrix n n 𝕜<VAR>hMdet : M.det ≠ 0<VAR>hdiag : ∀ (D : n → 𝕜), (diagonal D).det ≠ 0 → P (diagonal D)<VAR>htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix<VAR>hmul : ∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)<VAR>Q : Matrix n n 𝕜 → Prop := fun N => N.det ≠ 0 ∧ P N<VAR>this : Q M<GOAL>P M
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>completedHurwitzZetaEven a s = completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s)
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>(hurwitzEvenFEPair a).Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 - ((hurwitzEvenFEPair a).ε / (↑(hurwitzEvenFEPair a).k - s / 2)) • (hurwitzEvenFEPair a).g₀ / 2 = completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s)
<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✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hk : p ^ (k + 1) ≠ 2<GOAL>Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = (-1) ^ (φ (↑p ^ (k + 1)) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 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>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hk : p ^ (k + 1) ≠ 2<GOAL>Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f g : ↥(simpleFunc E p μ)<GOAL>↑(toSimpleFunc (f - g)) =ᶠ[ae μ] ↑(toSimpleFunc f) - ↑(toSimpleFunc g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f g : ↥(simpleFunc E p μ)<VAR>a✝ : α<GOAL>↑(toSimpleFunc (f - g)) a✝ = ↑↑↑(f - g) a✝ → ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑(toSimpleFunc g) a✝ = ↑↑↑g a✝ → ↑↑(↑f - ↑g) a✝ = (↑↑↑f - ↑↑↑g) a✝ → ↑(toSimpleFunc (f - g)) a✝ = (↑(toSimpleFunc f) - ↑(toSimpleFunc g)) a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f g : ↥(simpleFunc E p μ)<VAR>a✝ : α<GOAL>↑(toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝ → ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑(toSimpleFunc g) a✝ = ↑↑↑g a✝ → ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → ↑(toSimpleFunc (f - g)) a✝ = ↑(toSimpleFunc f) a✝ - ↑(toSimpleFunc g) a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : t =ᶠ[ae μ] univ<GOAL>s ∪ t =ᶠ[ae μ] univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : t =ᶠ[ae μ] univ<GOAL>univ = s ∪ univ
<VAR>a b : String<GOAL>a.firstDiffPos b = { byteIdx := utf8Len (List.takeWhile₂ (fun x x_1 => decide (x = x_1)) a.data b.data).fst }
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>γ : α → Type u_2<VAR>δ : α → Type u_3<VAR>s : (a : α) → Finset (γ a)<GOAL>(piFinset s).Nonempty ↔ ∀ (a : α), (s a).Nonempty
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>a : Ordinal.{u_1}<GOAL>nfp id a = id a
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>a : Ordinal.{u_1}<GOAL>(sup fun n => id a) = id a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>C : ι → Set α<VAR>f : (x : ι) → β → ↑(C x)<VAR>hf : ∀ (x : ι), Surjective (f x)<VAR>x : α<GOAL>(x ∈ ⋃ y, range fun x => ↑(f x y)) ↔ x ∈ ⋃ x, C x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>C : ι → Set α<VAR>f : (x : ι) → β → ↑(C x)<VAR>hf : ∀ (x : ι), Surjective (f x)<VAR>x : α<GOAL>(∃ i, x ∈ range fun x => ↑(f x i)) ↔ ∃ i, x ∈ C i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>insert a (Ioc a b) = Icc a b
<VAR>p n : ℕ<GOAL>p ^ padicValNat p n ∣ n
<VAR>p : ℕ<GOAL>p ^ padicValNat p 0 ∣ 0
<VAR>p n : ℕ<VAR>hn : n > 0<GOAL>p ^ padicValNat p n ∣ n
<VAR>n : ℕ<VAR>hn : n > 0<GOAL>1 ^ padicValNat 1 n ∣ n
<VAR>p n : ℕ<VAR>hn : n > 0<VAR>hp : p ≠ 1<GOAL>p ^ padicValNat p n ∣ n
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>ne : Nonempty ι<VAR>e f : OrthonormalBasis ι ℝ E<VAR>x : Orientation ℝ E ι<GOAL>(e.adjustToOrientation x).toBasis.det = e.toBasis.det ∨ (e.adjustToOrientation x).toBasis.det = -e.toBasis.det
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>ι : Type v<VAR>inst✝⁶ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁴ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝³ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>injective : ∀ (i : ι), Function.Injective ⇑(g i)<GOAL>Function.Injective ⇑(lift R ι G f g Hg)
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>ι : Type v<VAR>inst✝⁶ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁴ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝³ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>injective : ∀ (i : ι), Function.Injective ⇑(g i)<VAR>h✝ : IsEmpty ι<GOAL>Function.Injective ⇑(lift R ι G f g Hg)
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>ι : Type v<VAR>inst✝⁶ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁴ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝³ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>injective : ∀ (i : ι), Function.Injective ⇑(g i)<VAR>h✝ : Nonempty ι<GOAL>Function.Injective ⇑(lift R ι G f g Hg)
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>ι : Type v<VAR>inst✝⁶ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁴ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝³ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>h✝ : Nonempty ι<VAR>injective : ∀ (i : ι) (a : G i), (g i) a = 0 → a = 0<GOAL>∀ (a : DirectLimit G f), (lift R ι G f g Hg) a = 0 → a = 0
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>ι : Type v<VAR>inst✝⁶ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁴ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝³ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>h✝ : Nonempty ι<VAR>injective : ∀ (i : ι) (a : G i), (g i) a = 0 → a = 0<VAR>z : DirectLimit G f<VAR>hz : (lift R ι G f g Hg) z = 0<GOAL>z = 0
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>ι : Type v<VAR>inst✝⁶ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁴ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝³ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>g✝ : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) ((f i j hij) x) = (g✝ i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>h✝ : Nonempty ι<VAR>injective : ∀ (i : ι) (a : G i), (g✝ i) a = 0 → a = 0<VAR>i✝ : ι<VAR>g : G i✝<VAR>hz : (lift R ι G f g✝ Hg) ((of R ι G f i✝) g) = 0<GOAL>(of R ι G f i✝) g = 0
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>ι : Type v<VAR>inst✝⁶ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁴ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝³ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>g✝ : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) ((f i j hij) x) = (g✝ i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>h✝ : Nonempty ι<VAR>injective : ∀ (i : ι) (a : G i), (g✝ i) a = 0 → a = 0<VAR>i✝ : ι<VAR>g : G i✝<VAR>hz : (g✝ i✝) g = 0<GOAL>(of R ι G f i✝) g = 0
<VAR>R✝ : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : Ring R✝<VAR>inst✝⁴ : Ring S<VAR>f : R✝ →+* S<VAR>I✝ : Type u_3<VAR>e : I✝ → R✝<VAR>he✝ : OrthogonalIdempotents e<VAR>inst✝³ : Fintype I✝<VAR>he : CompleteOrthogonalIdempotents e<VAR>I : Type u_4<VAR>inst✝² : Fintype I<VAR>inst✝¹ : DecidableEq I<VAR>R : I → Type u_5<VAR>inst✝ : (i : I) → Ring (R i)<GOAL>CompleteOrthogonalIdempotents fun x => Pi.single x 1
<VAR>R✝ : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : Ring R✝<VAR>inst✝⁴ : Ring S<VAR>f : R✝ →+* S<VAR>I✝ : Type u_3<VAR>e : I✝ → R✝<VAR>he✝ : OrthogonalIdempotents e<VAR>inst✝³ : Fintype I✝<VAR>he : CompleteOrthogonalIdempotents e<VAR>I : Type u_4<VAR>inst✝² : Fintype I<VAR>inst✝¹ : DecidableEq I<VAR>R : I → Type u_5<VAR>inst✝ : (i : I) → Ring (R i)<GOAL>∀ (i j : I), i ≠ j → Pi.single i 1 * Pi.single j 1 = 0
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : CommSemiring R<VAR>f : M →+ ι<VAR>m : M<VAR>r : R<GOAL>(decomposeAux f) (Finsupp.single m r) = (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m r, ⋯⟩
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : CommSemiring R<VAR>f : M →+ ι<VAR>m : M<VAR>r : R<GOAL>r • { toFun := fun m => (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f (Multiplicative.toAdd m))) ⟨Finsupp.single (Multiplicative.toAdd m) 1, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ } (Multiplicative.ofAdd m) = (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m r, ⋯⟩
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : CommSemiring R<VAR>f : M →+ ι<VAR>m : M<VAR>r : R<GOAL>(DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f (Multiplicative.toAdd (Multiplicative.ofAdd m)))) (r • ⟨Finsupp.single (Multiplicative.toAdd (Multiplicative.ofAdd m)) 1, ⋯⟩) = (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m r, ⋯⟩
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : CommSemiring R<VAR>f : M →+ ι<VAR>m : M<VAR>r : R<GOAL>GradedMonoid.mk (f (Multiplicative.toAdd (Multiplicative.ofAdd m))) (r • ⟨Finsupp.single (Multiplicative.toAdd (Multiplicative.ofAdd m)) 1, ⋯⟩) = GradedMonoid.mk (f m) ⟨Finsupp.single m r, ⋯⟩
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : CommSemiring R<VAR>f : M →+ ι<VAR>m : M<VAR>r : R<GOAL>↑(GradedMonoid.mk (f (Multiplicative.toAdd (Multiplicative.ofAdd m))) (r • ⟨Finsupp.single (Multiplicative.toAdd (Multiplicative.ofAdd m)) 1, ⋯⟩)).snd = ↑(GradedMonoid.mk (f m) ⟨Finsupp.single m r, ⋯⟩).snd
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : CommSemiring R<VAR>f : M →+ ι<VAR>m : M<VAR>r : R<GOAL>Finsupp.single (Multiplicative.toAdd (Multiplicative.ofAdd m)) (r * 1) = ↑(GradedMonoid.mk (f m) ⟨Finsupp.single m r, ⋯⟩).snd
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : CommSemiring R<VAR>f : M →+ ι<VAR>m : M<VAR>r : R<GOAL>Finsupp.single (Multiplicative.toAdd (Multiplicative.ofAdd m)) r = ↑(GradedMonoid.mk (f m) ⟨Finsupp.single m r, ⋯⟩).snd
<VAR>a : Ordinal.{u_1}<GOAL>1 ^ a = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : LinearOrderedField 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : ContinuousConstSMul 𝕜 E<VAR>inst✝ : LocallyConvexSpace 𝕜 E<VAR>s t : Set E<VAR>disj : Disjoint s t<VAR>hs₁ : Convex 𝕜 s<VAR>hs₂ : IsCompact s<VAR>ht₁ : Convex 𝕜 t<VAR>ht₂ : IsClosed t<VAR>this : UniformSpace E := TopologicalAddGroup.toUniformSpace E<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : LinearOrderedField 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : ContinuousConstSMul 𝕜 E<VAR>inst✝ : LocallyConvexSpace 𝕜 E<VAR>s t : Set E<VAR>disj : Disjoint s t<VAR>hs₁ : Convex 𝕜 s<VAR>hs₂ : IsCompact s<VAR>ht₁ : Convex 𝕜 t<VAR>ht₂ : IsClosed t<VAR>this✝ : UniformSpace E := TopologicalAddGroup.toUniformSpace E<VAR>this : UniformAddGroup E<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : LinearOrderedField 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : ContinuousConstSMul 𝕜 E<VAR>inst✝ : LocallyConvexSpace 𝕜 E<VAR>s t : Set E<VAR>disj : Disjoint s t<VAR>hs₁ : Convex 𝕜 s<VAR>hs₂ : IsCompact s<VAR>ht₁ : Convex 𝕜 t<VAR>ht₂ : IsClosed t<VAR>this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E<VAR>this✝ : UniformAddGroup E<VAR>this : (comap (fun x => x.2 - x.1) (𝓝 0)).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.2 - x.1) ⁻¹' id i<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : LinearOrderedField 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : ContinuousConstSMul 𝕜 E<VAR>inst✝ : LocallyConvexSpace 𝕜 E<VAR>s t : Set E<VAR>disj : Disjoint s t<VAR>hs₁ : Convex 𝕜 s<VAR>hs₂ : IsCompact s<VAR>ht₁ : Convex 𝕜 t<VAR>ht₂ : IsClosed t<VAR>this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E<VAR>this✝ : UniformAddGroup E<VAR>this : (uniformity E).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.2 - x.1) ⁻¹' id i<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : LinearOrderedField 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : ContinuousConstSMul 𝕜 E<VAR>inst✝ : LocallyConvexSpace 𝕜 E<VAR>s t : Set E<VAR>disj : Disjoint s t<VAR>hs₁ : Convex 𝕜 s<VAR>hs₂ : IsCompact s<VAR>ht₁ : Convex 𝕜 t<VAR>ht₂ : IsClosed t<VAR>this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E<VAR>this✝ : UniformAddGroup E<VAR>this : (uniformity E).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.2 - x.1) ⁻¹' id i<VAR>V : Set E<VAR>hV : Disjoint (⋃ x ∈ s, UniformSpace.ball x ((fun x => x.2 - x.1) ⁻¹' id V)) (⋃ x ∈ t, UniformSpace.ball x ((fun x => x.2 - x.1) ⁻¹' id V))<VAR>hV0 : 0 ∈ V<VAR>hVopen : IsOpen V<VAR>hVconvex : Convex 𝕜 V<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : LinearOrderedField 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : ContinuousConstSMul 𝕜 E<VAR>inst✝ : LocallyConvexSpace 𝕜 E<VAR>s t : Set E<VAR>disj : Disjoint s t<VAR>hs₁ : Convex 𝕜 s<VAR>hs₂ : IsCompact s<VAR>ht₁ : Convex 𝕜 t<VAR>ht₂ : IsClosed t<VAR>this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E<VAR>this✝ : UniformAddGroup E<VAR>this : (uniformity E).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.2 - x.1) ⁻¹' id i<VAR>V : Set E<VAR>hV : Disjoint (⋃ x ∈ s, UniformSpace.ball x ((fun x => x.2 - x.1) ⁻¹' id V)) (⋃ x ∈ t, UniformSpace.ball x ((fun x => x.2 - x.1) ⁻¹' id V))<VAR>hV0 : 0 ∈ V<VAR>hVopen : IsOpen V<VAR>hVconvex : Convex 𝕜 V<GOAL>Disjoint (s + V) (t + V)