ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>x y : M × ↥S<GOAL>(AddLocalization.r S) x y ↔ ∃ c, ↑c + (↑y.2 + x.1) = ↑c + (↑x.2 + y.1)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>x y : M × ↥S<GOAL>(AddLocalization.r S) x y ↔ Setoid.r x y
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>x y : M × ↥S<GOAL>(Localization.r S) x y ↔ Setoid.r x y
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>a c : M<VAR>b d : ↥S<GOAL>AddLocalization.mk a b = AddLocalization.mk c d ↔ (AddLocalization.r S) (a, b) (c, d)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>a c : M<VAR>b d : ↥S<GOAL>Localization.mk a b = Localization.mk c d ↔ (Localization.r S) (a, b) (c, d)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>a c : M<VAR>b d : ↥S<GOAL>AddLocalization.mk a b + AddLocalization.mk c d = AddLocalization.mk (a + c) (b + d)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>a c : M<VAR>b d : ↥S<GOAL>Localization.mk a b * Localization.mk c d = Localization.mk (a * c) (b * d)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<GOAL>Localization.mk 1 1 = 1
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<GOAL>AddLocalization.mk 0 0 = 0
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>n : ℕ<VAR>a : M<VAR>b : ↥S<GOAL>n • AddLocalization.mk a b = AddLocalization.mk (n • a) (n • b)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>n : ℕ<VAR>a : M<VAR>b : ↥S<GOAL>Localization.mk a b ^ n = Localization.mk (a ^ n) (b ^ n)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>p : Localization S → Sort u<VAR>f : (a : M) → (b : ↥S) → p (Localization.mk a b)<VAR>H : ∀ {a c : M} {b d : ↥S} (h : (Localization.r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d<VAR>a : M<VAR>b : ↥S<GOAL>Localization.rec f H (Localization.mk a b) = f a b
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>p : AddLocalization S → Sort u<VAR>f : (a : M) → (b : ↥S) → p (AddLocalization.mk a b)<VAR>H : ∀ {a c : M} {b d : ↥S} (h : (AddLocalization.r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d<VAR>a : M<VAR>b : ↥S<GOAL>AddLocalization.rec f H (AddLocalization.mk a b) = f a b
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>p : Sort u<VAR>f : M → ↥S → p<VAR>H : ∀ {a c : M} {b d : ↥S}, (Localization.r S) (a, b) (c, d) → f a b = f c d<VAR>a : M<VAR>b : ↥S<GOAL>(Localization.mk a b).liftOn f H = f a b
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>p : Sort u<VAR>f : M → ↥S → p<VAR>H : ∀ {a c : M} {b d : ↥S}, (AddLocalization.r S) (a, b) (c, d) → f a b = f c d<VAR>a : M<VAR>b : ↥S<GOAL>(AddLocalization.mk a b).liftOn f H = f a b
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>p : Localization S → Prop<VAR>H : ∀ (y : M × ↥S), p (Localization.mk y.1 y.2)<VAR>x : Localization S<GOAL>p x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>p : AddLocalization S → Prop<VAR>H : ∀ (y : M × ↥S), p (AddLocalization.mk y.1 y.2)<VAR>x : AddLocalization S<GOAL>p x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>p : AddLocalization S → Prop<VAR>x : AddLocalization S<VAR>H : ∀ (y : M × ↥S), p (AddLocalization.mk y.1 y.2)<GOAL>p x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>p : Localization S → Prop<VAR>x : Localization S<VAR>H : ∀ (y : M × ↥S), p (Localization.mk y.1 y.2)<GOAL>p x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>p : Sort u_4<VAR>f : M → ↥S → M → ↥S → p<VAR>H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S}, (Localization.r S) (a, b) (a', b') → (Localization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d'<VAR>a c : M<VAR>b d : ↥S<GOAL>(Localization.mk a b).liftOn₂ (Localization.mk c d) f H = f a b c d
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>p : Sort u_4<VAR>f : M → ↥S → M → ↥S → p<VAR>H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S}, (AddLocalization.r S) (a, b) (a', b') → (AddLocalization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d'<VAR>a c : M<VAR>b d : ↥S<GOAL>(AddLocalization.mk a b).liftOn₂ (AddLocalization.mk c d) f H = f a b c d
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>p : AddLocalization S → AddLocalization S → Prop<VAR>x y : AddLocalization S<VAR>H : ∀ (x y : M × ↥S), p (AddLocalization.mk x.1 x.2) (AddLocalization.mk y.1 y.2)<GOAL>p x y
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>p : Localization S → Localization S → Prop<VAR>x y : Localization S<VAR>H : ∀ (x y : M × ↥S), p (Localization.mk x.1 x.2) (Localization.mk y.1 y.2)<GOAL>p x y
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>p : Localization S → Localization S → Localization S → Prop<VAR>x y z : Localization S<VAR>H : ∀ (x y z : M × ↥S), p (Localization.mk x.1 x.2) (Localization.mk y.1 y.2) (Localization.mk z.1 z.2)<GOAL>p x y z
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>p : AddLocalization S → AddLocalization S → AddLocalization S → Prop<VAR>x y z : AddLocalization S<VAR>H : ∀ (x y z : M × ↥S), p (AddLocalization.mk x.1 x.2) (AddLocalization.mk y.1 y.2) (AddLocalization.mk z.1 z.2)<GOAL>p x y z
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>y : ↥S<GOAL>(Localization.r S) 1 (↑y, y)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>y : ↥S<GOAL>(AddLocalization.r S) 0 (↑y, y)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>x y : M × ↥S<VAR>h : ↑y.2 * x.1 = ↑x.2 * y.1<GOAL>(Localization.r S) x y
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>x y : M × ↥S<VAR>h : ↑y.2 + x.1 = ↑x.2 + y.1<GOAL>(AddLocalization.r S) x y
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>a : ↥S<GOAL>Localization.mk (↑a) a = 1
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>a : ↥S<GOAL>AddLocalization.mk (↑a) a = 0
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>R : Type u_4<VAR>SMul R M<VAR>IsScalarTower R M M<VAR>c : R<VAR>a : M<VAR>b : ↥S<GOAL>c • Localization.mk a b = Localization.mk (c • a) b
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f g : S.LocalizationMap N<VAR>h : ∀ (x : M), f.toMap x = g.toMap x<GOAL>f = g
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f g : S.LocalizationMap N<VAR>h : ∀ (x : M), f.toMap x = g.toMap x<GOAL>f = g
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f g : S.LocalizationMap N<GOAL>f = g ↔ ∀ (x : M), f.toMap x = g.toMap x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f g : S.LocalizationMap N<GOAL>f = g ↔ ∀ (x : M), f.toMap x = g.toMap x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<GOAL>Function.Injective AddSubmonoid.LocalizationMap.toMap
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<GOAL>Function.Injective Submonoid.LocalizationMap.toMap
<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>y : ↥S<GOAL>IsAddUnit (f.toMap ↑y)
<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>y : ↥S<GOAL>IsUnit (f.toMap ↑y)
<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>∃ x, z + f.toMap ↑x.2 = f.toMap x.1
<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>∃ x, z * f.toMap ↑x.2 = f.toMap x.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 w : N<GOAL>∃ z' w' d, z + f.toMap ↑d = f.toMap z' ∧ w + f.toMap ↑d = f.toMap w'
<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 w : N<GOAL>∃ z' w' d, z * f.toMap ↑d = f.toMap z' ∧ w * f.toMap ↑d = f.toMap w'
<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 y : M<GOAL>f.toMap x = f.toMap y ↔ ∃ c, ↑c + x = ↑c + y
<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 y : M<GOAL>f.toMap x = f.toMap y ↔ ∃ c, ↑c * x = ↑c * y
<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>z + f.toMap ↑(f.sec z).2 = f.toMap (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>f : S.LocalizationMap N<VAR>z : N<GOAL>z * f.toMap ↑(f.sec z).2 = f.toMap (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>f : S.LocalizationMap N<VAR>z : N<GOAL>f.toMap (f.sec z).1 = f.toMap ↑(f.sec z).2 * z
<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.toMap (f.sec z).1 = f.toMap ↑(f.sec z).2 + z
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : M →+ N<VAR>h : ∀ (y : ↥S), IsAddUnit (f ↑y)<VAR>y : ↥S<VAR>w z : N<GOAL>w + ↑(-(IsAddUnit.liftRight (f.restrict S) h) y) = z ↔ w = f ↑y + z
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : M →* N<VAR>h : ∀ (y : ↥S), IsUnit (f ↑y)<VAR>y : ↥S<VAR>w z : N<GOAL>w * ↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ = z ↔ w = f ↑y * z
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : M →+ N<VAR>h : ∀ (y : ↥S), IsAddUnit (f ↑y)<VAR>y : ↥S<VAR>w z : N<GOAL>z = w + ↑(-(IsAddUnit.liftRight (f.restrict S) h) y) ↔ z + f ↑y = w
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : M →* N<VAR>h : ∀ (y : ↥S), IsUnit (f ↑y)<VAR>y : ↥S<VAR>w z : N<GOAL>z = w * ↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ ↔ z * f ↑y = w
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : M →* N<VAR>h : ∀ (y : ↥S), IsUnit (f ↑y)<VAR>x₁ x₂ : M<VAR>y₁ y₂ : ↥S<GOAL>f x₁ * ↑((IsUnit.liftRight (f.restrict S) h) y₁)⁻¹ = f x₂ * ↑((IsUnit.liftRight (f.restrict S) h) y₂)⁻¹ ↔ f (x₁ * ↑y₂) = f (x₂ * ↑y₁)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : M →+ N<VAR>h : ∀ (y : ↥S), IsAddUnit (f ↑y)<VAR>x₁ x₂ : M<VAR>y₁ y₂ : ↥S<GOAL>f x₁ + ↑(-(IsAddUnit.liftRight (f.restrict S) h) y₁) = f x₂ + ↑(-(IsAddUnit.liftRight (f.restrict S) h) y₂) ↔ f (x₁ + ↑y₂) = f (x₂ + ↑y₁)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : M →* N<VAR>hf : ∀ (y : ↥S), IsUnit (f ↑y)<VAR>y z : ↥S<VAR>h : ((IsUnit.liftRight (f.restrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.restrict S) hf) z)⁻¹<GOAL>f ↑y = f ↑z
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : M →+ N<VAR>hf : ∀ (y : ↥S), IsAddUnit (f ↑y)<VAR>y z : ↥S<VAR>h : -(IsAddUnit.liftRight (f.restrict S) hf) y = -(IsAddUnit.liftRight (f.restrict S) hf) z<GOAL>f ↑y = f ↑z
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : M →+ N<VAR>h : ∀ (y : ↥S), IsAddUnit (f ↑y)<VAR>y : ↥S<VAR>z : N<VAR>H : f ↑y + z = 0<GOAL>↑(-(IsAddUnit.liftRight (f.restrict S) h) y) = z
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : M →* N<VAR>h : ∀ (y : ↥S), IsUnit (f ↑y)<VAR>y : ↥S<VAR>z : N<VAR>H : f ↑y * z = 1<GOAL>↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ = z
<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 y : M<VAR>c : ↥S<VAR>h : f.toMap (↑c + x) = f.toMap (↑c + y)<GOAL>f.toMap x = f.toMap y
<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 y : M<VAR>c : ↥S<VAR>h : f.toMap (↑c * x) = f.toMap (↑c * y)<GOAL>f.toMap x = f.toMap y
<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 y : M<VAR>c : ↥S<VAR>h : f.toMap (x + ↑c) = f.toMap (y + ↑c)<GOAL>f.toMap x = f.toMap y
<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 y : M<VAR>c : ↥S<VAR>h : f.toMap (x * ↑c) = f.toMap (y * ↑c)<GOAL>f.toMap x = f.toMap y
<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₁ x₂ : M<VAR>y₁ y₂ : ↥S<GOAL>f.mk' (x₁ * x₂) (y₁ * y₂) = f.mk' x₁ y₁ * f.mk' x₂ y₂
<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₁ x₂ : M<VAR>y₁ y₂ : ↥S<GOAL>f.mk' (x₁ + x₂) (y₁ + y₂) = f.mk' x₁ y₁ + f.mk' x₂ y₂
<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 : M<GOAL>f.mk' x 0 = f.toMap 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 : M<GOAL>f.mk' x 1 = f.toMap 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>z : N<GOAL>f.mk' (f.sec z).1 (f.sec z).2 = 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.mk' (f.sec z).1 (f.sec z).2 = z
<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>∃ x y, f.mk' x y = 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>∃ x y, f.mk' x y = z
<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 : M<VAR>y : ↥S<GOAL>f.mk' x y + f.toMap ↑y = f.toMap 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 : M<VAR>y : ↥S<GOAL>f.mk' x y * f.toMap ↑y = f.toMap 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 : M<VAR>y : ↥S<GOAL>f.toMap ↑y * f.mk' x y = f.toMap 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>x : M<VAR>y : ↥S<GOAL>f.toMap ↑y + f.mk' x y = f.toMap 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 : M<VAR>y : ↥S<VAR>z : N<GOAL>z = f.mk' x y ↔ z * f.toMap ↑y = f.toMap 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>x : M<VAR>y : ↥S<VAR>z : N<GOAL>z = f.mk' x y ↔ z + f.toMap ↑y = f.toMap 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 : M<VAR>y : ↥S<VAR>z : N<GOAL>f.mk' x y = z ↔ f.toMap x = z * f.toMap ↑y
<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 : M<VAR>y : ↥S<VAR>z : N<GOAL>f.mk' x y = z ↔ f.toMap x = z + f.toMap ↑y
<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₁ x₂ : M<VAR>y₁ y₂ : ↥S<GOAL>f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (↑y₂ + x₁) = f.toMap (↑y₁ + 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₁ x₂ : M<VAR>y₁ y₂ : ↥S<GOAL>f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (↑y₂ * x₁) = f.toMap (↑y₁ * 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₁ x₂ : M<VAR>y₁ y₂ : ↥S<GOAL>f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (x₁ * ↑y₂) = f.toMap (x₂ * ↑y₁)
<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₁ x₂ : M<VAR>y₁ y₂ : ↥S<GOAL>f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (x₁ + ↑y₂) = f.toMap (x₂ + ↑y₁)
<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>a₁ b₁ : M<VAR>a₂ b₂ : ↥S<GOAL>f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ ∃ c, ↑c * (↑b₂ * a₁) = ↑c * (↑a₂ * b₁)
<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>a₁ b₁ : M<VAR>a₂ b₂ : ↥S<GOAL>f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ ∃ c, ↑c + (↑b₂ + a₁) = ↑c + (↑a₂ + b₁)
<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>a₁ b₁ : M<VAR>a₂ b₂ : ↥S<GOAL>f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ (AddLocalization.r S) (a₁, a₂) (b₁, b₂)
<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>a₁ b₁ : M<VAR>a₂ b₂ : ↥S<GOAL>f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ (Localization.r S) (a₁, a₂) (b₁, b₂)
<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 : S.LocalizationMap P<VAR>x y : M<GOAL>f.toMap x = f.toMap y ↔ g.toMap x = g.toMap 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 : S.LocalizationMap P<VAR>x y : M<GOAL>f.toMap x = f.toMap y ↔ g.toMap x = g.toMap 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 : S.LocalizationMap P<VAR>x₁ x₂ : M<VAR>y₁ y₂ : ↥S<GOAL>f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ g.mk' x₁ y₁ = g.mk' x₂ 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 : S.LocalizationMap P<VAR>x₁ x₂ : M<VAR>y₁ y₂ : ↥S<GOAL>f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ g.mk' x₁ y₁ = g.mk' x₂ y₂
<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 : M<VAR>y : ↥S<GOAL>∃ c, ↑c + (↑(f.sec (f.mk' x y)).2 + x) = ↑c + (↑y + (f.sec (f.mk' x y)).1)
<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 : M<VAR>y : ↥S<GOAL>∃ c, ↑c * (↑(f.sec (f.mk' x y)).2 * x) = ↑c * (↑y * (f.sec (f.mk' x y)).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>a₁ b₁ : M<VAR>a₂ b₂ : ↥S<VAR>H : ↑a₂ + b₁ = ↑b₂ + a₁<GOAL>f.mk' a₁ a₂ = f.mk' b₁ b₂
<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>a₁ b₁ : M<VAR>a₂ b₂ : ↥S<VAR>H : ↑a₂ * b₁ = ↑b₂ * a₁<GOAL>f.mk' a₁ a₂ = f.mk' b₁ b₂
<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>a₁ b₁ : M<VAR>a₂ b₂ : ↥S<VAR>H : b₁ + ↑a₂ = a₁ + ↑b₂<GOAL>f.mk' a₁ a₂ = f.mk' b₁ b₂
<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>a₁ b₁ : M<VAR>a₂ b₂ : ↥S<VAR>H : b₁ * ↑a₂ = a₁ * ↑b₂<GOAL>f.mk' a₁ a₂ = f.mk' b₁ b₂
<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>a : M<VAR>b c : ↥S<GOAL>f.mk' (a + ↑c) (b + c) = f.mk' a b
<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>a : M<VAR>b c : ↥S<GOAL>f.mk' (a * ↑c) (b * c) = f.mk' a b
<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>a b : M<VAR>d : ↥S<GOAL>f.mk' a d = f.mk' b d ↔ ∃ c, ↑c * a = ↑c * b
<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>a b : M<VAR>d : ↥S<GOAL>f.mk' a d = f.mk' b d ↔ ∃ c, ↑c + a = ↑c + b
<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>y : ↥S<GOAL>f.mk' (↑y) y = 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>y : ↥S<GOAL>f.mk' (↑y) y = 0
<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 : M<VAR>H : x ∈ S<GOAL>f.mk' x ⟨x, H⟩ = 0
<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 : M<VAR>H : x ∈ S<GOAL>f.mk' x ⟨x, H⟩ = 1
<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₁ x₂ : M<VAR>y : ↥S<GOAL>f.toMap x₁ * f.mk' x₂ y = f.mk' (x₁ * x₂) y
<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₁ x₂ : M<VAR>y : ↥S<GOAL>f.toMap x₁ + f.mk' x₂ y = f.mk' (x₁ + x₂) y
<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₁ x₂ : M<VAR>y : ↥S<GOAL>f.mk' x₂ y * f.toMap x₁ = f.mk' (x₁ * x₂) y
<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₁ x₂ : M<VAR>y : ↥S<GOAL>f.mk' x₂ y + f.toMap x₁ = f.mk' (x₁ + x₂) y
<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 : M<VAR>y : ↥S<GOAL>f.toMap x + f.mk' 0 y = f.mk' x y
<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 : M<VAR>y : ↥S<GOAL>f.toMap x * f.mk' 1 y = f.mk' x y
<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 : M<VAR>y : ↥S<GOAL>f.mk' (x + ↑y) y = f.toMap 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 : M<VAR>y : ↥S<GOAL>f.mk' (x * ↑y) y = f.toMap 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 : M<VAR>y : ↥S<GOAL>f.mk' (↑y * x) y = f.toMap 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>x : M<VAR>y : ↥S<GOAL>f.mk' (↑y + x) y = 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>j : N →+ P<VAR>y : ↥S<GOAL>IsAddUnit ((j.comp f.toMap) ↑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>j : N →* P<VAR>y : ↥S<GOAL>IsUnit ((j.comp f.toMap) ↑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 y : M<VAR>h : f.toMap x = f.toMap y<GOAL>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>hg : ∀ (y : ↥S), IsAddUnit (g ↑y)<VAR>x y : M<VAR>h : f.toMap x = f.toMap y<GOAL>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>Q : Type u_4<VAR>CommMonoid 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)