-- Mathlib/RingTheory/Finiteness/TensorProduct.lean
theorem exists_fg_le_eq_rTensor_subtype (x : N ⊗ M) :
    ∃ (J : Submodule R N) (_ : J.FG) (y : J ⊗ M), x = rTensor M J.subtype y

Proof state:
case add.intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : ↥J₁ ⊗[R] M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : ↥J₂ ⊗[R] M
⊢ ∃ J, ∃ (_ : J.FG), ∃ y, (rTensor M J₁.subtype) y₁ + (rTensor M J₂.subtype) y₂ = (rTensor M J.subtype) y

Tactic:
refine ⟨J₁ ⊔ J₂, fg₁.sup fg₂,
  rTensor M (J₁.inclusion le_sup_left) y₁ + rTensor M (J₂.inclusion le_sup_right) y₂, ?_⟩

Result:
case add.intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : ↥J₁ ⊗[R] M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : ↥J₂ ⊗[R] M
⊢ (rTensor M J₁.subtype) y₁ + (rTensor M J₂.subtype) y₂ =
    (rTensor M (J₁ ⊔ J₂).subtype) ((rTensor M (inclusion ⋯)) y₁ + (rTensor M (inclusion ⋯)) y₂)

Proof state:
case tmul
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
i : N
m : M
⊢ ∃ J, ∃ (_ : J.FG), ∃ y, i ⊗ₜ[R] m = (rTensor M J.subtype) y

Tactic:
exact ⟨R ∙ i, fg_span_singleton i, ⟨i, mem_span_singleton_self _⟩ ⊗ₜ[R] m, rfl⟩

Result:
no goals

Proof state:
case add.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x₂ : N ⊗[R] M
ihx₂ : ∃ J, ∃ (_ : J.FG), ∃ y, x₂ = (rTensor M J.subtype) y
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : ↥J₁ ⊗[R] M
⊢ ∃ J, ∃ (_ : J.FG), ∃ y, (rTensor M J₁.subtype) y₁ + x₂ = (rTensor M J.subtype) y

Tactic:
obtain ⟨J₂, fg₂, y₂, rfl⟩ := ihx₂

Result:
case add.intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : ↥J₁ ⊗[R] M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : ↥J₂ ⊗[R] M
⊢ ∃ J, ∃ (_ : J.FG), ∃ y, (rTensor M J₁.subtype) y₁ + (rTensor M J₂.subtype) y₂ = (rTensor M J.subtype) y

Proof state:
case add.intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : ↥J₁ ⊗[R] M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : ↥J₂ ⊗[R] M
⊢ (rTensor M J₁.subtype) y₁ + (rTensor M J₂.subtype) y₂ =
    (rTensor M (J₁ ⊔ J₂).subtype) ((rTensor M (inclusion ⋯)) y₁ + (rTensor M (inclusion ⋯)) y₂)

Tactic:
rw [map_add, ← rTensor_comp_apply, ← rTensor_comp_apply]

Result:
case add.intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : ↥J₁ ⊗[R] M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : ↥J₂ ⊗[R] M
⊢ (rTensor M J₁.subtype) y₁ + (rTensor M J₂.subtype) y₂ =
    (rTensor M ((J₁ ⊔ J₂).subtype ∘ₗ inclusion ⋯)) y₁ + (rTensor M ((J₁ ⊔ J₂).subtype ∘ₗ inclusion ⋯)) y₂

Proof state:
case add.intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : ↥J₁ ⊗[R] M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : ↥J₂ ⊗[R] M
⊢ (rTensor M J₁.subtype) y₁ + (rTensor M J₂.subtype) y₂ =
    (rTensor M ((J₁ ⊔ J₂).subtype ∘ₗ inclusion ⋯)) y₁ + (rTensor M ((J₁ ⊔ J₂).subtype ∘ₗ inclusion ⋯)) y₂

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : N ⊗[R] M
⊢ ∃ J, ∃ (_ : J.FG), ∃ y, x = (rTensor M J.subtype) y

Tactic:
induction x with
| zero => exact ⟨⊥, fg_bot, 0, rfl⟩
| tmul i m => exact ⟨R ∙ i, fg_span_singleton i, ⟨i, mem_span_singleton_self _⟩ ⊗ₜ[R] m, rfl⟩
| add x₁ x₂ ihx₁ ihx₂ =>
  obtain ⟨J₁, fg₁, y₁, rfl⟩ := ihx₁
  obtain ⟨J₂, fg₂, y₂, rfl⟩ := ihx₂
  refine ⟨J₁ ⊔ J₂, fg₁.sup fg₂,
    rTensor M (J₁.inclusion le_sup_left) y₁ + rTensor M (J₂.inclusion le_sup_right) y₂, ?_⟩
  rw [map_add, ← rTensor_comp_apply, ← rTensor_comp_apply]
  rfl

Result:
no goals

Proof state:
case zero
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ ∃ J, ∃ (_ : J.FG), ∃ y, 0 = (rTensor M J.subtype) y

Tactic:
exact ⟨⊥, fg_bot, 0, rfl⟩

Result:
no goals

Proof state:
case add
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x₁ x₂ : N ⊗[R] M
ihx₁ : ∃ J, ∃ (_ : J.FG), ∃ y, x₁ = (rTensor M J.subtype) y
ihx₂ : ∃ J, ∃ (_ : J.FG), ∃ y, x₂ = (rTensor M J.subtype) y
⊢ ∃ J, ∃ (_ : J.FG), ∃ y, x₁ + x₂ = (rTensor M J.subtype) y

Tactic:
obtain ⟨J₁, fg₁, y₁, rfl⟩ := ihx₁

Result:
case add.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x₂ : N ⊗[R] M
ihx₂ : ∃ J, ∃ (_ : J.FG), ∃ y, x₂ = (rTensor M J.subtype) y
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : ↥J₁ ⊗[R] M
⊢ ∃ J, ∃ (_ : J.FG), ∃ y, (rTensor M J₁.subtype) y₁ + x₂ = (rTensor M J.subtype) y