-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem ext {f g : LocalizationMap S N} (h : ∀ x, f.toMap x = g.toMap x) : f = g

Proof state:
case mk.mk.mk.mk
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
toOneHom✝¹ : OneHom M N
map_mul'✝¹ : ∀ (x y : M), toOneHom✝¹.toFun (x * y) = toOneHom✝¹.toFun x * toOneHom✝¹.toFun y
map_units'✝¹ : ∀ (y : ↥S), IsUnit ((↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun ↑y)
surj'✝¹ :
  ∀ (z : N),
    ∃ x,
      z * (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun ↑x.2 =
        (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun x.1
exists_of_eq✝¹ :
  ∀ (x y : M),
    (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun x =
        (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun y →
      ∃ c, ↑c * x = ↑c * y
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), toOneHom✝.toFun (x * y) = toOneHom✝.toFun x * toOneHom✝.toFun y
map_units'✝ : ∀ (y : ↥S), IsUnit ((↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun ↑y)
surj'✝ :
  ∀ (z : N),
    ∃ x,
      z * (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun ↑x.2 =
        (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun x.1
exists_of_eq✝ :
  ∀ (x y : M),
    (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun x =
        (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun y →
      ∃ c, ↑c * x = ↑c * y
h :
  ∀ (x : M),
    { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹, map_units' := map_units'✝¹, surj' := surj'✝¹,
            exists_of_eq := exists_of_eq✝¹ }.toMap
        x =
      { toOneHom := toOneHom✝, map_mul' := map_mul'✝, map_units' := map_units'✝, surj' := surj'✝,
            exists_of_eq := exists_of_eq✝ }.toMap
        x
⊢ { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹, map_units' := map_units'✝¹, surj' := surj'✝¹,
      exists_of_eq := exists_of_eq✝¹ } =
    { toOneHom := toOneHom✝, map_mul' := map_mul'✝, map_units' := map_units'✝, surj' := surj'✝,
      exists_of_eq := exists_of_eq✝ }

Tactic:
simp only [mk.injEq, MonoidHom.mk.injEq]

Result:
case mk.mk.mk.mk
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
toOneHom✝¹ : OneHom M N
map_mul'✝¹ : ∀ (x y : M), toOneHom✝¹.toFun (x * y) = toOneHom✝¹.toFun x * toOneHom✝¹.toFun y
map_units'✝¹ : ∀ (y : ↥S), IsUnit ((↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun ↑y)
surj'✝¹ :
  ∀ (z : N),
    ∃ x,
      z * (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun ↑x.2 =
        (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun x.1
exists_of_eq✝¹ :
  ∀ (x y : M),
    (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun x =
        (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun y →
      ∃ c, ↑c * x = ↑c * y
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), toOneHom✝.toFun (x * y) = toOneHom✝.toFun x * toOneHom✝.toFun y
map_units'✝ : ∀ (y : ↥S), IsUnit ((↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun ↑y)
surj'✝ :
  ∀ (z : N),
    ∃ x,
      z * (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun ↑x.2 =
        (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun x.1
exists_of_eq✝ :
  ∀ (x y : M),
    (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun x =
        (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun y →
      ∃ c, ↑c * x = ↑c * y
h :
  ∀ (x : M),
    { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹, map_units' := map_units'✝¹, surj' := surj'✝¹,
            exists_of_eq := exists_of_eq✝¹ }.toMap
        x =
      { toOneHom := toOneHom✝, map_mul' := map_mul'✝, map_units' := map_units'✝, surj' := surj'✝,
            exists_of_eq := exists_of_eq✝ }.toMap
        x
⊢ toOneHom✝¹ = toOneHom✝

Proof state:
case mk.mk.mk.mk
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
toOneHom✝¹ : OneHom M N
map_mul'✝¹ : ∀ (x y : M), toOneHom✝¹.toFun (x * y) = toOneHom✝¹.toFun x * toOneHom✝¹.toFun y
map_units'✝¹ : ∀ (y : ↥S), IsUnit ((↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun ↑y)
surj'✝¹ :
  ∀ (z : N),
    ∃ x,
      z * (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun ↑x.2 =
        (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun x.1
exists_of_eq✝¹ :
  ∀ (x y : M),
    (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun x =
        (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun y →
      ∃ c, ↑c * x = ↑c * y
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), toOneHom✝.toFun (x * y) = toOneHom✝.toFun x * toOneHom✝.toFun y
map_units'✝ : ∀ (y : ↥S), IsUnit ((↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun ↑y)
surj'✝ :
  ∀ (z : N),
    ∃ x,
      z * (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun ↑x.2 =
        (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun x.1
exists_of_eq✝ :
  ∀ (x y : M),
    (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun x =
        (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun y →
      ∃ c, ↑c * x = ↑c * y
h :
  ∀ (x : M),
    { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹, map_units' := map_units'✝¹, surj' := surj'✝¹,
            exists_of_eq := exists_of_eq✝¹ }.toMap
        x =
      { toOneHom := toOneHom✝, map_mul' := map_mul'✝, map_units' := map_units'✝, surj' := surj'✝,
            exists_of_eq := exists_of_eq✝ }.toMap
        x
⊢ toOneHom✝¹ = toOneHom✝

Tactic:
exact OneHom.ext h

Result:
no goals