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
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
⊢ Eq (α := (M →ₗ[R] M) →ₗ[R] LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (N →ₗ[R] N) R)
    (compr₂ (mapBilinear (RingHom.id R) M N M N) (trace R (M ⊗[R] N))) (compl₁₂ (lsmul R R) (trace R M) (trace R N))
have Surjective : Eq (α := Dual R M ⊗[R] M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R)
  (compl₁₂ (compr₂ (mapBilinear (RingHom.id R) M N M N) (trace R (M ⊗[R] N))) (dualTensorHom R M M)
    (dualTensorHom R N N))
  (compl₁₂ (compl₁₂ (lsmul R R) (trace R M) (trace R N)) (dualTensorHom R M M) (dualTensorHom R N N))
Tactic: apply
    (compl₁₂_inj (show Surjective (dualTensorHom R M M) from (dualTensorHomEquiv R M M).surjective)
        (show Surjective (dualTensorHom R N N) from (dualTensorHomEquiv R N N).surjective)).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
⊢ Eq (α := Dual R M ⊗[R] M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R)
    (compl₁₂ (compr₂ (mapBilinear (RingHom.id R) M N M N) (trace R (M ⊗[R] N))) (dualTensorHom R M M)
      (dualTensorHom R N N))
    (compl₁₂ (compl₁₂ (lsmul R R) (trace R M) (trace R N)) (dualTensorHom R M M) (dualTensorHom R N N))
have a : ∀ (f : Dual R M) (m : M) (g : Dual R N) (n : N),
  Eq.{u_1 + 1} (α := R)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (compl₁₂ (compr₂ (mapBilinear (RingHom.id R) M N M N) (trace R (M ⊗[R] N)))
                                    (dualTensorHom R M M) (dualTensorHom R N N)) :
                                Dual R M →ₗ[R] M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R) :
                              (a : Dual R M) → M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R)
                            f :
                          M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R) :
                        (a : M) → Dual R N ⊗[R] N →ₗ[R] R)
                      m) :
                  Dual R N →ₗ[R] N →ₗ[R] R) :
                (a : Dual R N) → N →ₗ[R] R)
              g :
            N →ₗ[R] R) :
          (a : N) → R)
        n :
      R)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (compl₁₂ (compl₁₂ (lsmul R R) (trace R M) (trace R N)) (dualTensorHom R M M)
                                    (dualTensorHom R N N)) :
                                Dual R M →ₗ[R] M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R) :
                              (a : Dual R M) → M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R)
                            f :
                          M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R) :
                        (a : M) → Dual R N ⊗[R] N →ₗ[R] R)
                      m) :
                  Dual R N →ₗ[R] N →ₗ[R] R) :
                (a : Dual R N) → N →ₗ[R] R)
              g :
            N →ₗ[R] R) :
          (a : N) → R)
        n :
      R)
Tactic: ext f m g n
-- 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
⊢ Eq (α := (N →ₗ[R] M) →ₗ[R] (M →ₗ[R] N) →ₗ[R] R) (compr₂ (llcomp R M N M) (trace R M))
    (compr₂ (flip (llcomp R N M N)) (trace R N))
have Surjective : Eq (α := Dual R N ⊗[R] M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R)
  (compl₁₂ (compr₂ (llcomp R M N M) (trace R M)) (dualTensorHom R N M) (dualTensorHom R M N))
  (compl₁₂ (compr₂ (flip (llcomp R N M N)) (trace R N)) (dualTensorHom R N M) (dualTensorHom R M N))
Tactic: apply
    (compl₁₂_inj (show Surjective (dualTensorHom R N M) from (dualTensorHomEquiv R N M).surjective)
        (show Surjective (dualTensorHom R M N) from (dualTensorHomEquiv R M N).surjective)).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
⊢ Eq (α := Dual R N ⊗[R] M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R)
    (compl₁₂ (compr₂ (llcomp R M N M) (trace R M)) (dualTensorHom R N M) (dualTensorHom R M N))
    (compl₁₂ (compr₂ (flip (llcomp R N M N)) (trace R N)) (dualTensorHom R N M) (dualTensorHom R M N))
have a : ∀ (g : Dual R N) (m : M) (f : Dual R M) (n : N),
  Eq.{u_1 + 1} (α := R)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (compl₁₂ (compr₂ (llcomp R M N M) (trace R M)) (dualTensorHom R N M)
                                    (dualTensorHom R M N)) :
                                Dual R N →ₗ[R] M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R) :
                              (a : Dual R N) → M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R)
                            g :
                          M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R) :
                        (a : M) → Dual R M ⊗[R] N →ₗ[R] R)
                      m) :
                  Dual R M →ₗ[R] N →ₗ[R] R) :
                (a : Dual R M) → N →ₗ[R] R)
              f :
            N →ₗ[R] R) :
          (a : N) → R)
        n :
      R)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (compl₁₂ (compr₂ (flip (llcomp R N M N)) (trace R N)) (dualTensorHom R N M)
                                    (dualTensorHom R M N)) :
                                Dual R N →ₗ[R] M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R) :
                              (a : Dual R N) → M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R)
                            g :
                          M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R) :
                        (a : M) → Dual R M ⊗[R] N →ₗ[R] R)
                      m) :
                  Dual R M →ₗ[R] N →ₗ[R] R) :
                (a : Dual R M) → N →ₗ[R] R)
              f :
            N →ₗ[R] R) :
          (a : N) → R)
        n :
      R)
Tactic: ext g m f n
-- 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
f : M →ₗ[R] M
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R (Dual R M) : (a : Dual R M →ₗ[R] Dual R M) → R)
        ((Dual.transpose : (a : M →ₗ[R] M) → Dual R M →ₗ[R] Dual R M) f : Dual R M →ₗ[R] Dual R M) :
      R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have rw : Eq.{u_1 + 1} (α := R) ((trace R (Dual R M) ∘ₗ Dual.transpose : (a : M →ₗ[R] M) → R) f : R)
  ((trace R M : (a : M →ₗ[R] M) → R) f : R)
Tactic: rw [← comp_apply, trace_transpose]
-- 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
f : M →ₗ[R] M
rw :
  Eq.{u_1 + 1} (α := R) ((trace R (Dual R M) ∘ₗ Dual.transpose : (a : M →ₗ[R] M) → R) f : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R (Dual R M) : (a : Dual R M →ₗ[R] Dual R M) → R)
        ((Dual.transpose : (a : M →ₗ[R] M) → Dual R M →ₗ[R] Dual R M) f : Dual R M →ₗ[R] Dual R M) :
      R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have rw₁ : Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
Tactic: rw [← comp_apply, trace_transpose]
-- 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 ⊗[R] N) : (a : M ⊗[R] N →ₗ[R] M ⊗[R] N) → R) (map f g) =
    HMul.hMul (α := 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)
  ((((compr₂ (mapBilinear (RingHom.id R) M N M N) (trace R (M ⊗[R] N)) : (a : M →ₗ[R] M) → (N →ₗ[R] N) →ₗ[R] R) f :
          LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (N →ₗ[R] N) R) :
        (a : N →ₗ[R] N) → R)
      g :
    R)
  ((((compl₁₂ (lsmul R R) (trace R M) (trace R N) : (a : M →ₗ[R] M) → (N →ₗ[R] N) →ₗ[R] R) f :
          LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (N →ₗ[R] N) R) :
        (a : N →ₗ[R] N) → R)
      g :
    R)
Tactic: have h := LinearMap.ext_iff.1 (LinearMap.ext_iff.1 (trace_tensorProduct R M N) f) g
-- 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] N
g : N →ₗ[R] M
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R)
    ((trace R N : (a : N →ₗ[R] N) → R) (f ∘ₗ g) : R)
have h : Eq.{u_1 + 1} (α := R)
  ((((compr₂ (llcomp R M N M) (trace R M) : (a : N →ₗ[R] M) → (M →ₗ[R] N) →ₗ[R] R) g : (M →ₗ[R] N) →ₗ[R] R) :
        (a : M →ₗ[R] N) → R)
      f :
    R)
  ((((compr₂ (flip (llcomp R N M N)) (trace R N) : (a : N →ₗ[R] M) → (M →ₗ[R] N) →ₗ[R] R) g : (M →ₗ[R] N) →ₗ[R] R) :
        (a : M →ₗ[R] N) → R)
      f :
    R)
Tactic: have h := LinearMap.ext_iff.1 (LinearMap.ext_iff.1 (trace_comp_comm R M N) g) f
-- 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
f : M →ₗ[R] R
x : M
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f.smulRight x) : R) ((f : (a : M) → R) x : R)
have rw : Eq.{u_1 + 1} (α := R)
  (Matrix.trace.{u_2, u_1} (n := Free.ChooseBasisIndex R M)
      ((toMatrix (Free.chooseBasis R M) (Free.chooseBasis R M) :
          (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R)
        (f.smulRight
          (∑ i : Free.ChooseBasisIndex R M,
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
              ((((Basis.repr (Free.chooseBasis R M) : (a : M) → Free.ChooseBasisIndex R M →₀ R) x :
                      Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
                    (a : Free.ChooseBasisIndex R M) → R)
                  i :
                R)
              ((Free.chooseBasis R M : (a : Free.ChooseBasisIndex R M) → M) i : M)))) :
    R)
  ((f : (a : M) → R)
      (∑ i : Free.ChooseBasisIndex R M,
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
          ((((Basis.repr (Free.chooseBasis R M) : (a : M) → Free.ChooseBasisIndex R M →₀ R) x :
                  Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
                (a : Free.ChooseBasisIndex R M) → R)
              i :
            R)
          ((Free.chooseBasis R M : (a : Free.ChooseBasisIndex R M) → M) i : M)) :
    R)
Tactic: rw [trace_eq_matrix_trace _ (Free.chooseBasis R M), ← (Free.chooseBasis R M).sum_repr x]
-- 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
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : Free R N
inst_8 : Module.Finite R N
inst_9 : Free R P
inst_10 : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
⊢ Eq.{u_1 + 1} (α := R) ((trace R P : (a : P →ₗ[R] P) → R) (g ∘ₗ f ∘ₗ h) : R)
    ((trace R N : (a : N →ₗ[R] N) → R) (f ∘ₗ h ∘ₗ g) : R)
have rw : Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((f ∘ₗ h) ∘ₗ g) : R)
  ((trace R N : (a : N →ₗ[R] N) → R) (f ∘ₗ h ∘ₗ g) : R)
Tactic: rw [trace_comp_comm', comp_assoc]
-- 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
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : Free R N
inst_8 : Module.Finite R N
inst_9 : Free R P
inst_10 : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
rw :
  Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((f ∘ₗ h) ∘ₗ g) : R)
    ((trace R N : (a : N →ₗ[R] N) → R) (f ∘ₗ h ∘ₗ g) : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R P : (a : P →ₗ[R] P) → R) (g ∘ₗ f ∘ₗ h) : R)
    ((trace R N : (a : N →ₗ[R] N) → R) (f ∘ₗ h ∘ₗ g) : R)
have rw₁ : Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) (f ∘ₗ h ∘ₗ g) : R)
  ((trace R N : (a : N →ₗ[R] N) → R) (f ∘ₗ h ∘ₗ g) : R)
Tactic: rw [trace_comp_comm', comp_assoc]
-- 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
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : Free R M
inst_8 : Module.Finite R M
inst_9 : Free R P
inst_10 : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
⊢ Eq.{u_1 + 1} (α := R) ((trace R P : (a : P →ₗ[R] P) → R) ((g ∘ₗ f) ∘ₗ h) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) ((h ∘ₗ g) ∘ₗ f) : R)
have rw : Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (h ∘ₗ g ∘ₗ f) : R)
  ((trace R M : (a : M →ₗ[R] M) → R) ((h ∘ₗ g) ∘ₗ f) : R)
Tactic: rw [trace_comp_comm', ← comp_assoc]
-- 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
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : Free R M
inst_8 : Module.Finite R M
inst_9 : Free R P
inst_10 : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
rw :
  Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (h ∘ₗ g ∘ₗ f) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) ((h ∘ₗ g) ∘ₗ f) : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R P : (a : P →ₗ[R] P) → R) ((g ∘ₗ f) ∘ₗ h) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) ((h ∘ₗ g) ∘ₗ f) : R)
have rw₁ : Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) ((h ∘ₗ g) ∘ₗ f) : R)
  ((trace R M : (a : M →ₗ[R] M) → R) ((h ∘ₗ g) ∘ₗ f) : R)
Tactic: rw [trace_comp_comm', ← comp_assoc]
-- 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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
⊢ Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have pos : ∀ (hM : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)),
  Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
Tactic: by_cases hM : ∃ s : Finset M, Nonempty (Basis s 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
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
pos :
  ∀ (hM : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)),
    Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) f : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have neg : ∀ (hM : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)),
  Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
Tactic: by_cases hM : ∃ s : Finset M, Nonempty (Basis s 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
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)
⊢ Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have pos : ∀ (s : Finset M) (b : Basis (↥s) R M),
  Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
Tactic: obtain ⟨s, ⟨b⟩⟩ := hM
Cleared hypotheses: hM
-- 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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
⊢ Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have this : Module.Finite R M
Tactic: haveI := Module.Finite.of_basis b
-- 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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this : Module.Finite R M
⊢ Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have this₁ : Free R M
Tactic: haveI := (Module.free_def R M).mpr ⟨_, ⟨b⟩⟩
-- 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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this_1 : Module.Finite R M
this : Free R M
⊢ Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have this₁ : Module.Finite R N
Tactic: haveI := Module.Finite.of_basis (b.map e)
-- 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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this_1 : Module.Finite R M
this_2 : Free R M
this : Module.Finite R N
⊢ Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have this₁ : Free R N
Tactic: haveI := (Module.free_def R N).mpr ⟨_, ⟨(b.map e).reindex (e.toEquiv.image _)⟩⟩
-- 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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this_1 : Module.Finite R M
this_2 : Free R M
this_3 : Module.Finite R N
this : Free R N
⊢ Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have pos : Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) (((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) : R)
  ((trace R M : (a : M →ₗ[R] M) → R) f : R)
Tactic: rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe,
      LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, id_comp]
-- 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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this_1 : Module.Finite R M
this_2 : Free R M
this_3 : Module.Finite R N
this : Free R N
pos :
  Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) (((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have pos₁ : Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) ((↑e.symm : N →ₗ[R] M) ∘ₗ (↑e : M →ₗ[R] N) ∘ₗ f) : R)
  ((trace R M : (a : M →ₗ[R] M) → R) f : R)
Tactic: rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe,
      LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, id_comp]
-- 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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this_1 : Module.Finite R M
this_2 : Free R M
this_3 : Module.Finite R N
this : Free R N
pos :
  Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) (((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
pos₁ :
  Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) ((↑e.symm : N →ₗ[R] M) ∘ₗ (↑e : M →ₗ[R] N) ∘ₗ f) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have pos₂ : Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (((↑e.symm : N →ₗ[R] M) ∘ₗ (↑e : M →ₗ[R] N)) ∘ₗ f) : R)
  ((trace R M : (a : M →ₗ[R] M) → R) f : R)
Tactic: rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe,
      LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, id_comp]
-- 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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this_1 : Module.Finite R M
this_2 : Free R M
this_3 : Module.Finite R N
this : Free R N
pos :
  Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) (((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
pos₁ :
  Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) ((↑e.symm : N →ₗ[R] M) ∘ₗ (↑e : M →ₗ[R] N) ∘ₗ f) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
pos₂ :
  Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (((↑e.symm : N →ₗ[R] M) ∘ₗ (↑e : M →ₗ[R] N)) ∘ₗ f) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have pos₃ : Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) ((↑(e ≪≫ₗ e.symm) : M →ₗ[R] M) ∘ₗ f) : R)
  ((trace R M : (a : M →ₗ[R] M) → R) f : R)
Tactic: rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe,
      LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, id_comp]