awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
intro : ∀ (val : Fintype ι), Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
intro₁ :
  ∀ (val : Fintype ι) (i : ι × ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
            Dual R M ⊗[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
            Dual R M ⊗[R] M) :
        R)
intro₂ :
  ∀ (val : Fintype ι) (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) (i, j) :
            Dual R M ⊗[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) (i, j) :
            Dual R M ⊗[R] M) :
        R)
intro₃ :
  ∀ (val : Fintype ι) (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j) :
            M →ₗ[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
intro₄ :
  ∀ (val : Fintype ι) (i j : ι),
    Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single j i 1) : R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
⊢ Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
have intro₅ : ∀ (val : Fintype ι) (i : ι),
  Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single i i 1) : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) i : Dual R M ⊗[R] M) : R)
Tactic: classical
    cases nonempty_fintype ι
    apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)
    rintro ⟨i, j⟩
    simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]
    rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]
    obtain rfl | hij := eq_or_ne i j
    · simp
    rw [Matrix.trace_single_eq_of_ne j i (1 : R) hij.symm]
    simp [hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
intro : ∀ (val : Fintype ι), Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
intro₁ :
  ∀ (val : Fintype ι) (i : ι × ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
            Dual R M ⊗[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
            Dual R M ⊗[R] M) :
        R)
intro₂ :
  ∀ (val : Fintype ι) (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) (i, j) :
            Dual R M ⊗[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) (i, j) :
            Dual R M ⊗[R] M) :
        R)
intro₃ :
  ∀ (val : Fintype ι) (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j) :
            M →ₗ[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
intro₄ :
  ∀ (val : Fintype ι) (i j : ι),
    Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single j i 1) : R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
intro₅ :
  ∀ (val : Fintype ι) (i : ι),
    Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single i i 1) : R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) i : Dual R M ⊗[R] M) : R)
⊢ Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
have intro₆ : ∀ (val : Fintype ι) (i j : ι) (hij : i ≠ j),
  Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single j i 1) : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
Tactic: classical
    cases nonempty_fintype ι
    apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)
    rintro ⟨i, j⟩
    simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]
    rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]
    obtain rfl | hij := eq_or_ne i j
    · simp
    rw [Matrix.trace_single_eq_of_ne j i (1 : R) hij.symm]
    simp [hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
intro : ∀ (val : Fintype ι), Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
intro₁ :
  ∀ (val : Fintype ι) (i : ι × ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
            Dual R M ⊗[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
            Dual R M ⊗[R] M) :
        R)
intro₂ :
  ∀ (val : Fintype ι) (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) (i, j) :
            Dual R M ⊗[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) (i, j) :
            Dual R M ⊗[R] M) :
        R)
intro₃ :
  ∀ (val : Fintype ι) (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j) :
            M →ₗ[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
intro₄ :
  ∀ (val : Fintype ι) (i j : ι),
    Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single j i 1) : R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
intro₅ :
  ∀ (val : Fintype ι) (i : ι),
    Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single i i 1) : R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) i : Dual R M ⊗[R] M) : R)
intro₆ intro₇ :
  ∀ (val : Fintype ι) (i j : ι) (hij : i ≠ j),
    Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single j i 1) : R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
⊢ Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
have intro₈ : ∀ (val : Fintype ι) (i j : ι) (hij : i ≠ j),
  Eq.{u_1 + 1} (α := R) (0 : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
Tactic: classical
    cases nonempty_fintype ι
    apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)
    rintro ⟨i, j⟩
    simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]
    rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]
    obtain rfl | hij := eq_or_ne i j
    · simp
    rw [Matrix.trace_single_eq_of_ne j i (1 : R) hij.symm]
    simp [hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
x : Dual R M ⊗[R] M
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R) ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) x : M →ₗ[R] M) : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) x : R)
have rw : Eq.{u_1 + 1} (α := R) ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R) x : R)
  ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) x : R)
Tactic: rw [← comp_apply, trace_eq_contract]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
x : Dual R M ⊗[R] M
rw :
  Eq.{u_1 + 1} (α := R) ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R) x : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) x : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R) ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) x : M →ₗ[R] M) : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) x : R)
have rw₁ : Eq.{u_1 + 1} (α := R) ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) x : R)
  ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) x : R)
Tactic: rw [← comp_apply, trace_eq_contract]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)
have inl : Subsingleton R → Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
inl : Subsingleton R → Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)
have inr : Nontrivial R → Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
h : Nontrivial R
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)
have inr : ∀ (b : Basis (Free.ChooseBasisIndex R M) R M),
  Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)
Tactic: have b := Module.Free.chooseBasis R M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
h : Nontrivial R
b : Basis (Free.ChooseBasisIndex R M) R M
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)
have inr : Eq.{u_1 + 1} (α := R) (Matrix.trace.{u_2, u_1} (n := Free.ChooseBasisIndex R M) 1)
  (↑(Fintype.card.{u_2} (Free.ChooseBasisIndex R M)) : R)
Tactic: rw [trace_eq_matrix_trace R b, toMatrix_one, finrank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) id : R) ((↑(finrank R M) : R) : R)
have rw : Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)
Tactic: rw [← Module.End.one_eq_id, trace_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
rw : Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) id : R) ((↑(finrank R M) : R) : R)
have rw₁ : Eq.{u_1 + 1} (α := R) (↑(finrank R M) : R) (↑(finrank R M) : R)
Tactic: rw [← Module.End.one_eq_id, trace_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M →ₗ[R] M) R) (trace R (Dual R M) ∘ₗ Dual.transpose)
    (trace R M)
have h : Function.Surjective (α := Dual R M ⊗[R] M) (β := M →ₗ[R] M)
  (⇑(↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M) : (a : Dual R M ⊗[R] M) → M →ₗ[R] M)
Tactic: have h : Function.Surjective e.toLinearMap := e.surjective
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h :
  Function.Surjective (α := Dual R M ⊗[R] M) (β := M →ₗ[R] M)
    (⇑(↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M) : (a : Dual R M ⊗[R] M) → M →ₗ[R] M)
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M →ₗ[R] M) R) (trace R (Dual R M) ∘ₗ Dual.transpose)
    (trace R M)
have refine : (trace R (Dual R M) ∘ₗ Dual.transpose) ∘ₗ (↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M) =
  trace R M ∘ₗ (↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M)
Tactic: refine (cancel_right h).1 ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h :
  Function.Surjective (α := Dual R M ⊗[R] M) (β := M →ₗ[R] M)
    (⇑(↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M) : (a : Dual R M ⊗[R] M) → M →ₗ[R] M)
⊢ (trace R (Dual R M) ∘ₗ Dual.transpose) ∘ₗ (↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M) =
    trace R M ∘ₗ (↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M)
have a : ∀ (f : Dual R M) (m : M),
  Eq.{u_1 + 1} (α := R)
    (((((AlgebraTensorModule.curry ((trace R (Dual R M) ∘ₗ Dual.transpose) ∘ₗ (↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M)) :
                  Dual R M →ₗ[R] M →ₗ[R] R) :
                (a : Dual R M) → M →ₗ[R] R)
              f :
            M →ₗ[R] R) :
          (a : M) → R)
        m :
      R)
    (((((AlgebraTensorModule.curry (trace R M ∘ₗ (↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M)) : Dual R M →ₗ[R] M →ₗ[R] R) :
                (a : Dual R M) → M →ₗ[R] R)
              f :
            M →ₗ[R] R) :
          (a : M) → R)
        m :
      R)
Tactic: ext f m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
e : (Dual R M ⊗[R] M × Dual R N ⊗[R] N) ≃ₗ[R] Prod.{u_2, u_3} (M →ₗ[R] M) (N →ₗ[R] N) :=
  LinearEquiv.prodCongr (dualTensorHomEquiv R M M) (dualTensorHomEquiv R N N)
⊢ Eq (α := Prod.{u_2, u_3} (M →ₗ[R] M) (N →ₗ[R] N) →ₗ[R] R) (trace R (M × N) ∘ₗ prodMapLinear R M N M N R)
    (coprod id id ∘ₗ prodMap (trace R M) (trace R N))
have h : Function.Surjective (α := Dual R M ⊗[R] M × Dual R N ⊗[R] N) (β := Prod.{u_2, u_3} (M →ₗ[R] M) (N →ₗ[R] N))
  (⇑(↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N)) :
    (a : Dual R M ⊗[R] M × Dual R N ⊗[R] N) → (M →ₗ[R] M) × (N →ₗ[R] N))
Tactic: have h : Function.Surjective e.toLinearMap := e.surjective
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
e : (Dual R M ⊗[R] M × Dual R N ⊗[R] N) ≃ₗ[R] Prod.{u_2, u_3} (M →ₗ[R] M) (N →ₗ[R] N) :=
  LinearEquiv.prodCongr (dualTensorHomEquiv R M M) (dualTensorHomEquiv R N N)
h :
  Function.Surjective (α := Dual R M ⊗[R] M × Dual R N ⊗[R] N) (β := Prod.{u_2, u_3} (M →ₗ[R] M) (N →ₗ[R] N))
    (⇑(↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N)) :
      (a : Dual R M ⊗[R] M × Dual R N ⊗[R] N) → (M →ₗ[R] M) × (N →ₗ[R] N))
⊢ Eq (α := Prod.{u_2, u_3} (M →ₗ[R] M) (N →ₗ[R] N) →ₗ[R] R) (trace R (M × N) ∘ₗ prodMapLinear R M N M N R)
    (coprod id id ∘ₗ prodMap (trace R M) (trace R N))
have refine : (trace R (M × N) ∘ₗ prodMapLinear R M N M N R) ∘ₗ
    (↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N)) =
  (coprod id id ∘ₗ prodMap (trace R M) (trace R N)) ∘ₗ
    (↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N))
Tactic: refine (cancel_right h).1 ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
e : (Dual R M ⊗[R] M × Dual R N ⊗[R] N) ≃ₗ[R] Prod.{u_2, u_3} (M →ₗ[R] M) (N →ₗ[R] N) :=
  LinearEquiv.prodCongr (dualTensorHomEquiv R M M) (dualTensorHomEquiv R N N)
h :
  Function.Surjective (α := Dual R M ⊗[R] M × Dual R N ⊗[R] N) (β := Prod.{u_2, u_3} (M →ₗ[R] M) (N →ₗ[R] N))
    (⇑(↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N)) :
      (a : Dual R M ⊗[R] M × Dual R N ⊗[R] N) → (M →ₗ[R] M) × (N →ₗ[R] N))
⊢ (trace R (M × N) ∘ₗ prodMapLinear R M N M N R) ∘ₗ
      (↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N)) =
    (coprod id id ∘ₗ prodMap (trace R M) (trace R N)) ∘ₗ
      (↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N))
have hl : ∀ (x : Dual R M) (x_1 : M),
  Eq.{u_1 + 1} (α := R)
    (((((AlgebraTensorModule.curry
                    (((trace R (M × N) ∘ₗ prodMapLinear R M N M N R) ∘ₗ
                        (↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N))) ∘ₗ
                      inl R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)) :
                  Dual R M →ₗ[R] M →ₗ[R] R) :
                (a : Dual R M) → M →ₗ[R] R)
              x :
            M →ₗ[R] R) :
          (a : M) → R)
        x_1 :
      R)
    (((((AlgebraTensorModule.curry
                    (((coprod id id ∘ₗ prodMap (trace R M) (trace R N)) ∘ₗ
                        (↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N))) ∘ₗ
                      inl R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)) :
                  Dual R M →ₗ[R] M →ₗ[R] R) :
                (a : Dual R M) → M →ₗ[R] R)
              x :
            M →ₗ[R] R) :
          (a : M) → R)
        x_1 :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
e : (Dual R M ⊗[R] M × Dual R N ⊗[R] N) ≃ₗ[R] Prod.{u_2, u_3} (M →ₗ[R] M) (N →ₗ[R] N) :=
  LinearEquiv.prodCongr (dualTensorHomEquiv R M M) (dualTensorHomEquiv R N N)
h :
  Function.Surjective (α := Dual R M ⊗[R] M × Dual R N ⊗[R] N) (β := Prod.{u_2, u_3} (M →ₗ[R] M) (N →ₗ[R] N))
    (⇑(↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N)) :
      (a : Dual R M ⊗[R] M × Dual R N ⊗[R] N) → (M →ₗ[R] M) × (N →ₗ[R] N))
hl :
  ∀ (x : Dual R M) (x_1 : M),
    Eq.{u_1 + 1} (α := R)
      (((((AlgebraTensorModule.curry
                      (((trace R (M × N) ∘ₗ prodMapLinear R M N M N R) ∘ₗ
                          (↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N))) ∘ₗ
                        inl R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)) :
                    Dual R M →ₗ[R] M →ₗ[R] R) :
                  (a : Dual R M) → M →ₗ[R] R)
                x :
              M →ₗ[R] R) :
            (a : M) → R)
          x_1 :
        R)
      (((((AlgebraTensorModule.curry
                      (((coprod id id ∘ₗ prodMap (trace R M) (trace R N)) ∘ₗ
                          (↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N))) ∘ₗ
                        inl R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)) :
                    Dual R M →ₗ[R] M →ₗ[R] R) :
                  (a : Dual R M) → M →ₗ[R] R)
                x :
              M →ₗ[R] R) :
            (a : M) → R)
          x_1 :
        R)
⊢ (trace R (M × N) ∘ₗ prodMapLinear R M N M N R) ∘ₗ
      (↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N)) =
    (coprod id id ∘ₗ prodMap (trace R M) (trace R N)) ∘ₗ
      (↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N))
have hr : ∀ (x : Dual R N) (x_1 : N),
  Eq.{u_1 + 1} (α := R)
    (((((AlgebraTensorModule.curry
                    (((trace R (M × N) ∘ₗ prodMapLinear R M N M N R) ∘ₗ
                        (↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N))) ∘ₗ
                      inr R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)) :
                  Dual R N →ₗ[R] N →ₗ[R] R) :
                (a : Dual R N) → N →ₗ[R] R)
              x :
            N →ₗ[R] R) :
          (a : N) → R)
        x_1 :
      R)
    (((((AlgebraTensorModule.curry
                    (((coprod id id ∘ₗ prodMap (trace R M) (trace R N)) ∘ₗ
                        (↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N))) ∘ₗ
                      inr R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)) :
                  Dual R N →ₗ[R] N →ₗ[R] R) :
                (a : Dual R N) → N →ₗ[R] R)
              x :
            N →ₗ[R] R) :
          (a : N) → R)
        x_1 :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
⊢ (trace R (M × N) : (a : M × N →ₗ[R] M × N) → R) (f.prodMap g) =
    HAdd.hAdd (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R) ((trace R N : (a : N →ₗ[R] N) → R) g : R)
have h : Eq.{u_1 + 1} (α := R) ((trace R (M × N) ∘ₗ prodMapLinear R M N M N R : (a : (M →ₗ[R] M) × (N →ₗ[R] N)) → R) (f, g) : R)
  ((coprod id id ∘ₗ prodMap (trace R M) (trace R N) : (a : (M →ₗ[R] M) × (N →ₗ[R] N)) → R) (f, g) : R)
Tactic: have h := LinearMap.ext_iff.1 (trace_prodMap R M N) (f, g)