awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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' N'' : Type v'⦄ [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''⦄,
    Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
      Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
        (⇑(rTensor M g) : (a : N' ⊗[R] M) → N'' ⊗[R] M)
N' N'' : Type v'
x_1 : AddCommGroup N'
x_2 : AddCommGroup N''
x_3 : Module R N'
x_4 : Module R N''
f : N' →ₗ[R] N''
hf : Injective (α := N') (β := N'') (⇑f : (a : N') → N'')
x_5 : N' ⊗[R] M
hx : Eq (α := N'' ⊗[R] M) ((rTensor M f : (a : N' ⊗[R] M) → N'' ⊗[R] M) x_5 : N'' ⊗[R] M) (0 : N'' ⊗[R] M)
x : N'
⊢ Eq (α := N'') ((f : (a : N') → N'') x : N'') (0 : N'') ↔ 0 = x

Tactic:
(f.map_eq_zero_iff hf).trans eq_comm

Premises used: eq_comm, Iff.trans, LinearMap.map_eq_zero_iff
-- 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' N'' : Type v'⦄ [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''⦄,
    Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
      Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
        (⇑(rTensor M g) : (a : N' ⊗[R] M) → N'' ⊗[R] M)
N' N'' : Type v'
x_1 : AddCommGroup N'
x_2 : AddCommGroup N''
x_3 : Module R N'
x_4 : Module R N''
f : N' →ₗ[R] N''
hf : Injective (α := N') (β := N'') (⇑f : (a : N') → N'')
x_5 : N' ⊗[R] M
hx : Eq (α := N'' ⊗[R] M) ((rTensor M f : (a : N' ⊗[R] M) → N'' ⊗[R] M) x_5 : N'' ⊗[R] M) (0 : N'' ⊗[R] M)
x : N'
⊢ Eq (α := N'') ((f : (a : N') → N'') x : N'') (0 : N'') ↔ 0 = x

Tactic:
exact (f.map_eq_zero_iff hf).trans eq_comm

Premises used: eq_comm, Iff.trans, LinearMap.map_eq_zero_iff
-- 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' N'' : Type v'⦄ [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''⦄,
    Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
      Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
        (⇑(rTensor M g) : (a : N' ⊗[R] M) → N'' ⊗[R] M)
N' N'' : Type v'
x_1 : AddCommGroup N'
x_2 : AddCommGroup N''
x_3 : Module R N'
x_4 : Module R N''
f : N' →ₗ[R] N''
hf : Injective (α := N') (β := N'') (⇑f : (a : N') → N'')
x : N' ⊗[R] M
hx : Eq (α := N'' ⊗[R] M) ((rTensor M f : (a : N' ⊗[R] M) → N'' ⊗[R] M) x : N'' ⊗[R] M) (0 : N'' ⊗[R] M)
⊢ Membership.mem (γ := Submodule R (N' ⊗[R] M)) ⊥ x

Tactic:
simpa [Eq.comm] using @H PUnit N' N'' _ _ _ _ _ _ 0 f (fun x ↦ by
    simp_rw [Set.mem_range, LinearMap.zero_apply, exists_const]
    exact (f.map_eq_zero_iff hf).trans eq_comm) x |>.mp hx

Premises used: Iff.mp, Eq.comm
-- 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' N'' : Type (max u v)⦄ [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : AddCommGroup N'']
      [inst_6 : Module R N] [inst_7 : Module R N'] [inst_8 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
        Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
          (⇑(rTensor M g) : (a : N' ⊗[R] M) → N'' ⊗[R] M)

Tactic:
iff_rTensor_exact'

Premises used: Module.Flat.iff_rTensor_exact'
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : CommSemiring S
inst_6 : Algebra S A
inst_7 : SMulCommClass R S A
inst_8 : Module.Flat R A
hb : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
⊢ Function.Injective (α := A) (β := A ⊗[R] B)
    (Function.comp (β := A ⊗[R] R) (⇑(LinearMap.lTensor A (Algebra.linearMap R B)) : (a : A ⊗[R] R) → A ⊗[R] B)
      (⇑(LinearEquiv.symm (_root_.TensorProduct.rid R A)) : (a : A) → A ⊗[R] R))

Tactic:
Module.Flat.lTensor_preserves_injective_linearMap (M := A) (Algebra.linearMap R B) hb |>.comp
      (_root_.TensorProduct.rid R A).symm.injective

Premises used: LinearEquiv.symm, Module.Flat.lTensor_preserves_injective_linearMap, TensorProduct.rid, Algebra.linearMap, Function.Injective.comp, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : CommSemiring S
inst_6 : Algebra S A
inst_7 : SMulCommClass R S A
inst_8 : Module.Flat R A
hb : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
h :
  Eq (α := A → A ⊗[R] B) (⇑includeLeft : (a : A) → A ⊗[R] B)
    (Function.comp (β := A ⊗[R] R) (⇑(LinearMap.lTensor A (Algebra.linearMap R B)) : (a : A ⊗[R] R) → A ⊗[R] B)
      (⇑(LinearEquiv.symm (_root_.TensorProduct.rid R A)) : (a : A) → A ⊗[R] R))
⊢ Function.Injective (α := A) (β := A ⊗[R] B) (⇑includeLeft : (a : A) → A ⊗[R] B)

Tactic:
convert!
    Module.Flat.lTensor_preserves_injective_linearMap (M := A) (Algebra.linearMap R B) hb |>.comp
      (_root_.TensorProduct.rid R A).symm.injective

Premises used: LinearEquiv.symm, Module.Flat.lTensor_preserves_injective_linearMap, TensorProduct.rid, Algebra.linearMap, Function.Injective.comp, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : CommSemiring S
inst_6 : Algebra S A
inst_7 : SMulCommClass R S A
inst_8 : Module.Flat R A
hb : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
h :
  ∀ (x : A),
    Eq (α := A ⊗[R] B) ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
      (Function.comp (β := A ⊗[R] R) (⇑(LinearMap.lTensor A (Algebra.linearMap R B)) : (a : A ⊗[R] R) → A ⊗[R] B)
          (⇑(LinearEquiv.symm (_root_.TensorProduct.rid R A)) : (a : A) → A ⊗[R] R) x :
        A ⊗[R] B)
⊢ Eq (α := A → A ⊗[R] B) (⇑includeLeft : (a : A) → A ⊗[R] B)
    (Function.comp (β := A ⊗[R] R) (⇑(LinearMap.lTensor A (Algebra.linearMap R B)) : (a : A ⊗[R] R) → A ⊗[R] B)
      (⇑(LinearEquiv.symm (_root_.TensorProduct.rid R A)) : (a : A) → A ⊗[R] R))

Tactic:
ext
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : CommSemiring S
inst_6 : Algebra S A
inst_7 : SMulCommClass R S A
inst_8 : Module.Flat R A
hb : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
x : A
⊢ Eq (α := A ⊗[R] B) ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
    (Function.comp (β := A ⊗[R] R) (⇑(LinearMap.lTensor A (Algebra.linearMap R B)) : (a : A ⊗[R] R) → A ⊗[R] B)
        (⇑(LinearEquiv.symm (_root_.TensorProduct.rid R A)) : (a : A) → A ⊗[R] R) x :
      A ⊗[R] B)

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Module.Flat R B
ha : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Function.Injective (α := B) (β := A ⊗[R] B)
    (Function.comp (β := R ⊗[R] B) (⇑(LinearMap.rTensor B (Algebra.linearMap R A)) : (a : R ⊗[R] B) → A ⊗[R] B)
      (⇑(LinearEquiv.symm (_root_.TensorProduct.lid R B)) : (a : B) → R ⊗[R] B))

Tactic:
Module.Flat.rTensor_preserves_injective_linearMap (M := B) (Algebra.linearMap R A) ha |>.comp
      (_root_.TensorProduct.lid R B).symm.injective

Premises used: LinearEquiv.symm, Algebra.linearMap, Function.Injective.comp, TensorProduct.lid, LinearEquiv.injective, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Module.Flat R B
ha : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
h :
  Eq (α := B → A ⊗[R] B) (⇑includeRight : (a : B) → A ⊗[R] B)
    (Function.comp (β := R ⊗[R] B) (⇑(LinearMap.rTensor B (Algebra.linearMap R A)) : (a : R ⊗[R] B) → A ⊗[R] B)
      (⇑(LinearEquiv.symm (_root_.TensorProduct.lid R B)) : (a : B) → R ⊗[R] B))
⊢ Function.Injective (α := B) (β := A ⊗[R] B) (⇑includeRight : (a : B) → A ⊗[R] B)

Tactic:
convert!
    Module.Flat.rTensor_preserves_injective_linearMap (M := B) (Algebra.linearMap R A) ha |>.comp
      (_root_.TensorProduct.lid R B).symm.injective

Premises used: LinearEquiv.symm, Algebra.linearMap, Function.Injective.comp, TensorProduct.lid, LinearEquiv.injective, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Module.Flat R B
ha : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
h :
  ∀ (x : B),
    Eq (α := A ⊗[R] B) ((includeRight : (a : B) → A ⊗[R] B) x : A ⊗[R] B)
      (Function.comp (β := R ⊗[R] B) (⇑(LinearMap.rTensor B (Algebra.linearMap R A)) : (a : R ⊗[R] B) → A ⊗[R] B)
          (⇑(LinearEquiv.symm (_root_.TensorProduct.lid R B)) : (a : B) → R ⊗[R] B) x :
        A ⊗[R] B)
⊢ Eq (α := B → A ⊗[R] B) (⇑includeRight : (a : B) → A ⊗[R] B)
    (Function.comp (β := R ⊗[R] B) (⇑(LinearMap.rTensor B (Algebra.linearMap R A)) : (a : R ⊗[R] B) → A ⊗[R] B)
      (⇑(LinearEquiv.symm (_root_.TensorProduct.lid R B)) : (a : B) → R ⊗[R] B))

Tactic:
ext
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Module.Flat R B
ha : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
x : B
⊢ Eq (α := A ⊗[R] B) ((includeRight : (a : B) → A ⊗[R] B) x : A ⊗[R] B)
    (Function.comp (β := R ⊗[R] B) (⇑(LinearMap.rTensor B (Algebra.linearMap R A)) : (a : R ⊗[R] B) → A ⊗[R] B)
        (⇑(LinearEquiv.symm (_root_.TensorProduct.lid R B)) : (a : B) → R ⊗[R] B) x :
      A ⊗[R] B)

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Module.Flat R A
M : Type u_5
inst_4 : AddCommMonoid M
inst_5 : Module R M
p : Submodule R M
⊢ Function.Injective (α := TensorProduct.{u_1, u_3, u_5} R A ↥p) (β := ↥(baseChange A p))
    (⇑(toBaseChange A p) : (a : A ⊗[R] ↥p) → ↥(baseChange A p))

Tactic:
(p.subtype.baseChange A).injective_rangeRestrict_iff.mpr
    (Module.Flat.lTensor_preserves_injective_linearMap p.subtype (injective_subtype p))

Premises used: Iff.mpr, LinearMap.baseChange, Module.Flat.lTensor_preserves_injective_linearMap, Set.Mem, Submodule.injective_subtype, Submodule.subtype, LinearMap.injective_rangeRestrict_iff
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Module.Flat R A
M : Type u_5
inst_4 : AddCommMonoid M
inst_5 : Module R M
p : Submodule R M
a : A
m : ↥p
⊢ Eq (α := TensorProduct.{u_1, u_3, u_5} R A ↥p)
    ((LinearEquiv.symm (toLinearEquiv A p) : (a : ↥(baseChange A p)) → A ⊗[R] ↥p)
        (Subtype.mk (p := fun (x : A ⊗[R] M) ↦ Membership.mem (γ := Submodule A (A ⊗[R] M)) (baseChange A p) x)
          (a ⊗ₜ[R] (↑m : M)) ⋯) :
      TensorProduct.{u_1, u_3, u_5} R A ↥p)
    (a ⊗ₜ[R] m : TensorProduct.{u_1, u_3, u_5} R A ↥p)

Tactic:
(toBaseChange.toLinearEquiv A p).symm_apply_apply (a ⊗ₜ[R] m)

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, Submodule.toBaseChange.toLinearEquiv, LinearEquiv.symm_apply_apply, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : R →ₗ[R] N
h : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := N) (⇑f : (a : R) → N)
inst_5 : Module.Flat R M
inst_6 : Nontrivial M
⊢ Nontrivial (M ⊗[R] N)

Tactic:
Module.Flat.lTensor_preserves_injective_linearMap (M := M) f h |>.comp
    (TensorProduct.rid R M).symm.injective |>.nontrivial

Premises used: LinearEquiv.symm, Module.Flat.lTensor_preserves_injective_linearMap, TensorProduct.rid, Function.Injective.nontrivial, Function.Injective.comp, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : R →ₗ[R] M
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := M) (⇑f : (a : R) → M)
inst_5 : Module.Flat R N
inst_6 : Nontrivial N
⊢ Nontrivial (M ⊗[R] N)

Tactic:
Module.Flat.rTensor_preserves_injective_linearMap (M := N) f h |>.comp
    (TensorProduct.lid R N).symm.injective |>.nontrivial

Premises used: LinearEquiv.symm, Function.Injective.nontrivial, Function.Injective.comp, TensorProduct.lid, LinearEquiv.injective, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
P : Type u_4
Q : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
inst_9 : Module.Flat R M
inst_10 : Module.Flat R Q
hf : Function.Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Function.Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
rw :
  Function.Injective (α := P ⊗[R] Q) (β := M ⊗[R] N)
    (⇑(LinearMap.lTensor M g ∘ₗ LinearMap.rTensor Q f) : (a : P ⊗[R] Q) → M ⊗[R] N)
⊢ Function.Injective (α := P ⊗[R] Q) (β := M ⊗[R] N) (⇑(map f g) : (a : P ⊗[R] Q) → M ⊗[R] N)

Tactic:
rw [← LinearMap.lTensor_comp_rTensor]

Premises used: LinearMap.lTensor_comp_rTensor
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
P : Type u_4
Q : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
inst_9 : Module.Flat R M
inst_10 : Module.Flat R Q
hf : Function.Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Function.Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
⊢ Function.Injective (α := P ⊗[R] Q) (β := M ⊗[R] N)
    (⇑(LinearMap.lTensor M g ∘ₗ LinearMap.rTensor Q f) : (a : P ⊗[R] Q) → M ⊗[R] N)

Tactic:
(Module.Flat.lTensor_preserves_injective_linearMap g hg).comp
    (Module.Flat.rTensor_preserves_injective_linearMap f hf)

Premises used: Module.Flat.lTensor_preserves_injective_linearMap, Quotient.liftOn', AddCon.liftOn, Function.Injective.comp, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
P : Type u_4
Q : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
inst_9 : Module.Flat R M
inst_10 : Module.Flat R Q
hf : Function.Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Function.Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
⊢ Function.Injective (α := P ⊗[R] Q) (β := M ⊗[R] N)
    (⇑(LinearMap.lTensor M g ∘ₗ LinearMap.rTensor Q f) : (a : P ⊗[R] Q) → M ⊗[R] N)

Tactic:
exact (Module.Flat.lTensor_preserves_injective_linearMap g hg).comp
    (Module.Flat.rTensor_preserves_injective_linearMap f hf)

Premises used: Module.Flat.lTensor_preserves_injective_linearMap, Function.Injective.comp, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
P : Type u_4
Q : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
inst_9 : Module.Flat R P
inst_10 : Module.Flat R N
hf : Function.Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Function.Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
rw :
  Function.Injective (α := P ⊗[R] Q) (β := M ⊗[R] N)
    (⇑(LinearMap.rTensor N f ∘ₗ LinearMap.lTensor P g) : (a : P ⊗[R] Q) → M ⊗[R] N)
⊢ Function.Injective (α := P ⊗[R] Q) (β := M ⊗[R] N) (⇑(map f g) : (a : P ⊗[R] Q) → M ⊗[R] N)

Tactic:
rw [← LinearMap.rTensor_comp_lTensor]

Premises used: LinearMap.rTensor_comp_lTensor
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
P : Type u_4
Q : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
inst_9 : Module.Flat R P
inst_10 : Module.Flat R N
hf : Function.Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Function.Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
⊢ Function.Injective (α := P ⊗[R] Q) (β := M ⊗[R] N)
    (⇑(LinearMap.rTensor N f ∘ₗ LinearMap.lTensor P g) : (a : P ⊗[R] Q) → M ⊗[R] N)

Tactic:
(Module.Flat.rTensor_preserves_injective_linearMap f hf).comp
    (Module.Flat.lTensor_preserves_injective_linearMap g hg)

Premises used: Module.Flat.lTensor_preserves_injective_linearMap, Quotient.liftOn', AddCon.liftOn, Function.Injective.comp, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
P : Type u_4
Q : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
inst_9 : Module.Flat R P
inst_10 : Module.Flat R N
hf : Function.Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Function.Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
⊢ Function.Injective (α := P ⊗[R] Q) (β := M ⊗[R] N)
    (⇑(LinearMap.rTensor N f ∘ₗ LinearMap.lTensor P g) : (a : P ⊗[R] Q) → M ⊗[R] N)

Tactic:
exact (Module.Flat.rTensor_preserves_injective_linearMap f hf).comp
    (Module.Flat.lTensor_preserves_injective_linearMap g hg)

Premises used: Module.Flat.lTensor_preserves_injective_linearMap, Function.Injective.comp, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
inst_5 : Module.Flat R M
hv : LinearIndependent R v
hw : LinearIndependent R w
⊢ Function.Injective (α := ι × κ →₀ R) (β := M ⊗[R] N)
    (Function.comp (β := (ι →₀ R) ⊗[R] (κ →₀ R))
      (⇑(map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w)) : (a : (ι →₀ R) ⊗[R] (κ →₀ R)) → M ⊗[R] N)
      (⇑(LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) : (a : ι × κ →₀ R) → (ι →₀ R) ⊗[R] (κ →₀ R)))

Tactic:
(TensorProduct.map_injective_of_flat_flat _ _ hv hw).comp
      (finsuppTensorFinsupp' _ _ _).symm.injective

Premises used: LinearEquiv.symm, TensorProduct.map_injective_of_flat_flat, Function.Injective.comp, finsuppTensorFinsupp', LinearEquiv.injective
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
inst_5 : Module.Flat R M
hv : LinearIndependent R v
hw : LinearIndependent R w
h :
  Eq (α := (ι × κ →₀ R) → M ⊗[R] N)
    (⇑(Finsupp.linearCombination R fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2) : (a : ι × κ →₀ R) → M ⊗[R] N)
    (Function.comp (β := (ι →₀ R) ⊗[R] (κ →₀ R))
      (⇑(map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w)) : (a : (ι →₀ R) ⊗[R] (κ →₀ R)) → M ⊗[R] N)
      (⇑(LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) : (a : ι × κ →₀ R) → (ι →₀ R) ⊗[R] (κ →₀ R)))
⊢ Function.Injective (α := ι × κ →₀ R) (β := M ⊗[R] N)
    (⇑(Finsupp.linearCombination R fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2) : (a : ι × κ →₀ R) → M ⊗[R] N)

Tactic:
convert!
    (TensorProduct.map_injective_of_flat_flat _ _ hv hw).comp
      (finsuppTensorFinsupp' _ _ _).symm.injective

Premises used: LinearEquiv.symm, TensorProduct.map_injective_of_flat_flat, Function.Injective.comp, finsuppTensorFinsupp', LinearEquiv.injective
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
inst_5 : Module.Flat R M
hv : LinearIndependent R v
hw : LinearIndependent R w
h :
  Eq (α := (ι × κ →₀ R) →ₗ[R] M ⊗[R] N) (Finsupp.linearCombination R fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2)
    (map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ
      (↑(LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) : (ι × κ →₀ R) →ₗ[R] (ι →₀ R) ⊗[R] (κ →₀ R)))
⊢ Eq (α := (ι × κ →₀ R) → M ⊗[R] N)
    (⇑(Finsupp.linearCombination R fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2) : (a : ι × κ →₀ R) → M ⊗[R] N)
    (⇑(map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ
          (↑(LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) : (ι × κ →₀ R) →ₗ[R] (ι →₀ R) ⊗[R] (κ →₀ R))) :
      (a : ι × κ →₀ R) → M ⊗[R] N)

Tactic:
congr!
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
inst_5 : Module.Flat R M
hv : LinearIndependent R v
hw : LinearIndependent R w
h :
  ∀ (i : ι × κ),
    Eq (α := M ⊗[R] N)
      (((Finsupp.linearCombination R fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2) ∘ₗ Finsupp.lsingle i : (a : R) → M ⊗[R] N) 1)
      (((map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ
              (↑(LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) : (ι × κ →₀ R) →ₗ[R] (ι →₀ R) ⊗[R] (κ →₀ R))) ∘ₗ
            Finsupp.lsingle i :
          (a : R) → M ⊗[R] N)
        1)
⊢ Eq (α := (ι × κ →₀ R) →ₗ[R] M ⊗[R] N) (Finsupp.linearCombination R fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2)
    (map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ
      (↑(LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) : (ι × κ →₀ R) →ₗ[R] (ι →₀ R) ⊗[R] (κ →₀ R)))

Tactic:
ext i