awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : Dual R M
p : P
hl :
  ∀ (x : M),
    Eq.{u_5 + 1} (α := P)
      ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inl R M N :
            (a : M) → P × Q)
          x).1
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
              inl R M N :
            (a : M) → P × Q)
          x).1
hl₁ :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := Q)
      ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inl R M N :
            (a : M) → P × Q)
          x).2
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
              inl R M N :
            (a : M) → P × Q)
          x).2
⊢ Eq (α := M × N →ₗ[R] P × Q) (prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0)
    ((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
      ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p))
have hr : ∀ (x : N),
  Eq.{u_5 + 1} (α := P)
    ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inr R M N : (a : N) → P × Q)
        x).1
    (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
              ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
            inr R M N :
          (a : N) → P × Q)
        x).1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : Dual R M
p : P
hl :
  ∀ (x : M),
    Eq.{u_5 + 1} (α := P)
      ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inl R M N :
            (a : M) → P × Q)
          x).1
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
              inl R M N :
            (a : M) → P × Q)
          x).1
hl₁ :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := Q)
      ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inl R M N :
            (a : M) → P × Q)
          x).2
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
              inl R M N :
            (a : M) → P × Q)
          x).2
hr :
  ∀ (x : N),
    Eq.{u_5 + 1} (α := P)
      ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inr R M N :
            (a : N) → P × Q)
          x).1
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
              inr R M N :
            (a : N) → P × Q)
          x).1
⊢ Eq (α := M × N →ₗ[R] P × Q) (prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0)
    ((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
      ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p))
have hr₁ : ∀ (x : N),
  Eq.{u_6 + 1} (α := Q)
    ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inr R M N : (a : N) → P × Q)
        x).2
    (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
              ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
            inr R M N :
          (a : N) → P × Q)
        x).2
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
g : Dual R N
q : Q
⊢ Eq (α := M × N →ₗ[R] P × Q) (prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)))
    ((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
      ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q))
have hl : ∀ (x : M),
  Eq.{u_5 + 1} (α := P)
    ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inl R M N : (a : M) → P × Q)
        x).1
    (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
              ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
            inl R M N :
          (a : M) → P × Q)
        x).1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
g : Dual R N
q : Q
hl :
  ∀ (x : M),
    Eq.{u_5 + 1} (α := P)
      ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inl R M N :
            (a : M) → P × Q)
          x).1
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
              inl R M N :
            (a : M) → P × Q)
          x).1
⊢ Eq (α := M × N →ₗ[R] P × Q) (prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)))
    ((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
      ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q))
have hl₁ : ∀ (x : M),
  Eq.{u_6 + 1} (α := Q)
    ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inl R M N : (a : M) → P × Q)
        x).2
    (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
              ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
            inl R M N :
          (a : M) → P × Q)
        x).2
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
g : Dual R N
q : Q
hl :
  ∀ (x : M),
    Eq.{u_5 + 1} (α := P)
      ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inl R M N :
            (a : M) → P × Q)
          x).1
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
              inl R M N :
            (a : M) → P × Q)
          x).1
hl₁ :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := Q)
      ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inl R M N :
            (a : M) → P × Q)
          x).2
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
              inl R M N :
            (a : M) → P × Q)
          x).2
⊢ Eq (α := M × N →ₗ[R] P × Q) (prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)))
    ((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
      ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q))
have hr : ∀ (x : N),
  Eq.{u_5 + 1} (α := P)
    ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inr R M N : (a : N) → P × Q)
        x).1
    (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
              ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
            inr R M N :
          (a : N) → P × Q)
        x).1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
g : Dual R N
q : Q
hl :
  ∀ (x : M),
    Eq.{u_5 + 1} (α := P)
      ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inl R M N :
            (a : M) → P × Q)
          x).1
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
              inl R M N :
            (a : M) → P × Q)
          x).1
hl₁ :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := Q)
      ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inl R M N :
            (a : M) → P × Q)
          x).2
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
              inl R M N :
            (a : M) → P × Q)
          x).2
hr :
  ∀ (x : N),
    Eq.{u_5 + 1} (α := P)
      ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inr R M N :
            (a : N) → P × Q)
          x).1
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
              inr R M N :
            (a : N) → P × Q)
          x).1
⊢ Eq (α := M × N →ₗ[R] P × Q) (prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)))
    ((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
      ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q))
have hr₁ : ∀ (x : N),
  Eq.{u_6 + 1} (α := Q)
    ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inr R M N : (a : N) → P × Q)
        x).2
    (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
              ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
            inr R M N :
          (a : N) → P × Q)
        x).2
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : Dual R M
p : P
g : Dual R N
q : Q
⊢ Eq (α := M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    (TensorProduct.map ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p))
      ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)))
    ((dualTensorHom R (M ⊗[R] N) (P ⊗[R] Q) : (a : Dual R (M ⊗[R] N) ⊗[R] (P ⊗[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q)
      ((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N)) (f ⊗ₜ[R] g) ⊗ₜ[R] (p ⊗ₜ[R] q)))
have H : ∀ (m : M) (n : N),
  Eq (α := P ⊗[R] Q)
    ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R M N)
                  (TensorProduct.map ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p))
                    ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q))) :
                (a : M) → N →ₗ[R] P ⊗[R] Q)
              m :
            N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        n :
      P ⊗[R] Q)
    ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R M N)
                  ((dualTensorHom R (M ⊗[R] N) (P ⊗[R] Q) :
                      (a : Dual R (M ⊗[R] N) ⊗[R] (P ⊗[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q)
                    ((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N)) (f ⊗ₜ[R] g) ⊗ₜ[R]
                      (p ⊗ₜ[R] q))) :
                (a : M) → N →ₗ[R] P ⊗[R] Q)
              m :
            N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        n :
      P ⊗[R] Q)
Tactic: ext m n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : Dual R M
n : N
g : Dual R N
p : P
⊢ (dualTensorHom R N P : (a : Dual R N ⊗[R] P) → N →ₗ[R] P) (g ⊗ₜ[R] p) ∘ₗ
      (dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (f ⊗ₜ[R] n) =
    HSMul.hSMul (α := R) (β := M →ₗ[R] P) ((g : (a : N) → R) n : R)
      ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p) : M →ₗ[R] P)
have h : ∀ (m : M),
  Eq.{u_5 + 1} (α := P)
    (((dualTensorHom R N P : (a : Dual R N ⊗[R] P) → N →ₗ[R] P) (g ⊗ₜ[R] p) ∘ₗ
            (dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (f ⊗ₜ[R] n) :
          (a : M) → P)
        m :
      P)
    ((HSMul.hSMul (α := R) (β := M →ₗ[R] P) ((g : (a : N) → R) n : R)
            ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p) : M →ₗ[R] P) :
          (a : M) → P)
        m :
      P)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : Dual R M
n : N
g : Dual R N
p : P
m : M
⊢ Eq.{u_5 + 1} (α := P)
    (((dualTensorHom R N P : (a : Dual R N ⊗[R] P) → N →ₗ[R] P) (g ⊗ₜ[R] p) ∘ₗ
            (dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (f ⊗ₜ[R] n) :
          (a : M) → P)
        m :
      P)
    ((HSMul.hSMul (α := R) (β := M →ₗ[R] P) ((g : (a : N) → R) n : R)
            ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p) : M →ₗ[R] P) :
          (a : M) → P)
        m :
      P)
have h : HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((f : (a : M) → R) m : R)
    (HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((g : (a : N) → R) n : R) p) =
  HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((g : (a : N) → R) n : R)
    (HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((f : (a : M) → R) m : R) p)
Tactic: simp only [coe_comp, Function.comp_apply, dualTensorHom_apply, map_smul, LinearMap.smul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : Dual R M
n : N
g : Dual R N
p : P
m : M
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((f : (a : M) → R) m : R)
      (HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((g : (a : N) → R) n : R) p) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((g : (a : N) → R) n : R)
      (HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((f : (a : M) → R) m : R) p)
have h : HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((g : (a : N) → R) n : R)
    (HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((f : (a : M) → R) m : R) p) =
  HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((g : (a : N) → R) n : R)
    (HSMul.hSMul.{u_2, u_5, u_5} (α := R) ((f : (a : M) → R) m : R) p)
Tactic: rw [smul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : Type u_7
n : Type u_8
inst_5 : Fintype m
inst_6 : Finite n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i : n
⊢ Eq (α := Matrix n m R)
    ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
        ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) :
      Matrix n m R)
    (Matrix.single i j 1 : Matrix n m R)
have a : ∀ (i' : n) (j' : m),
  Eq.{u_2 + 1} (α := R)
    ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
        ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
      R)
    (Matrix.single i j 1 i' j' : R)
Tactic: ext i' j'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : Type u_7
n : Type u_8
inst_5 : Fintype m
inst_6 : Finite n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
⊢ Eq.{u_2 + 1} (α := R)
    ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
        ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
      R)
    (Matrix.single i j 1 i' j' : R)
have pos : ∀ (hij : i = i' ∧ j = j'),
  Eq.{u_2 + 1} (α := R)
    ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
        ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
      R)
    (Matrix.single i j 1 i' j' : R)
Tactic: by_cases hij : i = i' ∧ j = j'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : Type u_7
n : Type u_8
inst_5 : Fintype m
inst_6 : Finite n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
pos :
  ∀ (hij : i = i' ∧ j = j'),
    Eq.{u_2 + 1} (α := R)
      ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
          ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
        R)
      (Matrix.single i j 1 i' j' : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
        ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
      R)
    (Matrix.single i j 1 i' j' : R)
have neg : ∀ (hij : ¬(i = i' ∧ j = j')),
  Eq.{u_2 + 1} (α := R)
    ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
        ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
      R)
    (Matrix.single i j 1 i' j' : R)
Tactic: by_cases hij : i = i' ∧ j = j'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (hypothesis)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : Type u_7
n : Type u_8
inst_5 : Fintype m
inst_6 : Finite n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬(i = i' ∧ j = j')
⊢ Eq.{u_2 + 1} (α := R)
    ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
        ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
      R)
    (Matrix.single i j 1 i' j' : R)
have hij₁ : ¬i = i' ∨ ¬j = j'
Tactic: rw [and_iff_not_or_not, Classical.not_not] at hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : Type u_7
n : Type u_8
inst_5 : Fintype m
inst_6 : Finite n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬i = i' ∨ ¬j = j'
⊢ Eq.{u_2 + 1} (α := R)
    ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
        ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
      R)
    (Matrix.single i j 1 i' j' : R)
have neg : ∀ (hij : ¬i = i'),
  Eq.{u_2 + 1} (α := R)
    ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
        ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
      R)
    (Matrix.single i j 1 i' j' : R)
Tactic: rcases hij with hij | hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : Type u_7
n : Type u_8
inst_5 : Fintype m
inst_6 : Finite n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬i = i' ∨ ¬j = j'
neg :
  ∀ (hij : ¬i = i'),
    Eq.{u_2 + 1} (α := R)
      ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
          ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
        R)
      (Matrix.single i j 1 i' j' : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
        ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
      R)
    (Matrix.single i j 1 i' j' : R)
have neg₁ : ∀ (hij : ¬j = j'),
  Eq.{u_2 + 1} (α := R)
    ((toMatrix bM bN : (a : M →ₗ[R] N) → Matrix n m R)
        ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (bM.coord j ⊗ₜ[R] (bN : (a : n) → N) i)) i' j' :
      R)
    (Matrix.single i j 1 i' j' : R)
Tactic: rcases hij with hij | hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : DecidableEq ι
inst_10 : Fintype ι
b : Basis ι R M
⊢ Eq (α := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] N)
    (dualTensorHom R M N ∘ₗ
      ∑ i : ι,
        (TensorProduct.mk R (Dual R M) N : (a : Dual R M) → N →ₗ[R] Dual R M ⊗[R] N)
            ((b.dualBasis : (a : ι) → Dual R M) i) ∘ₗ
          (applyₗ : (a : M) → (M →ₗ[R] N) →ₗ[R] N) ((b : (a : ι) → M) i))
    LinearMap.id
have h : ∀ (f : M →ₗ[R] N) (m : M),
  Eq.{u_4 + 1} (α := N)
    ((((dualTensorHom R M N ∘ₗ
                  ∑ i : ι,
                    (TensorProduct.mk R (Dual R M) N : (a : Dual R M) → N →ₗ[R] Dual R M ⊗[R] N)
                        ((b.dualBasis : (a : ι) → Dual R M) i) ∘ₗ
                      (applyₗ : (a : M) → (M →ₗ[R] N) →ₗ[R] N) ((b : (a : ι) → M) i) :
                (a : M →ₗ[R] N) → M →ₗ[R] N)
              f :
            M →ₗ[R] N) :
          (a : M) → N)
        m :
      N)
    ((((LinearMap.id : (a : M →ₗ[R] N) → M →ₗ[R] N) f : M →ₗ[R] N) : (a : M) → N) m : N)
Tactic: ext f m