awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
V : Type u_3
inst_3 : AddCommMonoid V
inst_4 : Module R V
W : Type u_4
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
i : ι
pf : RingHomInvPair (RingHom.id S) (RingHom.id S)
pf_1 : SMulCommClass R S S
pf_2 : IsScalarTower R S S
pf_3 : IsScalarTower R S (ι →₀ S)
ibcRA : IsBaseChange (M := ι →₀ R) (N := ι →₀ S) S (Finsupp.mapRange.linearMap (Algebra.linearMap R S))
this :
  Eq (α := TensorProduct R S (ι →₀ R))
    ((ibcRA.equiv.symm : (a : ι →₀ S) → TensorProduct R S (ι →₀ R)) (Finsupp.single i 1) : TensorProduct R S (ι →₀ R))
    (1 ⊗ₜ[R] Finsupp.single i 1 : TensorProduct R S (ι →₀ R))
⊢ Eq.{u_4 + 1} (α := W)
    ((ibc.equiv : (a : TensorProduct R S V) → W)
        (((LinearEquiv.symm (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.refl S S) b.repr) :
                TensorProduct R S (ι →₀ R) ≃ₗ[S] TensorProduct R S V) :
              (a : TensorProduct R S (ι →₀ R)) → TensorProduct R S V)
            ((ibcRA.equiv.symm : (a : ι →₀ S) → TensorProduct R S (ι →₀ R)) (Finsupp.single i 1)) :
          TensorProduct R S V) :
      W)
    ((ε : (a : V) → W) ((b : (a : ι) → V) i : V) : W)

Tactic:
simp [this, IsBaseChange.equiv_tmul]

Premises used: IsBaseChange.equiv_tmul
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
V : Type u_3
inst_3 : AddCommMonoid V
inst_4 : Module R V
W : Type u_4
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
rw :
  ((Finsupp.sum ((b.repr : (a : V) → ι →₀ R) v) fun (a : ι) (b_1 : R) ↦
          ((basis b ibc).repr : (a : W) → ι →₀ S)
            ((ε : (a : V) → W) (HSMul.hSMul (β := V) b_1 ((b : (a : ι) → V) a : V))) :
        (a : ι) → S)
      i :
    S)
| (((((basis b ibc).repr : (a : W) → ι →₀ S) ((ε : (a : V) → W) v) : ι →₀ S) : (a : ι) → S) i : S)

Tactic:
rw [← b.linearCombination_repr v, Finsupp.linearCombination_apply,
    map_finsuppSum, map_finsuppSum]

Premises used: Finsupp.linearCombination_apply, Module.Basis.linearCombination_repr, map_finsuppSum
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
V : Type u_3
inst_3 : AddCommMonoid V
inst_4 : Module R V
W : Type u_4
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
conv_lhs :
  Eq.{u_2 + 1} (α := S)
    ((Finsupp.sum ((b.repr : (a : V) → ι →₀ R) v) fun (a : ι) (b_1 : R) ↦
            ((basis b ibc).repr : (a : W) → ι →₀ S)
              ((ε : (a : V) → W) (HSMul.hSMul (β := V) b_1 ((b : (a : ι) → V) a : V))) :
          (a : ι) → S)
        i :
      S)
    ((algebraMap R S : (a : R) → S) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R) : S)
⊢ Eq.{u_2 + 1} (α := S) (((((basis b ibc).repr : (a : W) → ι →₀ S) ((ε : (a : V) → W) v) : ι →₀ S) : (a : ι) → S) i : S)
    ((algebraMap R S : (a : R) → S) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R) : S)

Tactic:
conv_lhs => rw [← b.linearCombination_repr v, Finsupp.linearCombination_apply,
    map_finsuppSum, map_finsuppSum]

Premises used: Finsupp.linearCombination_apply, Module.Basis.linearCombination_repr, map_finsuppSum
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
V : Type u_3
inst_3 : AddCommMonoid V
inst_4 : Module R V
W : Type u_4
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
simp :
  Eq.{u_2 + 1} (α := S)
    (Finsupp.sum ((b.repr : (a : V) → ι →₀ R) v) fun (a₁ : ι) (b_1 : R) ↦
        ((((basis b ibc).repr : (a : W) → ι →₀ S)
                (HSMul.hSMul (β := W) b_1 ((ε : (a : V) → W) ((b : (a : ι) → V) a₁ : V) : W)) :
              ι →₀ S) :
            (a : ι) → S)
          i :
      S)
    ((algebraMap R S : (a : R) → S) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R) : S)
⊢ Eq.{u_2 + 1} (α := S)
    ((Finsupp.sum ((b.repr : (a : V) → ι →₀ R) v) fun (a : ι) (b_1 : R) ↦
            ((basis b ibc).repr : (a : W) → ι →₀ S)
              ((ε : (a : V) → W) (HSMul.hSMul (β := V) b_1 ((b : (a : ι) → V) a : V))) :
          (a : ι) → S)
        i :
      S)
    ((algebraMap R S : (a : R) → S) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R) : S)

Tactic:
simp only [map_smul, Finsupp.sum_apply]

Premises used: Finsupp.sum_apply, map_smul
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
V : Type u_3
inst_3 : AddCommMonoid V
inst_4 : Module R V
W : Type u_4
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
rw :
  Eq.{u_2 + 1} (α := S)
    (((((basis b ibc).repr : (a : W) → ι →₀ S)
              (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := W)
                ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R)
                ((ε : (a : V) → W) ((b : (a : ι) → V) i : V) : W)) :
            ι →₀ S) :
          (a : ι) → S)
        i :
      S)
    ((algebraMap R S : (a : R) → S) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R) : S)
h₀ :
  ∀ (b_1 : ι),
    Ne.{u_1 + 1} (α := R) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) b_1 : R) (0 : R) →
      b_1 ≠ i →
        Eq.{u_2 + 1} (α := S)
          (((((basis b ibc).repr : (a : W) → ι →₀ S)
                    (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := W)
                      ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) b_1 : R)
                      ((ε : (a : V) → W) ((b : (a : ι) → V) b_1 : V) : W)) :
                  ι →₀ S) :
                (a : ι) → S)
              i :
            S)
          (0 : S)
h₁ :
  Eq.{u_1 + 1} (α := R) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R) (0 : R) →
    Eq.{u_2 + 1} (α := S)
      (((((basis b ibc).repr : (a : W) → ι →₀ S)
                (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := W) 0 ((ε : (a : V) → W) ((b : (a : ι) → V) i : V) : W)) :
              ι →₀ S) :
            (a : ι) → S)
          i :
        S)
      (0 : S)
⊢ Eq.{u_2 + 1} (α := S)
    (Finsupp.sum ((b.repr : (a : V) → ι →₀ R) v) fun (a₁ : ι) (b_1 : R) ↦
        ((((basis b ibc).repr : (a : W) → ι →₀ S)
                (HSMul.hSMul (β := W) b_1 ((ε : (a : V) → W) ((b : (a : ι) → V) a₁ : V) : W)) :
              ι →₀ S) :
            (a : ι) → S)
          i :
      S)
    ((algebraMap R S : (a : R) → S) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R) : S)

Tactic:
rw [Finsupp.sum_eq_single i]

Premises used: Finsupp.sum_eq_single
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
V : Type u_3
inst_3 : AddCommMonoid V
inst_4 : Module R V
W : Type u_4
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
rw :
  Eq.{u_2 + 1} (α := S)
    ((HSMul.hSMul (α := S) (β := ι →₀ S)
            ((algebraMap R S : (a : R) → S) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R) : S)
            (((basis b ibc).repr : (a : W) → ι →₀ S) ((basis b ibc : (a : ι) → W) i) : ι →₀ S) :
          (a : ι) → S)
        i :
      S)
    ((algebraMap R S : (a : R) → S) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R) : S)
⊢ Eq.{u_2 + 1} (α := S)
    (((((basis b ibc).repr : (a : W) → ι →₀ S)
              (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := W)
                ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R)
                ((ε : (a : V) → W) ((b : (a : ι) → V) i : V) : W)) :
            ι →₀ S) :
          (a : ι) → S)
        i :
      S)
    ((algebraMap R S : (a : R) → S) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R) : S)

Tactic:
rw [← IsScalarTower.algebraMap_smul S (b.repr v i) (ε (b i)),
      map_smul, ← ibc.basis_apply]

Premises used: Module.Basis.repr, IsScalarTower.algebraMap_smul, IsBaseChange.basis_apply, DFunLike.coe, map_smul
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
V : Type u_3
inst_3 : AddCommMonoid V
inst_4 : Module R V
W : Type u_4
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ Eq.{u_2 + 1} (α := S)
    ((HSMul.hSMul (α := S) (β := ι →₀ S)
            ((algebraMap R S : (a : R) → S) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R) : S)
            (((basis b ibc).repr : (a : W) → ι →₀ S) ((basis b ibc : (a : ι) → W) i) : ι →₀ S) :
          (a : ι) → S)
        i :
      S)
    ((algebraMap R S : (a : R) → S) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R) : S)

Tactic:
simp [Finsupp.single_eq_same, Algebra.algebraMap_eq_smul_one]

Premises used: Finsupp.single_eq_same, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
V : Type u_3
inst_3 : AddCommMonoid V
inst_4 : Module R V
W : Type u_4
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i i' : ι
h₀ :
  Ne.{u_1 + 1} (α := R) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i' : R) (0 : R) →
    i' ≠ i →
      Eq.{u_2 + 1} (α := S)
        (((((basis b ibc).repr : (a : W) → ι →₀ S)
                  (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := W)
                    ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i' : R)
                    ((ε : (a : V) → W) ((b : (a : ι) → V) i' : V) : W)) :
                ι →₀ S) :
              (a : ι) → S)
            i :
          S)
        (0 : S)
⊢ Ne.{u_1 + 1} (α := R) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i' : R) (0 : R) →
    i' ≠ i →
      Eq.{u_2 + 1} (α := S)
        (((((basis b ibc).repr : (a : W) → ι →₀ S)
                  (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := W)
                    ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i' : R)
                    ((ε : (a : V) → W) ((b : (a : ι) → V) i' : V) : W)) :
                ι →₀ S) :
              (a : ι) → S)
            i :
          S)
        (0 : S)

Tactic:
_
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
V : Type u_3
inst_3 : AddCommMonoid V
inst_4 : Module R V
W : Type u_4
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i i' : ι
h_1 : Ne.{u_1 + 1} (α := R) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i' : R) (0 : R)
h : i' ≠ i
h₀ :
  Eq.{u_2 + 1} (α := S)
    ((HSMul.hSMul (α := S) (β := ι →₀ S)
            ((algebraMap R S : (a : R) → S) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i' : R) : S)
            (((basis b ibc).repr : (a : W) → ι →₀ S) ((basis b ibc : (a : ι) → W) i') : ι →₀ S) :
          (a : ι) → S)
        i :
      S)
    (0 : S)
⊢ Eq.{u_2 + 1} (α := S)
    (((((basis b ibc).repr : (a : W) → ι →₀ S)
              (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := W)
                ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i' : R)
                ((ε : (a : V) → W) ((b : (a : ι) → V) i' : V) : W)) :
            ι →₀ S) :
          (a : ι) → S)
        i :
      S)
    (0 : S)

Tactic:
rw [← IsScalarTower.algebraMap_smul S (b.repr v i') (ε (b i')), map_smul,
      ← ibc.basis_apply]

Premises used: Module.Basis.repr, IsScalarTower.algebraMap_smul, IsBaseChange.basis_apply, DFunLike.coe, map_smul
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
V : Type u_3
inst_3 : AddCommMonoid V
inst_4 : Module R V
W : Type u_4
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i i' : ι
h_1 : Ne.{u_1 + 1} (α := R) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i' : R) (0 : R)
h : i' ≠ i
⊢ Eq.{u_2 + 1} (α := S)
    ((HSMul.hSMul (α := S) (β := ι →₀ S)
            ((algebraMap R S : (a : R) → S) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i' : R) : S)
            (((basis b ibc).repr : (a : W) → ι →₀ S) ((basis b ibc : (a : ι) → W) i') : ι →₀ S) :
          (a : ι) → S)
        i :
      S)
    (0 : S)

Tactic:
simp [Finsupp.single_eq_of_ne (Ne.symm h)]

Premises used: Finsupp.single_eq_of_ne, Ne.symm
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
V : Type u_3
inst_3 : AddCommMonoid V
inst_4 : Module R V
W : Type u_4
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ Eq.{u_1 + 1} (α := R) ((((b.repr : (a : V) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R) (0 : R) →
    Eq.{u_2 + 1} (α := S)
      (((((basis b ibc).repr : (a : W) → ι →₀ S)
                (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := W) 0 ((ε : (a : V) → W) ((b : (a : ι) → V) i : V) : W)) :
              ι →₀ S) :
            (a : ι) → S)
          i :
        S)
      (0 : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
V : Type u_3
inst_3 : AddCommMonoid V
inst_4 : Module R V
W : Type u_4
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
h :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := S)
      (((((basis b ibc).repr : (a : W) → ι →₀ S) ((ε : (a : V) → W) v) : ι →₀ S) : (a : ι) → S) i : S)
      ((((Finsupp.mapRange.linearMap (Algebra.linearMap R S) : (a : ι →₀ R) → ι →₀ S) ((b.repr : (a : V) → ι →₀ R) v) :
              ι →₀ S) :
            (a : ι) → S)
          i :
        S)
⊢ Eq (α := ι →₀ S) (((basis b ibc).repr : (a : W) → ι →₀ S) ((ε : (a : V) → W) v) : ι →₀ S)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap R S) : (a : ι →₀ R) → ι →₀ S) ((b.repr : (a : V) → ι →₀ R) v) :
      ι →₀ S)

Tactic:
ext i
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
V : Type u_3
inst_3 : AddCommMonoid V
inst_4 : Module R V
W : Type u_4
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ Eq.{u_2 + 1} (α := S) (((((basis b ibc).repr : (a : W) → ι →₀ S) ((ε : (a : V) → W) v) : ι →₀ S) : (a : ι) → S) i : S)
    ((((Finsupp.mapRange.linearMap (Algebra.linearMap R S) : (a : ι →₀ R) → ι →₀ S) ((b.repr : (a : V) → ι →₀ R) v) :
            ι →₀ S) :
          (a : ι) → S)
        i :
      S)

Tactic:
simp [basis_repr_comp_apply]

Premises used: IsBaseChange.basis_repr_comp_apply
-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
V : Type u_3
inst_3 : AddCommMonoid V
inst_4 : Module R V
W : Type u_4
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : IsScalarTower R S W
ε : V →ₗ[R] W
ibc : IsBaseChange S ε
inst_9 : Module.Free R V
⊢ Module.Free S W

Tactic:
Module.Free.of_basis (ibc.basis (Module.Free.chooseBasis R V))

Premises used: Module.Free.of_basis, IsBaseChange.basis, Module.Free.chooseBasis
-- 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 ι
⊢ IsBaseChange (M := ι →₀ A) (N := V) R (Finsupp.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
j : R ⊗[A] (ι →₀ A) ≃ₗ[R] ι →₀ R := finsuppScalarRight A R R ι
refine_1 : R ⊗[A] (ι →₀ A) ≃ₗ[R] V
refine_2 :
  ∀ (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:
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
j : R ⊗[A] (ι →₀ A) ≃ₗ[R] ι →₀ R := finsuppScalarRight A R R ι
refine_1 :
  Function.Bijective (α := R ⊗[A] (ι →₀ A)) (β := V)
    (⇑(Finsupp.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 (Finsupp.linearCombination R b ∘ₗ j)

Premises used: LinearMap.comp, Finsupp.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
j : R ⊗[A] (ι →₀ A) ≃ₗ[R] ι →₀ R := finsuppScalarRight A R R ι
refine_1 :
  Function.Bijective (α := ι →₀ R) (β := V) (⇑(Finsupp.linearCombination R (⇑b : (a : ι) → V)) : (a : ι →₀ R) → V)
⊢ Function.Bijective (α := R ⊗[A] (ι →₀ A)) (β := V)
    (⇑(Finsupp.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
j : R ⊗[A] (ι →₀ A) ≃ₗ[R] ι →₀ R := finsuppScalarRight A R R ι
⊢ Function.Bijective (α := ι →₀ R) (β := V) (⇑(Finsupp.linearCombination R (⇑b : (a : ι) → V)) : (a : ι →₀ R) → V)

Tactic:
simp [Function.Bijective,
        ← span_range_eq_top_iff_surjective_finsuppLinearCombination,
        ← linearIndependent_iff_injective_finsuppLinearCombination,
        Module.Basis.span_eq, b.linearIndependent]

Premises used: linearIndependent_iff_injective_finsuppLinearCombination, Module.Basis.linearIndependent, Function.Bijective, span_range_eq_top_iff_surjective_finsuppLinearCombination, 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
j : R ⊗[A] (ι →₀ A) ≃ₗ[R] ι →₀ R := finsuppScalarRight A R R ι
x : ι →₀ A
⊢ Eq.{u_1 + 1} (α := R) ((algebraMap A R : (a : A) → R) 0 : R) (0 : R)

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
j : R ⊗[A] (ι →₀ A) ≃ₗ[R] ι →₀ R := finsuppScalarRight A R R ι
x : ι →₀ A
this :
  Eq (α := ι →₀ R) ((j : (a : R ⊗[A] (ι →₀ A)) → ι →₀ R) (1 ⊗ₜ[A] x) : ι →₀ R)
    (Finsupp.mapRange (⇑(algebraMap A R) : (a : A) → R) ⋯ x : ι →₀ R)
⊢ 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)

Tactic:
simp [this, Finsupp.linearCombination_apply, Finsupp.sum_mapRange_index]

Premises used: Finsupp.linearCombination_apply, Finsupp.sum_mapRange_index
-- 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
refine_2 :
  Eq (α := ι →₀ R) ((j : (a : R ⊗[A] (ι →₀ A)) → ι →₀ R) (1 ⊗ₜ[A] x) : ι →₀ R)
    (Finsupp.mapRange (⇑(algebraMap A R) : (a : A) → R) ⋯ x : ι →₀ R)
⊢ 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)

Tactic:
suffices (j (1 ⊗ₜ[A] x)) = x.mapRange (algebraMap A R) (by simp) by
      simp [this, Finsupp.linearCombination_apply, Finsupp.sum_mapRange_index]
-- 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
refine_2 :
  ∀ (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)
⊢ Eq (α := ι →₀ R) ((j : (a : R ⊗[A] (ι →₀ A)) → ι →₀ R) (1 ⊗ₜ[A] x) : ι →₀ R)
    (Finsupp.mapRange (⇑(algebraMap A R) : (a : A) → R) ⋯ x : ι →₀ R)

Tactic:
ext i