-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
/-- The linear map `(LocalizedModule S M) → (LocalizedModule S M)` from `iso` is the identity. -/
lemma iso_localizedModule_eq_refl : iso S (mkLinearMap S M) = refl R (LocalizedModule S M)

Proof state:
R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ iso S (mkLinearMap S M) = LinearEquiv.refl R (LocalizedModule S M)

Tactic:
let f := mkLinearMap S M

Result:
R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
⊢ iso S (mkLinearMap S M) = LinearEquiv.refl R (LocalizedModule S M)

Proof state:
R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
e : LocalizedModule S M →ₗ[R] LocalizedModule S M
left✝ : e ∘ₗ f = f
univ : ∀ (y : LocalizedModule S M →ₗ[R] LocalizedModule S M), (fun l => l ∘ₗ f = f) y → y = e
⊢ (fun l => l ∘ₗ f = f) ↑(LinearEquiv.refl R (LocalizedModule S M))

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
e : LocalizedModule S M →ₗ[R] LocalizedModule S M
left✝ : e ∘ₗ f = f
univ : ∀ (y : LocalizedModule S M →ₗ[R] LocalizedModule S M), (fun l => l ∘ₗ f = f) y → y = e
⊢ e = ↑(LinearEquiv.refl R (LocalizedModule S M))

Tactic:
exact Eq.symm <| univ (refl R (LocalizedModule S M)) (by simp)

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
⊢ iso S (mkLinearMap S M) = LinearEquiv.refl R (LocalizedModule S M)

Tactic:
obtain ⟨e, _, univ⟩ := is_universal S f f (map_units f)

Result:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
e : LocalizedModule S M →ₗ[R] LocalizedModule S M
left✝ : e ∘ₗ f = f
univ : ∀ (y : LocalizedModule S M →ₗ[R] LocalizedModule S M), (fun l => l ∘ₗ f = f) y → y = e
⊢ iso S (mkLinearMap S M) = LinearEquiv.refl R (LocalizedModule S M)

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
e : LocalizedModule S M →ₗ[R] LocalizedModule S M
left✝ : e ∘ₗ f = f
univ : ∀ (y : LocalizedModule S M →ₗ[R] LocalizedModule S M), (fun l => l ∘ₗ f = f) y → y = e
⊢ iso S (mkLinearMap S M) = LinearEquiv.refl R (LocalizedModule S M)

Tactic:
rw [← toLinearMap_inj, univ (iso S f) ((eq_toLinearMap_symm_comp f f).1 (iso_symm_comp S f).symm)]

Result:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
e : LocalizedModule S M →ₗ[R] LocalizedModule S M
left✝ : e ∘ₗ f = f
univ : ∀ (y : LocalizedModule S M →ₗ[R] LocalizedModule S M), (fun l => l ∘ₗ f = f) y → y = e
⊢ e = ↑(LinearEquiv.refl R (LocalizedModule S M))