ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>self : M →ₗ⁅R,L⁆ N<VAR>x : L<VAR>m : M<GOAL>(↑self).toFun ⁅x, m⁆ = ⁅x, (↑self).toFun m⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<GOAL>⇑↑f = ⇑f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<VAR>c : R<VAR>x : M<GOAL>f (c • x) = c • f x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<VAR>x y : M<GOAL>f (x + y) = f x + f y
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<VAR>x y : M<GOAL>f (x - y) = f x - f y
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<VAR>x : M<GOAL>f (-x) = -f x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<VAR>x : L<VAR>m : M<GOAL>f ⁅x, m⁆ = ⁅x, f m⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>LieRingModule L P<VAR>LieModule R L N<VAR>LieModule R L P<VAR>f : M →ₗ⁅R,L⁆ N →ₗ[R] P<VAR>x : L<VAR>m : M<VAR>n : N<GOAL>⁅x, (f m) n⁆ = (f ⁅x, m⁆) n + (f m) ⁅x, n⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<GOAL>f 0 = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<GOAL>⇑LieModuleHom.id = id
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>x : M<GOAL>LieModuleHom.id x = x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<GOAL>⇑0 = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>m : M<GOAL>0 m = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<GOAL>Function.Injective DFunLike.coe
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f g : M →ₗ⁅R,L⁆ N<VAR>h : ∀ (m : M), f m = g m<GOAL>f = g
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f g : M →ₗ⁅R,L⁆ N<GOAL>f = g ↔ ∀ (m : M), f m = g m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f g : M →ₗ⁅R,L⁆ N<VAR>h : f = g<VAR>x : M<GOAL>f x = g x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<VAR>h : ∀ {x : L} {m : M}, (↑f).toFun ⁅x, m⁆ = ⁅x, (↑f).toFun m⁆<GOAL>{ toLinearMap := ↑f, map_lie' := h } = f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f : M →ₗ[R] N<VAR>h : ∀ {x : L} {m : M}, f.toFun ⁅x, m⁆ = ⁅x, f.toFun m⁆<GOAL>⇑{ toLinearMap := f, map_lie' := h } = ⇑f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f : M →ₗ[R] N<VAR>h : ∀ {x : L} {m : M}, f.toFun ⁅x, m⁆ = ⁅x, f.toFun m⁆<GOAL>↑{ toLinearMap := f, map_lie' := h } = f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>LieRingModule L P<VAR>f : N →ₗ⁅R,L⁆ P<VAR>g : M →ₗ⁅R,L⁆ N<VAR>m : M<GOAL>(f.comp g) m = f (g m)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>LieRingModule L P<VAR>f : N →ₗ⁅R,L⁆ P<VAR>g : M →ₗ⁅R,L⁆ N<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>LieRingModule L P<VAR>f : N →ₗ⁅R,L⁆ P<VAR>g : M →ₗ⁅R,L⁆ N<GOAL>↑(f.comp g) = ↑f ∘ₗ ↑g
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f g : M →ₗ⁅R,L⁆ N<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f g : M →ₗ⁅R,L⁆ N<VAR>m : M<GOAL>(f + g) m = f m + g m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f g : M →ₗ⁅R,L⁆ N<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f g : M →ₗ⁅R,L⁆ N<VAR>m : M<GOAL>(f - g) m = f m - g m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<GOAL>⇑(-f) = -⇑f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<VAR>m : M<GOAL>(-f) m = -f m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>n : ℕ<VAR>f : M →ₗ⁅R,L⁆ N<GOAL>⇑(n • f) = n • ⇑f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>n : ℕ<VAR>f : M →ₗ⁅R,L⁆ N<VAR>m : M<GOAL>(n • f) m = n • f m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>z : ℤ<VAR>f : M →ₗ⁅R,L⁆ N<GOAL>⇑(z • f) = z • ⇑f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>z : ℤ<VAR>f : M →ₗ⁅R,L⁆ N<VAR>m : M<GOAL>(z • f) m = z • f m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>LieModule R L N<VAR>t : R<VAR>f : M →ₗ⁅R,L⁆ N<GOAL>⇑(t • f) = t • ⇑f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>LieModule R L N<VAR>t : R<VAR>f : M →ₗ⁅R,L⁆ N<VAR>m : M<GOAL>(t • f) m = t • f m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>self : M ≃ₗ⁅R,L⁆ N<GOAL>Function.RightInverse self.invFun (↑self.toLieModuleHom).toFun
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>self : M ≃ₗ⁅R,L⁆ N<GOAL>Function.LeftInverse self.invFun (↑self.toLieModuleHom).toFun
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>e : M ≃ₗ⁅R,L⁆ N<GOAL>⇑e.toLieModuleHom = ⇑e
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>e : M ≃ₗ⁅R,L⁆ N<GOAL>Function.Injective ⇑e
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>e : M ≃ₗ⁅R,L⁆ N<GOAL>Function.Surjective ⇑e
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<VAR>g : N → M<VAR>h₁ : Function.LeftInverse g (↑f).toFun<VAR>h₂ : Function.RightInverse g (↑f).toFun<GOAL>{ toLieModuleHom := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toEquiv = { toFun := ⇑f, invFun := g, left_inv := h₁, right_inv := h₂ }
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<VAR>invFun : N → M<VAR>h₁ : Function.LeftInverse invFun (↑f).toFun<VAR>h₂ : Function.RightInverse invFun (↑f).toFun<GOAL>⇑{ toLieModuleHom := f, invFun := invFun, left_inv := h₁, right_inv := h₂ } = ⇑f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>e : M ≃ₗ⁅R,L⁆ N<GOAL>⇑e.toLinearEquiv = ⇑e
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<GOAL>Function.Injective LieModuleEquiv.toEquiv
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>e₁ e₂ : M ≃ₗ⁅R,L⁆ N<VAR>h : ∀ (m : M), e₁ m = e₂ m<GOAL>e₁ = e₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>m : M<GOAL>1 m = m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>m : M<GOAL>LieModuleEquiv.refl m = m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>e : M ≃ₗ⁅R,L⁆ N<VAR>x : N<GOAL>e (e.symm x) = x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>e : M ≃ₗ⁅R,L⁆ N<VAR>x : M<GOAL>e.symm (e x) = x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>m : M<VAR>n : N<VAR>e : M ≃ₗ⁅R,L⁆ N<GOAL>e m = n ↔ m = e.symm n
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>e : M ≃ₗ⁅R,L⁆ N<GOAL>e.symm.symm = e
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<GOAL>Function.Bijective LieModuleEquiv.symm
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>LieRingModule L P<VAR>e₁ : M ≃ₗ⁅R,L⁆ N<VAR>e₂ : N ≃ₗ⁅R,L⁆ P<VAR>m : M<GOAL>(e₁.trans e₂) m = e₂ (e₁ m)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>LieRingModule L P<VAR>e₁ : M ≃ₗ⁅R,L⁆ N<VAR>e₂ : N ≃ₗ⁅R,L⁆ P<GOAL>(e₁.trans e₂).symm = e₂.symm.trans e₁.symm
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>e : M ≃ₗ⁅R,L⁆ N<GOAL>e.trans e.symm = LieModuleEquiv.refl
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>LieRingModule L M<VAR>LieRingModule L N<VAR>e : M ≃ₗ⁅R,L⁆ N<GOAL>e.symm.trans e = LieModuleEquiv.refl
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>ε : α<VAR>ε0 : 0 < ε<GOAL>∃ δ > 0, ∀ {a₁ a₂ b₁ b₂ : β}, abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ + a₂ - (b₁ + b₂)) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>ε K₁ K₂ : α<VAR>ε0 : 0 < ε<GOAL>∃ δ > 0, ∀ {a₁ a₂ b₁ b₂ : β}, abv a₁ < K₁ → abv b₂ < K₂ → abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ * a₂ - b₁ * b₂) < ε
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_3<VAR>DivisionRing β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>ε K : α<VAR>ε0 : 0 < ε<VAR>K0 : 0 < K<GOAL>∃ δ > 0, ∀ {a b : β}, K ≤ abv a → K ≤ abv b → abv (a - b) < δ → abv (a⁻¹ - b⁻¹) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : ℕ → β<VAR>hf : IsCauSeq abv f<VAR>ε : α<VAR>ε0 : 0 < ε<GOAL>∃ i, ∀ j ≥ i, ∀ k ≥ i, abv (f j - f k) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : ℕ → β<VAR>hf : IsCauSeq abv f<VAR>ε : α<VAR>ε0 : 0 < ε<GOAL>∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - f j) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : ℕ → β<VAR>hf : IsCauSeq abv f<GOAL>∃ r, ∀ (i : ℕ), abv (f i) < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : ℕ → β<VAR>hf : IsCauSeq abv f<VAR>x : α<GOAL>∃ r > x, ∀ (i : ℕ), abv (f i) < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x : β<GOAL>IsCauSeq abv fun x_1 => x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>hf : IsCauSeq abv f<VAR>hg : IsCauSeq abv g<GOAL>IsCauSeq abv (f + g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>hf : IsCauSeq abv f<VAR>hg : IsCauSeq abv g<GOAL>IsCauSeq abv (f * g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : ℕ → β<GOAL>IsCauSeq abv (-f) ↔ IsCauSeq abv f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>f g : CauSeq β abv<VAR>h : ∀ (i : ℕ), ↑f i = ↑g i<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>f : CauSeq β abv<GOAL>IsCauSeq abv ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>f : CauSeq β abv<VAR>ε : α<GOAL>0 < ε → ∃ i, ∀ j ≥ i, abv (↑f j - ↑f i) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>ε : α<GOAL>0 < ε → ∃ i, ∀ j ≥ i, ∀ k ≥ i, abv (↑f j - ↑f k) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>ε : α<GOAL>0 < ε → ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (↑f k - ↑f j) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<GOAL>∃ r, ∀ (i : ℕ), abv (↑f i) < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>x : α<GOAL>∃ r > x, ∀ (i : ℕ), abv (↑f i) < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : CauSeq β abv<GOAL>↑(f + g) = ↑f + ↑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>i : ℕ<GOAL>↑(f + g) i = ↑f i + ↑g i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x : β<GOAL>↑(CauSeq.const abv x) = Function.const ℕ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x : β<VAR>i : ℕ<GOAL>↑(CauSeq.const abv x) i = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x y : β<GOAL>CauSeq.const abv x = CauSeq.const abv y ↔ x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<GOAL>↑0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<GOAL>↑1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>i : ℕ<GOAL>↑0 i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>i : ℕ<GOAL>↑1 i = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<GOAL>CauSeq.const abv 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<GOAL>CauSeq.const abv 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x y : β<GOAL>CauSeq.const abv (x + y) = CauSeq.const abv x + CauSeq.const abv y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : CauSeq β abv<GOAL>↑(f * g) = ↑f * ↑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>i : ℕ<GOAL>↑(f * g) i = ↑f i * ↑g i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x y : β<GOAL>CauSeq.const abv (x * y) = CauSeq.const abv x * CauSeq.const abv y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<GOAL>↑(-f) = -↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>i : ℕ<GOAL>↑(-f) i = -↑f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x : β<GOAL>CauSeq.const abv (-x) = -CauSeq.const abv x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : CauSeq β abv<GOAL>↑(f - g) = ↑f - ↑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>i : ℕ<GOAL>↑(f - g) i = ↑f i - ↑g i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x y : β<GOAL>CauSeq.const abv (x - y) = CauSeq.const abv x - CauSeq.const abv y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>G : Type u_3<VAR>SMul G β<VAR>IsScalarTower G β β<VAR>a : G<VAR>f : CauSeq β abv<GOAL>↑(a • f) = a • ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>G : Type u_3<VAR>SMul G β<VAR>IsScalarTower G β β<VAR>a : G<VAR>f : CauSeq β abv<VAR>i : ℕ<GOAL>↑(a • f) i = a • ↑f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>G : Type u_3<VAR>SMul G β<VAR>IsScalarTower G β β<VAR>a : G<VAR>x : β<GOAL>CauSeq.const abv (a • x) = a • CauSeq.const abv x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>n : ℕ<GOAL>↑(f ^ n) = ↑f ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>n i : ℕ<GOAL>↑(f ^ n) i = ↑f i ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x : β<VAR>n : ℕ<GOAL>CauSeq.const abv (x ^ n) = CauSeq.const abv x ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hf : f.LimZero<VAR>hg : g.LimZero<GOAL>(f + g).LimZero
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>g : CauSeq β abv<VAR>hg : g.LimZero<GOAL>(f * g).LimZero
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>g : CauSeq β abv<VAR>hg : f.LimZero<GOAL>(f * g).LimZero
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : f.LimZero<GOAL>(-f).LimZero
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hf : f.LimZero<VAR>hg : g.LimZero<GOAL>(f - g).LimZero