awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 y : M ⊗[R] N
hy : ∃ (S : M →₀ N), y = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
Sx : M →₀ N
hx : x = Sx.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
add :
  ∀ (Sy : M →₀ N) (hy : y = Sy.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n),
    ∃ (S : M →₀ N), x + y = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
⊢ ∃ (S : M →₀ N), x + y = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n

Tactic:
obtain ⟨Sy, hy⟩ := hy
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
h : x + y = (Sx + Sy).sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
⊢ ∃ (S : M →₀ N), x + y = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n

Tactic:
use Sx + Sy
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
h :
  HAdd.hAdd (α := M ⊗[R] N) (Sx.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n) (Sy.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n) =
    (Sx + Sy).sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
⊢ x + y = (Sx + Sy).sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n

Tactic:
rw [hx, hy]
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
⊢ ∀ (a : M), Eq (α := M ⊗[R] N) (a ⊗ₜ[R] 0) 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
⊢ HAdd.hAdd (α := M ⊗[R] N) (Sx.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n) (Sy.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n) =
    (Sx + Sy).sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n

Tactic:
exact (Finsupp.sum_add_index' (by simp) TensorProduct.tmul_add).symm

Premises used: Finsupp.sum_add_index', Eq.symm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 : M ⊗[R] N
zero : ∃ (S : M →₀ N), Eq (α := M ⊗[R] N) 0 (S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n)
tmul : ∀ (x : M) (y : N), ∃ (S : M →₀ N), Eq (α := M ⊗[R] N) (x ⊗ₜ[R] y) (S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n)
add :
  ∀ (x y : M ⊗[R] N) (hx : ∃ (S : M →₀ N), x = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n)
    (hy : ∃ (S : M →₀ N), y = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n),
    ∃ (S : M →₀ N), x + y = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
⊢ ∃ (S : M →₀ N), x = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n

Tactic:
induction x with
  | zero => exact ⟨0, by simp⟩
  | tmul x y => exact ⟨Finsupp.single x y, by simp⟩
  | add x y hx hy =>
    obtain ⟨Sx, hx⟩ := hx
    obtain ⟨Sy, hy⟩ := hy
    use Sx + Sy
    rw [hx, hy]
    exact (Finsupp.sum_add_index' (by simp) TensorProduct.tmul_add).symm

Premises used: Finsupp.sum_add_index', Submodule.zero, TensorProduct.tmul, Submodule.add, Eq.symm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 : M ⊗[R] N
obtain :
  ∀ (S : N →₀ M)
    (h :
      Eq (α := N ⊗[R] M) ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) x : N ⊗[R] M)
        (S.sum fun (m : N) (n : M) ↦ m ⊗ₜ[R] n : N ⊗[R] M)),
    ∃ (S : N →₀ M), x = S.sum fun (n : N) (m : M) ↦ m ⊗ₜ[R] n
⊢ ∃ (S : N →₀ M), x = S.sum fun (n : N) (m : M) ↦ m ⊗ₜ[R] n

Tactic:
obtain ⟨S, h⟩ := exists_finsupp_left (TensorProduct.comm R M N x)

Premises used: TensorProduct.comm, TensorProduct.exists_finsupp_left, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 : M ⊗[R] N
S : N →₀ M
h :
  Eq (α := N ⊗[R] M) ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) x : N ⊗[R] M)
    (S.sum fun (m : N) (n : M) ↦ m ⊗ₜ[R] n : N ⊗[R] M)
⊢ ∃ (S : N →₀ M), x = S.sum fun (n : N) (m : M) ↦ m ⊗ₜ[R] n

Tactic:
⟨S, (TensorProduct.comm R M N).injective ?_⟩

Premises used: TensorProduct.comm, Exists.intro, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 : M ⊗[R] N
S : N →₀ M
h :
  Eq (α := N ⊗[R] M) ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) x : N ⊗[R] M)
    (S.sum fun (m : N) (n : M) ↦ m ⊗ₜ[R] n : N ⊗[R] M)
refine :
  Eq (α := N ⊗[R] M) ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) x : N ⊗[R] M)
    ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) (S.sum fun (n : N) (m : M) ↦ m ⊗ₜ[R] n) : N ⊗[R] M)
⊢ ∃ (S : N →₀ M), x = S.sum fun (n : N) (m : M) ↦ m ⊗ₜ[R] n

Tactic:
refine ⟨S, (TensorProduct.comm R M N).injective ?_⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 : M ⊗[R] N
S : N →₀ M
h :
  Eq (α := N ⊗[R] M) ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) x : N ⊗[R] M)
    (S.sum fun (m : N) (n : M) ↦ m ⊗ₜ[R] n : N ⊗[R] M)
simp_rw :
  Eq (α := N ⊗[R] M) (S.sum fun (m : N) (n : M) ↦ m ⊗ₜ[R] n)
    ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) (S.sum fun (n : N) (m : M) ↦ m ⊗ₜ[R] n))
simp_rw₁ :
  Eq (α := N ⊗[R] M) (∑ x ∈ S.support, x ⊗ₜ[R] (S : (a : N) → M) x)
    ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) (∑ x ∈ S.support, (S : (a : N) → M) x ⊗ₜ[R] x))
simp_rw₂ :
  Eq (α := N ⊗[R] M) (∑ x ∈ S.support, x ⊗ₜ[R] (S : (a : N) → M) x)
    (∑ x ∈ S.support, (TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) ((S : (a : N) → M) x ⊗ₜ[R] x))
⊢ Eq (α := N ⊗[R] M) ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) x : N ⊗[R] M)
    ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) (S.sum fun (n : N) (m : M) ↦ m ⊗ₜ[R] n) : N ⊗[R] M)

Tactic:
simp_rw [h, Finsupp.sum, map_sum, comm_tmul]

Premises used: Finsupp.sum, map_sum, TensorProduct.comm_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 : M ⊗[R] N
obtain :
  ∀ (S : M →₀ N) (h : x = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n), ∃ (S : Finset (M × N)), x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ ∃ (S : Finset (M × N)), x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2

Tactic:
obtain ⟨S, h⟩ := exists_finsupp_left x

Premises used: TensorProduct.exists_finsupp_left
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
h₁ : x = ∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2
⊢ ∃ (S : Finset (M × N)), x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2

Tactic:
use S.graph

Premises used: Finsupp.graph
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
h₁ : Eq (α := M ⊗[R] N) (∑ a ∈ S.support, a ⊗ₜ[R] (S : (a : M) → N) a) (∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2)
⊢ x = ∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2

Tactic:
rw [h, Finsupp.sum]

Premises used: Finsupp.sum
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
h₁ : ∀ a ∈ S.support, Membership.mem (α := M × N) S.graph ((a, (S : (a : M) → N) a) : M × N)
h₂ : ∀ a ∈ S.graph, a.1 ∈ S.support
h₃ : ∀ a ∈ S.support, ((a, (S : (a : M) → N) a) : M × N).1 = a
h₄ : ∀ a ∈ S.graph, (a.1, (S : (a : M) → N) a.1) = a
h₅ :
  ∀ a ∈ S.support,
    Eq (α := M ⊗[R] N) (a ⊗ₜ[R] (S : (a : M) → N) a : M ⊗[R] N)
      (((a, (S : (a : M) → N) a) : M × N).1 ⊗ₜ[R] (a, (S : (a : M) → N) a).2 : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N) (∑ a ∈ S.support, a ⊗ₜ[R] (S : (a : M) → N) a) (∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2)

Tactic:
apply Finset.sum_nbij' (fun m ↦ ⟨m, S m⟩) Prod.fst

Premises used: Prod.fst, Finset.sum_nbij'
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.support, Membership.mem (α := M × N) S.graph ((a, (S : (a : M) → N) a) : M × N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.graph, a.1 ∈ S.support

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.support, ((a, (S : (a : M) → N) a) : M × N).1 = a

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.graph, (a.1, (S : (a : M) → N) a.1) = a

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.support,
    Eq (α := M ⊗[R] N) (a ⊗ₜ[R] (S : (a : M) → N) a : M ⊗[R] N)
      (((a, (S : (a : M) → N) a) : M × N).1 ⊗ₜ[R] (a, (S : (a : M) → N) a).2 : M ⊗[R] N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 (M ⊗[R] N)
hs : s.Finite
simp_rw : ∃ (M' : Submodule R M) (N' : Submodule R N), M'.FG ∧ N'.FG ∧ s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N),
    Module.Finite.{u_1, u_2} R ↥M' ∧ Module.Finite.{u_1, u_3} R ↥N' ∧ s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))

Tactic:
simp_rw [Module.Finite.iff_fg]

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 (M ⊗[R] N)
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N), M'.FG ∧ N'.FG ∧ ∅ ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))

Tactic:
⟨_, _, fg_bot, fg_bot, Set.empty_subset _⟩

Premises used: And.intro, Set.empty_subset, Exists.intro, Submodule.fg_bot
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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 (M ⊗[R] N)
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N), M'.FG ∧ N'.FG ∧ ∅ ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))

Tactic:
exact ⟨_, _, fg_bot, fg_bot, Set.empty_subset _⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h : a ∉ s
hs : s.Finite
ih : ∃ (M' : Submodule R M) (N' : Submodule R N), M'.FG ∧ N'.FG ∧ s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
insert :
  ∀ (M' : Submodule R M) (N' : Submodule R N) (hM' : M'.FG) (hN' : N'.FG)
    (h : s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))),
    ∃ (M' : Submodule R M) (N' : Submodule R N),
      M'.FG ∧ N'.FG ∧ Insert.insert a s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ Insert.insert a s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))

Tactic:
obtain ⟨M', N', hM', hN', h⟩ := ih
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : a ∉ s
hs : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N), M'.FG ∧ N'.FG ∧ insert a s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))

Tactic:
TensorProduct.induction_on a ?_ (fun x y ↦ ?_) fun x y hx hy ↦ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : a ∉ s
hs : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
insert :
  ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ Insert.insert 0 s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
insert₁ :
  ∀ (x : M) (y : N),
    ∃ (M' : Submodule R M) (N' : Submodule R N),
      M'.FG ∧ N'.FG ∧ Insert.insert (x ⊗ₜ[R] y) s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
insert₂ :
  ∀ (x y : M ⊗[R] N)
    (hx :
      ∃ (M' : Submodule R M) (N' : Submodule R N),
        M'.FG ∧ N'.FG ∧ Insert.insert x s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N)))
    (hy :
      ∃ (M' : Submodule R M) (N' : Submodule R N),
        M'.FG ∧ N'.FG ∧ Insert.insert y s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))),
    ∃ (M' : Submodule R M) (N' : Submodule R N),
      M'.FG ∧ N'.FG ∧ Insert.insert (x + y) s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ Insert.insert a s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))

Tactic:
refine TensorProduct.induction_on a ?_ (fun x y ↦ ?_) fun x y hx hy ↦ ?_
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : a ∉ s
hs : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N), M'.FG ∧ N'.FG ∧ insert 0 s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))

Tactic:
⟨M', N', hM', hN', Set.insert_subset (zero_mem _) h⟩

Premises used: And.intro, Exists.intro, ZeroMemClass.zero_mem, Set.insert_subset
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : a ∉ s
hs : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N), M'.FG ∧ N'.FG ∧ insert 0 s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))

Tactic:
exact ⟨M', N', hM', hN', Set.insert_subset (zero_mem _) h⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : a ∉ s
hs : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
x : M
y : N
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ insert (x ⊗ₜ[R] y) s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))

Tactic:
⟨_, _, hM'.sup (fg_span_singleton x),
      hN'.sup (fg_span_singleton y), Set.insert_subset ?_ fun z hz ↦ ?_⟩

Premises used: And.intro, Exists.intro, Submodule.fg_span_singleton, Submodule.FG.sup, Set.insert_subset
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : a ∉ s
hs : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
x : M
y : N
insert : x ⊗ₜ[R] y ∈ (↑(mapIncl (M' ⊔ R ∙ x) (N' ⊔ R ∙ y)).range : Set (M ⊗[R] N))
insert₁ : ∀ (z : M ⊗[R] N) (hz : z ∈ s), z ∈ (↑(mapIncl (M' ⊔ R ∙ x) (N' ⊔ R ∙ y)).range : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ Insert.insert (x ⊗ₜ[R] y) s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))

Tactic:
refine ⟨_, _, hM'.sup (fg_span_singleton x),
      hN'.sup (fg_span_singleton y), Set.insert_subset ?_ fun z hz ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : a ∉ s
hs : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
x : M
y : N
⊢ x ⊗ₜ[R] y ∈ (↑(mapIncl (M' ⊔ R ∙ x) (N' ⊔ R ∙ y)).range : Set (M ⊗[R] N))

Tactic:
⟨⟨x, mem_sup_right (mem_span_singleton_self x)⟩ ⊗ₜ
        ⟨y, mem_sup_right (mem_span_singleton_self y)⟩, rfl⟩

Premises used: Set.Mem, setOf, Submodule.mem_span_singleton_self, Subtype.mk, Exists.intro, TensorProduct.tmul, Set.range, Submodule.mem_sup_right, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : a ∉ s
hs : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
x : M
y : N
⊢ x ⊗ₜ[R] y ∈ (↑(mapIncl (M' ⊔ R ∙ x) (N' ⊔ R ∙ y)).range : Set (M ⊗[R] N))

Tactic:
exact ⟨⟨x, mem_sup_right (mem_span_singleton_self x)⟩ ⊗ₜ
        ⟨y, mem_sup_right (mem_span_singleton_self y)⟩, rfl⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : a ∉ s
hs : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
x : M
y : N
z : M ⊗[R] N
hz : z ∈ s
⊢ z ∈ (↑(mapIncl (M' ⊔ R ∙ x) (N' ⊔ R ∙ y)).range : Set (M ⊗[R] N))

Tactic:
range_mapIncl_mono le_sup_left le_sup_left (h hz)

Premises used: le_sup_left, Set.Mem, TensorProduct.range_mapIncl_mono
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : a ∉ s
hs : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
x : M
y : N
z : M ⊗[R] N
hz : z ∈ s
⊢ z ∈ (↑(mapIncl (M' ⊔ R ∙ x) (N' ⊔ R ∙ y)).range : Set (M ⊗[R] N))

Tactic:
exact range_mapIncl_mono le_sup_left le_sup_left (h hz)

Premises used: le_sup_left, TensorProduct.range_mapIncl_mono
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : a ∉ s
hs : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
x y : M ⊗[R] N
hx :
  ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ Insert.insert x s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
hy :
  ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ Insert.insert y s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
insert :
  ∀ (M₁' : Submodule R M) (N₁' : Submodule R N) (hM₁' : M₁'.FG) (hN₁' : N₁'.FG)
    (h₁ : Insert.insert x s ⊆ (↑(mapIncl M₁' N₁').range : Set (M ⊗[R] N))),
    ∃ (M' : Submodule R M) (N' : Submodule R N),
      M'.FG ∧ N'.FG ∧ Insert.insert (x + y) s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ Insert.insert (x + y) s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))

Tactic:
obtain ⟨M₁', N₁', hM₁', hN₁', h₁⟩ := hx
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
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_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : a ∉ s
hs : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
x y : M ⊗[R] N
hy :
  ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ Insert.insert y s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : Insert.insert x s ⊆ (↑(mapIncl M₁' N₁').range : Set (M ⊗[R] N))
insert :
  ∀ (M₂' : Submodule R M) (N₂' : Submodule R N) (hM₂' : M₂'.FG) (hN₂' : N₂'.FG)
    (h₂ : Insert.insert y s ⊆ (↑(mapIncl M₂' N₂').range : Set (M ⊗[R] N))),
    ∃ (M' : Submodule R M) (N' : Submodule R N),
      M'.FG ∧ N'.FG ∧ Insert.insert (x + y) s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ Insert.insert (x + y) s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))

Tactic:
obtain ⟨M₂', N₂', hM₂', hN₂', h₂⟩ := hy