awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_6
inst : CommRing R
S : Type u_7
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_8
inst_3 : AddCommGroup M
inst_4 : Module R M
P : Type u_9
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : Module S P
inst_8 : IsScalarTower R S P
inst_9 : Free R M
inst_10 : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
inl :
  ∀ (hR : Subsingleton R),
    Eq.{u_7 + 1} (α := S)
      ((LinearMap.det : (a : P →ₗ[S] P) → S) ((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f : P →ₗ[S] P) : S)
      ((algebraMap R S : (a : R) → S) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) : S)
inr :
  ∀ (hR : Nontrivial R),
    Eq.{u_7 + 1} (α := S)
      ((LinearMap.det : (a : P →ₗ[S] P) → S) ((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f : P →ₗ[S] P) : S)
      ((algebraMap R S : (a : R) → S) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) : S)
⊢ Eq.{u_7 + 1} (α := S)
    ((LinearMap.det : (a : P →ₗ[S] P) → S) ((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f : P →ₗ[S] P) : S)
    ((algebraMap R S : (a : R) → S) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) : S)

Tactic:
rcases subsingleton_or_nontrivial R with hR | hR

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_6
inst : CommRing R
S : Type u_7
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_8
inst_3 : AddCommGroup M
inst_4 : Module R M
P : Type u_9
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : Module S P
inst_8 : IsScalarTower R S P
inst_9 : Free R M
inst_10 : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
hR : Subsingleton R
⊢ Subsingleton M

Tactic:
have : Subsingleton M := Module.subsingleton R M
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_6
inst : CommRing R
S : Type u_7
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_8
inst_3 : AddCommGroup M
inst_4 : Module R M
P : Type u_9
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : Module S P
inst_8 : IsScalarTower R S P
inst_9 : Free R M
inst_10 : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
hR : Subsingleton R
this : Subsingleton M
⊢ f = 1

Tactic:
Subsingleton.eq_one f

Premises used: Subsingleton.eq_one
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_6
inst : CommRing R
S : Type u_7
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_8
inst_3 : AddCommGroup M
inst_4 : Module R M
P : Type u_9
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : Module S P
inst_8 : IsScalarTower R S P
inst_9 : Free R M
inst_10 : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
hR : Subsingleton R
this : Subsingleton M
⊢ f = 1

Tactic:
exact Subsingleton.eq_one f

Premises used: Subsingleton.eq_one
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_6
inst : CommRing R
S : Type u_7
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_8
inst_3 : AddCommGroup M
inst_4 : Module R M
P : Type u_9
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : Module S P
inst_8 : IsScalarTower R S P
inst_9 : Free R M
inst_10 : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
hR : Subsingleton R
⊢ f = 1

Tactic:
have : f = 1 := by
      have : Subsingleton M := Module.subsingleton R M
      exact Subsingleton.eq_one f
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_6
inst : CommRing R
S : Type u_7
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_8
inst_3 : AddCommGroup M
inst_4 : Module R M
P : Type u_9
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : Module S P
inst_8 : IsScalarTower R S P
inst_9 : Free R M
inst_10 : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
hR : Subsingleton R
this : f = 1
⊢ Eq.{u_7 + 1} (α := S)
    ((LinearMap.det : (a : P →ₗ[S] P) → S) ((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f : P →ₗ[S] P) : S)
    ((algebraMap R S : (a : R) → S) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) : S)

Tactic:
simp [this, endHom_one]

Premises used: IsBaseChange.endHom_one
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : AddCommMonoid M'
inst_8 : AddCommMonoid N'
inst_9 : Module R M'
inst_10 : Module R N'
inst_11 : Module S M'
inst_12 : Module S N'
inst_13 : IsScalarTower R S M'
inst_14 : IsScalarTower R S N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
hf : IsBaseChange S f
hg : IsBaseChange S g
apply :
  ∀ (x : M × N),
    Eq (α := M' × N')
      (((prodRight R S S M N ≪≫ₗ hf.equiv.prodCongr hg.equiv : S ⊗[R] (M × N) ≃ₗ[S] M' × N') :
            (a : S ⊗[R] (M × N)) → M' × N')
          (1 ⊗ₜ[R] x) :
        M' × N')
      ((f.prodMap g : (a : M × N) → M' × N') x : M' × N')
⊢ IsBaseChange S (f.prodMap g)

Tactic:
apply of_equiv (prodRight R _ S M N ≪≫ₗ hf.equiv.prodCongr hg.equiv)

Premises used: LinearEquiv.prodCongr, TensorProduct.prodRight, IsBaseChange.of_equiv, LinearEquiv.trans, IsBaseChange.equiv
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : AddCommMonoid M'
inst_8 : AddCommMonoid N'
inst_9 : Module R M'
inst_10 : Module R N'
inst_11 : Module S M'
inst_12 : Module S N'
inst_13 : IsScalarTower R S M'
inst_14 : IsScalarTower R S N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
hf : IsBaseChange S f
hg : IsBaseChange S g
p : M × N
⊢ Eq (α := M' × N')
    (((prodRight R S S M N ≪≫ₗ hf.equiv.prodCongr hg.equiv : S ⊗[R] (M × N) ≃ₗ[S] M' × N') :
          (a : S ⊗[R] (M × N)) → M' × N')
        (1 ⊗ₜ[R] p) :
      M' × N')
    ((f.prodMap g : (a : M × N) → M' × N') p : M' × N')

Tactic:
simp [equiv_tmul]

Premises used: IsBaseChange.equiv_tmul
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
inst_3 : Finite ι
M : ι → Type u_4
M' : ι → Type u_5
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → AddCommMonoid (M' i)
inst_6 : (i : ι) → Module.{u_1, u_4} R (M i)
inst_7 : (i : ι) → Module.{u_1, u_5} R (M' i)
inst_8 : (i : ι) → Module.{u_2, u_5} S (M' i)
inst_9 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_5} R S (M' i)
f : (i : ι) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (M i) (M' i)
hf : ∀ (i : ι), IsBaseChange S (f i)
intro :
  ∀ (val : Fintype ι),
    IsBaseChange (R := R) (M := (i : ι) → M i) (N := (i : ι) → M' i) S
      (LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i)
⊢ IsBaseChange (R := R) (M := (i : ι) → M i) (N := (i : ι) → M' i) S
    (LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
inst_3 : Finite ι
M : ι → Type u_4
M' : ι → Type u_5
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → AddCommMonoid (M' i)
inst_6 : (i : ι) → Module.{u_1, u_4} R (M i)
inst_7 : (i : ι) → Module.{u_1, u_5} R (M' i)
inst_8 : (i : ι) → Module.{u_2, u_5} S (M' i)
inst_9 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_5} R S (M' i)
f : (i : ι) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (M i) (M' i)
hf : ∀ (i : ι), IsBaseChange S (f i)
val : Fintype ι
intro :
  ∀ (x : (i : ι) → M i),
    Eq (α := (i : ι) → M' i)
      ((((piRight R S S M : S ⊗[R] ((i : ι) → M i) ≃ₗ[S] (i : ι) → TensorProduct.{u_1, u_2, u_4} R S (M i)) ≪≫ₗ
                (LinearEquiv.piCongrRight (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (M i)) (ψ := M')
                    fun (i : ι) ↦ ⋯.equiv :
                  ((i : ι) → TensorProduct.{u_1, u_2, u_4} R S (M i)) ≃ₗ[S] (i : ι) → M' i) :
              S ⊗[R] ((i : ι) → M i) ≃ₗ[S] (i : ι) → M' i) :
            (a : S ⊗[R] ((i : ι) → M i)) → (i : ι) → M' i)
          (1 ⊗ₜ[R] x) :
        (i : ι) → M' i)
      ((LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i : (a : (i : ι) → M i) → (i : ι) → M' i)
          x :
        (i : ι) → M' i)
⊢ IsBaseChange (R := R) (M := (i : ι) → M i) (N := (i : ι) → M' i) S
    (LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i)

Tactic:
apply of_equiv <| piRight R S _ M ≪≫ₗ .piCongrRight fun i ↦ (hf i).equiv

Premises used: IsBaseChange.of_equiv, TensorProduct.piRight
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
inst_3 : Finite ι
M : ι → Type u_4
M' : ι → Type u_5
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → AddCommMonoid (M' i)
inst_6 : (i : ι) → Module.{u_1, u_4} R (M i)
inst_7 : (i : ι) → Module.{u_1, u_5} R (M' i)
inst_8 : (i : ι) → Module.{u_2, u_5} S (M' i)
inst_9 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_5} R S (M' i)
f : (i : ι) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (M i) (M' i)
hf : ∀ (i : ι), IsBaseChange S (f i)
val : Fintype ι
x : (i : ι) → M i
intro :
  ∀ (i : ι),
    Eq.{u_5 + 1} (α := M' i)
      ((((piRight R S S M : S ⊗[R] ((i : ι) → M i) ≃ₗ[S] (i : ι) → TensorProduct.{u_1, u_2, u_4} R S (M i)) ≪≫ₗ
                (LinearEquiv.piCongrRight (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (M i)) (ψ := M')
                    fun (i : ι) ↦ ⋯.equiv :
                  ((i : ι) → TensorProduct.{u_1, u_2, u_4} R S (M i)) ≃ₗ[S] (i : ι) → M' i) :
              S ⊗[R] ((i : ι) → M i) ≃ₗ[S] (i : ι) → M' i) :
            (a : S ⊗[R] ((i : ι) → M i)) → (i : ι) → M' i)
          (1 ⊗ₜ[R] x) i :
        M' i)
      ((LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i : (a : (i : ι) → M i) → (i : ι) → M' i) x
          i :
        M' i)
⊢ Eq (α := (i : ι) → M' i)
    ((((piRight R S S M : S ⊗[R] ((i : ι) → M i) ≃ₗ[S] (i : ι) → TensorProduct.{u_1, u_2, u_4} R S (M i)) ≪≫ₗ
              (LinearEquiv.piCongrRight (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (M i)) (ψ := M')
                  fun (i : ι) ↦ ⋯.equiv :
                ((i : ι) → TensorProduct.{u_1, u_2, u_4} R S (M i)) ≃ₗ[S] (i : ι) → M' i) :
            S ⊗[R] ((i : ι) → M i) ≃ₗ[S] (i : ι) → M' i) :
          (a : S ⊗[R] ((i : ι) → M i)) → (i : ι) → M' i)
        (1 ⊗ₜ[R] x) :
      (i : ι) → M' i)
    ((LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i : (a : (i : ι) → M i) → (i : ι) → M' i) x :
      (i : ι) → M' i)

Tactic:
ext i
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
inst_3 : Finite ι
M : ι → Type u_4
M' : ι → Type u_5
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → AddCommMonoid (M' i)
inst_6 : (i : ι) → Module.{u_1, u_4} R (M i)
inst_7 : (i : ι) → Module.{u_1, u_5} R (M' i)
inst_8 : (i : ι) → Module.{u_2, u_5} S (M' i)
inst_9 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_5} R S (M' i)
f : (i : ι) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (M i) (M' i)
hf : ∀ (i : ι), IsBaseChange S (f i)
val : Fintype ι
x : (i : ι) → M i
i : ι
⊢ Eq.{u_5 + 1} (α := M' i)
    ((((piRight R S S M : S ⊗[R] ((i : ι) → M i) ≃ₗ[S] (i : ι) → TensorProduct.{u_1, u_2, u_4} R S (M i)) ≪≫ₗ
              (LinearEquiv.piCongrRight (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (M i)) (ψ := M')
                  fun (i : ι) ↦ ⋯.equiv :
                ((i : ι) → TensorProduct.{u_1, u_2, u_4} R S (M i)) ≃ₗ[S] (i : ι) → M' i) :
            S ⊗[R] ((i : ι) → M i) ≃ₗ[S] (i : ι) → M' i) :
          (a : S ⊗[R] ((i : ι) → M i)) → (i : ι) → M' i)
        (1 ⊗ₜ[R] x) i :
      M' i)
    ((LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i : (a : (i : ι) → M i) → (i : ι) → M' i) x
        i :
      M' i)

Tactic:
simp [equiv_tmul]

Premises used: IsBaseChange.equiv_tmul
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
inst_3 : Finite ι
M : ι → Type u_4
M' : ι → Type u_5
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → AddCommMonoid (M' i)
inst_6 : (i : ι) → Module.{u_1, u_4} R (M i)
inst_7 : (i : ι) → Module.{u_1, u_5} R (M' i)
inst_8 : (i : ι) → Module.{u_2, u_5} S (M' i)
inst_9 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_5} R S (M' i)
f : (i : ι) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (M i) (M' i)
hf : ∀ (i : ι), IsBaseChange S (f i)
intro :
  ∀ (val : Fintype ι),
    IsBaseChange (R := R) (M := (i : ι) → M i) (N := (i : ι) → M' i) S
      (LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i)
intro₁ intro₂ :
  ∀ (val : Fintype ι) (x : (i : ι) → M i),
    Eq (α := (i : ι) → M' i)
      ((((piRight R S S M : S ⊗[R] ((i : ι) → M i) ≃ₗ[S] (i : ι) → TensorProduct.{u_1, u_2, u_4} R S (M i)) ≪≫ₗ
                (LinearEquiv.piCongrRight (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (M i)) (ψ := M')
                    fun (i : ι) ↦ ⋯.equiv :
                  ((i : ι) → TensorProduct.{u_1, u_2, u_4} R S (M i)) ≃ₗ[S] (i : ι) → M' i) :
              S ⊗[R] ((i : ι) → M i) ≃ₗ[S] (i : ι) → M' i) :
            (a : S ⊗[R] ((i : ι) → M i)) → (i : ι) → M' i)
          (1 ⊗ₜ[R] x) :
        (i : ι) → M' i)
      ((LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i : (a : (i : ι) → M i) → (i : ι) → M' i)
          x :
        (i : ι) → M' i)
intro₃ :
  ∀ (val : Fintype ι) (x : (i : ι) → M i) (i : ι),
    Eq.{u_5 + 1} (α := M' i)
      ((((piRight R S S M : S ⊗[R] ((i : ι) → M i) ≃ₗ[S] (i : ι) → TensorProduct.{u_1, u_2, u_4} R S (M i)) ≪≫ₗ
                (LinearEquiv.piCongrRight (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (M i)) (ψ := M')
                    fun (i : ι) ↦ ⋯.equiv :
                  ((i : ι) → TensorProduct.{u_1, u_2, u_4} R S (M i)) ≃ₗ[S] (i : ι) → M' i) :
              S ⊗[R] ((i : ι) → M i) ≃ₗ[S] (i : ι) → M' i) :
            (a : S ⊗[R] ((i : ι) → M i)) → (i : ι) → M' i)
          (1 ⊗ₜ[R] x) i :
        M' i)
      ((LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i : (a : (i : ι) → M i) → (i : ι) → M' i) x
          i :
        M' i)
⊢ IsBaseChange (R := R) (M := (i : ι) → M i) (N := (i : ι) → M' i) S
    (LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i)

Tactic:
classical
  cases nonempty_fintype ι
  apply of_equiv <| piRight R S _ M ≪≫ₗ .piCongrRight fun i ↦ (hf i).equiv
  intro x
  ext i
  simp [equiv_tmul]

Premises used: IsBaseChange.of_equiv, nonempty_fintype, IsBaseChange.equiv_tmul
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
inst_3 : Finite ι
M : Type u_4
M' : Type u_5
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid M'
inst_6 : Module R M
inst_7 : Module R M'
inst_8 : Module S M'
inst_9 : IsScalarTower R S M'
f : M →ₗ[R] M'
hf : IsBaseChange S f
⊢ IsBaseChange S (f.compLeft ι)

Tactic:
IsBaseChange.pi (f := fun _ ↦ f) (fun _ ↦ hf)

Premises used: IsBaseChange.pi, LinearMap.pi, LinearMap.compLeft
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S_1
inst_2 : Algebra R S_1
S : Submonoid R
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : AddCommMonoid M'
inst_8 : AddCommMonoid N'
inst_9 : Module R M'
inst_10 : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
inst_11 : IsLocalizedModule S f
inst_12 : IsLocalizedModule S g
this_1 : Module.{u_1, u_5} (Localization (M := R) S) M' := module S f
this : Module.{u_1, u_6} (Localization (M := R) S) N' := module S g
rw : IsBaseChange (Localization (M := R) S) (f.prodMap g)
⊢ IsLocalizedModule S (f.prodMap g)

Tactic:
rw [isLocalizedModule_iff_isBaseChange S (Localization S)]

Premises used: isLocalizedModule_iff_isBaseChange, Localization
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S_1
inst_2 : Algebra R S_1
S : Submonoid R
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : AddCommMonoid M'
inst_8 : AddCommMonoid N'
inst_9 : Module R M'
inst_10 : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
inst_11 : IsLocalizedModule S f
inst_12 : IsLocalizedModule S g
this_1 : Module.{u_1, u_5} (Localization (M := R) S) M' := module S f
this : Module.{u_1, u_6} (Localization (M := R) S) N' := module S g
hf : IsBaseChange (Localization (M := R) S) f
hg : IsBaseChange (Localization (M := R) S) g
⊢ IsBaseChange (Localization (M := R) S) (f.prodMap g)

Tactic:
apply IsBaseChange.prodMap

Premises used: IsBaseChange.prodMap
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S_1
inst_2 : Algebra R S_1
S : Submonoid R
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : AddCommMonoid M'
inst_8 : AddCommMonoid N'
inst_9 : Module R M'
inst_10 : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
inst_11 : IsLocalizedModule S f
inst_12 : IsLocalizedModule S g
this_1 : Module.{u_1, u_5} (Localization (M := R) S) M' := module S f
this : Module.{u_1, u_6} (Localization (M := R) S) N' := module S g
hf : IsLocalizedModule S f
⊢ IsBaseChange (Localization (M := R) S) f

Tactic:
rw [← isLocalizedModule_iff_isBaseChange S]

Premises used: isLocalizedModule_iff_isBaseChange
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S_1
inst_2 : Algebra R S_1
S : Submonoid R
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : AddCommMonoid M'
inst_8 : AddCommMonoid N'
inst_9 : Module R M'
inst_10 : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
inst_11 : IsLocalizedModule S f
inst_12 : IsLocalizedModule S g
this_1 : Module.{u_1, u_5} (Localization (M := R) S) M' := module S f
this : Module.{u_1, u_6} (Localization (M := R) S) N' := module S g
⊢ IsLocalizedModule S f

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S_1
inst_2 : Algebra R S_1
S : Submonoid R
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : AddCommMonoid M'
inst_8 : AddCommMonoid N'
inst_9 : Module R M'
inst_10 : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
inst_11 : IsLocalizedModule S f
inst_12 : IsLocalizedModule S g
this_1 : Module.{u_1, u_5} (Localization (M := R) S) M' := module S f
this : Module.{u_1, u_6} (Localization (M := R) S) N' := module S g
hg : IsLocalizedModule S g
⊢ IsBaseChange (Localization (M := R) S) g

Tactic:
rw [← isLocalizedModule_iff_isBaseChange S]

Premises used: isLocalizedModule_iff_isBaseChange
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S_1
inst_2 : Algebra R S_1
S : Submonoid R
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : AddCommMonoid M'
inst_8 : AddCommMonoid N'
inst_9 : Module R M'
inst_10 : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
inst_11 : IsLocalizedModule S f
inst_12 : IsLocalizedModule S g
this_1 : Module.{u_1, u_5} (Localization (M := R) S) M' := module S f
this : Module.{u_1, u_6} (Localization (M := R) S) N' := module S g
⊢ IsLocalizedModule S g

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S_1
inst_2 : Algebra R S_1
S : Submonoid R
ι : Type u_3
inst_3 : Finite ι
M : ι → Type u_4
M' : ι → Type u_5
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → AddCommMonoid (M' i)
inst_6 : (i : ι) → Module.{u_1, u_4} R (M i)
inst_7 : (i : ι) → Module.{u_1, u_5} R (M' i)
f : (i : ι) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (M i) (M' i)
inst_8 : ∀ (i : ι), IsLocalizedModule S (f i)
this : (i : ι) → Module.{u_1, u_5} (Localization (M := R) S) (M' i) := fun (i : ι) ↦ module S (f i)
rw :
  IsBaseChange (R := R) (M := (i : ι) → M i) (N := (i : ι) → M' i) (Localization (M := R) S)
    (LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i)
⊢ IsLocalizedModule (M := (i : ι) → M i) (M' := (i : ι) → M' i) S
    (LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i)

Tactic:
rw [isLocalizedModule_iff_isBaseChange S (Localization S)]

Premises used: isLocalizedModule_iff_isBaseChange, Localization
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S_1
inst_2 : Algebra R S_1
S : Submonoid R
ι : Type u_3
inst_3 : Finite ι
M : ι → Type u_4
M' : ι → Type u_5
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → AddCommMonoid (M' i)
inst_6 : (i : ι) → Module.{u_1, u_4} R (M i)
inst_7 : (i : ι) → Module.{u_1, u_5} R (M' i)
f : (i : ι) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (M i) (M' i)
inst_8 : ∀ (i : ι), IsLocalizedModule S (f i)
this : (i : ι) → Module.{u_1, u_5} (Localization (M := R) S) (M' i) := fun (i : ι) ↦ module S (f i)
hf : ∀ (i : ι), IsBaseChange (Localization (M := R) S) (f i)
⊢ IsBaseChange (R := R) (M := (i : ι) → M i) (N := (i : ι) → M' i) (Localization (M := R) S)
    (LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i)

Tactic:
apply IsBaseChange.pi

Premises used: IsBaseChange.pi
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S_1
inst_2 : Algebra R S_1
S : Submonoid R
ι : Type u_3
inst_3 : Finite ι
M : ι → Type u_4
M' : ι → Type u_5
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → AddCommMonoid (M' i)
inst_6 : (i : ι) → Module.{u_1, u_4} R (M i)
inst_7 : (i : ι) → Module.{u_1, u_5} R (M' i)
f : (i : ι) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (M i) (M' i)
inst_8 : ∀ (i : ι), IsLocalizedModule S (f i)
this : (i : ι) → Module.{u_1, u_5} (Localization (M := R) S) (M' i) := fun (i : ι) ↦ module S (f i)
i : ι
hf : IsLocalizedModule S (f i)
⊢ IsBaseChange (Localization (M := R) S) (f i)

Tactic:
rw [← isLocalizedModule_iff_isBaseChange S]

Premises used: isLocalizedModule_iff_isBaseChange
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S_1
inst_2 : Algebra R S_1
S : Submonoid R
ι : Type u_3
inst_3 : Finite ι
M : ι → Type u_4
M' : ι → Type u_5
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → AddCommMonoid (M' i)
inst_6 : (i : ι) → Module.{u_1, u_4} R (M i)
inst_7 : (i : ι) → Module.{u_1, u_5} R (M' i)
f : (i : ι) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (M i) (M' i)
inst_8 : ∀ (i : ι), IsLocalizedModule S (f i)
this : (i : ι) → Module.{u_1, u_5} (Localization (M := R) S) (M' i) := fun (i : ι) ↦ module S (f i)
i : ι
⊢ IsLocalizedModule S (f i)

Tactic:
infer_instance