ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Div G<VAR>Div H<VAR>a b : G × H<GOAL>(a / b).2 = a.2 / b.2
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Sub G<VAR>Sub H<VAR>a b : G × H<GOAL>(a - b).2 = a.2 - b.2
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Sub G<VAR>Sub H<VAR>x₁ x₂ : G<VAR>y₁ y₂ : H<GOAL>(x₁, y₁) - (x₂, y₂) = (x₁ - x₂, y₁ - y₂)
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Div G<VAR>Div H<VAR>x₁ x₂ : G<VAR>y₁ y₂ : H<GOAL>(x₁, y₁) / (x₂, y₂) = (x₁ / x₂, y₁ / y₂)
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Sub G<VAR>Sub H<VAR>a b : G × H<GOAL>(a - b).swap = a.swap - b.swap
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Div G<VAR>Div H<VAR>a b : G × H<GOAL>(a / b).swap = a.swap / b.swap
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Mul M<VAR>Mul N<VAR>x y z : M × N<VAR>hm : SemiconjBy x.1 y.1 z.1<VAR>hn : SemiconjBy x.2 y.2 z.2<GOAL>SemiconjBy x y z
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Add M<VAR>Add N<VAR>x y z : M × N<VAR>hm : AddSemiconjBy x.1 y.1 z.1<VAR>hn : AddSemiconjBy x.2 y.2 z.2<GOAL>AddSemiconjBy x y z
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Add M<VAR>Add N<VAR>x y z : M × N<GOAL>AddSemiconjBy x y z ↔ AddSemiconjBy x.1 y.1 z.1 ∧ AddSemiconjBy x.2 y.2 z.2
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Mul M<VAR>Mul N<VAR>x y z : M × N<GOAL>SemiconjBy x y z ↔ SemiconjBy x.1 y.1 z.1 ∧ SemiconjBy x.2 y.2 z.2
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Add M<VAR>Add N<VAR>x y : M × N<VAR>hm : AddCommute x.1 y.1<VAR>hn : AddCommute x.2 y.2<GOAL>AddCommute x y
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Mul M<VAR>Mul N<VAR>x y : M × N<VAR>hm : Commute x.1 y.1<VAR>hn : Commute x.2 y.2<GOAL>Commute x y
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Add M<VAR>Add N<VAR>x y : M × N<GOAL>AddCommute x y ↔ AddCommute x.1 y.1 ∧ AddCommute x.2 y.2
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Mul M<VAR>Mul N<VAR>x y : M × N<GOAL>Commute x y ↔ Commute x.1 y.1 ∧ Commute x.2 y.2
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Add M<VAR>Add N<GOAL>⇑(AddHom.fst M N) = Prod.fst
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Mul M<VAR>Mul N<GOAL>⇑(MulHom.fst M N) = Prod.fst
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Mul M<VAR>Mul N<GOAL>⇑(MulHom.snd M N) = Prod.snd
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Add M<VAR>Add N<GOAL>⇑(AddHom.snd M N) = Prod.snd
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Add M<VAR>Add N<VAR>Add P<VAR>f : AddHom M N<VAR>g : AddHom M P<GOAL>⇑(f.prod g) = Pi.prod ⇑f ⇑g
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Mul M<VAR>Mul N<VAR>Mul P<VAR>f : M →ₙ* N<VAR>g : M →ₙ* P<GOAL>⇑(f.prod g) = Pi.prod ⇑f ⇑g
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Add M<VAR>Add N<VAR>Add P<VAR>f : AddHom M N<VAR>g : AddHom M P<VAR>x : M<GOAL>(f.prod g) x = (f x, g x)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Mul M<VAR>Mul N<VAR>Mul P<VAR>f : M →ₙ* N<VAR>g : M →ₙ* P<VAR>x : M<GOAL>(f.prod g) x = (f x, g x)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Add M<VAR>Add N<VAR>Add P<VAR>f : AddHom M N<VAR>g : AddHom M P<GOAL>(AddHom.fst N P).comp (f.prod g) = f
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Mul M<VAR>Mul N<VAR>Mul P<VAR>f : M →ₙ* N<VAR>g : M →ₙ* P<GOAL>(MulHom.fst N P).comp (f.prod g) = f
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Add M<VAR>Add N<VAR>Add P<VAR>f : AddHom M N<VAR>g : AddHom M P<GOAL>(AddHom.snd N P).comp (f.prod g) = g
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Mul M<VAR>Mul N<VAR>Mul P<VAR>f : M →ₙ* N<VAR>g : M →ₙ* P<GOAL>(MulHom.snd N P).comp (f.prod g) = g
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Mul M<VAR>Mul N<VAR>Mul P<VAR>f : M →ₙ* N × P<GOAL>((MulHom.fst N P).comp f).prod ((MulHom.snd N P).comp f) = f
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Add M<VAR>Add N<VAR>Add P<VAR>f : AddHom M (N × P)<GOAL>((AddHom.fst N P).comp f).prod ((AddHom.snd N P).comp f) = f
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>M' : Type u_8<VAR>N' : Type u_9<VAR>Mul M<VAR>Mul N<VAR>Mul M'<VAR>Mul N'<VAR>f : M →ₙ* M'<VAR>g : N →ₙ* N'<GOAL>f.prodMap g = (f.comp (MulHom.fst M N)).prod (g.comp (MulHom.snd M N))
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>M' : Type u_8<VAR>N' : Type u_9<VAR>Add M<VAR>Add N<VAR>Add M'<VAR>Add N'<VAR>f : AddHom M M'<VAR>g : AddHom N N'<GOAL>f.prodMap g = (f.comp (AddHom.fst M N)).prod (g.comp (AddHom.snd M N))
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>M' : Type u_8<VAR>N' : Type u_9<VAR>Add M<VAR>Add N<VAR>Add M'<VAR>Add N'<VAR>f : AddHom M M'<VAR>g : AddHom N N'<GOAL>⇑(f.prodMap g) = Prod.map ⇑f ⇑g
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>M' : Type u_8<VAR>N' : Type u_9<VAR>Mul M<VAR>Mul N<VAR>Mul M'<VAR>Mul N'<VAR>f : M →ₙ* M'<VAR>g : N →ₙ* N'<GOAL>⇑(f.prodMap g) = Prod.map ⇑f ⇑g
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>M' : Type u_8<VAR>N' : Type u_9<VAR>Add M<VAR>Add N<VAR>Add M'<VAR>Add N'<VAR>Add P<VAR>f : AddHom P M<VAR>g : AddHom P N<VAR>f' : AddHom M M'<VAR>g' : AddHom N N'<GOAL>(f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>M' : Type u_8<VAR>N' : Type u_9<VAR>Mul M<VAR>Mul N<VAR>Mul M'<VAR>Mul N'<VAR>Mul P<VAR>f : P →ₙ* M<VAR>g : P →ₙ* N<VAR>f' : M →ₙ* M'<VAR>g' : N →ₙ* N'<GOAL>(f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Add M<VAR>Add N<VAR>AddCommSemigroup P<VAR>f : AddHom M P<VAR>g : AddHom N P<VAR>p : M × N<GOAL>(f.coprod g) p = f p.1 + g p.2
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Mul M<VAR>Mul N<VAR>CommSemigroup P<VAR>f : M →ₙ* P<VAR>g : N →ₙ* P<VAR>p : M × N<GOAL>(f.coprod g) p = f p.1 * g p.2
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Mul M<VAR>Mul N<VAR>CommSemigroup P<VAR>Q : Type u_8<VAR>CommSemigroup Q<VAR>h : P →ₙ* Q<VAR>f : M →ₙ* P<VAR>g : N →ₙ* P<GOAL>h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Add M<VAR>Add N<VAR>AddCommSemigroup P<VAR>Q : Type u_8<VAR>AddCommSemigroup Q<VAR>h : AddHom P Q<VAR>f : AddHom M P<VAR>g : AddHom N P<GOAL>h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>⇑(MonoidHom.fst M N) = Prod.fst
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>⇑(AddMonoidHom.fst M N) = Prod.fst
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>⇑(AddMonoidHom.snd M N) = Prod.snd
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>⇑(MonoidHom.snd M N) = Prod.snd
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<VAR>x : M<GOAL>(MonoidHom.inl M N) x = (x, 1)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>x : M<GOAL>(AddMonoidHom.inl M N) x = (x, 0)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<VAR>y : N<GOAL>(MonoidHom.inr M N) y = (1, y)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>y : N<GOAL>(AddMonoidHom.inr M N) y = (0, y)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>(AddMonoidHom.fst M N).comp (AddMonoidHom.inl M N) = AddMonoidHom.id M
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>(MonoidHom.fst M N).comp (MonoidHom.inl M N) = MonoidHom.id M
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>(AddMonoidHom.snd M N).comp (AddMonoidHom.inl M N) = 0
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>(MonoidHom.snd M N).comp (MonoidHom.inl M N) = 1
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>(AddMonoidHom.fst M N).comp (AddMonoidHom.inr M N) = 0
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>(MonoidHom.fst M N).comp (MonoidHom.inr M N) = 1
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>(MonoidHom.snd M N).comp (MonoidHom.inr M N) = MonoidHom.id N
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>(AddMonoidHom.snd M N).comp (AddMonoidHom.inr M N) = AddMonoidHom.id N
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>m : M<VAR>n : N<GOAL>AddCommute ((AddMonoidHom.inl M N) m) ((AddMonoidHom.inr M N) n)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<VAR>m : M<VAR>n : N<GOAL>Commute ((MonoidHom.inl M N) m) ((MonoidHom.inr M N) n)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>f : M →+ N<VAR>g : M →+ P<GOAL>⇑(f.prod g) = Pi.prod ⇑f ⇑g
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>f : M →* N<VAR>g : M →* P<GOAL>⇑(f.prod g) = Pi.prod ⇑f ⇑g
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>f : M →+ N<VAR>g : M →+ P<VAR>x : M<GOAL>(f.prod g) x = (f x, g x)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>f : M →* N<VAR>g : M →* P<VAR>x : M<GOAL>(f.prod g) x = (f x, g x)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>f : M →+ N<VAR>g : M →+ P<GOAL>(AddMonoidHom.fst N P).comp (f.prod g) = f
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>f : M →* N<VAR>g : M →* P<GOAL>(MonoidHom.fst N P).comp (f.prod g) = f
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>f : M →+ N<VAR>g : M →+ P<GOAL>(AddMonoidHom.snd N P).comp (f.prod g) = g
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>f : M →* N<VAR>g : M →* P<GOAL>(MonoidHom.snd N P).comp (f.prod g) = g
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>f : M →* N × P<GOAL>((MonoidHom.fst N P).comp f).prod ((MonoidHom.snd N P).comp f) = f
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>f : M →+ N × P<GOAL>((AddMonoidHom.fst N P).comp f).prod ((AddMonoidHom.snd N P).comp f) = f
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<VAR>M' : Type u_8<VAR>N' : Type u_9<VAR>MulOneClass M'<VAR>MulOneClass N'<VAR>f : M →* M'<VAR>g : N →* N'<GOAL>f.prodMap g = (f.comp (MonoidHom.fst M N)).prod (g.comp (MonoidHom.snd M N))
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>M' : Type u_8<VAR>N' : Type u_9<VAR>AddZeroClass M'<VAR>AddZeroClass N'<VAR>f : M →+ M'<VAR>g : N →+ N'<GOAL>f.prodMap g = (f.comp (AddMonoidHom.fst M N)).prod (g.comp (AddMonoidHom.snd M N))
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<VAR>M' : Type u_8<VAR>N' : Type u_9<VAR>MulOneClass M'<VAR>MulOneClass N'<VAR>f : M →* M'<VAR>g : N →* N'<GOAL>⇑(f.prodMap g) = Prod.map ⇑f ⇑g
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>M' : Type u_8<VAR>N' : Type u_9<VAR>AddZeroClass M'<VAR>AddZeroClass N'<VAR>f : M →+ M'<VAR>g : N →+ N'<GOAL>⇑(f.prodMap g) = Prod.map ⇑f ⇑g
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>M' : Type u_8<VAR>N' : Type u_9<VAR>AddZeroClass M'<VAR>AddZeroClass N'<VAR>AddZeroClass P<VAR>f : P →+ M<VAR>g : P →+ N<VAR>f' : M →+ M'<VAR>g' : N →+ N'<GOAL>(f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>M' : Type u_8<VAR>N' : Type u_9<VAR>MulOneClass M'<VAR>MulOneClass N'<VAR>MulOneClass P<VAR>f : P →* M<VAR>g : P →* N<VAR>f' : M →* M'<VAR>g' : N →* N'<GOAL>(f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddCommMonoid P<VAR>f : M →+ P<VAR>g : N →+ P<VAR>p : M × N<GOAL>(f.coprod g) p = f p.1 + g p.2
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>CommMonoid P<VAR>f : M →* P<VAR>g : N →* P<VAR>p : M × N<GOAL>(f.coprod g) p = f p.1 * g p.2
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>CommMonoid P<VAR>f : M →* P<VAR>g : N →* P<GOAL>(f.coprod g).comp (MonoidHom.inl M N) = f
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddCommMonoid P<VAR>f : M →+ P<VAR>g : N →+ P<GOAL>(f.coprod g).comp (AddMonoidHom.inl M N) = f
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddCommMonoid P<VAR>f : M →+ P<VAR>g : N →+ P<GOAL>(f.coprod g).comp (AddMonoidHom.inr M N) = g
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>CommMonoid P<VAR>f : M →* P<VAR>g : N →* P<GOAL>(f.coprod g).comp (MonoidHom.inr M N) = g
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>CommMonoid P<VAR>f : M × N →* P<GOAL>(f.comp (MonoidHom.inl M N)).coprod (f.comp (MonoidHom.inr M N)) = f
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddCommMonoid P<VAR>f : M × N →+ P<GOAL>(f.comp (AddMonoidHom.inl M N)).coprod (f.comp (AddMonoidHom.inr M N)) = f
<VAR>M : Type u_8<VAR>N : Type u_9<VAR>AddCommMonoid M<VAR>AddCommMonoid N<GOAL>(AddMonoidHom.inl M N).coprod (AddMonoidHom.inr M N) = AddMonoidHom.id (M × N)
<VAR>M : Type u_8<VAR>N : Type u_9<VAR>CommMonoid M<VAR>CommMonoid N<GOAL>(MonoidHom.inl M N).coprod (MonoidHom.inr M N) = MonoidHom.id (M × N)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddCommMonoid P<VAR>Q : Type u_8<VAR>AddCommMonoid Q<VAR>h : P →+ Q<VAR>f : M →+ P<VAR>g : N →+ P<GOAL>h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>CommMonoid P<VAR>Q : Type u_8<VAR>CommMonoid Q<VAR>h : P →* Q<VAR>f : M →* P<VAR>g : N →* P<GOAL>h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>⇑AddEquiv.prodComm = Prod.swap
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>⇑MulEquiv.prodComm = Prod.swap
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>⇑MulEquiv.prodComm.symm = Prod.swap
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>⇑AddEquiv.prodComm.symm = Prod.swap
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<VAR>M' : Type u_8<VAR>N' : Type u_9<VAR>MulOneClass M'<VAR>MulOneClass N'<VAR>mnmn : (M × N) × M' × N'<GOAL>(MulEquiv.prodProdProdComm M N M' N') mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>M' : Type u_8<VAR>N' : Type u_9<VAR>AddZeroClass M'<VAR>AddZeroClass N'<VAR>mnmn : (M × N) × M' × N'<GOAL>(AddEquiv.prodProdProdComm M N M' N') mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<VAR>M' : Type u_8<VAR>N' : Type u_9<VAR>MulOneClass M'<VAR>MulOneClass N'<GOAL>↑(MulEquiv.prodProdProdComm M N M' N') = Equiv.prodProdProdComm M N M' N'
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>M' : Type u_8<VAR>N' : Type u_9<VAR>AddZeroClass M'<VAR>AddZeroClass N'<GOAL>↑(AddEquiv.prodProdProdComm M N M' N') = Equiv.prodProdProdComm M N M' N'
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<VAR>M' : Type u_8<VAR>N' : Type u_9<VAR>MulOneClass M'<VAR>MulOneClass N'<GOAL>(MulEquiv.prodProdProdComm M N M' N').symm = MulEquiv.prodProdProdComm M M' N N'
<VAR>α : Type u_8<VAR>Monoid α<VAR>x : αˣ<GOAL>(Units.embedProduct α) x = (↑x, MulOpposite.op ↑x⁻¹)
<VAR>α : Type u_8<VAR>AddMonoid α<VAR>x : AddUnits α<GOAL>(AddUnits.embedProduct α) x = (↑x, AddOpposite.op ↑(-x))
<VAR>α : Type u_8<VAR>AddMonoid α<GOAL>Function.Injective ⇑(AddUnits.embedProduct α)
<VAR>α : Type u_8<VAR>Monoid α<GOAL>Function.Injective ⇑(Units.embedProduct α)
<VAR>α : Type u_8<VAR>CommSemigroup α<VAR>a : α × α<GOAL>mulMulHom a = a.1 * a.2
<VAR>α : Type u_8<VAR>AddCommSemigroup α<VAR>a : α × α<GOAL>addAddHom a = a.1 + a.2
<VAR>α : Type u_8<VAR>CommMonoid α<GOAL>∀ (a : α × α), mulMonoidHom a = mulMulHom.toFun a
<VAR>α : Type u_8<VAR>AddCommMonoid α<GOAL>∀ (a : α × α), addAddMonoidHom a = addAddHom.toFun a
<VAR>α : Type u_8<VAR>SubtractionCommMonoid α<VAR>a : α × α<GOAL>subAddMonoidHom a = a.1 - a.2
<VAR>α : Type u_8<VAR>DivisionCommMonoid α<VAR>a : α × α<GOAL>divMonoidHom a = a.1 / a.2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>Algebra ℚ R<VAR>Algebra ℚ S<VAR>f : R →+* S<GOAL>↑f.toRatAlgHom = f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>Algebra ℚ R<VAR>Algebra ℚ S<VAR>f : R →ₐ[ℚ] S<GOAL>(↑f).toRatAlgHom = f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>Algebra ℚ R<VAR>Algebra ℚ S<VAR>self : R →ₐ[ℚ] S<GOAL>RingHom.equivRatAlgHom.symm self = self.toRingHom
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>Algebra ℚ R<VAR>Algebra ℚ S<VAR>f : R →+* S<GOAL>RingHom.equivRatAlgHom f = f.toRatAlgHom
<VAR>A : Type u_1<VAR>AddMonoid A<VAR>M : Type u_2<VAR>Monoid M<VAR>self : AddChar A M<VAR>a b : A<GOAL>self.toFun (a + b) = self.toFun a * self.toFun b
<VAR>A : Type u_1<VAR>AddMonoid A<VAR>M : Type u_2<VAR>Monoid M<VAR>self : AddChar A M<GOAL>self.toFun 0 = 1
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>f g : AddChar A M<VAR>h : ∀ (x : A), f x = g x<GOAL>f = g
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>f : A → M<VAR>map_zero_eq_one' : f 0 = 1<VAR>map_add_eq_mul' : ∀ (a b : A), f (a + b) = f a * f b<GOAL>⇑{ toFun := f, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' } = f
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>ψ : AddChar A M<GOAL>ψ 0 = 1
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>ψ : AddChar A M<VAR>x y : A<GOAL>ψ (x + y) = ψ x * ψ y
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>ψ : AddChar A M<VAR>a : Multiplicative A<GOAL>ψ.toMonoidHom a = ψ (Multiplicative.toAdd a)
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>ψ : AddChar A M<VAR>n : ℕ<VAR>x : A<GOAL>ψ (n • x) = ψ x ^ n
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>ψ : AddChar A M<GOAL>⇑(AddChar.toMonoidHomEquiv ψ) = ⇑ψ ∘ ⇑Multiplicative.toAdd
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>ψ : Multiplicative A →* M<GOAL>⇑(AddChar.toMonoidHomEquiv.symm ψ) = ⇑ψ ∘ ⇑Multiplicative.ofAdd
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>ψ : AddChar A M<VAR>a : Multiplicative A<GOAL>(AddChar.toMonoidHomEquiv ψ) a = ψ (Multiplicative.toAdd a)
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>ψ : Multiplicative A →* M<VAR>a : A<GOAL>(AddChar.toMonoidHomEquiv.symm ψ) a = ψ (Multiplicative.ofAdd a)
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>ψ : AddChar A M<GOAL>⇑ψ.toAddMonoidHom = ⇑Additive.ofMul ∘ ⇑ψ
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>ψ : AddChar A M<VAR>a : A<GOAL>ψ.toAddMonoidHom a = Additive.ofMul (ψ a)
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>ψ : AddChar A M<GOAL>⇑(AddChar.toAddMonoidHomEquiv ψ) = ⇑Additive.ofMul ∘ ⇑ψ
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>ψ : A →+ Additive M<GOAL>⇑(AddChar.toAddMonoidHomEquiv.symm ψ) = ⇑Additive.toMul ∘ ⇑ψ
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>ψ : AddChar A M<VAR>a : A<GOAL>(AddChar.toAddMonoidHomEquiv ψ) a = Additive.ofMul (ψ a)
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>ψ : A →+ Additive M<VAR>a : A<GOAL>(AddChar.toAddMonoidHomEquiv.symm ψ) a = Additive.toMul (ψ a)
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<GOAL>⇑1 = 1
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>a : A<GOAL>1 a = 1
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>N : Type u_5<VAR>Monoid N<VAR>f : M →* N<VAR>φ : AddChar A M<GOAL>⇑(f.compAddChar φ) = ⇑f ∘ ⇑φ
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>N : Type u_4<VAR>AddMonoid A<VAR>Monoid M<VAR>Monoid N<VAR>f : M →* N<VAR>φ : AddChar A M<GOAL>⇑(f.compAddChar φ) = ⇑f ∘ ⇑φ
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>N : Type u_4<VAR>AddMonoid A<VAR>Monoid M<VAR>Monoid N<VAR>ψ : AddChar A M<VAR>hψ : Function.Surjective ⇑ψ<GOAL>Function.Injective fun f => f.compAddChar ψ
<VAR>B : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>AddMonoid B<VAR>Monoid M<VAR>Monoid N<VAR>f : M →* N<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective fun ψ => f.compAddChar ψ
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>M : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>Monoid M<VAR>φ : AddChar B M<VAR>f : A →+ B<GOAL>⇑(φ.compAddMonoidHom f) = ⇑φ ∘ ⇑f
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>M : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>Monoid M<VAR>ψ : AddChar B M<VAR>f : A →+ B<VAR>a : A<GOAL>(ψ.compAddMonoidHom f) a = ψ (f a)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>M : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>Monoid M<VAR>f : A →+ B<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Injective fun ψ => ψ.compAddMonoidHom f
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>M : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>Monoid M<VAR>ψ : AddChar B M<VAR>hψ : Function.Injective ⇑ψ<GOAL>Function.Injective fun f => ψ.compAddMonoidHom f
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>ψ : AddChar A M<GOAL>ψ = 1 ↔ ∀ (x : A), ψ x = 1
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>ψ : AddChar A M<GOAL>ψ ≠ 1 ↔ ∃ x, ψ x ≠ 1
<VAR>A : Type u_1<VAR>M : Type u_3<VAR>AddMonoid A<VAR>Monoid M<VAR>ψ : AddChar A M<GOAL>ψ.IsNontrivial ↔ ψ ≠ 1
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>AddMonoid A<VAR>CommMonoid M<VAR>ψ χ : AddChar A M<GOAL>⇑(ψ * χ) = ⇑ψ * ⇑χ
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>AddMonoid A<VAR>CommMonoid M<VAR>ψ : AddChar A M<VAR>n : ℕ<GOAL>⇑(ψ ^ n) = ⇑ψ ^ n
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>AddMonoid A<VAR>CommMonoid M<VAR>ψ φ : AddChar A M<VAR>a : A<GOAL>(ψ * φ) a = ψ a * φ a
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>AddMonoid A<VAR>CommMonoid M<VAR>ψ : AddChar A M<VAR>n : ℕ<VAR>a : A<GOAL>(ψ ^ n) a = ψ a ^ n
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>AddCommGroup A<VAR>CommMonoid M<VAR>ψ : AddChar A M<VAR>x : A<GOAL>ψ⁻¹ x = ψ (-x)
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>AddGroup A<VAR>Monoid M<VAR>φ : AddChar A M<VAR>a : A<GOAL>IsUnit (φ a)
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>AddGroup A<VAR>DivisionMonoid M<VAR>ψ : AddChar A M<VAR>a : A<GOAL>ψ (-a) = (ψ a)⁻¹
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>AddGroup A<VAR>DivisionMonoid M<VAR>ψ : AddChar A M<VAR>n : ℤ<VAR>a : A<GOAL>ψ (n • a) = ψ a ^ n
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>AddCommGroup A<VAR>DivisionCommMonoid M<VAR>ψ : AddChar A M<VAR>x : A<GOAL>ψ⁻¹ x = (ψ x)⁻¹
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>AddCommGroup A<VAR>DivisionCommMonoid M<VAR>ψ : AddChar A M<VAR>a b : A<GOAL>ψ (a - b) = ψ a / ψ b
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>AddCommGroup A<VAR>DivisionCommMonoid M<VAR>ψ : AddChar A M<GOAL>Function.Injective ⇑ψ ↔ ∀ ⦃x : A⦄, ψ x = 1 → x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>CommMonoid M<VAR>ψ : AddChar R M<VAR>r x : R<GOAL>(ψ.mulShift r) x = ψ (r * x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>CommMonoid M<VAR>ψ : AddChar R M<GOAL>ψ⁻¹ = ψ.mulShift (-1)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>CommMonoid M<VAR>ψ : AddChar R M<VAR>n : ℕ<VAR>x : R<GOAL>(ψ.mulShift ↑n) x = ψ x ^ n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>CommMonoid M<VAR>ψ : AddChar R M<VAR>n : ℕ<GOAL>ψ ^ n = ψ.mulShift ↑n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>CommMonoid M<VAR>ψ : AddChar R M<VAR>r s : R<GOAL>ψ.mulShift r * ψ.mulShift s = ψ.mulShift (r + s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>CommMonoid M<VAR>ψ : AddChar R M<VAR>r s : R<GOAL>(ψ.mulShift r).mulShift s = ψ.mulShift (r * s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>CommMonoid M<VAR>ψ : AddChar R M<GOAL>ψ.mulShift 0 = 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>CommMonoid M<VAR>ψ : AddChar R M<GOAL>ψ.mulShift 1 = ψ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>CommMonoid M<VAR>ψ : AddChar R M<VAR>u : R<VAR>hu : IsUnit u<GOAL>ψ.mulShift u = 1 ↔ ψ = 1