awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
t : ι → Type u_11
inst_3 : (i : ι) → AddCommMonoid (t i)
inst_4 : (i : ι) → Module.{u_4, u_11} R (t i)
f : (i : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
e : ι ≃ ι₂
m : (i : ι₂) → s ((e.symm : (a : ι₂) → ι) i)
⊢ Eq (α := ⨂[R] (i : ι), t i)
    (((map (s := s) (t := t) f ∘ₗ
                (↑(LinearEquiv.symm (reindex R s e)) :
                  (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] ⨂[R] (i : ι), s i)).compMultilinearMap
            (M₁ := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))
            (tprod R (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))) :
          (a : (i : ι₂) → s ((e.symm : (a : ι₂) → ι) i)) → ⨂[R] (i : ι), t i)
        m :
      ⨂[R] (i : ι), t i)
    ((LinearMap.compMultilinearMap (M₁ := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))
            ((↑(LinearEquiv.symm (reindex R t e)) :
                (⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] ⨂[R] (i : ι), t i) ∘ₗ
              map (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) (t := fun (i : ι₂) ↦
                t ((e.symm : (a : ι₂) → ι) i)) fun (i : ι₂) ↦ f ((e.symm : (a : ι₂) → ι) i))
            (tprod R (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))) :
          (a : (i : ι₂) → s ((e.symm : (a : ι₂) → ι) i)) → ⨂[R] (i : ι), t i)
        m :
      ⨂[R] (i : ι), t i)
have H : Eq (α := ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i))
  ((reindex R t e : (a : ⨂[R] (i : ι), t i) → ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i))
      (((map (s := s) (t := t) f ∘ₗ
                (↑(LinearEquiv.symm (reindex R s e)) :
                  (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] ⨂[R] (i : ι), s i)).compMultilinearMap
            (M₁ := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))
            (tprod R (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))) :
          (a : (i : ι₂) → s ((e.symm : (a : ι₂) → ι) i)) → ⨂[R] (i : ι), t i)
        m) :
    ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i))
  ((reindex R t e : (a : ⨂[R] (i : ι), t i) → ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i))
      ((LinearMap.compMultilinearMap (M₁ := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))
            ((↑(LinearEquiv.symm (reindex R t e)) :
                (⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] ⨂[R] (i : ι), t i) ∘ₗ
              map (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) (t := fun (i : ι₂) ↦
                t ((e.symm : (a : ι₂) → ι) i)) fun (i : ι₂) ↦ f ((e.symm : (a : ι₂) → ι) i))
            (tprod R (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))) :
          (a : (i : ι₂) → s ((e.symm : (a : ι₂) → ι) i)) → ⨂[R] (i : ι), t i)
        m) :
    ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i))
Tactic: apply LinearEquiv.injective (reindex R t e)
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : IsEmpty ι
x : ⨂[R] (i : ι), s i
⊢ (fun (r : R) ↦
        HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
          ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))))
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
            (⨂[R] (i : ι), s i) →ₗ[R] R) :
          (a : ⨂[R] (i : ι), s i) → R)
        x) =
    x
have refine_1 : ∀ (r : R) (f : (i : ι) → s i),
  (fun (r : R) ↦
        HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
          ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))))
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
            (⨂[R] (i : ι), s i) →ₗ[R] R) :
          (a : ⨂[R] (i : ι), s i) → R)
        (HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
          ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i))) =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i)
Tactic: refine x.induction_on ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : IsEmpty ι
x : ⨂[R] (i : ι), s i
refine_1 :
  ∀ (r : R) (f : (i : ι) → s i),
    (fun (r : R) ↦
          HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
            ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))))
        ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
              (⨂[R] (i : ι), s i) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), s i) → R)
          (HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
            ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i))) =
      HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i)
⊢ (fun (r : R) ↦
        HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
          ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))))
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
            (⨂[R] (i : ι), s i) →ₗ[R] R) :
          (a : ⨂[R] (i : ι), s i) → R)
        x) =
    x
have refine_2 : ∀ (x y : ⨂[R] (i : ι), s i),
  (fun (r : R) ↦
          HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
            ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))))
        ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
              (⨂[R] (i : ι), s i) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), s i) → R)
          x) =
      x →
    (fun (r : R) ↦
            HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
              ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))))
          ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
                (⨂[R] (i : ι), s i) →ₗ[R] R) :
              (a : ⨂[R] (i : ι), s i) → R)
            y) =
        y →
      (fun (r : R) ↦
            HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
              ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))))
          ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
                (⨂[R] (i : ι), s i) →ₗ[R] R) :
              (a : ⨂[R] (i : ι), s i) → R)
            (x + y)) =
        x + y
Tactic: refine x.induction_on ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : IsEmpty ι
x_1 : ⨂[R] (i : ι), s i
x : R
y : (i : ι) → s i
⊢ (fun (r : R) ↦
        HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
          ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))))
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
            (⨂[R] (i : ι), s i) →ₗ[R] R) :
          (a : ⨂[R] (i : ι), s i) → R)
        (HSMul.hSMul (β := ⨂[R] (i : ι), s i) x
          ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) y : ⨂[R] (i : ι), s i))) =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) x
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) y : ⨂[R] (i : ι), s i)
have refine_1 : HSMul.hSMul (β := ⨂[R] (i : ι), s i) x
    ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
  HSMul.hSMul (β := ⨂[R] (i : ι), s i) x
    ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) y : ⨂[R] (i : ι), s i)
Tactic: simp only [map_smulₛₗ, RingHom.id_apply, lift.tprod, constOfIsEmpty_apply, const_apply,
        smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : IsEmpty ι
x_1 : ⨂[R] (i : ι), s i
x : R
y : (i : ι) → s i
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) x
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) y : ⨂[R] (i : ι), s i)
have refine_1 : isEmptyElim (p := s) = y
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : IsEmpty ι
x_1 x y : ⨂[R] (i : ι), s i
hx :
  HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), s i)
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
              (⨂[R] (i : ι), s i) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), s i) → R)
          x :
        R)
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
    x
hy :
  HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), s i)
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
              (⨂[R] (i : ι), s i) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), s i) → R)
          y :
        R)
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
    y
⊢ HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), s i)
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
              (⨂[R] (i : ι), s i) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), s i) → R)
          (x + y) :
        R)
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
    x + y
have refine_2 : HSMul.hSMul (β := ⨂[R] (i : ι), s i)
    (HAdd.hAdd (α := R) (β := R)
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
              (⨂[R] (i : ι), s i) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), s i) → R)
          x :
        R)
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
              (⨂[R] (i : ι), s i) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), s i) → R)
          y :
        R))
    ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
  x + y
Tactic: rw [map_add, add_smul, hx, hy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : IsEmpty ι
x_1 x y : ⨂[R] (i : ι), s i
hx :
  HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), s i)
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
              (⨂[R] (i : ι), s i) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), s i) → R)
          x :
        R)
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
    x
hy :
  HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), s i)
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
              (⨂[R] (i : ι), s i) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), s i) → R)
          y :
        R)
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
    y
refine_2 :
  HSMul.hSMul (β := ⨂[R] (i : ι), s i)
      (HAdd.hAdd (α := R) (β := R)
        ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
                (⨂[R] (i : ι), s i) →ₗ[R] R) :
              (a : ⨂[R] (i : ι), s i) → R)
            x :
          R)
        ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
                (⨂[R] (i : ι), s i) →ₗ[R] R) :
              (a : ⨂[R] (i : ι), s i) → R)
            y :
          R))
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
    x + y
⊢ HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), s i)
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
              (⨂[R] (i : ι), s i) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), s i) → R)
          (x + y) :
        R)
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
    x + y
have refine_2₁ : HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), s i)
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
              (⨂[R] (i : ι), s i) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), s i) → R)
          x :
        R)
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) +
    HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), s i)
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
              (⨂[R] (i : ι), s i) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), s i) → R)
          y :
        R)
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
  x + y
Tactic: rw [map_add, add_smul, hx, hy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : Subsingleton ι
i₀ : ι
inst_11 : DecidableEq ι
m : (i : ι) → s i
i : ι
⊢ ∀ (x y : s i), update (β := s) m i (x + y) i₀ = update (β := s) m i x i₀ + update (β := s) m i y i₀
have rw : ∀ (x y : s i₀), update (β := s) m i₀ (x + y) i₀ = update (β := s) m i₀ x i₀ + update (β := s) m i₀ y i₀
Tactic: rw [Subsingleton.elim i i₀]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : Subsingleton ι
i₀ : ι
inst_11 : DecidableEq ι
m : (i : ι) → s i
i : ι
⊢ ∀ (c : R) (x : s i), update (β := s) m i (c • x) i₀ = c • update (β := s) m i x i₀
have rw : ∀ (c : R) (x : s i₀), update (β := s) m i₀ (c • x) i₀ = c • update (β := s) m i₀ x i₀
Tactic: rw [Subsingleton.elim i i₀]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : Subsingleton ι
i₀ : ι
⊢ Eq.{u_7 + 1} (α := s i₀ →ₗ[R] s i₀)
    ((lift (s := s) : (a : MultilinearMap R s (s i₀)) → (⨂[R] (i : ι), s i) →ₗ[R] s i₀)
        (MultilinearMap.mk (M₁ := s) (fun (f : (i : ι) → s i) ↦ f i₀) ⋯ ⋯) ∘ₗ
      { toFun := fun (x : s i₀) ↦ (tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (update (β := s) 0 i₀ x),
        map_add' := ⋯, map_smul' := ⋯ })
    LinearMap.id
have h : ∀ (x : s i₀),
  Eq (α := s i₀)
    (((lift (s := s) : (a : MultilinearMap R s (s i₀)) → (⨂[R] (i : ι), s i) →ₗ[R] s i₀)
              (MultilinearMap.mk (M₁ := s) (fun (f : (i : ι) → s i) ↦ f i₀) sorry sorry) ∘ₗ
            {
              toFun := fun (x : s i₀) ↦
                (tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (update (β := s) 0 i₀ x),
              map_add' := sorry, map_smul' := sorry } :
          (a : s i₀) → s i₀)
        x :
      s i₀)
    ((LinearMap.id : (a : s i₀) → s i₀) x : s i₀)
Tactic: ext _
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : Subsingleton ι
i₀ : ι
⊢ Eq (α := (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι), s i)
    ({ toFun := fun (x : s i₀) ↦ (tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (update (β := s) 0 i₀ x),
        map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
      (lift (s := s) : (a : MultilinearMap R s (s i₀)) → (⨂[R] (i : ι), s i) →ₗ[R] s i₀)
        (MultilinearMap.mk (M₁ := s) (fun (f : (i : ι) → s i) ↦ f i₀) ⋯ ⋯))
    LinearMap.id
have H : ∀ (f : (i : ι) → s i),
  Eq (α := ⨂[R] (i : ι), s i)
    ((LinearMap.compMultilinearMap (M₁ := s)
            ({
                toFun := fun (x : s i₀) ↦
                  (tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (update (β := s) 0 i₀ x),
                map_add' := sorry, map_smul' := sorry } ∘ₗ
              (lift (s := s) : (a : MultilinearMap R s (s i₀)) → (⨂[R] (i : ι), s i) →ₗ[R] s i₀)
                (MultilinearMap.mk (M₁ := s) (fun (f : (i : ι) → s i) ↦ f i₀) sorry sorry))
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι), s i)
        f :
      ⨂[R] (i : ι), s i)
    ((LinearMap.compMultilinearMap (M₁ := s) LinearMap.id (tprod R (s := s)) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i)
        f :
      ⨂[R] (i : ι), s i)
Tactic: ext f
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (hypothesis)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : Subsingleton ι
i₀ : ι
f : (i : ι) → s i
⊢ Eq (α := ⨂[R] (i : ι), s i)
    ((LinearMap.compMultilinearMap (M₁ := s)
            ({
                toFun := fun (x : s i₀) ↦
                  (tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (update (β := s) 0 i₀ x),
                map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
              (lift (s := s) : (a : MultilinearMap R s (s i₀)) → (⨂[R] (i : ι), s i) →ₗ[R] s i₀)
                (MultilinearMap.mk (M₁ := s) (fun (f : (i : ι) → s i) ↦ f i₀) ⋯ ⋯))
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι), s i)
        f :
      ⨂[R] (i : ι), s i)
    ((LinearMap.compMultilinearMap (M₁ := s) LinearMap.id (tprod R (s := s)) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i)
        f :
      ⨂[R] (i : ι), s i)
have h : update (β := s) 0 i₀ (f i₀) = f
Tactic: have h : update (0 : (i : ι) → s i) i₀ (f i₀) = f := update_eq_self i₀ f
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
N : ι ⊕ ι₂ → Type u_12
inst_10 : (i : ι ⊕ ι₂) → AddCommMonoid (N i)
inst_11 : (i : ι ⊕ ι₂) → Module.{u_4, u_12} R (N i)
x : (i : ι ⊕ ι₂) → N i
⊢ Eq (α := ⨂[R] (i : ι ⊕ ι₂), N i)
    (⨂ₜ[R] (t : ι ⊕ ι₂),
        Sum.rec (motive := fun (x : ι ⊕ ι₂) ↦ N x) (fun (i₁ : ι) ↦ x (Sum.inl i₁)) (fun (i₂ : ι₂) ↦ x (Sum.inr i₂)) t :
      ⨂[R] (i : ι ⊕ ι₂), N i)
    ((tprod R (s := N) : (a : (i : ι ⊕ ι₂) → N i) → ⨂[R] (i : ι ⊕ ι₂), N i) x : ⨂[R] (i : ι ⊕ ι₂), N i)
have H : (fun (t : ι ⊕ ι₂) ↦
    Sum.rec (motive := fun (x : ι ⊕ ι₂) ↦ N x) (fun (i₁ : ι) ↦ x (Sum.inl i₁)) (fun (i₂ : ι₂) ↦ x (Sum.inr i₂)) t) =
  x
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
N : ι ⊕ ι₂ → Type u_12
inst_10 : (i : ι ⊕ ι₂) → AddCommMonoid (N i)
inst_11 : (i : ι ⊕ ι₂) → Module.{u_4, u_12} R (N i)
x : (i : ι ⊕ ι₂) → N i
⊢ (fun (t : ι ⊕ ι₂) ↦
      Sum.rec (motive := fun (x : ι ⊕ ι₂) ↦ N x) (fun (i₁ : ι) ↦ x (Sum.inl i₁)) (fun (i₂ : ι₂) ↦ x (Sum.inr i₂)) t) =
    x
have H : ∀ (val : ι),
  Eq (α := N (Sum.inl val))
    (Sum.rec (motive := fun (x : ι ⊕ ι₂) ↦ N x) (fun (i₁ : ι) ↦ x (Sum.inl i₁)) (fun (i₂ : ι₂) ↦ x (Sum.inr i₂))
      (Sum.inl val))
    (x (Sum.inl val))
Tactic: ext (_ | _)