ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_2<VAR>self : NegZeroClass G<GOAL>-0 = 0
<VAR>G : Type u_2<VAR>self : InvOneClass G<GOAL>1⁻¹ = 1
<VAR>G : Type u_1<VAR>InvOneClass G<GOAL>1⁻¹ = 1
<VAR>G : Type u_1<VAR>NegZeroClass G<GOAL>-0 = 0
<VAR>G : Type u<VAR>self : SubtractionMonoid G<VAR>a b : G<GOAL>a + b = 0 → -a = b
<VAR>G : Type u<VAR>self : SubtractionMonoid G<VAR>a b : G<GOAL>-(a + b) = -b + -a
<VAR>G : Type u<VAR>self : DivisionMonoid G<VAR>a b : G<GOAL>a * b = 1 → a⁻¹ = b
<VAR>G : Type u<VAR>self : DivisionMonoid G<VAR>a b : G<GOAL>(a * b)⁻¹ = b⁻¹ * a⁻¹
<VAR>G : Type u_1<VAR>SubtractionMonoid G<VAR>a b : G<GOAL>-(a + b) = -b + -a
<VAR>G : Type u_1<VAR>DivisionMonoid G<VAR>a b : G<GOAL>(a * b)⁻¹ = b⁻¹ * a⁻¹
<VAR>G : Type u_1<VAR>DivisionMonoid G<VAR>a b : G<GOAL>a * b = 1 → a⁻¹ = b
<VAR>G : Type u_1<VAR>SubtractionMonoid G<VAR>a b : G<GOAL>a + b = 0 → -a = b
<VAR>G : Type u_1<VAR>DivisionMonoid G<VAR>a b : G<VAR>h : a * b = 1<GOAL>b⁻¹ = a
<VAR>G : Type u_1<VAR>SubtractionMonoid G<VAR>a b : G<VAR>h : a + b = 0<GOAL>-b = a
<VAR>G : Type u_1<VAR>SubtractionMonoid G<VAR>a b : G<VAR>h : a + b = 0<GOAL>a = -b
<VAR>G : Type u_1<VAR>DivisionMonoid G<VAR>a b : G<VAR>h : a * b = 1<GOAL>a = b⁻¹
<VAR>G : Type u<VAR>self : Group G<VAR>a : G<GOAL>a⁻¹ * a = 1
<VAR>A : Type u<VAR>self : AddGroup A<VAR>a : A<GOAL>-a + a = 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a : G<GOAL>-a + a = 0
<VAR>G : Type u_1<VAR>Group G<VAR>a : G<GOAL>a⁻¹ * a = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<VAR>h : a + b = 0<GOAL>-a = b
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<VAR>h : a * b = 1<GOAL>a⁻¹ = b
<VAR>G : Type u_1<VAR>Group G<VAR>a : G<GOAL>a * a⁻¹ = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a : G<GOAL>a + -a = 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<GOAL>-a + (a + b) = b
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<GOAL>a⁻¹ * (a * b) = b
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<GOAL>a * (a⁻¹ * b) = b
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<GOAL>a + (-a + b) = b
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<GOAL>a + b + -b = a
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<GOAL>a * b * b⁻¹ = a
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<GOAL>a * b⁻¹ * b = a
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<GOAL>a + -b + b = a
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>a b : G<GOAL>-a + b + a = b
<VAR>G : Type u_1<VAR>CommGroup G<VAR>a b : G<GOAL>a⁻¹ * b * a = b
<VAR>G : Type u_1<VAR>CommGroup G<VAR>a b : G<GOAL>a * b * a⁻¹ = b
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>a b : G<GOAL>a + b + -a = b
<VAR>G : Type u_1<VAR>CommGroup G<VAR>a b : G<GOAL>a⁻¹ * (b * a) = b
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>a b : G<GOAL>-a + (b + a) = b
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>a b : G<GOAL>a + (b + -a) = b
<VAR>G : Type u_1<VAR>CommGroup G<VAR>a b : G<GOAL>a * (b * a⁻¹) = b
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Zero M<VAR>Zero N<VAR>f : ZeroHom M N<VAR>g : N → M<VAR>h₁ : Function.LeftInverse g ⇑f<GOAL>∀ (a : N), (f.inverse g h₁) a = g a
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>One M<VAR>One N<VAR>f : OneHom M N<VAR>g : N → M<VAR>h₁ : Function.LeftInverse g ⇑f<GOAL>∀ (a : N), (f.inverse g h₁) a = g a
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>g : N → M<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>∀ (a : N), (f.inverse g h₁ h₂) a = g a
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>g : N → M<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>∀ (a : N), (f.inverse g h₁ h₂) a = g a
<VAR>A : Type u_12<VAR>B : Type u_13<VAR>AddMonoid A<VAR>AddMonoid B<VAR>f : A →+ B<VAR>g : B → A<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>∀ (a : B), (f.inverse g h₁ h₂) a = g a
<VAR>A : Type u_12<VAR>B : Type u_13<VAR>Monoid A<VAR>Monoid B<VAR>f : A →* B<VAR>g : B → A<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>∀ (a : B), (f.inverse g h₁ h₂) a = g a
<VAR>F : Type u_12<VAR>A : outParam (Type u_13)<VAR>B : outParam (Type u_14)<VAR>Add A<VAR>Add B<VAR>EquivLike F A B<VAR>self : AddEquivClass F A B<VAR>f : F<VAR>a b : A<GOAL>f (a + b) = f a + f b
<VAR>F : Type u_12<VAR>A : outParam (Type u_13)<VAR>B : outParam (Type u_14)<VAR>Mul A<VAR>Mul B<VAR>EquivLike F A B<VAR>self : MulEquivClass F A B<VAR>f : F<VAR>a b : A<GOAL>f (a * b) = f a * f b
<VAR>F : Type u_1<VAR>M : Type u_12<VAR>N : Type u_13<VAR>MulOneClass M<VAR>MulOneClass N<VAR>EquivLike F M N<VAR>MulEquivClass F M N<VAR>h : F<VAR>x : M<GOAL>h x = 1 ↔ x = 1
<VAR>F : Type u_1<VAR>M : Type u_12<VAR>N : Type u_13<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>EquivLike F M N<VAR>AddEquivClass F M N<VAR>h : F<VAR>x : M<GOAL>h x = 0 ↔ x = 0
<VAR>F : Type u_1<VAR>M : Type u_12<VAR>N : Type u_13<VAR>MulOneClass M<VAR>MulOneClass N<VAR>EquivLike F M N<VAR>MulEquivClass F M N<VAR>h : F<VAR>x : M<GOAL>h x ≠ 1 ↔ x ≠ 1
<VAR>F : Type u_1<VAR>M : Type u_12<VAR>N : Type u_13<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>EquivLike F M N<VAR>AddEquivClass F M N<VAR>h : F<VAR>x : M<GOAL>h x ≠ 0 ↔ x ≠ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>EquivLike F α β<VAR>Mul α<VAR>Mul β<VAR>MulEquivClass F α β<GOAL>Function.Injective MulEquivClass.toMulEquiv
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>EquivLike F α β<VAR>Add α<VAR>Add β<VAR>AddEquivClass F α β<GOAL>Function.Injective AddEquivClass.toAddEquiv
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f : M ≃* N<GOAL>f.toEquiv = ↑f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f : M ≃+ N<GOAL>f.toEquiv = ↑f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f : M ≃* N<GOAL>f.toMulHom = ↑f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f : M ≃+ N<GOAL>f.toAddHom = ↑f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f : M ≃* N<GOAL>⇑↑f = ⇑f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f : M ≃+ N<GOAL>⇑↑f = ⇑f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f : M ≃* N<GOAL>⇑f.toMulHom = ⇑f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f : M ≃+ N<GOAL>⇑f.toAddHom = ⇑f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f : M ≃+ N<VAR>x y : M<GOAL>f (x + y) = f x + f y
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f : M ≃* N<VAR>x y : M<GOAL>f (x * y) = f x * f y
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>e : M ≃* N<GOAL>Function.Bijective ⇑e
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>e : M ≃+ N<GOAL>Function.Bijective ⇑e
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>e : M ≃+ N<GOAL>Function.Injective ⇑e
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>e : M ≃* N<GOAL>Function.Injective ⇑e
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>e : M ≃+ N<GOAL>Function.Surjective ⇑e
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>e : M ≃* N<GOAL>Function.Surjective ⇑e
<VAR>M : Type u_12<VAR>N : Type u_13<VAR>Mul M<VAR>Mul N<VAR>h : M ≃* N<VAR>x y : N<GOAL>h.symm (x * y) = h.symm x * h.symm y
<VAR>M : Type u_12<VAR>N : Type u_13<VAR>Add M<VAR>Add N<VAR>h : M ≃+ N<VAR>x y : N<GOAL>h.symm (x + y) = h.symm x + h.symm y
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f : M ≃* N<GOAL>f.invFun = ⇑f.symm
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f : M ≃+ N<GOAL>f.invFun = ⇑f.symm
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f : M ≃+ N<GOAL>⇑(↑f).symm = ⇑f.symm
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f : M ≃* N<GOAL>⇑(↑f).symm = ⇑f.symm
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f : M ≃* N<GOAL>EquivLike.inv f = ⇑f.symm
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f : M ≃+ N<GOAL>EquivLike.inv f = ⇑f.symm
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f : M ≃+ N<GOAL>↑f.symm = (↑f).symm
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f : M ≃* N<GOAL>↑f.symm = (↑f).symm
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f : M ≃ N<VAR>hf : ∀ (x y : M), f (x * y) = f x * f y<GOAL>⇑{ toEquiv := f, map_mul' := hf } = ⇑f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f : M ≃ N<VAR>hf : ∀ (x y : M), f (x + y) = f x + f y<GOAL>⇑{ toEquiv := f, map_add' := hf } = ⇑f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f : M ≃+ N<GOAL>f.symm.symm = f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f : M ≃* N<GOAL>f.symm.symm = f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<GOAL>Function.Bijective MulEquiv.symm
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<GOAL>Function.Bijective AddEquiv.symm
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f : M ≃ N<VAR>h : ∀ (x y : M), f.toFun (x * y) = f.toFun x * f.toFun y<GOAL>{ toEquiv := f, map_mul' := h }.symm = { toEquiv := f.symm, map_mul' := ⋯ }
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f : M ≃ N<VAR>h : ∀ (x y : M), f.toFun (x + y) = f.toFun x + f.toFun y<GOAL>{ toEquiv := f, map_add' := h }.symm = { toEquiv := f.symm, map_add' := ⋯ }
<VAR>M : Type u_6<VAR>Mul M<GOAL>(MulEquiv.refl M).symm = MulEquiv.refl M
<VAR>M : Type u_6<VAR>Add M<GOAL>(AddEquiv.refl M).symm = AddEquiv.refl M
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>e : M ≃+ N<VAR>y : N<GOAL>e (e.symm y) = y
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>e : M ≃* N<VAR>y : N<GOAL>e (e.symm y) = y
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>e : M ≃* N<VAR>x : M<GOAL>e.symm (e x) = x
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>e : M ≃+ N<VAR>x : M<GOAL>e.symm (e x) = x
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>e : M ≃* N<GOAL>⇑e.symm ∘ ⇑e = id
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>e : M ≃+ N<GOAL>⇑e.symm ∘ ⇑e = id
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>e : M ≃* N<GOAL>⇑e ∘ ⇑e.symm = id
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>e : M ≃+ N<GOAL>⇑e ∘ ⇑e.symm = id
<VAR>M : Type u_6<VAR>Mul M<GOAL>⇑(MulEquiv.refl M) = id
<VAR>M : Type u_6<VAR>Add M<GOAL>⇑(AddEquiv.refl M) = id
<VAR>M : Type u_6<VAR>Mul M<VAR>m : M<GOAL>(MulEquiv.refl M) m = m
<VAR>M : Type u_6<VAR>Add M<VAR>m : M<GOAL>(AddEquiv.refl M) m = m
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Mul M<VAR>Mul N<VAR>Mul P<VAR>e₁ : M ≃* N<VAR>e₂ : N ≃* P<GOAL>⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Add M<VAR>Add N<VAR>Add P<VAR>e₁ : M ≃+ N<VAR>e₂ : N ≃+ P<GOAL>⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Mul M<VAR>Mul N<VAR>Mul P<VAR>e₁ : M ≃* N<VAR>e₂ : N ≃* P<VAR>m : M<GOAL>(e₁.trans e₂) m = e₂ (e₁ m)
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Add M<VAR>Add N<VAR>Add P<VAR>e₁ : M ≃+ N<VAR>e₂ : N ≃+ P<VAR>m : M<GOAL>(e₁.trans e₂) m = e₂ (e₁ m)
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Mul M<VAR>Mul N<VAR>Mul P<VAR>e₁ : M ≃* N<VAR>e₂ : N ≃* P<VAR>p : P<GOAL>(e₁.trans e₂).symm p = e₁.symm (e₂.symm p)
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Add M<VAR>Add N<VAR>Add P<VAR>e₁ : M ≃+ N<VAR>e₂ : N ≃+ P<VAR>p : P<GOAL>(e₁.trans e₂).symm p = e₁.symm (e₂.symm p)
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>e : M ≃* N<VAR>x y : M<GOAL>e x = e y ↔ x = y
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>e : M ≃+ N<VAR>x y : M<GOAL>e x = e y ↔ x = y
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>e : M ≃* N<VAR>x : M<VAR>y : N<GOAL>e x = y ↔ x = e.symm y
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>e : M ≃+ N<VAR>x : M<VAR>y : N<GOAL>e x = y ↔ x = e.symm y
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>e : M ≃* N<VAR>x : N<VAR>y : M<GOAL>e.symm x = y ↔ x = e y
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>e : M ≃+ N<VAR>x : N<VAR>y : M<GOAL>e.symm x = y ↔ x = e y
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>e : M ≃* N<VAR>x : N<VAR>y : M<GOAL>y = e.symm x ↔ e y = x
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>e : M ≃+ N<VAR>x : N<VAR>y : M<GOAL>y = e.symm x ↔ e y = x
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>α : Type u_12<VAR>e : M ≃* N<VAR>f : N → α<VAR>g : M → α<GOAL>f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>α : Type u_12<VAR>e : M ≃+ N<VAR>f : N → α<VAR>g : M → α<GOAL>f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>α : Type u_12<VAR>e : M ≃* N<VAR>f : N → α<VAR>g : M → α<GOAL>g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>α : Type u_12<VAR>e : M ≃+ N<VAR>f : N → α<VAR>g : M → α<GOAL>g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>α : Type u_12<VAR>e : M ≃+ N<VAR>f : α → M<VAR>g : α → N<GOAL>f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>α : Type u_12<VAR>e : M ≃* N<VAR>f : α → M<VAR>g : α → N<GOAL>f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>α : Type u_12<VAR>e : M ≃* N<VAR>f : α → M<VAR>g : α → N<GOAL>⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>α : Type u_12<VAR>e : M ≃+ N<VAR>f : α → M<VAR>g : α → N<GOAL>⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>e : M ≃* N<GOAL>e.symm.trans e = MulEquiv.refl N
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>e : M ≃+ N<GOAL>e.symm.trans e = AddEquiv.refl N
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>e : M ≃* N<GOAL>e.trans e.symm = MulEquiv.refl M
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>e : M ≃+ N<GOAL>e.trans e.symm = AddEquiv.refl M
<VAR>M : Type u_6<VAR>N : Type u_7<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_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f g : M ≃+ N<VAR>h : ∀ (x : M), f x = g x<GOAL>f = g
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f g : M ≃* N<GOAL>f = g ↔ ∀ (x : M), f x = g x
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f g : M ≃+ N<GOAL>f = g ↔ ∀ (x : M), f x = g x
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>e : M ≃* N<VAR>e' : N → M<VAR>h₁ : Function.LeftInverse e' ⇑e<VAR>h₂ : Function.RightInverse e' ⇑e<VAR>h₃ : ∀ (x y : M), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y<GOAL>{ toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃ } = e
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>e : M ≃+ N<VAR>e' : N → M<VAR>h₁ : Function.LeftInverse e' ⇑e<VAR>h₂ : Function.RightInverse e' ⇑e<VAR>h₃ : ∀ (x y : M), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y<GOAL>{ toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_add' := h₃ } = e
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>e : M ≃+ N<VAR>f : N → M<VAR>h₁ : Function.LeftInverse (⇑e) f<VAR>h₂ : Function.RightInverse (⇑e) f<VAR>h₃ : ∀ (x y : N), { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y<GOAL>{ toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂, map_add' := h₃ } = e.symm
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>e : M ≃* N<VAR>f : N → M<VAR>h₁ : Function.LeftInverse (⇑e) f<VAR>h₂ : Function.RightInverse (⇑e) f<VAR>h₃ : ∀ (x y : N), { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y<GOAL>{ toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂, map_mul' := h₃ } = e.symm
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f : M ≃+ N<VAR>x x' : M<GOAL>x = x' → f x = f x'
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f : M ≃* N<VAR>x x' : M<GOAL>x = x' → f x = f x'
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f g : M ≃* N<VAR>h : f = g<VAR>x : M<GOAL>f x = g x
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f g : M ≃+ N<VAR>h : f = g<VAR>x : M<GOAL>f x = g x
<VAR>M : Type u_6<VAR>MulOneClass M<GOAL>↑(MulEquiv.refl M) = MonoidHom.id M
<VAR>M : Type u_6<VAR>AddZeroClass M<GOAL>↑(AddEquiv.refl M) = AddMonoidHom.id M
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>e₁ : M ≃* N<VAR>e₂ : N ≃* P<GOAL>↑(e₁.trans e₂) = (↑e₂).comp ↑e₁
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>e₁ : M ≃+ N<VAR>e₂ : N ≃+ P<GOAL>↑(e₁.trans e₂) = (↑e₂).comp ↑e₁
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>e : M ≃+ N<GOAL>(↑e).comp ↑e.symm = AddMonoidHom.id N
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>e : M ≃* N<GOAL>(↑e).comp ↑e.symm = MonoidHom.id N
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>e : M ≃+ N<GOAL>(↑e.symm).comp ↑e = AddMonoidHom.id M
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>e : M ≃* N<GOAL>(↑e.symm).comp ↑e = MonoidHom.id M
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>e : M ≃+ N<GOAL>Function.Injective fun f => f.comp ↑e
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>e : M ≃* N<GOAL>Function.Injective fun f => f.comp ↑e
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>e : M ≃* N<GOAL>Function.Injective fun f => (↑e).comp f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>e : M ≃+ N<GOAL>Function.Injective fun f => (↑e).comp f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>h : M ≃* N<GOAL>h 1 = 1
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>h : M ≃+ N<GOAL>h 0 = 0
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>h : M ≃* N<VAR>x : M<GOAL>h x = 1 ↔ x = 1
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>h : M ≃+ N<VAR>x : M<GOAL>h x = 0 ↔ x = 0
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>h : M ≃+ N<VAR>x : M<GOAL>h x ≠ 0 ↔ x ≠ 0
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>h : M ≃* N<VAR>x : M<GOAL>h x ≠ 1 ↔ x ≠ 1
<VAR>M : Type u_12<VAR>N : Type u_13<VAR>F : Type u_14<VAR>Mul M<VAR>Mul N<VAR>FunLike F M N<VAR>MulHomClass F M N<VAR>f : F<VAR>hf : Function.Bijective ⇑f<VAR>a : M<GOAL>(MulEquiv.ofBijective f hf) a = f a
<VAR>M : Type u_12<VAR>N : Type u_13<VAR>F : Type u_14<VAR>Add M<VAR>Add N<VAR>FunLike F M N<VAR>AddHomClass F M N<VAR>f : F<VAR>hf : Function.Bijective ⇑f<VAR>a : M<GOAL>(AddEquiv.ofBijective f hf) a = f a
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>n : N<VAR>f : M →* N<VAR>hf : Function.Bijective ⇑f<GOAL>f ((MulEquiv.ofBijective f hf).symm n) = n
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>n : N<VAR>f : M →+ N<VAR>hf : Function.Bijective ⇑f<GOAL>f ((AddEquiv.ofBijective f hf).symm n) = n
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>e : M ≃+ N<GOAL>⇑e.toAddMonoidHom = ⇑e
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>e : M ≃* N<GOAL>⇑e.toMonoidHom = ⇑e
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M ≃* N<GOAL>f.toMonoidHom = ↑f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M ≃+ N<GOAL>f.toAddMonoidHom = ↑f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>Function.Injective MulEquiv.toMonoidHom
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>Function.Injective AddEquiv.toAddMonoidHom
<VAR>M : Type u_12<VAR>N : Type u_13<VAR>P : Type u_14<VAR>Q : Type u_15<VAR>Mul P<VAR>Mul Q<VAR>f : M ≃ N<VAR>g : P ≃* Q<VAR>h : M → P<VAR>n : N<GOAL>(MulEquiv.arrowCongr f g) h n = g (h (f.symm n))
<VAR>M : Type u_12<VAR>N : Type u_13<VAR>P : Type u_14<VAR>Q : Type u_15<VAR>Add P<VAR>Add Q<VAR>f : M ≃ N<VAR>g : P ≃+ Q<VAR>h : M → P<VAR>n : N<GOAL>(AddEquiv.arrowCongr f g) h n = g (h (f.symm n))
<VAR>M : Type u_12<VAR>N : Type u_13<VAR>P : Type u_14<VAR>Q : Type u_15<VAR>MulOneClass M<VAR>MulOneClass N<VAR>CommMonoid P<VAR>CommMonoid Q<VAR>f : M ≃* N<VAR>g : P ≃* Q<VAR>h : M →* P<GOAL>(f.monoidHomCongr g) h = g.toMonoidHom.comp (h.comp f.symm.toMonoidHom)
<VAR>M : Type u_12<VAR>N : Type u_13<VAR>P : Type u_14<VAR>Q : Type u_15<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>f : M ≃+ N<VAR>g : P ≃+ Q<VAR>h : M →+ P<GOAL>(f.addMonoidHomCongr g) h = g.toAddMonoidHom.comp (h.comp f.symm.toAddMonoidHom)
<VAR>η : Type u_12<VAR>Ms : η → Type u_13<VAR>Ns : η → Type u_14<VAR>(j : η) → Mul (Ms j)<VAR>(j : η) → Mul (Ns j)<VAR>es : (j : η) → Ms j ≃* Ns j<VAR>x : (j : η) → Ms j<VAR>j : η<GOAL>(MulEquiv.piCongrRight es) x j = (es j) (x j)
<VAR>η : Type u_12<VAR>Ms : η → Type u_13<VAR>Ns : η → Type u_14<VAR>(j : η) → Add (Ms j)<VAR>(j : η) → Add (Ns j)<VAR>es : (j : η) → Ms j ≃+ Ns j<VAR>x : (j : η) → Ms j<VAR>j : η<GOAL>(AddEquiv.piCongrRight es) x j = (es j) (x j)
<VAR>η : Type u_12<VAR>Ms : η → Type u_13<VAR>(j : η) → Mul (Ms j)<GOAL>(MulEquiv.piCongrRight fun j => MulEquiv.refl (Ms j)) = MulEquiv.refl ((j : η) → Ms j)
<VAR>η : Type u_12<VAR>Ms : η → Type u_13<VAR>(j : η) → Add (Ms j)<GOAL>(AddEquiv.piCongrRight fun j => AddEquiv.refl (Ms j)) = AddEquiv.refl ((j : η) → Ms j)
<VAR>η : Type u_12<VAR>Ms : η → Type u_13<VAR>Ns : η → Type u_14<VAR>(j : η) → Mul (Ms j)<VAR>(j : η) → Mul (Ns j)<VAR>es : (j : η) → Ms j ≃* Ns j<GOAL>(MulEquiv.piCongrRight es).symm = MulEquiv.piCongrRight fun i => (es i).symm
<VAR>η : Type u_12<VAR>Ms : η → Type u_13<VAR>Ns : η → Type u_14<VAR>(j : η) → Add (Ms j)<VAR>(j : η) → Add (Ns j)<VAR>es : (j : η) → Ms j ≃+ Ns j<GOAL>(AddEquiv.piCongrRight es).symm = AddEquiv.piCongrRight fun i => (es i).symm
<VAR>η : Type u_12<VAR>Ms : η → Type u_13<VAR>Ns : η → Type u_14<VAR>Ps : η → Type u_15<VAR>(j : η) → Add (Ms j)<VAR>(j : η) → Add (Ns j)<VAR>(j : η) → Add (Ps j)<VAR>es : (j : η) → Ms j ≃+ Ns j<VAR>fs : (j : η) → Ns j ≃+ Ps j<GOAL>(AddEquiv.piCongrRight es).trans (AddEquiv.piCongrRight fs) = AddEquiv.piCongrRight fun i => (es i).trans (fs i)
<VAR>η : Type u_12<VAR>Ms : η → Type u_13<VAR>Ns : η → Type u_14<VAR>Ps : η → Type u_15<VAR>(j : η) → Mul (Ms j)<VAR>(j : η) → Mul (Ns j)<VAR>(j : η) → Mul (Ps j)<VAR>es : (j : η) → Ms j ≃* Ns j<VAR>fs : (j : η) → Ns j ≃* Ps j<GOAL>(MulEquiv.piCongrRight es).trans (MulEquiv.piCongrRight fs) = MulEquiv.piCongrRight fun i => (es i).trans (fs i)
<VAR>ι : Type u_12<VAR>M : ι → Type u_13<VAR>(j : ι) → Mul (M j)<VAR>Unique ι<VAR>x : M default<VAR>i : ι<GOAL>(MulEquiv.piUnique M).symm x i = uniqueElim x i
<VAR>ι : Type u_12<VAR>M : ι → Type u_13<VAR>(j : ι) → Add (M j)<VAR>Unique ι<VAR>x : M default<VAR>i : ι<GOAL>(AddEquiv.piUnique M).symm x i = uniqueElim x i
<VAR>ι : Type u_12<VAR>M : ι → Type u_13<VAR>(j : ι) → Add (M j)<VAR>Unique ι<VAR>f : (i : ι) → M i<GOAL>(AddEquiv.piUnique M) f = f default
<VAR>ι : Type u_12<VAR>M : ι → Type u_13<VAR>(j : ι) → Mul (M j)<VAR>Unique ι<VAR>f : (i : ι) → M i<GOAL>(MulEquiv.piUnique M) f = f default
<VAR>G : Type u_10<VAR>H : Type u_11<VAR>AddGroup G<VAR>SubtractionMonoid H<VAR>h : G ≃+ H<VAR>x : G<GOAL>h (-x) = -h x
<VAR>G : Type u_10<VAR>H : Type u_11<VAR>Group G<VAR>DivisionMonoid H<VAR>h : G ≃* H<VAR>x : G<GOAL>h x⁻¹ = (h x)⁻¹
<VAR>G : Type u_10<VAR>H : Type u_11<VAR>AddGroup G<VAR>SubtractionMonoid H<VAR>h : G ≃+ H<VAR>x y : G<GOAL>h (x - y) = h x - h y
<VAR>G : Type u_10<VAR>H : Type u_11<VAR>Group G<VAR>DivisionMonoid H<VAR>h : G ≃* H<VAR>x y : G<GOAL>h (x / y) = h x / h y