-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem fromLocalizedModule.inj : Function.Injective <| fromLocalizedModule S f := fun x y eq1 => by
  induction' x with a b
  induction' y with a' b'
  simp only [fromLocalizedModule_mk] at eq1
  rw [Module.End_algebraMap_isUnit_inv_apply_eq_iff, ← LinearMap.map_smul,
    Module.End_algebraMap_isUnit_inv_apply_eq_iff'] at eq1
  rw [LocalizedModule.mk_eq, ← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def,
    Submonoid.smul_def, f.map_smul, f.map_smul, eq1]

Proof state:
case h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
y : LocalizedModule S M
a : M
b : ↥S
eq1 : (fromLocalizedModule S f) (LocalizedModule.mk a b) = (fromLocalizedModule S f) y
⊢ LocalizedModule.mk a b = y

Tactic:
induction' y with a' b'

Result:
case h.h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : (fromLocalizedModule S f) (LocalizedModule.mk a b) = (fromLocalizedModule S f) (LocalizedModule.mk a' b')
⊢ LocalizedModule.mk a b = LocalizedModule.mk a' b'

Proof state:
case h.h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : ↑b • f a' = ↑b' • f a
⊢ LocalizedModule.mk a b = LocalizedModule.mk a' b'

Tactic:
rw [LocalizedModule.mk_eq, ← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def,
  Submonoid.smul_def, f.map_smul, f.map_smul, eq1]

Result:
no goals

Proof state:
case h.h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : (fromLocalizedModule S f) (LocalizedModule.mk a b) = (fromLocalizedModule S f) (LocalizedModule.mk a' b')
⊢ LocalizedModule.mk a b = LocalizedModule.mk a' b'

Tactic:
simp only [fromLocalizedModule_mk] at eq1

Result:
case h.h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : ↑⋯.unit⁻¹ (f a) = ↑⋯.unit⁻¹ (f a')
⊢ LocalizedModule.mk a b = LocalizedModule.mk a' b'

Proof state:
case h.h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : ↑⋯.unit⁻¹ (f a) = ↑⋯.unit⁻¹ (f a')
⊢ LocalizedModule.mk a b = LocalizedModule.mk a' b'

Tactic:
rw [Module.End_algebraMap_isUnit_inv_apply_eq_iff, ← LinearMap.map_smul,
  Module.End_algebraMap_isUnit_inv_apply_eq_iff'] at eq1

Result:
case h.h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : ↑b • f a' = ↑b' • f a
⊢ LocalizedModule.mk a b = LocalizedModule.mk a' b'

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x y : LocalizedModule S M
eq1 : (fromLocalizedModule S f) x = (fromLocalizedModule S f) y
⊢ x = y

Tactic:
induction' x with a b

Result:
case h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
y : LocalizedModule S M
a : M
b : ↥S
eq1 : (fromLocalizedModule S f) (LocalizedModule.mk a b) = (fromLocalizedModule S f) y
⊢ LocalizedModule.mk a b = y