ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>Mul M<VAR>c d : Con M<GOAL>c = d ↔ ∀ (x y : M), c x y ↔ d x y
<VAR>M : Type u_1<VAR>Mul M<VAR>c d : Con M<GOAL>⇑c = ⇑d ↔ c = d
<VAR>M : Type u_1<VAR>Add M<VAR>c d : AddCon M<GOAL>⇑c = ⇑d ↔ c = d
<VAR>M : Type u_4<VAR>Add M<VAR>c : AddCon M<VAR>x : M<GOAL>Quot.mk (⇑c) x = ↑x
<VAR>M : Type u_4<VAR>Mul M<VAR>c : Con M<VAR>x : M<GOAL>Quot.mk (⇑c) x = ↑x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>cM : AddCon M<VAR>cN : AddCon N<VAR>φ : cM.Quotient → cN.Quotient → Sort u_4<VAR>a : M<VAR>b : N<VAR>f : (x : M) → (y : N) → φ ↑x ↑y<VAR>h : ∀ (x : M) (y : N) (x' : M) (y' : N), cM x x' → cN y y' → HEq (f x y) (f x' y')<GOAL>AddCon.hrecOn₂ (↑a) (↑b) f h = f a b
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>cM : Con M<VAR>cN : Con N<VAR>φ : cM.Quotient → cN.Quotient → Sort u_4<VAR>a : M<VAR>b : N<VAR>f : (x : M) → (y : N) → φ ↑x ↑y<VAR>h : ∀ (x : M) (y : N) (x' : M) (y' : N), cM x x' → cN y y' → HEq (f x y) (f x' y')<GOAL>Con.hrecOn₂ (↑a) (↑b) f h = f a b
<VAR>M : Type u_1<VAR>Mul M<VAR>c : Con M<VAR>C : c.Quotient → Prop<VAR>q : c.Quotient<VAR>H : ∀ (x : M), C ↑x<GOAL>C q
<VAR>M : Type u_1<VAR>Add M<VAR>c : AddCon M<VAR>C : c.Quotient → Prop<VAR>q : c.Quotient<VAR>H : ∀ (x : M), C ↑x<GOAL>C q
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>c : Con M<VAR>d : Con N<VAR>C : c.Quotient → d.Quotient → Prop<VAR>p : c.Quotient<VAR>q : d.Quotient<VAR>H : ∀ (x : M) (y : N), C ↑x ↑y<GOAL>C p q
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>c : AddCon M<VAR>d : AddCon N<VAR>C : c.Quotient → d.Quotient → Prop<VAR>p : c.Quotient<VAR>q : d.Quotient<VAR>H : ∀ (x : M) (y : N), C ↑x ↑y<GOAL>C p q
<VAR>M : Type u_1<VAR>Mul M<VAR>c : Con M<VAR>a b : M<GOAL>↑a = ↑b ↔ c a b
<VAR>M : Type u_1<VAR>Add M<VAR>c : AddCon M<VAR>a b : M<GOAL>↑a = ↑b ↔ c a b
<VAR>M : Type u_1<VAR>Add M<VAR>c : AddCon M<GOAL>AddCon.addKer AddCon.toQuotient ⋯ = c
<VAR>M : Type u_1<VAR>Mul M<VAR>c : Con M<GOAL>Con.mulKer Con.toQuotient ⋯ = c
<VAR>M : Type u_1<VAR>Add M<VAR>c : AddCon M<VAR>x y : M<GOAL>↑(x + y) = ↑x + ↑y
<VAR>M : Type u_1<VAR>Mul M<VAR>c : Con M<VAR>x y : M<GOAL>↑(x * y) = ↑x * ↑y
<VAR>M : Type u_1<VAR>Mul M<VAR>β : Sort u_4<VAR>c : Con M<VAR>f : M → β<VAR>h : ∀ (a b : M), c a b → f a = f b<VAR>x : M<GOAL>Con.liftOn (↑x) f h = f x
<VAR>M : Type u_1<VAR>Add M<VAR>β : Sort u_4<VAR>c : AddCon M<VAR>f : M → β<VAR>h : ∀ (a b : M), c a b → f a = f b<VAR>x : M<GOAL>AddCon.liftOn (↑x) f h = f x
<VAR>M : Type u_1<VAR>Mul M<VAR>c d : Con M<GOAL>c ≤ d ↔ ∀ {x y : M}, c x y → d x y
<VAR>M : Type u_1<VAR>Add M<VAR>c d : AddCon M<GOAL>c ≤ d ↔ ∀ {x y : M}, c x y → d x y
<VAR>M : Type u_1<VAR>Mul M<VAR>S : Set (Con M)<GOAL>(sInf S).toSetoid = sInf (Con.toSetoid '' S)
<VAR>M : Type u_1<VAR>Add M<VAR>S : Set (AddCon M)<GOAL>(sInf S).toSetoid = sInf (AddCon.toSetoid '' S)
<VAR>M : Type u_1<VAR>Mul M<VAR>S : Set (Con M)<GOAL>⇑(sInf S) = sInf (DFunLike.coe '' S)
<VAR>M : Type u_1<VAR>Add M<VAR>S : Set (AddCon M)<GOAL>⇑(sInf S) = sInf (DFunLike.coe '' S)
<VAR>M : Type u_1<VAR>Mul M<VAR>ι : Sort u_4<VAR>f : ι → Con M<GOAL>⇑(iInf f) = ⨅ i, ⇑(f i)
<VAR>M : Type u_1<VAR>Add M<VAR>ι : Sort u_4<VAR>f : ι → AddCon M<GOAL>⇑(iInf f) = ⨅ i, ⇑(f i)
<VAR>M : Type u_1<VAR>Add M<VAR>c d : AddCon M<GOAL>⇑(c ⊓ d) = ⇑c ⊓ ⇑d
<VAR>M : Type u_1<VAR>Mul M<VAR>c d : Con M<GOAL>⇑(c ⊓ d) = ⇑c ⊓ ⇑d
<VAR>M : Type u_1<VAR>Add M<VAR>c d : AddCon M<VAR>x y : M<GOAL>(c ⊓ d) x y ↔ c x y ∧ d x y
<VAR>M : Type u_1<VAR>Mul M<VAR>c d : Con M<VAR>x y : M<GOAL>(c ⊓ d) x y ↔ c x y ∧ d x y
<VAR>M : Type u_1<VAR>Add M<VAR>r : M → M → Prop<GOAL>addConGen r = sInf {s | ∀ (x y : M), r x y → s x y}
<VAR>M : Type u_1<VAR>Mul M<VAR>r : M → M → Prop<GOAL>conGen r = sInf {s | ∀ (x y : M), r x y → s x y}
<VAR>M : Type u_1<VAR>Mul M<VAR>r : M → M → Prop<VAR>c : Con M<VAR>h : ∀ (x y : M), r x y → c x y<GOAL>conGen r ≤ c
<VAR>M : Type u_1<VAR>Add M<VAR>r : M → M → Prop<VAR>c : AddCon M<VAR>h : ∀ (x y : M), r x y → c x y<GOAL>addConGen r ≤ c
<VAR>M : Type u_1<VAR>Add M<VAR>r s : M → M → Prop<VAR>h : ∀ (x y : M), r x y → s x y<GOAL>addConGen r ≤ addConGen s
<VAR>M : Type u_1<VAR>Mul M<VAR>r s : M → M → Prop<VAR>h : ∀ (x y : M), r x y → s x y<GOAL>conGen r ≤ conGen s
<VAR>M : Type u_1<VAR>Mul M<VAR>c : Con M<GOAL>conGen ⇑c = c
<VAR>M : Type u_1<VAR>Add M<VAR>c : AddCon M<GOAL>addConGen ⇑c = c
<VAR>M : Type u_1<VAR>Mul M<VAR>r : M → M → Prop<GOAL>conGen ⇑(conGen r) = conGen r
<VAR>M : Type u_1<VAR>Add M<VAR>r : M → M → Prop<GOAL>addConGen ⇑(addConGen r) = addConGen r
<VAR>M : Type u_1<VAR>Add M<VAR>c d : AddCon M<GOAL>c ⊔ d = addConGen fun x y => c x y ∨ d x y
<VAR>M : Type u_1<VAR>Mul M<VAR>c d : Con M<GOAL>c ⊔ d = conGen fun x y => c x y ∨ d x y
<VAR>M : Type u_1<VAR>Mul M<VAR>c d : Con M<GOAL>c ⊔ d = conGen (⇑c ⊔ ⇑d)
<VAR>M : Type u_1<VAR>Add M<VAR>c d : AddCon M<GOAL>c ⊔ d = addConGen (⇑c ⊔ ⇑d)
<VAR>M : Type u_1<VAR>Add M<VAR>S : Set (AddCon M)<GOAL>sSup S = addConGen fun x y => ∃ c ∈ S, c x y
<VAR>M : Type u_1<VAR>Mul M<VAR>S : Set (Con M)<GOAL>sSup S = conGen fun x y => ∃ c ∈ S, c x y
<VAR>M : Type u_1<VAR>Mul M<VAR>S : Set (Con M)<GOAL>sSup S = conGen (sSup (DFunLike.coe '' S))
<VAR>M : Type u_1<VAR>Add M<VAR>S : Set (AddCon M)<GOAL>sSup S = addConGen (sSup (DFunLike.coe '' S))
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>c : Con M<VAR>f : M → N<VAR>H : ∀ (x y : M), f (x * y) = f x * f y<VAR>h : Con.mulKer f H ≤ c<VAR>hf : Function.Surjective f<GOAL>c.mapGen f = c.mapOfSurjective f H h hf
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>c : AddCon M<VAR>f : M → N<VAR>H : ∀ (x y : M), f (x + y) = f x + f y<VAR>h : AddCon.addKer f H ≤ c<VAR>hf : Function.Surjective f<GOAL>c.mapGen f = c.mapOfSurjective f H h hf
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : M → N<VAR>H : ∀ (x y : M), f (x + y) = f x + f y<VAR>c : AddCon N<VAR>x y : M<GOAL>(AddCon.comap f H c) x y ↔ c (f x) (f y)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M → N<VAR>H : ∀ (x y : M), f (x * y) = f x * f y<VAR>c : Con N<VAR>x y : M<GOAL>(Con.comap f H c) x y ↔ c (f x) (f y)
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>c : Con M<GOAL>↑1 = 1
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>c : AddCon M<GOAL>↑0 = 0
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>c : Con M<VAR>x y : M<GOAL>(x, y) ∈ ↑c ↔ (x, y) ∈ c
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>c : AddCon M<VAR>x y : M<GOAL>(x, y) ∈ ↑c ↔ (x, y) ∈ c
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>c d : Con M<VAR>H : ↑c = ↑d<GOAL>c = d
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>c d : AddCon M<VAR>H : ↑c = ↑d<GOAL>c = d
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>c d : Con M<GOAL>c ≤ d ↔ ↑c ≤ ↑d
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>c d : AddCon M<GOAL>c ≤ d ↔ ↑c ≤ ↑d
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass P<VAR>f : M →* P<VAR>x y : M<GOAL>(Con.ker f) x y ↔ f x = f y
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass P<VAR>f : M →+ P<VAR>x y : M<GOAL>(AddCon.ker f) x y ↔ f x = f y
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>c : Con M<GOAL>Con.ker c.mk' = c
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>c : AddCon M<GOAL>AddCon.ker c.mk' = c
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>c : Con M<GOAL>Function.Surjective ⇑c.mk'
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>c : AddCon M<GOAL>Function.Surjective ⇑c.mk'
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>c : AddCon M<GOAL>⇑c.mk' = AddCon.toQuotient
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>c : Con M<GOAL>⇑c.mk' = Con.toQuotient
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>c : Con M<GOAL>MonoidHom.mrange c.mk' = ⊤
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>c : AddCon M<GOAL>AddMonoidHom.mrange c.mk' = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>c : AddCon M<VAR>f : N →+ M<GOAL>AddCon.comap ⇑f ⋯ c = AddCon.ker (c.mk'.comp f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>c : Con M<VAR>f : N →* M<GOAL>Con.comap ⇑f ⋯ c = Con.ker (c.mk'.comp f)
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass P<VAR>c : Con M<VAR>f : M →* P<VAR>H : c ≤ Con.ker f<VAR>x : M<GOAL>(c.lift f H) (c.mk' x) = f x
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass P<VAR>c : AddCon M<VAR>f : M →+ P<VAR>H : c ≤ AddCon.ker f<VAR>x : M<GOAL>(c.lift f H) (c.mk' x) = f x
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass P<VAR>c : AddCon M<VAR>f : M →+ P<VAR>H : c ≤ AddCon.ker f<VAR>x : M<GOAL>(c.lift f H) ↑x = f x
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass P<VAR>c : Con M<VAR>f : M →* P<VAR>H : c ≤ Con.ker f<VAR>x : M<GOAL>(c.lift f H) ↑x = f x
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass P<VAR>c : AddCon M<VAR>f : M →+ P<VAR>H : c ≤ AddCon.ker f<GOAL>(c.lift f H).comp c.mk' = f
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass P<VAR>c : Con M<VAR>f : M →* P<VAR>H : c ≤ Con.ker f<GOAL>(c.lift f H).comp c.mk' = f
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass P<VAR>c : AddCon M<VAR>f : c.Quotient →+ P<GOAL>c.lift (f.comp c.mk') ⋯ = f
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass P<VAR>c : Con M<VAR>f : c.Quotient →* P<GOAL>c.lift (f.comp c.mk') ⋯ = f
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass P<VAR>c : Con M<VAR>f g : c.Quotient →* P<VAR>h : ∀ (a : M), f ↑a = g ↑a<GOAL>f = g
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass P<VAR>c : AddCon M<VAR>f g : c.Quotient →+ P<VAR>h : ∀ (a : M), f ↑a = g ↑a<GOAL>f = g
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass P<VAR>c : Con M<VAR>f : M →* P<VAR>H : c ≤ Con.ker f<VAR>g : c.Quotient →* P<VAR>Hg : g.comp c.mk' = f<GOAL>g = c.lift f H
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass P<VAR>c : AddCon M<VAR>f : M →+ P<VAR>H : c ≤ AddCon.ker f<VAR>g : c.Quotient →+ P<VAR>Hg : g.comp c.mk' = f<GOAL>g = c.lift f H
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass P<VAR>c : AddCon M<VAR>f : M →+ P<VAR>H : c ≤ AddCon.ker f<GOAL>AddMonoidHom.mrange (c.lift f H) = AddMonoidHom.mrange f
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass P<VAR>c : Con M<VAR>f : M →* P<VAR>H : c ≤ Con.ker f<GOAL>MonoidHom.mrange (c.lift f H) = MonoidHom.mrange f
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass P<VAR>c : AddCon M<VAR>f : M →+ P<VAR>h : c ≤ AddCon.ker f<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑(c.lift f h)
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass P<VAR>c : Con M<VAR>f : M →* P<VAR>h : c ≤ Con.ker f<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑(c.lift f h)
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass P<VAR>c : Con M<VAR>f : M →* P<VAR>H : c ≤ Con.ker f<VAR>h : Function.Injective ⇑(c.lift f H)<GOAL>Con.ker f = c
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass P<VAR>c : AddCon M<VAR>f : M →+ P<VAR>H : c ≤ AddCon.ker f<VAR>h : Function.Injective ⇑(c.lift f H)<GOAL>AddCon.ker f = c
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass P<VAR>f : M →* P<VAR>x : M<GOAL>(Con.kerLift f) ↑x = f x
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass P<VAR>f : M →+ P<VAR>x : M<GOAL>(AddCon.kerLift f) ↑x = f x
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass P<VAR>f : M →+ P<GOAL>AddMonoidHom.mrange (AddCon.kerLift f) = AddMonoidHom.mrange f
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass P<VAR>f : M →* P<GOAL>MonoidHom.mrange (Con.kerLift f) = MonoidHom.mrange f
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass P<VAR>f : M →* P<GOAL>Function.Injective ⇑(Con.kerLift f)
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass P<VAR>f : M →+ P<GOAL>Function.Injective ⇑(AddCon.kerLift f)
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>c d : AddCon M<VAR>h : c ≤ d<VAR>x : c.Quotient<GOAL>(c.map d h) x = (c.lift d.mk' ⋯) x
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>c d : Con M<VAR>h : c ≤ d<VAR>x : c.Quotient<GOAL>(c.map d h) x = (c.lift d.mk' ⋯) x
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass P<VAR>f : M →+ P<VAR>g : P → M<VAR>hf : Function.RightInverse g ⇑f<GOAL>∀ (a : P), (AddCon.quotientKerEquivOfRightInverse f g hf).symm a = (AddCon.toQuotient ∘ g) a
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass P<VAR>f : M →* P<VAR>g : P → M<VAR>hf : Function.RightInverse g ⇑f<VAR>a : (Con.ker f).Quotient<GOAL>(Con.quotientKerEquivOfRightInverse f g hf) a = (Con.kerLift f) a
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass P<VAR>f : M →* P<VAR>g : P → M<VAR>hf : Function.RightInverse g ⇑f<GOAL>∀ (a : P), (Con.quotientKerEquivOfRightInverse f g hf).symm a = (Con.toQuotient ∘ g) a
<VAR>M : Type u_1<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass P<VAR>f : M →+ P<VAR>g : P → M<VAR>hf : Function.RightInverse g ⇑f<VAR>a : (AddCon.ker f).Quotient<GOAL>(AddCon.quotientKerEquivOfRightInverse f g hf) a = (AddCon.kerLift f) a
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>c : AddCon M<VAR>n : ℕ<VAR>w x : M<GOAL>c w x → c (n • w) (n • x)
<VAR>M : Type u_4<VAR>Monoid M<VAR>c : Con M<VAR>n : ℕ<VAR>w x : M<GOAL>c w x → c (w ^ n) (x ^ n)
<VAR>α : Type u_4<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>VAdd α M<VAR>VAddAssocClass α M M<VAR>c : AddCon M<VAR>a : α<VAR>w x : M<VAR>h : c w x<GOAL>c (a +ᵥ w) (a +ᵥ x)
<VAR>α : Type u_4<VAR>M : Type u_5<VAR>MulOneClass M<VAR>SMul α M<VAR>IsScalarTower α M M<VAR>c : Con M<VAR>a : α<VAR>w x : M<VAR>h : c w x<GOAL>c (a • w) (a • x)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>c : AddCon M<VAR>f : M → M<VAR>hf : ∀ (x : M), c (f x + x) 0<VAR>x y : M<VAR>h : c x y<GOAL>c (f x) (f y)
<VAR>M : Type u_1<VAR>Monoid M<VAR>c : Con M<VAR>f : M → M<VAR>hf : ∀ (x : M), c (f x * x) 1<VAR>x y : M<VAR>h : c x y<GOAL>c (f x) (f y)
<VAR>M : Type u_1<VAR>AddGroup M<VAR>c : AddCon M<VAR>x y : M<VAR>h : c x y<GOAL>c (-x) (-y)
<VAR>M : Type u_1<VAR>Group M<VAR>c : Con M<VAR>x y : M<VAR>h : c x y<GOAL>c x⁻¹ y⁻¹
<VAR>M : Type u_1<VAR>Group M<VAR>c : Con M<VAR>w x y z : M<GOAL>c w x → c y z → c (w / y) (x / z)
<VAR>M : Type u_1<VAR>AddGroup M<VAR>c : AddCon M<VAR>w x y z : M<GOAL>c w x → c y z → c (w - y) (x - z)
<VAR>M : Type u_1<VAR>Group M<VAR>c : Con M<VAR>n : ℤ<VAR>w x : M<GOAL>c w x → c (w ^ n) (x ^ n)
<VAR>M : Type u_1<VAR>AddGroup M<VAR>c : AddCon M<VAR>n : ℤ<VAR>w x : M<GOAL>c w x → c (n • w) (n • x)
<VAR>M : Type u_1<VAR>α : Type u_4<VAR>Monoid M<VAR>c : Con M<VAR>f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α<VAR>Hf : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1), c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'<VAR>x y : M<VAR>hxy : ↑x * ↑y = 1<VAR>hyx : ↑y * ↑x = 1<GOAL>Con.liftOnUnits { val := ↑x, inv := ↑y, val_inv := hxy, inv_val := hyx } f Hf = f x y ⋯ ⋯
<VAR>M : Type u_1<VAR>α : Type u_4<VAR>AddMonoid M<VAR>c : AddCon M<VAR>f : (x y : M) → c (x + y) 0 → c (y + x) 0 → α<VAR>Hf : ∀ (x y : M) (hxy : c (x + y) 0) (hyx : c (y + x) 0) (x' y' : M) (hxy' : c (x' + y') 0) (hyx' : c (y' + x') 0), c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'<VAR>x y : M<VAR>hxy : ↑x + ↑y = 0<VAR>hyx : ↑y + ↑x = 0<GOAL>AddCon.liftOnAddUnits { val := ↑x, neg := ↑y, val_neg := hxy, neg_val := hyx } f Hf = f x y ⋯ ⋯
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>c : AddCon M<VAR>p : AddUnits c.Quotient → Prop<VAR>u : AddUnits c.Quotient<VAR>H : ∀ (x y : M) (hxy : c (x + y) 0) (hyx : c (y + x) 0), p { val := ↑x, neg := ↑y, val_neg := ⋯, neg_val := ⋯ }<GOAL>p u
<VAR>M : Type u_1<VAR>Monoid M<VAR>c : Con M<VAR>p : c.Quotientˣ → Prop<VAR>u : c.Quotientˣ<VAR>H : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1), p { val := ↑x, inv := ↑y, val_inv := ⋯, inv_val := ⋯ }<GOAL>p u
<VAR>α : Type u_4<VAR>M : Type u_5<VAR>MulOneClass M<VAR>SMul α M<VAR>IsScalarTower α M M<VAR>c : Con M<VAR>a : α<VAR>x : M<GOAL>↑(a • x) = a • ↑x
<VAR>α : Type u_4<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>VAdd α M<VAR>VAddAssocClass α M M<VAR>c : AddCon M<VAR>a : α<VAR>x : M<GOAL>↑(a +ᵥ x) = a +ᵥ ↑x
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>N : Type u_3<VAR>β : Type u_4<VAR>SMul M α<VAR>SMul N α<VAR>SMulCommClass M N α<VAR>SMul N β<VAR>c : Mᵈᵐᵃ<VAR>f : α →ₑ[id] β<VAR>a : α<GOAL>(c • f) a = f (DomMulAct.mk.symm c • a)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>N : Type u_3<VAR>β : Type u_4<VAR>SMul M α<VAR>SMul N α<VAR>SMulCommClass M N α<VAR>SMul N β<VAR>c : M<VAR>f : α →ₑ[id] β<VAR>a : α<GOAL>(DomMulAct.mk c • f) a = f (c • a)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>AddMonoid A<VAR>DistribSMul M A<VAR>Monoid N<VAR>AddMonoid B<VAR>DistribMulAction N A<VAR>SMulCommClass M N A<VAR>DistribMulAction N B<VAR>c : Mᵈᵐᵃ<VAR>f : A →+[N] B<VAR>a : A<GOAL>(c • f) a = f (DomMulAct.mk.symm c • a)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>AddMonoid A<VAR>DistribSMul M A<VAR>Monoid N<VAR>AddMonoid B<VAR>DistribMulAction N A<VAR>SMulCommClass M N A<VAR>DistribMulAction N B<VAR>c : M<VAR>f : A →+[N] B<VAR>a : A<GOAL>(DomMulAct.mk c • f) a = f (c • a)
<VAR>M : Type u_1<VAR>Zero M<GOAL>DomAddAct.mk 0 = 0
<VAR>M : Type u_1<VAR>One M<GOAL>DomMulAct.mk 1 = 1
<VAR>M : Type u_1<VAR>Zero M<GOAL>DomAddAct.mk.symm 0 = 0
<VAR>M : Type u_1<VAR>One M<GOAL>DomMulAct.mk.symm 1 = 1
<VAR>M : Type u_1<VAR>Add M<VAR>a b : M<GOAL>DomAddAct.mk (a + b) = DomAddAct.mk b + DomAddAct.mk a
<VAR>M : Type u_1<VAR>Mul M<VAR>a b : M<GOAL>DomMulAct.mk (a * b) = DomMulAct.mk b * DomMulAct.mk a
<VAR>M : Type u_1<VAR>Add M<VAR>a b : Mᵈᵃᵃ<GOAL>DomAddAct.mk.symm (a + b) = DomAddAct.mk.symm b + DomAddAct.mk.symm a
<VAR>M : Type u_1<VAR>Mul M<VAR>a b : Mᵈᵐᵃ<GOAL>DomMulAct.mk.symm (a * b) = DomMulAct.mk.symm b * DomMulAct.mk.symm a
<VAR>M : Type u_1<VAR>Neg M<VAR>a : M<GOAL>DomAddAct.mk (-a) = -DomAddAct.mk a
<VAR>M : Type u_1<VAR>Inv M<VAR>a : M<GOAL>DomMulAct.mk a⁻¹ = (DomMulAct.mk a)⁻¹
<VAR>M : Type u_1<VAR>Inv M<VAR>a : Mᵈᵐᵃ<GOAL>DomMulAct.mk.symm a⁻¹ = (DomMulAct.mk.symm a)⁻¹
<VAR>M : Type u_1<VAR>Neg M<VAR>a : Mᵈᵃᵃ<GOAL>DomAddAct.mk.symm (-a) = -DomAddAct.mk.symm a
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>n : ℕ<GOAL>DomMulAct.mk (a ^ n) = DomMulAct.mk a ^ n
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>n : ℕ<GOAL>DomAddAct.mk (n • a) = n • DomAddAct.mk a
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : Mᵈᵐᵃ<VAR>n : ℕ<GOAL>DomMulAct.mk.symm (a ^ n) = DomMulAct.mk.symm a ^ n
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : Mᵈᵃᵃ<VAR>n : ℕ<GOAL>DomAddAct.mk.symm (n • a) = n • DomAddAct.mk.symm a
<VAR>M : Type u_1<VAR>DivInvMonoid M<VAR>a : M<VAR>n : ℤ<GOAL>DomMulAct.mk (a ^ n) = DomMulAct.mk a ^ n
<VAR>M : Type u_1<VAR>SubNegMonoid M<VAR>a : M<VAR>n : ℤ<GOAL>DomAddAct.mk (n • a) = n • DomAddAct.mk a
<VAR>M : Type u_1<VAR>DivInvMonoid M<VAR>a : Mᵈᵐᵃ<VAR>n : ℤ<GOAL>DomMulAct.mk.symm (a ^ n) = DomMulAct.mk.symm a ^ n
<VAR>M : Type u_1<VAR>SubNegMonoid M<VAR>a : Mᵈᵃᵃ<VAR>n : ℤ<GOAL>DomAddAct.mk.symm (n • a) = n • DomAddAct.mk.symm a
<VAR>M : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<VAR>VAdd M α<VAR>c : Mᵈᵃᵃ<VAR>f : α → β<VAR>a : α<GOAL>(c +ᵥ f) a = f (DomAddAct.mk.symm c +ᵥ a)
<VAR>M : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<VAR>SMul M α<VAR>c : Mᵈᵐᵃ<VAR>f : α → β<VAR>a : α<GOAL>(c • f) a = f (DomMulAct.mk.symm c • a)
<VAR>M : Type u_5<VAR>A : Type u_7<VAR>B : Type u_8<VAR>Monoid M<VAR>Monoid A<VAR>MulDistribMulAction M A<VAR>MulOneClass B<VAR>c : Mᵈᵐᵃ<VAR>f : A →* B<VAR>a : A<GOAL>(c • f) a = f (DomMulAct.mk.symm c • a)
<VAR>M : Type u_5<VAR>A : Type u_7<VAR>B : Type u_8<VAR>Monoid M<VAR>Monoid A<VAR>MulDistribMulAction M A<VAR>MulOneClass B<VAR>c : M<VAR>f : A →* B<VAR>a : A<GOAL>(DomMulAct.mk c • f) a = f (c • a)
<VAR>A : Type u_5<VAR>B : Type u_6<VAR>M : Type u_7<VAR>AddMonoid A<VAR>DistribSMul M A<VAR>AddZeroClass B<VAR>c : Mᵈᵐᵃ<VAR>f : A →+ B<VAR>a : A<GOAL>(c • f) a = f (DomMulAct.mk.symm c • a)
<VAR>A : Type u_5<VAR>B : Type u_6<VAR>M : Type u_7<VAR>AddMonoid A<VAR>DistribSMul M A<VAR>AddZeroClass B<VAR>c : M<VAR>f : A →+ B<VAR>a : A<GOAL>(DomMulAct.mk c • f) a = f (c • a)
<VAR>A : Type u_5<VAR>B : Type u_6<VAR>M : Type u_7<VAR>AddMonoid A<VAR>DistribSMul M A<VAR>AddZeroClass B<VAR>c : Mᵈᵐᵃ<VAR>f : A →+ B<GOAL>⇑(c • f) = c • ⇑f
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : ℕ<VAR>x : α<GOAL>{ val := n } +ᵥ x = f^[n] x
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : ℕ<VAR>x : α<GOAL>{ val := n } • x = f^[n] x
<VAR>α : Type u<VAR>β : Type v<VAR>GroupWithZero α<VAR>MulAction α β<VAR>c : α<VAR>hc : c ≠ 0<VAR>x : β<GOAL>c⁻¹ • c • x = x
<VAR>α : Type u<VAR>β : Type v<VAR>GroupWithZero α<VAR>MulAction α β<VAR>c : α<VAR>hc : c ≠ 0<VAR>x : β<GOAL>c • c⁻¹ • x = x
<VAR>α : Type u<VAR>β : Type v<VAR>GroupWithZero α<VAR>MulAction α β<VAR>a : α<VAR>ha : a ≠ 0<VAR>x y : β<GOAL>a⁻¹ • x = y ↔ x = a • y
<VAR>α : Type u<VAR>β : Type v<VAR>GroupWithZero α<VAR>MulAction α β<VAR>a : α<VAR>ha : a ≠ 0<VAR>x y : β<GOAL>x = a⁻¹ • y ↔ a • x = y
<VAR>α : Type u<VAR>β : Type v<VAR>GroupWithZero α<VAR>MulAction α β<VAR>Mul β<VAR>SMulCommClass α β β<VAR>IsScalarTower α β β<VAR>a b : β<VAR>c : α<VAR>hc : c ≠ 0<GOAL>Commute a (c • b) ↔ Commute a b
<VAR>α : Type u<VAR>β : Type v<VAR>GroupWithZero α<VAR>MulAction α β<VAR>Mul β<VAR>SMulCommClass α β β<VAR>IsScalarTower α β β<VAR>a b : β<VAR>c : α<VAR>hc : c ≠ 0<GOAL>Commute (c • a) b ↔ Commute a b
<VAR>α : Type u<VAR>β : Type v<VAR>GroupWithZero α<VAR>MulAction α β<VAR>a : α<VAR>ha : a ≠ 0<VAR>b : β<GOAL>(Equiv.smulRight ha) b = a • b
<VAR>α : Type u<VAR>β : Type v<VAR>GroupWithZero α<VAR>MulAction α β<VAR>a : α<VAR>ha : a ≠ 0<VAR>b : β<GOAL>(Equiv.smulRight ha).symm b = a⁻¹ • b
<VAR>α : Type u<VAR>β : Type v<VAR>GroupWithZero α<VAR>MulAction α β<VAR>a : α<VAR>ha : a ≠ 0<GOAL>Function.Bijective fun x => a • x
<VAR>α : Type u<VAR>β : Type v<VAR>GroupWithZero α<VAR>MulAction α β<VAR>a : α<VAR>ha : a ≠ 0<GOAL>Function.Injective fun x => a • x
<VAR>α : Type u<VAR>β : Type v<VAR>GroupWithZero α<VAR>MulAction α β<VAR>a : α<VAR>ha : a ≠ 0<GOAL>Function.Surjective fun x => a • x
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>AddMonoid β<VAR>DistribMulAction α β<VAR>x : α<GOAL>∀ (a : β), (DistribMulAction.toAddEquiv β x).symm a = x⁻¹ • a
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>AddMonoid β<VAR>DistribMulAction α β<VAR>x : α<GOAL>∀ (a : β), (DistribMulAction.toAddEquiv β x) a = x • a
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>AddMonoid β<VAR>DistribMulAction α β<VAR>x : α<GOAL>(DistribMulAction.toAddAut α β) x = DistribMulAction.toAddEquiv β x
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>AddMonoid β<VAR>DistribMulAction α β<VAR>a : α<VAR>x : β<GOAL>a • x = 0 ↔ x = 0
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>AddMonoid β<VAR>DistribMulAction α β<VAR>a : α<VAR>x : β<GOAL>a • x ≠ 0 ↔ x ≠ 0
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>Monoid β<VAR>MulDistribMulAction α β<VAR>x : α<GOAL>∀ (a : β), (MulDistribMulAction.toMulEquiv β x) a = x • a
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>Monoid β<VAR>MulDistribMulAction α β<VAR>x : α<GOAL>∀ (a : β), (MulDistribMulAction.toMulEquiv β x).symm a = x⁻¹ • a
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>Monoid β<VAR>MulDistribMulAction α β<VAR>x : α<GOAL>(MulDistribMulAction.toMulAut α β) x = MulDistribMulAction.toMulEquiv β x
<VAR>G : Type u_1<VAR>A : Type u_2<VAR>H : Type u_3<VAR>Group G<VAR>MulAction G A<VAR>Monoid H<VAR>x : G<GOAL>∀ (a : A → H) (a_1 : A), (MulEquiv.symm (mulAutArrow x)) a a_1 = (x⁻¹ • a) a_1
<VAR>G : Type u_1<VAR>A : Type u_2<VAR>H : Type u_3<VAR>Group G<VAR>MulAction G A<VAR>Monoid H<VAR>x : G<GOAL>∀ (a : A → H) (a_1 : A), (mulAutArrow x) a a_1 = (x • a) a_1
<VAR>α : Type u<VAR>β : Type v<VAR>Monoid α<VAR>AddMonoid β<VAR>DistribMulAction α β<VAR>u : α<VAR>hu : IsUnit u<VAR>x : β<GOAL>u • x = 0 ↔ x = 0
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>Monoid β<VAR>AddGroup β<VAR>DistribMulAction α β<VAR>IsScalarTower α β β<VAR>SMulCommClass α β β<VAR>r : α<VAR>a : β<GOAL>IsUnit (r • 1 - a) ↔ IsUnit (1 - r⁻¹ • a)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Monoid M<VAR>MulAction M α<VAR>s : Set α<VAR>m : M<GOAL>m ∈ fixingSubmonoid M s ↔ ∀ y ∈ s, m • y = y
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Monoid M<VAR>MulAction M α<GOAL>GaloisConnection (⇑OrderDual.toDual ∘ fixingSubmonoid M) ((fun P => MulAction.fixedPoints (↥P) α) ∘ ⇑OrderDual.ofDual)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Monoid M<VAR>MulAction M α<GOAL>Antitone fun s => fixingSubmonoid M s