-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem of_linearDisjoint_fg_left
    (H : ∀ M' : Submodule R S, M' ≤ M → M'.FG → M'.LinearDisjoint N) :
    M.LinearDisjoint N := (linearDisjoint_iff _ _).2 fun x y hxy ↦ by
  obtain ⟨M', hM, hFG, h⟩ :=
    TensorProduct.exists_finite_submodule_left_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 M' hM hFG).injective (by simp [← mulMap_comp_rTensor _ hM, 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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : Module.Finite R ↥M'
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))
⊢ 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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))
⊢ x = y

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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM)) x' = x
y' : ↥M' ⊗[R] ↥N
hy' : (LinearMap.rTensor (↥N) (inclusion hM)) y' = y
⊢ x' = y'

Tactic:
exact (H M' hM hFG).injective (by simp [← mulMap_comp_rTensor _ hM, 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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))
⊢ x ∈ {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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))
⊢ 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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM)) x' = x
⊢ 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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM)) x' = x
y' : ↥M' ⊗[R] ↥N
hy' : (LinearMap.rTensor (↥N) (inclusion hM)) 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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM)) x' = x
y' : ↥M' ⊗[R] ↥N
hy' : (LinearMap.rTensor (↥N) (inclusion hM)) y' = y
⊢ (LinearMap.rTensor (↥N) (inclusion hM)) x' = (LinearMap.rTensor (↥N) (inclusion hM)) 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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM)) x' = x
y' : ↥M' ⊗[R] ↥N
hy' : (LinearMap.rTensor (↥N) (inclusion hM)) y' = y
⊢ (LinearMap.rTensor (↥N) (inclusion hM)) x' = (LinearMap.rTensor (↥N) (inclusion hM)) 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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM)) x' = x
y' : ↥M' ⊗[R] ↥N
hy' : (LinearMap.rTensor (↥N) (inclusion hM)) y' = y
⊢ 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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM)) x' = x
⊢ y ∈ {x, y}

Tactic:
simp

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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
⊢ x = y

Tactic:
obtain ⟨M', hM, hFG, h⟩ :=
  TensorProduct.exists_finite_submodule_left_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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : Module.Finite R ↥M'
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))
⊢ 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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM)) x' = x
y' : ↥M' ⊗[R] ↥N
hy' : (LinearMap.rTensor (↥N) (inclusion hM)) y' = y
⊢ (M'.mulMap N) x' = (M'.mulMap N) y'

Tactic:
simp [← mulMap_comp_rTensor _ hM, hx', hy', hxy]

Result:
no goals