awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M_1 : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M_1
inst_2 : Module R M_1
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
ι : Type v
M : ι → Type w
inst_9 : (i : ι) → AddCommMonoid (M i)
inst_10 : (i : ι) → Module.{u, w} R (M i)
inst_11 : ∀ (i : ι), Flat.{u, w} R (M i)
⊢ Flat R (Π₀ (i : ι), M i)

Tactic:
dfinsupp_iff.mpr ‹_›

Premises used: Iff.mpr, Module.Flat.dfinsupp_iff
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
ι : Type v
⊢ Flat R (ι →₀ R)

Tactic:
of_linearEquiv (finsuppLEquivDirectSum R R ι)

Premises used: finsuppLEquivDirectSum, Module.Flat.of_linearEquiv
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
ι : Type v
⊢ Flat R (ι →₀ R)

Tactic:
exact of_linearEquiv (finsuppLEquivDirectSum R R ι)

Premises used: finsuppLEquivDirectSum, Module.Flat.of_linearEquiv
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
ι : Type v
⊢ Flat R (ι →₀ R)

Tactic:
classical exact of_linearEquiv (finsuppLEquivDirectSum R R ι)
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
inst_9 : Projective R M
⊢ Flat R M

Tactic:
have ⟨e, he⟩:= Module.projective_def'.mp ‹_›
  of_retract _ _ he

Premises used: id, _private.0.Module.Flat.of_projective.match_1, Module.Flat, Module.Flat.of_retract, Module.projective_def', Iff.mp, Finsupp.linearCombination
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
inst_9 : Free R M
⊢ Flat R M

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P_1 : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P_1
inst_6 : Module R P_1
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
S : Type u_4
inst_9 : CommSemiring S
inst_10 : Algebra R S
inst_11 : Module S M
inst_12 : IsScalarTower R S M
inst_13 : Flat S M
inst_14 : Flat R N
P : Type u_4
x : AddCommMonoid P
x_1 : Module S P
I : Submodule S P
this : Module S (RestrictScalars R S P) := RestrictScalars.moduleOrig R S P
change :
  ∀ (I : Submodule S (RestrictScalars R S P)),
    Injective (α := ↥I ⊗[S] (M ⊗[R] N)) (β := P ⊗[S] (M ⊗[R] N))
      (⇑(rTensor (M ⊗[R] N) I.subtype) : (a : ↥I ⊗[S] (M ⊗[R] N)) → P ⊗[S] (M ⊗[R] N))
⊢ Injective (α := ↥I ⊗[S] (M ⊗[R] N)) (β := P ⊗[S] (M ⊗[R] N))
    (⇑(rTensor (M ⊗[R] N) I.subtype) : (a : ↥I ⊗[S] (M ⊗[R] N)) → P ⊗[S] (M ⊗[R] N))

Tactic:
change Submodule S (RestrictScalars R S P) at I

Premises used: Submodule, RestrictScalars
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P_1 : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P_1
inst_6 : Module R P_1
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
S : Type u_4
inst_9 : CommSemiring S
inst_10 : Algebra R S
inst_11 : Module S M
inst_12 : IsScalarTower R S M
inst_13 : Flat S M
inst_14 : Flat R N
P : Type u_4
x : AddCommMonoid P
x_1 : Module S P
this : Module S (RestrictScalars R S P) := RestrictScalars.moduleOrig R S P
I : Submodule S (RestrictScalars R S P)
change :
  Injective (α := ↥I ⊗[S] (M ⊗[R] N)) (β := RestrictScalars R S P ⊗[S] (M ⊗[R] N))
    (⇑(rTensor (M ⊗[R] N) I.subtype) : (a : ↥I ⊗[S] (M ⊗[R] N)) → RestrictScalars R S P ⊗[S] (M ⊗[R] N))
⊢ Injective (α := ↥I ⊗[S] (M ⊗[R] N)) (β := P ⊗[S] (M ⊗[R] N))
    (⇑(rTensor (M ⊗[R] N) I.subtype) : (a : ↥I ⊗[S] (M ⊗[R] N)) → P ⊗[S] (M ⊗[R] N))

Tactic:
change Function.Injective (rTensor _ I.subtype)

Premises used: Submodule.subtype, Function.Injective, DFunLike.coe, LinearMap.rTensor
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P_1 : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P_1
inst_6 : Module R P_1
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
S : Type u_4
inst_9 : CommSemiring S
inst_10 : Algebra R S
inst_11 : Module S M
inst_12 : IsScalarTower R S M
inst_13 : Flat S M
inst_14 : Flat R N
P : Type u_4
x : AddCommMonoid P
x_1 : Module S P
this : Module S (RestrictScalars R S P) := RestrictScalars.moduleOrig R S P
I : Submodule S (RestrictScalars R S P)
⊢ Injective (α := ↥I ⊗[S] (M ⊗[R] N)) (β := RestrictScalars R S P ⊗[S] (M ⊗[R] N))
    (⇑(rTensor (M ⊗[R] N) I.subtype) : (a : ↥I ⊗[S] (M ⊗[R] N)) → RestrictScalars R S P ⊗[S] (M ⊗[R] N))

Tactic:
simpa [AlgebraTensorModule.rTensor_tensor] using
      rTensor_preserves_injective_linearMap (.restrictScalars R <| I.subtype.rTensor M)
      (rTensor_preserves_injective_linearMap _ I.injective_subtype)

Premises used: LinearMap.restrictScalars, TensorProduct.AlgebraTensorModule.rTensor_tensor, Submodule.injective_subtype, Submodule.subtype, Module.Flat.rTensor_preserves_injective_linearMap, LinearMap.rTensor
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
inst_9 : Flat R M
inst_10 : Flat R N
⊢ Flat R (M ⊗[R] N)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
rw :
  Injective (α := ι →₀ S) (β := S ⊗[R] M)
    (⇑(lTensor S (Finsupp.linearCombination R v) ∘ₗ
          (↑(LinearEquiv.symm (finsuppScalarRight R R S ι)) : (ι →₀ S) →ₗ[R] S ⊗[R] (ι →₀ R))) :
      (a : ι →₀ S) → S ⊗[R] M)
⊢ LinearIndependent S (M := S ⊗[R] M) fun (x : ι) ↦ 1 ⊗ₜ[R] v x

Tactic:
rw [LinearIndependent, ← LinearMap.coe_restrictScalars R,
    Finsupp.linearCombination_one_tmul]

Premises used: Finsupp.linearCombination_one_tmul, LinearMap.coe_restrictScalars, LinearIndependent
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
classical :
  Injective (α := ι →₀ S) (β := S ⊗[R] M)
    (⇑(lTensor S (Finsupp.linearCombination R v) ∘ₗ
          (↑(LinearEquiv.symm (finsuppScalarRight R R S ι)) : (ι →₀ S) →ₗ[R] S ⊗[R] (ι →₀ R))) :
      (a : ι →₀ S) → S ⊗[R] M)
⊢ LinearIndependent S (M := S ⊗[R] M) fun (x : ι) ↦ 1 ⊗ₜ[R] v x

Tactic:
classical rw [LinearIndependent, ← LinearMap.coe_restrictScalars R,
    Finsupp.linearCombination_one_tmul]

Premises used: Finsupp.linearCombination_one_tmul, LinearMap.coe_restrictScalars, LinearIndependent
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ Injective (α := ι →₀ S) (β := S ⊗[R] M)
    (⇑(lTensor S (Finsupp.linearCombination R v) ∘ₗ
          (↑(LinearEquiv.symm (finsuppScalarRight R R S ι)) : (ι →₀ S) →ₗ[R] S ⊗[R] (ι →₀ R))) :
      (a : ι →₀ S) → S ⊗[R] M)

Tactic:
simpa using lTensor_preserves_injective_linearMap _ hv

Premises used: Module.Flat.lTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : FaithfulSMul R S
inst_6 : Flat R M
h :
  ∀ (x : M),
    Eq (α := S ⊗[R] M) (((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1 : (a : M) → S ⊗[R] M) x : S ⊗[R] M)
      (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
          (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M) x :
        S ⊗[R] M)
⊢ Eq (α := (a : M) → S ⊗[R] M) (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)
    (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
      (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M))

Tactic:
ext
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : FaithfulSMul R S
inst_6 : Flat R M
x : M
⊢ Eq (α := S ⊗[R] M) (((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1 : (a : M) → S ⊗[R] M) x : S ⊗[R] M)
    (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
        (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M) x :
      S ⊗[R] M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : FaithfulSMul R S
inst_6 : Flat R M
⊢ Eq (α := (a : M) → S ⊗[R] M) (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)
    (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
      (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M))

Tactic:
have : TensorProduct.mk R S M 1 =
      (Algebra.linearMap R S).rTensor M ∘ (TensorProduct.lid R M).symm := by ext; simp
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : FaithfulSMul R S
inst_6 : Flat R M
this :
  Eq (α := (a : M) → S ⊗[R] M) (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)
    (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
      (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M))
rw :
  Injective (α := M) (β := S ⊗[R] M)
    (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
      (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M))
⊢ Injective (α := M) (β := S ⊗[R] M) (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : FaithfulSMul R S
inst_6 : Flat R M
this :
  Eq (α := (a : M) → S ⊗[R] M) (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)
    (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
      (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M))
⊢ Injective (α := M) (β := S ⊗[R] M)
    (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
      (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M))

Tactic:
Injective.comp ?_ (LinearEquiv.injective _)

Premises used: Function.Injective.comp, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : FaithfulSMul R S
inst_6 : Flat R M
this :
  Eq (α := (a : M) → S ⊗[R] M) (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)
    (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
      (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M))
refine : Injective (α := R ⊗[R] M) (β := S ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
⊢ Injective (α := M) (β := S ⊗[R] M)
    (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
      (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M))

Tactic:
refine Injective.comp ?_ (LinearEquiv.injective _)

Premises used: Function.Injective.comp, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : FaithfulSMul R S
inst_6 : Flat R M
this :
  Eq (α := (a : M) → S ⊗[R] M) (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)
    (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
      (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M))
⊢ Injective (α := R ⊗[R] M) (β := S ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)

Tactic:
Flat.rTensor_preserves_injective_linearMap _ <| FaithfulSMul.algebraMap_injective R S

Premises used: FaithfulSMul.algebraMap_injective, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : FaithfulSMul R S
inst_6 : Flat R M
this :
  Eq (α := (a : M) → S ⊗[R] M) (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)
    (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
      (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M))
⊢ Injective (α := R ⊗[R] M) (β := S ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)

Tactic:
exact Flat.rTensor_preserves_injective_linearMap _ <| FaithfulSMul.algebraMap_injective R S

Premises used: FaithfulSMul.algebraMap_injective, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type u_4
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : FaithfulSMul R S
inst_8 : Flat R N
f g : M →ₗ[R] N
h :
  Eq (α := S ⊗[R] M →ₗ[S] S ⊗[R] N)
    ((baseChangeHom R S M N : (a : M →ₗ[R] N) → S ⊗[R] M →ₗ[S] S ⊗[R] N) f : S ⊗[R] M →ₗ[S] S ⊗[R] N)
    ((baseChangeHom R S M N : (a : M →ₗ[R] N) → S ⊗[R] M →ₗ[S] S ⊗[R] N) g : S ⊗[R] M →ₗ[S] S ⊗[R] N)
h₁ : ∀ (m : M), Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) m : N) ((g : (a : M) → N) m : N)
⊢ f = g

Tactic:
ext m
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type u_4
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : FaithfulSMul R S
inst_8 : Flat R N
f g : M →ₗ[R] N
h :
  Eq (α := S ⊗[R] M →ₗ[S] S ⊗[R] N)
    ((baseChangeHom R S M N : (a : M →ₗ[R] N) → S ⊗[R] M →ₗ[S] S ⊗[R] N) f : S ⊗[R] M →ₗ[S] S ⊗[R] N)
    ((baseChangeHom R S M N : (a : M →ₗ[R] N) → S ⊗[R] M →ₗ[S] S ⊗[R] N) g : S ⊗[R] M →ₗ[S] S ⊗[R] N)
m : M
⊢ Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) m : N) ((g : (a : M) → N) m : N)

Tactic:
simpa using Flat.tensorProduct_mk_injective R N S <| LinearMap.congr_fun h (1 ⊗ₜ[R] m)

Premises used: LinearMap.congr_fun, Module.Flat.tensorProduct_mk_injective, TensorProduct.tmul, OfNat.ofNat
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v', u} R
h : Flat R M
N N' : Type v'
inst_4 : AddCommGroup N
inst_5 : AddCommGroup N'
inst_6 : Module R N
inst_7 : Module R N'
f : N →ₗ[R] N'
⊢ Injective (α := N) (β := N') (⇑f : (a : N) → N') →
    Injective (α := N ⊗[R] M) (β := N' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)

Tactic:
apply rTensor_preserves_injective_linearMap

Premises used: Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : Module R N] [inst_7 : Module R N']
    (f : N →ₗ[R] N'),
    Injective (α := N) (β := N') (⇑f : (a : N) → N') →
      Injective (α := N ⊗[R] M) (β := N' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
P N : Type v'
x : AddCommMonoid P
x_1 : AddCommMonoid N
x_2 : Module R P
x_3 : Module R N
this_1 : AddCommGroup P := addCommMonoidToAddCommGroup R
this : AddCommGroup N := addCommMonoidToAddCommGroup R
⊢ ∀ (f : P →ₗ[R] N),
    Injective (α := P) (β := N) (⇑f : (a : P) → N) →
      Injective (α := P ⊗[R] M) (β := N ⊗[R] M) (⇑(rTensor M f) : (a : P ⊗[R] M) → N ⊗[R] M)

Tactic:
apply h
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Flat R M ↔
    ∀ ⦃N N' : Type (max u v)⦄ [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
      [inst_6 : Module R N'] (f : N →ₗ[R] N'),
      Injective (α := N) (β := N') (⇑f : (a : N) → N') →
        Injective (α := N ⊗[R] M) (β := N' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)

Tactic:
iff_rTensor_preserves_injective_linearMap'

Premises used: Module.Flat.iff_rTensor_preserves_injective_linearMap'
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v', u} R
simp_rw :
  (∀ ⦃N N' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : Module R N] [inst_7 : Module R N']
      (f : N →ₗ[R] N'),
      Injective (α := N) (β := N') (⇑f : (a : N) → N') →
        Injective (α := N ⊗[R] M) (β := N' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)) ↔
    ∀ ⦃N N' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : Module R N] [inst_7 : Module R N']
      (f : N →ₗ[R] N'),
      Injective (α := N) (β := N') (⇑f : (a : N) → N') →
        Injective (α := M ⊗[R] N) (β := M ⊗[R] N') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
⊢ Flat R M ↔
    ∀ ⦃N N' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : Module R N] [inst_7 : Module R N']
      (f : N →ₗ[R] N'),
      Injective (α := N) (β := N') (⇑f : (a : N) → N') →
        Injective (α := M ⊗[R] N) (β := M ⊗[R] N') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')

Tactic:
simp_rw [iff_rTensor_preserves_injective_linearMap', LinearMap.lTensor_inj_iff_rTensor_inj]

Premises used: Module.Flat.iff_rTensor_preserves_injective_linearMap', LinearMap.lTensor_inj_iff_rTensor_inj
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Flat R M ↔
    ∀ ⦃N N' : Type (max u v)⦄ [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
      [inst_6 : Module R N'] (f : N →ₗ[R] N'),
      Injective (α := N) (β := N') (⇑f : (a : N) → N') →
        Injective (α := M ⊗[R] N) (β := M ⊗[R] N') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')

Tactic:
iff_lTensor_preserves_injective_linearMap'

Premises used: Module.Flat.iff_lTensor_preserves_injective_linearMap'
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst_4 : AddCommGroup N
inst_5 : AddCommGroup N'
inst_6 : AddCommGroup N''
inst_7 : Module R N
inst_8 : Module R N'
inst_9 : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact.{u_1, u_2, u_3} (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'')
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : LinearMap.{u, u, u_2, u_3} (RingHom.id R) (N' ⧸ f.range) N'' :=
  g.range.subtype ∘ₗ
    (↑g.quotKerEquivRange : N' ⧸ g.ker →ₗ[R] ↥g.range) ∘ₗ
      (↑(f.range.quotEquivOfEq g.ker ⋯) : N' ⧸ f.range →ₗ[R] N' ⧸ g.ker)
exact1 :
  Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := TensorProduct.{u, v, u_2} R M (N' ⧸ f.range))
    (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑(lTensor M π) : (a : M ⊗[R] N') → M ⊗[R] (N' ⧸ f.range))
rw :
  Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
    (⇑(lTensor M ι ∘ₗ lTensor M π) : (a : M ⊗[R] N') → M ⊗[R] N'')
⊢ Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
    (⇑(lTensor M g) : (a : M ⊗[R] N') → M ⊗[R] N'')

Tactic:
rw [show g = ι.comp π from rfl, lTensor_comp]

Premises used: LinearMap.lTensor_comp, rfl
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst_4 : AddCommGroup N
inst_5 : AddCommGroup N'
inst_6 : AddCommGroup N''
inst_7 : Module R N
inst_8 : Module R N'
inst_9 : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact.{u_1, u_2, u_3} (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'')
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : LinearMap.{u, u, u_2, u_3} (RingHom.id R) (N' ⧸ f.range) N'' :=
  g.range.subtype ∘ₗ
    (↑g.quotKerEquivRange : N' ⧸ g.ker →ₗ[R] ↥g.range) ∘ₗ
      (↑(f.range.quotEquivOfEq g.ker ⋯) : N' ⧸ f.range →ₗ[R] N' ⧸ g.ker)
exact1 :
  Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := TensorProduct.{u, v, u_2} R M (N' ⧸ f.range))
    (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑(lTensor M π) : (a : M ⊗[R] N') → M ⊗[R] (N' ⧸ f.range))
⊢ Injective.{u_2 + 1, u_3 + 1} (α := N' ⧸ f.range) (β := N'') (⇑ι : (a : N' ⧸ f.range) → N'')

Tactic:
simpa [ι, -Subtype.val_injective] using Subtype.val_injective

Premises used: Subtype.val_injective