-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
lemma map_iso_commute (g : M₀ →ₗ[R] M₁) : (map S f₀ f₁) g ∘ₗ (iso S f₀) =
    (iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g

Proof state:
case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
x : LocalizedModule S M₀
m : M₀
s : ↥S
⊢ ((algebraMap R (Module.End R M₁')) ↑s) (((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m s)) =
    ((algebraMap R (Module.End R M₁')) ↑s)
      ((↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s))

Tactic:
repeat rw [Module.algebraMap_end_apply, ← CompatibleSMul.map_smul, smul'_mk, ← mk_smul, mk_cancel]

Result:
case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
x : LocalizedModule S M₀
m : M₀
s : ↥S
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m 1) =
    (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m 1)

Proof state:
case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
x : LocalizedModule S M₀
m : M₀
s : ↥S
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m 1) =
    (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m 1)

Tactic:
simp

Result:
case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
x : LocalizedModule S M₀
m : M₀
s : ↥S
⊢ f₁ (g m) = (iso S f₁) (((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m 1))

Proof state:
case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
x : LocalizedModule S M₀
m : M₀
s : ↥S
⊢ f₁ (g m) = (iso S f₁) (((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m 1))

Tactic:
simp [map, lift, iso_localizedModule_eq_refl, lift_mk]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
x : LocalizedModule S M₀
m : M₀
s : ↥S
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m 1) =
    ((algebraMap R (Module.End R M₁')) ↑s)
      ((↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s))

Tactic:
rw [Module.algebraMap_end_apply, ← CompatibleSMul.map_smul, smul'_mk, ← mk_smul, mk_cancel]

Result:
case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
x : LocalizedModule S M₀
m : M₀
s : ↥S
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m 1) =
    (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m 1)

Proof state:
case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
x : LocalizedModule S M₀
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) x = (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) x

Tactic:
refine induction_on (fun m s ↦ ((Module.End_isUnit_iff _).1 (map_units f₁ s)).1 ?_) x

Result:
case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
x : LocalizedModule S M₀
m : M₀
s : ↥S
⊢ ((algebraMap R (Module.End R M₁')) ↑s) (((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m s)) =
    ((algebraMap R (Module.End R M₁')) ↑s)
      ((↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s))

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
⊢ (map S f₀ f₁) g ∘ₗ ↑(iso S f₀) = ↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
x : LocalizedModule S M₀
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) x = (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) x