awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Finsupp.sum_eq_single i]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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)
              (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)
have 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)
Tactic: rw [← IsScalarTower.algebraMap_smul S (b.repr v i) (ε (b i)),
      map_smul, ← ibc.basis_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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)
    (((((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)
have 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)
Tactic: rw [← IsScalarTower.algebraMap_smul S (b.repr v i') (ε (b i')), map_smul,
      ← ibc.basis_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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
⊢ 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)
have 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)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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))
have refine_1 : R ⊗[A] (ι →₀ A) ≃ₗ[R] V
Tactic: refine of_equiv ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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
⊢ IsBaseChange (M := ι →₀ A) (N := V) R (Finsupp.linearCombination A (⇑b : (a : ι) → V))
have refine_2 : ∀ (x : ι →₀ A),
  Eq.{u_2 + 1} (α := V)
    ((LinearEquiv.ofBijective (Finsupp.linearCombination R (⇑b : (a : ι) → V) ∘ₗ (↑j : R ⊗[A] (ι →₀ A) →ₗ[R] ι →₀ R))
            sorry :
          (a : R ⊗[A] (ι →₀ A)) → V)
        (1 ⊗ₜ[A] x) :
      V)
    ((Finsupp.linearCombination A (⇑b : (a : ι) → V) : (a : ι →₀ A) → V) x : V)
Tactic: refine of_equiv ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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 ι
⊢ R ⊗[A] (ι →₀ A) ≃ₗ[R] V
have 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)
Tactic: apply LinearEquiv.ofBijective (Finsupp.linearCombination R b ∘ₗ j)
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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 ⊗[A] (ι →₀ A)) (β := V)
    (⇑(Finsupp.linearCombination R (⇑b : (a : ι) → V) ∘ₗ (↑j : R ⊗[A] (ι →₀ A) →ₗ[R] ι →₀ R)) :
      (a : R ⊗[A] (ι →₀ A)) → V)
have refine_1 : Function.Bijective (α := ι →₀ R) (β := V) (⇑(Finsupp.linearCombination R (⇑b : (a : ι) → V)) : (a : ι →₀ R) → V)
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, j.bijective.of_comp_iff]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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_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)
have refine_2 : Eq (α := ι →₀ R) ((j : (a : R ⊗[A] (ι →₀ A)) → ι →₀ R) (1 ⊗ₜ[A] x) : ι →₀ R)
  (Finsupp.mapRange (⇑(algebraMap A R) : (a : A) → R) sorry x : ι →₀ R)
Tactic: suffices (j (1 ⊗ₜ[A] x)) = x.mapRange (algebraMap A R) (by simp) by
      simp [this, Finsupp.linearCombination_apply, Finsupp.sum_mapRange_index]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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 (α := ι →₀ R) ((j : (a : R ⊗[A] (ι →₀ A)) → ι →₀ R) (1 ⊗ₜ[A] x) : ι →₀ R)
    (Finsupp.mapRange (⇑(algebraMap A R) : (a : A) → R) ⋯ x : ι →₀ R)
have 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) sorry x : (a : ι) → R) i : R)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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))
⊢ IsBaseChange (M := ι →₀ A) (N := V) R (Finsupp.linearCombination A (⇑b : (a : ι) → V))
have refine_1 : R ⊗[A] (ι →₀ A) ≃ₗ[R] 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]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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
⊢ IsBaseChange (M := ι →₀ A) (N := V) R (Finsupp.linearCombination A (⇑b : (a : ι) → V))
have 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))
            sorry :
          (a : R ⊗[A] (ι →₀ A)) → V)
        (1 ⊗ₜ[A] x) :
      V)
    ((Finsupp.linearCombination A (⇑b : (a : ι) → V) : (a : ι →₀ A) → V) x : 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]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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 ι
⊢ IsBaseChange (M := ι → A) (N := V) R (Fintype.linearCombination A (⇑b : (a : ι) → V))
have have : ∀ (this : DecidableEq ι), IsBaseChange (M := ι → A) (N := V) R (Fintype.linearCombination A (⇑b : (a : ι) → V))
Tactic: have : DecidableEq ι := Classical.typeDecidableEq ι
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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))
have refine_1 : R ⊗[A] (ι → A) ≃ₗ[R] V
Tactic: refine of_equiv ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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
⊢ IsBaseChange (M := ι → A) (N := V) R (Fintype.linearCombination A (⇑b : (a : ι) → V))
have refine_2 : ∀ (x : ι → A),
  Eq.{u_2 + 1} (α := V)
    ((LinearEquiv.ofBijective (Fintype.linearCombination R (⇑b : (a : ι) → V) ∘ₗ (↑j : R ⊗[A] (ι → A) →ₗ[R] ι → R)) sorry :
          (a : R ⊗[A] (ι → A)) → V)
        (1 ⊗ₜ[A] x) :
      V)
    ((Fintype.linearCombination A (⇑b : (a : ι) → V) : (a : ι → A) → V) x : V)
Tactic: refine of_equiv ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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 ι
⊢ R ⊗[A] (ι → A) ≃ₗ[R] V
have 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)
Tactic: apply LinearEquiv.ofBijective (Fintype.linearCombination R b ∘ₗ j)
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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 ⊗[A] (ι → A)) (β := V)
    (⇑(Fintype.linearCombination R (⇑b : (a : ι) → V) ∘ₗ (↑j : R ⊗[A] (ι → A) →ₗ[R] ι → R)) : (a : R ⊗[A] (ι → A)) → V)
have refine_1 : Function.Bijective (α := ι → R) (β := V) (⇑(Fintype.linearCombination R (⇑b : (a : ι) → V)) : (a : ι → R) → V)
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, j.bijective.of_comp_iff]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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
⊢ 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)
have 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))
Tactic: simp only [LinearEquiv.ofBijective_apply, LinearMap.coe_comp, LinearEquiv.coe_coe,
      Function.comp_apply, Fintype.linearCombination_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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
⊢ 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))
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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
⊢ 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)
have 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)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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) ((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)
have 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)
Tactic: rw [TensorProduct.piScalarRight_apply, TensorProduct.piScalarRightHom_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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
⊢ (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)
have 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
Tactic: rw [← LinearEquiv.symm_apply_eq]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (goal)
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
⊢ (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
have 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
Tactic: rw [Fintype.linearCombination_apply, b.equivFun_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S P
inst_10 : IsScalarTower R S P
ε : N →ₗ[R] P
x y : S
⊢ 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 ε)
have 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)
Tactic: ext