awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_8
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : Type u_22
inst_3 : DecidableEq ι
M : ι → Type u_23
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → Module.{u_1, u_23} R (M i)
i : ι
x : N
m : M i
j : ι
h : ¬i = j
⊢ Eq (α := TensorProduct.{u_1, u_8, u_23} R N (M j)) (x ⊗ₜ[R] Pi.single (M := M) i m j)
    (Pi.single (M := fun (i : ι) ↦ TensorProduct.{u_1, u_8, u_23} R N (M i)) i
      (x ⊗ₜ[R] m : TensorProduct.{u_1, u_8, u_23} R N (M i)) j)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_8
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : Type u_22
inst_3 : DecidableEq ι
M : ι → Type u_23
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → Module.{u_1, u_23} R (M i)
i : ι
x : N
m : M i
j : ι
pos :
  ∀ (h : i = j),
    Eq (α := TensorProduct.{u_1, u_23, u_8} R (M j) N) (Pi.single (M := M) i m j ⊗ₜ[R] x)
      (Pi.single (M := fun (i : ι) ↦ TensorProduct.{u_1, u_23, u_8} R (M i) N) i
        (m ⊗ₜ[R] x : TensorProduct.{u_1, u_23, u_8} R (M i) N) j)
neg :
  ∀ (h : ¬i = j),
    Eq (α := TensorProduct.{u_1, u_23, u_8} R (M j) N) (Pi.single (M := M) i m j ⊗ₜ[R] x)
      (Pi.single (M := fun (i : ι) ↦ TensorProduct.{u_1, u_23, u_8} R (M i) N) i
        (m ⊗ₜ[R] x : TensorProduct.{u_1, u_23, u_8} R (M i) N) j)
⊢ Eq (α := TensorProduct.{u_1, u_23, u_8} R (M j) N) (Pi.single (M := M) i m j ⊗ₜ[R] x)
    (Pi.single (M := fun (i : ι) ↦ TensorProduct.{u_1, u_23, u_8} R (M i) N) i
      (m ⊗ₜ[R] x : TensorProduct.{u_1, u_23, u_8} R (M i) N) j)

Tactic:
by_cases h : i = j
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_8
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : Type u_22
inst_3 : DecidableEq ι
M : ι → Type u_23
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → Module.{u_1, u_23} R (M i)
i : ι
x : N
m : M i
j : ι
h : i = j
⊢ Eq (α := TensorProduct.{u_1, u_23, u_8} R (M j) N) (Pi.single (M := M) i m j ⊗ₜ[R] x)
    (Pi.single (M := fun (i : ι) ↦ TensorProduct.{u_1, u_23, u_8} R (M i) N) i
      (m ⊗ₜ[R] x : TensorProduct.{u_1, u_23, u_8} R (M i) N) j)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_8
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : Type u_22
inst_3 : DecidableEq ι
M : ι → Type u_23
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → Module.{u_1, u_23} R (M i)
i : ι
x : N
m : M i
j : ι
h : ¬i = j
⊢ Eq (α := TensorProduct.{u_1, u_23, u_8} R (M j) N) (Pi.single (M := M) i m j ⊗ₜ[R] x)
    (Pi.single (M := fun (i : ι) ↦ TensorProduct.{u_1, u_23, u_8} R (M i) N) i
      (m ⊗ₜ[R] x : TensorProduct.{u_1, u_23, u_8} R (M i) N) j)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
α : Type u_22
m : α → M
n : N
⊢ Eq (α := M ⊗[R] N) ((∑ a ∈ ∅, m a) ⊗ₜ[R] n) (∑ a ∈ ∅, m a ⊗ₜ[R] n)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
α : Type u_22
m : α → M
n : N
a : α
s : Finset α
has : a ∉ s
ih : Eq (α := M ⊗[R] N) ((∑ a ∈ s, m a) ⊗ₜ[R] n) (∑ a ∈ s, m a ⊗ₜ[R] n)
⊢ Eq (α := M ⊗[R] N) ((∑ a ∈ insert a s, m a) ⊗ₜ[R] n) (∑ a ∈ insert a s, m a ⊗ₜ[R] n)

Tactic:
simp [Finset.sum_insert has, add_tmul, ih]

Premises used: TensorProduct.add_tmul, Finset.sum_insert
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
α : Type u_22
s : Finset α
m : α → M
n : N
empty : Eq (α := M ⊗[R] N) ((∑ a ∈ ∅, m a) ⊗ₜ[R] n) (∑ a ∈ ∅, m a ⊗ₜ[R] n)
insert :
  ∀ (a : α) (s : Finset α) (has : a ∉ s) (ih : Eq (α := M ⊗[R] N) ((∑ a ∈ s, m a) ⊗ₜ[R] n) (∑ a ∈ s, m a ⊗ₜ[R] n)),
    Eq (α := M ⊗[R] N) ((∑ a ∈ Insert.insert a s, m a) ⊗ₜ[R] n) (∑ a ∈ Insert.insert a s, m a ⊗ₜ[R] n)
⊢ Eq (α := M ⊗[R] N) ((∑ a ∈ s, m a) ⊗ₜ[R] n) (∑ a ∈ s, m a ⊗ₜ[R] n)

Tactic:
induction s using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, add_tmul, ih]

Premises used: Insert.insert, TensorProduct.add_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
α : Type u_22
s : Finset α
m : α → M
n : N
empty : Eq (α := M ⊗[R] N) ((∑ a ∈ ∅, m a) ⊗ₜ[R] n) (∑ a ∈ ∅, m a ⊗ₜ[R] n)
insert :
  ∀ (a : α) (s : Finset α) (has : a ∉ s) (ih : Eq (α := M ⊗[R] N) ((∑ a ∈ s, m a) ⊗ₜ[R] n) (∑ a ∈ s, m a ⊗ₜ[R] n)),
    Eq (α := M ⊗[R] N) ((∑ a ∈ Insert.insert a s, m a) ⊗ₜ[R] n) (∑ a ∈ Insert.insert a s, m a ⊗ₜ[R] n)
⊢ Eq (α := M ⊗[R] N) ((∑ a ∈ s, m a) ⊗ₜ[R] n) (∑ a ∈ s, m a ⊗ₜ[R] n)

Tactic:
classical
    induction s using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, add_tmul, ih]

Premises used: Insert.insert, TensorProduct.add_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : M
α : Type u_22
n : α → N
⊢ Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ∑ a ∈ ∅, n a) (∑ a ∈ ∅, m ⊗ₜ[R] n a)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : M
α : Type u_22
n : α → N
a : α
s : Finset α
has : a ∉ s
ih : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ∑ a ∈ s, n a) (∑ a ∈ s, m ⊗ₜ[R] n a)
⊢ Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ∑ a ∈ insert a s, n a) (∑ a ∈ insert a s, m ⊗ₜ[R] n a)

Tactic:
simp [Finset.sum_insert has, tmul_add, ih]

Premises used: TensorProduct.tmul_add, Finset.sum_insert
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : M
α : Type u_22
s : Finset α
n : α → N
empty : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ∑ a ∈ ∅, n a) (∑ a ∈ ∅, m ⊗ₜ[R] n a)
insert :
  ∀ (a : α) (s : Finset α) (has : a ∉ s) (ih : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ∑ a ∈ s, n a) (∑ a ∈ s, m ⊗ₜ[R] n a)),
    Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ∑ a ∈ Insert.insert a s, n a) (∑ a ∈ Insert.insert a s, m ⊗ₜ[R] n a)
⊢ Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ∑ a ∈ s, n a) (∑ a ∈ s, m ⊗ₜ[R] n a)

Tactic:
induction s using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, tmul_add, ih]

Premises used: Insert.insert, TensorProduct.tmul_add
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : M
α : Type u_22
s : Finset α
n : α → N
empty : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ∑ a ∈ ∅, n a) (∑ a ∈ ∅, m ⊗ₜ[R] n a)
insert :
  ∀ (a : α) (s : Finset α) (has : a ∉ s) (ih : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ∑ a ∈ s, n a) (∑ a ∈ s, m ⊗ₜ[R] n a)),
    Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ∑ a ∈ Insert.insert a s, n a) (∑ a ∈ Insert.insert a s, m ⊗ₜ[R] n a)
⊢ Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ∑ a ∈ s, n a) (∑ a ∈ s, m ⊗ₜ[R] n a)

Tactic:
classical
    induction s using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, tmul_add, ih]

Premises used: Insert.insert, TensorProduct.tmul_add
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
h :
  ∀ (t : M ⊗[R] N),
    Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t})
        t ↔
      Membership.mem (γ := Submodule R (M ⊗[R] N)) ⊤ t
⊢ Eq (α := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) ⊤

Tactic:
ext t
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
t : M ⊗[R] N
h : Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) t
⊢ Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) t ↔
    Membership.mem (γ := Submodule R (M ⊗[R] N)) ⊤ t

Tactic:
simp only [Submodule.mem_top, iff_true]

Premises used: iff_true, Submodule.mem_top
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
t : M ⊗[R] N
⊢ Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) t

Tactic:
t.induction_on ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
t : M ⊗[R] N
h : Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) 0
h₁ :
  ∀ (x : M) (y : N),
    Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t})
      (x ⊗ₜ[R] y)
h₂ :
  ∀ (x y : M ⊗[R] N),
    Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t})
        x →
      Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t})
          y →
        Membership.mem (γ := Submodule R (M ⊗[R] N))
          (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) (x + y)
⊢ Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) t

Tactic:
refine t.induction_on ?_ ?_ ?_
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
t : M ⊗[R] N
⊢ Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) 0

Tactic:
Submodule.zero_mem _

Premises used: Set.Mem, Submodule.zero_mem
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
t : M ⊗[R] N
⊢ Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) 0

Tactic:
exact Submodule.zero_mem _

Premises used: Submodule.zero_mem
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
t : M ⊗[R] N
m : M
n : N
h : Membership.mem (γ := Set (M ⊗[R] N)) {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t} (m ⊗ₜ[R] n)
⊢ Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t})
    (m ⊗ₜ[R] n)

Tactic:
apply Submodule.subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
t : M ⊗[R] N
m : M
n : N
w : M
w₁ : N
h : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] n) (m ⊗ₜ[R] n)
⊢ Membership.mem (γ := Set (M ⊗[R] N)) {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t} (m ⊗ₜ[R] n)

Tactic:
use m, n
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
t t₁ t₂ : M ⊗[R] N
ht₁ :
  Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) t₁
ht₂ :
  Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) t₂
⊢ Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t})
    (t₁ + t₂)

Tactic:
Submodule.add_mem _ ht₁ ht₂

Premises used: Set.Mem, Submodule.add_mem
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
t t₁ t₂ : M ⊗[R] N
ht₁ :
  Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) t₁
ht₂ :
  Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) t₂
⊢ Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t})
    (t₁ + t₂)

Tactic:
exact Submodule.add_mem _ ht₁ ht₂

Premises used: Submodule.add_mem
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
rw :
  LE.le (α := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t})
    (Submodule.span R
      (Set.image2
        (fun (m : M) (n : N) ↦ (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m : N →ₗ[R] M ⊗[R] N) : (a : N) → M ⊗[R] N) n)
        (↑⊤ : Set M) (↑⊤ : Set N)))
⊢ Eq (α := Submodule R (M ⊗[R] N)) (Submodule.map₂ (mk R M N) ⊤ ⊤) ⊤

Tactic:
rw [← top_le_iff, ← span_tmul_eq_top, Submodule.map₂_eq_span_image2]

Premises used: TensorProduct.span_tmul_eq_top, Submodule.map₂_eq_span_image2, top_le_iff
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
⊢ LE.le (α := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t})
    (Submodule.span R
      (Set.image2
        (fun (m : M) (n : N) ↦ (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m : N →ₗ[R] M ⊗[R] N) : (a : N) → M ⊗[R] N) n)
        (↑⊤ : Set M) (↑⊤ : Set N)))

Tactic:
Submodule.span_mono fun _ ⟨m, n, h⟩ => ⟨m, trivial, n, trivial, h⟩

Premises used: trivial, Membership.mem, SetLike.coe, Set.image2, And.intro, Submodule.span_mono, Exists.intro, Top.top, DFunLike.coe, _private.0.TensorProduct.map₂_mk_top_top_eq_top.match_1, TensorProduct.mk
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
⊢ LE.le (α := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t})
    (Submodule.span R
      (Set.image2
        (fun (m : M) (n : N) ↦ (((mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m : N →ₗ[R] M ⊗[R] N) : (a : N) → M ⊗[R] N) n)
        (↑⊤ : Set M) (↑⊤ : Set N)))

Tactic:
exact Submodule.span_mono fun _ ⟨m, n, h⟩ => ⟨m, trivial, n, trivial, h⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ (m : M) (n : N), HAdd.hAdd (α := M ⊗[R] N) (m₁ ⊗ₜ[R] n₁) (m₂ ⊗ₜ[R] n₂) = m ⊗ₜ[R] n
h₁ : Eq (α := M ⊗[R] N) 0 (0 ⊗ₜ[R] 0)
⊢ ∃ (m : M) (n : N), Eq (α := M ⊗[R] N) 0 (m ⊗ₜ[R] n)

Tactic:
use 0, 0
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ (m : M) (n : N), HAdd.hAdd (α := M ⊗[R] N) (m₁ ⊗ₜ[R] n₁) (m₂ ⊗ₜ[R] n₂) = m ⊗ₜ[R] n
h₁ h₂ : Eq (α := M ⊗[R] N) 0 0
⊢ Eq (α := M ⊗[R] N) 0 (0 ⊗ₜ[R] 0)

Tactic:
rw [TensorProduct.zero_tmul]

Premises used: TensorProduct.zero_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ (m : M) (n : N), HAdd.hAdd (α := M ⊗[R] N) (m₁ ⊗ₜ[R] n₁) (m₂ ⊗ₜ[R] n₂) = m ⊗ₜ[R] n
m : M
n : N
w : M
w₁ : N
h₁ : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] n) (m ⊗ₜ[R] n)
⊢ ∃ (m_1 : M) (n_1 : N), Eq (α := M ⊗[R] N) (m ⊗ₜ[R] n) (m_1 ⊗ₜ[R] n_1)

Tactic:
use m, n
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ (m : M) (n : N), HAdd.hAdd (α := M ⊗[R] N) (m₁ ⊗ₜ[R] n₁) (m₂ ⊗ₜ[R] n₂) = m ⊗ₜ[R] n
x y : M ⊗[R] N
h₁ : ∃ (m : M) (n : N), x = m ⊗ₜ[R] n
h₂ : ∃ (m : M) (n : N), y = m ⊗ₜ[R] n
add : ∀ (m₁ : M) (n₁ : N), ∃ (m : M) (n : N), m₁ ⊗ₜ[R] n₁ + y = m ⊗ₜ[R] n
⊢ ∃ (m : M) (n : N), x + y = m ⊗ₜ[R] n

Tactic:
obtain ⟨m₁, n₁, rfl⟩ := h₁

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ (m : M) (n : N), HAdd.hAdd (α := M ⊗[R] N) (m₁ ⊗ₜ[R] n₁) (m₂ ⊗ₜ[R] n₂) = m ⊗ₜ[R] n
y : M ⊗[R] N
h₂ : ∃ (m : M) (n : N), y = m ⊗ₜ[R] n
m₁ : M
n₁ : N
add : ∀ (m₂ : M) (n₂ : N), ∃ (m : M) (n : N), HAdd.hAdd (α := M ⊗[R] N) (m₁ ⊗ₜ[R] n₁) (m₂ ⊗ₜ[R] n₂) = m ⊗ₜ[R] n
⊢ ∃ (m : M) (n : N), m₁ ⊗ₜ[R] n₁ + y = m ⊗ₜ[R] n

Tactic:
obtain ⟨m₂, n₂, rfl⟩ := h₂

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ (m : M) (n : N), HAdd.hAdd (α := M ⊗[R] N) (m₁ ⊗ₜ[R] n₁) (m₂ ⊗ₜ[R] n₂) = m ⊗ₜ[R] n
m₁ : M
n₁ : N
m₂ : M
n₂ : N
⊢ ∃ (m : M) (n : N), HAdd.hAdd (α := M ⊗[R] N) (m₁ ⊗ₜ[R] n₁) (m₂ ⊗ₜ[R] n₂) = m ⊗ₜ[R] n

Tactic:
apply h
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x : M ⊗[R] N
h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ (m : M) (n : N), HAdd.hAdd (α := M ⊗[R] N) (m₁ ⊗ₜ[R] n₁) (m₂ ⊗ₜ[R] n₂) = m ⊗ₜ[R] n
zero : ∃ (m : M) (n : N), Eq (α := M ⊗[R] N) 0 (m ⊗ₜ[R] n)
tmul : ∀ (m : M) (n : N), ∃ (m_1 : M) (n_1 : N), Eq (α := M ⊗[R] N) (m ⊗ₜ[R] n) (m_1 ⊗ₜ[R] n_1)
add :
  ∀ (x y : M ⊗[R] N) (h₁ : ∃ (m : M) (n : N), x = m ⊗ₜ[R] n) (h₂ : ∃ (m : M) (n : N), y = m ⊗ₜ[R] n),
    ∃ (m : M) (n : N), x + y = m ⊗ₜ[R] n
⊢ ∃ (m : M) (n : N), x = m ⊗ₜ[R] n

Tactic:
induction x with
  | zero =>
    use 0, 0
    rw [TensorProduct.zero_tmul]
  | tmul m n => use m, n
  | add x y h₁ h₂ =>
    obtain ⟨m₁, n₁, rfl⟩ := h₁
    obtain ⟨m₂, n₂, rfl⟩ := h₂
    apply h

Premises used: TensorProduct.zero_tmul, TensorProduct.tmul, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
x_1 x_2 : ι
h : x_1 ≤ x_2
x : TensorProduct.{u_1, u_3, u_4} R (G x_1) M
⊢ Eq (α := Module.DirectLimit G f ⊗[R] M)
    (((fun (x : ι) ↦
              (LinearMap.rTensor M (of R ι G f x) :
                TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
            x_2 :
          (a : G x_2 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
        ((LinearMap.rTensor M (f x_1 x_2 h) : (a : G x_1 ⊗[R] M) → G x_2 ⊗[R] M) x) :
      Module.DirectLimit G f ⊗[R] M)
    (((fun (x : ι) ↦
              (LinearMap.rTensor M (of R ι G f x) :
                TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
            x_1 :
          (a : G x_1 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
        x :
      Module.DirectLimit G f ⊗[R] M)

Tactic:
x.induction_on ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
x_1 x_2 : ι
h : x_1 ≤ x_2
x : TensorProduct.{u_1, u_3, u_4} R (G x_1) M
⊢ Eq (α := Module.DirectLimit G f ⊗[R] M)
    (((fun (x : ι) ↦
            (LinearMap.rTensor M (of R ι G f x) :
              TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
          x_2 :
        (a : G x_2 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
      ((LinearMap.rTensor M (f x_1 x_2 h) : (a : G x_1 ⊗[R] M) → G x_2 ⊗[R] M) 0))
    (((fun (x : ι) ↦
            (LinearMap.rTensor M (of R ι G f x) :
              TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
          x_1 :
        (a : G x_1 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
      0)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
x_1 x_2 : ι
h : x_1 ≤ x_2
x : TensorProduct.{u_1, u_3, u_4} R (G x_1) M
⊢ ∀ (x : G x_1) (y : M),
    Eq (α := Module.DirectLimit G f ⊗[R] M)
      (((fun (x : ι) ↦
                (LinearMap.rTensor M (of R ι G f x) :
                  TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
              x_2 :
            (a : G x_2 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
          ((LinearMap.rTensor M (f x_1 x_2 h) : (a : G x_1 ⊗[R] M) → G x_2 ⊗[R] M) (x ⊗ₜ[R] y)) :
        Module.DirectLimit G f ⊗[R] M)
      (((fun (x : ι) ↦
                (LinearMap.rTensor M (of R ι G f x) :
                  TensorProduct.{u_1, u_3, u_4} R (G x) M →ₗ[R] Module.DirectLimit G f ⊗[R] M))
              x_1 :
            (a : G x_1 ⊗[R] M) → Module.DirectLimit G f ⊗[R] M)
          (x ⊗ₜ[R] y) :
        Module.DirectLimit G f ⊗[R] M)

Tactic:
aesop