awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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_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)
⊢ 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)
have neg : ∀ (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: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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 : ι
⊢ 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)
have 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)
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ Eq (α := M ⊗[R] N) ((∑ a ∈ s, m a) ⊗ₜ[R] n) (∑ a ∈ s, m a ⊗ₜ[R] n)
have empty : Eq (α := M ⊗[R] N) ((∑ a ∈ ∅, m a) ⊗ₜ[R] n) (∑ a ∈ ∅, m a ⊗ₜ[R] n)
Tactic: induction s using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, add_tmul, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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)
⊢ Eq (α := M ⊗[R] N) ((∑ a ∈ s, m a) ⊗ₜ[R] n) (∑ a ∈ s, m a ⊗ₜ[R] n)
have 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 a s, m a) ⊗ₜ[R] n) (∑ a ∈ insert 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ Eq (α := M ⊗[R] N) ((∑ a ∈ s, m a) ⊗ₜ[R] n) (∑ a ∈ s, m a ⊗ₜ[R] n)
have empty : Eq (α := M ⊗[R] N) ((∑ a ∈ ∅, m a) ⊗ₜ[R] n) (∑ a ∈ ∅, 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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)
⊢ Eq (α := M ⊗[R] N) ((∑ a ∈ s, m a) ⊗ₜ[R] n) (∑ a ∈ s, m a ⊗ₜ[R] n)
have 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 a s, m a) ⊗ₜ[R] n) (∑ a ∈ insert 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ∑ a ∈ s, n a) (∑ a ∈ s, m ⊗ₜ[R] n a)
have empty : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ∑ a ∈ ∅, n a) (∑ a ∈ ∅, m ⊗ₜ[R] n a)
Tactic: induction s using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, tmul_add, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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)
⊢ Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ∑ a ∈ s, n a) (∑ a ∈ s, m ⊗ₜ[R] n a)
have 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 a s, n a) (∑ a ∈ insert 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ∑ a ∈ s, n a) (∑ a ∈ s, m ⊗ₜ[R] n a)
have empty : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ∑ a ∈ ∅, n a) (∑ a ∈ ∅, 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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)
⊢ Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ∑ a ∈ s, n a) (∑ a ∈ s, m ⊗ₜ[R] n a)
have 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 a s, n a) (∑ a ∈ insert 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ Eq (α := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) ⊤
have 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
Tactic: ext t
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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 ↔
    Membership.mem (γ := Submodule R (M ⊗[R] N)) ⊤ t
have h : Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) t
Tactic: simp only [Submodule.mem_top, iff_true]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
have h : Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) 0
Tactic: refine t.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) t
have 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)
Tactic: refine t.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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)
⊢ Membership.mem (γ := Submodule R (M ⊗[R] N)) (Submodule.span R {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}) t
have 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)
Tactic: refine t.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ 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)
have h : Membership.mem (γ := Set (M ⊗[R] N)) {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t} (m ⊗ₜ[R] n)
Tactic: apply Submodule.subset_span
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ Membership.mem (γ := Set (M ⊗[R] N)) {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t} (m ⊗ₜ[R] n)
have h : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] n) (m ⊗ₜ[R] n)
Tactic: use m, n
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ Eq (α := Submodule R (M ⊗[R] N)) (Submodule.map₂ (mk R M N) ⊤ ⊤) ⊤
have 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)))
Tactic: rw [← top_le_iff, ← span_tmul_eq_top, Submodule.map₂_eq_span_image2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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), Eq (α := M ⊗[R] N) 0 (m ⊗ₜ[R] n)
have h₁ : Eq (α := M ⊗[R] N) 0 (0 ⊗ₜ[R] 0)
Tactic: use 0, 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ Eq (α := M ⊗[R] N) 0 (0 ⊗ₜ[R] 0)
have h₁ : Eq (α := M ⊗[R] N) 0 0
Tactic: rw [TensorProduct.zero_tmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ ∃ (m_1 : M) (n_1 : N), Eq (α := M ⊗[R] N) (m ⊗ₜ[R] n) (m_1 ⊗ₜ[R] n_1)
have h₁ : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] n) (m ⊗ₜ[R] n)
Tactic: use m, n
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ ∃ (m : M) (n : N), x + y = m ⊗ₜ[R] n
have add : ∀ (m₁ : M) (n₁ : N), ∃ (m : M) (n : N), m₁ ⊗ₜ[R] n₁ + y = m ⊗ₜ[R] n
Tactic: obtain ⟨m₁, n₁, rfl⟩ := h₁
Cleared hypotheses: x, h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ ∃ (m : M) (n : N), m₁ ⊗ₜ[R] n₁ + y = m ⊗ₜ[R] n
have add : ∀ (m₂ : M) (n₂ : N), ∃ (m : M) (n : N), HAdd.hAdd (α := M ⊗[R] N) (m₁ ⊗ₜ[R] n₁) (m₂ ⊗ₜ[R] n₂) = m ⊗ₜ[R] n
Tactic: obtain ⟨m₂, n₂, rfl⟩ := h₂
Cleared hypotheses: y, h₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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
⊢ ∃ (m : M) (n : N), x = m ⊗ₜ[R] n
have zero : ∃ (m : M) (n : N), Eq (α := M ⊗[R] N) 0 (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
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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)
⊢ ∃ (m : M) (n : N), x = m ⊗ₜ[R] n
have tmul : ∀ (m : M) (n : N), ∃ (m_1 : M) (n_1 : N), Eq (α := M ⊗[R] N) (m ⊗ₜ[R] n) (m_1 ⊗ₜ[R] n_1)
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
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
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)
⊢ ∃ (m : M) (n : N), x = m ⊗ₜ[R] n
have 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
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
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.DirectLimit (goal)
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)
have refine_1 : 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: refine x.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.DirectLimit (goal)
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
refine_1 :
  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)
⊢ 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)
have refine_2 : ∀ (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: refine x.induction_on ?_ ?_ ?_