awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Eq (α :=
    (Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M) fun (i j : ι) (h : i ≤ j) ↦
        LinearMap.rTensor M (f i j h)) →ₗ[R]
      Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M) fun (i j : ι) (h : i ≤ j) ↦
        LinearMap.rTensor M (f i j h))
    (toDirectLimit (G := G) f M ∘ₗ fromDirectLimit (G := G) f M) LinearMap.id
have h : ∀ (i : ι) (x : G i) (x_1 : M),
  Eq (α :=
    Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M) fun (i j : ι) (h : i ≤ j) ↦
      LinearMap.rTensor M (f i j h))
    ((((LinearMap.compr₂ₛₗ (mk R (G i) M)
                  ((toDirectLimit (G := G) f M ∘ₗ fromDirectLimit (G := G) f M) ∘ₗ
                    of R ι (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M)
                      (fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h)) i) :
                (a : G i) →
                  M →ₗ[R]
                    Module.DirectLimit (fun (x : ι) ↦ G x ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦
                      LinearMap.rTensor M (f i j h))
              x :
            M →ₗ[R]
              Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M)
                fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h)) :
          (a : M) →
            Module.DirectLimit (fun (x : ι) ↦ G x ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h))
        x_1 :
      Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M) fun (i j : ι) (h : i ≤ j) ↦
        LinearMap.rTensor M (f i j h))
    ((((LinearMap.compr₂ₛₗ (σ₃₄ := RingHom.id R) (mk R (G i) M)
                  (LinearMap.id ∘ₗ
                    of R ι (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M)
                      (fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h)) i) :
                (a : G i) →
                  M →ₗ[R]
                    Module.DirectLimit (fun (x : ι) ↦ G x ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦
                      LinearMap.rTensor M (f i j h))
              x :
            M →ₗ[R]
              Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M)
                fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h)) :
          (a : M) →
            Module.DirectLimit (fun (x : ι) ↦ G x ⊗[R] M) fun (i j : ι) (h : i ≤ j) ↦ LinearMap.rTensor M (f i j h))
        x_1 :
      Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_3, u_4} R (G x) M) fun (i j : ι) (h : i ≤ j) ↦
        LinearMap.rTensor M (f i j h))
Tactic: ext
-- 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
⊢ Eq (α := Module.DirectLimit G f ⊗[R] M →ₗ[R] Module.DirectLimit G f ⊗[R] M)
    (fromDirectLimit (G := G) f M ∘ₗ toDirectLimit (G := G) f M) LinearMap.id
have H : ∀ (i : ι) (x : G i) (x_1 : M),
  Eq (α := Module.DirectLimit G f ⊗[R] M)
    ((((LinearMap.compr₂ₛₗ (mk R (Module.DirectLimit G f) M)
                    (fromDirectLimit (G := G) f M ∘ₗ toDirectLimit (G := G) f M) ∘ₗ
                  of R ι G f i :
                (a : G i) → M →ₗ[R] Module.DirectLimit G f ⊗[R] M)
              x :
            M →ₗ[R] Module.DirectLimit G f ⊗[R] M) :
          (a : M) → Module.DirectLimit G f ⊗[R] M)
        x_1 :
      Module.DirectLimit G f ⊗[R] M)
    ((((LinearMap.compr₂ₛₗ (mk R (Module.DirectLimit G f) M) LinearMap.id ∘ₗ of R ι G f i :
                (a : G i) → M →ₗ[R] Module.DirectLimit G f ⊗[R] M)
              x :
            M →ₗ[R] Module.DirectLimit G f ⊗[R] M) :
          (a : M) → Module.DirectLimit G f ⊗[R] M)
        x_1 :
      Module.DirectLimit G f ⊗[R] M)
Tactic: ext
-- 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
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
i : ι
x : TensorProduct.{u_1, u_3, u_4} R (G i) M
⊢ (LinearMap.rTensor M (f i i ⋯) : (a : G i ⊗[R] M) → G i ⊗[R] M) x = x
have h : f i i sorry = LinearMap.id
Tactic: convert! LinearMap.rTensor_id_apply M (G i) 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
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
i : ι
x : TensorProduct.{u_1, u_3, u_4} R (G i) M
⊢ f i i ⋯ = LinearMap.id
have h : ∀ (x : G i), Eq (α := G i) ((f i i sorry : (a : G i) → G i) x : G i) ((LinearMap.id : (a : G i) → G i) x : G i)
Tactic: ext
-- 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
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
x_1 x_2 x_3 : ι
h : x_3 ≤ x_2
h_1 : x_2 ≤ x_1
x : TensorProduct.{u_1, u_3, u_4} R (G x_3) M
⊢ Eq (α := TensorProduct.{u_1, u_3, u_4} R (G x_1) M)
    ((LinearMap.rTensor M (f x_2 x_1 h_1) : (a : G x_2 ⊗[R] M) → G x_1 ⊗[R] M)
        ((LinearMap.rTensor M (f x_3 x_2 h) : (a : G x_3 ⊗[R] M) → G x_2 ⊗[R] M) x) :
      TensorProduct.{u_1, u_3, u_4} R (G x_1) M)
    ((LinearMap.rTensor M (f x_3 x_1 ⋯) : (a : G x_3 ⊗[R] M) → G x_1 ⊗[R] M) x :
      TensorProduct.{u_1, u_3, u_4} R (G x_1) M)
have h : f x_2 x_1 h_1 ∘ₗ f x_3 x_2 h = f x_3 x_1 sorry
Tactic: convert! ← (LinearMap.rTensor_comp_apply M _ _ x).symm
-- 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
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
x_1 x_2 x_3 : ι
h : x_3 ≤ x_2
h_1 : x_2 ≤ x_1
x : TensorProduct.{u_1, u_3, u_4} R (G x_3) M
⊢ f x_2 x_1 h_1 ∘ₗ f x_3 x_2 h = f x_3 x_1 ⋯
have h : ∀ (x : G x_3),
  Eq (α := G x_1) ((f x_2 x_1 h_1 ∘ₗ f x_3 x_2 h : (a : G x_3) → G x_1) x : G x_1)
    ((f x_3 x_1 sorry : (a : G x_3) → G x_1) x : G x_1)
Tactic: ext
-- 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
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
i : ι
x : TensorProduct.{u_1, u_4, u_3} R M (G i)
⊢ (LinearMap.lTensor M (f i i ⋯) : (a : M ⊗[R] G i) → M ⊗[R] G i) x = x
have h : f i i sorry = LinearMap.id
Tactic: convert! LinearMap.lTensor_id_apply M _ 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
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
i : ι
x : TensorProduct.{u_1, u_4, u_3} R M (G i)
⊢ f i i ⋯ = LinearMap.id
have h : ∀ (x : G i), Eq (α := G i) ((f i i sorry : (a : G i) → G i) x : G i) ((LinearMap.id : (a : G i) → G i) x : G i)
Tactic: ext
-- 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
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
x_1 x_2 x_3 : ι
h₁ : x_3 ≤ x_2
h₂ : x_2 ≤ x_1
x : TensorProduct.{u_1, u_4, u_3} R M (G x_3)
⊢ Eq (α := TensorProduct.{u_1, u_4, u_3} R M (G x_1))
    ((LinearMap.lTensor M (f x_2 x_1 h₂) : (a : M ⊗[R] G x_2) → M ⊗[R] G x_1)
        ((LinearMap.lTensor M (f x_3 x_2 h₁) : (a : M ⊗[R] G x_3) → M ⊗[R] G x_2) x) :
      TensorProduct.{u_1, u_4, u_3} R M (G x_1))
    ((LinearMap.lTensor M (f x_3 x_1 ⋯) : (a : M ⊗[R] G x_3) → M ⊗[R] G x_1) x :
      TensorProduct.{u_1, u_4, u_3} R M (G x_1))
have h : f x_2 x_1 h₂ ∘ₗ f x_3 x_2 h₁ = f x_3 x_1 sorry
Tactic: convert! ← (LinearMap.lTensor_comp_apply M _ _ x).symm
-- 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
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
x_1 x_2 x_3 : ι
h₁ : x_3 ≤ x_2
h₂ : x_2 ≤ x_1
x : TensorProduct.{u_1, u_4, u_3} R M (G x_3)
⊢ f x_2 x_1 h₂ ∘ₗ f x_3 x_2 h₁ = f x_3 x_1 ⋯
have h : ∀ (x : G x_3),
  Eq (α := G x_1) ((f x_2 x_1 h₂ ∘ₗ f x_3 x_2 h₁ : (a : G x_3) → G x_1) x : G x_1)
    ((f x_3 x_1 sorry : (a : G x_3) → G x_1) x : G x_1)
Tactic: ext
-- 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 y : M ⊗[R] N
hx : ∃ (S : Multiset (M × N)), x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)
hy : ∃ (S : Multiset (M × N)), y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)
⊢ ∃ (S : Multiset (M × N)), x + y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)
have add : ∀ (Sx : Multiset (M × N)) (hx : x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx)),
  ∃ (S : Multiset (M × N)), x + y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)
Tactic: obtain ⟨Sx, hx⟩ := 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
x y : M ⊗[R] N
hy : ∃ (S : Multiset (M × N)), y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)
Sx : Multiset (M × N)
hx : x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx)
⊢ ∃ (S : Multiset (M × N)), x + y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)
have add : ∀ (Sy : Multiset (M × N)) (hy : y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy)),
  ∃ (S : Multiset (M × N)), x + y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)
Tactic: obtain ⟨Sy, hy⟩ := 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
x y : M ⊗[R] N
Sx : Multiset (M × N)
hx : x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx)
Sy : Multiset (M × N)
hy : y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy)
⊢ x + y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) (Sx + Sy))
have rw : x + y =
  (HAdd.hAdd (α := Multiset (M ⊗[R] N)) (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx)
      (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy)).sum
Tactic: rw [Multiset.map_add, Multiset.sum_add, 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
x y : M ⊗[R] N
Sx : Multiset (M × N)
hx : x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx)
Sy : Multiset (M × N)
hy : y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy)
rw :
  x + y =
    (HAdd.hAdd (α := Multiset (M ⊗[R] N)) (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx)
        (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy)).sum
⊢ x + y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) (Sx + Sy))
have rw₁ : x + y =
  HAdd.hAdd (α := M ⊗[R] N) (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx))
    (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy))
Tactic: rw [Multiset.map_add, Multiset.sum_add, 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
x y : M ⊗[R] N
Sx : Multiset (M × N)
hx : x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx)
Sy : Multiset (M × N)
hy : y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy)
rw :
  x + y =
    (HAdd.hAdd (α := Multiset (M ⊗[R] N)) (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx)
        (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy)).sum
rw₁ :
  x + y =
    HAdd.hAdd (α := M ⊗[R] N) (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx))
      (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy))
⊢ x + y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) (Sx + Sy))
have rw₂ : Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx) + y =
  HAdd.hAdd (α := M ⊗[R] N) (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx))
    (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy))
Tactic: rw [Multiset.map_add, Multiset.sum_add, 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
x y : M ⊗[R] N
Sx : Multiset (M × N)
hx : x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx)
Sy : Multiset (M × N)
hy : y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy)
rw :
  x + y =
    (HAdd.hAdd (α := Multiset (M ⊗[R] N)) (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx)
        (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy)).sum
rw₁ :
  x + y =
    HAdd.hAdd (α := M ⊗[R] N) (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx))
      (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy))
rw₂ :
  Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx) + y =
    HAdd.hAdd (α := M ⊗[R] N) (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx))
      (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy))
⊢ x + y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) (Sx + Sy))
have rw₃ : HAdd.hAdd (α := M ⊗[R] N) (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx))
    (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy)) =
  HAdd.hAdd (α := M ⊗[R] N) (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx))
    (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy))
Tactic: rw [Multiset.map_add, Multiset.sum_add, 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
x : M ⊗[R] N
⊢ ∃ (S : Multiset (M × N)), x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)
have zero : ∃ (S : Multiset (M × N)), Eq (α := M ⊗[R] N) 0 (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S))
Tactic: induction x with
  | zero => exact ⟨0, by simp⟩
  | tmul x y => exact ⟨{(x, y)}, by simp⟩
  | add x y hx hy =>
    obtain ⟨Sx, hx⟩ := hx
    obtain ⟨Sy, hy⟩ := hy
    exact ⟨Sx + Sy, by rw [Multiset.map_add, Multiset.sum_add, hx, hy]⟩
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
zero : ∃ (S : Multiset (M × N)), Eq (α := M ⊗[R] N) 0 (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S))
⊢ ∃ (S : Multiset (M × N)), x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)
have tmul : ∀ (x : M) (y : N),
  ∃ (S : Multiset (M × N)),
    Eq (α := M ⊗[R] N) (x ⊗ₜ[R] y) (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S))
Tactic: induction x with
  | zero => exact ⟨0, by simp⟩
  | tmul x y => exact ⟨{(x, y)}, by simp⟩
  | add x y hx hy =>
    obtain ⟨Sx, hx⟩ := hx
    obtain ⟨Sy, hy⟩ := hy
    exact ⟨Sx + Sy, by rw [Multiset.map_add, Multiset.sum_add, hx, hy]⟩
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
zero : ∃ (S : Multiset (M × N)), Eq (α := M ⊗[R] N) 0 (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S))
tmul :
  ∀ (x : M) (y : N),
    ∃ (S : Multiset (M × N)),
      Eq (α := M ⊗[R] N) (x ⊗ₜ[R] y) (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S))
⊢ ∃ (S : Multiset (M × N)), x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)
have add : ∀ (x y : M ⊗[R] N) (hx : ∃ (S : Multiset (M × N)), x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S))
  (hy : ∃ (S : Multiset (M × N)), y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)),
  ∃ (S : Multiset (M × N)), x + y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)
Tactic: induction x with
  | zero => exact ⟨0, by simp⟩
  | tmul x y => exact ⟨{(x, y)}, by simp⟩
  | add x y hx hy =>
    obtain ⟨Sx, hx⟩ := hx
    obtain ⟨Sy, hy⟩ := hy
    exact ⟨Sx + Sy, by rw [Multiset.map_add, Multiset.sum_add, hx, hy]⟩
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 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
have add : ∀ (Sx : M →₀ N) (hx : x = Sx.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 ⟨Sx, hx⟩ := 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
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
⊢ ∃ (S : M →₀ N), x + y = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
have 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
Tactic: obtain ⟨Sy, hy⟩ := 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
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
⊢ ∃ (S : M →₀ N), x + y = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
have h : x + y = (Sx + Sy).sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
Tactic: use Sx + Sy
-- 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 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
⊢ x + y = (Sx + Sy).sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
have 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
Tactic: rw [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
x : M ⊗[R] N
⊢ ∃ (S : M →₀ N), x = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
have zero : ∃ (S : M →₀ N), Eq (α := M ⊗[R] N) 0 (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
zero : ∃ (S : M →₀ N), Eq (α := M ⊗[R] N) 0 (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 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)
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