R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.678047
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
m : M'
⊢ ↑(iso S f) (↑(LinearEquiv.symm (iso S f)) m) =
    ↑(iso S f)
      (LocalizedModule.mk (Exists.choose (_ : ∃ x, x.snd • m = ↑f x.fst)).fst
        (Exists.choose (_ : ∃ x, x.snd • m = ↑f x.fst)).snd)
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.678047
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
m : M'
⊢ ↑(LinearEquiv.symm (iso S f)) m =
    LocalizedModule.mk (Exists.choose (_ : ∃ x, x.snd • m = ↑f x.fst)).fst
      (Exists.choose (_ : ∃ x, x.snd • m = ↑f x.fst)).snd
apply_fun iso S f using LinearEquiv.injective (iso S f)
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.678047
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
m : M'
⊢ m =
    ↑(iso S f)
      (LocalizedModule.mk (Exists.choose (_ : ∃ x, x.snd • m = ↑f x.fst)).fst
        (Exists.choose (_ : ∃ x, x.snd • m = ↑f x.fst)).snd)
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.678047
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
m : M'
⊢ ↑(iso S f) (↑(LinearEquiv.symm (iso S f)) m) =
    ↑(iso S f)
      (LocalizedModule.mk (Exists.choose (_ : ∃ x, x.snd • m = ↑f x.fst)).fst
        (Exists.choose (_ : ∃ x, x.snd • m = ↑f x.fst)).snd)
rw [LinearEquiv.apply_symm_apply]
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.678047
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
m : M'
⊢ m =
    fromLocalizedModule' S f
      (LocalizedModule.mk (Exists.choose (_ : ∃ x, x.snd • m = ↑f x.fst)).fst
        (Exists.choose (_ : ∃ x, x.snd • m = ↑f x.fst)).snd)
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.678047
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
m : M'
⊢ m =
    ↑(iso S f)
      (LocalizedModule.mk (Exists.choose (_ : ∃ x, x.snd • m = ↑f x.fst)).fst
        (Exists.choose (_ : ∃ x, x.snd • m = ↑f x.fst)).snd)
simp only [iso_apply, LinearMap.toFun_eq_coe, fromLocalizedModule_mk]
no goals
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.678047
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
m : M'
⊢ m =
    fromLocalizedModule' S f
      (LocalizedModule.mk (Exists.choose (_ : ∃ x, x.snd • m = ↑f x.fst)).fst
        (Exists.choose (_ : ∃ x, x.snd • m = ↑f x.fst)).snd)
erw [Module.End_algebraMap_isUnit_inv_apply_eq_iff', (surj' _).choose_spec]