awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.CategoryTheory
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
inst_1 : Flat R (↑M : Type u)
C : ShortComplex (ModuleCat R)
hC :
  Function.Exact (M := (↑C.X₁ : Type u)) (N := (↑C.X₂ : Type u)) (P := (↑C.X₃ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) C.f) :
      (a : (↑C.X₁ : Type u)) → (↑C.X₂ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) C.g) :
      (a : (↑C.X₂ : Type u)) → (↑C.X₃ : Type u))
⊢ Function.Exact (M := (↑(ShortComplex.X₁ (C.map (tensorLeft M))) : Type u)) (N :=
    (↑(ShortComplex.X₂ (C.map (tensorLeft M))) : Type u)) (P := (↑(ShortComplex.X₃ (C.map (tensorLeft M))) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ShortComplex.X₁ (C.map (tensorLeft M))) (ShortComplex.f (C.map (tensorLeft M)))) :
      (a : (↑(C.map (tensorLeft M)).X₁ : Type u)) → (↑(C.map (tensorLeft M)).X₂ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ShortComplex.X₂ (C.map (tensorLeft M))) (ShortComplex.g (C.map (tensorLeft M)))) :
      (a : (↑(C.map (tensorLeft M)).X₂ : Type u)) → (↑(C.map (tensorLeft M)).X₃ : Type u))

Tactic:
lTensor_exact M hC

Premises used: Module.Flat.lTensor_exact, Quotient, ModuleCat.carrier, TensorProduct, AddCon.Quotient
-- Module: Mathlib.RingTheory.Flat.CategoryTheory
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
inst_1 : Flat R (↑M : Type u)
C : ShortComplex (ModuleCat R)
hC :
  Function.Exact (M := (↑C.X₁ : Type u)) (N := (↑C.X₂ : Type u)) (P := (↑C.X₃ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) C.f) :
      (a : (↑C.X₁ : Type u)) → (↑C.X₂ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) C.g) :
      (a : (↑C.X₂ : Type u)) → (↑C.X₃ : Type u))
⊢ Function.Exact (M := (↑(ShortComplex.X₁ (C.map (tensorLeft M))) : Type u)) (N :=
    (↑(ShortComplex.X₂ (C.map (tensorLeft M))) : Type u)) (P := (↑(ShortComplex.X₃ (C.map (tensorLeft M))) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ShortComplex.X₁ (C.map (tensorLeft M))) (ShortComplex.f (C.map (tensorLeft M)))) :
      (a : (↑(C.map (tensorLeft M)).X₁ : Type u)) → (↑(C.map (tensorLeft M)).X₂ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ShortComplex.X₂ (C.map (tensorLeft M))) (ShortComplex.g (C.map (tensorLeft M)))) :
      (a : (↑(C.map (tensorLeft M)).X₂ : Type u)) → (↑(C.map (tensorLeft M)).X₃ : Type u))

Tactic:
exact lTensor_exact M hC

Premises used: Module.Flat.lTensor_exact, ModuleCat.carrier
-- Module: Mathlib.RingTheory.Flat.CategoryTheory
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
inst_1 : Flat R (↑M : Type u)
C : ShortComplex (ModuleCat R)
hC : C.Exact
rw :
  ∀
    (hC :
      Function.Exact (M := (↑C.X₁ : Type u)) (N := (↑C.X₂ : Type u)) (P := (↑C.X₃ : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) C.f) :
          (a : (↑C.X₁ : Type u)) → (↑C.X₂ : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) C.g) :
          (a : (↑C.X₂ : Type u)) → (↑C.X₃ : Type u))),
    Function.Exact (M := (↑(ShortComplex.X₁ (C.map (tensorRight M))) : Type u)) (N :=
      (↑(ShortComplex.X₂ (C.map (tensorRight M))) : Type u)) (P :=
      (↑(ShortComplex.X₃ (C.map (tensorRight M))) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ShortComplex.X₁ (C.map (tensorRight M)))
            (ShortComplex.f (C.map (tensorRight M)))) :
        (a : (↑(C.map (tensorRight M)).X₁ : Type u)) → (↑(C.map (tensorRight M)).X₂ : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ShortComplex.X₂ (C.map (tensorRight M)))
            (ShortComplex.g (C.map (tensorRight M)))) :
        (a : (↑(C.map (tensorRight M)).X₂ : Type u)) → (↑(C.map (tensorRight M)).X₃ : Type u))
⊢ ShortComplex.Exact (C.map (tensorRight M))

Tactic:
rw [moduleCat_exact_iff_function_exact] at hC ⊢

Premises used: CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact
-- Module: Mathlib.RingTheory.Flat.CategoryTheory
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
inst_1 : Flat R (↑M : Type u)
C : ShortComplex (ModuleCat R)
hC :
  Function.Exact (M := (↑C.X₁ : Type u)) (N := (↑C.X₂ : Type u)) (P := (↑C.X₃ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) C.f) :
      (a : (↑C.X₁ : Type u)) → (↑C.X₂ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) C.g) :
      (a : (↑C.X₂ : Type u)) → (↑C.X₃ : Type u))
⊢ Function.Exact (M := (↑(ShortComplex.X₁ (C.map (tensorRight M))) : Type u)) (N :=
    (↑(ShortComplex.X₂ (C.map (tensorRight M))) : Type u)) (P := (↑(ShortComplex.X₃ (C.map (tensorRight M))) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ShortComplex.X₁ (C.map (tensorRight M))) (ShortComplex.f (C.map (tensorRight M)))) :
      (a : (↑(C.map (tensorRight M)).X₁ : Type u)) → (↑(C.map (tensorRight M)).X₂ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ShortComplex.X₂ (C.map (tensorRight M))) (ShortComplex.g (C.map (tensorRight M)))) :
      (a : (↑(C.map (tensorRight M)).X₂ : Type u)) → (↑(C.map (tensorRight M)).X₃ : Type u))

Tactic:
rTensor_exact M hC

Premises used: Module.Flat.rTensor_exact, Quotient, ModuleCat.carrier, TensorProduct, AddCon.Quotient
-- Module: Mathlib.RingTheory.Flat.CategoryTheory
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
inst_1 : Flat R (↑M : Type u)
C : ShortComplex (ModuleCat R)
hC :
  Function.Exact (M := (↑C.X₁ : Type u)) (N := (↑C.X₂ : Type u)) (P := (↑C.X₃ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) C.f) :
      (a : (↑C.X₁ : Type u)) → (↑C.X₂ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) C.g) :
      (a : (↑C.X₂ : Type u)) → (↑C.X₃ : Type u))
⊢ Function.Exact (M := (↑(ShortComplex.X₁ (C.map (tensorRight M))) : Type u)) (N :=
    (↑(ShortComplex.X₂ (C.map (tensorRight M))) : Type u)) (P := (↑(ShortComplex.X₃ (C.map (tensorRight M))) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ShortComplex.X₁ (C.map (tensorRight M))) (ShortComplex.f (C.map (tensorRight M)))) :
      (a : (↑(C.map (tensorRight M)).X₁ : Type u)) → (↑(C.map (tensorRight M)).X₂ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ShortComplex.X₂ (C.map (tensorRight M))) (ShortComplex.g (C.map (tensorRight M)))) :
      (a : (↑(C.map (tensorRight M)).X₂ : Type u)) → (↑(C.map (tensorRight M)).X₃ : Type u))

Tactic:
exact rTensor_exact M hC

Premises used: Module.Flat.rTensor_exact, ModuleCat.carrier
-- Module: Mathlib.RingTheory.Flat.CategoryTheory
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
⊢ Flat R (↑M : Type u) ↔ ∀ (C : ShortComplex (ModuleCat R)), C.Exact → ShortComplex.Exact (C.map (tensorLeft M))

Tactic:
⟨fun _ _ ↦ lTensor_shortComplex_exact _ _, fun H ↦ iff_lTensor_exact.2
    fun _ _ _ _ _ _ _ _ _ f g h ↦
      moduleCat_exact_iff_function_exact _ |>.1 <|
      H (.mk (ModuleCat.ofHom f) (ModuleCat.ofHom g)
        (ModuleCat.hom_ext (DFunLike.ext _ _ h.apply_apply_eq_zero)))
          (moduleCat_exact_iff_function_exact _ |>.2 h)⟩

Premises used: Function.Exact.apply_apply_eq_zero, Iff.mpr, DFunLike.ext, CategoryTheory.ShortComplex.mk, Module.Flat.lTensor_shortComplex_exact, Module.Flat.iff_lTensor_exact, CategoryTheory.MonoidalCategory.tensorLeft, CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact, Iff.intro, CategoryTheory.CategoryStruct.comp, Iff.mp, CategoryTheory.ShortComplex.map, ModuleCat.hom_ext, ModuleCat.ofHom, OfNat.ofNat, ModuleCat.Hom.hom
-- Module: Mathlib.RingTheory.Flat.CategoryTheory
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
⊢ Flat R (↑M : Type u) ↔ ∀ (C : ShortComplex (ModuleCat R)), C.Exact → ShortComplex.Exact (C.map (tensorRight M))

Tactic:
⟨fun _ _ ↦ rTensor_shortComplex_exact _ _, fun H ↦ iff_rTensor_exact.2
    fun _ _ _ _ _ _ _ _ _ f g h ↦
      moduleCat_exact_iff_function_exact _ |>.1 <|
      H (.mk (ModuleCat.ofHom f) (ModuleCat.ofHom g)
        (ModuleCat.hom_ext (DFunLike.ext _ _ h.apply_apply_eq_zero)))
          (moduleCat_exact_iff_function_exact _ |>.2 h)⟩

Premises used: Function.Exact.apply_apply_eq_zero, Iff.mpr, DFunLike.ext, CategoryTheory.ShortComplex.mk, CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact, CategoryTheory.MonoidalCategory.tensorRight, Module.Flat.iff_rTensor_exact, Iff.intro, CategoryTheory.CategoryStruct.comp, Iff.mp, CategoryTheory.ShortComplex.map, ModuleCat.hom_ext, ModuleCat.ofHom, OfNat.ofNat, ModuleCat.Hom.hom, Module.Flat.rTensor_shortComplex_exact
-- Module: Mathlib.RingTheory.Flat.CategoryTheory
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
rw :
  PreservesFiniteLimits (tensorLeft M) ∧ PreservesFiniteColimits (tensorLeft M) ↔ PreservesFiniteLimits (tensorLeft M)
⊢ Flat R (↑M : Type u) ↔ PreservesFiniteLimits (tensorLeft M)

Tactic:
rw [Module.Flat.iff_lTensor_preserves_shortComplex_exact,
    ((Functor.exact_tfae <| tensorLeft M).out 1 3 :)]

Premises used: Module.Flat.iff_lTensor_preserves_shortComplex_exact, CategoryTheory.MonoidalCategory.tensorLeft, List.TFAE.out, OfNat.ofNat, CategoryTheory.Functor.exact_tfae
-- Module: Mathlib.RingTheory.Flat.CategoryTheory
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
⊢ PreservesFiniteLimits (tensorLeft M) ∧ PreservesFiniteColimits (tensorLeft M) ↔ PreservesFiniteLimits (tensorLeft M)

Tactic:
simp [show PreservesFiniteColimits (tensorLeft M) from inferInstance]

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Flat.CategoryTheory
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
inst_1 rw : Flat R (↑M : Type u)
⊢ PreservesFiniteLimits (tensorLeft M)

Tactic:
rw [← iff_preservesFiniteLimits_tensorLeft]

Premises used: Module.Flat.iff_preservesFiniteLimits_tensorLeft
-- Module: Mathlib.RingTheory.Flat.CategoryTheory
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
inst_1 : Flat R (↑M : Type u)
⊢ Flat R (↑M : Type u)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Flat.CategoryTheory
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
h : PreservesFiniteLimits (tensorRight M)
rw : PreservesFiniteLimits (tensorLeft M)
⊢ Flat R (↑M : Type u)

Tactic:
rw [iff_preservesFiniteLimits_tensorLeft]

Premises used: Module.Flat.iff_preservesFiniteLimits_tensorLeft
-- Module: Mathlib.RingTheory.Flat.CategoryTheory
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
h : PreservesFiniteLimits (tensorRight M)
⊢ PreservesFiniteLimits (tensorLeft M)

Tactic:
preservesFiniteLimits_of_natIso (BraidedCategory.tensorLeftIsoTensorRight M).symm

Premises used: CategoryTheory.BraidedCategory.tensorLeftIsoTensorRight, CategoryTheory.Iso.symm, CategoryTheory.Limits.preservesFiniteLimits_of_natIso
-- Module: Mathlib.RingTheory.Flat.CategoryTheory
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
h : PreservesFiniteLimits (tensorRight M)
⊢ PreservesFiniteLimits (tensorLeft M)

Tactic:
exact preservesFiniteLimits_of_natIso (BraidedCategory.tensorLeftIsoTensorRight M).symm

Premises used: CategoryTheory.BraidedCategory.tensorLeftIsoTensorRight, CategoryTheory.Iso.symm, CategoryTheory.Limits.preservesFiniteLimits_of_natIso
-- Module: Mathlib.RingTheory.Flat.CategoryTheory
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
inst_1 : Flat R (↑M : Type u)
⊢ PreservesFiniteLimits (tensorRight M)

Tactic:
preservesFiniteLimits_of_natIso (BraidedCategory.tensorLeftIsoTensorRight M)

Premises used: CategoryTheory.BraidedCategory.tensorLeftIsoTensorRight, CategoryTheory.Limits.preservesFiniteLimits_of_natIso
-- Module: Mathlib.RingTheory.Flat.Domain
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
⊢ Injective (α := P ⊗[R] Q) (β := M ⊗[R] N) (⇑(map f g) : (a : P ⊗[R] Q) → M ⊗[R] N)

Tactic:
.of_comp (f := TensorProduct.mk R K _ 1) ?_

Premises used: Function.Injective.of_comp
-- Module: Mathlib.RingTheory.Flat.Domain
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
refine :
  Injective (α := P ⊗[R] Q) (β := K ⊗[R] (M ⊗[R] N))
    (comp (β := M ⊗[R] N)
      (⇑((mk R K (M ⊗[R] N) : (a : K) → M ⊗[R] N →ₗ[R] K ⊗[R] (M ⊗[R] N)) 1) : (a : M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
      (⇑(map f g) : (a : P ⊗[R] Q) → M ⊗[R] N))
⊢ Injective (α := P ⊗[R] Q) (β := M ⊗[R] N) (⇑(map f g) : (a : P ⊗[R] Q) → M ⊗[R] N)

Tactic:
refine .of_comp (f := TensorProduct.mk R K _ 1) ?_
-- Module: Mathlib.RingTheory.Flat.Domain
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
⊢ Injective (α := K ⊗[R] P ⊗[K] (K ⊗[R] Q)) (β := K ⊗[R] M ⊗[K] (K ⊗[R] N))
    (⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) :
      (a : K ⊗[R] P ⊗[K] (K ⊗[R] Q)) → K ⊗[R] M ⊗[K] (K ⊗[R] N))

Tactic:
have H₁ := TensorProduct.map_injective_of_flat_flat (f.baseChange K) (g.baseChange K)
    (Module.Flat.lTensor_preserves_injective_linearMap f hf)
    (Module.Flat.lTensor_preserves_injective_linearMap g hg)
-- Module: Mathlib.RingTheory.Flat.Domain
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
H₁ :
  Injective (α := K ⊗[R] P ⊗[K] (K ⊗[R] Q)) (β := K ⊗[R] M ⊗[K] (K ⊗[R] N))
    (⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) :
      (a : K ⊗[R] P ⊗[K] (K ⊗[R] Q)) → K ⊗[R] M ⊗[K] (K ⊗[R] N))
⊢ Injective (α := K ⊗[R] P ⊗[R] Q) (β := K ⊗[R] P ⊗[K] (K ⊗[R] Q))
    (⇑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q) :
          K ⊗[R] P ⊗[R] Q ≃ₗ[K] K ⊗[R] P ⊗[K] (K ⊗[R] Q)) :
      (a : K ⊗[R] P ⊗[R] Q) → K ⊗[R] P ⊗[K] (K ⊗[R] Q))

Tactic:
have H₂ := (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm.injective
-- Module: Mathlib.RingTheory.Flat.Domain
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
H₁ :
  Injective (α := K ⊗[R] P ⊗[K] (K ⊗[R] Q)) (β := K ⊗[R] M ⊗[K] (K ⊗[R] N))
    (⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) :
      (a : K ⊗[R] P ⊗[K] (K ⊗[R] Q)) → K ⊗[R] M ⊗[K] (K ⊗[R] N))
H₂ :
  Injective (α := K ⊗[R] P ⊗[R] Q) (β := K ⊗[R] P ⊗[K] (K ⊗[R] Q))
    (⇑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q) :
          K ⊗[R] P ⊗[R] Q ≃ₗ[K] K ⊗[R] P ⊗[K] (K ⊗[R] Q)) :
      (a : K ⊗[R] P ⊗[R] Q) → K ⊗[R] P ⊗[K] (K ⊗[R] Q))
⊢ Injective (α := K ⊗[R] M ⊗[K] (K ⊗[R] N)) (β := K ⊗[R] M ⊗[R] N)
    (⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N : K ⊗[R] M ⊗[K] (K ⊗[R] N) ≃ₗ[K] K ⊗[R] M ⊗[R] N) :
      (a : K ⊗[R] M ⊗[K] (K ⊗[R] N)) → K ⊗[R] M ⊗[R] N)

Tactic:
have H₃ := (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N).injective
-- Module: Mathlib.RingTheory.Flat.Domain
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
H₁ :
  Injective (α := K ⊗[R] P ⊗[K] (K ⊗[R] Q)) (β := K ⊗[R] M ⊗[K] (K ⊗[R] N))
    (⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) :
      (a : K ⊗[R] P ⊗[K] (K ⊗[R] Q)) → K ⊗[R] M ⊗[K] (K ⊗[R] N))
H₂ :
  Injective (α := K ⊗[R] P ⊗[R] Q) (β := K ⊗[R] P ⊗[K] (K ⊗[R] Q))
    (⇑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q) :
          K ⊗[R] P ⊗[R] Q ≃ₗ[K] K ⊗[R] P ⊗[K] (K ⊗[R] Q)) :
      (a : K ⊗[R] P ⊗[R] Q) → K ⊗[R] P ⊗[K] (K ⊗[R] Q))
H₃ :
  Injective (α := K ⊗[R] M ⊗[K] (K ⊗[R] N)) (β := K ⊗[R] M ⊗[R] N)
    (⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N : K ⊗[R] M ⊗[K] (K ⊗[R] N) ≃ₗ[K] K ⊗[R] M ⊗[R] N) :
      (a : K ⊗[R] M ⊗[K] (K ⊗[R] N)) → K ⊗[R] M ⊗[R] N)
⊢ Injective (α := K ⊗[R] (P ⊗[R] Q)) (β := K ⊗[R] P ⊗[R] Q)
    (⇑(LinearEquiv.symm (AlgebraTensorModule.assoc R R K K P Q) : K ⊗[R] (P ⊗[R] Q) ≃ₗ[K] K ⊗[R] P ⊗[R] Q) :
      (a : K ⊗[R] (P ⊗[R] Q)) → K ⊗[R] P ⊗[R] Q)

Tactic:
have H₄ := (AlgebraTensorModule.assoc R R K K P Q).symm.injective
-- Module: Mathlib.RingTheory.Flat.Domain
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
H₁ :
  Injective (α := K ⊗[R] P ⊗[K] (K ⊗[R] Q)) (β := K ⊗[R] M ⊗[K] (K ⊗[R] N))
    (⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) :
      (a : K ⊗[R] P ⊗[K] (K ⊗[R] Q)) → K ⊗[R] M ⊗[K] (K ⊗[R] N))
H₂ :
  Injective (α := K ⊗[R] P ⊗[R] Q) (β := K ⊗[R] P ⊗[K] (K ⊗[R] Q))
    (⇑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q) :
          K ⊗[R] P ⊗[R] Q ≃ₗ[K] K ⊗[R] P ⊗[K] (K ⊗[R] Q)) :
      (a : K ⊗[R] P ⊗[R] Q) → K ⊗[R] P ⊗[K] (K ⊗[R] Q))
H₃ :
  Injective (α := K ⊗[R] M ⊗[K] (K ⊗[R] N)) (β := K ⊗[R] M ⊗[R] N)
    (⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N : K ⊗[R] M ⊗[K] (K ⊗[R] N) ≃ₗ[K] K ⊗[R] M ⊗[R] N) :
      (a : K ⊗[R] M ⊗[K] (K ⊗[R] N)) → K ⊗[R] M ⊗[R] N)
H₄ :
  Injective (α := K ⊗[R] (P ⊗[R] Q)) (β := K ⊗[R] P ⊗[R] Q)
    (⇑(LinearEquiv.symm (AlgebraTensorModule.assoc R R K K P Q) : K ⊗[R] (P ⊗[R] Q) ≃ₗ[K] K ⊗[R] P ⊗[R] Q) :
      (a : K ⊗[R] (P ⊗[R] Q)) → K ⊗[R] P ⊗[R] Q)
⊢ Injective (α := K ⊗[R] M ⊗[R] N) (β := K ⊗[R] (M ⊗[R] N))
    (⇑(AlgebraTensorModule.assoc R R K K M N : K ⊗[R] M ⊗[R] N ≃ₗ[K] K ⊗[R] (M ⊗[R] N)) :
      (a : K ⊗[R] M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))

Tactic:
have H₅ := (AlgebraTensorModule.assoc R R K K M N).injective
-- Module: Mathlib.RingTheory.Flat.Domain
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
H₁ :
  Injective (α := K ⊗[R] P ⊗[K] (K ⊗[R] Q)) (β := K ⊗[R] M ⊗[K] (K ⊗[R] N))
    (⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) :
      (a : K ⊗[R] P ⊗[K] (K ⊗[R] Q)) → K ⊗[R] M ⊗[K] (K ⊗[R] N))
H₂ :
  Injective (α := K ⊗[R] P ⊗[R] Q) (β := K ⊗[R] P ⊗[K] (K ⊗[R] Q))
    (⇑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q) :
          K ⊗[R] P ⊗[R] Q ≃ₗ[K] K ⊗[R] P ⊗[K] (K ⊗[R] Q)) :
      (a : K ⊗[R] P ⊗[R] Q) → K ⊗[R] P ⊗[K] (K ⊗[R] Q))
H₃ :
  Injective (α := K ⊗[R] M ⊗[K] (K ⊗[R] N)) (β := K ⊗[R] M ⊗[R] N)
    (⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N : K ⊗[R] M ⊗[K] (K ⊗[R] N) ≃ₗ[K] K ⊗[R] M ⊗[R] N) :
      (a : K ⊗[R] M ⊗[K] (K ⊗[R] N)) → K ⊗[R] M ⊗[R] N)
H₄ :
  Injective (α := K ⊗[R] (P ⊗[R] Q)) (β := K ⊗[R] P ⊗[R] Q)
    (⇑(LinearEquiv.symm (AlgebraTensorModule.assoc R R K K P Q) : K ⊗[R] (P ⊗[R] Q) ≃ₗ[K] K ⊗[R] P ⊗[R] Q) :
      (a : K ⊗[R] (P ⊗[R] Q)) → K ⊗[R] P ⊗[R] Q)
H₅ :
  Injective (α := K ⊗[R] M ⊗[R] N) (β := K ⊗[R] (M ⊗[R] N))
    (⇑(AlgebraTensorModule.assoc R R K K M N : K ⊗[R] M ⊗[R] N ≃ₗ[K] K ⊗[R] (M ⊗[R] N)) :
      (a : K ⊗[R] M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
⊢ Injective (α := R ⊗[R] (P ⊗[R] Q)) (β := K ⊗[R] (P ⊗[R] Q))
    (⇑(LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K)) : (a : R ⊗[R] (P ⊗[R] Q)) → K ⊗[R] (P ⊗[R] Q))

Tactic:
have H₆ := Module.Flat.rTensor_preserves_injective_linearMap (M := P ⊗[R] Q)
    (Algebra.linearMap R K) (FaithfulSMul.algebraMap_injective R K)