awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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)
⊢ ∃ (S : M →₀ N), x = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
have 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
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
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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), x = S.sum fun (n : N) (m : M) ↦ m ⊗ₜ[R] n
have 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
Tactic: obtain ⟨S, h⟩ := exists_finsupp_left (TensorProduct.comm R M N x)
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
have 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)
Tactic: refine ⟨S, (TensorProduct.comm R M N).injective ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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)
⊢ 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)
have 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))
Tactic: simp_rw [h, Finsupp.sum, map_sum, comm_tmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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))
⊢ 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)
have 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))
Tactic: simp_rw [h, Finsupp.sum, map_sum, comm_tmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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))
⊢ 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)
have 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))
Tactic: simp_rw [h, Finsupp.sum, map_sum, comm_tmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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 : Finset (M × N)), x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
have 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
Tactic: obtain ⟨S, h⟩ := exists_finsupp_left x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
⊢ ∃ (S : Finset (M × N)), x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
have h₁ : x = ∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2
Tactic: use S.graph
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
⊢ x = ∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2
have h₁ : Eq (α := M ⊗[R] N) (∑ a ∈ S.support, a ⊗ₜ[R] (S : (a : M) → N) a) (∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2)
Tactic: rw [h, Finsupp.sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
⊢ Eq (α := M ⊗[R] N) (∑ a ∈ S.support, a ⊗ₜ[R] (S : (a : M) → N) a) (∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2)
have h₁ : ∀ a ∈ S.support, Membership.mem (α := M × N) S.graph ((a, (S : (a : M) → N) a) : M × N)
Tactic: apply Finset.sum_nbij' (fun m ↦ ⟨m, S m⟩) Prod.fst
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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)
⊢ Eq (α := M ⊗[R] N) (∑ a ∈ S.support, a ⊗ₜ[R] (S : (a : M) → N) a) (∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2)
have h₂ : ∀ a ∈ S.graph, a.1 ∈ S.support
Tactic: apply Finset.sum_nbij' (fun m ↦ ⟨m, S m⟩) Prod.fst
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
⊢ Eq (α := M ⊗[R] N) (∑ a ∈ S.support, a ⊗ₜ[R] (S : (a : M) → N) a) (∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2)
have h₃ : ∀ a ∈ S.support, ((a, (S : (a : M) → N) a) : M × N).1 = a
Tactic: apply Finset.sum_nbij' (fun m ↦ ⟨m, S m⟩) Prod.fst
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
⊢ Eq (α := M ⊗[R] N) (∑ a ∈ S.support, a ⊗ₜ[R] (S : (a : M) → N) a) (∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2)
have h₄ : ∀ a ∈ S.graph, (a.1, (S : (a : M) → N) a.1) = a
Tactic: apply Finset.sum_nbij' (fun m ↦ ⟨m, S m⟩) Prod.fst
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
⊢ Eq (α := M ⊗[R] N) (∑ a ∈ S.support, a ⊗ₜ[R] (S : (a : M) → N) a) (∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2)
have 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)
Tactic: apply Finset.sum_nbij' (fun m ↦ ⟨m, S m⟩) Prod.fst
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
⊢ ∃ (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))
have simp_rw : ∃ (M' : Submodule R M) (N' : Submodule R N), M'.FG ∧ N'.FG ∧ s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
Tactic: simp_rw [Module.Finite.iff_fg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N), M'.FG ∧ N'.FG ∧ insert a s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
have 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 a s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
Tactic: obtain ⟨M', N', hM', hN', h⟩ := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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))
have insert : ∃ (M' : Submodule R M) (N' : Submodule R N), M'.FG ∧ N'.FG ∧ insert 0 s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
Tactic: refine TensorProduct.induction_on a ?_ (fun x y ↦ ?_) fun x y hx hy ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ Insert.insert a s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
have 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))
Tactic: refine TensorProduct.induction_on a ?_ (fun x y ↦ ?_) fun x y hx hy ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ Insert.insert a s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
have 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))
Tactic: refine TensorProduct.induction_on a ?_ (fun x y ↦ ?_) fun x y hx hy ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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))
have insert : x ⊗ₜ[R] y ∈ (↑(mapIncl (M' ⊔ R ∙ x) (N' ⊔ R ∙ y)).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 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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))
⊢ ∃ (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))
have insert₁ : ∀ (z : M ⊗[R] N) (hz : z ∈ s), z ∈ (↑(mapIncl (M' ⊔ R ∙ x) (N' ⊔ R ∙ y)).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 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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 x s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
hy : ∃ (M' : Submodule R M) (N' : Submodule R N), M'.FG ∧ N'.FG ∧ insert y s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ insert (x + y) s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
have insert : ∀ (M₁' : Submodule R M) (N₁' : Submodule R N) (hM₁' : M₁'.FG) (hN₁' : N₁'.FG)
  (h₁ : insert x s ⊆ (↑(mapIncl M₁' N₁').range : Set (M ⊗[R] N))),
  ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ insert (x + y) s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
Tactic: obtain ⟨M₁', N₁', hM₁', hN₁', h₁⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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 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 x s ⊆ (↑(mapIncl M₁' N₁').range : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ insert (x + y) s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
have insert : ∀ (M₂' : Submodule R M) (N₂' : Submodule R N) (hM₂' : M₂'.FG) (hN₂' : N₂'.FG)
  (h₂ : insert y s ⊆ (↑(mapIncl M₂' N₂').range : Set (M ⊗[R] N))),
  ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ insert (x + y) s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
Tactic: obtain ⟨M₂', N₂', hM₂', hN₂', h₂⟩ := hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : insert x 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 y s ⊆ (↑(mapIncl M₂' N₂').range : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ insert (x + y) s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
have insert : x ∈ (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range
Tactic: refine ⟨_, _, hM₁'.sup hM₂', hN₁'.sup hN₂', Set.insert_subset (add_mem ?_ ?_) fun z hz ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
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
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : Insert.insert y s ⊆ (↑(mapIncl M₂' N₂').range : Set (M ⊗[R] N))
insert : x ∈ (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range
⊢ ∃ (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))
have insert₁ : y ∈ (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range
Tactic: refine ⟨_, _, hM₁'.sup hM₂', hN₁'.sup hN₂', Set.insert_subset (add_mem ?_ ?_) fun z hz ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
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
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : Insert.insert y s ⊆ (↑(mapIncl M₂' N₂').range : Set (M ⊗[R] N))
insert : x ∈ (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range
insert₁ : y ∈ (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range
⊢ ∃ (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))
have insert₂ : ∀ (z : M ⊗[R] N) (hz : z ∈ s), z ∈ (↑(mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range : Set (M ⊗[R] N))
Tactic: refine ⟨_, _, hM₁'.sup hM₂', hN₁'.sup hN₂', Set.insert_subset (add_mem ?_ ?_) fun z hz ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N), M'.FG ∧ N'.FG ∧ s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
have empty : ∃ (M' : Submodule R M) (N' : Submodule R N), M'.FG ∧ N'.FG ∧ ∅ ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
Tactic: induction s, hs using Set.Finite.induction_on with
  | empty => exact ⟨_, _, fg_bot, fg_bot, Set.empty_subset _⟩
  | @insert a s _ _ ih =>
  obtain ⟨M', N', hM', hN', h⟩ := ih
  refine TensorProduct.induction_on a ?_ (fun x y ↦ ?_) fun x y hx hy ↦ ?_
  · exact ⟨M', N', hM', hN', Set.insert_subset (zero_mem _) h⟩
  · refine ⟨_, _, hM'.sup (fg_span_singleton x),
      hN'.sup (fg_span_singleton y), Set.insert_subset ?_ fun z hz ↦ ?_⟩
    · exact ⟨⟨x, mem_sup_right (mem_span_singleton_self x)⟩ ⊗ₜ
        ⟨y, mem_sup_right (mem_span_singleton_self y)⟩, rfl⟩
    · exact range_mapIncl_mono le_sup_left le_sup_left (h hz)
  · obtain ⟨M₁', N₁', hM₁', hN₁', h₁⟩ := hx
    obtain ⟨M₂', N₂', hM₂', hN₂', h₂⟩ := hy
    refine ⟨_, _, hM₁'.sup hM₂', hN₁'.sup hN₂', Set.insert_subset (add_mem ?_ ?_) fun z hz ↦ ?_⟩
    · exact range_mapIncl_mono le_sup_left le_sup_left (h₁ (Set.mem_insert x s))
    · exact range_mapIncl_mono le_sup_right le_sup_right (h₂ (Set.mem_insert y s))
    · exact range_mapIncl_mono le_sup_left le_sup_left (h₁ (Set.subset_insert x s hz))
Cleared hypotheses: hs