-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem span_tmul_eq_top : Submodule.span R { t : M ⊗[R] N | ∃ m n, m ⊗ₜ n = t } = ⊤

Proof state:
case h.refine_2.a
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
m : M
n : N
⊢ m ⊗ₜ[R] n ∈ {t | ∃ m n, m ⊗ₜ[R] n = t}

Tactic:
use m, n

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} = ⊤

Tactic:
ext t

Result:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
⊢ t ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} ↔ t ∈ ⊤

Proof state:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
⊢ t ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

Tactic:
refine t.induction_on ?_ ?_ ?_

Result:
case h.refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
⊢ 0 ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

case h.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
⊢ ∀ (x : M) (y : N), x ⊗ₜ[R] y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

case h.refine_3
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
⊢ ∀ (x y : M ⊗[R] N),
    x ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} →
      y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} → x + y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

Proof state:
case h.refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
⊢ 0 ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

Tactic:
exact Submodule.zero_mem _

Result:
no goals

Proof state:
case h.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
⊢ ∀ (x : M) (y : N), x ⊗ₜ[R] y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

Tactic:
intro m n

Result:
case h.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
m : M
n : N
⊢ m ⊗ₜ[R] n ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

Proof state:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
⊢ t ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} ↔ t ∈ ⊤

Tactic:
simp only [Submodule.mem_top, iff_true]

Result:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
⊢ t ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

Proof state:
case h.refine_3
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
⊢ ∀ (x y : M ⊗[R] N),
    x ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} →
      y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} → x + y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

Tactic:
intro t₁ t₂ ht₁ ht₂

Result:
case h.refine_3
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t t₁ t₂ : M ⊗[R] N
ht₁ : t₁ ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}
ht₂ : t₂ ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}
⊢ t₁ + t₂ ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

Proof state:
case h.refine_3
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t t₁ t₂ : M ⊗[R] N
ht₁ : t₁ ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}
ht₂ : t₂ ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}
⊢ t₁ + t₂ ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

Tactic:
exact Submodule.add_mem _ ht₁ ht₂

Result:
no goals

Proof state:
case h.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
m : M
n : N
⊢ m ⊗ₜ[R] n ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

Tactic:
apply Submodule.subset_span

Result:
case h.refine_2.a
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
m : M
n : N
⊢ m ⊗ₜ[R] n ∈ {t | ∃ m n, m ⊗ₜ[R] n = t}