awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (α := Dual R M ⊗[R] N →ₗ[R] Dual R M ⊗[R] 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)) ∘ₗ
      dualTensorHom R M N)
    LinearMap.id
have H : ∀ (f : Dual R M) (m : N),
  Eq (α := Dual R M ⊗[R] N)
    ((((compr₂ₛₗ (TensorProduct.mk R (Dual 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)) ∘ₗ
                    dualTensorHom R M N) :
                (a : Dual R M) → N →ₗ[R] Dual R M ⊗[R] N)
              f :
            N →ₗ[R] Dual R M ⊗[R] N) :
          (a : N) → Dual R M ⊗[R] N)
        m :
      Dual R M ⊗[R] N)
    ((((compr₂ₛₗ (TensorProduct.mk R (Dual R M) N) LinearMap.id : (a : Dual R M) → N →ₗ[R] Dual R M ⊗[R] N) f :
            N →ₗ[R] Dual R M ⊗[R] N) :
          (a : N) → Dual R M ⊗[R] N)
        m :
      Dual R M ⊗[R] N)
Tactic: ext f m
-- 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
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
x : Dual R M ⊗[R] N
⊢ Eq (α := M →ₗ[R] N) ((dualTensorHomEquivOfBasis b : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) x : M →ₗ[R] N)
    ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) x : M →ₗ[R] N)
have h : ∀ (x_1 : M),
  Eq.{u_4 + 1} (α := N)
    ((((dualTensorHomEquivOfBasis b : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x_1 : N)
    ((((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x_1 : N)
Tactic: ext
-- 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
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
x : Dual R M ⊗[R] N
⊢ (LinearEquiv.symm (dualTensorHomEquivOfBasis b) : (a : M →ₗ[R] N) → Dual R M ⊗[R] N)
      ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) x) =
    x
have rw : (LinearEquiv.symm (dualTensorHomEquivOfBasis b) : (a : M →ₗ[R] N) → Dual R M ⊗[R] N)
    ((dualTensorHomEquivOfBasis b : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) x) =
  x
Tactic: rw [← dualTensorHomEquivOfBasis_apply b,
    LinearEquiv.symm_apply_apply <| dualTensorHomEquivOfBasis (N := N) b]
-- 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
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
x : Dual R M ⊗[R] N
rw :
  (LinearEquiv.symm (dualTensorHomEquivOfBasis b) : (a : M →ₗ[R] N) → Dual R M ⊗[R] N)
      ((dualTensorHomEquivOfBasis b : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) x) =
    x
⊢ (LinearEquiv.symm (dualTensorHomEquivOfBasis b) : (a : M →ₗ[R] N) → Dual R M ⊗[R] N)
      ((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) x) =
    x
have rw₁ : x = x
Tactic: rw [← dualTensorHomEquivOfBasis_apply b,
    LinearEquiv.symm_apply_apply <| dualTensorHomEquivOfBasis (N := N) b]
-- 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
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
x : M →ₗ[R] N
⊢ (dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N)
      ((LinearEquiv.symm (dualTensorHomEquivOfBasis b) : (a : M →ₗ[R] N) → Dual R M ⊗[R] N) x) =
    x
have rw : (dualTensorHomEquivOfBasis b : (a : Dual R M ⊗[R] N) → M →ₗ[R] N)
    ((LinearEquiv.symm (dualTensorHomEquivOfBasis b) : (a : M →ₗ[R] N) → Dual R M ⊗[R] N) x) =
  x
Tactic: rw [← dualTensorHomEquivOfBasis_apply b, LinearEquiv.apply_symm_apply]
-- 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
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
x : M →ₗ[R] N
rw :
  (dualTensorHomEquivOfBasis b : (a : Dual R M ⊗[R] N) → M →ₗ[R] N)
      ((LinearEquiv.symm (dualTensorHomEquivOfBasis b) : (a : M →ₗ[R] N) → Dual R M ⊗[R] N) x) =
    x
⊢ (dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N)
      ((LinearEquiv.symm (dualTensorHomEquivOfBasis b) : (a : M →ₗ[R] N) → Dual R M ⊗[R] N) x) =
    x
have rw₁ : x = x
Tactic: rw [← dualTensorHomEquivOfBasis_apply b, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (hypothesis)
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
e : P ⊗[R] (Dual R M ⊗[R] Q) ≃ₗ[R] P ⊗[R] (M →ₗ[R] Q) :=
  TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
⊢ Eq (α := P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q)
    (↑(lTensorHomEquivHomLTensor R M P Q) : P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q)
    (lTensorHomToHomLTensor (RingHom.id R) M P Q)
have h : Function.Surjective (α := P ⊗[R] (Dual R M ⊗[R] Q)) (β := P ⊗[R] (M →ₗ[R] Q))
  (⇑(↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q)) : (a : P ⊗[R] (Dual R M ⊗[R] Q)) → P ⊗[R] (M →ₗ[R] Q))
Tactic: have h : Function.Surjective e.toLinearMap := e.surjective
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
e : P ⊗[R] (Dual R M ⊗[R] Q) ≃ₗ[R] P ⊗[R] (M →ₗ[R] Q) :=
  TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
h :
  Function.Surjective (α := P ⊗[R] (Dual R M ⊗[R] Q)) (β := P ⊗[R] (M →ₗ[R] Q))
    (⇑(↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q)) : (a : P ⊗[R] (Dual R M ⊗[R] Q)) → P ⊗[R] (M →ₗ[R] Q))
⊢ Eq (α := P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q)
    (↑(lTensorHomEquivHomLTensor R M P Q) : P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q)
    (lTensorHomToHomLTensor (RingHom.id R) M P Q)
have refine : (↑(lTensorHomEquivHomLTensor R M P Q) : P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q) ∘ₗ
    (↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q)) =
  lTensorHomToHomLTensor (RingHom.id R) M P Q ∘ₗ (↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q))
Tactic: refine (cancel_right h).1 ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
e : P ⊗[R] (Dual R M ⊗[R] Q) ≃ₗ[R] P ⊗[R] (M →ₗ[R] Q) :=
  TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
h :
  Function.Surjective (α := P ⊗[R] (Dual R M ⊗[R] Q)) (β := P ⊗[R] (M →ₗ[R] Q))
    (⇑(↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q)) : (a : P ⊗[R] (Dual R M ⊗[R] Q)) → P ⊗[R] (M →ₗ[R] Q))
⊢ (↑(lTensorHomEquivHomLTensor R M P Q) : P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q) ∘ₗ
      (↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q)) =
    lTensorHomToHomLTensor (RingHom.id R) M P Q ∘ₗ (↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q))
have H : ∀ (f : P) (q : Dual R M) (m : Q) (x : M),
  Eq (α := P ⊗[R] Q)
    ((((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R (Dual R M) Q)
                        ((compr₂ₛₗ (TensorProduct.mk R P (Dual R M ⊗[R] Q))
                              ((↑(lTensorHomEquivHomLTensor R M P Q) : P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q) ∘ₗ
                                (↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q))) :
                            (a : P) → Dual R M ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                          f) :
                      (a : Dual R M) → Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                    q :
                  Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                (a : Q) → M →ₗ[R] P ⊗[R] Q)
              m :
            M →ₗ[R] P ⊗[R] Q) :
          (a : M) → P ⊗[R] Q)
        x :
      P ⊗[R] Q)
    ((((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R (Dual R M) Q)
                        ((compr₂ₛₗ (TensorProduct.mk R P (Dual R M ⊗[R] Q))
                              (lTensorHomToHomLTensor (RingHom.id R) M P Q ∘ₗ
                                (↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q))) :
                            (a : P) → Dual R M ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                          f) :
                      (a : Dual R M) → Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                    q :
                  Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                (a : Q) → M →ₗ[R] P ⊗[R] Q)
              m :
            M →ₗ[R] P ⊗[R] Q) :
          (a : M) → P ⊗[R] Q)
        x :
      P ⊗[R] Q)
Tactic: ext f q m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (hypothesis)
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
e : Dual R M ⊗[R] P ⊗[R] Q ≃ₗ[R] (M →ₗ[R] P) ⊗[R] Q :=
  TensorProduct.congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)
⊢ Eq (α := (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
    (↑(rTensorHomEquivHomRTensor R M P Q) : (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
    (rTensorHomToHomRTensor (RingHom.id R) M P Q)
have h : Function.Surjective (α := Dual R M ⊗[R] P ⊗[R] Q) (β := (M →ₗ[R] P) ⊗[R] Q)
  (⇑(↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q) : (a : Dual R M ⊗[R] P ⊗[R] Q) → (M →ₗ[R] P) ⊗[R] Q)
Tactic: have h : Function.Surjective e.toLinearMap := e.surjective
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
e : Dual R M ⊗[R] P ⊗[R] Q ≃ₗ[R] (M →ₗ[R] P) ⊗[R] Q :=
  TensorProduct.congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)
h :
  Function.Surjective (α := Dual R M ⊗[R] P ⊗[R] Q) (β := (M →ₗ[R] P) ⊗[R] Q)
    (⇑(↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q) : (a : Dual R M ⊗[R] P ⊗[R] Q) → (M →ₗ[R] P) ⊗[R] Q)
⊢ Eq (α := (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
    (↑(rTensorHomEquivHomRTensor R M P Q) : (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
    (rTensorHomToHomRTensor (RingHom.id R) M P Q)
have refine : (↑(rTensorHomEquivHomRTensor R M P Q) : (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) ∘ₗ
    (↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q) =
  rTensorHomToHomRTensor (RingHom.id R) M P Q ∘ₗ (↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q)
Tactic: refine (cancel_right h).1 ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
e : Dual R M ⊗[R] P ⊗[R] Q ≃ₗ[R] (M →ₗ[R] P) ⊗[R] Q :=
  TensorProduct.congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)
h :
  Function.Surjective (α := Dual R M ⊗[R] P ⊗[R] Q) (β := (M →ₗ[R] P) ⊗[R] Q)
    (⇑(↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q) : (a : Dual R M ⊗[R] P ⊗[R] Q) → (M →ₗ[R] P) ⊗[R] Q)
⊢ (↑(rTensorHomEquivHomRTensor R M P Q) : (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) ∘ₗ
      (↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q) =
    rTensorHomToHomRTensor (RingHom.id R) M P Q ∘ₗ (↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q)
have H : ∀ (f : Dual R M) (p : P) (q : Q) (m : M),
  Eq (α := P ⊗[R] Q)
    ((((((((compr₂ₛₗ (TensorProduct.mk R (Dual R M) P)
                              (compr₂ₛₗ (TensorProduct.mk R (Dual R M ⊗[R] P) Q)
                                ((↑(rTensorHomEquivHomRTensor R M P Q) : (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) ∘ₗ
                                  (↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q))) :
                            (a : Dual R M) → P →ₗ[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                          f :
                        P →ₗ[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                      (a : P) → Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                    p :
                  Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                (a : Q) → M →ₗ[R] P ⊗[R] Q)
              q :
            M →ₗ[R] P ⊗[R] Q) :
          (a : M) → P ⊗[R] Q)
        m :
      P ⊗[R] Q)
    ((((((((compr₂ₛₗ (TensorProduct.mk R (Dual R M) P)
                              (compr₂ₛₗ (TensorProduct.mk R (Dual R M ⊗[R] P) Q)
                                (rTensorHomToHomRTensor (RingHom.id R) M P Q ∘ₗ
                                  (↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q))) :
                            (a : Dual R M) → P →ₗ[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                          f :
                        P →ₗ[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                      (a : P) → Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                    p :
                  Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                (a : Q) → M →ₗ[R] P ⊗[R] Q)
              q :
            M →ₗ[R] P ⊗[R] Q) :
          (a : M) → P ⊗[R] Q)
        m :
      P ⊗[R] Q)
Tactic: ext f p q m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
x : P ⊗[R] (M →ₗ[R] Q)
⊢ Eq (α := M →ₗ[R] P ⊗[R] Q)
    ((lTensorHomEquivHomLTensor R M P Q : (a : P ⊗[R] (M →ₗ[R] Q)) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
    ((lTensorHomToHomLTensor (RingHom.id R) M P Q : (a : P ⊗[R] (M →ₗ[R] Q)) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
have rw : Eq (α := M →ₗ[R] P ⊗[R] Q)
  (((↑(lTensorHomEquivHomLTensor R M P Q) : P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
        (a : P ⊗[R] (M →ₗ[R] Q)) → M →ₗ[R] P ⊗[R] Q)
      x :
    M →ₗ[R] P ⊗[R] Q)
  ((lTensorHomToHomLTensor (RingHom.id R) M P Q : (a : P ⊗[R] (M →ₗ[R] Q)) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
Tactic: rw [← LinearEquiv.coe_toLinearMap, lTensorHomEquivHomLTensor_toLinearMap]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
x : P ⊗[R] (M →ₗ[R] Q)
rw :
  Eq (α := M →ₗ[R] P ⊗[R] Q)
    (((↑(lTensorHomEquivHomLTensor R M P Q) : P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
          (a : P ⊗[R] (M →ₗ[R] Q)) → M →ₗ[R] P ⊗[R] Q)
        x :
      M →ₗ[R] P ⊗[R] Q)
    ((lTensorHomToHomLTensor (RingHom.id R) M P Q : (a : P ⊗[R] (M →ₗ[R] Q)) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
⊢ Eq (α := M →ₗ[R] P ⊗[R] Q)
    ((lTensorHomEquivHomLTensor R M P Q : (a : P ⊗[R] (M →ₗ[R] Q)) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
    ((lTensorHomToHomLTensor (RingHom.id R) M P Q : (a : P ⊗[R] (M →ₗ[R] Q)) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
have rw₁ : Eq (α := M →ₗ[R] P ⊗[R] Q)
  ((lTensorHomToHomLTensor (RingHom.id R) M P Q : (a : P ⊗[R] (M →ₗ[R] Q)) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
  ((lTensorHomToHomLTensor (RingHom.id R) M P Q : (a : P ⊗[R] (M →ₗ[R] Q)) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
Tactic: rw [← LinearEquiv.coe_toLinearMap, lTensorHomEquivHomLTensor_toLinearMap]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
x : (M →ₗ[R] P) ⊗[R] Q
⊢ Eq (α := M →ₗ[R] P ⊗[R] Q)
    ((rTensorHomEquivHomRTensor R M P Q : (a : (M →ₗ[R] P) ⊗[R] Q) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
    ((rTensorHomToHomRTensor (RingHom.id R) M P Q : (a : (M →ₗ[R] P) ⊗[R] Q) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
have rw : Eq (α := M →ₗ[R] P ⊗[R] Q)
  (((↑(rTensorHomEquivHomRTensor R M P Q) : (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
        (a : (M →ₗ[R] P) ⊗[R] Q) → M →ₗ[R] P ⊗[R] Q)
      x :
    M →ₗ[R] P ⊗[R] Q)
  ((rTensorHomToHomRTensor (RingHom.id R) M P Q : (a : (M →ₗ[R] P) ⊗[R] Q) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
Tactic: rw [← LinearEquiv.coe_toLinearMap, rTensorHomEquivHomRTensor_toLinearMap]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
x : (M →ₗ[R] P) ⊗[R] Q
rw :
  Eq (α := M →ₗ[R] P ⊗[R] Q)
    (((↑(rTensorHomEquivHomRTensor R M P Q) : (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
          (a : (M →ₗ[R] P) ⊗[R] Q) → M →ₗ[R] P ⊗[R] Q)
        x :
      M →ₗ[R] P ⊗[R] Q)
    ((rTensorHomToHomRTensor (RingHom.id R) M P Q : (a : (M →ₗ[R] P) ⊗[R] Q) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
⊢ Eq (α := M →ₗ[R] P ⊗[R] Q)
    ((rTensorHomEquivHomRTensor R M P Q : (a : (M →ₗ[R] P) ⊗[R] Q) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
    ((rTensorHomToHomRTensor (RingHom.id R) M P Q : (a : (M →ₗ[R] P) ⊗[R] Q) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
have rw₁ : Eq (α := M →ₗ[R] P ⊗[R] Q)
  ((rTensorHomToHomRTensor (RingHom.id R) M P Q : (a : (M →ₗ[R] P) ⊗[R] Q) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
  ((rTensorHomToHomRTensor (RingHom.id R) M P Q : (a : (M →ₗ[R] P) ⊗[R] Q) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
Tactic: rw [← LinearEquiv.coe_toLinearMap, rTensorHomEquivHomRTensor_toLinearMap]
-- 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
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : Free R N
inst_12 : Module.Finite R N
⊢ Eq (α := (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    (↑(homTensorHomEquiv R M N P Q) : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    (homTensorHomMap (RingHom.id R) M N P Q)
have H : ∀ (m : M →ₗ[R] P) (n : N →ₗ[R] Q) (x : M) (x_1 : N),
  Eq (α := P ⊗[R] Q)
    ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R M N)
                  ((((compr₂ₛₗ (TensorProduct.mk R (M →ₗ[R] P) (N →ₗ[R] Q))
                              (↑(homTensorHomEquiv R M N P Q) :
                                (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q) :
                            (a : M →ₗ[R] P) → (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q)
                          m :
                        (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q) :
                      (a : N →ₗ[R] Q) → M ⊗[R] N →ₗ[R] P ⊗[R] Q)
                    n) :
                (a : M) → N →ₗ[R] P ⊗[R] Q)
              x :
            N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        x_1 :
      P ⊗[R] Q)
    ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R M N)
                  ((((compr₂ₛₗ (TensorProduct.mk R (M →ₗ[R] P) (N →ₗ[R] Q)) (homTensorHomMap (RingHom.id R) M N P Q) :
                            (a : M →ₗ[R] P) → (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q)
                          m :
                        (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q) :
                      (a : N →ₗ[R] Q) → M ⊗[R] N →ₗ[R] P ⊗[R] Q)
                    n) :
                (a : M) → N →ₗ[R] P ⊗[R] Q)
              x :
            N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        x_1 :
      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
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 : Free R M
inst_10 : Module.Finite R M
inst_11 : Free R N
inst_12 : Module.Finite R N
x : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)
⊢ Eq (α := M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    ((homTensorHomEquiv R M N P Q : (a : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q) x :
      M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    ((homTensorHomMap (RingHom.id R) M N P Q : (a : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q) x :
      M ⊗[R] N →ₗ[R] P ⊗[R] Q)
have rw : Eq (α := M ⊗[R] N →ₗ[R] P ⊗[R] Q)
  (((↑(homTensorHomEquiv R M N P Q) : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q) :
        (a : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q)
      x :
    M ⊗[R] N →ₗ[R] P ⊗[R] Q)
  ((homTensorHomMap (RingHom.id R) M N P Q : (a : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q) x :
    M ⊗[R] N →ₗ[R] P ⊗[R] Q)
Tactic: rw [← LinearEquiv.coe_toLinearMap, homTensorHomEquiv_toLinearMap]
-- 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
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : Free R N
inst_12 : Module.Finite R N
x : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)
rw :
  Eq (α := M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    (((↑(homTensorHomEquiv R M N P Q) : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q) :
          (a : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q)
        x :
      M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    ((homTensorHomMap (RingHom.id R) M N P Q : (a : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q) x :
      M ⊗[R] N →ₗ[R] P ⊗[R] Q)
⊢ Eq (α := M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    ((homTensorHomEquiv R M N P Q : (a : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q) x :
      M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    ((homTensorHomMap (RingHom.id R) M N P Q : (a : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q) x :
      M ⊗[R] N →ₗ[R] P ⊗[R] Q)
have rw₁ : Eq (α := M ⊗[R] N →ₗ[R] P ⊗[R] Q)
  ((homTensorHomMap (RingHom.id R) M N P Q : (a : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q) x :
    M ⊗[R] N →ₗ[R] P ⊗[R] Q)
  ((homTensorHomMap (RingHom.id R) M N P Q : (a : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q) x :
    M ⊗[R] N →ₗ[R] P ⊗[R] Q)
Tactic: rw [← LinearEquiv.coe_toLinearMap, homTensorHomEquiv_toLinearMap]