ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>One M<VAR>One N<VAR>g : M → N<VAR>hg : g 1 = 1<VAR>f : α → M<GOAL>Function.mulSupport (g ∘ f) ⊆ Function.mulSupport f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>Zero N<VAR>g : M → N<VAR>hg : g 0 = 0<VAR>f : α → M<GOAL>Function.support (g ∘ f) ⊆ Function.support f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>Zero N<VAR>g : M → N<VAR>hg : ∀ {x : M}, g x = 0 → x = 0<VAR>f : α → M<GOAL>Function.support f ⊆ Function.support (g ∘ f)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>One M<VAR>One N<VAR>g : M → N<VAR>hg : ∀ {x : M}, g x = 1 → x = 1<VAR>f : α → M<GOAL>Function.mulSupport f ⊆ Function.mulSupport (g ∘ f)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>One M<VAR>One N<VAR>g : M → N<VAR>hg : ∀ {x : M}, g x = 1 ↔ x = 1<VAR>f : α → M<GOAL>Function.mulSupport (g ∘ f) = Function.mulSupport f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>Zero N<VAR>g : M → N<VAR>hg : ∀ {x : M}, g x = 0 ↔ x = 0<VAR>f : α → M<GOAL>Function.support (g ∘ f) = Function.support f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>One M<VAR>One N<VAR>g : M → N<VAR>f : α → M<VAR>hg : ∀ {x : M}, x ∈ Set.range f → (g x = 1 ↔ x = 1)<GOAL>Function.mulSupport (g ∘ f) = Function.mulSupport f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>Zero N<VAR>g : M → N<VAR>f : α → M<VAR>hg : ∀ {x : M}, x ∈ Set.range f → (g x = 0 ↔ x = 0)<GOAL>Function.support (g ∘ f) = Function.support f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>One M<VAR>g : β → M<VAR>f : α → β<GOAL>Function.mulSupport (g ∘ f) = f ⁻¹' Function.mulSupport g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>g : β → M<VAR>f : α → β<GOAL>Function.support (g ∘ f) = f ⁻¹' Function.support g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>Zero N<VAR>f : α → M<VAR>g : α → N<GOAL>(Function.support fun x => (f x, g x)) = Function.support f ∪ Function.support g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>One M<VAR>One N<VAR>f : α → M<VAR>g : α → N<GOAL>(Function.mulSupport fun x => (f x, g x)) = Function.mulSupport f ∪ Function.mulSupport g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>Zero N<VAR>f : α → M × N<GOAL>Function.support f = (Function.support fun x => (f x).1) ∪ Function.support fun x => (f x).2
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>One M<VAR>One N<VAR>f : α → M × N<GOAL>Function.mulSupport f = (Function.mulSupport fun x => (f x).1) ∪ Function.mulSupport fun x => (f x).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>One M<VAR>f : α × β → M<VAR>a : α<GOAL>(Function.mulSupport fun b => f (a, b)) ⊆ Prod.snd '' Function.mulSupport f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α × β → M<VAR>a : α<GOAL>(Function.support fun b => f (a, b)) ⊆ Prod.snd '' Function.support f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>One M<VAR>f : α × β → M<GOAL>Function.mulSupport (Function.curry f) = Prod.fst '' Function.mulSupport f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α × β → M<GOAL>Function.support (Function.curry f) = Prod.fst '' Function.support f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>One M<VAR>f : α × β → M<GOAL>(Function.mulSupport fun a b => f (a, b)) = Prod.fst '' Function.mulSupport f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α × β → M<GOAL>(Function.support fun a b => f (a, b)) = Prod.fst '' Function.support f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>f g : α → M<GOAL>(Function.support fun x => f x + g x) ⊆ Function.support f ∪ Function.support g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>MulOneClass M<VAR>f g : α → M<GOAL>(Function.mulSupport fun x => f x * g x) ⊆ Function.mulSupport f ∪ Function.mulSupport g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddMonoid M<VAR>f : α → M<VAR>n : ℕ<GOAL>(Function.support fun x => n • f x) ⊆ Function.support f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Monoid M<VAR>f : α → M<VAR>n : ℕ<GOAL>(Function.mulSupport fun x => f x ^ n) ⊆ Function.mulSupport f
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>SubtractionMonoid G<VAR>f : α → G<GOAL>(Function.support fun x => -f x) = Function.support f
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>DivisionMonoid G<VAR>f : α → G<GOAL>(Function.mulSupport fun x => (f x)⁻¹) = Function.mulSupport f
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>DivisionMonoid G<VAR>f : α → G<GOAL>Function.mulSupport f⁻¹ = Function.mulSupport f
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>SubtractionMonoid G<VAR>f : α → G<GOAL>Function.support (-f) = Function.support f
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>DivisionMonoid G<VAR>f g : α → G<GOAL>(Function.mulSupport fun x => f x * (g x)⁻¹) ⊆ Function.mulSupport f ∪ Function.mulSupport g
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>SubtractionMonoid G<VAR>f g : α → G<GOAL>(Function.support fun x => f x + -g x) ⊆ Function.support f ∪ Function.support g
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>DivisionMonoid G<VAR>f g : α → G<GOAL>(Function.mulSupport fun x => f x / g x) ⊆ Function.mulSupport f ∪ Function.mulSupport g
<VAR>α : Type u_1<VAR>G : Type u_9<VAR>SubtractionMonoid G<VAR>f g : α → G<GOAL>(Function.support fun x => f x - g x) ⊆ Function.support f ∪ Function.support g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>Zero M<VAR>f : α → M<VAR>s : Set β<VAR>g : β → α<GOAL>g '' s ∩ Function.support f = g '' (s ∩ Function.support (f ∘ g))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>One M<VAR>f : α → M<VAR>s : Set β<VAR>g : β → α<GOAL>g '' s ∩ Function.mulSupport f = g '' (s ∩ Function.mulSupport (f ∘ g))
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>DecidableEq A<VAR>Zero B<VAR>a : A<VAR>b : B<GOAL>Function.support (Pi.single a b) ⊆ {a}
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>DecidableEq A<VAR>One B<VAR>a : A<VAR>b : B<GOAL>Function.mulSupport (Pi.mulSingle a b) ⊆ {a}
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>DecidableEq A<VAR>One B<VAR>a : A<GOAL>Function.mulSupport (Pi.mulSingle a 1) = ∅
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>DecidableEq A<VAR>Zero B<VAR>a : A<GOAL>Function.support (Pi.single a 0) = ∅
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>DecidableEq A<VAR>One B<VAR>a : A<VAR>b : B<VAR>h : b ≠ 1<GOAL>Function.mulSupport (Pi.mulSingle a b) = {a}
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>DecidableEq A<VAR>Zero B<VAR>a : A<VAR>b : B<VAR>h : b ≠ 0<GOAL>Function.support (Pi.single a b) = {a}
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>DecidableEq A<VAR>One B<VAR>a : A<VAR>b : B<VAR>DecidableEq B<GOAL>Function.mulSupport (Pi.mulSingle a b) = if b = 1 then ∅ else {a}
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>DecidableEq A<VAR>Zero B<VAR>a : A<VAR>b : B<VAR>DecidableEq B<GOAL>Function.support (Pi.single a b) = if b = 0 then ∅ else {a}
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>DecidableEq A<VAR>Zero B<VAR>b b' : B<VAR>hb : b ≠ 0<VAR>hb' : b' ≠ 0<VAR>i j : A<GOAL>Disjoint (Function.support (Pi.single i b)) (Function.support (Pi.single j b')) ↔ i ≠ j
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>DecidableEq A<VAR>One B<VAR>b b' : B<VAR>hb : b ≠ 1<VAR>hb' : b' ≠ 1<VAR>i j : A<GOAL>Disjoint (Function.mulSupport (Pi.mulSingle i b)) (Function.mulSupport (Pi.mulSingle j b')) ↔ i ≠ j
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C₁<VAR>CategoryTheory.Category.{u_5, u_2} C₂<VAR>CategoryTheory.Category.{u_6, u_3} D<VAR>CategoryTheory.Preadditive C₁<VAR>CategoryTheory.Limits.HasZeroMorphisms C₂<VAR>CategoryTheory.Preadditive D<VAR>K₁ : CochainComplex C₁ ℤ<VAR>K₂ : CochainComplex C₂ ℤ<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>F.Additive<VAR>∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>x i : ℤ<GOAL>∀ (x_1 : ℤ), ((K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).hom.f i).f x_1 = 𝟙 ((F.obj (K₁.X (i + x))).obj (K₂.X x_1))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C₁<VAR>CategoryTheory.Category.{u_5, u_2} C₂<VAR>CategoryTheory.Category.{u_6, u_3} D<VAR>CategoryTheory.Preadditive C₁<VAR>CategoryTheory.Limits.HasZeroMorphisms C₂<VAR>CategoryTheory.Preadditive D<VAR>K₁ : CochainComplex C₁ ℤ<VAR>K₂ : CochainComplex C₂ ℤ<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>F.Additive<VAR>∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>x i : ℤ<GOAL>∀ (x_1 : ℤ), ((K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).inv.f i).f x_1 = 𝟙 ((F.obj (K₁.X (i + x))).obj (K₂.X x_1))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C₁<VAR>CategoryTheory.Category.{u_5, u_2} C₂<VAR>CategoryTheory.Category.{u_6, u_3} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C₁<VAR>CategoryTheory.Preadditive C₂<VAR>CategoryTheory.Preadditive D<VAR>K₁ : CochainComplex C₁ ℤ<VAR>K₂ : CochainComplex C₂ ℤ<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>∀ (X₁ : C₁), (F.obj X₁).Additive<VAR>y i : ℤ<GOAL>∀ (i_1 : ℤ), ((K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).inv.f i).f i_1 = 𝟙 ((F.obj (K₁.X i)).obj (K₂.X (i_1 + y)))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C₁<VAR>CategoryTheory.Category.{u_5, u_2} C₂<VAR>CategoryTheory.Category.{u_6, u_3} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C₁<VAR>CategoryTheory.Preadditive C₂<VAR>CategoryTheory.Preadditive D<VAR>K₁ : CochainComplex C₁ ℤ<VAR>K₂ : CochainComplex C₂ ℤ<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>∀ (X₁ : C₁), (F.obj X₁).Additive<VAR>y i : ℤ<GOAL>∀ (i_1 : ℤ), ((K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom.f i).f i_1 = 𝟙 ((F.obj (K₁.X i)).obj (K₂.X (i_1 + y)))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>CategoryTheory.Category.{u_4, u_3} D<VAR>CategoryTheory.Preadditive C₁<VAR>CategoryTheory.Preadditive C₂<VAR>CategoryTheory.Preadditive D<VAR>K₁ : CochainComplex C₁ ℤ<VAR>K₂ : CochainComplex C₂ ℤ<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>F.Additive<VAR>∀ (X₁ : C₁), (F.obj X₁).Additive<VAR>x y : ℤ<VAR>K₁.HasMapBifunctor K₂ F<GOAL>K₁.mapBifunctorShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F x ≪≫ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).mapIso (K₁.mapBifunctorShift₂Iso K₂ F y) = (x * y).negOnePow • ((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorShift₂Iso K₂ F y ≪≫ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).mapIso (K₁.mapBifunctorShift₁Iso K₂ F x) ≪≫ (CategoryTheory.shiftFunctorComm (CochainComplex D ℤ) x y).app (K₁.mapBifunctor K₂ F)
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>x : AddSubmonoid M<GOAL>↑x.op = AddOpposite.unop ⁻¹' ↑x
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>x : Submonoid M<GOAL>↑x.op = MulOpposite.unop ⁻¹' ↑x
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>x : Mᵃᵒᵖ<VAR>S : AddSubmonoid M<GOAL>x ∈ S.op ↔ AddOpposite.unop x ∈ S
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>x : Mᵐᵒᵖ<VAR>S : Submonoid M<GOAL>x ∈ S.op ↔ MulOpposite.unop x ∈ S
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>x : Submonoid Mᵐᵒᵖ<GOAL>↑x.unop = MulOpposite.op ⁻¹' ↑x
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>x : AddSubmonoid Mᵃᵒᵖ<GOAL>↑x.unop = AddOpposite.op ⁻¹' ↑x
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>x : M<VAR>S : Submonoid Mᵐᵒᵖ<GOAL>x ∈ S.unop ↔ MulOpposite.op x ∈ S
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>x : M<VAR>S : AddSubmonoid Mᵃᵒᵖ<GOAL>x ∈ S.unop ↔ AddOpposite.op x ∈ S
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<GOAL>S.op.unop = S
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S : Submonoid M<GOAL>S.op.unop = S
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S : Submonoid Mᵐᵒᵖ<GOAL>S.unop.op = S
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S : AddSubmonoid Mᵃᵒᵖ<GOAL>S.unop.op = S
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S₁ : Submonoid M<VAR>S₂ : Submonoid Mᵐᵒᵖ<GOAL>S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S₁ : AddSubmonoid M<VAR>S₂ : AddSubmonoid Mᵃᵒᵖ<GOAL>S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S₁ : Submonoid Mᵐᵒᵖ<VAR>S₂ : Submonoid M<GOAL>S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S₁ : AddSubmonoid Mᵃᵒᵖ<VAR>S₂ : AddSubmonoid M<GOAL>S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S₁ S₂ : Submonoid M<GOAL>S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S₁ S₂ : AddSubmonoid M<GOAL>S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S₁ S₂ : Submonoid Mᵐᵒᵖ<GOAL>S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S₁ S₂ : AddSubmonoid Mᵃᵒᵖ<GOAL>S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>x : AddSubmonoid Mᵃᵒᵖ<GOAL>(RelIso.symm AddSubmonoid.opEquiv) x = x.unop
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>x : AddSubmonoid M<GOAL>AddSubmonoid.opEquiv x = x.op
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>x : Submonoid M<GOAL>Submonoid.opEquiv x = x.op
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>x : Submonoid Mᵐᵒᵖ<GOAL>(RelIso.symm Submonoid.opEquiv) x = x.unop
<VAR>M : Type u_2<VAR>AddZeroClass M<GOAL>⊥.op = ⊥
<VAR>M : Type u_2<VAR>MulOneClass M<GOAL>⊥.op = ⊥
<VAR>M : Type u_2<VAR>MulOneClass M<GOAL>⊥.unop = ⊥
<VAR>M : Type u_2<VAR>AddZeroClass M<GOAL>⊥.unop = ⊥
<VAR>M : Type u_2<VAR>AddZeroClass M<GOAL>⊤.op = ⊤
<VAR>M : Type u_2<VAR>MulOneClass M<GOAL>⊤.op = ⊤
<VAR>M : Type u_2<VAR>MulOneClass M<GOAL>⊤.unop = ⊤
<VAR>M : Type u_2<VAR>AddZeroClass M<GOAL>⊤.unop = ⊤
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S₁ S₂ : Submonoid M<GOAL>(S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S₁ S₂ : AddSubmonoid M<GOAL>(S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S₁ S₂ : AddSubmonoid Mᵃᵒᵖ<GOAL>(S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S₁ S₂ : Submonoid Mᵐᵒᵖ<GOAL>(S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S₁ S₂ : AddSubmonoid M<GOAL>(S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S₁ S₂ : Submonoid M<GOAL>(S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S₁ S₂ : Submonoid Mᵐᵒᵖ<GOAL>(S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S₁ S₂ : AddSubmonoid Mᵃᵒᵖ<GOAL>(S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S : Set (AddSubmonoid M)<GOAL>(sSup S).op = sSup (AddSubmonoid.unop ⁻¹' S)
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S : Set (Submonoid M)<GOAL>(sSup S).op = sSup (Submonoid.unop ⁻¹' S)
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S : Set (AddSubmonoid Mᵃᵒᵖ)<GOAL>(sSup S).unop = sSup (AddSubmonoid.op ⁻¹' S)
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S : Set (Submonoid Mᵐᵒᵖ)<GOAL>(sSup S).unop = sSup (Submonoid.op ⁻¹' S)
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S : Set (Submonoid M)<GOAL>(sInf S).op = sInf (Submonoid.unop ⁻¹' S)
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S : Set (AddSubmonoid M)<GOAL>(sInf S).op = sInf (AddSubmonoid.unop ⁻¹' S)
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S : Set (AddSubmonoid Mᵃᵒᵖ)<GOAL>(sInf S).unop = sInf (AddSubmonoid.op ⁻¹' S)
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S : Set (Submonoid Mᵐᵒᵖ)<GOAL>(sInf S).unop = sInf (Submonoid.op ⁻¹' S)
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S : ι → AddSubmonoid M<GOAL>(iSup S).op = ⨆ i, (S i).op
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S : ι → Submonoid M<GOAL>(iSup S).op = ⨆ i, (S i).op
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S : ι → AddSubmonoid Mᵃᵒᵖ<GOAL>(iSup S).unop = ⨆ i, (S i).unop
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S : ι → Submonoid Mᵐᵒᵖ<GOAL>(iSup S).unop = ⨆ i, (S i).unop
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S : ι → Submonoid M<GOAL>(iInf S).op = ⨅ i, (S i).op
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S : ι → AddSubmonoid M<GOAL>(iInf S).op = ⨅ i, (S i).op
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>MulOneClass M<VAR>S : ι → Submonoid Mᵐᵒᵖ<GOAL>(iInf S).unop = ⨅ i, (S i).unop
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>S : ι → AddSubmonoid Mᵃᵒᵖ<GOAL>(iInf S).unop = ⨅ i, (S i).unop
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>s : Set M<GOAL>(Submonoid.closure s).op = Submonoid.closure (MulOpposite.unop ⁻¹' s)
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>s : Set M<GOAL>(AddSubmonoid.closure s).op = AddSubmonoid.closure (AddOpposite.unop ⁻¹' s)
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>s : Set Mᵃᵒᵖ<GOAL>(AddSubmonoid.closure s).unop = AddSubmonoid.closure (AddOpposite.op ⁻¹' s)
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>s : Set Mᵐᵒᵖ<GOAL>(Submonoid.closure s).unop = Submonoid.closure (MulOpposite.op ⁻¹' s)
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>H : AddSubmonoid M<VAR>b : { b // (fun x => x ∈ H.op) b }<GOAL>↑(H.equivOp.symm b) = AddOpposite.unop ↑b
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>H : AddSubmonoid M<VAR>a : { a // (fun x => x ∈ H) a }<GOAL>↑(H.equivOp a) = AddOpposite.op ↑a
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>H : Submonoid M<VAR>b : { b // (fun x => x ∈ H.op) b }<GOAL>↑(H.equivOp.symm b) = MulOpposite.unop ↑b
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>H : Submonoid M<VAR>a : { a // (fun x => x ∈ H) a }<GOAL>↑(H.equivOp a) = MulOpposite.op ↑a
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>Monotone AddSubmonoid.addUnits
<VAR>M : Type u_1<VAR>Monoid M<GOAL>Monotone Submonoid.units
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<GOAL>S.units.ofUnits ≤ S
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<GOAL>S.addUnits.ofAddUnits ≤ S
<VAR>M : Type u_1<VAR>Monoid M<GOAL>Monotone Subgroup.ofUnits
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>Monotone AddSubgroup.ofAddUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Subgroup Mˣ<GOAL>S.ofUnits.units = S
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubgroup (AddUnits M)<GOAL>S.ofAddUnits.addUnits = S
<VAR>M : Type u_1<VAR>Monoid M<GOAL>GaloisConnection Subgroup.ofUnits Submonoid.units
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>GaloisConnection AddSubgroup.ofAddUnits AddSubmonoid.addUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>H : Subgroup Mˣ<GOAL>H.ofUnits ≤ S ↔ H ≤ S.units
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>H : AddSubgroup (AddUnits M)<GOAL>H.ofAddUnits ≤ S ↔ H ≤ S.addUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>x : Mˣ<GOAL>x ∈ S.units ↔ ↑x ∈ S ∧ ↑x⁻¹ ∈ S
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>x : AddUnits M<GOAL>x ∈ S.addUnits ↔ ↑x ∈ S ∧ ↑(-x) ∈ S
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>x : Mˣ<VAR>h₁ : ↑x ∈ S<VAR>h₂ : ↑x⁻¹ ∈ S<GOAL>x ∈ S.units
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>x : AddUnits M<VAR>h₁ : ↑x ∈ S<VAR>h₂ : ↑(-x) ∈ S<GOAL>x ∈ S.addUnits
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>x : AddUnits M<VAR>h : x ∈ S.addUnits<GOAL>↑x ∈ S
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>x : Mˣ<VAR>h : x ∈ S.units<GOAL>↑x ∈ S
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>x : AddUnits M<VAR>h : x ∈ S.addUnits<GOAL>↑(-x) ∈ S
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>x : Mˣ<VAR>h : x ∈ S.units<GOAL>↑x⁻¹ ∈ S
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>x : (↥S)ˣ<GOAL>↑↑x⁻¹ * ↑↑x = 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>x : AddUnits ↥S<GOAL>↑↑(-x) + ↑↑x = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>x : (↥S)ˣ<GOAL>↑↑x * ↑↑x⁻¹ = 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>x : AddUnits ↥S<GOAL>↑↑x + ↑↑(-x) = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>x : Mˣ<VAR>h : x ∈ S.units<GOAL>⟨(Units.coeHom M) x⁻¹, ⋯⟩ * ⟨(Units.coeHom M) x, ⋯⟩ = 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>x : AddUnits M<VAR>h : x ∈ S.addUnits<GOAL>⟨(AddUnits.coeHom M) (-x), ⋯⟩ + ⟨(AddUnits.coeHom M) x, ⋯⟩ = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>x : Mˣ<VAR>h : x ∈ S.units<GOAL>⟨(Units.coeHom M) x, ⋯⟩ * ⟨(Units.coeHom M) x⁻¹, ⋯⟩ = 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>x : AddUnits M<VAR>h : x ∈ S.addUnits<GOAL>⟨(AddUnits.coeHom M) x, ⋯⟩ + ⟨(AddUnits.coeHom M) (-x), ⋯⟩ = 0
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>x y : AddUnits M<VAR>h₁ : x ∈ S.addUnits<VAR>h₂ : y ∈ S.addUnits<GOAL>x + y ∈ S.addUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>x y : Mˣ<VAR>h₁ : x ∈ S.units<VAR>h₂ : y ∈ S.units<GOAL>x * y ∈ S.units
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>x : Mˣ<VAR>h : x ∈ S.units<GOAL>x⁻¹ ∈ S.units
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>x : AddUnits M<VAR>h : x ∈ S.addUnits<GOAL>-x ∈ S.addUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>x : Mˣ<GOAL>x⁻¹ ∈ S.units ↔ x ∈ S.units
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>x : AddUnits M<GOAL>-x ∈ S.addUnits ↔ x ∈ S.addUnits
<VAR>M : Type u_1<VAR>Monoid M<GOAL>⊤.units = ⊤
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>⊤.addUnits = ⊤
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S T : AddSubmonoid M<GOAL>(S ⊓ T).addUnits = S.addUnits ⊓ T.addUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>S T : Submonoid M<GOAL>(S ⊓ T).units = S.units ⊓ T.units
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set (AddSubmonoid M)<GOAL>(sInf s).addUnits = ⨅ S ∈ s, S.addUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set (Submonoid M)<GOAL>(sInf s).units = ⨅ S ∈ s, S.units
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>ι : Sort u_2<VAR>f : ι → AddSubmonoid M<GOAL>(iInf f).addUnits = ⨅ i, (f i).addUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>ι : Sort u_2<VAR>f : ι → Submonoid M<GOAL>(iInf f).units = ⨅ i, (f i).units
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>f : (i : ι) → κ i → AddSubmonoid M<GOAL>(⨅ i, ⨅ j, f i j).addUnits = ⨅ i, ⨅ j, (f i j).addUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>f : (i : ι) → κ i → Submonoid M<GOAL>(⨅ i, ⨅ j, f i j).units = ⨅ i, ⨅ j, (f i j).units
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>⊥.addUnits = ⊥
<VAR>M : Type u_1<VAR>Monoid M<GOAL>⊥.units = ⊥
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>Function.Surjective AddSubmonoid.addUnits
<VAR>M : Type u_1<VAR>Monoid M<GOAL>Function.Surjective Submonoid.units
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>Function.LeftInverse AddSubmonoid.addUnits AddSubgroup.ofAddUnits
<VAR>M : Type u_1<VAR>Monoid M<GOAL>Function.LeftInverse Submonoid.units Subgroup.ofUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Subgroup Mˣ<VAR>x : M<GOAL>x ∈ S.ofUnits ↔ ∃ y ∈ S, ↑y = x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubgroup (AddUnits M)<VAR>x : M<GOAL>x ∈ S.ofAddUnits ↔ ∃ y ∈ S, ↑y = x
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Subgroup Mˣ<VAR>x : M<VAR>y : Mˣ<VAR>h₁ : y ∈ S<VAR>h₂ : ↑y = x<GOAL>x ∈ S.ofUnits
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubgroup (AddUnits M)<VAR>x : M<VAR>y : AddUnits M<VAR>h₁ : y ∈ S<VAR>h₂ : ↑y = x<GOAL>x ∈ S.ofAddUnits
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubgroup (AddUnits M)<VAR>x : M<VAR>h : x ∈ S.ofAddUnits<GOAL>∃ y ∈ S, ↑y = x
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Subgroup Mˣ<VAR>x : M<VAR>h : x ∈ S.ofUnits<GOAL>∃ y ∈ S, ↑y = x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubgroup (AddUnits M)<VAR>y : AddUnits M<VAR>hy : ↑y ∈ S.ofAddUnits<GOAL>y ∈ S
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Subgroup Mˣ<VAR>y : Mˣ<VAR>hy : ↑y ∈ S.ofUnits<GOAL>y ∈ S
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubgroup (AddUnits M)<VAR>x : M<VAR>hx : x ∈ S.ofAddUnits<GOAL>IsAddUnit x
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Subgroup Mˣ<VAR>x : M<VAR>hx : x ∈ S.ofUnits<GOAL>IsUnit x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubgroup (AddUnits M)<VAR>x : AddUnits M<VAR>h : ↑x ∈ S.ofAddUnits<GOAL>S.addUnit_of_mem_ofAddUnits h = x
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Subgroup Mˣ<VAR>x : Mˣ<VAR>h : ↑x ∈ S.ofUnits<GOAL>S.unit_of_mem_ofUnits h = x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubgroup (AddUnits M)<VAR>x : M<VAR>h : x ∈ S.ofAddUnits<GOAL>↑(S.addUnit_of_mem_ofAddUnits h) = x
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Subgroup Mˣ<VAR>x : M<VAR>h : x ∈ S.ofUnits<GOAL>↑(S.unit_of_mem_ofUnits h) = x
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Subgroup Mˣ<VAR>x : M<VAR>h : x ∈ S.ofUnits<GOAL>S.unit_of_mem_ofUnits h ∈ S
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubgroup (AddUnits M)<VAR>x : M<VAR>h : x ∈ S.ofAddUnits<GOAL>S.addUnit_of_mem_ofAddUnits h ∈ S
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubgroup (AddUnits M)<VAR>x : M<VAR>h₁ : IsAddUnit x<VAR>h₂ : x ∈ S.ofAddUnits<GOAL>h₁.addUnit = S.addUnit_of_mem_ofAddUnits h₂
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Subgroup Mˣ<VAR>x : M<VAR>h₁ : IsUnit x<VAR>h₂ : x ∈ S.ofUnits<GOAL>h₁.unit = S.unit_of_mem_ofUnits h₂