awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S P
inst_10 : IsScalarTower R S P
inst_11 : Free R M
inst_12 : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
set :
  let ι := Free.ChooseBasisIndex R M;
  ∀ (b : Basis ι R M),
    Function.Bijective (α := S ⊗[R] (M →ₗ[R] N)) (β := M →ₗ[R] P)
      (⇑(linearMapRightBaseChangeHom S M ε : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P) : (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
⊢ Function.Bijective (α := S ⊗[R] (M →ₗ[R] N)) (β := M →ₗ[R] P)
    (⇑(linearMapRightBaseChangeHom S M ε : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P) : (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)

Tactic:
set ι := Free.ChooseBasisIndex R M

Premises used: Module.Free.ChooseBasisIndex
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S P
inst_10 : IsScalarTower R S P
inst_11 : Free R M
inst_12 : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
have :
  ∀ (this : Fintype (Free.ChooseBasisIndex R M)),
    Function.Bijective (α := S ⊗[R] (M →ₗ[R] N)) (β := M →ₗ[R] P)
      (⇑(linearMapRightBaseChangeHom S M ε : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P) : (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
⊢ Function.Bijective (α := S ⊗[R] (M →ₗ[R] N)) (β := M →ₗ[R] P)
    (⇑(linearMapRightBaseChangeHom S M ε : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P) : (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)

Tactic:
have := Free.ChooseBasisIndex.fintype R M
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S P
inst_10 : IsScalarTower R S P
inst_11 : Free R M
inst_12 : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this_1 : Fintype (Free.ChooseBasisIndex R M)
e : (M →ₗ[R] N) ≃ₗ[R] ι → N := LinearEquiv.congrLeft N R b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift N R R ι)
f : (M →ₗ[R] P) ≃ₗ[S] ι → P := LinearEquiv.congrLeft P S b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift P R S ι)
h : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P := linearMapRightBaseChangeHom S M ε
e' : S ⊗[R] (M →ₗ[R] N) ≃ₗ[S] S ⊗[R] (ι → N) := LinearEquiv.baseChange R S (M →ₗ[R] N) (ι → N) e
h' : S ⊗[R] (ι → N) →ₗ[S] ι → P :=
  ((↑f : (M →ₗ[R] P) →ₗ[S] ι → P) ∘ₗ linearMapRightBaseChangeHom S M ε) ∘ₗ
    (↑e'.symm : S ⊗[R] (ι → N) →ₗ[S] S ⊗[R] (M →ₗ[R] N))
this : Function.Bijective (α := S ⊗[R] (ι → N)) (β := ι → P) (⇑h' : (a : S ⊗[R] (ι → N)) → ι → P)
⊢ Function.Bijective (α := S ⊗[R] (M →ₗ[R] N)) (β := M →ₗ[R] P)
    (⇑(linearMapRightBaseChangeHom S M ε : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P) : (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)

Tactic:
simpa [h'] using this
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S P
inst_10 : IsScalarTower R S P
inst_11 : Free R M
inst_12 : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this : Fintype (Free.ChooseBasisIndex R M)
e : (M →ₗ[R] N) ≃ₗ[R] ι → N := LinearEquiv.congrLeft N R b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift N R R ι)
f : (M →ₗ[R] P) ≃ₗ[S] ι → P := LinearEquiv.congrLeft P S b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift P R S ι)
h : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P := linearMapRightBaseChangeHom S M ε
e' : S ⊗[R] (M →ₗ[R] N) ≃ₗ[S] S ⊗[R] (ι → N) := LinearEquiv.baseChange R S (M →ₗ[R] N) (ι → N) e
h' : S ⊗[R] (ι → N) →ₗ[S] ι → P :=
  ((↑f : (M →ₗ[R] P) →ₗ[S] ι → P) ∘ₗ linearMapRightBaseChangeHom S M ε) ∘ₗ
    (↑e'.symm : S ⊗[R] (ι → N) →ₗ[S] S ⊗[R] (M →ₗ[R] N))
suffices : Function.Bijective (α := S ⊗[R] (ι → N)) (β := ι → P) (⇑h' : (a : S ⊗[R] (ι → N)) → ι → P)
⊢ Function.Bijective (α := S ⊗[R] (M →ₗ[R] N)) (β := M →ₗ[R] P)
    (⇑(linearMapRightBaseChangeHom S M ε : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P) : (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)

Tactic:
suffices Function.Bijective h' by simpa [h'] using this
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S P
inst_10 : IsScalarTower R S P
inst_11 : Free R M
inst_12 : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this_1 : Fintype (Free.ChooseBasisIndex R M)
e : (M →ₗ[R] N) ≃ₗ[R] ι → N := LinearEquiv.congrLeft N R b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift N R R ι)
f : (M →ₗ[R] P) ≃ₗ[S] ι → P := LinearEquiv.congrLeft P S b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift P R S ι)
h : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P := linearMapRightBaseChangeHom S M ε
e' : S ⊗[R] (M →ₗ[R] N) ≃ₗ[S] S ⊗[R] (ι → N) := LinearEquiv.baseChange R S (M →ₗ[R] N) (ι → N) e
h' : S ⊗[R] (ι → N) →ₗ[S] ι → P :=
  ((↑f : (M →ₗ[R] P) →ₗ[S] ι → P) ∘ₗ linearMapRightBaseChangeHom S M ε) ∘ₗ
    (↑e'.symm : S ⊗[R] (ι → N) →ₗ[S] S ⊗[R] (M →ₗ[R] N))
this : h' = (↑⋯.equiv : S ⊗[R] (ι → N) →ₗ[S] ι → P)
simp :
  Function.Bijective (α := S ⊗[R] (ι → N)) (β := ι → P)
    (⇑(↑⋯.equiv : S ⊗[R] (ι → N) →ₗ[S] ι → P) : (a : S ⊗[R] (ι → N)) → ι → P)
⊢ Function.Bijective (α := S ⊗[R] (ι → N)) (β := ι → P) (⇑h' : (a : S ⊗[R] (ι → N)) → ι → P)

Tactic:
simp only [this]
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S P
inst_10 : IsScalarTower R S P
inst_11 : Free R M
inst_12 : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this_1 : Fintype (Free.ChooseBasisIndex R M)
e : (M →ₗ[R] N) ≃ₗ[R] ι → N := LinearEquiv.congrLeft N R b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift N R R ι)
f : (M →ₗ[R] P) ≃ₗ[S] ι → P := LinearEquiv.congrLeft P S b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift P R S ι)
h : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P := linearMapRightBaseChangeHom S M ε
e' : S ⊗[R] (M →ₗ[R] N) ≃ₗ[S] S ⊗[R] (ι → N) := LinearEquiv.baseChange R S (M →ₗ[R] N) (ι → N) e
h' : S ⊗[R] (ι → N) →ₗ[S] ι → P :=
  ((↑f : (M →ₗ[R] P) →ₗ[S] ι → P) ∘ₗ linearMapRightBaseChangeHom S M ε) ∘ₗ
    (↑e'.symm : S ⊗[R] (ι → N) →ₗ[S] S ⊗[R] (M →ₗ[R] N))
this : h' = (↑⋯.equiv : S ⊗[R] (ι → N) →ₗ[S] ι → P)
⊢ Function.Bijective (α := S ⊗[R] (ι → N)) (β := ι → P)
    (⇑(↑⋯.equiv : S ⊗[R] (ι → N) →ₗ[S] ι → P) : (a : S ⊗[R] (ι → N)) → ι → P)

Tactic:
apply LinearEquiv.bijective

Premises used: LinearEquiv.bijective
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S P
inst_10 : IsScalarTower R S P
inst_11 : Free R M
inst_12 : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this : Fintype (Free.ChooseBasisIndex R M)
e : (M →ₗ[R] N) ≃ₗ[R] ι → N := LinearEquiv.congrLeft N R b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift N R R ι)
f : (M →ₗ[R] P) ≃ₗ[S] ι → P := LinearEquiv.congrLeft P S b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift P R S ι)
h : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P := linearMapRightBaseChangeHom S M ε
e' : S ⊗[R] (M →ₗ[R] N) ≃ₗ[S] S ⊗[R] (ι → N) := LinearEquiv.baseChange R S (M →ₗ[R] N) (ι → N) e
h' : S ⊗[R] (ι → N) →ₗ[S] ι → P :=
  ((↑f : (M →ₗ[R] P) →ₗ[S] ι → P) ∘ₗ linearMapRightBaseChangeHom S M ε) ∘ₗ
    (↑e'.symm : S ⊗[R] (ι → N) →ₗ[S] S ⊗[R] (M →ₗ[R] N))
suffices : h' = (↑⋯.equiv : S ⊗[R] (ι → N) →ₗ[S] ι → P)
⊢ Function.Bijective (α := S ⊗[R] (ι → N)) (β := ι → P) (⇑h' : (a : S ⊗[R] (ι → N)) → ι → P)

Tactic:
suffices h' = (finitePow ι ibc).equiv by
    simp only [this]
    apply LinearEquiv.bijective
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S P
inst_10 : IsScalarTower R S P
inst_11 : Free R M
inst_12 : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this_1 : Fintype (Free.ChooseBasisIndex R M)
e : (M →ₗ[R] N) ≃ₗ[R] ι → N := LinearEquiv.congrLeft N R b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift N R R ι)
f : (M →ₗ[R] P) ≃ₗ[S] ι → P := LinearEquiv.congrLeft P S b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift P R S ι)
h : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P := linearMapRightBaseChangeHom S M ε
e' : S ⊗[R] (M →ₗ[R] N) ≃ₗ[S] S ⊗[R] (ι → N) := LinearEquiv.baseChange R S (M →ₗ[R] N) (ι → N) e
h' : S ⊗[R] (ι → N) →ₗ[S] ι → P :=
  ((↑f : (M →ₗ[R] P) →ₗ[S] ι → P) ∘ₗ linearMapRightBaseChangeHom S M ε) ∘ₗ
    (↑e'.symm : S ⊗[R] (ι → N) →ₗ[S] S ⊗[R] (M →ₗ[R] N))
this :
  (↑f : (M →ₗ[R] P) →ₗ[S] ι → P) ∘ₗ linearMapRightBaseChangeHom S M ε =
    (↑⋯.equiv : S ⊗[R] (ι → N) →ₗ[S] ι → P) ∘ₗ (↑e' : S ⊗[R] (M →ₗ[R] N) →ₗ[S] S ⊗[R] (ι → N))
⊢ h' = (↑⋯.equiv : S ⊗[R] (ι → N) →ₗ[S] ι → P)

Tactic:
simp [h', this, ← LinearEquiv.trans_assoc e'.symm e']

Premises used: LinearEquiv.symm, LinearEquiv.trans_assoc
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S P
inst_10 : IsScalarTower R S P
inst_11 : Free R M
inst_12 : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this : Fintype (Free.ChooseBasisIndex R M)
e : (M →ₗ[R] N) ≃ₗ[R] ι → N := LinearEquiv.congrLeft N R b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift N R R ι)
f : (M →ₗ[R] P) ≃ₗ[S] ι → P := LinearEquiv.congrLeft P S b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift P R S ι)
h : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P := linearMapRightBaseChangeHom S M ε
e' : S ⊗[R] (M →ₗ[R] N) ≃ₗ[S] S ⊗[R] (ι → N) := LinearEquiv.baseChange R S (M →ₗ[R] N) (ι → N) e
h' : S ⊗[R] (ι → N) →ₗ[S] ι → P :=
  ((↑f : (M →ₗ[R] P) →ₗ[S] ι → P) ∘ₗ linearMapRightBaseChangeHom S M ε) ∘ₗ
    (↑e'.symm : S ⊗[R] (ι → N) →ₗ[S] S ⊗[R] (M →ₗ[R] N))
suffices :
  (↑f : (M →ₗ[R] P) →ₗ[S] ι → P) ∘ₗ linearMapRightBaseChangeHom S M ε =
    (↑⋯.equiv : S ⊗[R] (ι → N) →ₗ[S] ι → P) ∘ₗ (↑e' : S ⊗[R] (M →ₗ[R] N) →ₗ[S] S ⊗[R] (ι → N))
⊢ h' = (↑⋯.equiv : S ⊗[R] (ι → N) →ₗ[S] ι → P)

Tactic:
suffices f.toLinearMap.comp (linearMapRightBaseChangeHom S M ε) =
      (finitePow ι ibc).equiv.toLinearMap.comp e'.toLinearMap by
    simp [h', this, ← LinearEquiv.trans_assoc e'.symm e']
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S P
inst_10 : IsScalarTower R S P
inst_11 : Free R M
inst_12 : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this : Fintype (Free.ChooseBasisIndex R M)
e : (M →ₗ[R] N) ≃ₗ[R] ι → N := LinearEquiv.congrLeft N R b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift N R R ι)
f : (M →ₗ[R] P) ≃ₗ[S] ι → P := LinearEquiv.congrLeft P S b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift P R S ι)
h : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P := linearMapRightBaseChangeHom S M ε
e' : S ⊗[R] (M →ₗ[R] N) ≃ₗ[S] S ⊗[R] (ι → N) := LinearEquiv.baseChange R S (M →ₗ[R] N) (ι → N) e
h' : S ⊗[R] (ι → N) →ₗ[S] ι → P :=
  ((↑f : (M →ₗ[R] P) →ₗ[S] ι → P) ∘ₗ linearMapRightBaseChangeHom S M ε) ∘ₗ
    (↑e'.symm : S ⊗[R] (ι → N) →ₗ[S] S ⊗[R] (M →ₗ[R] N))
a :
  ∀ (φ : M →ₗ[R] N) (i : ι),
    Eq.{u_5 + 1} (α := P)
      ((((AlgebraTensorModule.curry ((↑f : (M →ₗ[R] P) →ₗ[S] ι → P) ∘ₗ linearMapRightBaseChangeHom S M ε) :
                  S →ₗ[S] (M →ₗ[R] N) →ₗ[R] ι → P) :
                (a : S) → (M →ₗ[R] N) →ₗ[R] ι → P)
              1 :
            (a : M →ₗ[R] N) → ι → P)
          φ i :
        P)
      ((((AlgebraTensorModule.curry
                    ((↑⋯.equiv : S ⊗[R] (ι → N) →ₗ[S] ι → P) ∘ₗ (↑e' : S ⊗[R] (M →ₗ[R] N) →ₗ[S] S ⊗[R] (ι → N))) :
                  S →ₗ[S] (M →ₗ[R] N) →ₗ[R] ι → P) :
                (a : S) → (M →ₗ[R] N) →ₗ[R] ι → P)
              1 :
            (a : M →ₗ[R] N) → ι → P)
          φ i :
        P)
⊢ (↑f : (M →ₗ[R] P) →ₗ[S] ι → P) ∘ₗ linearMapRightBaseChangeHom S M ε =
    (↑⋯.equiv : S ⊗[R] (ι → N) →ₗ[S] ι → P) ∘ₗ (↑e' : S ⊗[R] (M →ₗ[R] N) →ₗ[S] S ⊗[R] (ι → N))

Tactic:
ext φ i
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S P
inst_10 : IsScalarTower R S P
inst_11 : Free R M
inst_12 : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this : Fintype (Free.ChooseBasisIndex R M)
e : (M →ₗ[R] N) ≃ₗ[R] ι → N := LinearEquiv.congrLeft N R b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift N R R ι)
f : (M →ₗ[R] P) ≃ₗ[S] ι → P := LinearEquiv.congrLeft P S b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift P R S ι)
h : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P := linearMapRightBaseChangeHom S M ε
e' : S ⊗[R] (M →ₗ[R] N) ≃ₗ[S] S ⊗[R] (ι → N) := LinearEquiv.baseChange R S (M →ₗ[R] N) (ι → N) e
h' : S ⊗[R] (ι → N) →ₗ[S] ι → P :=
  ((↑f : (M →ₗ[R] P) →ₗ[S] ι → P) ∘ₗ linearMapRightBaseChangeHom S M ε) ∘ₗ
    (↑e'.symm : S ⊗[R] (ι → N) →ₗ[S] S ⊗[R] (M →ₗ[R] N))
φ : M →ₗ[R] N
i : ι
a :
  Eq.{u_5 + 1} (α := P)
    ((f : (a : M →ₗ[R] P) → ι → P)
        (((linearMapRightBaseChangeHom S M ε : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P) :
              (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
            (1 ⊗ₜ[R] φ) :
          M →ₗ[R] P)
        i :
      P)
    ((⋯.equiv : (a : S ⊗[R] (ι → N)) → ι → P)
        ((e' : (a : S ⊗[R] (M →ₗ[R] N)) → S ⊗[R] (ι → N)) (1 ⊗ₜ[R] φ) : S ⊗[R] (ι → N)) i :
      P)
⊢ Eq.{u_5 + 1} (α := P)
    ((((AlgebraTensorModule.curry ((↑f : (M →ₗ[R] P) →ₗ[S] ι → P) ∘ₗ linearMapRightBaseChangeHom S M ε) :
                S →ₗ[S] (M →ₗ[R] N) →ₗ[R] ι → P) :
              (a : S) → (M →ₗ[R] N) →ₗ[R] ι → P)
            1 :
          (a : M →ₗ[R] N) → ι → P)
        φ i :
      P)
    ((((AlgebraTensorModule.curry
                  ((↑⋯.equiv : S ⊗[R] (ι → N) →ₗ[S] ι → P) ∘ₗ (↑e' : S ⊗[R] (M →ₗ[R] N) →ₗ[S] S ⊗[R] (ι → N))) :
                S →ₗ[S] (M →ₗ[R] N) →ₗ[R] ι → P) :
              (a : S) → (M →ₗ[R] N) →ₗ[R] ι → P)
            1 :
          (a : M →ₗ[R] N) → ι → P)
        φ i :
      P)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S P
inst_10 : IsScalarTower R S P
inst_11 : Free R M
inst_12 : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this : Fintype (Free.ChooseBasisIndex R M)
e : (M →ₗ[R] N) ≃ₗ[R] ι → N := LinearEquiv.congrLeft N R b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift N R R ι)
f : (M →ₗ[R] P) ≃ₗ[S] ι → P := LinearEquiv.congrLeft P S b.repr ≪≫ₗ LinearEquiv.symm (Finsupp.llift P R S ι)
h : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P := linearMapRightBaseChangeHom S M ε
e' : S ⊗[R] (M →ₗ[R] N) ≃ₗ[S] S ⊗[R] (ι → N) := LinearEquiv.baseChange R S (M →ₗ[R] N) (ι → N) e
h' : S ⊗[R] (ι → N) →ₗ[S] ι → P :=
  ((↑f : (M →ₗ[R] P) →ₗ[S] ι → P) ∘ₗ linearMapRightBaseChangeHom S M ε) ∘ₗ
    (↑e'.symm : S ⊗[R] (ι → N) →ₗ[S] S ⊗[R] (M →ₗ[R] N))
φ : M →ₗ[R] N
i : ι
⊢ Eq.{u_5 + 1} (α := P)
    ((f : (a : M →ₗ[R] P) → ι → P)
        (((linearMapRightBaseChangeHom S M ε : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P) :
              (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
            (1 ⊗ₜ[R] φ) :
          M →ₗ[R] P)
        i :
      P)
    ((⋯.equiv : (a : S ⊗[R] (ι → N)) → ι → P)
        ((e' : (a : S ⊗[R] (M →ₗ[R] N)) → S ⊗[R] (ι → N)) (1 ⊗ₜ[R] φ) : S ⊗[R] (ι → N)) i :
      P)

Tactic:
simp [f, e', linearMapRightBaseChangeHom, LinearEquiv.baseChange, equiv_tmul,
    LinearEquiv.congrLeft, e]

Premises used: IsBaseChange.linearMapRightBaseChangeHom, LinearEquiv.baseChange, LinearEquiv.congrLeft, IsBaseChange.equiv_tmul
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S P
inst_10 : IsScalarTower R S P
inst_11 : Free R M
inst_12 : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
apply :
  ∀ (x : M →ₗ[R] N),
    Eq (α := M →ₗ[R] P)
      ((linearMapRightBaseChangeEquiv M ibc : (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P) (1 ⊗ₜ[R] x) : M →ₗ[R] P)
      ((compRight R ε : (a : M →ₗ[R] N) → M →ₗ[R] P) x : M →ₗ[R] P)
⊢ IsBaseChange (M := M →ₗ[R] N) S (compRight R ε)

Tactic:
apply of_equiv (linearMapRightBaseChangeEquiv M ibc)

Premises used: IsBaseChange.of_equiv, IsBaseChange.linearMapRightBaseChangeEquiv
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S P
inst_10 : IsScalarTower R S P
inst_11 : Free R M
inst_12 : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
f : M →ₗ[R] N
⊢ Eq (α := M →ₗ[R] P)
    ((linearMapRightBaseChangeEquiv M ibc : (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P) (1 ⊗ₜ[R] f) : M →ₗ[R] P)
    ((compRight R ε : (a : M →ₗ[R] N) → M →ₗ[R] P) f : M →ₗ[R] P)

Tactic:
simp [linearMapRightBaseChangeEquiv, linearMapRightBaseChangeHom]

Premises used: IsBaseChange.linearMapRightBaseChangeHom, IsBaseChange.linearMapRightBaseChangeEquiv
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
Q : Type u_6
inst_9 : AddCommMonoid Q
inst_10 : Module R Q
inst_11 : Module S P
inst_12 : IsScalarTower R S P
inst_13 : Module S Q
inst_14 : IsScalarTower R S Q
α : M →ₗ[R] P
j : IsBaseChange S α
β : N →ₗ[R] Q
f : M →ₗ[R] N
p : P
⊢ Eq.{u_6 + 1} (α := Q)
    (((((j.linearMapLeftRightHom β : (M →ₗ[R] N) →ₗ[R] P →ₗ[S] Q) : (a : M →ₗ[R] N) → P →ₗ[S] Q) f : P →ₗ[S] Q) :
          (a : P) → Q)
        p :
      Q)
    (((((liftBaseChangeEquiv S : (M →ₗ[R] Q) ≃ₗ[S] S ⊗[R] M →ₗ[S] Q) : (a : M →ₗ[R] Q) → S ⊗[R] M →ₗ[S] Q) (β ∘ₗ f) :
            S ⊗[R] M →ₗ[S] Q) :
          (a : S ⊗[R] M) → Q)
        ((j.equiv.symm : (a : P) → S ⊗[R] M) p : S ⊗[R] M) :
      Q)

Tactic:
rfl
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
Q : Type u_6
inst_9 : AddCommMonoid Q
inst_10 : Module R Q
inst_11 : Module S P
inst_12 : IsScalarTower R S P
inst_13 : Module S Q
inst_14 : IsScalarTower R S Q
α : M →ₗ[R] P
j : IsBaseChange S α
β : N →ₗ[R] Q
f : M →ₗ[R] N
m : M
⊢ Eq.{u_6 + 1} (α := Q)
    (((((j.linearMapLeftRightHom β : (M →ₗ[R] N) →ₗ[R] P →ₗ[S] Q) : (a : M →ₗ[R] N) → P →ₗ[S] Q) f : P →ₗ[S] Q) :
          (a : P) → Q)
        ((α : (a : M) → P) m : P) :
      Q)
    ((β : (a : N) → Q) ((f : (a : M) → N) m : N) : Q)

Tactic:
simp [linearMapLeftRightHom_apply, IsBaseChange.equiv_symm_apply]

Premises used: IsBaseChange.equiv_symm_apply, IsBaseChange.linearMapLeftRightHom_apply
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
Q : Type u_6
inst_9 : AddCommMonoid Q
inst_10 : Module R Q
inst_11 : Module S P
inst_12 : IsScalarTower R S P
inst_13 : Module S Q
inst_14 : IsScalarTower R S Q
α : M →ₗ[R] P
j : IsBaseChange S α
β : N →ₗ[R] Q
f : M →ₗ[R] N
h :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := Q)
      (((↑R :
                  {S : Type u_2} →
                    {M : Type u_5} →
                      {M₂ : Type u_6} →
                        [inst : Semiring R] →
                          [inst_15 : Semiring S] →
                            [inst_16 : AddCommMonoid M] →
                              [inst_17 : AddCommMonoid M₂] →
                                [inst_18 : Module R M] →
                                  [inst_19 : Module R M₂] →
                                    [inst_20 : Module S M] →
                                      [inst_21 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (S := S)
                (((j.linearMapLeftRightHom β : (M →ₗ[R] N) →ₗ[R] P →ₗ[S] Q) : (a : M →ₗ[R] N) → P →ₗ[S] Q) f) ∘ₗ
              α :
            (a : M) → Q)
          x :
        Q)
      ((β ∘ₗ f : (a : M) → Q) x : Q)
⊢ (↑R :
          {S : Type u_2} →
            {M : Type u_5} →
              {M₂ : Type u_6} →
                [inst : Semiring R] →
                  [inst_15 : Semiring S] →
                    [inst_16 : AddCommMonoid M] →
                      [inst_17 : AddCommMonoid M₂] →
                        [inst_18 : Module R M] →
                          [inst_19 : Module R M₂] →
                            [inst_20 : Module S M] →
                              [inst_21 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (S := S) (((j.linearMapLeftRightHom β : (M →ₗ[R] N) →ₗ[R] P →ₗ[S] Q) : (a : M →ₗ[R] N) → P →ₗ[S] Q) f) ∘ₗ
      α =
    β ∘ₗ f

Tactic:
ext