ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Mul M<VAR>Mul N<VAR>f : M → N<VAR>hmul : ∀ (x y : M), f (x * y) = f x * f y<GOAL>⇑{ toFun := f, map_mul' := hmul } = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Add M<VAR>Add N<VAR>f : M → N<VAR>hmul : ∀ (x y : M), f (x + y) = f x + f y<GOAL>⇑{ toFun := f, map_add' := hmul } = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<GOAL>f.toFun = ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<GOAL>f.toFun = ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : OneHom M N<VAR>hmul : ∀ (x y : M), f.toFun (x * y) = f.toFun x * f.toFun y<GOAL>⇑{ toOneHom := f, map_mul' := hmul } = ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : ZeroHom M N<VAR>hmul : ∀ (x y : M), f.toFun (x + y) = f.toFun x + f.toFun y<GOAL>⇑{ toZeroHom := f, map_add' := hmul } = ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<GOAL>⇑↑f = ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<GOAL>⇑↑f = ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<GOAL>(↑f).toFun = ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<GOAL>(↑f).toFun = ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Zero M<VAR>Zero N<VAR>f g : ZeroHom M N<VAR>h : ∀ (x : M), f x = g x<GOAL>f = g
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>One M<VAR>One N<VAR>f g : OneHom M N<VAR>h : ∀ (x : M), f x = g x<GOAL>f = g
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Mul M<VAR>Mul N<VAR>f g : M →ₙ* N<VAR>h : ∀ (x : M), f x = g x<GOAL>f = g
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Add M<VAR>Add N<VAR>f g : AddHom M N<VAR>h : ∀ (x : M), f x = g x<GOAL>f = g
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f g : M →+ N<VAR>h : ∀ (x : M), f x = g x<GOAL>f = g
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f g : M →* N<VAR>h : ∀ (x : M), f x = g x<GOAL>f = g
<VAR>M : Type u_4<VAR>G : Type u_7<VAR>Group G<VAR>MulOneClass M<VAR>f : M → G<VAR>map_mul : ∀ (a b : M), f (a * b) = f a * f b<GOAL>⇑(MonoidHom.mk' f map_mul) = f
<VAR>M : Type u_4<VAR>G : Type u_7<VAR>AddGroup G<VAR>AddZeroClass M<VAR>f : M → G<VAR>map_mul : ∀ (a b : M), f (a + b) = f a + f b<GOAL>⇑(AddMonoidHom.mk' f map_mul) = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Zero M<VAR>Zero N<VAR>f : ZeroHom 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 : OneHom 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>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hmul : ∀ (x y : M), f (x * y) = f x * f y<GOAL>{ toFun := ⇑f, map_mul' := hmul } = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hmul : ∀ (x y : M), f (x + y) = f x + f y<GOAL>{ toFun := ⇑f, map_add' := hmul } = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<VAR>hmul : ∀ (x y : M), (↑f).toFun (x + y) = (↑f).toFun x + (↑f).toFun y<GOAL>{ toZeroHom := ↑f, map_add' := hmul } = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<VAR>hmul : ∀ (x y : M), (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y<GOAL>{ toOneHom := ↑f, map_mul' := hmul } = f
<VAR>M : Type u_4<VAR>N : Type u_5<GOAL>∀ {x : Zero M} {x_1 : Zero N} (f : ZeroHom M N) (f' : M → N) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
<VAR>M : Type u_4<VAR>N : Type u_5<GOAL>∀ {x : One M} {x_1 : One N} (f : OneHom M N) (f' : M → N) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
<VAR>M : Type u_4<VAR>N : Type u_5<GOAL>∀ {x : Zero M} {x_1 : Zero N} (f : ZeroHom M N) (f' : M → N) (h : f' = ⇑f), f.copy f' h = f
<VAR>M : Type u_4<VAR>N : Type u_5<GOAL>∀ {x : One M} {x_1 : One N} (f : OneHom M N) (f' : M → N) (h : f' = ⇑f), f.copy f' h = f
<VAR>M : Type u_4<VAR>N : Type u_5<GOAL>∀ {x : Mul M} {x_1 : Mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
<VAR>M : Type u_4<VAR>N : Type u_5<GOAL>∀ {x : Add M} {x_1 : Add N} (f : AddHom M N) (f' : M → N) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
<VAR>M : Type u_4<VAR>N : Type u_5<GOAL>∀ {x : Add M} {x_1 : Add N} (f : AddHom M N) (f' : M → N) (h : f' = ⇑f), f.copy f' h = f
<VAR>M : Type u_4<VAR>N : Type u_5<GOAL>∀ {x : Mul M} {x_1 : Mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = ⇑f), f.copy f' h = f
<VAR>M : Type u_4<VAR>N : Type u_5<GOAL>∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} (f : M →+ N) (f' : M → N) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
<VAR>M : Type u_4<VAR>N : Type u_5<GOAL>∀ {x : MulOneClass M} {x_1 : MulOneClass N} (f : M →* N) (f' : M → N) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
<VAR>M : Type u_4<VAR>N : Type u_5<GOAL>∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} (f : M →+ N) (f' : M → N) (h : f' = ⇑f), f.copy f' h = f
<VAR>M : Type u_4<VAR>N : Type u_5<GOAL>∀ {x : MulOneClass M} {x_1 : MulOneClass N} (f : M →* N) (f' : M → N) (h : f' = ⇑f), f.copy f' h = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>One M<VAR>One N<VAR>f : OneHom M N<GOAL>f 1 = 1
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Zero M<VAR>Zero N<VAR>f : ZeroHom M N<GOAL>f 0 = 0
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<GOAL>f 1 = 1
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<GOAL>f 0 = 0
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>a b : M<GOAL>f (a * b) = f a * f b
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>a b : M<GOAL>f (a + b) = f a + f b
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<VAR>a b : M<GOAL>f (a + b) = f a + f b
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<VAR>a b : M<GOAL>f (a * b) = f a * f b
<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>x : M<VAR>hx : ∃ y, x + y = 0<GOAL>∃ y, f x + y = 0
<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>x : M<VAR>hx : ∃ y, x * y = 1<GOAL>∃ y, f x * y = 1
<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>x : M<VAR>hx : ∃ y, y * x = 1<GOAL>∃ y, y * f x = 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>x : M<VAR>hx : ∃ y, y + x = 0<GOAL>∃ y, y + f x = 0
<VAR>M : Type u_10<VAR>Zero M<VAR>x : M<GOAL>(ZeroHom.id M) x = x
<VAR>M : Type u_10<VAR>One M<VAR>x : M<GOAL>(OneHom.id M) x = x
<VAR>M : Type u_10<VAR>Mul M<VAR>x : M<GOAL>(MulHom.id M) x = x
<VAR>M : Type u_10<VAR>Add M<VAR>x : M<GOAL>(AddHom.id M) x = x
<VAR>M : Type u_10<VAR>AddZeroClass M<VAR>x : M<GOAL>(AddMonoidHom.id M) x = x
<VAR>M : Type u_10<VAR>MulOneClass M<VAR>x : M<GOAL>(MonoidHom.id M) x = x
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>One M<VAR>One N<VAR>One P<VAR>g : OneHom N P<VAR>f : OneHom M N<GOAL>⇑(g.comp f) = ⇑g ∘ ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Zero M<VAR>Zero N<VAR>Zero P<VAR>g : ZeroHom N P<VAR>f : ZeroHom M N<GOAL>⇑(g.comp f) = ⇑g ∘ ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Mul M<VAR>Mul N<VAR>Mul P<VAR>g : N →ₙ* P<VAR>f : M →ₙ* N<GOAL>⇑(g.comp f) = ⇑g ∘ ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Add M<VAR>Add N<VAR>Add P<VAR>g : AddHom N P<VAR>f : AddHom M N<GOAL>⇑(g.comp f) = ⇑g ∘ ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>g : N →* P<VAR>f : M →* N<GOAL>⇑(g.comp f) = ⇑g ∘ ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>g : N →+ P<VAR>f : M →+ N<GOAL>⇑(g.comp f) = ⇑g ∘ ⇑f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>One M<VAR>One N<VAR>One P<VAR>g : OneHom N P<VAR>f : OneHom M N<VAR>x : M<GOAL>(g.comp f) x = g (f x)
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Zero M<VAR>Zero N<VAR>Zero P<VAR>g : ZeroHom N P<VAR>f : ZeroHom M N<VAR>x : M<GOAL>(g.comp f) x = g (f x)
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Add M<VAR>Add N<VAR>Add P<VAR>g : AddHom N P<VAR>f : AddHom M N<VAR>x : M<GOAL>(g.comp f) x = g (f x)
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Mul M<VAR>Mul N<VAR>Mul P<VAR>g : N →ₙ* P<VAR>f : M →ₙ* N<VAR>x : M<GOAL>(g.comp f) x = g (f x)
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>g : N →* P<VAR>f : M →* N<VAR>x : M<GOAL>(g.comp f) x = g (f x)
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>g : N →+ P<VAR>f : M →+ N<VAR>x : M<GOAL>(g.comp f) x = g (f x)
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_10<VAR>One M<VAR>One N<VAR>One P<VAR>One Q<VAR>f : OneHom M N<VAR>g : OneHom N P<VAR>h : OneHom P Q<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_10<VAR>Zero M<VAR>Zero N<VAR>Zero P<VAR>Zero Q<VAR>f : ZeroHom M N<VAR>g : ZeroHom N P<VAR>h : ZeroHom P Q<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_10<VAR>Mul M<VAR>Mul N<VAR>Mul P<VAR>Mul Q<VAR>f : M →ₙ* N<VAR>g : N →ₙ* P<VAR>h : P →ₙ* Q<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_10<VAR>Add M<VAR>Add N<VAR>Add P<VAR>Add Q<VAR>f : AddHom M N<VAR>g : AddHom N P<VAR>h : AddHom P Q<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_10<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>MulOneClass Q<VAR>f : M →* N<VAR>g : N →* P<VAR>h : P →* Q<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_10<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>AddZeroClass Q<VAR>f : M →+ N<VAR>g : N →+ P<VAR>h : P →+ Q<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>One M<VAR>One N<VAR>One P<VAR>g₁ g₂ : OneHom N P<VAR>f : OneHom M N<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Zero M<VAR>Zero N<VAR>Zero P<VAR>g₁ g₂ : ZeroHom N P<VAR>f : ZeroHom M N<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Add M<VAR>Add N<VAR>Add P<VAR>g₁ g₂ : AddHom N P<VAR>f : AddHom M N<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Mul M<VAR>Mul N<VAR>Mul P<VAR>g₁ g₂ : N →ₙ* P<VAR>f : M →ₙ* N<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>g₁ g₂ : N →* P<VAR>f : M →* N<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>g₁ g₂ : N →+ P<VAR>f : M →+ N<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Zero M<VAR>Zero N<VAR>Zero P<VAR>g : ZeroHom N P<VAR>f₁ f₂ : ZeroHom M N<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>One M<VAR>One N<VAR>One P<VAR>g : OneHom N P<VAR>f₁ f₂ : OneHom M N<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Add M<VAR>Add N<VAR>Add P<VAR>g : AddHom N P<VAR>f₁ f₂ : AddHom M N<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Mul M<VAR>Mul N<VAR>Mul P<VAR>g : N →ₙ* P<VAR>f₁ f₂ : M →ₙ* N<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>g : N →* P<VAR>f₁ f₂ : M →* N<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>g : N →+ P<VAR>f₁ f₂ : M →+ N<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>Function.Injective MonoidHom.toOneHom
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>Function.Injective AddMonoidHom.toZeroHom
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>Function.Injective AddMonoidHom.toAddHom
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>Function.Injective MonoidHom.toMulHom
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Zero M<VAR>Zero N<VAR>f : ZeroHom M N<GOAL>f.comp (ZeroHom.id M) = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>One M<VAR>One N<VAR>f : OneHom M N<GOAL>f.comp (OneHom.id M) = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<GOAL>f.comp (AddHom.id M) = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<GOAL>f.comp (MulHom.id M) = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<GOAL>f.comp (AddMonoidHom.id M) = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<GOAL>f.comp (MonoidHom.id M) = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>One M<VAR>One N<VAR>f : OneHom M N<GOAL>(OneHom.id N).comp f = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Zero M<VAR>Zero N<VAR>f : ZeroHom M N<GOAL>(ZeroHom.id N).comp f = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<GOAL>(AddHom.id N).comp f = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<GOAL>(MulHom.id N).comp f = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<GOAL>(MonoidHom.id N).comp f = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<GOAL>(AddMonoidHom.id N).comp f = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Monoid M<VAR>Monoid N<VAR>f : M →* N<VAR>a : M<VAR>n : ℕ<GOAL>f (a ^ n) = f a ^ n
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddMonoid M<VAR>AddMonoid N<VAR>f : M →+ N<VAR>a : M<VAR>n : ℕ<GOAL>f (n • a) = n • f a
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>SubNegMonoid M<VAR>SubNegMonoid N<VAR>f : M →+ N<VAR>hf : ∀ (x : M), f (-x) = -f x<VAR>a : M<VAR>n : ℤ<GOAL>f (n • a) = n • f a
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>DivInvMonoid M<VAR>DivInvMonoid N<VAR>f : M →* N<VAR>hf : ∀ (x : M), f x⁻¹ = (f x)⁻¹<VAR>a : M<VAR>n : ℤ<GOAL>f (a ^ n) = f a ^ n
<VAR>M : Type u_4<VAR>MulOneClass M<VAR>f : Monoid.End M<VAR>n : ℕ<GOAL>⇑(f ^ n) = (⇑f)^[n]
<VAR>M : Type u_4<VAR>MulOneClass M<GOAL>⇑1 = id
<VAR>M : Type u_4<VAR>MulOneClass M<VAR>f g : Monoid.End M<GOAL>⇑(f * g) = ⇑f ∘ ⇑g
<VAR>A : Type u_10<VAR>AddZeroClass A<GOAL>⇑1 = id
<VAR>A : Type u_10<VAR>AddZeroClass A<VAR>f g : AddMonoid.End A<GOAL>⇑(f * g) = ⇑f ∘ ⇑g
<VAR>A : Type u_10<VAR>AddZeroClass A<VAR>f : AddMonoid.End A<VAR>n : ℕ<GOAL>⇑(f ^ n) = (⇑f)^[n]
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Zero M<VAR>Zero N<VAR>x : M<GOAL>0 x = 0
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>One M<VAR>One N<VAR>x : M<GOAL>1 x = 1
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>MulOneClass M<VAR>MulOneClass N<VAR>x : M<GOAL>1 x = 1
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>x : M<GOAL>0 x = 0
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>One M<VAR>One N<VAR>One P<VAR>f : OneHom M N<GOAL>OneHom.comp 1 f = 1
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Zero M<VAR>Zero N<VAR>Zero P<VAR>f : ZeroHom M N<GOAL>ZeroHom.comp 0 f = 0
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>One M<VAR>One N<VAR>One P<VAR>f : OneHom N P<GOAL>f.comp 1 = 1
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Zero M<VAR>Zero N<VAR>Zero P<VAR>f : ZeroHom N P<GOAL>f.comp 0 = 0
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>f : M →* N<GOAL>MonoidHom.comp 1 f = 1
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>f : M →+ N<GOAL>AddMonoidHom.comp 0 f = 0
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>f : N →+ P<GOAL>f.comp 0 = 0
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>f : N →* P<GOAL>f.comp 1 = 1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>SubtractionMonoid β<VAR>f : α →+ β<VAR>a : α<GOAL>f (-a) = -f a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>DivisionMonoid β<VAR>f : α →* β<VAR>a : α<GOAL>f a⁻¹ = (f a)⁻¹
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>SubtractionMonoid β<VAR>f : α →+ β<VAR>g : α<VAR>n : ℤ<GOAL>f (n • g) = n • f g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>DivisionMonoid β<VAR>f : α →* β<VAR>g : α<VAR>n : ℤ<GOAL>f (g ^ n) = f g ^ n
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>SubtractionMonoid β<VAR>f : α →+ β<VAR>g h : α<GOAL>f (g - h) = f g - f h
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>DivisionMonoid β<VAR>f : α →* β<VAR>g h : α<GOAL>f (g / h) = f g / f h
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>SubtractionMonoid β<VAR>f : α →+ β<VAR>g h : α<GOAL>f (g + -h) = f g + -f h
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>DivisionMonoid β<VAR>f : α →* β<VAR>g h : α<GOAL>f (g * h⁻¹) = f g * (f h)⁻¹
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>f : α → M<GOAL>Function.mulSupport f = f ⁻¹' {1}ᶜ
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → M<GOAL>Function.support f = f ⁻¹' {0}ᶜ
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>f : α → M<VAR>x : α<GOAL>x ∉ Function.mulSupport f ↔ f x = 1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → M<VAR>x : α<GOAL>x ∉ Function.support f ↔ f x = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>f : α → M<GOAL>(Function.mulSupport f)ᶜ = {x | f x = 1}
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → M<GOAL>(Function.support f)ᶜ = {x | f x = 0}
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>f : α → M<VAR>x : α<GOAL>x ∈ Function.mulSupport f ↔ f x ≠ 1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → M<VAR>x : α<GOAL>x ∈ Function.support f ↔ f x ≠ 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>f : α → M<VAR>s : Set α<GOAL>Function.mulSupport f ⊆ s ↔ ∀ (x : α), f x ≠ 1 → x ∈ s
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → M<VAR>s : Set α<GOAL>Function.support f ⊆ s ↔ ∀ (x : α), f x ≠ 0 → x ∈ s
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → M<VAR>s : Set α<GOAL>Function.support f ⊆ s ↔ ∀ x ∉ s, f x = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>f : α → M<VAR>s : Set α<GOAL>Function.mulSupport f ⊆ s ↔ ∀ x ∉ s, f x = 1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>f : α → M<VAR>s : Set α<GOAL>Function.mulSupport f = s ↔ (∀ x ∈ s, f x ≠ 1) ∧ ∀ x ∉ s, f x = 1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → M<VAR>s : Set α<GOAL>Function.support f = s ↔ (∀ x ∈ s, f x ≠ 0) ∧ ∀ x ∉ s, f x = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>f g : α → M<GOAL>f = g ↔ Function.mulSupport f = Function.mulSupport g ∧ ∀ x ∈ Function.mulSupport f, f x = g x
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f g : α → M<GOAL>f = g ↔ Function.support f = Function.support g ∧ ∀ x ∈ Function.support f, f x = g x
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>DecidableEq α<VAR>f : α → M<VAR>x : α<VAR>y : M<VAR>hy : y ≠ 1<GOAL>Function.mulSupport (Function.update f x y) = insert x (Function.mulSupport f)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>DecidableEq α<VAR>f : α → M<VAR>x : α<VAR>y : M<VAR>hy : y ≠ 0<GOAL>Function.support (Function.update f x y) = insert x (Function.support f)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>DecidableEq α<VAR>f : α → M<VAR>x : α<GOAL>Function.support (Function.update f x 0) = Function.support f \ {x}
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>DecidableEq α<VAR>f : α → M<VAR>x : α<GOAL>Function.mulSupport (Function.update f x 1) = Function.mulSupport f \ {x}
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>DecidableEq α<VAR>DecidableEq M<VAR>f : α → M<VAR>x : α<VAR>y : M<GOAL>Function.mulSupport (Function.update f x y) = if y = 1 then Function.mulSupport f \ {x} else insert x (Function.mulSupport f)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>DecidableEq α<VAR>DecidableEq M<VAR>f : α → M<VAR>x : α<VAR>y : M<GOAL>Function.support (Function.update f x y) = if y = 0 then Function.support f \ {x} else insert x (Function.support f)
<VAR>α : Type u_1<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>Zero N<VAR>f : α → M'<VAR>g : α → N<GOAL>Function.support (Function.extend f g 0) ⊆ f '' Function.support g
<VAR>α : Type u_1<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>One N<VAR>f : α → M'<VAR>g : α → N<GOAL>Function.mulSupport (Function.extend f g 1) ⊆ f '' Function.mulSupport g
<VAR>α : Type u_1<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>One N<VAR>f : α → M'<VAR>g : α → N<VAR>hf : Function.Injective f<GOAL>Function.mulSupport (Function.extend f g 1) = f '' Function.mulSupport g
<VAR>α : Type u_1<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>Zero N<VAR>f : α → M'<VAR>g : α → N<VAR>hf : Function.Injective f<GOAL>Function.support (Function.extend f g 0) = f '' Function.support g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → M<VAR>s : Set α<GOAL>Disjoint (Function.support f) s ↔ Set.EqOn f 0 s
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>f : α → M<VAR>s : Set α<GOAL>Disjoint (Function.mulSupport f) s ↔ Set.EqOn f 1 s
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → M<VAR>s : Set α<GOAL>Disjoint s (Function.support f) ↔ Set.EqOn f 0 s
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>f : α → M<VAR>s : Set α<GOAL>Disjoint s (Function.mulSupport f) ↔ Set.EqOn f 1 s
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → M<GOAL>Function.support f = ∅ ↔ f = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>f : α → M<GOAL>Function.mulSupport f = ∅ ↔ f = 1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → M<GOAL>(Function.support f).Nonempty ↔ f ≠ 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>f : α → M<GOAL>(Function.mulSupport f).Nonempty ↔ f ≠ 1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>f : α → M<GOAL>Set.range f ⊆ insert 1 (f '' Function.mulSupport f)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → M<GOAL>Set.range f ⊆ insert 0 (f '' Function.support f)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>f : α → M<VAR>k : Set α<VAR>h : Function.mulSupport f ⊆ k<GOAL>Set.range f = f '' k ∨ Set.range f = insert 1 (f '' k)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → M<VAR>k : Set α<VAR>h : Function.support f ⊆ k<GOAL>Set.range f = f '' k ∨ Set.range f = insert 0 (f '' k)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<GOAL>Function.mulSupport 1 = ∅
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<GOAL>Function.support 0 = ∅
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<GOAL>(Function.mulSupport fun x => 1) = ∅
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<GOAL>(Function.support fun x => 0) = ∅
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>c : M<VAR>hc : c ≠ 0<GOAL>(Function.support fun x => c) = Set.univ
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>One M<VAR>c : M<VAR>hc : c ≠ 1<GOAL>(Function.mulSupport fun x => c) = Set.univ
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Zero M<VAR>Zero N<VAR>Zero P<VAR>op : M → N → P<VAR>op1 : op 0 0 = 0<VAR>f : α → M<VAR>g : α → N<GOAL>(Function.support fun x => op (f x) (g x)) ⊆ Function.support f ∪ Function.support g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>P : Type u_8<VAR>One M<VAR>One N<VAR>One P<VAR>op : M → N → P<VAR>op1 : op 1 1 = 1<VAR>f : α → M<VAR>g : α → N<GOAL>(Function.mulSupport fun x => op (f x) (g x)) ⊆ Function.mulSupport f ∪ Function.mulSupport g