ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>g : N →+ P<VAR>f : M →+ N<GOAL>AddSubmonoid.comap f (AddMonoidHom.mker g) = AddMonoidHom.mker (g.comp f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>g : N →* P<VAR>f : M →* N<GOAL>Submonoid.comap f (MonoidHom.mker g) = MonoidHom.mker (g.comp f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<GOAL>AddSubmonoid.comap f ⊥ = AddMonoidHom.mker f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<GOAL>Submonoid.comap f ⊥ = MonoidHom.mker f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>S : AddSubmonoid M<VAR>f : M →+ N<GOAL>AddMonoidHom.mker (f.restrict S) = AddSubmonoid.comap S.subtype (AddMonoidHom.mker f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>S : Submonoid M<VAR>f : M →* N<GOAL>MonoidHom.mker (f.restrict S) = Submonoid.comap S.subtype (MonoidHom.mker f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<GOAL>MonoidHom.mker f.mrangeRestrict = MonoidHom.mker f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<GOAL>AddMonoidHom.mker f.mrangeRestrict = AddMonoidHom.mker f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoidHom.mker 0 = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>MonoidHom.mker 1 = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>AddZeroClass M'<VAR>AddZeroClass N'<VAR>f : M →+ N<VAR>g : M' →+ N'<VAR>S : AddSubmonoid N<VAR>S' : AddSubmonoid N'<GOAL>AddSubmonoid.comap (f.prodMap g) (S.prod S') = (AddSubmonoid.comap f S).prod (AddSubmonoid.comap g S')
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>MulOneClass M'<VAR>MulOneClass N'<VAR>f : M →* N<VAR>g : M' →* N'<VAR>S : Submonoid N<VAR>S' : Submonoid N'<GOAL>Submonoid.comap (f.prodMap g) (S.prod S') = (Submonoid.comap f S).prod (Submonoid.comap g S')
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>MulOneClass M'<VAR>MulOneClass N'<VAR>f : M →* N<VAR>g : M' →* N'<GOAL>MonoidHom.mker (f.prodMap g) = (MonoidHom.mker f).prod (MonoidHom.mker g)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>AddZeroClass M'<VAR>AddZeroClass N'<VAR>f : M →+ N<VAR>g : M' →+ N'<GOAL>AddMonoidHom.mker (f.prodMap g) = (AddMonoidHom.mker f).prod (AddMonoidHom.mker g)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoidHom.mker (AddMonoidHom.inl M N) = ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>MonoidHom.mker (MonoidHom.inl M N) = ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoidHom.mker (AddMonoidHom.inr M N) = ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>MonoidHom.mker (MonoidHom.inr M N) = ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>MonoidHom.mker (MonoidHom.fst M N) = ⊥.prod ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoidHom.mker (AddMonoidHom.fst M N) = ⊥.prod ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoidHom.mker (AddMonoidHom.snd M N) = ⊤.prod ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>MonoidHom.mker (MonoidHom.snd M N) = ⊤.prod ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<VAR>N' : AddSubmonoid N<VAR>x : ↥(AddSubmonoid.comap f N')<GOAL>↑((f.addSubmonoidComap N') x) = f ↑x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<VAR>N' : Submonoid N<VAR>x : ↥(Submonoid.comap f N')<GOAL>↑((f.submonoidComap N') x) = f ↑x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<VAR>M' : Submonoid M<VAR>x : ↥M'<GOAL>↑((f.submonoidMap M') x) = f ↑x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<VAR>M' : AddSubmonoid M<VAR>x : ↥M'<GOAL>↑((f.addSubmonoidMap M') x) = f ↑x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<VAR>M' : Submonoid M<GOAL>Function.Surjective ⇑(f.submonoidMap M')
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<VAR>M' : AddSubmonoid M<GOAL>Function.Surjective ⇑(f.addSubmonoidMap M')
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>MonoidHom.mrange (MonoidHom.inl M N) = ⊤.prod ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoidHom.mrange (AddMonoidHom.inl M N) = ⊤.prod ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>MonoidHom.mrange (MonoidHom.inr M N) = ⊥.prod ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoidHom.mrange (AddMonoidHom.inr M N) = ⊥.prod ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>MonoidHom.mrange (MonoidHom.inl M N) = Submonoid.comap (MonoidHom.snd M N) ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoidHom.mrange (AddMonoidHom.inl M N) = AddSubmonoid.comap (AddMonoidHom.snd M N) ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>MonoidHom.mrange (MonoidHom.inr M N) = Submonoid.comap (MonoidHom.fst M N) ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoidHom.mrange (AddMonoidHom.inr M N) = AddSubmonoid.comap (AddMonoidHom.fst M N) ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoidHom.mrange (AddMonoidHom.fst M N) = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>MonoidHom.mrange (MonoidHom.fst M N) = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>MonoidHom.mrange (MonoidHom.snd M N) = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoidHom.mrange (AddMonoidHom.snd M N) = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>s : AddSubmonoid M<VAR>t : AddSubmonoid N<GOAL>s.prod t = ⊥ ↔ s = ⊥ ∧ t = ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>s : Submonoid M<VAR>t : Submonoid N<GOAL>s.prod t = ⊥ ↔ s = ⊥ ∧ t = ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>s : Submonoid M<VAR>t : Submonoid N<GOAL>s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>s : AddSubmonoid M<VAR>t : AddSubmonoid N<GOAL>s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>AddMonoidHom.mrange (AddMonoidHom.inl M N) ⊔ AddMonoidHom.mrange (AddMonoidHom.inr M N) = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>MonoidHom.mrange (MonoidHom.inl M N) ⊔ MonoidHom.mrange (MonoidHom.inr M N) = ⊤
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s : Submonoid M<GOAL>MonoidHom.mrange s.subtype = s
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>s : AddSubmonoid M<GOAL>AddMonoidHom.mrange s.subtype = s
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<GOAL>S = ⊤ ↔ ∀ (x : M), x ∈ S
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<GOAL>S = ⊤ ↔ ∀ (x : M), x ∈ S
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<GOAL>S = ⊥ ↔ ∀ x ∈ S, x = 1
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<GOAL>S = ⊥ ↔ ∀ x ∈ S, x = 0
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<VAR>Subsingleton ↥S<GOAL>S = ⊥
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<VAR>Subsingleton ↥S<GOAL>S = ⊥
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<GOAL>Nontrivial ↥S ↔ ∃ x ∈ S, x ≠ 1
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<GOAL>Nontrivial ↥S ↔ ∃ x ∈ S, x ≠ 0
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<GOAL>S = ⊥ ∨ Nontrivial ↥S
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<GOAL>S = ⊥ ∨ Nontrivial ↥S
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<GOAL>S = ⊥ ∨ ∃ x ∈ S, x ≠ 1
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<GOAL>S = ⊥ ∨ ∃ x ∈ S, x ≠ 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<VAR>g : N → M<VAR>h : Function.LeftInverse g ⇑f<GOAL>∀ (a : ↥(AddMonoidHom.mrange f)), (AddEquiv.ofLeftInverse' f h).symm a = g ↑a
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<VAR>g : N → M<VAR>h : Function.LeftInverse g ⇑f<GOAL>∀ (a : ↥(MonoidHom.mrange f)), (MulEquiv.ofLeftInverse' f h).symm a = g ↑a
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<VAR>g : N → M<VAR>h : Function.LeftInverse g ⇑f<VAR>a : M<GOAL>(AddEquiv.ofLeftInverse' f h) a = f.mrangeRestrict a
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass 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.mrangeRestrict a
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>e : M ≃* N<VAR>S : Submonoid M<VAR>g : ↥S<GOAL>↑((e.submonoidMap S) g) = e ↑g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>e : M ≃+ N<VAR>S : AddSubmonoid M<VAR>g : ↥S<GOAL>↑((e.addSubmonoidMap S) g) = e ↑g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>e : M ≃+ N<VAR>S : AddSubmonoid M<VAR>g : ↥(AddSubmonoid.map (↑e) S)<GOAL>(e.addSubmonoidMap S).symm g = ⟨e.symm ↑g, ⋯⟩
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>e : M ≃* N<VAR>S : Submonoid M<VAR>g : ↥(Submonoid.map (↑e) S)<GOAL>(e.submonoidMap S).symm g = ⟨e.symm ↑g, ⋯⟩
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>S : AddSubmonoid M<VAR>e : M ≃+ N<GOAL>S.equivMapOfInjective ↑e ⋯ = e.addSubmonoidMap S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>S : Submonoid M<VAR>e : M ≃* N<GOAL>S.equivMapOfInjective ↑e ⋯ = e.submonoidMap S
<VAR>M' : Type u_5<VAR>α : Type u_6<VAR>MulOneClass M'<VAR>SMul M' α<VAR>S : Submonoid M'<VAR>g : ↥S<VAR>a : α<GOAL>g • a = ↑g • a
<VAR>M' : Type u_5<VAR>α : Type u_6<VAR>AddZeroClass M'<VAR>VAdd M' α<VAR>S : AddSubmonoid M'<VAR>g : ↥S<VAR>a : α<GOAL>g +ᵥ a = ↑g +ᵥ a
<VAR>M' : Type u_5<VAR>α : Type u_6<VAR>AddZeroClass M'<VAR>VAdd M' α<VAR>S : AddSubmonoid M'<VAR>g : M'<VAR>hg : g ∈ S<VAR>a : α<GOAL>⟨g, hg⟩ +ᵥ a = g +ᵥ a
<VAR>M' : Type u_5<VAR>α : Type u_6<VAR>MulOneClass M'<VAR>SMul M' α<VAR>S : Submonoid M'<VAR>g : M'<VAR>hg : g ∈ S<VAR>a : α<GOAL>⟨g, hg⟩ • a = g • a
<VAR>M : Type u_1<VAR>Monoid M<VAR>x : ↥(IsUnit.submonoid M)<GOAL>↑(Submonoid.unitsTypeEquivIsUnitSubmonoid.symm x) = ↑x
<VAR>M : Type u_1<VAR>Monoid M<VAR>x : Mˣ<GOAL>↑(Submonoid.unitsTypeEquivIsUnitSubmonoid x) = ↑x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>x : AddUnits M<GOAL>↑(AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid x) = ↑x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>x : ↥(IsAddUnit.addSubmonoid M)<GOAL>↑(AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid.symm x) = ↑x
<VAR>M : Type u_1<VAR>Monoid M<VAR>x : ↥(IsUnit.submonoid M)<GOAL>↑(Submonoid.unitsTypeEquivIsUnitSubmonoid.symm x)⁻¹ = ↑(Classical.choose ⋯)⁻¹
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>x : ↥(IsAddUnit.addSubmonoid M)<GOAL>↑(-AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid.symm x) = ↑(-Classical.choose ⋯)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>S : Submonoid N<GOAL>Submonoid.map f (Submonoid.comap f S) = S ⊓ MonoidHom.mrange f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>S : AddSubmonoid N<GOAL>AddSubmonoid.map f (AddSubmonoid.comap f S) = S ⊓ AddMonoidHom.mrange f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>S : Submonoid N<VAR>h : S ≤ MonoidHom.mrange f<GOAL>Submonoid.map f (Submonoid.comap f S) = S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>S : AddSubmonoid N<VAR>h : S ≤ AddMonoidHom.mrange f<GOAL>AddSubmonoid.map f (AddSubmonoid.comap f S) = S
<VAR>α : Type u<VAR>Zero α<GOAL>ULift.down 0 = 0
<VAR>α : Type u<VAR>One α<GOAL>ULift.down 1 = 1
<VAR>α : Type u<VAR>x y : ULift.{v, u} α<VAR>Add α<GOAL>(x + y).down = x.down + y.down
<VAR>α : Type u<VAR>x y : ULift.{v, u} α<VAR>Mul α<GOAL>(x * y).down = x.down * y.down
<VAR>α : Type u<VAR>x y : ULift.{v, u} α<VAR>Sub α<GOAL>(x - y).down = x.down - y.down
<VAR>α : Type u<VAR>x y : ULift.{v, u} α<VAR>Div α<GOAL>(x / y).down = x.down / y.down
<VAR>α : Type u<VAR>x : ULift.{v, u} α<VAR>Neg α<GOAL>(-x).down = -x.down
<VAR>α : Type u<VAR>x : ULift.{v, u} α<VAR>Inv α<GOAL>x⁻¹.down = x.down⁻¹
<VAR>α : Type u<VAR>β : Type u_1<VAR>VAdd α β<VAR>a : α<VAR>b : ULift.{v, u_1} β<GOAL>(a +ᵥ b).down = a +ᵥ b.down
<VAR>α : Type u<VAR>β : Type u_1<VAR>SMul α β<VAR>a : α<VAR>b : ULift.{v, u_1} β<GOAL>(a • b).down = a • b.down
<VAR>α : Type u<VAR>β : Type u_1<VAR>Pow α β<VAR>a : ULift.{v, u} α<VAR>b : β<GOAL>(a ^ b).down = a.down ^ b
<VAR>α : Type u<VAR>NatCast α<VAR>n : ℕ<GOAL>{ down := ↑n } = ↑n
<VAR>α : Type u<VAR>NatCast α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>{ down := OfNat.ofNat n } = OfNat.ofNat n
<VAR>α : Type u<VAR>IntCast α<VAR>n : ℤ<GOAL>{ down := ↑n } = ↑n
<VAR>α : Type u<VAR>NatCast α<VAR>n : ℕ<GOAL>(↑n).down = ↑n
<VAR>α : Type u<VAR>NatCast α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).down = OfNat.ofNat n
<VAR>α : Type u<VAR>IntCast α<VAR>n : ℤ<GOAL>(↑n).down = ↑n
<VAR>n : ℕ<VAR>a : Fin (n + 1)<GOAL>↑(a - 1) = if a = 0 then n else ↑a - 1
<VAR>n : ℕ<VAR>k : Fin (n + 2)<GOAL>k < k - 1 ↔ k = 0
<VAR>n : ℕ<VAR>k : Fin (n + 1)<GOAL>k ≤ k - 1 ↔ k = 0
<VAR>n : ℕ<VAR>k : Fin (n + 1)<GOAL>k - 1 < k ↔ 0 < k
<VAR>n : ℕ<GOAL>-Fin.last n = 1
<VAR>n : ℕ<GOAL>-↑n = 1
<VAR>m n : ℕ<GOAL>m • n = m * n
<VAR>a : Multiplicative ℕ<VAR>b : ℕ<GOAL>Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * b
<VAR>a b : ℕ<GOAL>Multiplicative.ofAdd (a * b) = Multiplicative.ofAdd a ^ b
<VAR>n : ℕ<GOAL>Even n ↔ n % 2 = 0
<VAR>n : ℕ<GOAL>¬Even n ↔ n % 2 = 1
<VAR>n : ℕ<GOAL>¬2 ∣ n ↔ n % 2 = 1
<VAR>n : ℕ<GOAL>Even (n + 1) ↔ ¬Even n
<VAR>m : ℕ<GOAL>(m + 1) % 2 = 0 ↔ m % 2 = 1
<VAR>m : ℕ<GOAL>(m + 1) % 2 = 1 ↔ m % 2 = 0
<VAR>n : ℕ<GOAL>¬2 ∣ 2 * n + 1
<VAR>n : ℕ<GOAL>0 < n → ¬2 ∣ 2 * n - 1
<VAR>m n : ℕ<GOAL>Even (m ^ n) ↔ Even m ∧ n ≠ 0
<VAR>m n : ℕ<VAR>h : n ≠ 0<GOAL>Even (m ^ n) ↔ Even m
<VAR>n : ℕ<GOAL>Even (n * (n + 1))
<VAR>n : ℕ<GOAL>Even (n * (n - 1))
<VAR>n : ℕ<GOAL>Even n → 2 * (n / 2) = n
<VAR>n : ℕ<GOAL>Even n → n / 2 * 2 = n
<VAR>u : AddUnits ℕ<GOAL>u = 0
<VAR>n : ℕ<GOAL>IsUnit n ↔ n = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>VAdd α β<GOAL>VAdd.vadd = HVAdd.hVAdd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<GOAL>SMul.smul = HSMul.hSMul
<VAR>G : Type u<VAR>Mul G<VAR>self : IsLeftCancelMul G<VAR>a b c : G<GOAL>a * b = a * c → b = c
<VAR>G : Type u<VAR>Mul G<VAR>self : IsRightCancelMul G<VAR>a b c : G<GOAL>a * b = c * b → a = c
<VAR>G : Type u<VAR>Add G<VAR>self : IsLeftCancelAdd G<VAR>a b c : G<GOAL>a + b = a + c → b = c
<VAR>G : Type u<VAR>Add G<VAR>self : IsRightCancelAdd G<VAR>a b c : G<GOAL>a + b = c + b → a = c
<VAR>G : Type u_1<VAR>Add G<VAR>IsLeftCancelAdd G<VAR>a b c : G<GOAL>a + b = a + c → b = c
<VAR>G : Type u_1<VAR>Mul G<VAR>IsLeftCancelMul G<VAR>a b c : G<GOAL>a * b = a * c → b = c
<VAR>G : Type u_1<VAR>Mul G<VAR>IsLeftCancelMul G<VAR>a b c : G<GOAL>a * b = a * c ↔ b = c
<VAR>G : Type u_1<VAR>Add G<VAR>IsLeftCancelAdd G<VAR>a b c : G<GOAL>a + b = a + c ↔ b = c
<VAR>G : Type u_1<VAR>Add G<VAR>IsRightCancelAdd G<VAR>a b c : G<GOAL>a + b = c + b → a = c
<VAR>G : Type u_1<VAR>Mul G<VAR>IsRightCancelMul G<VAR>a b c : G<GOAL>a * b = c * b → a = c
<VAR>G : Type u_1<VAR>Add G<VAR>IsRightCancelAdd G<VAR>a b c : G<GOAL>b + a = c + a ↔ b = c
<VAR>G : Type u_1<VAR>Mul G<VAR>IsRightCancelMul G<VAR>a b c : G<GOAL>b * a = c * a ↔ b = c
<VAR>G : Type u<VAR>self : Semigroup G<VAR>a b c : G<GOAL>a * b * c = a * (b * c)
<VAR>G : Type u<VAR>self : AddSemigroup G<VAR>a b c : G<GOAL>a + b + c = a + (b + c)
<VAR>G : Type u_1<VAR>Semigroup G<VAR>a b c : G<GOAL>a * b * c = a * (b * c)
<VAR>G : Type u_1<VAR>AddSemigroup G<VAR>a b c : G<GOAL>a + b + c = a + (b + c)
<VAR>G : Type u<VAR>self : AddCommMagma G<VAR>a b : G<GOAL>a + b = b + a
<VAR>G : Type u<VAR>self : CommMagma G<VAR>a b : G<GOAL>a * b = b * a
<VAR>G : Type u_1<VAR>CommMagma G<VAR>a b : G<GOAL>a * b = b * a
<VAR>G : Type u_1<VAR>AddCommMagma G<VAR>a b : G<GOAL>a + b = b + a
<VAR>G : Type u<VAR>AddCommMagma G<VAR>IsRightCancelAdd G<GOAL>IsLeftCancelAdd G
<VAR>G : Type u<VAR>CommMagma G<VAR>IsRightCancelMul G<GOAL>IsLeftCancelMul G
<VAR>G : Type u<VAR>CommMagma G<VAR>IsLeftCancelMul G<GOAL>IsRightCancelMul G
<VAR>G : Type u<VAR>AddCommMagma G<VAR>IsLeftCancelAdd G<GOAL>IsRightCancelAdd G
<VAR>G : Type u<VAR>CommMagma G<VAR>IsLeftCancelMul G<GOAL>IsCancelMul G
<VAR>G : Type u<VAR>AddCommMagma G<VAR>IsLeftCancelAdd G<GOAL>IsCancelAdd G
<VAR>G : Type u<VAR>CommMagma G<VAR>IsRightCancelMul G<GOAL>IsCancelMul G
<VAR>G : Type u<VAR>AddCommMagma G<VAR>IsRightCancelAdd G<GOAL>IsCancelAdd G
<VAR>G : Type u<VAR>self : LeftCancelSemigroup G<VAR>a b c : G<GOAL>a * b = a * c → b = c
<VAR>G : Type u<VAR>self : AddLeftCancelSemigroup G<VAR>a b c : G<GOAL>a + b = a + c → b = c
<VAR>G : Type u<VAR>self : RightCancelSemigroup G<VAR>a b c : G<GOAL>a * b = c * b → a = c
<VAR>G : Type u<VAR>self : AddRightCancelSemigroup G<VAR>a b c : G<GOAL>a + b = c + b → a = c
<VAR>M : Type u<VAR>self : MulOneClass M<VAR>a : M<GOAL>1 * a = a
<VAR>M : Type u<VAR>self : MulOneClass M<VAR>a : M<GOAL>a * 1 = a
<VAR>M : Type u<VAR>self : AddZeroClass M<VAR>a : M<GOAL>a + 0 = a
<VAR>M : Type u<VAR>self : AddZeroClass M<VAR>a : M<GOAL>0 + a = a
<VAR>M : Type u<VAR>m₁ m₂ : AddZeroClass M<GOAL>Add.add = Add.add → m₁ = m₂
<VAR>M : Type u<VAR>m₁ m₂ : MulOneClass M<GOAL>Mul.mul = Mul.mul → m₁ = m₂
<VAR>M : Type u<VAR>AddZeroClass M<VAR>a : M<GOAL>0 + a = a
<VAR>M : Type u<VAR>MulOneClass M<VAR>a : M<GOAL>1 * a = a
<VAR>M : Type u<VAR>AddZeroClass M<VAR>a : M<GOAL>a + 0 = a
<VAR>M : Type u<VAR>MulOneClass M<VAR>a : M<GOAL>a * 1 = a
<VAR>M : Type u<VAR>self : AddMonoid M<VAR>x : M<GOAL>AddMonoid.nsmul 0 x = 0
<VAR>M : Type u<VAR>self : AddMonoid M<VAR>n : ℕ<VAR>x : M<GOAL>AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
<VAR>M : Type u<VAR>self : Monoid M<VAR>x : M<GOAL>Monoid.npow 0 x = 1
<VAR>M : Type u<VAR>self : Monoid M<VAR>n : ℕ<VAR>x : M<GOAL>Monoid.npow (n + 1) x = Monoid.npow n x * x
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>n : ℕ<VAR>x : M<GOAL>AddMonoid.nsmul n x = n • x
<VAR>M : Type u_2<VAR>Monoid M<VAR>n : ℕ<VAR>x : M<GOAL>Monoid.npow n x = x ^ n
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a b c : M<VAR>hba : b + a = 0<VAR>hac : a + c = 0<GOAL>b = c
<VAR>M : Type u_2<VAR>Monoid M<VAR>a b c : M<VAR>hba : b * a = 1<VAR>hac : a * c = 1<GOAL>b = c
<VAR>M : Type u_2<VAR>Monoid M<VAR>a : M<GOAL>a ^ 0 = 1
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a : M<GOAL>0 • a = 0
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a : M<VAR>n : ℕ<GOAL>(n + 1) • a = n • a + a
<VAR>M : Type u_2<VAR>Monoid M<VAR>a : M<VAR>n : ℕ<GOAL>a ^ (n + 1) = a ^ n * a
<VAR>M : Type u_2<VAR>Monoid M<VAR>a : M<GOAL>a ^ 1 = a
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a : M<GOAL>1 • a = a
<VAR>M : Type u_2<VAR>Monoid M<VAR>a : M<VAR>n : ℕ<GOAL>a ^ (n + 1) = a * a ^ n
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a : M<VAR>n : ℕ<GOAL>(n + 1) • a = a + n • a
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a : M<VAR>n : ℕ<GOAL>n • a + a = a + n • a
<VAR>M : Type u_2<VAR>Monoid M<VAR>a : M<VAR>n : ℕ<GOAL>a ^ n * a = a * a ^ n
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a : M<GOAL>2 • a = a + a
<VAR>M : Type u_2<VAR>Monoid M<VAR>a : M<GOAL>a ^ 2 = a * a
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a : M<GOAL>3 • a = a + a + a
<VAR>M : Type u_2<VAR>Monoid M<VAR>a : M<GOAL>a ^ 3 = a * a * a
<VAR>M : Type u_2<VAR>Monoid M<VAR>a : M<GOAL>a ^ 3 = a * (a * a)
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a : M<GOAL>3 • a = a + (a + a)
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>n : ℕ<GOAL>n • 0 = 0
<VAR>M : Type u_2<VAR>Monoid M<VAR>n : ℕ<GOAL>1 ^ n = 1
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a : M<VAR>m n : ℕ<GOAL>(m + n) • a = m • a + n • a
<VAR>M : Type u_2<VAR>Monoid M<VAR>a : M<VAR>m n : ℕ<GOAL>a ^ (m + n) = a ^ m * a ^ n
<VAR>M : Type u_2<VAR>Monoid M<VAR>a : M<VAR>m n : ℕ<GOAL>a ^ m * a ^ n = a ^ n * a ^ m
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a : M<VAR>m n : ℕ<GOAL>m • a + n • a = n • a + m • a
<VAR>M : Type u_2<VAR>Monoid M<VAR>a : M<VAR>m n : ℕ<GOAL>a ^ (m * n) = (a ^ m) ^ n
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a : M<VAR>m n : ℕ<GOAL>(m * n) • a = n • m • a
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a : M<VAR>m n : ℕ<GOAL>(m * n) • a = m • n • a
<VAR>M : Type u_2<VAR>Monoid M<VAR>a : M<VAR>m n : ℕ<GOAL>a ^ (m * n) = (a ^ n) ^ m
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a : M<VAR>m n : ℕ<GOAL>n • m • a = m • n • a
<VAR>M : Type u_2<VAR>Monoid M<VAR>a : M<VAR>m n : ℕ<GOAL>(a ^ m) ^ n = (a ^ n) ^ m
<VAR>A : Type u_2<VAR>self : InvolutiveNeg A<VAR>x : A<GOAL>- -x = x
<VAR>G : Type u_2<VAR>self : InvolutiveInv G<VAR>x : G<GOAL>x⁻¹⁻¹ = x
<VAR>G : Type u_1<VAR>InvolutiveNeg G<VAR>a : G<GOAL>- -a = a
<VAR>G : Type u_1<VAR>InvolutiveInv G<VAR>a : G<GOAL>a⁻¹⁻¹ = a
<VAR>G : Type u<VAR>self : DivInvMonoid G<VAR>n : ℕ<VAR>a : G<GOAL>DivInvMonoid.zpow (Int.ofNat n.succ) a = DivInvMonoid.zpow (Int.ofNat n) a * a
<VAR>G : Type u<VAR>self : DivInvMonoid G<VAR>n : ℕ<VAR>a : G<GOAL>DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
<VAR>G : Type u<VAR>self : DivInvMonoid G<VAR>a : G<GOAL>DivInvMonoid.zpow 0 a = 1
<VAR>G : Type u<VAR>self : DivInvMonoid G<VAR>a b : G<GOAL>a / b = a * b⁻¹
<VAR>G : Type u<VAR>self : SubNegMonoid G<VAR>a : G<GOAL>SubNegMonoid.zsmul 0 a = 0
<VAR>G : Type u<VAR>self : SubNegMonoid G<VAR>n : ℕ<VAR>a : G<GOAL>SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
<VAR>G : Type u<VAR>self : SubNegMonoid G<VAR>a b : G<GOAL>a - b = a + -b
<VAR>G : Type u<VAR>self : SubNegMonoid G<VAR>n : ℕ<VAR>a : G<GOAL>SubNegMonoid.zsmul (Int.ofNat n.succ) a = SubNegMonoid.zsmul (Int.ofNat n) a + a
<VAR>G : Type u_1<VAR>DivInvMonoid G<VAR>n : ℤ<VAR>x : G<GOAL>DivInvMonoid.zpow n x = x ^ n
<VAR>G : Type u_1<VAR>SubNegMonoid G<VAR>n : ℤ<VAR>x : G<GOAL>SubNegMonoid.zsmul n x = n • x
<VAR>G : Type u_1<VAR>SubNegMonoid G<VAR>a : G<GOAL>0 • a = 0
<VAR>G : Type u_1<VAR>DivInvMonoid G<VAR>a : G<GOAL>a ^ 0 = 1
<VAR>G : Type u_1<VAR>SubNegMonoid G<VAR>a : G<VAR>n : ℕ<GOAL>↑n • a = n • a
<VAR>G : Type u_1<VAR>DivInvMonoid G<VAR>a : G<VAR>n : ℕ<GOAL>a ^ ↑n = a ^ n
<VAR>G : Type u_1<VAR>DivInvMonoid G<VAR>a : G<VAR>n : ℕ<GOAL>a ^ OfNat.ofNat n = a ^ OfNat.ofNat n
<VAR>G : Type u_1<VAR>SubNegMonoid G<VAR>a : G<VAR>n : ℕ<GOAL>OfNat.ofNat n • a = OfNat.ofNat n • a
<VAR>G : Type u_1<VAR>DivInvMonoid G<VAR>a : G<VAR>n : ℕ<GOAL>a ^ Int.negSucc n = (a ^ (n + 1))⁻¹
<VAR>G : Type u_2<VAR>SubNegMonoid G<VAR>a : G<VAR>n : ℕ<GOAL>Int.negSucc n • a = -((n + 1) • a)
<VAR>G : Type u_1<VAR>SubNegMonoid G<VAR>a b : G<GOAL>a - b = a + -b
<VAR>G : Type u_1<VAR>DivInvMonoid G<VAR>a b : G<GOAL>a / b = a * b⁻¹
<VAR>G : Type u_1<VAR>SubNegMonoid G<VAR>a : G<GOAL>1 • a = a
<VAR>G : Type u_1<VAR>DivInvMonoid G<VAR>a : G<GOAL>a ^ 1 = a
<VAR>G : Type u_1<VAR>SubNegMonoid G<VAR>a : G<GOAL>2 • a = a + a
<VAR>G : Type u_1<VAR>DivInvMonoid G<VAR>a : G<GOAL>a ^ 2 = a * a
<VAR>G : Type u_1<VAR>DivInvMonoid G<VAR>x : G<GOAL>x ^ (-1) = x⁻¹
<VAR>G : Type u_1<VAR>SubNegMonoid G<VAR>x : G<GOAL>-1 • x = -x
<VAR>G : Type u_1<VAR>SubNegMonoid G<VAR>a : G<VAR>n : ℕ<GOAL>0 < n → -↑n • a = -(n • a)
<VAR>G : Type u_1<VAR>DivInvMonoid G<VAR>a : G<VAR>n : ℕ<GOAL>0 < n → a ^ (-↑n) = (a ^ n)⁻¹