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
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 →ₗ[S] P) ((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1) 1
have 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)
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 α
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)
have 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)
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]
Cleared hypotheses: 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 α
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)
⊢ Eq (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) p : P) ((1 : (a : P) → P) p : P)
have 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)
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]
Cleared hypotheses: 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 α
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)
⊢ Eq (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) p : P) ((1 : (a : P) → P) p : P)
have 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)
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]
Cleared hypotheses: 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 α
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)
⊢ Eq (α := P) (((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) 1 : (a : P) → P) p : P) ((1 : (a : P) → P) p : P)
have 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)
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]
Cleared hypotheses: 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
inst_9 : Free R M
inst_10 : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
⊢ IsBaseChange S j.endHom
have apply : ∀ (x : M →ₗ[R] M),
  Eq.{u_5 + 1} (α := P →ₗ[S] P)
    ((equiv sorry ≪≫ₗ 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)
Tactic: apply of_equiv <|
      (j.linearMapRight M).equiv ≪≫ₗ liftBaseChangeEquiv S ≪≫ₗ LinearEquiv.congrLeft P 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
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
⊢ 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)
have h : ∀ (p : P),
  Eq (α := P)
    ((((equiv sorry ≪≫ₗ 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: 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
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
⊢ 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)
have 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)
Tactic: ext i j
-- 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
ibcM : IsBaseChange S α
ι : Type u_7
inst_9 : DecidableEq ι
inst_10 : Fintype ι
b : Basis ι R M
f : M →ₗ[R] M
⊢ 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)
have 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)
Tactic: ext i j
-- 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
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)
    ((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)
have 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)
Tactic: simp only [toMatrix_apply, Matrix.map_apply]
-- 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
⊢ 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 inl : ∀ (hR : Subsingleton R),
  Eq.{u_7 + 1} (α := S)
    ((LinearMap.det : (a : P →ₗ[S] P) → S) ((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f : P →ₗ[S] P) : S)
    ((algebraMap R S : (a : R) → S) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) : S)
Tactic: rcases subsingleton_or_nontrivial R with hR | hR
-- 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
inl :
  ∀ (hR : Subsingleton R),
    Eq.{u_7 + 1} (α := S)
      ((LinearMap.det : (a : P →ₗ[S] P) → S) ((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f : P →ₗ[S] P) : S)
      ((algebraMap R S : (a : R) → S) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) : S)
⊢ 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 : ∀ (hR : Nontrivial R),
  Eq.{u_7 + 1} (α := S)
    ((LinearMap.det : (a : P →ₗ[S] P) → S) ((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f : P →ₗ[S] P) : S)
    ((algebraMap R S : (a : R) → S) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) : S)
Tactic: rcases subsingleton_or_nontrivial R with hR | hR
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (hypothesis)
Goal:
R : Type u_6
inst : CommRing R
S : Type u_7
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_8
inst_3 : AddCommGroup M
inst_4 : Module R M
P : Type u_9
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : Module S P
inst_8 : IsScalarTower R S P
inst_9 : Free R M
inst_10 : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
hR : Subsingleton R
⊢ f = 1
have this : Subsingleton M
Tactic: have : Subsingleton M := Module.subsingleton R M
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (hypothesis)
Goal:
R : Type u_6
inst : CommRing R
S : Type u_7
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_8
inst_3 : AddCommGroup M
inst_4 : Module R M
P : Type u_9
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : Module S P
inst_8 : IsScalarTower R S P
inst_9 : Free R M
inst_10 : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
hR : Subsingleton R
⊢ 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 this : f = 1
Tactic: have : f = 1 := by
      have : Subsingleton M := Module.subsingleton R M
      exact Subsingleton.eq_one f
-- 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
⊢ 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)
  ((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)
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.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)
⊢ 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)
  (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)
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.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)
⊢ 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)
  (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)
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.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)
⊢ 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)
  (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)
Tactic: rw [← f.det_toMatrix b, ← (j.endHom f).det_toMatrix (j.basis b),
    endHom_toMatrix, ← RingHom.mapMatrix_apply, ← RingHom.map_det]