ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A → B<VAR>h : ∀ (x y : A), f (x + y) = f x + f y<VAR>h₀ : ∀ (m : R) (x : A), { toFun := f, map_add' := h }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := h }.toFun x<VAR>h₁ : Coalgebra.counit ∘ₗ { toFun := f, map_add' := h, map_smul' := h₀ } = Coalgebra.counit<VAR>h₂ : TensorProduct.map { toFun := f, map_add' := h, map_smul' := h₀ } { toFun := f, map_add' := h, map_smul' := h₀ } ∘ₗ Coalgebra.comul = Coalgebra.comul ∘ₗ { toFun := f, map_add' := h, map_smul' := h₀ }<VAR>h₃ : B → A<VAR>h₄ : Function.LeftInverse h₃ { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂ }.toFun<VAR>h₅ : Function.RightInverse h₃ { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂ }.toFun<GOAL>⇑{ toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄, right_inv := h₅ } = f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e : A ≃ₗc[R] B<GOAL>⇑↑e = ⇑e
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A ≃ₗc[R] B<GOAL>f.toLinearEquiv = ↑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A ≃ₗc[R] B<GOAL>f.toCoalgHom = ↑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e : A ≃ₗc[R] B<GOAL>↑↑e = ↑↑e
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e e' : A ≃ₗc[R] B<VAR>h : ∀ (x : A), e x = e' x<GOAL>e = e'
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e e' : A ≃ₗc[R] B<GOAL>e = e' ↔ ∀ (x : A), e x = e' x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e : A ≃ₗc[R] B<VAR>x x' : A<GOAL>x = x' → e x = e x'
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e e' : A ≃ₗc[R] B<VAR>h : e = e'<VAR>x : A<GOAL>e x = e' x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>CoalgebraStruct R A<VAR>a : A<GOAL>(CoalgEquiv.refl R A) a = a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>CoalgebraStruct R A<GOAL>∀ (a : A), (CoalgEquiv.refl R A).invFun a = a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>CoalgebraStruct R A<GOAL>↑(CoalgEquiv.refl R A) = LinearEquiv.refl R A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>CoalgebraStruct R A<GOAL>↑(CoalgEquiv.refl R A) = CoalgHom.id R A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e : A ≃ₗc[R] B<GOAL>↑e.symm = (↑e).symm
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e : A ≃ₗc[R] B<GOAL>↑↑e.symm = ↑(↑e).symm
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e : A ≃ₗc[R] B<GOAL>e.invFun = ⇑e.symm
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e : A ≃ₗc[R] B<GOAL>e.toEquiv.symm = ↑e.symm
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>AddCommMonoid C<VAR>Module R A<VAR>Module R B<VAR>Module R C<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>e₁₂ : A ≃ₗc[R] B<VAR>e₂₃ : B ≃ₗc[R] C<GOAL>∀ (a : C), (e₁₂.trans e₂₃).invFun a = (↑e₁₂).symm ((↑e₂₃).symm a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>AddCommMonoid C<VAR>Module R A<VAR>Module R B<VAR>Module R C<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>e₁₂ : A ≃ₗc[R] B<VAR>e₂₃ : B ≃ₗc[R] C<GOAL>∀ (a : A), (e₁₂.trans e₂₃) a = e₂₃ (e₁₂ a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>AddCommMonoid C<VAR>Module R A<VAR>Module R B<VAR>Module R C<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>e₁₂ : A ≃ₗc[R] B<VAR>e₂₃ : B ≃ₗc[R] C<GOAL>↑(e₁₂.trans e₂₃) = ↑e₁₂ ≪≫ₗ ↑e₂₃
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>AddCommMonoid C<VAR>Module R A<VAR>Module R B<VAR>Module R C<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>e₁₂ : A ≃ₗc[R] B<VAR>e₂₃ : B ≃ₗc[R] C<GOAL>↑(e₁₂.trans e₂₃) = e₂₃.comp ↑e₁₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>AddCommMonoid C<VAR>Module R A<VAR>Module R B<VAR>Module R C<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>e₁₂ : A ≃ₗc[R] B<VAR>e₂₃ : B ≃ₗc[R] C<GOAL>(↑e₁₂).trans ↑e₂₃ = ↑(e₁₂.trans e₂₃)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Submodule R M<GOAL>N.FG ↔ ∃ S, S.Finite ∧ Submodule.span R S = N
<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>P : Submodule ℕ M<GOAL>P.FG ↔ P.FG
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>P : Submodule ℤ G<GOAL>P.FG ↔ P.toAddSubgroup.FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Submodule R M<GOAL>N.FG ↔ ∃ n s, Submodule.span R (Set.range s) = N
<VAR>R : Type u_3<VAR>CommRing R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>hn : N.FG<VAR>hin : N ≤ I • N<GOAL>∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>hn : N.FG<VAR>hin : N ≤ I • N<GOAL>∃ r ∈ I, ∀ n ∈ N, r • n = n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⊥.FG
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>(Subalgebra.toSubmodule ⊥).FG
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>I : (Submodule R A)ˣ<GOAL>(↑I).FG
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>I : Submodule R A<VAR>hI : IsUnit I<GOAL>I.FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<VAR>hs : s.Finite<GOAL>(Submodule.span R s).FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>(Submodule.span R {x}).FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N₁ N₂ : Submodule R M<VAR>hN₁ : N₁.FG<VAR>hN₂ : N₂.FG<GOAL>(N₁ ⊔ N₂).FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>N : ι → Submodule R M<VAR>h : ∀ i ∈ s, (N i).FG<GOAL>(s.sup N).FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>N : ι → Submodule R M<VAR>h : ∀ i ∈ s, (N i).FG<GOAL>(⨆ i ∈ s, N i).FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_3<VAR>Finite ι<VAR>N : ι → Submodule R M<VAR>h : ∀ (i : ι), (N i).FG<GOAL>(iSup N).FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>Module R P<VAR>f : M →ₗ[R] P<VAR>N : Submodule R M<VAR>hs : N.FG<GOAL>(Submodule.map f N).FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>Module R P<VAR>f : M →ₗ[R] P<VAR>hf : Function.Injective ⇑f<VAR>N : Submodule R M<VAR>hfn : (Submodule.map f N).FG<GOAL>N.FG
<VAR>R : Type u_4<VAR>M : Type u_5<VAR>P : Type u_6<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup P<VAR>Module R P<VAR>f : M →ₗ[R] P<VAR>hf : LinearMap.ker f = ⊥<VAR>N : Submodule R M<VAR>hfn : (Submodule.map f N).FG<GOAL>N.FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Submodule R M<GOAL>⊤.FG ↔ N.FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>Module R P<VAR>e : M ≃ₗ[R] P<VAR>h : ⊤.FG<GOAL>⊤.FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>Module R P<VAR>sb : Submodule R M<VAR>sc : Submodule R P<VAR>hsb : sb.FG<VAR>hsc : sc.FG<GOAL>(sb.prod sc).FG
<VAR>R : Type u_1<VAR>Semiring R<VAR>ι : Type u_4<VAR>M : ι → Type u_5<VAR>Finite ι<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>p : (i : ι) → Submodule R (M i)<VAR>hsb : ∀ (i : ι), (p i).FG<GOAL>(Submodule.pi Set.univ p).FG
<VAR>R : Type u_4<VAR>M : Type u_5<VAR>P : Type u_6<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup P<VAR>Module R P<VAR>f : M →ₗ[R] P<VAR>s : Submodule R M<VAR>hs1 : (Submodule.map f s).FG<VAR>hs2 : (s ⊓ LinearMap.ker f).FG<GOAL>s.FG
<VAR>R : Type u_4<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>P : Submodule R M → Prop<VAR>h₁ : ∀ (x : M), P (Submodule.span R {x})<VAR>h₂ : ∀ (M₁ M₂ : Submodule R M), P M₁ → P M₂ → P (M₁ ⊔ M₂)<VAR>N : Submodule R M<VAR>hN : N.FG<GOAL>P N
<VAR>R : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>AddCommGroup P<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf1 : (LinearMap.ker f).FG<VAR>hf2 : (LinearMap.ker g).FG<VAR>hsur : Function.Surjective ⇑f<GOAL>(LinearMap.ker (g ∘ₗ f)).FG
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>M : Type u_6<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>AddCommGroup M<VAR>Module S M<VAR>Module R M<VAR>IsScalarTower R S M<VAR>N : Submodule S M<VAR>hfin : N.FG<VAR>h : Function.Surjective ⇑(algebraMap R S)<GOAL>(Submodule.restrictScalars R N).FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Submodule R M<VAR>hM' : M'.FG<VAR>N : ℕ →o Submodule R M<VAR>H : iSup ⇑N = M'<GOAL>∃ n, M' = N n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Submodule R M<GOAL>s.FG ↔ CompleteLattice.IsCompactElement s
<VAR>R : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>I : Submodule R N<VAR>x : TensorProduct R (↥I) M<GOAL>∃ J, ∃ (_ : J.FG) (hle : J ≤ I), ∃ y, x = (LinearMap.rTensor M (Submodule.inclusion hle)) y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p : Submodule R M<VAR>q : Submodule R N<VAR>hp : p.FG<VAR>hq : q.FG<GOAL>(Submodule.map₂ f p q).FG
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>M N : Submodule R A<VAR>hm : M.FG<VAR>hn : N.FG<GOAL>(M * N).FG
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submodule R A<VAR>h : M.FG<VAR>n : ℕ<GOAL>(M ^ n).FG
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal R<VAR>h : I.FG<VAR>f : R →+* S<GOAL>(Ideal.map f I).FG
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing S<VAR>CommRing A<VAR>f : R →+* S<VAR>g : S →+* A<VAR>hf : (RingHom.ker f).FG<VAR>hg : (RingHom.ker g).FG<VAR>hsur : Function.Surjective ⇑f<GOAL>(RingHom.ker (g.comp f)).FG
<VAR>R : Type u_3<VAR>CommSemiring R<VAR>I : Ideal R<VAR>h : I.radical.FG<GOAL>∃ n, I.radical ^ n ≤ I
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>self : Module.Finite R M<GOAL>⊤.FG
<VAR>R : Type u_6<VAR>M : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Module.Finite R M ↔ ⊤.FG
<VAR>M : Type u_6<VAR>AddCommMonoid M<GOAL>Module.Finite ℕ M ↔ AddMonoid.FG M
<VAR>G : Type u_6<VAR>AddCommGroup G<GOAL>Module.Finite ℤ G ↔ AddGroup.FG G
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module.Finite R M<GOAL>∃ n s, Submodule.span R (Set.range s) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module.Finite R M<GOAL>∃ n f, Function.Surjective ⇑f
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>hM : Module.Finite R M<VAR>f : M →ₗ[R] N<VAR>hf : Function.Surjective ⇑f<GOAL>Module.Finite R N
<VAR>R : Type u_6<VAR>A : Type u_7<VAR>M : Type u_8<VAR>CommSemiring R<VAR>Semiring A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>Algebra R A<VAR>IsScalarTower R A M<VAR>hM : Module.Finite R M<GOAL>Module.Finite A M
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Module.Finite R M<VAR>e : M ≃ₗ[R] N<GOAL>Module.Finite R N
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>e : M ≃ₗ[R] N<GOAL>Module.Finite R M ↔ Module.Finite R N
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Submodule R M<GOAL>Module.Finite R ↥N ↔ N.FG
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : Set M<VAR>hA : A.Finite<GOAL>Module.Finite R ↥(Submodule.span R A)
<VAR>R : Type u_6<VAR>M : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module.Finite R M<VAR>f : Module.End R M<GOAL>IsNilpotent f ↔ ∀ (m : M), ∃ n, (f ^ n) m = 0
<VAR>R : Type u_6<VAR>A : Type u_7<VAR>M : Type u_8<VAR>Semiring R<VAR>Semiring A<VAR>Module R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>Module.Finite R A<VAR>Module.Finite A M<GOAL>Module.Finite R M
<VAR>A₁ : Type u_6<VAR>B₁ : Type u_7<VAR>A₂ : Type u_8<VAR>B₂ : Type u_9<VAR>CommRing A₁<VAR>CommRing B₁<VAR>CommRing A₂<VAR>CommRing B₂<VAR>Algebra A₁ B₁<VAR>Algebra A₂ B₂<VAR>e₁ : A₁ ≃+* A₂<VAR>e₂ : B₁ ≃+* B₂<VAR>he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)<VAR>Module.Finite A₁ B₁<GOAL>Module.Finite A₂ B₂
<VAR>R : Type u_6<VAR>M : Type u_7<VAR>Ring R<VAR>Nontrivial R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_8<VAR>Module.Finite R M<VAR>b : Basis ι R M<GOAL>Finite ι
<VAR>A : Type u_1<VAR>CommRing A<GOAL>(RingHom.id A).Finite
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>CommRing B<VAR>f : A →+* B<VAR>hf : Function.Surjective ⇑f<GOAL>f.Finite
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>CommRing C<VAR>g : B →+* C<VAR>f : A →+* B<VAR>hg : g.Finite<VAR>hf : f.Finite<GOAL>(g.comp f).Finite
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>CommRing C<VAR>f : A →+* B<VAR>g : B →+* C<VAR>h : (g.comp f).Finite<GOAL>g.Finite
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<GOAL>(AlgHom.id R A).Finite
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>CommRing C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>g : B →ₐ[R] C<VAR>f : A →ₐ[R] B<VAR>hg : g.Finite<VAR>hf : f.Finite<GOAL>(g.comp f).Finite
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Surjective ⇑f<GOAL>f.Finite
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>CommRing C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>f : A →ₐ[R] B<VAR>g : B →ₐ[R] C<VAR>h : (g.comp f).Finite<GOAL>g.Finite
<VAR>R : Type u_1<VAR>Semiring R<VAR>s : Unit →₀ ℕ<VAR>n : ℕ<VAR>h : s () = n<GOAL>PowerSeries.coeff R n = MvPowerSeries.coeff R s
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ ψ : PowerSeries R<VAR>h : ∀ (n : ℕ), (PowerSeries.coeff R n) φ = (PowerSeries.coeff R n) ψ<GOAL>φ = ψ
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ ψ : PowerSeries R<GOAL>φ = ψ ↔ ∀ (n : ℕ), (PowerSeries.coeff R n) φ = (PowerSeries.coeff R n) ψ
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>f : ℕ → R<GOAL>(PowerSeries.coeff R n) (PowerSeries.mk f) = f n
<VAR>R : Type u_1<VAR>Semiring R<VAR>m n : ℕ<VAR>a : R<GOAL>(PowerSeries.coeff R m) ((PowerSeries.monomial R n) a) = if m = n then a else 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>a : R<GOAL>(PowerSeries.monomial R n) a = PowerSeries.mk fun m => if m = n then a else 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>a : R<GOAL>(PowerSeries.coeff R n) ((PowerSeries.monomial R n) a) = a
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<GOAL>PowerSeries.coeff R n ∘ₗ PowerSeries.monomial R n = LinearMap.id
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<GOAL>Commute φ PowerSeries.X
<VAR>R : Type u_1<VAR>Semiring R<GOAL>⇑(PowerSeries.coeff R 0) = ⇑(PowerSeries.constantCoeff R)
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<GOAL>(PowerSeries.coeff R 0) φ = (PowerSeries.constantCoeff R) φ
<VAR>R : Type u_1<VAR>Semiring R<GOAL>⇑(PowerSeries.monomial R 0) = ⇑(PowerSeries.C R)
<VAR>R : Type u_1<VAR>Semiring R<VAR>a : R<GOAL>(PowerSeries.monomial R 0) a = (PowerSeries.C R) a
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>a : R<GOAL>(PowerSeries.coeff R n) ((PowerSeries.C R) a) = if n = 0 then a else 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>a : R<GOAL>(PowerSeries.coeff R 0) ((PowerSeries.C R) a) = a
<VAR>R : Type u_1<VAR>Semiring R<VAR>a : R<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>(PowerSeries.coeff R n) ((PowerSeries.C R) a) = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>a : R<VAR>n : ℕ<GOAL>(PowerSeries.coeff R (n + 1)) ((PowerSeries.C R) a) = 0
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Function.Injective ⇑(PowerSeries.C R)
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Subsingleton (PowerSeries R) ↔ Subsingleton R
<VAR>R : Type u_1<VAR>Semiring R<GOAL>PowerSeries.X = (PowerSeries.monomial R 1) 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<GOAL>(PowerSeries.coeff R n) PowerSeries.X = if n = 1 then 1 else 0
<VAR>R : Type u_1<VAR>Semiring R<GOAL>(PowerSeries.coeff R 0) PowerSeries.X = 0
<VAR>R : Type u_1<VAR>Semiring R<GOAL>(PowerSeries.coeff R 1) PowerSeries.X = 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>Nontrivial R<GOAL>PowerSeries.X ≠ 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<GOAL>PowerSeries.X ^ n = (PowerSeries.monomial R n) 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>m n : ℕ<GOAL>(PowerSeries.coeff R m) (PowerSeries.X ^ n) = if m = n then 1 else 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<GOAL>(PowerSeries.coeff R n) (PowerSeries.X ^ n) = 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<GOAL>(PowerSeries.coeff R n) 1 = if n = 0 then 1 else 0
<VAR>R : Type u_1<VAR>Semiring R<GOAL>(PowerSeries.coeff R 0) 1 = 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>φ ψ : PowerSeries R<GOAL>(PowerSeries.coeff R n) (φ * ψ) = ∑ p ∈ Finset.antidiagonal n, (PowerSeries.coeff R p.1) φ * (PowerSeries.coeff R p.2) ψ
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>φ : PowerSeries R<VAR>a : R<GOAL>(PowerSeries.coeff R n) (φ * (PowerSeries.C R) a) = (PowerSeries.coeff R n) φ * a
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>φ : PowerSeries R<VAR>a : R<GOAL>(PowerSeries.coeff R n) ((PowerSeries.C R) a * φ) = a * (PowerSeries.coeff R n) φ
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>Module R S<VAR>n : ℕ<VAR>φ : PowerSeries S<VAR>a : R<GOAL>(PowerSeries.coeff S n) (a • φ) = a • (PowerSeries.coeff S n) φ
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>Module R S<VAR>φ : PowerSeries S<VAR>a : R<GOAL>(PowerSeries.constantCoeff S) (a • φ) = a • (PowerSeries.constantCoeff S) φ
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : PowerSeries R<VAR>a : R<GOAL>a • f = (PowerSeries.C R) a * f
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>φ : PowerSeries R<GOAL>(PowerSeries.coeff R (n + 1)) (φ * PowerSeries.X) = (PowerSeries.coeff R n) φ
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>φ : PowerSeries R<GOAL>(PowerSeries.coeff R (n + 1)) (PowerSeries.X * φ) = (PowerSeries.coeff R n) φ
<VAR>R : Type u_1<VAR>Semiring R<VAR>a : R<GOAL>(PowerSeries.constantCoeff R) ((PowerSeries.C R) a) = a
<VAR>R : Type u_1<VAR>Semiring R<GOAL>(PowerSeries.constantCoeff R).comp (PowerSeries.C R) = RingHom.id R
<VAR>R : Type u_1<VAR>Semiring R<GOAL>(PowerSeries.constantCoeff R) 0 = 0
<VAR>R : Type u_1<VAR>Semiring R<GOAL>(PowerSeries.constantCoeff R) 1 = 1
<VAR>R : Type u_1<VAR>Semiring R<GOAL>(PowerSeries.constantCoeff R) PowerSeries.X = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : ℕ → R<GOAL>(PowerSeries.constantCoeff R) (PowerSeries.mk f) = f 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<GOAL>(PowerSeries.coeff R 0) (φ * PowerSeries.X) = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<GOAL>(PowerSeries.coeff R 0) (PowerSeries.X * φ) = 0
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Function.Surjective ⇑(PowerSeries.constantCoeff R)
<VAR>R : Type u_1<VAR>Semiring R<VAR>x : R<VAR>k n : ℕ<GOAL>(PowerSeries.coeff R n) ((PowerSeries.C R) x * PowerSeries.X ^ k) = if n = k then x else 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : PowerSeries R<VAR>n d : ℕ<GOAL>(PowerSeries.coeff R (d + n)) (p * PowerSeries.X ^ n) = (PowerSeries.coeff R d) p
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : PowerSeries R<VAR>n d : ℕ<GOAL>(PowerSeries.coeff R (d + n)) (PowerSeries.X ^ n * p) = (PowerSeries.coeff R d) p
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : PowerSeries R<VAR>n d : ℕ<GOAL>(PowerSeries.coeff R d) (p * PowerSeries.X ^ n) = if n ≤ d then (PowerSeries.coeff R (d - n)) p else 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : PowerSeries R<VAR>n d : ℕ<GOAL>(PowerSeries.coeff R d) (PowerSeries.X ^ n * p) = if n ≤ d then (PowerSeries.coeff R (d - n)) p else 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<VAR>h : IsUnit φ<GOAL>IsUnit ((PowerSeries.constantCoeff R) φ)
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<GOAL>φ = (PowerSeries.mk fun p => (PowerSeries.coeff R (p + 1)) φ) * PowerSeries.X + (PowerSeries.C R) ((PowerSeries.constantCoeff R) φ)
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<GOAL>φ = (PowerSeries.X * PowerSeries.mk fun p => (PowerSeries.coeff R (p + 1)) φ) + (PowerSeries.C R) ((PowerSeries.constantCoeff R) φ)
<VAR>R : Type u_1<VAR>Semiring R<GOAL>⇑(PowerSeries.map (RingHom.id R)) = id
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>T : Type u_3<VAR>Semiring S<VAR>Semiring T<VAR>f : R →+* S<VAR>g : S →+* T<GOAL>PowerSeries.map (g.comp f) = (PowerSeries.map g).comp (PowerSeries.map f)
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>φ : PowerSeries R<GOAL>(PowerSeries.coeff S n) ((PowerSeries.map f) φ) = f ((PowerSeries.coeff R n) φ)
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>f : R →+* S<VAR>r : R<GOAL>(PowerSeries.map f) ((PowerSeries.C R) r) = (PowerSeries.C S) (f r)