awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : TensorProduct.{u_1, u_3, u_2} R (↥J₁) M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : TensorProduct.{u_1, u_3, u_2} R (↥J₂) M
⊢ ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
    HAdd.hAdd (α := N ⊗[R] M) (β := N ⊗[R] M) ((rTensor M J₁.subtype : (a : ↥J₁ ⊗[R] M) → N ⊗[R] M) y₁ : N ⊗[R] M)
        ((rTensor M J₂.subtype : (a : ↥J₂ ⊗[R] M) → N ⊗[R] M) y₂ : N ⊗[R] M) =
      (rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y

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

Premises used: le_sup_left, le_sup_right, Submodule.inclusion, HAdd.hAdd, Max.max, Exists.intro, Submodule.FG.sup, DFunLike.coe, LinearMap.rTensor
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : TensorProduct.{u_1, u_3, u_2} R (↥J₁) M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : TensorProduct.{u_1, u_3, u_2} R (↥J₂) M
add :
  HAdd.hAdd (α := N ⊗[R] M) (β := N ⊗[R] M) ((rTensor M J₁.subtype : (a : ↥J₁ ⊗[R] M) → N ⊗[R] M) y₁ : N ⊗[R] M)
      ((rTensor M J₂.subtype : (a : ↥J₂ ⊗[R] M) → N ⊗[R] M) y₂ : N ⊗[R] M) =
    (rTensor M (J₁ ⊔ J₂).subtype : (a : ↥(J₁ ⊔ J₂) ⊗[R] M) → N ⊗[R] M)
      (HAdd.hAdd (α := TensorProduct.{u_1, u_3, u_2} R (↥(J₁ ⊔ J₂)) M) (β :=
        TensorProduct.{u_1, u_3, u_2} R (↥(J₁ ⊔ J₂)) M)
        ((rTensor M (inclusion ⋯) : (a : ↥J₁ ⊗[R] M) → ↥(J₁ ⊔ J₂) ⊗[R] M) y₁ :
          TensorProduct.{u_1, u_3, u_2} R (↥(J₁ ⊔ J₂)) M)
        ((rTensor M (inclusion ⋯) : (a : ↥J₂ ⊗[R] M) → ↥(J₁ ⊔ J₂) ⊗[R] M) y₂ :
          TensorProduct.{u_1, u_3, u_2} R (↥(J₁ ⊔ J₂)) M))
⊢ ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
    HAdd.hAdd (α := N ⊗[R] M) (β := N ⊗[R] M) ((rTensor M J₁.subtype : (a : ↥J₁ ⊗[R] M) → N ⊗[R] M) y₁ : N ⊗[R] M)
        ((rTensor M J₂.subtype : (a : ↥J₂ ⊗[R] M) → N ⊗[R] M) y₂ : N ⊗[R] M) =
      (rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y

Tactic:
refine ⟨J₁ ⊔ J₂, fg₁.sup fg₂,
      rTensor M (J₁.inclusion le_sup_left) y₁ + rTensor M (J₂.inclusion le_sup_right) y₂, ?_⟩
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : TensorProduct.{u_1, u_3, u_2} R (↥J₁) M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : TensorProduct.{u_1, u_3, u_2} R (↥J₂) M
add :
  HAdd.hAdd (α := N ⊗[R] M) (β := N ⊗[R] M) ((rTensor M J₁.subtype : (a : ↥J₁ ⊗[R] M) → N ⊗[R] M) y₁ : N ⊗[R] M)
      ((rTensor M J₂.subtype : (a : ↥J₂ ⊗[R] M) → N ⊗[R] M) y₂ : N ⊗[R] M) =
    HAdd.hAdd (α := N ⊗[R] M) (β := N ⊗[R] M)
      ((rTensor M ((J₁ ⊔ J₂).subtype ∘ₗ inclusion ⋯) : (a : ↥J₁ ⊗[R] M) → N ⊗[R] M) y₁ : N ⊗[R] M)
      ((rTensor M ((J₁ ⊔ J₂).subtype ∘ₗ inclusion ⋯) : (a : ↥J₂ ⊗[R] M) → N ⊗[R] M) y₂ : N ⊗[R] M)
⊢ HAdd.hAdd (α := N ⊗[R] M) (β := N ⊗[R] M) ((rTensor M J₁.subtype : (a : ↥J₁ ⊗[R] M) → N ⊗[R] M) y₁ : N ⊗[R] M)
      ((rTensor M J₂.subtype : (a : ↥J₂ ⊗[R] M) → N ⊗[R] M) y₂ : N ⊗[R] M) =
    (rTensor M (J₁ ⊔ J₂).subtype : (a : ↥(J₁ ⊔ J₂) ⊗[R] M) → N ⊗[R] M)
      (HAdd.hAdd (α := TensorProduct.{u_1, u_3, u_2} R (↥(J₁ ⊔ J₂)) M) (β :=
        TensorProduct.{u_1, u_3, u_2} R (↥(J₁ ⊔ J₂)) M)
        ((rTensor M (inclusion ⋯) : (a : ↥J₁ ⊗[R] M) → ↥(J₁ ⊔ J₂) ⊗[R] M) y₁ :
          TensorProduct.{u_1, u_3, u_2} R (↥(J₁ ⊔ J₂)) M)
        ((rTensor M (inclusion ⋯) : (a : ↥J₂ ⊗[R] M) → ↥(J₁ ⊔ J₂) ⊗[R] M) y₂ :
          TensorProduct.{u_1, u_3, u_2} R (↥(J₁ ⊔ J₂)) M))

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

Premises used: map_add, LinearMap.rTensor_comp_apply
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : TensorProduct.{u_1, u_3, u_2} R (↥J₁) M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : TensorProduct.{u_1, u_3, u_2} R (↥J₂) M
⊢ HAdd.hAdd (α := N ⊗[R] M) (β := N ⊗[R] M) ((rTensor M J₁.subtype : (a : ↥J₁ ⊗[R] M) → N ⊗[R] M) y₁ : N ⊗[R] M)
      ((rTensor M J₂.subtype : (a : ↥J₂ ⊗[R] M) → N ⊗[R] M) y₂ : N ⊗[R] M) =
    HAdd.hAdd (α := N ⊗[R] M) (β := N ⊗[R] M)
      ((rTensor M ((J₁ ⊔ J₂).subtype ∘ₗ inclusion ⋯) : (a : ↥J₁ ⊗[R] M) → N ⊗[R] M) y₁ : N ⊗[R] M)
      ((rTensor M ((J₁ ⊔ J₂).subtype ∘ₗ inclusion ⋯) : (a : ↥J₂ ⊗[R] M) → N ⊗[R] M) y₂ : N ⊗[R] M)

Tactic:
rfl
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x : N ⊗[R] M
zero :
  ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
    Eq (α := N ⊗[R] M) (0 : N ⊗[R] M) ((rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)
tmul :
  ∀ (i : N) (m : M),
    ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
      Eq (α := N ⊗[R] M) (i ⊗ₜ[R] m) ((rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y)
add :
  ∀ (x₁ x₂ : N ⊗[R] M)
    (ihx₁ :
      ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
        x₁ = (rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y)
    (ihx₂ :
      ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
        x₂ = (rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y),
    ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
      x₁ + x₂ = (rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) y
⊢ ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
    x = (rTensor M J.subtype : (a : ↥J ⊗[R] M) → N ⊗[R] M) 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

Premises used: map_add, LinearMap.rTensor_comp_apply, Submodule.zero, TensorProduct.tmul, Submodule.add, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (N ⊗[R] M)
hs : s.Finite
choose :
  ∀ (J : (x : N ⊗[R] M) → Submodule R N) (fg : ∀ (x : N ⊗[R] M), (J x).FG)
    (y : (x : N ⊗[R] M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M)
    (eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x)),
    ∃ (J : Submodule R N) (_ : J.FG), s ⊆ (↑(range (rTensor M J.subtype)) : Set (N ⊗[R] M))
⊢ ∃ (J : Submodule R N) (_ : J.FG), s ⊆ (↑(range (rTensor M J.subtype)) : Set (N ⊗[R] M))

Tactic:
choose J fg y eq using exists_fg_le_eq_rTensor_subtype (R := R) (M := M) (N := N)

Premises used: Submodule.exists_fg_le_eq_rTensor_subtype
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (N ⊗[R] M)
hs : s.Finite
J : (x : N ⊗[R] M) → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x)
rw :
  ∀ (hs : Finite (↑s : Type (max u_2 u_3))) (J : (x : N ⊗[R] M) → Submodule R N) (fg : ∀ (x : N ⊗[R] M), (J x).FG)
    (y : (x : N ⊗[R] M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M)
    (eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x)),
    ∃ (J : Submodule R N) (_ : J.FG), s ⊆ (↑(range (rTensor M J.subtype)) : Set (N ⊗[R] M))
⊢ ∃ (J : Submodule R N) (_ : J.FG), s ⊆ (↑(range (rTensor M J.subtype)) : Set (N ⊗[R] M))

Tactic:
rw [← Set.finite_coe_iff] at hs

Premises used: Set.finite_coe_iff
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (N ⊗[R] M)
hs : Finite (↑s : Type (max u_2 u_3))
J : (x : N ⊗[R] M) → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x)
⊢ ∃ (J : Submodule R N) (_ : J.FG), s ⊆ (↑(range (rTensor M J.subtype)) : Set (N ⊗[R] M))

Tactic:
⟨⨆ x : s, J x, fg_iSup _ fun _ ↦ fg _, fun x hx ↦
    ⟨rTensor M (inclusion <| le_iSup _ ⟨x, hx⟩) (y x), .trans ?_ (eq x).symm⟩⟩

Premises used: iSup, le_iSup, Submodule.fg_iSup, Submodule.inclusion, Exists.intro, Eq.symm, Subtype.val, DFunLike.coe, Eq.trans, LinearMap.rTensor
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (N ⊗[R] M)
hs : Finite (↑s : Type (max u_2 u_3))
J : (x : N ⊗[R] M) → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x)
refine :
  ∀ (x : N ⊗[R] M) (hx : x ∈ s),
    Eq (α := N ⊗[R] M)
      ((rTensor M (Submodule.subtype (⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M))) :
            (a : ↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M)) ⊗[R] M) → N ⊗[R] M)
          (((rTensor M (inclusion ⋯) :
                TensorProduct.{u_1, u_3, u_2} R (↥(J (↑(Subtype.mk (p := fun (x : N ⊗[R] M) ↦ x ∈ s) x hx) : N ⊗[R] M)))
                    M →ₗ[R]
                  TensorProduct.{u_1, u_3, u_2} R (↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M))) M) :
              (a : ↥(J (↑⟨x, hx⟩ : N ⊗[R] M)) ⊗[R] M) → ↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M)) ⊗[R] M)
            (y x)) :
        N ⊗[R] M)
      ((rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x) : N ⊗[R] M)
⊢ ∃ (J : Submodule R N) (_ : J.FG), s ⊆ (↑(range (rTensor M J.subtype)) : Set (N ⊗[R] M))

Tactic:
refine ⟨⨆ x : s, J x, fg_iSup _ fun _ ↦ fg _, fun x hx ↦
    ⟨rTensor M (inclusion <| le_iSup _ ⟨x, hx⟩) (y x), .trans ?_ (eq x).symm⟩⟩
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (N ⊗[R] M)
hs : Finite (↑s : Type (max u_2 u_3))
J : (x : N ⊗[R] M) → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x)
x : N ⊗[R] M
hx : x ∈ s
rw :
  Eq (α := N ⊗[R] M)
    (((rTensor M (Submodule.subtype (⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M)) ∘ₗ inclusion ⋯) :
            TensorProduct.{u_1, u_3, u_2} R (↥(J (↑(Subtype.mk (p := fun (x : N ⊗[R] M) ↦ x ∈ s) x hx) : N ⊗[R] M)))
                M →ₗ[R]
              N ⊗[R] M) :
          (a : ↥(J (↑⟨x, hx⟩ : N ⊗[R] M)) ⊗[R] M) → N ⊗[R] M)
        (y x) :
      N ⊗[R] M)
    ((rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x) : N ⊗[R] M)
⊢ Eq (α := N ⊗[R] M)
    ((rTensor M (Submodule.subtype (⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M))) :
          (a : ↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M)) ⊗[R] M) → N ⊗[R] M)
        (((rTensor M (inclusion ⋯) :
              TensorProduct.{u_1, u_3, u_2} R (↥(J (↑(Subtype.mk (p := fun (x : N ⊗[R] M) ↦ x ∈ s) x hx) : N ⊗[R] M)))
                  M →ₗ[R]
                TensorProduct.{u_1, u_3, u_2} R (↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M))) M) :
            (a : ↥(J (↑⟨x, hx⟩ : N ⊗[R] M)) ⊗[R] M) → ↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M)) ⊗[R] M)
          (y x)) :
      N ⊗[R] M)
    ((rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x) : N ⊗[R] M)

Tactic:
rw [← comp_apply, ← rTensor_comp]

Premises used: LinearMap.comp_apply, LinearMap.rTensor_comp
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (N ⊗[R] M)
hs : Finite (↑s : Type (max u_2 u_3))
J : (x : N ⊗[R] M) → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x)
x : N ⊗[R] M
hx : x ∈ s
⊢ Eq (α := N ⊗[R] M)
    (((rTensor M (Submodule.subtype (⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : N ⊗[R] M)) ∘ₗ inclusion ⋯) :
            TensorProduct.{u_1, u_3, u_2} R (↥(J (↑(Subtype.mk (p := fun (x : N ⊗[R] M) ↦ x ∈ s) x hx) : N ⊗[R] M)))
                M →ₗ[R]
              N ⊗[R] M) :
          (a : ↥(J (↑⟨x, hx⟩ : N ⊗[R] M)) ⊗[R] M) → N ⊗[R] M)
        (y x) :
      N ⊗[R] M)
    ((rTensor M (J x).subtype : (a : ↥(J x) ⊗[R] M) → N ⊗[R] M) (y x) : N ⊗[R] M)

Tactic:
rfl
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
I : Submodule R N
x : TensorProduct.{u_1, u_3, u_2} R (↥I) M
obtain :
  ∀ (J : Submodule R ↥I) (fg : J.FG) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
    ∃ (J_1 : Submodule R N) (_ : J_1.FG) (hle : J_1 ≤ I) (y_1 : TensorProduct.{u_1, u_3, u_2} R (↥J_1) M),
      Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥I) M)
        ((rTensor M J.subtype : (a : ↥J ⊗[R] M) → ↥I ⊗[R] M) y : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
        ((rTensor M (inclusion hle) : (a : ↥J_1 ⊗[R] M) → ↥I ⊗[R] M) y_1 : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
⊢ ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I) (y : TensorProduct.{u_1, u_3, u_2} R (↥J) M),
    x = (rTensor M (inclusion hle) : (a : ↥J ⊗[R] M) → ↥I ⊗[R] M) y

Tactic:
obtain ⟨J, fg, y, rfl⟩ := exists_fg_le_eq_rTensor_subtype x

Premises used: Submodule.exists_fg_le_eq_rTensor_subtype, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
I : Submodule R N
J : Submodule R ↥I
fg : J.FG
y : TensorProduct.{u_1, u_3, u_2} R (↥J) M
⊢ ∃ (J_1 : Submodule R N) (_ : J_1.FG) (hle : J_1 ≤ I) (y_1 : TensorProduct.{u_1, u_3, u_2} R (↥J_1) M),
    Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥I) M)
      ((rTensor M J.subtype : (a : ↥J ⊗[R] M) → ↥I ⊗[R] M) y : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
      ((rTensor M (inclusion hle) : (a : ↥J_1 ⊗[R] M) → ↥I ⊗[R] M) y_1 : TensorProduct.{u_1, u_3, u_2} R (↥I) M)

Tactic:
⟨J.map I.subtype, fg.map _, I.map_subtype_le J, rTensor M (I.subtype.submoduleMap J) y, ?_⟩

Premises used: Submodule.FG.map, LinearMap.submoduleMap, Exists.intro, Submodule.subtype, Submodule.map, DFunLike.coe, Submodule.map_subtype_le, LinearMap.rTensor
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
I : Submodule R N
J : Submodule R ↥I
fg : J.FG
y : TensorProduct.{u_1, u_3, u_2} R (↥J) M
refine :
  Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥I) M)
    ((rTensor M J.subtype : (a : ↥J ⊗[R] M) → ↥I ⊗[R] M) y : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
    ((rTensor M (inclusion ⋯) : (a : ↥(map I.subtype J) ⊗[R] M) → ↥I ⊗[R] M)
        ((rTensor M (I.subtype.submoduleMap J) : (a : ↥J ⊗[R] M) → ↥(map I.subtype J) ⊗[R] M) y) :
      TensorProduct.{u_1, u_3, u_2} R (↥I) M)
⊢ ∃ (J_1 : Submodule R N) (_ : J_1.FG) (hle : J_1 ≤ I) (y_1 : TensorProduct.{u_1, u_3, u_2} R (↥J_1) M),
    Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥I) M)
      ((rTensor M J.subtype : (a : ↥J ⊗[R] M) → ↥I ⊗[R] M) y : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
      ((rTensor M (inclusion hle) : (a : ↥J_1 ⊗[R] M) → ↥I ⊗[R] M) y_1 : TensorProduct.{u_1, u_3, u_2} R (↥I) M)

Tactic:
refine ⟨J.map I.subtype, fg.map _, I.map_subtype_le J, rTensor M (I.subtype.submoduleMap J) y, ?_⟩
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
I : Submodule R N
J : Submodule R ↥I
fg : J.FG
y : TensorProduct.{u_1, u_3, u_2} R (↥J) M
rw :
  Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥I) M)
    ((rTensor M J.subtype : (a : ↥J ⊗[R] M) → ↥I ⊗[R] M) y : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
    ((rTensor M (inclusion ⋯ ∘ₗ I.subtype.submoduleMap J) : (a : ↥J ⊗[R] M) → ↥I ⊗[R] M) y :
      TensorProduct.{u_1, u_3, u_2} R (↥I) M)
⊢ Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥I) M)
    ((rTensor M J.subtype : (a : ↥J ⊗[R] M) → ↥I ⊗[R] M) y : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
    ((rTensor M (inclusion ⋯) : (a : ↥(map I.subtype J) ⊗[R] M) → ↥I ⊗[R] M)
        ((rTensor M (I.subtype.submoduleMap J) : (a : ↥J ⊗[R] M) → ↥(map I.subtype J) ⊗[R] M) y) :
      TensorProduct.{u_1, u_3, u_2} R (↥I) M)

Tactic:
rw [← LinearMap.rTensor_comp_apply]

Premises used: LinearMap.rTensor_comp_apply
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
I : Submodule R N
J : Submodule R ↥I
fg : J.FG
y : TensorProduct.{u_1, u_3, u_2} R (↥J) M
⊢ Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥I) M)
    ((rTensor M J.subtype : (a : ↥J ⊗[R] M) → ↥I ⊗[R] M) y : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
    ((rTensor M (inclusion ⋯ ∘ₗ I.subtype.submoduleMap J) : (a : ↥J ⊗[R] M) → ↥I ⊗[R] M) y :
      TensorProduct.{u_1, u_3, u_2} R (↥I) M)

Tactic:
rfl
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
I : Submodule R N
s : Set (TensorProduct.{u_1, u_3, u_2} R (↥I) M)
hs : s.Finite
choose :
  ∀ (J : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → Submodule R N)
    (fg : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), (J x).FG)
    (hle : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), J x ≤ I)
    (y : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M)
    (eq :
      ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M),
        x = (rTensor M (inclusion ⋯) : (a : ↥(J x) ⊗[R] M) → ↥I ⊗[R] M) (y x)),
    ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I), s ⊆ (↑(range (rTensor M (inclusion hle))) : Set (↥I ⊗[R] M))
⊢ ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I), s ⊆ (↑(range (rTensor M (inclusion hle))) : Set (↥I ⊗[R] M))

Tactic:
choose J fg hle y eq using exists_fg_le_eq_rTensor_inclusion (M := M) (I := I)

Premises used: Submodule.exists_fg_le_eq_rTensor_inclusion
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
I : Submodule R N
s : Set (TensorProduct.{u_1, u_3, u_2} R (↥I) M)
hs : s.Finite
J : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → Submodule R N
fg : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), (J x).FG
hle : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), J x ≤ I
y : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M
eq :
  ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), x = (rTensor M (inclusion ⋯) : (a : ↥(J x) ⊗[R] M) → ↥I ⊗[R] M) (y x)
rw :
  ∀ (hs : Finite (↑s : Type (max u_2 u_3))) (J : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → Submodule R N)
    (fg : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), (J x).FG)
    (hle : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), J x ≤ I)
    (y : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M)
    (eq :
      ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M),
        x = (rTensor M (inclusion ⋯) : (a : ↥(J x) ⊗[R] M) → ↥I ⊗[R] M) (y x)),
    ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I), s ⊆ (↑(range (rTensor M (inclusion hle))) : Set (↥I ⊗[R] M))
⊢ ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I), s ⊆ (↑(range (rTensor M (inclusion hle))) : Set (↥I ⊗[R] M))

Tactic:
rw [← Set.finite_coe_iff] at hs

Premises used: Set.finite_coe_iff
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
I : Submodule R N
s : Set (TensorProduct.{u_1, u_3, u_2} R (↥I) M)
hs : Finite (↑s : Type (max u_2 u_3))
J : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → Submodule R N
fg : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), (J x).FG
hle : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), J x ≤ I
y : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M
eq :
  ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), x = (rTensor M (inclusion ⋯) : (a : ↥(J x) ⊗[R] M) → ↥I ⊗[R] M) (y x)
⊢ ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I), s ⊆ (↑(range (rTensor M (inclusion hle))) : Set (↥I ⊗[R] M))

Tactic:
⟨⨆ x : s, J x, fg_iSup _ fun _ ↦ fg _, iSup_le fun _ ↦ hle _, fun x hx ↦
    ⟨rTensor M (inclusion <| le_iSup _ ⟨x, hx⟩) (y x), .trans ?_ (eq x).symm⟩⟩

Premises used: iSup, le_iSup, Submodule.fg_iSup, Submodule.inclusion, Exists.intro, iSup_le, Eq.symm, Subtype.val, DFunLike.coe, Eq.trans, LinearMap.rTensor
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
I : Submodule R N
s : Set (TensorProduct.{u_1, u_3, u_2} R (↥I) M)
hs : Finite (↑s : Type (max u_2 u_3))
J : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → Submodule R N
fg : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), (J x).FG
hle : ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), J x ≤ I
y : (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) → TensorProduct.{u_1, u_3, u_2} R (↥(J x)) M
eq :
  ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M), x = (rTensor M (inclusion ⋯) : (a : ↥(J x) ⊗[R] M) → ↥I ⊗[R] M) (y x)
refine :
  ∀ (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) (hx : x ∈ s),
    Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥I) M)
      ((rTensor M (inclusion ⋯) : (a : ↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : ↥I ⊗[R] M)) ⊗[R] M) → ↥I ⊗[R] M)
          (((rTensor M (inclusion ⋯) :
                TensorProduct.{u_1, u_3, u_2} R
                    (↥(J
                        (↑(Subtype.mk (p := fun (x : TensorProduct.{u_1, u_3, u_2} R (↥I) M) ↦ x ∈ s) x hx) :
                          ↥I ⊗[R] M)))
                    M →ₗ[R]
                  TensorProduct.{u_1, u_3, u_2} R (↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : ↥I ⊗[R] M))) M) :
              (a : ↥(J (↑⟨x, hx⟩ : ↥I ⊗[R] M)) ⊗[R] M) →
                ↥(⨆ (x : (↑s : Type (max u_2 u_3))), J (↑x : ↥I ⊗[R] M)) ⊗[R] M)
            (y x)) :
        TensorProduct.{u_1, u_3, u_2} R (↥I) M)
      ((rTensor M (inclusion ⋯) : (a : ↥(J x) ⊗[R] M) → ↥I ⊗[R] M) (y x) : TensorProduct.{u_1, u_3, u_2} R (↥I) M)
⊢ ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I), s ⊆ (↑(range (rTensor M (inclusion hle))) : Set (↥I ⊗[R] M))

Tactic:
refine ⟨⨆ x : s, J x, fg_iSup _ fun _ ↦ fg _, iSup_le fun _ ↦ hle _, fun x hx ↦
    ⟨rTensor M (inclusion <| le_iSup _ ⟨x, hx⟩) (y x), .trans ?_ (eq x).symm⟩⟩