awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
g : S →ₐ[R] R
s : S
hs : Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
h :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
h₁ :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
h₂ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₃ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₄ : Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((g : (a : S) → R) s : R) 1) (1 ⊗ₜ[R] s)
h₅ : Eq (α := R ⊗[R] S) (HSMul.hSMul (α := R) (β := R) ((g : (a : S) → R) s : R) 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)
h₆ : Eq (α := R ⊗[R] S) (HMul.hMul (α := R) (β := R) ((g : (a : S) → R) s : R) (1 : R) ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)
h₇ : Eq (α := R ⊗[R] S) ((g : (a : S) → R) s ⊗ₜ[R] 1 : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
h₈ : Eq (α := R ⊗[R] S) ((g : (a : S) → R) s ⊗ₜ[R] (AlgHom.id R S : (a : S) → S) 1 : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
h₉ :
  Eq (α := R ⊗[R] S)
    (((TensorProduct.map g (AlgHom.id R S) : S ⊗[R] S →ₐ[R] R ⊗[R] S) : (a : S ⊗[R] S) → R ⊗[R] S) (s ⊗ₜ[R] 1) :
      R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
h₁₀ :
  Eq (α := R ⊗[R] S)
    (((TensorProduct.map g (AlgHom.id R S) : S ⊗[R] S →ₐ[R] R ⊗[R] S) : (a : S ⊗[R] S) → R ⊗[R] S) (1 ⊗ₜ[R] s) :
      R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
h₁₁ : Eq (α := R ⊗[R] S) ((g : (a : S) → R) 1 ⊗ₜ[R] (AlgHom.id R S : (a : S) → S) s : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
h₁₂ : Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (AlgHom.id R S : (a : S) → S) s : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
⊢ Eq (α := R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S)
        ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R)) :
      R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
have h₁₃ : Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] s) (1 ⊗ₜ[R] s)
Tactic: rw [TensorProduct.lid_symm_apply, TensorProduct.lid_symm_apply,
    ← mul_one ((Algebra.linearMap R S) _), Algebra.coe_linearMap, ← Algebra.smul_def,
    ← TensorProduct.smul_tmul, smul_eq_mul, mul_one, ← AlgHom.id_apply (R := R) (1 : S),
    ← TensorProduct.map_tmul,
    sub_eq_zero.mp ((TensorProduct.includeLeftSubRight_apply s).symm.trans hs),
    TensorProduct.map_tmul, map_one, AlgHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_3
inst : CommRing R
S : Type u_4
T : Type u_5
inst_1 : CommRing T
inst_2 : Algebra R T
inst_3 : Ring S
inst_4 : Algebra R S
inst_5 : Module.FaithfullyFlat R T
h : IsEffective T (T ⊗[R] S)
⊢ IsEffective R S
have refine_1 : Eq (α := T ⊗[R] R →+ T ⊗[R] S)
  (AddMonoidHom.comp (↑(Algebra.linearMap T (T ⊗[R] S)) : T →+ T ⊗[R] S)
    (AddEquiv.toAddMonoidHom (AlgEquiv.toAddEquiv (TensorProduct.rid R R T : T ⊗[R] R ≃ₐ[R] T))))
  (AddMonoidHom.comp (AddMonoidHom.id (T ⊗[R] S))
    (↑(LinearMap.lTensor T (Algebra.linearMap R S)) : T ⊗[R] R →+ T ⊗[R] S))
Tactic: refine Module.FaithfullyFlat.lTensor_reflects_exact _ _ _ _ <|
    AddMonoidHom.exact_iff_of_surjective_of_bijective_of_injective
      ((Algebra.linearMap R S).lTensor T) ((TensorProduct.includeLeftSubRight R S).lTensor T)
      (Algebra.linearMap T (T ⊗[R] S)) (TensorProduct.includeLeftSubRight T (T ⊗[R] S))
      (TensorProduct.rid R R T).toAddMonoidHom (AddMonoidHom.id (T ⊗[R] S))
      (TensorProduct.AlgebraTensorModule.distribBaseChange R T S S).toAddMonoidHom ?_ ?_
      (TensorProduct.rid R R T).surjective Function.bijective_id
      ((TensorProduct.AlgebraTensorModule.distribBaseChange R T S S).injective) |>.mpr ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_3
inst : CommRing R
S : Type u_4
T : Type u_5
inst_1 : CommRing T
inst_2 : Algebra R T
inst_3 : Ring S
inst_4 : Algebra R S
inst_5 : Module.FaithfullyFlat R T
h : IsEffective T (T ⊗[R] S)
refine_1 :
  Eq (α := T ⊗[R] R →+ T ⊗[R] S)
    (AddMonoidHom.comp (↑(Algebra.linearMap T (T ⊗[R] S)) : T →+ T ⊗[R] S)
      (AddEquiv.toAddMonoidHom (AlgEquiv.toAddEquiv (TensorProduct.rid R R T : T ⊗[R] R ≃ₐ[R] T))))
    (AddMonoidHom.comp (AddMonoidHom.id (T ⊗[R] S))
      (↑(LinearMap.lTensor T (Algebra.linearMap R S)) : T ⊗[R] R →+ T ⊗[R] S))
⊢ IsEffective R S
have refine_2 : Eq (α := T ⊗[R] S →+ T ⊗[R] S ⊗[T] (T ⊗[R] S))
  (AddMonoidHom.comp (↑(TensorProduct.includeLeftSubRight T (T ⊗[R] S)) : T ⊗[R] S →+ T ⊗[R] S ⊗[T] (T ⊗[R] S))
    (AddMonoidHom.id (T ⊗[R] S)))
  (AddMonoidHom.comp
    (LinearMap.toAddMonoidHom
      (↑(TensorProduct.AlgebraTensorModule.distribBaseChange R T S S) :
        T ⊗[R] (S ⊗[R] S) →ₗ[T] T ⊗[R] S ⊗[T] (T ⊗[R] S)))
    (↑(LinearMap.lTensor T (TensorProduct.includeLeftSubRight R S)) : T ⊗[R] S →+ T ⊗[R] (S ⊗[R] S)))
Tactic: refine Module.FaithfullyFlat.lTensor_reflects_exact _ _ _ _ <|
    AddMonoidHom.exact_iff_of_surjective_of_bijective_of_injective
      ((Algebra.linearMap R S).lTensor T) ((TensorProduct.includeLeftSubRight R S).lTensor T)
      (Algebra.linearMap T (T ⊗[R] S)) (TensorProduct.includeLeftSubRight T (T ⊗[R] S))
      (TensorProduct.rid R R T).toAddMonoidHom (AddMonoidHom.id (T ⊗[R] S))
      (TensorProduct.AlgebraTensorModule.distribBaseChange R T S S).toAddMonoidHom ?_ ?_
      (TensorProduct.rid R R T).surjective Function.bijective_id
      ((TensorProduct.AlgebraTensorModule.distribBaseChange R T S S).injective) |>.mpr ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_3
inst : CommRing R
S : Type u_4
T : Type u_5
inst_1 : CommRing T
inst_2 : Algebra R T
inst_3 : Ring S
inst_4 : Algebra R S
inst_5 : Module.FaithfullyFlat R T
h : IsEffective T (T ⊗[R] S)
⊢ Eq (α := T ⊗[R] R →+ T ⊗[R] S)
    (AddMonoidHom.comp (↑(Algebra.linearMap T (T ⊗[R] S)) : T →+ T ⊗[R] S)
      (AddEquiv.toAddMonoidHom (AlgEquiv.toAddEquiv (TensorProduct.rid R R T : T ⊗[R] R ≃ₐ[R] T))))
    (AddMonoidHom.comp (AddMonoidHom.id (T ⊗[R] S))
      (↑(LinearMap.lTensor T (Algebra.linearMap R S)) : T ⊗[R] R →+ T ⊗[R] S))
have refine_1 : ∀ (x : T ⊗[R] R),
  Eq (α := T ⊗[R] S)
    ((AddMonoidHom.comp (↑(Algebra.linearMap T (T ⊗[R] S)) : T →+ T ⊗[R] S)
            (AddEquiv.toAddMonoidHom (AlgEquiv.toAddEquiv (TensorProduct.rid R R T : T ⊗[R] R ≃ₐ[R] T))) :
          (a : T ⊗[R] R) → T ⊗[R] S)
        x :
      T ⊗[R] S)
    ((AddMonoidHom.comp (AddMonoidHom.id (T ⊗[R] S))
            (↑(LinearMap.lTensor T (Algebra.linearMap R S)) : T ⊗[R] R →+ T ⊗[R] S) :
          (a : T ⊗[R] R) → T ⊗[R] S)
        x :
      T ⊗[R] S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_3
inst : CommRing R
S : Type u_4
T : Type u_5
inst_1 : CommRing T
inst_2 : Algebra R T
inst_3 : Ring S
inst_4 : Algebra R S
inst_5 : Module.FaithfullyFlat R T
h : IsEffective T (T ⊗[R] S)
x : T ⊗[R] R
⊢ Eq (α := T ⊗[R] S)
    ((AddMonoidHom.comp (↑(Algebra.linearMap T (T ⊗[R] S)) : T →+ T ⊗[R] S)
            (AddEquiv.toAddMonoidHom (AlgEquiv.toAddEquiv (TensorProduct.rid R R T : T ⊗[R] R ≃ₐ[R] T))) :
          (a : T ⊗[R] R) → T ⊗[R] S)
        x :
      T ⊗[R] S)
    ((AddMonoidHom.comp (AddMonoidHom.id (T ⊗[R] S))
            (↑(LinearMap.lTensor T (Algebra.linearMap R S)) : T ⊗[R] R →+ T ⊗[R] S) :
          (a : T ⊗[R] R) → T ⊗[R] S)
        x :
      T ⊗[R] S)
have refine_1 : Eq (α := T ⊗[R] S) (((TensorProduct.rid R R T : T ⊗[R] R ≃ₐ[R] T) : (a : T ⊗[R] R) → T) x ⊗ₜ[R] 1 : T ⊗[R] S)
  (((TensorProduct.AlgebraTensorModule.rid R R T : T ⊗[R] R ≃ₗ[R] T) : (a : T ⊗[R] R) → T) x ⊗ₜ[R] 1 : T ⊗[R] S)
Tactic: simp [← Algebra.TensorProduct.linearMap_comp_rid]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_3
inst : CommRing R
S : Type u_4
T : Type u_5
inst_1 : CommRing T
inst_2 : Algebra R T
inst_3 : Ring S
inst_4 : Algebra R S
inst_5 : Module.FaithfullyFlat R T
h : IsEffective T (T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S →+ T ⊗[R] S ⊗[T] (T ⊗[R] S))
    (AddMonoidHom.comp (↑(TensorProduct.includeLeftSubRight T (T ⊗[R] S)) : T ⊗[R] S →+ T ⊗[R] S ⊗[T] (T ⊗[R] S))
      (AddMonoidHom.id (T ⊗[R] S)))
    (AddMonoidHom.comp
      (LinearMap.toAddMonoidHom
        (↑(TensorProduct.AlgebraTensorModule.distribBaseChange R T S S) :
          T ⊗[R] (S ⊗[R] S) →ₗ[T] T ⊗[R] S ⊗[T] (T ⊗[R] S)))
      (↑(LinearMap.lTensor T (TensorProduct.includeLeftSubRight R S)) : T ⊗[R] S →+ T ⊗[R] (S ⊗[R] S)))
have refine_2 : ∀ (x : T ⊗[R] S),
  Eq (α := T ⊗[R] S ⊗[T] (T ⊗[R] S))
    ((AddMonoidHom.comp (↑(TensorProduct.includeLeftSubRight T (T ⊗[R] S)) : T ⊗[R] S →+ T ⊗[R] S ⊗[T] (T ⊗[R] S))
            (AddMonoidHom.id (T ⊗[R] S)) :
          (a : T ⊗[R] S) → T ⊗[R] S ⊗[T] (T ⊗[R] S))
        x :
      T ⊗[R] S ⊗[T] (T ⊗[R] S))
    ((AddMonoidHom.comp
            (LinearMap.toAddMonoidHom
              (↑(TensorProduct.AlgebraTensorModule.distribBaseChange R T S S) :
                T ⊗[R] (S ⊗[R] S) →ₗ[T] T ⊗[R] S ⊗[T] (T ⊗[R] S)))
            (↑(LinearMap.lTensor T (TensorProduct.includeLeftSubRight R S)) : T ⊗[R] S →+ T ⊗[R] (S ⊗[R] S)) :
          (a : T ⊗[R] S) → T ⊗[R] S ⊗[T] (T ⊗[R] S))
        x :
      T ⊗[R] S ⊗[T] (T ⊗[R] S))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
⊢ Function.Bijective (α := R) (β :=
    (↑(CategoryTheory.Limits.Cone.pt (F :=
          CategoryTheory.Limits.parallelPair (X := CommRingCat.of S) (Y :=
            CategoryTheory.Limits.Cocone.pt (F :=
              CategoryTheory.Limits.span (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
                (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (CommRingCat.pushoutCocone R S S))
            (CategoryTheory.Limits.PushoutCocone.inl (CommRingCat.pushoutCocone R S S))
            (CategoryTheory.Limits.PushoutCocone.inr (CommRingCat.pushoutCocone R S S)))
          (CommRingCat.equalizerFork (CategoryTheory.Limits.PushoutCocone.inl (CommRingCat.pushoutCocone R S S))
            (CategoryTheory.Limits.PushoutCocone.inr (CommRingCat.pushoutCocone R S S)))) :
      Type u))
    (⇑(codRestrictEqLocusPushoutCocone R S) :
      (a : R) →
        (↑(CommRingCat.equalizerFork (CommRingCat.pushoutCocone R S S).inl (CommRingCat.pushoutCocone R S S).inr).pt :
          Type u))
have left : Function.Injective (α := R) (β :=
  (↑(CategoryTheory.Limits.Cone.pt (F :=
        CategoryTheory.Limits.parallelPair (X := CommRingCat.of S) (Y :=
          CategoryTheory.Limits.Cocone.pt (F :=
            CategoryTheory.Limits.span (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
              (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
            (CommRingCat.pushoutCocone R S S))
          (CategoryTheory.Limits.PushoutCocone.inl (CommRingCat.pushoutCocone R S S))
          (CategoryTheory.Limits.PushoutCocone.inr (CommRingCat.pushoutCocone R S S)))
        (CommRingCat.equalizerFork (CategoryTheory.Limits.PushoutCocone.inl (CommRingCat.pushoutCocone R S S))
          (CategoryTheory.Limits.PushoutCocone.inr (CommRingCat.pushoutCocone R S S)))) :
    Type u))
  (⇑(codRestrictEqLocusPushoutCocone R S) :
    (a : R) →
      (↑(CommRingCat.equalizerFork (CommRingCat.pushoutCocone R S S).inl (CommRingCat.pushoutCocone R S S).inr).pt :
        Type u))
Tactic: constructor
-- 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 ε
i : ι
⊢ Eq.{u_4 + 1} (α := W) ((basis b ibc : (a : ι) → W) i : W) ((ε : (a : V) → W) ((b : (a : ι) → V) i : V) : W)
have simp : 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)
          ((LinearEquiv.symm (equiv sorry) : (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 only [basis, LinearEquiv.baseChange, Module.Basis.coe_ofRepr, LinearEquiv.trans_symm,
    LinearEquiv.symm_symm, LinearEquiv.trans_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 ε
i : ι
⊢ 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)
            ((LinearEquiv.symm (equiv ⋯) : (a : ι →₀ S) → TensorProduct R S (ι →₀ R)) (Finsupp.single i 1)) :
          TensorProduct R S V) :
      W)
    ((ε : (a : V) → W) ((b : (a : ι) → V) i : V) : W)
have generalize_proofs : ∀ (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))),
  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: generalize_proofs _ _ _ _ ibcRA
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeFree (hypothesis)
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))
⊢ 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)
have 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))
Tactic: have : ibcRA.equiv.symm (Finsupp.single i 1) = 1 ⊗ₜ (Finsupp.single i 1) := by
    simp [LinearEquiv.symm_apply_eq, IsBaseChange.equiv_tmul]
-- 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 : ι
| (((((basis b ibc).repr : (a : W) → ι →₀ S) ((ε : (a : V) → W) v) : ι →₀ S) : (a : ι) → S) i : S)
have 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)
Tactic: rw [← b.linearCombination_repr v, Finsupp.linearCombination_apply,
    map_finsuppSum, map_finsuppSum]
-- 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) ((ε : (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)
have 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)
Tactic: conv_lhs => rw [← b.linearCombination_repr v, Finsupp.linearCombination_apply,
    map_finsuppSum, map_finsuppSum]
-- 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)
    ((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)
have 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)
Tactic: simp only [map_smul, Finsupp.sum_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 : ι
⊢ 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 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)
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 : ι
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)
⊢ 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₀ : ∀ (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)
Tactic: rw [Finsupp.sum_eq_single i]