ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>Add M<VAR>S : AddSubsemigroup M<GOAL>S = ⊤ ↔ ∀ (x : M), x ∈ S
<VAR>M : Type u_1<VAR>Mul M<VAR>S : Subsemigroup M<GOAL>S = ⊤ ↔ ∀ (x : M), x ∈ S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>g : N → M<VAR>h : Function.LeftInverse g ⇑f<VAR>a : M<GOAL>(AddEquiv.ofLeftInverse f h) a = f.srangeRestrict a
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>g : N → M<VAR>h : Function.LeftInverse g ⇑f<GOAL>∀ (a : ↥f.srange), (AddEquiv.ofLeftInverse f h).symm a = g ↑a
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>g : N → M<VAR>h : Function.LeftInverse g ⇑f<GOAL>∀ (a : ↥f.srange), (MulEquiv.ofLeftInverse f h).symm a = g ↑a
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>g : N → M<VAR>h : Function.LeftInverse g ⇑f<VAR>a : M<GOAL>(MulEquiv.ofLeftInverse f h) a = f.srangeRestrict a
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>e : M ≃+ N<VAR>S : AddSubsemigroup M<VAR>x : ↥(AddSubsemigroup.map (↑e) S)<GOAL>↑((e.subsemigroupMap S).symm x) = e.symm ↑x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>e : M ≃+ N<VAR>S : AddSubsemigroup M<VAR>x : ↥S<GOAL>↑((e.subsemigroupMap S) x) = e ↑x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>e : M ≃* N<VAR>S : Subsemigroup M<VAR>x : ↥(Subsemigroup.map (↑e) S)<GOAL>↑((e.subsemigroupMap S).symm x) = e.symm ↑x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>e : M ≃* N<VAR>S : Subsemigroup M<VAR>x : ↥S<GOAL>↑((e.subsemigroupMap S) x) = e ↑x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>S : Subsemigroup N<GOAL>Subsemigroup.map f (Subsemigroup.comap f S) = S ⊓ f.srange
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>S : AddSubsemigroup N<GOAL>AddSubsemigroup.map f (AddSubsemigroup.comap f S) = S ⊓ f.srange
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>S : Subsemigroup N<VAR>h : S ≤ f.srange<GOAL>Subsemigroup.map f (Subsemigroup.comap f S) = S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>S : AddSubsemigroup N<VAR>h : S ≤ f.srange<GOAL>AddSubsemigroup.map f (AddSubsemigroup.comap f S) = S
<VAR>G : Type u_10<VAR>AddGroup G<VAR>x : G<GOAL>↑(toAddUnits x) = x
<VAR>G : Type u_10<VAR>Group G<VAR>x : G<GOAL>↑(toUnits x) = x
<VAR>G : Type u_10<VAR>Group G<VAR>x : Gˣ<GOAL>toUnits.symm x = ↑x
<VAR>G : Type u_10<VAR>AddGroup G<VAR>x : AddUnits G<GOAL>toAddUnits.symm x = ↑x
<VAR>G : Type u_12<VAR>AddGroup G<VAR>x : AddUnits G<GOAL>toAddUnits ↑x = x
<VAR>G : Type u_12<VAR>Group G<VAR>x : Gˣ<GOAL>toUnits ↑x = x
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Monoid M<VAR>Monoid N<VAR>h : M ≃* N<GOAL>(Units.mapEquiv h).symm = Units.mapEquiv h.symm
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Monoid M<VAR>Monoid N<VAR>h : M ≃* N<VAR>x : Mˣ<GOAL>↑((Units.mapEquiv h) x) = h ↑x
<VAR>M : Type u_6<VAR>AddMonoid M<VAR>u : AddUnits M<GOAL>⇑u.addLeft = fun x => ↑u + x
<VAR>M : Type u_6<VAR>Monoid M<VAR>u : Mˣ<GOAL>⇑u.mulLeft = fun x => ↑u * x
<VAR>M : Type u_6<VAR>Monoid M<VAR>u : Mˣ<GOAL>Equiv.symm u.mulLeft = u⁻¹.mulLeft
<VAR>M : Type u_6<VAR>AddMonoid M<VAR>u : AddUnits M<GOAL>Equiv.symm u.addLeft = (-u).addLeft
<VAR>M : Type u_6<VAR>Monoid M<VAR>a : Mˣ<GOAL>Function.Bijective fun x => ↑a * x
<VAR>M : Type u_6<VAR>AddMonoid M<VAR>a : AddUnits M<GOAL>Function.Bijective fun x => ↑a + x
<VAR>M : Type u_6<VAR>Monoid M<VAR>u : Mˣ<GOAL>⇑u.mulRight = fun x => x * ↑u
<VAR>M : Type u_6<VAR>AddMonoid M<VAR>u : AddUnits M<GOAL>⇑u.addRight = fun x => x + ↑u
<VAR>M : Type u_6<VAR>Monoid M<VAR>u : Mˣ<GOAL>Equiv.symm u.mulRight = u⁻¹.mulRight
<VAR>M : Type u_6<VAR>AddMonoid M<VAR>u : AddUnits M<GOAL>Equiv.symm u.addRight = (-u).addRight
<VAR>M : Type u_6<VAR>AddMonoid M<VAR>a : AddUnits M<GOAL>Function.Bijective fun x => x + ↑a
<VAR>M : Type u_6<VAR>Monoid M<VAR>a : Mˣ<GOAL>Function.Bijective fun x => x * ↑a
<VAR>G : Type u_10<VAR>Group G<VAR>a : G<GOAL>⇑(Equiv.mulLeft a) = fun x => a * x
<VAR>G : Type u_10<VAR>AddGroup G<VAR>a : G<GOAL>⇑(Equiv.addLeft a) = fun x => a + x
<VAR>G : Type u_10<VAR>AddGroup G<VAR>a : G<GOAL>⇑(Equiv.symm (Equiv.addLeft a)) = fun x => -a + x
<VAR>G : Type u_10<VAR>Group G<VAR>a : G<GOAL>⇑(Equiv.symm (Equiv.mulLeft a)) = fun x => a⁻¹ * x
<VAR>G : Type u_10<VAR>Group G<VAR>a : G<GOAL>Equiv.symm (Equiv.mulLeft a) = Equiv.mulLeft a⁻¹
<VAR>G : Type u_10<VAR>AddGroup G<VAR>a : G<GOAL>Equiv.symm (Equiv.addLeft a) = Equiv.addLeft (-a)
<VAR>G : Type u_10<VAR>Group G<VAR>a : G<GOAL>Function.Bijective fun x => a * x
<VAR>G : Type u_10<VAR>AddGroup G<VAR>a : G<GOAL>Function.Bijective fun x => a + x
<VAR>G : Type u_10<VAR>Group G<VAR>a : G<GOAL>⇑(Equiv.mulRight a) = fun x => x * a
<VAR>G : Type u_10<VAR>AddGroup G<VAR>a : G<GOAL>⇑(Equiv.addRight a) = fun x => x + a
<VAR>G : Type u_10<VAR>AddGroup G<VAR>a : G<GOAL>Equiv.symm (Equiv.addRight a) = Equiv.addRight (-a)
<VAR>G : Type u_10<VAR>Group G<VAR>a : G<GOAL>Equiv.symm (Equiv.mulRight a) = Equiv.mulRight a⁻¹
<VAR>G : Type u_10<VAR>AddGroup G<VAR>a : G<GOAL>⇑(Equiv.symm (Equiv.addRight a)) = fun x => x + -a
<VAR>G : Type u_10<VAR>Group G<VAR>a : G<GOAL>⇑(Equiv.symm (Equiv.mulRight a)) = fun x => x * a⁻¹
<VAR>G : Type u_10<VAR>Group G<VAR>a : G<GOAL>Function.Bijective fun x => x * a
<VAR>G : Type u_10<VAR>AddGroup G<VAR>a : G<GOAL>Function.Bijective fun x => x + a
<VAR>G : Type u_10<VAR>Group G<VAR>a b : G<GOAL>(Equiv.divLeft a) b = a / b
<VAR>G : Type u_10<VAR>AddGroup G<VAR>a b : G<GOAL>(Equiv.subLeft a).symm b = -b + a
<VAR>G : Type u_10<VAR>AddGroup G<VAR>a b : G<GOAL>(Equiv.subLeft a) b = a - b
<VAR>G : Type u_10<VAR>Group G<VAR>a b : G<GOAL>(Equiv.divLeft a).symm b = b⁻¹ * a
<VAR>G : Type u_10<VAR>AddGroup G<VAR>a : G<GOAL>Equiv.subLeft a = Equiv.trans (Equiv.neg G) (Equiv.addLeft a)
<VAR>G : Type u_10<VAR>Group G<VAR>a : G<GOAL>Equiv.divLeft a = Equiv.trans (Equiv.inv G) (Equiv.mulLeft a)
<VAR>G : Type u_10<VAR>AddGroup G<VAR>a b : G<GOAL>(Equiv.subRight a).symm b = b + a
<VAR>G : Type u_10<VAR>AddGroup G<VAR>a b : G<GOAL>(Equiv.subRight a) b = b - a
<VAR>G : Type u_10<VAR>Group G<VAR>a b : G<GOAL>(Equiv.divRight a).symm b = b * a
<VAR>G : Type u_10<VAR>Group G<VAR>a b : G<GOAL>(Equiv.divRight a) b = b / a
<VAR>G : Type u_10<VAR>Group G<VAR>a : G<GOAL>Equiv.divRight a = Equiv.mulRight a⁻¹
<VAR>G : Type u_10<VAR>AddGroup G<VAR>a : G<GOAL>Equiv.subRight a = Equiv.addRight (-a)
<VAR>α : Type u_2<VAR>Monoid α<VAR>p : { p // p.1 * p.2 = 1 ∧ p.2 * p.1 = 1 }<GOAL>↑((unitsEquivProdSubtype α).symm p)⁻¹ = (↑p).2
<VAR>α : Type u_2<VAR>Monoid α<VAR>u : αˣ<GOAL>↑((unitsEquivProdSubtype α) u) = (↑u, ↑u⁻¹)
<VAR>α : Type u_2<VAR>Monoid α<VAR>p : { p // p.1 * p.2 = 1 ∧ p.2 * p.1 = 1 }<GOAL>↑((unitsEquivProdSubtype α).symm p) = (↑p).1
<VAR>G : Type u_12<VAR>DivisionCommMonoid G<GOAL>∀ (a : G), (MulEquiv.inv G) a = a⁻¹
<VAR>G : Type u_12<VAR>SubtractionCommMonoid G<GOAL>∀ (a : G), (AddEquiv.neg G) a = -a
<VAR>G : Type u_12<VAR>SubtractionCommMonoid G<GOAL>(AddEquiv.neg G).symm = AddEquiv.neg G
<VAR>G : Type u_12<VAR>DivisionCommMonoid G<GOAL>(MulEquiv.inv G).symm = MulEquiv.inv G
<VAR>F : Type u_1<VAR>M : Type u_12<VAR>N : Type u_13<VAR>AddMonoid M<VAR>AddMonoid N<VAR>EquivLike F M N<VAR>AddMonoidHomClass F M N<VAR>f : F<VAR>m : M<GOAL>IsAddUnit (f m) ↔ IsAddUnit m
<VAR>F : Type u_1<VAR>M : Type u_12<VAR>N : Type u_13<VAR>Monoid M<VAR>Monoid N<VAR>EquivLike F M N<VAR>MonoidHomClass F M N<VAR>f : F<VAR>m : M<GOAL>IsUnit (f m) ↔ IsUnit m
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>R : Type u_4<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>N₁ : ι → Submodule R M₁<VAR>h₁ : DirectSum.IsInternal N₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>N₂ : ι → Submodule R M₂<VAR>h₂ : DirectSum.IsInternal N₂<VAR>κ₁ : ι → Type u_7<VAR>κ₂ : ι → Type u_8<VAR>(i : ι) → Fintype (κ₁ i)<VAR>∀ (i : ι), Finite (κ₂ i)<VAR>(i : ι) → DecidableEq (κ₁ i)<VAR>Fintype ι<VAR>b₁ : (i : ι) → Basis (κ₁ i) R ↥(N₁ i)<VAR>b₂ : (i : ι) → Basis (κ₂ i) R ↥(N₂ i)<VAR>f : M₁ →ₗ[R] M₂<VAR>hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N₁ i) ↑(N₂ i)<GOAL>(LinearMap.toMatrix (h₁.collectedBasis b₁) (h₂.collectedBasis b₂)) f = Matrix.blockDiagonal' fun i => (LinearMap.toMatrix (b₁ i) (b₂ i)) (f.restrict ⋯)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : ι → Submodule R M<VAR>DecidableEq ι<VAR>κ : ι → Type u_4<VAR>(i : ι) → Fintype (κ i)<VAR>(i : ι) → DecidableEq (κ i)<VAR>s : Finset ι<VAR>h : DirectSum.IsInternal fun i => N ↑i<VAR>b : (i : { x // x ∈ s }) → Basis (κ ↑i) R ↥(N ↑i)<VAR>σ : ι → ι<VAR>hσ : ∀ (i : ι), σ i ≠ i<VAR>f : Module.End R M<VAR>hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N (σ i))<VAR>hN : ∀ i ∉ s, N i = ⊥<GOAL>((LinearMap.toMatrix (h.collectedBasis b) (h.collectedBasis b)) f).diag = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : ι → Submodule R M<VAR>DecidableEq ι<VAR>h : DirectSum.IsInternal N<VAR>∀ (i : ι), Module.Finite R ↥(N i)<VAR>∀ (i : ι), Module.Free R ↥(N i)<VAR>Fintype ι<VAR>f : M →ₗ[R] M<VAR>hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N i)<GOAL>(LinearMap.trace R M) f = ∑ i : ι, (LinearMap.trace R ↥(N i)) (f.restrict ⋯)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : ι → Submodule R M<VAR>DecidableEq ι<VAR>h : DirectSum.IsInternal N<VAR>∀ (i : ι), Module.Finite R ↥(N i)<VAR>∀ (i : ι), Module.Free R ↥(N i)<VAR>hN : {i | N i ≠ ⊥}.Finite<VAR>f : M →ₗ[R] M<VAR>hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N i)<GOAL>(LinearMap.trace R M) f = ∑ i ∈ hN.toFinset, (LinearMap.trace R ↥(N i)) (f.restrict ⋯)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : ι → Submodule R M<VAR>DecidableEq ι<VAR>h : DirectSum.IsInternal N<VAR>∀ (i : ι), Module.Finite R ↥(N i)<VAR>∀ (i : ι), Module.Free R ↥(N i)<VAR>IsNoetherian R M<VAR>σ : ι → ι<VAR>hσ : ∀ (i : ι), σ i ≠ i<VAR>f : Module.End R M<VAR>hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N (σ i))<GOAL>(LinearMap.trace R M) f = 0
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>f g : Module.End R M<VAR>h_comm : Commute f g<VAR>hf : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<VAR>hg : ∀ (μ : R), (LinearMap.trace R ↥(⨆ k, (f.genEigenspace μ) k)) (LinearMap.restrict g ⋯) = 0<GOAL>(LinearMap.trace R M) (g ∘ₗ f) = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : ι → Submodule R M<VAR>s : Set ι<VAR>f : Module.End R M<VAR>hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N i)<GOAL>Set.MapsTo ⇑f ↑(⨆ i ∈ s, N i) ↑(⨆ i ∈ s, N i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : ι → Submodule R M<VAR>∀ (i : ι), Module.Finite R ↥(N i)<VAR>∀ (i : ι), Module.Free R ↥(N i)<VAR>s : Finset ι<VAR>h : CompleteLattice.Independent fun i => N ↑i<VAR>f : Module.End R M<VAR>hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N i)<VAR>p : Submodule R M<VAR>hp : p = ⨆ i ∈ s, N i<VAR>hp' : Set.MapsTo ⇑f ↑p ↑p := ⋯<GOAL>(LinearMap.trace R ↥p) (LinearMap.restrict f hp') = ∑ i ∈ s, (LinearMap.trace R ↥(N i)) (LinearMap.restrict f ⋯)
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>M M' : ModuleCat S<VAR>g : M ⟶ M'<VAR>x : ↑((ModuleCat.restrictScalars f).obj M)<GOAL>((ModuleCat.restrictScalars f).map g) x = g x
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>M : ModuleCat S<VAR>r : R<VAR>m : ↑((ModuleCat.restrictScalars f).obj M)<GOAL>r • m = f r • m
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>M : ModuleCat S<VAR>r : R<VAR>m : ↑M<GOAL>let m' := m;
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>M : ModuleCat R<VAR>N : ModuleCat S<VAR>g : ↑M →ₛₗ[f] ↑N<VAR>a : ↑M<GOAL>((ModuleCat.semilinearMapAddEquiv f M N) g) a = g a
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>M : ModuleCat R<VAR>N : ModuleCat S<VAR>g : M ⟶ (ModuleCat.restrictScalars f).obj N<VAR>a : ↑M<GOAL>((ModuleCat.semilinearMapAddEquiv f M N).symm g) a = g a
<VAR>R : Type u₁<VAR>Ring R<VAR>f : R →+* R<VAR>hf : f = RingHom.id R<VAR>M : ModuleCat R<VAR>x : ↑M<GOAL>(ModuleCat.restrictScalarsId'App f hf M).hom x = x
<VAR>R : Type u₁<VAR>Ring R<VAR>f : R →+* R<VAR>hf : f = RingHom.id R<VAR>M : ModuleCat R<VAR>x : ↑M<GOAL>(ModuleCat.restrictScalarsId'App f hf M).inv x = x
<VAR>R : Type u₁<VAR>Ring R<VAR>f : R →+* R<VAR>hf : f = RingHom.id R<VAR>X : ModuleCat R<GOAL>(ModuleCat.restrictScalarsId' f hf).inv.app X = (ModuleCat.restrictScalarsId'App f hf X).inv
<VAR>R : Type u₁<VAR>Ring R<VAR>f : R →+* R<VAR>hf : f = RingHom.id R<VAR>X : ModuleCat R<GOAL>(ModuleCat.restrictScalarsId' f hf).hom.app X = (ModuleCat.restrictScalarsId'App f hf X).hom
<VAR>R : Type u₁<VAR>Ring R<VAR>f : R →+* R<VAR>hf : f = RingHom.id R<VAR>M N : ModuleCat R<VAR>φ : M ⟶ N<GOAL>(ModuleCat.restrictScalars f).map φ ≫ (ModuleCat.restrictScalarsId'App f hf N).hom = (ModuleCat.restrictScalarsId'App f hf M).hom ≫ φ
<VAR>R : Type u₁<VAR>Ring R<VAR>f : R →+* R<VAR>hf : f = RingHom.id R<VAR>M N : ModuleCat R<VAR>φ : M ⟶ N<GOAL>φ ≫ (ModuleCat.restrictScalarsId'App f hf N).inv = (ModuleCat.restrictScalarsId'App f hf M).inv ≫ (ModuleCat.restrictScalars f).map φ
<VAR>R₁ : Type u₁<VAR>R₂ : Type u₂<VAR>R₃ : Type u₃<VAR>Ring R₁<VAR>Ring R₂<VAR>Ring R₃<VAR>f : R₁ →+* R₂<VAR>g : R₂ →+* R₃<VAR>gf : R₁ →+* R₃<VAR>hgf : gf = g.comp f<VAR>M : ModuleCat R₃<VAR>x : ↑M<GOAL>(ModuleCat.restrictScalarsComp'App f g gf hgf M).hom x = x
<VAR>R₁ : Type u₁<VAR>R₂ : Type u₂<VAR>R₃ : Type u₃<VAR>Ring R₁<VAR>Ring R₂<VAR>Ring R₃<VAR>f : R₁ →+* R₂<VAR>g : R₂ →+* R₃<VAR>gf : R₁ →+* R₃<VAR>hgf : gf = g.comp f<VAR>M : ModuleCat R₃<VAR>x : ↑M<GOAL>(ModuleCat.restrictScalarsComp'App f g gf hgf M).inv x = x
<VAR>R₁ : Type u₁<VAR>R₂ : Type u₂<VAR>R₃ : Type u₃<VAR>Ring R₁<VAR>Ring R₂<VAR>Ring R₃<VAR>f : R₁ →+* R₂<VAR>g : R₂ →+* R₃<VAR>gf : R₁ →+* R₃<VAR>hgf : gf = g.comp f<VAR>X : ModuleCat R₃<GOAL>(ModuleCat.restrictScalarsComp' f g gf hgf).inv.app X = (ModuleCat.restrictScalarsComp'App f g gf hgf X).inv
<VAR>R₁ : Type u₁<VAR>R₂ : Type u₂<VAR>R₃ : Type u₃<VAR>Ring R₁<VAR>Ring R₂<VAR>Ring R₃<VAR>f : R₁ →+* R₂<VAR>g : R₂ →+* R₃<VAR>gf : R₁ →+* R₃<VAR>hgf : gf = g.comp f<VAR>X : ModuleCat R₃<GOAL>(ModuleCat.restrictScalarsComp' f g gf hgf).hom.app X = (ModuleCat.restrictScalarsComp'App f g gf hgf X).hom
<VAR>R₁ : Type u₁<VAR>R₂ : Type u₂<VAR>R₃ : Type u₃<VAR>Ring R₁<VAR>Ring R₂<VAR>Ring R₃<VAR>f : R₁ →+* R₂<VAR>g : R₂ →+* R₃<VAR>gf : R₁ →+* R₃<VAR>hgf : gf = g.comp f<VAR>M N : ModuleCat R₃<VAR>φ : M ⟶ N<GOAL>(ModuleCat.restrictScalars gf).map φ ≫ (ModuleCat.restrictScalarsComp'App f g gf hgf N).hom = (ModuleCat.restrictScalarsComp'App f g gf hgf M).hom ≫ (ModuleCat.restrictScalars f).map ((ModuleCat.restrictScalars g).map φ)
<VAR>R₁ : Type u₁<VAR>R₂ : Type u₂<VAR>R₃ : Type u₃<VAR>Ring R₁<VAR>Ring R₂<VAR>Ring R₃<VAR>f : R₁ →+* R₂<VAR>g : R₂ →+* R₃<VAR>gf : R₁ →+* R₃<VAR>hgf : gf = g.comp f<VAR>M N : ModuleCat R₃<VAR>φ : M ⟶ N<GOAL>(ModuleCat.restrictScalars f).map ((ModuleCat.restrictScalars g).map φ) ≫ (ModuleCat.restrictScalarsComp'App f g gf hgf N).inv = (ModuleCat.restrictScalarsComp'App f g gf hgf M).inv ≫ (ModuleCat.restrictScalars gf).map φ
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>M : ModuleCat R<GOAL>ModuleCat.ExtendScalars.map' f (𝟙 M) = 𝟙 (ModuleCat.ExtendScalars.obj' f M)
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>M₁ M₂ M₃ : ModuleCat R<VAR>l₁₂ : M₁ ⟶ M₂<VAR>l₂₃ : M₂ ⟶ M₃<GOAL>ModuleCat.ExtendScalars.map' f (l₁₂ ≫ l₂₃) = ModuleCat.ExtendScalars.map' f l₁₂ ≫ ModuleCat.ExtendScalars.map' f l₂₃
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>M : ModuleCat R<VAR>s s' : S<VAR>m : ↑M<GOAL>s • s' ⊗ₜ[R] m = (s * s') ⊗ₜ[R] m
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>M M' : ModuleCat R<VAR>g : M ⟶ M'<VAR>s : S<VAR>m : ↑M<GOAL>((ModuleCat.extendScalars f).map g) (s ⊗ₜ[R] m) = s ⊗ₜ[R] g m
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : S<VAR>g : ↑((ModuleCat.restrictScalars f).obj (ModuleCat.mk S)) →ₗ[R] M<VAR>s' : S<GOAL>(s • g) s' = g (s' * s)
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>M M' : ModuleCat R<VAR>g : M ⟶ M'<VAR>h : ↑(ModuleCat.CoextendScalars.obj' f M)<GOAL>(ModuleCat.CoextendScalars.map' f g) h = g ∘ₗ h
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>M : ModuleCat R<VAR>g : ↑((ModuleCat.coextendScalars f).obj M)<VAR>s s' : S<GOAL>(s • g).toFun s' = g.toFun (s' * s)
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>M M' : ModuleCat R<VAR>g : M ⟶ M'<VAR>x : ↑((ModuleCat.coextendScalars f).obj M)<VAR>s : S<GOAL>(((ModuleCat.coextendScalars f).map g) x).toFun s = g (x.toFun s)
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (ModuleCat.restrictScalars f).obj Y ⟶ X<VAR>y : ↑Y<VAR>s : S<GOAL>((ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction f g) y) s = g (s • y)
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : Y ⟶ (ModuleCat.coextendScalars f).obj X<VAR>y : ↑Y<GOAL>(ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction f g) y = (g y).toFun 1
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (ModuleCat.extendScalars f).obj X ⟶ Y<VAR>x : ↑X<GOAL>(ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars f g) x = g (1 ⊗ₜ[R] x)
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>s : S<VAR>g : X ⟶ (ModuleCat.restrictScalars f).obj Y<VAR>x : ↑X<GOAL>(ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) x = s • g x
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : X ⟶ (ModuleCat.restrictScalars f).obj Y<VAR>z : ↑((ModuleCat.extendScalars f).obj X)<GOAL>(ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars f g) z = (TensorProduct.lift { toFun := fun s => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) z
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : X ⟶ (ModuleCat.restrictScalars f).obj Y<GOAL>(ModuleCat.ExtendRestrictScalarsAdj.homEquiv f).symm g = ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars f g
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<GOAL>∀ (x : ModuleCat R), (ModuleCat.ExtendRestrictScalarsAdj.unit f).app x = ModuleCat.ExtendRestrictScalarsAdj.Unit.map f
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>Y : ModuleCat S<VAR>a : TensorProduct R S ↑Y<GOAL>(ModuleCat.ExtendRestrictScalarsAdj.Counit.map f) a = (TensorProduct.lift { toFun := fun s => { toFun := fun y => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) a
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<GOAL>∀ (x : ModuleCat S), (ModuleCat.ExtendRestrictScalarsAdj.counit f).app x = ModuleCat.ExtendRestrictScalarsAdj.Counit.map f
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>N : Type u_3<VAR>DivisionMonoid G<VAR>Monoid N<VAR>FunLike F G N<VAR>MonoidHomClass F G N<VAR>x : G<VAR>hx : IsUnit x<VAR>f g : F<VAR>h : f x = g x<GOAL>f x⁻¹ = g x⁻¹
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>N : Type u_3<VAR>SubtractionMonoid G<VAR>AddMonoid N<VAR>FunLike F G N<VAR>AddMonoidHomClass F G N<VAR>x : G<VAR>hx : IsAddUnit x<VAR>f g : F<VAR>h : f x = g x<GOAL>f (-x) = g (-x)
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>Group G<VAR>Monoid M<VAR>FunLike F G M<VAR>MonoidHomClass F G M<VAR>f g : F<VAR>x : G<VAR>h : f x = g x<GOAL>f x⁻¹ = g x⁻¹
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>AddGroup G<VAR>AddMonoid M<VAR>FunLike F G M<VAR>AddMonoidHomClass F G M<VAR>f g : F<VAR>x : G<VAR>h : f x = g x<GOAL>f (-x) = g (-x)
<VAR>M : Type u<VAR>N : Type v<VAR>AddMonoid M<VAR>AddMonoid N<VAR>f : M →+ N<VAR>x : AddUnits M<GOAL>↑((AddUnits.map f) x) = f ↑x
<VAR>M : Type u<VAR>N : Type v<VAR>Monoid M<VAR>Monoid N<VAR>f : M →* N<VAR>x : Mˣ<GOAL>↑((Units.map f) x) = f ↑x
<VAR>M : Type u<VAR>N : Type v<VAR>AddMonoid M<VAR>AddMonoid N<VAR>f : M →+ N<VAR>u : AddUnits M<GOAL>↑(-(AddUnits.map f) u) = f ↑(-u)
<VAR>M : Type u<VAR>N : Type v<VAR>Monoid M<VAR>Monoid N<VAR>f : M →* N<VAR>u : Mˣ<GOAL>↑((Units.map f) u)⁻¹ = f ↑u⁻¹
<VAR>M : Type u<VAR>N : Type v<VAR>P : Type w<VAR>Monoid M<VAR>Monoid N<VAR>Monoid P<VAR>f : M →* N<VAR>g : N →* P<GOAL>Units.map (g.comp f) = (Units.map g).comp (Units.map f)
<VAR>M : Type u<VAR>N : Type v<VAR>P : Type w<VAR>AddMonoid M<VAR>AddMonoid N<VAR>AddMonoid P<VAR>f : M →+ N<VAR>g : N →+ P<GOAL>AddUnits.map (g.comp f) = (AddUnits.map g).comp (AddUnits.map f)
<VAR>M : Type u<VAR>N : Type v<VAR>AddMonoid M<VAR>AddMonoid N<VAR>f : M →+ N<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective ⇑(AddUnits.map f)
<VAR>M : Type u<VAR>N : Type v<VAR>Monoid M<VAR>Monoid N<VAR>f : M →* N<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective ⇑(Units.map f)
<VAR>M : Type u<VAR>Monoid M<GOAL>Units.map (MonoidHom.id M) = MonoidHom.id Mˣ
<VAR>M : Type u<VAR>AddMonoid M<GOAL>AddUnits.map (AddMonoidHom.id M) = AddMonoidHom.id (AddUnits M)
<VAR>M : Type u<VAR>AddMonoid M<VAR>x : AddUnits M<GOAL>(AddUnits.coeHom M) x = ↑x
<VAR>M : Type u<VAR>Monoid M<VAR>x : Mˣ<GOAL>(Units.coeHom M) x = ↑x
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>u : αˣ<VAR>n : ℤ<GOAL>↑(u ^ n) = ↑u ^ n
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>u : AddUnits α<VAR>n : ℤ<GOAL>↑(n • u) = n • ↑u
<VAR>α : Type u_1<VAR>M : Type u<VAR>AddMonoid M<VAR>SubtractionMonoid α<VAR>F : Type u_2<VAR>FunLike F M α<VAR>AddMonoidHomClass F M α<VAR>f : F<VAR>u : AddUnits M<GOAL>f ↑(-u) = -f ↑u
<VAR>α : Type u_1<VAR>M : Type u<VAR>Monoid M<VAR>DivisionMonoid α<VAR>F : Type u_2<VAR>FunLike F M α<VAR>MonoidHomClass F M α<VAR>f : F<VAR>u : Mˣ<GOAL>f ↑u⁻¹ = (f ↑u)⁻¹
<VAR>M : Type u<VAR>N : Type v<VAR>Monoid M<VAR>Monoid N<VAR>f : M →* N<VAR>g : M → Nˣ<VAR>h : ∀ (x : M), ↑(g x) = f x<VAR>x : M<GOAL>↑((Units.liftRight f g h) x) = f x
<VAR>M : Type u<VAR>N : Type v<VAR>AddMonoid M<VAR>AddMonoid N<VAR>f : M →+ N<VAR>g : M → AddUnits N<VAR>h : ∀ (x : M), ↑(g x) = f x<VAR>x : M<GOAL>↑((AddUnits.liftRight f g h) x) = f x
<VAR>M : Type u<VAR>N : Type v<VAR>AddMonoid M<VAR>AddMonoid N<VAR>f : M →+ N<VAR>g : M → AddUnits N<VAR>h : ∀ (x : M), ↑(g x) = f x<VAR>x : M<GOAL>f x + ↑(-(AddUnits.liftRight f g h) x) = 0
<VAR>M : Type u<VAR>N : Type v<VAR>Monoid M<VAR>Monoid N<VAR>f : M →* N<VAR>g : M → Nˣ<VAR>h : ∀ (x : M), ↑(g x) = f x<VAR>x : M<GOAL>f x * ↑((Units.liftRight f g h) x)⁻¹ = 1
<VAR>M : Type u<VAR>N : Type v<VAR>Monoid M<VAR>Monoid N<VAR>f : M →* N<VAR>g : M → Nˣ<VAR>h : ∀ (x : M), ↑(g x) = f x<VAR>x : M<GOAL>↑((Units.liftRight f g h) x)⁻¹ * f x = 1
<VAR>M : Type u<VAR>N : Type v<VAR>AddMonoid M<VAR>AddMonoid N<VAR>f : M →+ N<VAR>g : M → AddUnits N<VAR>h : ∀ (x : M), ↑(g x) = f x<VAR>x : M<GOAL>↑(-(AddUnits.liftRight f g h) x) + f x = 0
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>Group G<VAR>Monoid M<VAR>f : G →* M<VAR>g : G<GOAL>↑(f.toHomUnits g) = f g
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>AddGroup G<VAR>AddMonoid M<VAR>f : G →+ M<VAR>g : G<GOAL>↑(f.toHomAddUnits g) = f g
<VAR>F : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>FunLike F M N<VAR>AddMonoid M<VAR>AddMonoid N<VAR>AddMonoidHomClass F M N<VAR>f : F<VAR>x : M<VAR>h : IsAddUnit x<GOAL>IsAddUnit (f x)
<VAR>F : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>FunLike F M N<VAR>Monoid M<VAR>Monoid N<VAR>MonoidHomClass F M N<VAR>f : F<VAR>x : M<VAR>h : IsUnit x<GOAL>IsUnit (f x)
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>M : Type u_4<VAR>N : Type u_5<VAR>FunLike F M N<VAR>FunLike G N M<VAR>AddMonoid M<VAR>AddMonoid N<VAR>AddMonoidHomClass G N M<VAR>f : F<VAR>x : M<VAR>g : G<VAR>hfg : Function.LeftInverse ⇑g ⇑f<VAR>h : IsAddUnit (f x)<GOAL>IsAddUnit x