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
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
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:
simp [linearMapLeftRightHom_comp_apply]

Premises used: IsBaseChange.linearMapLeftRightHom_comp_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
inst_15 : Free R M
inst_16 : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
β : N →ₗ[R] Q
k : IsBaseChange S β
apply :
  ∀ (x : 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] x) :
        P →ₗ[S] Q)
      (((j.linearMapLeftRightHom β : (M →ₗ[R] N) →ₗ[R] P →ₗ[S] Q) : (a : M →ₗ[R] N) → P →ₗ[S] Q) x : P →ₗ[S] Q)
⊢ IsBaseChange (N := P →ₗ[S] Q) S (j.linearMapLeftRightHom β : (M →ₗ[R] N) →ₗ[R] P →ₗ[S] Q)

Tactic:
apply of_equiv <|
      (k.linearMapRight M).equiv ≪≫ₗ liftBaseChangeEquiv S ≪≫ₗ LinearEquiv.congrLeft Q S j.equiv

Premises used: IsBaseChange.of_equiv, LinearEquiv.congrLeft, LinearMap.liftBaseChangeEquiv, IsBaseChange.linearMapRight, IsBaseChange.equiv
-- 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
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
h :
  ∀ (p : P),
    Eq.{u_6 + 1} (α := 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) :
            (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)
⊢ 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)

Tactic:
ext p
-- 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
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
p : P
⊢ Eq.{u_6 + 1} (α := 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) :
          (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:
simp [IsBaseChange.equiv_tmul, LinearEquiv.congrLeft, linearMapLeftRightHom_apply]

Premises used: LinearEquiv.congrLeft, IsBaseChange.equiv_tmul, 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
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
p : P
⊢ Eq (α := P) ((((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f : P →ₗ[S] P) : (a : P) → P) p : P)
    (((((liftBaseChangeEquiv S : (M →ₗ[R] P) ≃ₗ[S] S ⊗[R] M →ₗ[S] P) : (a : M →ₗ[R] P) → S ⊗[R] M →ₗ[S] P) (α ∘ₗ f) :
            S ⊗[R] M →ₗ[S] P) :
          (a : S ⊗[R] M) → P)
        ((j.equiv.symm : (a : P) → S ⊗[R] M) p : S ⊗[R] M) :
      P)

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
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
m : M
⊢ Eq (α := P) ((((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f : P →ₗ[S] P) : (a : P) → P) ((α : (a : M) → P) m : P) : P)
    ((α : (a : M) → P) ((f : (a : M) → M) m : M) : P)

Tactic:
simp [endHom_apply, IsBaseChange.equiv_symm_apply]

Premises used: IsBaseChange.equiv_symm_apply, IsBaseChange.endHom_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
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
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)
⊢ (↑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

Tactic:
ext
-- 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
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
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:
simp [endHom_comp_apply]

Premises used: IsBaseChange.endHom_comp_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
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 α
h : ∀ (p : P), Eq (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) p : P) ((1 : (a : P) → P) p : P)
⊢ Eq.{u_5 + 1} (α := P →ₗ[S] P) ((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1) 1

Tactic:
ext p
-- 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
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 α
⊢ Eq.{u_5 + 1} (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) 0 : P) ((1 : (a : P) → P) 0 : 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
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 α
x y : P
hx : Eq (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) x : P) ((1 : (a : P) → P) x : P)
hy : Eq (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) y : P) ((1 : (a : P) → P) y : P)
⊢ Eq (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) (x + y) : P) ((1 : (a : P) → P) (x + y) : P)

Tactic:
simp [hx, hy]
-- 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
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 α
s : S
n : P
h : Eq (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) n : P) ((1 : (a : P) → P) n : P)
⊢ Eq (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) (s • n) : P) ((1 : (a : P) → P) (s • n) : P)

Tactic:
simp [h]
-- 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
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 α
m : M
⊢ Eq.{u_5 + 1} (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) ((α : (a : M) → P) m : P) : P)
    ((1 : (a : P) → P) ((α : (a : M) → P) m : P) : P)

Tactic:
simp [endHom_comp_apply]

Premises used: IsBaseChange.endHom_comp_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
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 α
p : P
h : Eq.{u_5 + 1} (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) 0 : P) ((1 : (a : P) → P) 0 : P)
h₁ :
  ∀ (x y : P)
    (hx : Eq (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) x : P) ((1 : (a : P) → P) x : P))
    (hy : Eq (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) y : P) ((1 : (a : P) → P) y : P)),
    Eq (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) (x + y) : P) ((1 : (a : P) → P) (x + y) : P)
h₂ :
  ∀ (s : S) (n : P)
    (h : Eq (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) n : P) ((1 : (a : P) → P) n : P)),
    Eq (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) (s • n) : P) ((1 : (a : P) → P) (s • n) : P)
h₃ :
  ∀ (m : M),
    Eq.{u_5 + 1} (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) ((α : (a : M) → P) m : P) : P)
      ((1 : (a : P) → P) ((α : (a : M) → P) m : P) : P)
⊢ Eq (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) p : P) ((1 : (a : P) → P) p : P)

Tactic:
induction p using j.inductionOn with
  | zero => simp
  | add x y hx hy => simp [hx, hy]
  | smul _ _ h => simp [h]
  | tmul m => simp [endHom_comp_apply]

Premises used: IsBaseChange.endHom_comp_apply, TensorProduct.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
P : Type u_5
inst_5 : AddCommMonoid 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 α
apply :
  ∀ (x : M →ₗ[R] M),
    Eq.{u_5 + 1} (α := P →ₗ[S] P)
      ((equiv ⋯ ≪≫ₗ liftBaseChangeEquiv S ≪≫ₗ LinearEquiv.congrLeft P S j.equiv : (a : S ⊗[R] (M →ₗ[R] M)) → P →ₗ[S] P)
          (1 ⊗ₜ[R] x) :
        P →ₗ[S] P)
      ((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) x : P →ₗ[S] P)
⊢ IsBaseChange S j.endHom

Tactic:
apply of_equiv <|
      (j.linearMapRight M).equiv ≪≫ₗ liftBaseChangeEquiv S ≪≫ₗ LinearEquiv.congrLeft P S j.equiv

Premises used: IsBaseChange.of_equiv, LinearEquiv.congrLeft, LinearMap.liftBaseChangeEquiv, IsBaseChange.linearMapRight, IsBaseChange.equiv
-- 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
P : Type u_5
inst_5 : AddCommMonoid 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
h :
  ∀ (p : P),
    Eq (α := P)
      ((((equiv ⋯ ≪≫ₗ liftBaseChangeEquiv S ≪≫ₗ LinearEquiv.congrLeft P S j.equiv :
                  (a : S ⊗[R] (M →ₗ[R] M)) → P →ₗ[S] P)
                (1 ⊗ₜ[R] f) :
              P →ₗ[S] P) :
            (a : P) → P)
          p :
        P)
      ((((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f : P →ₗ[S] P) : (a : P) → P) p : P)
⊢ Eq.{u_5 + 1} (α := P →ₗ[S] P)
    ((equiv ⋯ ≪≫ₗ liftBaseChangeEquiv S ≪≫ₗ LinearEquiv.congrLeft P S j.equiv : (a : S ⊗[R] (M →ₗ[R] M)) → P →ₗ[S] P)
        (1 ⊗ₜ[R] f) :
      P →ₗ[S] P)
    ((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f : P →ₗ[S] P)

Tactic:
ext p
-- 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
P : Type u_5
inst_5 : AddCommMonoid 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
p : P
⊢ Eq (α := P)
    ((((equiv ⋯ ≪≫ₗ liftBaseChangeEquiv S ≪≫ₗ LinearEquiv.congrLeft P S j.equiv : (a : S ⊗[R] (M →ₗ[R] M)) → P →ₗ[S] P)
              (1 ⊗ₜ[R] f) :
            P →ₗ[S] P) :
          (a : P) → P)
        p :
      P)
    ((((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f : P →ₗ[S] P) : (a : P) → P) p : P)

Tactic:
simp [equiv_tmul, LinearEquiv.congrLeft, endHom_apply]

Premises used: IsBaseChange.endHom_apply, 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
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
β : N →ₗ[R] Q
ibcM : IsBaseChange S α
ibcN : IsBaseChange S β
ι : Type u_7
θ : Type u_8
inst_15 : DecidableEq ι
inst_16 : Fintype ι
inst_17 : Finite θ
b : Basis ι R M
c : Basis θ R N
f : M →ₗ[R] N
a :
  ∀ (i : θ) (j : ι),
    Eq.{u_2 + 1} (α := S)
      ((toMatrix (basis b ibcM) (basis c ibcN) : (a : P →ₗ[S] Q) → Matrix θ ι S)
          (((ibcM.linearMapLeftRightHom β : (M →ₗ[R] N) →ₗ[R] P →ₗ[S] Q) : (a : M →ₗ[R] N) → P →ₗ[S] Q) f) i j :
        S)
      (Matrix.map.{u_1, u_2, u_8, u_7} (α := R) ((toMatrix b c : (a : M →ₗ[R] N) → Matrix θ ι R) f)
          (⇑(algebraMap R S) : (a : R) → S) i j :
        S)
⊢ Eq (α := Matrix θ ι S)
    ((toMatrix (basis b ibcM) (basis c ibcN) : (a : P →ₗ[S] Q) → Matrix θ ι S)
        (((ibcM.linearMapLeftRightHom β : (M →ₗ[R] N) →ₗ[R] P →ₗ[S] Q) : (a : M →ₗ[R] N) → P →ₗ[S] Q) f) :
      Matrix θ ι S)
    (Matrix.map.{u_1, u_2, u_8, u_7} (α := R) ((toMatrix b c : (a : M →ₗ[R] N) → Matrix θ ι R) f)
        (⇑(algebraMap R S) : (a : R) → S) :
      Matrix θ ι S)

Tactic:
ext i j
-- 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
β : N →ₗ[R] Q
ibcM : IsBaseChange S α
ibcN : IsBaseChange S β
ι : Type u_7
θ : Type u_8
inst_15 : DecidableEq ι
inst_16 : Fintype ι
inst_17 : Finite θ
b : Basis ι R M
c : Basis θ R N
f : M →ₗ[R] N
i : θ
j : ι
⊢ Eq.{u_2 + 1} (α := S)
    ((toMatrix (basis b ibcM) (basis c ibcN) : (a : P →ₗ[S] Q) → Matrix θ ι S)
        (((ibcM.linearMapLeftRightHom β : (M →ₗ[R] N) →ₗ[R] P →ₗ[S] Q) : (a : M →ₗ[R] N) → P →ₗ[S] Q) f) i j :
      S)
    (Matrix.map.{u_1, u_2, u_8, u_7} (α := R) ((toMatrix b c : (a : M →ₗ[R] N) → Matrix θ ι R) f)
        (⇑(algebraMap R S) : (a : R) → S) i j :
      S)

Tactic:
simp only [toMatrix_apply, Matrix.map_apply, basis_apply,
    linearMapLeftRightHom_comp_apply, basis_repr_comp_apply]

Premises used: IsBaseChange.basis_repr_comp_apply, IsBaseChange.linearMapLeftRightHom_comp_apply, Matrix.map_apply, IsBaseChange.basis_apply, LinearMap.toMatrix_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
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
ibcM : IsBaseChange S α
ι : Type u_7
inst_9 : DecidableEq ι
inst_10 : Fintype ι
b : Basis ι R M
f : M →ₗ[R] M
a :
  ∀ (i j : ι),
    Eq.{u_2 + 1} (α := S)
      ((toMatrix (basis b ibcM) (basis b ibcM) : (a : P →ₗ[S] P) → Matrix ι ι S)
          ((ibcM.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f) i j :
        S)
      (Matrix.map.{u_1, u_2, u_7, u_7} (α := R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f)
          (⇑(algebraMap R S) : (a : R) → S) i j :
        S)
⊢ Eq (α := Matrix ι ι S)
    ((toMatrix (basis b ibcM) (basis b ibcM) : (a : P →ₗ[S] P) → Matrix ι ι S)
        ((ibcM.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f) :
      Matrix ι ι S)
    (Matrix.map.{u_1, u_2, u_7, u_7} (α := R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f)
        (⇑(algebraMap R S) : (a : R) → S) :
      Matrix ι ι S)

Tactic:
ext i j
-- 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
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
ibcM : IsBaseChange S α
ι : Type u_7
inst_9 : DecidableEq ι
inst_10 : Fintype ι
b : Basis ι R M
f : M →ₗ[R] M
i j : ι
a :
  Eq.{u_2 + 1} (α := S)
    (((((basis b ibcM).repr : (a : P) → ι →₀ S)
              ((((ibcM.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f : P →ₗ[S] P) : (a : P) → P)
                ((basis b ibcM : (a : ι) → P) j : P)) :
            ι →₀ S) :
          (a : ι) → S)
        i :
      S)
    ((algebraMap R S : (a : R) → S)
        ((((b.repr : (a : M) → ι →₀ R) ((f : (a : M) → M) ((b : (a : ι) → M) j : M)) : ι →₀ R) : (a : ι) → R) i : R) :
      S)
⊢ Eq.{u_2 + 1} (α := S)
    ((toMatrix (basis b ibcM) (basis b ibcM) : (a : P →ₗ[S] P) → Matrix ι ι S)
        ((ibcM.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f) i j :
      S)
    (Matrix.map.{u_1, u_2, u_7, u_7} (α := R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f)
        (⇑(algebraMap R S) : (a : R) → S) i j :
      S)

Tactic:
simp only [toMatrix_apply, Matrix.map_apply]

Premises used: Matrix.map_apply, LinearMap.toMatrix_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
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
ibcM : IsBaseChange S α
ι : Type u_7
inst_9 : DecidableEq ι
inst_10 : Fintype ι
b : Basis ι R M
f : M →ₗ[R] M
i j : ι
⊢ Eq.{u_2 + 1} (α := S)
    (((((basis b ibcM).repr : (a : P) → ι →₀ S)
              ((((ibcM.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f : P →ₗ[S] P) : (a : P) → P)
                ((basis b ibcM : (a : ι) → P) j : P)) :
            ι →₀ S) :
          (a : ι) → S)
        i :
      S)
    ((algebraMap R S : (a : R) → S)
        ((((b.repr : (a : M) → ι →₀ R) ((f : (a : M) → M) ((b : (a : ι) → M) j : M)) : ι →₀ R) : (a : ι) → R) i : R) :
      S)

Tactic:
simp only [basis_apply, endHom_comp_apply, basis_repr_comp_apply]

Premises used: IsBaseChange.basis_repr_comp_apply, IsBaseChange.endHom_comp_apply, IsBaseChange.basis_apply