awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
N' : Submodule R S
hN : N' ≤ N
hFG : Module.Finite.{u, v} R ↥N'
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))
⊢ N'.FG

Tactic:
rw [Module.Finite.iff_fg] at hFG

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
N' : Submodule R S
hN : N' ≤ N
hFG : Module.Finite.{u, v} R ↥N'
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))
hFG₁ : N'.FG
⊢ {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))

Tactic:
rw [Module.Finite.iff_fg] at hFG

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))
⊢ Membership.mem (γ := Set (↥M ⊗[R] ↥N)) {x, y} x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))
obtain :
  ∀ (x' : ↥M ⊗[R] ↥N') (hx' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) x' = x), x = y
⊢ x = y

Tactic:
obtain ⟨x', hx'⟩ := h (show x ∈ {x, y} by simp)
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) x' = x
⊢ Membership.mem (γ := Set (↥M ⊗[R] ↥N)) {x, y} y

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) x' = x
obtain :
  ∀ (y' : ↥M ⊗[R] ↥N') (hy' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) y' = y), x = y
⊢ x = y

Tactic:
obtain ⟨y', hy'⟩ := h (show y ∈ {x, y} by simp)
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) x' = x
y' : ↥M ⊗[R] ↥N'
hy' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) y' = y
rw :
  Eq (α := ↥M ⊗[R] ↥N) ((LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) x' : ↥M ⊗[R] ↥N)
    ((LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) y' : ↥M ⊗[R] ↥N)
⊢ x = y

Tactic:
rw [← hx', ← hy']
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) x' = x
y' : ↥M ⊗[R] ↥N'
hy' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) y' = y
h₁ : x' = y'
⊢ Eq (α := ↥M ⊗[R] ↥N) ((LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) x' : ↥M ⊗[R] ↥N)
    ((LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) y' : ↥M ⊗[R] ↥N)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) x' = x
y' : ↥M ⊗[R] ↥N'
hy' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) y' = y
⊢ Eq (α := S) ((M.mulMap N' : (a : ↥M ⊗[R] ↥N') → S) x' : S) ((M.mulMap N' : (a : ↥M ⊗[R] ↥N') → S) y' : S)

Tactic:
simp [← mulMap_comp_lTensor _ hN, hx', hy', hxy]

Premises used: Submodule.mulMap_comp_lTensor
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) x' = x
y' : ↥M ⊗[R] ↥N'
hy' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) y' = y
⊢ x' = y'

Tactic:
exact (H N' hN hFG).injective (by simp [← mulMap_comp_lTensor _ hN, hx', hy', hxy])

Premises used: Submodule.LinearDisjoint.injective
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ (M' N' : Submodule R S), M' ≤ M → N' ≤ N → M'.FG → N'.FG → M'.LinearDisjoint N'
⊢ M.LinearDisjoint N

Tactic:
of_linearDisjoint_fg_left _ _ fun _ hM hM' ↦
    of_linearDisjoint_fg_right _ _ fun _ hN hN' ↦ H _ _ hM hN hM' hN'

Premises used: Submodule.LinearDisjoint.of_linearDisjoint_fg_left, Submodule.LinearDisjoint.of_linearDisjoint_fg_right
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
⊢ N.LinearDisjoint M

Tactic:
H.symm_of_commute fun _ _ ↦ mul_comm _ _

Premises used: Submodule.LinearDisjoint.symm_of_commute, mul_comm, Subtype.val
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submodule R S
⊢ M.LinearDisjoint N ↔ N.LinearDisjoint M

Tactic:
⟨LinearDisjoint.symm, LinearDisjoint.symm⟩

Premises used: Submodule.LinearDisjoint.symm, Iff.intro
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ (mulLeftMap N m).ker = ⊥

Tactic:
LinearMap.ker_eq_bot_of_injective ?_

Premises used: LinearMap.ker_eq_bot_of_injective
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
refine : Function.Injective (α := Finsupp.{u_1, v} ι ↥N) (β := S) (⇑(mulLeftMap N m) : (a : ι →₀ ↥N) → S)
⊢ (mulLeftMap N m).ker = ⊥

Tactic:
refine LinearMap.ker_eq_bot_of_injective ?_

Premises used: LinearMap.ker_eq_bot_of_injective
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
simp_rw :
  Function.Injective (α := (ι →₀ R) ⊗[R] ↥N) (β := S)
    (Function.comp (β := ↥M ⊗[R] ↥N) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
      (⇑(LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)) : (a : (ι →₀ R) ⊗[R] ↥N) → ↥M ⊗[R] ↥N))
⊢ Function.Injective (α := Finsupp.{u_1, v} ι ↥N) (β := S) (⇑(mulLeftMap N m) : (a : ι →₀ ↥N) → S)

Tactic:
simp_rw [mulLeftMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe,
    ← Function.comp_assoc, EquivLike.injective_comp]

Premises used: EquivLike.injective_comp, LinearMap.coe_comp, Submodule.mulLeftMap_eq_mulMap_comp, LinearEquiv.coe_coe, Function.comp_assoc
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
classical :
  Function.Injective (α := (ι →₀ R) ⊗[R] ↥N) (β := S)
    (Function.comp (β := ↥M ⊗[R] ↥N) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
      (⇑(LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)) : (a : (ι →₀ R) ⊗[R] ↥N) → ↥M ⊗[R] ↥N))
⊢ Function.Injective (α := Finsupp.{u_1, v} ι ↥N) (β := S) (⇑(mulLeftMap N m) : (a : ι →₀ ↥N) → S)

Tactic:
classical simp_rw [mulLeftMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe,
    ← Function.comp_assoc, EquivLike.injective_comp]

Premises used: EquivLike.injective_comp, LinearMap.coe_comp, Submodule.mulLeftMap_eq_mulMap_comp, LinearEquiv.coe_coe, Function.comp_assoc
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective (α := ι →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : ι →₀ R) → ↥M)

Tactic:
rw [LinearIndependent] at hm

Premises used: LinearIndependent
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥N
ι : Type u_1
m : ι → ↥M
hm : Function.Injective (α := ι →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : ι →₀ R) → ↥M)
⊢ Function.Injective (α := (ι →₀ R) ⊗[R] ↥N) (β := S)
    (Function.comp (β := ↥M ⊗[R] ↥N) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
      (⇑(LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)) : (a : (ι →₀ R) ⊗[R] ↥N) → ↥M ⊗[R] ↥N))

Tactic:
H.injective.comp (Module.Flat.rTensor_preserves_injective_linearMap (M := N) _ hm)

Premises used: Submodule.LinearDisjoint.injective, Function.Injective.comp, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥N
ι : Type u_1
m : ι → ↥M
hm : Function.Injective (α := ι →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : ι →₀ R) → ↥M)
⊢ Function.Injective (α := (ι →₀ R) ⊗[R] ↥N) (β := S)
    (Function.comp (β := ↥M ⊗[R] ↥N) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
      (⇑(LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)) : (a : (ι →₀ R) ⊗[R] ↥N) → ↥M ⊗[R] ↥N))

Tactic:
exact H.injective.comp (Module.Flat.rTensor_preserves_injective_linearMap (M := N) _ hm)

Premises used: Submodule.LinearDisjoint.injective, Function.Injective.comp, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
ι : Type u_1
m : Basis.{u_1, u, v} ι R ↥M
H : Eq (α := Submodule R (Finsupp.{u_1, v} ι ↥N)) (LinearMap.ker (mulLeftMap (M := M) N (⇑m : (a : ι) → ↥M))) ⊥
⊢ M.LinearDisjoint N

Tactic:
of_basis_left' M N m (LinearMap.ker_eq_bot.1 H)

Premises used: Submodule.LinearDisjoint.of_basis_left'
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥M
ι : Type u_1
n : ι → ↥N
hn : LinearIndependent R n
⊢ (M.mulRightMap n).ker = ⊥

Tactic:
LinearMap.ker_eq_bot_of_injective ?_

Premises used: LinearMap.ker_eq_bot_of_injective
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥M
ι : Type u_1
n : ι → ↥N
hn : LinearIndependent R n
refine : Function.Injective (α := Finsupp.{u_1, v} ι ↥M) (β := S) (⇑(M.mulRightMap n) : (a : ι →₀ ↥M) → S)
⊢ (M.mulRightMap n).ker = ⊥

Tactic:
refine LinearMap.ker_eq_bot_of_injective ?_

Premises used: LinearMap.ker_eq_bot_of_injective
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥M
ι : Type u_1
n : ι → ↥N
hn : LinearIndependent R n
simp_rw :
  Function.Injective (α := ↥M ⊗[R] (ι →₀ R)) (β := S)
    (Function.comp (β := ↥M ⊗[R] ↥N) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
      (⇑(LinearMap.lTensor (↥M) (Finsupp.linearCombination R n)) : (a : ↥M ⊗[R] (ι →₀ R)) → ↥M ⊗[R] ↥N))
⊢ Function.Injective (α := Finsupp.{u_1, v} ι ↥M) (β := S) (⇑(M.mulRightMap n) : (a : ι →₀ ↥M) → S)

Tactic:
simp_rw [mulRightMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe,
    ← Function.comp_assoc, EquivLike.injective_comp]

Premises used: EquivLike.injective_comp, Submodule.mulRightMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_assoc
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥M
ι : Type u_1
n : ι → ↥N
hn : LinearIndependent R n
classical :
  Function.Injective (α := ↥M ⊗[R] (ι →₀ R)) (β := S)
    (Function.comp (β := ↥M ⊗[R] ↥N) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
      (⇑(LinearMap.lTensor (↥M) (Finsupp.linearCombination R n)) : (a : ↥M ⊗[R] (ι →₀ R)) → ↥M ⊗[R] ↥N))
⊢ Function.Injective (α := Finsupp.{u_1, v} ι ↥M) (β := S) (⇑(M.mulRightMap n) : (a : ι →₀ ↥M) → S)

Tactic:
classical simp_rw [mulRightMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe,
    ← Function.comp_assoc, EquivLike.injective_comp]

Premises used: EquivLike.injective_comp, Submodule.mulRightMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_assoc
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥M
ι : Type u_1
n : ι → ↥N
hn : LinearIndependent R n
⊢ Function.Injective (α := ι →₀ R) (β := ↥N) (⇑(Finsupp.linearCombination R n) : (a : ι →₀ R) → ↥N)

Tactic:
rw [LinearIndependent] at hn

Premises used: LinearIndependent
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥M
ι : Type u_1
n : ι → ↥N
hn : Function.Injective (α := ι →₀ R) (β := ↥N) (⇑(Finsupp.linearCombination R n) : (a : ι →₀ R) → ↥N)
⊢ Function.Injective (α := ↥M ⊗[R] (ι →₀ R)) (β := S)
    (Function.comp (β := ↥M ⊗[R] ↥N) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
      (⇑(LinearMap.lTensor (↥M) (Finsupp.linearCombination R n)) : (a : ↥M ⊗[R] (ι →₀ R)) → ↥M ⊗[R] ↥N))

Tactic:
H.injective.comp (Module.Flat.lTensor_preserves_injective_linearMap (M := M) _ hn)

Premises used: Module.Flat.lTensor_preserves_injective_linearMap, Submodule.LinearDisjoint.injective, Function.Injective.comp
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥M
ι : Type u_1
n : ι → ↥N
hn : Function.Injective (α := ι →₀ R) (β := ↥N) (⇑(Finsupp.linearCombination R n) : (a : ι →₀ R) → ↥N)
⊢ Function.Injective (α := ↥M ⊗[R] (ι →₀ R)) (β := S)
    (Function.comp (β := ↥M ⊗[R] ↥N) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
      (⇑(LinearMap.lTensor (↥M) (Finsupp.linearCombination R n)) : (a : ↥M ⊗[R] (ι →₀ R)) → ↥M ⊗[R] ↥N))

Tactic:
exact H.injective.comp (Module.Flat.lTensor_preserves_injective_linearMap (M := M) _ hn)

Premises used: Module.Flat.lTensor_preserves_injective_linearMap, Submodule.LinearDisjoint.injective, Function.Injective.comp
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
ι : Type u_1
n : Basis.{u_1, u, v} ι R ↥N
H : Eq (α := Submodule R (Finsupp.{u_1, v} ι ↥M)) (LinearMap.ker (M.mulRightMap (N := N) (⇑n : (a : ι) → ↥N))) ⊥
⊢ M.LinearDisjoint N

Tactic:
of_basis_right' M N n (LinearMap.ker_eq_bot.1 H)

Premises used: Submodule.LinearDisjoint.of_basis_right'
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥M
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
⊢ Function.Injective (α := κ →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : κ →₀ R) → ↥M)

Tactic:
rw [LinearIndependent] at hm hn ⊢

Premises used: LinearIndependent
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥M
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
hm₁ : Function.Injective (α := κ →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : κ →₀ R) → ↥M)
⊢ Function.Injective (α := ι →₀ R) (β := ↥N) (⇑(Finsupp.linearCombination R n) : (a : ι →₀ R) → ↥N)

Tactic:
rw [LinearIndependent] at hm hn ⊢

Premises used: LinearIndependent
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥M
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective (α := κ →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : κ →₀ R) → ↥M)
hn : Function.Injective (α := ι →₀ R) (β := ↥N) (⇑(Finsupp.linearCombination R n) : (a : ι →₀ R) → ↥N)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] (ι →₀ R) := LinearMap.rTensor (ι →₀ R) (Finsupp.linearCombination R m)
i2 : ↥M ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.lTensor (↥M) (Finsupp.linearCombination R n)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
⊢ Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := ↥M ⊗[R] (ι →₀ R))
    (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → ↥M ⊗[R] (ι →₀ R))

Tactic:
have h1 : Function.Injective i1 := Module.Flat.rTensor_preserves_injective_linearMap _ hm
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥M
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective (α := κ →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : κ →₀ R) → ↥M)
hn : Function.Injective (α := ι →₀ R) (β := ↥N) (⇑(Finsupp.linearCombination R n) : (a : ι →₀ R) → ↥N)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] (ι →₀ R) := LinearMap.rTensor (ι →₀ R) (Finsupp.linearCombination R m)
i2 : ↥M ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.lTensor (↥M) (Finsupp.linearCombination R n)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
h1 :
  Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := ↥M ⊗[R] (ι →₀ R))
    (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → ↥M ⊗[R] (ι →₀ R))
⊢ Function.Injective (α := ↥M ⊗[R] (ι →₀ R)) (β := ↥M ⊗[R] ↥N) (⇑i2 : (a : ↥M ⊗[R] (ι →₀ R)) → ↥M ⊗[R] ↥N)

Tactic:
have h2 : Function.Injective i2 := Module.Flat.lTensor_preserves_injective_linearMap _ hn
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥M
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective (α := κ →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : κ →₀ R) → ↥M)
hn : Function.Injective (α := ι →₀ R) (β := ↥N) (⇑(Finsupp.linearCombination R n) : (a : ι →₀ R) → ↥N)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] (ι →₀ R) := LinearMap.rTensor (ι →₀ R) (Finsupp.linearCombination R m)
i2 : ↥M ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.lTensor (↥M) (Finsupp.linearCombination R n)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
h1 :
  Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := ↥M ⊗[R] (ι →₀ R))
    (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → ↥M ⊗[R] (ι →₀ R))
h2 : Function.Injective (α := ↥M ⊗[R] (ι →₀ R)) (β := ↥M ⊗[R] ↥N) (⇑i2 : (a : ↥M ⊗[R] (ι →₀ R)) → ↥M ⊗[R] ↥N)
⊢ Function.Injective (α := κ × ι →₀ R) (β := S) (⇑i : (a : κ × ι →₀ R) → S)

Tactic:
have h : Function.Injective i := H.injective.comp h2 |>.comp h1 |>.comp i0.injective