awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)

Tactic:
simp [finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

Premises used: finsuppTensorFinsupp'_symm_single_eq_single_one_tmul
-- 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
s : Set ι
t : Set κ
inst_5 : Module.Flat R M
hv : LinearIndepOn R v s
hw : LinearIndepOn R w t
⊢ LinearIndepOn R (M := M ⊗[R] N) (fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2) (s ×ˢ t)

Tactic:
((hv.tmul_of_flat_left hw).comp _ (Equiv.Set.prod _ _).injective :)

Premises used: LinearIndependent.tmul_of_flat_left, Equiv.Set.prod, Equiv.injective, TensorProduct.tmul, LinearIndependent.comp, LinearIndepOn
-- 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 N
hv : LinearIndependent R v
hw : LinearIndependent R w
⊢ LinearIndependent R (M := M ⊗[R] N) fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2

Tactic:
(((TensorProduct.comm R N M).toLinearMap.linearIndependent_iff_of_injOn
    (TensorProduct.comm R N M).injective.injOn).mpr
      (hw.tmul_of_flat_left hv)).comp Prod.swap Prod.swap_bijective.injective

Premises used: Iff.mpr, TensorProduct.comm, Quotient.liftOn', AddCon.liftOn, Function.Injective.injOn, Prod.swap_bijective, List.foldl, LinearIndependent.tmul_of_flat_left, Function.Bijective.injective, LinearEquiv.toLinearMap, LinearMap.linearIndependent_iff_of_injOn, TensorProduct.tmul, Prod.swap, LinearEquiv.injective, LinearIndependent.comp, 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
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
s : Set ι
t : Set κ
inst_5 : Module.Flat R N
hv : LinearIndepOn R v s
hw : LinearIndepOn R w t
⊢ LinearIndepOn R (M := M ⊗[R] N) (fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2) (s ×ˢ t)

Tactic:
((hv.tmul_of_flat_right hw).comp _ (Equiv.Set.prod _ _).injective :)

Premises used: Equiv.Set.prod, Equiv.injective, TensorProduct.tmul, LinearIndependent.tmul_of_flat_right, LinearIndependent.comp, LinearIndepOn
-- 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 : Submodule R M
q : Submodule R N
inst_5 : Module.Flat R M
inst_6 : Module.Flat.{u_1, u_3} R ↥q
⊢ Function.Injective (α := TensorProduct.{u_1, u_2, u_3} R ↥p ↥q) (β := M ⊗[R] N)
    (⇑(mapIncl p q) : (a : ↥p ⊗[R] ↥q) → M ⊗[R] N)

Tactic:
TensorProduct.map_injective_of_flat_flat _ _ p.subtype_injective q.subtype_injective

Premises used: TensorProduct.map_injective_of_flat_flat, Submodule.subtype_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
p : Submodule R M
q : Submodule R N
inst_5 : Module.Flat.{u_1, u_2} R ↥p
inst_6 : Module.Flat R N
⊢ Function.Injective (α := TensorProduct.{u_1, u_2, u_3} R ↥p ↥q) (β := M ⊗[R] N)
    (⇑(mapIncl p q) : (a : ↥p ⊗[R] ↥q) → M ⊗[R] N)

Tactic:
TensorProduct.map_injective_of_flat_flat' _ _ p.subtype_injective q.subtype_injective

Premises used: TensorProduct.map_injective_of_flat_flat', Submodule.subtype_injective
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
h : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
inst_5 : Module.Flat R A
inst_6 : Nontrivial A
⊢ Nontrivial (A ⊗[R] B)

Tactic:
TensorProduct.nontrivial_of_linearMap_injective_of_flat_left R A B (Algebra.linearMap R B) h

Premises used: Algebra.linearMap, TensorProduct.nontrivial_of_linearMap_injective_of_flat_left
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
inst_5 : Module.Flat R B
inst_6 : Nontrivial B
⊢ Nontrivial (A ⊗[R] B)

Tactic:
TensorProduct.nontrivial_of_linearMap_injective_of_flat_right R A B (Algebra.linearMap R A) h

Premises used: TensorProduct.nontrivial_of_linearMap_injective_of_flat_right, Algebra.linearMap
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₂ : Type u_8
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₂
inst_10 : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : M₁ →ₗ[R] N₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₂ →ₗ[R] N₂
hi : Function.Injective.{u_6 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i : (a : M₂) → N₂)
inst_11 : Module.Flat R M₁
x : M
⊢ Eq.{u_3 + 1} (α := N) ((hf.map hg LinearMap.id i : (a : M) → N) 0 : N)
    (Function.comp (α := M) (β := M₁ ⊗[R] N₂) (⇑hg.equiv : (a : M₁ ⊗[R] N₂) → N)
        (Function.comp (β := M₁ ⊗[R] M₂) (⇑(LinearMap.lTensor M₁ i) : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] N₂)
          (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂))
        0 :
      N)

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₂ : Type u_8
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₂
inst_10 : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : M₁ →ₗ[R] N₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₂ →ₗ[R] N₂
hi : Function.Injective.{u_6 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i : (a : M₂) → N₂)
inst_11 : Module.Flat R M₁
x : M
⊢ ∀ (x : M₁) (y : M₂),
    Eq.{u_3 + 1} (α := N)
      ((hf.map hg LinearMap.id i : (a : M) → N) ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M) :
        N)
      (Function.comp (α := M) (β := M₁ ⊗[R] N₂) (⇑hg.equiv : (a : M₁ ⊗[R] N₂) → N)
          (Function.comp (β := M₁ ⊗[R] M₂) (⇑(LinearMap.lTensor M₁ i) : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] N₂)
              (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂) :
            M → M₁ ⊗[R] N₂)
          ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M) :
        N)

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₂ : Type u_8
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₂
inst_10 : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : M₁ →ₗ[R] N₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₂ →ₗ[R] N₂
hi : Function.Injective.{u_6 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i : (a : M₂) → N₂)
inst_11 : Module.Flat R M₁
x x_1 x_2 : M
hx :
  Eq.{u_3 + 1} (α := N) ((hf.map hg LinearMap.id i : (a : M) → N) x_1 : N)
    (Function.comp (β := M₁ ⊗[R] N₂) (⇑hg.equiv : (a : M₁ ⊗[R] N₂) → N)
        (Function.comp (β := M₁ ⊗[R] M₂) (⇑(LinearMap.lTensor M₁ i) : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] N₂)
          (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂))
        x_1 :
      N)
hy :
  Eq.{u_3 + 1} (α := N) ((hf.map hg LinearMap.id i : (a : M) → N) x_2 : N)
    (Function.comp (β := M₁ ⊗[R] N₂) (⇑hg.equiv : (a : M₁ ⊗[R] N₂) → N)
        (Function.comp (β := M₁ ⊗[R] M₂) (⇑(LinearMap.lTensor M₁ i) : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] N₂)
          (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂))
        x_2 :
      N)
⊢ Eq.{u_3 + 1} (α := N) ((hf.map hg LinearMap.id i : (a : M) → N) (x_1 + x_2) : N)
    (Function.comp (β := M₁ ⊗[R] N₂) (⇑hg.equiv : (a : M₁ ⊗[R] N₂) → N)
        (Function.comp (β := M₁ ⊗[R] M₂) (⇑(LinearMap.lTensor M₁ i) : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] N₂)
          (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂))
        (x_1 + x_2) :
      N)

Tactic:
simp [hx, hy]
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₂ : Type u_8
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₂
inst_10 : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : M₁ →ₗ[R] N₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₂ →ₗ[R] N₂
hi : Function.Injective.{u_6 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i : (a : M₂) → N₂)
inst_11 : Module.Flat R M₁
⊢ Eq (α := (a : M) → N) (⇑(hf.map hg LinearMap.id i) : (a : M) → N)
    (Function.comp (β := M₁ ⊗[R] N₂) (⇑hg.equiv : (a : M₁ ⊗[R] N₂) → N)
      (Function.comp (β := M₁ ⊗[R] M₂) (⇑(LinearMap.lTensor M₁ i) : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] N₂)
        (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂)))

Tactic:
have h : hf.map hg LinearMap.id i = hg.equiv ∘ i.lTensor M₁ ∘ hf.equiv.symm :=
    funext fun x ↦ hf.inductionOn x (by simp) (by simp) (fun _ _ hx hy ↦ by simp [hx, hy])
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₂ : Type u_8
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₂
inst_10 : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : M₁ →ₗ[R] N₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₂ →ₗ[R] N₂
hi : Function.Injective.{u_6 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i : (a : M₂) → N₂)
inst_11 : Module.Flat R M₁
h :
  Eq (α := (a : M) → N) (⇑(hf.map hg LinearMap.id i) : (a : M) → N)
    (Function.comp (β := M₁ ⊗[R] N₂) (⇑hg.equiv : (a : M₁ ⊗[R] N₂) → N)
      (Function.comp (β := M₁ ⊗[R] M₂) (⇑(LinearMap.lTensor M₁ i) : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] N₂)
        (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂)))
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑(hf.map hg LinearMap.id i) : (a : M) → N)

Tactic:
simpa [h] using Module.Flat.lTensor_preserves_injective_linearMap i hi

Premises used: Module.Flat.lTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₁
inst_10 : Module R N₁
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : N₁ →ₗ[R] M₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₁ →ₗ[R] N₁
hi : Function.Injective.{u_5 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i : (a : M₁) → N₁)
inst_11 : Module.Flat R M₂
x : M
⊢ Eq.{u_3 + 1} (α := N) ((hf.map hg i LinearMap.id : (a : M) → N) 0 : N)
    (Function.comp (α := M) (β := N₁ ⊗[R] M₂) (⇑hg.equiv : (a : N₁ ⊗[R] M₂) → N)
        (Function.comp (β := M₁ ⊗[R] M₂) (⇑(LinearMap.rTensor M₂ i) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] M₂)
          (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂))
        0 :
      N)

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₁
inst_10 : Module R N₁
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : N₁ →ₗ[R] M₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₁ →ₗ[R] N₁
hi : Function.Injective.{u_5 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i : (a : M₁) → N₁)
inst_11 : Module.Flat R M₂
x : M
⊢ ∀ (x : M₁) (y : M₂),
    Eq.{u_3 + 1} (α := N)
      ((hf.map hg i LinearMap.id : (a : M) → N) ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M) :
        N)
      (Function.comp (α := M) (β := N₁ ⊗[R] M₂) (⇑hg.equiv : (a : N₁ ⊗[R] M₂) → N)
          (Function.comp (β := M₁ ⊗[R] M₂) (⇑(LinearMap.rTensor M₂ i) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] M₂)
              (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂) :
            M → N₁ ⊗[R] M₂)
          ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M) :
        N)

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₁
inst_10 : Module R N₁
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : N₁ →ₗ[R] M₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₁ →ₗ[R] N₁
hi : Function.Injective.{u_5 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i : (a : M₁) → N₁)
inst_11 : Module.Flat R M₂
x x_1 x_2 : M
hx :
  Eq.{u_3 + 1} (α := N) ((hf.map hg i LinearMap.id : (a : M) → N) x_1 : N)
    (Function.comp (β := N₁ ⊗[R] M₂) (⇑hg.equiv : (a : N₁ ⊗[R] M₂) → N)
        (Function.comp (β := M₁ ⊗[R] M₂) (⇑(LinearMap.rTensor M₂ i) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] M₂)
          (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂))
        x_1 :
      N)
hy :
  Eq.{u_3 + 1} (α := N) ((hf.map hg i LinearMap.id : (a : M) → N) x_2 : N)
    (Function.comp (β := N₁ ⊗[R] M₂) (⇑hg.equiv : (a : N₁ ⊗[R] M₂) → N)
        (Function.comp (β := M₁ ⊗[R] M₂) (⇑(LinearMap.rTensor M₂ i) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] M₂)
          (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂))
        x_2 :
      N)
⊢ Eq.{u_3 + 1} (α := N) ((hf.map hg i LinearMap.id : (a : M) → N) (x_1 + x_2) : N)
    (Function.comp (β := N₁ ⊗[R] M₂) (⇑hg.equiv : (a : N₁ ⊗[R] M₂) → N)
        (Function.comp (β := M₁ ⊗[R] M₂) (⇑(LinearMap.rTensor M₂ i) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] M₂)
          (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂))
        (x_1 + x_2) :
      N)

Tactic:
simp [hx, hy]
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₁
inst_10 : Module R N₁
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : N₁ →ₗ[R] M₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₁ →ₗ[R] N₁
hi : Function.Injective.{u_5 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i : (a : M₁) → N₁)
inst_11 : Module.Flat R M₂
⊢ Eq (α := (a : M) → N) (⇑(hf.map hg i LinearMap.id) : (a : M) → N)
    (Function.comp (β := N₁ ⊗[R] M₂) (⇑hg.equiv : (a : N₁ ⊗[R] M₂) → N)
      (Function.comp (β := M₁ ⊗[R] M₂) (⇑(LinearMap.rTensor M₂ i) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] M₂)
        (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂)))

Tactic:
have h : hf.map hg i LinearMap.id = hg.equiv ∘ i.rTensor M₂ ∘ hf.equiv.symm :=
    funext fun x ↦ hf.inductionOn x (by simp) (by simp) (fun _ _ hx hy ↦ by simp [hx, hy])
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₁
inst_10 : Module R N₁
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : N₁ →ₗ[R] M₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₁ →ₗ[R] N₁
hi : Function.Injective.{u_5 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i : (a : M₁) → N₁)
inst_11 : Module.Flat R M₂
h :
  Eq (α := (a : M) → N) (⇑(hf.map hg i LinearMap.id) : (a : M) → N)
    (Function.comp (β := N₁ ⊗[R] M₂) (⇑hg.equiv : (a : N₁ ⊗[R] M₂) → N)
      (Function.comp (β := M₁ ⊗[R] M₂) (⇑(LinearMap.rTensor M₂ i) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] M₂)
        (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂)))
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑(hf.map hg i LinearMap.id) : (a : M) → N)

Tactic:
simpa [h] using Module.Flat.rTensor_preserves_injective_linearMap i hi

Premises used: Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : Module R N₁
inst_12 : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective.{u_5 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
h₂ : Function.Injective.{u_6 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
inst_13 : Module.Flat R M₂
inst_14 : Module.Flat R N₁
x : M
⊢ Eq.{u_3 + 1} (α := N) ((hf.map hg i₁ i₂ : (a : M) → N) 0 : N)
    (Function.comp (α := M) (β := N₁ ⊗[R] N₂) (⇑hg.equiv : (a : N₁ ⊗[R] N₂) → N)
        (Function.comp (β := M₁ ⊗[R] M₂) (⇑(TensorProduct.map i₁ i₂) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
          (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂))
        0 :
      N)

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : Module R N₁
inst_12 : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective.{u_5 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
h₂ : Function.Injective.{u_6 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
inst_13 : Module.Flat R M₂
inst_14 : Module.Flat R N₁
x : M
⊢ ∀ (x : M₁) (y : M₂),
    Eq.{u_3 + 1} (α := N)
      ((hf.map hg i₁ i₂ : (a : M) → N) ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M) : N)
      (Function.comp (α := M) (β := N₁ ⊗[R] N₂) (⇑hg.equiv : (a : N₁ ⊗[R] N₂) → N)
          (Function.comp (β := M₁ ⊗[R] M₂) (⇑(TensorProduct.map i₁ i₂) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
              (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂) :
            M → N₁ ⊗[R] N₂)
          ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M) :
        N)

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : Module R N₁
inst_12 : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective.{u_5 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
h₂ : Function.Injective.{u_6 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
inst_13 : Module.Flat R M₂
inst_14 : Module.Flat R N₁
x x_1 x_2 : M
hx :
  Eq.{u_3 + 1} (α := N) ((hf.map hg i₁ i₂ : (a : M) → N) x_1 : N)
    (Function.comp (β := N₁ ⊗[R] N₂) (⇑hg.equiv : (a : N₁ ⊗[R] N₂) → N)
        (Function.comp (β := M₁ ⊗[R] M₂) (⇑(TensorProduct.map i₁ i₂) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
          (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂))
        x_1 :
      N)
hy :
  Eq.{u_3 + 1} (α := N) ((hf.map hg i₁ i₂ : (a : M) → N) x_2 : N)
    (Function.comp (β := N₁ ⊗[R] N₂) (⇑hg.equiv : (a : N₁ ⊗[R] N₂) → N)
        (Function.comp (β := M₁ ⊗[R] M₂) (⇑(TensorProduct.map i₁ i₂) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
          (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂))
        x_2 :
      N)
⊢ Eq.{u_3 + 1} (α := N) ((hf.map hg i₁ i₂ : (a : M) → N) (x_1 + x_2) : N)
    (Function.comp (β := N₁ ⊗[R] N₂) (⇑hg.equiv : (a : N₁ ⊗[R] N₂) → N)
        (Function.comp (β := M₁ ⊗[R] M₂) (⇑(TensorProduct.map i₁ i₂) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
          (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂))
        (x_1 + x_2) :
      N)

Tactic:
simp [hx, hy]
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : Module R N₁
inst_12 : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective.{u_5 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
h₂ : Function.Injective.{u_6 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
inst_13 : Module.Flat R M₂
inst_14 : Module.Flat R N₁
⊢ Eq (α := (a : M) → N) (⇑(hf.map hg i₁ i₂) : (a : M) → N)
    (Function.comp (β := N₁ ⊗[R] N₂) (⇑hg.equiv : (a : N₁ ⊗[R] N₂) → N)
      (Function.comp (β := M₁ ⊗[R] M₂) (⇑(TensorProduct.map i₁ i₂) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
        (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂)))

Tactic:
have h : hf.map hg i₁ i₂ = hg.equiv ∘ TensorProduct.map i₁ i₂ ∘ hf.equiv.symm :=
    funext fun x ↦ hf.inductionOn x (by simp) (by simp) (fun _ _ hx hy ↦ by simp [hx, hy])
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : Module R N₁
inst_12 : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective.{u_5 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
h₂ : Function.Injective.{u_6 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
inst_13 : Module.Flat R M₂
inst_14 : Module.Flat R N₁
h :
  Eq (α := (a : M) → N) (⇑(hf.map hg i₁ i₂) : (a : M) → N)
    (Function.comp (β := N₁ ⊗[R] N₂) (⇑hg.equiv : (a : N₁ ⊗[R] N₂) → N)
      (Function.comp (β := M₁ ⊗[R] M₂) (⇑(TensorProduct.map i₁ i₂) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
        (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂)))
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑(hf.map hg i₁ i₂) : (a : M) → N)

Tactic:
simpa [h] using map_injective_of_flat_flat i₁ i₂ h₁ h₂

Premises used: TensorProduct.map_injective_of_flat_flat