awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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)
h₁₃ h₁₄ : Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] s) (1 ⊗ₜ[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)

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]

Premises used: TensorProduct.smul_tmul, Algebra.TensorProduct.map_tmul, sub_eq_zero, Algebra.linearMap, map_one, Iff.mp, Algebra.smul_def, smul_eq_mul, mul_one, OfNat.ofNat, Algebra.coe_linearMap, Eq.symm, DFunLike.coe, Algebra.TensorProduct.includeLeftSubRight_apply, Algebra.TensorProduct.lid_symm_apply, Eq.trans, AlgHom.id_apply
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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

Tactic:
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 ‹_›

Premises used: Algebra.IsEffective, Module.FaithfullyFlat.lTensor_reflects_exact
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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))
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)))
⊢ IsEffective 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 ‹_›

Premises used: LinearMap.toAddMonoidHom, Iff.mpr, Function.bijective_id, TensorProduct.AlgebraTensorModule.distribBaseChange, AddEquiv.toAddMonoidHom, AddMonoidHom.id, Module.FaithfullyFlat.lTensor_reflects_exact, LinearEquiv.toLinearMap, TensorProduct, AlgEquiv.toAddEquiv, Algebra.TensorProduct.rid, LinearEquiv.injective, AlgEquiv.surjective, AddMonoidHom.exact_iff_of_surjective_of_bijective_of_injective
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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 :
  ∀ (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)
⊢ 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:
ext
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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
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)
⊢ 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:
simp [← Algebra.TensorProduct.linearMap_comp_rid]

Premises used: Algebra.TensorProduct.linearMap_comp_rid
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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) (((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:
rfl
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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_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))
⊢ 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:
ext
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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] 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:
simp
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
Goal:
R : Type u_3
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
⊢ IsEffective R S

Tactic:
of_isEffective_tensorProduct_of_faithfullyFlat _ _ _ (of_section (TensorProduct.lmul'' R))

Premises used: Algebra.IsEffective.of_section, Algebra.IsEffective.of_isEffective_tensorProduct_of_faithfullyFlat, Algebra.TensorProduct.lmul''
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : Ring S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
⊢ ∀ (x : R),
    Membership.mem (α := S) (γ := Subring (↑(CommRingCat.of S) : Type u))
      (RingHom.eqLocus (S :=
        (↑(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)) :
          Type u))
        (CommRingCat.Hom.hom (CategoryTheory.Limits.PushoutCocone.inl (CommRingCat.pushoutCocone R S S)))
        (CommRingCat.Hom.hom (CategoryTheory.Limits.PushoutCocone.inr (CommRingCat.pushoutCocone R S S))))
      ((algebraMap R S : (a : R) → S) x : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
⊢ 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:
RingHom.injective_codRestrict.mpr (FaithfulSMul.algebraMap_injective _ _)

Premises used: Iff.mpr, Set.Mem, RingHom.injective_codRestrict, setOf, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
⊢ 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:
codRestrictEqLocusPushoutCocone.injective_of_faithfulSMul _ _

Premises used: Algebra.codRestrictEqLocusPushoutCocone.injective_of_faithfulSMul
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
⊢ 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:
exact codRestrictEqLocusPushoutCocone.injective_of_faithfulSMul _ _

Premises used: Algebra.codRestrictEqLocusPushoutCocone.injective_of_faithfulSMul
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
⊢ Function.Surjective (α := 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:
codRestrictEqLocusPushoutCocone.surjective_of_isEffective _ _ (.of_faithfullyFlat R S)

Premises used: Algebra.IsEffective.of_faithfullyFlat, Algebra.codRestrictEqLocusPushoutCocone.surjective_of_isEffective
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.FaithfullyFlat R S
⊢ Function.Surjective (α := 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:
exact codRestrictEqLocusPushoutCocone.surjective_of_isEffective _ _ (.of_faithfullyFlat R S)

Premises used: Algebra.IsEffective.of_faithfullyFlat, Algebra.codRestrictEqLocusPushoutCocone.surjective_of_isEffective
-- 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 : ι
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 ⋯) : (a : ι →₀ S) → TensorProduct R S (ι →₀ R)) (Finsupp.single i 1)) :
          TensorProduct R S V) :
      W)
    ((ε : (a : V) → W) ((b : (a : ι) → V) i : V) : W)
⊢ Eq.{u_4 + 1} (α := W) ((basis b ibc : (a : ι) → W) i : 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]

Premises used: LinearEquiv.trans_apply, LinearEquiv.symm_symm, LinearEquiv.baseChange, Module.Basis.coe_ofRepr, LinearEquiv.trans_symm, IsBaseChange.basis
-- 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 : ι
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)
⊢ 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)

Tactic:
generalize_proofs _ _ _ _ ibcRA
-- 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))
⊢ 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]