ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>T : AddSubmonoid P<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>hg : ∀ (y : ↥S), g ↑y ∈ T<VAR>k : T.LocalizationMap Q<VAR>x y : M<VAR>h : f.toMap x = f.toMap y<GOAL>k.toMap (g x) = k.toMap (g y)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>x : M<VAR>y : ↥S<GOAL>(f.lift hg) (f.mk' x y) = g x * ↑((IsUnit.liftRight (g.restrict S) hg) y)⁻¹
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>hg : ∀ (y : ↥S), IsAddUnit (g ↑y)<VAR>x : M<VAR>y : ↥S<GOAL>(f.lift hg) (f.mk' x y) = g x + ↑(-(IsAddUnit.liftRight (g.restrict S) hg) y)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>hg : ∀ (y : ↥S), IsAddUnit (g ↑y)<VAR>z : N<VAR>v : P<GOAL>(f.lift hg) z = v ↔ g (f.sec z).1 = g ↑(f.sec z).2 + v
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>z : N<VAR>v : P<GOAL>(f.lift hg) z = v ↔ g (f.sec z).1 = g ↑(f.sec z).2 * v
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>hg : ∀ (y : ↥S), IsAddUnit (g ↑y)<VAR>z : N<VAR>w v : P<GOAL>(f.lift hg) z + w = v ↔ g (f.sec z).1 + w = g ↑(f.sec z).2 + v
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>z : N<VAR>w v : P<GOAL>(f.lift hg) z * w = v ↔ g (f.sec z).1 * w = g ↑(f.sec z).2 * v
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>x : M<VAR>v : P<VAR>y : ↥S<GOAL>(f.lift hg) (f.mk' x y) = v ↔ g x = g ↑y * v
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>hg : ∀ (y : ↥S), IsAddUnit (g ↑y)<VAR>x : M<VAR>v : P<VAR>y : ↥S<GOAL>(f.lift hg) (f.mk' x y) = v ↔ g x = g ↑y + v
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>z : N<GOAL>(f.lift hg) z * g ↑(f.sec z).2 = g (f.sec z).1
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>hg : ∀ (y : ↥S), IsAddUnit (g ↑y)<VAR>z : N<GOAL>(f.lift hg) z + g ↑(f.sec z).2 = g (f.sec z).1
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>hg : ∀ (y : ↥S), IsAddUnit (g ↑y)<VAR>z : N<GOAL>g ↑(f.sec z).2 + (f.lift hg) z = g (f.sec z).1
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>z : N<GOAL>g ↑(f.sec z).2 * (f.lift hg) z = g (f.sec z).1
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>x : M<GOAL>(f.lift hg) (f.toMap x) = g x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>hg : ∀ (y : ↥S), IsAddUnit (g ↑y)<VAR>x : M<GOAL>(f.lift hg) (f.toMap x) = g x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>hg : ∀ (y : ↥S), IsAddUnit (g ↑y)<VAR>x y : M × ↥S<GOAL>(f.lift hg) (f.mk' x.1 x.2) = (f.lift hg) (f.mk' y.1 y.2) ↔ g (x.1 + ↑y.2) = g (y.1 + ↑x.2)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>x y : M × ↥S<GOAL>(f.lift hg) (f.mk' x.1 x.2) = (f.lift hg) (f.mk' y.1 y.2) ↔ g (x.1 * ↑y.2) = g (y.1 * ↑x.2)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<GOAL>(f.lift hg).comp f.toMap = g
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>hg : ∀ (y : ↥S), IsAddUnit (g ↑y)<GOAL>(f.lift hg).comp f.toMap = g
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>j : N →+ P<GOAL>f.lift ⋯ = j
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>j : N →* P<GOAL>f.lift ⋯ = j
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>j k : N →+ P<VAR>h : ∀ (a : M), (j.comp f.toMap) a = (k.comp f.toMap) a<GOAL>j = k
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>j k : N →* P<VAR>h : ∀ (a : M), (j.comp f.toMap) a = (k.comp f.toMap) a<GOAL>j = k
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>hg : ∀ (y : ↥S), IsAddUnit (g ↑y)<VAR>j : N →+ P<VAR>hj : ∀ (x : M), j (f.toMap x) = g x<GOAL>f.lift hg = j
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>j : N →* P<VAR>hj : ∀ (x : M), j (f.toMap x) = g x<GOAL>f.lift hg = j
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : S.LocalizationMap N<VAR>x : N<GOAL>(f.lift ⋯) x = x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : S.LocalizationMap N<VAR>x : N<GOAL>(f.lift ⋯) x = x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : S.LocalizationMap N<VAR>T : AddSubmonoid M<VAR>hST : S ≤ T<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>A : Type u_5<VAR>AddCommMonoid A<VAR>l : M →+ A<VAR>hl : ∀ (w : ↥T), IsAddUnit (l ↑w)<GOAL>(k.lift hl).comp (f.lift ⋯) = f.lift ⋯
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : S.LocalizationMap N<VAR>T : Submonoid M<VAR>hST : S ≤ T<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>A : Type u_5<VAR>CommMonoid A<VAR>l : M →* A<VAR>hl : ∀ (w : ↥T), IsUnit (l ↑w)<GOAL>(k.lift hl).comp (f.lift ⋯) = f.lift ⋯
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : S.LocalizationMap N<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>k : S.LocalizationMap Q<VAR>A : Type u_5<VAR>CommMonoid A<VAR>l : M →* A<VAR>hl : ∀ (w : ↥S), IsUnit (l ↑w)<GOAL>(k.lift hl).comp (f.lift ⋯) = f.lift hl
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : S.LocalizationMap N<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>k : S.LocalizationMap Q<VAR>A : Type u_5<VAR>AddCommMonoid A<VAR>l : M →+ A<VAR>hl : ∀ (w : ↥S), IsAddUnit (l ↑w)<GOAL>(k.lift hl).comp (f.lift ⋯) = f.lift hl
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : S.LocalizationMap P<VAR>z : N<GOAL>(k.lift ⋯) ((f.lift ⋯) z) = z
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : S.LocalizationMap P<VAR>z : N<GOAL>(k.lift ⋯) ((f.lift ⋯) z) = z
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>hg : ∀ (y : ↥S), IsAddUnit (g ↑y)<GOAL>Function.Surjective ⇑(f.lift hg) ↔ ∀ (v : P), ∃ x, v + g ↑x.2 = g x.1
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<GOAL>Function.Surjective ⇑(f.lift hg) ↔ ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>hg : ∀ (y : ↥S), IsAddUnit (g ↑y)<GOAL>Function.Injective ⇑(f.lift hg) ↔ ∀ (x y : M), f.toMap x = f.toMap y ↔ g x = g y
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<GOAL>Function.Injective ⇑(f.lift hg) ↔ ∀ (x y : M), f.toMap x = f.toMap y ↔ g x = g y
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>T : AddSubmonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>x : M<GOAL>(f.map hy k) (f.toMap x) = k.toMap (g x)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>x : M<GOAL>(f.map hy k) (f.toMap x) = k.toMap (g x)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>T : AddSubmonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>k : T.LocalizationMap Q<GOAL>(f.map hy k).comp f.toMap = k.toMap.comp g
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>k : T.LocalizationMap Q<GOAL>(f.map hy k).comp f.toMap = k.toMap.comp g
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>x : M<VAR>y : ↥S<GOAL>(f.map hy k) (f.mk' x y) = k.mk' (g x) ⟨g ↑y, ⋯⟩
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>T : AddSubmonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>x : M<VAR>y : ↥S<GOAL>(f.map hy k) (f.mk' x y) = k.mk' (g x) ⟨g ↑y, ⋯⟩
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>z : N<VAR>u : Q<GOAL>(f.map hy k) z = u ↔ k.toMap (g (f.sec z).1) = k.toMap (g ↑(f.sec z).2) * u
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>T : AddSubmonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>z : N<VAR>u : Q<GOAL>(f.map hy k) z = u ↔ k.toMap (g (f.sec z).1) = k.toMap (g ↑(f.sec z).2) + u
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>T : AddSubmonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>z : N<GOAL>(f.map hy k) z + k.toMap (g ↑(f.sec z).2) = k.toMap (g (f.sec z).1)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>z : N<GOAL>(f.map hy k) z * k.toMap (g ↑(f.sec z).2) = k.toMap (g (f.sec z).1)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>T : AddSubmonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>z : N<GOAL>k.toMap (g ↑(f.sec z).2) + (f.map hy k) z = k.toMap (g (f.sec z).1)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>z : N<GOAL>k.toMap (g ↑(f.sec z).2) * (f.map hy k) z = k.toMap (g (f.sec z).1)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : S.LocalizationMap N<VAR>z : N<GOAL>(f.map ⋯ f) z = z
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : S.LocalizationMap N<VAR>z : N<GOAL>(f.map ⋯ f) z = z
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>A : Type u_5<VAR>CommMonoid A<VAR>U : Submonoid A<VAR>R : Type u_6<VAR>CommMonoid R<VAR>j : U.LocalizationMap R<VAR>l : P →* A<VAR>hl : ∀ (w : ↥T), l ↑w ∈ U<GOAL>(k.map hl j).comp (f.map hy k) = f.map ⋯ j
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>T : AddSubmonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>A : Type u_5<VAR>AddCommMonoid A<VAR>U : AddSubmonoid A<VAR>R : Type u_6<VAR>AddCommMonoid R<VAR>j : U.LocalizationMap R<VAR>l : P →+ A<VAR>hl : ∀ (w : ↥T), l ↑w ∈ U<GOAL>(k.map hl j).comp (f.map hy k) = f.map ⋯ j
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>A : Type u_5<VAR>CommMonoid A<VAR>U : Submonoid A<VAR>R : Type u_6<VAR>CommMonoid R<VAR>j : U.LocalizationMap R<VAR>l : P →* A<VAR>hl : ∀ (w : ↥T), l ↑w ∈ U<VAR>x : N<GOAL>(k.map hl j) ((f.map hy k) x) = (f.map ⋯ j) x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>T : AddSubmonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>A : Type u_5<VAR>AddCommMonoid A<VAR>U : AddSubmonoid A<VAR>R : Type u_6<VAR>AddCommMonoid R<VAR>j : U.LocalizationMap R<VAR>l : P →+ A<VAR>hl : ∀ (w : ↥T), l ↑w ∈ U<VAR>x : N<GOAL>(k.map hl j) ((f.map hy k) x) = (f.map ⋯ j) x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>hg : Function.Injective ⇑g<VAR>k : (AddSubmonoid.map g S).LocalizationMap Q<GOAL>Function.Injective ⇑(f.map ⋯ k)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>hg : Function.Injective ⇑g<VAR>k : (Submonoid.map g S).LocalizationMap Q<GOAL>Function.Injective ⇑(f.map ⋯ k)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →+ P<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>hg : Function.Surjective ⇑g<VAR>k : (AddSubmonoid.map g S).LocalizationMap Q<GOAL>Function.Surjective ⇑(f.map ⋯ k)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>hg : Function.Surjective ⇑g<VAR>k : (Submonoid.map g S).LocalizationMap Q<GOAL>Function.Surjective ⇑(f.map ⋯ k)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>g : M →* P<VAR>x : M<VAR>F : Submonoid.LocalizationMap.AwayMap x N<VAR>hg : IsUnit (g x)<VAR>a : M<GOAL>(Submonoid.LocalizationMap.AwayMap.lift x F hg) ((Submonoid.LocalizationMap.toMap F) a) = g a
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>g : M →* P<VAR>x : M<VAR>F : Submonoid.LocalizationMap.AwayMap x N<VAR>hg : IsUnit (g x)<GOAL>(Submonoid.LocalizationMap.AwayMap.lift x F hg).comp (Submonoid.LocalizationMap.toMap F) = g
<VAR>A : Type u_4<VAR>AddCommMonoid A<VAR>x : A<VAR>B : Type u_5<VAR>AddCommMonoid B<VAR>F : AddSubmonoid.LocalizationMap.AwayMap x B<VAR>C : Type u_6<VAR>AddCommMonoid C<VAR>g : A →+ C<VAR>hg : IsAddUnit (g x)<VAR>a : A<GOAL>(AddSubmonoid.LocalizationMap.AwayMap.lift x F hg) ((AddSubmonoid.LocalizationMap.toMap F) a) = g a
<VAR>A : Type u_4<VAR>AddCommMonoid A<VAR>x : A<VAR>B : Type u_5<VAR>AddCommMonoid B<VAR>F : AddSubmonoid.LocalizationMap.AwayMap x B<VAR>C : Type u_6<VAR>AddCommMonoid C<VAR>g : A →+ C<VAR>hg : IsAddUnit (g x)<GOAL>(AddSubmonoid.LocalizationMap.AwayMap.lift x F hg).comp (AddSubmonoid.LocalizationMap.toMap F) = g
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : S.LocalizationMap P<VAR>x : N<GOAL>(f.mulEquivOfLocalizations k) x = (f.lift ⋯) x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : S.LocalizationMap P<VAR>x : N<GOAL>(f.addEquivOfLocalizations k) x = (f.lift ⋯) x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : S.LocalizationMap P<VAR>x : P<GOAL>(f.mulEquivOfLocalizations k).symm x = (k.lift ⋯) x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : S.LocalizationMap P<VAR>x : P<GOAL>(f.addEquivOfLocalizations k).symm x = (k.lift ⋯) x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : S.LocalizationMap P<GOAL>(k.addEquivOfLocalizations f).symm = f.addEquivOfLocalizations k
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : S.LocalizationMap P<GOAL>(k.mulEquivOfLocalizations f).symm = f.mulEquivOfLocalizations k
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : N ≃* P<VAR>x : M<GOAL>(f.ofMulEquivOfLocalizations k).toMap x = k (f.toMap x)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : N ≃+ P<VAR>x : M<GOAL>(f.ofAddEquivOfLocalizations k).toMap x = k (f.toMap x)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : N ≃+ P<GOAL>(f.ofAddEquivOfLocalizations k).toMap = k.toAddMonoidHom.comp f.toMap
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : N ≃* P<GOAL>(f.ofMulEquivOfLocalizations k).toMap = k.toMonoidHom.comp f.toMap
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : N ≃* P<VAR>x : M<GOAL>k.symm ((f.ofMulEquivOfLocalizations k).toMap x) = f.toMap x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : N ≃+ P<VAR>x : M<GOAL>k.symm ((f.ofAddEquivOfLocalizations k).toMap x) = f.toMap x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : P ≃+ N<VAR>x : M<GOAL>k ((f.ofAddEquivOfLocalizations k.symm).toMap x) = f.toMap x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : P ≃* N<VAR>x : M<GOAL>k ((f.ofMulEquivOfLocalizations k.symm).toMap x) = f.toMap x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : N ≃* P<VAR>x : M<VAR>y : P<GOAL>(f.ofMulEquivOfLocalizations k).toMap x = y ↔ f.toMap x = k.symm y
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : N ≃+ P<VAR>x : M<VAR>y : P<GOAL>(f.ofAddEquivOfLocalizations k).toMap x = y ↔ f.toMap x = k.symm y
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : S.LocalizationMap P<GOAL>f.ofAddEquivOfLocalizations (f.addEquivOfLocalizations k) = k
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : S.LocalizationMap P<GOAL>f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k) = k
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : S.LocalizationMap P<VAR>x : M<GOAL>(f.ofAddEquivOfLocalizations (f.addEquivOfLocalizations k)).toMap x = k.toMap x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : S.LocalizationMap P<VAR>x : M<GOAL>(f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k)).toMap x = k.toMap x