awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
h : Function.Injective (α := κ × ι →₀ R) (β := S) (⇑i : (a : κ × ι →₀ R) → S)
h₁ :
  ∀ (x : κ × ι),
    Eq.{v + 1} (α := S) ((i ∘ₗ Finsupp.lsingle x : (a : R) → S) 1 : S)
      (((Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) ∘ₗ Finsupp.lsingle x :
            (a : R) → S)
          1 :
        S)
⊢ i = Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)

Tactic:
ext x
-- 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)
h : Function.Injective (α := κ × ι →₀ R) (β := S) (⇑i : (a : κ × ι →₀ R) → S)
x : κ × ι
⊢ Eq.{v + 1} (α := S) ((i ∘ₗ Finsupp.lsingle x : (a : R) → S) 1 : S)
    (((Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) ∘ₗ Finsupp.lsingle x :
          (a : R) → S)
        1 :
      S)

Tactic:
simp [i, i0, i1, i2, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

Premises used: finsuppTensorFinsupp'_symm_single_eq_single_one_tmul
-- 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)
h : Function.Injective (α := κ × ι →₀ R) (β := S) (⇑i : (a : κ × ι →₀ R) → S)
⊢ i = Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)

Tactic:
have : i = Finsupp.linearCombination R fun i ↦ (m i.1).1 * (n i.2).1 := by
    ext x
    simp [i, i0, i1, i2, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]
-- 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)
h : Function.Injective (α := κ × ι →₀ R) (β := S) (⇑i : (a : κ × ι →₀ R) → S)
this : i = Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (h :
      Function.Injective (α := κ × ι →₀ R) (β := S)
        (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S))
    (this : i = Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)),
    Function.Injective (α := κ × ι →₀ R) (β := S)
      (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S)
⊢ Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S)

Tactic:
rwa [this] at h
-- 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
ι : 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 ↥N
κ : 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 ↥N
κ : 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] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
⊢ Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := (κ →₀ R) ⊗[R] ↥N)
    (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → (κ →₀ R) ⊗[R] ↥N)

Tactic:
have h1 : Function.Injective i1 := 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 ↥N
κ : 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] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
h1 :
  Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := (κ →₀ R) ⊗[R] ↥N)
    (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → (κ →₀ R) ⊗[R] ↥N)
⊢ Function.Injective (α := (κ →₀ R) ⊗[R] ↥N) (β := ↥M ⊗[R] ↥N) (⇑i2 : (a : (κ →₀ R) ⊗[R] ↥N) → ↥M ⊗[R] ↥N)

Tactic:
have h2 : Function.Injective i2 := 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 ↥N
κ : 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] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
h1 :
  Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := (κ →₀ R) ⊗[R] ↥N)
    (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → (κ →₀ R) ⊗[R] ↥N)
h2 : Function.Injective (α := (κ →₀ R) ⊗[R] ↥N) (β := ↥M ⊗[R] ↥N) (⇑i2 : (a : (κ →₀ R) ⊗[R] ↥N) → ↥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
-- 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
ι : 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] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
h1 :
  Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := (κ →₀ R) ⊗[R] ↥N)
    (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → (κ →₀ R) ⊗[R] ↥N)
h2 : Function.Injective (α := (κ →₀ R) ⊗[R] ↥N) (β := ↥M ⊗[R] ↥N) (⇑i2 : (a : (κ →₀ R) ⊗[R] ↥N) → ↥M ⊗[R] ↥N)
h : Function.Injective (α := κ × ι →₀ R) (β := S) (⇑i : (a : κ × ι →₀ R) → S)
h₁ :
  ∀ (x : κ × ι),
    Eq.{v + 1} (α := S) ((i ∘ₗ Finsupp.lsingle x : (a : R) → S) 1 : S)
      (((Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) ∘ₗ Finsupp.lsingle x :
            (a : R) → S)
          1 :
        S)
⊢ i = Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)

Tactic:
ext x
-- 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
ι : 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] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
h1 :
  Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := (κ →₀ R) ⊗[R] ↥N)
    (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → (κ →₀ R) ⊗[R] ↥N)
h2 : Function.Injective (α := (κ →₀ R) ⊗[R] ↥N) (β := ↥M ⊗[R] ↥N) (⇑i2 : (a : (κ →₀ R) ⊗[R] ↥N) → ↥M ⊗[R] ↥N)
h : Function.Injective (α := κ × ι →₀ R) (β := S) (⇑i : (a : κ × ι →₀ R) → S)
x : κ × ι
⊢ Eq.{v + 1} (α := S) ((i ∘ₗ Finsupp.lsingle x : (a : R) → S) 1 : S)
    (((Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) ∘ₗ Finsupp.lsingle x :
          (a : R) → S)
        1 :
      S)

Tactic:
simp [i, i0, i1, i2, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

Premises used: finsuppTensorFinsupp'_symm_single_eq_single_one_tmul
-- 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
ι : 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] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
h1 :
  Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := (κ →₀ R) ⊗[R] ↥N)
    (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → (κ →₀ R) ⊗[R] ↥N)
h2 : Function.Injective (α := (κ →₀ R) ⊗[R] ↥N) (β := ↥M ⊗[R] ↥N) (⇑i2 : (a : (κ →₀ R) ⊗[R] ↥N) → ↥M ⊗[R] ↥N)
h : Function.Injective (α := κ × ι →₀ R) (β := S) (⇑i : (a : κ × ι →₀ R) → S)
⊢ i = Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)

Tactic:
have : i = Finsupp.linearCombination R fun i ↦ (m i.1).1 * (n i.2).1 := by
    ext x
    simp [i, i0, i1, i2, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]
-- 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
ι : 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] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
h1 :
  Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := (κ →₀ R) ⊗[R] ↥N)
    (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → (κ →₀ R) ⊗[R] ↥N)
h2 : Function.Injective (α := (κ →₀ R) ⊗[R] ↥N) (β := ↥M ⊗[R] ↥N) (⇑i2 : (a : (κ →₀ R) ⊗[R] ↥N) → ↥M ⊗[R] ↥N)
h : Function.Injective (α := κ × ι →₀ R) (β := S) (⇑i : (a : κ × ι →₀ R) → S)
this : i = Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (h :
      Function.Injective (α := κ × ι →₀ R) (β := S)
        (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S))
    (this : i = Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)),
    Function.Injective (α := κ × ι →₀ R) (β := S)
      (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S)
⊢ Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S)

Tactic:
rwa [this] at h
-- 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
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
inl : Flat.{u, v} R ↥M → LinearIndependent R (M := S) fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)
inr : Flat.{u, v} R ↥N → LinearIndependent R (M := S) fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)
⊢ LinearIndependent R (M := S) fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)

Tactic:
rcases hf with _ | _
-- 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
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
h : Flat.{u, v} R ↥M
⊢ LinearIndependent R (M := S) fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)

Tactic:
H.linearIndependent_mul_of_flat_left hm hn

Premises used: Submodule.LinearDisjoint.linearIndependent_mul_of_flat_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
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
h : Flat.{u, v} R ↥M
⊢ LinearIndependent R (M := S) fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)

Tactic:
exact H.linearIndependent_mul_of_flat_left hm hn

Premises used: Submodule.LinearDisjoint.linearIndependent_mul_of_flat_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
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
h : Flat.{u, v} R ↥N
⊢ LinearIndependent R (M := S) fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)

Tactic:
H.linearIndependent_mul_of_flat_right hm hn

Premises used: Submodule.LinearDisjoint.linearIndependent_mul_of_flat_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
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
h : Flat.{u, v} R ↥N
⊢ LinearIndependent R (M := S) fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)

Tactic:
exact H.linearIndependent_mul_of_flat_right hm hn

Premises used: Submodule.LinearDisjoint.linearIndependent_mul_of_flat_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
κ : Type u_1
ι : Type u_2
m : Basis.{u_1, u, v} κ R ↥M
n : Basis.{u_2, u, v} ι R ↥N
H :
  LinearIndependent R (M := S) fun (i : κ × ι) ↦
    HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)
⊢ Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦
          HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)) :
      (a : κ × ι →₀ R) → S)

Tactic:
rw [LinearIndependent] at H

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
κ : Type u_1
ι : Type u_2
m : Basis.{u_1, u, v} κ R ↥M
n : Basis.{u_2, u, v} ι R ↥N
H :
  Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦
          HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)) :
      (a : κ × ι →₀ R) → S)
⊢ M.LinearDisjoint N

Tactic:
of_basis_mul' M N m n H

Premises used: Submodule.LinearDisjoint.of_basis_mul'
-- 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
ι : Type u_2
m : Basis.{u_1, u, v} κ R ↥M
n : Basis.{u_2, u, v} ι R ↥N
H :
  Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦
          HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)) :
      (a : κ × ι →₀ R) → S)
⊢ M.LinearDisjoint N

Tactic:
exact of_basis_mul' M N m n H

Premises used: Submodule.LinearDisjoint.of_basis_mul'
-- 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
M' : Submodule R S
h : M' ≤ M
inst_3 : Flat.{u, v} R ↥N
i : ↥M' ⊗[R] ↥N →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (inclusion h)
⊢ Function.Injective (α := ↥M' ⊗[R] ↥N) (β := S) (⇑i : (a : ↥M' ⊗[R] ↥N) → S)

Tactic:
have hi : Function.Injective i := H.injective.comp <|
    Module.Flat.rTensor_preserves_injective_linearMap _ <| inclusion_injective h
-- 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
M' : Submodule R S
h : M' ≤ M
inst_3 : Flat.{u, v} R ↥N
i : ↥M' ⊗[R] ↥N →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (inclusion h)
hi : Function.Injective (α := ↥M' ⊗[R] ↥N) (β := S) (⇑i : (a : ↥M' ⊗[R] ↥N) → S)
a :
  ∀ (x : ↥M') (x_1 : ↥N),
    Eq (α := S)
      (((((TensorProduct.AlgebraTensorModule.curry i : ↥M' →ₗ[R] ↥N →ₗ[R] S) : (a : ↥M') → ↥N →ₗ[R] S) x : ↥N →ₗ[R] S) :
            (a : ↥N) → S)
          x_1 :
        S)
      (((((TensorProduct.AlgebraTensorModule.curry (M'.mulMap N) : ↥M' →ₗ[R] ↥N →ₗ[R] S) : (a : ↥M') → ↥N →ₗ[R] S) x :
              ↥N →ₗ[R] S) :
            (a : ↥N) → S)
          x_1 :
        S)
⊢ i = M'.mulMap N

Tactic:
ext
-- 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
M' : Submodule R S
h : M' ≤ M
inst_3 : Flat.{u, v} R ↥N
i : ↥M' ⊗[R] ↥N →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (inclusion h)
hi : Function.Injective (α := ↥M' ⊗[R] ↥N) (β := S) (⇑i : (a : ↥M' ⊗[R] ↥N) → S)
x : ↥M'
x_1 : ↥N
⊢ Eq (α := S)
    (((((TensorProduct.AlgebraTensorModule.curry i : ↥M' →ₗ[R] ↥N →ₗ[R] S) : (a : ↥M') → ↥N →ₗ[R] S) x : ↥N →ₗ[R] S) :
          (a : ↥N) → S)
        x_1 :
      S)
    (((((TensorProduct.AlgebraTensorModule.curry (M'.mulMap N) : ↥M' →ₗ[R] ↥N →ₗ[R] S) : (a : ↥M') → ↥N →ₗ[R] S) x :
            ↥N →ₗ[R] S) :
          (a : ↥N) → S)
        x_1 :
      S)

Tactic:
simp [i]