Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝³⁰ : CommSemiring A
inst✝²⁹ : Algebra R A
inst✝²⁸ : IsLocalization S A
M : Type u_3
inst✝²⁷ : AddCommMonoid M
inst✝²⁶ : Module R M
M' : Type u_4
inst✝²⁵ : AddCommMonoid M'
inst✝²⁴ : Module R M'
inst✝²³ : Module A M'
inst✝²² : IsScalarTower R A M'
f : M →ₗ[R] M'
M₁ : Type ?u.45
M₂ : Type ?u.47
B : Type ?u.69
C : Type ?u.81
inst✝²¹ : AddCommMonoid M₁
inst✝²⁰ : AddCommMonoid M₂
inst✝¹⁹ : Module R M₁
inst✝¹⁸ : Module R M₂
inst✝¹⁷ : Module A M₁
inst✝¹⁶ : Module A M₂
inst✝¹⁵ : IsScalarTower R A M₁
inst✝¹⁴ : IsScalarTower R A M₂
inst✝¹³ : Semiring B
inst✝¹² : Algebra R B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : IsScalarTower R A B
inst✝⁹ : Semiring C
inst✝⁸ : Algebra R C
inst✝⁷ : Algebra A C
inst✝⁶ : IsScalarTower R A C
N : Type u_5
N' : Type u_6
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
eM : M' ≃ₗ[R] Localization S ⊗[R] M := IsLocalizedModule.linearEquiv S f ((mk R (Localization S) M) 1)
eN : N' ≃ₗ[R] Localization S ⊗[R] N := IsLocalizedModule.linearEquiv S g ((mk R (Localization S) N) 1)
x✝¹ : M
x✝ : N
⊢ f (x✝¹, x✝).1 =
    ↑eM.symm
      ((((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).1,
              ((mk R (Localization S) N)
                  ((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).2)
                (↑(AlgebraTensorModule.rid (Localization S) (Localization S) (Localization S ⊗[R] M)).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1,
                    ↑(LinearEquiv.refl R N).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).2).2).1,
          (((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).1,
              ((mk R (Localization S) N)
                  ((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).2)
                (↑(AlgebraTensorModule.rid (Localization S) (Localization S) (Localization S ⊗[R] M)).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1,
                    ↑(LinearEquiv.refl R N).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).2).2).2).1

pp: case refine_2
R : Type u_1
inst✝³¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝³⁰ : CommSemiring A
inst✝²⁹ : Algebra R A
inst✝²⁸ : IsLocalization S A
M : Type u_3
inst✝²⁷ : AddCommMonoid M
inst✝²⁶ : Module R M
M' : Type u_4
inst✝²⁵ : AddCommMonoid M'
inst✝²⁴ : Module R M'
inst✝²³ : Module A M'
inst✝²² : IsScalarTower R A M'
f : M →ₗ[R] M'
M₁ : Type ?u.45
M₂ : Type ?u.47
B : Type ?u.69
C : Type ?u.81
inst✝²¹ : AddCommMonoid M₁
inst✝²⁰ : AddCommMonoid M₂
inst✝¹⁹ : Module R M₁
inst✝¹⁸ : Module R M₂
inst✝¹⁷ : Module A M₁
inst✝¹⁶ : Module A M₂
inst✝¹⁵ : IsScalarTower R A M₁
inst✝¹⁴ : IsScalarTower R A M₂
inst✝¹³ : Semiring B
inst✝¹² : Algebra R B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : IsScalarTower R A B
inst✝⁹ : Semiring C
inst✝⁸ : Algebra R C
inst✝⁷ : Algebra A C
inst✝⁶ : IsScalarTower R A C
N : Type u_5
N' : Type u_6
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
eM : M' ≃ₗ[R] Localization S ⊗[R] M := IsLocalizedModule.linearEquiv S f ((mk R (Localization S) M) 1)
eN : N' ≃ₗ[R] Localization S ⊗[R] N := IsLocalizedModule.linearEquiv S g ((mk R (Localization S) N) 1)
x✝¹ : M
x✝ : N
⊢ g (x✝¹, x✝).2 =
    ↑eN.symm
      ((((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).1,
              ((mk R (Localization S) N)
                  ((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).2)
                (↑(AlgebraTensorModule.rid (Localization S) (Localization S) (Localization S ⊗[R] M)).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1,
                    ↑(LinearEquiv.refl R N).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).2).2).1,
          (((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).1,
              ((mk R (Localization S) N)
                  ((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).2)
                (↑(AlgebraTensorModule.rid (Localization S) (Localization S) (Localization S ⊗[R] M)).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1,
                    ↑(LinearEquiv.refl R N).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).2).2).2).2

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
inst✝³¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝³⁰ : CommSemiring A
inst✝²⁹ : Algebra R A
inst✝²⁸ : IsLocalization S A
M : Type u_3
inst✝²⁷ : AddCommMonoid M
inst✝²⁶ : Module R M
M' : Type u_4
inst✝²⁵ : AddCommMonoid M'
inst✝²⁴ : Module R M'
inst✝²³ : Module A M'
inst✝²² : IsScalarTower R A M'
f : M →ₗ[R] M'
M₁ : Type ?u.45
M₂ : Type ?u.47
B : Type ?u.69
C : Type ?u.81
inst✝²¹ : AddCommMonoid M₁
inst✝²⁰ : AddCommMonoid M₂
inst✝¹⁹ : Module R M₁
inst✝¹⁸ : Module R M₂
inst✝¹⁷ : Module A M₁
inst✝¹⁶ : Module A M₂
inst✝¹⁵ : IsScalarTower R A M₁
inst✝¹⁴ : IsScalarTower R A M₂
inst✝¹³ : Semiring B
inst✝¹² : Algebra R B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : IsScalarTower R A B
inst✝⁹ : Semiring C
inst✝⁸ : Algebra R C
inst✝⁷ : Algebra A C
inst✝⁶ : IsScalarTower R A C
N : Type u_5
N' : Type u_6
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
eM : M' ≃ₗ[R] Localization S ⊗[R] M := IsLocalizedModule.linearEquiv S f ((mk R (Localization S) M) 1)
eN : N' ≃ₗ[R] Localization S ⊗[R] N := IsLocalizedModule.linearEquiv S g ((mk R (Localization S) N) 1)
x✝¹ : M
x✝ : N
⊢ f (x✝¹, x✝).1 =
    ↑eM.symm
      ((((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).1,
              ((mk R (Localization S) N)
                  ((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).2)
                (↑(AlgebraTensorModule.rid (Localization S) (Localization S) (Localization S ⊗[R] M)).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1,
                    ↑(LinearEquiv.refl R N).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).2).2).1,
          (((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).1,
              ((mk R (Localization S) N)
                  ((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).2)
                (↑(AlgebraTensorModule.rid (Localization S) (Localization S) (Localization S ⊗[R] M)).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1,
                    ↑(LinearEquiv.refl R N).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).2).2).2).1

case refine_2
R : Type u_1
inst✝³¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝³⁰ : CommSemiring A
inst✝²⁹ : Algebra R A
inst✝²⁸ : IsLocalization S A
M : Type u_3
inst✝²⁷ : AddCommMonoid M
inst✝²⁶ : Module R M
M' : Type u_4
inst✝²⁵ : AddCommMonoid M'
inst✝²⁴ : Module R M'
inst✝²³ : Module A M'
inst✝²² : IsScalarTower R A M'
f : M →ₗ[R] M'
M₁ : Type ?u.45
M₂ : Type ?u.47
B : Type ?u.69
C : Type ?u.81
inst✝²¹ : AddCommMonoid M₁
inst✝²⁰ : AddCommMonoid M₂
inst✝¹⁹ : Module R M₁
inst✝¹⁸ : Module R M₂
inst✝¹⁷ : Module A M₁
inst✝¹⁶ : Module A M₂
inst✝¹⁵ : IsScalarTower R A M₁
inst✝¹⁴ : IsScalarTower R A M₂
inst✝¹³ : Semiring B
inst✝¹² : Algebra R B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : IsScalarTower R A B
inst✝⁹ : Semiring C
inst✝⁸ : Algebra R C
inst✝⁷ : Algebra A C
inst✝⁶ : IsScalarTower R A C
N : Type u_5
N' : Type u_6
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
eM : M' ≃ₗ[R] Localization S ⊗[R] M := IsLocalizedModule.linearEquiv S f ((mk R (Localization S) M) 1)
eN : N' ≃ₗ[R] Localization S ⊗[R] N := IsLocalizedModule.linearEquiv S g ((mk R (Localization S) N) 1)
x✝¹ : M
x✝ : N
⊢ g (x✝¹, x✝).2 =
    ↑eN.symm
      ((((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).1,
              ((mk R (Localization S) N)
                  ((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).2)
                (↑(AlgebraTensorModule.rid (Localization S) (Localization S) (Localization S ⊗[R] M)).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1,
                    ↑(LinearEquiv.refl R N).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).2).2).1,
          (((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).1,
              ((mk R (Localization S) N)
                  ((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).2)
                (↑(AlgebraTensorModule.rid (Localization S) (Localization S) (Localization S ⊗[R] M)).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1,
                    ↑(LinearEquiv.refl R N).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).2).2).2).2