awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra A R
inst_5 : Module A V
inst_6 : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
j : R ⊗[A] (ι →₀ A) ≃ₗ[R] ι →₀ R := finsuppScalarRight A R R ι
x : ι →₀ A
i : ι
⊢ Eq.{u_1 + 1} (α := R) ((((j : (a : R ⊗[A] (ι →₀ A)) → ι →₀ R) (1 ⊗ₜ[A] x) : ι →₀ R) : (a : ι) → R) i : R)
    ((Finsupp.mapRange (⇑(algebraMap A R) : (a : A) → R) ⋯ x : (a : ι) → R) i : R)

Tactic:
simp [j, Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra A R
inst_5 : Module A V
inst_6 : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
let let₁ let₂ : IsBaseChange (M := ι →₀ A) (N := V) R (Finsupp.linearCombination A (⇑b : (a : ι) → V))
refine_1 : R ⊗[A] (ι →₀ A) ≃ₗ[R] V
refine_2 refine_2₁ :
  let j : R ⊗[A] (ι →₀ A) ≃ₗ[R] ι →₀ R := finsuppScalarRight A R R ι;
  ∀ (x : ι →₀ A),
    Eq.{u_2 + 1} (α := V)
      ((LinearEquiv.ofBijective (Finsupp.linearCombination R (⇑b : (a : ι) → V) ∘ₗ (↑j : R ⊗[A] (ι →₀ A) →ₗ[R] ι →₀ R))
              ⋯ :
            (a : R ⊗[A] (ι →₀ A)) → V)
          (1 ⊗ₜ[A] x) :
        V)
      ((Finsupp.linearCombination A (⇑b : (a : ι) → V) : (a : ι →₀ A) → V) x : V)
⊢ IsBaseChange (M := ι →₀ A) (N := V) R (Finsupp.linearCombination A (⇑b : (a : ι) → V))

Tactic:
classical
  let j := TensorProduct.finsuppScalarRight A R R ι
  refine of_equiv ?_ ?_
  · apply LinearEquiv.ofBijective (Finsupp.linearCombination R b ∘ₗ j)
    rw [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, j.bijective.of_comp_iff]
    simp [Function.Bijective,
        ← span_range_eq_top_iff_surjective_finsuppLinearCombination,
        ← linearIndependent_iff_injective_finsuppLinearCombination,
        Module.Basis.span_eq, b.linearIndependent]
  · intro x
    suffices (j (1 ⊗ₜ[A] x)) = x.mapRange (algebraMap A R) (by simp) by
      simp [this, Finsupp.linearCombination_apply, Finsupp.sum_mapRange_index]
    ext i
    simp [j, Algebra.algebraMap_eq_smul_one]

Premises used: linearIndependent_iff_injective_finsuppLinearCombination, Algebra.algebraMap_eq_smul_one, IsBaseChange.of_equiv, LinearMap.coe_comp, Module.Basis.linearIndependent, Function.Bijective, span_range_eq_top_iff_surjective_finsuppLinearCombination, LinearEquiv.coe_toLinearMap, Module.Basis.span_eq
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra A R
inst_5 : Module A V
inst_6 : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst_7 : Fintype ι
have : ∀ (this : DecidableEq ι), IsBaseChange (M := ι → A) (N := V) R (Fintype.linearCombination A (⇑b : (a : ι) → V))
⊢ IsBaseChange (M := ι → A) (N := V) R (Fintype.linearCombination A (⇑b : (a : ι) → V))

Tactic:
have : DecidableEq ι := Classical.typeDecidableEq ι
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra A R
inst_5 : Module A V
inst_6 : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst_7 : Fintype ι
this : DecidableEq ι
j : R ⊗[A] (ι → A) ≃ₗ[R] ι → R := piScalarRight A R R ι
⊢ IsBaseChange (M := ι → A) (N := V) R (Fintype.linearCombination A (⇑b : (a : ι) → V))

Tactic:
of_equiv ?_ ?_

Premises used: IsBaseChange.of_equiv
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra A R
inst_5 : Module A V
inst_6 : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst_7 : Fintype ι
this : DecidableEq ι
j : R ⊗[A] (ι → A) ≃ₗ[R] ι → R := piScalarRight A R R ι
refine_1 : R ⊗[A] (ι → A) ≃ₗ[R] V
refine_2 :
  ∀ (x : ι → A),
    Eq.{u_2 + 1} (α := V)
      ((LinearEquiv.ofBijective (Fintype.linearCombination R (⇑b : (a : ι) → V) ∘ₗ (↑j : R ⊗[A] (ι → A) →ₗ[R] ι → R))
              ⋯ :
            (a : R ⊗[A] (ι → A)) → V)
          (1 ⊗ₜ[A] x) :
        V)
      ((Fintype.linearCombination A (⇑b : (a : ι) → V) : (a : ι → A) → V) x : V)
⊢ IsBaseChange (M := ι → A) (N := V) R (Fintype.linearCombination A (⇑b : (a : ι) → V))

Tactic:
refine of_equiv ?_ ?_

Premises used: IsBaseChange.of_equiv
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra A R
inst_5 : Module A V
inst_6 : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst_7 : Fintype ι
this : DecidableEq ι
j : R ⊗[A] (ι → A) ≃ₗ[R] ι → R := piScalarRight A R R ι
refine_1 :
  Function.Bijective (α := R ⊗[A] (ι → A)) (β := V)
    (⇑(Fintype.linearCombination R (⇑b : (a : ι) → V) ∘ₗ (↑j : R ⊗[A] (ι → A) →ₗ[R] ι → R)) : (a : R ⊗[A] (ι → A)) → V)
⊢ R ⊗[A] (ι → A) ≃ₗ[R] V

Tactic:
apply LinearEquiv.ofBijective (Fintype.linearCombination R b ∘ₗ j)

Premises used: LinearMap.comp, Fintype.linearCombination, DFunLike.coe, LinearEquiv.ofBijective
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra A R
inst_5 : Module A V
inst_6 : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst_7 : Fintype ι
this : DecidableEq ι
j : R ⊗[A] (ι → A) ≃ₗ[R] ι → R := piScalarRight A R R ι
refine_1 :
  Function.Bijective (α := ι → R) (β := V) (⇑(Fintype.linearCombination R (⇑b : (a : ι) → V)) : (a : ι → R) → V)
⊢ Function.Bijective (α := R ⊗[A] (ι → A)) (β := V)
    (⇑(Fintype.linearCombination R (⇑b : (a : ι) → V) ∘ₗ (↑j : R ⊗[A] (ι → A) →ₗ[R] ι → R)) : (a : R ⊗[A] (ι → A)) → V)

Tactic:
rw [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, j.bijective.of_comp_iff]

Premises used: LinearEquiv.bijective, Function.Bijective.of_comp_iff, LinearMap.coe_comp, LinearEquiv.coe_toLinearMap
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra A R
inst_5 : Module A V
inst_6 : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst_7 : Fintype ι
this : DecidableEq ι
j : R ⊗[A] (ι → A) ≃ₗ[R] ι → R := piScalarRight A R R ι
⊢ Function.Bijective (α := ι → R) (β := V) (⇑(Fintype.linearCombination R (⇑b : (a : ι) → V)) : (a : ι → R) → V)

Tactic:
simp [Function.Bijective,
        ← span_range_eq_top_iff_surjective_fintypeLinearCombination,
        ← linearIndependent_iff_injective_fintypeLinearCombination,
        Module.Basis.span_eq, b.linearIndependent]

Premises used: span_range_eq_top_iff_surjective_fintypeLinearCombination, linearIndependent_iff_injective_fintypeLinearCombination, Module.Basis.linearIndependent, Function.Bijective, Module.Basis.span_eq
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra A R
inst_5 : Module A V
inst_6 : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst_7 : Fintype ι
this : DecidableEq ι
j : R ⊗[A] (ι → A) ≃ₗ[R] ι → R := piScalarRight A R R ι
x : ι → A
refine_2 :
  Eq.{u_2 + 1} (α := V)
    (∑ i : ι,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((j : (a : R ⊗[A] (ι → A)) → ι → R) (1 ⊗ₜ[A] x) i : R)
        ((b : (a : ι) → V) i : V))
    (∑ i : ι, HSMul.hSMul (β := V) (x i) ((b : (a : ι) → V) i : V))
⊢ Eq.{u_2 + 1} (α := V)
    ((LinearEquiv.ofBijective (Fintype.linearCombination R (⇑b : (a : ι) → V) ∘ₗ (↑j : R ⊗[A] (ι → A) →ₗ[R] ι → R)) ⋯ :
          (a : R ⊗[A] (ι → A)) → V)
        (1 ⊗ₜ[A] x) :
      V)
    ((Fintype.linearCombination A (⇑b : (a : ι) → V) : (a : ι → A) → V) x : V)

Tactic:
simp only [LinearEquiv.ofBijective_apply, LinearMap.coe_comp, LinearEquiv.coe_coe,
      Function.comp_apply, Fintype.linearCombination_apply]

Premises used: LinearEquiv.ofBijective_apply, LinearMap.coe_comp, Function.comp_apply, Fintype.linearCombination_apply, LinearEquiv.coe_coe
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra A R
inst_5 : Module A V
inst_6 : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst_7 : Fintype ι
this : DecidableEq ι
j : R ⊗[A] (ι → A) ≃ₗ[R] ι → R := piScalarRight A R R ι
x : ι → A
refine_2 :
  Eq (α := ι → V)
    (fun (i : ι) ↦
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((j : (a : R ⊗[A] (ι → A)) → ι → R) (1 ⊗ₜ[A] x) i : R)
        ((b : (a : ι) → V) i : V))
    fun (i : ι) ↦ HSMul.hSMul (β := V) (x i) ((b : (a : ι) → V) i : V)
⊢ Eq.{u_2 + 1} (α := V)
    (∑ i : ι,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((j : (a : R ⊗[A] (ι → A)) → ι → R) (1 ⊗ₜ[A] x) i : R)
        ((b : (a : ι) → V) i : V))
    (∑ i : ι, HSMul.hSMul (β := V) (x i) ((b : (a : ι) → V) i : V))

Tactic:
congr
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra A R
inst_5 : Module A V
inst_6 : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst_7 : Fintype ι
this : DecidableEq ι
j : R ⊗[A] (ι → A) ≃ₗ[R] ι → R := piScalarRight A R R ι
x : ι → A
refine_2 :
  ∀ (i : ι),
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((j : (a : R ⊗[A] (ι → A)) → ι → R) (1 ⊗ₜ[A] x) i : R)
        ((b : (a : ι) → V) i : V) =
      HSMul.hSMul (β := V) (x i) ((b : (a : ι) → V) i : V)
⊢ Eq (α := ι → V)
    (fun (i : ι) ↦
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((j : (a : R ⊗[A] (ι → A)) → ι → R) (1 ⊗ₜ[A] x) i : R)
        ((b : (a : ι) → V) i : V))
    fun (i : ι) ↦ HSMul.hSMul (β := V) (x i) ((b : (a : ι) → V) i : V)

Tactic:
ext i
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra A R
inst_5 : Module A V
inst_6 : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst_7 : Fintype ι
this : DecidableEq ι
j : R ⊗[A] (ι → A) ≃ₗ[R] ι → R := piScalarRight A R R ι
x : ι → A
i : ι
refine_2 :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((fun (j : ι) ↦ HSMul.hSMul (β := R) (x j) 1) i)
      ((b : (a : ι) → V) i : V) =
    HSMul.hSMul (β := V) (x i) ((b : (a : ι) → V) i : V)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((j : (a : R ⊗[A] (ι → A)) → ι → R) (1 ⊗ₜ[A] x) i : R)
      ((b : (a : ι) → V) i : V) =
    HSMul.hSMul (β := V) (x i) ((b : (a : ι) → V) i : V)

Tactic:
rw [TensorProduct.piScalarRight_apply, TensorProduct.piScalarRightHom_tmul]

Premises used: TensorProduct.piScalarRight_apply, TensorProduct.piScalarRightHom_tmul
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra A R
inst_5 : Module A V
inst_6 : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst_7 : Fintype ι
this : DecidableEq ι
j : R ⊗[A] (ι → A) ≃ₗ[R] ι → R := piScalarRight A R R ι
x : ι → A
i : ι
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((fun (j : ι) ↦ HSMul.hSMul (β := R) (x j) 1) i)
      ((b : (a : ι) → V) i : V) =
    HSMul.hSMul (β := V) (x i) ((b : (a : ι) → V) i : V)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra A R
inst_5 : Module A V
inst_6 : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst_7 : Fintype ι
a : ι → A
v : V
rw :
  (Fintype.linearCombination A (⇑b : (a : ι) → V) : (a : ι → A) → V) a = v ↔
    (b.equivFun.symm : (a : ι → R) → V) ((⇑(algebraMap A R) : (a : A) → R) ∘ a) = v
⊢ (Fintype.linearCombination A (⇑b : (a : ι) → V) : (a : ι → A) → V) a = v ↔
    Eq (α := ι → R) ((⇑(algebraMap A R) : (a : A) → R) ∘ a) ((b.equivFun : (a : V) → ι → R) v)

Tactic:
rw [← LinearEquiv.symm_apply_eq]

Premises used: LinearEquiv.symm_apply_eq
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra A R
inst_5 : Module A V
inst_6 : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst_7 : Fintype ι
a : ι → A
v : V
rw :
  ∑ i : ι, HSMul.hSMul (β := V) (a i) ((b : (a : ι) → V) i : V) = v ↔
    ∑ i : ι,
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) (((⇑(algebraMap A R) : (a : A) → R) ∘ a) i)
          ((b : (a : ι) → V) i : V) =
      v
⊢ (Fintype.linearCombination A (⇑b : (a : ι) → V) : (a : ι → A) → V) a = v ↔
    (b.equivFun.symm : (a : ι → R) → V) ((⇑(algebraMap A R) : (a : A) → R) ∘ a) = v

Tactic:
rw [Fintype.linearCombination_apply, b.equivFun_symm_apply]

Premises used: Module.Basis.equivFun_symm_apply, Fintype.linearCombination_apply
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra A R
inst_5 : Module A V
inst_6 : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst_7 : Fintype ι
a : ι → A
v : V
⊢ ∑ i : ι, HSMul.hSMul (β := V) (a i) ((b : (a : ι) → V) i : V) = v ↔
    ∑ i : ι,
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) (((⇑(algebraMap A R) : (a : A) → R) ∘ a) i)
          ((b : (a : ι) → V) i : V) =
      v

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
ε : N →ₗ[R] P
x y : S
h :
  ∀ (x_1 : M →ₗ[R] N) (x_2 : M),
    Eq.{u_5 + 1} (α := P)
      ((((HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) (x + y) (compRight R ε) : (a : M →ₗ[R] N) → M →ₗ[R] P) x_1 :
              M →ₗ[R] P) :
            (a : M) → P)
          x_2 :
        P)
      ((((HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) x (compRight R ε) +
                    HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) y (compRight R ε) :
                  (a : M →ₗ[R] N) → M →ₗ[R] P)
                x_1 :
              M →ₗ[R] P) :
            (a : M) → P)
          x_2 :
        P)
⊢ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) (x + y) (compRight R ε) =
    HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) x (compRight R ε) +
      HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) y (compRight R ε)

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
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
x y : S
x_1 : M →ₗ[R] N
x_2 : M
⊢ Eq.{u_5 + 1} (α := P)
    ((((HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) (x + y) (compRight R ε) : (a : M →ₗ[R] N) → M →ₗ[R] P) x_1 :
            M →ₗ[R] P) :
          (a : M) → P)
        x_2 :
      P)
    ((((HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) x (compRight R ε) +
                  HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) y (compRight R ε) :
                (a : M →ₗ[R] N) → M →ₗ[R] P)
              x_1 :
            M →ₗ[R] P) :
          (a : M) → P)
        x_2 :
      P)

Tactic:
simp [add_smul]

Premises used: add_smul
-- 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
ε : N →ₗ[R] P
r : R
s : S
⊢ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) (r • s) (compRight R ε) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
      (HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε))

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
ε : N →ₗ[R] P
s : S
x : S ⊗[R] (M →ₗ[R] N)
simp :
  (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)
⊢ 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)

Tactic:
simp only [AddHom.toFun_eq_coe, coe_toAddHom, RingHom.id_apply]

Premises used: RingHom.id_apply, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom
-- 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
ε : N →ₗ[R] P
s : S
⊢ (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)
      (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' := ⋯,
              map_smul' := ⋯ : S →ₗ[R] (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P } :
          (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
        0)

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
ε : N →ₗ[R] P
s : S
x y : S ⊗[R] (M →ₗ[R] N)
hx :
  (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)
hy :
  (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 • y) =
    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)
          y :
        M →ₗ[R] P)
⊢ (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 + y)) =
    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 + y) :
        M →ₗ[R] P)

Tactic:
simp [smul_add, hx, hy]

Premises used: smul_add
-- 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
ε : N →ₗ[R] P
s t : S
f : 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)
      (HSMul.hSMul (β := S ⊗[R] (M →ₗ[R] N)) s (t ⊗ₜ[R] f)) =
    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)
          (t ⊗ₜ[R] f) :
        M →ₗ[R] P)

Tactic:
simp [TensorProduct.smul_tmul', mul_smul]

Premises used: TensorProduct.smul_tmul', SemigroupAction.mul_smul
-- 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 :
  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)
⊢ S ⊗[R] (M →ₗ[R] N) ≃ₗ[S] M →ₗ[R] P

Tactic:
apply LinearEquiv.ofBijective (linearMapRightBaseChangeHom S M ε)

Premises used: IsBaseChange.linearMapRightBaseChangeHom, LinearEquiv.ofBijective