awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
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
ε : N →ₗ[R] P
s : S
x : S ⊗[R] (M →ₗ[R] N)
⊢ AddHom.toFun
      (toAddHom (S := R) (σ := RingHom.id R)
        (TensorProduct.lift
          { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε), map_add' := ⋯,
            map_smul' := ⋯ }))
      (s • x) =
    HSMul.hSMul (α := S) (β := M →ₗ[R] P) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun
        (toAddHom (S := R) (σ := RingHom.id R)
          (TensorProduct.lift
            { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε), map_add' := ⋯,
              map_smul' := ⋯ : S →ₗ[R] (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P }))
        x)
have simp : (TensorProduct.lift
        { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε), map_add' := sorry,
          map_smul' := sorry } :
      (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
    (s • x) =
  HSMul.hSMul (β := M →ₗ[R] P) s
    ((TensorProduct.lift
            { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε), map_add' := sorry,
              map_smul' := sorry : S →ₗ[R] (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P } :
          (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
        x :
      M →ₗ[R] P)
Tactic: simp only [AddHom.toFun_eq_coe, coe_toAddHom, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
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
ε : N →ₗ[R] P
s : S
x : S ⊗[R] (M →ₗ[R] N)
⊢ (TensorProduct.lift
          { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε), map_add' := ⋯,
            map_smul' := ⋯ } :
        (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
      (s • x) =
    HSMul.hSMul (β := M →ₗ[R] P) s
      ((TensorProduct.lift
              { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε), map_add' := ⋯,
                map_smul' := ⋯ : S →ₗ[R] (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P } :
            (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
          x :
        M →ₗ[R] P)
have zero : (TensorProduct.lift
        { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε), map_add' := sorry,
          map_smul' := sorry } :
      (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
    (HSMul.hSMul (β := S ⊗[R] (M →ₗ[R] N)) s 0) =
  HSMul.hSMul (β := M →ₗ[R] P) s
    ((TensorProduct.lift
          { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε), map_add' := sorry,
            map_smul' := sorry : S →ₗ[R] (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P } :
        (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
      0)
Tactic: induction x using TensorProduct.induction_on with
    | zero => simp
    | add x y hx hy => simp [smul_add, hx, hy]
    | tmul t f => simp [TensorProduct.smul_tmul', mul_smul]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
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 ε
⊢ S ⊗[R] (M →ₗ[R] N) ≃ₗ[S] M →ₗ[R] P
have apply : 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: apply LinearEquiv.ofBijective (linearMapRightBaseChangeHom S M ε)
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
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
⊢ 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)
have 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)
Tactic: set ι := Free.ChooseBasisIndex R M
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
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
⊢ 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)
have 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)
Tactic: have := Free.ChooseBasisIndex.fintype R M
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
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))
⊢ 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)
have suffices : Function.Bijective (α := S ⊗[R] (ι → N)) (β := ι → P) (⇑h' : (a : S ⊗[R] (ι → N)) → ι → P)
Tactic: suffices Function.Bijective h' by simpa [h'] using this
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
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) (⇑h' : (a : S ⊗[R] (ι → N)) → ι → P)
have simp : Function.Bijective (α := S ⊗[R] (ι → N)) (β := ι → P)
  (⇑(↑sorry.equiv : S ⊗[R] (ι → N) →ₗ[S] ι → P) : (a : S ⊗[R] (ι → N)) → ι → P)
Tactic: simp only [this]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
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))
⊢ Function.Bijective (α := S ⊗[R] (ι → N)) (β := ι → P) (⇑h' : (a : S ⊗[R] (ι → N)) → ι → P)
have suffices : h' = (↑sorry.equiv : S ⊗[R] (ι → N) →ₗ[S] ι → P)
Tactic: suffices h' = (finitePow ι ibc).equiv by
    simp only [this]
    apply LinearEquiv.bijective
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
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))
⊢ h' = (↑⋯.equiv : S ⊗[R] (ι → N) →ₗ[S] ι → P)
have suffices : (↑f : (M →ₗ[R] P) →ₗ[S] ι → P) ∘ₗ linearMapRightBaseChangeHom S M ε =
  (↑sorry.equiv : S ⊗[R] (ι → N) →ₗ[S] ι → P) ∘ₗ (↑e' : S ⊗[R] (M →ₗ[R] N) →ₗ[S] S ⊗[R] (ι → N))
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']
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
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))
⊢ (↑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))
have 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
                  ((↑sorry.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: ext φ i
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
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)
    ((((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)
have 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)
  ((sorry.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
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
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 ε
⊢ IsBaseChange (M := M →ₗ[R] N) S (compRight R ε)
have 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)
Tactic: apply of_equiv (linearMapRightBaseChangeEquiv M ibc)
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
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
⊢ (↑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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
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
inst_15 : Free R M
inst_16 : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
β : N →ₗ[R] Q
k : IsBaseChange S β
⊢ IsBaseChange (N := P →ₗ[S] Q) S (j.linearMapLeftRightHom β : (M →ₗ[R] N) →ₗ[R] P →ₗ[S] Q)
have apply : ∀ (x : M →ₗ[R] N),
  Eq (α := P →ₗ[S] Q)
    ((equiv sorry ≪≫ₗ liftBaseChangeEquiv S ≪≫ₗ LinearEquiv.congrLeft Q S j.equiv : (a : S ⊗[R] (M →ₗ[R] N)) → P →ₗ[S] Q)
        (1 ⊗ₜ[R] x) :
      P →ₗ[S] Q)
    (((j.linearMapLeftRightHom β : (M →ₗ[R] N) →ₗ[R] P →ₗ[S] Q) : (a : M →ₗ[R] N) → P →ₗ[S] Q) x : P →ₗ[S] Q)
Tactic: apply of_equiv <|
      (k.linearMapRight M).equiv ≪≫ₗ liftBaseChangeEquiv S ≪≫ₗ LinearEquiv.congrLeft Q S j.equiv
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
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
inst_15 : Free R M
inst_16 : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
β : N →ₗ[R] Q
k : IsBaseChange S β
f : M →ₗ[R] N
⊢ Eq (α := P →ₗ[S] Q)
    ((equiv ⋯ ≪≫ₗ liftBaseChangeEquiv S ≪≫ₗ LinearEquiv.congrLeft Q S j.equiv : (a : S ⊗[R] (M →ₗ[R] N)) → P →ₗ[S] Q)
        (1 ⊗ₜ[R] f) :
      P →ₗ[S] Q)
    (((j.linearMapLeftRightHom β : (M →ₗ[R] N) →ₗ[R] P →ₗ[S] Q) : (a : M →ₗ[R] N) → P →ₗ[S] Q) f : P →ₗ[S] Q)
have h : ∀ (p : P),
  Eq.{u_6 + 1} (α := Q)
    ((((equiv sorry ≪≫ₗ liftBaseChangeEquiv S ≪≫ₗ LinearEquiv.congrLeft Q S j.equiv : (a : S ⊗[R] (M →ₗ[R] N)) → P →ₗ[S] Q)
              (1 ⊗ₜ[R] f) :
            P →ₗ[S] Q) :
          (a : P) → Q)
        p :
      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)
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
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
P : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : Module S P
inst_8 : IsScalarTower R S P
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
⊢ (↑R :
          {S : Type u_2} →
            {M M₂ : Type u_5} →
              [inst : Semiring R] →
                [inst_9 : Semiring S] →
                  [inst_10 : AddCommMonoid M] →
                    [inst_11 : AddCommMonoid M₂] →
                      [inst_12 : Module R M] →
                        [inst_13 : Module R M₂] →
                          [inst_14 : Module S M] →
                            [inst_15 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (S := S) ((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f) ∘ₗ
      α =
    α ∘ₗ f
have h : ∀ (x : M),
  Eq.{u_5 + 1} (α := P)
    (((↑R :
                {S : Type u_2} →
                  {M M₂ : Type u_5} →
                    [inst : Semiring R] →
                      [inst_9 : Semiring S] →
                        [inst_10 : AddCommMonoid M] →
                          [inst_11 : AddCommMonoid M₂] →
                            [inst_12 : Module R M] →
                              [inst_13 : Module R M₂] →
                                [inst_14 : Module S M] →
                                  [inst_15 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (S := S) ((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f) ∘ₗ
            α :
          (a : M) → P)
        x :
      P)
    ((α ∘ₗ f : (a : M) → P) x : P)
Tactic: ext