ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : ChainComplex V ℕ<GOAL>C.augmentTruncate.hom.f 0 = 𝟙 (C.X 0)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : ChainComplex V ℕ<VAR>i : ℕ<GOAL>C.augmentTruncate.hom.f (i + 1) = 𝟙 (C.X (i + 1))
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : ChainComplex V ℕ<GOAL>C.augmentTruncate.inv.f 0 = 𝟙 (C.X 0)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : ChainComplex V ℕ<VAR>i : ℕ<GOAL>C.augmentTruncate.inv.f (i + 1) = 𝟙 (C.X (i + 1))
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<VAR>i : ℕ<GOAL>(CochainComplex.truncate.obj C).X i = C.X (i + 1)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<VAR>i j : ℕ<GOAL>(CochainComplex.truncate.obj C).d i j = C.d (i + 1) (j + 1)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>∀ {X Y : CochainComplex V ℕ} (f : X ⟶ Y) (i : ℕ), (CochainComplex.truncate.map f).f i = f.f (i + 1)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<VAR>X : V<VAR>f : X ⟶ C.X 0<VAR>w : f ≫ C.d 0 1 = 0<GOAL>(C.augment f w).X 0 = X
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<VAR>X : V<VAR>f : X ⟶ C.X 0<VAR>w : f ≫ C.d 0 1 = 0<VAR>i : ℕ<GOAL>(C.augment f w).X (i + 1) = C.X i
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<VAR>X : V<VAR>f : X ⟶ C.X 0<VAR>w : f ≫ C.d 0 1 = 0<GOAL>(C.augment f w).d 0 1 = f
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<VAR>X : V<VAR>f : X ⟶ C.X 0<VAR>w : f ≫ C.d 0 1 = 0<VAR>i j : ℕ<GOAL>(C.augment f w).d (i + 1) (j + 1) = C.d i j
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<VAR>X : V<VAR>f : X ⟶ C.X 0<VAR>w : f ≫ C.d 0 1 = 0<VAR>i : ℕ<GOAL>(C.truncateAugment f w).hom.f i = 𝟙 (C.X i)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<VAR>X : V<VAR>f : X ⟶ C.X 0<VAR>w : f ≫ C.d 0 1 = 0<VAR>i : ℕ<GOAL>(C.truncateAugment f w).inv.f i = 𝟙 ((CochainComplex.truncate.obj (C.augment f w)).X i)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<VAR>i : ℕ<GOAL>C.d 0 (i + 2) = 0
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<GOAL>C.augmentTruncate.hom.f 0 = 𝟙 (C.X 0)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<VAR>i : ℕ<GOAL>C.augmentTruncate.hom.f (i + 1) = 𝟙 (C.X (i + 1))
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<GOAL>C.augmentTruncate.inv.f 0 = 𝟙 (C.X 0)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<VAR>i : ℕ<GOAL>C.augmentTruncate.inv.f (i + 1) = 𝟙 (C.X (i + 1))
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>Add ι<VAR>(i : ι) → AddCommMonoid (A i)<VAR>self : DirectSum.GNonUnitalNonAssocSemiring A<VAR>i j : ι<VAR>b : A j<GOAL>GradedMonoid.GMul.mul 0 b = 0
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>Add ι<VAR>(i : ι) → AddCommMonoid (A i)<VAR>self : DirectSum.GNonUnitalNonAssocSemiring A<VAR>i j : ι<VAR>a : A i<VAR>b c : A j<GOAL>GradedMonoid.GMul.mul a (b + c) = GradedMonoid.GMul.mul a b + GradedMonoid.GMul.mul a c
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>Add ι<VAR>(i : ι) → AddCommMonoid (A i)<VAR>self : DirectSum.GNonUnitalNonAssocSemiring A<VAR>i j : ι<VAR>a b : A i<VAR>c : A j<GOAL>GradedMonoid.GMul.mul (a + b) c = GradedMonoid.GMul.mul a c + GradedMonoid.GMul.mul b c
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>Add ι<VAR>(i : ι) → AddCommMonoid (A i)<VAR>self : DirectSum.GNonUnitalNonAssocSemiring A<VAR>i j : ι<VAR>a : A i<GOAL>GradedMonoid.GMul.mul a 0 = 0
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddMonoid ι<VAR>(i : ι) → AddCommMonoid (A i)<VAR>self : DirectSum.GSemiring A<VAR>n : ℕ<GOAL>DirectSum.GSemiring.natCast (n + 1) = DirectSum.GSemiring.natCast n + GradedMonoid.GOne.one
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddMonoid ι<VAR>(i : ι) → AddCommMonoid (A i)<VAR>self : DirectSum.GSemiring A<GOAL>DirectSum.GSemiring.natCast 0 = 0
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddMonoid ι<VAR>(i : ι) → AddCommGroup (A i)<VAR>self : DirectSum.GRing A<VAR>n : ℕ<GOAL>DirectSum.GRing.intCast (Int.negSucc n) = -DirectSum.GSemiring.natCast (n + 1)
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddMonoid ι<VAR>(i : ι) → AddCommGroup (A i)<VAR>self : DirectSum.GRing A<VAR>n : ℕ<GOAL>DirectSum.GRing.intCast ↑n = DirectSum.GSemiring.natCast n
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>(i : ι) → AddCommMonoid (A i)<VAR>i j : ι<VAR>a : A i<VAR>b : A j<VAR>h : GradedMonoid.mk i a = GradedMonoid.mk j b<GOAL>(DirectSum.of A i) a = (DirectSum.of A j) b
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>Zero ι<VAR>GradedMonoid.GOne A<VAR>(i : ι) → AddCommMonoid (A i)<GOAL>1 = (DirectSum.of A 0) GradedMonoid.GOne.one
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>Add ι<VAR>(i : ι) → AddCommMonoid (A i)<VAR>DirectSum.GNonUnitalNonAssocSemiring A<VAR>i j : ι<VAR>a : A i<VAR>b : A j<GOAL>((DirectSum.gMulHom A) a) b = GradedMonoid.GMul.mul a b
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>Add ι<VAR>(i : ι) → AddCommMonoid (A i)<VAR>DirectSum.GNonUnitalNonAssocSemiring A<VAR>a b : DirectSum ι fun i => A i<GOAL>((DirectSum.mulHom A) a) b = a * b
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>Add ι<VAR>(i : ι) → AddCommMonoid (A i)<VAR>DirectSum.GNonUnitalNonAssocSemiring A<VAR>i j : ι<VAR>a : A i<VAR>b : A j<GOAL>((DirectSum.mulHom A) ((DirectSum.of A i) a)) ((DirectSum.of A j) b) = (DirectSum.of A (i + j)) (GradedMonoid.GMul.mul a b)
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>Add ι<VAR>(i : ι) → AddCommMonoid (A i)<VAR>DirectSum.GNonUnitalNonAssocSemiring A<VAR>i j : ι<VAR>a : A i<VAR>b : A j<GOAL>(DirectSum.of A i) a * (DirectSum.of A j) b = (DirectSum.of A (i + j)) (GradedMonoid.GMul.mul a b)
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>x : DirectSum ι fun i => A i<GOAL>1 * x = x
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>x : DirectSum ι fun i => A i<GOAL>x * 1 = x
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>a b c : DirectSum ι fun i => A i<GOAL>a * b * c = a * (b * c)
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>i : ι<VAR>a : A i<VAR>n : ℕ<GOAL>(DirectSum.of A i) a ^ n = (DirectSum.of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>α : Type u_3<VAR>l : List α<VAR>fι : α → ι<VAR>fA : (a : α) → A (fι a)<GOAL>(DirectSum.of A (l.dProdIndex fι)) (l.dProd fι fA) = (List.map (fun a => (DirectSum.of A (fι a)) (fA a)) l).prod
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>n : ℕ<VAR>fι : Fin n → ι<VAR>fA : (a : Fin n) → A (fι a)<GOAL>(List.ofFn fun a => (DirectSum.of A (fι a)) (fA a)).prod = (DirectSum.of A ((List.finRange n).dProdIndex fι)) ((List.finRange n).dProd fι fA)
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>(i : ι) → (x : A i) → Decidable (x ≠ 0)<VAR>a a' : DirectSum ι fun i => A i<GOAL>a * a' = DFinsupp.sum a fun i ai => DFinsupp.sum a' fun j aj => (DirectSum.of A (i + j)) (GradedMonoid.GMul.mul ai aj)
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>(i : ι) → (x : A i) → Decidable (x ≠ 0)<VAR>a a' : DirectSum ι fun i => A i<GOAL>a * a' = ∑ ij ∈ DFinsupp.support a ×ˢ DFinsupp.support a', (DirectSum.of A (ij.1 + ij.2)) (GradedMonoid.GMul.mul (a ij.1) (a' ij.2))
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddCommMonoid ι<VAR>DirectSum.GCommSemiring A<VAR>a b : DirectSum ι fun i => A i<GOAL>a * b = b * a
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>Zero ι<VAR>GradedMonoid.GOne A<VAR>(i : ι) → AddCommMonoid (A i)<GOAL>(DirectSum.of A 0) 1 = 1
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>AddZeroClass ι<VAR>(i : ι) → AddCommMonoid (A i)<VAR>DirectSum.GNonUnitalNonAssocSemiring A<VAR>i : ι<VAR>a : A 0<VAR>b : A i<GOAL>(DirectSum.of A i) (a • b) = (DirectSum.of A 0) a * (DirectSum.of A i) b
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>AddZeroClass ι<VAR>(i : ι) → AddCommMonoid (A i)<VAR>DirectSum.GNonUnitalNonAssocSemiring A<VAR>a b : A 0<GOAL>(DirectSum.of A 0) (a * b) = (DirectSum.of A 0) a * (DirectSum.of A 0) b
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>a : A 0<VAR>n : ℕ<GOAL>(DirectSum.of A 0) (a ^ n) = (DirectSum.of A 0) a ^ n
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>n : ℕ<GOAL>(DirectSum.of A 0) ↑n = ↑n
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(DirectSum.of A 0) (OfNat.ofNat n) = OfNat.ofNat n
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>(i : ι) → AddCommGroup (A i)<VAR>AddMonoid ι<VAR>DirectSum.GRing A<VAR>n : ℤ<GOAL>(DirectSum.of A 0) ↑n = ↑n
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>Semiring R<VAR>F G : (DirectSum ι fun i => A i) →+* R<VAR>h : ∀ (i : ι), (↑F).comp (DirectSum.of A i) = (↑G).comp (DirectSum.of A i)<GOAL>F = G
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>Semiring R<VAR>f g : (DirectSum ι fun i => A i) →+* R<VAR>h : ∀ (i : ι) (x : A i), f ((DirectSum.of A i) x) = g ((DirectSum.of A i) x)<GOAL>f = g
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>Semiring R<VAR>f : (i : ι) → A i →+ R<VAR>hone : (f 0) GradedMonoid.GOne.one = 1<VAR>hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj<VAR>a : DirectSum ι fun i => A i<GOAL>(DirectSum.toSemiring f hone hmul) a = (DirectSum.toAddMonoid f) a
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>Semiring R<VAR>f : (i : ι) → A i →+ R<VAR>hone : (f 0) GradedMonoid.GOne.one = 1<VAR>hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj<VAR>i : ι<VAR>x : A i<GOAL>(DirectSum.toSemiring f hone hmul) ((DirectSum.of A i) x) = (f i) x
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>Semiring R<VAR>f : (i : ι) → A i →+ R<VAR>hone : (f 0) GradedMonoid.GOne.one = 1<VAR>hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj<GOAL>↑(DirectSum.toSemiring f hone hmul) = DirectSum.toAddMonoid f
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>Semiring R<VAR>f : { f // f GradedMonoid.GOne.one = 1 ∧ ∀ {i j : ι} (ai : A i) (aj : A j), f (GradedMonoid.GMul.mul ai aj) = f ai * f aj }<GOAL>DirectSum.liftRingHom f = DirectSum.toSemiring (fun x => ↑f) ⋯ ⋯
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>(i : ι) → AddCommMonoid (A i)<VAR>AddMonoid ι<VAR>DirectSum.GSemiring A<VAR>Semiring R<VAR>F : (DirectSum ι fun i => A i) →+* R<VAR>i : ι<GOAL>↑(DirectSum.liftRingHom.symm F) = (↑F).comp (DirectSum.of A i)
<VAR>M : Type u_10<VAR>N : Type u_11<VAR>Zero M<VAR>Zero N<VAR>self : ZeroHom M N<GOAL>self.toFun 0 = 0
<VAR>F : Type u_10<VAR>M : outParam (Type u_11)<VAR>N : outParam (Type u_12)<VAR>Zero M<VAR>Zero N<VAR>FunLike F M N<VAR>self : ZeroHomClass F M N<VAR>f : F<GOAL>f 0 = 0
<VAR>M : Type u_10<VAR>N : Type u_11<VAR>Add M<VAR>Add N<VAR>self : AddHom M N<VAR>x y : M<GOAL>self.toFun (x + y) = self.toFun x + self.toFun y
<VAR>F : Type u_10<VAR>M : outParam (Type u_11)<VAR>N : outParam (Type u_12)<VAR>Add M<VAR>Add N<VAR>FunLike F M N<VAR>self : AddHomClass F M N<VAR>f : F<VAR>x y : M<GOAL>f (x + y) = f x + f y
<VAR>M : Type u_10<VAR>N : Type u_11<VAR>One M<VAR>One N<VAR>self : OneHom M N<GOAL>self.toFun 1 = 1
<VAR>F : Type u_10<VAR>M : outParam (Type u_11)<VAR>N : outParam (Type u_12)<VAR>One M<VAR>One N<VAR>FunLike F M N<VAR>self : OneHomClass F M N<VAR>f : F<GOAL>f 1 = 1
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>Zero M<VAR>Zero N<VAR>FunLike F M N<VAR>ZeroHomClass F M N<VAR>f : F<GOAL>f 0 = 0
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>One M<VAR>One N<VAR>FunLike F M N<VAR>OneHomClass F M N<VAR>f : F<GOAL>f 1 = 1
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>Zero M<VAR>Zero N<VAR>FunLike F M N<VAR>ZeroHomClass F M N<VAR>f : F<GOAL>⇑f ∘ 0 = 0
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>One M<VAR>One N<VAR>FunLike F M N<VAR>OneHomClass F M N<VAR>f : F<GOAL>⇑f ∘ 1 = 1
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>Zero M<VAR>Zero N<VAR>FunLike F M N<VAR>Subsingleton M<VAR>ZeroHomClass F M N<GOAL>Subsingleton F
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>One M<VAR>One N<VAR>FunLike F M N<VAR>Subsingleton M<VAR>OneHomClass F M N<GOAL>Subsingleton F
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>Zero M<VAR>Zero N<VAR>FunLike F M N<VAR>ZeroHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>x : M<GOAL>f x = 0 ↔ x = 0
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>One M<VAR>One N<VAR>FunLike F M N<VAR>OneHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>x : M<GOAL>f x = 1 ↔ x = 1
<VAR>R : Type u_10<VAR>S : Type u_11<VAR>F : Type u_12<VAR>Zero R<VAR>Zero S<VAR>FunLike F R S<VAR>ZeroHomClass F R S<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>x : R<GOAL>f x ≠ 0 ↔ x ≠ 0
<VAR>R : Type u_10<VAR>S : Type u_11<VAR>F : Type u_12<VAR>One R<VAR>One S<VAR>FunLike F R S<VAR>OneHomClass F R S<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>x : R<GOAL>f x ≠ 1 ↔ x ≠ 1
<VAR>R : Type u_10<VAR>S : Type u_11<VAR>F : Type u_12<VAR>Zero R<VAR>Zero S<VAR>FunLike F R S<VAR>ZeroHomClass F R S<VAR>f : F<VAR>x : R<VAR>hx : f x ≠ 0<GOAL>x ≠ 0
<VAR>R : Type u_10<VAR>S : Type u_11<VAR>F : Type u_12<VAR>One R<VAR>One S<VAR>FunLike F R S<VAR>OneHomClass F R S<VAR>f : F<VAR>x : R<VAR>hx : f x ≠ 1<GOAL>x ≠ 1
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>One M<VAR>One N<VAR>FunLike F M N<VAR>OneHomClass F M N<VAR>f : F<GOAL>⇑↑f = ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>Zero M<VAR>Zero N<VAR>FunLike F M N<VAR>ZeroHomClass F M N<VAR>f : F<GOAL>⇑↑f = ⇑f
<VAR>M : Type u_10<VAR>N : Type u_11<VAR>Mul M<VAR>Mul N<VAR>self : M →ₙ* N<VAR>x y : M<GOAL>self.toFun (x * y) = self.toFun x * self.toFun y
<VAR>F : Type u_10<VAR>M : outParam (Type u_11)<VAR>N : outParam (Type u_12)<VAR>Mul M<VAR>Mul N<VAR>FunLike F M N<VAR>self : MulHomClass F M N<VAR>f : F<VAR>x y : M<GOAL>f (x * y) = f x * f y
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>Add M<VAR>Add N<VAR>FunLike F M N<VAR>AddHomClass F M N<VAR>f : F<VAR>x y : M<GOAL>f (x + y) = f x + f y
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>Mul M<VAR>Mul N<VAR>FunLike F M N<VAR>MulHomClass F M N<VAR>f : F<VAR>x y : M<GOAL>f (x * y) = f x * f y
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>Mul M<VAR>Mul N<VAR>FunLike F M N<VAR>MulHomClass F M N<VAR>f : F<VAR>g h : ι → M<GOAL>⇑f ∘ (g * h) = ⇑f ∘ g * ⇑f ∘ h
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>Add M<VAR>Add N<VAR>FunLike F M N<VAR>AddHomClass F M N<VAR>f : F<VAR>g h : ι → M<GOAL>⇑f ∘ (g + h) = ⇑f ∘ g + ⇑f ∘ h
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>Mul M<VAR>Mul N<VAR>FunLike F M N<VAR>MulHomClass F M N<VAR>f : F<GOAL>⇑↑f = ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>Add M<VAR>Add N<VAR>FunLike F M N<VAR>AddHomClass F M N<VAR>f : F<GOAL>⇑↑f = ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>FunLike F M N<VAR>AddMonoidHomClass F M N<VAR>f : F<GOAL>⇑↑f = ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>MulOneClass M<VAR>MulOneClass N<VAR>FunLike F M N<VAR>MonoidHomClass F M N<VAR>f : F<GOAL>⇑↑f = ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>MulOneClass M<VAR>MulOneClass N<VAR>FunLike F M N<VAR>MonoidHomClass F M N<VAR>f : F<VAR>a b : M<VAR>h : a * b = 1<GOAL>f a * f b = 1
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>F : Type u_9<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>FunLike F M N<VAR>AddMonoidHomClass F M N<VAR>f : F<VAR>a b : M<VAR>h : a + b = 0<GOAL>f a + f b = 0
<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>SubNegMonoid G<VAR>SubNegMonoid H<VAR>AddMonoidHomClass F G H<VAR>f : F<VAR>hf : ∀ (a : G), f (-a) = -f a<VAR>a b : G<GOAL>f (a - b) = f a - f b
<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>DivInvMonoid G<VAR>DivInvMonoid H<VAR>MonoidHomClass F G H<VAR>f : F<VAR>hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹<VAR>a b : G<GOAL>f (a / b) = f a / f b
<VAR>ι : Type u_1<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>DivInvMonoid G<VAR>DivInvMonoid H<VAR>MonoidHomClass F G H<VAR>f : F<VAR>hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹<VAR>g h : ι → G<GOAL>⇑f ∘ (g / h) = ⇑f ∘ g / ⇑f ∘ h
<VAR>ι : Type u_1<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>SubNegMonoid G<VAR>SubNegMonoid H<VAR>AddMonoidHomClass F G H<VAR>f : F<VAR>hf : ∀ (a : G), f (-a) = -f a<VAR>g h : ι → G<GOAL>⇑f ∘ (g - h) = ⇑f ∘ g - ⇑f ∘ h
<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>Group G<VAR>DivisionMonoid H<VAR>MonoidHomClass F G H<VAR>f : F<VAR>a : G<GOAL>f a⁻¹ = (f a)⁻¹
<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>AddGroup G<VAR>SubtractionMonoid H<VAR>AddMonoidHomClass F G H<VAR>f : F<VAR>a : G<GOAL>f (-a) = -f a
<VAR>ι : Type u_1<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>Group G<VAR>DivisionMonoid H<VAR>MonoidHomClass F G H<VAR>f : F<VAR>g : ι → G<GOAL>⇑f ∘ g⁻¹ = (⇑f ∘ g)⁻¹
<VAR>ι : Type u_1<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>AddGroup G<VAR>SubtractionMonoid H<VAR>AddMonoidHomClass F G H<VAR>f : F<VAR>g : ι → G<GOAL>⇑f ∘ (-g) = -⇑f ∘ g
<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>AddGroup G<VAR>SubtractionMonoid H<VAR>AddMonoidHomClass F G H<VAR>f : F<VAR>a b : G<GOAL>f (a + -b) = f a + -f b
<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>Group G<VAR>DivisionMonoid H<VAR>MonoidHomClass F G H<VAR>f : F<VAR>a b : G<GOAL>f (a * b⁻¹) = f a * (f b)⁻¹
<VAR>ι : Type u_1<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>Group G<VAR>DivisionMonoid H<VAR>MonoidHomClass F G H<VAR>f : F<VAR>g h : ι → G<GOAL>⇑f ∘ (g * h⁻¹) = ⇑f ∘ g * (⇑f ∘ h)⁻¹
<VAR>ι : Type u_1<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>AddGroup G<VAR>SubtractionMonoid H<VAR>AddMonoidHomClass F G H<VAR>f : F<VAR>g h : ι → G<GOAL>⇑f ∘ (g + -h) = ⇑f ∘ g + -⇑f ∘ h
<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>AddGroup G<VAR>SubtractionMonoid H<VAR>AddMonoidHomClass F G H<VAR>f : F<VAR>a b : G<GOAL>f (a - b) = f a - f b
<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>Group G<VAR>DivisionMonoid H<VAR>MonoidHomClass F G H<VAR>f : F<VAR>a b : G<GOAL>f (a / b) = f a / f b
<VAR>ι : Type u_1<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>Group G<VAR>DivisionMonoid H<VAR>MonoidHomClass F G H<VAR>f : F<VAR>g h : ι → G<GOAL>⇑f ∘ (g / h) = ⇑f ∘ g / ⇑f ∘ h
<VAR>ι : Type u_1<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>AddGroup G<VAR>SubtractionMonoid H<VAR>AddMonoidHomClass F G H<VAR>f : F<VAR>g h : ι → G<GOAL>⇑f ∘ (g - h) = ⇑f ∘ g - ⇑f ∘ h
<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>AddMonoid G<VAR>AddMonoid H<VAR>AddMonoidHomClass F G H<VAR>f : F<VAR>n : ℕ<VAR>a : G<GOAL>f (n • a) = n • f a
<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>Monoid G<VAR>Monoid H<VAR>MonoidHomClass F G H<VAR>f : F<VAR>a : G<VAR>n : ℕ<GOAL>f (a ^ n) = f a ^ n
<VAR>ι : Type u_1<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>AddGroup G<VAR>SubtractionMonoid H<VAR>AddMonoidHomClass F G H<VAR>f : F<VAR>g : ι → G<VAR>n : ℕ<GOAL>⇑f ∘ (n • g) = n • ⇑f ∘ g
<VAR>ι : Type u_1<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>Group G<VAR>DivisionMonoid H<VAR>MonoidHomClass F G H<VAR>f : F<VAR>g : ι → G<VAR>n : ℕ<GOAL>⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n
<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>SubNegMonoid G<VAR>SubNegMonoid H<VAR>AddMonoidHomClass F G H<VAR>f : F<VAR>hf : ∀ (x : G), f (-x) = -f x<VAR>a : G<VAR>n : ℤ<GOAL>f (n • a) = n • f a
<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>DivInvMonoid G<VAR>DivInvMonoid H<VAR>MonoidHomClass F G H<VAR>f : F<VAR>hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹<VAR>a : G<VAR>n : ℤ<GOAL>f (a ^ n) = f a ^ n
<VAR>ι : Type u_1<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>DivInvMonoid G<VAR>DivInvMonoid H<VAR>MonoidHomClass F G H<VAR>f : F<VAR>hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹<VAR>g : ι → G<VAR>n : ℤ<GOAL>⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n
<VAR>ι : Type u_1<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>SubNegMonoid G<VAR>SubNegMonoid H<VAR>AddMonoidHomClass F G H<VAR>f : F<VAR>hf : ∀ (x : G), f (-x) = -f x<VAR>g : ι → G<VAR>n : ℤ<GOAL>⇑f ∘ (n • g) = n • ⇑f ∘ g
<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>Group G<VAR>DivisionMonoid H<VAR>MonoidHomClass F G H<VAR>f : F<VAR>g : G<VAR>n : ℤ<GOAL>f (g ^ n) = f g ^ n
<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>AddGroup G<VAR>SubtractionMonoid H<VAR>AddMonoidHomClass F G H<VAR>f : F<VAR>n : ℤ<VAR>g : G<GOAL>f (n • g) = n • f g
<VAR>ι : Type u_1<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>AddGroup G<VAR>SubtractionMonoid H<VAR>AddMonoidHomClass F G H<VAR>f : F<VAR>g : ι → G<VAR>n : ℤ<GOAL>⇑f ∘ (n • g) = n • ⇑f ∘ g
<VAR>ι : Type u_1<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>FunLike F G H<VAR>Group G<VAR>DivisionMonoid H<VAR>MonoidHomClass F G H<VAR>f : F<VAR>g : ι → G<VAR>n : ℤ<GOAL>⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Zero M<VAR>Zero N<VAR>f : M → N<VAR>h1 : f 0 = 0<GOAL>⇑{ toFun := f, map_zero' := h1 } = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>One M<VAR>One N<VAR>f : M → N<VAR>h1 : f 1 = 1<GOAL>⇑{ toFun := f, map_one' := h1 } = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Zero M<VAR>Zero N<VAR>f : ZeroHom M N<GOAL>f.toFun = ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>One M<VAR>One N<VAR>f : OneHom M N<GOAL>f.toFun = ⇑f