awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
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 : Nontrivial R
b : Basis (Fin (finrank R M)) R M := finBasis R M
inr :
  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)
        (Matrix.det (n := Fin (finrank R M))
          ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f)) :
      S)
inr₁ :
  Eq.{u_7 + 1} (α := S)
    (Matrix.det (n := Fin (finrank R M))
        ((toMatrix (basis b j) (basis b j) : (a : P →ₗ[S] P) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) S)
          ((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f)) :
      S)
    ((algebraMap R S : (a : R) → S)
        (Matrix.det (n := Fin (finrank R M))
          ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f)) :
      S)
inr₂ :
  Eq.{u_7 + 1} (α := S)
    (Matrix.det (n := Fin (finrank R M))
        (Matrix.map.{u_6, u_7, 0, 0} (α := R)
          ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f)
          (⇑(algebraMap R S) : (a : R) → S)) :
      S)
    ((algebraMap R S : (a : R) → S)
        (Matrix.det (n := Fin (finrank R M))
          ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f)) :
      S)
inr₃ :
  Eq.{u_7 + 1} (α := S)
    (Matrix.det (n := Fin (finrank R M))
        (((RingHom.mapMatrix (algebraMap R S) :
              RingHom.{u_6, u_7} (Matrix (Fin (finrank R M)) (Fin (finrank R M)) R)
                (Matrix (Fin (finrank R M)) (Fin (finrank R M)) S)) :
            (a : Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) S)
          ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f)) :
      S)
    ((algebraMap R S : (a : R) → S)
        (Matrix.det (n := Fin (finrank R M))
          ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f)) :
      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)
have inr₄ : Eq.{u_7 + 1} (α := S)
  ((algebraMap R S : (a : R) → S)
      (Matrix.det (n := Fin (finrank R M))
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f)) :
    S)
  ((algebraMap R S : (a : R) → S)
      (Matrix.det (n := Fin (finrank R M))
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f)) :
    S)
Tactic: rw [← f.det_toMatrix b, ← (j.endHom f).det_toMatrix (j.basis b),
    endHom_toMatrix, ← RingHom.mapMatrix_apply, ← RingHom.map_det]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
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
⊢ IsBaseChange S (f.prodMap g)
have 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')
Tactic: apply of_equiv (prodRight R _ S M N ≪≫ₗ hf.equiv.prodCongr hg.equiv)
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
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)
⊢ IsBaseChange (R := R) (M := (i : ι) → M i) (N := (i : ι) → M' i) S
    (LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i)
have 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)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
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 ι
⊢ IsBaseChange (R := R) (M := (i : ι) → M i) (N := (i : ι) → M' i) S
    (LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i)
have 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 : ι) ↦ sorry.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: apply of_equiv <| piRight R S _ M ≪≫ₗ .piCongrRight fun i ↦ (hf i).equiv
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
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
⊢ 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)
have 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 : ι) ↦ sorry.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
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
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)
⊢ IsBaseChange (R := R) (M := (i : ι) → M i) (N := (i : ι) → M' i) S
    (LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
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)
have 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 : ι) ↦ sorry.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: classical
  cases nonempty_fintype ι
  apply of_equiv <| piRight R S _ M ≪≫ₗ .piCongrRight fun i ↦ (hf i).equiv
  intro x
  ext i
  simp [equiv_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
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)
⊢ IsBaseChange (R := R) (M := (i : ι) → M i) (N := (i : ι) → M' i) S
    (LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i)
have 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 : ι) ↦ sorry.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: classical
  cases nonempty_fintype ι
  apply of_equiv <| piRight R S _ M ≪≫ₗ .piCongrRight fun i ↦ (hf i).equiv
  intro x
  ext i
  simp [equiv_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
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.prodMap g)
have rw : IsBaseChange (Localization (M := R) S) (f.prodMap g)
Tactic: rw [isLocalizedModule_iff_isBaseChange S (Localization S)]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
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
⊢ IsBaseChange (Localization (M := R) S) (f.prodMap g)
have hf : IsBaseChange (Localization (M := R) S) f
Tactic: apply IsBaseChange.prodMap
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
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
⊢ IsBaseChange (Localization (M := R) S) (f.prodMap g)
have hg : IsBaseChange (Localization (M := R) S) g
Tactic: apply IsBaseChange.prodMap
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
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)
⊢ IsLocalizedModule (M := (i : ι) → M i) (M' := (i : ι) → M' i) S
    (LinearMap.pi (φ := M') fun (i : ι) ↦ f i ∘ₗ LinearMap.proj (φ := M) i)
have 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)
Tactic: rw [isLocalizedModule_iff_isBaseChange S (Localization S)]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
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)
⊢ 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)
have hf : ∀ (i : ι), IsBaseChange (Localization (M := R) S) (f i)
Tactic: apply IsBaseChange.pi
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
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 : ι
⊢ IsBaseChange (Localization (M := R) S) (f i)
have hf : IsLocalizedModule S (f i)
Tactic: rw [← isLocalizedModule_iff_isBaseChange S]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
N : ι → Type u_4
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u_1, u_4} R (N i)
P : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (P i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (P i)
inst_7 : (i : ι) → Module.{u_2, u_5} S (P i)
inst_8 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_5} R S (P i)
ε : (i : ι) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (N i) (P i)
ibc : ∀ (i : ι), IsBaseChange S (ε i)
⊢ IsBaseChange S (lmap (M := N) (N := P) ε)
have apply : ∀ (x : ⨁ (i : ι), N i),
  Eq (α := ⨁ (i : ι), P i)
    ((((directSumRight R S S N : (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≪≫ₗ
              (congrLinearEquiv (N := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (N i)) (P := P) fun (i : ι) ↦
                  sorry.equiv :
                (⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≃ₗ[S] ⨁ (i : ι), P i) :
            (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), P i) :
          (a : S ⊗[R] ⨁ (i : ι), N i) → ⨁ (i : ι), P i)
        (1 ⊗ₜ[R] x) :
      ⨁ (i : ι), P i)
    ((lmap (M := N) (N := P) ε : (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i) x : ⨁ (i : ι), P i)
Tactic: apply of_equiv <| directSumRight R S S N ≪≫ₗ congrLinearEquiv fun i ↦ (ibc i).equiv
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
N : ι → Type u_4
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u_1, u_4} R (N i)
P : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (P i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (P i)
inst_7 : (i : ι) → Module.{u_2, u_5} S (P i)
inst_8 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_5} R S (P i)
ε : (i : ι) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (N i) (P i)
ibc : ∀ (i : ι), IsBaseChange S (ε i)
x : ⨁ (i : ι), N i
⊢ Eq (α := ⨁ (i : ι), P i)
    ((((directSumRight R S S N : (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≪≫ₗ
              (congrLinearEquiv (N := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (N i)) (P := P) fun (i : ι) ↦
                  ⋯.equiv :
                (⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≃ₗ[S] ⨁ (i : ι), P i) :
            (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), P i) :
          (a : S ⊗[R] ⨁ (i : ι), N i) → ⨁ (i : ι), P i)
        (1 ⊗ₜ[R] x) :
      ⨁ (i : ι), P i)
    ((lmap (M := N) (N := P) ε : (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i) x : ⨁ (i : ι), P i)
have w : ∀ (i : ι),
  (((((directSumRight R S S N : (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≪≫ₗ
                  (congrLinearEquiv (N := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (N i)) (P := P) fun (i : ι) ↦
                      sorry.equiv :
                    (⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≃ₗ[S] ⨁ (i : ι), P i) :
                (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), P i) :
              (a : S ⊗[R] ⨁ (i : ι), N i) → ⨁ (i : ι), P i)
            (1 ⊗ₜ[R] x) :
          ⨁ (i : ι), P i) :
        (a : ι) → P a)
      i =
    (((lmap (M := N) (N := P) ε : (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i) x : ⨁ (i : ι), P i) : (a : ι) → P a) i
Tactic: ext