-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem of_linearDisjoint_fg_right
    (H : ∀ N' : Submodule R S, N' ≤ N → N'.FG → M.LinearDisjoint N') :
    M.LinearDisjoint N := (linearDisjoint_iff _ _).2 fun x y hxy ↦ by
  obtain ⟨N', hN, hFG, h⟩ :=
    TensorProduct.exists_finite_submodule_right_of_finite' {x, y} (Set.toFinite _)
  rw [Module.Finite.iff_fg] at hFG
  obtain ⟨x', hx'⟩ := h (show x ∈ {x, y} by simp)
  obtain ⟨y', hy'⟩ := h (show y ∈ {x, y} by simp)
  rw [← hx', ← hy']; congr
  exact (H N' hN hFG).injective (by simp [← mulMap_comp_lTensor _ hN, hx', hy', hxy])

Proof state:
case intro.intro.intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))
⊢ x = y

Tactic:
obtain ⟨x', hx'⟩ := h (show x ∈ {x, y} by simp)

Result:
case intro.intro.intro.intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN)) x' = x
⊢ x = y

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
⊢ x = y

Tactic:
obtain ⟨N', hN, hFG, h⟩ :=
  TensorProduct.exists_finite_submodule_right_of_finite' {x, y} (Set.toFinite _)

Result:
case intro.intro.intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : Module.Finite R ↥N'
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))
⊢ x = y

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))
⊢ x ∈ {x, y}

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.h.e_6.h
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN)) x' = x
y' : ↥M ⊗[R] ↥N'
hy' : (LinearMap.lTensor (↥M) (inclusion hN)) y' = y
⊢ x' = y'

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

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN)) x' = x
y' : ↥M ⊗[R] ↥N'
hy' : (LinearMap.lTensor (↥M) (inclusion hN)) y' = y
⊢ (M.mulMap N') x' = (M.mulMap N') y'

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

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN)) x' = x
y' : ↥M ⊗[R] ↥N'
hy' : (LinearMap.lTensor (↥M) (inclusion hN)) y' = y
⊢ (LinearMap.lTensor (↥M) (inclusion hN)) x' = (LinearMap.lTensor (↥M) (inclusion hN)) y'

Tactic:
congr

Result:
case intro.intro.intro.intro.intro.h.e_6.h
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN)) x' = x
y' : ↥M ⊗[R] ↥N'
hy' : (LinearMap.lTensor (↥M) (inclusion hN)) y' = y
⊢ x' = y'

Proof state:
case intro.intro.intro.intro.intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN)) x' = x
y' : ↥M ⊗[R] ↥N'
hy' : (LinearMap.lTensor (↥M) (inclusion hN)) y' = y
⊢ x = y

Tactic:
rw [← hx', ← hy']

Result:
case intro.intro.intro.intro.intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN)) x' = x
y' : ↥M ⊗[R] ↥N'
hy' : (LinearMap.lTensor (↥M) (inclusion hN)) y' = y
⊢ (LinearMap.lTensor (↥M) (inclusion hN)) x' = (LinearMap.lTensor (↥M) (inclusion hN)) y'

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN)) x' = x
⊢ y ∈ {x, y}

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : Module.Finite R ↥N'
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))
⊢ x = y

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

Result:
case intro.intro.intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))
⊢ x = y